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

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