Academic
Publications
Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive Invariants

Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive Invariants,10.1007/11513988_19,Roope Kaivola

Formal Verification of Pentium® 4 Components with Symbolic Simulation and Inductive Invariants   (Citations: 6)
BibTex | RIS | RefWorks Download
We describe a practical methodology for large-scale formal verification of control-intensive industrial circuits. It combines symbolic simulation with human-generated inductive invariants, and a proof tool for verifying implications between constraint lists. The approach has emerged from extensive experiences in the formal verification of key parts of the Intel IA-32 Pentium ® 4 microprocessor designs. We discuss it the context of two case studies: Pentium 4 register renaming mechanism and BUS recycle logic.
Conference: Computer Aided Verification - CAV , pp. 170-184, 2005
Cumulative Annual
View Publication
The following links allow you to view full publications. These links are maintained by other sources not affiliated with Microsoft Academic Search.
Sort by: