Experience with embedding hardware description languages in HOL

Richard Boulton, Andrew Gordon, Mike Gordon, John Harrison, John Herbert and John Van Tassel.

Proceedings of the IFIP TC10/WG 10.2 International Conference on Theorem Provers in Circuit Design: Theory, Practice and Experience, Nijmegen. North-Holland, IFIP Transactions A-10, pp. 129-156, 1993.

Abstract:

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.

PostScript

Bibtex entry:

@INPROCEEDINGS{boulton-tpcd,
        crossref        = "tpcd93",
        author          = "Richard Boulton and Andrew Gordon and
                           Mike Gordon and John Harrison and
                           John Herbert and John Van Tassel",
        title           = "Experience with embedding hardware description
                           languages in {HOL}",
        pages           = "129--156"}

@PROCEEDINGS{tpcd93,
        editor          = "Victoria Stavridou and Thomas F. Melham and
                           R. T. Boute",
        booktitle       = "Proceedings of the {IFIP} {TC10/WG 10.2}
                           International Conference on Theorem Provers in
                           Circuit Design: Theory, Practice and Experience",
        series          = "IFIP Transactions A: Computer Science and
                           Technology",
        volume          = "A-10",
        address         = "Nijmegen, The Netherlands",
        date            = "22--24 June 1993",
        year            = 1993,
        publisher       = "North-Holland"}