Formal methods for ranking counter examples through assumption mining

Mitra, S. ; Banerjee, A. ; Dasgupta, P. (2012) Formal methods for ranking counter examples through assumption mining In: 2012 Design, Automation & Test in Europe Conference & Exhibition (DATE), 12-16 March 2012, Dresden, Germany.

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 post-facto addition to new assertions which cover the bug scenario. Formally verifying properties defined over such deeply embedded portions of the logic is challenging because formal methods do not scale to the size of the entire logic, and verifying the property 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 conflicts with the mined assume properties. Experimental results demonstrate an amazing 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:Conference or Workshop Item (Paper)
Source:Copyright of this article belongs to Institute of Electrical and Electronics Engineers.
Keywords:Logic Design; Embedded Systems; Formal Verification; Logic Circuits
ID Code:101626
Deposited On:12 Dec 2016 10:58
Last Modified:12 Dec 2016 11:01

Repository Staff Only: item control page