Model checking Verilog descriptions of cell libraries

M. Raffelsieper, J.W. Roorda, M.R. Mousavi

    Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

    6 Citations (Scopus)


    We present a formal semantics for a subset of Verilog, commonly used to describe cell libraries, in terms of transition systems. Such transition systems can serve as input to symbolic model checking, for example equivalence checking with a transistor netlist description. We implement our formal semantics as an encoding from the subset of Verilog to the input language of the SMV model-checker. Experiments show that this approach is able to verify complete cell libraries.
    Original languageEnglish
    Title of host publicationProceedings 9th International Conference on Application of Concurrency to System Design (ACSD'09, Augsburg, Germany, July 1-3, 2009)
    PublisherInstitute of Electrical and Electronics Engineers
    Publication statusPublished - 2009


    Dive into the research topics of 'Model checking Verilog descriptions of cell libraries'. Together they form a unique fingerprint.

    Cite this