From algebraic semantics to denotational semantics for verilog

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

12 Scopus citations

Abstract

This paper considers how the algebraic semantics for Verilog relates with its denotational semantics. Our approach is to derive the denotational semantics from the algebraic semantics. We first present the algebraic laws for Verilog. Every program can be expressed as a guarded choice that can model the execution of a program. In order to investigate the parallel expansion laws, a sequence is introduced, which indicates the instantaneous action is due to which exact parallel component. A normal form is defined for each program by using the locality sequence. We provide a strategy for deriving the denotational semantics based on the algebraic normal form. Using the strategy, the denotational semantics for every program can be calculated. Program equivalence can also be explored by using the derived denotational semantics.

Original languageEnglish
Title of host publicationProceedings - 11th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2006
PublisherInstitute of Electrical and Electronics Engineers Inc.
Pages139-151
Number of pages13
ISBN (Print)9780769525303
DOIs
StatePublished - 2006
Event11th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2006 - Stanford, CA, United States
Duration: 15 Aug 200617 Aug 2006

Publication series

NameProceedings of the IEEE International Conference on Engineering of Complex Computer Systems, ICECCS
ISSN (Print)2770-8527
ISSN (Electronic)2770-8535

Conference

Conference11th IEEE International Conference on Engineering of Complex Computer Systems, ICECCS 2006
Country/TerritoryUnited States
CityStanford, CA
Period15/08/0617/08/06

Fingerprint

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

Cite this