User Case Study

In prior articles I’ve written in general terms of about formally verifying the impact of adding low power control circuitry with Jasper’s Low Power Verification App.

At the recent Jasper User’s Group meeting on Oct. 22, a real world case study of this app in action at STMicro’s R&D center in India was presented. Here are some highlights from this paper:

DUT in question: an ARM-based, quad core CPU subsystem with multiple power domains.

Verification Goals & Strategy

• Exhaustive verification of interface slices and signals across multiple power domains.
• Shorten the overall schedule by reducing dependence on test bench development for certain aspects of low power verification.
• Reduce cycle time and be able to quickly start low-power verification.
• Use Jasper formal apps for exhaustive verification high risk areas, and/or for tasks where formal is significantly more efficient and effective than simulation-based approaches.

 Formal environment and tools

• Inputs: RTL, Power Intent (UPF).
• Jasper Apps used: the main platform Formal Property Verification app, the Connectivity Verification App, the Control/Status Register Verification App, and of course the Low Power Verification App.
• Several of Jasper’s “Intelligent Proof Kits” assertion-based verification IPs was also employed. Specifically, the IPKs for ACE, AXI3, APB, and ATB.

 Key verification tasks

• Exhaustive verification of clamp value correctness during isolation.
• Prove data integrity for the interface slices.
• Verify interface protocol certification in all valid power states.

 Methodology

• (Re-)Use the same formal verification environment for both low power and baseline functional verification.
• However, for the low power-centric analysis some additional constraints had to be added.

Results

• Formal low power verification setup was completed within couple of days (in contrast to the weeks corresponding simulation test benches would have taken to write and debug).
• Within the first hour of the analysis the Low Power Verification App surprised us by unearthing problems with some clamp values thought to be correct.
• The low power aspects of APB, AXI3, ACE & ATB interface slices for protocol correctness and data integrity were exhaustively proven to be valid in all power states.

In summary, as advertised, Jasper’s Low Power Verification flow “has improved our power-aware verification coverage with reduced cycle time.” An added benefit was/is that the reuse of the power-aware properties for future projects/derivatives is easy. The assertions are in IEEE standard SVA and very easy to modify. Finally, another unexpected bonus of this process was how easy it was for engineers who were completely new to formal technology to take advantage of its power.

Taking a step back, this success story is but one of 14 user presentations delivered at the Jasper User’s 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).