Department of Computer Science and Technology

Technical reports

Model checking the AMBA protocol in HOL

Hasan Amjad

September 2004, 27 pages

DOIhttps://doi.org/10.48456/tr-602

Abstract

The Advanced Microcontroller Bus Architecture (AMBA) is an open System-on-Chip bus protocol for high-performance buses on low-power devices. In this report we implement a simple model of AMBA and use model checking and theorem proving to verify latency, arbitration, coherence and deadlock freedom properties of the implementation.

Full text

PDF (0.3 MB)

BibTeX record

@TechReport{UCAM-CL-TR-602,
  author =	 {Amjad, Hasan},
  title = 	 {{Model checking the AMBA protocol in HOL}},
  year = 	 2004,
  month = 	 sep,
  url = 	 {https://www.cl.cam.ac.uk/techreports/UCAM-CL-TR-602.pdf},
  institution =  {University of Cambridge, Computer Laboratory},
  doi = 	 {10.48456/tr-602},
  number = 	 {UCAM-CL-TR-602}
}