## 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.

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 language | English |
---|---|

Title of host publication | Proceedings of Formal Methods in Computer-Aided Design (FMCAD 2016) |

Publisher | IEEE Computer Society Press |

Pages | 41-48 |

Number of pages | 8 |

ISBN (Electronic) | 978-0-9835678-6-8 |

Publication status | Published - 3 Oct 2016 |

Event | Formal Methods in Computer-Aided Design (FMCAD 2016) - Mountain View, CA, United States Duration: 3 Oct 2016 → 6 Oct 2016 |

### Conference

Conference | Formal Methods in Computer-Aided Design (FMCAD 2016) |
---|---|

Country/Territory | United States |

City | Mountain View, CA |

Period | 3/10/16 → 6/10/16 |