About: Framework for Formal Verification of Clock Domain Crossing

Facets (new session)
Description
Metadata
Settings
- owl:sameAs
- Inference Rule:

About: Framework for Formal Verification of Clock Domain Crossing Goto Sponge NotDistinct Permalink

An Entity of Type : http://linked.opendata.cz/ontology/domain/vavai/Vysledek, within Data Space : linked.opendata.cz associated with source document(s)

Attributes	Values
rdf:type	skos:Concept http://linked.opendata.cz/ontology/domain/vavai/Vysledek
rdfs:seeAlso	http://www.fit.vutbr.cz/~smrcka/w/doku.php?id=research:cdcreloaded
Description	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 or in 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. 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 or in 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. (en)
Title	Framework for Formal Verification of Clock Domain Crossing Framework for Formal Verification of Clock Domain Crossing (en)
skos:prefLabel	Framework for Formal Verification of Clock Domain Crossing Framework for Formal Verification of Clock Domain Crossing (en)
skos:notation	RIV/00216305:26230/10:PR25258!RIV12-GA0-26230___
http://linked.open...avai/riv/aktivita	P Z
http://linked.open...avai/riv/aktivity	P(GAP103/10/0306), Z(MSM0021630528)
http://linked.open...vai/riv/dodaniDat	2012
http://linked.open...aciTvurceVysledku	Vojnar, Tomáš Smrčka, Aleš
http://linked.open.../riv/druhVysledku	R - Software
http://linked.open...iv/duvernostUdaju	S - Úplné a pravdivé údaje nepodléhající ochraně podle zvláštních právních předpisů
http://linked.open...onomickeParametry	Volně šiřitelný software poskytovaný pod licencí GNU GPL v3.
http://linked.open...titaPredkladatele	Vysoké učení technické v Brně / Fakulta informačních technologií
http://linked.open...dnocenehoVysledku	259731
http://linked.open...ai/riv/idVysledku	RIV/00216305:26230/10:PR25258
http://linked.open...terniIdentifikace	cdcreloaded
http://linked.open...riv/jazykVysledku	eng - angličtina
http://linked.open.../riv/klicovaSlova	clock-domain crossing, formal verification, environment specification (en)
http://linked.open.../riv/klicoveSlovo	formal verification clock-domain crossing environment specification
http://linked.open...ontrolniKodProRIV	[FF9A0DF2B977]
http://linked.open.../licencniPoplatek	N - Poskytovatel licence na výsledek nepožaduje licenční poplatek
http://linked.open...okalizaceVysledku	http://www.fit.vutbr.cz/~smrcka/w/doku.php?id=research:cdcreloaded
http://linked.open...in/vavai/riv/obor	IN
http://linked.open...ichTvurcuVysledku	2 (xsd:int)
http://linked.open...cetTvurcuVysledku	2 (xsd:int)
http://linked.open...vavai/riv/projekt	Static and Dynamic Verification of Programs with Advanced Features of Concurrency and Unboundedness
http://linked.open...UplatneniVysledku	2010
http://linked.open...echnickeParametry	Č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 otevřeným kódem. Nástroje slouží jako rozhraní příkazové řádky ke knihovnám implementující danou funkci. Programy a knihovny jsou použitelné pro všechny platformy podporující interpret jazyka Python. Rozsah všech zdrojových kódů včetně testů je cca 9 tisíc řádků. Volně šiřitelný software poskytovaný pod licencí GNU GPL v3, její znění je na http://www.gnu.org/licenses/gpl-3.0.txt.
http://linked.open...iv/tvurceVysledku	Vojnar, Tomáš Smrčka, Aleš
http://linked.open...avai/riv/vlastnik	Vysoké učení technické v Brně
http://linked.open...itiJinymSubjektem	A - Nabytí licence je nutné vždy
http://linked.open...n/vavai/riv/zamer	Výzkum informačních technologií z hlediska bezpečnosti
http://localhost/t...ganizacniJednotka	26230
is http://linked.open...avai/riv/vysledek of	Framework for Formal Verification of Clock Domain Crossing Framework for Formal Verification of Clock Domain Crossing

Faceted Search & Find service v1.16.118 as of Jun 21 2024

Alternative Linked Data Documents: ODE Content Formats:

RDF

ODATA

Microdata

About

OpenLink Virtuoso version 07.20.3240 as of Jun 21 2024, on Linux (x86_64-pc-linux-gnu), Single-Server Edition (126 GB total memory, 47 GB memory in use)
Data on this page belongs to its respective rights holders.
Virtuoso Faceted Browser Copyright © 2009-2024 OpenLink Software