西安电子科技大学学报（自然科学版）
西安電子科技大學學報（自然科學版）
서안전자과기대학학보（자연과학판）
JOURNAL OF XIDIAN UNIVERSITY(NATURAL SCIENCE)
2009年
5期
877-884
,共8页
组合电路%等价性检验%电路推理%与非图
組閤電路%等價性檢驗%電路推理%與非圖
조합전로%등개성검험%전로추리%여비도
大部分基于SAT的组合电路等价性检验方法是将两个待检验的电路组合成一个miter电路,将这个电路变换成CNF形式,然后调用一个SAT判定器来确定这个CNF是否是可满足的.但是,当miter电路被变换成CNF之后,就丢掉了电路的结构信息.针对这种方法的不足,先假定miter的输出为1,然后从miter的输出端开始,回溯检查是否存在冲突来判定miter的可满足性.利用AIG的特点,把每个节点的四种输入组合归结为一种,从而使推理得到了简化.实验表明,此方法有更快的处理速度.
大部分基于SAT的組閤電路等價性檢驗方法是將兩箇待檢驗的電路組閤成一箇miter電路,將這箇電路變換成CNF形式,然後調用一箇SAT判定器來確定這箇CNF是否是可滿足的.但是,噹miter電路被變換成CNF之後,就丟掉瞭電路的結構信息.針對這種方法的不足,先假定miter的輸齣為1,然後從miter的輸齣耑開始,迴溯檢查是否存在遲突來判定miter的可滿足性.利用AIG的特點,把每箇節點的四種輸入組閤歸結為一種,從而使推理得到瞭簡化.實驗錶明,此方法有更快的處理速度.
대부분기우SAT적조합전로등개성검험방법시장량개대검험적전로조합성일개miter전로,장저개전로변환성CNF형식,연후조용일개SAT판정기래학정저개CNF시부시가만족적.단시,당miter전로피변환성CNF지후,취주도료전로적결구신식.침대저충방법적불족,선가정miter적수출위1,연후종miter적수출단개시,회소검사시부존재충돌래판정miter적가만족성.이용AIG적특점,파매개절점적사충수입조합귀결위일충,종이사추리득도료간화.실험표명,차방법유경쾌적처리속도.
