國立虎尾科技大學 |

Word-level abstractions for sequential design verification using algebraic geometry.

Record Type:	Language materials, manuscript : Monograph/item
Title/Author:	Word-level abstractions for sequential design verification using algebraic geometry./
Author:	Sun, Xiaojun.
Description:	1 online resource (194 pages)
Notes:	Source: Dissertation Abstracts International, Volume: 78-10(E), Section: B.
Contained By:	Dissertation Abstracts International78-10B(E).
Subject:	Computer engineering. -
Online resource:	click for full text (PQDT)
ISBN:	9781369775198

Word-level abstractions for sequential design verification using algebraic geometry.
Sun, Xiaojun.

Word-level abstractions for sequential design verification using algebraic geometry. - 1 online resource (194 pages)

Source: Dissertation Abstracts International, Volume: 78-10(E), Section: B.

Thesis (Ph.D.)

Includes bibliographical references

Formal verification of hardware designs has become an essential component of the overall system design flow. The designs are generally modeled as finite state machines, on which property and equivalence checking problems are solved for verification. Reachability analysis forms the core of these techniques. However, increasing size and complexity of the circuits causes the state explosion problem. Abstraction is the key to tackling the scalability challenges.

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

Mode of access: World Wide Web

ISBN: 9781369775198Subjects--Topical Terms:

569006
Computer engineering.
Index Terms--Genre/Form:

554714
Electronic books.

Word-level abstractions for sequential design verification using algebraic geometry.
LDR:03397ntm a2200397Ki 4500 001 909743
005 20180426091045.5
006 m o u
007 cr mn||||a|a||
008 190606s2017 xx obm 000 0 eng d
020 $a 9781369775198
035 $a (MiAaPQ)AAI10265398
035 $a (MiAaPQ)utah:13772
035 $a AAI10265398
040 $a MiAaPQ $b eng $c MiAaPQ
099 $a TUL $f hyy $c available through World Wide Web
100 1 $a Sun, Xiaojun. $3 1180669
245 1 0 $a Word-level abstractions for sequential design verification using algebraic geometry.
264 0 $c 2017
300 $a 1 online resource (194 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: 78-10(E), Section: B.
500 $a Adviser: Priyank Kalla.
502 $a Thesis (Ph.D.) $c The University of Utah $d 2017.
504 $a Includes bibliographical references
520 $a Formal verification of hardware designs has become an essential component of the overall system design flow. The designs are generally modeled as finite state machines, on which property and equivalence checking problems are solved for verification. Reachability analysis forms the core of these techniques. However, increasing size and complexity of the circuits causes the state explosion problem. Abstraction is the key to tackling the scalability challenges.
520 $a This dissertation presents new techniques for word-level abstraction with applications in sequential design verification. By bundling together k bit-level state-variables into one word-level constraint expression, the state-space is construed as solutions (variety) to a set of polynomial constraints (ideal), modeled over the finite (Galois) field of 2.
520 $a k elements. Subsequently,techniques from algebraic geometry --- notably, Groebner basis theory and technology --- are researched to perform reachability analysis and verification of sequential circuits. This approach adds a "word-level dimension" to state-space abstraction and verification to make the process more efficient.
520 $a While algebraic geometry provides powerful abstraction and reasoning capabilities, the algorithms exhibit high computational complexity. In the dissertation, we show that by analyzing the constraints, it is possible to obtain more insights about the polynomial ideals, which can be exploited to overcome the complexity. Using our algorithm design and implementations, we demonstrate how to perform reachability analysis of finite-state machines purely at the word level. Using this concept, we perform scalable verification of sequential arithmetic circuits. As contemporary approaches make use of resolution proofs and unsatisfiable cores for state-space abstraction, we introduce the algebraic geometry analog of unsatisfiable cores, and present algorithms to extract and refine unsatisfiable cores of polynomial ideals. Experiments are performed to demonstrate the efficacy of our approaches.
533 $a Electronic reproduction. $b Ann Arbor, Mich. : $c ProQuest, $d 2018
538 $a Mode of access: World Wide Web
650 4 $a Computer engineering. $3 569006
650 4 $a Electrical engineering. $3 596380
650 4 $a Mathematics. $3 527692
655 7 $a Electronic books. $2 local $3 554714
690 $a 0464
690 $a 0544
690 $a 0405
710 2 $a ProQuest Information and Learning Co. $3 1178819
710 2 $a The University of Utah. $b Electrical and Computer Engineering. $3 1180670
773 0 $t Dissertation Abstracts International $g 78-10B(E).
856 4 0 $u http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=10265398 $z click for full text (PQDT)