Detail publikace

Verification of Asynchronous and Parametrized Hardware Designs

Originální název

Verification of Asynchronous and Parametrized Hardware Designs

Anglický název

Verification of Asynchronous and Parametrized Hardware Designs

Jazyk

en

Originální abstrakt

Two original approaches to formal verification of hardware designs are introduced. In particular, we aim at model checking of circuits with multiple clocks and verification of parametrized hardware designs. Considering the former contribution, we introduce four methods which we use for modelling the clock domain crossing of a circuit. Models derived in such a way can then be model checked as usual while possible problems stemming from the synchronization within a circuit are implicitly covered. Four proposed ways of modelling a data transfer differ in their precision and the incurred verification cost. In the latter contribution, our proposed approach of verification is based on a translation of parametrized hardware designs to counter automata and on exploiting the recent advances achieved in the area of their automated formal verification. A parametrized hardware design translated to a counter automaton can be verified for all possible values of parameters at once.

Anglický abstrakt

Two original approaches to formal verification of hardware designs are introduced. In particular, we aim at model checking of circuits with multiple clocks and verification of parametrized hardware designs. Considering the former contribution, we introduce four methods which we use for modelling the clock domain crossing of a circuit. Models derived in such a way can then be model checked as usual while possible problems stemming from the synchronization within a circuit are implicitly covered. Four proposed ways of modelling a data transfer differ in their precision and the incurred verification cost. In the latter contribution, our proposed approach of verification is based on a translation of parametrized hardware designs to counter automata and on exploiting the recent advances achieved in the area of their automated formal verification. A parametrized hardware design translated to a counter automaton can be verified for all possible values of parameters at once.

BibTex


@article{BUT50297,
  author="Aleš {Smrčka}",
  title="Verification of Asynchronous and Parametrized Hardware Designs",
  annote="Two original approaches to formal verification of hardware designs are
introduced. In particular, we aim at model checking of circuits with multiple
clocks and verification of parametrized hardware designs. Considering the former
contribution, we introduce four methods which we use for modelling the clock
domain crossing of a circuit. Models derived in such a way can then be model
checked as usual while possible problems stemming from the synchronization within
a circuit are implicitly covered. Four proposed ways of modelling a data transfer
differ in their precision and the incurred verification cost. In the latter
contribution, our proposed approach of verification is based on a translation of
parametrized hardware designs to counter automata and on exploiting the recent
advances achieved in the area of their automated formal verification.
A parametrized hardware design translated to a counter automaton can be verified
for all possible values of parameters at once.",
  address="NEUVEDEN",
  chapter="50297",
  edition="NEUVEDEN",
  howpublished="print",
  institution="NEUVEDEN",
  number="2",
  volume="2",
  year="2010",
  month="december",
  pages="60--69",
  publisher="NEUVEDEN",
  type="journal article - other"
}