We gratefully acknowledge support from
the Simons Foundation and member institutions.
Full-text links:

Download:

Current browse context:

cs.LO

Change to browse by:

References & Citations

DBLP - CS Bibliography

Bookmark

(what is this?)
CiteULike logo BibSonomy logo Mendeley logo del.icio.us logo Digg logo Reddit logo ScienceWISE logo

Computer Science > Logic in Computer Science

Title: Full abstraction for digital circuits

Abstract: This paper refines the existing axiomatic semantics of digital circuits with delay and feedback, in which circuits are constructed as morphisms in a freely generated cartesian traced (dataflow) category. First, we give a cleaner presentation, making a clearer distinction between syntax and semantics, including a full formalisation of the semantics as stream functions. As part of this effort, we refocus the categorical framework through the lens of string diagrams, which not only makes reading equations more intuitive but removes bureaucracy such as associativity from proofs. We also extend the existing framework with a new axiom, inspired by the Kleene fixed-point theorem, which allows circuits with non-delay-guarded feedback, typically handled poorly by traditional methodologies, to be replaced with a series of finitely iterated circuits. This eliminates the possibility of infinitely unfolding a circuit; instead, one can always reduce a circuit to some (possibly undefined) value. To fully characterise the stream functions that correspond to digital circuits, we examine how the behaviour of the latter can be modelled using Mealy machines. By establishing that the translation between sequential circuits and Mealy machines preserves their behaviour, one can observe that circuits always implement monotone stream functions with finite stream derivatives.
Comments: Reworded section 5, 23 pages, 6 figures
Subjects: Logic in Computer Science (cs.LO); Programming Languages (cs.PL); Category Theory (math.CT)
Cite as: arXiv:2201.10456 [cs.LO]
  (or arXiv:2201.10456v3 [cs.LO] for this version)

Submission history

From: George Kaye [view email]
[v1] Tue, 25 Jan 2022 16:58:10 GMT (49kb)
[v2] Wed, 26 Jan 2022 15:10:49 GMT (50kb)
[v3] Thu, 3 Feb 2022 15:24:58 GMT (51kb)

Link back to: arXiv, form interface, contact.