模型检验中迁移关系的分组策略  

Strategy to Group Partitioned Transition Relationship in Model Checking

作　　者：邵明[1] 李光辉[1] 李晓维[2] 

机构地区：[1]中国科学院计算技术研究所信息网络研究室 [2]浙江林学院信息系,杭州311300

出　　处：《计算机辅助设计与图形学学报》2003年第9期1101-1104,共4页Journal of Computer-Aided Design & Computer Graphics

基　　金：国家自然科学基金重点项目 ( 90 2 0 70 0 2 );北京市科技重点项目(H0 2 0 12 0 12 0 13 0 )资助

摘　　要：迁移关系的构建是基于BDD模型检验中的一个重要环节 ,而建立占内存尽可能小且运算高效的迁移关系一直是难点 ,通常做法是对迁移关系进行分割 提出一种的对按位分割后的迁移关系进行分组的方法 通过对IS CAS 89中时序电路的试验表明 。In BDD-based model checking, it is a critical step to build a small and efficient transition relationship. An effective method is to partition it according to the bit of future state. The author proposed a strategy to group the partitioned transition relationship. The experiment conducted on the benchmark of ISCAS89 exhibits that our method is more effective under certain conditions.

关 键 词：集成电路 设计 模型检验 迁移关系 分组策略 BDD模型 

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