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

点击翻译按钮获取中文摘要

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.