Formal verification of high-level conformance with symbolic simulation

We describe a practical methodology for large-scale full formal validation of industrial circuits. The approach targets conformance of register-transfer level circuit descriptions with abstract high-level models. It is supported by a proof tool that combines symbolic simulation with human-generated inductive invariants. The approach has emerged from extensive experiences in the validation of key parts of Intel IA-32 microprocessor designs, and it has allowed us to completely verify feedback-intensive circuits beyond the capabilities of most other tools. We discuss the methodology the context of two case studies: a register file bypass network and a cache invalidation protocol.