Conference paper

SMRČKA Aleš, ŘEHÁK Vojtěch, VOJNAR Tomáš, ŠAFRÁNEK David, MATOUŠEK Petr and ŘEHÁK Zdeněk. Verifying VHDL Design with Multiple Clocks in SMV. In: Formal Methods: Applications and Technology. Bonn: Springer Verlag, 2007, pp. 148-164. ISSN 0302-9743.
Publication language:english
Original title:Verifying VHDL Design with Multiple Clocks in SMV
Title (cs):Verifikace návrhu VHDL s více hodinami v SMV
Pages:148-164
Proceedings:Formal Methods: Applications and Technology
Conference:FMICS06
Series:Lecture Notes in Computer Science 4346
Place:Bonn, DE
Year:2007
Journal:Lecture Notes in Computer Science, Vol. 2007, No. 4346, DE
ISSN:0302-9743
Publisher:Springer Verlag
URL:http://www.fit.vutbr.cz/~smrcka/pub/fmics06.pdf [PDF]
Keywords
model checking, hardware, VHDL, multiple clocks, SMV
Annotation
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.
Abstract
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{\v{s}} Smr{\v{c}}ka and Vojt{\v{e}}ch {\v{R}}eh{\'{a}}k
	and Tom{\'{a}}{\v{s}} Vojnar and David {\v{S}}afr{\'{a}}nek
	and Petr Matou{\v{s}}ek and Zden{\v{e}}k {\v{R}}eh{\'{a}}k},
   title = {Verifying VHDL Design with Multiple Clocks in SMV},
   pages = {148--164},
   booktitle = {Formal Methods: Applications and Technology},
   series = {Lecture Notes in Computer Science 4346},
   journal = {Lecture Notes in Computer Science},
   volume = {2007},
   number = {4346},
   year = {2007},
   location = {Bonn, DE},
   publisher = {Springer Verlag},
   ISSN = {0302-9743},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php?id=8371}
}

Your IPv4 address: 54.145.85.87
Switch to IPv6 connection

DNSSEC [dnssec]