Jean Vuillemin (ENS, Paris)

A digital function f maps sequences of binary inputs into binary outputs. It is causal when the outputs, at each discrete integer time n, depend exclusively upon the input values seen so far, from cycles 0 through n. A causal digital function f is characterised by its truth table F. It is an infinite sequence of bits F0…Fn… which is identified with the formal power series F(z) = sum Fn 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 & al is used to characterise the class of causal finite C&F digital functions:

Theorem 1 A digital function f may computed by a finite digital synchronous circuit, if and only if, it is causal and its truth table is algebraic over the field F2 [z] of polynomial fractions modulo 2.

Each C&F digital function f may thus be represented by a finite characteristic polynomial, of which truth table F is the only root, modulo 2. In theory, the dual problems of automatic circuit verification and synthesis are reduced to solving finite polynomial equations. This opens a new approach, to sequential circuit design, test, and proofs.

An algorithm and data structure is introduced, as a basis to the approach: it constructs a canonical finite circuit SDD(f), by “recursively sampling” the truth table F of a C&F function f. When applied to a combinatorial function f, SDD(f) is identical to the classical OBDD(f) DAG structure, from Bryant. For a sequential function f, SDD(f) is a cyclic data structure, which canonically represents the minimal FSM for f.

We show that one may compute sequential operations o(f,g) in polynomial time & space: |SDD(o(f,g))| < |SDD(o)|x|SDD(f)|x|SDD(g)|. In the worst case, the size of |SDD(f)|<2^2^|f| may be related to the size of f by a double exponential (for combinatorial f, a single exponential |OBDD(f)|<2^|f|).