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 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.

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