Advertisement

CheckSpec: A Tool for Consistency and Coverage Analysis of Assertion Specifications

  • Ansuman Banerjee
  • Kausik Datta
  • Pallab Dasgupta
Part of the Lecture Notes in Computer Science book series (LNCS, volume 5311)

Abstract

As more and more chip design companies attempt to integrate formal property verification (FPV) and assertion-based verification (ABV) into their pre-silicon validation flows, the main challenge that they face is in the task of expressing the design intent correctly and accurately in terms of formal properties. Incomplete specifications allow bugs to escape detection, while inconsistent specifications lead to the loss of validation effort, since the error lies in the specification itself. In this paper, we present CheckSpec, a tool for automatically checking the consistency and completeness of assertion specifications written in System Verilog Assertions (SVA). CheckSpec comprises of two main engines, namely (a) Certify: that certifies a given assertion suite to be free from inconsistencies and (b) Quantify: that quantifies the completeness of a given assertion suite. On one hand, CheckSpec will help verification teams to avoid significant waste of validation effort arising out of inconsistent specifications. On the other hand, this will provide a first-cut estimate of the comprehensiveness of an assertion specification suite. The adoption of CheckSpec in the mainstream validation flow can significantly increase the productivity of assertion verification technologies.

Keywords

Coverage Analysis Linear Temporal Logic Design Intent Validation Effort Bounded Model Check 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. 1.
    ARM AMBA Specification Rev 2.0, http://www.arm.com
  2. 2.
    Das, S., et al.: Formal Methods for Analyzing the Completeness of an Assertion Suite against a High-Level Fault model. In: VLSI Design (2005)Google Scholar
  3. 3.
    Dasgupta, P.: A Roadmap for Formal Property Verification. Springer, Heidelberg (2006)CrossRefGoogle Scholar
  4. 4.
  5. 5.
    Open Core Protocol, http://www.ocpip.org

Copyright information

© Springer-Verlag Berlin Heidelberg 2008

Authors and Affiliations

  • Ansuman Banerjee
    • 1
  • Kausik Datta
    • 1
  • Pallab Dasgupta
    • 2
  1. 1.Interra Systems India Pvt. Ltd.India
  2. 2.Indian Institute of Technology KharagpurIndia

Personalised recommendations