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

Sequential Equivalence Verification Combining Relational Modeling with Term Rewriting Technique

作　　者：杨志[1] 马光胜[1] 刘晓晓 

机构地区：[1]哈尔滨工程大学计算机科学与技术学院,哈尔滨150001

出　　处：《微电子学》2009年第2期259-262,共4页Microelectronics

基　　金：国家自然科学基金资助项目"基于多项式符号代数的系统芯片DA新方法研究"(60273081)

摘　　要：提出一个新颖的时序电路等价验证的方法框架。该方法有效地结合了关系建模和项重写技术。首先利用带有测试条件的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.

关 键 词：时序等价验证 关系建模 项重写 形式验证 

分 类 号：TP391.7[自动化与计算机技术—计算机应用技术]