Graham is VP of Marketing at Real Intent. He has over 20 years experience in the design automation industry. He has founded startups, brought Nassda to an IPO and previously was Sales and Marketing Director at Internet Business Systems, a web portal company. Graham has a Bachelor of Computer … More »
Progressive Static Verification Leads to Earlier and Faster Timing Sign-off
January 30th, 2014 by Graham Bell
January 22, 2014 — As SOC design crosses the billion-gate threshold the cost of errors grows dramatically. The demand that engineers ensure their work is as correct as possible — and as soon as possible — in the design process has become more insistent. Letting errors slip forward one stage closer to implementation means their impact will grow while their causes become obscured and success is delayed. The design sign-off process itself has grown more complex, and the register-transfer level (RTL) is now where sign-off begins.
A starting point for the sign-off regimen is verification of the timing behavior of the heterogeneous IP used in an SOC and how the IP interfaces with the host design, including how clocks and signals cross any interfaces. Clocking schemes must be defined to enable earlier static analysis before it reaches the simulation stage. However, before timing analysis and simulation begin, designs must be cleaned using Lint tools.
Modern Lint tools have evolved to the point where they can handle full-chip designs and yet still offer concise hierarchical reporting. The availability of low-noise reporting means less time waiving violations and more time cleaning easy-to-fix issues. Because of the lower-noise, designers can use the tool earlier and more often. However, an RTL Lint tool requires only rule-setup and, therefore, cannot provide a deep analysis.
Automatic formal RTL analysis builds on Lint cleaning for early detection of functional issues and takes advantage of clock definitions for the design. Because automated formal performs a sequential analysis and does constant propagation, it can do a deeper design exploration to uncover potential problems. Formal analysis can eliminate potential failures reported in Lint. Designers benefit from early static analysis of problems such as potential FSM deadlocks, bus issues and even X-value propagation.
Billion-gate designs have millions of flip-flops to initialize. Many of the IP blocks used in such designs also have their own initialization schemes. It is neither practical nor desirable to wire a reset signal to every single flop. It makes more sense to route resets to an optimal minimum set of flops and initialize the rest through the logic, but this is a significant RTL-coding challenge.
Flip-flop reset analysis ensures that the SOC design will come in a known good state, and in later iterations of the design it can be used to save chip area and routing resources through a more intelligent application of reset signals. The analysis of any system with such a reset and initialization scheme is bound to identify many Xs. For designers, the issue is in knowing which ones matter, because dealing with unnecessary Xs wastes time and resources. But missing an X state that does matter can increase the likelihood of late-stage debug and cause insidious functional failures and, ultimately, re-spins.
As a last step, it is important to manage the way simulation and synthesis processes handle the unknown (X) states thrown up by power-management strategies that turn blocks on and off, and adjust clocks crossing between domains. A proper analysis of this issue can reveal functional bugs that have been hidden at the RTL level by too much optimism about the impact of X states, and also can reduce the impact of excessive pessimism given to X states after synthesis.
Timing constraints (SDC) are a key input to the gate-level synthesis of designs, so SDC management and checking ensure correct timing for the block and full-chip level, so long as any changes in the RTL are reflected in the SDC files for the design. And the SDC itself needs to be verified for correctness and consistency, which is essential for other analyses, such as clock design crossing.
Clock domain crossing analysis, so important for design reuse, IP, and complex power-management schemes, can be carried out using a combination of formal and structural methods. It helps trap the corner-case combinations of timing and functionality that lead to errors.
For all the formal checks, a little more information is required beyond just using the structural checks. In structural checking, the environment can be captured automatically with very little user input required for resets and clocks. In contrast, formal checks require that all reset signals be associated very accurately with their corresponding clocks. All clock frequencies must be specified for appropriate formal checks to be made on fast-to-slow clock-domain crossings. So setup for formal is necessarily more complex and requires detailed design knowledge about all the frequencies of clocks and combinations of those frequencies. For example, multi-mode designs also require users to specify the selection signals for mode selection.
Power analysis and optimization techniques address issues such as retention-flop and isolation-cell analysis and optimization, clock/ power gating, and sequential/ combinational optimizations. These interventions can be so extensive that it makes sense to go back to the other static analyses to recheck the design.
Combining these static-verification steps can sign-off the RTL for clocking and reset issues to reduce the simulation burden of testing functionality and the synthesis burden of trying to implement conflicted code from disparate IP. It means the design will be as correct as possible as soon as possible, with reduced risk of failure at the implementation stage.