For formal verification of large-scale digital circuits, a method using satisfiability checking of logic with equality and uninterpreted functions has been proposed. This logic, however, does not consider specific properties of functions or predicates at all, e.g. associative property of addition. In order to ease this problem, we introduce "equivalence constraint" that is a set of formulas representing the properties of functions and predicates, and check the satisfiability of formulas under the constraint. In this report, we show an algorithm for checking satisfiability with equivalence constraint and also experimental results.

This letter handles symbolic simulation for high-level hardware design descriptions including uninterpreted functions. Two new heuristics are introduced, which are named "symbolic function table" and "synchronization". In the experiment, the equivalence of a hardware/software codesign was checked up to a given finite number of cycles, which is composed of a behavioral design, that is, a small DSP program written in C, and its register-transfer-level implementation, a VLIW architecture with an assembly program. Our symbolic simulator succeeded in checking the equivalence of the two descriptions which were not tractable without the heuristics.

This paper deals with formal verification of high-level designs, in particular, symbolic comparison of register-transfer-level descriptions and behavioral descriptions. We use state machines extended by quantifier-free first-order logic with equality, as models of those descriptions. We cannot adopt the classical notion of equivalence for state machines, because the signals in the corresponding outputs of such two descriptions do not change in the same way. This paper defines a new notion of consistency based on signal-transitions of the corresponding outputs, and proposes an algorithm for checking consistency of those descriptions, up to a limited number of steps from initial states. As an example of high-level designs, we take a simple hardware/software codesign. A C program for digital signal processing called PARCOR filter was compared with its corresponding design given as a register-transfer-level description, which is composed of a VLIW architecture and assembly code. Since this example terminates within approximately 4500 steps, symbolic exploration of a finite number of steps is sufficient to verify the descriptions. Our prototype verifier succeeded in the verification of this example in 31 minutes.