Counterexample ranking using mined invariants

Abstract

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.