Publication detail

Verifying Parametrised Hardware Designs Via Counter Automata

SMRČKA, A. VOJNAR, T.

Original Title

Verifying Parametrised Hardware Designs Via Counter Automata

Type

article in a collection out of WoS and Scopus

Language

English

Original 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

Authors

SMRČKA, A.; VOJNAR, T.

RIV year

2008

Released

13. 2. 2008

Publisher

Springer Verlag

Location

Heidelberg

ISBN

0302-9743

Periodical

Lecture Notes in Computer Science

Year of study

4899

State

Federal Republic of Germany

Pages from

51

Pages to

68

Pages count

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