Detail publikace

Verifying VHDL Design with Multiple Clocks in SMV

SMRČKA Aleš, ŘEHÁK Vojtěch, VOJNAR Tomáš, ŠAFRÁNEK David, MATOUŠEK Petr a ŘEHÁK Zdeněk. Verifying VHDL Design with Multiple Clocks in SMV. In: Proceedings of FMICS 2006. Bonn, 2006, s. 140-155.
Název česky
Verifying VHDL Design with Multiple Clocks in SMV
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT)
Řehák Vojtěch, doc. RNDr. (FI MUNI)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Šafránek David, doc. Mgr., Ph.D. (FI MUNI)
Matoušek Petr, doc. Ing., Ph.D., M.A. (UIFS FIT VUT)
Řehák Zdeněk (FI MUNI)
URL
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.

Rok
2006
Strany
140-155
Sborník
Proceedings of FMICS 2006
Konference
Formal Methods for Industrial Critical Systems, Bonn, DE
Místo
Bonn, DE
BibTeX
@INPROCEEDINGS{FITPUB8205,
   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 = "140--155",
   booktitle = "Proceedings of FMICS 2006",
   year = 2006,
   location = "Bonn, DE",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/8205"
}
Nahoru