| A designed system must be tested in order to examine whether it contain error or bugs. Verification is a way to examine the design before it is fabricated to avoid wasting time and costs. The traditional way to verify a system is using exhaustive method, creating a full list of all possible inputs and outputs combinations and verify whether they are completely correct. The modern approach is using the formal method, which uses exhaustive algorithm and mathematical proving. In this thesis, a design of 8-bit Arithmetic and Logic Unit (ALU) is verified using the formal method. The designed ALU operations are AND, OR, XOR, and NOT for logical operation, addition, subtraction, and multiplication for arithmetic operation, and bit shifting operation. The verified design is simulated in ModelSim software and implemented on Spartan-3E FPGA board. The simulation and implementation, show that the designed ALU fulfills the specification and proves that formal method is able to verify the design efficiently. |