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 protoco...

Full description

Saved in:
Bibliographic Details
Main Authors: Fuess, M.E., Leeser, M., Leonard, T.
Format: Conference Proceeding
Language:English
Subjects:
Acceleration
Design methodology
explicit-state
Field programmable gate arrays
Formal verification
fpga
Hardware
hash compaction
model checking
murphi
phast
Process design
Protocols
Safety
State-space methods
Testing
Citations: Items that cite this one
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
DOI:10.1109/FCCM.2008.36