A Formal Executable Semantics of Verilog

This paper describes a formal executable semantics for the Verilog hardware description language. The goal of the authors' 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. Their 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.

Provided by: University of Illinois Topic: Software Date Added: May 2010 Format: PDF

Download Now

Find By Topic