The formal definition of a synchronous hardware-description language in higher order logic
- 2 January 2003
- conference paper
- conference paper
- Published by Institute of Electrical and Electronics Engineers (IEEE)
- p. 531-534
- https://doi.org/10.1109/iccd.1992.276230
Abstract
If formal methods of hardware verification are to have any impact on the practices of working designers, connections must be made between the languages used in practice to design circuits and those used for research into hardware verification. SILAGE is a simple data-flow language used for specifying digital signal processing circuits. Higher-order logic (HOL) is extensively used for research into hardware verification. A novel combination of operational and predictive semantics is used to define formally a substantial subset of SILAGE by mapping SILAGE definitions into HOL predicates. The authors sketch the method used, discuss what is gained by a formal definition, and explain an immediate practical application: secure transformational design of SILAGE circuits as theorem proving in HOL.<>Keywords
This publication has 9 references indexed in Scilit:
- Correctness preserving transformations on the Hough algorithmPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2003
- Formal methods for silicon compilationPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- PHIDEO: a silicon compiler for high speed algorithmsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- How to prove the completeness of a set of register level design transformationsPublished by Institute of Electrical and Electronics Engineers (IEEE) ,2002
- Fast prototyping of datapath-intensive architecturesIEEE Design & Test of Computers, 1991
- Proof-aided design of verified hardwarePublished by Association for Computing Machinery (ACM) ,1991
- The high-level synthesis of digital systemsProceedings of the IEEE, 1990
- Cathedral-II: A Silicon Compiler for Digital Signal ProcessingIEEE Design & Test of Computers, 1986
- An Abstract Model of Behavior for Hardware DescriptionsIEEE Transactions on Computers, 1983