# Categorical Semantics of Digital Circuits

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

## Standard

**Categorical Semantics of Digital Circuits.** / Ghica, Dan; Jung, Achim.

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution

## Harvard

*Proceedings of Formal Methods in Computer-Aided Design (FMCAD 2016).*IEEE Computer Society Press, pp. 41-48, Formal Methods in Computer-Aided Design (FMCAD 2016), Mountain View, CA, United States, 3/10/16.

## APA

*Proceedings of Formal Methods in Computer-Aided Design (FMCAD 2016)*(pp. 41-48). IEEE Computer Society Press.

## Vancouver

## Author

## Bibtex

}

## RIS

TY - GEN

T1 - Categorical Semantics of Digital Circuits

AU - Ghica, Dan

AU - Jung, Achim

PY - 2016/10/3

Y1 - 2016/10/3

N2 - 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 wetarget is circuits with discrete signal levels, discrete time, and explicit delays, which is appropriate for modelling a range of components such as booleangates 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), whilequotienting it with a notion of equivalence corresponding to input-output observability. Using wellknown results about the correspondence between freemonoidal 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.

AB - 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 wetarget is circuits with discrete signal levels, discrete time, and explicit delays, which is appropriate for modelling a range of components such as booleangates 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), whilequotienting it with a notion of equivalence corresponding to input-output observability. Using wellknown results about the correspondence between freemonoidal 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.

M3 - Conference contribution

SP - 41

EP - 48

BT - Proceedings of Formal Methods in Computer-Aided Design (FMCAD 2016)

PB - IEEE Computer Society Press

T2 - Formal Methods in Computer-Aided Design (FMCAD 2016)

Y2 - 3 October 2016 through 6 October 2016

ER -