Functional Type Expressions of Sequential Circuits with the Notion of Referring Forms

From a theoretical perspective, sequential circuits are described using Mealy machines (or Mealy automata) [2, 3]. For arbitrary sets $I$ and $O$, a Mealy machine $(S,\psi)$ with input $I$ and output $O$ consists of a set $S$ of states and transition function $\psi:S\to(O\times S)^{I}$. When a previous state $s\in S$ and current input $i\in I$ are provided, a tuple of the current output and state $\psi\,s\,i\in O\times S$ is derived. For a given initial state, the Mealy machine $(S,\psi)$ behaves as a causal stream function of type $I^{\mathbb{N}_{1}}\to O^{\mathbb{N}_{1}}$, where $\mathbb{N}_{1}$ denotes the natural numbers $\{1,2,\cdots\}$, excluding zero, as ordinal numbers. (We also use $\mathbb{N}_{0}$ for $\{0,1,\cdots\}$ later.) Domain $I^{\mathbb{N}_{1}}$ and codomain $O^{\mathbb{N}_{1}}$ represent infinite input and output streams over time; that is, the input and output signals, respectively. Causal means that the current output depends only on past and current inputs and not on future inputs.

This function is constructed from the transition function $\psi$ of the Mealy machine, as follows: Given an initial state $s_{0}$ and a finite input stream $(i_{1},i_{2},\cdots,i_{n})\in I^{n}$, the output stream $(o_{1},o_{2},\cdots,o_{n})\in O^{n}$ is determined by $(o_{j},s_{j})=\psi\,s_{j-1}\,i_{j}\;(j\in\mathbb{N}_{1})$. Conversely, [4] proved that an arbitrary causal stream function $f:I^{\mathbb{N}_{1}}\to O^{\mathbb{N}_{1}}$ can be represented using the corresponding Mealy machine. Therefore, we investigate the causal stream functions $I^{\mathbb{N}_{1}}\to O^{\mathbb{N}_{1}}$ instead of Mealy machines.

We consider a causal stream function $f\,:\,I^{\mathbb{N}_{1}}\to O^{\mathbb{N}_{1}}$. Because it is causal, the $n$-th output $o_{n}$ depends on an $n$-length input stream $(i_{1},i_{2},\cdots,i_{n})$, and $f$ can be expressed by a family of functions $\{\,f_{n}\,:\,I^{n}\to O\,\}_{n\in\mathbb{N}_{1}}$. We denote this function family as

to simplify the later expressions.

We must consider the product type of the input to develop our theory further. When the input $I$ of the causal stream functions (1) is converted into the product $I_{A}\times I_{B}$, it becomes $(I_{A}\times I_{B})^{+}\cong I_{A}^{\;+}\times I_{B}^{\;+}$ and the type is isomorphic to

by Currying. Note that the two pluses above must be interpreted as the same number; that is, $\{\,I_{A}^{\;\,n}\to I_{B}^{\;\,n}\to O\,\}_{n\in\mathbb{N}_{1}}$ in the expression of function families, which differs from the usual definition $A^{+}=A+(A\times A)+\cdots+A^{\mathbb{N}}$.

We also require notions of the dependent types [5, 6] for sets and elements instead of types and terms. For given $A\in Set$ and $\alpha:A\to Set$, a subset $(a:A)\times\alpha\,a\,\subset\,A\times{\displaystyle\sum_{x\in A}}\,\alpha\,x$ is defined as

where $(a:A)$ represents a domain $A$ and an arbitrary $a$ is obtained from $A$ for later expressions. In this study, $(a:A)$ denotes a domain with dependent types, as explained above, and $a\in A$ denotes the usual proposition.

For functions with two-part inputs, such as (2), we introduce the notion that a given first input restricts the second input domain. To express this notion, we use dependent types and consider

where $\mathcal{P}$ denotes the power sets. We use the control input $C$ and data input $I$ instead of $I_{A}$ and $I_{B}$ in (2). The second domain of the upper expression in (6) is not the entire data input $I^{+}$, but only part of it, as if it were filtered based on the control input $\sigma$. For example, for given $\phi_{n}:C^{n}\to\mathcal{P}(I^{n})$ and $\sigma_{n}=(c_{1},c_{2},\cdots,c_{n})$, $\phi_{n}\,\sigma_{n}:=I\times\cdots\times I$ means that $f_{n}\,\sigma_{n}$ can refer to all past inputs, whereas $\phi_{n}\,\sigma_{n}:=\emptyset\times\cdots\times\emptyset\times I$ means that $f_{n}\,\sigma_{n}$ can refer to the current input only. In addition, we assume that a given first value $\sigma:C^{+}$ of $f$ does not influence the final function $\phi\,\sigma\to O$; that is, $\phi\,\sigma=\phi\,\sigma^{\prime}$ implies $f\,\sigma=f\,\sigma^{\prime}$.

Our model can be made more precise by focusing on the first and final time steps. In the first time step, no past is referred to; thus, $C^{+}$ must be modified to $C^{*}$. In the final time step, the current input is always referred to, because we consider Mealy machines. Finally, we obtain the following definition, originally proposed in [1]:

The current input $I$ is always provided, and the restriction map $\phi$ considers only past inputs and not current inputs. A restriction map $\phi$ comprehends how the circuit refers to the past with the passage of time.

The notion of domain restriction (9) contains the control signal $\sigma\in C^{*}$; however, to study the reference method, we only require the image $\phi\,\sigma$. We omit the control signal $\sigma$ from the expression of the domain restriction (9), which helps us to observe how the circuit refers to past inputs easily.

Roughly, referring forms represent a memory element of the target circuit and a given control signal to the memory element; they provide the manner in which the circuit refers to past inputs. When (10) is precisely expressed as a family of functions,

and the referring form is $\{\rho_{n}:\mathcal{P}(I^{n})\}_{n\in\mathbb{N}_{0}}$. The set $\{\rho_{n}\}_{n\in\mathbb{N}_{0}}$ can be regarded as $\rho:(n:\mathbb{N}_{0})\to\mathcal{P}(I^{n})$ and approximately $\rho:\mathbb{N}_{0}\to\mathcal{P}(I^{\mathbb{N}_{0}})$.

We present an example of referring forms for a D-flip-flop (D-FF) as a sequential circuit, with data input $I$, output $O$, and a clock. Because the D-FF holds the input value at the latest edge of the clock, the referring form $\rho$ behaves as shown in Fig. 3; during time $n,\cdots,n+3$, $\rho$ provides the input value at $n$, following which $\rho$ provides the input value at $n+4$. An excerpt from the overall type expressions is as follows:

where $(\times I)$ means that the current input is not referred to by the D-FF. Note that the referring form shown in Fig. 3 is regarded as $\mathcal{P}(I)^{*}$ because $\mathcal{P}(I)^{*}\cong\mathcal{P}(I^{*})$ and may be intuitively comprehensible. Henceforth, this isomorphism is sometimes used implicitly.

Owing to the abstractness of types, we can express a class of circuits such as synchronous circuits, as shown in Fig. LABEL:fig:Sync(a), in an expression; the referring form is shown in (b). The input $I$ is held and can be referred to at every edge of the clock. Unlike D-FFs, synchronous circuits can potentially refer to all past inputs at the clock edges through their feedback loop.

Next, we consider multiple clock domain circuits, as shown in Fig. 3. With the general description, their referring form becomes the same that of as Fig. LABEL:fig:Sync(b) for synchronous circuits because every FF may hold data from the input $I$ and outputs from all of the FFs. In fact, when multiple clock domains are required, multiple parts should independently have different clock domains; for instance, Fig. LABEL:fig:2CDin(a) has $clock1$ to latch input $I$, followed by the general $clock2$ domain circuit. The referring form in Fig. LABEL:fig:2CDin(b) indicates that the latest input $I$ latched by $clock1$ is delivered to the $clock2$ domain when $clock2$ ticks.