PhD Thesis

< back to PhD thesis

« Conclusive formal verification of clock domain crossing properties ».

Author: G. Plassan
Advisor: D. Borrione
Co-advisor: K. Morin-Allory , H.-J. Peter
President of jury: N. Halbwachs
thesis reviewer(s): J.-P. Talpin, W. Kunz,
These de Doctorat Université Grenoble Alpes
Speciality: informatique
Defense: March 28 2018
ISBN: 978-2-11-129240-6


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, dots 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.

pdf pdf