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.
