IDEALS Home University of Illinois at Urbana-Champaign logo The Alma Mater The Main Quad

A Formal Executable Semantics of Verilog

Show full item record

Bookmark or cite this item: http://hdl.handle.net/2142/17079

Files in this item

File Description Format
PDF memocode-tech-report.pdf (279KB) (no description provided) PDF
Title: A Formal Executable Semantics of Verilog
Author(s): Meredith, Patrick; Katelman, Michael; Meseguer, Jose; Roşu, Grigore
Subject(s): Programming Languages Language Semantics Verilog Rewriting Logic rewriting logic semantics
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 Verilog-based 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.
Issue Date: 2010-07
Citation Info: @techreport{ author={Patrick O'Neil Meredith and Michael Katelman and Jos{\'e} Meseguer and Grigore Ro\c{s}u}, title={A Formal Executable Semantics of {V}erilog}, institution={University of Illinois at Urbana Champaign}, year={2010} }
Genre: Technical Report
Type: Text
Language: English
URI: http://hdl.handle.net/2142/17079
Publication Status: unpublished
Peer Reviewed: is peer reviewed
Sponsor: CCF-0916893CNS-0720512CCF-0905584CCF-0448501NNL08AA23C
Date Available in IDEALS: 2010-09-07
 

This item appears in the following Collection(s)

Show full item record

Item Statistics

  • Total Downloads: 328
  • Downloads this Month: 6
  • Downloads Today: 1

Browse

My Account

Information

Access Key