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
      • Fault Campaign for Mixed-Signal - 5/4
      • 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
  • February 2013
  • Using Formal Analysis to “Block and Tackle”

Using Formal Analysis to “Block and Tackle”

Verification Horizons - Tom Fitzpatrick, Editor

Using Formal Analysis to Block and Tackle by Paul B. Egan, Rockwell Automation

INTRODUCTION

Using formal analysis to validate chip level connectivity is one of "The Top Five Formal Verification Applications" (Verification Horizons Oct 2012), and has been proven as the most efficient way to verify interconnects in complex Systems on Chips (SoCs) [3, 4, 5]. So, could formal analysis also be applied at the module level, even small modules? To test our theory, formal connectivity verification was first run on a relatively small block that contained eight instances each of seven different modules (56 instances total). We discovered that, not only does it work well on small blocks, formal analysis found two bugs that would have been very difficult to find in simulation.

Traditionally, connectivity verification at the block level has been completed using dynamic simulation, and typically involves writing directed tests to toggle the top level signals, then debugging why signal values did not transition as expected. For modules with a high number of wires and many modes of operation, the number of required tests quickly becomes unmanageable. We were searching for a better approach.

This article will explain how we applied formal analysis at the block level, extended this to full chip and describe how we significantly reduced verification time at both the block and chip level. Just like a block and tackle provides a mechanical advantage, the formal connectivity flow provides a verification advantage.

APPROACH

Formal connectivity verification was first used on a relatively small block (retriggerable timers) that contained eight instances of seven different modules (56 instances total). The sub-modules are connected to common busses at the top level of the block; several instances have a port that forms a part-select (slice) for a vector net. The RTL code for this module is very compact due to the use of a generate construct (pseudo code shown here):

genvar gen_modules;
generate for (gen_modules = 0; gen_modules < NUM_OF_MODULES; gen_modules++) begin : gen_blk_module_1 module_1 u_module_1 () end endgenerate : : generate for (gen_modules = 0; gen_modules < NUM_OF_MODULES; gen_modules++) begin : gen_blk_module_N module_N u_module_N () end endgenerate

The connectivity verification flow is a very simple three step process as shown in Figure 1.

Figure 1. Connectivity Formal Verification Flow

Figure 1. Connectivity Formal Verification Flow
  1. Create a spreadsheet that defines point to point connections
  2. Run script to generate properties
  3. Run static Formal Verification

STEP 1: CREATE THE SPREADSHEET

The connectivity is defined in a Tab Separated Value (TSV) file (shown below) that can be created using any standard text editor, but using a spreadsheet tool like MS-Excel or OpenOffice Calc makes the data entry easier. For the retriggerable timers block, the connections are all point to point without any delay, so the "connect" keyword is used for the connectivity check:

# connectivity
checks
pointA pointB
connect comparator_blks[0].comparator.secondary_
trigger_count_rd_data[2:0]
secondary_trigger_count_rd_data[2:0]
connect comparator_blks[1].comparator.secondary_
trigger_count_rd_data[2:0]
secondary_trigger_count_rd_data[5:3]


STEP 2: RUN SCRIPT TO GENERATE PROPERTIES

Once the TSV file has been created, run the utility to generate the properties used for formal verification.

GenConn timers.tsv -m -tsv -sva -o checkers.sv

STEP 3: RUN STATIC FORMAL VERIFICATION

The next step in the process is to run Formal analysis using the generated checkers. Two additional files are required to run Formal, an initialization sequence file that describes the reset sequence for the design and a directives file that defines the clock(s). The design and checkers are compiled, and Formal is run:

vlib work
vmap work work
vlog –f filelist –sv
vlog –sv checkers.sv

qformal –c –od conn_results –do "do directives.tcl; \
formal compile –d retriggerable_timers_wrapper
               –cuname bindings; \
formal verify –init init.seq –effort high; exit"

The compilation and Formal analysis commands are best done using a script in the language of your choice (i.e. TCL, Make, Perl, Python, etc). After confirming all syntax and hierarchical paths were correct on a single connection, we added the remaining paths to the TSV file. This block has 112 connections, but only 14 unique connections per instance so populating the TSV file was easily done using copy/paste/edit.

Once we were comfortable with the connectivity verification flow on a small block, the next step was to use this process on a larger, more complex block - the I/O multiplexer (pin_multiplex) block in our design. Our design has 8 groups of General Purpose Input Output (GPIO) pins, each with 16 pins that can be connected to 16 different peripherals (SPI, Ethernet, UART, I2C, etc) inside the chip, or configured as a plain old input or output. The pin_multiplex block is a large programmable multiplexor that connects the peripherals in the SoC core to/from the I/O pads through the GPIO block. The GPIO block contains additional multiplexing logic that we verified with chip level connectivity testing.

The pin_multiplex block has approximately 6144 paths to check – 2048 outputs, 2048 output enables, 2048 inputs. Creating the TSV file for this block took a bit more time, and uses a conditional connect check:

# G1-0 pointA pointB condition
cond output_state[0] g1_out_region_state[0] (out_region_config_0_ff[3:0]==4'h2) &
(region_enable_g1_g2_ff[0]==1'b1)

After we completed testing at the block level, we ran at the chip level. The pin_multiplex TSV file was used as a starting point for the top level TSV file; path names were edited using global search/replace, and the condition was updated to include the GPIO block:

# G1–0 pointA pointB condition
cond neo_top_
wrapper.u_
neo_top.u_
neo_core.u_
pin_multiplex.
output_state[0]
neo_top_wrapper.u_
neo_top.G1_core_
out[0]]
(neo_top_wrapper.u_neo_top.u_
neo_core.u_pin_multiplex.
out_region_config_0_ff[3:0]==4'h2)
& (neo_top_wrapper.u_neo_top.u_
neo_core.u_pin_multiplex.region_
enable_g1_g2_ff[0]==1'b1) & (neo_top_
wrapper.u_neo_top.u_neo_core.u_gpio.
gpo_enbl_g1_g2_rd_data[0]==1'b0) &
(neo_top_wrapper.u_neo_top.u_neo_
core.u_gpio.gpo_invert_g1_g2_rd_
data[0]==1'b0)


RESULTS

Formal analysis on the retriggerable timers block found two bugs that would have been very difficult to find in simulation: incorrect vector bit-select, and an incorrect indexed part select on a vectored net connection (see code on the opposite page).

For this particular block, tool setup was insignificant, less than an hour to create an input spreadsheet; runtime was less than 2 minutes. Closer inspection of the RTL shows there are several potential errors that were easily detected using Formal:

  • Vector order on secondary_trigger_count_rd_data
  • Vector bit select
  • Indexed part-select base expression (vector[base_expr+: width_expr])
  • Indexed part-select width expression
  • Indexed part-select operator (-:, +:)

Note: For detailed syntax rules see IEEE 1364-2005 section 5.2.1 Vector bit-select and part-select addressing Analysis of the pin_multiplex block found several "showstopper" bugs:

  • Incorrect output enable on a SPI port
  • Incorrect output enables on the ECC pins for a memory port
  • Missing pin assignments for a memory port
  • Pin connections where none should exist

Since our chip is designed to boot from an external device, the first two bugs would have made the chip almost unusable. Setup, analysis and debugging failures took about 32 hours, and runtime was about 2 or 3 minutes. We estimate using formal analysis to verify connectivity was more than 10X faster than using simulation. Another critical advantage is that formal is exhaustive; not only were all "legal" pin assignments validated, we confirmed there were no "illegal" pin assignments either. For example, a SPI clock can be connected to only 4 of the 128 available pins. Verifying the legal pin connections in simulation can be done during chip level functional testing of the peripherals, but it is much more difficult to verify if the SPI clock is connected to any of the 124 pins it shouldn't be.

Connectivity checking at the chip level was nearly as easy as our smallest block since we had already verified the pin_ multiplex block. Setup and analysis was less than 16 hours; runtime was less than 5 minutes, and no bugs were found.

:
output logic [23:0] secondary_trigger_count_rd_data,
:
generate for (gen_modules = 0; gen_modules < NUM_OF_TIMERS; gen_modules++)
 begin : seed_enable_blks
         seed_enable #(
         // Parameters
          .NUM_OF_SEC_TRIGGERS (NUM_OF_SEC_TRIGGERS)
         )
         u_seed_enable
             (
             // Interfaces
             .ahb_if (ahb_if),
             // Bug #1
             // gen_control_reg should be gen_modules
             .compare_control (compare_control[gen_control_reg]),
             // Outputs
             .execute_seed_logic (execute_seed_logic[gen_modules]),
             .seed_logic_phase (seed_logic_phase[gen_modules]),
             // Inputs
             .compare_active (compare_active[gen_modules]),
             .compare_type (compare_type[gen_modules]),
             // Bug #2 [gen_modules +: 3] should be [gen_modules*3 +: 3]
             .secondary_trigger_count_rd_data(secondary_trigger_count_rd_data[gen_modules +: 3])
             );
 end
endgenerate // block : seed_enable_blks

CONCLUSIONS

Formal analysis for SoC interconnect verification is a proven methodology and this technique should also be applied at the module level, even small blocks. This is especially true for any modules that have a large number of wide busses connected, and modules that use Generate constructs and/ or Vectors with part-selects (base_expr +/-: width_expr). The setup is semi-automated, does not require a testbench, has fast runtime, and is well supported by the Electronic Design Automation (EDA) tool vendors.

Where the connectivity flow really shined was for the dreaded late stage design change. In our case a change request was made to add an output signal to two multiplexed output pins; the initial estimate of schedule impact was 1 week to implement and verify; the actual verification took less than 15 minutes – edit 4 lines in the TSV file and rerun Formal.

TIPS

  • Use a SystemVerilog wrapper on the top module. Most simulation tools don't support interfaces on top level ports. Even if there are no interfaces on the top module, having a wrapper makes it easier if an interface is added later in the design cycle.
  • Always start small; verify a single path first. Once you have identified the correct design hierarchical paths and signal names, adding remaining connections is easy (copy, paste, edit).
  • For chip level connectivity verification, only compile the modules you need. This will improve runtime, and tools will automatically blackbox empty modules. There is no reason to compile modules that do not affect connectivity.
  • For chip level connectivity verification, bypass internal clock generators like PLL's and connect directly to the clock you need in the top level wrapper using a hierarchical assign statement:

    assign u_neo_top.u_neo_core.clk_apb1x = clk_apb1x ;

REFERENCES

  1. "IEEE Standard for Verilog Hardware Description Language", IEEE STD 1364-2005, 2005
  2. "IEEE Standard for System Verilog-Unified Hardware Design, Specification, and Verification Language", 1800-2009, 2009
  3. Mark Handover, Abdelouahab Ayari, "Using Formal Verification to check SoC connectivity correctness", Mentor Graphics
  4. Olivia Wu, "Push Button Verification of Complex Pad Ring Logic Direct from an Executable Specification" Proceedings of the 48th Design Automation Conference, 2011
  5. Subir K. Roy, "Top Level SoC Interconnectivity Verification using Formal Techniques", International Workshop on Microprocessor Test and Verification, Austin, Texas,USA, 2007

Back to Top

Table of Contents

Verification Horizons Articles:

  • What Do Meteorologists and Verification Technologists Have in Common?

  • Using Formal Analysis to "Block and Tackle"

  • Bringing Verification and Validation under One Umbrella

  • System Level Code Coverage using Vista Architect and SystemC?

  • The Evolution of UPF: What's Next?

  • Top Five Reasons Why Every DV Engineer Will Love the Latest SystemVerilog 2012 Features

  • SVA in a UVM Class-based Environment

  • The Formal Verification of Design Constraints

  • OVM to UVM Migration, or "There and Back Again: A Consultant's Tale"

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