Continue to Site

# Optimizing Formal Verification through Complexity Management

In the realm of formal verification, complexity is a critical factor that influences the efficiency and success of verification processes. This blog delves into advanced techniques to manage and reduce complexity, ensuring a more streamlined and effective formal verification process.

Formal Complexity Defined

Formal complexity is essentially how challenging it is for a verification tool to obtain a conclusive result. It is influenced by several factors, including the size and diameter of the design. Unlike common assumptions, size is not measured by the number of gates but by the number of primary inputs and state bits, excluding those with constant values. The symptoms of high complexity include long run times, high memory consumption, and undetermined results.

Size Contribution Factors

The size of a design, in the context of formal verification, is better understood as the number of primary inputs and state bits that vary. Constraints and auxiliary code can also add state bits, thereby increasing complexity. The size relevant for formal analysis is the Cone of Influence (COI) size, which is typically a fraction of the entire design size but crucial for evaluating individual assertions.

Diameter and Its Impact

Diameter refers to the number of steps required to reach all reachable states from the initial state. While it can vary significantly, large diameters do not always correlate with slow performance, and small diameters can sometimes result in slower runs due to secondary complexity factors. The diameter must be assessed in conjunction with the COI size to understand its true impact on complexity.

The Role of Properties and Assertions

Properties in formal verification can significantly increase complexity by adding to both size and diameter. Assertions and constraints need careful consideration as they can either mitigate or exacerbate complexity. For instance, temporal functions and certain operators can infer additional state bits, thereby complicating the verification process.

Basic Techniques for Complexity Reduction

Several strategies can be employed to manage and reduce complexity in formal verification:

1. Environment Simplification: Simplifying the environment using constraints can effectively reduce complexity. Fixed value constraints, in particular, can reduce the size and diameter by making state bits constant.

Figure 1. complexity reduction method: environment simplification​

2. Abstraction: Formal analysis tools often use abstractions to optimize performance. Abstractions focus on analyzing a portion of the design rather than the entire design, thereby improving the efficiency of proven results.
3. Local Assertions: Assertions that are local, such as protocol properties, typically do not require the entire COI to pass. These assertions can take advantage of locality to simplify the verification process.
4. Property Simplification: Splitting complex assertions into smaller, more manageable pieces can reduce complexity. This divide-and-conquer approach ensures that each smaller COI is less complex, making verification more efficient.

Figure 2. complexity reduction method: property simplification​

1. Black Boxing:
By treating certain parts of the design, such as memories, as black boxes, the outputs become primary inputs that the tool can drive. This technique reduces the overall complexity by excluding the state-holding elements from the analysis.
2. Parameterization: Setting design parameters to the smallest meaningful values can significantly reduce complexity. This approach is particularly effective for detecting failures during initial verification stages.
3. Partitioning: Introducing additional hierarchy levels or re-partitioning existing blocks can focus formal analysis on specific areas. This technique should be used sparingly due to its labor-intensive nature but can be highly effective in certain scenarios.

Figure 3. complexity reduction method: partitioning​

Managing Performance Variability

The performance of formal analysis can vary widely due to first and second-order complexity factors. Small changes in design or properties can significantly impact performance. Therefore, while size and diameter can provide an initial assessment, the actual performance will often depend on the intricate details of design structure and state transitions.

Conclusion

Understanding and managing complexity in formal verification is crucial for achieving efficient and conclusive results. By employing advanced techniques such as environment simplification, abstraction, local assertions, property simplification, and black boxing, verification engineers can tackle the inherent challenges of formal analysis. Through careful consideration of these factors, the formal verification process can be optimized, leading to better performance and more reliable outcomes.
With a wealth of experience in formal verification projects, I specialize in two critical solutions: formal signoff with full proof and formal signoff with coverage. Throughout my career, I have successfully tackled a diverse range of designs, including Instruction units, Standard interfaces, User-defined interfaces, Bus matrices, Caches, MMUs, Schedulers, DMA controllers, Memory controllers, Interrupt controllers, Power management units, and various specific functional modules.

Drawing on this extensive project experience and a deep understanding of various design types, I have developed a unique formal verification methodology. This methodology has been honed through practical application and has proven highly effective in ensuring design correctness and efficiency.

One of my key achievements has been the independent creation of a comprehensive formal verification IP library. This library comprises nearly 200 units, encompassing basic, common, VIP, and flow libraries. These resources, combined with my methodology, have been successfully deployed in the product development workflows of numerous leading chip companies. The results speak for themselves, with significant improvements in verification effectiveness and performance observed across the board.

My goal is to share this expertise with students at EDA Academy, providing them with practical insights and industry best practices that they can apply directly to their own projects. By imparting this knowledge, I aim to empower learners to achieve their verification goals with confidence and efficiency.

Explore our current Formal Verification courses:

There are no comments to display.

Author
Peng Yu