Detail produktu

Framework for Formal Verification of Clock Domain Crossing

Vznik: 2010

Název česky
Framework pro formální verifikaci asynchronních komponent
Typ
software
Licence
vyžadována - zdarma
Autoři
Klíčová slova

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

Popis

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.

Umístění
Licence

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

Soubory
Projekty
Výzkumné skupiny
Pracoviště
Nahoru