The State of the Art in Digital Assertions

  • Owner: Scott Cranston
  • Secondary Owner: Ed Cerny

Use Models

There are two basic use models currently used for digital assertions:
  • Designers embed the assertions directly in the design. This can be done both at the block level and the subsystem level. These assertions are then passed on to others down the flow to ensure proper use an behavior, document intended use, and to enforce rules of usage
  • Verification Engineers (VE) add more complete checks of behavior at a system level. Since VE's are typically not allowed to make changes in the design, these assertions sit off to the side of the design using such capabilities as the PSL vunit or the SystemVerilog bind construct.

Types of Verification

  • Dynamic ABV - uses a simulator and a testbench to search for assertion violations
  • Formal ABV - formal engine exhaustively explores the state space trying to prove or disprove assertions
  • Hybrid ABV - Simulate to a certain spot, then explore the surrounding state space

Languages

  • PSL - Property Specification Language (came from IBM Sugar)
    • Relative Strengths: language neutral (Verilog, VHDL, SystemVerilog, SystemC); boolean and temporal layers are not strongly connected, easier to port to a new language
  • SystemVerilog Assertions- as name suggests, part of SystemVerilog language
    • Relative Strengths: Allows local variables that carry state
    • Weaknesses: (obviously) very tied to a particular language
  • OVL - Open Verification Library - not really a language, a set of models which implement assertion semantics. Typically not used by VE's. Captured by Mentor. IAL (Incisive Assertion Library) is the Cadence-friendly version of this.
    • Relative Strengths: Familiarity (no need to learn a new language). Easier to do things "correctly" as correct usage is enforced.

Standards

  • PSL - Accelera
  • SystemVerilog - IEEE P1800-2005
  • OVL - Accelera OVL 2.3

Tools

  • Simulators
    • Cadence NC, Simvision Assertion Browser
    • Mentor Questa
  • Formal Verifiers

Description of the current technology in use in the digital world. Languages, use models, tools, standards

-- AnandHimyanshu - 04 Feb 2009

Topic revision: r3 - 2009-02-18 - 16:33:07 - ScottCranston
 
Copyright © 2008-2024 by the contributing authors. All material on this collaboration platform is the property of the contributing authors.
Ideas, requests, problems regarding TWiki? Send feedback