Categorical Semantics of Digital Circuits

Dan Ghica, Achim Jung

Research output: Chapter in Book/Report/Conference proceedingConference contribution

209 Downloads (Pure)

Abstract

This paper proposes a categorical theory of digital circuits based on monoidal categories and graph rewriting. The main goal of this paper is conceptual:
to fill a foundational gap in reasoning about digital circuits, which is currently almost exclusively semantic (simulations). The level of abstraction we
target is circuits with discrete signal levels, discrete time, and explicit delays, which is appropriate for modelling a range of components such as boolean
gates or transistors working in saturation mode. We start with an algebraic signature consisting of the basic electronic components of a given class of circuits and extend it gradually (and in a free way) with further algebraic structure (representing circuit combinations, delays, and feedback), while
quotienting it with a notion of equivalence corresponding to input-output observability. Using wellknown results about the correspondence between free
monoidal categories and graph-like structures we can develop, in a principled way, a graph rewriting system which is shown to be useful in reasoning about such circuits. We illustrate the power of our system by reasoning equationally about a challenging class of circuits: combinational circuits with feedback.
Original languageEnglish
Title of host publicationProceedings of Formal Methods in Computer-Aided Design (FMCAD 2016)
PublisherIEEE Computer Society Press
Pages41-48
Number of pages8
ISBN (Electronic)978-0-9835678-6-8
Publication statusPublished - 3 Oct 2016
Event Formal Methods in Computer-Aided Design (FMCAD 2016) - Mountain View, CA, United States
Duration: 3 Oct 20166 Oct 2016

Conference

Conference Formal Methods in Computer-Aided Design (FMCAD 2016)
Country/TerritoryUnited States
CityMountain View, CA
Period3/10/166/10/16

Fingerprint

Dive into the research topics of 'Categorical Semantics of Digital Circuits'. Together they form a unique fingerprint.

Cite this