Soundness, completeness and non-redundancy of operational semantics for Verilog based on denotational semantics

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

9 Scopus citations

Abstract

This paper investigates three significant questions of Verilog’s operational semantics: soundness, completeness and non-redundancy. Our understanding for these three questions is denotational-based. We provide an operational semantics for Verilog and prove that our operational semantics is sound, complete and non-redundant.

Original languageEnglish
Title of host publicationFormal Methods and Software Engineering - 4th International Conference on Formal Engineering Methods, ICFEM 2002, Proceedings
EditorsChris George, Huaikou Miao
PublisherSpringer Verlag
Pages600-612
Number of pages13
ISBN (Print)9783540000297
DOIs
StatePublished - 2002
Externally publishedYes
Event4th International Conference on Formal Engineering Methods, ICFEM 2002 - Shanghai, China
Duration: 21 Oct 200225 Oct 2002

Publication series

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

Conference

Conference4th International Conference on Formal Engineering Methods, ICFEM 2002
Country/TerritoryChina
CityShanghai
Period21/10/0225/10/02

Fingerprint

Dive into the research topics of 'Soundness, completeness and non-redundancy of operational semantics for Verilog based on denotational semantics'. Together they form a unique fingerprint.

Cite this