Formal Verification Of Datapaths Based On Polynomial Symbolic Algebra

ABSTRACT:In modern world, the IC industry develops rapidly. More and more electronic products come to our life with profound influence. As the size, capability and functional complexity of integrated circuit desige increasing, the size of circuits themselves becomes smaller. And the functional verification has been the main bottleneck in the design process. Traditional verification methods always base on simulation, they cannot support today's tremendous verification demand gradually. Instead, new type of method such as formal verification has been paid more attentions in academic community and industry world.Existing formal verification techniques are mostly fit for verification of low-level control-dominated circuits. They are difficult to satisfy the verification requirements of high-level data-dominated plans. With a hard work, scientists develop a new theory called polynomial symbolic algebra, which can be a very effective technique for representation and computation of integrated circuit designs. What's more, it successfully overcomes some weak points of the traditional formal verification methods to a certain degree. The reseaches of this thesis are as follows:1. For the mainstream formal verification methods, this thesis does an in-depth study, which includes expounding the main principles and means of these methods and specifying the comparison and analysis between them.2. This thesis based on Wu-Ritt and Groebner basis gives the following research in functional equivalence verification of high-level datapaths:firstly, we can model datapaths at higher levels of abstraction directly under the theory of PSA. The general form of the polynomial set representations of high-level datapaths and the method to construct it are presented. Then, starting from the common zeros of polynomial set, the functional equivalence of high-level datapaths is defined. Furthermore, a new effective functional equivalence verification algorithm based on PSA is created. And its correctness is proved under an experiment. At last this thesis gives a further study direction.