( ESNUG 562 Item 7 ) -------------------------------------------- [09/28/16]
Subject: And then Hardee corrects Jim Hogan's ABV and Formal Apps tables
My table summary of the 4 major players in formal verification tools...
My table summary on the 16 major types of Formal Apps...
- Jim Hogan
Vista Ventures LLC, OneSpin BoD Los Gatos, CA
From: [ Pete Hardee of Cadence ]
Hi, John,
There were 18 mistakes in Jim's original reference post on Formal ABV tools
and their associated Formal Apps. I documented and corrected those mistakes
in ESNUG 562 #6.
In this same spirit, I found an additional 24 mistakes in Jim's ABV tool
and formal apps comparison tables. Rather than belabour Hogon's errors,
here are the two correct comparision tables (with the corrections in red.)
I can't fault Hogan on this. He's an analog guy. His attempt at this
reference post was good, but it needed help to be 100% truthful. Even the
CEO of OneSpin, Raik Brinkmann, found 18 other additional "insufficiencies"
in Jim Hogan's orginal Formal Guide in ESNUG 558 #6 -- and Jim is on Raik's
board of directors!
- Pete Hardee
Cadence Design San Jose, CA
---- ---- ---- ---- ---- ---- ----
Below are the corrected 4 major players in formal verification tools.
(Look at the ABV metrics/gotchas in ESNUG 558 #3 if you have questions
about how Jim defined each row in this table.)
|
Formal ABV Tool
|
Cadence
Jasper, IFV
|
Mentor
Questa FV, Calypto
|
OneSpin
Verify
|
Synopsys
VC Formal
|
|
Performance-Capacity-Convergence Estimate
|
21 formal engines. Manual + automatic selection. Optimized Formal model. Mature autoprove strategies
|
~10 formal engines, Manual + automatic selection. Basic Formal Model.
|
15-20 formal engines, Manual + automatic selection. Optimized Formal model.
|
~4-5 formal engines. Manual selection. Basic Formal model.
|
|
Debug
|
Graphical debugger w/ formal based root cause, and what-if analysis. Trace generation. HDL test generation.
|
Graphical debugger w/ root cause analysis. Trace generation.
|
Graphical debugger w/ root cause analysis. Trace generation. HDL Test Generation
|
Graphical debugger w/ root cause analysis.
|
|
Setup and Control
|
Assertion templates. Ctrl signal recognition. TCL.
|
Some signal recognition. TCL.
|
Assertion templates. Ctrl Signal recognition. TCL.
|
TCL. Ask vendor.
|
|
Property types
|
Safety, Activation, Liveness, Coverage, Structural.
|
Safety, Activation, Structural
|
Safety, Activation, Liveness, Coverage, Structural.
|
Safety, Activation.
|
|
Standard Language Support Assertions
|
SVA, PSL, VHDL
|
SVA, PSL
|
SVA, PSL, VHDL, C
|
SVA
|
|
Coverage mechanisms
|
Assertion coverage. COI-based constraint and property analysis. Proof Core (accurate engine-level) coverage.
|
Assertion coverage.
|
Assertion coverage. Observation coverage.
|
Mutation analysis.
|
|
Formal-Stimulation Interoperability
|
Closed db read/write for an intelligent CDNS formal-simulation coverage and unified analysis. UCIS write.
|
Open db. UCIS read/write.
|
Open db. UCIS read/write.
|
Closed db read/write.
|
|
Engine Access
|
Parallel engine. (>1000 engines on server farm; flexible ProofGrid control) Standard license.
|
Standard license.
|
Parallel engine. Cloud support. Standard and token licensing.
|
Standard licence.
|
|
Access to Formal Expert AE Support
|
Large focused group of corporate AEs, large group of formal specialist FAEs, even larger group of formal-knowledgeable verification FAEs.
|
Small number of specialized AEs
|
Focused group of Field and Corporate AEs
|
Some experts recently hired
|
---- ---- ---- ---- ---- ---- ----
And here's the corrected 16 20 major types of Formal Apps.
(Look at the APPS metrics/gotchas in ESNUG 558 #4 if you have questions
about Jim's terminology or defintions.)
|
|
Formal App Vendor
|
Cadence
|
Mentor
|
OneSpin
|
Synopsys
|
Real-Intent
|
|
1
|
Register checking
|
Yes
|
Yes
|
Yes
|
-
|
-
|
|
2
|
Connectivity checking
|
Yes
|
Yes
|
Yes
|
Yes
|
-
|
|
3
|
Structural Property Synthesis/Generation
|
Yes
|
Yes
|
Yes
|
-
|
Yes
|
|
4
|
Activation Checks & Code Unreachability
|
Yes
|
Yes
|
Yes
|
Yes
|
-
|
|
5
|
Scoreboarding
|
Yes
|
-
|
Yes
|
Yes
|
-
|
|
6
|
Safety Fault Analysis
|
-
|
-
|
Yes
|
-
|
-
|
|
7
|
Security Verification
|
Yes
|
Yes
|
Yes
|
-
|
-
|
|
8
|
Clock Domain Crossing - Location
|
Yes
|
Yes
|
Yes
|
Yes
|
Yes
|
|
8
|
Clock Domain Crossing - Analysis
|
Yes
|
Yes
|
-
|
Yes
|
Yes
|
|
9
|
Power Domain Management
|
Yes
|
Yes
|
-
|
-
|
-
|
|
10
|
X Propagation Checking
|
Yes
|
Yes
|
Yes
|
-
|
Yes
|
|
11
|
Abstract Assertion Authoring
|
Yes
|
Yes
|
Yes
|
-
|
-
|
|
12
|
Sim-Trace Property Synthesis
|
Yes
|
Yes
|
-
|
Yes
|
-
|
|
13
|
Protocol Compliance
|
Yes
|
Yes
|
Yes
|
Yes
|
-
|
|
14
|
Sequential RTL
Equiv Checking
|
Jasper SEC app. Aimed at full proofs for sign-off i.e. infinite cycles
|
Calypto SLEC. 50 behavioral cycles.
|
360 EC-RTL. 50 cycles.
|
SpringSoft Hector. Maybe 10 cycles.
|
-
|
|
15
|
Arithmetic Precision Analysis
|
Yes
|
-
|
Yes
|
-
|
-
|
|
16
|
3rd Party App Marketplace
|
Yes. (Open platform enables users to create their own apps.)
|
-
|
Yes
|
-
|
-
|
|
17
|
Simulation Coverage Unreachability App
|
Yes
|
-
|
-
|
-
|
-
|
|
18
|
Architectural Modeling App
|
Yes
|
-
|
-
|
-
|
-
|
|
19
|
System-level Deadlock Detection App
|
Yes
|
-
|
-
|
-
|
-
|
|
20
|
Post-Silicon
Debug App
|
Yes
|
-
|
-
|
-
|
-
|
---- ---- ---- ---- ---- ---- ----
|
Pete Hardee spent 10+ years at Synopsys and CoWare trying to inflict SystemC
on the world. In 2010, Pete jumped over to CDNS to manage their
olde Incisive Formal and now their new JasperGold tools. Since Pete is Welsh
and was raised in the UK, the correct way to read this is with a British accent.
|
Related Articles:
CDNS Pete Hardee cites 18 mistakes on Jim Hogan's Formal Guide
Hogan on Cadence, Mentor, OneSpin, Real Intent, Synopsys formal
OneSpin CEO cites 8 "insufficiencies" in Jim Hogan's Formal Guide
---- ---- ---- ---- ---- ---- ----
Join
Index
Next->Item
|
|
