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

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

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.