A Formal Framework for High Level Synthesis of Digital Designs
Khaled M. Elleithy, Magdy Bayoumi · 1990
The major drawback of reported high level synthesis techniques is their limited applicability to a specific class of algoriehms without extendibility to general algorithms and the lack of a formal approach to prove the correctness of the such techniques. In this paper, we introduce a novel approach for high level synthesis from p-recursive alg+ rithms. Two features are provided by the approach: com-pleteness and correctness. Completeness means the ability to use the approach for any general algorithm. Correctness is achieved by using a set of transformations that are proved to be correct. A formal framework for the synthesis procedure has been developed which can be easily automated. A given algorithm will be represented in a new developed language termed Algorithm Specification Language (ASL). ASL has the ability to describe any gen-eral algorithm. An automatic procedure is used to transform an ASL representation into a specific realization specification using a correctness preserving set of transfor-mations. The realization format is based on representing the digital architectures by a Realization Specification Language(RSL). 1.