Title :
Verification of Hardware Designs: A Case Study
Author :
Zhang, Nan ; Duan, Zhenhua
Author_Institution :
ISN Lab., Xidian Univ., Xi´´an, China
Abstract :
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.
Keywords :
adders; formal verification; logic design; temporal logic; axiom; formal verification; full adder design; functional verification; hardware design verification; propositional projection temporal logic; syntax; system semantics; Adders; Computer bugs; Hardware; Logic gates; Production; Semantics; Syntactics; Full Adder; Hardware; Temporal Logic; Verification;
Conference_Titel :
Computers, Networks, Systems and Industrial Engineering (CNSI), 2011 First ACIS/JNU International Conference on
Conference_Location :
Jeju Island
Print_ISBN :
978-1-4577-0180-1
DOI :
10.1109/CNSI.2011.77
