Research On SAT-based Formal Verification Approach For Digital Circuits

With the rapid development of semiconductor technology, the complexity of integrated circuits is increasing with exponential order. The development of EDA technology is relatively backward, verification becomes the bottleneck of the whole IC design flow. The BDD based formal verification method is an automated method, but it can only suitable for small and middle scale circuits, while for large scale circuits its states space will explode. The breakthrough results received in the research of SAT problems make it possible for some problems of EDA fields to be solved by SAT solver. However, general SAT solver is not always the best when solving the problem of a special field. A deep research on SAT based digital circuit formal verification approach and FPGA mapping approach has been done in our thesis. Circuits'structure and the information of special problem are used to improve SAT algorithm, the contributions of the thesis are as follows.1) For SAT-based equivalence checking, the original solver zChaff* can't take full use of the information of circuit's observability don't cares (ODC). Aiming at this problem, an improved SAT algorithm zChaff+ is proposed. First, the concept of control uniqueness is introduced according to the relationship of inputs and outputs of logic gates. Next, based on the theory of CNF carrying ODC condition, the losses of ODC conditions are reduced by without ordering the variables in computing ODC conditions; the control uniqueness of the circuit is guaranteed by making no decision on variables which only appear in the ODC conditions. Theoretical analysis and experimental results show that the improved SAT solver zChaff+has smaller search space and higher speed when solving equivalence checking problems.2) For SAT based preimage computation problem in unbound model checking, an improved SAT algorithm All-SAT+is proposed. Firstly, zChaff+is selected as the standard SAT solver, and it is improved further on decision making by choosing variable appearing in ODC conditions most first. In this way, bigger solution cube or smaller conflict clause is produced, and the memory space required is reduced, mean while, the total enumeration steps are also reduced. Secondly, in order to catch more solutions in every enumeration step, an improved solution cubes enlarge algorithm of lifting checking only state variable is used. Thirdly, the ZBDD model is used to store and combine the solutions. Lastly, Don't Care States learning is used to avoid searching unnecessary states space, and sharing learning clauses of increment technology is used to improve the algorithm efficency. The experiment results show the improved algorithm All-SAT+reduce the number of solutions and time of pre-image computation, which is much quicker than the algorithms lifting and Lipi.3) For over-satisfied problem of hybrid SAT algorithm consisted with random exploration and DPLL algorithm, an improved algorithm HBISAT+ is proposed. The hybrid algorithm is improve by the method of using circuit observability, which includes the improved random algorithm WalkSAT and the DPLL algorithm zChaff* presented in previous paper. Improved heuristic strategies are used to select padding clauses, the iterative number of the algorithm is reduced and the efficiency is improved. The experiment results show, the hybrid algorithm is much quicker than DPLL algorithm, while the improved algorithm HBISAT+ is 27% quicker than original algorithm, which proves the hybrid algorithm improved by using the circuit observability can solve hard equivalence checking problems more efficiently.4) For the large amount of calculation bringed by input permutation in SAT based FPGA technology mapping algorithm, an improved mapping algorithm is proposed. Symmetrical information in PLB structures and Boolean function are used, the input permutation problem is transfered into the problem of allocation, only necessary permutations are generated directly, and the satifiability checking is conducted on necessary permutations. The experiment results show that the speed of the improved algorithm is 32% quicker than algorithm SAT-BM-I presented in previous paper, which proves the scale of problem satisfiability solving is greatly reduced in the improved algorithm, and the efficiency of mapping algorithm is improved.