( ESNUG 582 Item 6 ) ---------------------------------------------- [05/02/18]
Subject: Oski on Teradyne's CDNlive award winning "basics of formal" talk
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 of Oski Tech
http://www.deepchip.com/items/0582-05.html
From: [ Kamal Sekhon of Oski Tech ]
Hi, John,
Here's the Teradyne Jasper story. They're new to Jasper. This first part
is their fundamentals of formal.
- Kamal Sekhon
Oski Technology San Jose, CA
---- ---- ---- ---- ---- ---- ----
Kamel Belhous & Joe Panec of Teradyne
This talk won the best presentation award for Boston CDNlive'17 conference
in its track.
It was great in that he shared his team's first experience using simulation
along with JasperGold after migrating from IFV -- but as a Formal expert, I
do feel that his presentation was light on deep dives into how Formal was
used or could have been used -- which made it hard for us to comment on how
or what they could have done better.
What made the talk was how Kamel outlined in detail the basic principles and
benefits of Formal.
Formal Fundamentals
(click on pic to enlarge image)
|
Formal Properties
(click on pic to enlarge image)
|
Formal Constraints
(click on pic to enlarge image)
|
Formal Static State Exploration
(click on pic to enlarge image)
|
Notice how Formal tries to reach (cover) all possible states at
all cycles in your design.
Formal vs. Verilog Simulation/Emulation
(click on pic to enlarge image)
|
Notice how Simulation/Emulation only reaches (covers) a few
possible states and only at certain cycles in your design.
A Simple FIFO Example
(click on pic to enlarge image)
|
Notice setting up the constraints (expectations about how the
input to the FIFO should behave) and assertions (expected output
from the FIFO.)
(click on pic to enlarge image)
|
Using these input constraints and output assertions JasperGold
then determines one of three possible results for each assertion.
1. Full Proof. A specific assertion is mathematically
proven to be true for all states at all cycles.
2. Undertermined. A specific assertion is holds true
for all states up to a certain number of cycles.
("No failure found in 157 cycles.")
3. Counterexample. A specific assertion is found to be
false for all states at a certain specific cycle.
("Counterexample found at cycle 14.")
Keep in mind these 3 possible results are based on your inputs
meeting the specific input constraints only. If you feed your
FIFO drunken (outside of the constraints) input, JasperGold will
neither prove nor disprove your design.
Formal's Sweet Spot
(click on pic to enlarge image)
|
Formal work well on designs/blocks with 10k-100k registers and
for depths up to 100 cycles.
Also overconstraining inputs can explode your Formal runtimes.
Using Cover Properties As A Bug Hunting Technique In Formal
(click on pic to enlarge image)
|
Helper Covers tell JasperGold "during state-space explorations
you must make sure you visit these specific states." JasperGold
then naturally looks around in the neighborhood of any state it
visits -- where it might suddenly find a bug.
(click on pic to enlarge image)
|
Helper Covers must be close enough to each other such that Formal
can reach it! (Otherwise it's unreachable and JasperGold spends
a lot of time trying to reach it.)
Why Everyone Loves Assertions And ABV
(click on pic to enlarge image)
|
(click on pic to enlarge image)
|
(click on pic to enlarge image)
|
Using ABV For Both Verification And Design Engineers
(click on pic to enlarge image)
|
(click on pic to enlarge image)
|
---- ---- ---- ---- ---- ---- ----
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
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
|
