Formal Modeling and Model Checking Analysis of the Avalon System-on-Chip Bus Protocol
Tianlong Gu · Journal of Guilin University of Electronic Technology · 2009
In Bus-based on-chip system(SOC),kinds of IP cores are interconnected by On-chip-bus(OCB) and the data interactive is to comply with the bus protocol.As a core technology in SOC,the chip bus protocol greatly determines reliability in SOC.The characteristic and complexity bring great challenge for formal analysis and verification.In this paper,the Avalon Onchip-bus was used as an example,and an efficient way for formal analysis of the system on a programmable bus protocol was developed.Firstly,the information was abstractly extracted according to the protocol specification,and the mode of finite state machine for Avalon bus protocol was created.At the same time the interrelated properties of the protocol was strictly described by computation tree logic.Finally,the properties were analyzed and verified by the mode checking tool of SMV.The result of verification shows that the basic properties of the Avalon bus protocol were well kept and the potential flaws in design were not to arise in the multi-task system of Avalon bus.