Groebner Bases Based Verification Solution for SystemVerilog Concurrent Assertions
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 polynom...
Saved in:
| Main Authors: | , , , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2014-01-01
|
| Series: | Journal of Applied Mathematics |
| Online Access: | http://dx.doi.org/10.1155/2014/194574 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832564789365178368 |
|---|---|
| author | Ning Zhou Xinyan Gao Jinzhao Wu Jianchao Wei Dakui Li |
| author_facet | Ning Zhou Xinyan Gao Jinzhao Wu Jianchao Wei Dakui Li |
| author_sort | Ning Zhou |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-f836846f7ced4a38b3f4c8b40715cfa3 |
| institution | Kabale University |
| issn | 1110-757X 1687-0042 |
| language | English |
| publishDate | 2014-01-01 |
| publisher | Wiley |
| record_format | Article |
| series | Journal of Applied Mathematics |
| spelling | doaj-art-f836846f7ced4a38b3f4c8b40715cfa32025-02-03T01:10:12ZengWileyJournal of Applied Mathematics1110-757X1687-00422014-01-01201410.1155/2014/194574194574Groebner Bases Based Verification Solution for SystemVerilog Concurrent AssertionsNing Zhou0Xinyan Gao1Jinzhao Wu2Jianchao Wei3Dakui Li4School of Computer and Information Technology, Beijing Jiaotong University, Beijing 10044, ChinaG & S Labs, School of Software of Dalian University of Technology, Dalian 116620, ChinaSchool of Computer and Information Technology, Beijing Jiaotong University, Beijing 10044, ChinaG & S Labs, School of Software of Dalian University of Technology, Dalian 116620, ChinaG & S Labs, School of Software of Dalian University of Technology, Dalian 116620, ChinaWe 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.http://dx.doi.org/10.1155/2014/194574 |
| spellingShingle | Ning Zhou Xinyan Gao Jinzhao Wu Jianchao Wei Dakui Li Groebner Bases Based Verification Solution for SystemVerilog Concurrent Assertions Journal of Applied Mathematics |
| title | Groebner Bases Based Verification Solution for SystemVerilog Concurrent Assertions |
| title_full | Groebner Bases Based Verification Solution for SystemVerilog Concurrent Assertions |
| title_fullStr | Groebner Bases Based Verification Solution for SystemVerilog Concurrent Assertions |
| title_full_unstemmed | Groebner Bases Based Verification Solution for SystemVerilog Concurrent Assertions |
| title_short | Groebner Bases Based Verification Solution for SystemVerilog Concurrent Assertions |
| title_sort | groebner bases based verification solution for systemverilog concurrent assertions |
| url | http://dx.doi.org/10.1155/2014/194574 |
| work_keys_str_mv | AT ningzhou groebnerbasesbasedverificationsolutionforsystemverilogconcurrentassertions AT xinyangao groebnerbasesbasedverificationsolutionforsystemverilogconcurrentassertions AT jinzhaowu groebnerbasesbasedverificationsolutionforsystemverilogconcurrentassertions AT jianchaowei groebnerbasesbasedverificationsolutionforsystemverilogconcurrentassertions AT dakuili groebnerbasesbasedverificationsolutionforsystemverilogconcurrentassertions |