scholarly journals Wu’s Characteristic Set Method for SystemVerilog Assertions Verification

2013 ◽  
Vol 2013 ◽  
pp. 1-14 ◽  
Author(s):  
Xinyan Gao ◽  
Ning Zhou ◽  
Jinzhao Wu ◽  
Dakui Li
Keyword(s):  
Polynomial System ◽  
Algebraic Approach ◽  
Digital Circuit ◽  
Characteristic Set ◽  
Wu's Method ◽  
Verification Methods ◽  
Polynomial Modeling ◽  
Characteristic Set Method ◽  
Algorithm Framework ◽  
Algebraic Representations

We propose a verification solution based on characteristic set of Wu’s method towards SystemVerilog assertion checking over digital circuit systems. We define a suitable subset of SVAs so that an efficient polynomial modeling mechanism for both circuit descriptions and assertions can be applied. We present an algorithm framework based on the algebraic representations using characteristic set of polynomial system. This symbolic algebraic approach is a useful supplement to the existent verification methods based on simulation.

scholarly journals Algebraic Verification Method for SEREs Properties via Groebner Bases Approaches

2013 ◽  
Vol 2013 ◽  
pp. 1-10 ◽  
Author(s):  
Ning Zhou ◽  
Jinzhao Wu ◽  
Xinyan Gao
Keyword(s):  
Algebraic Approach ◽  
Digital Systems ◽  
Groebner Bases ◽  
Symbolic Simulation ◽  
Verification Method ◽  
Symbolic Representations ◽  
Temporal Properties ◽  
Verification Methods ◽  
Algorithm Framework ◽  
Algebraic Representations

This work presents an efficient solution using computer algebra system to perform linear temporal properties verification for synchronous digital systems. The method is essentially based on both Groebner bases approaches and symbolic simulation. A mechanism for constructing canonical polynomial set based symbolic representations for both circuit descriptions and assertions is studied. We then present a complete checking algorithm framework based on these algebraic representations by using Groebner bases. The computational experience result in this work shows that the algebraic approach is a quite competitive checking method and will be a useful supplement to the existent verification methods based on simulation.

scholarly journals Groebner Bases Based Verification Solution for SystemVerilog Concurrent Assertions

2014 ◽  
Vol 2014 ◽  
pp. 1-15
Author(s):  
Ning Zhou ◽  
Xinyan Gao ◽  
Jinzhao Wu ◽  
Jianchao Wei ◽  
Dakui Li
Keyword(s):  
Case Studies ◽  
Symbolic Computation ◽  
Computer Algebra ◽  
Polynomial Ring ◽  
Digital Circuit ◽  
Groebner Bases ◽  
Symbolic Representations ◽  
Polynomial Modeling ◽  
Algorithm Framework ◽  
Algebraic Representations

We introduce an approach exploiting the power of polynomial ring algebra to perform SystemVerilog assertion verification over digital circuit systems. This method is based on Groebner bases theory and sequential properties checking. We define a constrained subset of SVAs so that an efficient polynomial modeling mechanism for both circuit descriptions and assertions can be applied. We present an algorithm framework based on the algebraic representations using Groebner bases 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.

Sign in / Sign up

Export Citation Format

Share Document