Článek ve sborníku konference

 
Smrčka, A., Řehák, V., Vojnar, T., Šafránek, D., Matoušek, P., Řehák, Z.: Verifying VHDL Design with Multiple Clocks in SMV, In: Proceedings of FMICS 2006, Bonn, DE, 2006, s. 140-155
Jazyk publikace:angličtina
Název publikace:Verifying VHDL Design with Multiple Clocks in SMV
Název (cs):Verifying VHDL Design with Multiple Clocks in SMV
Strany:140-155
Sborník:Proceedings of FMICS 2006
Konference:Formal Methods for Industrial Critical Systems
Místo vydání:Bonn, DE
Rok:2006
URL:http://www.fit.vutbr.cz/~smrcka/pub/MulClks-FMICS06.pdf [PDF]
Klíčová slova
model checking, hardware, VHDL, multiple clocks, SMV
Anotace
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.
BibTeX:
@INPROCEEDINGS{
   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},
   pages = {140--155},
   booktitle = {Proceedings of FMICS 2006},
   year = {2006},
   location = {Bonn, DE},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=8205}
}