UC Berkeley

Model Checking (MC) on a word-level circuit has important applications in the IC design industry, where MC is used to prove that a word-level circuit always satisfies a set of given properties.

MC is challenging at the word level, when complex arithmetic operators like multipliers are involved.

Abstraction and refinement are commonly used to address challenging MC problems.

If an abstraction is proved, so is the original problem.

Otherwise, spurious counterexamples are analyzed to refine abstractions.

Although many abstraction refinement algorithms for word-level MC have been developed, few take full advantage of state-of-the-art bit-level MC algorithms, like Property Directed Reachability (PDR), which is considered the most efficient method for deriving unbounded proofs.

Therefore, this thesis presents several techniques that enable efficient word-level MC by performing abstraction refinement at the word-level while verifying abstractions at the bit-level.

To compute good abstractions and refinements at the word-level, novel refinement strategies were proposed to take advantage of both structural and proof-based analysis.

The proposed strategies are shown to achieve a good balance between the sizes of the abstractions and the number of refinement iterations needed for convergence.

To achieve efficient integration of abstraction refinement and bit-level MC algorithms,

a bit-level algorithm, PDRA, was created, that minimally modifies the original PDR algorithm to perform on-the-fly abstraction refinement.

Inspired by this, a word-level algorithm, PDR-WLA, was developed that efficiently integrates bit-level PDR implementations with word-level abstraction refinement. An important feature is the re-use of reachability information learned in previous refinement iterations.

Motivated by real industrial benchmarks characterized by having many related arithmetic operators,

a word-level MC algorithm, UFAR, was proposed that uses uninterpreted functions (UF) constraints as a method of refinement.

A UF constraint, between a pair of word-level operators, requires that if their inputs are equal then their outputs are equal.

To enhance the applicability of UF constraints, a procedure for normalizing operators was devised. This allows UF constraints to be applied to a pair of same-type operators with different operator sizes and signedness.

UFAR explicitly encodes UF constraints into word-level circuits. This allows any bit-level or word-level MC algorithm to be used, including both PDRA and PDR-WLA.

All these developments were implemented in a publically available model checking system, ABC.

Experiments were done which show that UFAR successfully solves most cases in a large set of challenging benchmarks provided by an industrial collaborator.