Image Computation and Predicate Refinement for RTL Verilog using Word Level Proofs

Automated abstraction is the enabling technique for model checking large circuits. Predicate abstraction is one of the most promising abstraction techniques. It relies on the efficient computation of predicate images and the right choice of predicates. Existing algorithms use a net-list-level circuit model for computing predicate images. 1) This paper describes a proof-based algorithm that computes an over-approximation of the predicate image at the word-level, and thus, scales to larger circuits. 2) The previous work relies on the computation of the weakest preconditions in order to refine the set of predicates. In contrast to that, the paper proposed to extract predicates from a word-level proof to refine the set of predicates