Publication detail
Verifying VHDL Design with Multiple Clocks in SMV
SMRČKA, A. ŘEHÁK, V. VOJNAR, T. ŠAFRÁNEK, D. MATOUŠEK, P. ŘEHÁK, Z.
Original Title
Verifying VHDL Design with Multiple Clocks in SMV
Type
conference paper
Language
English
Original Abstract
The paper considers the problem of model checking real-life VHDL-basedhardware designs via their automated transformation to a modelverifiable using the SMV model checker. In particular, model checkingof asynchronous designs, ie. designs driven by multiple clocks, isdiscussed. Two original approaches to compiling asynchronous VHDLdesigns to the SMV language such that errors possibly arising from theasynchronicity are preserved are proposed. The paper also presentsresults of experiments with using the proposed methods for verificationof several real-life asynchronous components of an FPGA-based routerbeing developed within the Liberouter project.
Keywords
model checking, hardware, VHDL, multiple clocks, SMV
Authors
SMRČKA, A.; ŘEHÁK, V.; VOJNAR, T.; ŠAFRÁNEK, D.; MATOUŠEK, P.; ŘEHÁK, Z.
RIV year
2007
Released
16. 7. 2007
Publisher
Springer Verlag
Location
Bonn
ISBN
978-3-540-70951-0
Book
Formal Methods: Applications and Technology
Edition
Lecture Notes in Computer Science 4346
ISBN
0302-9743
Periodical
Lecture Notes in Computer Science
Year of study
2007
Number
4346
State
Federal Republic of Germany
Pages from
148
Pages to
164
Pages count
16
BibTex
@inproceedings{BUT30749,
author="Aleš {Smrčka} and Vojtěch {Řehák} and Tomáš {Vojnar} and David {Šafránek} 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"
}