Portal de Periódicos da CAPES

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

2005; Springer Science+Business Media; Linguagem: Inglês

10.1007/11513988_19

1611-3349

Roope Kaivola,

Model-Driven Software Engineering Techniques

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.