A Multi-Environment Formal Verification Methodology for Catching Latency-Induced RTL Hangs
Abstract
Hang detection in designs which involve a system of interacting state machines has been challenging to the traditional dynamic simulations methodology. This difficulty arises because simulation is non-exhaustive, often failing to trigger the rare, deep-cycle corner cases where deadlocks and livelocks reside. In contrast, Formal Property Verification (FPV) employs mathematical breadth-first search to exhaustively identify circular dependencies and provide concise Counter-Examples (CEX) for rapid debugging.
This paper presents an FPV methodology applied to the Google Connect-Disconnect Block (GCDB), which manages power states and interface fencing via interacting Requestor and Completer FSMs. To address the risks of non-deterministic path delays and asynchronous clock domains across physically distant subsystems, we developed three distinct FPV environments: synchronous, asynchronous, and asynchronous with injected path delays.
Integrating these setups proved instrumental in uncovering 8 bugs in simulation-clean RTL. Identified issues included hangs from non-deterministic delays, timing-dependent races, transaction starvation, and deadlocks during simultaneous power-down requests. This methodology demonstrates how modeling physical latencies within a formal framework detects elusive "silicon-killer" bugs that traditional simulation inherently overlooks.
This paper presents an FPV methodology applied to the Google Connect-Disconnect Block (GCDB), which manages power states and interface fencing via interacting Requestor and Completer FSMs. To address the risks of non-deterministic path delays and asynchronous clock domains across physically distant subsystems, we developed three distinct FPV environments: synchronous, asynchronous, and asynchronous with injected path delays.
Integrating these setups proved instrumental in uncovering 8 bugs in simulation-clean RTL. Identified issues included hangs from non-deterministic delays, timing-dependent races, transaction starvation, and deadlocks during simultaneous power-down requests. This methodology demonstrates how modeling physical latencies within a formal framework detects elusive "silicon-killer" bugs that traditional simulation inherently overlooks.
