Formal verification experiences
Spiral refinement methodology for silicon bug hunting
The “spiral refinement” bug hunt methodology
Formal verification has been used successfully by a lot of companies to verify complex SOCs [1][2] and safety-critical designs [3]. As described in [1][5], it has been used extensively for A, B, C:
Assurance, to prove and confirm the correctness of design behavior.
Bug hunting, to find known or explore unknown bugs in the design.
Coverage closure, to determine if a coverage statement/bin/element is reachable or unreachable.
Using formal verification to uncover new bugs is emerging as an efficient verification approach when functional simulation regression is stabilized and not finding as many bugs as before. In this paper, we will focus on the most advanced usage of formal verification: silicon bug hunt. Based on our experience, silicon bugs are incredibly tricky. Most of them happen deep in functional operation under unusual combinations of events and scenarios. We had tried various sophisticated approaches and gathered significant experiences in this area.
Experienced formal verification users know how to refine the results of formal verification intuitively. However, new users have found this skill challenging to master, hence, lead to frustration and disappointment. In this paper, we capture the refinement process into a step-by step methodology, formulate it graphically so that it is easy to understand and replicate.