Please use this identifier to cite or link to this item:
http://hdl.handle.net/11375/11188
Full metadata record
DC Field | Value | Language |
---|---|---|
dc.contributor.advisor | Lawford, Mark | en_US |
dc.contributor.author | Deng, Honghan | en_US |
dc.date.accessioned | 2014-06-18T16:53:51Z | - |
dc.date.available | 2014-06-18T16:53:51Z | - |
dc.date.created | 2011-09-15 | en_US |
dc.date.issued | 2011-10 | en_US |
dc.identifier.other | opendissertations/6175 | en_US |
dc.identifier.other | 7188 | en_US |
dc.identifier.other | 2240955 | en_US |
dc.identifier.uri | http://hdl.handle.net/11375/11188 | - |
dc.description.abstract | <p>In design verication, although simulation is still a widely used verication</p> <p>technique in FPGA design, formal verication is obtaining greater acceptance</p> <p>as the complexity of designs increases. In the simulation method, for a circuit</p> <p>with n inputs and m registers an exhaustive test vector will have as many as</p> <p>2<sup>(m+n)</sup> elements making it impractical for many modern circuits. Therefore</p> <p>this method is incomplete, i.e., it may fail to catch some design errors due to</p> <p>the lack of complete test coverage. Formal verication can be introduced as a</p> <p>complement to traditional verication techniques.</p> <p>The primary objectives of this thesis are determining: (i) how to for-</p> <p>malize FPGA implementations at dierent levels of abstraction, and (ii) how</p> <p>to prove their functional correctness. This thesis explores two variations of a</p> <p>formal verication framework by proving the functional correctness of several</p> <p>FPGA implementations of commonly used safety subsystem components us-</p> <p>ing the theorem prover PVS. We formalize components at the netlist level and</p> <p>the Verilog Register Transfer HDL level, preserving their functional semantics.</p> <p>Based on these formal models, we prove correctness conditions for the com-</p> <p>ponents using PVS. Finally, we present some techniques which can facilitate</p> <p>the proving process and describe some general strategies which can be used to</p> <p>prove properties of a synchronous circuit design.</p> | en_US |
dc.subject | Formal method | en_US |
dc.subject | PVS | en_US |
dc.subject | Hardware verification | en_US |
dc.subject | FPGA | en_US |
dc.subject | HDL. | en_US |
dc.subject | Digital Circuits | en_US |
dc.subject | Hardware Systems | en_US |
dc.subject | Other Computer Engineering | en_US |
dc.subject | Digital Circuits | en_US |
dc.title | Formal Verification of FPGA Based Systems | en_US |
dc.type | thesis | en_US |
dc.contributor.department | Software Engineering | en_US |
dc.description.degree | Master of Applied Science (MASc) | en_US |
Appears in Collections: | Open Access Dissertations and Theses |
Files in This Item:
File | Size | Format | |
---|---|---|---|
fulltext.pdf | 4.03 MB | Adobe PDF | View/Open |
Items in MacSphere are protected by copyright, with all rights reserved, unless otherwise indicated.