Verification of Asynchronous and Parametrized Hardware Designs
The result's identifiers
Result code in IS VaVaI
<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F10%3APU91969" target="_blank" >RIV/00216305:26230/10:PU91969 - isvavai.cz</a>
Result on the web
—
DOI - Digital Object Identifier
—
Alternative languages
Result language
angličtina
Original language name
Verification of Asynchronous and Parametrized Hardware Designs
Original language description
Two original approaches to formal verification of hardware designs are introduced. 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 onexploiting 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.
Czech name
—
Czech description
—
Classification
Type
J<sub>x</sub> - Unclassified - Peer-reviewed scientific article (Jimp, Jsc and Jost)
CEP classification
JC - Computer hardware and software
OECD FORD branch
—
Result continuities
Project
<a href="/en/project/GAP103%2F10%2F0306" target="_blank" >GAP103/10/0306: Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness</a><br>
Continuities
Z - Vyzkumny zamer (s odkazem do CEZ)<br>S - Specificky vyzkum na vysokych skolach
Others
Publication year
2010
Confidentiality
S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů
Data specific for result type
Name of the periodical
Information Sciences and Technologies Bulletin of the ACM Slovakia
ISSN
1338-1237
e-ISSN
—
Volume of the periodical
2
Issue of the periodical within the volume
2
Country of publishing house
SK - SLOVAKIA
Number of pages
10
Pages from-to
60-69
UT code for WoS article
—
EID of the result in the Scopus database
—