Font Size: a A A

Research On Formal Methods For Digital Circuit Verification Based On Polynomial Symbolic Algebra

Posted on:2010-02-23Degree:DoctorType:Dissertation
Country:ChinaCandidate:Z YangFull Text:PDF
GTID:1118360302487123Subject:Computer application technology
Abstract/Summary:PDF Full Text Request
As the size and functional complexity of integrated circuits increase, functional verification has been the main bottleneck of the design flow. Traditional simulation based verification methods cannot meet with the tremendous verification demand of today's complex integrated circuit designs. Because of this, formal verification techniques, such as model checking and equivalence verification, receive more and more attention from academic circle as an important assistant. Existing formal verification techniques are mostly based on bit-level methods, such as BDD and Boolean SAT, which are generally geared towards verification of low-level control-dominated circuits, and are hard to satisfy the verification requirements of high-level data-dominated designs. As a newly devolopted technique for circuit representation and computation, polynomial symbolic algebra can overcome some drawbacks of BDD and Boolean SAT. This thesis investigates the application of polynomial symbolic algebra in digital cricuit verification deeply. The contributions of this thesis are as follows.(1) A model checking approach based on polynomial symbolic algebra has been proposed. First, a new concept called state transition system is obtained by extending the concept of classical Kripke structure, which is used to represent the control logic of high-level designs as a substitution of the latter. Datapath and control logic of high-level designs can thus be modeled in a unified framework using polynomial method, and frequent constraint propagation and backtracking between data domain and control domain are therefore avoided. Then, a framework for high-level model checking is presented. In the framework, the original model checking problem is translated into a first-order theorem proving problem, in which both hypothesis and conclusion of the theorem are of polynomial form. A symbolic computation based decision procedure is ultilized to prove the theorem efficiently. The experimental results on some typical high-level designs show that, the proposed approach is on average one to five times faster than the nonlinear solver based high-level model checking approache, while keeping the verification accuracy. (2) An equivalence verification method based on polynomial symbolic algebra has been proposed. Datapaths are modeled at higher levels of abstraction directly. The general form of the polynomial set representations of high-level datapaths and the method to construct it are presented. Since high-level datapaths no longer need to be transformed into gate-level netlists, our approach usually involves much less signal variables and constraints for a given verification problem compared with the BDD and Boolean SAT based equivalence verification methods. Furthermore, the functional equivalence of high-level datapaths is defined from the prospective of common zeros of polynomial sets, and an efficient algebraic solution based on symbolic computation is presented. The experimental results on some benchmark datapaths show that, the proposed method is on everage one factor to one order of magnitude faster than the *BMD and integer linear programming based equivalence verification methods, while keeping the error detecting capability.(3) The hierarchical verification methods based on polynomial symbolic algebra have been proposed. First, a generalized list based hierarichical representation for circuit designs is introduced. Based on this hierarchical representation and ultilizing the elimination and extension theorems from polynomial algebra, a new method is proposed to calculate the functionality of circuit designs, which breaks the original calculation into small sub-tasks to finish recursively. The computational efficiency can thus be improved efficienctly. Applying this new calculation method to design verification, hierarchical model checking and equivalence verification methods are realized. The experimental results show that, the hierarchical verification methods are much more efficient than the original verification methods. For our experimental circuits, efficiencies of the model checking and equivalence verification algorithms increase 23% and 17% respectively.
Keywords/Search Tags:Formal verification, Model checking, Equivalence verification, Hierarchical, Polynomial symbolic algebra
PDF Full Text Request
Related items