| 数字电路设计中的符号模型检验技术 |
| |
| 引用本文： | 刘建元. 数字电路设计中的符号模型检验技术[J]. 微电子学与计算机, 2002, 19(10): 11-12,16 |
| |
| 作者姓名： | 刘建元 |
| |
| 作者单位： | 西安邮电学院,西安,710061 |
| |
| 基金项目： | 国家自然科学基金(69473017) |
| |
| 摘 要： | 符号模型检验把有序二叉判定图OBDD技术引入到模型检验中，有效地缓解了状态组合爆炸问题。文章主要介绍了CTL模型检验基本概念和原理，给出了符号模型检验算法，验证了模4计数器的某些特性。
|
| 关 键 词： | 数字电路设计 有序二叉判定图 分支时态逻辑 模型检验 符号模型检验 OBDD |
Symbolic Model Checking for Digital Circuit Design |
| |
| LIU Jian yuan. Symbolic Model Checking for Digital Circuit Design[J]. Microelectronics & Computer, 2002, 19(10): 11-12,16 |
| |
| Authors: | LIU Jian yuan |
| |
| Abstract: | Model checking is a main aspect of formal verification. Symbolic model checking is an approach to avoid the combination state explosion in model checking using OBDD. This paper mainly introduces the basic conception and principle of CTL model checking. The arithmetic of symbolic model checking is given. Some of the features of the model four counter are verified. |
| |
| Keywords: | Ordered binary decision diagram Computational tree logic Model checking Symbolic model checking |
| 本文献已被 CNKI 维普 万方数据 等数据库收录！ |
