Study On The Formal Verification Methods Of Combinatorial Circuit

One of the critical problems in designing a very large scale digital circuit is how to check the correctness of the design. However, the complexity of the design verification is exponential with the increase of the chip scale. The traditional verification method can't eliminate all the design error. Therefore, many people tum to various formal verification methods to grantee the correctness of the design under any inputs.Formal verification is one of the key technologies in EDA, and it becomes more and more important in circuit design. In the first part of this paper, the development of EDA is described and the significance of the topic is narrated. Then the conception of formal verification and the technique of formal verification, such as equivalence checking, model checking and theorem proving are briefly introduced. The main content is the methods of formal verification? which are modified.Equivalence checking is an important method of formal verification. However, only the low level information is considered in general verification. In this paper, the high level specification information is considered in the equivalence checking of combinational circuit. Polynomial is an effective method in representing circuit. While for circuit containing branches, the order is too high. An effective method of polynomial representation of combinational circuit with branches is given. If we consider don't care items, the process of computing the order of the polynomial representation is reduced greatly. Then, a method of equivalence checking based on polynomial representation is proposed.With the increase of the circuit scale, more and more complex designs are based on IP. Because of the protection of IP, the design verification with black box becomes a very important task. The methods on this point in literatures are mostly based on BDD. In this paper, a characteristic function method based onpolynomial representation is given, which can availably verify combinational circuit containing black box.