The Many Flavors of Equivalence Checking: Part 3, How SLEC Brings Automated, Exhaustive Formal Analysis to Low Power Clock Gating Verification
[Preface / reminders: Part 1 of this series focused on synthesis validation with LEC and SLEC, and Part 2 describes how SLEC brings automated, exhaustive formal analysis to ECO/bug fix verification]
Whether you are designing a mobile device to make the most of every joule in the battery, or a rack-mounted system to run as cool as possible to minimize HVAC costs, minimizing power consumption is often THE over-arching operational requirement for products both big and small. Among the strategies that customers employ to reduce dynamic power consumption is to literally stop the clock signal feeding a given IP inside a chip, when said-IP is not needed. The term-of-art is “low power clock gating” (LPGC), and in general the implementation of this technique in RTL designs is as straightforward as it sounds: control logic for the power management functionality is effectively hooked up to one side of an AND gate, with the given IPs clock signal on the other side. Easy, right?
Of course, there is a catch – a big, potentially chip killing catch: as you can imagine, if there is the slightest mistake in your low power control logic, your IP(s) will be shut down at the wrong times; potentially ruining the chip/system. Hence, the dozens of customers that I’ve seen use LPCG also add extra logic that can disable the clock gating logic. The great formal methodology reference book Formal Verification: An Essential Toolkit for Modern VLSI Design describes this practice succinctly:
Chicken bits, also known by the less colorful term defeature bits, are extra control signals exposed to the driver to disable a feature in silicon. They are used to provide the ability to “chicken out” of design changes made where confidence is not high; this often happens when fixing a bug very late in a project, or when a critical new feature is added at the last minute. Most fixes to stable designs these days do implement chicken bits, and many bugs result when they unintentionally affect other functionality. Validation of a chicken bit can be challenging, because disabling a feature is often as intrusive in the code as the feature itself.(1)
With this definition in-mind, the goal of verifying chicken bit logic is to confirm that this extra circuitry does not interfere with the rest of the DUT’s operation when the chicken bit is off.
Rephrasing, a DUT without any chicken bit logic should perform identically to a DUT WITH chicken bit logic that is not activated.
Enter Sequential Logic Equivalence Checking (SLEC)
It should be clear by now that this is an ideal use case for a tool that can do an exhaustive comparison of two RTL DUTs – one without any chicken bit logic, and the original DUT with the protective logic added but tied off. In short, this is a perfect application of formal-based Sequential Logic Equivalence Checking (SLEC) verification. As shown in Figure 1 below, simply tie the inputs together, and let the Questa SLEC tool do the work:
Figure 1: SLEC Low Power Clock Gating (LPGC) verification flow
As with the logic synthesis validation case described in Part 1 of this series, by definition any differences detected between the “Specification” and “Implementation” code are clearly a bad thing and need to be fixed ASAP.
One final note: this might not seem like such a big deal and/or such a very hard problem that it calls for the “big guns” of an exhaustive, automated formal verification app like Questa SLEC. But I can tell you from personal experience that I know of customers that have had to have their chips re-spun because there was an error in the LPCG logic – one that was not detected by their simulation or hardware-assisted verification flows – that had to be “fixed” in the lab by turning on the chicken bit logic via firmware. Unfortunately for them, this meant the chip ran too hot for their end customer, and they lost the socket. Suffice to say chicken bit verification with formal-based SLEC analysis is now their Plan of Record.
But Wait, There’s More …
Imagine you were to take this article and replace the words “chicken bit” with “safety mechanism” – i.e. for your safety-critical design you needed to employ extra logic to mitigate the propagation of faults to outputs. In Part 4, I’ll describe how Questa SLEC can be applied to this high-stakes verification challenge.
Until then, may your power consumption be low, and your throughput be high!
Joe Hupcey III,
for the Questa Formal team
Reference Links:
Part 2: How SLEC Brings Automated, Exhaustive Formal Analysis to ECO/Bug Fix Verification
