國立高雄大學圖資館 |

Language: English

Back

Automatic generation of invariants i...

Abu-Haimed, Husam Saad.

Automatic generation of invariants in formal verification of microprocessors and memory systems.

Record Type:	Electronic resources : Monograph/item
Title/Author:	Automatic generation of invariants in formal verification of microprocessors and memory systems.
Author:	Abu-Haimed, Husam Saad.
Description:	149 p.
Notes:	Adviser: David L. Dill.
Notes:	Source: Dissertation Abstracts International, Volume: 65-09, Section: B, page: 4656.
Contained By:	Dissertation Abstracts International65-09B.
Subject:	Computer Science.
Online resource:	http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3145447
ISBN:	0496043501

Automatic generation of invariants in formal verification of microprocessors and memory systems.
Abu-Haimed, Husam Saad.

Automatic generation of invariants in formal verification of microprocessors and memory systems. - 149 p.

Adviser: David L. Dill.

Thesis (Ph.D.)--Stanford University, 2004.

Finally, we introduce a sound and complete abstraction method that maps an infinite system to a finite system that can be verified with model checking techniques. This abstraction technique applies only to a certain class of systems what we characterize.

ISBN: 0496043501Subjects--Topical Terms:

212513
Computer Science.

Automatic generation of invariants in formal verification of microprocessors and memory systems.
LDR:03244nmm _2200325 _450 001 162848
005 20051017073529.5
008 090528s2004 eng d
020 $a 0496043501
035 $a 00149349
040 $a UnM $c UnM
100 0 $a Abu-Haimed, Husam Saad. $3 227993
245 1 0 $a Automatic generation of invariants in formal verification of microprocessors and memory systems.
300 $a 149 p.
500 $a Adviser: David L. Dill.
500 $a Source: Dissertation Abstracts International, Volume: 65-09, Section: B, page: 4656.
502 $a Thesis (Ph.D.)--Stanford University, 2004.
520 # $a Finally, we introduce a sound and complete abstraction method that maps an infinite system to a finite system that can be verified with model checking techniques. This abstraction technique applies only to a certain class of systems what we characterize.
520 # $a First, we propose a formulation of hardware correctness based on the idea of functional equivalence. We show how functional equivalence can be used to prove the correctness of microprocessors and memory systems and other kinds of hardware. Functional equivalence makes verifying systems such as microprocessors much easier than other approaches in the literature. Moreover, it is applicable to a much larger class of systems.
520 # $a Formal verification of complex hardware designs is a very challenging process especially for designs such as microprocessors due to their sheer complexity. The main difficulty in verifying such systems is in finding and strengthening invariants. In this thesis, we introduced several techniques to alleviate the problem of finding and strengthening invariants for such systems.
520 # $a Then, we introduce a method we call symbolic consistency testing that reduces the effort needed to generate inductive invariants. The method uses k-step induction to strengthen the property (functional equivalence) and relies on the user to find symbolic test vectors . These test vectors are used to eliminate existential quantifiers in the k-step induction using a technique we call predicate instantiation. We show how this method works successfully on a number of examples of cached memory systems.
520 # $a To further reduce the manual effort needed to verify such systems, we introduce a refinement heuristic that tries to automatically find the symbolic test vectors. The heuristic finds the required test vectors for all the examples we consider very quickly.
520 # $a We also introduced a semi-formal method that can be used with systems that are too complex for symbolic consistency testing. This is a debugging method that uses structural constraints within the system to remove incoherent states from the state space. This method is able to find all bugs in our examples and it is in general more efficient than symbolic consistency testing.
590 $a School code: 0212.
650 # 0 $a Computer Science. $3 212513
650 # 0 $a Engineering, Electronics and Electrical. $3 226981
690 $a 0544
690 $a 0984
710 0 # $a Stanford University. $3 212607
773 0 # $g 65-09B. $t Dissertation Abstracts International
790 $a 0212
790 1 0 $a Dill, David L., $e advisor
791 $a Ph.D.
792 $a 2004
856 4 0 $u http://libsw.nuk.edu.tw:81/login?url=http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3145447 $z http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3145447