We discuss lessons learned during a verification case study involving the PCI 2.1 protocol.

Motivated by our unsuccessful initial attempt to verify the property using theorem proving,

we defined an abstraction such that we could exhaustively check the property in about 60

seconds using a model checker. The abstraction used structural and data abstractions and

was shown to be safe using trace inclusion refinement. In this report we discuss the lessons

learned in applying theorem proving, then a combination of theorem proving and model

checking to the problem of verifying a large protocol defined over branching networks.

We hope that the lessons learned here will be useful to other members of the verification

community.