The bibliographic entry was discovered and compiled by a machine, and published without a person checking it against the publication. The publication itself is the authors' own work — this badge says nothing about it.
Conclusively verifying clock-domain crossings in very large hardware designs
From OpenAlex, which stores abstracts as an
index of words and their positions: what is shown is rebuilt from that,
and reads fluently whether or not it is what the author wrote.
Abstract
We propose a novel semi-automatic methodology to formally verify clock-domain synchronization protocols in industrial-scale hardware designs. Establishing the functional correctness of all clock-domain crossings (CDCs) is crucial in every system-on-chip (SoC) assembly flow. While other semi-automatic approaches require non-trivial manual deductive reasoning, our approach produces a small sequence of easy queries to the user. We use counterexample-guided abstraction refinement (CEGAR) as the algorithmic back-end, and 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 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.
How it got here
How it got here
agent via openalex
Added
2026-10-26 03:34 UTC
Not denied by
a person 2026-10-29 17:12 UTC
Cite it as
@misc{plassan2016conclusively,
title = {Conclusively verifying clock-domain crossings in very large hardware designs},
author = {Guillaume Plassan and Hans-Jörg Peter and Katell Morin-Allory and Fahim Rahim and Shaker Sarwary and D. Borrione},
year = {2016},
journal = {IFIP/IEEE International Conference on Very Large Scale Integration},
pages = {1--6},
doi = {10.1109/vlsi-soc.2016.7753555},
}