Logic Circuits Verification Based On BDD

Rapid advances in VLSI technology have led to increased complexity in current hardware designs. Therefore, checking for correctness of operation has become an extremely difficult task. However, early detection of errors in designs is imperative, in order to avoid higher production development costs which are associated with the rectification of errors late in the design cycle or after the fabrication has been completed.Traditionally, designs have been verified by extensive simulation, a model is built, either in hardware or software, and a large number of test inputs are applied. The behavior of the model is compared to that of a reference model. This methodology offers no guarantees of correctness. In particular, for larger designs, simulation may cost years, we can not tolerate. Formal verification, as one of complementary approaches, has been put forward to solve these problems. The key characteristic of this approach is that formal methods are applied to actually construct a mathematical proof for the correctness of the design. Formal verification can drastically reduce design time and cover completely, it uses hardware description, rather than stimuli or wave-forms, this can verify designs and detect error quickly. Equivalence verification, as one of formal verification methods, is used to verify the circuits which are synthesized and modified. Equivalence verification is used to verify the RTL and RTL, RTL and gate-netlist, gate-netlist and gate-netlist.This dissertation introduces some traditional verification methods of combinational circuits and sequential circuits, and then analyzes, compares, summarizes and develops on the basis of them. The main contents include some aspects below.1,Introduce the main engine of equivalence checking is BDD, it can express the Boolean function very simply and take up less memory. It is able to verify larger size of circuits.2,Combine the advantage of simulation verification and formal verification, we propose the hybrid verification method. Simulation verification method can check larger size of circuits, but it seriously dependents on the test vectors and can not completely cover; formal verification methods can completely cover the circuits, but only can verify small-scale circuits. Combine the advantage of them, we not only verify larger size of circuits but also cover the circuits completely.3,We propose random simulation of analog verification. The main method is to give the circuit input test vectors and compare each node. It is different with traditional simulation methods, the purpose of simulation is not to verify the circuit but initial match of the internal nodes and registers of the circuit. 4,We use structural similarity technology. There are many similar structure between the logic circuit synthesized and original circuit, we can merge them and simplify the circuit, thus reducing the difficult of verification.5,We use cut and local BDD verification technology. Cut and local BDD are very important methods of equivalence checking, in this paper we use the equivalent parts of random simulation and structural similarity as cut , establish the local BDD from cut to output. This can further reduce the difficult of verification.