Research On RTL-gate Equivalence Checking

VLSI verification takes about two thirds of the whole design time. In modern design flow of SoC, to guarantee the functional consistency of different abstract layers, a formal verification technique called Equivalence Checking (EC) is widely used. One challenging problem in EC is the verification of arithmetic designs. In the past few years, the author took part in the research and development of ZDFV Equivalence Checking System. Based on ZDFV work, the thesis focuses on the following key problems: how to construct an efficient synthesis engine; how to improve the structural similarity of the two designs; how to verify data path designs efficiently; how to use half adder graph to perform arithmetic unit verification; and how to use the hybrid SAT engine in the existing verification flow. The thesis includes the following original ideas and contributions.1. Research on developing high efficient synthesis engine. Synthesis engine transforms a RTL design into a gate level netlist. The quality of the result gate netlist has a significant effect on the entire verification performance. With studying and analyzing of Icarus Verilog synthesis engine and other synthesis systems/ algorithms, an effective synthesis flow was proposed and implemented in ZDFV. The synthesis engines supports module reuse, macro definition and synthesis directives. Experiments on widely used IWLS₂005_bechmarks_Vl .0 benchmark designs show that, compared with Icarus system, our synthesis method reduces the total synthesis and flattening time by 98%.2. Study on improving the module level similarity. The state-of-the-art equivalence checking algorithms fully exploit the similarity of the two designs. Better similarity means better performance. A new flow for RTL to gate level netlist equivalence checking was proposed. Our new flow first extracts design information, then synthesize the design, find internal potential equivalent point pairs and verify these potential equivalent point pairs. Unlike traditional flows, the new flow analyzes how different level of synthesis optimizations may affect the design similarity. The synthesis decision making takes different IP implementations into consideration and use heuristics to get better similarity. Experiments conducted on multipliers with different implementations show this leads to 3% to 28% running time reduction of the verification engine.3. Equivalence checking of datapath: Datapath consists of series arithmetic operations, which can be optimized according to some transformation rules. Verification of different level representations of datapath was discussed. A RTL datapath rewriting technique was developed to achieve better design similarity. For adder and multiplier tree expressions, the proposed technique also considers the variable ordering and variable combinations. Experiments on multiplier tree and adder tree expressions exhibit running time reduction of 83% to 99%, and 40% to 80% respectively.4. Arithmetic unit check with half adder graph technique: Binary Moment Diagram (BMD) technique has been used in multiplier equivalence checking. Unlike BDD, BMD adds weight (moment) on edges and thus reduces the node quantity of the diagram. A new circuit abstraction method, half adder graph was proposed to represent arithmetic circuits during the synthesis period. The new synthesis engine first analyzes the implementation of the arithmetic unit to gets its architectural information. Then use the information to guide the synthesis of the corresponding RTL design. Applying this approach on multiplier circuits, the performance of verification engine has been improved by 4%～63%.5. A new equivalence checking flow based on hybrid SAT engine: In traditional equivalence checking flow, since the verification engines are gate-based, the RTL designs have to been synthesized to gate level netlists first. In this RTL to gate translation process, some structural information of the designs is lost. In this research, a hybrid SAT engine based verification flow was proposed. The constraint propagation process in the hybrid SAT engine was discussed. Compared with traditional flow, up to 99% verification time reduction was achieved when verifying single adder unit and adder tree expressions.