Verification of Asynchronous and Parametrized Hardware Designs
Aleö Smr · 2010
Two original approaches to formal verication of hardware designs are introduced. In particular, we aim at model checking of circuits with multiple clocks and verication 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 dier in their precision and the incurred verication cost. In the latter contribution, our proposed approach of verication 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 verication. A parametrized hardware design translated to a counter automaton can be veried for all possible values of parameters at once.