Publication Details

Verifying VHDL Design with Multiple Clocks in SMV

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. Lecture Notes in Computer Science, vol. 4346. Bonn: Springer Verlag, 2007, pp. 148-164. ISSN 0302-9743.
Czech title
Verifikace návrhu VHDL s více hodinami v SMV
Type
conference paper
Language
english
Authors
Smrčka Aleš, Ing., Ph.D. (DITS FIT BUT)
Řehák Vojtěch, doc. RNDr. (FI MUNI)
Vojnar Tomáš, prof. Ing., Ph.D. (DITS FIT BUT)
Šafránek David, doc. Mgr., Ph.D. (FI MUNI)
Matoušek Petr, doc. Ing., Ph.D., M.A. (DIFS FIT BUT)
Řehák Zdeněk (FI MUNI)
URL
Keywords

model checking, hardware, VHDL, multiple clocks, SMV

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.

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.

Published
2007
Pages
148-164
Journal
Lecture Notes in Computer Science, vol. 4346, ISSN 0302-9743
Proceedings
Formal Methods: Applications and Technology
Series
Lecture Notes in Computer Science
Conference
FMICS06, Bonn, DE
Publisher
Springer Verlag
Place
Bonn, DE
BibTeX
@INPROCEEDINGS{FITPUB8371,
   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",
   journal = "Lecture Notes in Computer Science",
   volume = 4346,
   year = 2007,
   location = "Bonn, DE",
   publisher = "Springer Verlag",
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/8371"
}
Back to top