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

Anglický název

Verifying Parametrised Hardware Designs Via Counter Automata

Jazyk

en

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.

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

Dokumenty

BibTex


@inproceedings{BUT30897,
  author="Aleš {Smrčka} and Tomáš {Vojnar}",
  title="Verifying Parametrised Hardware Designs Via Counter Automata",
  annote="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.",
  address="Springer Verlag",
  booktitle="Hardware and Software, Verification and Testing",
  chapter="30897",
  edition="Lecture Notes in Computer Science",
  howpublished="print",
  institution="Springer Verlag",
  journal="Lecture Notes in Computer Science (IF 0,513)",
  year="2008",
  month="february",
  pages="51--68",
  publisher="Springer Verlag",
  type="conference paper"
}