MonographSMRČKA Aleš and VOJNAR Tomáš. Verification of Asynchronous and Parametrized Hardware Designs. Brno: Faculty of Information Technology BUT, 2010. ISBN 9788021442146.  Publication language:  english 

Original title:  Verification of Asynchronous and Parametrized Hardware Designs 

Title (cs):  Verifikace asynchronních a parametrických návrhů hardware 

Pages:  115 

Series:  FIT Monograph 

Place:  Brno, CZ 

Year:  2010 

ISBN:  9788021442146 

Publisher:  Faculty of Information Technology BUT 

Keywords 

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

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: 

@BOOK{
author = {Ale{\v{s}} Smr{\v{c}}ka and Tom{\'{a}}{\v{s}} Vojnar},
title = {Verification of Asynchronous and Parametrized Hardware
Designs},
pages = {115},
series = {FIT Monograph},
year = {2010},
location = {Brno, CZ},
publisher = {Faculty of Information Technology BUT},
ISBN = {9788021442146},
language = {english},
url = {http://www.fit.vutbr.cz/research/view_pub.php.en.iso88592?id=9454}
} 
