pyrope

name	pyrope
description	Write and check Pyrope (LiveHD's HDL). Use when creating or editing .prp files, translating Verilog to/from Pyrope, or answering Pyrope syntax questions.

Writing Pyrope

Pyrope is a hardware description language: every construct elaborates to wires, muxes, flops, and memories. This file is the working subset needed to generate correct code. The full spec lives in ~/projs/docs/docs/pyrope/ (chapters 00–13; 01b-quick_intro.md is the human-oriented condensation of this skill). Always verify generated code with lhd (last section).

Ground rules

• Comments are // only. ; is the same as a newline. No variable shadowing, anywhere.
• Every declaration starts with a kind keyword — data: const / mut / wire / reg; lambda: comb / pipe / mod / fluid. Prefix modifiers: comptime, pub. Assignment prefixes: wrap, sat. stage[N] is a mod-only declaration modifier.
• Every data declaration needs = value:
  • a concrete value (0, false, "", (x=1)) — the normal case
  • nil — invalid / "no value yet"; reading it is an error; the default for tuples; reg x = nil declares a register with no reset; wire x = nil forward-declares an as-yet-undriven net (see Wire below)
  • 0sb? / 0ub? / 0ub10??01 — unknown bits (Verilog x); a valid integer value that x-propagates (0sb? + 1 == 0sb??, 0sb? | 1 == 1)
  • There is no bare ?, no _ default, and no 0b prefix (write 0ub/0sb explicitly).
• comptime must be written explicitly (comptime const SIZE = 16). Uppercase naming carries no comptime meaning.
• Integers are unlimited-precision signed. u8, i4, unsigned, int(min=0, max=300) are range constraints on that one type (u<N> max is 2^N−1). 1K == 1024, also M/G/T.
• bool and int never mix: if x != 0 {}, casts int(true), boolean(v#[3]). and/or/implies/not are boolean-only (short-circuit); & | ^ ~ ~& ~| ~^ are bitwise integer ops. There are only easy % (modulo power 2) and no exponent op.
• Precedence is shallow — parenthesize: 3 & 4*4 is a compile error; write 3 & (4*4). Comparisons chain in one direction (a <= b < c).

Lambdas (the only functions)

kind	contract
comb	Pure combinational, zero cycles. No reg (only ::[debug] state). ref args allowed (acts as an implicit output, still combinational). Inlined when not fully typed.
pipe[N]	Fixed latency N > 0: every output lands exactly N cycles after its inputs; never a comb input→output path. A feedback reg is state (adds no latency); an unconditionally-written feedforward reg is a pipeline stage counted in N. A conditional write ⇒ state register.
pipe[A..=B] / bare pipe	Latency range / fully flexible; the caller picks via stage[N]. pipe calls are only legal inside mod.
mod	No constraints (Mealy, Moore, orchestrator). Every output declares its landing cycle at the interface: -> (x:u8@[2], y:u8@[0]). @[0] = comb feedthrough (legal in mod, forbidden in pipe); @[] = unconstrained opt-out; omitting @[...] is a compile error. Registered output: -> (reg count:u8@[0]) — the q is the output.
fluid	Transactional valid/retry handshakes (.[valid], .[retry], .[fire]). Callable only from mod/fluid. (TBD: parses only, no lowering.)

comb add(a:u8, b:u8) -> (r:u9) { r = a + b }
pub comb get5() -> (v) { v = 5 }       // pub = importable from other files

Outputs — always declared by name in -> (...); the clause is mandatory (-> () for none); only self-methods may omit it. The body assigns the outputs — a trailing bare expression does nothing. return is a terminator only: return X is a syntax error. Assign first, then return (for a conditional early exit, wrap it: if cond { return }). Callers get a named tuple (r.next); a single-output tuple auto-unwraps. Destructuring binds by name — const (b, c) = f(...) (order irrelevant); rename with (x=f.b) = f(...). Unnamed RHS tuples destructure positionally.

Calls — parentheses always (noarg()); a bare lambda name is a value (higher-order), never a call. Name every argument: f(a=1, b=2). Unnamed is OK only when: the lambda has a single argument, the passed variable's name equals the parameter name, or the types are unambiguous. UFCS x.f(args) works only when f declares self as first parameter; self binds positionally, never f(self=...); ref self needs a mut receiver. ref must be written at the declaration and the call: comb inc(ref a) -> () { a += 1 } … inc(ref y).

Overloading/generics — overload by gathering: const add = [add1, add2]; a call dispatches (comptime) to the FIRST gathered lambda that can accept it (tuple order, no ambiguity error; no-match = compile error). "Can accept" uses the SAME argument rules as a direct call (same-kind positional args must still be named). Generics: comb f<T>(a:T, b:T) -> (r) — a per-call-site type-macro expansion. Bind explicitly (f<u8>(a=1, b=2), one type per generic, in order) or let T infer (unify) from the actuals' declared types; bare literals leave T as the unbounded kind (f(a=1, b=2) → T = int). A generic mod/pipe mints one module per binding (madd__u8_u8). Both overloading and generics are enabled — emit them when they fit. They are still lightly tested (generics more than gathered-set dispatch), so if a call hits tolg-error: call to '<set>' has no hardware lowering or a wrong dispatch, that is a LiveHD bug to report, not a reason to avoid the construct. Comptime parameters live in the [...] slot: comb g[n:int=1](x) -> (r), called as g[3](x=2). Varargs (...args) gather leftovers (args[i] / args.NAME). There is no placeholder lambda sugar — no _/_0/_1 shorthands; pass a named comb (mymap.each(inc)).

Constructor — init is the only implicit hook: a comb, run once at construction (mut x:T = v or explicit T(v)); overload via const init = [fn1, fn2]. There are no getter/setter hooks — after construction, all reads/writes are structural. Extension methods can be added later: Typ.double = some_comb.

Tuples, arrays, types

mut p = (mut x:u8 = 0, mut y:u8 = 0)   // named fields use a kind keyword
const iface = (
  ,mut value:u8 = 0
  ,comb read(self) -> (v:u8) { v = self.value }
  ,comb inc(ref self)        { wrap self.value += 1 }
)
mut t = (1, 2, 3)                      // positional entries are bare values
mut arr = [1, 2, 3]                    // [] = array: all entries same type

• Access: p.x, t[0], a['r1']. Integer indices select positional entries only; named fields are name-access only.
• (...a, b=2) splices in place (duplicate name = error).
• A selector [...] takes ONE expression (int, string, range, or a conditional) — a[0,1] is not allowed.
• Mutability: outer const freezes every field; inner const pins one field of a mut tuple.
• type Foo = (mut color:string = "", mut value:i33 = nil) declares a type. Complicated lambda types must be declared ahead with type, never inline.
• Structural typing operators: does (a covers b's structure; u32 does u16), equals, case (does + defined-value match; nil/0sb? wildcards), is (nominal), has (field), in (membership). Negate with not (...) — there are no !has/!in/!and forms.
• :Type annotations only at declaration sites. Check elsewhere with cassert(x does T); convert with constructor calls: u8(x), int(s), string(n). There is no _ wildcard — outputs must be named (comb() -> (res:int)), and type-shape operands write the bare type (x does u8, not x does _:u8).
• Enums: enum State = (Idle, Run, Done) — one-hot encoding by default; any explicit value (or an :int type) switches to sequential; hierarchical enums nest. Always compare against names (state == State.Idle), never raw integers. Casts: string(E.a), E("a").
• Ranges: 0..=7, 0..<8, 2..+3, optional step 2; ascending only. Open ends in selectors (a[1..]); negative = distance from the end (b#[1..=-2]).

Bit selection and reduction

v#[3]            // bit 3            v#[1..=4]    // bit slice (zext result)
v#sext[0..=2]    // sign-extended slice
v#|[..]  v#&[..]  v#^[..]  v#+[..]   // or/and/xor-reduce, popcount (lower to int 0/1)
trans#[0] = v#[1]   // LHS bit assign; every dest bit driven exactly once
const onehot = 1 << (1, 4, 3)        // == 0ub01_1010

#[] is bits, [] is tuple/array elements, @[N] is a cycle typecheck — never mix them. Bit concatenation = explicit per-range LHS assigns into a typed destination (no {a,b} form).

Statements

• if c { } elif { } else { } — also an expression form. unique if asserts mutually exclusive conditions (one-hot mux; replaces tri-state).
• match — parallel-unique case (implicit assume of mutual exclusivity and exhaustiveness), NOT priority. The else arm is optional: omit it when the arms already cover the whole key space (e.g. every value of a bounded uN/sN selector). An omitted else behaves like an unreachable else { assert(false) } — it lowers to a don't-care (the __hotmux none-of slot is never selected), and a constant selector matching no arm yields nil (exactly like an if/elif chain with no else). Add an explicit else only for a real catch-all value or a cassert(false). A bare value means ==. Arms: == v, in (2,3), case (a=1), < 5, else. If two arms can match the same value (e.g. == 0 and < 8), the lowered __hotmux gets a non-one-hot select and the output is X — for priority/overlapping conditions use if/elif/else. The selector can declare locals: match const t = f(); t { ... }.
• There are no when/unless trailing gates (removed from the language). All gating — comptime or runtime — uses an if block: if DEBUG { assert(x) }, if enable { count += 1 }. A comptime-false condition folds the block away entirely.
• Loops for i in 0..<N {}, while, loop are fully unrolled — bounds must be comptime. break/continue work. Iterate tuples (for (i, v) in t.enumerate()), mutate via for x in ref t { x += 1 }. Build tuples by accumulating: mut acc:[] = nil … acc ++= v (there are no comprehensions).
• Code blocks { ... } are expressions evaluating to their last expression (mut a = {mut d=3; d+1} + 100); they may not have outer side effects.
• wrap / sat prefix every narrowing assignment (wrap c = a + 1, sat d += 1); an unannotated narrowing assignment is a compile error.

Registers and timing

reg counter:u8 = 0            // '= 0' is the RESET value (nil ⇒ no reset)
const q   = counter           // bare name reads current q (snapshot first if needed)
counter += 1                  // write with plain =/+=; lands at the cycle boundary
const old = past[2](counter)  // value 2 cycles ago (compiler inserts 2 flops) (TBD: not lowered yet)

• There is no @[-1]/@[1] register indexing — those are pre-3.0 forms. The old .[defer] end-of-cycle read no longer exists — use a wire (below) for next-state reads and backward edges.
• Register attributes at declaration: reg c:u8:[clock_pin=ref clk2, reset_pin=ref rst2, sync=false, posclk=false, retime] = 3. _pin attributes connect wires → they need ref (a comptime constant like reset_pin=false doesn't). sync defaults true (async reset = sync=false); retime lets synthesis move/merge the flop.
• Multi-cycle reset code: assign a lambda by name (no parens): reg arr:[1024]Tag = my_reset_mod.

Wire — single-driver combinational nets

wire declares ONE combinational net with exactly one driver, modeled on a Verilog continuous-assign / net. Unlike mut (whose value is the last write in program order, where a read-before-write is an error), a wire may be read before its driver appears textually — every read observes the single resolved driver, regardless of statement position. This is the construct for closing interconnect rings and feeding a register's next-state into a same-cycle consumer (it replaces the removed .[defer] read).

reg counter:u32 = 0
wire nx:u32 = nil      // forward-declared, as-yet-undriven net
nx = counter + 1       // the ONE driver (may appear later in program order)
counter = nx           // registered write
const also = nx + 1    // same-cycle consumer reads the same net

• Exactly one driver. A mux (an if/match expression, or mutually-exclusive conditional writes) counts as one driver. A second unconditional assignment, a never-driven net, or an incompletely-driven net (driven on some paths only) is a compile error.
• wire removes textual ordering only, not cyclic dataflow: a net that combinationally feeds itself is a real comb loop and is rejected (SCC check). A ring is legal only when a reg breaks it.

Pipelining inside mod

pipe mul(a:u16, b:u16) -> (c:u32) { c = a * b }
pipe add(a:u32, b:u32) -> (c:u32) { wrap c = a + b }

mod mac(in1:u16, in2:u16) -> (out:u32@[4]) {
  stage[3] tmp     = mul(a=in1, b=in2)            // RHS delivered 3 cycles later
  stage[3] in1_d   = in1                          // pure 3-cycle delay
  stage[1] out@[4] = add(a=tmp@[3], b=in1_d@[3])  // all alignments typechecked
}

• stage[N] — declaration modifier, mod-only, N > 0 (stage[0] is an error; plain = is same-cycle). Also stage[A..=B] and stage[] (tool picks). N is the latency of the RHS, relative.
• x@[N] — pure cycle typecheck (absolute cycle counted from the lambda inputs), legal on LHS and RHS, in mod and pipe bodies. It never inserts flops; a mismatch is a compile error. @[] opts out.
• A bare/ranged pipe call must be consumed by stage[N]. There is no implicit alignment: to mix values from different cycles, delay explicitly with stage[N] x = v or past[n](v).
• Accumulator over a pipelined unit (state regs read q at their home stage):

mod accum(in1:u16, in2:u16) -> (out:u32@[3]) {
  reg total:u32 = 0
  stage[3] tmp = mul(a=in1, b=in2)
  wrap total = total + tmp@[3]
  out = total
}

Memories

reg mem:[256]u32 = 0       // async mem: 0-cycle read, fwd by default, reset to 0
reg mem2:[16]i8 = nil      // no reset
mut scratch:[] = nil       // plain array: no persistence across cycles
mut m2:[4][8]u8 = 13       // multi-dimensional, row-major

Read mem[addr]; write if we { mem[addr] = din }. Indices can be enum- or range-constrained (mut x:[X]u3, mut s:[-8..<7]u3). A synchronous SRAM is an async mem with flopped address or flopped data, or a direct stage[1..<inf] res = __memory(cfg) RTL instantiation. Physically pooled memories are shared with regref("mem_pool/buf0") — behaves like a local reg (reads q, sequential by construction, one functional writer globally).

Verification

• assert(...), cassert(...) (must hold at compile time), optimize(...) (assert + lets synthesis assume it), requires(...)/ensures(...) (lambda pre/post), cover(...), covercase(GRP, cond, "msg"). Always parenthesized; optional trailing message. always_assert etc. also check during reset/invalid.
• test "name {}", arg { ... } blocks: step [n], waitfor(ref cond_var, timeout=N), peek/poke("path", v), force/release, spawn name = { ... } with join/cancel, sigref("top/a/b") (debug-only, any signal) and regref (any register in debug contexts).
• Temporal library (debug-only except past): past[n](x), next[n](x), rose[w](x), fell, stable, changed, eventually[1..=32](x), always[w](x); attribute sugar sig.[rising] / .[falling] / .[changed]. SVA $rose(req) |-> ##[1:10] $rose(ack) becomes assert(rose(req) implies rose[1..=10](ack)).
• Random: x.[rand] (simulation) / x.[crand] (comptime). lec(gold, impl) checks combinational equivalence.
• puts("a={a} b={}", b) (interpolation in double quotes, queued to end of cycle, allowed in comb), print, format, cputs (compile-time print).

Files, visibility, instantiation

• A file's top scope is setup code, run once. Only pub top-scope lambdas, types, and constants can be imported: const lib = import("file") / import("proj/file"). pub mut and pub reg are compile errors — use regref for cross-hierarchy registers.
• Pin the generated netlist/Verilog module name with the lg attribute: pub comb my_top::[lg="chip_top"](...) — pub-only, comptime string; the import key stays my_top (only the lgraph/module artifact is renamed, and it becomes importable as import("lg:chip_top")). lg on a non-pub or non-lambda errors; two units pinned to the same name are diagnosed. Never invent pub("name").
• A fully typed pipe/mod lowers to a module; an untyped one is a per-call template (every actual feeding it must have a declared type).
• Do not instantiate conditionally to "save hardware": a lambda called inside if/match behaves as if inlined there with valid-gated inputs. Structure the design with unconditional calls and mux the results when that is the intent.

Canonical patterns

// Counter — three spellings
mod counter1(enable:bool) -> (value:u8@[0]) {
  reg count:u8 = 0
  value = count
  if enable { wrap count += 1 }
}
mod counter2(enable:bool) -> (reg count:u8@[0]) {  // registered output (q is the output)
  if enable { wrap count += 1 }                    //   — does NOT lower yet (home -1); prefer counter1
}
pipe[1] counter3(enable:bool) -> (reg count:u8) {  // pipe state output: home stage N-1
  if enable { wrap count += 1 }
}

// FSM — names are case-insensitive, so the reg can't be `state` (collides with
// the `State` type); use `st`. The `else` here is the Done/catch-all arm.
enum State = (Idle, Run, Done)

mod fsm(start:bool, fin:bool) -> (busy:bool@[0]) {
  reg st:State = State.Idle
  busy = st == State.Run
  match st {
    == State.Idle { if start { st = State.Run  } }
    == State.Run  { if fin   { st = State.Done } }
    else          { st = State.Idle }
  }
}

// 1-cycle dual-port RAM
pipe[1] dpram(we:bool, waddr:u8, raddr:u8, wdata:u32) -> (rdata:u32) {
  reg mem:[256]u32 = 0
  if we { mem[waddr] = wdata }
  rdata = mem[raddr]
}

Verilog ↔ Pyrope quick map

Verilog	Pyrope
module m(...)	mod m(...) -> (out:T@[N]) (or pipe[N]/comb)
input [7:0] x / output [7:0] y	x:u8 input / y:u8@[N] mod output
reg [7:0] x + reset	reg x:u8 = 0
reg [7:0] x / procedural blocking =	mut x:u8 = 0
wire [7:0] x / continuous assign	wire x:u8 = ... (single-driver net)
x <= y (non-blocking)	x = y on a reg (registered write)
parameter/localparam N = 8	comptime const N = 8
always @(posedge clk) / @(*)	implicit — reg vs mut
case (x) ... endcase	match x { == v {...} else {...} }
x[6:3]	x#[3..=6]
{a, b} concat	per-range LHS bit assigns into a typed dest
4'b10x? / x value	0ub10?? / 0sb?
one-hot mux / tri-state bus	unique if (lowers to __hotmux)
SVA assertion	assert(... implies eventually[w](...))
testbench initial	test "name" { ... step ... }

Gotchas — check before emitting code

1. return X is always wrong — assign the named output, then bare return.
2. Outputs must be named in -> (...); no positional returns; clause is mandatory (except self methods).
3. match else is optional — omit it when the arms exhaustively cover the selector (an omitted else is an unreachable assert(false) / don't-care). Add else only for a real catch-all.
4. when/unless trailing gates no longer exist — count += 1 when enable is a syntax error; write if enable { count += 1 }.
5. .[defer] no longer exists — use a wire (single-driver net, readable before its driver) for backward edges and same-cycle next-state reads.
6. @[N] never inserts flops (pure check); stage[N] inserts them (mod-only). pipe calls need stage[N] at the call site.
7. A mod output without @[N]/@[] at the interface is a compile error; a pipe[0] or a comb path through a pipe is illegal (use comb).
8. No bool/int mixing: if 5 {} is a type error → if 5 != 0 {}. Reduce ops (x#|[..]) return int 0/1, not bool.
9. Narrowing assignments need wrap/sat; widths come from types (int(min,max)/uN), never from a :[max=...] attribute set.
10. Loop bounds must be comptime (loops unroll). No runtime loops, no comprehensions.
11. 0b1010 is invalid — 0ub1010/0sb1010. Bare ? and _ initializers no longer exist; use nil or 0sb?.
12. ++ is tuple/string concat, never arithmetic. #[] bits vs [] elements vs @[] cycles.
13. Name your call arguments (f(a=1, b=2)); UFCS only on self lambdas; ref written at declaration and call.
14. No getter/setter hooks; only init. Reads never invoke code implicitly.
15. _pin register attributes need ref (clock_pin=ref clk); reset value is the = expr initializer; sync=false for async reset.
16. Enum comparisons use names (State.Idle), never the underlying integer.
17. Names are case-insensitive — a variable that is the lowercase of a type collides (enum State + reg state is an error; use reg st:State).

Not yet implemented (avoid emitting)

Valid spec Pyrope that LiveHD does not lower yet (15-tbd.md in the docs is the authoritative list). Do not generate these unless explicitly asked:

• fluid lambdas / valid-retry handshakes (parses only)
• Temporal library: past[n]/next[n]/rose/fell/stable/changed/ eventually/always, .[rising]/.[falling]
• Testbench extras: peek/poke, waitfor, force/release, sigref, spawn/join/cancel (plain test/step works)
• import("prp") stdlib; comptime-computed / inferred-type memory init (reg mem2 = reset_value — literal/scalar init contents DO work); macro= attribute; in-language lec()

Documented forms that still do NOT lower (re-verified against a fresh lhd build 2026-06-21 — upass.tolg errors out; use the workaround):

• Registered-output interface form mod f(...) -> (reg count:u8@[0]) → state register 'count' homes at stage 0 ... requires home -1. Use a body register: mod f(...) -> (count:u8@[0]) { reg c:u8=0; count=c; ... }.
• Hierarchical enums enum E=(,a=(,x,,y), ,b) → read of undefined variable 'x' (nested member names read as scope). Use a flat enum.

Recently fixed — these NOW lower correctly (safe to emit; older builds and earlier revisions of this skill told you to avoid them):

• Reduction operators a#|[..] a#&[..] a#^[..] a#+[..] (popcount) — lower to Verilog (|x)/(&x)/(^x)/adder-tree. Result is still int 0/1, never bool.
• implies as a hardware signal r = p implies q → (~p)|q.
• Tuple/struct-typed ports comb f(ar:(x:u3,y:i4)) -> (p:(q:u8,r:u8)) — the SSA flatten is automatic; reads/writes of the dotted leaves lower.
• Runtime (non-comptime) bit index a#[i], and runtime index into a const-array literal const arr=[..]; arr[i] (lowers to a __hotmux).
• Runtime typecasts int(a<b), u8(x), bool(x) (range-checked, e.g. u8(0x1F0) errors).
• Full-width signed slice i8#[..] (now all bits) and open-ended slice a#[k..] (now keeps the offset) — both were previously silently wrong.

Runtime wrap/sat and enum-typed register resets ARE implemented. Per-range LHS bit-assembly into a reg works (reg r:u12=0; r#[0..=7]=a; r#[8..=11]=b keeps BOTH writes; conditional partial writes compose too) — it USED to drop every write but the last; fixed in upass.ssa (reg set_mask din threading). Covered by the bitset_reg/bitset_mut equiv tests. Imports: import("file") (all pub) or import("file.pub_name") (one entry); directories use slashes; no glob patterns.

Checking code with lhd

lhd is the LiveHD CLI (on $PATH; in a livehd checkout build with bazel build //lhd:lhd → ./bazel-bin/lhd/lhd). It is stateless and deterministic; the exit code is the verdict (0 = pass).

lhd compile foo.prp                   # parse + lower + diagnostics (no emit; quick check)
lhd compile foo.prp --top NAME --emit verilog:foo.v --workdir tmp   # full lowering + netlist
lhd scan foo.prp                      # list the file's imports
lhd lsp                               # Pyrope language server over stdio (prplsp wrapper)
# equivalence-check a .prp against a golden .v (module names: prp = file.entity):
lhd lec --impl foo.prp --ref gold.v --impl-top foo.top --ref-top gold --set lec.solver=cvc5
lhd lec --impl foo.prp --ref gold.v --impl-top foo.top --ref-top gold --set lec.solver=lgyosys

lhd lec has two backends and they can disagree: cvc5 reasons on the LGraph directly; lgyosys reasons on the cgen-emitted Verilog — so a cgen bug, or cvc5 k-induction on a wide enum/state reg, or a no-reset flop, makes one pass while the other fails. When a verdict surprises you, get an independent oracle: emit the netlist (--emit verilog) and simulate it against the golden with iverilog/verilator over an exhaustive (small) or random input sweep.

Diagnostics render clang-style on stderr; add --emit diagnostics:PATH for a JSONL stream (fields: severity, code, category, pass, message, span, hint). Triage by category:

• syntax / name / type / bitwidth — the Pyrope source is wrong: fix it.
• unsupported — valid Pyrope that LiveHD cannot lower yet (e.g. reduction ops a#|[..], temporal ops like past[n], fluid lowering — see the not-yet-implemented list above). Rewrite around it for synthesis; do not "fix" correct source. The front-end usually still accepts it (the unsupported diagnostic comes from a later lowering stage).
• internal — a LiveHD bug: reduce to a repro; do not change the source.

The frontend is more permissive than the spec (it may accept stale forms the docs forbid), so passing lhd compile is necessary but not sufficient — follow this skill's rules for style/semantics, and use lhd to catch mechanical errors. Generated module names are file.entity (e.g. cnt.counter); pin them with the lg attribute when a fixed name is needed.