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.