Model Checking Verilog Descriptions of Cell Libraries.

M. Raffelsieper, J.-W. Roorda, and M.R. Mousavi. Proceedings of the 9th International Conference on Application of Concurrency to System Design (ACSD'09), Augsburg, Germany, IEEE CS, 2009.

Abstract

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.

@InProceedings{MousaviAcsd07,
    author      = "Raffelsieper, M. and Roorda, J.-W. and Mousavi, M.R.",
    title       = "Model Checking {Verilog} Descriptions of Cell Libraries.",
    booktitle   = "Proceedings of the 9th International Conference on Application of Concurrency to System Design (ACSD'09)",
    publisher   = "IEEE Computer Society Press, Los Alamitos, CA, USA, 2009"
}