Assertive verification: a ten-minute primer

Increased use of third-party IP, such as cores, accompanies this move towards SoCs. Verifying and distributing IP to minimize the integration effort poses an array of challenges. The IP distributor has to create their design to work in an extremely wide variety of environments and maintain compliance to a standard, if applicable. The quality and exhaustiveness of the IP distributor's verification effort directly impacts the customer's experience when integrating the IP.

In general, functional verification is a bottleneck in the design development process and it commands a lot more attention and respect than in the past.

Assertion checks
Every design has fundamental characteristics that must hold true during operation in order for the design to work properly. For instance, a bus may have a Signal B that must always goes low three to five clocks cycles after Signal A goes high; a bug exists if Signal B does not adhere to this property at any time during operation. This fundamental characteristic can be defined as an individual code entity known as a property.

Properties can be implemented in either Verilog, VHDL, or an FPL (Formal Property Language). Additional code can be wrapped around basic properties and/or combined properties to build more complex properties. Entire monitors/checkers can even be built this way. A collection of basic properties, complex properties, and monitors are usually stored together in a property library. Assertions call out properties and check that the properties hold true at a given time (temporal) or at all times (static).

For whitebox verification, which is design implementation specific, design engineers can embed assertion calls inline with their RTL design. The assertion calls are written in the same language as the property library or as comments, similar to a Synopsys directive. Either way, the assertions do not get synthesized. For blackbox verification, verification engineers can instantiate assertion calls in a testbench. Assertions can be inserted at various places in or around a design:

• Around multiply instantiated blocks (such as third-party IP or reusable designs)
• Inline with code (for example, ensuring that a fundamental condition is always met)
• At the system level (for example, bus protocol monitors)
• At block boundaries (for instance, ensuring designers adhere to a negotiated interface between blocks designed by different designers)

Assertions can be simulated with the RTL to act as watchdogs throughout the simulation. IP vendors can significantly leverage this by embedding assertions in their designs. The assertions ensure the quality and proper use of the IP, while staying invisible to the customer except to flag a bug.

When used with HDL simulators, assertions can significantly reduce debug time by more directly pointing engineers to where a fault has occurred in the design. Additionally, designers can do more debug on their own d esigns, thus flushing out bugs earlier in the development process.

If the assertions are written in an FPL, an appropriate FPL compiler must compile the assertions before simulation. There is not yet a standardized FPL, but Accellera, a major electronic industry standards initiatives organization, is working toward proposing an FPL for IEEE standardization. Accellera selected IBM's internally developed FPL called "Sugar" from the four FPL submissions from members:

• Temporal e (Verisity)
• Sugar (IBM)
• CBV (Motorola)
• ForSpec (Intel)

After Accellera rejected ForSpec, Synopsys quickly joined with Intel and is now commercially packaging the language as part of its OpenVera hardware verification language. 0-In Design Automation has its own FPL variant, which uses pragmas (comment directives in the RTL) to declare assertions. OpenVera assertions call upon properties from the OVA (OpenVera Assertion) library, and 0-In Design Automation uses properties from its 0-In CheckWare libra ry. Both libraries contain predefined properties and are user expandable.

The OVL (Open Verification Library) is another assertion property library, but it's written in Verilog and VHDL rather than in an FPL. HDLs are not optimized for expressing temporal statements, but OVL is free and easily accessible for downloading from the
Figure 1 -- Simulation cycles vs. gate count
(Source: Faster and Smarter Verification; Manoj Gandhi, Sr. VP/GM Verification Technology Group, Synopsys, Inc.)

Equivalence checkers and property checkers are the two types of formal verification tools. Equivalence checkers compare that two representations of a design are functionally the same. Property checkers step through the different combinations at a design's inputs and concurrently run various checks against the design:

• Assertion checks
• Semantic inconsistency checks
  • Synopsys full case and parallel case directives
  • X-assignment
  • Casex
  • Casez
  • Range overflow
  • Uninitialized registers
• Structural inconsistency checks
  • Bus contention and floating bus issues
  • Sequential analysis
  • Stuck tri-state enables
  • Clock domain crossing checks