Implementing Murf: Accelerating Large State Space Exploration on FPGAs

PHAST, a Pipelined Hardware Accelerated STate Checker, achieves a 30x end-to-end speedup of a large state space exploration application in the form of an explicit state model checker. PHAST is a re-implementation, to accommodate FPGA hardware, of the Murphi verifier developed at Stanford University. Explicit state model checking explores a large state space and checks properties defined by the user. The FPGA infrastructure for PHAST can be reused for many different models and properties. 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. Analysis of the DASH model as verified by PHAST indicates that the speedup will stay constant independent of the model being explored. The current implementation of PHAST, implemented on an Alpha-Data board with a Xilinx Virtex 5 and 1 GB of SDRAM, has the ability to explore up to 300,000 states in the DASH model. This model, with close to one hundred thousand states and 220 rules, takes up less than forty percent on the Virtex chip and less than thirty percent of the block RAMs. PHAST takes advantage of the flexible memory architecture and inherent concurrency provided by an FPGA to explore large state spaces. With access to more memory, PHAST could explore a much larger state space. This paper focuses on the generic structure developed for a hardware implementation of model checking as an example of accelerating large state space exploration. The main contributions in this paper lie in the hardware implementation specifics, including pipelining state generation to generate a new state every cycle and check that invariants, or safety properties, hold for all states; as well as efficiently implementing hash compaction and hash table lookups with a CAM for duplication detection and collision handling. The current implementation of PHAST uses a CAM to improve- the generated number of states by over 20,000. Large state space exploration is an application area particularly well suited to FPGA acceleration. State space exploration applications developed on GPUs have good results or small states, but none have managed to exhibit both characteristics.