Verifying VHDL Design with Multiple Clocks in SMV

Verifikace návrhu VHDL s více hodinami v SMV

conference paper

English

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

• http://www.fit.vutbr.cz/~smrcka/pub/fmics06.pdf PDF

model checking, hardware, VHDL, multiple clocks, SMV

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.

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.

2007

148–164

Lecture Notes in Computer Science, vol. 2007, no. 4346, ISSN 0302-9743

Formal Methods: Applications and Technology

Lecture Notes in Computer Science 4346

978-3-540-70951-0

Springer Verlag

Bonn