An animatable operational semantics of the Verilog hardware description language

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

19 Scopus citations

Abstract

An operational semantics of a significant subset of the Verilog hardware description language (HDL) is presented. The semantics is encoded using the logic programming language Prolog in a literate programming style. This allows the associated documentation to be maintained in step with the semantics, and the printed version to be presented in a standard mathematical operational semantics style. It also enables the semantics to be directly animated using a Prolog interpreter. Using this approach allows the exploration of sometimes subtle behaviours of parallel programs and the possibility of rapid changes or additions to the semantics of the language covered that could be missed otherwise. In addition, it provides and extra check on the validity of the operational semantics.

Original languageEnglish
Title of host publicationICFEM 2000 - 3rd IEEE International Conference on Formal Engineering Methods
EditorsJohn A. McDermid, Shaoying Liu, Michael G. Hinchey
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages199-207
Number of pages9
ISBN (Electronic)0769508227, 9780769508221
DOIs
StatePublished - 2000
Externally publishedYes
Event3rd IEEE International Conference on Formal Engineering Methods, ICFEM 2000 - York, United Kingdom
Duration: 4 Sep 20006 Sep 2000

Publication series

NameICFEM 2000 - 3rd IEEE International Conference on Formal Engineering Methods

Conference

Conference3rd IEEE International Conference on Formal Engineering Methods, ICFEM 2000
Country/TerritoryUnited Kingdom
CityYork
Period4/09/006/09/00

Keywords

  • Animation
  • Documentation
  • Hardware design languages
  • Helium
  • Interleaved codes
  • Logic programming
  • Standards Working Groups
  • Standards development
  • Uniform resource locators
  • Very high speed integrated circuits

Fingerprint

Dive into the research topics of 'An animatable operational semantics of the Verilog hardware description language'. Together they form a unique fingerprint.

Cite this