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:
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:
- 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