Synchronous Decision Diagrams: a Data Structure for Representing Finite Sequential Digital Functions

A digital function $f$ maps sequences of binary inputs into binary outputs. It is causal when the outputs at time $n$ depend exclusively upon the input values from cycles 0 through $n$. A causal digital function $f$ is characterized by its truth table $F$. It is an infinite sequence of bits which is identified with the formal power series $F(z) = \sum F_n z^n$, with coefficients in the binary field. In order to be computable by some physical device, a digital function must be causal, and represented by some finite system. A result by Christol \emph{et al.\/} is used to characterize the class of causal finite digital functions: a digital function $f$ can be computed by a finite digital synchronous circuit, if and only if it is causal and its truth table is algebraic over the field of polynomial fractions modulo 2. Each causal finite function $f$ may thus be represented by a finite characteristic polynomial, whose truth table $F$ is the only root modulo 2. The problems of circuit verification and synthesis are thus reduced to solving finite polynomial equations. An algorithm is introduced together with a data structure in order to construct a canonical finite circuit, by ``recursively sampling'' the algebraic truth table $F$ of a causal finite function $f$. When $f$ is a combinatorial function, this circuit is identical to Bryant's classical DAG structure. In general, it is a cyclic data structure, which is shown to represent the minimal FSM for $f$. In the worst case, its size is doubly exponential in the size of $f$ efficient algorithms exist to operate on these circuits, in: - constant time for $f(zx)$, $f(1+zx)$; - linear time for $~f(x)$, $zf(x)$, the inverse $g(f(x))=x$, and the fixed point $y = zg(x,y)$; - quadratic time for the composition $f(g(x))$ and for Boolean operations $f(x)$ \& $f(y)$, ... ; - cubic time for the more general composition $f(g(x),h(x))$. The SDD opens an approach to sequential circuit synthesis and verification, whose implementation is straightforward in a high-level language, and which can automatically cope with synchronous circuits of limited size.