Establishing PCI compliance using formal verification: a case study

This paper presents a case study in the practical application of formal verification. Specifically, we describe our experience in applying the formal verification technique of symbolic model checking to the verification of PCI bus bridges. During the last 2 years, we have used symbolic model checking to verify more than 12 hardware designs, including a number of PCI bus bridges. This use of formal verification has led to the better understanding of formal verification capabilities and the establishment of formal verification techniques as a standard verification tool in the Haifa Design Group at IBM´s Haifa Research Laboratory. More than 5 PCI bus bridge designs have been verified using formal verification, including a design in which formal verification was used to do all checks at the unit level. A PCI bus bridge design that was verified with formal verification was announced as an IBM product and became available to customers after a single tape-out