Design Article
Case Study: Can you afford to ignore formal analysis?
Joachim Knäblein and Hans Sahm, Alcatel-Lucent
11/30/2010 10:15 PM EST
Verification results
At the end of the verification process, 20 design blocks of varying complexity the HW/SW interface, data stream processing modules, FSMs, memory-controlled data processor were checked by the formal verification team. The following tables show some of the results.
Table 1 lists which types of defects were found with formal verification:
At the end of the verification process, 20 design blocks of varying complexity the HW/SW interface, data stream processing modules, FSMs, memory-controlled data processor were checked by the formal verification team. The following tables show some of the results.
Table 1 lists which types of defects were found with formal verification:
Table 2 lists the actions which were taken when a defect was found:
Finally, Table 3 shows a classification of the defects according to the likelihood of finding these defects during an extended simulation-based verification.
As a conclusion, formal verification found around 30 really critical defects that were missed or likely would have been missed by simulation. These defects were critical, so that we implemented hardware design modifications despite being in the late stages of design.
It is in the nature of this two-step approach – first simulation then formal verification – that the additional detected defects were mainly corner cases. Corner-case verification is vital. In the field, the system is subject to a number of stimuli exceeding that of the simulated stimuli by many orders of magnitude. Thus, exotic corner cases can – and do – easily occur. If systems fail sporadically in the field, it is typically very hard to find the cause. Although exotic defects may occur rarely, when they do occur, they can cost a great deal. This is why they must be eliminated early in the design phase before tape-out. The formal methods developed in the HERKULES project proved to be an effective means to achieve this goal.
It is in the nature of this two-step approach – first simulation then formal verification – that the additional detected defects were mainly corner cases. Corner-case verification is vital. In the field, the system is subject to a number of stimuli exceeding that of the simulated stimuli by many orders of magnitude. Thus, exotic corner cases can – and do – easily occur. If systems fail sporadically in the field, it is typically very hard to find the cause. Although exotic defects may occur rarely, when they do occur, they can cost a great deal. This is why they must be eliminated early in the design phase before tape-out. The formal methods developed in the HERKULES project proved to be an effective means to achieve this goal.
|
|
|
|
|
Navigate to related information
jadesbox
12/10/2010 3:35 AM EST
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?
Sign in to Reply
jknaeblein
12/16/2010 4:30 AM EST
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.
Sign in to Reply