Difference between revisions of "A Formal Executable Semantics of Verilog"

From FSL
Jump to: navigation, search
Line 1: Line 1:
 +
===MEMOCODE'10===
 +
 
<pub id='meredith-katelman-meseguer-rosu-2010-memocode' template='PubDefaultWithAbstractAndTitle'></pub>
 
<pub id='meredith-katelman-meseguer-rosu-2010-memocode' template='PubDefaultWithAbstractAndTitle'></pub>
 +
 +
===Technical Report===
 +
 +
<pub id='meredith-katelman-meseguer-rosu-2010-tr' template='PubDefaultWithAbstractAndTitle'></pub>

Revision as of 17:31, 7 September 2010

MEMOCODE'10

A Formal Executable Semantics of Verilog
Patrick Meredith, Michael Katelman, Jose Meseguer and Grigore Rosu
MEMOCODE'10, IEEE, pp 179-188. 2010
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.
PDF, Slides(PDF), Sources, Verilog Semantics, IEEE, MEMOCODE'10, BIB


Technical Report

A Formal Executable Semantics of Verilog
Patrick Meredith, Michael Katelman, Jose Meseguer and Grigore Rosu
Technical Report http://hdl.handle.net/2142/17079, July 2010
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.
PDF, TR@UIUC, BIB

Personal tools
Namespaces

Variants
Actions
Navigation