Accelerating Formal Verification of Cache Coherence Protocols Using FPGAs
PHAST, a Pipelined Hardware Accelerated STate Checker, achieves a 50x speedup for explicit state model checking of Murφ models. PHAST is a reimplementation, to accommodate FPGA hardware, of the Murφ verifier developed at Stanford University. PHAST takes advantage of the flexible memory architecture and inherent concurrency provided by an FPGA to accelerate model checking. PHAST is currently implemented on an Alpha-Data board with a Xilinx Virtex 5 chip and 1 GB of DDR-II SDRAM connected to the host computer by a PCI-X bus. In designs such as PHAST, where the data is created and managed locally and the connection is not the bottleneck, FPGAs can yield very good acceleration. Using PHAST, we achieved a fifty times application speedup in actual running hardware compared to Murφ on an example of a counter. The same structure developed for this simple example can be reused for much more complex models. Our model of the DASH protocol is similar in size and complexity to models Intel uses to validate proposed features of future processors: state sizes between 1200 and 1800 bits and a transition relation with more than 100 rules. Preliminary analysis of the DASH model as verified by PHAST indicates that with a careful implementation, the speedup will stay constant. This paper focuses on the generic structure developed for a hardware implementation of model checking as well as the changes to Murφ to accommodate FPGA hardware. PHAST is the first complete implementation of model checking in FPGA hardware.
Software Implementation - Murφ
Phast's target models are of similar complexity to models of an Intel processor feature
Hardware Implementation - PHAST
PHAST is a pipelined hardware implementation of the Murφ verifier. States start in the Next State Generator, and stored in the Lookup Pending Queue while they are hashed and looked up in the hash table.
M. E. Fuess, M. Leeser, and T. Leonard, "An FPGA Implementation of Explicit State Model Checking". FCCM, 2008.