Formal Verification of Microprocessors

Symbolic Simulation.- High-Level Modeling of Microprocessors.- Boolean Satisfiability Procedures.- Proving Safety of Pipelined Microprocessors by Exploiting Positive Equality.- Formal Verification of Pipelined Microprocessors with Exceptions, Branch Prediction, and Multicycle Functional Units.- Analysis of Counterexamples.- Formal Verification of Pipelined Microprocessors with Instruction Queues.- Formal Verification of Pipelined Microprocessors with Delayed Branches.- Formal Verification of Pipelined Microprocessors with Data Value Prediction.- Formal Verification of Binary Code Compatibility of Pipelined Microprocessors.- Using Positive Equality to Prove Liveness of Pipelined Microprocessors.- Proving Liveness for Pipelined Microprocessors with Multicycle Functional Units.- Formal Verification of a VLIW Processor Inspired by the Intel Itanium.- Formal Verification of an Out-of-Order Superscalar Processor Inspired by the PowerPC 750.- Translating Equational Logic to Boolean Formulas.- Applying Rewriting Rules to Automatically Abstract Memories.- Efficient Translation to CNF by Exploiting the Block-Level Structure of Boolean Formulas.- Exploiting Unobservability in Translation to SAT.- Efficient Use of Parallel Processor Environments for SAT Solving.- Putting the SAT Techniques All Together.