Verilog Combinational Equivalence Checking Based On SMT Constraint Solver

With the development of the scalability and complexity of integrated circuit, the traditionsimulation based proof technique could not meet the need of developing large-scare hardwaresystem. The formal verification method, which is a supplement of simulation based technique,uses the mathematic logic in building the formal model of the system and reasoning, andtherefore strictly proves whether the system satisfy the specification. The formal verificationmethod is complete as it wouldn’t miss the cornel case. The formal verification method hasbecome an essential verification technique in modern integrated circuit development, andtherefore doing further research on it has significance value.The formal verification method includes the equivalence checking, theorem proving andmodel checking. In this paper we are focus on the equivalence checking problem ofcombinational circuits. Most previous works on combinational equivalence checking usedBDDs and other Boolean level representations to formulate and solve the problem, andtherefore the system model must be transformed and represented by Boolean variables.However, the arithmetic circuit usually includes word level arithmetic operations, and thistransformation will lose the information presented in the high level speciation. To overcomethis limitation, the word level proof techniques like Word Level Decision Diagrams (WLDD),Weighted Generalized List (WGL) and Satisfiability Module Theory (SMT) were proposed.The SMT can efficiently handle the designs containing word-level arithmetic operators andbit-level Boolean logic.In this paper, we present a technique checking the equivalence of two combinationalcircuits based on word level constraint solver. First, the reference and implementation circuitsare parsed by the front-end lexical and syntax analyzer. Then after elaboration process, theformal model defining the system constraint are extracted separately, and finally a Mitercircuit is constructed and handed over to the back-end constraint solver. By extracting theformal model using Static Single Assignment (SSA) form, combined with STP-a word-levelconstraint solver, we implement a Verilog combinational equivalence checker. Theexperimental results indicate that our method can utilize word-level information to speed upthe process of verification, and result in a decrease in memory usage.There are usually some equivalent nodes between the two circuits to be verified. Thestructure-based combinational equivalence checking method exploits structure similaritiesbetween internal nodes of the two circuits and uses this information to simplify the verification. One of these methods is introducing cut-points for the internal equivalent nodes.With these internal equivalent nodes, we can reconstruct the circuits by substitute some of thesub-circuits to cut-points, and therefore treated them as primary inputs, which will made therepresentation of the circuits much smaller, and result in a reduction in the memory usage andan improvement in the scalability of the circuits that the equivalence checking tools can beverified. This procedure looses the constraints and made the range of the value that thecircuits can get in these places much wider. Therefore, if the circuits are equivalent aftersimplified, the original two circuits are equivalent. Or else, we can get a counter example.That is, a group of assignments of the inputs of the simplified circuits. If the original circuitscan get these assignments in the corresponding place, the original two circuits are notequivalent. Or else, the counter example is spurious. The problem that the original circuits areequivalent while the simplified circuits are not equivalent is called the false-negative problem.The false-negative is very common in the cut-point based equivalence checking. One ofthe false-negative elimination methods is to substitute some of the cut-points to thecorresponding sub-circuits. The iteration procedure is continued, until the circuits are provedto be equivalent, or the counter example is proved to be real, that is the circuits are notequivalent.In this paper, we proposed a method for selecting the cut-points for substitution when thefalse-negative happens. We find the root cause of the false-negative with the unsatisfiable core,and only substitute the set of cut-points that caused the false-negatives. In this way, we canavoid the substitution of irrelevant cut-points and result in a reduction in the number ofiterations.