Modeling multi-rate DSP specification semantics for formal transformational design in HOL (Q1334899)

The authors describe the formal multi-rate semantics of a substantial subset of Silage which is a high-level applicative language for the specification of DSP algorithms. Specifications in Silage can be synthesized to hardware by the CATHEDRAL silicon compilers. Because of transformations to Silage code in order to optimize a specification it is necessary to guarantee that these transformations preserve the behaviour of the specified algorithm. First the paper concentrates on the exact definition of the semantics of the specification language. The correctness of the possible transformations is then proved in HOL, which is a proof generating system for higher-order logic. For these purposes the authors first describe the basic concepts of Silage to model time and period of digital signals. The most important elements of Silage are clearly illustrated by examples. In order to consistently map Silage programs into their meaning in the HOL logic the authors next describe the basic concepts of HOL and show how the time and signal concept of Silage is modelled in HOL. The interpretation of the semantics of Silage programs into the corresponding HOL terms is automatically performed by an ML program. It is an important aspect to prove the correctness of transformations during the specification of algorithms in order to preserve the behaviour of the description. From that point the paper deals with an interesting approach to avoid inconsistencies during optimization operations concerning chip-area or timing beaviour of a DSP algorithm.