( DAC'19 Item 3d ) ------------------------------------------------ [02/20/20]
Subject: Real Intent's AutoFormal *formal* linting makes Best of 2019 #3d
PRAKASH'S BREAKOUT (part II): Formal linting goes waaay back. This is NOT
just linting (which are static structural checks on your Verilog on syntax,
semantics, coding styles, etc.) it's *formal* voodoo brought into linting.
It started with Real Intent Verix IIV (2000), JasperGold SuperLint (2009),
Atrenta Advanced Lint (2011), and Mentor AutoCheck (2013).
In the early years, all four formal linters were pretty much the same. They
ran ~6 hours, generated 60% signal-to-noise violations reports, and at most
handled 100 K gate blocks. Over the next 15 years that max block size grew
to around 500 K gates -- which was a 500 K gate brick wall that kept formal
linting as a niche tool.
So engineers continued to use VCS/Incisive/Questa for dynamic simulation;
which risked missing bugs due to coverage issues for key control logic such
as FSMs, deadlocks, and range violations.
Plus they kept using good olde (static) structural linters like Atrenta
Spyglass and Real Intent Ascent Lint to chug along doing what they *could*
do by statically checking syntax, style, naming conventions, plus finding
some functional errors. It's not sexy, but it's still chugging along today.
(See DAC'19 #3b)
---- ---- ---- ---- ---- ---- ----
FAST FORWARD TO THE YEAR 2019 and for the first time in over a decade, I get
some user comments (and benchmarks even!) on formal lint again -- all around
Real Intent Ascent AutoFormal beating "other similar tools" -- because these
users don't want to catch hell from SNPS/CDNS/MENT for showing benchmarks where
their tools lose. (SNPS has Spyglass Lint Advanced, CDNS has the JasperGold
SuperLint App, and MENT has Questa AutoCheck.)
And these formal lint user comments boiled down to:
Table 1: Formal Linting in 2019
|
Tool
|
Max Capacity
|
Runtime
|
Signal
to
Noise
|
Real Intent
Ascent
AutoFormal
|
5 M gates
1 M gates
500 K gates
|
10 - 15 hours
6 - 8 hours
5 - 6 hours
|
80% to 97%
|
JasperGold
SuperLint App
Spyglass
Lint Advanced
Questa
AutoCheck
|
500 K to
800 K gates
|
11 - 15 hours
|
40% to 80%
|
AND KA-BOOM! Did you see that? With that 5 million gates in 12 to 15 hours,
Ascent AutoFormal broke through the capacity-runtime wall.
Suddenly that "niche tool" status for formal linting trapped at 500 K gates
drops away! Most blocks today are 3 to 5 M gates -- a 10X jump to 5 M gates
means formal linting can go mainstream for *real* design blocks now.
Higher capacity also catches more violations. If you did ten 500 K gate
blocks you might find 3 major violations, but put that same functionality
all into one 5 M gate block, you might suddenly catch 12 major violations.
You lose checking visibility when you have lots of small block boundaries.
"AutoFormal is our 2nd hottest selling new tool, behind Meridian RDC," said
Prakash Narain, CEO of Real Intent. I asked him: "Why can't CDNS/SNPS/MENT
R&D just do formal lint like you're doing? Their R&D guys aren't dumb."
Prakash replied: "We get this 10X+ capacity advantage because our engine is
tuned exclusively for formal linting -- while Cadence-Synopsys-Mentor all
rely on general ABV-engines. Two decades of focusing our formal on linting
gives us an advantage that our competitors cannot match with just a simple
6 month catch-up R&D push."
FINDS TROUBLEMAKERS: On the purely tech side, it was interesting how users
cited how powerful AutoFormal was in bird dogging root cause errors vs.
swamping you with a flood of secondary errors.
"With our prior automated formal tool, we had to identify the root
causes manually. It cost us excessive design iterations to do this,
and we could even miss bugs ... the other tool had 10X more
violations for us to review."
- [ An Anon User ]
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
QUESTION ASKED:
Q: "What were the 3 or 4 most INTERESTING specific EDA tools
you've seen this year? WHY did they interest you?"
---- ---- ---- ---- ---- ---- ----
Real Intent Ascent AutoFormal
We use AutoFormal for early functional verification. We needed more
efficiency for our logic simulation and formal checks.
We had to review 100,000+ errors and warnings for formal checks.
AutoFormal helped reduce our VCS logic simulation time by ~30 percent.
Our VCS reduction is in great part because AutoFormal separates out
each root-cause-error as the primary failure from all other violations.
- AutoFormal categorizes all the reported failures/violations
into root cause errors vs. "symptoms."
- It has a violation causation tree window that displays the
root-cause-errors, and then shows the secondary failures the
result from the propagation of each root cause error.
This AutoFormal root-cause-error function compressed our review items
tremendously -- saving our engineers a lot of debug time.
With the rival formal linter, we had to identify the root causes
manually. It cost us excessive design iterations to do this, and we
could even miss bugs.
We used AutoFormal formal linting to do focused checks for behavioral
control, FSMs and tristate drivers. It helped us find critical
deadlocks in our FSM.
To give you a simple example, for one set of formal checks we ran:
- Real Intent Ascent AutoFormal
Reported only 1 primary error and 9 secondary warnings
- the rival formal linter
Presented all 10 violations as errors.
Had 10X more violations for us to review.
On bigger designs with more checks, this can add up!
Because of this, Real Intent reduced both our review time and our debug
iteration time.
---- ---- ---- ---- ---- ---- ----
We estimate Real Intent AutoFormal cuts our VCS & Questa simulation
effort by around 10%.
Our designers and our verification engineers both use Ascent AutoFormal.
We run it before and after VCS/Questa simulation.
In some cases, the designer codes in System Verilog and runs simulation
tasks simultaneously while the verification engineer runs AutoFormal
after confirming the simulation results.
Real Intent improved AutoFormal's capacity and speed up in 2019, and
it now has 5 million gate capacity -- even though we use it mostly
for much smaller blocks when writing code.
We've also seen a 3.5X performance speedup with multiple cores for this
newer release.
- We ran 14 blocks (4.5K gates) through it at once on 4 cores
- AutoFormal's runtime was 740 secs.
AutoFormal categorizes the violations by:
1. Root Cause Errors, then
2. Secondary violations resulting from the root cause error
propagation, then
3. Duplicate errors, such as from multiple instances, then
4. Structural violations that can be found by an RTL linter
(so they do not need sequential analysis).
Ascent AutoFormal's "smart" reporting feature reduces our follow-up
analysis of the report results by 50%-80% -- as compared with other
tools that do not have this feature.
AutoFormal has a two-step Set-Up & Verify process:
1. Set-Up
We just put in our System Verilog RTL and AutoFormal
automatically does the set-up.
It generates an environment that defines the clocks &
resets and runs crosschecks. We then review the
environment file.
2. Verify
We run it's formal analysis.
Setting up AutoFormal for our first design took us about
1 day. This included both the tool installation work
and the execution environment setup work.
Our next design only took 1 hour to set up.
Some of the checks AutoFormal runs that we found useful:
- FSM deadlocks & unreachable state checks
- Coverage issues (e.g. constant nets, constant
RTL expressions...)
- Dead code checks
Some of the above control logic aspects are missed by VCS/Questa
simulation.
Plus, Real Intent automatically generated the checks based on our
design, so our designers did not need to learn an assertion language
or manually creating assertions to use it.
Debug Environment
Some of AutoFormal's useful debug features are:
- Range violation checks
- Conditional RTL construct checks to identify the
conditional type
- Automatic VCD traces that show time of failure plus the
event sequence that led to the undesired condition
- Integrated schematics
I strongly recommend AutoFormal formal linting to other designers.
In particular, AutoFormal's two-step verification method (setup/verify)
and the "smart" reporting function (root cause analysis) features
not found in other similar tools.
These contribute tremendously to our verification efficiency.
---- ---- ---- ---- ---- ---- ----
Real Intent Ascent AutoFormal is a powerful automated formal analysis
tool that lets us do our design reviews much more efficiently. We
have so many lines of code that there is no way we can do a complete
peer review.
It's really fast. It can run 100K gates in minutes.
Our designers and our verification engineers both use it. It's quick
to set up -- under an hour. And it only takes day or so for our
designers to learn to use it.
Some of the Ascent AutoFormal checks we use are:
- Unreachable states
- Constant nets, constant assignments that can cause coverage issues
- FSM deadlocks
- Array bounds violations
- Dead code checks (code that cannot be executed)
Our designs are DO254 compliant, and AutoFormal helps there, too.
AutoFormal performs an exhaustive verification that checks for all
states. In contrast, simulation is only as good as the inputs you
provide, so it would be nearly impossible to simulate all the
potential conditions.
Our methodology
All our designers verify their own designs. They typically run Ascent
Lint first, then AutoFormal, then Cadence Incisive simulation.
Although they always run Ascent Lint first, they will sometimes run
AutoFormal in parallel with the Incisive simulation.
Root cause reports
We use its root cause reports all the time. It groups violations by
root cause, secondary, duplicate instances, and structural. We use
the report to pinpoint where our design issues are and then zone in
on where we need to focus attention.
Debug
AutoFormal's debug environment has some useful parts:
- Range violation checks that show whether a violation is out
of bounds in the high or low direction.
- Automatic VCD traces - show the sequence of events leading to
a failure, along with the time of the failure. This is useful
when you see an issue and are not 100% sure how to trace back
to the source.
I'd definitely recommend Ascent AutoFormal. It's simple and powerful,
and Real Intent's root cause report really helps you to pinpoint areas
of interest.
I see no reason for designers to *not* use it.
---- ---- ---- ---- ---- ---- ----
Our verification guys are trying to talk design management into buying
some RealIntent AutoFormal licenses.
---- ---- ---- ---- ---- ---- ----
Related Articles
Real Intent Meridian CDC & Verix CDC tools take Best of 2019 #3a
Ascent Lint less noisy vs. SNPS Spyglass makes Best of 2019 #3b
Real Intent Meridian RDC has 20X less noise gets Best of 2019 #3c
Real Intent's AutoFormal *formal* linting makes Best of 2019 #3d
Join
Index
Next->Item
|
|
