( ESNUG 582 Item 5 ) ---------------------------------------------- [05/02/18]
From: [ Kamal Sekhon of Oski Tech ]
Subject: Oski on how ADI uses JasperGold apps to speed-up tricky STA signoff
Hi, John,
Here's my trip report of the recent Boston CDNlive'17 conference. Since we
at Oski are a verification consulting house, it makes sense that I cover the
two leading Jasper papers at that users group meeting.
What follows is how ADI uses JasperGold help close static timing analysis
in chip sign-off.
- Kamal Sekhon
Oski Technology San Jose, CA
---- ---- ---- ---- ---- ---- ----
John Mackintosh of Analog Devices
John talked about how JasperGold does Formal when mixed with STA multi-cycle
path analysis (i.e. Synopsys Primetime or Cadence Tempus). It is common for
a STA tool to report violations on "false" paths which required engineers to
manually analyze the design to determine if the reported path is a valid
single cycle path -- or a path that needs to be "waivered".
This is error prone for complex designs. And incorrectly dispositioning a
path as "false" is catastrophic. This talk covered how to use Jasper FPV
to conclusively determine if a path is "false" or not.
And Jasper's "cover -path" is at the core of this approach.
(click on pic to enlarge image)
|
When "cover -path" is combined with some testbench code, Jasper can prove
that a signal propagates through a specified path in a single clock cycle.
(click on pic to enlarge image)
|
John showed Jasper proving a suspected false "path 14" to instead be a valid
path and it helped visualize the scenario that activated that path.
However, before he got there, John used Formal as a simple property cover.
(click on pic to enlarge image)
|
Here, he wrote a property based on the STA path report that described a
signal propagating through the path in 1 cycle. If covered by Jasper FPV,
the path would be proven valid and should not be waived. If the path was
not covered, then nothing would be proven, but confidence would increase
that the path was not a valid single cycle path.
(click on pic to enlarge image)
|
Step 1 was to distill the raw STA report by removing synthesis nets that do
not exist in RTL and annotate edge direction (F=Falling, R=Rising).
(click on pic to enlarge image)
|
Step 2 required writing the property using the SVA language and the final
step was to run Jasper FPV and attempt to cover the property.
(click on pic to enlarge image)
|
The result was that the property was successfully covered.
(click on pic to enlarge image)
|
However, he soon realized that this approach was flawed. Simply covering
this property proved a set of edges will happen within 1 cycle on the
specified nodes. It did not prove causality. Specifically, it did not
prove that at falling edge at the start of the path propagates along the
specified path causing the series of edge transitions. Instead, the edge
transitions in the cover trace could be (and were) caused by multiple other
logic cones. The cover does not represent 1 single cycle path, which was
required for the problem at hand.
(click on pic to enlarge image)
|
At this point he used the Jasper FPV "cover -path" to generate a cover
property that checks whether the value of a signal can be propagated to
another signal (one signal can control another signal).
(click on pic to enlarge image)
|
Using the "cover -trace" command.
(click on pic to enlarge image)
|
Once implemented, the cover trace revealed that the signal values could
be propagated in the same cycle. Waiving the path would have resulted in
a silicon bug and therefore the timing had to be fixed.
---- ---- ---- ---- ---- ---- ----
John then outlined 3 limitations with the "cover -trace" tool:
(click on pic to enlarge image)
|
(click on pic to enlarge image)
|
(click on pic to enlarge image)
|
(click on pic to enlarge image)
|
He then closed with tips:
(click on pic to enlarge image)
|
(click on pic to enlarge image)
|
His tips were on how to make the methodology more efficient. For example,
leveraging the cluster can accelerate the proof process. This can be done
by setting the socket communication "ON" for multiple JasperGold engines
to talk with each other and using set_proofgrid_shell to specify the grid
submission command. The commands should be added in the TCL script before
the "prove" command. The user should also define "control" paths to help
debug and test setup.
Analog's talk outlined a good basic use of Formal. It will be interesting
to see how deeper Formal use will affect their design and verification
efforts -- particularly if a more sign-off-driven approach is used.
---- ---- ---- ---- ---- ---- ----
What follows in the next links (ESNUG 582 #6 and #7) is Kamel Belhous and
Joe Panec of Teradyne ramping up on using JasperGold to replace the old
Cadence Incisive Formal Verifier (IFV/IEV) -- with a focus on replicating
the UNReachability (UNR) flow to find RTL dead code.
- Kamal Sekhon
Oski Technology San Jose, CA
---- ---- ---- ---- ---- ---- ----
|
Kamal Sekhon works as a verification consultant at Oski Tech in San Jose, CA. She's big fan of
the Denver Broncos and she still can't get over their 5 wins, 11 losses 2017 record. |
Related Articles
Formal users share 8 upsides, 6 downsides, and 13 best practices
Oski on how to do signoff with bounded (incomplete) formal proofs
Vigyan of Oski on DVcon'15, Aart, formal guidelines, goal-posting
How I unwittingly started BRCM's Formal Verification Users Group
Join
Index
Next->Item
|
