Formal Verification of a Public-Domain DDR2 Controller Design

Using the Sun OpenSPARC DDR2 Memory Controller design that has been in the open-source public domain, this paper removes much of the mystery in a successful application of end-to-end formal verification on a memory controller design.