A Caltech Library Service

Semantics of VLSI synthesis


Van der Goot, Marcel Rene (1995) Semantics of VLSI synthesis. Dissertation (Ph.D.), California Institute of Technology. doi:10.7907/SR5V-KT18.


We develop a new form of formal operational semantics, suitable for concurrent programming languages. The semantics directly supports sequential and parallel composition, rendezvous synchronization, shared variables, and non-determinism. Based on an abstract notion of program execution, a refinement relation is defined. We show how the refinement relation can be used to prove that one program implements another. We use the operational semantics as a semantic framework for a synthesis method for asynchronous VLSI circuits. We define the semantics of the programming notations that are used, and use the refinement relation to prove the correctness of the program transformations that form the basis of the synthesis method. Among other transformations, we proof the correctness of the replacement of atomic synchronization actions by handshake protocols, and the transformation of a sequence of actions into a network of concurrently executing gates.

Item Type:Thesis (Dissertation (Ph.D.))
Degree Grantor:California Institute of Technology
Division:Engineering and Applied Science
Major Option:Computer Science
Thesis Availability:Public (worldwide access)
Research Advisor(s):
  • Martin, Alain J.
Thesis Committee:
  • Martin, Alain J. (chair)
  • Sanders, Beverly
  • Hofstee, H. Peter
  • Chandy, K. Mani
  • Abu-Mostafa, Yaser S.
Defense Date:26 May 1995
Non-Caltech Author Email:vdgoot (AT)
Record Number:CaltechETD:etd-10162007-093427
Persistent URL:
Default Usage Policy:No commercial reproduction, distribution, display or performance rights in this work are provided.
ID Code:4110
Deposited By: Imported from ETD-db
Deposited On:26 Oct 2007
Last Modified:21 Dec 2019 02:04

Thesis Files

PDF (Van_der_goot_mr_1995.pdf) - Final Version
See Usage Policy.


Repository Staff Only: item control page