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!
cited_by cdi_FETCH-LOGICAL-c218t-7d7819668b12d4028b623a8cab1b4e79f84c7f4fabfdcb5ac2ea1ac1db466ba53
cites
container_end_page 126
container_issue
container_start_page 119
container_title
container_volume
creator Fuess, M.E.
Leeser, M.
Leonard, T.
description 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_str_mv 10.1109/FCCM.2008.36
format conference_proceeding
fullrecord <record><control><sourceid>ieee_6IE</sourceid><recordid>TN_cdi_ieee_primary_4724895</recordid><sourceformat>XML</sourceformat><sourcesystem>PC</sourcesystem><ieee_id>4724895</ieee_id><sourcerecordid>4724895</sourcerecordid><originalsourceid>FETCH-LOGICAL-c218t-7d7819668b12d4028b623a8cab1b4e79f84c7f4fabfdcb5ac2ea1ac1db466ba53</originalsourceid><addsrcrecordid>eNotj8tKw0AYRgekoK3duXMzL5A4t8xlGUJTCy0Kresyl390NDeaLPTtjdSz-eAsPjgIPVCSU0rMU11Vh5wRonMub9CSKGkKzonSC7T804ZpxuktWo_jJ5nhRqhC3iFVdrh-3ZZ41w4NtNBNdkp9h_uIN99Dk3yasuPsAB_6AA2uPsB_pe79Hi2ibUZY_-8KvdWbU_Wc7V-2u6rcZ55RPWUqKE2NlNpRFgRh2knGrfbWUSdAmaiFV1FE62LwrrCegaXW0-CElM4WfIUer78JAM7DJbX28nMWigk9B_4CYkZFRg</addsrcrecordid><sourcetype>Publisher</sourcetype><iscdi>true</iscdi><recordtype>conference_proceeding</recordtype></control><display><type>conference_proceeding</type><title>An FPGA Implementation of Explicit-State Model Checking</title><source>IEEE Electronic Library (IEL) Conference Proceedings</source><creator>Fuess, M.E. ; Leeser, M. ; Leonard, T.</creator><creatorcontrib>Fuess, M.E. ; Leeser, M. ; Leonard, T.</creatorcontrib><description>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.</description><identifier>ISBN: 0769533078</identifier><identifier>ISBN: 9780769533070</identifier><identifier>DOI: 10.1109/FCCM.2008.36</identifier><identifier>LCCN: 2008928231</identifier><language>eng</language><publisher>IEEE</publisher><subject>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</subject><ispartof>2008 16th International Symposium on Field-Programmable Custom Computing Machines, 2008, p.119-126</ispartof><woscitedreferencessubscribed>false</woscitedreferencessubscribed><citedby>FETCH-LOGICAL-c218t-7d7819668b12d4028b623a8cab1b4e79f84c7f4fabfdcb5ac2ea1ac1db466ba53</citedby></display><links><openurl>$$Topenurl_article</openurl><openurlfulltext>$$Topenurlfull_article</openurlfulltext><thumbnail>$$Tsyndetics_thumb_exl</thumbnail><linktohtml>$$Uhttps://ieeexplore.ieee.org/document/4724895$$EHTML$$P50$$Gieee$$H</linktohtml><link.rule.ids>309,310,780,784,789,790,2058,27925,54920</link.rule.ids><linktorsrc>$$Uhttps://ieeexplore.ieee.org/document/4724895$$EView_record_in_IEEE$$FView_record_in_$$GIEEE</linktorsrc></links><search><creatorcontrib>Fuess, M.E.</creatorcontrib><creatorcontrib>Leeser, M.</creatorcontrib><creatorcontrib>Leonard, T.</creatorcontrib><title>An FPGA Implementation of Explicit-State Model Checking</title><title>2008 16th International Symposium on Field-Programmable Custom Computing Machines</title><addtitle>FCCM</addtitle><description>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.</description><subject>Acceleration</subject><subject>Design methodology</subject><subject>explicit-state</subject><subject>Field programmable gate arrays</subject><subject>Formal verification</subject><subject>fpga</subject><subject>Hardware</subject><subject>hash compaction</subject><subject>model checking</subject><subject>murphi</subject><subject>phast</subject><subject>Process design</subject><subject>Protocols</subject><subject>Safety</subject><subject>State-space methods</subject><subject>Testing</subject><isbn>0769533078</isbn><isbn>9780769533070</isbn><fulltext>true</fulltext><rsrctype>conference_proceeding</rsrctype><creationdate>2008</creationdate><recordtype>conference_proceeding</recordtype><sourceid>6IE</sourceid><recordid>eNotj8tKw0AYRgekoK3duXMzL5A4t8xlGUJTCy0Kresyl390NDeaLPTtjdSz-eAsPjgIPVCSU0rMU11Vh5wRonMub9CSKGkKzonSC7T804ZpxuktWo_jJ5nhRqhC3iFVdrh-3ZZ41w4NtNBNdkp9h_uIN99Dk3yasuPsAB_6AA2uPsB_pe79Hi2ibUZY_-8KvdWbU_Wc7V-2u6rcZ55RPWUqKE2NlNpRFgRh2knGrfbWUSdAmaiFV1FE62LwrrCegaXW0-CElM4WfIUer78JAM7DJbX28nMWigk9B_4CYkZFRg</recordid><startdate>200804</startdate><enddate>200804</enddate><creator>Fuess, M.E.</creator><creator>Leeser, M.</creator><creator>Leonard, T.</creator><general>IEEE</general><scope>6IE</scope><scope>6IL</scope><scope>CBEJK</scope><scope>RIE</scope><scope>RIL</scope></search><sort><creationdate>200804</creationdate><title>An FPGA Implementation of Explicit-State Model Checking</title><author>Fuess, M.E. ; Leeser, M. ; Leonard, T.</author></sort><facets><frbrtype>5</frbrtype><frbrgroupid>cdi_FETCH-LOGICAL-c218t-7d7819668b12d4028b623a8cab1b4e79f84c7f4fabfdcb5ac2ea1ac1db466ba53</frbrgroupid><rsrctype>conference_proceedings</rsrctype><prefilter>conference_proceedings</prefilter><language>eng</language><creationdate>2008</creationdate><topic>Acceleration</topic><topic>Design methodology</topic><topic>explicit-state</topic><topic>Field programmable gate arrays</topic><topic>Formal verification</topic><topic>fpga</topic><topic>Hardware</topic><topic>hash compaction</topic><topic>model checking</topic><topic>murphi</topic><topic>phast</topic><topic>Process design</topic><topic>Protocols</topic><topic>Safety</topic><topic>State-space methods</topic><topic>Testing</topic><toplevel>online_resources</toplevel><creatorcontrib>Fuess, M.E.</creatorcontrib><creatorcontrib>Leeser, M.</creatorcontrib><creatorcontrib>Leonard, T.</creatorcontrib><collection>IEEE Electronic Library (IEL) Conference Proceedings</collection><collection>IEEE Proceedings Order Plan All Online (POP All Online) 1998-present by volume</collection><collection>IEEE Xplore All Conference Proceedings</collection><collection>IEEE Xplore</collection><collection>IEEE Proceedings Order Plans (POP All) 1998-Present</collection></facets><delivery><delcategory>Remote Search Resource</delcategory><fulltext>fulltext_linktorsrc</fulltext></delivery><addata><au>Fuess, M.E.</au><au>Leeser, M.</au><au>Leonard, T.</au><format>book</format><genre>proceeding</genre><ristype>CONF</ristype><atitle>An FPGA Implementation of Explicit-State Model Checking</atitle><btitle>2008 16th International Symposium on Field-Programmable Custom Computing Machines</btitle><stitle>FCCM</stitle><date>2008-04</date><risdate>2008</risdate><spage>119</spage><epage>126</epage><pages>119-126</pages><isbn>0769533078</isbn><isbn>9780769533070</isbn><abstract>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.</abstract><pub>IEEE</pub><doi>10.1109/FCCM.2008.36</doi><tpages>8</tpages></addata></record>
fulltext fulltext_linktorsrc
identifier ISBN: 0769533078
ispartof 2008 16th International Symposium on Field-Programmable Custom Computing Machines, 2008, p.119-126
issn
language eng
recordid cdi_ieee_primary_4724895
source IEEE Electronic Library (IEL) Conference Proceedings
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
title An FPGA Implementation of Explicit-State Model Checking
url http://sfxeu10.hosted.exlibrisgroup.com/loughborough?ctx_ver=Z39.88-2004&ctx_enc=info:ofi/enc:UTF-8&ctx_tim=2024-12-27T01%3A46%3A17IST&url_ver=Z39.88-2004&url_ctx_fmt=infofi/fmt:kev:mtx:ctx&rfr_id=info:sid/primo.exlibrisgroup.com:primo3-Article-ieee_6IE&rft_val_fmt=info:ofi/fmt:kev:mtx:book&rft.genre=proceeding&rft.atitle=An%20FPGA%20Implementation%20of%20Explicit-State%20Model%20Checking&rft.btitle=2008%2016th%20International%20Symposium%20on%20Field-Programmable%20Custom%20Computing%20Machines&rft.au=Fuess,%20M.E.&rft.date=2008-04&rft.spage=119&rft.epage=126&rft.pages=119-126&rft.isbn=0769533078&rft.isbn_list=9780769533070&rft_id=info:doi/10.1109/FCCM.2008.36&rft_dat=%3Cieee_6IE%3E4724895%3C/ieee_6IE%3E%3Cgrp_id%3Ecdi_FETCH-LOGICAL-c218t-7d7819668b12d4028b623a8cab1b4e79f84c7f4fabfdcb5ac2ea1ac1db466ba53%3C/grp_id%3E%3Coa%3E%3C/oa%3E%3Curl%3E%3C/url%3E&rft_id=info:oai/&rft_id=info:pmid/&rft_ieee_id=4724895&rfr_iscdi=true