Talking about the weather, but in a formal way (2)

The synchronous view uses the existence of the critical delay to abstract from edge propagation. Since real delays have no influence on the result, we can ignore them and work in discrete time, seeing the circuit as just another means of solving the Boolean equations that describe it. The simplest way is to adopt the assumption of perfect synchronism, which assumes that the circuit calculates outputs in zero time. Then, when we compose sub-circuits, in sequence, in parallel, or by looping outputs back to inputs (provided the resulting graph remains acyclic), the calculation always takes place in time zero, and all Boolean simplifications are applicable. The circuit designer can work in perfect synchronicity, with his CAD system calculating the physical stabilization time for a given technology. Of course, he must act to improve the actual computation time if his conceptual circuit is not fast enough for the physical requirements.

The rest of the lecture delved into Combinatorics circuit design, through the addition of two n-bit words to produce an n+1-bit result. The simple method is that of the school: for each pair of input bits_ai,_bi we instantiate a _FullAdderi adder with inputs_ai,_bi and an incoming carry_ci given by c0₌ 0 and_ci+1 =_ri for i > 0. The sum bits are the outputs_{si of the FullAdderi} for 0 ≤ i < n and the most significant bit_{sn = rn-1}. The circuit is linear in size in n, but its critical delay determined by the holdback path is also linear in n, which is too slow as soon as n is not very small.

The critical delay can be improved by varioustime-space exchanges. Thevon Neumann adder is based on the key ideas of dichotomy and speculation. The idea of dichotomy is to cut the input word in the middle and simultaneously add the low-weight half-words and the high-weight half-words. But the incoming carry of the high weights is the outgoing carry of the sum of the low weights. The idea of the speculation is to simultaneously calculate the two possible sums of the strong weights according to whether their incoming carry is 0 or 1, and then select the correct sum according to the effective carry of the weak weights, the other sum being simply ignored. The selection is made using mux(x,y,z) multiplexers, which calculate y if x is 1 and z if x is 0. The partial sums of the high and low weight half-words are calculated recursively using the same method. The critical path is then created by the multiplexer tree resulting from the recursion development: it is logarithmic (size 6 instead of 64 for 64 bits). Of course, this time acceleration comes at a cost in terms of space and energy, since we're calculating information only to ignore it later.

Another method, inspired by functional programming, is due to J. Vuillemin and F. Preparata. Its key is that the function_fi:_{ri → ri+1} for propagating the carry at stage i depends only on the two bits_ai and_bi: it is the constant function 0 if_ai and_bi are both 0, the identity function if one is 0 and the other 1, and the constant function 1 if both are 1. Since the global incoming carry is 0, we have_{ri+1 = fi}(_fi-1(...(_f1(_f0(0))))), so_ri+1 = (_fi◦fi-1◦..._◦f1◦f0)(0). Since the composition of functions is associative, it can be calculated dichotomously, for example as ((_f7◦f6)◦(_f5◦f4))◦((_f3◦f2)◦(_f1◦f0)) for n = 8. The compositions can therefore be calculated by a tree of parallel calculations, therefore in logarithmic depth and time. In the circuit, a function f : bool → bool is represented by its truth table, i.e. by the pair coded on two wires _f0 and _f1. The application of f to x is calculated by f(x) = mux(x, _f1, _f0), and the composition g◦f, by (g◦f_)i = mux(_fi, _g1, _g0) for i = 1,2. See the videos or the lecture boards for the resulting circuit, which is particularly elegant.

A very different addition uses redundant bases. A very simple presentation by J. Vuillemin works with soft numbers, i.e. pairs of numbers A = (a', a'') encoding the value a' + a'' in several ways. For example, 3 is coded (0,3), (1,2), (2,1) or (3,0). It's easy to see that the adder in figure 2 calculates in constant time (independent of the number of bits) a soft number whose value is the sum of the values of the input soft numbers. Of course, we can't read the result directly without ending with another addition summing its two components, but this structure is very efficient when we have a list of numbers to add up. Efficient multiplication can thus be achieved by first constructing the matrix of individual products (simple Boolean conjunctions in base 2), shifting the results as in school, and then adding the resulting numbers using a dichotomous tree of soft adders: this produces a soft result in logarithmic time, which only needs to be hardened into a single number using a final logarithmic adder, such as the von Neumann adder. The surprising result is that multiplication is actually calculated in logarithmic time. Redundant bases are also fundamental to efficient division, and it was an error in tabulating soft divisions in a non-binary base that led to the famous Pentium Pro bug that cost Intel $475 million in 1994.


The lecture ended with a reminder of an important result on cyclic circuits, already presented in 2010. It involves generalizing the notion of critical path by getting rid of the acyclicity constraint, i.e. knowing when a cyclic circuit computes deterministically and in predictable time for all wire and gate delays. This question is important both because cyclic circuits are generated naturally by synthesis from high-level languages and because a cyclic circuit can be exponentially smaller than any acyclic circuit for certain Boolean functions [2]. Our result is that a cyclic circuit is acceptable for the previous criterion if and only if its outputs can be computed using only the laws of constructive logic, which prohibits the excluded third " x or not x = 1". Thus, the electrical calculation of Hamlet 's circuit defined by the equation ToBe = ToBeor not ToBe does not converge for certain wire and gate delays, because its logical solution of the equation requires the excluded third.

The constructive restriction is natural, as the excluded third would require a speculation on the result that electrons are quite incapable of realizing. But proving the result is difficult. A new version of this proof due to Mendler [3] will be presented in the 2014 lecture. It uses a constructive temporal logic that closely mixes continuous and discrete aspects. It also shows that a circuit should be seen not only as a calculating machine but also as a proving machine, giving an electric view of the fundamental Curry-Howard correspondence between l-calculus calculations and intuitionistic logic proofs [4].