Taylor Expansion Diagrams: A Compact Canonical Representation for RTL Verification

泰勒展开图：RTL 验证的紧凑规范表示

• 批准号: 0204146
• 负责人: Maciej Ciesielski
• 金额: $ 28万
• 依托单位: University of Massachusetts Amherst
• 依托单位国家: 美国
• 项目类别: Continuing Grant
• 财政年份: 2002
• 资助国家: 美国
• 起止时间: 2002-07-01 至 2006-06-30
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=0204146&HistoricalAwards=false
• 关键词: Taylor; Expansion; Diagrams; Compact; Canonical

The goal of this work is to develop a new canonical representation and an efficient verification infrastructure to support the RTL verification of large designs. The proposed graph-based representation, called Taylor Expansion Diagram, is based on a different decomposition principle than used by decisiondiagrams such as BDDs and BMDs. It is obtained by treating the symbolic expression of the design as a continuous, differentiable function and applying Taylor series expansion with respect to its word-level variables. The resulting Taylor Expansion Diagram (TED) is canonical for a fixed ordering of variables. TEDs can be used to represent functions containing both algebraic and Boolean expressions, facilitating the representation of complex designs with arithmetic operators and Boolean logic, typically encountered in RTL specifications. We are building an RTL verification infrastructure centered around TED that can be used to verify functional equivalence of RTL designs. We are developing systematic, algorithmic techniques for constructing and manipulating TED representations of HDL designs, based on the new theory.We are also investigating how to exploit TEDs for implementation verification, that is checking functional equivalence between an RTL specification and its logic, gate-level implementation. By carrying out extensive experiments, the applicability of TEDs to realistic designs with arithmetic circuits and Boolean logic must be evaluated, and the performance of TEDs compared against that of BDDs and *BMDs.This project has also an important educational role of teaching students about modern design representations from decision diagrams to more abstract, word-level data structures in the context of design synthesis and verification.

这项工作的目的是开发新的规范表示和有效的验证基础架构，以支持大型设计的RTL验证。所提出的基于图的表示，称为Taylor扩展图，基于与BDD和BMD等决策图所使用的分解原理不同。通过将设计的符号表达视为连续的，可区分的函数，并针对其单词级别的变量应用了泰勒级数的扩展。所得的泰勒膨胀图（TED）对于变量的固定顺序是规范。 TED可以用来表示包含代数和布尔表达式的功能，从而促进使用算术运算符和布尔逻辑的复杂设计的表示，通常在RTL规范中遇到。我们正在建立一个以TED为中心的RTL验证基础架构，该基础架构可用于验证RTL设计的功能等效性。 我们正在开发基于新理论的HDL设计的系统，算法技术，用于构建和操纵HDL设计的TED表示。我们还正在研究如何利用TED进行实施验证，这正在检查RTL规范及其逻辑，门级实现之间的功能等效性。 通过进行广泛的实验，必须评估TED在具有算术电路和布尔逻辑的现实设计上的适用性，并且TEDS与BDDS和 *BMDS的表现相比，TEDS的表现也具有与BDDS和 *BMDS的相比。该项目还具有教学学生的重要教育作用，从而将学生从决策图到更摘要，文字级别，级别的数据结构的现代设计表示形式进行了教学。