Stefano Basagni, Laurie Smith King
Date of Award
Master of Science
Department or Academic Unit
College of Engineering, Department of Electrical and Computer Engineering
computer engineering, breadth first search, formal verification, FPGA, model checking, Murphi, PHAST
Electrical and Computer Engineering | Engineering
Verification has become an increasingly important part of the hardware design process. One technique used to verify digital circuits is explicit state model checking. PHAST, a Pipelined Hardware Accelerated STate Checker, achieves a 30x speedup for explicit state model checking of Murphi models over software implementations used in industry. PHAST is a reimplementation, to accommodate FPGA hardware and to utilize SDRAM, of the Murphi verifier developed at Stanford University. Murphi has been used to verify hardware and protocols, cache coherency protocols particularly. Murphi is used in industry due to its success in finding real design errors. PHAST takes advantage of the flexible memory architecture and inherent concurrency provided by an FPGA to accelerate model checking. 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. The PHAST architecture can handle hundreds of transition relations and tens of thousands of states. Using PHAST, we achieved a thirty times application speedup in actual running hardware compared to Murphi on an example of a counter. The same structure developed for this simple example was also reused for a model of the DASH multiprocessor. The model of the DASH protocol is similar in size and complexity to models Intel uses to validate features of processors. Preliminary analysis of the DASH model as verified by PHAST indicates the speedup will stay constant across a large number of models. PHAST is the first complete implementation of model checking in FPGA hardware.
Mary Ellen Tie
Tie, Mary Ellen, "Accelerating explicit state model checking on an FPGA: PHAST" (2012). Electrical and Computer Engineering Master's Theses. Paper 82. http://hdl.handle.net/2047/d20002661
Click button above to open, or right-click to save.