( DAC'19 Item 5c ) ------------------------------------------------ [02/28/20]
Subject: OneSpin in formal areas where Cadence is NOT is Best of 2019 #5c
CARVING OUT NEW NICHES: At DAC 2019, I gave Raik Brinkmann a hard time about
his OneSpin tools missing in action in my 2018 survey. His comeback was:
And sure enough, here's the users this year commenting on each of these
specialized 4 OneSpin apps. (It's common for formal tools to be sold as
an "app" instead of a standalone SW package.)
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
---- ---- ---- ---- ---- ---- ----
QUESTION ASKED:
Q: "What were the 3 or 4 most INTERESTING specific EDA tools
you've seen this year? WHY did they interest you?"
---- ---- ---- ---- ---- ---- ----
OneSpin FPGA App
Our university's cyber physical systems lab adopted OneSpin to assist in
our design of highly safe and secure FPGA-based devices for our sponsors,
including the energy industry and DoD.
Our lab has worked with a variety of tool chains and sees OneSpin as a
standout in formal-based FPGA design verification.
OneSpin's formal verification is a significant factor in highly critical
systems. Also, the fact that their tools work with other higher-level
design workflows -- such as the MathWorks Simulink model-based design
and engineering tools -- was critical for us as well.
---- ---- ---- ---- ---- ---- ----
OneSpin DV-Verify SystemC/C++ App
We use OneSpin DV-Verify for SystemC as early in the process as
possible. We view it as both a linter and a DV tool so the earlier
we run it, the sooner we can keep certain issues from propagating
throughout our code.
We began using it in early 2019. We justified our purchase based upon
DV-Verify removing defects earlier in our C design process with reduced
compute resource usage.
DV-Verify's biggest benefit for us is its application for SystemC.
- We are not aware of another Formal tool that has SystemC
support. Secondarily, the apps provide huge benefit with
little engineering investment.
- Although other formal tools provide simple apps, the checks
that they do are not as useful to our problem space as
those that OneSpin implemented.
We ran our evaluation with a OneSpin engineer onsite. After that, it
was easy for us to use the tool. We have hit some issues but have had
excellent support and bug fix turnaround from OneSpin's engineering
team.
Generally, the OneSpin SystemC/C++ app is easy to use:
- SystemC/C++ initialization checks. The app accurately
provided a list of uninitialized registers. We initially had
to screen them as many times, certain types of status
indicators are not reset -- this is normal from a procedural
standpoint.
- Array out-of-bounds. Earlier versions of the app used give
false checks on array out_of_bounds on "for" and "while"
loops, but now that is fixed.
- Overflows. The Integer overflow checks point out a few
coding-style issues. For example:
// this line shows as an integer overflow error.
sample_i_mult_out = sample_i_mult(13,2);
LHS is 12 bits, RHS is 18 bits with range selection. To avoid
an integer overflow check fail, an explicit cast is needed to
show that this is user-intended behavior
sample_i_mult_out = sc_int<12>(sample_i_mult(13,2));
We also used the tool to run the checks below, though it did not flag
any failures:
- Integer-redundant checks.
- Dead code / unreachable code.
- Potential simulation/synthesis mismatches
- Checks (intentionally) undefined reg effect
Finally, DV-Verify lets you specify assertions. We have not yet used
this but do plan to make the capability a part of our methodology.
(Since we have not used the assertions or the property checking
features, we cannot give feedback on nor recommend those features.)
OneSpin is currently the only game in town for SystemC. So, I can
easily recommend DV-Verify for SystemC/C++ by that metric.
We also think OneSpin's engineering support is a big reason to recommend
the tool. Their support has easily met or exceeded the support we've
seen from the Big 3 EDA companies.
---- ---- ---- ---- ---- ---- ----
OneSpin 360 DV - Floating Point Unit (FPU) App
Our floating-point hardware IP is heavily used for machine learning
and deep learning chips.
We use their FPU app, with its assertion-based VIP, to formally verify
our floating-point unit's System Verilog RTL code.
We initially did an eval with other vendors; but no other tool on the
market met our specific needs.
OneSpin supports the IEEE 754 floating-point specification, which is
terribly complex.
- They claim their FPU app is 100% compliant with the standard.
- They also claim it supports all operands (addition, subtraction
multiplication and division), rounding modes, and exception
flags.
We've used all the operands except for division, as our RTL did not
perform division.
OneSpin DV-FPU App vs Simulation
With simulation, it's hard to guarantee that you are compliant with the
IEEE 754 standard. You'd have to use external models for the RTL and
run lots and lots of simulations -- however, SV simulation with
constrained-random testbenches can only prove so many corner cases.
E.g. 32 x 32 bits would be impossible to prove with RTL simulation.
Without formal, you cannot have a full proof.
While with the OneSpin DV FPU app, you can prove compliance.
The way the FPU app works
- You use the FPU App's VIP library calls/functions to help you
write the assertions. The App has built functions for IEEE 754.
- The DV-Verify formal tool tries to break the assertions -- if
it doesn't break, you pass. If it does breaks, it tells you
the stimulus conditions that broke it.
FPU App examples
1. Multiplication operand
If I want to do multiplication, I write an assertion for it using the
library provided by OneSpin DV FPU app (versus writing it all on my
own).
The library functions are called IEEE_X and follow the IEEE format.
Additionally, with FPUs, when you multiply two numbers, it can become a
denormal number. There is a rounding node to see if it will be a small
or big number. OneSpin runs specific algorithms take care of this for
you -- rather than you having to going to the IEEE spec to do so.
2. Customized precision
OneSpin supports multiple precisions. So, as part of the library set up
function, you can configure your bit-widths to customize the precision.
We would specify single or half precision and the app would take care of
it. (OneSpin claims support for double precision also, but we have not
tested it.)
3. Comparison functions
OneSpin uses formal to compare, though it must first know what you want
it to compare against.
4. Functional Coverage
We used cover properties for the functional coverage of our FPU and were
fully covered per our specifications.
Case study -- Only 3 week ramp up
It only took us about 3 weeks to ramp up using the tool, including going
through a first-time learning curve. This was important for us, as we
didn't have budget to assign multiple team members full-time. The bulk
of our learning curve was learning the App and the library functions.
You set up your constraints for DV-Verify, which is simple. The app
uses OneSpin's DV-Verify formal verification tool under the hood -- so
you don't need to learn the tool.
- We tested the OneSpin DV-FPU App against a design we had
already (mostly) simulated, where we already knew we had bugs.
- Each operation took less than 5 minutes to get a full proof.
In our case we bypassed denormal, so it was fast
- OneSpin found the (known) bugs.
- The app also found a corner case. However, our implementation
was slightly different than the standard, so no changes were
needed.
We've now used the OneSpin DV-FPU app in production and taped out the
chip. We got the silicon back with no issues with the floating-point
unit (so far ... Knock on wood!)
OneSpin was a perfect fit for us. They have great support also.
We are very happy.
---- ---- ---- ---- ---- ---- ----
OneSpin Safety Critical Apps
OneSpin has a dedicated team working on solutions for safety critical
designs. They work closely with us (the customer) and are continuously
extending their safety portfolio.
We have some experience with the fault injection app and also had a
brief look at the propagation app:
- Fault Propagation App -- can formally prove that a fault is
redundant / cannot be propagated to functional outputs. This
helps reduce fault simulation time and prune the fault list.
- Fault Injection App -- can be used to support the calculation
of safety metrics for ISO 26262. It automatically injects
faults into the design and then evaluates whether the fault
can propagate to functional outputs, and whether it gets
detected by our built-in fault detection mechanisms.
The strength of this approach is that it is exact: if the
formal tool classifies a fault as safe the user can be certain
that there exists no scenario where the fault can affect the
output without being noticed.
We are not currently using these safety critical apps in production;
however, we intend to employ them in future.
Once every few years we have a look at formal tools from other vendors.
Our experience is that the OneSpin's formal engines are best at solving
hard formal problems, whereas other tools may be faster at solving
simpler formal problems and may have better debugging capabilities.
I'd certainly recommend DV-Verify. It has features that no other formal
tool provides. It's a good value for money and continues to have the
best cost-benefit ratio.
---- ---- ---- ---- ---- ---- ----
Related Articles
OneSpin DV-Verify's surprise comeback in ABV is Best of 2019 #5a
Cadence JasperGold still formal ABV favorite is Best of 2019 #5b
OneSpin in formal areas where Cadence is NOT is Best of 2019 #5c
Join
Index
Next->Item
|
|
