International Business Machines Corporation
Scalable model checking in functional verification by integrating user-guided abstraction

Abstract:

A method, system and computer program product for appending abstractions to a testbench used for verifying the design of an electronic circuit. According to an embodiment of the invention, a method comprises identifying a set L of one or more support properties l for a set P of one or more properties p for a given electronic circuit; computing a plurality of hardware signals s of the given electronic circuit; and creating a plurality of abstract signals ABS, including declaring a fresh abstract signal abs_s for each of the hardware signals s, and creating a fresh abstract signal abs_l for each of the support properties l of the set L; for each of the properties p of the set P, creating an abstract property version abs_p; and appending the abstract signals ABS and the abstract property abs_p to the testbench to form an appended testbench.