Verification Academy

Search form

My Account Menu

  • Register
  • Log In
  • Topics
  • Courses
  • Forums
  • Patterns Library
  • Cookbooks
  • Events
  • More
  • All Topics
    The Verification Academy offers users multiple entry points to find the information they need. One of these entry points is through Topic collections. These topics are industry standards that all design and verification engineers should recognize. While we continue to add new topics, users are encourage to further refine collection information to meet their specific interests.
    • Languages & Standards

      • Portable Test and Stimulus
      • Functional Safety
      • Design & Verification Languages
    • Methodologies

      • UVM - Universal Verification Methodology
      • UVM Framework
      • UVM Connect
      • FPGA Verification
      • Coverage
    • Techniques & Tools

      • Verification IP
      • Simulation-Based Techniques
      • Planning, Measurement, and Analysis
      • Formal-Based Techniques
      • Debug
      • Clock-Domain Crossing
      • Acceleration
  • All Courses
    The Verification Academy is organized into a collection of free online courses, focusing on various key aspects of advanced functional verification. Each course consists of multiple sessions—allowing the participant to pick and choose specific topics of interest, as well as revisit any specific topics for future reference. After completing a specific course, the participant should be armed with enough knowledge to then understand the necessary steps required for maturing their own organization’s skills and infrastructure on the specific topic of interest. The Verification Academy will provide you with a unique opportunity to develop an understanding of how to mature your organization’s processes so that you can then reap the benefits that advanced functional verification offers.
    • Universal Verification Methodology (UVM)

      • Advanced UVM
      • Basic UVM
      • Introduction to UVM
      • UVM Connect
      • UVM Debug
      • UVMF - One Bite at a Time
    • Featured Courses

      • Introduction to ISO 26262
      • Introduction to DO-254
      • Clock-Domain Crossing Verification
      • Portable Stimulus Basics
      • Power Aware CDC Verification
      • Power Aware Verification
      • SystemVerilog OOP for UVM Verification
    • Additional Courses

      • Assertion-Based Verification
      • An Introduction to Unit Testing with SVUnit
      • Evolving FPGA Verification Capabilities
      • Metrics in SoC Verification
      • SystemVerilog Testbench Acceleration
      • Testbench Co-Emulation: SystemC & TLM-2.0
      • Verification Planning and Management
      • VHDL-2008 Why It Matters
    • Formal-Based Techniques

      • Formal Assertion-Based Verification
      • Formal-Based Technology: Automatic Formal Solutions
      • Formal Coverage
      • Getting Started with Formal-Based Technology
      • Handling Inconclusive Assertions in Formal Verification
      • Sequential Logic Equivalence Checking
    • Analog/Mixed Signal

      • AMS Design Configuration Schemes
      • Improve AMS Verification Performance
      • Improve AMS Verification Quality
  • All Forum Topics
    The Verification Community is eager to answer your UVM, SystemVerilog and Coverage related questions. We encourage you to take an active role in the Forums by answering and commenting to any questions that you are able to.
    • UVM Forum

      • Active Questions
      • Solutions
      • Replies
      • No Replies
      • Search
      • UVM Forum
    • SystemVerilog Forum

      • Active Questions
      • Solutions
      • Replies
      • No Replies
      • Search
      • SystemVerilog Forum
    • Coverage Forum

      • Active Questions
      • Solutions
      • Replies
      • No Replies
      • Search
      • Coverage Forum
    • Additional Forums

      • Announcements
      • Downloads
      • OVM Forum
  • Patterns Library
    The Verification Academy Patterns Library contains a collection of solutions to many of today's verification problems. The patterns contained in the library span across the entire domain of verification (i.e., from specification to methodology to implementation—and across multiple verification engines such as formal, simulation, and emulation).
    • Implementation Patterns

      • Environment Patterns
      • Stimulus Patterns
      • Analysis Patterns
      • All Implementation Patterns
    • Specification Patterns

      • Occurrence Property Patterns
      • Order Property Patterns
      • All Specification Patterns
    • Pattern Resources

      • Start Here - Patterns Library Overview
      • Whitepaper - Taking Reuse to the Next Level
      • Verification Horizons - The Verification Academy Patterns Library
      • Contribute a Pattern to the Library
  • All Cookbooks
    Find all the methodology you need in this comprehensive and vast collection. The UVM and Coverage Cookbooks contain dozens of informative, executable articles covering all aspects of UVM and Coverage.
    • UVM Cookbook

      • UVM Basics
      • Testbench Architecture
      • DUT-Testbench Connections
      • Configuring a Test Environment
      • Analysis Components & Techniques
      • End Of Test Mechanisms
      • Sequences
      • The UVM Messaging System
      • Other Stimulus Techniques
      • Register Abstraction Layer
      • Testbench Acceleration through Co-Emulation
      • Debug of SV and UVM
      • UVM Connect - SV-SystemC interoperability
      • UVM Versions and Compatibility
      • UVM Cookbook
    • Coding Guidelines & Deployment

      • Code Examples
      • UVM Verification Component
      • Package/Organization
      • Questa/Compiling UVM
      • SystemVerilog Guidelines
      • SystemVerilog Performance Guidelines
      • UVM Guidelines
      • UVM Performance Guidelines
    • Coverage Cookbook

      • Introduction
      • What is Coverage?
      • Kinds of Coverage
      • Specification to Testplan
      • Testplan to Functional Coverage
      • Bus Protocol Coverage
      • Block Level Coverage
      • Datapath Coverage
      • SoC Coverage Example
      • Requirements Writing Guidelines
      • Coverage Cookbook
  • All Events
    No one argues that the challenges of verification are growing exponentially. What is needed to meet these challenges are tools, methodologies and processes that can help you transform your verification environment. These recorded seminars from Verification Academy trainers and users provide examples for adoption of new technologies and how to evolve your verification process.
    • Upcoming & Featured Events

      • Creating an Optimal Safety Architecture  - February 9th
      • The ABC of Formal Verification - February 11th
      • Events Calendar
    • On Demand Seminars

      • I'm Excited About Formal...
      • Visualizer Coverage
      • Formal-based ‘X’ Verification
      • 2020 Functional Verification Study
      • All On-Demand Seminars
    • Recording Archive

      • Improving Your SystemVerilog & UVM Skills
      • Should I Kill My Formal Run?
      • Visualizer Debug Environment
      • All Recordings
    • Mentor Training Center

      • SystemVerilog for Verification
      • SystemVerilog UVM
      • UVM Framework
      • Instructor-led Training
    • Mentor Learning Center

      • SystemVerilog Fundamentals
      • SystemVerilog UVM
      • Questa Simulation Coverage Acceleration Apps with inFact
      • View all Learning Paths
  • About Verification Academy
    The Verification Academy will provide you with a unique opportunity to develop an understanding of how to mature your organization's processes so that you can then reap the benefits that advanced functional verification offers.
    • Blog & News

      • Verification Horizons Blog
      • Academy News
      • Academy Newsletter
      • Technical Resources
    • Verification Horizons Publication

      • Verification Horizons - November 2020
      • Verification Horizons - July 2020
      • Verification Horizons - March 2020
      • Issue Archive
    • About Us

      • Verification Academy Overview
      • Subject Matter Experts
      • Contact Us
    • Training

      • Questa® & ModelSim®
      • Questa® inFact
      • Functional Verification Library
  • Home /
  • Verification Horizons /
  • July 2020 /
  • Formal Is The “New Normal” — Deploy These FV Apps In Your Next Project

Formal Is The “New Normal” — Deploy These FV Apps In Your Next Project

Verification Horizons - Tom Fitzpatrick, Editor

 | Verification Horizons - July 2020 by Ajeetha Kumari, Hemamalini Sundaram, and Darshan Ballari, VerifWorks, LLC and CVC Pvt., Ltd.

INTRODUCTION

Formal verification is now pervasive in many chip design verification projects. Key to this widespread adoption is the availability of automated “apps” that makes it easy to deploy Formal in hitherto simulation-only projects. We at VerifWorks have a long history of formal deployment at many design houses and have seen the challenges engineers face while adopting the same. We have also trained hundreds of engineers to use Formal with ABV (Assertion-Based Verification) through CVC. Having such widespread experience in deploying Formal, our team has seen Formal becoming the “new normal” with many teams adopting it in their projects.

Some of the key enablers in Formal adoption are:

  • Availability of assertions/properties
  • Identifying the right block/task for Formal in a simulation-dominant project

In this article, we will share our experiences in overcoming the above challenges using Questa® Formal and associated apps such as:

  • Questa® AutoCheck
  • Questa® Register Check
  • Questa® Connectivity Check

CATEGORIZING FORMAL DEPLOYMENTS

We classify Formal into two broad categories:

  • SDF – Specification Driven Formal
  • IDF – Implementation Driven Formal

SDF – Specification Driven Formal

SDF – starts with specification and extracts properties, then deploys a formal verification tool such as Questa® Formal. A good example is configuration and status registers (CSRs) that are omnipresent in modern day configurable designs. There are certain classes of properties that can be extracted from these specifications. These are ideal candidates for Formal as the process is automated and repeatable.

Connectivity verification is another good example of SDF. In complex subsystems and SoCs, several IPs are integrated. Given that the IPs are verified stand-alone, their connectivity is a key aspect at sub-system and SoC level verification. Also, pin muxing is a common technique used by architects to keep the pin count reasonable in the final die/assembly. Such requirements on connectivity are typically captured and verified using Questa® ConnectCheck.

Extracting properties manually from a specification is another critical step in Formal deployment. Once identified, users code these properties in SystemVerilog Assertions (SVA) syntax. Such properties can then be verified using Questa® PropCheck.

IDF – Implementation Driven Formal

Given the vast amount of reuse in modern day systems, deploying Formal in real life often involves an existing implementation along with its specification. Typically, some parts of the specification change from one chip to another (in a derivative product) and some of these changes can be quickly verified using Formal. Many a times, original designers are no longer the owners of new, derivative designs, prompting a thorough check for any potential misuse of legacy code. This is where an automated checking tool such as Questa® AutoCheck comes very handy.

SDF - QUESTA® REGISTER CHECK

As noted earlier, configuration registers are key elements in configurable IPs and SoCs. Some of the common checks needed for many of these registers are:

  • Out-of-reset-value checks
  • Address map related checks
  • Policy Checks such as W1C (Write-1-to-clear), etc.

Users often capture register definitions in one of the standard formats such as:

  • IP-XACT
  • SystemRDL

Though these are well-defined formats, teams often use custom formats based on

  • Microsoft® Excel®
  • CSV
  • XML
  • YAML
  • JSON, etc.

Given the regular structure of register specifications and the formats such as CSV/XML, ready-made apps are available to generate checkers/SVA automatically from these formats. For instance, Questa® Formal supports CSV, IP-XACT and XML as shown below in figure 1.

Figure 1 - Questa® AutoCheck


Often, we find that teams use slightly modified schema in XML and/or custom extensions to IP-XACT, etc. In such cases, we at VerifWorks provide custom adaptors for non-standard CSR specification formats such as YAML, XML, etc. We make them compatible with Questa® Register Check’s desired format to improve productivity.

qverify_memmap is an executable used to generate the policy checks from XML/CSV in Questa®. A typical run shows the following output summary:

Figure 2 - Output summary


This summary is very useful to quickly review for correct translation of user intent to generated checkers. If there are tweaks needed to get the address space correct, for example, users can modify the input XML and quickly regenerate the checkers using the qverify_memmap command.

Next step in Register Check is to run the generated checkers using Formal Engines. The Questa® Formal GUI provides an intuitive, easy-to-navigate view of the formal runs as shown above in figure 3.

Figure 3 - Questa® Formal GUI


As a quick summary, register verification can easily be pushed to formal verification with apps such as Register Check.

SDF - QUESTA® CONNECTIVITY CHECK

SoCs have several IPs connected and logic to handle pin muxing, etc. At the SoC level, one of the key challenges is to verify the connectivity of various IPs.

Verifying connectivity/paths

Consider a connection as shown below in figure 4:

Figure 4 - IP Connectivity


To verify the above paths, we need 3 key elements:

  • Stimulus (Src, Enable, Clk, Reset)
  • Checkers – a_path_chk_0 : assert property (en_0 == 0 |-> ##LAT dst_0 == $past(src_0, LAT));
  • Coverage – ensure all combinations are verified

Writing simulation tests to verify such structures is tedious and error-prone. Questa® Formal provides an efficient alternative for connectivity verification via the Connect Check app. Before we look at how we deploy Questa® Connectivity Check, let’s enumerate typical types of connections that we find in designs.

Types of connections/paths

We can classify different paths as below:

  • Simple, direct connections:


  • A set of signals multiplexed to a common bus:


  • Tie-offs – 0/1:


  • Several flip-flops may appear between the source signal point to the destination:


  • While several flip-flops may appear between the source signal point to the destination along with a multiplexor at the destination, each path may have a different latency.

Using Questa® Connectivity Check App

As with any Formal verification, assertions need to be fed as input to the formal engines. Questa® Connectivity Check is an app that generates the necessary assertions from a simple CSV format as input. Figure 5 below is a flow diagram from Questa® documentation to show the process.

Figure 5 - Questa® Connectivity Check


We used this on a cloud platform IP that performs compression of the data stored on the cloud. Figure 6 below is a sample CSV file that we used as input to Questa® FV.

Figure 6 - Sample CSV file


Once the connectivity CSV file is ready, we can run with Questa® Connectivity Check. A sample debug session is shown in figure 7 below.

Figure 7 - Questa® Connectivity Check sample debug session


Questa® FV provides a fully integrated GUI to show source code of the design, connections and the result of FV runs.

Simplifying connection specification

One of the challenges with CSV files is the readability of the code. Also for certain repeated connections, a CSV file tends to become too verbose and lengthy. Our consulting team at VerifWorks developed a Python app around Questa® Connectivity Check that takes a PATHS file as input and generates a Questa-friendly CSV file. A sample PATHS file is shown in figure 8 below:

Figure 8 - Sample PATHS file


With the PATHS file, the code is very readable, and users can add additional comments. It also supports iterative connectivity to capture recurring connections using a for loop like syntax. Connectivity verification becomes more productive when using a PATHS file and Questa® Connectivity Check.

Bridging Connectivity to the Simulation World

At times, users want to replay some of the connectivity checks in a typical simulation world using UVM. We have built a Python-based app to replay Formal connectivity with an auto-generated UVM test. We use our Go2UVM layer to simplify the stimulus creation and assist in auto-generated tests.

Figure 9 - Go2UVM layer


This flow comes in very handy when some of the connections are inconclusive in Formal engines even after long runs.

IDF - QUESTA® AUTOCHECK

As mentioned earlier, often teams find it necessary to deploy Formal on an existing RTL design. We deploy IDF – Implementation Driven Formal methodology in such cases.

Who will write the assertions?

Many engineers face this dilemma – what are some of the possible assertions/properties for my design? In our experience, this has been perhaps the single biggest reason why engineers hesitate to use Formal: its lack of properties /assertions.

Questa® AutoCheck addresses this problem nicely by automatically generating properties for common, known issues by analyzing your RTL code, as shown in figure 10 below.

Figure 10 - Questa® AutoCheck


Given the RTL design, Questa® AutoCheck analyzes and presents a set of extracted properties/observations in a table format as shown in figure 11 below. It also provides the design hierarchy, schematic and a table/list of checks.

Figure 11 - Questa® AutoCheck extracted properties/observations


Questa® classifies these properties into 40+ different categories and presents each to the user. While some of the checks are like classical lint-type checks, having a formal engine to extract such checks is powerful as it reduces the noise that is prevalent in a typical RTL lint tool.

Some of the common checks our teams found very useful in Questa® AutoCheck, along with its perceived value are discussed below. It is important to appreciate that this is a subset that our consulting team found most valuable in recent projects, this list can vary from design to design.

X_ASSIGN_REACHABLE

One of the common coding styles is to assign X (Unknown) even at RTL stage to catch any errors as early as possible. The intention is not to exercise that piece of logic under normal working conditions and if it indeed occurs, a pessimistic X propagation would help flag it in simulations.

An orthogonal design practice in low power designs is to let tools introduce/inject X’s when a block is in power-down mode. In a recent customer design that involved Low Power at the RTL stage, it was critical to differentiate X’s emerging due to power-down semantics from those due to explicit X assignments.

Questa® AutoCheck is designed to identify issues such as X propagation automatically and flags if an X-assignment is reachable, without having to run any simulation vectors. This can save many hours of debug in such scenarios.

SLIST_INCOMPLETE

Synthesis-Simulation mismatch is a well-researched topic. One of the sources for this issue is an incomplete sensitivity list in a typical always block in Verilog. Though well-known, new comers still make this mistake, especially when they don’t use the SystemVerilog enhanced always_comb block. Finding these issues during Synthesis and gate-level simulation is a painful and long process. Questa® AutoCheck enables users to find these much earlier in design cycle.

FSM_UNREACHABLE_TRANS

Many Lint tools perform detailed FSM analysis and flag potential issues. Sometimes tools tend to be very pessimistic and throw too many violations, making such reports too verbose. This leads to lot of time spent in analyzing such violation reports. However, a clear selection of most valuable checks from FSM reports based on design style can help prevent costly design errors. One such example in Questa® AutoCheck is FSM_UNREACHABLE_TRANS.

This is reported when a defined transition (as in RTL code below, in RED) can never occur due to the logic surrounding the FSM; in this specific example, assume that the logic around this FSM ensures that the value of i is always 1 when state == S2. Such cases will be harder to analyze by code reviews and an automated, formal mechanism to flag these is very useful.

Figure 12 - FSM example


Reusing AutoCheck in Simulation

Once these properties are generated for a given RTL, they are typically verified in Questa® Formal itself. This flow provides confidence for those properties that pass. However, for the failing ones, it requires user intervention to debug and analyze the failures. Some of these failing properties can be further propagated to simulation as part of the well-known assume-guarantee principle. For instance, if AutoCheck reported a possible out-of-bound access issue, to ensure that the bounds are within legal limits, it requires to be guaranteed by the preceding block driving this signal.

We at VerifWorks have developed a library of properties that can help in this process. Think of these as templates that users can leverage and plug these auto-generated properties into a simulation with Questa®, or any simulator.

SUMMARY

As the title of the article reads, Formal is the “new normal” and with real-life deployment case studies, we have shared our experience of how Questa® Formal apps help in adopting Formal verification. We highlighted common problems that can be easily solved by Formal tools along with apps. We have also highlighted some of the custom plug-ins that we have developed to bridge Formal and Simulation. With that, we hope that more and more teams adopt this “new normal” and become more productive!

Back to Top

Table of Contents

Verification Horizons Articles:

  • What do Grubhub®, Doordash®, and Verification Technology Have in Common?

  • Formal Is The “New Normal” - Deploy These FV Apps In Your Next Project

  • Understanding the SVA Engine Using the Fork-Join Model

  • Bridging the Portability Gap for UVM SPI VIP Core Reuse From IP to Sub-System and SoC Using Portable Stimulus

  • PCIe Simulation Speed-Up Using Mentor QVIP with PLDA PCIe Controller for DMA Application

  • Extending SoC Design Verification Methods for RISC-V Processor DV

  • Addressing VHDL Verification Challenges with OSVVM

  • Effective Validation Method of Safety Mechanism Compliant with ISO 26262

© Mentor, a Siemens Business, All rights reserved www.mentor.com

Footer Menu

  • Sitemap
  • Terms & Conditions
  • Verification Horizons Blog
  • LinkedIn Group
SiteLock