Přístupnostní navigace
E-application
Search Search Close
Publication detail
SMRČKA, A. ŘEHÁK, V. VOJNAR, T. ŠAFRÁNEK, D. MATOUŠEK, P. ŘEHÁK, Z.
Original Title
Verifying VHDL Design with Multiple Clocks in SMV
Type
conference proceedings
Language
English
Original 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.
Keywords
model checking, hardware, VHDL, multiple clocks, SMV
Authors
SMRČKA, A.; ŘEHÁK, V.; VOJNAR, T.; ŠAFRÁNEK, D.; MATOUŠEK, P.; ŘEHÁK, Z.
RIV year
2006
Released
26. 8. 2006
Location
Bonn
Pages from
140
Pages to
155
Pages count
16
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" }