Detail publikace

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. Verifying VHDL Design with Multiple Clocks in SMV. Proceedings of FMICS 2006. Bonn: 2006. p. 140-155.

Název česky

Typ

konferenční sborník (ne článek)

Jazyk

anglicky

Autoři

Smrčka Aleš, Ing., Ph.D. (UITS)
Řehák Vojtěch, doc. RNDr.
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
Šafránek David, doc. RNDr., Ph.D.
Matoušek Petr, doc. Ing., Ph.D., M.A. (UIFS)
Řehák Zdeněk

URL

http://www.fit.vutbr.cz/~smrcka/pub/MulClks-FMICS06.pdf PDF

Klíčová slova

model checking, hardware, VHDL, multiple clocks, SMV

Abstrakt

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.

Rok

2006

Strany

140–155

Kniha

Proceedings of FMICS 2006

Konference

Formal Methods for Industrial Critical Systems, Bonn, DE

Místo

Bonn

BibTeX

@proceedings{BUT22281,
  editor="Aleš {Smrčka} and Vojtěch {Řehák} and Tomáš {Vojnar} and David {Šafránek} and Petr {Matoušek} and Zdeněk {Řehák}",
  title="Verifying VHDL Design with Multiple Clocks in SMV",
  year="2006",
  pages="140--155",
  address="Bonn"
}