Conference paper

SMRČKA Aleš and VOJNAR Tomáš. Verifying Parametrised Hardware Designs Via Counter Automata. In: Hardware and Software, Verification and Testing. Heidelberg: Springer Verlag, 2008, pp. 51-68. ISSN 0302-9743.
Publication language:english
Original title:Verifying Parametrised Hardware Designs Via Counter Automata
Title (cs):Verifikace parametrických hardwarových návrhů pomocí čítačových automatů
Pages:51-68
Proceedings:Hardware and Software, Verification and Testing
Conference:Haifa Verification Conference 2007
Series:Lecture Notes in Computer Science 4899
Place:Heidelberg, DE
Year:2008
Journal:Lecture Notes in Computer Science, Vol. 2008, No. 4899, DE
ISSN:0302-9743
Publisher:Springer Verlag
URL:http://www.fit.vutbr.cz/~smrcka/pub/hvc07.pdf [PDF]
Keywords
formal verification, hardware design, counter automaton, VHDL
Annotation
The paper presents a new approach to formal verification of generic (i.e. parametrised) hardware designs specified in VHDL. The proposed approach is based on a translation of such designs to counter automata and on exploiting the recent advances achieved in the area of their automated formal verification. We have implemented the proposed translation. Using one of the state-of-the-art tools for verification of counter automata, we were then able to verify several non-trivial properties of parametrised VHDL components, including a real-life one.
BibTeX:
@INPROCEEDINGS{
   author = {Ale{\v{s}} Smr{\v{c}}ka and Tom{\'{a}}{\v{s}} Vojnar},
   title = {Verifying Parametrised Hardware Designs Via Counter Automata},
   pages = {51--68},
   booktitle = {Hardware and Software, Verification and Testing},
   series = {Lecture Notes in Computer Science 4899},
   journal = {Lecture Notes in Computer Science},
   volume = {2008},
   number = {4899},
   year = {2008},
   location = {Heidelberg, DE},
   publisher = {Springer Verlag},
   ISSN = {0302-9743},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=8526}
}

Your IPv4 address: 54.227.127.109
Switch to IPv6 connection

DNSSEC [dnssec]