Diagrammatic Semantics for Digital Circuits
We introduce a general diagrammatic theory of digital circuits, based on connections between monoidal categories and graph rewriting. The main achievement of the paper is conceptual, filling a foundational gap in reasoning syntactically and symbolically about a large class of digital circuits (discrete values, discrete delays, feedback). This complements the dominant approach to circuit modelling, which relies on simulation. The main advantage of our symbolic approach is the enabling of automated reasoning about parametrised circuits, with a potentially interesting new application to partial evaluation of digital circuits. Relative to the recent interest and activity in categorical and diagrammatic methods, our work makes several new contributions. The most important is establishing that categories of digital circuits are Cartesian and admit, in the presence of feedback expressive iteration axioms. The second is producing a general yet simple graph-rewrite framework for reasoning about such categories in which the rewrite rules are computationally efficient, opening the way for practical applications.
digital circuits
monoidal categories
string diagrams
rewriting
operational semantics
24:1-24:16
Regular Paper
Dan R.
Ghica
Dan R. Ghica
Achim
Jung
Achim Jung
Aliaume
Lopez
Aliaume Lopez
10.4230/LIPIcs.CSL.2017.24
Samson Abramsky and Bob Coecke. A categorical semantics of quantum protocols. In LICS, pages 415-425, 2004.
Stephen L. Bloom and Zoltán Ésik. Iteration Theories: The Equational Logic of Iterative Processes. Springer-Verlag New York, Inc., New York, NY, USA, 1993.
Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. Rewriting modulo symmetric monoidal structure. In LICS, pages 710-719, 2016.
Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi. Full abstraction for signal flow graphs. In POPL, pages 515-526, 2015.
Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi. Lawvere categories as composed props. In CMCS, pages 11-32, 2016.
Virgil Emil Căzănescu and Gheorghe Ştefănescu. Towards a new algebraic foundation of flowchart scheme theory. Fund. Inf., 13(2):171-210, 1990.
Charles Consel and Olivier Danvy. Tutorial notes on partial evaluation. In POPL, pages 493-501, 1993.
Andrea Corradini, Ugo Montanari, Francesca Rossi, Hartmut Ehrig, Reiko Heckel, and Michael Löwe. Algebraic approaches to graph transformation - part i: Basic concepts and double pushout approach. In Handbook of Graph Grammars, pages 163-246, 1997.
Samuel Eilenberg and Jesse B. Wright. Automata in general algebras. Information and Control, 11(4):452-470, 1967.
Calvin C. Elgot. Monadic computation and iterative algebraic theories. Studies in Logic and the Foundations of Mathematics, 80:175-230, 1975.
Dan R. Ghica. Diagrammatic reasoning for delay-insensitive asynchronous circuits. In Computation, Logic, Games, and Quantum Foundations, pages 52-68, 2013.
Dan R. Ghica, Achim Jung, and Aliaume Lopez. Diagrammatic semantics for digital circuits. In Quantum Physics and Logic (QPL), 2017. forthcoming.
D. R. Ghica and A. Jung. Categorical semantics of digital circuits. In Formal Methods in Computer-Aided Design (FMCAD), 2016.
Makoto Hamana. Strongly normalising cyclic data computation by iteration categories of second-order algebraic theories. In FCSD, pages 21:1-21:18, 2016.
Masahito Hasegawa. Models of Sharing Graphs: A Categorical Semantics of let and letrec. Springer Verlag, 1999.
Masahito Hasegawa. The uniformity principle on traced monoidal categories. Electr. Notes Theor. Comput. Sci., 69:137-155, 2002.
IEEE model standards group. IEEE standard multivalue logic system for VHDL model interoperability (std_logic_1164), May 1993. URL: http://dx.doi.org/10.1109/IEEESTD.1993.115571.
http://dx.doi.org/10.1109/IEEESTD.1993.115571
André Joyal and Ross Street. The geometry of tensor calculus, I. Adv. in Math., 88(1):55-112, 1991.
André Joyal, Ross Street, and Dominic Verity. Traced monoidal categories. In Math. Proc. of the Cambridge Phil. Soc., volume 119, pages 447-468. Cambridge Univ. Press, 1996.
Aleks Kissinger. Pictures of Processes. PhD thesis, University of Oxford, 2011. arXiv:1203.0202v2.
Robert P. Kurshan and Kenneth L. McMillan. Analysis of digital circuits through symbolic reduction. IEEE Trans. on CAD of Integrated Circuits and Systems, 10(11):1356-1371, 1991.
Stephen Lack. Composing PROPs. Theory and App. of Categories, 13(9):147-163, 2004.
Peter J. Landin. An abstract machine for designers of computing languages. In Proc. IFIP Congress, volume 65, 1965.
Charles E. Leiserson and James B. Saxe. Retiming synchronous circuitry. Algorithmica, 6(1-6):5-35, 1991.
Wayne Luk. Pipelining and transposing heterogeneous array designs. J. of VLSI Sig. Proc. Sys., 5(1):7-20, 1993.
Sharad Malik. Analysis of cyclic combinational circuits. In Proc. IEEE/ACM Int. Conf. on Comp. Aided Design, pages 618-625, 1993.
Michael Mendler, Thomas R. Shiple, and Gérard Berry. Constructive boolean circuits and the exactness of timed ternary simulation. Form. Meth. Syst. Des., 40(3):283-329, 2012.
Gordon D. Plotkin. A structural approach to operational semantics. J. Log. Algebr. Program., 60-61:17-139, 2004.
Peter Selinger. A survey of graphical languages for monoidal categories. In New structures for physics, pages 289-355. Springer, 2010.
Mary Sheeran. muFP, A language for VLSI design. In LISP and Func. Prog., pages 104-112, 1984.
Alex Simpson and Gordon Plotkin. Complete axioms for categorical fixed-point operators. In Logic in Computer Science, 2000. Proceedings. 15th Annual IEEE Symposium on, pages 30-41. IEEE, 2000.
Creative Commons Attribution 3.0 Unported license
https://creativecommons.org/licenses/by/3.0/legalcode