Verified high-level synthesis
Richard Chapman · 1994
We show that it is feasible to verify parts of a high-level synthesis system by giving semantics to the representation languages used and showing that the algorithms produce designs with meanings that refine their specifications. Previous efforts attempting to relate hardware verification techniques and high-level synthesis have concentrated on showing that the individual designs produced by synthesis systems are correct, usually in a post hoc manner. The BEDROC synthesis system translates a behavioral specification written in a Pascal-like language to an implementation in field-programmable gate-arrays. We give operational and denotational models to BEDROC's specification language, HardwarePal, and show that they are equivalent. BEDROC first translates the specification into a dependence flow graph (dfg), via an algorithm we devised. We have found the dependence flow graph, originally developed for use in parallelizing compilers, to be a good intermediate form for optimization and scheduling of hardware. We have extended the operational semantics of dependence flow graphs to describe hardware, and shown that the algorithms used to build and optimize the dependence flow graph are correct. We use the dfg as a basis for scheduling. We show that the schedule derived from the dfg is correct. Lower levels of BEDROC, developed by other members of the BEDROC project, do data path allocation, boolean optimization, translation to Xilinx netlist format, placement, and routing. As an example, we examine the 5th order wave digital elliptic filter from the High Level Synthesis Workshop benchmark set, for which a design was synthesized using BEDROC. We examine the role played by the parts of the system discussed here. We believe that this work gives evidence that the design of high level synthesis systems can benefit from the use of formal methods. No performance penalty need be paid, either. As designs grow increasingly complex, the value of a guarantee of correctness for the systems output can only increase.