以对电路的一个输出的验证为例，假设两个电路的该输出的OBDD分别为obdd1、obdd2，形式验证部分的算法伪代码描述如下：
　　　　{
　　　　生成两个电路的二叉判决图obdd1,obdd2。
　　　　if (obdd1 == obdd2)
　　　　报告两个电路相等；
　　　　else {
　　　　　　　obdd3 = obdd1 XOR obdd2; //obdd3即两个电路的不一致的地方。
　　　　if (输入了不管项信息) {
　　　　　　　生成不管项部分的OBDD表达式obdd4;
　　　　　　　if (obdd4包含obdd3)
　　　　　　　　两个电路的不同部分属于不管项，可以忽略；
　　　　　　　else {
　　　　　　　　　　temp_obdd1 = obdd1 OR obdd4;
　　　　　　　　　　temp_obdd2 = obdd2 OR obdd4;
　　　　　　　　　　obdd3 = temp_obdd1 XOR temp_obdd2;
　　　　　　　　　　}
　　　　　　　}
　　　　输出使obdd3为真的向量；/*即导致两个电路功能不同的向量*/
　　　　}

　　验证两个逻辑电路等价，只要比较两个OBDD是否一致即可。如果电路中包括了不管项，则要对两个电路中的不同部分（用obdd3表示）中包含于不管项OBDD的部分（用obdd3表示）去除，剩余的就是真正不同部分，报告错误。