The Formal Definition of a Synchronous Hardware-Description Language in Higher Order Logic

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.