Fixed-width multiplexers -- definitions

A width-bit multiplexer consumes one control bit, a left payload, and a right payload. Each output bit uses two internal AND gates and one output OR gate. Free edge negation supplies the negated control edge.

def Complexity.BitString.multiplexerInput {width : ℕ} (control : Bool) (left right : BitString width) : BitString (1 + (width + width))

Canonical input order for a fixed-width multiplexer: control, left payload, then right payload.

Equations

• Complexity.BitString.multiplexerInput control left right i = Fin.addCases (fun (x : Fin 1) => control) (Fin.append left right) i

def Complexity.Circuit.multiplexerInternalGate (width : ℕ) (index : Fin (width + width)) : { gate : Gate Basis.andOr2 (1 + (width + width) + (width + width)) // ∀ (input : Fin gate.fanIn), ↑(gate.inputs input) < 1 + (width + width) + ↑index }

One internal conjunction in the multiplexer. The first block selects left payload bits under the control; the second selects right payload bits under the negated control.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.Circuit.multiplexerOutputGate (width : ℕ) (coordinate : Fin width) : Gate Basis.andOr2 (1 + (width + width) + (width + width))

Output disjunction joining the selected left and right contributions at one payload coordinate.

Equations

• One or more equations did not get rendered due to their size.

def Complexity.Circuit.multiplexer (width : ℕ) [NeZero width] : Circuit Basis.andOr2 (1 + (width + width)) width (width + width)

Fixed-width fan-in-two multiplexer.

Equations

• One or more equations did not get rendered due to their size.