Abstract: With the advent and popularity of multi-core architecture, on-chip bus (OCB) is gradually becoming the bottleneck of the functionality and performance of the system on chip (SoC). Consequently, the formal verification of OCB turns to be a significant aspect of SoC design. As a key formal verification technique, model checking performs an exhaustive procedure to automatically examine behaviors of SoC and determine if the specifications are satisfied by it. Nevertheless, model checking suffers from state space explosion problem while the expressive power of the existing specification languages such as computation tree logic (CTL) and linear temporal logic (LTL) is limited. This paper presents a propositional projection temporal logic (PPTL) based symbolic model checking approach for WISHBONE on-chip bus. With this approach, the WISHBONE bus designed in Verilog hardware description language (HDL) is transformed to system model described in SMV input language of NuSMV model checker, while the desired property is expressed in a PPTL formula. Then whether the system model satisfies the property or not can be determined with PLSMC, a PPTL symbolic model checking tool proposed in our previous work. The experiment results show that this approach can be applied to the verification of qualitative properties, as well as quantitative properties such as iteration and time duration for WISHBONE on-chip bus.