Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics

TL;DR

This thesis develops a comprehensive, mathematically rigorous, compositional theory of synchronous digital circuits using denotational, operational, and algebraic semantics, and extends diagram rewriting techniques for circuit reasoning.

Contribution

It introduces a fully formalized semantic framework for digital circuits and extends string diagram rewriting with hypergraphs, enabling advanced reasoning and a new hardware description language.

Findings

Defined denotational semantics as causal stream functions

Established operational semantics via global transformations and local reductions

Developed algebraic equations for circuit normalization and encoding

Abstract

This thesis details 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 of sequential circuit morphisms, and then builds three different semantic theories: 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 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 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.