基于OBDD时序电路设计的验证

Verification of sequential circuit design based on OBDD

依据有序二叉判定图 (OBDD)和计算树逻辑 (或称分支时态逻辑 )CTL(ComputationalTreeLogic)的基本原理 ,分析了基于OBDD和CTL的验证数字电路设计的基本原理 ,并在此基础上 。

Ordered binary decision diagram is a data structure of Boolean function canonical representation. OBDD can be used to check some properties of Boolean function such as satisfy ability, equivalence, etc. This paper introduces the basic conception of OBDD and CTL, mainly the principle based on OBDD and CTL of verification of digital design. The method of sequential circuits equivalence checking is given.