Článek ve sborníku konference

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. Bonn: Springer Verlag, 2007, s. 148-164. ISSN 0302-9743.
Jazyk publikace:angličtina
Název publikace:Verifying VHDL Design with Multiple Clocks in SMV
Název (cs):Verifikace návrhu VHDL s více hodinami v SMV
Strany:148-164
Sborník:Formal Methods: Applications and Technology
Konference:FMICS06
Řada knih:Lecture Notes in Computer Science 4346
Místo vydání:Bonn, DE
Rok:2007
Časopis:Lecture Notes in Computer Science, roč. 2007, č. 4346, DE
ISSN:0302-9743
Vydavatel:Springer Verlag
URL:http://www.fit.vutbr.cz/~smrcka/pub/fmics06.pdf [PDF]
Klíčová slova
model checking, hardware, VHDL, multiple clocks, SMV
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.
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.
BibTeX:
@INPROCEEDINGS{
   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 4346},
   journal = {Lecture Notes in Computer Science},
   volume = {2007},
   number = {4346},
   year = {2007},
   location = {Bonn, DE},
   publisher = {Springer Verlag},
   ISSN = {0302-9743},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php.cs?id=8371}
}

Vaše IPv4 adresa: 3.91.79.74
Přepnout na https

DNSSEC [dnssec]