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

Sequential Equivalence Verification Combining Relational Modeling with Term Rewriting Technique

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

A novel framework for sequential equivalence verification was proposed, which combines relational modeling with term rewriting efficiently. In this approach, sequential designs were modeled with Kleene algebra with tests as relational expressions. Equivalence verification was then performed by rewriting these relational expressions. Compared with traditional equivalence verification methods based on state space traversal, the proposed approach provides a new thought for sequential equivalence verification.