DocumentCode
2741840
Title
Formal verification method for combinatorial circuits at high level design
Author
Kitamichi, Junji ; Kageyama, Hiroyuki ; Funabiki, Nobuo
Author_Institution
Graduate Sch. of Eng. Sci., Osaka Univ., Japan
fYear
1999
fDate
18-21 Jan 1999
Firstpage
319
Abstract
In this paper, we propose a formal verification method for combinatorial circuits at high level design. The specification is described by both integer and Boolean variables for input and output variables, and the implementation is described by only Boolean variables. Our verification method judges the equivalence between the specification and the implementation by deciding the truth of the Presburger sentence. We show experimental results on some benchmarks, such as a 4 bit ALU and multiplier, by our method
Keywords
Boolean functions; circuit CAD; combinational circuits; formal verification; high level synthesis; Boolean variables; Presburger sentence; combinatorial circuits; formal verification method; high level design; implementation; input variables; integer variables; output variables; specification; Circuit synthesis; Design engineering; Formal verification; Informatics; Logic functions; Very large scale integration;
fLanguage
English
Publisher
ieee
Conference_Titel
Design Automation Conference, 1999. Proceedings of the ASP-DAC '99. Asia and South Pacific
Conference_Location
Wanchai
Print_ISBN
0-7803-5012-X
Type
conf
DOI
10.1109/ASPDAC.1999.760023
Filename
760023
Link To Document