Formal verification method for combinatorial circuits at high level design
説明
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.
収録刊行物
-
- Proceedings of the ASP-DAC '99 Asia and South Pacific Design Automation Conference 1999 (Cat. No.99EX198)
-
Proceedings of the ASP-DAC '99 Asia and South Pacific Design Automation Conference 1999 (Cat. No.99EX198) 319-322 vol.1, 1999-01-01
IEEE