Attributes | Values |
---|
rdf:type
| |
rdfs:seeAlso
| |
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
| |
http://linked.open...avai/riv/aktivity
| - P(GAP103/10/0306), Z(MSM0021630528)
|
http://linked.open...vai/riv/dodaniDat
| |
http://linked.open...aciTvurceVysledku
| |
http://linked.open.../riv/druhVysledku
| |
http://linked.open...iv/duvernostUdaju
| |
http://linked.open...onomickeParametry
| - Volně šiřitelný software poskytovaný pod licencí GNU GPL v3.
|
http://linked.open...titaPredkladatele
| |
http://linked.open...dnocenehoVysledku
| |
http://linked.open...ai/riv/idVysledku
| - RIV/00216305:26230/10:PR25258
|
http://linked.open...terniIdentifikace
| |
http://linked.open...riv/jazykVysledku
| |
http://linked.open.../riv/klicovaSlova
| - clock-domain crossing, formal verification, environment specification (en)
|
http://linked.open.../riv/klicoveSlovo
| |
http://linked.open...ontrolniKodProRIV
| |
http://linked.open.../licencniPoplatek
| |
http://linked.open...okalizaceVysledku
| |
http://linked.open...in/vavai/riv/obor
| |
http://linked.open...ichTvurcuVysledku
| |
http://linked.open...cetTvurcuVysledku
| |
http://linked.open...vavai/riv/projekt
| |
http://linked.open...UplatneniVysledku
| |
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
| |
http://linked.open...itiJinymSubjektem
| |
http://linked.open...n/vavai/riv/zamer
| |
http://localhost/t...ganizacniJednotka
| |