利用状态缓存的时序等价性验证算法  

Sequential Equivalence Checking Algorithm Using States Caching

作　　者：杨军[1] 翁延龄[1] 葛海通[1] 严晓浪[1] 

机构地区：[1]浙江大学超大规模集成电路设计研究所,杭州310027

出　　处：《计算机辅助设计与图形学学报》2008年第2期149-154,共6页Journal of Computer-Aided Design & Computer Graphics

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

摘　　要：为了提高时序电路的等价性验证速度,提出一种改进的基于寄存器匹配的验证算法.除了利用原像计算避免误判之外,该算法还将可达状态和不可达状态引入到验证过程中.将仿真过程中从初始状态可以到达的状态记录为可达状态,将验证过程中确认不能从初始状态到达的状态记录为不可达状态,利用它们减少验证过程中的原像计算.基于mcnc91电路的实验数据表明,该算法有效地减少了验证时间.An improved algorithm based on register mapping is proposed to increase the speed of equivalence checking for sequential circuits. It not only used pre-image computation to avoid false negative, but also incorporated reachable states and unreachable states in the verification process. States that can be reached from the initial state in simulation are collected as reachable states, states that cannot be reached from the initial state in verification are collected as unreachable states, they are used to reduce pre-image computation. Experimental results based on mcncgl show that the algorithm can reduce verification time efficiently.

关 键 词：时序等价性验证 寄存器匹配 原像计算 可达状态 不可达状态 

分 类 号：TP302[自动化与计算机技术—计算机系统结构]