A monadic approach to automated reasoning for Bluespec SystemVerilog

Dominic Richards, David Lester

    Research output: Contribution to journalLetterpeer-review

    Abstract

    We embed a non-trivial subset of Bluespec SystemVerilog (BSV) in the higher order logic of the PVS theorem prover. Owing to the clean semantics of BSV, application of monadic techniques leads to a surprisingly elegant embedding, in which hardware designs are translated into logic almost verbatim, preserving types and language constructs. The resulting specifications are compatible with the built-in model checker of PVS, which can automatically prove an important class of temporal logic theorems, and can also be used in conjunction with the powerful proof strategies of PVS, including automatic predicate abstraction, to verify a broader class of properties than can be achieved with model checking alone. Bluespec SystemVerilog is a hardware description language based on the guarded action model of concurrency. It has an elegant semantics, which has previously been shown to support design verification by hand proof: to date, however, little work has been conducted on the application of automated reasoning to BSV designs. © 2011 Springer-Verlag London Limited.
    Original languageEnglish
    Pages (from-to)85-95
    Number of pages10
    JournalInnovations in Systems and Software Engineering
    Volume7
    Issue number2
    DOIs
    Publication statusPublished - Jun 2011

    Keywords

    • Bluespec
    • Formal verification
    • Hardware
    • Model checker
    • Monad
    • Theorem prover

    Fingerprint

    Dive into the research topics of 'A monadic approach to automated reasoning for Bluespec SystemVerilog'. Together they form a unique fingerprint.

    Cite this