Equivalence Checking

Everyone is consumed by power these days. The less power our devices use, the better—the longer our batteries will last, the more applications we can use simultaneously, the less HVAC capacity is required by the data center, etc. Clock-gating is one widely used technique to save power in ASIC designs. However, clock gating can significantly impact the structural and behavioral elements of the original design, risking errors that can cause parts of the chip to “go dark” or require workarounds that ironically necessitate more power consumption. In a nutshell, the key verification question becomes, “Did the functionality change when we put in the clock-gating logic?

Although logic synthesis tools pledge to guarantee that the low power enabled netlist is logically equivalent to the RTL source code, a volatile mix of HDL and power intent file semantics can lead to unexpected errors in programs, along with issues that arise when manual alterations are made to the netlist. Hence, it’s necessary to produce a RTL golden reference model. Any changes to the netlist due to power control circuitry can be compared to that model to ensure they don’t alter the intended behavior of the design. In short, sequential equivalency checking is required.

While some amount of simulation-based cross-checking is a worthwhile part of any functional verification regression suite, even the most sophisticated simulation-based equivalency checking methodology simply cannot reach all possible corner cases. Therefore, a formal approach to sequential equivalence checking becomes necessary to exhaustively make sure that the RTL design spec and the low power-optimized RTL design implementation with the clock-gating circuitry exhibit the same behaviors.

The flow for formally verifying these clock-gating issues is very straightforward when using Jasper’s Sequential Equivalence Checking (SEC) App. First, you provide the App with both the original design specification and the low power enhanced implementation. You also include set-up information such as the clocking information, and if necessary a mapping file to reflect trivial name changes in the inputs/outputs information. The SEC App then takes this data and exhaustively determines whether or not you have perfect equivalency. If you have, then you are done! If not, then you can debug the mismatching scenarios using the SEC App’s intuitive debug capability. The GUI not only displays the waveform data from the specification and the implementation side-by-side, but also the source-level debug code to rapidly compare the detected differences. Consequently, you can focus on specific areas of interest rather than having to sift through entire cones of logic.

Note that the SEC App includes a special formal engine that’s optimized for sequential equivalence checking. It runs 2 to 10 times faster than a traditional formal property engine applied to sequential equivalence checking.

In summary, achieving low power optimization in your design can cause bugs to occur creating undesired behavior. To make sure that specified behavior doesn’t change during power optimization, formal sequential equivalence checking is required, and the Jasper’s SEC App is turnkey solution for this challenge.

For a more in depth look at how Jasper’s SEC App works, you can check out the video “High-Performance RTL vs. RTL for Sequential Equivalence Checking.”