Formal modeling and model checking analysis of the Wishbone System-on-Chip bus protocol

Abstract

The Wishbone System-on-Chip bus protocol, which is developed by the Silicore Corporation, in connection with its characteristics and complexity, it is verified by the model checking approach. Firstly, the communication model of IP cores is created, and a FSM modeling approach for the model is proposed. Secondly, the non-starvation and fairness properties are specified using the computation tree logic. Finally these properties are verified against the model with the help of the model checking tool SMV. The result shows that there is a bus starvation scenario which will be caused by the unfairness of arbiter. This research demonstrates that there are some flaws with the specification of Wishbone System-on-Chip bus protocol. It also reflects that the arbitration mechanism is prone to flaw and therefore the formal modeling and verification is necessary. © 2012 Springer-Verlag.