Researchon AHB Bus Formal Verification Methodbasedon UPPAAL

AMBA Bus is one of the BUS standard that is used for high performance embedded system of ARM. AHB is a high performance system bus. It Is able to keep the external memory band width and provides interfaces communicating with CPU,memory on-chip and other DMA. It is well-known that a tiny defect might make a system fail, so it is necessary and valuable to verify a AHB implementation before it is on the market. However, the challenge of verification is how to ensure the correctness of real system, in this paper, we adopt one of the most popular formal methods, e.g., model checking.In this paper, wee first introduce the architecture and SystemC based transaction model of AMBA AHB; and then the UPPAAL styled timed automaton semantics of the SystemC language; Then,with transaction model of AHB and the previous semantics, a way of translation AMBA AHB into timed automata is shown; And finally, we introduce our verification procedures with UPPAAL by several concrete examples.According to the result of our paper, it is efficient to verify AHB standard by timed automata method of UPPAAL. This provides a better solution for the verification of several important properties of AHB.