Research On Simulation Verification Based On Algebraic Symbolic Computation

Traditional simulation method and formal verification consist of two main methods of the verification theory of IC design. Simulation method is practical and widely used because of simple underlying principle. However, simulation method is unable to cover complete tests. In contrast, formal verification method is totally complete, although its application is limited.The hybrid verification, which combines simulation method and formal verification method, has been lying in the field of verification for decades. The hybrid verification, which links the dynamics of simulation with the advantage of formal method without test cases, is the method standing on the theoretical and practical background. This thesis focuses on the combination of symbolic computation theory and simulation method.In the field of verification of digital IC, symbolic simulation, which checks the truth of assumed conditions or assertions and verifies the functional validity by performing the dynamic symbolic executions of systems, is an effective approach playing an important role in engineering applications. Since the current symbolic simulation on a high level usually leads to space explosion and symbolic output difficultly decided, the constructive theory of symbolic simulation is limited as well as its application. Hence, we introduce the method of algebraic symbolic computation into the field of symbolic simulation as the core of verifiable computation. We focus on the theoretical issues during the algebraization of symbolic simulation algorithms with the verification methodology based on assertions, and study the implementation of algebraization algorithms based on Groebner basis and Wu’s char-set. Main contributions of the dissertation are as follows:(1) The verification of algebraic symbolic simulation assertions on PSL boolean level.The emphases are transforming the verification on PSL boolean level into the algebraic problem in the symbolic computation theory, and constructing the framework of algebraic simulation verification. The boolean assertion in question and the structure of system symbolic execution is transformed a collection of non-linear algebraic equations. In this article, we use polynomials based on date flow. We modify the definition of boolean logic in the specification of PSL logic with respect to the feature of symbolic algebra, and define the requirements of verifying signal logic and assertion logic. The boolean level of PSL is the foundation of our method, though it is simple. Furthermore, we study the verification algorithm based on Groebner basis and Wu’s char-set after achieving the algebraization of boolean assertion and combinational circuit. Our algorithms are demonstrated with a few cases.(2) The verification of algebraic symbolic simulation assertions on PSL temporal level.The emphases are transforming the verification on PSL temporal level into the algebraic problem in symbolic computation theory, and constructing the framework of algebraic simulation verification. We focus on the specification and verification of symbolic assertions by comparing symbolic simulation with Symbolic Trajectory Evaluation (STE) technique. Since the boolean truth and voltage of electric signals are not distinguished in PSL specifications, the algebraic symbolic verification is not applicable. Hence, we define the constraint subset of SERE and algebraize each temporal operator. Then, we study the method of modeling temporal circuits as parameterized polynomials. Finally, we study of the specification and verification of temporal assertions by introducing Symbolic Trajectory Evaluation (STE) technique.(3) The verification of algebraic symbolic simulation assertions on System Verilog.In this section, we introduce an approach exploiting the power of polynomial ring algebra to perform System Verilog assertion verification over digital circuit systems. This method is based on algebraic symbolic computation theory and sequential properties checking. Firstly, we define a constrained subset of SVAs so that an efficient polynomial modeling mechanism for both circuit descriptions and assertions can be applied. Then we perform algebraization of SVA operators for the constrained subset, and do translation of SVAs into polynomial set representations; Finally, based on PSL boolean level and temporal level, we provide a symbolic computation based algebraic algorithm for SVAs verification.We present an algorithm framework based on the algebraic representations using Groebner bases and Wu’s method for concurrent SVAs checking. Case studies show that computer algebra can provide canonical symbolic representations for both assertions and circuit designs and can act as a novel solver engine from the viewpoint of symbolic computation.In conclusion, this paper proposes an assertion checking method of algebraic symbolic simulation for integrated circuit, which based on assertion verification methodology. This method bridges the gaps among algebraic symbolic computation, formal method and simulation technique and avoids the fragmentation of formal method and traditional circuit verification method. We also investigate an algebraic approach to traditional simulation method and formal method, and provide a new solution for IC verification theory.