Detail publikačního výsledku

Verifying Parametrised Hardware Designs Via Counter Automata

SMRČKA, A.; VOJNAR, T.

Originální název

Verifying Parametrised Hardware Designs Via Counter Automata

Anglický název

Verifying Parametrised Hardware Designs Via Counter Automata

Druh

Stať ve sborníku mimo WoS a Scopus

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.

Anglický 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

Klíčová slova v angličtině

formal verification, hardware design, counter automaton, VHDL

Autoři

SMRČKA, A.; VOJNAR, T.

Rok RIV

2010

Vydáno

13.02.2008

Nakladatel

Springer Verlag

Místo

Heidelberg

Kniha

Hardware and Software, Verification and Testing

Edice

Lecture Notes in Computer Science

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Svazek

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