Verification of Hardware Designs: A Case Study
Nan Zhang, Zhenhua Duan · 2011
As size and complexity have increased, formal verification of hardware designs is a challenge to us. This paper presents a case study for verification of a full adder design using the axiom system of Propositional Projection Temporal Logic (PPTL). The paper focuses on the functional verification of the adder. To this end, the syntax, semantics and axiom system for PPTL are briefly introduced. Further, functions and architectures of full adders are presented respectively. Finally, the correctness of the full adder is verified.