High-Level Formal Verification Based On Polynomial Symbolic Algebra Module

The microelectronics technology, which contain tens of millions of components of the Integrated Circuits (IC) has been able to survey the plot produced, the real SoC (System on a Chip) is a reality. The ability of integrated circuits fabrication exceeds its designa. The crucial problem in VLSI designation is how to check the design correctness, i.e.design verification. Because of the complexity of design verification increasing exponentially with the scale of chip, the commercial verification mathods,such as simulation,testing and emulation.are not completely for large scale system. The complexity of Integrated Circuits technical art make the cost of fabrication fairly expansive. In the past twenty years, people has found a new method—formal verification. It is a hopeful method for the design verification of VLSI. Formal verification means the process of verfication is mathematical, and not as simulation technology which is experimental. Mathematical verification conquers the insufficient of simulation for completeness, and can reduce time for verification. Formal verification is the automatical verification for cirsuits description, and can reduce the complexity of verification.This paper gives the study of polynomial symbolic algebraic theory in formal verification method.The appliance of polynomial symbolic algebraic in formal verification ,people have given two polynamial denotative module WGLs (Weighted Generalized Lists) and TEDs (Taylor Expansion Diagrams),and gives the corresponding equivalence checking algorithms .The important work of this paper as follows.1) Basing on WGLs module,the equivalence checking bettwen high-level specifications and implementation of circuits is given. Beause WGLs can't present the circuits' descriptions which contain Boolen variables and word level variables ,this paper presents a new model LWGLs (Labeled and Weighted Generalized Lists) basing on WGLs. LWGLs can present the circuits' descriptions which contain Boolen variables and word level variables, and can be applied to...