用布尔可满足性验证逻辑电路的等价性

提出了使用布尔可满足性来验证数字电路的等价性验证方法.这一验证方法把每个电路抽象成一个有限状态机,为两个待验证的电路构造积机,把等价性验证问题转换成了积机的断言问题.改进了Tseitin变换方法,用于把电路约束问题变换成合取范式公式.用先进的布尔可满足性求解器zChaff判定积机所生成的布尔公式的可满足性.事例电路验证说明了该方法的有效性.

Verifying Equivalence of Logic Circuits with Boolean Satisfiability

This paper presents the equivalence verification method of digital circuits by means of Boolean Satisfiability(SAT).It first extracts the circuit under test into a finite state machine(FSM),and then builds a product machine of two finite state machines,which transforms the problem of equivalence of two circuits into the one of the asserted product machine.The Tseitin's transformation method is improved and is used for converting the circuit constrained problems to CNF(Conjunctive Normal Form) formulas.Its satisfiability is then handed over to the state-of-the-art solver Chaff to check.The testing of example circuits demonstrates the effectiveness of this approach.