A formal executable semantics of verilog

Patrick Meredith, Michael Katelman, José Meseguer, Grigore Rosu

Research output: Chapter in Book/Report/Conference proceedingConference contribution

Abstract

This paper describes a formal executable semantics for the Verilog hardware description language. The goal of our formalization is to provide a concise and mathematically rigorous reference augmenting the prose of the official language standard, and ultimately to aid developers of Verilogbased tools; e.g., simulators, test generators, and verification tools. Our semantics applies equally well to both synthesizeable and behavioral designs and is given in a familiar, operational-style within a logic providing important additional benefits above and beyond static formalization. In particular, it is executable and searchable so that one can ask questions about how a, possibly nondeterministic, Verilog program can legally behave under the formalization. The formalization should not be seen as the final word on Verilog, but rather as a starting point and basis for community discussions on the Verilog semantics.

Original languageEnglish (US)
Title of host publication8th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2010
Pages179-188
Number of pages10
DOIs
StatePublished - 2010
Event8th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2010 - Grenoble, France
Duration: Jul 26 2010Jul 28 2010

Publication series

Name8th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2010

Other

Other8th ACM/IEEE International Conference on Formal Methods and Models for Codesign, MEMOCODE 2010
CountryFrance
CityGrenoble
Period7/26/107/28/10

ASJC Scopus subject areas

  • Computational Theory and Mathematics
  • Hardware and Architecture
  • Software

Fingerprint Dive into the research topics of 'A formal executable semantics of verilog'. Together they form a unique fingerprint.

Cite this