Presidential Young Investigator Award: Formal Verification of Hardware Synthesis Systems

该项目的目标是开发一种经过正式验证的 用于从硬件描述生成硬件描述的高级合成系统 并发程序 并发程序广泛用于指定 分布式系统，如通信网络。 然而，在这方面， 规范只是分布式系统设计一个方面。 实现该规范需要生成硬件， 软件组件，不幸的是，没有方法来 确保该实施是正确的。 现在用于硬件设计的主要验证工具是 仿真 仿真不能探索复杂系统的完整状态空间， 系统，因此没有给予足够的信心的行为 安全关键应用的正确性。 正式设计 为推理并发程序而开发的技术不 遭受这种“状态爆炸”问题;然而，没有现有的 合成系统可以从并发程序生成硬件，同时 保证行为特性得以保留。 这个项目 将开发必要的工具，以证明一个国家的最先进的高 水平合成程序是行为保持的。

The goal of this project is the development of a formally verified high level synthesis system for generating hardware descriptions from concurrent programs. Concurrent programs are widely used to specify distributed systems such as communication networks. However, specification is just one aspect of distributed system design. Implementing the specification requires generating hardware and software components and, unfortunately, no methodology exists for ensuring that this implementation is correct. The primary verification tool now used in hardware design is simulation. Simulation cannot explore the full state space of complex systems and hence does not give sufficient confidence of behavioral correctness for safety critical applications. The formal design techniques developed for reasoning about concurrent programs do not suffer from this "state explosion" problem; however, no existing synthesis system can generate hardware from a concurrent program while guaranteeing that behavioral properties are preserved. This project will develop the tools necessary to prove that a state-of-the-art high level synthesis program is behavior preserving.