Loading...
Please wait, while we are loading the content...
Similar Documents
Image computation and predicate refinement for RTL verilog using word level proofs (2007)
| Content Provider | CiteSeerX |
|---|---|
| Author | Kroening, Daniel |
| Description | 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 wordlevel, 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, we propose to extract predicates from a word-level proof to refine the set of predicates. 1 |
| File Format | |
| Language | English |
| Publisher Date | 2007-01-01 |
| Publisher Institution | In Design, Automation and Test in Europe (DATE’07 |
| Access Restriction | Open |
| Subject Keyword | Image Computation Enabling Technique Predicate Abstraction Large Circuit Net-list-level Circuit Model Word Level Proof Proof-based Algorithm Promising Abstraction Technique Predicate Image Word-level Proof Previous Work Relies Algorithm Use Right Choice Rtl Verilog Efficient Computation |
| Content Type | Text |
| Resource Type | Article |
