Relational STE and theorem proving for formal verification of industrial circuit designs
Model checking by symbolic trajectory evaluation, orchestrated in a flexible functional-programming framework, is a well-established technology for correctness verification of industrial-scale circuit designs. Most verifications in this domain require decomposition into subproblems that symbolic tra...
| Asıl Yazarlar: | , , |
|---|---|
| Materyal Türü: | Conference item |
| Baskı/Yayın Bilgisi: |
2013
|
| _version_ | 1826306252101124096 |
|---|---|
| author | O'Leary, J Kaivola, R Melham, T |
| author_facet | O'Leary, J Kaivola, R Melham, T |
| author_sort | O'Leary, J |
| collection | OXFORD |
| description | Model checking by symbolic trajectory evaluation, orchestrated in a flexible functional-programming framework, is a well-established technology for correctness verification of industrial-scale circuit designs. Most verifications in this domain require decomposition into subproblems that symbolic trajectory evaluation can handle, and deductive theorem proving has long been proposed as a complement to symbolic trajectory evaluation to enable such compositional reasoning. This paper describes an approach to verification by symbolic simulation, called Relational STE, that raises verification properties to the purely logical level suitable for compositional reasoning in a theorem prover. We also introduce a new deductive theorem prover, called Goaled, that has been integrated into Intel's Forte verification framework for this purpose. We illustrate the effectiveness of this combination of technologies by describing a general framework, accessible to non-experts, that is widely used for verification and regression validation of integer multipliers at Intel. © 2013 FMCAD Inc. |
| first_indexed | 2024-03-07T06:45:07Z |
| format | Conference item |
| id | oxford-uuid:fa9c8e48-118a-4fc8-b0b4-2fddbb3e4b01 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T06:45:07Z |
| publishDate | 2013 |
| record_format | dspace |
| spelling | oxford-uuid:fa9c8e48-118a-4fc8-b0b4-2fddbb3e4b012022-03-27T13:07:14ZRelational STE and theorem proving for formal verification of industrial circuit designsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:fa9c8e48-118a-4fc8-b0b4-2fddbb3e4b01Symplectic Elements at Oxford2013O'Leary, JKaivola, RMelham, TModel checking by symbolic trajectory evaluation, orchestrated in a flexible functional-programming framework, is a well-established technology for correctness verification of industrial-scale circuit designs. Most verifications in this domain require decomposition into subproblems that symbolic trajectory evaluation can handle, and deductive theorem proving has long been proposed as a complement to symbolic trajectory evaluation to enable such compositional reasoning. This paper describes an approach to verification by symbolic simulation, called Relational STE, that raises verification properties to the purely logical level suitable for compositional reasoning in a theorem prover. We also introduce a new deductive theorem prover, called Goaled, that has been integrated into Intel's Forte verification framework for this purpose. We illustrate the effectiveness of this combination of technologies by describing a general framework, accessible to non-experts, that is widely used for verification and regression validation of integer multipliers at Intel. © 2013 FMCAD Inc. |
| spellingShingle | O'Leary, J Kaivola, R Melham, T Relational STE and theorem proving for formal verification of industrial circuit designs |
| title | Relational STE and theorem proving for formal verification of industrial circuit designs |
| title_full | Relational STE and theorem proving for formal verification of industrial circuit designs |
| title_fullStr | Relational STE and theorem proving for formal verification of industrial circuit designs |
| title_full_unstemmed | Relational STE and theorem proving for formal verification of industrial circuit designs |
| title_short | Relational STE and theorem proving for formal verification of industrial circuit designs |
| title_sort | relational ste and theorem proving for formal verification of industrial circuit designs |
| work_keys_str_mv | AT olearyj relationalsteandtheoremprovingforformalverificationofindustrialcircuitdesigns AT kaivolar relationalsteandtheoremprovingforformalverificationofindustrialcircuitdesigns AT melhamt relationalsteandtheoremprovingforformalverificationofindustrialcircuitdesigns |