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)

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.
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
Pages128-137
Publication statusPublished - 2009

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

Cite this