Deriving Structural RT-Implementations from Algorithmic Descriptions by means of Logical Transformations.
Christian Blumenröhr, Dirk Eisenbiegler · 1998
This paper presents a formal synthesis approach where the mapping of an algorithmic description towards its structural implementation at the RT-level is performed by means of basic logical transformations in a higher order logic theorem prover. The approach goes beyond pure basic blocks and allows representing and synthesizing arbitrary computable programs. A functional style is used for representing algorithms based on basic µ-recursive operators whose semantics is defined within higher order logic.