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

为了提高时序电路的等价性验证速度,提出一种改进的基于寄存器匹配的验证算法.除了利用原像计算避免误判之外,该算法还将可达状态和不可达状态引入到验证过程中.将仿真过程中从初始状态可以到达的状态记录为可达状态,将验证过程中确认不能从初始状态到达的状态记录为不可达状态,利用它们减少验证过程中的原像计算.基于mcnc91电路的实验数据表明,该算法有效地减少了验证时间.

Sequential Equivalence Checking Algorithm Using States Caching

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.