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
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;
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
DOI :
10.1109/ASPDAC.1999.760023
