Dissertation

SMRČKA Aleš. Verification of Asynchronous and Parametrized Hardware Designs. Brno: Department of Intelligent Systems FIT BUT, 2010.
Publication language:english
Original title:Verification of Asynchronous and Parametrized Hardware Designs
Title (cs):Verifikace asynchronních a parametrických návrhů hardware
Pages:124
Place:Brno, CZ
Year:2010
Publisher:Department of Intelligent Systems FIT BUT
Files: 
+Type Name +Title Size Modified
iconphdthesis.pdfdisertace743 KB2010-12-17 15:27:31
^ Select all
With selected:
Keywords
Formal verification, modelling hardware design, clock domain crossing, parametrized hardware design, counter automata.
Annotation
In this thesis, 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.
BibTeX:
@PHDTHESIS{
   author = {Aleš Smrčka},
   title = {Verification of Asynchronous and Parametrized Hardware
	Designs},
   pages = {124},
   year = {2010},
   location = {Brno, CZ},
   publisher = {Department of Intelligent Systems FIT BUT},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=9435}
}

Your IPv4 address: 54.83.230.137
Switch to IPv6 connection

DNSSEC [dnssec]