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

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.