Synopsys Formal Verification SIG 2023

The frontiers of formal verification technology are rapidly expanding beyond digital design verification, thereby opening new, diverse, and impactful opportunities for formal verification practitioners. This keynote presentation will explore the short- and long-term vision for what is to come, and the corresponding deep technical challenges. We delve into areas such as mixed-signal systems, embedded control software, security, and trusted AI/ML, and examine the corresponding fundamental shifts induced by real numbers, dense time, and complex arithmetic functions. By examining the current advancements and discussing futuristic domains, we hope to shed light on the transformative potential of formal verification in ensuring the reliability and correctness of systems across various industrial domains.

In this presentation, we discuss our experience using VC Formal DPV to verify and achieve proof convergence for complex datapath blocks.

The setup in formal tools such as Synopsys VC Formal is quick and easy. For complex designs, to achieve proof convergence, we used a combination of standard techniques, such as case split and assume-guarantee reasoning, as well as careful selection of a reference model. We also used RTL-to-RTL equivalence checking whenever possible.

Our experience shows that formal verification can deliver high design quality and improve verification efficiency compared to simulation.

It is a common practice in the verification methodology to leverage formal unreachability analysis (UNR) to remove unreachable coverage goals during simulation so as to reach coverage closure faster. In modern designs, the formal model created by UNR can have tens or even hundreds of millions of cover properties. Typical formal complexity management techniques such as black-boxing or abstraction are less desirable because coverage closure requires comprehensive review of all RTL.

Manual partitioning of the design to create separate formal models is an unscalable and iterative process that requires deep analysis to configure each run with potentially zero re-use. Further, as the number of partitions increase, the knowledge of passed parameters and constants along with the fundamental benefit of exclusion propagation is lost in the process.

In this presentation, we will describe both the benefits achieved and the lessons learned using Synopsys VC Formal FCA's new Auto-Scale SoC feature which automatically partitions the designs and performs parallel unreachability analysis with optimized and reduced formal models. We will demonstrate the convergence improvement on real design examples.

Formal verification can handle tasks that are extremely difficult in simulation, such as checking forward progress to ensure that a system eventually reaches a desired state or completes its intended behavior. Forward progress verification guarantees that a system continuously makes progress and avoids getting stuck in an undesirable or deadlock state.

This presentation focuses on the different techniques and methodologies employed to analyze and prove forward progress. We begin by introducing the concept of forward progress and its significance in the context of formal verification.  We discuss the potential risks associated with the absence of forward progress, such as system hang-ups or failures to complete critical tasks.

Next, we delve into the challenges faced in verifying forward progress properties and highlight the limitations of traditional verification methods. We will discuss various approaches for ensuring forward progress in the design, using both Liveness and Safety assertions and examine how and where each assertion type should be used. We show case studies that demonstrate the application of forward progress checks and the types of critical issues found in the designs. 

Finally, we will discuss the future directions and open challenges in forward progress verification, such as handling complex and dynamic system behaviors, scalability in large designs, and the integration of forward progress checks with other formal verification techniques.

Signoff is an important step in formal verification methodology to measure the quality and completeness of the formal testbench. Analysis of the set of SystemVerilog Assertions (SVA) used for verification can reveal parts of the design that are never included due to constraints, missing properties, or poor-quality properties.

Synopsys VC Formal delivers a unique approach to formal verification signoff where the quality of the formal testbench is mapped to standard coverage metrics such as line, branch, condition, toggle, and FSM state/transition. The unified coverage dashboard clearly highlights parts of the design where properties are missing or not providing enough verification value. A unique combination of over-constraint analysis, Cone of Influence (COI) structural analysis, formal core (logic explored during formal analysis) functional analysis, and fault injection and detection analysis, are the four pillars of the VC Formal signoff flow.

We will give an overview of the next generation Formal Verification Signoff flow enabled by Synopsys VC Formal and give a demonstration highlighting the easy-of-use of the unified coverage dashboard.

Power switch-off of design blocks/IPs which are not active is an effective technique to reduce power consumption in modern SoCs. Hardware state retention can be achieved using retention flops where the retention cell information is specified in the UPF (Unified Power format). Hardware state retention of every register in a design however has a cost. Thus selective, or partial, state retention is an efficient mechanism to bring down the area cost of retention. 

A major challenge with a partial retention scheme is to verify that it can be done safely and correctly without any loss of design state when power is gated. Missing retention information will result in loss of hardware state and will lead to functional failure. On the other hand, the retention list might contain some flops which are not required to be retained, and this will increase area.

Identifying and removing unwanted retention flops from UPF would help to save area. Conventional simulation-based verification techniques to verify retention sufficiency is infeasible as complete functional test suite of design block needs to be run in power aware simulation mode and this will need exhaustive effort in terms of test bench support and debug.

In this presentation, we will discuss alternative design verification methodology to check retention sufficiency using formal based sequential equivalence techniques.

Verification of datapath circuits is a challenging task due to the complex logic involved and to the amount of corner cases to consider. Complete signoff is required and, given that exhaustive simulation is impossible in practical cases, formal verification is the only real option. Equivalence checking against a golden or existing reference design is usually used to satisfy correctness concerns. Synopsys VC Formal DPV is a powerful formal equivalence checking tool for this kind of task and, when used by an expert engineer, very hard proofs can be completed.

We propose a rewriting framework deploying bitwidth dependent rewrites based on the e-graph data structure, providing a powerful assistant to Synopsys VC Formal DPV. The correctness of the rewriting steps is proven using Synopsys VC Formal DPV itself. With this assistant, we can produce a conclusive answer for cases initially inconclusive or reduce the overall runtime of already converging cases. When this is not possible, the assistant produces a simplified equivalence checking problem, requiring less human intervention to converge than the initial one.

This presentation aims to discuss the benefits of automation in streamlining the formal verification process and increasing its visibility to management. Focusing on two key stages, data collection and indicator generation, the presentation will demonstrate how accurate formal coverage data and meaningful indicators can facilitate informed decision-making and timely project signoffs.

Emphasis will be placed on practical implementation, particularly on collecting formal coverage data and producing indicators tailored to project management needs. Attendees will gain a clear understanding of the advantages of automating indicators for formal signoff and the knowledge to implement these techniques within their organizations.

The formal verification team at Samsung Austin R&D Center has a very successful SEQ methodology for finding clock-gating bugs long before they would be found in simulation or emulation.  In this presentation, we describe the importance of formally verifying clock-gating logic, the methodology we use to ensure the correctness of our Synopsys VC Formal SEQ testbenches, and the automation we use for reporting our results to the RTL design team and project management.  We also offer some advice on how to explain formal results to engineers who might not be familiar with these techniques.

In this session, Synopsys will share a number of innovative capabilities recently developed and soon to be coming in VC Formal. These will cover impressive performance improvements, powerful convergence guidance techniques, insightful signoff features and new applications.