Document Open Access Logo

Diagrammatic Semantics for Digital Circuits

Authors Dan R. Ghica, Achim Jung, Aliaume Lopez

PDF
Thumbnail PDF

File

LIPIcs.CSL.2017.24.pdf
  • Filesize: 0.72 MB
  • 16 pages

Document Identifiers

Author Details

Dan R. Ghica
Achim Jung
Aliaume Lopez

Cite AsGet BibTex

Dan R. Ghica, Achim Jung, and Aliaume Lopez. Diagrammatic Semantics for Digital Circuits. In 26th EACSL Annual Conference on Computer Science Logic (CSL 2017). Leibniz International Proceedings in Informatics (LIPIcs), Volume 82, pp. 24:1-24:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2017)
https://doi.org/10.4230/LIPIcs.CSL.2017.24

Abstract

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.
Keywords
  • digital circuits
  • monoidal categories
  • string diagrams
  • rewriting
  • operational semantics

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

References

  1. Samson Abramsky and Bob Coecke. A categorical semantics of quantum protocols. In LICS, pages 415-425, 2004. Google Scholar
  2. 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. Google Scholar
  3. Filippo Bonchi, Fabio Gadducci, Aleks Kissinger, Pawel Sobocinski, and Fabio Zanasi. Rewriting modulo symmetric monoidal structure. In LICS, pages 710-719, 2016. Google Scholar
  4. Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi. Full abstraction for signal flow graphs. In POPL, pages 515-526, 2015. Google Scholar
  5. Filippo Bonchi, Pawel Sobocinski, and Fabio Zanasi. Lawvere categories as composed props. In CMCS, pages 11-32, 2016. Google Scholar
  6. 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. Google Scholar
  7. Charles Consel and Olivier Danvy. Tutorial notes on partial evaluation. In POPL, pages 493-501, 1993. Google Scholar
  8. 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. Google Scholar
  9. Samuel Eilenberg and Jesse B. Wright. Automata in general algebras. Information and Control, 11(4):452-470, 1967. Google Scholar
  10. Calvin C. Elgot. Monadic computation and iterative algebraic theories. Studies in Logic and the Foundations of Mathematics, 80:175-230, 1975. Google Scholar
  11. Dan R. Ghica. Diagrammatic reasoning for delay-insensitive asynchronous circuits. In Computation, Logic, Games, and Quantum Foundations, pages 52-68, 2013. Google Scholar
  12. Dan R. Ghica, Achim Jung, and Aliaume Lopez. Diagrammatic semantics for digital circuits. In Quantum Physics and Logic (QPL), 2017. forthcoming. Google Scholar
  13. D. R. Ghica and A. Jung. Categorical semantics of digital circuits. In Formal Methods in Computer-Aided Design (FMCAD), 2016. Google Scholar
  14. Makoto Hamana. Strongly normalising cyclic data computation by iteration categories of second-order algebraic theories. In FCSD, pages 21:1-21:18, 2016. Google Scholar
  15. Masahito Hasegawa. Models of Sharing Graphs: A Categorical Semantics of let and letrec. Springer Verlag, 1999. Google Scholar
  16. Masahito Hasegawa. The uniformity principle on traced monoidal categories. Electr. Notes Theor. Comput. Sci., 69:137-155, 2002. Google Scholar
  17. 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.
  18. André Joyal and Ross Street. The geometry of tensor calculus, I. Adv. in Math., 88(1):55-112, 1991. Google Scholar
  19. 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. Google Scholar
  20. Aleks Kissinger. Pictures of Processes. PhD thesis, University of Oxford, 2011. arXiv:1203.0202v2. Google Scholar
  21. 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. Google Scholar
  22. Stephen Lack. Composing PROPs. Theory and App. of Categories, 13(9):147-163, 2004. Google Scholar
  23. Peter J. Landin. An abstract machine for designers of computing languages. In Proc. IFIP Congress, volume 65, 1965. Google Scholar
  24. Charles E. Leiserson and James B. Saxe. Retiming synchronous circuitry. Algorithmica, 6(1-6):5-35, 1991. Google Scholar
  25. Wayne Luk. Pipelining and transposing heterogeneous array designs. J. of VLSI Sig. Proc. Sys., 5(1):7-20, 1993. Google Scholar
  26. Sharad Malik. Analysis of cyclic combinational circuits. In Proc. IEEE/ACM Int. Conf. on Comp. Aided Design, pages 618-625, 1993. Google Scholar
  27. 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. Google Scholar
  28. Gordon D. Plotkin. A structural approach to operational semantics. J. Log. Algebr. Program., 60-61:17-139, 2004. Google Scholar
  29. Peter Selinger. A survey of graphical languages for monoidal categories. In New structures for physics, pages 289-355. Springer, 2010. Google Scholar
  30. Mary Sheeran. muFP, A language for VLSI design. In LISP and Func. Prog., pages 104-112, 1984. Google Scholar
  31. 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. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact