Verification of Asynchronous and Parametrized Hardware Designs

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F10%3APU90556" target="_blank" >RIV/00216305:26230/10:PU90556 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Verification of Asynchronous and Parametrized Hardware Designs

Popis výsledku v původním jazyce

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 introducefour 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&nbsp; within a circuit are implicitly covered. Fourproposed 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 andon 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.

Název v anglickém jazyce

Verification of Asynchronous and Parametrized Hardware Designs

Popis výsledku anglicky

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 introducefour 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&nbsp; within a circuit are implicitly covered. Fourproposed 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 andon 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.

Druh

B - Odborná kniha

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GAP103%2F10%2F0306" target="_blank" >GAP103/10/0306: Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti</a><br>

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)<br>S - Specificky vyzkum na vysokych skolach

Rok uplatnění

2010

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

ISBN

978-80-214-4214-6

Počet stran knihy

115

Název nakladatele

Faculty of Information Technology BUT

Místo vydání

Brno

Kód UT WoS knihy

—