A syntax is compositional if complex components can be constructed out of simpler ones on the basis of their interfaces, without inspecting their internals. Digital circuits, despite having been studied for nearly a century and used at scale for about half that time, have until recently evaded a fully compositional theoretical understanding. The sticking point has been the need to avoid feedback loops that bypass memory elements, the so called `combinational feedback' problem. This requires examining the internal structure of a circuit, defeating compositionality. Recent work remedied this theoretical shortcoming by showing how digital circuits can be presented compositionally as morphisms in a freely generated Cartesian traced (dataflow) category. The focus was to support a better syntactical understanding of digital circuits, culminating in the formulation of novel operational semantics for digital circuits using an equational theory. The goals of this paper are twofold. First we formalise the semantics of digital circuits by interpreting them as functions on streams with certain properties. Second we refine the previous equational theory so that it is in perfect agreement with the semantic model. To support this result we introduce two key equations: the first can eliminate non-delay-guarded feedback via finite unfoldings, and the second can translate between circuits with the same behaviour syntactically by reducing the problem to checking a finite number of closed circuits. While these are enough to establish a correspondence between the denotational and the equational frameworks, we also show how simpler equations can be derived for more intuitive reasoning. The most important consequence of this is that we can now give a recipe that ensures a circuit always produces observable output, thus using the denotational model to inform and improve the operational semantics.

翻译：组合语法是指，复杂组件可以基于其接口由简单组件构建，而无需检查其内部结构。尽管数字电路已被研究近一个世纪，并大规模应用约半个世纪，但直到最近才获得完全组合的理论理解。其难点在于需要避免绕过存储元件的反馈环路，即所谓的“组合反馈”问题。这要求检查电路内部结构，从而破坏了组合性。近期工作通过展示数字电路如何作为自由生成的笛卡尔迹（数据流）范畴中的态射进行组合化呈现，弥补了这一理论缺陷。该工作侧重于支持对数字电路更好的语法理解，最终利用等式理论为数字电路制定了新的操作语义。本文目标有二：首先，通过将数字电路解释为具有特定性质的流上的函数，形式化其语义；其次，完善先前的等式理论，使其与语义模型完美吻合。为支撑这一结果，我们引入两个关键等式：第一个通过有限展开消除非延迟保护反馈，第二个通过将问题简化为检查有限个封闭电路，在语法上翻译具有相同行为的电路。虽然这足以建立指称语义与等式框架之间的对应关系，但我们还展示了如何推导更简洁的等式以进行更直观的推理。最重要的是，我们现在能给出确保电路始终产生可观测输出的方法，从而利用指称模型指导并改进操作语义。