▶ Open this chapter in JupyterLite

Chapter 4 — Modules and Composition

Real designs aren't single combinational expressions or single counters — they're module hierarchies. An ALU contains an adder, a shifter, and a comparator. A SoC contains a CPU, a bus, and a memory controller. This chapter is about how to structure modules in Sparkle.

The two big tools:

1. `declare_signal_state` — names the I/O record of a multi-output module. Instead of returning an anonymous tuple Signal dom (BitVec 8 × BitVec 8), you return a named Signal dom AluOut whose accessors give you .result and .flagsZero by name. Wire names in the generated Verilog follow the field names. 2. `circuit do` + module composition — you call one module from inside another's circuit do block; the synthesiser turns the call into a Verilog module … (…); instance.

import Sparkle
import Sparkle.Compiler.Elab
import Display

open Sparkle.Core.Domain
open Sparkle.Core.Signal

namespace Notebooks.Ch04

4.1 Why anonymous tuples are painful

Suppose you build a half-adder that returns (sum, carry). A bare tuple works for tiny modules:

def halfAdder ... : Signal dom Bool × Signal dom Bool := ...

but caller-site code becomes hard to read:

let (sum, carry) := halfAdder a b   -- which is which?

and the generated Verilog wires get autogenerated names like _gen_t0, _gen_t1 — useless when you're staring at a waveform.

For anything past two outputs, pattern-matching on a tuple is also a synthesis hazard (see Ch 2 §2.3 — Lean erases the destructuring before synthesis runs).

4.2 declare_signal_state — the named record

The macro turns this:

declare_signal_state HalfAdderOut
  | sum   : Bool := false
  | carry : Bool := false

into all of the following at elaboration time:

1. Type alias — HalfAdderOut becomes Bool × Bool (right-nested tuple). 2. Accessor defs:

These use projN! under the hood, so they synthesise to plain wire references. 3. Default value — HalfAdderOut.default : HalfAdderOut is (false, false), paired by the field defaults. 4. `Inhabited` instance — so register-init expressions (Signal.reg HalfAdderOut.default) typecheck. 5. `HalfAdderOut.wireNames : Array String` — the strings ["_gen_sum", "_gen_carry"] the synthesiser uses to name Verilog wires. 6. `HalfAdderOut.fromWires : Array UInt32 → HalfAdderOut` — converts raw simulator wires back into the typed record. 7. `HalfAdderOut.mk` — a named-field constructor:

   HalfAdderOut.mk (sum := xorWire) (carry := andWire)

The whole macro is in Sparkle/Core/StateMacro.lean (~150 lines). It's just sugar — you could write all seven defs by hand.

4.3 Building a half-adder with HalfAdderOut

Instead of returning a bare tuple, we package the outputs as a Signal dom HalfAdderOut. HalfAdderOut.mk takes the two output signals as named fields.

def halfAdder {dom : DomainConfig}
    (a b : Signal dom Bool) : Signal dom HalfAdderOut :=
  HalfAdderOut.mk (sum := a ^^^ b) (carry := a &&& b)

Reading the outputs uses the named-field accessors generated by declare_signal_state. Spell them as HalfAdderOut.sum out, not out.sum — Lean's record-dot syntax tries to look up .sum on the outer Signal type first and fails.

def halfAdderSum {dom : DomainConfig}
    (a b : Signal dom Bool) : Signal dom Bool :=
  HalfAdderOut.sum (halfAdder a b)

def halfAdderCarry {dom : DomainConfig}
    (a b : Signal dom Bool) : Signal dom Bool :=
  HalfAdderOut.carry (halfAdder a b)

4.4 bundleAll! — the lower-level primitive

HalfAdderOut.mk is a thin wrapper over bundleAll!, which takes a list of signals and packs them into the corresponding right-nested tuple type. You'll see bundleAll! in older IP code:

-- old style — bundleAll! by position
def halfAdderOld ... : Signal dom (Bool × Bool) :=
  bundleAll! [a ^^^ b, a &&& b]

It works, it synthesises, but the field names are lost. Prefer declare_signal_state + .mk in your own code.

4.5 A 4-bit ALU

Now we put it together. An ALU takes a 2-bit op, two 4-bit operands, and returns a result + a zero flag.

declare_signal_state AluOut
  | result    : BitVec 4 := 0#4
  | flagsZero : Bool     := false

-- ALU op encoding.
def OP_ADD : BitVec 2 := 0#2
def OP_SUB : BitVec 2 := 1#2
def OP_AND : BitVec 2 := 2#2
def OP_OR  : BitVec 2 := 3#2

def alu4 {dom : DomainConfig}
    (op : Signal dom (BitVec 2))
    (a b : Signal dom (BitVec 4)) : Signal dom AluOut :=
  let isAdd := op === OP_ADD
  let isSub := op === OP_SUB
  let isAnd := op === OP_AND
  let result :=
    Signal.mux isAdd (a + b)
      (Signal.mux isSub (a - b)
        (Signal.mux isAnd (a &&& b) (a ||| b)))
  let zero := result === 0#4
  AluOut.mk (result := result) (flagsZero := zero)

4.5b Sketching the datapath with #mermaid

Before staring at generated Verilog it helps to fix a mental picture of the datapath. #mermaid — provided by xeus-lean and stubbed offline — accepts a flowchart string and renders it inline.

#mermaid "flowchart LR
  A[a : BitVec 4] --> ADD((+))
  B[b : BitVec 4] --> ADD
  A --> SUB((-))
  B --> SUB
  A --> AND((&&&))
  B --> AND
  A --> OR((|||))
  B --> OR
  ADD --> M[mux op]
  SUB --> M
  AND --> M
  OR --> M
  OP[op : BitVec 2] --> M
  M --> OUT[result]
  M --> Z{== 0}
  Z --> ZF[flagsZero]"

4.5c A block-accurate diagram with Sparkle.Display.Diagram

Sparkle.Display.Diagram.blockDiagram renders a Diagram value (nodes + edges, each with column / row coordinates) as inline SVG. Unlike #mermaid it stays inside Lean — useful when the picture is derived from a real datapath value rather than authored as a side artefact. Ch 3 §3.4 introduced the structures; this is the same library, used here for a richer ALU schematic.

def aluDiagram : Sparkle.Display.Diagram.Diagram := {
  nodes := [
    { id := "a",   label := "a",         kind := .port,  col := 0, row := 0 },
    { id := "b",   label := "b",         kind := .port,  col := 0, row := 1 },
    { id := "op",  label := "op",        kind := .port,  col := 0, row := 4 },
    { id := "add", label := "+",         kind := .adder, col := 1, row := 0 },
    { id := "sub", label := "-",         kind := .adder, col := 1, row := 1 },
    { id := "and", label := "&&&",       kind := .andG,  col := 1, row := 2 },
    { id := "or",  label := "|||",       kind := .orG,   col := 1, row := 3 },
    { id := "mux", label := "mux op",    kind := .mux,   col := 2, row := 1, inputs := 4 },
    { id := "z",   label := "== 0",      kind := .const, col := 3, row := 2 },
    { id := "y",   label := "result",    kind := .port,  col := 3, row := 1 },
    { id := "zf",  label := "flagsZero", kind := .port,  col := 4, row := 2 } ],
  edges := [
    { src := "a",   dst := "add" }, { src := "b",   dst := "add" },
    { src := "a",   dst := "sub" }, { src := "b",   dst := "sub" },
    { src := "a",   dst := "and" }, { src := "b",   dst := "and" },
    { src := "a",   dst := "or"  }, { src := "b",   dst := "or"  },
    { src := "add", dst := "mux" }, { src := "sub", dst := "mux" },
    { src := "and", dst := "mux" }, { src := "or",  dst := "mux" },
    { src := "op",  dst := "mux" },
    { src := "mux", dst := "y"   }, { src := "mux", dst := "z"   },
    { src := "z",   dst := "zf"  } ]
}

#eval Sparkle.Display.Diagram.blockDiagram aluDiagram

For this particular module — the ALU we wrote at the top of the chapter — #showDiagram alu4 would produce an equivalent auto-generated picture in one line, no hand-built node list needed. The hand-built version stays useful for one-off teaching figures (different layout, custom labels) where you want full control over the picture.

4.6 Verilog generation

Watch the wire names in the synthesised module — result and flagsZero, not _gen_t0 and _gen_t1.

#synthesizeVerilog alu4

4.6b Module hierarchy — the default is to flatten it

When one def calls another, the generated Verilog inlines the callee's body into the caller — the call site looks like direct assign / always_ff statements, not a module foo (...) instance. This is what most users want when sketching combinational logic: alias-style helpers, one-line wrappers, and typeclass / OfNat machinery shouldn't multiply the module count of every caller.

To opt in to a real Verilog module boundary — when you want a re-usable component to survive into place-and-route as its own compile unit — tag the definition with @[hardware_module].

What you get by default (no attribute)

The same one-cycle latch we'll use as a running example, with no attribute on it, and a parent that chains two copies in series. Because the default is inline, latch8 never appears as its own Verilog module — its body is expanded twice into latch8x2.

def latch8 (x : Signal defaultDomain (BitVec 8))
    : Signal defaultDomain (BitVec 8) :=
  circuit do
    let r ← Signal.reg 0#8
    r <~ x
    return r

def latch8x2 (x : Signal defaultDomain (BitVec 8))
    : Signal defaultDomain (BitVec 8) :=
  latch8 (latch8 x)

#synthesizeVerilogDesign latch8x2

The generated Verilog has one module (latch8x2), with two copies of the latch's always_ff body sitting next to each other inside it. No inst_latch8_* instance, no separate module latch8 (...).

Opting in — @[hardware_module]

Tag the helper to promote it to its own Verilog module:

@[hardware_module]
def latch8mod (x : Signal defaultDomain (BitVec 8))
    : Signal defaultDomain (BitVec 8) :=
  circuit do
    let r ← Signal.reg 0#8
    r <~ x
    return r

def latch8modx2 (x : Signal defaultDomain (BitVec 8))
    : Signal defaultDomain (BitVec 8) :=
  latch8mod (latch8mod x)

#synthesizeVerilogDesign latch8modx2

Now the generated Verilog has two modules:

module latch8mod ( ... );          // child: defined once
  ...
endmodule

module latch8modx2 (               // parent: instantiates latch8mod twice
    input  logic [7:0] _gen_x,
    input  logic       clk,
    input  logic       rst,
    output logic [7:0] out);
  latch8mod _tmp_inst_latch8mod_1 (.clk(clk), .rst(rst), ._gen_x(_gen_x),       .out(_tmp_arg0_0));
  latch8mod _tmp_inst_latch8mod_3 (.clk(clk), .rst(rst), ._gen_x(_tmp_arg0_0),  .out(_tmp_result_2));
  assign out = _tmp_result_2;
endmodule

The two _tmp_inst_latch8mod_* instance names are auto-generated and unique — same module, two physical copies on the chip. Sparkle also auto-routes the parent's clk / rst ports into each child's clock / reset port (you don't write the wiring yourself), and auto-adds those ports to the parent if its children need them.

When to use @[hardware_module]

The hierarchy boundary is a real signal to the back end, not just cosmetic:

uses module boundaries for floorplan / region constraints.

block once and instantiate it many times — important for QoR on big designs.

against its own constraints, then drop it into the parent.

Use @[hardware_module] on:

CPU, an ALU you'll port to other projects, an arbiter, a FIFO).

out-of-context synthesise as its own block.

Skip the attribute (= inline) for:

no hardware identity of their own.

in the generated SV.

Self-documenting inline: @[inline_hardware]

@[inline_hardware] is accepted as a no-op marker for "always inline". Today it has no effect over the default, but it's a clear signal to a future reader that you've thought about the boundary and decided NOT to promote it to a module. Sparkle's own primitive combinators (Signal.map, Signal.mux, Signal.fst, BitVec arithmetic instances, …) carry this tag internally as documentation.

4.7 Theorem — ALU matches a behavioural spec

Over BitVec 4 (16 inputs each side) and 4 ops, the input space is small enough to enumerate exhaustively. We define a behavioural spec in plain Lean and prove the Sparkle implementation agrees on every input.

def aluSpec (op : BitVec 2) (a b : BitVec 4) : (BitVec 4 × Bool) :=
  let r :=
    if op == OP_ADD then a + b
    else if op == OP_SUB then a - b
    else if op == OP_AND then a &&& b
    else a ||| b
  (r, r == 0#4)

The proof is a deliberate pattern: we capture the Sparkle design as a plain Lean function (aluPlain) by sampling the Signal view at one cycle, then decide the ∀-quantified equality across the small input space.

-- Plain-Lean view of the design: lift inputs to constant signals
-- and read the output at cycle 0.
def aluPlain (op : BitVec 2) (a b : BitVec 4) : (BitVec 4 × Bool) :=
  let out := alu4 (dom := defaultDomain)
                  (Signal.lit defaultDomain op)
                  (Signal.lit defaultDomain a)
                  (Signal.lit defaultDomain b)
  let r := AluOut.result out
  let z := AluOut.flagsZero out
  (r.val 0, z.val 0)

example : ∀ op a b, aluPlain op a b = aluSpec op a b := by
  decide

4.8 Exercise — extend the ALU with shift-left

Add a fifth ALU op: SHL shifts a left by b (treating b as a 4-bit shift amount, max 15). You'll need a third bit in op : BitVec 3 and a Signal.mux chain.

Update the spec, prove the new design matches. Reference solution in Solutions/Ch04.lean.

-- TODO: extend the ALU here.

end Notebooks.Ch04