| 基于OBDD时序电路设计的验证 |
| |
| 引用本文： | 刘建元.基于OBDD时序电路设计的验证[J].陕西师范大学学报,2002,30(2):55-58. |
| |
| 作者姓名： | 刘建元 |
| |
| 作者单位： | 西安邮电学院计算机科学系 陕西西安710061 |
| |
| 基金项目： | 国家自然科学基金资助项目 (6 94 730 17) |
| |
| 摘 要： | 依据有序二叉判定图（OBDD）和计算树逻辑（或称分支时态逻辑）CTL（Computational Tree Logic)的基本原理，分析了基于OBDD和CTL的验证数据电路设计的基本原理，并在此基础上，给出了时序电路等价验证的方法。
|
| 关 键 词： | OBDD 时序电路 有序二叉判定图 分支时态逻辑 等价性检验 符号模型检验 布尔函数 电路设计 |
| 文章编号： | 1001-3857(2002)02-0055-04 |
| 修稿时间： | 2001年10月10 |
Verification of sequential circuit design based on OBDD |
| |
| LIU Jian,yuan.Verification of sequential circuit design based on OBDD[J].Journal of Shaanxi Normal University: Nat Sci Ed,2002,30(2):55-58. |
| |
| Authors: | LIU Jian yuan |
| |
| Abstract: | 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. |
| |
| Keywords: | ordered binary decision diagram computational tree logic equivalence checking symbolic model checking |
| 本文献已被 CNKI 维普 等数据库收录！ |
