Formal Verification of the PCI Local Bus: A Step Towards IP Core Based System-On-Chip Design Verification
Dong Wang · 1999
We describe a methodology for verifying system-on-chip designs. In our methodology, the problem of verifying system-on-chip designs is decomposed into three tasks. First, we verify, once and for all, the standard bus interconnecting IP Cores in the system. The next task is to verify the glue logic, which connects the IP Cores to the buses. Finally, using the verified bus protocols and the IP core designs, temporal properties about the complete system are deduced. To illustrate our methodology, we verify the PCI Local Bus, a widely used bus protocol in system-on-chip designs. We demonstrate various modeling and verification techniques for buses by modeling the PCI Local Bus with the symbolic model checker SMV. We have found two potential bugs in the PCI bus specification that await confirmation of the PCI Special Interest Group(PCI-SIG). Thesis Advisor: EDMUND M. CLARKE Title: FORE Systems Professor of Computer Science and Professor of Department of Electrical and Computer Engineering(C) Thesis Reader: Randal E. Bryant Title: President’s Professor of Computer Science with courtesy appointment in Electrical and Computer Engineering