Symbolic Simulation with Approximate Values
Symbolic Simulation with Approximate Values
复制标题
具有近似值的符号模拟
DOI：
10.1007/3-540-40922-x_29
复制
发表时间：
2000
期刊：
影响因子：
--
通讯作者：
R. Bryant
中科院分区：
文献类型：
--
作者：
Chris Wilson;D. Dill;R. Bryant
使用二元决策图 (BDD) 进行模型检查等符号方法在验证大型设计方面取得的成功有限，因为 BDD 大小经常超出内存容量。符号模拟是一种通过允许用户指定测试中符号变量的数量来控制 BDD 大小的方法。然而，在具有大量符号变量的大型设计中使用符号仿真时，BDD 仍然可能会崩溃。本文描述了限制符号模拟中值的内部表示大小的技术，无论存在多少符号变量。基本思想是在内部节点上使用近似值；近似值是由值 0、1 和 X 的组合组成的值。如果已知内部节点不会影响正在测试的功能，则模拟器可以为该节点输出 X 值，从而减少表示该节点值所需的时间和内存量。我们的算法使用符号输入变量的分类来确定哪些节点值可以更近似，哪些节点值可以更精确。
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.