( ESNUG 582 Item 7 ) ---------------------------------------------- [05/02/18]
Subject: Oski on the Jasper-new-user Teradyne's results verifying two chips
What follows in the next link is how Teradyne used JasperGold to do
formal on two chips:
1.) To do a formal connectivity test on the extracted Verilog
of a Virtuoso generated 27-input OR gate in a "large Mixed-
Signal SoC".
2.) To do a formal state UNReachability test to find dead code
in a "large Digital SoC".
And to share their ramp-up experiences with JasperGold.
- Kamal Sekhon of Oski Tech
http://www.deepchip.com/items/0582-06.html
From: [ Kamal Sekhon of Oski Tech ]
Hi, John,
Finally, here's the Teradyne-Jasper new user results.
- Kamal Sekhon
Oski Technology San Jose, CA
---- ---- ---- ---- ---- ---- ----
With both designs, JasperGold FVP was run after RTL freeze and after dynamic
simulations coverage closure was completed with 100% code and functional
coverage.
---- ---- ---- ---- ---- ---- ----
The large Mixed-Signal SoC
The Teradyne folks used to do their connectivity testing for years using
the Cadence IFV flow. This paper was them migrating over to JasperGold
to do the same task.
(click on pic to enlarge image)
|
Their new Jasper connectivity flow is used on a Verilog netlist extracted
from Virtuoso. It begins with making sure all voltage and bias current
path connections are specified using the Excel-based Jasper Connectivity
template. The switch path transistors were then modeled as a one- or two-
stage multiplexer.
What they learned is Formal acts on synthesized RTL differently than how
dynamic simulation acts on RTL.
(click on pic to enlarge image)
|
They checked all combinations of inputs-to-outputs for their 27-input OR
gate design. They tried reverse connectivity generation for the initial
debug to ensure each path connection from input-to-output. They imported
reverse connectivity generation connections into the Excel-based Jasper
Connectivity template. Their Logic OR gate was implemented as a tree of
discrete NAND, NOR and INVERTER gates.
What they learned is that ternary (3-input) operators are not supported
by the reverse connectivity engine and that reverse connectivity output
is not directly importable to Excel. So instead everything had to be
remapped to binary operators for this JasperGold connectivity flow to
work.
They also proved the connectivity from their digital register block to
their analog interface and from the analog interface through syncers
back to the same register block. That was to check the correct clock
latency (i.e. minimum latency based on the number of syncers).
---- ---- ---- ---- ---- ---- ----
The large Digital SoC
This was a complex controller block which gets data from a DRAM by way of
16 different AXI masters.
From the slide above you can see the controller was complicated. It took
25 assertions for JasperGold.
The end result was it found 3 bugs -- 2 bugs in FIFO control and 1 bug in
error detection. These bugs would be very hard to catch in simulations
because of the long run times, and the fact that they were embedded deep
in the design. Constrained random would have missed these bugs.
Once the bugs were fixed, JasperGold provided exhaustive proofs of the
correctness of the design with respect to the 25 assertions.
No emulation was used.
Some insights on how Formal use could have been improved:
Again, the details are light here probably because JasperGold was being
used for the first time. Teradyne used it in the "bug-hunting" mode and
measured its success by tracking the bugs they found. To improve further,
Formal could be used for sign-off -- where their blocks are completely
verified with only Formal -- so no simulation Testbench needs to be
developed.
While "bug hunting" is valuable, Formal sign-off truly leverages the power
of Formal verification to provide the necessary confidence quicker.
---- ---- ---- ---- ---- ---- ----
The JasperGold Adoption Timeline
The first design (27-input OR) took 2 weeks from set-up to finding 3 bugs.
The second design only took 48 hours once their 25 assertions were written.
For Teradyne, teaching their engineers how to write good assertions and how
to check constraint assumptions were their two next biggest steps.
- Kamal Sekhon
Oski Technology San Jose, CA
---- ---- ---- ---- ---- ---- ----
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
|
