Result 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.
Type
conference paper
Language
English
Authors
Smrčka Aleš, Ing., Ph.D., DITS (FIT)
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
Abstract

The paper presents a new approach to formal verification of generic(i.e. parametrised) hardware designs specified in VHDL. The proposedapproach is based on a translation of such designs to counter automataand on exploiting the recent advances achieved in the area of theirautomated formal verification. We have implemented the proposedtranslation. Using one of the state-of-the-art tools for verificationof counter automata, we were then able to verify several non-trivialproperties of parametrised VHDL components, including a real-life one.

Keywords

formal verification, hardware design, counter automaton, VHDL

URL
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
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"
}
Projects
Optická síť národního výzkumu a její nové aplikace, MŠMT, Výzkumná centra (2000-2004), MSM6383917201, start: 2004-01-01, end: 2010-12-31, completed
Security-Oriented Research in Information Technology, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, start: 2007-01-01, end: 2013-12-31, running
Research groups
Automated Analysis and Verification Research Group - VeriFIT (RG VERIFIT)
Departments
Department of Intelligent Systems (DITS)
Back to top