| SMRČKA, Aleš, Vojtěch ŘEHÁK, Tomáš VOJNAR, David ŠAFRÁNEK, Petr MATOUŠEK and Zdeněk ŘEHÁK. Verifying VHDL Designs with Multiple Clocks in SMV. In Formal Methods Applications and Technology, 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006, and 5th International Workshop on Parallel and Distributed Methods in Verification, PDMC 2006. Bonn: Springer-Verlag. p. 148-164, 16 pp. ISBN 978-3-540-70951-0. 2007. |
Other formats:
BibTeX
LaTeX
RIS
@inproceedings{639264,
author = {Smrčka, Aleš and Řehák, Vojtěch and Vojnar, Tomáš and Šafránek, David and Matoušek, Petr and Řehák, Zdeněk},
address = {Bonn},
booktitle = {Formal Methods Applications and Technology, 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006, and 5th International Workshop on Parallel and Distributed Methods in Verification, PDMC 2006},
keywords = {formal verification; model checking; VHDL; asynchronous clock domains},
language = {eng},
location = {Bonn},
isbn = {978-3-540-70951-0},
pages = {148-164},
publisher = {Springer-Verlag},
title = {Verifying VHDL Designs with Multiple Clocks in SMV},
year = {2007}
}
TY - JOUR
ID - 639264
AU - Smrčka, Aleš - Řehák, Vojtěch - Vojnar, Tomáš - Šafránek, David - Matoušek, Petr - Řehák, Zdeněk
PY - 2007
TI - Verifying VHDL Designs with Multiple Clocks in SMV
PB - Springer-Verlag
CY - Bonn
SN - 9783540709510
KW - formal verification
KW - model checking
KW - VHDL
KW - asynchronous clock domains
N2 - 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, i.e. 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.
ER -
SMRČKA, Aleš, Vojtěch ŘEHÁK, Tomáš VOJNAR, David ŠAFRÁNEK, Petr MATOUŠEK and Zdeněk ŘEHÁK. Verifying VHDL Designs with Multiple Clocks in SMV. In \textit{Formal Methods Applications and Technology, 11th International Workshop on Formal Methods for Industrial Critical Systems, FMICS 2006, and 5th International Workshop on Parallel and Distributed Methods in Verification, PDMC 2006}. Bonn: Springer-Verlag. p.~148-164, 16 pp. ISBN~978-3-540-70951-0. 2007.
|
