High level synthesis based on formal methods

High-level synthesis, the task of automatically transforming behavioural descriptions at the algorithmic level into register transfer level structures, is conquered today almost always by use of heuristics. This prevents giving a guarantee either for the design optimality or the correctness, although these are the most essential criteria. By applying formal methods, both issues can be formally proven. This paper presents 3 aspects of HLS, that have been solved using formal methods, namely (1) the formal verification that those hardware modules allocated to realize a particular RT level operation are actually doing so with respect to functionality and timing, (2) an exact solution of the scheduling problem that is yet able to cope with more practical constraints than any heuristical procedure currently known and (3) the formally based synthesis of communication-dominated hardware, an important application area that is largely unnoticed by today´s HLS systems