Title :
The formal definition of a synchronous hardware-description language in higher order logic
Author :
Gordon, Andrew D.
Author_Institution :
Comput. Lab., Cambridge Univ., UK
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 :
formal verification; parallel languages; specification languages; theorem proving; SILAGE; data-flow language; digital signal processing circuits; formal definition; hardware verification; higher order logic; predictive semantics; secure transformational design; synchronous hardware-description language; theorem proving; Algorithm design and analysis; Circuit synthesis; Digital signal processing; Hardware design languages; High level synthesis; Laboratories; Logic; Signal design; Signal processing algorithms; Signal synthesis;
Conference_Titel :
Computer Design: VLSI in Computers and Processors, 1992. ICCD '92. Proceedings, IEEE 1992 International Conference on
Conference_Location :
Cambridge, MA
Print_ISBN :
0-8186-3110-4
DOI :
10.1109/ICCD.1992.276230
