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.