Detail 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. Verifying VHDL Design with Multiple Clocks in SMV. In Formal Methods: Applications and Technology. Lecture Notes in Computer Science. Lecture Notes in Computer Science 4346. Bonn: Springer Verlag, 2007. no. 4346, p. 148-164. ISBN: 978-3-540-70951-0. ISSN: 0302-9743.
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Smrčka Aleš, Ing., Ph.D., FIT (FIT), UITS (FIT)
Řehák Vojtěch, doc. RNDr.
Vojnar Tomáš, prof. Ing., Ph.D., UITS (FIT)
Šafránek David
Šafránek David, doc. RNDr., Ph.D.
Matoušek Petr, doc. Ing., Ph.D., M.A., UIFS (FIT)
Řehák Zdeněk
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, 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.

Klíčová slova

model checking, hardware, VHDL, multiple clocks, SMV

URL
Anotace

Článek popisuje problém užití metody model checking reálného návrhu hardware ve VHDL pomocí automatizované transformace do verifikovatelného modelu a následné verifikace pomocí SMV nástroje. Konkrétně je uvažován model checking asynchronních návrhů tj. návrhů řízené více než jedněmi hodinami. Jsou navrženy dva originální přístupy k překladu asynchronního návrhu ve VHDL do jazyka SMV. Navržený překlad je bezpečný vůči chybám, které mohou být způsobeny asynchronní povahou návrhu. Článek také prezentuje výsledky experimentů pomocí navržených metod na několika reálných asynchronních komponentách směrovače založeného na FPGA vyvíjeného v rámci projektu Liberouter.

Rok
2007
Strany
148–164
Časopis
Lecture Notes in Computer Science, roč. 2007, č. 4346, ISSN 0302-9743
Sborník
Formal Methods: Applications and Technology
Řada
Lecture Notes in Computer Science 4346
Konference
FMICS06
ISBN
978-3-540-70951-0
Vydavatel
Springer Verlag
Místo
Bonn
BibTeX 
@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"
}
Projekty
Automatizované metody a nástroje pro vývoj spolehlivých paralelních a distribuovaných systémů, GAČR, Standardní projekty, GA102/04/0780, zahájení: 2004-01-01, ukončení: 2006-12-31, ukončen
Optická síť národního výzkumu a její nové aplikace, MŠMT, Výzkumná centra (2000-2004), MSM6383917201, zahájení: 2004-01-01, ukončení: 2010-12-31, ukončen
Rámec pro formální specifikace a prototypování síťových aplikací informačních systémů, GAČR, Standardní projekty, GA102/05/0723, zahájení: 2005-01-01, ukončení: 2007-12-31, ukončen
Výzkum informačních technologií z hlediska bezpečnosti, MŠMT, Institucionální prostředky SR ČR (např. VZ, VC), MSM0021630528, zahájení: 2007-01-01, ukončení: 2013-12-31, řešení
Výzkumné skupiny
Výzkumná skupina automatizované analýzy a verifikace - VeriFIT (VZ VERIFIT)
Pracoviště
Ústav informačních systémů (UIFS)
Ústav inteligentních systémů (UITS)
Nahoru