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.
lists which types of defects were found with formal verification:
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.