Algebraic Verification Method for SEREs Properties via Groebner Bases Approaches
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...
Saved in:
| Main Authors: | , , |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Wiley
2013-01-01
|
| Series: | Journal of Applied Mathematics |
| Online Access: | http://dx.doi.org/10.1155/2013/272781 |
| Tags: |
Add Tag
No Tags, Be the first to tag this record!
|
| _version_ | 1832564195770499072 |
|---|---|
| author | Ning Zhou Jinzhao Wu Xinyan Gao |
| author_facet | Ning Zhou Jinzhao Wu Xinyan Gao |
| author_sort | Ning Zhou |
| collection | DOAJ |
| description | 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. |
| format | Article |
| id | doaj-art-5cf05166cf0441e3b83567214a7e4299 |
| institution | Kabale University |
| issn | 1110-757X 1687-0042 |
| language | English |
| publishDate | 2013-01-01 |
| publisher | Wiley |
| record_format | Article |
| series | Journal of Applied Mathematics |
| spelling | doaj-art-5cf05166cf0441e3b83567214a7e42992025-02-03T01:11:36ZengWileyJournal of Applied Mathematics1110-757X1687-00422013-01-01201310.1155/2013/272781272781Algebraic Verification Method for SEREs Properties via Groebner Bases ApproachesNing Zhou0Jinzhao Wu1Xinyan Gao2School of Computer and Information Technology, Beijing Jiaotong University, Beijing 10044, ChinaSchool of Computer and Information Technology, Beijing Jiaotong University, Beijing 10044, ChinaSchool of Software of Dalian University of Technology, Dalian 116620, ChinaThis 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.http://dx.doi.org/10.1155/2013/272781 |
| spellingShingle | Ning Zhou Jinzhao Wu Xinyan Gao Algebraic Verification Method for SEREs Properties via Groebner Bases Approaches Journal of Applied Mathematics |
| title | Algebraic Verification Method for SEREs Properties via Groebner Bases Approaches |
| title_full | Algebraic Verification Method for SEREs Properties via Groebner Bases Approaches |
| title_fullStr | Algebraic Verification Method for SEREs Properties via Groebner Bases Approaches |
| title_full_unstemmed | Algebraic Verification Method for SEREs Properties via Groebner Bases Approaches |
| title_short | Algebraic Verification Method for SEREs Properties via Groebner Bases Approaches |
| title_sort | algebraic verification method for seres properties via groebner bases approaches |
| url | http://dx.doi.org/10.1155/2013/272781 |
| work_keys_str_mv | AT ningzhou algebraicverificationmethodforserespropertiesviagroebnerbasesapproaches AT jinzhaowu algebraicverificationmethodforserespropertiesviagroebnerbasesapproaches AT xinyangao algebraicverificationmethodforserespropertiesviagroebnerbasesapproaches |