Publication Details

Verifying Parametrised Hardware Designs Via Counter Automata

SMRČKA, A.; VOJNAR, T. Verifying Parametrised Hardware Designs Via Counter Automata. Hardware and Software, Verification and Testing. Lecture Notes in Computer Science. Lecture Notes in Computer Science. Heidelberg: Springer Verlag, 2008. p. 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)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS)
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
Publisher
Springer Verlag
Place
Heidelberg
BibTeX 
@inproceedings{BUT30897,
  author="Aleš {Smrčka} and Tomáš {Vojnar}",
  title="Verifying Parametrised Hardware Designs Via Counter Automata",
  booktitle="Hardware and Software, Verification and Testing",
  year="2008",
  series="Lecture Notes in Computer Science",
  journal="Lecture Notes in Computer Science",
  volume="4899",
  pages="51--68",
  publisher="Springer Verlag",
  address="Heidelberg",
  issn="0302-9743",
  url="http://www.fit.vutbr.cz/~smrcka/pub/hvc07.pdf"
}
Back to top