Categorical Semantics of Digital Circuits

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

Standard

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

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

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

Harvard

Ghica, D & Jung, A 2016, Categorical Semantics of Digital Circuits. in 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

Ghica, D., & Jung, A. (2016). Categorical Semantics of Digital Circuits. In Proceedings of Formal Methods in Computer-Aided Design (FMCAD 2016) (pp. 41-48). IEEE Computer Society Press.

Vancouver

Ghica D, Jung A. Categorical Semantics of Digital Circuits. In Proceedings of Formal Methods in Computer-Aided Design (FMCAD 2016). IEEE Computer Society Press. 2016. p. 41-48

Author

Ghica, Dan ; Jung, Achim. / Categorical Semantics of Digital Circuits. Proceedings of Formal Methods in Computer-Aided Design (FMCAD 2016). IEEE Computer Society Press, 2016. pp. 41-48

Bibtex

@inproceedings{38a8976621e74411a7f9bee5d841fcf8,
title = "Categorical Semantics of Digital Circuits",
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 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.",
author = "Dan Ghica and Achim Jung",
year = "2016",
month = oct,
day = "3",
language = "English",
pages = "41--48",
booktitle = "Proceedings of Formal Methods in Computer-Aided Design (FMCAD 2016)",
publisher = "IEEE Computer Society Press",
note = " Formal Methods in Computer-Aided Design (FMCAD 2016) ; Conference date: 03-10-2016 Through 06-10-2016",

}

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 -