对两个输入电路进行等价性验证的具体做法是首先建立待验证电路的OBDD,然后检验它们是否相同。根据不同情况,可以采用两种策略来进行验证:
  策略1: 使用一个变量序分别建立两个待验证电路的整个OBDD,然后进行比较。相对而言,采用这种策略速度更快,但存储要求较大;它还有一个好处就是建立了电路的完整OBDD,因而其结果可以直接用于综合等其它目的。考虑到在绝大多数情况下,该策略能够在有限的时间和存储要求下完成验证,系统在缺省情况下采用该策略。
  策略2: 逐个建立并比较两个待验证电路的每个输出的OBDD,由于与每个输出有关的输入和逻辑单元相对较少,再加上在需要时,可以对不同的输出使用不同的变量序,因而采用这种策略的存储要求相对较小,可以验证更大的电路。这种策略的缺陷是所建立的OBDD不能用于其它目的。
  对于某些电路,如果不能验证整个电路的等价性,还可以使用策略2验证电路的某个或某些输出的等价性。
  对于有较多部分相同的电路,系统可以首先进行同构比较,发现并排除完全同构的部分,仅对不同构的部分进行验证。系统也可以对用户指定的部分电路进行验证。
  对电路的局部进行验证是通过对电路作下述处理来实现的:(1)把局部电路的输入改为电路的输入;(2)把局部电路的输出改为电路的输出;(3)忽略电路的其它部分。