Design Con 2015
Breaking News
Comments
Newest First | Oldest First | Threaded View
jknaeblein
User Rank
Rookie
re: Case Study: Can you afford to ignore formal analysis?
jknaeblein   12/16/2010 9:30:35 AM
NO RATINGS
Hi jadesbox, thank you for your inquiry. Some remarks related to your questions: The two-teams-approach, of course, was only possible due to the fact that we had some funding by the german government for this. Yes, we also tried to re-simulate bugs, which had been found with formal simulation. The typical procedure, when a bug was found in the formal domain, was to contact the block designer. The block designer took the stimuli of the counterexample, tried to reproduce the bug in simulation to understand what's happening and corrected it. Then we redid the formal verification part to check if the bug really disappeared and no new bug had been introduced by the fix. We tried to run the SVA assertion in simulation as well, but they did not run out-of-the-box. The reason was that currently formal and simulation tools support different SVA subsets and interpret some SVA constructs differently (see article). So it was quite a hard job to migrate formal properties to simulation. Moreover, doing a migration in the direction as proposed seems to me to be of an academic nature. With the claim of the formal approach to be exhaustive, simulation can only detect bugs, which have been found previously by formal.

jadesbox
User Rank
Rookie
re: Case Study: Can you afford to ignore formal analysis?
jadesbox   12/10/2010 8:35:17 AM
NO RATINGS
Nice to see 2 teams running in parallel to really assess dynamic and static verification benefits (usually case studies first use a verification then teh other and conclude only on the missed bugs of a method, not a real comparison!) You've run the Formal verification on the design that was only verified and debuged via simulation based verification.But did you try the simulation based verification environment on the Formally verified only design? By the way, did you run the SVA assertions dynamically as well? were they able to catch the bugs without running Static Fomal analysis?



Most Recent Comments
Linzee
 
rick merritt
 
rick merritt
 
Anand.Yaligar
 
Anand.Yaligar
 
Anand.Yaligar
 
Anand.Yaligar
 
Anand.Yaligar
 
resistion
Top Comments of the Week
Flash Poll
Like Us on Facebook

Datasheets.com Parts Search

185 million searchable parts
(please enter a part number or hit search to begin)
EE Life
Frankenstein's Fix, Teardowns, Sideshows, Design Contests, Reader Content & More
Max Maxfield

Tired Old iPad 2 vs. Shiny New iPad Air 2
Max Maxfield
6 comments
I remember when the first iPad came out deep in the mists of time we used to call 2010. Actually, that's only four years ago, but it seems like a lifetime away -- I mean; can you remember ...

<b><a href=Betajet">

The Circle – The Future's Imperfect in the Present Tense
Betajet
5 comments
The Circle, a satirical, dystopian novel published in 2013 by San Francisco-based writer Dave Eggers, is about a large, very powerful technology company that combines aspects of Google, ...

Martin Rowe

Make This Engineering Museum a Reality
Martin Rowe
Post a comment
Vincent Valentine is a man on a mission. He wants to make the first house to ever have a telephone into a telephone museum. Without help, it may not happen.

Rich Quinnell

Making the Grade in Industrial Design
Rich Quinnell
16 comments
As every developer knows, there are the paper specifications for a product design, and then there are the real requirements. The paper specs are dry, bland, and rigidly numeric, making ...

Special Video Section
The LT8640 is a 42V, 5A synchronous step-down regulator ...
The LTC2000 high-speed DAC has low noise and excellent ...
How do you protect the load and ensure output continues to ...
General-purpose DACs have applications in instrumentation, ...
Linear Technology demonstrates its latest measurement ...
10:29
Demos from Maxim Integrated at Electronica 2014 show ...
Bosch CEO Stefan Finkbeiner shows off latest combo and ...
STMicroelectronics demoed this simple gesture control ...
Keysight shows you what signals lurk in real-time at 510MHz ...
TE Connectivity's clear-plastic, full-size model car shows ...
Why culture makes Linear Tech a winner.
Recently formed Architects of Modern Power consortium ...
Specially modified Corvette C7 Stingray responds to ex Indy ...
Avago’s ACPL-K30T is the first solid-state driver qualified ...
NXP launches its line of multi-gate, multifunction, ...
Doug Bailey, VP of marketing at Power Integrations, gives a ...
See how to ease software bring-up with DesignWare IP ...
DesignWare IP Prototyping Kits enable fast software ...
This video explores the LT3086, a new member of our LDO+ ...
In today’s modern electronic systems, the need for power ...