Framework for Formal Verification of Clock Domain Crossing

křížení časových domén, formální verifikace, specifikace okolí

Konvenční přístup formální verifikace návrhů hardware je založen na modelování nulového zpoždění při změně hodnot řídicích signálů. Taková abstrakce však skrývá možné problémy vznikající v křížení časových domén (CDC), jejichž kořeny spočívají buď v metastabilitě signálů nebo ve špatném návrhu synchronizačního protokolu. CDCreloaded je framework sdružující vše, co je potřeba pro formální verifikaci a analýzu návrhů hardware včetně asynchronních komponent. Framework se skládá z několika komponent: (i) nástroje cdcreveal pro detekci a rozšíření částí návrhu, které jsou citlivé na problémy týkající se CDC, (ii) nástroje envgen pro generování prostředí verifikované komponenty a (iii) nástroje niCE pro tvorbu filtrovaného obsahu z poskytnutého protipříkladu pro ulehčení analýzy objevené chyby.

http://www.fit.vutbr.cz/~smrcka/w/doku.php?id=research:cdcreloaded

Volně šiřitelný software poskytovaný pod licencí GNU GPL v3.