Nonlinear quantification scheduling in image computation
Nonlinear quantification scheduling in image computation
复制标题
图像计算中的非线性量化调度
DOI：
10.1109/iccad.2001.968636
复制
发表时间：
2001
期刊：
影响因子：
--
通讯作者：
Dong Wang
中科院分区：
文献类型：
--
作者：
P. Chauhan;E. Clarke;S. Jha;J. Kukula;T. Shiple;H. Veith;Dong Wang
从给定的状态集计算一步可达的状态集，即图像计算，是许多符号验证算法的关键步骤，包括模型检查和可达性分析。到目前为止，图像计算中量化调度的最佳方法都局限于线性调度，并带有一个合划分的转移关系。这将导致在图像计算过程中失去灵活性。我们将图像计算看作是为图像集构造最优解析树的问题。解析树的最优性由树计算过程中遇到的最大BDD定义。我们提出了一个新算法的动态和静态版本，VarScore，它利用了解析树方法为图像计算提供的灵活性。我们通过大量的实验表明，我们的技术优于迄今为止最著名的技术。
Computing the set of states reachable in one step from a given set of states, i.e. image computation, is a crucial step in several symbolic verification algorithms, including model checking and reachability analysis. So far, the best methods for quantification scheduling in image computation, with a conjunctively partitioned transition relation, have been restricted to a linear schedule. This results in a loss of flexibility during image computation. We view image computation as a problem of constructing an optimal parse tree for the image set. The optimality of a parse tree is defined by the largest BDD that is encountered during the computation of the tree. We present dynamic and static versions of a new algorithm, VarScore, which exploits the flexibility offered by the parse tree approach to the image computation. We show by extensive experimentation that our techniques outperform the best known techniques so far.