6.2 用二叉判决图验证组合电路的等价性
6.2.2 用BDD验证组合电路的等价性
用BDD表示布尔函数是正则的，即对于给定的一个变量序，功能相同的两个布尔函数的BDD表示是同构的。这个性质在组合电路的等价性验证中十分重要，也是等价性验证的基本依据。
1. 验证策略