Přístupnostní navigace
E-přihláška
Vyhledávání Vyhledat Zavřít
Detail publikace
SMRČKA, A. ŘEHÁK, V. VOJNAR, T. ŠAFRÁNEK, D. MATOUŠEK, P. ŘEHÁK, Z.
Originální název
Verifying VHDL Design with Multiple Clocks in SMV
Typ
článek ve sborníku ve WoS nebo Scopus
Jazyk
angličtina
Originální abstrakt
The paper considers the problem of model checking real-life VHDL-based hardware designs via their automated transformation to a model verifiable using the SMV model checker. In particular, model checking of asynchronous designs, ie. designs driven by multiple clocks, is discussed. Two original approaches to compiling asynchronous VHDL designs to the SMV language such that errors possibly arising from the asynchronicity are preserved are proposed. The paper also presents results of experiments with using the proposed methods for verification of several real-life asynchronous components of an FPGA-based router being developed within the Liberouter project.
Klíčová slova
model checking, hardware, VHDL, multiple clocks, SMV
Autoři
SMRČKA, A.; ŘEHÁK, V.; VOJNAR, T.; ŠAFRÁNEK, D.; MATOUŠEK, P.; ŘEHÁK, Z.
Rok RIV
2007
Vydáno
16. 7. 2007
Nakladatel
Springer Verlag
Místo
Bonn
ISBN
978-3-540-70951-0
Kniha
Formal Methods: Applications and Technology
Edice
Lecture Notes in Computer Science 4346
ISSN
0302-9743
Periodikum
Lecture Notes in Computer Science
Ročník
Číslo
4346
Stát
Spolková republika Německo
Strany od
148
Strany do
164
Strany počet
16
BibTex
@inproceedings{BUT30749, author="Aleš {Smrčka} and Vojtěch {Řehák} and Tomáš {Vojnar} and David {Šafránek} and Petr {Matoušek} and Zdeněk {Řehák}", title="Verifying VHDL Design with Multiple Clocks in SMV", booktitle="Formal Methods: Applications and Technology", year="2007", series="Lecture Notes in Computer Science 4346", journal="Lecture Notes in Computer Science", volume="2007", number="4346", pages="148--164", publisher="Springer Verlag", address="Bonn", isbn="978-3-540-70951-0", issn="0302-9743" }