The formal verification is able to check whether the implementation of a circuit design is functionally equivalent to an earlier version described at the same level of abstraction, it can show the correctness of a circuit design. A new circuit verification method based on cone-oriented circuit partitioning and decision diagrams is presented in this paper. First of all, the structure level of every signal line in a circuit is computed. Secondly, the circuit is partitioned into a lot of cone structures. The multiple-valued decision diagram corresponding to every cone structure is generated. The verification procedure is to compare the equivalence of the multiple-valued decision diagrams of two types of cone structures. Experimental results on a lot of benchmark circuits show the method presented in this paper can effectively perform the equivalence checking of circuits.
Formal verification of digital circuits using symbolic ternary system models
