Článek ve sborníku konference

CHARVÁT Lukáš, SMRČKA Aleš a VOJNAR Tomáš. Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description. In: Proceedings of the 13th International Workshop on Microprocessor Test and Verification (MTV 2012). Austin, TX: Institute of Electrical and Electronics Engineers, 2012, s. 6-12. ISBN 978-1-4673-4441-8. Dostupné z: http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6519727
Jazyk publikace:angličtina
Název publikace:Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description
Název (cs):Automatické formální ověření shody ISA a RTL návrhu mikroprocesoru
Strany:6-12
Sborník:Proceedings of the 13th International Workshop on Microprocessor Test and Verification (MTV 2012)
Konference:Microprocessor Test and Verification 2012
Místo vydání:Austin, TX, US
Rok:2012
URL:http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6519727
ISBN:978-1-4673-4441-8
DOI:10.1109/MTV.2012.19
Vydavatel:Institute of Electrical and Electronics Engineers
Soubory: 
+Typ Jméno Název Vel. Poslední změna
iconmtv12.pdf181 KB2012-09-08 22:15:53
^ Vybrat vše
S vybranými:
Klíčová slova
automatic formal verification, correspondence checking, ISA, microprocessor, instruction, RTL, bounded model checking
Anotace
Článek navrhuje automatický přístup na formální bázi navržený pro ověření shody mezi RTL implementací mikroprocesoru a popisu jeho architektury instrukční sady (ISA). Cíli návrhu jsou hledání chyb neobjevených funkční verifikací, minimální intervence uživatele v procesu verifikace a poskytnutí praktických výsledků vývojáři v krátkém čase. Hlavní myšlenkou je použití omezeného model checkingu ke kontrole, že výsledek produkovaný automaticky z modelů RTL a ISA daného procesoru je stejný pro každou instrukci a každý možný vstup. Ačkoliv přístup neposkytuje plnou formální verifikaci, experimenty s ním potvrzují, že díky jinému způsobu prozkoumání stavového prostoru testovaného návrhu je možné najít chyby nenalezené funkční verifikací, a je to tedy úspěšný doplněk k funkční verifikaci.
BibTeX:
@INPROCEEDINGS{
   author = {Luk{\'{a}}{\v{s}} Charv{\'{a}}t and Ale{\v{s}}
	Smr{\v{c}}ka and Tom{\'{a}}{\v{s}} Vojnar},
   title = {Automatic Formal Correspondence Checking of ISA
	and RTL Microprocessor Description},
   pages = {6--12},
   booktitle = {Proceedings of the 13th International Workshop on
	Microprocessor Test and Verification (MTV 2012)},
   year = {2012},
   location = {Austin, TX, US},
   publisher = {Institute of Electrical and Electronics Engineers},
   ISBN = {978-1-4673-4441-8},
   doi = {10.1109/MTV.2012.19},
   language = {english},
   url = {http://www.fit.vutbr.cz/research/view_pub.php.cs?id=10135}
}

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