Model checking Verilog descriptions of cell libraries

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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

6 Citaten (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.
Originele taal-2Engels
TitelProceedings 9th International Conference on Application of Concurrency to System Design (ACSD'09, Augsburg, Germany, July 1-3, 2009)
UitgeverijInstitute of Electrical and Electronics Engineers
StatusGepubliceerd - 2009

Vingerafdruk Duik in de onderzoeksthema's van 'Model checking Verilog descriptions of cell libraries'. Samen vormen ze een unieke vingerafdruk.

Citeer dit