Formal verification experiences

Several companies have used formal verification to perform silicon bug hunting. That is one of the most advanced usages of formal verification. It is a complex process that includes incorporating multiple sources of information and managing numerous success factors concurrently. This paper will present a “spiral refinement” bug hunt methodology that captures the success factors and guides the deployment of various formal techniques. The objective is to identify the significant challenges and gradually improve each of the factors to “zero-in” on the critical bugs.

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.