Detail publikace

Verifying Parametrised Hardware Designs Via Counter Automata

SMRČKA, A. VOJNAR, T.

Originální název

Verifying Parametrised Hardware Designs Via Counter Automata

Typ

článek ve sborníku mimo WoS a Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

formal verification, hardware design, counter automaton, VHDL

Autoři

SMRČKA, A.; VOJNAR, T.

Rok RIV

2008

Vydáno

13. 2. 2008

Nakladatel

Springer Verlag

Místo

Heidelberg

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Ročník

4899

Stát

Spolková republika Německo

Strany od

51

Strany do

68

Strany počet

18

URL

http://www.fit.vutbr.cz/~smrcka/pub/hvc07.pdf

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"
}