SHF: Small: Word-level Abstraction of Arithmetic Gate-level Circuits

随着集成电路复杂性的不断提高，硬件验证已经成为整个电子设计流程中的主导因素。尤其关键和具有挑战性的是对几乎每一种设计中存在的复杂算术组件的验证，从微处理器到医疗设备再到通信设备。与已经为其开发了有效的布尔方法的逻辑电路相比，算术硬件验证的困难在于需要分析的数据量和大小。需要开发基于比逻辑位更高的抽象级别的不同的数学模型来处理这种复杂性。这个项目通过开发从物理电路实现中抽象算术结构的新技术来解决这个问题。除了验证之外，从设计中提取更高级别的信息在硬件信任和安全应用程序中也很重要，在这些应用程序中，这些信息可用于分析设计以隔离恶意硬件。这项工作的成功实施将有助于开发最先进的电子设计自动化工具，并将提高设计生产率。该项目还将为这一技术领域的未来劳动力培养本科生、研究生和博士后。该项目将开发一种使用计算机代数方法从算术电路中提取高级信息的新方法。在这种方法中，电路元件，如逻辑门，在代数域被建模为伪布尔多项式。将多项式从电路输出重写到输入，可以提取嵌入在电路中的算术函数。在重写期间，检查中间伪布尔表达式以识别可能的算术结构。识别是使用一种新的“频谱分析”技术来完成的，该技术将多项式表达式与基本算术块的参考“频谱”进行匹配，例如乘法器、加法器和乘法和累加运算符。这种方法将从多项式表达式中提取词的成分，并从内部表达式中推理出词级结构。通过将逻辑和算术函数表示为伪布尔多项式，可以减轻基于布尔的方法中通常遇到的大小爆炸。

With an ever-increasing complexity of integrated circuits, hardware verification has become the dominating factor of the overall electronic design flow. Particularly critical and challenging is the verification of complex arithmetic components present in almost every design, from microprocessors to medical devices to a communication equipment. In contrast to logic circuits, for which effective Boolean methods have been developed, the difficulty of arithmetic hardware verification lies in the size and the amount of data that needs to be analyzed. Different mathematical models, based on higher abstraction level than logic bits need to be developed to deal with this complexity. This project addresses this problem by developing new techniques for abstracting arithmetic structures from physical circuit implementations. In addition to verification, abstracting higher-level information from a design is important in hardware trust and security applications, where it can be used to analyze the design to isolate malicious hardware. Successful implementation of this work will contribute to the development of the state-of-the-art tools for electronic design automation and will increase design productivity. The project will also train undergraduate and graduate students, postdocs for future workforce in this technical area.The project will develop a new method to abstract high-level information from arithmetic circuits using computer algebra approach. In this approach, circuit components, such as logic gates, are modeled in algebraic domain as pseudo-Boolean polynomials. Rewriting polynomials from circuit outputs to inputs makes it possible to extract arithmetic function embedded in the circuit. During the rewriting, the intermediate pseudo-Boolean expressions are examined in order to identify possible arithmetic structures. The identification is done using a novel "spectral analysis" technique, which matches the polynomial expressions against the reference "spectra" of basic arithmetic blocks, such as multipliers, adders, and multiply-and-accumulate operators. This approach will abstract word components from polynomial expressions to reason about the word-level structure from the internal expressions. By representing logic and arithmetic functions as pseudo-Boolean polynomials, it is possible to mitigate the size explosion typically encountered in Boolean based methods.