High-level synthesis tools generate RTL designs from algorithmic behavioral specifications and consist of well defined tasks. Widely used algorithms for these tasks retain the overall control flow structure of the behavioral specification allowing limited code motion. Further, HLS algorithms are oblivious to the mathematical properties of arithmetic and logic operators, selecting and sharing RTL library modules solely based on matching uninterpreted function symbols and constants. This paper reports a verification methodology that effectively exploits these features to achieve efficient and fully automated verification of synthesized designs and its incorporation in a relatively mature HLS tool.
展开▼
