Framework for Formal Verification of Clock Domain Crossing

Kód výsledku v IS VaVaI

<a href="https://www.isvavai.cz/riv?ss=detail&h=RIV%2F00216305%3A26230%2F10%3APR25258" target="_blank" >RIV/00216305:26230/10:PR25258 - isvavai.cz</a>

Výsledek na webu

—

DOI - Digital Object Identifier

—

Jazyk výsledku

angličtina

Název v původním jazyce

Framework for Formal Verification of Clock Domain Crossing

Popis výsledku v původním jazyce

Conventional technique of hardware design formal verification is based on modelling zero-delay changes of signal value. Unfortunatelly, this type of abstraction hides the problem of clock domain crossings (CDCs) which cause is either in metastability orin a synchronization protocol design. CDCreloaded is a framework which gathers all one need for formal verification and analysis of hardware designs including asynchronous components. The framework consists of several components including (i) the tool cdcreveal for detection and extending of parts of a design prone to CDC problems, (ii) the tool envgen for generating an environment of a verified component, and (iii) the tool for niCE for building a filtered content of a counter-example to make the analysis of a discovered fault easier for a QA engineer.

Název v anglickém jazyce

Framework for Formal Verification of Clock Domain Crossing

Popis výsledku anglicky

Conventional technique of hardware design formal verification is based on modelling zero-delay changes of signal value. Unfortunatelly, this type of abstraction hides the problem of clock domain crossings (CDCs) which cause is either in metastability orin a synchronization protocol design. CDCreloaded is a framework which gathers all one need for formal verification and analysis of hardware designs including asynchronous components. The framework consists of several components including (i) the tool cdcreveal for detection and extending of parts of a design prone to CDC problems, (ii) the tool envgen for generating an environment of a verified component, and (iii) the tool for niCE for building a filtered content of a counter-example to make the analysis of a discovered fault easier for a QA engineer.

Druh

R - Software

CEP obor

IN - Informatika

OECD FORD obor

—

Projekt

<a href="/cs/project/GAP103%2F10%2F0306" target="_blank" >GAP103/10/0306: Statická a dynamická verifikace programů s pokročilými rysy paralelismu a neomezenosti</a><br>

Návaznosti

Z - Vyzkumny zamer (s odkazem do CEZ)

Rok uplatnění

2010

Kód důvěrnosti údajů

S - Úplné a pravdivé údaje o projektu nepodléhají ochraně podle zvláštních právních předpisů

Interní identifikační kód produktu

cdcreloaded

Technické parametry

Volně šiřitelný software poskytovaný pod licencí GNU GPL v3, její znění je na http://www.gnu.org/licenses/gpl-3.0.txt. Čtyři nástroje v objektově-orientovaném návrhu v jazyku Python (verze vyšší nebo rovno 2.5 a nižší než 3.0) s ot

Ekonomické parametry

—

IČO vlastníka výsledku

00216305

Název vlastníka

Vysoké učení technické v Brně