Counterexample ranking using mined invariants

Mitra, Srobona ; Banerjee, Ansuman ; Dasgupta, Pallab ; Kumar, Harish (2013) Counterexample ranking using mined invariants IEEE Transactions on Computer-Aided Design of Integrated Circuits and Systems, 32 (12). pp. 1978-1991. ISSN 0278-0070

Full text not available from this repository.

Official URL:

Related URL:


Bug-fixing in deeply embedded portions of the logic is typically accompanied by the postfacto addition of new assertions, which cover the bug scenario. Formally verifying the assertions defined over such deeply embedded portions of the logic is challenging because formal methods do not scale to the size of the entire logic. Verifying the assertion on the embedded logic in isolation typically throws up a large number of counterexamples, many of which are spurious because the scenarios they depict are not possible in the entire logic. In this paper, we introduce the notion of ranking the counterexamples so that only the most likely counterexamples are presented to the designer. Our ranking is based on assume properties mined from simulation traces of the entire logic. We define a metric to compute a belief for each assume property that is mined, and rank counterexamples based on their relationships with the mined assume properties. Experimental results demonstrate a remarkable correlation between the real counterexamples (if they exist) and the proposed ranking metric, thereby establishing the proposed method as a very promising verification approach.

Item Type:Article
Source:Copyright of this article belongs to Institute of Electrical and Electronics Engineers.
Keywords:Simulation; Bayes Methods; Decision Trees; Formal Verification
ID Code:101008
Deposited On:09 Mar 2018 10:15
Last Modified:09 Mar 2018 10:15

Repository Staff Only: item control page