( DAC'16 Item 1c ) ---------------------------------------------- [12/09/16]
Subject: OneSpin's #2 in #1 "Best of 2016", the "we try harder" company
WE'RE THE OTHER GUYS: If you read earlier parts of this survey (DAC'16 #1b)
you'll see that with the Formal tool users that OneSpin DV-Verify has a
lot in common with Cadence JasperGold. Both have newfound capacity gains,
both do deep proofs, both have formal apps, both take SVA & PSL, both read
Verilog/VHDL/SV, plus both have a variety of formal engines.
Looking deeper into the comments, Jasper comes off as the Coca Cola of ABV
tool vendors. JasperGold is a stable, mature tool. It has a nice mix of
tried-and-true Formal apps and a very advanced debug environment that its
users love. And with 17 solid years in businesss, JasperGold has a large
user base and CDNS Sales loves selling JasperGold at a hefty mark-up.
Conversely, OneSpin appears to be the Diet 7 Up of ABV tool vendors. It's
a newer soda that's sold worldwide, but it's not as established as the 130
year old Coca Cola brand is. Both do their job, and OneSpin's debug
environment works well with some unique features, but it lacks many of the
sexy bell-and-whistles that the JasperGold Visualize debug environment has.
OneSpin's capacity is better on some designs, but Jasper does better on more
designs. Both have a full range of Formal Apps, but Jasper's are more well
known overall. OneSpin has a user base, but it's 1/4th the size of Jasper's
user base. And while DV-Verify ain't cheap, it doesn't get the mark-up that
JasperGold gets.
(I could go on, but I think you get my point...)
Using EDAC's last 4 quarters (2H15 + 1H16) the total Formal ABV market is
around $84 million total. One spy told me it ballpark breaks out to:
Cadence Jasper : :############################# $58M (69%)
OneSpin : :###### $12M (14%)
Mentor Questa FV : :## $4M (5%)
Synopsys VC Formal : :# $2M (3%)
While another spy told me it ballpark breaks out to:
Cadence Jasper : :######################### $50M (60%)
Mentor Questa FV : :########## $17M (20%)
OneSpin : :##### $11M (13%)
Synopsys VC Formal : :### $6M (7%)
Of course, these numbers exclude all equivalence checkers and linters; it's
only about the pure F-ABV tool market.
---- ---- ---- ---- ---- ---- ----
So I phoned Jim Hogan asking: "why is OneSpin 1/4th the size of Jasper even
though both companies' technologies started in 1999?"
First thing is Jim did was he corrected me by saying OneSpin is more like
Diet Mountain Dew. Me: "why?" Jim: "I like Mountain Dew better than 7 Up."
Anyway, when Jim got serious he told me a complicated investment fable about
how EDA start-ups have to "get past the Valley of Death"... I didn't quite
grasp what he was saying until he emailed me this graphic:
"Jasper got out of its Valley of Death in 2006. OneSpin got through
its Valley of Death in 2012.
After that, Kathryn had Jasper working on Formal apps 3 years before
OneSpin. That's a 3 to 6 year head start Jasper had.
Also, Jasper focused heavily on selling apps and AE's in North America,
while at the same time OneSpin focused on an automotive F-ABV tool for
Europe and Japan. That paid well for Jasper, but not for OneSpin.
By 2012, with fresh capital, Raik expanded OneSpin into North America
plus he added apps and strong coverage to his portfolio. OneSpin is
working hard to close that gap with Jasper."
- Jim Hogan, EDA investor & OneSpin MoB
So in a nutshell, OneSpin made some wrong business & technology turns, but
has righted the ship and is charging against Cadence full speed ahead now.
"Mistakes are always forgivable, if one has the courage to admit them."
- Bruce Lee, Hong Kong actor & martial artist (1940 - 1973)
---- ---- ---- ---- ---- ---- ----
WHY SMALL IS BIG: Three big upsides OneSpin have is because they're small,
they treat even smaller customers as if they're Intel, Apple, or Qualcomm;
plus DV-Verify sells for a much cheaper price than JasperGold does. And
for some reason, at least 4 users said they liked how OneSpin is does the
assertion Coverage thing -- yet no one likes how Jasper does it. (Huh?)
SORRY SYNOPSYS, SORRY MENTOR: there's a fourth (unstated) advantage that
OneSpin has in the Formal ABV tool market. If you look at the user
comments, not one stood up to gush about Aart's new VC Formal nor to gush
about Wally's Questa FV tool. Did you catch that? OneSpin #2 in a 2 tool
market! Synopsys & Mentor were F-ABV no shows.
"I don't get no respect..."
- Rodney Dangerfield, American comedian, (1921 - 2004)
QUESTION ASKED:
Q: "What were the 3 or 4 most INTERESTING specific EDA tools
you've seen this year? WHY did they interest you?"
---- ---- ---- ---- ---- ---- ----
We did an evaluation of OneSpin DV-Verify formal verification, and have
since licensed it.
We are a design services company, and our main application areas are
automotive, safety critical, and medical. Safety critical in general
is a main focus for us.
I've done formal verification in the past with tools such as Averant
Solidify (10 years ago) and Cadence IFV (5 years ago). About a year
ago, we evaluated Cadence Jasper; our OneSpin DV-Verify eval was this
year. We also enquired multiple times with Synopsys regarding their
new formal tool VC Formal.
1. Performance and Convergence
Having worked with other ABV Formal tools before, we were well
aware that huge performance and capacity differences exist.
This was an important part of our evaluation criteria.
We chose some of our existing designs which had proven problematic
with Cadence Jasper because
- JasperGold couldn't handle the required deep proofs
(e.g. 1,000's of cycles because of long delay counters), or
- We needed significant manual effort to guide the JasperGold
solvers.
With OneSpin DV-Verify, we were able to come to full proofs without
manual intervention. OneSpin seemed to be able to indeed find
deeper proofs as compared to JasperGold a year earlier.
In general, I've seen formal tool capacity increase from say around
250 cycle proof depths in reasonable time on a relatively small
design with a fair bunch of inconclusives 10 years ago -- to now
towards 10,000 cycle proofs on similar designs and around 1,000
cycle proofs on complete subsystems today.
This new capacity makes advocating for formal inside my compant so
much easier as it's very hard to explain inconclusives/bounded
proofs to management.
2. Set-Up Time
We were up and running DV-Verify within only a few hours, i.e. from
download and install to proofing our first modules and subsystems.
- OneSpin' setup is extremely easy as their tool automatically
detects clocks and resets.
- The basic OneSpin flow is: read Verilog/VHDL/System Verilog
with some assertions, and then prove. It couldn't be simpler
in my opinion.
- For more complex clocking the OneSpin tools had all the
necessary infrastructure.
Our normal tool evaluation flow is to ask the vendors to *not* send
an FAE to help us do the initial runs. Instead we want to have a
clear idea on how easy it is to use the tool ourselves and how well
the manuals are written.
This went very well for the OneSpin tools.
3. Formal Engine Selection
DV-Verify's engine selection heuristics do a very good job right
out of the box. We've only had a few deep proofs where we decided
to hand guide the OneSpin solver selection process.
As an end user we're not so concerned with the *number* of engines
a Formal tool has. What matters most is if the Formal tool can come
to a true/false statement rather than a bounded proof.
4. Observation Coverage
We routinely run DV-Verify's "quantify" coverage command after
design debug to get an idea what our assertions cover.
For novice users coming from HDL code (line) coverage this can be
a bit confusing as consecutive lines in a block can have different
coverage results. However, after a bit of explaining they quickly
get the idea.
5. Running System Verilog & PSL Assertions
We mostly run inline PSL assertions on VHDL code. With the OneSpin
tools we've not yet felt the need to use SystemVerilog assertions
(SVA), but this is still on our mind for some more exotic proofs
where PSL offers less features compared to SystemVerilog.
Comparing the tools:
- OneSpin supports PSL & SVA.
- Cadence Jasper supports PSL & SVA.
- Synopsys VC Formal doesn't support PSL, only does SVA.
Binding additional SystemVerilog assertions to an existing block is
very straightforward with OneSpin.
6. Debug
OneSpin's debugging is straightforward, though it's a bit basic
compared to the Cadence JasperGold debugger which offers more
features for what-if kind of analysis and automated "signal of
interest extraction" on the counterexample waveforms.
The OneSpin GUI looks very basic to the JasperGold GUI -- the
Jasper people clearly put a lot of effort into eye candy and
support for debug and exploration.
7. Customer Support
OneSpin's customer support system works very well.
- We always get feedback from OneSpin Support within a few hours,
and if a show stopper pops up, the're very quick to either
suggest a workaround and/or their R&D will compile a tool
update to fix the issue.
- Their support team also keeps us updated on their internal
progress fixing any issues. So we never have the worry that
our feedback is going into a big black hole or that we'd be
lucky if it ever got fixed.
OneSpin seems very focused on delivering good quality top-notch
products. The biggest strength of DV-Verify is that every release we
see actual improvements and progress.
OneSpin Is Tech Savvy & Small Customer Friendly:
With OneSpin we very quickly moved past the sales and marketing bla bla,
got in touch with their technical guys, did our thing, and licensed the
tools. We love this kind of efficiency as it keeps us focused on what
pays for the tools: designing and selling working chips.
For a smaller company such as ours, it's sometimes not easy to get past
the sales teams of bigger EDA companies who often seem uninterested in
"peanuts" accounts.
We were shopping for a hardcore formal tool and the way the OneSpin
token-based licensing works, we can also use the DV-Verify formal engine
tokens for their lighter DV-Inspect at no extra cost.
We were positively surprised by it, and use it frequently to assess
design quality and to point to areas of concern before doing any
behavioral or RTL simulations.
During my career I've used formal numerous times to "harden" modules
that were always in a state of flux due to the designers adding more
exception logic for every fail in dynamic simulations.
- In the end, we usually ended up with a very clean and readable
design as formal makes you think deeper about the function.
- The turnaround time is much faster than just running another
overnight regression.
That last sentence (faster turnaround) seems to trigger the big EDA
companies to put unrealistic prices on their formal tools -- for fear
it would eat away on their number of Verilog/VHDL/SV simulator sales.
That reasoning is totally flawed in my opinion. Formal allows the
verification guys to focus more on the real top-level functional bits
instead of having to trace faults in deep in the logic -- so they can
focus on producing more top-level test cases -- which in term is going
to require *more* simulator licenses (good for EDA Vendors) and
provide better quality (good for us).
---- ---- ---- ---- ---- ---- ----
We've been using the OneSpin DV-Verify formal tool for years now, mainly
on positioning designs in the past, and are currently expanding to also
use it for other product areas.
DV-Verify is actually collection of tools to use for different formal
checks via writing/proving assertions, along with push-button automated
checks (apps) that examine your RTL code and look for potential problems
with it. If you purchase the full-fledged OneSpin formal package, with
writing assertion and proving them, the formal apps come with it. Or
you can just buy the automated formal apps, and not the formal tool.
It's hard to put a number on OneSpin's capacity, as it depends on the
complexity of logical functions ultimately translating to state-space.
OneSpin's performance is quite good at the block level. At the
top level it becomes difficult, but not impossible. This is where
designer's creativity kicks in: there are always clever ways of
splitting proofs.
Observation Coverage is fairly new development for them. It's very
interesting, especially if you want to quantify where you stand with
your RTL with regard to your coverage. It's hungry in compute
resources, and takes an overnight run. I think this functionality is
unique to OneSpin.
OneSpin's safety critical functionality is something we will probably
look at soon. Essentially, it's similar to mutation analysis, which is
used for observation coverage, but the purpose is to inject faults, then
do the analysis as to whether they trigger your safety circuitry and how
faults propagate. (I'm describing this based on what I've heard as we
haven't used it yet.)
We use OneSpin with VHDL and Verilog. Most of our designs are mixed
language and it works fine -- no complaints. They've been supporting
mixed language flows for years; I think they are quite mature in that
regard.
Their debug is stable. They have efficient debugging, annotated
assertions and source code, a fan-in tracer and a good waveform viewer.
I would definitely recommend OneSpin. It's static code analysis is a
must for designers, and the same is true for its register checking.
For the verification experts: OneSpin also offers operation-based
verification methodology based on their TIDAL library. Anyone doing
processor-like designs should look into it.
DV-Verify's main value is coverage. If you start applying it early
enough it will guarantee your circuit is cleaner and have less problems
later. A lot depends on how much quality you need, e.g. for consumer
applications, I imagine it's less rigorous. As you go toward safety
critical it's a must.
---- ---- ---- ---- ---- ---- ----
I visited OneSpin at DAC.
I've only recently started investigating formal verification
methodologies for our designs, and interested to know what the industry
offered in this area.
Here is my feedback on OneSpin's DAC demo on their DV-Verify Assertion
Based Verification tool:
- The demo was insightful. We went over a few example cases on
running OneSpin's formal tools and provided coverage metrics
using assertions.
- Their code and functional coverage discussion was useful from a
theoretical perspective.
- We touched on verification using formal techniques like checking
for resets and X-propagation, etc. and cutting down on direct
RTL simulation-based testing time and effort.
- We briefly touched on functional safety. This is a critical
goal for my industry, so I was very interested in it.
Overall, their presentation was useful.
(My other experience is primarily with Mentor Graphics' 0-in/Questa
formal verification tools.)
---- ---- ---- ---- ---- ---- ----
Our experience with formal has been with OneSpin and JasperGold.
We verify control-logic heavy ASICs for custom applications. Over the
course of several years, we have tried 4 formal verification tools and
invested in Jasper and OneSpin for our production verification work.
Our workflow involves formal property verification: formal properties
are written against a design in SVA and then are loaded into the tools
along with the design.
All 4 of the formal tools that we have seen can ingest designs in VHDL,
Verilog, SystemVerilog, and formal properties in SVA (PSL, OVA etc...)
The differences in the 4 tools come down to:
1) ease of use
2) performance
3) cost
For a given property, the verification tool will tell you one of the
following:
1. Give indication that the property holds for your design.
2. Indicate that the property doesn't hold, and provide a
counter-example showing that property's failure.
3. Keep chugging along and not provide a result. (In this
case the property may have to be rewritten, additional
assumptions or abstractions made)
For simple properties with low complexity and limited time-span, the
formal tools perform similarly and produce results quickly. The tools
diverge in 1) the performance on complex properties and 2) how to debug
and visualize counter-examples.
OneSpin and JasperGold both have strengths and weaknesses.
OneSpin's comparative strengths are:
- Very good support for VHDL.
- OneSpin is cheaper. Bundling of essential features with their
core formal tool provide good value for the cost.
- Having a Windows version in addition to the usual Linux binary
(their Windows version doesn't do parallel processing).
OneSpin's weaknesses are:
- Debugging counter-examples: it cannot currently add custom
expressions to their debug waveform, or modify the property
that failed within the debug session.
- Performance of engine verification: Good but not as good as
Jasper's.
Jasper's strengths are:
- Debugging is superior. The counter-example debugging features
allow a "what-if" analysis by adding custom expressions and
constraints to the counter-example on the fly and update. This
makes the use of JasperGold very efficient.
- The verification engines in Jasper have a better performance than
all the other tools that we have used or tried.
Jasper's weaknesses are:
- For sophisticated VHDL designs, there are VHDL features that are
not supported or parsed correctly.
- Jasper's cost model requires licenses for every feature/app
(formal property verification vs X-propagation vs. static linting
vs code coverage etc.).
- Also, sometimes even manually written properties require an App
license. For example, we have encountered that a formal
property, manually written in SVA (involving X's) fed to the
JasperGold formal-property verification tool will not be verified
if you don't also have the X-propagation license.
OneSpin's overall advantages are in its support for VHDL and in
providing good value for the cost. OneSpin DV-Verify includes all the
common features (property verification, linting, code coverage, state
machine checks) etc.
Comparing exact costs is tricky due to the lack of standard pricing for
any of these tools, but we have found that OneSpin with all the extra
bundled features is similar in cost to the Jasper property verification.
---- ---- ---- ---- ---- ---- ----
OneSpin. It's the next best thing to Jasper.
It's not as powerful as Jasper, but has most of the basic functions.
OneSpin has grown in the past few years. They now have support
engineers in U.S.
---- ---- ---- ---- ---- ---- ----
OneSpin gave us an in-depth presentation at DAC.
Their DV-Verify formal ABV product seems easy to use.
Plus, designers can run it early without much setting up to sanitize the
source code before running simulations.
---- ---- ---- ---- ---- ---- ----
OneSpin DV-Verify.
Its formal ABV technology for identifying non-propagating faults is
differentiating.
OneSpin has some of the most innovative formal tools in the business.
---- ---- ---- ---- ---- ---- ----
OneSpin's DV-Verify RTL-to-RTL equivalency checking looked good.
---- ---- ---- ---- ---- ---- ----
Related Articles
How engineers feel about Formal verification vs. RTL simulation
Jasper's #1 in #1 "Best of 2016", through killer capacity & debug
OneSpin's #2 in #1 "Best of 2016", the "we try harder" company
And how JasperGold compares to OneSpin in the Formal Apps biz
Join
Index
Next->Item
|
|
