國立虎尾科技大學 |

A Formal Verification Methodology for Real-Time FPGA.

紀錄類型:	書目-語言資料,手稿 : Monograph/item
正題名/作者:	A Formal Verification Methodology for Real-Time FPGA./
作者:	Jabeen, Shaista.
面頁冊數:	1 online resource (104 pages)
附註:	Source: Dissertation Abstracts International, Volume: 79-02(E), Section: B.
Contained By:	Dissertation Abstracts International79-02B(E).
標題:	Electrical engineering. -
電子資源:	click for full text (PQDT)
ISBN:	9780355240078

A Formal Verification Methodology for Real-Time FPGA.
Jabeen, Shaista.

A Formal Verification Methodology for Real-Time FPGA. - 1 online resource (104 pages)

Source: Dissertation Abstracts International, Volume: 79-02(E), Section: B.

Thesis (Ph.D.)

Includes bibliographical references

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.

Electronic reproduction.
Ann Arbor, Mich. :
ProQuest,
2018

Mode of access: World Wide Web

ISBN: 9780355240078Subjects--Topical Terms:

596380
Electrical engineering.
Index Terms--Genre/Form:

554714
Electronic books.

A Formal Verification Methodology for Real-Time FPGA.
LDR:03356ntm a2200361Ki 4500 001 910817
005 20180517112611.5
006 m o u
007 cr mn||||a|a||
008 190606s2017 xx obm 000 0 eng d
020 $a 9780355240078
035 $a (MiAaPQ)AAI10617969
035 $a (MiAaPQ)ndsu:11841
035 $a AAI10617969
040 $a MiAaPQ $b eng $c MiAaPQ
099 $a TUL $f hyy $c available through World Wide Web
100 1 $a Jabeen, Shaista. $3 1182287
245 1 2 $a A Formal Verification Methodology for Real-Time FPGA.
264 0 $c 2017
300 $a 1 online resource (104 pages)
336 $a text $b txt $2 rdacontent
337 $a computer $b c $2 rdamedia
338 $a online resource $b cr $2 rdacarrier
500 $a Source: Dissertation Abstracts International, Volume: 79-02(E), Section: B.
500 $a Adviser: Sudarshan K. Srinivasan.
502 $a Thesis (Ph.D.) $c North Dakota State University $d 2017.
504 $a Includes bibliographical references
520 $a 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.
520 $a 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.
533 $a Electronic reproduction. $b Ann Arbor, Mich. : $c ProQuest, $d 2018
538 $a Mode of access: World Wide Web
650 4 $a Electrical engineering. $3 596380
650 4 $a Engineering. $3 561152
655 7 $a Electronic books. $2 local $3 554714
690 $a 0544
690 $a 0537
710 2 $a ProQuest Information and Learning Co. $3 1178819
710 2 $a North Dakota State University. $b Electrical and Computer Engineering. $3 1182288
773 0 $t Dissertation Abstracts International $g 79-02B(E).
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=10617969 $z click for full text (PQDT)