Compositional Control-Driven Boolean Circuits

Abstract

Boolean circuits abstract away from physical details to focus on the logical structure and computational behaviour of digital components. Although such circuits have been studied for many decades, compositionality has been widely ignored or examined in an informal manner, which is a property for combining circuits without delving into their internal structure, while supporting modularity and formal reasoning. In this paper, we address this longstanding theoretical gap by proposing colimit-based operators for compositional circuit construction. We define separate operators for forming sequential, parallel, branching and iterative circuits. As composites encapsulate explicit control flow, a new model of computation emerges which we refer to as (families of) control-driven Boolean circuits. We show how this model is at least as powerful as its classical counterpart. In other words, it is able to non-uniformly compute any Boolean function on inputs of arbitrary length.

Figures (7)

• Figure 1: The set-valued diagrams (a) and (b) capture the structure of trivial and primitive circuits, respectively. Here, $\triangle$ denotes symmetric set difference.
• Figure 2: A trivial circuit and two control-driven logical connectives. Intuitively, (a) has no behaviour because it has no units. Although variables are labelled with some type through a function $c$, we label them with identifiers for convenience.
• Figure 3: Elementary logical connectives as control-driven Boolean circuits.
• Figure 4: A branching circuit that captures the computational behaviour of the context-sensitive stochastic Boolean network presented in liang_stochastic_2012. For increased readability, computation units are annotated to make evident the behaviour they perform. Here, the symbols $\lnot$, $\uparrow$, $E$, $F$ and $J$ denote NOT, NAND, Boolean eater, fork and join functions. All of them are well-defined as per Definitions \ref{['def:cunit']} and \ref{['def:transition']}.
• Figure 5: A buffer is a total sequential circuit of two NOT primitives. Here, we demonstrate the modularity property of control-driven circuits. A similar black-boxing can be done with any of the composites displayed in Figures \ref{['fig:elementary-circuits']} and \ref{['fig:branching-example']}.

Theorems & Definitions (59)

• definition 1: Computation Unit
• definition 2: Control-Driven Boolean Circuit
• definition 3: Circuit Interface
• definition 4: Sound Circuit
• remark 1
• proposition 1
• proof
• definition 5: Circuit Morphism
• remark 2
• definition 6: Adjoint Morphism