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.

Originální název

Verifying VHDL Design with Multiple Clocks in SMV

Typ

článek ve sborníku ve WoS nebo Scopus

Jazyk

angličtina

Originální abstrakt

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.

Klíčová slova

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.

Rok RIV

2007

Vydáno

16. 7. 2007

Nakladatel

Springer Verlag

Místo

Bonn

ISBN

978-3-540-70951-0

Kniha

Formal Methods: Applications and Technology

Edice

Lecture Notes in Computer Science 4346

ISSN

0302-9743

Periodikum

Lecture Notes in Computer Science

Ročník

2007

Číslo

4346

Stát

Spolková republika Německo

Strany od

148

Strany do

164

Strany počet

16

BibTex

@inproceedings{BUT30749,
  author="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",
  booktitle="Formal Methods: Applications and Technology",
  year="2007",
  series="Lecture Notes in Computer Science 4346",
  journal="Lecture Notes in Computer Science",
  volume="2007",
  number="4346",
  pages="148--164",
  publisher="Springer Verlag",
  address="Bonn",
  isbn="978-3-540-70951-0",
  issn="0302-9743"
}