Technical reports
Model checking the AMBA protocol in HOL
Hasan Amjad
September 2004, 27 pages
DOI: 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} }