Browse by author
Lookup NU author(s): Dr Ghaith Tarawneh,
Dr Andrey Mokhov
Full text for this publication is not currently held within this repository. Alternative links are provided below where available.
© 2017 IEEE. 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 metastabilityinduced design failures. We discuss the features, underlying methodology and implementation of the tool then present use cases to compare it to commercial alternatives.
Author(s): Tarawneh G, Mokhov A
Publication type: Conference Proceedings (inc. Abstract)
Publication status: Published
Conference Name: Proceedings - International Conference on Application of Concurrency to System Design, ACSD
Year of Conference: 2017
Online publication date: 13/11/2017
Acceptance date: 25/06/2017
Library holdings: Search Newcastle University Library for this item