A Refinement Approach to Design and Verification of On−Chip Communication Protocols
Peter Böhm and Tom Melham
Abstract
Modern computer systems rely more and more on on-chip communication protocols to exchange data. To meet performance requirements these protocols have become highly complex, which usually makes their formal verification infeasible with reasonable time and effort. We present a new refinement approach to on-chip communication protocols that combines design and verification together, interleaving them hand-in-hand. Our modeling framework consists of design steps and design transformations formalized as finite state machines. Given a verified design step, transformations are used to extend the system with advanced features. A design transformation ensures that the extended design is correct if the previous system is correct. This approach is illustrated by an arbiter-based master-slave communication system inspired by the AMBA High-performance Bus architecture. Starting with a sequential protocol design, it is extended with pipelining and burst transfers. Transformations are generated from design constraints providing a basis for correctness-by-design of the derived system.
Details
| Book Title |
Proceedings of the Eighth Conference on Formal Methods in Computer−Aided Design (FMCAD'08) |
| ISBN |
978−1−4244−2735−2 |
| Location |
Portland‚ OR‚ USA |
| Month |
November |
| Pages |
136–143 |
| Publisher |
IEEE Computer Society |
| Year |
2008 |
Links
DOI (10.1109/FMCAD.2008.ECP.22)
Related pages
|
People |
|
|
Projects |
Verified Communication Protocols for Multicore/SoC Architectures |