Image computation and predicate refinement for RTL verilog using word level proofs
- Conference Paper
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 Show more
Book title2007 Design, Automation & Test in Europe Conference & Exhibition
Pages / Article No.
MoreShow all metadata