Detail publikace

Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description

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
Název česky
Automatické formální ověření shody ISA a RTL návrhu mikroprocesoru
Typ
článek ve sborníku konference
Jazyk
angličtina
Autoři
URL
Abstrakt

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

Rok
2012
Strany
6-12
Sborník
Proceedings of the 13th International Workshop on Microprocessor Test and Verification (MTV 2012)
Konference
Microprocessor Test and Verification 2012, Austin, TX, US
ISBN
978-1-4673-4441-8
Vydavatel
Institute of Electrical and Electronics Engineers
Místo
Austin, TX, US
DOI
BibTeX
@INPROCEEDINGS{FITPUB10135,
   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 = "https://www.fit.vut.cz/research/publication/10135"
}
Soubory
Nahoru