Department of Computer Science and Technology

Technical reports

Model checking the AMBA protocol in HOL

Hasan Amjad

September 2004, 27 pages

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},
  number = 	 {UCAM-CL-TR-602}
}