基于布尔可满足性的逻辑电路等价性验证方法

Equivalence Verification Method for Logic Circuits Based on Boolean Satisfiability

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

This paper presents the equivalence verification method based on Boolean Satisfiability （SAT）to solve the equivalence of circuits under test. It extracts the circuit under test into a finite state machine （FSM）, and then builds a product machine of two finite state machines, which converts the problem of equivalence of two circuits into the one of the asserted product machine. This paper improved the Tseitin＇s transformation method, and used for translation the circuit-constrained problems into CNF （Conjunctive Normal Form）formulas. Its satisfiability is then handed over to the state-of-the-art solver zChaff to check. Testing of example circuits demonstrate the effectiveness of this approach.