An FPGA Implementation of Explicit-State Model Checking

We present PHAST, a pipelined hardware accelerated explicit-state model checker. The algorithms and methodologies used to perform the state checking in PHAST are based on the Mur¿ verifier, developed at Stanford University. Mur¿ has been used to verify hardware and protocols, cache coherency protocols in particular. Mur¿ is used in industry due to its success in finding errors in real designs. Until now, Mur¿ and other model checkers have been solely performed in software. PHAST takes advantage of the flexible memory architecture on FPGA chips and the inherent concurrency available in hardware designs to accelerate model checking. Using PHAST in simulation, we achieved over 200× application speedup over Mur¿ on an example of a counter.