Skip to content

Putting blocks together

11. Building bigger blocks: composition

You build large systems by wiring small blocks together. VAR inst : OtherBlock; creates an instance; inst(In := expr, ...) wires its inputs; inst.Out reads its outputs. A start/stop station built from the reset-dominant RS latch (examples/composition/StartStop.zqel, reusing RS.zqel):

FUNCTION_BLOCK StartStop
VAR_INPUT
    Start : BOOL;
    Stop  : BOOL;
END_VAR
VAR_OUTPUT
    Running : BOOL;
END_VAR
VAR
    latch : RS;                    // an instance of the RS block from RS.zqel
END_VAR
IMPLEMENTATION
    latch(S := Start, R1 := Stop); // wire Start -> latch.S, Stop -> latch.R1
    Running := latch.Q1;           // expose the latch's output
END_IMPLEMENTATION
END_FUNCTION_BLOCK

The three lines of IMPLEMENTATION are exactly the three arrows into and out of the instance:

flowchart LR
    Start(["Start"]) --> S
    Stop(["Stop"]) --> R1
    subgraph latch["latch : RS"]
        S["S"]
        R1["R1"]
        Q1["Q1"]
    end
    Q1 --> Running(["Running"])

StartStop owns no memory of its own. Everything it remembers, it remembers through latch — which is why the latch's proven properties carry upward rather than needing to be restated here.

At compile time zqel flattens the instance in: the sub-block's internals become hidden locals of the parent, its inputs are replaced by the wired expressions, and latch.Q1 reads its freshly computed output. The generated ST shows the flattened result — the RS latch's equation, now with its state renamed latch__Q1:

VAR
    latch__Q1 : BOOL;              (* the sub-latch's memory, now a hidden local *)
    _latch__Q1_next : BOOL;
END_VAR
    _latch__Q1_next := (NOT Stop AND (Start OR latch__Q1));
    Running := (NOT Stop AND (Start OR latch__Q1));
    latch__Q1 := _latch__Q1_next;

Because composition is just flattening, everything else — proofs, backends — works unchanged. And the contracts compose:

  • A sub-block keeps its own INVARIANTs: instantiating a child never drops its safety proofs.
  • A parent may write invariants about a sub-instance's outputs (inst.Out).
  • A child's ASSUME is honoured based on how it is wired, and the compiler splits it accordingly. If it resolves to the parent's own inputs, it bubbles up as a premise on the parent (the parent's caller must honour it). If the parent instead supplies it with internal logic (a local, register or constant), the parent must discharge it — the premise becomes a proof obligation the parent proves on the spot (wiring it to D := TRUE compiles; wiring it to FALSE fails, as it must). Both directions work today. The split is syntactic (by which names the wired premise references), so a premise that mixes free inputs with internal state is not yet handled in full generality — the roadmap tracks the general “prove what you can, assume the residual” form.

11b. Template blocks — reusing logic at different sizes

Composition lets you wire a fixed-size RS latch into anything that needs one. But what if you want a dot-product block that works for vectors of different lengths? Without something more, you would write Vec3, Vec4, Vec5 as separate files — identical logic, different size. That is the monomorphism trap.

Type template parameters solve this. Put the size in angle brackets after the block name, then use it like an ordinary integer everywhere inside:

FUNCTION_BLOCK Vec<N: UINT>
VAR_INPUT
    a : ARRAY[0..N-1] OF LREAL;
    b : ARRAY[0..N-1] OF LREAL;
END_VAR
VAR_OUTPUT
    dot : LREAL;
END_VAR
IMPLEMENTATION
    dot := SUM(k IN 0..N-1 : a[k] * b[k]);
END_IMPLEMENTATION
END_FUNCTION_BLOCK

Save this as Vec.zqel. Now a parent block can wire in Vec<3> and Vec<4> as if they were ordinary sub-blocks:

FUNCTION_BLOCK TwoVecs
VAR_INPUT
    p3 : ARRAY[0..2] OF LREAL;  q3 : ARRAY[0..2] OF LREAL;
    p4 : ARRAY[0..3] OF LREAL;  q4 : ARRAY[0..3] OF LREAL;
END_VAR
VAR_OUTPUT
    d3 : LREAL;
    d4 : LREAL;
END_VAR
VAR
    v3 : Vec<3>;
    v4 : Vec<4>;
END_VAR
WIRING
    v3(a := p3, b := q3);
    v4(a := p4, b := q4);
    d3 := v3.dot;
    d4 := v4.dot;
END_WIRING
END_FUNCTION_BLOCK

The compiler monomorphizes each instantiation: it substitutes N = 3 into the full AST of Vec, resolves ARRAY[0..N-1] to ARRAY[0..2] and SUM(k IN 0..N-1 : …) to SUM(k IN 0..2 : …), names the result Vec<3>, and then compiles it as an ordinary concrete FB. Vec<3> and Vec<4> are independent concrete types: separate proofs, separate generated arrays, separate hidden locals after flattening.

Nothing about this sidesteps the rules you already know. The Bounded-Cycle Theorem still holds: every bound is a compile-time integer literal after substitution, so the compiler knows the size of every array and the range of every aggregate before it starts verifying anything.

Two type parameters work the same way. A 2×3 matrix-vector multiply:

FUNCTION_BLOCK MatVec<M: UINT, K: UINT>
VAR_INPUT
    a : ARRAY[0..M*K-1] OF LREAL;   (* row-major; a[i*K+k] is row i, col k *)
    x : ARRAY[0..K-1]   OF LREAL;
END_VAR
VAR_OUTPUT
    y : ARRAY[0..M-1] OF LREAL;
END_VAR
IMPLEMENTATION
    y := ARRAY(i IN 0..M-1 : SUM(k IN 0..K-1 : a[i*K+k] * x[k]));
END_IMPLEMENTATION
END_FUNCTION_BLOCK

VAR
    mv : MatVec<2, 3>;   (* M=2 rows, K=3 columns *)
END_VAR
WIRING
    mv(a := A, x := x);
    y := mv.y;
END_WIRING

For more detail — multiple parameters, wiring patterns, pitfalls — see the How-To: Use Template Blocks and the Concept: Template Blocks.

12. Physical units — catching “apples plus oranges” at compile time

A famous class of bugs is mixing incompatible physical quantities (adding a pressure to a temperature, or forgetting to multiply a flow by a time). zqel can catch these at compile time if you annotate your MATHREALs with units:

VAR_INPUT
    flow : MATHREAL<m3/h>;             // volumetric flow, cubic metres per hour
    cap  : MATHREAL<m3>;               // tank capacity, cubic metres
END_VAR
VAR_OUTPUT
    volume : MATHREAL<m3>;             // accumulated volume, cubic metres
END_VAR
IMPLEMENTATION
    volume:
        SET CLAMP(volume + flow * DT, 0.0, cap) OTHERWISE;
    ...

(Full example: examples/analog/flow_totalizer.zqel.) The compiler works out the dimension of every expression and checks consistency:

  • +, − and comparisons require compatible dimensions (a bare number adapts to either side).
  • * and / combine dimensions (multiply/divide the exponents).
  • DT has the dimension of time.

The key insight it proves here: flow (m³/h) times DT (s) has dimension m³ — a volume — because the two time dimensions cancel. So it may be added to volume. Try to add a raw flow to a volume and you get:

[dimension-mismatch] cannot apply '+' to incompatible dimensions m^3 and m^3/s

Units are a compile-time contract only: they are checked and then erased, so the generated ST/Rust is byte-for-byte identical whether or not you annotated them. They cost nothing at runtime and catch a whole category of engineering mistakes before the code ever runs.