Implementation of AMBA AHB protocol for Wide Narrow BUS-SLAVE combination using VHDL
Arvind Sahu · 2012
The Advanced Microcontroller Bus Architecture (AMBA) is an open System-on-Chip bus protocol for high-performance buses on low-power devices. In this paper 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. Typical microprocessor and memory verifications assume direct connections between processors, peripherals and memory, and zero latency data transfers. They abstract away the data transfer infrastructure as it is not relevant to the verification. However, this infrastructure is in itself quite complex and worthy of formal verification. The Advanced Microcontroller Bus Architecture1 (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 verify latency, arbitration, coherence and deadlock freedom properties of the implementation. The verification is conducted using a model checker for the modal μ-calculus Lμ, that has been embedded in the HOL theorem prover [3]. This allows results from the model checker to be represented as HOL theorems for full compositionality with more abstract theorems proved in HOL using a formal model theory of Lμ that we have also developed [4].