Presentation
Advancing CDC Formal Verification in Low-Power SoCs Using Power Intent and Smart Waiver Techniques
DescriptionIncorrect clock domain synchronization can cause critical functional bugs in SoCs, potentially requiring costly fixes. When low-power requirements with multiple switchable power domains are involved, CDC verification becomes more complex. In UPF-based low-power designs, isolation cells at power domain boundaries preserve signal integrity but may cause resynchronization issues if their enable signals are improperly synchronized, leading to metastability or failures. The presence of isolation cells, retention registers, and their enable signals increases the number of asynchronous paths to analyze.
This paper proposes a new flow based on formally proven' smart waiver CDC jointly with LPV that drastically reduces the number of CDC and RDC violations to analyze in a typical ultra-low-power SoC. Normally, the number of violations can be several hundred, but this flow safely waives those proved true through formal verification. The remaining violations can then be analyzed to uncover real resynchronization bugs.
In the presented test case, the number of violations to analyze was reduced by about 35%, enabling the discovery of bugs that might have been lost among the initial hundreds of violation reports. Formal verification remains the optimal method for CDC checking, and Jasper CDC with LPV enables power-aware CDC verification using UPF
This paper proposes a new flow based on formally proven' smart waiver CDC jointly with LPV that drastically reduces the number of CDC and RDC violations to analyze in a typical ultra-low-power SoC. Normally, the number of violations can be several hundred, but this flow safely waives those proved true through formal verification. The remaining violations can then be analyzed to uncover real resynchronization bugs.
In the presented test case, the number of violations to analyze was reduced by about 35%, enabling the discovery of bugs that might have been lost among the initial hundreds of violation reports. Formal verification remains the optimal method for CDC checking, and Jasper CDC with LPV enables power-aware CDC verification using UPF
Event Type
Engineering Poster
TimeMonday, July 275:00pm - 6:00pm PDT
LocationDAC Pavilion, Exhibit Floor