Computer Laboratory

Technical reports

Model checking the AMBA protocol in HOL

Hasan Amjad

September 2004, 27 pages


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

  author =	 {Amjad, Hasan},
  title = 	 {{Model checking the AMBA protocol in HOL}},
  year = 	 2004,
  month = 	 sep,
  url = 	 {},
  institution =  {University of Cambridge, Computer Laboratory},
  number = 	 {UCAM-CL-TR-602}