Detail publikace

Verifying VHDL Design with Multiple Clocks in SMV

SMRČKA Aleš, ŘEHÁK Vojtěch, VOJNAR Tomáš, ŠAFRÁNEK David, MATOUŠEK Petr a ŘEHÁK Zdeněk. Verifying VHDL Design with Multiple Clocks in SMV. In: Formal Methods: Applications and Technology. Lecture Notes in Computer Science, roč. 4346. Bonn: Springer Verlag, 2007, s. 148-164. ISSN 0302-9743.
Název česky
Verifikace návrhu VHDL s více hodinami v SMV
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT)
Řehák Vojtěch, doc. RNDr. (FI MUNI)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Šafránek David, doc. Mgr., Ph.D. (FI MUNI)
Matoušek Petr, doc. Ing., Ph.D., M.A. (UIFS FIT VUT)
Řehák Zdeněk (FI MUNI)
URL
Abstrakt

Č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.

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č. 4346, ISSN 0302-9743
Sborník
Formal Methods: Applications and Technology
Řada
Lecture Notes in Computer Science
Konference
FMICS06, Bonn, DE
Vydavatel
Springer Verlag
Místo
Bonn, DE
BibTeX 
@INPROCEEDINGS{FITPUB8371,
   author = "Ale\v{s} Smr\v{c}ka and Vojt\v{e}ch \v{R}eh\'{a}k and Tom\'{a}\v{s} Vojnar and David \v{S}afr\'{a}nek and Petr Matou\v{s}ek and Zden\v{e}k \v{R}eh\'{a}k",
   title = "Verifying VHDL Design with Multiple Clocks in SMV",
   pages = "148--164",
   booktitle = "Formal Methods: Applications and Technology",
   series = "Lecture Notes in Computer Science",
   journal = "Lecture Notes in Computer Science",
   volume = 4346,
   year = 2007,
   location = "Bonn, DE",
   publisher = "Springer Verlag",
   ISSN = "0302-9743",
   language = "english",
   url = "https://www.fit.vut.cz/research/publication/8371"
}
Nahoru