Detail publikace

Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description

CHARVÁT, L.; SMRČKA, A.; VOJNAR, T. Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description. Proceedings of the 13th International Workshop on Microprocessor Test and Verification (MTV 2012). Austin, TX: Institute of Electrical and Electronics Engineers, 2012. p. 6-12. ISBN: 978-1-4673-4441-8.
Název česky
Automatické formální ověření shody ISA a RTL návrhu mikroprocesoru
Typ
článek ve sborníku konference
Jazyk
anglicky
Autoři
Charvát Lukáš, Ing., Ph.D.
Smrčka Aleš, Ing., Ph.D. (UITS)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS)
URL
Klíčová slova

automatic formal verification, correspondence checking, ISA, microprocessor, instruction, RTL, bounded model checking

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)
ISBN
978-1-4673-4441-8
Vydavatel
Institute of Electrical and Electronics Engineers
Místo
Austin, TX
DOI
10.1109/MTV.2012.19
BibTeX 
@inproceedings{BUT97556,
  author="Lukáš {Charvát} and Aleš {Smrčka} and Tomáš {Vojnar}",
  title="Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description",
  booktitle="Proceedings of the 13th International Workshop on Microprocessor Test and Verification (MTV 2012)",
  year="2012",
  pages="6--12",
  publisher="Institute of Electrical and Electronics Engineers",
  address="Austin, TX",
  doi="10.1109/MTV.2012.19",
  isbn="978-1-4673-4441-8",
  url="http://ieeexplore.ieee.org/xpl/articleDetails.jsp?arnumber=6519727"
}
Nahoru