The best use of assertions in verification

Hardware designers and verification engineers have embraced the use of assertions. They are a way to formally specify a design's intended behavior, which must hold true during the course of a design cycle. They provide an efficient way of improving overall design cycle productivity by cutting verification time. Now, engineers do not need to go back to simulation traces and logic blocks to identify the exact cause of error, as was true in the conventional verification process, where the design was verified after implementation.

Assertions are written using formal semantics that can be verified for correctness through the use of software tools. Formal semantics make it possible to describe complex design properties in a simple and precise way and to detect hard-to-find and corner-case bugs. This reduces the designer's dependence on the use of simulation to check for functional correctness.

The verification engineer creates assertions at the specification level, while the designer creates assertions at the architectural level. They can be written in SystemVerilog Assertions, if the design is written in SystemVerilog, or Property Specification Language for independent hardware description languages, such as VHDL or Verilog.

Assertions are verified for correctness using both the simulation environment and formal environment, and design teams know they have written sufficient assertions when all points in the design specification are covered.

Do

• Start with a test plan-a document that comprises an important part of a verification environment. It monitors functional coverage of the verification process and provides feedback on the quality of the testbenches and stimulus. Then try using these time-saving techniques:

1. Write assertions along with the RTL code because it helps to identify bugs prior to any other form of verification.
2. Write simple assertions: They are easier to understand and debug.
3. Keep assertions close to the design code they are verifying to clarify the design intent verified using assertions.
4. Test each assertion as it is developed to reduce debug time.
5. Name assertions. This reduces the effort associated with debugging assertion condition failures.
6. Group similar assertions in assertion libraries to increase reusability. This is especially useful if the design has a large number of reusable components.

• Raise the level of abstraction to simplify the verification process.
• Measure functional coverage, which allows you to assess the quality of the verification effort. Functional coverage tools take assertion specification as input and give information on what checks, scenarios and data have been exercised.
• Document identified problems. Documenting techniques that have identified a bug provide information on the effectiveness of the verification process for future projects.

Don't

• Use "liveness" properties because simulation never fails on liveness properties. This can lead to a false positive scenario, where a problem could slip through. A liveness property is one that eventually becomes true after a nonfinite amount of time, or is unbounded in time. That is, if a signal "req" is asserted, the signal "ack" is asserted sometime in the future.
• Use vacuously true assertions, which may lead to false positive scenarios. An example is an assertion that states that if A happens, then B happens. Now, if A is never triggered in a design, then B is never tested.
• Synthesize assertions. Assertions should not appear in a synthesized netlist. Designers can put pragmas (translate_off/translate_on) around assertions, so that a synthesis tool can ignore assertions. They can also use an "ifdef" macro to enable or disable assertions. If a designer uses an assertion library, then he or she should insert this macro in the assertion library in order to reduce the workload.
• Use assertions for duplicate checks. Avoid adding assertions for features that have been tested with other verification techniques.
• Use assertions to verify all design features, since this increases the overall cost of adding assertions. Some of the design features for which assertions could be avoided are:

1. free-running clock,
2. glitch detection,
3. assertion code that is duplicating the RTL code. There is no need to have an assertion for an increment or decrement counter that changes value by 1.
4. Known correct components like a D flip-flop or 2:1 mux.

Vinima Aggarwal (vinima@verific.com), applications engineer at Verific Design Automation (Alameda, Calif.)