Word-level predicate-abstraction and refinement rechniques for verifying RTL Verilog
As a first step, most model checkers used in the hardware industry convert a high-level register-transfer-level (RTL) design into a netlist. However, algorithms that operate at the netlist level are unable to exploit the structure of the higher abstraction levels and, thus, are less scalable. The RT...
| Główni autorzy: | , , , |
|---|---|
| Format: | Journal article |
| Wydane: |
Institute of Electrical and Electronics Engineers
2008
|
| _version_ | 1826303250030133248 |
|---|---|
| author | Jain, H Kroening, D Sharygina, N al., E |
| author_facet | Jain, H Kroening, D Sharygina, N al., E |
| author_sort | Jain, H |
| collection | OXFORD |
| description | As a first step, most model checkers used in the hardware industry convert a high-level register-transfer-level (RTL) design into a netlist. However, algorithms that operate at the netlist level are unable to exploit the structure of the higher abstraction levels and, thus, are less scalable. The RTL of a hardware description language such as Verilog is similar to a software program with special features for hardware design such as bit-vector arithmetic and concurrency. This paper uses predicate abstraction, a software verification technique, for verifying RTL Verilog. There are two challenges when applying predicate abstraction to circuits: 1) the computation of the abstract model in presence of a large number of predicates and 2) the discovery of suitable word-level predicates for abstraction refinement. We address the first problem using a technique called predicate clustering. We address the second problem by computing the weakest preconditions of Verilog statements in order to obtain new word-level predicates during abstraction refinement. We compare the performance of our technique with localization reduction, a netlist-level abstraction technique, and report improvements on a set of benchmarks. |
| first_indexed | 2024-03-07T05:59:48Z |
| format | Journal article |
| id | oxford-uuid:ebc6ba1b-cfb7-46e5-a404-c93e21668076 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T05:59:48Z |
| publishDate | 2008 |
| publisher | Institute of Electrical and Electronics Engineers |
| record_format | dspace |
| spelling | oxford-uuid:ebc6ba1b-cfb7-46e5-a404-c93e216680762022-03-27T11:12:26ZWord-level predicate-abstraction and refinement rechniques for verifying RTL VerilogJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:ebc6ba1b-cfb7-46e5-a404-c93e21668076Symplectic Elements at OxfordInstitute of Electrical and Electronics Engineers2008Jain, HKroening, DSharygina, Nal., EAs a first step, most model checkers used in the hardware industry convert a high-level register-transfer-level (RTL) design into a netlist. However, algorithms that operate at the netlist level are unable to exploit the structure of the higher abstraction levels and, thus, are less scalable. The RTL of a hardware description language such as Verilog is similar to a software program with special features for hardware design such as bit-vector arithmetic and concurrency. This paper uses predicate abstraction, a software verification technique, for verifying RTL Verilog. There are two challenges when applying predicate abstraction to circuits: 1) the computation of the abstract model in presence of a large number of predicates and 2) the discovery of suitable word-level predicates for abstraction refinement. We address the first problem using a technique called predicate clustering. We address the second problem by computing the weakest preconditions of Verilog statements in order to obtain new word-level predicates during abstraction refinement. We compare the performance of our technique with localization reduction, a netlist-level abstraction technique, and report improvements on a set of benchmarks. |
| spellingShingle | Jain, H Kroening, D Sharygina, N al., E Word-level predicate-abstraction and refinement rechniques for verifying RTL Verilog |
| title | Word-level predicate-abstraction and refinement rechniques for verifying RTL Verilog |
| title_full | Word-level predicate-abstraction and refinement rechniques for verifying RTL Verilog |
| title_fullStr | Word-level predicate-abstraction and refinement rechniques for verifying RTL Verilog |
| title_full_unstemmed | Word-level predicate-abstraction and refinement rechniques for verifying RTL Verilog |
| title_short | Word-level predicate-abstraction and refinement rechniques for verifying RTL Verilog |
| title_sort | word level predicate abstraction and refinement rechniques for verifying rtl verilog |
| work_keys_str_mv | AT jainh wordlevelpredicateabstractionandrefinementrechniquesforverifyingrtlverilog AT kroeningd wordlevelpredicateabstractionandrefinementrechniquesforverifyingrtlverilog AT sharyginan wordlevelpredicateabstractionandrefinementrechniquesforverifyingrtlverilog AT ale wordlevelpredicateabstractionandrefinementrechniquesforverifyingrtlverilog |