Research On Generalized Symbolic Trajectory Evaluation Based Functional Verification For Parallel To Serial Signal Conversion Circuit

With the development and fast upgrading of integrated circuit design, the design cycle has been shortened,making the verification more important. And the growing complexity makes the verification much harder. The traditional verification is based on simulation which observes the outputs after giving the exact inputs. But this kind of verifycation has a long verification cycle and low coverage. Formal verification is a mathematical reasoning-based method. It abstracts the circuit into a model and verifies whether the system satisfies the given properties by mathematical reasoning. There can be 100% coverage and it will give a counterexample when there is one. However, because of its complexity of computation, it’s only applicable for small-scale circuit. There will be a state explosion problem when verifying large circuits. To improve efficiency and the scale of verification, the verification system needs a favorable data structure and algorithm.This thesis starts from introducing som frequently-used data structures and algorithms in formal verification and by comparing these methods it gives a method that makes use of both AIG and SAT-solver in GSTE, hoping to improve the efficiency and the verification scale. Also, this thesis gives an additional provement for GSTE.This thesis firstly introduces some frequently-used model check methods. After analyzing those methods, GSTE,including its extension for STE and the assertion graph(AG) in it, is discussed as the method used in this thesis. Also, a method for compress the storage space of the AG is proved here. Through the analysis of BDD, the cause of the verifying scale constraint of the current BDD-based GSTE verification method is found and the strategy of using AIG as the primary data structure is established. By using quantifier scheduling, the size of AIG is controlled and some optimization is used to make the scheduling faster. In this process, BDD is also used to simplify AIG when it comes to the threshold or even used to complete the computation. Comparing with the BDD-based method our AIG-based one can reduce the consumption of memory which brings the possibility for the improvement in efficiency.Against the state explosion that still appears when using AIG, this thesis combines the use of SAT-solver to continue the critical computation-quantifier elimination when it comes to the bottleneck. And by the optimization for the using of SAT-solver, the time consumed by the quantifier elimination process is reduced obviously improving the efficiency overall. By comparing the performance of the BDD-based method and our AIG-SAT-based method, it proves that the method in this thesis improve the scale of the circuit for verification and bring better performance when verifying relatively large scale circuit, such as the SPDIF_ENCODE module.