( DAC'20 Item 04c ) ----------------------------------------------- [03/09/21]
Subject: OneSpin extensible ABV plus formal linting is the Best of 2020 #4c
YOU CAN TWEAK IT: The core strength OneSpin ABV has is that it's tweakable
as a tool overall. For example, one user talks about tweaking OneSpin such
that his company has a custom app just so DV-Verify auto-generates assertions
for their proprietary internal programming language.
A different customer loves DV-Verify because he can access it at such a deep
low-level, he can create their own in-house OneSpin extensions to create a
whole set of custom formal tools just for his company's unique design style.
Try doing this with JasperGold or Questa Formal or VC Formal! (Good luck!)
Why can you tweak OneSpin SW? Because years ago OneSpin originally started
out as a "formal parts" EDA tool vendor.
KICKASS FORMAL LINT: The other thing the users liked in this year's survey is
OneSpin's main app, DV-Inspect, which is a formal linter that does functional
checks that complement what a normal RTL linter does.
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
QUESTION ASKED:
Q: "What were the 3 or 4 most INTERESTING specific EDA tools
you've seen in 2020? WHY did they interest you?"
---- ---- ---- ---- ---- ---- ----
Hi, John,
A few years ago I saw the user comments on DeepChip saying OneSpin was
a powerful tool. I told my management and that started us looking at
it. It's now my turn to pay it forward to others.
OneSpin DV-Verify takes your RTL code and the companion assertions and
verifies that your assertions hold true 100% of the time for your RTL
code.
Here's our case where we had two assertions hold true and all the others
failed.
If DV-Verify finds a failure, you double click on it, and it creates
a counterexample (Witness) to show you exactly how:
- all the signals that lead to the assertion fail, and
- the sequence that causes that assertion to fail
OneSpin gave us a two-day training on DV-Verify. After day two, I went
home, wrote an assertion, and ran the tool. I got immediate results for
something I would not have found until downstream in the flow otherwise.
(click on pic to enlarge image)
|
The tool has complex menus, but once you have a working example, it's
easier to use. You *must* keep your file size reasonable, as it's easy
to overwhelm a formal tool. I've run 600 assertions on a small file in
only 30 seconds.
If you have enough assertions covering your design, you can make sure it
works before running dynamic HDL simulations. For certain cases you'd
still need to run simulations, e.g. for system-level verification vs.
the nitty gritty in your design blocks.
You can run endless simulations and still not find a bug. However, if
you run formal using good assertions, you *know* you have a good design.
That's the power of formal verification. Each year OneSpin puts out a
holiday puzzle and you can solve it using simulation techniques (the
long way) or with OneSpin (the fast way). It always emphasizes the
power of a formal tool.
OneSpin has great customer service -- starting during the sales process
through using the tool, and well after the sale. They have a personal
touch. With OneSpin I get same day meeting with our AE (Sasha), who is
always willing to listen to our problems and help us overcoming them.
For example, we have a custom programming language. OneSpin created a
custom app to auto-generate assertions for us for our specific needs.
Then DV-Verify will verify it.
In contrast, with a big company, we submit a ticket and must then wait
a day for a response. No, thanks.
---- ---- ---- ---- ---- ---- ----
ONESPIN DV-VERIFY
We use OneSpin DV Verify to verify design IP after our design cycle is
complete -- in parallel with other verification methodologies. We
primarily use Verilog, SV, SVA languages, and occasionally PSL/VHDL.
We do IP verification for the DoD. This is critical to the Air Force's
plan for high re-use rather than continually re-purchasing the same IP
for each project.
This approach puts increased pressure on us assuring each highly re-used
IP is correct. To verify the IP, we use DV-Verify for block
verification, integration verification, and equivalence checking.
We are working towards developing our own in-house extensions as well as
partnering with OneSpin to develop specific IP verification capabilities.
OneSpin DV-Verify's biggest strength is the deep low-level control we
can get by using Tcl and through our OneSpin partnership.
Capacity / Performance
We've used DV-Verify on a 4 million gate design. OneSpin performance
was good, but keep in mind that the tool must be used appropriately.
We had to use black boxing to prevent unused parts of our design from
limiting DV-Verify's scope / performance.
Key Features & Apps
Quantify Observation Coverage. It uses a mutation algorithm. We are
currently branching out to use Quantify to actively verify IP.
DV-Inspect App. The automated structural and safety checks this
app provides is underrated in terms of utility. Much of the code we
evaluate is machine generated, which can lead to some surprising
mismatches. This app catches those mismatches!
The checks have been indispensable in evaluating such code on a large
scale and hunting down bugs. It can be quite time consuming, as the
errors would require a concerted effort to develop the tests to reveal
the problem. Just reviewing the DV-Inspect results is a great first
step in recognizing the true behavior of our design.
Connectivity App. Checks and assesses the connectivity between source
and destination signals laid out in the design specifications.
It provides a relatively simple workflow to write out the connectivity
specifications in a csv file, upload the csv file into the tool and
then automatically generate and verify the formal specifications against
the design. The IP assurance team has been able to perform and verify
connectivity checks with the RTL test articles provided to us by our DoD
customers.
Learning Curve
There are two distinct learning curves for DV-Verify.
- The learning curve associated with learning formal methods.
- The learning curve associated with learning OneSpin's tool suites.
Learning formal techniques is required for all formal verification
tools, regardless of the EDA vendor. It's easy to blame that curve on
the vendor, but I think it is inappropriate; it is important to learn it
all right away to prevent undetected errors or misinterpretation of
results.
Conclusion
I highly recommend OneSpin DV-Verify. OneSpin has been a critical
partner for us, both in supporting their tools and in prioritizing
new developments.
As a great example of that prioritization is there rapid development
of their RISC-V app. It was initially motivated by the DoD.
I especially recommend OneSpin products for people involved in sensitive
government projects. It's unusual in our industry to have both
excellent tool support and the ability to modify and expand the tool
lineup to meet emerging government needs so quickly.
They are a growing company that continues to operate with a startup
mindset. This is something we wish we could find a lot more of in the
EDA landscape.
---- ---- ---- ---- ---- ---- ----
I'm German. DV-Verify is good stuff! I recommend it.
---- ---- ---- ---- ---- ---- ----
I've known Raik for close to 15 years.
I am amazed how he and Jim Hogan took a failed OneSpin and not
only brought OneSpin back to life, but remade it into a successful
standalone EDA start-up in its own right.
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
ONESPIN DV-INSPECT
We use OneSpin DV-Inspect for coding rule checks, such as dead code and
redundant code, and for System-Verilog based formal verification, such
as APB4 bus protocol formal verification.
- It verifies that we have no unreachable design functions.
Our standard RTL linting tool cannot run dead code checks,
but DV-Inspect can.
- It also run tests for stuck signals and FSM transitions/states
before we do our full coverage simulation.
The largest block I've run through DV-Inspect it had several thousand
lines of code. In most cases, we don't need to write any assertions
to use it.
I'd recommend it -- it's a good tool to help to find design issues
before tape-out.
---- ---- ---- ---- ---- ---- ----
OneSpin DV-Inspect gives us an early, fast, and automatic way to detect
implementation issues with our RTL code.
Performance example:
- 8 blocks of 1656 lines
- Running a formal check with assertions took 0.99 seconds
We use it for the following checks.
1. RTL code syntactic and semantic analysis
e.g. Mismatch, Signal truncation / no sync, Sensitivity
issues, Unused signals and parameters
2. Activation/Coverage -- Ensures specific design functions can
be executed and are not blocked by unreachability.
e.g. Dead code checks, Stuck signals, FSM transitions & states
DV-Inspect is very convenient to use for early-stage design checks, even
before verification starts. OneSpin's support is quite good.
---- ---- ---- ---- ---- ---- ----
OneSpin's DV-Inspect is a formal app that our designers use for linting
their RTL source code; it checks their RTL for common mistakes.
- DV-Inspect is formal, so it can do many more checks than
a normal structural linter.
- You do not need to write assertions to use it.
- You also do not need to buy OneSpin's DV-Verify (their
main ABV tool) to use the DV-Inspect app. (Even though
we have both tools.)
DV-Inspect can be used by designers -- you don't have to learn how to do
formal verification or write assertions. Even so, it is a multi-level
tool, so takes some learning and expertise to use it fully.
It uses formal methods, so it takes longer to get good, detailed checks
than a standard linting tool. We do NOT run it block-by-block. Instead
I wait to use DV-Inspect at the top-level before doing heavy simulation
or formal. If you have a very large design, you'd need to break it up.
== DV-Inspect's Autochecks ==
1. Finite State Machines (FSM)
This check will show you dead RTL code that cannot be reached. For
example, if you have three state machines, A, B, and C, can you get from
state A to state C?
DV-Inspect also shows the different conditions to transition from state
to state. Finally, it will give you a warning that your RTL files have
changed since the last run.
2. Stick (Toggle) Coverage
This function shows you flip-flops or registers that stay constant at
either 0 or 1, instead of transitioning. Standard (non-formal) linting
tools don't offer this check.
If the tool finds no transition/toggle activity, it could because the
specification for the register was set to always be high.
However, it is more likely to be a mistake, such as a width issue. For
example,
- You may have allocated 10 registers, where only the lower
5 are used, while the upper 5 are not moving.
- You have too many leading bits in a calculation.
There are occasional false failures. E.g. in one case, I found a
failure related to an asynchronous loop -- formal doesn't know about
timing.
I've run this check on every project and I've found something every
time. Sometimes it is just junk code from a prior project, but
usually there is a legit problem that needs fixing.
3. General Checks
These are mostly math checks. For example, for an adder, DV-Inspect
will prove that the adder:
- Never overflows. E.g. if 2+2 assigned to a 3-bit field. This
stops it being truncated with not enough bits.
- No leading redundant bits. If 5+5 is assigned to 32 bits, the
tool will flag a width mismatch. DV-Inspect's formal analysis
would look at every single operation and determine that you
never have a large enough number to require 32 bits.
== Lint Browser ==
Although DV-Inspect's biggest "plus" is in its "Autochecks" functions,
it also has a lint browser. This is actually the first step I run.
This lint browser is closer in functionality to a normal linter. It
does have some noise, but less than a normal linter. To help reduce
the noise typical of normal lint checks, DV-Inspect lets you filter
between categories of checks, e.g. truncation, shift, and integer.
The structural checks are all available out-of-the-box. You don't need
to write any assertions. Below are examples of what DV-Inspect will
automatically find and flag "as is"..
1. Unused Parameters
The tool will highlight any unused parameters in your RTL.
2. "No sink" (a Signal is Not Used)
This can happen because you forgot to use the signal, or you just
mistyped it. It includes path details. The example below also
shows an asynchronous feedback loop.
3. Unused Module on Output Port
The tool will identify unused modules on your output port.
4. Init (Initialization) Checks
Checks that all flip-flops reset to a known value. For each
named group of flip-flops, the tool proves that every register
is reset to a known state -- or not.
5. Array Signals
Array of bits, or of registers (or other variables). Uses
formal techniques to determine if the value goes out of bounds
from what you allocated. Are you in bounds or did you overrun
it and try to access something that doesn't exist, such as
accessing memory beyond what you have?
6. Dead Code Checks
To debug dead code checks, you can double click to access the
built-in browser to view the actual RTL code for context.
---- ---- ---- ---- ---- ---- ----
We use DV-Inspect as a very detailed formal lint after SpyGlass.
---- ---- ---- ---- ---- ---- ----
Due to the runtimes required, we run 95% Synopsys SpyGlass
followed by 5% One-Spin DV-Inspect.
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
SYNOPSYS VC FORMAL AND SIEMENS QUESTA FORMAL
---- ---- ---- ---- ---- ---- ----
I suppose I should say VC Formal and Formality because we use it a lot.
---- ---- ---- ---- ---- ---- ----
Except for Calibre DRC/LVS, we're all most an all Synopsys house.
Frontend -- VCS, SpyGlass, ZeBu, VC Formal, Formality, PrimeTime
Backend -- Design Compiler, Fusion Compiler, Star-RC, Calibre
---- ---- ---- ---- ---- ---- ----
Our purchasing department says Synopsys VC Formal is good enough.
I'd rather we used JasperGold. It'd look better on my resume.
---- ---- ---- ---- ---- ---- ----
We were going to do JasperGold and Conformal LEC until our SNPS sales
guy dropped his pants and gave us VC Formal and Formality for a song.
---- ---- ---- ---- ---- ---- ----
I'm an olde tyme 0-in user who's been put on the Questa Formal train.
It works.
---- ---- ---- ---- ---- ---- ----
Related Articles
OneSpin's "going where Cadence isn't" approach is Best of 2020 #4a
Users say Jasper's 200K register block signoff is Best of 2020 #4b
OneSpin extensible ABV plus formal linting is the Best of 2020 #4c
Join
Index
Next->Item
|
|
