带黑盒组合电路的等价性验证  

An Equivalence Checking Algorithm for Combinational Circuits

作　　者：王瑞[1] 岳园[2] 张自强[1] 

机构地区：[1]兰州大学信息科学与工程学院,兰州730000 [2]西北民族大学计算机科学与信息学院,兰州730000

出　　处：《微计算机信息》2008年第26期258-260,共3页Control & Automation

基　　金："973"项目(2004CB318000)"数学机械方法及其在信息技术中的应用"的资助。

摘　　要：为了在早期阶段发现电路设计错误,需要对包含未知部分的实现电路和规范电路进行等价性验证。本文提出了一种"分而治之"的方法,把电路划分成若干子电路,使用四值逻辑模拟技术对电路未知部分进行量化,然后对子电路的合取范式进行可满足性验证。这种方法增强了算法的错误检测能力,通过在ISCAS’85基准电路和10个简单组合电路上得到的两组实验数据表明了此算法的有效性和可行性。Using equivalence checking between implementation with Black Boxes and specification in order to find design errors in early design stages. In this article, according to the ＂divide and conquer＂ approach, a whole circuit is divided into several sub-circuits and unknown constraints using four valued logic simulation technique. The algorithm enhances the capability of detecting errors. We give a series of experimental results on the ISCAS＇85 benchmark circuits and 10 simple combinational circuits demonstrating the effectiveness and feasibility of the algorithm.

关 键 词：等价性验证 黑盒 逻辑锥 可满足性验证 

分 类 号：TP391[自动化与计算机技术—计算机应用技术]