Formal techniques for effective co-verification of hardware/software co-designs
Verification is indispensable for building reliable of hardware/software co-designs. However, the scope of formal methods in this domain is limited. This is attributed to the lack of unified property specification languages, the semantic gap between hardware and software components, and the lack of...
| Auteurs principaux: | , , , |
|---|---|
| Format: | Conference item |
| Publié: |
Association for Computing Machinery
2017
|
| _version_ | 1826256761759203328 |
|---|---|
| author | Mukherjee, R Purandare, M Polig, R Kroening, D |
| author_facet | Mukherjee, R Purandare, M Polig, R Kroening, D |
| author_sort | Mukherjee, R |
| collection | OXFORD |
| description | Verification is indispensable for building reliable of hardware/software co-designs. However, the scope of formal methods in this domain is limited. This is attributed to the lack of unified property specification languages, the semantic gap between hardware and software components, and the lack of verifiers that support both C and Verilog/VHDL. To address these limitations, we present an approach that uses a bounded co-verification tool, HW-CBMC, for formally validating hardware/software co-designs written in Verilog and C. Properties are expressed in C enriched with special-purpose primitives that capture temporal correlation between hardware and software events. We present an industrial case-study, proving bounded safety properties as well as discovering critical co-design bugs on a large and complex text analytics FPGA accelerator from IBM. |
| first_indexed | 2024-03-06T18:07:23Z |
| format | Conference item |
| id | oxford-uuid:01e3de52-a922-409a-b526-f3265bec195f |
| institution | University of Oxford |
| last_indexed | 2024-03-06T18:07:23Z |
| publishDate | 2017 |
| publisher | Association for Computing Machinery |
| record_format | dspace |
| spelling | oxford-uuid:01e3de52-a922-409a-b526-f3265bec195f2022-03-26T08:37:30ZFormal techniques for effective co-verification of hardware/software co-designsConference itemhttp://purl.org/coar/resource_type/c_5794uuid:01e3de52-a922-409a-b526-f3265bec195fSymplectic Elements at OxfordAssociation for Computing Machinery2017Mukherjee, RPurandare, MPolig, RKroening, DVerification is indispensable for building reliable of hardware/software co-designs. However, the scope of formal methods in this domain is limited. This is attributed to the lack of unified property specification languages, the semantic gap between hardware and software components, and the lack of verifiers that support both C and Verilog/VHDL. To address these limitations, we present an approach that uses a bounded co-verification tool, HW-CBMC, for formally validating hardware/software co-designs written in Verilog and C. Properties are expressed in C enriched with special-purpose primitives that capture temporal correlation between hardware and software events. We present an industrial case-study, proving bounded safety properties as well as discovering critical co-design bugs on a large and complex text analytics FPGA accelerator from IBM. |
| spellingShingle | Mukherjee, R Purandare, M Polig, R Kroening, D Formal techniques for effective co-verification of hardware/software co-designs |
| title | Formal techniques for effective co-verification of hardware/software co-designs |
| title_full | Formal techniques for effective co-verification of hardware/software co-designs |
| title_fullStr | Formal techniques for effective co-verification of hardware/software co-designs |
| title_full_unstemmed | Formal techniques for effective co-verification of hardware/software co-designs |
| title_short | Formal techniques for effective co-verification of hardware/software co-designs |
| title_sort | formal techniques for effective co verification of hardware software co designs |
| work_keys_str_mv | AT mukherjeer formaltechniquesforeffectivecoverificationofhardwaresoftwarecodesigns AT purandarem formaltechniquesforeffectivecoverificationofhardwaresoftwarecodesigns AT poligr formaltechniquesforeffectivecoverificationofhardwaresoftwarecodesigns AT kroeningd formaltechniquesforeffectivecoverificationofhardwaresoftwarecodesigns |