论文部分内容阅读
提出一种基于排序二值判定图（OBDD）的符号模型检测中PRE 操作的改进算法。该算法处理PRE 步骤3（嵌套布尔存在量化）的方法是一次遍历“删除”所有被量化变量的节点,产生表示布尔函数与嵌套存在量化结果等价的不确定排序二值判定图,把不确定排序二值判定图转换成OBDD。实验表明,该算法能有效缩短计算时间,减少中间节点所需空间。