Reasoning about VHDL using operational and observational semantics

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

5 Citations (Scopus)
95 Downloads (Pure)

Abstract

We define a Plotkin-style structural operational semantics for a subset of vhdl that includes delta time, zero-delay scheduling and waits, arbitrary wait statements, and (commutative) resolution functions. While most of these features have been dealt with in separation, their combination is intricate. We follow closely the careful prose definition of vhdl as given in [9]. We prove a (conditional) monogenicity result for the operational semantics showing that the parallelism present in vhdl is benign. A classification of program behaviours is also given. While the semantics is of interest, of greater importance is the interpretation of the mature process algebra theory to our particular setting. An adaptation of bisimulation may be constructed but the concept of an observer, a process which inspects or acts as a test harness, turns out to be more useful. It leads naturally to a notion of observational equality that is a congruence with respect to parallel composition. This important result enables substitution of behaviourally equivalent subprograms without affecting the overall program behaviour. The capability to pass (incapability to fail) a test gives rise to a the may (must) preorder on processes. These preorders are shown to coincide. This work is supported by the euroform network sponsored by the Human Capital and Mobility programme of the European Community.
Original languageEnglish
Title of host publicationCorrect hardware design and verification methods : Proceedings of the IFIP WG 10.5 Advanced Research Working Conference ; October 2 - 4, 1995, Frankfurt/Main, Germany
EditorsPaolo E. Camurati, Hans Eveking
Place of PublicationBerlin
PublisherSpringer
Pages311-327
ISBN (Print)3-540-60385-9
DOIs
Publication statusPublished - 1995
Eventconference; Advanced Research Working Conference on Correct Hardware Design Methologies (CHARME) ; 8 (Frankfurt/Main) : 1995.10.02-04; 1995-10-02; 1995-10-04 -
Duration: 2 Oct 19954 Oct 1995

Publication series

NameLecture Notes in Computer Science
Volume987
ISSN (Print)0302-9743

Conference

Conferenceconference; Advanced Research Working Conference on Correct Hardware Design Methologies (CHARME) ; 8 (Frankfurt/Main) : 1995.10.02-04; 1995-10-02; 1995-10-04
Period2/10/954/10/95
OtherAdvanced Research Working Conference on Correct Hardware Design Methologies (CHARME) ; 8 (Frankfurt/Main) : 1995.10.02-04

Fingerprint

Dive into the research topics of 'Reasoning about VHDL using operational and observational semantics'. Together they form a unique fingerprint.

Cite this