Presentation
Multi-Tiered Physical-Aware Formal: Ensuring Latency-Robustness in Power Management Architecture and Design
DescriptionGoogle's Connect Disconnect Block (GCDB) manages interface connectivity for power management and clock gating. It orchestrates power state transitions (HWACG/HWAPG) and interface fencing to prevent data loss or coherency issues. Verification of GCDB must eliminate deadlocks, live-locks, and FSM hangs while ensuring protocol compliance, clock-gate integrity, correct FSM transitions and stability during Q-Stop clock randomization.
As the GCDB manages handshakes between physically separated blocks across asynchronous clock domains, signals experience non-deterministic physical routing latencies. These delays, combined with asynchronous clocks, can cause signals to arrive out of order, potentially breaking the design behaviors or causing system hangs. We must account for these path delays to ensure the handshake mechanisms don't fail, hang or cause data corruption.
This paper presents a multi-tiered verification strategy using Arch-Formal for high-level architecture verification and Formal Property Verification (FPV) for RTL analysis. To address physical realities, we enhanced FPV with custom FV modules to mimic signal skew and CDC uncertainties. In Arch-Formal, we modeled GCDB with unbounded path delays. Integrating these randomized arrival times proved instrumental in exposing elusive race conditions and deadlocks within both the Arch and design, ensuring robust operation against PVT variations and physical implementation constraints.
As the GCDB manages handshakes between physically separated blocks across asynchronous clock domains, signals experience non-deterministic physical routing latencies. These delays, combined with asynchronous clocks, can cause signals to arrive out of order, potentially breaking the design behaviors or causing system hangs. We must account for these path delays to ensure the handshake mechanisms don't fail, hang or cause data corruption.
This paper presents a multi-tiered verification strategy using Arch-Formal for high-level architecture verification and Formal Property Verification (FPV) for RTL analysis. To address physical realities, we enhanced FPV with custom FV modules to mimic signal skew and CDC uncertainties. In Arch-Formal, we modeled GCDB with unbounded path delays. Integrating these randomized arrival times proved instrumental in exposing elusive race conditions and deadlocks within both the Arch and design, ensuring robust operation against PVT variations and physical implementation constraints.
Event Type
Engineering Poster
TimeMonday, July 275:00pm - 6:00pm PDT
LocationDAC Pavilion, Exhibit Floor