Untwist your brain: efficient debugging and diagnosis of complex assertions

ABSTRACT

Assertions are recognized in the industry to be a major improvement in functional RTL verification flows. Today's standard assertion languages, such as SVA [1] and PSL [2], are very expressive, capable of describing sophisticated temporal design behavior at different abstraction levels. Nevertheless, most assertion users stick to writing simple assertions because of the intricacy and effort required to debug complex assertions -- one of the major bottlenecks in assertion based verification.

We present debugging and diagnosis techniques that automatically identify those parts of an assertion that cause the assertion to fail for a given design and that provide additional automation to efficiently identify the root cause of the failure. These techniques enable major effort savings when working with complex assertions, allowing engineers to use the full capabilities of assertion languages. This enables further productivity and quality improvements in functional verification by lifting mainstream assertion usage to higher abstraction levels such as efficient capture and verification of high-level design features, operations, and transactions. Advanced debugging automation is key for this progress - solving a problem that many designers and verification engineers face in their daily work.

REFERENCES

• 1: IEEE Standard 1800--2005 SystemVerilog: Unified Hardware Design, Specification and Verification Language, USA, 2005.
• 2: IEEE Standard 1850--2005 Property Specification Language (PSL), IEEE, Inc., New York, NY, USA, 2005.
• 3: http://www.onespin-solutions.com/360mv.php
• 4: R. Wille, G. Fey, M. Messing, R. Drechsler et. al.; Identifying a subset of SystemVerilog Assertions for Efficient Bounded Model Checking, Conf. on Digital System Design (DSD), 2008.
• 5: G. Fey, S. Staber, R. Bloem, R. Drechsler. Automatic fault localization for property checking. IEEE Trans. on CAD of Integrated Circuits and Systems, 27:1138--1149, 2008.
• 6: D. Bustan and J. Havlicek. Some complexity results for SystemVerilog Assertions. CAV 2006, volume 4144 of LNCS.
• 7: J. Bormann, S. Beyer, T. Blackmore, et al. Complete Formal Verification of TriCore2 and Other Processors, DVCon 2007

INDEX TERMS

Primary Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
      B.5.2 Design Aids
          Subjects: Verification

Additional Classification:
  B. Hardware
  B.5 REGISTER-TRANSFER-LEVEL IMPLEMENTATION
      B.5.2 Design Aids
          Subjects: Simulation
  B.6 LOGIC DESIGN
      B.6.3 Design Aids
          Subjects: Simulation; Verification
  B.7 INTEGRATED CIRCUITS
      B.7.2 Design Aids
          Subjects: Simulation; Verification

General Terms:
Algorithms, Design, Languages, Verification

Keywords:
SystemVerilog assertions, assertions, debugging, fault localization, functional verification, root cause analysis