國立高雄大學圖資館 |

Language: English

Back

Achieving scalable hardware verification with symbolic simulation.

Record Type:	Electronic resources : Monograph/item
Title/Author:	Achieving scalable hardware verification with symbolic simulation.
Author:	Bertacco, Valeria Maria.
Description:	165 p.
Notes:	Adviser: Kunle Olukotun.
Notes:	Source: Dissertation Abstracts International, Volume: 64-09, Section: B, page: 4515.
Contained By:	Dissertation Abstracts International64-09B.
Subject:	Engineering, Electronics and Electrical.
Online resource:	http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3104197
ISBN:	0496517651

Achieving scalable hardware verification with symbolic simulation.
Bertacco, Valeria Maria.

Achieving scalable hardware verification with symbolic simulation. [electronic resource] - 165 p.

Adviser: Kunle Olukotun.

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

Both of these techniques have been tested on the ISCAS and Logic Synthesis benchmark suites. The results show that the first technique can simulate very large trace sets in parallel, maintaining a simulation speed and memory profile that are much closer to logic simulation. The second technique is effective in reducing the memory requirements of symbolic simulation while preserving an exact state exploration.

ISBN: 0496517651Subjects--Topical Terms:

226981
Engineering, Electronics and Electrical.

Achieving scalable hardware verification with symbolic simulation.
LDR:03270nmm _2200289 _450 001 162163
005 20051017073417.5
008 230606s2003 eng d
020 $a 0496517651
035 $a 00148664
035 $a 162163
040 $a UnM $c UnM
100 0 $a Bertacco, Valeria Maria. $3 227279
245 1 0 $a Achieving scalable hardware verification with symbolic simulation. $h [electronic resource]
300 $a 165 p.
500 $a Adviser: Kunle Olukotun.
500 $a Source: Dissertation Abstracts International, Volume: 64-09, Section: B, page: 4515.
502 $a Thesis (Ph.D.)--Stanford University, 2003.
520 # $a Both of these techniques have been tested on the ISCAS and Logic Synthesis benchmark suites. The results show that the first technique can simulate very large trace sets in parallel, maintaining a simulation speed and memory profile that are much closer to logic simulation. The second technique is effective in reducing the memory requirements of symbolic simulation while preserving an exact state exploration.
520 # $a In recent years, the complexity of digital integrated circuit (IC) designs has grown at a challenging pace. Within this context, proper verification of an IC design has become a central aspect of the development cycle. Logic simulation is the accepted method for verification because of its scalability, although it can only visits a small fraction of the state space. Symbolic simulation is an alternative method that is attracting increasing interest because it can explore a major portion of the circuit's state space without the need of design-specific tests. The limiting factor to the mainstream deployment of this approach has been its complexity and unpredictable run-time behavior.
520 # $a This thesis presents two new symbolic simulation based approaches to the verification problem that radically improve scalability and narrow the performance gap between design complexity and verification. The first technique, Cycle-Based Symbolic Simulation, is a unique combination of formal methods and logic simulation to stimulate a circuit with a very large number of input combinations in parallel through the use of a parametric form. This approach maintains a high degree of scalability while achieving better efficiency than logic simulation.
520 # $a To better exploit the use of parameterization, Disjoint Support Decomposition Based Symbolic Simulation, our second technique, exploits the disjoint support decomposition (DSD) properties of the state functions. We develop a new algorithm that exposes the DSD of a Boolean function by restructuring its BDD representation. The new algorithm is very efficient in the sense that it has worst-case complexity that is only quadratic in the size of the initial BDD. We deployed this algorithm to find the DSD of the state functions in symbolic simulation, which we then use to generate a more compact, but exact, parametric form.
590 $a School code: 0212.
650 # 0 $a Engineering, Electronics and Electrical. $3 226981
650 # 0 $a Computer Science. $3 212513
710 0 # $a Stanford University. $3 212607
773 0 # $g 64-09B. $t Dissertation Abstracts International
790 $a 0212
790 1 0 $a Olukotun, Kunle, $e advisor
791 $a Ph.D.
792 $a 2003
856 4 0 $u http://libsw.nuk.edu.tw/login?url=http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3104197 $z http://pqdd.sinica.edu.tw/twdaoapp/servlet/advanced?query=3104197