Taylor Expansion Diagrams: A Compact Canonical Representation for RTL Verification

这项工作的目标是开发一种新的规范表示和高效的验证基础设施，以支持大型设计的RTL验证。所提出的基于图的表示被称为泰勒展开图，其基于不同于BDDS和BMDS等决策图所使用的分解原理。它是通过将设计的符号表达式视为连续的、可微的函数，并对其字级变量进行泰勒级数展开而得到的。由此得到的泰勒展开图(TED)对于固定的变量顺序是规范的。TED可用于表示同时包含代数和布尔表达式的函数，便于使用算术运算符和布尔逻辑表示通常在RTL规范中遇到的复杂设计。我们正在构建一个以TED为中心的RTL验证基础设施，可用于验证RTL设计的功能等价性。基于这一新理论，我们正在开发用于构建和处理硬件描述语言设计的TED表示的系统算法技术。我们还在研究如何利用TED进行实现验证，即检查RTL规范与其逻辑门级实现之间的功能等价性。通过广泛的实验，必须评估TEDS在具有算术电路和布尔逻辑的现实设计中的适用性，并将TED的性能与BDDS和*BMD进行比较。该项目还具有重要的教育作用，在设计综合和验证的背景下，向学生传授现代设计表示法，从决策图到更抽象的词级数据结构。

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.