Skip to Main content Skip to Navigation
Conference papers

Improving the Efficiency of Formal Verification: The Case of Clock-Domain Crossings

Abstract : We propose a novel semi-automatic methodology to formally verify clock-domain synchronization protocols in industrial-scale hardware designs. To establish the functional correctness of all clock-domain crossings (CDCs) in a system-on-chip (SoC), semi-automatic approaches require non-trivial manual deductive reasoning. In contrast, our approach produces a small sequence of easy queries to the user. The key idea is to use counterexample-guided abstraction refinement (CEGAR) as the algorithmic back-end. The user influences the course of the algorithm based on information extracted from intermediate abstract counterexamples. The workload on the user is small, both in terms of number of queries and the degree of design insight he is asked to provide. With this approach, we formally proved the correctness of every CDC in a recent SoC design from STMicroelectronics comprising over 300,000 registers and seven million gates.
Complete list of metadatas

Cited literature [24 references]  Display  Hide  Download

https://hal.inria.fr/hal-01675192
Contributor : Hal Ifip <>
Submitted on : Thursday, January 4, 2018 - 10:59:48 AM
Last modification on : Thursday, March 26, 2020 - 9:30:07 AM
Document(s) archivé(s) le : Wednesday, May 2, 2018 - 9:08:00 PM

File

456609_1_En_6_Chapter.pdf
Files produced by the author(s)

Licence


Distributed under a Creative Commons Attribution 4.0 International License

Identifiers

Citation

Guillaume Plassan, Hans-Jörg Peter, Katell Morin-Allory, Shaker Sarwary, Dominique Borrione. Improving the Efficiency of Formal Verification: The Case of Clock-Domain Crossings. 24th IFIP/IEEE International Conference on Very Large Scale Integration - System on a Chip (VLSISOC), Sep 2016, Tallinn, Estonia. pp.108-129, ⟨10.1007/978-3-319-67104-8_6⟩. ⟨hal-01675192⟩

Share

Metrics

Record views

255

Files downloads

452