@techreport{RR-08-05,
  abstract = "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.",
  author = "Peter B{\"o}hm, Tom Melham",
  institution = "OUCL",
  month = "April",
  number = "RR-08-05",
  pages = "16",
  title = "Design and Verification of On-Chip Communication Protocols",
  url = "http://web2.comlab.ox.ac.uk/oucl/publications/tr/RR-08-05.html",
  year = "2008",
}


    
      @inproceedings{bm:fmcad08,
  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.",
  author = "Peter B{\"o}hm, Tom Melham",
  booktitle = "Proceedings of the Eighth Conference on Formal Methods in Computer-Aided Design (FMCAD'08)",
  note = "to appear",
  publisher = "IEEE Computer Society",
  title = "A Refinement Approach to Design and Verification of On-Chip Communication Protocols",
  year = "2008",
}