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

Verification of sequential circuit design based on OBDD

作　　者：刘建元[1] 

机构地区：[1]西安邮电学院计算机科学系,陕西西安710061

出　　处：《陕西师范大学学报（自然科学版）》2002年第2期55-58,共4页Journal of Shaanxi Normal University：Natural Science Edition

基　　金：国家自然科学基金资助项目 (6 94 730 17)

摘　　要：依据有序二叉判定图 (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.

关 键 词：OBDD 时序电路 有序二叉判定图 分支时态逻辑 等价性检验 符号模型检验 布尔函数 电路设计 

分 类 号：TN791[电子电信—电路与系统]