Mechanical Approach to Linking Operational Semantics and Algebraic Semantics for Verilog Using Maude

Huibiao Zhu, Peng Liu, Jifeng He, Shengchao Qin

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    Abstract

    Verilog is a hardware description language (HDL) that has been standardized and widely used in industry. It contains interesting features such as event-driven computation and shared-variable concurrency. This paper considers how the algebraic semantics links with the operational semantics for Verilog. Our approach is to apply the equational and rewriting logic system Maude in exploring the linking theories. Firstly we present the algebraic semantics for Verilog. We introduce the concept of head normal form and every program is expressed as a guarded choice with location status. Secondly we present the strategy of deriving operational semantics from algebraic semantics. Our mechanical approach using Maude can visually show the head normal form of each program, as well as the execution steps of a program based on the derivation strategy. Finally we also mechanize the derived operational semantics. The results mechanized from the second and third exploration indicate that the transition system of the derived operational semantics is the same as the one based on the derivation strategy.
    Original languageEnglish
    Title of host publicationUnifying Theories of Programming, 4th International Symposium, UTP 2012, Paris, France, August 27-28, 2012, Revised Selected Papers
    EditorsB. Wolff, M. C. Gaudel, A. Feliachi
    PublisherSpringer Berlin
    Pages164-185
    ISBN (Electronic)9783642357053
    ISBN (Print)9783642357046
    DOIs
    Publication statusPublished - 2012
    EventUnifying Theories of Programming, 4th International Symposium - Paris, France
    Duration: 27 Aug 201228 Aug 2012
    Conference number: 4

    Publication series

    NameNotes in Computer Science
    PublisherSpringer, Berlin
    Volume7681

    Conference

    ConferenceUnifying Theories of Programming, 4th International Symposium
    Abbreviated titleUTP 2012
    CountryFrance
    CityParis
    Period27/08/1228/08/12

    Fingerprint Dive into the research topics of 'Mechanical Approach to Linking Operational Semantics and Algebraic Semantics for Verilog Using Maude'. Together they form a unique fingerprint.

  • Cite this

    Zhu, H., Liu, P., He, J., & Qin, S. (2012). Mechanical Approach to Linking Operational Semantics and Algebraic Semantics for Verilog Using Maude. In B. Wolff, M. C. Gaudel, & A. Feliachi (Eds.), Unifying Theories of Programming, 4th International Symposium, UTP 2012, Paris, France, August 27-28, 2012, Revised Selected Papers (pp. 164-185). (Notes in Computer Science; Vol. 7681). Springer Berlin. https://doi.org/10.1007/978-3-642-35705-3_8