DocumentCode
2300898
Title
Verification of Hardware Designs: A Case Study
Author
Zhang, Nan ; Duan, Zhenhua
Author_Institution
ISN Lab., Xidian Univ., Xi´´an, China
fYear
2011
fDate
23-25 May 2011
Firstpage
198
Lastpage
203
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;
fLanguage
English
Publisher
ieee
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
Type
conf
DOI
10.1109/CNSI.2011.77
Filename
5954308
Link To Document