Detail publikace

Verifying VHDL Design with Multiple Clocks in SMV

Originální název

Verifying VHDL Design with Multiple Clocks in SMV

Anglický název

Verifying VHDL Design with Multiple Clocks in SMV

Jazyk

en

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.

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

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",
  annote="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.",
  address="Springer Verlag",
  booktitle="Formal Methods: Applications and Technology",
  chapter="30749",
  edition="Lecture Notes in Computer Science 4346",
  howpublished="print",
  institution="Springer Verlag",
  journal="Lecture Notes in Computer Science (IF 0,513)",
  number="4346",
  year="2007",
  month="july",
  pages="148--164",
  publisher="Springer Verlag",
  type="conference paper"
}