Framework for Formal Verification of Clock Domain Crossing |
| Authors: | Smrčka Aleš, Vojnar Tomáš |
|---|
| Type: | software |
| Created: | 2010 |
| Licence: | required - no fee | | Files: | |
|---|
|
| | Keywords: | clock-domain crossing, formal verification, environment specification |
| 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. |
| Location: |
|---|
| http://www.fit.vutbr.cz/~smrcka/w/doku.php?id=research:cdcreloaded |
| Research groups: |
|---|
|
| Departments: |
|---|
|
| Licence terms: |
|---|
| Free software under the terms of the GNU GPL v3 license. |
|
Faculty of Information Technology
![[dnssec]](/common/img/dnssec.png)