Paper Info
Title
Symbolic Simulation with Approximate Values
Abstract
Symbolic methods such as model checking using binary decision diagrams (BDDs) have had limited success in verifying large designs because BDD sizes regularly exceed memory capacity. Symbolic simulation is a method that controls BDD size by allowing the user to specify the number of symbolic variables in a test. However, BDDs still may blow up when using symbolic simulation in large designs with a large number of symbolic variables. This paper describes techniques for limiting the size of the internal representation of values in symbolic simulation no matter how many symbolic variables are present. The basic idea is to use approximate values on internal nodes; an approximate value is one that consists of combinations of the values 0, 1, and X. If an internal node is known not to affect the functionality being tested, then the simulator can output a value of X for this node, reducing the amount of time and memory required to represent the value of this node. Our algorithm uses categorization of the symbolic input variables to determine which node values can be more approximate and which can be more exact.
Year
DOI
Venue
2000
10.1007/3-540-40922-X_29
FMCAD
Keywords
Field
DocType
internal representation,symbolic variable,symbolic simulation,symbolic method,node value,bdd size,internal node,symbolic input variable,approximate value,approximate values,large design,model checking
Symbolic simulation,Model checking,Computer science,Binary decision diagram,Symbolic computation,Theoretical computer science,Distributed computing,Discrete mathematics,Tree (data structure),Algorithm,Symbolic data analysis,Formal verification,Symbolic trajectory evaluation
Conference
Volume
ISSN
ISBN
1954
0302-9743
3-540-41219-0
Citations 
PageRank 
References 
14
0.77
14
Authors
3
Name
Order
Citations
PageRank
Chris Wilson1151.50
David L. Dill2126291293.07
Randal E. Bryant392041194.64