Applications Of Formal Verification In EDA

Formal verification technology originated in the20th century, the software crisis in60years. Until the70’s, formal verification technology is transformational for theprogram in general, that a simple scientific calculation, counting and other functions ofthe software. The great success comes from the late80’s,Symbolic Model Checking(Symbolic Model Checking) methods are proposed and implemented in hardwareverification. In1987, McMillan PhD thesis, used BDD (Binary Decision Diagram)technology in model checking for the first time, thus greatly easing the space explosionproblem. However, people soon discovered that, for complex systems, space explosionproblem is still difficult to overcome which led to bounded model checking techniquesproposed in1999. Overall, the model checking in hardware verification method issuccessful, the fundamental reason is the hardware usually has hierarchical and morestructured, compared to the complexity of the software program structure, is easier todescribe and verify.This paper mainly discuss formal verification and how to use it in integrated circuitdesign. Firstly, we introduce the status of formal verification and IC design flow, thenintroduce the framed temporal logic programming language. We implement thedescription of simple sequential circuits using this language. After that, we discuss thedesign principle and transplantation framework of tools used for model checking,andverify the simple circuits described by the framed temporal logic programminglanguage.Finally, this paper introduce the boolean satisfiability and equivalence checking.The paper also discuss the logic synthesis process, design principles and synthesis toolsof IC design in detail, and implement the equivalence checking of combinationalcircuits before and after logic synthesis process using SAT solver.