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 desing. The specification is described by both integer and Boolean variables for input and output variable,s and the implementation is described by only Boolean variables. Our verification method judges the equivalence between the specification and the implementation by deciding the tructh of presburger sentence. We show experimental results on some benchmarks, such as 4bit ALU, multiplier, by our method.