Please use this identifier to cite or link to this item:
http://hdl.handle.net/11375/12555
Title: | A Formal Approach to Concurrent Error Detection in FPGA LUTs |
Authors: | Bergstra, Jameson P. |
Advisor: | Lawford, Mark Nicolici, Nicola |
Department: | Computing and Software |
Keywords: | SEUs;Error Detection;SAT solvers;Synthesis;Digital Circuits;Digital Circuits |
Publication Date: | Oct-2012 |
Abstract: | In this thesis we discuss a formal approach to the design of concurrent error detection (CED) logic in field-programmable gate arrays (FPGAs). Single event upsets (SEUs) occurring in look-up table (LUT) configuration bits are considered as the fault model. Our approach involves representing the LUT network of the design implemented in the FPGA with constraints to model the presence of SEUs as a boolean formula in conjunctive normal form. A quantified boolean formula (QBF) based approach to designing CED logic based on parity check codes is found to be infeasible for designs of a realistic size. It is shown that a satisfiability (SAT) solver can be used to find variable assignments that indicate which circuit outputs can be corrupted by upset events in the specified fault model. An algorithm is presented to automatically generate a parity check code, which will identify with one clock cycle detection latency a malfunction caused by an SEU. The resulting parity check logic can be verified using a SAT solver and it is shown to require fewer LUT resources than duplication for most circuits. |
URI: | http://hdl.handle.net/11375/12555 |
Identifier: | opendissertations/7431 8485 3344563 |
Appears in Collections: | Open Access Dissertations and Theses |
Files in This Item:
File | Size | Format | |
---|---|---|---|
fulltext.pdf | 457.58 kB | Adobe PDF | View/Open |
Items in MacSphere are protected by copyright, with all rights reserved, unless otherwise indicated.