Getting started with formal verification

Need for Higher level of Validation

As design complexity is increasing, the goal of 100% functional coverage becomes harder to achieve even after using constrained random stimulus and directed scenarios, therefore there is a need to adopt new methods of validation.

The verification engineering team tries to break down the RTL design into pieces and analyse them – independently and then in sync. This takes time! Design verification takes almost 80% of the overall time spent on chip development and verification engineers lose hair, sleep, peace, patience and weekends on tight deadlines to deliver the quality of verification.

Each miss from the verification team can cost a potential revenue loss of millions. The bugs can result in rolling back all the produced silicon from the market. One example was when Samsung rolled back its Galaxy Note 7. Turns out the device was failing due to battery short circuit, which was missed during the verification of the design. RTL designing and verification is a tricky task because we can’t give an update or version upgrade like what happens in the software industry and we can’t translate our design to silicon for each update in design. Hence, we need to verify and thoroughly analyse the design before actually sending the design to foundry. As we can rightly guess, this is a very expensive process both in terms of time and money.

The figure above shows how the delay in the making of a chip affects the cost. This shows that as many bugs as possible needs to be removed in the early stages and new design errors should not be introduced while refining the design.

Introduction to Formal Verification

Formal verification uses mathematical models/methods to prove or disprove the correctness of the system’s design with respect to formal specifications expressed as properties to verify the design thoroughly. It covers all the possible values a design variable can take and hence generating all the possible scenarios and stimulus for the design. We can theoretically achieve 100% coverage, which is a huge boost to the confidence of the design.

Formal verification is a technique used in different stages in ASIC project life cycle like front end verification, Logic Synthesis, Post Routing Checks and also for ECOs. But when we delve deeper, the formal verification used for verifying RTLs is entirely different from others.

Formal Verification Techniques:

The following figure illustrates the various formal verification techniques:

What is Formal Property Verification (FPV)?

What is formal property verification? A natural language such as English allows us to interpret the term formal property verification in two ways, namely:

• Verification of formal properties, or
• Formal methods for property verification(widely used interpretation by formal engineers)

FPV is the simplest form of formal verification; it is a method to prove the correctness of a design or show root cause of an error by rigorous mathematical procedures. This does not mean that the user must be a mathematician. It does not require test benches or stimuli and turnaround time is very less.

How FPV is Done?

In practice, there are two ways in which property verification is done today. These are static Assertion-based Verification (ABV) and dynamic Assertion-based Verification (ABV). In both forms, formal properties specify the correct requirements of the design, and the goal is to check whether a given implementation satisfies the properties. Static ABV techniques formally verify whether all possible behaviors of the design satisfy the given properties. Dynamic ABV is a simulation-based approach, where the properties are checked over a simulation run – the verification is thereby confined to only those behaviors that are encountered during the simulation.

Property checking can be done by using either using property languages (for example, ITL Interval Language) or Assertion languages (SVA, PSL, etc.). SVA is the assertions subset of the System Verilog language. Assertions or properties are primarily used to validate the behavior of a design and can be checked statically by property checker tool and proves whether or not a design meets its specifications. A holding SVA/ITL/PSL means that the assertion/property has been formally and exhaustively checked and it holds in all possible traces of the design. A failing SVA/ITL/PSL means that a counterexample was found that represents a violation of the intended design behavior.

Formal verification tool automatically uses its magic to generate the stimulus and implicitly covers all the cases. The only requirement of Formal tool is to give it the RTL design and a formal description of the specifications in form of PROPERTIES for covering all the input and output combinations exhaustively. Basically Formal Verification works on the principle of “failing to fail” to prove the design’s correctness. It generates all the possible stimulus and tries to fail our check. When it fails to fail – it states our design is correct else it stop immediately once a failure is found.

Let’s understand this through an example: We need to verify a DUT. We have two options:

• We can generate possible input and output combinations on our own and write very specific test patterns to validate that the input we provided generates the expected output. This is known as Directed Testing of the design of Directed Verification. We use SV, UVM test-benches to write specific testcases to check the DUT.
• The other option is – a tool generates all the possible inputs possible for our design and we only describe the behavior or relationship of input with the output. This description of behavior is done using SVA(system Verilog Assertions).

What type of designs can be easily verified using FPV?

Key Differences between Simulation and Formal:

What are Formal Engines?

Just like the engines of a car or any other vehicle. Formal engine is the actual heart and soul of the Formal Tool. It is the driving force. It determines how exhaustively the tool is verifying. It contains the algorithm which mathematically proves the correctness of our design.

What are the EDA tools and supported apps available?

There are many tools in the industry which uses formal methodology to achieve a particular purpose.

• Synopsys:Synopsys provides VC Formal tool which covers a wide range of formal applications such as assertion-based verification, connectivity verification, sequential verification, etc. There is VC LP which is mainly used to verify formally the low poour design intent.
• Siemens/Mentor Graphics: Siemens/Mentor Graphics Questa tool also provides formal verification specific applications such as Questa Connectivity check, Questa post silicon debug, Questa property check, Questa Register check, etc.
• JasperGold from Cadence: Cadence JasperGold tool supports many ‘Apps’ through which certain formal verification tasks can be performed very easily. Along with that, for standard interfaces, assertions/properties can be generated automatically or readily available as Assertion Based Verification IPs (ABVIP).
  • Formal Property Verification (FPV)
  • Unreachability Analysis (UNR)
  • Pin connectivity verification (CONN)
  • Configuration register verification (CSR)
  • AMBA Interface protocol compliance verification using ABVIPs (FPV)
  • Formal Coverage (COV)
  • Formal Superlint/ Auto Formal Lint (AFL)
  • Sequential RTL equivalence (SEC)
  • Security Path Verification (SPV)
  • Functional Safety Verification (FSV)

FPV Flow, Environment and Setup

Formal verification tools try to prove design correctness by analysing the space of possible behaviors of a design with static analysis algorithms, without simulating the design behavior over time. Therefore, formal techniques do not need a traditional testbench with dynamic tests/stimuli. Before starting formal verification, we must specify design intent, usually in the form of properties or assertions. This gives the tool a formal basis to reason about the design, and to identify violations that signify problems or bugs.

Formal tool doesn’t require a big SV/UVM based testbench. The tool creates a mathematical model for both the design and the specified assertions and try to prove one model against the other. In the process, it automatically checks whether the defined assertion is valid for all the legal possible stimuli defined by the set of user constraints.

Formal tool requires the clocks and resets to be specified before the actual formal analysis/verification begins. Formal tool can infer clocks based on how they are used in the design. But specifying clocks explicitly would help the tool analyse the sequential behavior of the design accurately. Also specifying the reset would help the tool apply reset for a few cycles and reset the design to a known state. And the other way of getting to a known state is to load waveforms from the simulation. This would help in reducing the non-deterministic values on non-resettable flops for formal analysis. More the non-deterministic values, the formal analysis would be more pessimistic. It would be good to reduce the state space by initializing the design using waveforms.

Sometimes we may need control over the state space. Legalize our state space by specifying constraints. Constraints direct the formal tool to choose values that follow the constraints. If we don’t specify the constraints, tool tries to mathematically prove the assertion for all the possible stimuli which may not be the desired behavior.

Formal verification tools ensure faster run times for comparatively small designs. However, adding assertions can take some time before doing actual verification. Also, time taken for establishing a given proof (assertions) can increase exponentially with the size of the design under consideration. We can direct the tool on what engine it should use and how much time it needs to spend on proving assertions, etc.

FPV Flow and Setup

Sample TCL File

Advantages of  FPV over Simulation approach

• Verification is mostly fully automatic except for initial set-up, property coding
• Verification can be started as soon as RTL is ready. It need not wait for the readiness of complete RTL. It can start the analysis even with basic functionalities:
  • Reset Analysis
  • Sanity checks, etc.
• As testbench is not required, stimulus generation will be automatically managed by the FA tool with or without constraints around it
• The prove will be extremely fast compared to dynamic simulations.
• Simulations usually takes more time to detect the corner cases, FSM deadlock conditions. Sometimes it need additional metrics (coverage data) to identify the corners. But FA tool can easily find and reach those cases in quick time (fraction of minutes)
• Both black box and white box approach can be used
• There is no specific testbench required to drive stimulus to the DUT. Thus, formal can be applied to the designs in very early phases of the project.
• Gives a higher level of confidence than simulation alone. Formal should be considered as complementary to simulation rather than replacing simulations entirely.
• Can replace millions of simulation cycles.
• Allows a more concrete mapping of specifications/design-intent to the actual design.

Limitations of Formal Verification:

Even though formal verification has many advantages it does have certain disadvantages:

• As the design size grows, the state-space increases exponentially. So, when compared to a design with 2048 flops, a design with 2049 flops will have an exponential increase in the state space. Hence as the design size increases, quickly we reach an upper limit where the machine cannot handle the size of the design or the time taken to explore the state space starts to reach a point of diminishing returns. This is called the problem of state-space explosion.
• FA is not suitable for data paths functions except for simple functions. This is true especially for algorithmic blocks
• FA is good for verifying a system but not for validating the system (As Validation usually can be done only dynamically and formal verification is a static process).
• FA can only handle RTL logic. Any analog block will get black boxed or can be removed from the DUT during FA

Conclusion:

References

Cadence Learning and Support 

support.cadence.com 

• JasperGoldProduct Page 
• User’s Manuals 
• Command Reference Manual

JasperGold FPV App User Guide 2021.09

 https://support.cadence.com/apex/techpubDocVieourPage?%26xmlName%3D=jasper_apps_userguide.xml&path=jasper_apps_userguide%2Fjasper_apps_userguide2022.03%2FJGA_overview.html

• Rapid Adoption Kits (RAKs)

Cadence JasperGold DPV Rapid Adoption Kit (Presentation) 

https://support.cadence.com/apex/ArticleAttachmentPortal?id=a1O0V000009ESwWUAW&pageName=ArticleContent&oMenu=People%20who%20viewed%20this%20also%20viewed

• Video Reference: JUG 2020 Webinar Video Series 

Link: https://support.cadence.com/apex/ArticleAttachmentPortal?id=a1O3w00000ADivx