Establishing PCI compliance using formal verification: A case study

A case study on the practical application of formal verification technique of symbolic model checking to the verification of PCI bus bridges is presented. The paper covers the practical aspects of formal verification and shows its efficiency in the verification of real designs. The process of modelling the environment is discussed and typical rules of a PCI bus bridge and the reusability of those rules from design to design is examined. Results of the process, including the number of bugs discovered and the effort required to discover bugs/prove a property are investigated.