Detail publikačního výsledku

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.

Originální název

Verifying VHDL Design with Multiple Clocks in SMV

Anglický název

Verifying VHDL Design with Multiple Clocks in SMV

Druh

Konferenční sborník (ne stať)

Originální 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, 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.

Anglický 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, 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.

Klíčová slova

model checking, hardware, VHDL, multiple clocks, SMV

Klíčová slova v angličtině

model checking, hardware, VHDL, multiple clocks, SMV

Autoři

SMRČKA, A.; ŘEHÁK, V.; VOJNAR, T.; ŠAFRÁNEK, D.; MATOUŠEK, P.; ŘEHÁK, Z.

Vydáno

26.08.2006

Místo

Bonn

Kniha

Proceedings of FMICS 2006

Strany od

140

Strany do

155

Strany počet

16

Plný text v Digitální knihovně

http://hdl.handle.net/

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"
}