Publication detail

Verification of Asynchronous and Parametrized Hardware Designs

SMRČKA, A. VOJNAR, T.

Original Title

Verification of Asynchronous and Parametrized Hardware Designs

English Title

Verification of Asynchronous and Parametrized Hardware Designs

Type

book

Language

en

Original Abstract

We introduce two original approaches to formal verification of hardware designs. 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.

English abstract

We introduce two original approaches to formal verification of hardware designs. 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.

Keywords

Formal verification, modelling hardware design, clock domain crossing, parametrized hardware design, counter automata.

RIV year

2010

Released

31.12.2010

Publisher

Faculty of Information Technology BUT

Location

Brno

ISBN

978-80-214-4214-6

Edition

FIT Monograph

Edition number

NEUVEDEN

Pages count

115

Documents

BibTex


@book{BUT61925,
  author="Aleš {Smrčka} and Tomáš {Vojnar}",
  title="Verification of Asynchronous and Parametrized Hardware Designs",
  annote="We introduce two original approaches to formal verification of hardware designs.
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="Faculty of Information Technology BUT",
  chapter="61925",
  edition="FIT Monograph",
  howpublished="print",
  institution="Faculty of Information Technology BUT",
  year="2010",
  month="december",
  pages="0--0",
  publisher="Faculty of Information Technology BUT",
  type="book"
}