| dc.contributor.author | Jabeen, Shaista | |
| dc.description.abstract | Real-time systems in safety-critical and mission-critical domains have stringent or hard timing constraints. The correctness of such systems is of prime importance to avoid any unacceptable consequences like a big financial loss or a human life loss. With dynamic performance demands and the system complexity, there is an increased difficulty to prove and verify the correctness of a real-time system design. There is a shifting trend of implementing the complex real-time systems using hardware based solutions instead of software based solutions. The interaction between multiple system components and functional behavior of individual modules needs to be checked for correctness not only functionally, but also with respect to the time. Field programmable gate arrays (FPGAs) are getting popular in a wide variety of safety-critical real- time system applications for last two decades. FPGAs have predictable timing behavior, low cost and they outperform over general purpose CPUs. In this dissertation, we present a new formal verification approach that addresses the functional and timing correctness attributes of FPGA-based designs in safety-critical real-time applications. Our technique is a refinement-based deductive verification technique, which tells what it means for a system at lower abstraction level to be equivalent to a system specification at a higher level. We used the notion of Well-Founded Simulation, which explains the reasoning for a single step transition of RTL design in FPGA implementation. Initially, the system specification is obtained as a timed transition model. The implementation circuit in FPGA is also modeled as a timed transition system. Stuttering phenomenon and rank are used to prove the safety and liveness properties of the system. We devised a set of proof obligation templates for functional and timing verification, respectively. The proof obligation templates were successfully applied to some case studies. The developed technique can be extended to the applications which employ network on chip in their design. | en_US |
| dc.publisher | North Dakota State University | en_US |
| dc.rights | NDSU Policy 190.6.2 | |
| dc.title | A Formal Verification Methodology for Real-time FPGA | en_US |
| dc.type | Dissertation | en_US |
| dc.type | Video | en_US |
| dc.date.accessioned | 2017-10-24T14:03:52Z | |
| dc.date.available | 2017-10-24T14:03:52Z | |
| dc.date.issued | 2017 | |
| dc.identifier.uri | https://hdl.handle.net/10365/26685 | |
| dc.title.alternative | A Formal Verification Methodology for Real-time Field Programmable Gate Array (FPGA) | en_US |
| dc.rights.uri | https://www.ndsu.edu/fileadmin/policy/190.pdf | |
| ndsu.degree | Doctor of Philosophy (PhD) | en_US |
| ndsu.college | Engineering | en_US |
| ndsu.department | Electrical and Computer Engineering | en_US |
| ndsu.program | Electrical and Computer Engineering | en_US |
| ndsu.advisor | Srinivasan, Sudarshan K. | |
