Word level predicate abstraction and refinement for verifying RTL verilog
Model checking techniques applied to large industrial circuits suffer from the state space explosion problem. A major technique to address this problem is abstraction. The most commonly used abstraction technique for hardware verification is localization reduction, which removes latches that are not...
| Autores principales: | , , , |
|---|---|
| Otros Autores: | |
| Formato: | Conference item |
| Publicado: |
Association for Computing Machinery
2005
|
| _version_ | 1826293855866060800 |
|---|---|
| author | Jain, H Sharygina, N Kroening, D Clarke, E |
| author2 | Jr, W |
| author_facet | Jr, W Jain, H Sharygina, N Kroening, D Clarke, E |
| author_sort | Jain, H |
| collection | OXFORD |
| description | Model checking techniques applied to large industrial circuits suffer from the state space explosion problem. A major technique to address this problem is abstraction. The most commonly used abstraction technique for hardware verification is localization reduction, which removes latches that are not relevant to the property. However, localization reduction fails to reduce the size of the model if the property actually depends on most of the latches. This paper proposes to use predicate abstraction for verifying RTL Verilog, a technique successfully used for software verification. The main challenge when using predicate abstraction is the discovery of suitable predicates. We propose to use weakest preconditions of Verilog statements in order to obtain new predicates during abstraction refinement. This technique has not been applied to circuits before. On benchmarks taken from an industrial microprocessor, we successfully verified safety properties with more than 32,000 latches in the cone of influence. We compare the performance of our technique with a modern model checker that implements localization reduction. |
| first_indexed | 2024-03-07T03:36:36Z |
| format | Conference item |
| id | oxford-uuid:bc816dd0-99b0-47cf-a0ee-04f7dae09dfa |
| institution | University of Oxford |
| last_indexed | 2024-03-07T03:36:36Z |
| publishDate | 2005 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | oxford-uuid:bc816dd0-99b0-47cf-a0ee-04f7dae09dfa2022-03-27T05:24:52ZWord level predicate abstraction and refinement for verifying RTL verilogConference itemhttp://purl.org/coar/resource_type/c_5794uuid:bc816dd0-99b0-47cf-a0ee-04f7dae09dfaSymplectic Elements at OxfordAssociation for Computing Machinery2005Jain, HSharygina, NKroening, DClarke, EJr, WMartin, GKahng, AModel checking techniques applied to large industrial circuits suffer from the state space explosion problem. A major technique to address this problem is abstraction. The most commonly used abstraction technique for hardware verification is localization reduction, which removes latches that are not relevant to the property. However, localization reduction fails to reduce the size of the model if the property actually depends on most of the latches. This paper proposes to use predicate abstraction for verifying RTL Verilog, a technique successfully used for software verification. The main challenge when using predicate abstraction is the discovery of suitable predicates. We propose to use weakest preconditions of Verilog statements in order to obtain new predicates during abstraction refinement. This technique has not been applied to circuits before. On benchmarks taken from an industrial microprocessor, we successfully verified safety properties with more than 32,000 latches in the cone of influence. We compare the performance of our technique with a modern model checker that implements localization reduction. |
| spellingShingle | Jain, H Sharygina, N Kroening, D Clarke, E Word level predicate abstraction and refinement for verifying RTL verilog |
| title | Word level predicate abstraction and refinement for verifying RTL verilog |
| title_full | Word level predicate abstraction and refinement for verifying RTL verilog |
| title_fullStr | Word level predicate abstraction and refinement for verifying RTL verilog |
| title_full_unstemmed | Word level predicate abstraction and refinement for verifying RTL verilog |
| title_short | Word level predicate abstraction and refinement for verifying RTL verilog |
| title_sort | word level predicate abstraction and refinement for verifying rtl verilog |
| work_keys_str_mv | AT jainh wordlevelpredicateabstractionandrefinementforverifyingrtlverilog AT sharyginan wordlevelpredicateabstractionandrefinementforverifyingrtlverilog AT kroeningd wordlevelpredicateabstractionandrefinementforverifyingrtlverilog AT clarkee wordlevelpredicateabstractionandrefinementforverifyingrtlverilog |