PR: feat: tagma hardware fixture specs, decode projector, and coverage gate #47 - #49
Conversation
metasmile
left a comment
metasmile
left a comment
There was a problem hiding this comment.
Reviewed the Tagma fixtures, decode projector, and coverage gate. Actionable items: add --pull=always to the coverage docker fallbacks, add a comment to the generated SV about the negative-offset case, and reconcile the README validation table with main at merge. The tautology note on tagma_demo_top is informational.
| | Constraint types | 13 (range, even, eq, neq, lt, gt, le, ge, oneof, cross, bitmask, enable_mask, enable_set) | | ||
| | Tests | 92 (73 lib + 14 CLI + 5 structural), all passing | | ||
| | Projector types | 4 (sum, identity, parity, tagma_decode) | | ||
| | Tests | 101 (73 lib + 18 CLI + 5 tagma + 5 structural), all passing | |
There was a problem hiding this comment.
This line will conflict with main's validation table, which the CLI structural integration (already merged) restructured and updated to 97 tests. After merging this branch into that main, the reconciled count is 105 (73 lib + 19 CLI + 5 tagma + 8 structural), and the Coverage gate / Projector types rows should be kept alongside the restructured metrics. Please reconcile the README table at merge time.
There was a problem hiding this comment.
This fixture is a tautology: the 11,172 combinations are exactly the product of the three field ranges, so every combination passes without any constraint. It documents the decoder codomain (and the devlog says so explicitly), but it adds no verification beyond the ranges themselves. Acceptable as documentation; consider dropping it if it ever becomes a maintenance burden.
| crate::spec::ProjectorSpec::Parity { field } => { | ||
| format!("{}[0]", field) | ||
| } | ||
| crate::spec::ProjectorSpec::TagmaDecode { field, base } => { |
There was a problem hiding this comment.
The generated SV computes (code - base) / 588 and (code - base) % 28 on a possibly negative value for code points below the block base. SystemVerilog integer division and modulo semantics for negative operands are tool-dependent, but this assertion module is only exercised on the valid domain, so out-of-domain behavior is irrelevant to the check. A short comment noting that the expression is only meaningful for code >= base would prevent a future reader from "fixing" the negative case.
| EV_SYNTH_BACKEND=yosys LLVM_PROFILE_FILE="$PROFRAW_DIR/ev-ext-%p-%m.profraw" \ | ||
| "$EV_COV" synth --target "$ALL_PASS" >/dev/null | ||
| else | ||
| docker run --rm -v "$(pwd):/workspace" -w /workspace \ |
There was a problem hiding this comment.
The docker fallback runs docker run without a pull policy, so it uses whatever ghcr.io/ssccsorg/ev:latest is cached locally. In CI the runner is fresh and always fetches, but on a machine with a warm docker cache a stale image would silently change the yosys/spike versions used for the external backend runs, making the coverage numbers non-reproducible. Add --pull=always to both docker invocations (or an explicit docker pull step) so the gate is deterministic.
1 participant
Summary
Adds the Tagma hardware verification slice of the syntagma hardware track to ev, per issue #47, plus the decode projector extension of issue #46 (milestone 2).
Changes
tests/fixtures/tagma/tagma_decoder.xif.yaml: decoder input domain contract (65,536 raw, 11,172 valid), pinning the U+D7A3 boundary correction.tests/fixtures/tagma/tagma_demo_top.xif.yaml: demo top output axis space (11,172, all valid).tagma_decodeprojector (issue Tagma decoder execution path verification: ev as an independent channel #46 milestone 2):ProjectorSpec::TagmaDecodeinsrc/spec/mod.rs, evaluator insrc/verify/registry.rspacking the decomposition into the golden-anchor layout offset[28:15] i[14:10] m[9:5] f[4:0], and thesv_projectorarm insrc/synth/mod.rs. The projection of code 0xAC00 + k equals line k ofsyntagma/hw/rtl/golden_anchors.hex(spot values 0x00000000, 0x00008001, 0x00010002 confirmed; full 11,172-domain loop in tests).tests/tagma_fixture.rs(5 lib-level tests incl. projection spot values and SV generation),tests/cli_test.rs(+3),run.shassertions, R4 CLI test un-ignored.scripts/coverage.sh,Makefile coverage,run.sh --coverage,coveragejob inbuild-ev.yml(80% lines/regions, Spike/Yosys/sim backends exercised via local tools or the ev image). Measured 83.35% lines / 82.34% regions at the time of writing.docs/devlog/2026-08-23-tagma-hw-fixtures.md, README fixture table, projectors, coverage gate rows.Validation
cargo test --release: 101 passing (73 lib + 18 CLI + 5 tagma + 5 structural), 1 ignored (the 33M CLI test, tracked by CLI structural integration + CVA6 full struct_enum benchmark verification #42).bash run.sh --code: fmt, clippy, build, test, bench all pass.bash run.sh --coverage: gate passes (82.30% regions / 83.27% lines at HEAD).Related
tests/cli_test.rs,run.sh, and the README validation table with PR for CLI structural integration + CVA6 full struct_enum benchmark verification #42 (CLI structural integration); the R4 test conflict resolves to the CLI structural integration + CVA6 full struct_enum benchmark verification #42 version.