Experience with Embedding Hardware Description Languages in HOL
- Richard J. Boulton ,
- Andy Gordon ,
- Michael J. C. Gordon ,
- John Harrison ,
- John Herbert ,
- John Van Tassel
Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience |
Published by North-Holland Publishing Co.
The semantics of hardware description languages can be represented in higher order logic. This provides a formal definition that is suitable for machine processing. Experiments are in progress at Cambridge to see whether this method can be the basis of practical tools based on the HOL theorem-proving assistant. Three languages are being investigated: ELLA, Silage and VHDL. The approaches taken for these languages are compared and current progress on building semantically-based theorem-proving tools is discussed.