Functional Verification Sign-Off is the crux of the design verification problem faced by latest Silicon Designs on the Simulation/Stimulus Driven and the Formal Verification Platforms. Formal Verification Convergence is a custom specific criterion depending on the success, failure, exhaustiveness and reachability of the verification goals generated and validated by the Formal Tool. One of the key techniques in Formal Verification is the ability to mathematically prove the equivalence between two different versions of the same RTL Designs. Those RTL Design versions may differ in terms of Feature addition/removal or Bug Fixes or Low Power Capability or specific requirements. Synopsys VC Formal ^TM tool provides this formal verification technique using a built-in Formal Application known as ‘Sequential Equivalence (SEQ)’ App. This Case Study outlines various approaches in deploying Formal SEQ App and an approach towards Faster Convergence.

1. Introduction

Complex & Computationally Intensive SOC Designs drive the functional verification complexity much beyond the realm of conventional verification techniques. Further the functional verification complexity is compounded by the shorter time-to-market requirements & performance intensive applications of the latest Silicon Designs [1].

Semiconductor & EDA Industries in collaboration with Research Community pushing the functional verification capabilities to address the ever-increasing design complexity. Those functional verification capabilities are improved through advent of language Capabilities like OOPs, Software Inspired capabilities like factory pattern, verification standards like UVM & PSS. Noticeably these exciting interventions are mostly centered on the heavily leveraged & standardized simulation driven dynamic verification platform.

2. Formal Verification

Formal Verification has been around for few decades co-existing with simulation driven dynamic verification platform. Concurrent and Exponential growth of AI/ML driven EDA Tool mathematical proofing capabilities, Hardware Computing Resources & Silicon Design Complexities bringing forth the Formal Verification towards addressing the verification gap (Figure 1).

Advanced Silicon Solutions for Artificial Intelligence, Machine Learning, Real Time Data Processing & High-Performance Computing are driving the Silicon Design Complexity that can be effectively handled by Mathematical Proofing techniques than Simulation driven verification techniques [2], [3], [4], [5]. Hence, it’s time for Formal Verification to be understood, leveraged & deployed for Silicon Design Verification.

3. Formal Convergence is a Challenge

Formal Verification Convergence is defined by the ability to mathematically prove the absence of bugs in the Design Under Test (DUT) based on the Formal Constraints, Checks & Verification Setup [6]. Formal Convergence as a criterion is characterized by the success, failure & inconclusiveness of the formal properties in each Formal Application Mode. Similar to Simulation’s Verification SignOff Criteria, the Formal Convergence depends on multitude of factors like DUT Complexity, Formal Constraints Complexity, Formal Checks & much more (Figure 2).

Formal Convergence is the single most complex & demanding activity [5] in the Formal Verification Flow (Figure 3). In this paper, we will discuss the Formal Convergence of Sequential Equivalence Checking Mode of the Formal Verification Platforms using Synopsys VC Formal ^TM Tool.

4. Sequential Equivalence Checking Mode (SEQ/SEC)

In SEQ Mode, the Formal Engine checks the functional behavior at all the output ports across two releases or versions of the same Design Under Test (DUT). Formal Engine utilizes both the state-matching and non-state matching algorithms to prove those DUT releases/versions are functionally equivalent [7]. In addition to output port checks, the SEQ mode also performs internal sequential difference checks to ensure the DUT similarity within Design States.

Synopsys VC Formal ^TM tool auto generates these output port checks for the given DUT (referred as SEQ_TOP). This SEQ mode reduces the verification turn-around time (TAT) and improves productivity by providing an approach to exhaustively verify the modified/implemented Design feature. This avoids the need to redo the verification of the entire design. Towards Formally verify the Clock Gating logic in our complex SOC design, we have developed Formal SEQ Verification Setup using Synopsys VC Formal ^TM tool. The two versions of the DUT are referred to as SPEC and IMPL in the SEQ mode nomenclature. Here specification-SPEC refers to the complex SOC design blocks without Clock Gating feature disabled and implementation-IMPL refers to complex SOC design blocks with Clock Gating feature enabled (Figure 4). 

5. SEQ Conventional Flow

In the conventional Flow of SEQ Mode, the Formal Engine checks the functional behavior at all the output ports of the top-level block across two versions of the same DUT (e.g., RTL Model A & RTL Model B as shown in Figure 5. Formal Engine proves or disproves the functional equivalence of the output ports of the top-level block in the SPEC & IMPL DUTs adhering to the defined Formal Input Constraints.

Though Formal Engine highlights internal sequential mismatches among with sub-blocks in the given DUT, there is NO output port level checks on the internal sub-blocks. Therefore, the Design Complexity of the entire DUT along with Formal Input Constraints plays a key role in the Formal Convergence.

6. SEQ Hierarchical Flow

Towards verifying the sub-block in each Top-Level Block without the need to develop Formal verification Setup, Synopsys VC Formal ^TM tool provides an approach known as ‘SEQ Hierarchical Verification Flow’. In this approach, we will be verifying the sub-block of a given Top-Level Block with complete reuse of the Formal Verification Setup & Input Constraints in the SEQ Mode as shown in the Figure 6. For the merit of this paper, we are utilizing the configuration#1 of the SEQ Hierarchical verification Flow defined in the Synopsys SolvNet Plus ^TM documentation [8]. Please refer to the SolvNet Plus ^TM documentation [9] for more details on the same.

7. Value Addition by SEQ Hierarchical Flow

It is imperative to understand the value of sub-block or unit, or IP level verification compared to the Top/System/SOC level verification in the Simulation Stimuli driven verification platform for obvious reasons. Similarly, there exists great potential & ROI in verifying the Sub-blocks in Formal Verification provided the reusability of Top-Level Verification Setup & Constraints. Further the SEQ Hierarchical Verification Flow provides the much-needed boost to achieve Formal Verification Convergence at a much-desired rate. Figure 7 highlights the key value addition of Sub-block Verification in the SEQ Mode.

8. Case Study

In this paper, we will be discussing the Formal SEQ Verification of Two Subsystem Level Top Blocks ‘A’ & ‘B’. These Blocks are few among the many subsystems with different functional capabilities & design complexities in the complex SOC (Figure 8).  

Refer below Table 1 for a high-level relative comparison of Blocks ‘A’ & ‘B’.

Table 1 : Relative Comparison of Case Study Blocks ‘A’ & ‘B’

8.1. Block ‘A’ – SEQ Conventional Setup

As Shown in the Figure 9, the Formal Engine drives the input ports of both the SPEC & IMPL (Top level block ‘A’) based on the Formal Input Constraints and generates the auto checks to compare the output ports of the SPEC & IMPL (Top level block ‘A’). Here the Formal Convergence of the auto checks on the output ports is impacted by the Design Complexity of the entire DUT – Top Level Block ‘A’ and its Sub-blocks. Owing to the Complex nature of the SOC Design & large Cone of Influence (COI), we have achieved <80% Formal Convergence in our Case Study for Clock Gating Verification of Top-Level Block ‘A’.

Despite various efforts to improve Formal Convergence by Formal Techniques (like Black Boxing, Abstractions, Design reductions, Enhances Engine & Effort level and much more), our verification returns were stagnated with the unrelenting Formal Convergence at level of < 80% for this Top-Level Block ‘A’. Hence, we have decided to deploy SEQ Hierarchical Flow to achieve the Formal Convergence of this Top-Level Block ‘A’.

8.2. Block ‘A’ – SEQ Hierarchical Setups

In the SEQ Hierarchical Verification Flow (Figure 10, Figure 11 & Figure 12) of Block ‘A’, the Formal Engine drives the input ports of both the SPEC & IMPL (Top level block ‘A’) based on the Formal Input Constraints identical to the SEQ Conventional Verification Flow.

But the Formal Engine generates auto checks to compare the output ports of the targeted Sub-block within the SPEC & IMPL blocks (Top level block ‘A’).  Multiple types of SEQ Hierarchical Verification Flow Testbenches were developed specific to each Sub-block which were chosen on selection criteria (refer next section).

For this case study, we have selected three sub-blocks (S1, S2 & S3) from Top Level Block ‘A’ for SEQ Hierarchical Verification Flow setups as show in the Figure 10, Figure 11 & Figure 12. Here the Formal Convergence of these newly generated auto checks on the sub-block output ports can be achieved much faster due to the limited nature of the Design Complexity & Cone Of Influence (COI) on these output checks.

8.3. Block ‘A’ – SEQ Conventional Setup with verified Sub-blocks Clock Gating Disabled

After successful verification closure of Sub-blocks S1, S2 & S3 using the SEQ Hierarchical Verification Flow of Top-Level Block ‘A’, we have created another version of the SEQ Conventional Flow setup the Top-Level Block ‘A’ with Clock Gating Disabled only those three verified sub-blocks (refer Figure 13). Thereby leveraging the Formal Verification Closure of those three sub-blocks within the Top-Level Block ‘A’ as well as reducing the Design Complexity & COI Effects on the Top-Level Output Port Checks of the Block ‘A’.

Now we have achieved a better & faster Formal Convergence of >09% on the Top-Level Block ‘A’ with the same Formal Verification Setup & Constraints except for Clock Gating disabled sub-blocks within the DUT.  This clearly proves the effectiveness of the SEQ Hierarchical Verification Flow on the selective Sub-Blocks (S1, S2 & S3) of the Top-Level Block ‘A’ to achieve faster Formal Convergence.

8.4. Sub-block Selection Criteria

Even though the Sub-block SEQ verification setup can be developed quickly with reusable components from Top Level SEQ verification setup, it is ineffective to perform Sub-block verification on all the first level sub-blocks within a Top-Level Block. Henceforth we have devised a selection criterion to choose a sub-block for SEQ Hierarchical Verification Flow. Please note this selection criteria may be effective specifically for this case study.

Factors involved in the selection criterion of a sub-block are: (not limited to)

1. Number of Inconclusive Top Level Block Checks impacted by the COI of this sub-block
2. Placement of this sub-block within the Logic Levels of the Top-Level Block
3. Proximity of this Sub-block to the Input/Output Ports of the Top-Level Block
4. Fan-in & Fan-out nature of this sub-block
5. Design Complexity of this sub-block

8.5. Block ‘B’ – SEQ Verification Setups

Considering that the verification setups of Top-Level Block ‘B’ is like the Top-Level Block ‘A’ as discussed in the previous sections, we are omitting the details on Top Level Block ‘B’ SEQ Verification Setup in this paper.

8.6. SEQ Verification Metrics Table

Based on this case study execution of Formal SEQ Verification on Top Level Blocks ‘A’ & ‘B’, we have captured the key metrics from the Synopsys VC Formal ^TM Tool execution. These metrics were gathered from various Formal runs with unchanged Formal Verification setup (except SEQ Flow change), Input Constraints, Design Versions of IMPL/SPEC, Tool Settings like Engine Selection, Number of Workers and so.

Table 2: SEQ Metrics of Block ‘A’

Table 3: SEQ Metrics of Block ‘B’

9. SEQ Verification Formal Convergence Rate

We have analyzed the Rate of Convergence for all the SEQ Verification Flow Setups discussed in this case study on Top Level Blocks ‘A’ & ‘B’.  

9.1. Block ‘A’ SEQ Verification Formal Convergence Rate

In this case study, we were able to achieve Formal Convergence at a faster rate for Top Level Block ‘A’ with clock gating disabled on verified sub-blocks (S1, S2 & S3) in comparison to the SEQ Conventional Verification Flow of Top-Level Block ‘A’ (refer Figure 14)

9.2. Block ‘B’ SEQ Verification Formal Convergence Rate

In this case study, we were able to achieve Formal Convergence at a faster rate for Top Level Block ‘B’ with clock gating disabled on verified sub-blocks (S1 & S2) in comparison to the SEQ Conventional Verification Flow of Top-Level Block ‘B’ (refer Figure 15)

10. Conclusions

This case study explored the Formal SEQ Verification setups with conventional and hierarchical flows on the Top-Level Blocks ‘A’ & ‘B’. Further we have devised an added ability to disable clock gating for verified sub-blocks using SEQ Hierarchical flow in the Top-Level Block SEQ Conventional Flow.

Table 4 : Relative Comparison of SEQ Flows’

In Table 4, we have highlighted the key comparative features of the SEQ Conventional and Hierarchical Flows.

Consequently, we were able to achieve faster convergence between the Top-Level blocks in the Formal SEQ Conventional Flow. Figure 16, Figure 17 & Figure 18 illustrates the recommendations on SEQ Hierarchical Flow from this Case Study.

Hence, we recommend the Formal SEQ Hierarchical flow on the Designs that need convergence improvements beyond the known formal convergence techniques.

Conflict of Interest

The authors declare no conflict of interest.

Acknowledgment

The authors acknowledge the support and guidance from the Synopsys VC Formal ^TM applications team and Samsung Austin Research Center (SARC) Design and verification teams.

1. Thalaimalai Vanaraj, M. Raj and L. Gopalakrishnan, “Functional Verification closure using Optimal Test scenarios for Digital designs,” 2020 Third International Conference on Smart Systems and Inventive Technology (ICSSIT), Tirunelveli, India, 2020, 535-538, doi: 10.1109/ICSSIT48917.2020.9214097.
2. https://www.researchgate.net/figure/Design-and-Verification Gaps-Design-productivity-growth-continues-to-remain-lower-than_fig3_237116903  
3. https://semiwiki.com/semiconductor-services/semico- research/293218-the-impact-of-ai-enabled-eda-tools-on-the-semiconductor-industry/
4. https://wiki.aiimpacts.org/doku.php?id=ai_timelines:hardware_and_ai_timelines:computing_capacity_of_all_gpus_and_tpus
5. https://aiimpacts.org/global-computing-capacity/
6. https://www.edn.com/ic-design-a-short-primer-on-the-formal-methods-based-verification/
7. https://dvcon-proceedings.org/wp-content/uploads/challenges-of-formal-verification-on-deep-learning-hardware-accelerator-paper.pdf
8. Synopsys VC Formal User Guide – https://www.synopsys.com/verification/static-and-formal-verification/vc-formal.html
9. Synopsys Documentations on SEQ Hierarchical Flow – SolvNet Plus site – https://www.synopsys.com/support/licensing-installation-computeplatforms/synopsys-documentation.html

Citations by Dimensions

Citations by PlumX

Crossref Citations

This paper is currently not cited.

No. of Downloads per Month

No. of Downloads per Country