本文提出了一种结合二叉判决图BDD和布尔可满足性SAT的新颖组合电路等价性验证技术 .算法是在与 /非图AIG中进行推理 ,并交替使用BDD扩展和基于电路SAT解算器简化电路 .如尚未解决 ,将用基于合取范式SAT解算器进行推理 .与已有算法相比主要有如下改进 :在AIG中结合多种引擎进行简化 ,不存在误判可能 ;充分利用了基于电路解算器和基于合取范式解算器各自优点 ,减小了SAT推理的搜索空间 .实验结果表明了本算法的有效性 .
科研之友
微信
新浪微博
Facebook
分享链接
