Improving the efficiency of formal verification: The case of clock-domain crossings

Citations of this article
Mendeley users who have this article in their library.

This artice is free to access.


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.




Plassan, G., Peter, H. J., Morin-Allory, K., Sarwary, S., & Borrione, D. (2017). Improving the efficiency of formal verification: The case of clock-domain crossings. In IFIP Advances in Information and Communication Technology (Vol. 508, pp. 108–129). Springer New York LLC.

Register to see more suggestions

Mendeley helps you to discover research relevant for your work.

Already have an account?

Save time finding and organizing research with Mendeley

Sign up for free