Design and Verification of On−Chip Communication Protocols
Modern computer systems rely more and more on on-chip communication protocols to exchange data. To tackle performance requirements these protocols have become highly complex, which makes their formal verification usually infeasible with reasonable time and effort. We present an initial case study fo...
| Հիմնական հեղինակներ: | , |
|---|---|
| Ձևաչափ: | Report |
| Հրապարակվել է: |
OUCL
2015
|
| _version_ | 1826287802378092544 |
|---|---|
| author | Böhm, P Melham, T |
| author_facet | Böhm, P Melham, T |
| author_sort | Böhm, P |
| collection | OXFORD |
| description | Modern computer systems rely more and more on on-chip communication protocols to exchange data. To tackle performance requirements these protocols have become highly complex, which makes their formal verification usually infeasible with reasonable time and effort. We present an initial case study for a new approach towards the design and verification of on-chip communication protocols. This new methodology combines the design and verification processes together, interleaving them in a hand-in-hand fashion. In our initial case study we present the design and verification of a simple arbiter-based master-slave communication system inspired by the AMBA High-performance Bus architecture. Starting with a rudimentary, sequential protocol, the design is extended by adding pipelining and burst transfers. Both extensions are realized as transformations of a previous version such that the correctness of the former leverages the verification of latter. Thus, we also argue about the correctness of both extended designs. |
| first_indexed | 2024-03-07T02:04:07Z |
| format | Report |
| id | oxford-uuid:9e5ec36e-c31b-4ad6-ac5c-75f3365042da |
| institution | University of Oxford |
| last_indexed | 2024-03-07T02:04:07Z |
| publishDate | 2015 |
| publisher | OUCL |
| record_format | dspace |
| spelling | oxford-uuid:9e5ec36e-c31b-4ad6-ac5c-75f3365042da2022-03-27T00:49:40ZDesign and Verification of On−Chip Communication ProtocolsReporthttp://purl.org/coar/resource_type/c_93fcuuid:9e5ec36e-c31b-4ad6-ac5c-75f3365042daDepartment of Computer ScienceOUCL2015Böhm, PMelham, TModern computer systems rely more and more on on-chip communication protocols to exchange data. To tackle performance requirements these protocols have become highly complex, which makes their formal verification usually infeasible with reasonable time and effort. We present an initial case study for a new approach towards the design and verification of on-chip communication protocols. This new methodology combines the design and verification processes together, interleaving them in a hand-in-hand fashion. In our initial case study we present the design and verification of a simple arbiter-based master-slave communication system inspired by the AMBA High-performance Bus architecture. Starting with a rudimentary, sequential protocol, the design is extended by adding pipelining and burst transfers. Both extensions are realized as transformations of a previous version such that the correctness of the former leverages the verification of latter. Thus, we also argue about the correctness of both extended designs. |
| spellingShingle | Böhm, P Melham, T Design and Verification of On−Chip Communication Protocols |
| title | Design and Verification of On−Chip Communication Protocols |
| title_full | Design and Verification of On−Chip Communication Protocols |
| title_fullStr | Design and Verification of On−Chip Communication Protocols |
| title_full_unstemmed | Design and Verification of On−Chip Communication Protocols |
| title_short | Design and Verification of On−Chip Communication Protocols |
| title_sort | design and verification of on chip communication protocols |
| work_keys_str_mv | AT bohmp designandverificationofonchipcommunicationprotocols AT melhamt designandverificationofonchipcommunicationprotocols |