Verified high-level synthesis front-end and simulator using dependence flow graphs
Ntsibane Stephen Ntlatlapa, Richard Chapman · 1999
We present a high-level synthesis methodology for efficient, formally verified tools to support translation of a design specification written in behavioral VHDL to dependence flow graphs. Dependence flow graphs are an intermediate form developed initially for parallelizing, optimizing compiler, but which are well suited for high-level synthesis. The verification is based on providing structural operational semantics for behavioral VHDL and showing that the translations carried out by the system preserve the semantics of the initial VHDL specification. To facilitate the verification process we present the structural operational semantics of synthesis-oriented behavioral VHDL and structural operational semantics of dependence flow graphs. This work is part of the project to develop formally verified high-level synthesis system that produce a register-transfer-level design from a behavioral specification, with very little or no user intervention. The verification process described here can be applied other parts of the system to produce a fully verified system. We discuss our implementation of the front-end, optimizer and behavioral simulator components of the proposed high-level synthesis system. The simulator represents the behavior described dependence flow graphs in structural VHDL. Finally, we discuss our implementation of the dependence flow graphs in graph modeling language, GML.