Automatic Formal Correspondence Checking of ISA and RTL Microprocessor Description

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

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