Verifying IP-core based system-on-chip designs

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, the complete system is verified. 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 protocol specification that await confirmation of the PCI Special Interest Group (PCI-SIG)