Improved Visibility in One-to-Many Trace Concretization

We present an improved algorithm for concretization of abstract eres in abstraction refinement-based invariant checking. The algorithm maps each transition of the abstract error trace to one or more transitions in the concrete model by using a combination of simulation and satisfiability checking. Prior simulationbased approaches were hindered by limited visibility, which often resulted in excessive backtracking or refinements. The proposed technique addresses this issue in three ways: By identifying variose addition to the abstract trace significantly improves its predictive power at a low computational cost; by combining SAT checks with pseudo-random simulation in the construction of the concrete trace; and by a more flexible budgeting of simulation vectors that accounts for the progress made in concretization.

• Type: Conference
• Year: 2008
• Where: DATE
• Authors: Kuntal Nanshi, Fabio Somenzi
• Keywords: Abstract Error Trace, Abstract Trace, DATE 2008, Hardware, Refinement-based Invariant Checking