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

SHF：小：算术门级电路的字级抽象

• 批准号: 1617708
• 负责人: Maciej Ciesielski
• 金额: $ 45万
• 依托单位: University of Massachusetts Amherst
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2016
• 资助国家: 美国
• 起止时间: 2016-06-15 至 2020-12-31
• 项目状态: 已结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=1617708&HistoricalAwards=false
• 关键词: SHF; Small; Word; level; Abstraction

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.

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