Formal Verification of Explicitly Parallel Microprocessors

摘要

This report contains a collection of the following papers: (1) Formal Verification of Explicitly Parallel Microprocessors, (2) Symbolic Simulation of Microprocessor Models using Type Classes in Haskell, (3) The Internet As A medium For Software Engineering Experiments, (4) Top level Refinement in Processor Verification, (5) On embedding a microarchitectural design language within Haskell, (6) Elementary Microarchitecture Algebra, (7) Recursive Function Definition over Coinductive Types, (8) DSL Implementation Using Staging and Mon ads, (9) Erasure for termination proofs.