Formal Co-Validation of Low-Level Hardware/Software Interfaces
Today's microelectronics industry is increasingly confronted with the challenge of developing and validating software that closely interacts with hardware. These interactions make it difficult to design and validate the hardware and software separately; instead, a verifiable co-design is requir...
| Main Authors: | , , , , , , , |
|---|---|
| Format: | Conference item |
| Published: |
2013
|
| _version_ | 1797077349159665664 |
|---|---|
| author | Horn, A Tautschnig, M Val, C Liang, L Melham, T Grundy, J Kroening, D IEEE |
| author_facet | Horn, A Tautschnig, M Val, C Liang, L Melham, T Grundy, J Kroening, D IEEE |
| author_sort | Horn, A |
| collection | OXFORD |
| description | Today's microelectronics industry is increasingly confronted with the challenge of developing and validating software that closely interacts with hardware. These interactions make it difficult to design and validate the hardware and software separately; instead, a verifiable co-design is required that takes them into account. This paper demonstrates a new approach to co-validation of hardware/software interfaces by formal, symbolic co-execution of an executable hardware model combined with the software that interacts with it. We illustrate and evaluate our technique on three realistic benchmarks in which software I/O is subject to hardware-specific protocol rules: a real-time clock, a temperature sensor on an I2C bus, and an Ethernet MAC. We provide experimental results that show our approach is both feasible as a bug-finding technique and scales to handle a significant degree of concurrency in the combined hardware/software model. © 2013 FMCAD Inc. |
| first_indexed | 2024-03-07T00:16:39Z |
| format | Conference item |
| id | oxford-uuid:7b10ab2d-00a7-4658-8d4f-3d6432013f33 |
| institution | University of Oxford |
| last_indexed | 2024-03-07T00:16:39Z |
| publishDate | 2013 |
| record_format | dspace |
| spelling | oxford-uuid:7b10ab2d-00a7-4658-8d4f-3d6432013f332022-03-26T20:48:14ZFormal Co-Validation of Low-Level Hardware/Software InterfacesConference itemhttp://purl.org/coar/resource_type/c_5794uuid:7b10ab2d-00a7-4658-8d4f-3d6432013f33Symplectic Elements at Oxford2013Horn, ATautschnig, MVal, CLiang, LMelham, TGrundy, JKroening, DIEEEToday's microelectronics industry is increasingly confronted with the challenge of developing and validating software that closely interacts with hardware. These interactions make it difficult to design and validate the hardware and software separately; instead, a verifiable co-design is required that takes them into account. This paper demonstrates a new approach to co-validation of hardware/software interfaces by formal, symbolic co-execution of an executable hardware model combined with the software that interacts with it. We illustrate and evaluate our technique on three realistic benchmarks in which software I/O is subject to hardware-specific protocol rules: a real-time clock, a temperature sensor on an I2C bus, and an Ethernet MAC. We provide experimental results that show our approach is both feasible as a bug-finding technique and scales to handle a significant degree of concurrency in the combined hardware/software model. © 2013 FMCAD Inc. |
| spellingShingle | Horn, A Tautschnig, M Val, C Liang, L Melham, T Grundy, J Kroening, D IEEE Formal Co-Validation of Low-Level Hardware/Software Interfaces |
| title | Formal Co-Validation of Low-Level Hardware/Software Interfaces |
| title_full | Formal Co-Validation of Low-Level Hardware/Software Interfaces |
| title_fullStr | Formal Co-Validation of Low-Level Hardware/Software Interfaces |
| title_full_unstemmed | Formal Co-Validation of Low-Level Hardware/Software Interfaces |
| title_short | Formal Co-Validation of Low-Level Hardware/Software Interfaces |
| title_sort | formal co validation of low level hardware software interfaces |
| work_keys_str_mv | AT horna formalcovalidationoflowlevelhardwaresoftwareinterfaces AT tautschnigm formalcovalidationoflowlevelhardwaresoftwareinterfaces AT valc formalcovalidationoflowlevelhardwaresoftwareinterfaces AT liangl formalcovalidationoflowlevelhardwaresoftwareinterfaces AT melhamt formalcovalidationoflowlevelhardwaresoftwareinterfaces AT grundyj formalcovalidationoflowlevelhardwaresoftwareinterfaces AT kroeningd formalcovalidationoflowlevelhardwaresoftwareinterfaces AT ieee formalcovalidationoflowlevelhardwaresoftwareinterfaces |