Formal Verification Method For Digital Circuits Based On Finite Ring Polynomials

Since integrated circuit designs are becoming more and more complex, functional validation has been the main bottleneck of the design flow. The design team spends more than 50% effort of the development on verification. The traditional simulation verification not only require much time, but also cannot guarantee full verification coverage, in a word, they cannot satisfy today's requirement in the verification of integrated circuits. Formal verification enumerates all possible conditions implicitly using mathematical methods, which can guarantee full verification coverage, its time is reduced greatly, therefore it is a feasible way to overcome verification bottleneck. Based on the theory of finite ring polynomial, the main focus of this thesis is equivalence checking and bounded model checking for the arithmetic dominant design (such as the digital signal processing system).The contributions of the thesis were as follows.(1) For the equivalence checking between logical level and register transfer level (RTL) of fixed-point datapaths, which implement the polynomial computations, an approach that the word-level descriptions for these datapaths were abstracted from their bit-level descriptions was proposed. Firstly, arithmeric transforms were used to describe the functions of logical gate-level for fixed-point datapaths, and polynomial functions were used to describe the functions of RTL. Secondly, the Newton interpolation method was used to abstract the arithmetic transforms to polynomial functions, and then the equivalence checking was implemented. Experimental results showed that the proposed algorithm was on average one to two factors faster than the existent algorithm for multiplier and one magnitude faster than the existent algorithm for some fixed-point datapaths.(2) For the equivalence checking between the design specifications of fixed-point datapath and its RTL implementations or its optimized counterpart, based on the minimal strong Gr(o|¨)bner basis of the ideal of vanishing polynomials, an algorithm of equivalence checking for fixed-point arithmetic datapaths was proposed. By modeling design specifications and register transfer level implementations for fixed-point datapaths as polynomial functions, the equivalence checking was reduced to verify whether a polynomial function is a vanishing polynomial, which can be solved by the minimal strong Gr(o|¨)bner basis of the ideal of vanishing polynomials efficiently. Theoretical analysis demonstrated that the upper bound of time complexity of the proposed algorithm was lower than the existent algorithm. Experimental results showed that the proposed algorithm was twice as fast as the existent algorithm for some fixed-point datapaths.(3) For the bounded model checking of high-level design verification of digital signal processing circuits, a bounded model checking method using Gr(o|¨)bner basis of finite ring polynomials was proposed. By modeling high-level designs and targeting properties as finite ring polynomial equations, bounded model checking was reduced to the task of theorem proving, which can be solved by Gr(o|¨)bner basis of finite ring polynomials efficiently. Experimental results showed that the proposed approach was on average one factor to one magnitude faster than the property checking approaches based on Boolean SAT and LP-based RTL SAT for some DSP circuits.