改进的时间帧展开的时序电路等价验证算法

A Modified Frame Expansion Based Sequential Equivalence Checking Algorithm

提出一种改进的基于时间帧展开的时序电路等价验证算法,其来源于模型检查中的基于数学归纳的验证算法,在使用并简化了SAT问题中不可满足子集提取过程后,将基本条件检查和归纳检查合并处理.为了能在时间帧展开过程中减少状态搜索空间,利用结构不动点技术并提出了准动态唯一状态约束等改进的方法.实验表明,随着时间帧的不断展开,文中算法运行时间的增长速度明显慢于基于数学归纳法的验证算法,其适合验证经过时序优化后的电路.

A new frame-expansion based sequential equivalence checking algorithm is proposed. It derives from the induction-based model checking algorithm, and merges the checking processes of base condition and induction condition using our simplified unsatisfiable core extraction in SAT problem. Furthermore, in order to reduce the state space searched during frame expansion, structural fixed-point technique is exploited, and quasi-dynamic unique state constraint is proposed. Experimental results show that during the expansion of circuit frames, the elapsed time of our method increases much slower than that of the induction based algorithm. The total elapsed time is also promising when verifying sequentially optimized circuits.