Result Details
Verifying VHDL Design with Multiple Clocks in SMV
Řehák Vojtěch, doc. RNDr.
Vojnar Tomáš, prof. Ing., Ph.D., DITS (FIT)
Šafránek David, doc. RNDr., Ph.D.
Šafránek David
Matoušek Petr, doc. Ing., Ph.D., M.A., DIFS (FIT)
Řehák Zdeněk
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, isdiscussed. Two original approaches to compiling asynchronous VHDLdesigns to the SMV language such that errors possibly arising from theasynchronicity are preserved are proposed. The paper also presentsresults of experiments with using the proposed methods for verificationof several real-life asynchronous components of an FPGA-based routerbeing developed within the Liberouter project.
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.
@inproceedings{BUT30749,
author="Aleš {Smrčka} and Vojtěch {Řehák} and Tomáš {Vojnar} and David {Šafránek} 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"
}Automated methods and tools supporting development of reliable parallel and distributed systems, GACR, Standardní projekty, GA102/04/0780, start: 2004-01-01, end: 2006-12-31, completed
Optická síť národního výzkumu a její nové aplikace, MŠMT, Výzkumná centra (2000-2004), MSM6383917201, start: 2004-01-01, end: 2010-12-31, completed
Security-Oriented Research in Information Technology, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, start: 2007-01-01, end: 2013-12-31, running