Collaborative Research: SHF: Medium: Automated Word Level Synthesis for Hardware Code Generation and Verified Abstraction

合作研究：SHF：Medium：用于硬件代码生成和验证抽象的自动字级合成

• 批准号: 2106949
• 负责人: Grigory Fedyukovich
• 金额: $ 44.99万
• 依托单位: Florida State University
• 依托单位国家: 美国
• 项目类别: Standard Grant
• 财政年份: 2021
• 资助国家: 美国
• 起止时间: 2021-07-15 至 2025-06-30
• 项目状态: 未结题
• 来源: https://www.nsf.gov/awardsearch/showAward?AWD_ID=2106949&HistoricalAwards=false
• 关键词: Collaborative; Research; SHF; Medium; Automated

The success of formal methods has enabled widespread applications in ensuring correctness, safety, and reliability of computing systems. This project on automated word-level synthesis is providing a core utility for diverse applications since the bit-vector representation of various computing systems is well-suited for both hardware designs and low-level software. By virtue of the underlying formal reasoning, the programs synthesized by the automated methods are guaranteed to be correct-by-construction, thus improving their quality and improving developer productivity. The two application domains targeted in this project – computer networks and systems-on-chips – form core components of the computing infrastructure that provides numerous products and services of interest to society. The research activities involve training and mentoring graduate students, and development of teaching material.Real-world applications that require bit-precise reasoning for synthesis and verification, such as in the domains of computer networks and hardware, remain challenging in terms of performance and scalability. One main reason is that existing techniques for synthesis over bitvectors rely largely on a translation of multi-bit words down to bits, called bit-blasting, which destroys the high-level structure in the application programs. This project aims to improve automated synthesis of word-level bit-precise programs, with applications in network packet processing and verification of systems-on-chip (SoCs). The core research activities include development of a new approach to word-level synthesis. The synthesizer is guided by word-level quantifier elimination over bit-vectors without bit-blasting. It also leverages the well-known framework of Syntax-Guided Synthesis (SyGuS), where the search for a program is guided by domain knowledge captured in the form of context-free grammars, program sketches, and partial specifications comprising input-output examples. The project develops suitable grammars and synthesis methods in two application domains: (1) synthesis of code for programmable network switches from high-level packet processing programs, and (2) synthesis of verified architecture-level abstractions from hardware designs of accelerators and processors in modern SoCs. These improve techniques for code generation (from high-level to low-level programs) and verified abstraction (from low-level to high-level programs), respectively.This award reflects NSF's statutory mission and has been deemed worthy of support through evaluation using the Foundation's intellectual merit and broader impacts review criteria.

形式化方法的成功使得在确保计算系统的正确性、安全性和可靠性方面得到了广泛的应用，这个关于自动字级合成的项目为各种应用提供了核心实用程序，因为各种计算系统的位向量表示是很好的。适用于硬件设计和低级软件。凭借底层的形式推理，自动化方法合成的程序可以保证构建正确，从而提高其质量并提高开发人员的工作效率。在这个项目中——计算机网络和片上系统– 形成计算基础设施的核心组件，提供社会感兴趣的众多产品和服务。研究活动包括培训和指导研究生以及开发教材。需要位精确推理来进行合成和验证的实际应用，例如在计算机网络和硬件领域，在性能和可扩展性方面仍然具有挑战性，一个主要原因是现有的位向量合成技术很大程度上依赖于将多位字转换为位，称为位爆破。破坏了高层结构该项目旨在改进字级位精度程序的自动合成，以及在网络数据包处理和片上系统（SoC）验证中的应用。该合成器通过位向量上的字级量词消除来指导，而无需位爆破，它还利用了众所周知的语法引导合成（SyGuS）框架，其中指导了程序的搜索。通过以上下文无关语法、程序草图和包括输入输出示例的部分规范的形式捕获的领域知识，该项目在两个应用领域开发合适的语法和综合方法：（1）从高级可编程网络交换机的代码综合。级数据包处理程序，以及 (2) 从现代 SoC 中的加速器和处理器的硬件设计中综合经过验证的架构级抽象。该奖项反映了 NSF 的法定使命，并通过使用基金会的智力价值和更广泛的影响审查标准进行评估，被认为值得支持。