Detail výsledku

Verification of Asynchronous and Parametrized Hardware Designs

SMRČKA, A.; VOJNAR, T. Verification of Asynchronous and Parametrized Hardware Designs. FIT Monograph. FIT Monograph. Brno: Faculty of Information Technology BUT, 2010. 115 p. ISBN: 978-80-214-4214-6.
Typ
odborná kniha
Jazyk
anglicky
Autoři
Abstrakt

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.

Klíčová slova

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

Rok
2010
Strany
115
Řada
FIT Monograph
ISBN
978-80-214-4214-6
Vydavatel
Faculty of Information Technology BUT
Místo
Brno
BibTeX
@book{BUT61925,
  author="Aleš {Smrčka} and Tomáš {Vojnar}",
  title="Verification of Asynchronous and Parametrized Hardware Designs",
  year="2010",
  publisher="Faculty of Information Technology BUT",
  address="Brno",
  series="FIT Monograph",
  pages="115",
  isbn="978-80-214-4214-6"
}
Projekty
Bezpečné, spolehlivé a adaptivní počítačové systémy, VUT, Vnitřní projekty VUT, FIT-S-10-1, zahájení: 2010-03-01, ukončení: 2010-12-31, ukončen
Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti, GAČR, Standardní projekty, GAP103/10/0306, zahájení: 2010-01-01, ukončení: 2013-12-31, řešení
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení
Výzkumné skupiny
Pracoviště
Nahoru