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, althoug...

Full description

Saved in:
Bibliographic Details
Main Authors: Grass, W., Mutz, M., Tiedemann, W.-D.
Format: Conference Proceeding
Language:English
Subjects:
Algorithm design and analysis
Computer science
Formal verification
Hardware
High level synthesis
Logic
Mathematics
Microwave integrated circuits
Registers
Timing
Online Access:Request full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.< >
DOI:10.1109/EURMIC.1994.390403