Publication Details

Verifying Parametrised Hardware Designs Via Counter Automata

SMRČKA Aleš and VOJNAR Tomáš. Verifying Parametrised Hardware Designs Via Counter Automata. In: Hardware and Software, Verification and Testing. Lecture Notes in Computer Science, vol. 4899. Heidelberg: Springer Verlag, 2008, pp. 51-68. ISSN 0302-9743.
Czech title
Verifikace parametrických hardwarových návrhů pomocí čítačových automatů
Type
conference paper
Language
english
Authors
Smrčka Aleš, Ing., Ph.D. (DITS FIT BUT)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
URL
Keywords

formal verification, hardware design, counter automaton, VHDL

Abstract

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.

Published
2008
Pages
51-68
Journal
Lecture Notes in Computer Science, vol. 4899, ISSN 0302-9743
Proceedings
Hardware and Software, Verification and Testing
Series
Lecture Notes in Computer Science
Conference
Haifa Verification Conference 2007, IBM Haifa Labs, IL
Publisher
Springer Verlag
Place
Heidelberg, DE
BibTeX 
@INPROCEEDINGS{FITPUB8526,
   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",
   journal = "Lecture Notes in Computer Science",
   volume = 4899,
   year = 2008,
   location = "Heidelberg, DE",
   publisher = "Springer Verlag",
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/8526"
}
Back to top