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?



Flash Poll
Top Comments of the Week
Like Us on Facebook
EE Times on Twitter
EE Times Twitter Feed

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

Feast Your Orbs on My Jiggly Exercise Machine
Max Maxfield
50 comments
Last weekend, I was chatting with my mother on the phone. She's all excited that I'm coming over to visit for a week in November. "I'll be seeing you in only seven weeks," she trilled ...

latest comment kfield Toy....or agony? :-)
Glen Chenier

Missing Datasheet Details Can Cause Problems
Glen Chenier
3 comments
It is often said that "the devil is in the details." All too often those details are hidden deep within a datasheet, where you can easily overlook them. When a datasheet reference circuit ...

David Blaza

RadioShack: The End Is Nigh!
David Blaza
123 comments
I'm feeling a little nostalgic today as I read about what looks like the imminent demise of RadioShack, at least as we currently know it. An old ubiquitous cartoon image popped into my ...

Larry Desjardin

Engineers Should Study Finance: 5 Reasons Why
Larry Desjardin
47 comments
I'm a big proponent of engineers learning financial basics. Why? Because engineers are making decisions all the time, in multiple ways. Having a good financial understanding guides these ...