Reducing Area and Power Consumption while Increasing Performance with Formal-based ‘X’ Verification

[Preface: on October 15 at 8am Pacific, Product Engineer Ping Yeung will be delivering a free, detailed technical webinar on the Formal-based ‘X’ Verification flow outlined in this post, including a real world case study. Register here.]

Whether you are designing an ASIC or FPGA, it is often beneficial to use as many non-resettable registers or flip flops as possible: such elements are often significantly smaller than their fully-resettable counterparts, consume less power, and have a higher operational frequency. But how can you conclusively determine the maximum number of these elements that you can safely use without risking the creation of harmful ‘X’ signal corruption that could lead to unpredictable behavior in silicon?

Phase “0”: Start with Simulation

First, it’s obviously a good thing to include X-propagation analysis in your constrained-random simulation testbench flow. Both Questa Simulation and Questa Power Aware Simulation support this, so be sure to take advantage of their capabilities as you develop your RTL regression suite. However, as they say in math class, X-propagation simulations are a “necessary, but not sufficient” step. It’s a fact that the results from even the most thoughtfully-designed UVM testbench simulation environment will not be exhaustive, leaving the door open for unwanted ‘X’s to appear. This is where the exhaustive nature of Formal analysis comes in to create a truly “safe” non-resettable register verification flow.

Phase 1: Preparation with Questa AutoCheck

Among the many capabilities of the Questa AutoCheck formal app is that without any testbench or user input the tool can exhaustively review your RTL code for common ‘X’ sources, non-resettable registers, and non-initialized memories. It does this by doing a synthesis of your RTL so its internal design representation is essentially the gates you will get in silicon, and then it goes on to automatically apply formal algorithms under-the-hood on the all the fan-in cones of your elaborated logic.

Specifically, not only does AutoCheck’s ‘X’ analysis automatically flag X-pessimism, X-optimism, inconsistent use of reset, multiply driven inputs, bus conflicts, and other common sources of ‘X’ trouble; it also reports unresolved registers and memories. Clearly the data from these analyses better be what you expected, or you have some bugs to fix.

Phase 2: Iteration with Questa X-Check

After taking care of “the ‘X’ basics” with AutoCheck, the main event is to confirm that your usage and distribution of all the area-and-power saving non-resettable registers doesn’t get you into trouble. This is when the Questa X-Check automated formal app applies. In a nutshell, using only your RTL and a specification of your initialization sequence, the Questa X-Check formal app automatically generates and analyzes assertions to rapidly identify chip-killing X-state issues. No knowledge of formal or property specification languages is required – all of that Formal stuff is automated under-the-hood. In the particular context of this flow, the app exhaustively identifies all the “safe” and unresolved non-resettable registers in the DUT, and also proves that a resister is/is not ok after initialization. No guess work or lingering doubts whether you have written enough tests – you get exhaustive results (and thus, peace of mind)!

Summary

Simulation alone is not enough to minimize risks from ‘X’ initialization, propagation, and corruption when employing non-resettable registers to reduce power and area. Fortunately, the automated, formal-based ‘X’ verification flow outlined above – elaborated in technical detail in this webinar – leverages exhaustive formal analysis under-the-hood without you having to learn formal. This flow has proven its worth on-site at customers, and the Questa Formal team is happy to coach you to achieve similar success.

Until next time, may your power consumption and area be low, and your throughput be high!

Joe Hupcey III and Ping Yeung
for the Questa Formal team

Special thanks to our colleagues Juho Jarvinen and Abdel Ayari for all their work with customers in developing this flow.

Reference link: detailed technical presentation on this flow