数字电路设计中的符号模型检验技术  

Symbolic Model Checking for Digital Circuit Design

作　　者：刘建元[1] 

机构地区：[1]西安邮电学院,西安710061

出　　处：《微电子学与计算机》2002年第10期11-12,16,共3页Microelectronics & Computer

基　　金：国家自然科学基金(69473017)

摘　　要：符号模型检验把有序二叉判定图OBDD技术引入到模型检验中,有效地缓解了状态组合爆炸问题。文章主要介绍了CTL模型检验基本概念和原理,给出了符号模型检验算法,验证了模4计数器的某些特性。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.

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

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