Tagma hw RTL fixture specs: feasible verification YAML specs and plan

[metasmile]

Goal

Deliver the feasible ev verification YAML specs for the four RTL artifacts added in the syntagma hardware track, and a plan that records what the current constraint set can and cannot express. This is the concrete fixture slice of ev issue #46 (Tagma decoder execution path verification), which stays open as the umbrella for the engine extension.

The four artifacts

Artifact (syntagma/hw/rtl/)	Role	Feasible as ev spec today
tagma_decoder.v	Combinational 3-axis decoder, code in [0xAC00, 0xD7A3] to (i, m, f)	Input domain contract only
tagma_demo_top.v	FPGA demo top, registered decoder outputs plus valid LED	Output axis space bounds only
tagma_decoder_tb.v	Exhaustive Verilator testbench (11,172 code points)	Not expressible; ev does not run Verilog
golden_anchors.hex	11,172 packed 29-bit reference vectors	Packed format documentable, decomposition not expressible

Scope

1. Add tests/fixtures/tagma/tagma_decoder.xif.yaml, the input domain contract: 65,536 raw combinations, 11,172 valid. This pins the boundary correction recorded in the syntagma devlog (last valid syllable U+D7A3, not U+D7AF).
2. Add tests/fixtures/tagma/tagma_demo_top.xif.yaml, the output axis space: 11,172 combinations, all valid.
3. Wire both into run.sh fixture assertions and tests/cli_test.rs.
4. Record the plan in docs/devlog/2026-08-23-tagma-hw-fixtures.md: which of the four artifacts map to constraints today, which need the decode projector or an arithmetic constraint (issue Tagma decoder execution path verification: ev as an independent channel #46), and the milestones.

Feasibility boundary

The decoder decomposition (i = offset / 588, m = (offset % 588) / 28, f = offset % 28) requires integer division and modulo by constants. The current 13 constraint types (range, even, eq, neq, lt, gt, le, ge, oneof, cross, bitmask, enable_mask, enable_set) cannot express arithmetic relations between fields, so the functional contract of the decoder and of the golden anchors is not expressible without an engine extension. A naive field-product spec over (offset, i, m, f) parses and runs (124,813,584 combinations under the 1B guard) but verifies nothing, since every combination passes. This is the core finding the plan records.

Acceptance criteria

• ev verify on tagma_decoder.xif.yaml reports 11,172 passed, 54,364 failed.
• ev verify on tagma_demo_top.xif.yaml reports 11,172 passed, 0 failed.
• run.sh --verify and cargo test --release pass with the new assertions.
• The plan devlog states explicitly which artifacts are not expressible with the current constraint set and which extension closes the gap.

References

• ev issue Tagma decoder execution path verification: ev as an independent channel #46: Tagma decoder execution path verification: ev as an independent channel
• syntagma issue PR: feat: make structural enumeration the CLI verify default #42 #48: hw: Tagma decoder RTL, FPGA verification, and standard cell synthesis report
• syntagma verification devlog: docs/devlogs/hw/2026-08-14-verification.md
• golden anchor pattern: issues Cross-verification harness: ev as reference for SSCCS standard experiment golden anchors #25 and SSCCS standard workspace golden anchor CI integration #28, ssccs/poc/baremetal_riscv/sv

[metasmile]

Branch 47-tagma-fixture-specs created from main (f8fba13) and linked to this issue for the fixture specs and plan work.

[metasmile]

Added the CI coverage gate on this branch (commit 53e007d).

Delivered:

• Makefile coverage target: cargo llvm-cov --release with 80% lines and 80% regions thresholds, excluding the environment-gated backends (synth/backends/spike.rs, synth/backends/yosys.rs, synth/sim.rs), which the integration pipeline exercises instead.
• run.sh --coverage mode delegating to make coverage.
• CI job coverage in build-ev.yml: installs cargo-llvm-cov (with RUSTFLAGS reset for the install step) and runs the gate on every push and PR.
• README quick start and validation table updated; plan devlog updated with a Coverage gate section.

Measured on the committed suite with backends excluded: 85.67% lines, 84.72% regions. The failure path was verified locally (99% threshold exits non-zero). The gate pass path and run.sh --code both pass.

[metasmile]

Correction to the coverage gate (commit 798774d): the Spike, Yosys, and simulation backends are no longer excluded from the measurement. scripts/coverage.sh runs the instrumented test suite (cargo llvm-cov --no-report), then exercises the three backends with the instrumented binary (local tools when present, the ev Docker image otherwise), writing profraw into target/llvm-cov-target/ so the final cargo llvm-cov report merges them. The gate now covers the full crate at 80% lines / 80% regions.

Measured locally with all backends merged: 83.35% lines, 82.34% regions (previously 73.92% with the backends at 0%). The backends went from 0% to spike.rs 62.38%, yosys.rs 58.28%, sim.rs 51.85% lines. The CI coverage job logs into GHCR and sets EV_IMAGE so the container runs the backends. Fail-closed: if a backend run cannot execute, the gate fails instead of silently excluding it.