The best paper winner at DVCon 2021 details a comprehensive methodology for making the best use of formal verification for bug hunting
Winner of the Best Paper Award at DVCon US 2021, Formal Verification Experiences: Spiral Refinement Methodology for Silicon Bug Hunt shares the trade secrets of experienced formal verification engineers so that new users can master the skills required to capture elusive silicon bugs in their designs.
Based on the authors’ experience, silicon bugs are extremely difficult to track down. Most happen deep in functional operation under unusual combinations of events and scenarios. As a result, the silicon bug hunt demands the most advanced weaponry in formal verification, assembled after years of experience testing various sophisticated approaches in this area.
The paper packages the formal verification refinement process based on this deep experience in a step-by-step methodology – the ‘spiral refinement’ bug hunt process. It has six main steps:
- Identify formal experts who can help with a project (this is most likely a management task).
- Use information from the lab, through divide-and-conquer or a process of elimination to identify the buggy modules.
- Write assertions to capture pre-conditions, bug scenarios, and if possible, the sequence of events.
- Identify and extract a set of good initial states from simulation traces.
- Run formal verification with minimal constraints to ensure formal has good reachability into the design.
- Refine the constraints and assertions to zero-in on the actual bugs.
The refinement process incorporates all the factors that determine the successful use of formal verification on a project. Various formal teams from multiple companies have identified six key factors based on their experiences:
- The complexity of the design.
- The quality of the sub-goals and target assertions.
- The completeness of the interface constraints.
- The control and orchestration of the formal engines.
- The quality of the initial states for formal exploration.
- The formal expertise of the users.
As shown in Figure 1, these factors can also be visualized as a type of spiral refinement radar to help users manage them and allow managers to visualize them. Combined with the new methodology, they capture the proven successful qualities of advanced formal verification techniques and help guide the deployment of various approaches. The process identifies any obstacles then gradually improves or refines each one so that users can zero-in on a bug in silicon. Once a bug has been identified, the formal verification environment can serve as a golden setup to verify any potential software and RTL fixes. The overall process is very efficient in reducing the turn-around time and helps prevent the introduction of new issues.
We can bring all this thinking together across three phases of a typical project: Initial, Improved and Final.
Phase 1: Initial
A. Complexity of the design
- It is unrealistic to expect formal verification to handle the complete SoC design, so achieve greater efficiency by focusing on the IP blocks with standard interfaces.
- Remove those blocks or functionalities that are not relevant for the properties.
- Turn memories and storage structures into black boxes.
B. Accessibility of formal experts
- Before deploying formal verification on a design, you must secure someone with formal expertise.
- Much like a simulation regression that will require a testbench environment, a formal regression will require a formal test environment as well. You need to construct one that consists of assert and cover properties, constraints for standard and proprietary interfaces, models for complex and formal unfriendly modules.
- More importantly, get your formal expert in the team to work with the designers to capture the design intents in properties and help those designers run formal verification on the blocks early in the design cycle as the RTL is being developed.
- The formal expert can also set up the formal regression runs, maintain them, and perform triage on issues when there are failures.
C. Control of formal engines
- You need to determine early on whether formal verification will be efficient in the design or not. Somme initial automatic formal checking of some pre-defined properties (e.g., dead code, FSM deadlock, etc) is an easy way to determine whether formal can control and observe the design.
- It is common for formal verification tools to have 10 or more formal engines for handling difficult design structures, finding counterexamples in complex situations, and/or addressing special formal properties (such as liveness). You should have a good understanding of the formal engines and the mechanism to control them.
D. Quality of the assertions
- The quality of the formal results will only be as good as the formal properties. Imprecise or incorrect properties will lead to false firings that will take time to debug.
- Formal verification can examine multiple properties simultaneously. Hence, users can capture numerous scenarios in different properties or capture a single scenario in multiple properties with varying flavors of expression.
- It is common for new users to find property languages (such as SVA or PSL) hard to use and/or difficult to make precise. To ease the learning curve, we encourage designers to use RTL modeling code to simplify problematic assertions into simple ones.
E. Proximity of the initial states
- Although toggling the reset signal is sufficient to initialize most design blocks, it is advantageous to have a good understanding of the design so that you can set up a meaningful initial state for formal runs.
F. Completeness of the constraints
- Constraints help to limit the design space for formal verification. They enable formal to create realistic counterexamples and to obtain proofs. You should use unconstrained stimulus at the beginning of the formal process. This will allow users to see firings from properties so that they can be ensured formal can explore those properties. Also, counterexamples can help users understand the properties better, making it easier to correct and refine the properties.
- To double-check the constraints, it is a good idea to include the constraints in the simulation environment. This will allow users to check whether the constraints are generally true or not.
Phases 2 and 3: Improved and Final
Bug hunting is a process based on continuous refinement. It is common for users to iterate between Phases 2 and 3 to explore the different scenarios of the bug(s).
A. Complexity of the design
- Besides turning unrelated modules into black boxes, other formal verification approaches that allow for fine-tuning by reducing complexity are cut points, counter, and memory remodeling. They give users more freedom to control the cut points directly.
B. Accessibility of formal experts: assigned in Phase 1.
C. Control of formal engines
- Different formal engines specialize in different classes of properties. As we are focusing on finding bugs, it is more efficient to deploy only the counterexample finding engines instead of the proof engines.
- Each formal engine has a different profile. By monitoring engine health, we can identify the most effective engines and their configurations. The tool can remember this information in the formal knowledge database for subsequent formal runs.
D. Quality of the assertions
- The assertions will be continuously updated. As we learn more about the design from the bug scenario(s) and/or the counterexamples from formal verification, we will refine the assertions. As formal verification can handle a lot of assertions concurrently, it is common to add assertions to cover different scenarios.
- Follow the two golden rules: (i) Keep properties as simple as possible. (ii) Keep properties as short as possible.
- Some inconclusive assertions may be inefficient for formal verification. We can reduce their complexity by reducing the depth, adding helper assertions, decomposition, and using an assume-guarantee approach.
E. Proximity of the initial states
- In a bug hunt (especially a silicon bug hunt) where the bug happens thousands of cycles into functional operation, formal verification does not recreate a long history of events. Traditional formal verification, which starts from time 0, is good for initial design verification, but it is inefficient for hunting complex functional bugs. The recommended methodology is to leverage functional simulation activity and start formal verification from interesting states in the simulation traces. Also, instead of using one initial state to start formal verification, multiple states from functional simulation can be used to launch multiple formal runs concurrently.
F. Completeness of the constraints:
- In general, it is dangerous to over-constrain the formal verification environment. When over-constrained, formal verification may not be able to find any counterexample. However, there are advantages to using constraints to improve the efficiency of the formal runs.
- Constraints can be used to set up a divide-and-conquer approach for formal verification. For instance, if a design can operate in different modes, we can set up multiple formal runs by constraining the mode of operation. Each of the formal runs will be more focused, and the results will be more straightforward to understand.
- There are situations where we can over constrain the formal environment. If we are looking for a bug under a unique circumstance, it is advantageous to over-constrain the environment to focus on that specific situation. At the same time, we may want to confirm the conditions under which a property is true. We can over-constrain the environment concerning these conditions so that the property can be proven.
Differences from traditional bug hunts
Using formal verification in a spiral refinement silicon bug hunting process differs from traditional model checking in several ways:
- Over-abstracting: Instead of verifying the whole design, we want to abstract or exclude the irrelevant modules so that formal verification can be as efficient as possible.
- Over-constraining: As we know which configuration, mode-of-operation, and interfaces caused the bug, we can constrain the design accordingly and disable the unused interfaces.
- Focused assertions: Based on the bug scenarios observed in the lab, we write properties to capture the bug scenarios and the pre-conditions that lead to the bug formulation.
- Deep initial state: Instead of starting formal verification from time 0, we can leverage simulation sequences to initialize the design amid functional operations or close to the bug formulation.
The full paper shows how to create the bug hunting radar charts, describes each of the steps of the hunt in great detail, and demonstrates its use via three case studies, including results. Follow this link to download Formal Verification Experiences: Spiral Refinement Methodology for Silicon Bug Hunt and master the most advanced formal verification techniques so you can successfully eliminate the most hard to track bugs in your cutting edge designs today.
About the authors
Ping Yeung, Ph.D. is the Principal Engineer in the IC Verification Systems division of Siemens EDA. He has more than 20 years of application, marketing, and product development experience in the EDA industry, including positions at 0-In, Synopsys, and Mentor Graphics. He holds 9 patents in the CDC and formal verification areas.
Mark Eslinger is a Product Engineer in the IC Verification Systems division of Siemens EDA, where he specializes in assertion-based methods and formal verification. Mark has more than 25 years of experience in design and verification, applications engineering, and technical marketing.
Jin Hou, Ph.D., is a product engineer for Questa Formal in the IC Verification Systems division of Siemens EDA. Jin has more than 12 years of experience in formal and assertion-based verification. She has worked as a CAE and PE, with experience in product definition, customer support, tool testing, customer training, and technical marketing, and is currently a PE for the Questa Formal Apps. Jin earned her Ph.D. at Université de Montréal, Montreal, Canada.