feat(cosim): reg_init register value-injection ($deposit at t0) (#108)

[robtaylor]

Summary

Implements #108 — reg_init register value-injection for cosim — and along the way fixes a pre-existing panic on SRAM-less cosim designs.

A new reg_init array in the testbench JSON deposits a definite value into chosen registers at tick 0 with $deposit semantics: the seed clears the power-up X-mask, then the design's own logic drives the register normally. It is not force — applied once, so a CDC crossing register carries real protocol data after t0 instead of being pinned to the seed (which would write zeros across the handshake).

This is the register sibling of sram_init and the fix path the maintainer root-caused in #102: depositing definite values on the unreset Hazard3 CDC launch registers (hazard3_apb_async_bridge.src_paddr_pwdata_pwrite / dst_prdata_pslverr) clears the conservative-X poison so X-aware cosim of debug-loaded firmware can proceed. It composes with the x-assert detection work (#106) — inject at the source, assert !$isunknown at the sink.

"reg_init": [
    { "name": "unreset_count", "value": 5, "width": 4 }
]

Implementation

• RegInitEntry { name, value, width } in TestbenchConfig (cosim-only — the sim path takes initial state from the VCD).
• resolve_to_input_state_pos (trace_signals.rs): resolves a register name to its DFF Q slot in input_map. Two subtleties that made bus bits and output-aliased registers resolve:
  • input_map is keyed by the bare aigpin (dff.q from add_aigpin), whereas pin2aigpin_iv is iv-encoded (aigpin << 1 | invert) — recover the bare aigpin with >> 1.
  • Scan all pins on the net, not just the first: the DFF Q driver pin isn't guaranteed to sort first.
  • Shared candidate→netid preamble factored out into resolve_net_id (also used by resolve_to_state_pos).
• Deposit writes the value and clears the X-mask in both state slots, so it survives state_prep's per-edge output→input copy (a DFF Q is sequential state, not re-driven by the BitOp schedule like primary inputs are).

Bonus fix — cosim on SRAM-less designs

cosim on a design with zero SRAM panicked: new_buffer(0) returns a nil MTLBuffer whose .contents() is null (foreign-types asserts non-null). The SRAM data buffer is now sized to max(1) word, matching the X-mask shadow buffer. This was never caught because the xprop_demo CI guard only exercised the sim path; this PR adds the first cosim coverage of a zero-SRAM design.

Testing

• Regression (CI + tests/xprop_cosim/): cosim A/B on the same SRAM-less design — without reg_init the unreset counter stays X (q_unreset = x); with a reg_init deposit on unreset_count, q_unreset reads known 0/1. New check.py reg-init mode (the inverse assertion of xprop mode).
• Verified locally: deposit makes q_unreset toggle 1,0,1,0… from the seed — known, and not pinned (proving $deposit, not force).
• 11 trace_signals unit tests pass; clean Metal build; /simplify run over the diff.

Notes / decisions

• width 1 (or omitted) → bare name; width > 1 → name[0]..name[width-1] resolved per-bit (synthesis scatters bus bits to non-contiguous state positions).
• Registers wider than 64 bits deposit bits ≥ 64 as 0 (documented) — exactly the "clear a wide unreset register to a definite 0" case the cosim --xprop: JTAG-DM firmware load writes no SRAM (debug-load path reads X) — not a read-mask bug #102 launch registers need.

Closes #108.

[robtaylor]

Field-testing this on a Hazard3 DTM+DM netlist surfaced a reg_init resolver gap worth fixing before merge — and I think the clean fix is parity with xsources/xroots (#109) rather than a local patch.

The bug

reg_init panics when a targeted register has a bit that synthesis
constant-folded:

thread 'main' panicked at src/sim/cosim_metal.rs:2712:21:
reg_init: cannot resolve register 'r[0]' to a DFF state slot
          (not a register, or name not found in netlist)

Concretely it hit hazard3_apb_async_bridge.dst_prdata_pslverr: 32 of its 33
bits are DFFs, but bit 0 (pslverr, never asserted by the DM) folds to
assign dst_prdata_pslverr[0] = 1'b0. reg_init resolves
src_paddr_pwdata_pwrite (all-DFF) fine but aborts the whole run on
dst_prdata_pslverr[0].

Minimal synthetic repro (Apache-2.0, ~30 lines, no external deps)

module reginit_constbit (input wire clk, en, input wire [2:0] din,
                         input wire [3:0] mask, output wire [3:0] dout);
    reg [3:0] r;
    always @(posedge clk) if (en) r <= {din, 1'b0};  // r[0] folds to constant
    assign dout = r & mask;                           // comb use keeps `r` named
endmodule

Synth to AIGPDK → r[3:1] are DFFs, r[0] is assign r[0] = 1'b0. Then
"reg_init": [{ "name": "r", "value": 0, "width": 4 }] panics on r[0].
(Happy to drop the full tests/reginit_repro/ — .v + synth.tcl +
sim_config.json + run.sh — wherever it's useful.)

Root cause + suggested fix (parity, not a skip-patch)

resolve_to_input_state_pos iterates every declared bit 0..width-1 and
requires each to be a DFF-Q slot. But xsources/xroots resolve the same
register without complaint, because they enumerate the register's DFF-Q
bits and never reference the constant bit.

So rather than a local "skip constant bits" patch, reg_init should reuse the
DFF-Q enumeration xsources already performs (same crate, Rust):

• resolve name → the set of DFF-Q state slots backing its bits;
• seed those, skip bits with no DFF (constant-folded → already definite);
• optionally debug-log skipped bits.

That gives parity by construction: anything xsources/xroots can name,
reg_init can seed — and the two stop disagreeing about the same netlist.

Explicitly out of scope

Registers the optimizer dissolved entirely (resource-shared/merged so the
net name vanishes — not just one bit constant-folded) can't be resolved by
name by reg_init or xroots; that needs real synthesis provenance
(berkeley-abc/abc#487 +
yosys plumbing) and is a separate goal from this parity fix.

(Aside: the field test also showed reactive cosim --xprop now loads the
debug-loaded register correctly on its own — data0_obs resolves definite —
so this particular case no longer needs reg_init; but the resolver gap is
worth fixing for the general primitive. Refs #108.)