Compositional verification: an industrial case study

We illustrate a compositional verification methodology using an industrial case study. In compositional verification, a user decomposes a system into blocks and derive system correctness based on block verification. We describe the verification of a PCI-Express Endpoint Controller design. Our experience shows that compositional techniques reduce verification complexity and allow users to find errors early in the design process.