Paper Info
Title
Modeling multi-rate DSP specification semantics for formal transformational design in HOL
Abstract
The CATHEDRAL Silicon Compilers synthesize hardware for DSP algorithms specified in Silage, a high level applicative language. In order to optimize the results of the silicon compilation in terms of chip-area and/or throughput, the user often massages the specification applying transformations to the Silage code. To guarantee that the transformations preserve the behavior of the specified algorithm, the formal semantics of the specification language had to be defined. The semantics has been used to prove in HOL the correctness of the transformations and to prove properties of the specification. We are currently building a system where a menu of useful andcorrectness preserving transformations will be available to the user. In this system the user could choose appropriate transformations from the menu taking advantage of his creativity and expertise to interactively guide the silicon compiler, without the risk of introducing inconsistencies. This article describes the formalmulti-rate semantics of a substantial subset of Silage and illustrates some formally verified transformations.
Year
DOI
Venue
1994
10.1007/BF01384234
Formal Methods in System Design
Keywords
Field
DocType
Semantics of specification languages,verifying and reasoning about programs,theorem proving,transformational design
Specification language,Operational semantics,Programming language,Silicon compiler,Computer science,Action semantics,Correctness,Theoretical computer science,Formal specification,Language Of Temporal Ordering Specification,Formal methods
Journal
Volume
Issue
ISSN
5
1-2
0925-9856
Citations 
PageRank 
References 
1
0.42
9
Authors
3
Name
Order
Citations
PageRank
Catia M. Angelo192.18
Luc Claesen2606.84
Hugo De Man32177257.77