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

      • CDC+RDC Analysis - 4/20
      • Low Power Verification - 4/29
      • User2User - 5/26
      • Webinar Calendar
    • On-Demand Webinars

      • Basic Abstraction Techniques
      • Safety Analysis Techniques
      • QVIP Workflow and Debug for PCIe
      • Writing a Proxy-driven Testbench
      • Achieving High Defect Coverage
      • Visualizer Features
      • Questa Static and Formal Apps
      • All On-Demand Webinars
    • Recording Archive

      • Siemens EDA 2021 Functional Verification Webinar Series
      • Improving Your SystemVerilog & UVM Skills
      • Should I Kill My Formal Run?
      • Visualizer Debug Environment
      • Industry Data & Surveys
      • All Recordings
    • Conferences

      • DVCon 2021
      • DVCon 2020
      • DAC 2019
      • All Conferences
    • Mentor Learning Center

      • SystemVerilog Fundamentals
      • SystemVerilog UVM
      • 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 - March 2021
      • Verification Horizons - November 2020
      • Verification Horizons - July 2020
      • Issue Archive
    • About Us

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

      • Questa Basic
      • Questa Advanced
      • Mastering Questa
  • Home
  • Verification Horizons
  • December 2017
  • Debugging Inconclusive Assertions and a Case Study

Debugging Inconclusive Assertions and a Case Study

Verification Horizons - Tom Fitzpatrick, Editor

Debugging Inconclusive Assertions and a Case Study by Jin Hou - Mentor, A Siemens Business

INTRODUCTION

Formal assertion-based verification uses formal technologies to analyze if a design satisfies a given set of properties. Formal verification doesn’t need simulation testbenches and can start much earlier in the verification process. There are three possible results for an assertion after formal runs: “proven,” “fired,” and “inconclusive.” Proven means that formal has done exhaustive mathematic analysis and proved the design satisfies the assertion and no legal stimulus sequence can violate the assertion. Fired means that formal has found an error trace showing the assertion violation. Inconclusive means that formal has only found bounded proof result, i.e., the assertion is true for the bounded cycle, but may be true or false for longer cycles. An inconclusive result cannot guarantee the design function associated with the assertion is correct.

Considering the size and complexity of designs today, formal users often encounter inconclusive results for some assertions, especially when users run formal on the blocks of designs that have long sequential depths, a huge number of state bits, and complicated mathematic operations. When we get inconclusive results, we can try some simple solutions; such as increasing the run time, running more cores, and using bigger machines. If the assertion still cannot converge, we need to debug the root cause of it. In this article, we discuss the flow to debug inconclusive assertions and use an ECC design as an example to show a decomposition technique for handling inconclusive assertions.

DEBUGGING INCONCLUSIVE ASSERTIONS

The flow of debugging the root causes of inclusive assertions is shown in Figure 1 and Figure 2, below. When an assertion cannot converge, the user has to check if the design is correctly initialized. Questa® PropCheck reports the registers that are still X or Z after initialization in the generated report “formal_verify.rpt.” The user can look at the two tables “X Registers in Starting State” and “Z Registers in Starting State” in the file to find out if the design is properly initialized. If it is not, the user has to fix it, either by changing the design, writing a correct initial sequence, or using the tool command “netlist initial.”

Figure 1. Flowchart (1)


Figure 2. Flowchart (2)


Incorrect constraints may increase formal complexity. Questa® PropCheck reports which ports are constrained and which assumptions are used in the “formal_verify.rpt” file. The user can set some ports to constant, such as setting mode pin to one mode at a time, to reduce the complexity of the circuit. The user can also get rid of some complicated logic by cutting signals, or blackboxing modules or instances. These are easy steps to do. After fixing the initial state, modifying port constraints, or getting rid of some complicated logic, the user can rerun the test. If these simple steps cannot solve the inconclusive issue, the user has to do more analysis on assumptions, assertions, and design logic. Further steps are shown in Figure 2 above.

Sometimes removing assumptions can reduce complexity for formal. If an assumption drags in extra design signals that are not in the Cone of Influence circuit (COI) of the assertion, removing the assumption may be helpful. If an assumption is really complicated, introducing lots of extra state bits, removing it may help. Removing constraints may allow illegal stimulus that can result in false firing. When the assertion is fired, the user can check the error trace generated by the tool to figure out the root cause: either a design bug or missing constraint. If an assertion can be proven with under-constraining, it is still true with more constraints, i.e., the proof is valid. Sometimes adding more constraints can reduce complexity. Reducing the number of values that inputs can get may help. When over-constraining inputs, assertion firing is valid, but proof may be false.

If assertions are not written in a formal-friendly style, performance can be affected significantly. The user may consider rewriting the assertion to reduce state bits and sequential latency. If an assertion is to verify the end-to-end property of a big design, the chance to converge is small. Decomposing an end-to-end property to several simpler properties with small latencies can improve performance a lot. Since Questa® PropCheck can automatically use proven assertions as assumptions for proving other assertions (called assume-guarantee), the user can add helper assertions to leverage the tool’s features to increase performance.

Big memories and counters can introduce a lot of state bits and large cycles for formal to analyze, which can be the root cause of an inconclusive issue. The user can find out the memories and counters used by Questa® PropCheck for a specific assertion by using “formal verify –show_active_logic.” The tool reports the active logic used by formal engines and orders the signals according to their significance. The signal affecting formal the most is listed on top. The user can reduce the size of the memories and counters in the list, or remodel them.

If the user has tried all the steps introduced above, but the assertion still cannot converge, the user can contact Mentor verification support team for help.

A CASE STUDY

The design is the ECC logic shown in Figure 3. The encoder generates a syndrome, then the data and syndrome are written to the FIFO, and the decoder reads the data and syndrome from the FIFO and decodes it. The design can correct maximum 2-bit random errors in the data.

Figure 3. ECC Design


The end-to-end property verifies that data can be corrected when errors are less than 3 bits. This assertion may not converge within a reasonable time due to the complicated mathematical operations in the encoder and decoder and the long latency and large state bits introduced by the FIFO. To verify this design, we can verify the encoder and decoder separately from verifying the FIFO. We have to create a wrapper that only instantiates the encoder and the decoder as shown in Figure 4.

Figure 4. Wrapper for the Encoder and the Decoder


After the FIFO is not included, the formal complexity for the property verifying the correctness of the encoder and the decoder is reduced a lot, and the property writing also becomes much simpler. The property can be written using SystemVerilog Assertions (SVA) or the tool command “netlist property” as follows:

SVA:

Check_err_corrected: assert property (@(posedge clk) disable iff (!rstn) dout == din);
 

Tool directive:

netlist property –name Check_err_corrected -assert {dout == din}
 

We can use Questa® PropCheck’s command “netlist cutpoint” to inject random errors using the following tcl file “inject_errors.tcl.”

 for {set i 0} {$i < 26} {incr i} {
    if {$i < 16} {
       netlist cutpoint data\[$i\] -cond (randbit\[$i\]==1'b1)
    } else { 
       netlist cutpoint syn\[[expr {$i-16}]\] -cond (randbit\[$i\]==1'b1)
    }
 }
 netlist property -name assume_2errs -assume
{$countones(randbit) <= 2}
 

Here “randbit” is an undriven wire defined in the wrapper. Formal considers undriven wires as free variables that can get any values randomly. When any bit of “randbit” is 1, the associated “data” bit or “syn” bit is cut. Since we define “assume_2errs” to constrain “randbit” to have maximum 2 bits of value 1, the maximum number of “data” and “syn” bits that can be cut is 2. When a signal is cut, it is not controlled by design logic anymore, instead it becomes a free variable for formal to control. The cut signal bits can be any value; as errors are injected when they get values different from the correct values. The above code can inject 0, 1, 2 errors randomly. When formal proves “check_err_corrected”, it proves “dout” always equals to “din” considering all random 0, 1, 2 errors. The Makefile to run the verification task is as follows:

 Run: compile formal
 compile:
	vlib work
	vlog rtl/wrapper.v –y ./rtl +incdir+./rtl +libext+.v
 formal:
	qverify –c –od log –do “ \
	do inject_errors.tcl; \
	netlist property –name Check_err_corrected –assert {dout==din}; \
	formal compile –d wrapper; \
	formal verify; \
 exit”
 

Now we have verified the encoder and the decoder. If the FIFO module has design bugs, the original ECC won’t work. We have to verify FIFO to make sure it is correct. We can use the Questa® QFL library to verify the FIFO. To use the library, we can simply copy the template “qfl_fifo_single_clock.template.sv” under the QFL installation directory to “bind_qfl_fifo.sv,” and modify the parameters and signal names to match the ECC design, shown below.

bind fifo qfl_fifo_single_clock
#(
    .WIDTH              (26),
    .DEPTH              (64),
    .TIMEOUT            (0),
    .ENQ_WIDTH          (1),
    .DEQ_WIDTH          (1),
    .ENABLE_ASSERT      (1),
    .ENABLE_COVER       (1)
)
    QFL_INSTANCE_FIFO_SINGLE_CLOCK
(
`ifdef QFL_TEMPLATE_PORT_CONNECTIONS_ALL
    .*
`else
    /*input   [ENQ_WIDTH - 1:0]           */    .enq        (push),
    /*input   [ENQ_WIDTH * WIDTH - 1:0]   */    .enq_data   (data_in),
    /*input   [DEQ_WIDTH - 1:0]           */    .deq        (pop),
    /*input   [DEQ_WIDTH * WIDTH - 1:0]   */    .deq_data   (data_out),
 
    /*input                               */    .clk        (clk),
    /*input                               */    .resetn     (rstn)
`endif
);
 

When verifying the FIFO, we can read in the original design ECC to make sure the FIFO is working in the context of the design. For verifying the FIFO, we don’t care about the actual value of the data written into the FIFO. To reduce the complexity, we cut the signals “data” and “syn” to remove the complicated encoder logic. Now “data” and “syn” become free inputs to the FIFO for formal. If the tool can verify that for any values written to the FIFO, the values are read out in the correct order from the FIFO, the data integrity feature of the FIFO is proven. Using the Questa® QFL FIFO library, the tool can automatically verify FIFO data integrity, no overflow, no underflow, and no timeout.

The Makefile to verify the FIFO is as follows. The first “vlog” command compiles the RTL files of the design, the second “vlog” command compiles the QFL library and the bind file. For the FIFO to work correctly, the primary inputs “wr_en” and “rd_en” have to be constrained such that when the FIFO is empty, “rd_en” cannot be issued, and when the FIFO is full, “wr_en” cannot be issued. We use the “netlist property” command to define these two constraints in the example.

INSTALL := $(shell qverify -install_path)
run: compile formal
compile:
   vlib work
   vlog rtl/ecc_top.v -y ./rtl  +incdir+./rtl +libext+.v
   vlog -sv -mfcu -cuname mybind qft_files/bind_qfl_fifo.sv \
   -y $(INSTALL)/share/QFL/checkers +libext+.sv \
   +incdir+$(INSTALL)/share/QFL/checkers
formal:
   qverify -c -od log -do " \
   netlist cutpoint data; \
   netlist cutpoint e_syn; \
   netlist property -name constr_no_underflow -assume {!(rd_en && empty)}; \
   netlist property -name constr_no_overflow -assume {!(wr_en && full)}; \
   formal compile -d ecc_top -cuname mybind; \
   formal verify; \
   exit"
 

SUMMARY

In this article we discussed the flow to debug inconclusive assertions and also some techniques to reduce formal complexity that may result in inconclusive assertions; including fixing incorrect initial state and incorrect constraints, removing complicated design logic by blackboxing design module/instance or cutting design signals, and reducing assertion complexity. We looked at a testcase where we reduced the complexity of the original end-to-end property by verifying the complicated arithmetic blocks and FIFO separately. There are a lot of creative ways to reduce formal complexity and get more results from formal runs. To learn more, you can check our Verification Academy website for the course “Handling Inconclusive Assertions in Formal Verification.”

Back to Top

Table of Contents

Verification Horizons Articles:

  • When It Comes to Verification, Hitting the Wall Can Be a Good Thing

  • How Static and Dynamic Failure Analysis Can Improve Productivity in the Assessment of Functional Safety

  • Step-by-step Tutorial for Connecting Questa® VIP into the Processor Verification Flow

  • PA GLS: The Power Aware Gate-level Simulation

  • Reset Verification in SoC Designs

  • Debugging Inconclusive Assertions and a Case Study

  • Getting Generic with Test Intent: Separating Test Intent from Design Details with Portable Stimulus

Siemens Digital Industries Software

Siemens Digital Industries Software

##TodayMeetsTomorrow

Solutions

  • Cloud
  • Mendix
  • Siemens EDA
  • MindSphere
  • Siemens PLM
  • View all portfolio

Explore

  • Digital Journeys
  • Community
  • Blog
  • Online Store

Siemens

  • About Us
  • Careers
  • Events
  • News and Press
  • Newsletter
  • Customer Stories

Contact Us

USA:

phone-office +1 800 547 3000

See our Worldwide Directory

  • Contact Us
  • Support Center
  • Give us Feedback
©2021 Siemens Digital Industries Software. All Rights Reserved.
Terms of Use Privacy Cookie Policy