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

摘要

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