Foundations of digital circuits: denotational, operational, and algebraic semantics with applications to graph rewriting

Kaye, George ORCID: 0000-0002-0515-4055 (2024). Foundations of digital circuits: denotational, operational, and algebraic semantics with applications to graph rewriting. University of Birmingham. Ph.D.

Preview

Kaye2024PhD.pdf
Text - Accepted Version
Available under License All rights reserved.
Download (2MB) | Preview

Abstract

This thesis details the culmination of a project to define a fully compositional theory of synchronous sequential circuits built from primitive components, motivated by applying techniques successfully used in programming languages to hardware.

The first part of the thesis defines the syntactic foundations required to create sequential circuit morphisms, and then builds three different semantic theories on top of this: denotational, operational and algebraic. We characterise the denotational semantics of sequential circuits as certain causal stream functions, as well as providing a link to existing circuit methodologies by mapping between circuit morphisms, stream functions and Mealy machines. The operational semantics is defined as a strategy for applying some global transformations followed by local reductions in order to demonstrate how a circuit processes a value, leading to a notion of observational equivalence. The algebraic semantics consists of equations for bringing circuits into a pseudo-normal form, and then encoding between different state sets. This part of the thesis concludes with a discussion of some novel applications, such as those for using partial evaluation for digital circuits.

While mathematically rigorous, the categorical string diagram formalism is not suited for reasoning computationally. The second part of this thesis details an extension of existing work on string diagram rewriting with hypergraphs so that it is compatible with the traced comonoid structure present in the category of digital circuits. We identify the properties that characterise cospans of hypergraphs corresponding to traced comonoid terms, and demonstrate how to identify rewriting contexts valid for rewriting modulo traced comonoid structure. We apply the graph rewriting framework to fixed point operators as well as the operational semantics from the first part, and present a new hardware description language based on these theoretical developments.

Type of Work:

Thesis (Doctorates > Ph.D.)

Award Type:

Doctorates > Ph.D.

Supervisor(s):