User Case Study: Using Formal To Verify Low Power Functionality And Eliminate Unwanted ‘Xs’

The cynics among us might argue that the addition of low power circuitry is a clever scheme by the energy industry to cause an equal amount of power to be consumed by low power verification as is saved by end-user usage.  As if modern SoC verification wasn’t challenging enough, the addition of low power can create corner cases that can escape even the most well-written UVM testbenches.  Indeed, a Jasper customer located in Asia recently came to the conclusion that an exhaustive, formal-based approach is the only way to ensure their DUT will be free of spec-busting, low-power bugs, as well as unwanted ‘Xs.’  Specifically, they put Jasper’s Low Power Verification and X-Propagation Verification Apps to the test on their latest chip — here are some highlights from this project:

• DUT in question
  • Customer had an SoC with 7 power domains.
  • All IP cores were ready at the start of the evaluation, and the chip integration was in the final stages of “fine tuning.”
  • UPF was available, but not yet finalized.
  • There was no retention in UPF.

• Project Goals
  • The scheduled tape-out date was 4 weeks from the start of adopting the new formal apps, so they needed results quickly.
  • Wanted a push-button solution (since few on the D&V team were familiar with formal)
  • The customer’s long-term goal is to develop a process / methodology that catches errors as early in design cycle as possible.

• Pain points
  • The customer had been using MVRC and MVSIM but conceded that this process failed to capture a bug where their isolation cells have clamp value problems.
  • Through MVSIM they eventually found the bug very late in the verification phase.
  • After adding in the low power circuitry, many unwanted ‘Xs’ appeared on signal lines, triggering numerous failures across the circuit.

• Formal environment and tools
  • Inputs: RTL and UPF
  • Jasper Apps used:
    • Low Power Verification (LPV) App
    • X-Propagation Verification (XPROP) App
    • The Visualize™ dynamic waveform manipulation and debug tool included in Jasper’s Formal Property Verification App (“FPV”).  (This App supports “What If?” analysis that enables the engineer to manipulate signals within legal limits on-the-fly, thus enabling engineers to instantly explore alternative reset implementations without having to recompile.)

• Methodology
  • Ran on chip level, to better fit into their current flow, but reduced logic accordingly depending on complexity of target (both design and power states):
  • For structural checks and power properties generated by JG-LPV
    • Ran on the whole chip with some black-boxes
    • At this level, included all 7 power domains in analysis
    • Used their own power management unit (PMU) and didn’t do any power sequence abstraction essentially verifying the PMU in conjunction with power aware design
  • For X-prop assertions generated by JG-XPROP
    • Further reduced the scale with more black-boxes
    • At this level, included 2 power domains in analysis
    • Used Jasper Power Sequencer Proof Accelerator to abstract and replace the already verified PMU

• Results
  • Types of bugs found (with LPV and X-Prop’s automatic assertions)
    • In general, Jasper’s LPV App caught bugs early in design cycle — bugs which the MVSIM flow had missed.
    • Power assertions pointed important bugs in their power management unit: the tool captured a problem where the designer actually used one of the isolation control signal as the power switch signal of another power domain. This can cause a glitch and subsequent X-Prop problems. The isolation cell is actually being used to control many subsequent logic units, and thus can cause massive X-Prop issues.
    • Clamp check inconsistencies found for several module outputs: they found bugs found with the clamp value checks which were missed earlier and caused some headaches because found later in design cycle.
    • The missing isolation cell for clock signal was found.
    • The X-Prop App itself exposed several unwanted ‘X’ sources in the design.
  • Increased productivity
    • According to one principal engineer, “Jasper’s LPV App is now the only tool that can do such low power clamp value and X-PROP checks. We don’t have any other good alternatives.”

Taking a step back, this success story is but one of many case studies where users were able to supplement, and even replace, simulation with Jasper formal verification with the benefit of increasing their productivity and end-product quality.  Similar stories from other users were recently shared at the annual Jasper Users Group meeting – the paper topics were a mix of novel, “pure formal” verification methodologies, and deep dives on specific apps like the story recounted above.  To see them for yourself, they are posted on Jasper’s Formal Expert site  (registration required).