Front-end Design And Implementation Of Equivalence Checking System Of Verilog HDL

The verification of correctness of integrated circuit design is always important inacademia and industry and paying more attention to the research subject. The difficulty ofverification of grow gradually with the rapid development of large scale integrated circuit.The traditional test methods such as simulation and simulation not only can’t completecoverage of the errors and spend a lot of time. Because of all these defects, the traditional testtechniques have been unable to keep up with the pace of the high speed development ofintegrated circuits. The formal verification method using mathematical method completelyproof or verify the circuit design scheme and consistency of the function of circuit designdescription Generally speaking, the formal verification method has three categories,equivalence checking, model checking and theorem proving. The core goal of equivalencechecking is to verify functional equivalence of the two design model and the principle isbased on mathematical theorems and axiom. Equivalence checking includes combinationalcircuit equivalence checking and sequential circuit equivalence checking. The main work ofour front-end of CEC (the Combinational Equivalence Checking) system is extracting formalmodel from Verilog source code. In formal verification, the first step is to build a formalmodel. Most of the academic tools represent the designs in BLIF or BLIF-MV network, whilecannot directly take Verilog source code as an input. However, Verilog and VHDL are themost common used hardware description languages for large scale integrated circuits. It isnecessary if the source code could be used directly, rather than an intermediate format. Wenotice that synthesizable Verilog is well-structured which can be represented in SSA (StaticSingle Assignment) form. In this paper, we describe a method that extracts formal modeldirectly from Verilog source code by converting the code to SSA form. With this method, wehave implemented a prototype system that extracts formal model of Verilog programs. Wealso prove the conversion function-preserving by translating SSA back to Verilog andchecking its equivalence with the primary design. The main procedure of front-end of CECsystem is as follows: 1.The lexical and syntax of Verilog HDL are analyzed by lexical analyzer and syntaxanalyzer, and generating an internal syntactic representation of the program. The mostcommon IR is the Abstract Syntax Tree (AST). Then we do Elaboration based on AST.Elaboration is a process of finding identifier definitions, resolving parameters overridden byinstantiation and defparam statements, and generating fully–expanded code. In ourimplementation, the elaboration phase revises the AST to meet the needs. The elaborationphase is a necessary pre-process for the SSA conversion.2.We extract formal model from Verilog and it is in this phase that our Verilog model istransformed into SSA form which can be exploited by back-end solver conveniently.3.After extracting formal model, we take the source code model as a reference model andthe model through the transition as an implementation model to check whether the conversionis function-preserving with Formality.From Verilog source model to our formal model, three transitions are needed: Verilogsource model to AST model, AST model to elaboration model and elaboration model to SSAform model. SSA form model is the final extraction model to hand over to back-end solver.