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.