基于模块的层次化模型判别  

Hierarchical Model Checking Based on Modules

作　　者：聂江波[1] 边计年[1] 薛宏熙[1] 吴为民[1] 朱明[1] 

机构地区：[1]清华大学计算机科学与技术系,北京100084

出　　处：《微电子学与计算机》2003年第12期64-67,共4页Microelectronics & Computer

基　　金：国家自然科学基金项目(90207017;60203011);国家973重点基础研究发展规划(G1998030403)

摘　　要：模型判别技术是验证时序电路的一种重要手段。使用高层次描述的电路设计,往往是由多个相互关联的部分组成,利用此特点,本文提出一种基于模块的层次化建模方法,通过对设计描述进行分析,并结合待验证的性质,达到提高模型判别器性能的目的。实验表明,用这种模型可以实现状态数的有效减少。As an important method to verify sequence circuit, model checking first transform the design implementation to Finite State Machine, and then search the state space to check if the specification is satisfied. In fact, the design implement described in high-level language always consists of many interrelated modules. According to this property, an approach to generate a hierarchical model based on modules is proposed in which the design implementation and the specification are both analyzed before building the FSMs. Experiments show that this method can reduce the number of the states effectively.

关 键 词：集成电路 设计 模块 层次化模型 模型判别 有限自动机 

分 类 号：TN402[电子电信—微电子学与固体电子学]