Study On The Application Of Formal Verification

The design of complex and high-speed chips requires novel theories and techniques in design automation. The research of EDA is realm for having challenge and contain development field. The application of formal verification in VLSI ware studies in this paper.Thesis discuss in-depth about the equivalence checking at first. Order Finite State Machine ware proposed to deal with the combinational equivalence checking. The implement of equivalence checking algorithm have been introduced in detail. Time complicacy size of this algorithm is polynomial scale under the theories analysis, and algorithm has put some upswing for the former combinational equivalence checking algorithm. The Order Finite State Machine is mew model for electric circuit describe, We can do combinational equivalence checking convenience and quickly by this model.The model checking method has been studied carefully, and analyzed the current theory achievement on model checking. Some trial have been done on circuit verification under the symbol model check terrace SMV system .The experiment show that it was feasibility and practicability. In the end we discuss another technique-the Theorem Proving method. And propose a new discompose strategy. Discompose according as proposition deduction rules. Using this strategy we can deal with large size circuit verification.