Browse Prior Art Database

Linear elimination of redundant variables for abstraction refinement

IP.com Disclosure Number: IPCOM000180736D
Original Publication Date: 2009-Mar-16
Included in the Prior Art Database: 2009-Mar-16
Document File: 1 page(s) / 44K

Publishing Venue

IBM

Abstract

SAT solvers are efficient at bounded model checking. Unbounded model checking is harder and very important in order to pass a design. The main challenge in unbounded model checking is proving faster on harder designs. Unbounded model checker performance is sensitive to the size and complexity of the problem. A major research effort is invested in abstracting these problems in order to enhance the abilities of the solvers. A leading method for abstraction is proof based abstraction refinement. We propose a method to make smaller abstractions than previously suggested while preserving the required invariants thus improving the performance of such algorithms.

This text was extracted from a PDF file.
This is the abbreviated version, containing approximately 73% of the total text.

Page 1 of 1

Linear elimination of redundant variables for abstraction refinement

Proof based abstraction refinement is based on an analysis of unsat cores. (detailed description in section 3.) Given a core C the set S of all signals in all clauses in C is computed. Once S is computed the set of all partitions of all signals in S is used to compute the next abstraction. We suggest to use a subset of the set S in order to create a smaller abstraction. Proof based abstraction refinement was proposed in "Automatic Abstractions without Counterexamples" at TACAS'03 by K.L. McMillan and N. Amla. Following is the pseudo of the algorithm:

1. result := unknown

2. k=0;

3. while (result is unknown)

4. sat

_

5. abstract

6. verifier

7. if (verifier

_result == Passed)

8. result = Passed;

9. k:=k+1

10. return result
Step 5 is performed as follows:

All constraints are translated into clauses.

Each constraint that has a clause in C is added to the abstract model.

We suggest the following technique to step 5, that reduces the size of the abstract model:

The design is split into partitions. Each partition describes the behavior of a given signal and is translated into a set of clauses. We define signal's "binding clauses" to be the clauses inside the signals partition that binds the signal to its partition.

For example:

The partition, x := exp can be translated into x

aux and aux

exp while aux is a boolean variable.

x

aux is translated into a cnformat (!x...