From operational semantics to denotational semantics for verilog

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

20 Scopus citations

Abstract

This paper presents the derivation of a denotational semantics from an operational semantics for a subset of the widely used hardware description language Verilog. Our aim is to build an equivalence between the operational and denotational semantics. We propose a discrete time semantic model for Verilog. Algebraic laws are also investigated in this paper, with the ultimate aim of providing a unified set of semantic views for Verilog.

Original languageEnglish
Title of host publicationCorrect Hardware Design and Verification Methods - 11th IFIP WG 10.5 Advanced Research Working Conference, CHARME 2001, Proceedings
EditorsTiziana Margaria, Tom Melham
PublisherSpringer Verlag
Pages449-464
Number of pages16
ISBN (Print)3540425411, 9783540425410
DOIs
StatePublished - 2001
Externally publishedYes
Event11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, CHARME 2001 held jointly with the 14th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009 - Livingston, United Kingdom
Duration: 4 Sep 20017 Sep 2001

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume2144
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference11th IFIP WG 10.5 Advanced Research Working Conference on Correct Hardware Design and Verification Methods, CHARME 2001 held jointly with the 14th International Conference on Theorem Proving in Higher Order Logics, TPHOLs 2009
Country/TerritoryUnited Kingdom
CityLivingston
Period4/09/017/09/01

Fingerprint

Dive into the research topics of 'From operational semantics to denotational semantics for verilog'. Together they form a unique fingerprint.

Cite this