Detail publikace
Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description
Smrčka Aleš, Ing., Ph.D. (UITS FIT VUT)
Vojnar Tomáš, prof. Ing., Ph.D. (UITS FIT VUT)
Č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.
@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" }