Research On Logic Equivalence Checking For Integrated Circuits

As the size of integrated circuits increases rapidly, their verificationbecomes more and more difficult. Traditional simulation and emulation not onlyrequire much time, but also cannot guarantee full verification coverage, in a word,they cannot satisfy today's requirement in the verification of integrated circuits.Formal verification uses mathematical methods to enumerate all possibleconditions implicitly, it can guarantee full verification coverage and needs muchless time, it's a feasible way to overcome verification bottleneck. As being apractical formal verification method, equivalence checking is always used toverify circuits' functionality after synthesis and manual modification. The mainfocus of this thesis is equivalence checking and it was explored in the followingthree aspects:1. When Verifying combinational circuits' functionality, it's not feasible tobuild BDDs for primary outputs directly. The internal equivalent nodes should bediscovered to form cuts, which can be used to separate the original verificationproblem into a series of small and easy problems. Aims at using cuts incombinational equivalence checking, a new method combining universal cut andspecial cut was proposed; aims at the false negatives caused by cut, a strategywhich paid more attention on removing dependencies among high level nodeswas proposed. Experimental results based on ISCAS85 show that the method canincrease verification speed of combinational circuits efficiently.2. When verifying the equivalence of sequential circuits, a lot of time isspent on pre-image computation, which is used to judge whether a state can bereached from the initial state. A new method using cached states was proposed inthis thesis. States that can be reached from the initial state in simulation werecollected as reachable states, states that cannot be reached from the initial state in verification were collected as unreachable states, and they were used to avoidrepeated pre-image computation. Experimental results based on MCNC91 showthe efficiency of this method.3. Satisfiability is the hotspot of research in recent ten years; it's more than apure mathematical problem, but is used widely in EDA domain. SAT is moreefficient in finding nodes that are not equivalent, while BDD is more efficient inproving nodes' equivalence. This thesis proposed a new method that combinedBDD and SAT in sequential equivalence checking, BDD engine was used first toverify the equivalence of nodes, if the limit was exceeded, SAT engine was usedinstead, in this way, both of their Strength can be exerted. Experimental resultsbased on ISCAS89 show that the combination of these two engines can reduceverification time efficiently.