METHOD FOR MEASURING ASSERTION DENSITY IN A SYSTEM OF VERIFYING INTEGRATED CIRCUIT DESIGN

摘要

An assertion-based verification tool for circuit designs includes an effective measurement of assertion density for any given generated set of assertions. A register-transfer level (RTL) description of an integrated circuit (IC) is used to compute a set of predicates. Then, determination is made as to the number of predicates that are satisfiable on the given set of assertions received respective of the RTL description.;Thereafter, simulation traces for the RTL are received and the number of predicates satisfiable on the simulation traces is computed. A figure of merit of assertion density is determined from the ratio of the respective numbers of predicates. The set of assertions may be modified as required to satisfy a predetermined threshold value of assertion density, to assure that a circuit is rigorously tested by the verification tool.

主权项

1. A method implemented in a programmable system for verifying a design of an integrated circuit, comprising:
a) providing a register-transfer language description of the integrated circuit to the system; b) generating a set of assertions sufficient to test a functionality of the integrated circuit; c) measuring an assertion density of the set of assertions, wherein the assertion density is measured by a comparison of a number of predicates computed from the description that are satisfiable on the set of assertions relative to a number of predicates satisfiable on a set of simulation traces of the integrated circuit; d) comparing the measured assertion density with a predetermined threshold; e) repeatedly modifying the set of assertions or generating a new set of assertions, and re-measuring the assertion density until the measured assertion density exceeds said threshold; and f) applying the particular set of assertions for which assertion density exceeds said threshold to a design verification of the integrated circuit.