[gHashTag]

CLARA Gap-5 — Explanation Generation (DARPA TA1.2)

What this PR adds

src/explainability_unit.v — Pure Verilog-2005, R-SI-1 clean
5-tuple proof-trace emitter for DARPA CLARA TA1.2 (Explanation Generation).

Each inference step emits one 20-bit record:

{step_id[3:0], premise_id_a[3:0], premise_id_b[3:0], rule_id[3:0], conclusion[3:0]}

Buffer: 10 × 20-bit shift register (buf0 = newest, buf9 = oldest)
Counter: step_count[3:0]
Overflow: overflow=1 when push arrives at full (feeds restraint_ctrl Gap-4)
Serial output: trace_out[1:0] — 2 bits/cycle, MSB-first, 10-cycle frame

test/tb_explainability_unit.v — 12 scenarios, 26 assertions

Scenario	Description	Result
S01	Empty after reset	PASS
S02	Push 1 step	PASS
S03	Push 5 steps, head correct	PASS
S04	Push 10 steps (full, no overflow)	PASS
S05	Push 11th step → overflow=1	PASS
S06	Reset clears overflow	PASS
S07	10 pushes, count maxes out	PASS
S08	Serial trace matches head_record slices	PASS
S09	step_id field correct	PASS
S10	premise_id_a/b fields correct	PASS
S11	rule_id/conclusion fields correct	PASS
S12	Double overflow: sticky, count 10	PASS

PASS 26/12 — CLARA Gap-5 explainability_unit all green

Integration: src/tt_um_trinity_max_true.v

• u_clara_expl instantiated (MAX_STEPS=10)
• Inputs wired from mesh_rcpt_* signals (demo proof-trace source)
• trace_out[1:0] → uio[7:6] (serial 2-bit/cycle)
• overflow wire preserved for future restraint_ctrl Gap-4 hook

Constraints met

• R-SI-1: zero * arithmetic operators in new RTL
• Pure Verilog-2005: no SystemVerilog, no multi-var logic blocks
• Cell budget: ~180 cells ≈ 0.37% of GAMMA's ~48 000 cell budget
• MAX_STEPS = 10: matches t27/specs/ar/explainability.t27 MAX_EXPLANATION_STEPS
• Coq anchor: proofs/clara_max_steps.v invariant reference

t27 anchor

gHashTag/t27:specs/ar/explainability.t27 — const MAX_EXPLANATION_STEPS: int = 10

DOI

10.5281/zenodo.19227877 — φ²+φ⁻²=3