Name
Title | ||
|---|---|---|
Formal Verification Of Clock Domain Crossing Using Gate-Level Models Of Metastable Flip-Flops |
Abstract | ||
|---|---|---|
Verifying clock domain boundary logic is a major challenge to the design of modern multi-clock systems. We present a novel verification approach that addresses the issue of domain crossing failures at a fundamental level. The approach relies on substituting flip-flops with model circuits and applying topological transformations to simulate the transfer of timing violations in gate-level netlists. This makes timing violations and their effects reproducible in discrete cycle-based simulation and amenable for identification and debugging similar to typical synchronous design failures. We show that this approach, when combined with formal verification, is inherently capable of reproducing many of the problematic issues at clock domain boundaries and outperforms the structural and functional heuristics used by state of the art commercial tools in several respects. It reports fewer false positives, can be applied to non-stereotypical designs, can determine failure consequences, can demonstrate failures in signal waveforms and requires no input from the designer about what design patterns are used. Case examples and verification results of several multi-clock testbench designs are presented. |
Year | Venue | Keywords |
|---|---|---|
2016 | PROCEEDINGS OF THE 2016 DESIGN, AUTOMATION & TEST IN EUROPE CONFERENCE & EXHIBITION (DATE) | Clock domain crossing, formal verification, metastability |
Field | DocType | ISSN |
Functional verification,Synchronization,Logic gate,Computer science,Parallel computing,Clock domain crossing,Software design pattern,Real-time computing,Heuristics,Formal verification,Debugging | Conference | 1530-1591 |
Citations | PageRank | References |
1 | 0.42 | 4 |
Authors | ||
3 | ||
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ghaith Tarawneh | 1 | 17 | 5.18 |
| Andrey Mokhov | 2 | 136 | 26.57 |
| Alex Yakovlev | 3 | 516 | 64.23 |