Conclusive formal verification of clock domain crossing properties
Where it appeared
| School | Université Grenoble Alpes |
|---|
From bibtex.
Abstract
Modern hardware designs typically comprise tens of clocks to optimize consumption and performance to the ongoing tasks. With the increasing number of clock-domain crossings as well as the huge complexity of modern SoCs, formally proving the functional integrity of data propagation became a major challenge. Several issues arise: setting up the design in a realistic mode, writing protocol assumptions modeling the environment, facing state-space explosion, analyzing counter-examples, ...The first contribution of this thesis aims at reaching a complete and realistic design setup. We use parametric liveness verification and a structural analysis of the design in order to identify behaviors of the clock and reset trees. The second contribution aims at avoiding state-space explosion, by combining localization abstractions of the design, and counter-example analysis. The key idea is to use counterexample-guided abstraction refinement as the algorithmic back-end, where the user influence the course of the algorithm based on relevant information extracted from intermediate abstract counterexamples. The third contribution aims at creating protocol assumptions for under-specified environments. First, multiple counter-examples are generated for an assertion, with different causes of failure. Then, information is mined from them and transformed into realistic protocol assumptions.Overall, this thesis shows that a conclusive formal verification can be obtained by combining inexpensive structural analysis along with exhaustive model checking.