结合关系建模与项重写技术的时序电路等价验证

提出一个新颖的时序电路等价验证的方法框架。该方法有效地结合了关系建模和项重写技术。首先利用带有测试条件的Kleene关系代数建模时序设计,进而通过对关系表达式的项重写来证明时序设计的等价性。与传统的基于状态空间遍历的时序等价验证方法相比,该方法提供了一种全新的思路。

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

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

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

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

一种基于状态转换图的时序电路等价验证算法

提出一种基于状态转换图的时序电路等价验证算法。此算法通过验证两时序电路的状态转换图是否同构,得到两电路是否等价的信息。若两状态转换图同构,则两图中的状态可一一匹配为等价状态对,算法将状态转换图存储为待验证等价状态对的形式,若所有待验证等价状态对均为等价,则两时序电路等价,反之,则不等价。此算法对ISCAS89测试电路进行验证,与基于BDD方法的SIS系统和基于时间帧展开算法相比,均有较好的结果。