论文部分内容阅读
提出了基于布尔可满足性（Boolean Satisfiability，SAT）的逻辑电路等价性验证方法。这一验证方法把每个电路抽象成一个有穷自动机（FSM），为两个待验证的电路构造积机，把等价性验证问题转换成了积机的断言判定问题。改进了Tseitin变换方法，并将其用于把电路约束问题变换成（Conjunctive Normal Form，CNF）公式。之后到用先进的CNFSAT求解器zChaff判定积机所生成的布尔公式的可满足性。事例电路验证说明了该方法的有效性。