CheckSpec: a tool for consistency and coverage analysis of assertion specifications

Banerjee, Ansuman ; Datta, Kausik ; Dasgupta, Pallab (2008) CheckSpec: a tool for consistency and coverage analysis of assertion specifications In: 6th International Symposium on Automated Technology for Verification and Analysis, ATVA 2008, 20-23 October 2008, Seoul, South Korea.

Full text not available from this repository.

Official URL:

Related URL:


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.

Item Type:Conference or Workshop Item (Paper)
Source:Copyright of this article belongs to Springer-Verlag Berlin Heidelberg.
ID Code:102327
Deposited On:09 Mar 2018 10:13
Last Modified:09 Mar 2018 10:13

Repository Staff Only: item control page