Home MultiValued Logic Synthesis Boolean Technology Mapping Berkeley Language and Automata Manipulation Combinational Verification PhysicallyAware Synthesis Download Software People / Contact 
The combinational verification capabilities of MVSIS include a BDDbased and a SATbased equivalence checking command. bddbased verificationThe 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 nondeterministic multivalued networks. In the case of nondeterministic networks, the containment of SSbehaviors of the networks is checked [3]. The BDDbased verifier can also return an error trace, which pinpoints the mismatch in the functionality of the two circuits. The error trace is a minterm in terms of (multivalued) 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. fraigbased verificationThe second verification option is based on the representation of Boolean functions in terms of AndInv Graphs (AIGs) [1]. A semicanonical 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 BDDbased one. It has been successfully used to verify industrial circuits with hundreds of thousands of gates. The FRAIGbased verification command can also be applied to the problem of bounded sequential verification, when a sequential circuit is unrolled for k timeframes and verified combinationally for all pairs of primary outputs of each time frame. This option may help quickly find bugs with short errortraces for large circuits after sequential optimization. softwareCommands "verify" (BDDbased) and "fraig_verify" (SATbased) in the latest version of MVSIS. publications

Contact 
©20022018 U.C. Regents 