Combinational Verification

The combinational verification capabilities of MVSIS include a BDD-based and a SAT-based equivalence checking command.

bdd-based verification

The first command represents a traditional approach, which constructs and compares the BDDs for the primary outputs of the two circuits to be verified. This command is applicable to non-deterministic multi-valued networks. In the case of non-deterministic networks, the containment of SS-behaviors of the networks is checked [3]. The BDD-based verifier can also return an error trace, which pin-points the mismatch in the functionality of the two circuits. The error trace is a minterm in terms of (multi-valued) primary input variables, for which one pair of the primary outputs of the two circuits produces different values. This verification option is only applicable to the circuits, for which BDDs can be efficiently constructed.

fraig-based verification

The second verification option is based on the representation of Boolean functions in terms of And-Inv Graphs (AIGs) [1]. A semi-canonical form AIGs, called Functionally Reduced AIGs [2], is used to prove equivalence of primary outputs in a way similar to the use of BDDs. The FRAIGs for the primary outputs of the two circuits are constructed and compared. The functional reduction of FRAIGs guarantees that the primary outputs are equal if and only if they are represented by the same FRAIG node. This command is currently applicable only to the binary circuits, but it is substantially more robust than the BDD-based one. It has been successfully used to verify industrial circuits with hundreds of thousands of gates. The FRAIG-based verification command can also be applied to the problem of bounded sequential verification, when a sequential circuit is unrolled for k time-frames and verified combinationally for all pairs of primary outputs of each time frame. This option may help quickly find bugs with short error-traces for large circuits after sequential optimization.

software

Commands "verify" (BDD-based) and "fraig_verify" (SAT-based) in the latest version of MVSIS.

Download Software

publications

1. A. Kuehlmann, V. Paruthi, F. Krohm, M. K. Ganai, "Robust Boolean Reasoning for Equivalence Checking and Functional Property Verification," IEEE TCAD, Vol. 21(12), Dec 2002, pp. 1377-1394.
2. A. Mishchenko, S.Chatterjee, R. Jiang, R. Brayton, "FRAIGS: A Unifying Representation for Logic Synthesis and Verification," ERL Technical Report, EECS Dept., UC Berkeley, March 2005. (PDF)
3. A. Mishchenko, R. Brayton, "A Theory of Non-Deterministic Networks," Accepted to IEEE TCAD, 2005. (PDF)