Name
Abstract | ||
|---|---|---|
This paper presents Xprova, an open-source formal verification tool for multi-clock designs. Xprova is a model checker that can discover property violations caused by the incorrect implementation of clock domain crossing circuits. Unlike existing clock domain crossing verification tools, Xprova does not rely on structural or functional analysis to detect deviations from standard design practices. Instead, it transforms the input circuit to model the onset and propagation of metastability digitally, then conducts a state space exploration to search for property violations. This approach is intrinsically capable of identifying several well-known clock domain crossing problems including missing synchronizers, path reconvergence issues and glitches. It also improves debuggability by generating counter-example waveforms showing the onset and mechanics of metastability-induced design failures. We discuss the features, underlying methodology and implementation of the tool then present use cases to compare it to commercial alternatives. |
Year | DOI | Venue |
|---|---|---|
2017 | 10.1109/ACSD.2017.22 | 2017 17th International Conference on Application of Concurrency to System Design (ACSD) |
Keywords | Field | DocType |
Xprova,open-source formal verification tool,multiclock designs,model checker,property violations,clock domain crossing circuits,verification tools,structural analysis,functional analysis,standard design practices,input circuit,state space exploration,clock domain crossing problems,metastability-induced design failures,built-in metastability modeling,counter-example waveforms,glitches,path reconvergence,missing synchronizers,clock domain crossing verification tools | Glitch,Synchronization,Use case,Model checking,Computer science,Clock domain crossing,Theoretical computer science,Real-time computing,Space exploration,Electronic circuit,Formal verification | Conference |
ISSN | ISBN | Citations |
1550-4808 | 978-1-5386-2868-3 | 1 |
PageRank | References | Authors |
0.37 | 4 | 2 |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ghaith Tarawneh | 1 | 17 | 5.18 |
| Andrey Mokhov | 2 | 136 | 26.57 |