PR: feat: tagma hardware fixture specs, decode projector, and coverage gate #47

.github/workflows/build-ev.yml

@@ -71,3 +71,31 @@ jobs:
             ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:latest \
             -c "cd /workspace && ./target/release/ev simulate --target tests/fixtures/common/all_pass.xif.yaml"
         shell: bash
+
+  coverage:
+    runs-on: ubuntu-latest
+    env:
+      EV_IMAGE: ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:latest
+    steps:
+      - uses: actions/checkout@v6
+
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          components: clippy, rustfmt, llvm-tools-preview
+
+      - uses: Swatinem/rust-cache@v2
+
+      - name: Log in to GitHub Container Registry
+        uses: docker/login-action@v4
+        with:
+          registry: ${{ env.REGISTRY }}
+          username: ${{ github.actor }}
+          password: ${{ secrets.GITHUB_TOKEN }}
+
+      - name: Install cargo-llvm-cov
+        env:
+          RUSTFLAGS: ""
+        run: cargo install cargo-llvm-cov --locked
+
+      - name: Coverage gate
+        run: bash run.sh --coverage

Makefile

@@ -1,4 +1,4 @@
-.PHONY: build test lint fmt check clean
+.PHONY: build test lint fmt check coverage clean
 
 build:
 	cargo build --release
@@ -18,5 +18,12 @@ check:
 	cargo build --release
 	cargo test --release
 
+# Code coverage gate (cargo-llvm-cov via scripts/coverage.sh). The Spike,
+# Yosys, and simulation backends are exercised with the instrumented binary
+# (local tools or the ev image), then merged into the report. Thresholds:
+# 80% lines and 80% regions on the full crate.
+coverage:
+	bash run.sh --coverage
+
 clean:
 	cargo clean

README.md

@@ -59,6 +59,7 @@ them), so Spike never executes them.
 ./run.sh --demo           # Channel demo: cross-verify golden anchors
 ./run.sh --code           # fmt -> clippy -> build -> test (strict)
 ./run.sh --verify         # Full verification including 33M combo fixture
+./run.sh --coverage       # Code coverage gate (cargo-llvm-cov, 80% thresholds)
 ```
 
 Or step-by-step:
@@ -152,12 +153,22 @@ Conditional field assignment — set fields to specified values on trigger:
       - { field: "rs1", value: 5 }
 ```
 
+The tagma_decode projector packs the Tagma Hangul decomposition of a
+field into the golden-anchor layout offset[28:15] i[14:10] m[9:5] f[4:0]:
+
+```yaml
+projector:
+  type: tagma_decode
+  field: "code"
+  base: 0xAC00
+```
+
 ### Built-in types
 
 **Constraints**: `range`, `even`, `eq`, `neq`, `lt`, `gt`, `le`, `ge`,
 `oneof`, `cross`, `bitmask`, `enable_mask`, `enable_set`.
 
-**Projectors**: `sum`, `identity`, `parity`.
+**Projectors**: `sum`, `identity`, `parity`, `tagma_decode`.
 
 All types are extensible via `ConstraintRegistry` and `ProjectorRegistry`.
 
@@ -177,6 +188,8 @@ Valid counts below are the `evaluate_all` results on the committed fixtures
 | `ibex/csr_access.xif.yaml` | Ibex-like CSR encoding | 49,152 | 49,152 |
 | `ibex/rv32imcb.xif.yaml` | Ibex RV32IMCB (ibex_decoder.sv) | 524,288 | 92,160 |
 | `ibex/rv32imcb_imm.xif.yaml` | Ibex RV32IMCB I-type encoding | 65,536 | 55,616 |
+| `tagma/tagma_decoder.xif.yaml` | Syntagma Tagma decoder valid input domain | 65,536 | 11,172 |
+| `tagma/tagma_demo_top.xif.yaml` | Syntagma Tagma FPGA demo output space | 11,172 | 11,172 |
 | `common/all_pass.xif.yaml` | Simple ALU (no constraints) | 1,024 | 1,024 |
 | `common/sample.xif.yaml` | Mixed pass/fail demo | 96 | 12 |
 
@@ -191,7 +204,9 @@ Valid counts below are the `evaluate_all` results on the committed fixtures
 | struct_enum benchmark (same machine, release) | 19.0 ms |
 | Spike backend | C/Rust recheck: 196,608 / 196,608 agree |
 | Constraint types | 13 (range, even, eq, neq, lt, gt, le, ge, oneof, cross, bitmask, enable_mask, enable_set) |
-| Tests | 97 (73 lib + 16 CLI + 8 structural), all passing, none ignored |
+| Projector types | 4 (sum, identity, parity, tagma_decode) |
+| Tests | 105 (73 lib + 19 CLI + 5 tagma + 8 structural), all passing, none ignored |
+| Coverage gate | 80% lines / 80% regions (llvm-cov, all modules incl. Spike/Yosys backends) |
 | Simulation backends | Mock (default), Spike (`EV_SIM_BACKEND=spike`) |
 
 Benchmark methodology and reproducibility: the structural pipeline is the
@@ -244,6 +259,7 @@ Backends are pluggable via environment variables:
 ## Prerequisites
 
 - Rust 1.85+ ([rustup](https://rustup.rs/))
+- cargo-llvm-cov (optional, for `--coverage`; needs the `llvm-tools-preview` rustup component)
 - Python 3 (for channel demo)
 - Yosys (optional, for synthesis)
 - Spike, riscv64-unknown-elf-gcc, riscv-pk (optional, for simulation)

docs/devlog/2026-08-23-tagma-hw-fixtures.md

@@ -0,0 +1,117 @@
+# Tagma hardware RTL fixture specs: feasibility and plan
+
+The syntagma hardware track (syntagma issue #48) delivered four RTL artifacts
+in `syntagma/hw/rtl/`. This devlog records which of the four can be expressed
+as ev verification specs with the current constraint set, which cannot, and
+the milestones that close the gap. The work follows ev issue #46 (Tagma
+decoder execution path verification), which scopes the engine extension this
+plan needs, and delivers the fixture slice under ev issue #47.
+
+## The four artifacts
+
+| Artifact | Role | Feasible as ev spec today |
+|---|---|---|
+| `tagma_decoder.v` | Combinational 3-axis decoder, code in [0xAC00, 0xD7A3] to (i, m, f) | Input domain contract |
+| `tagma_demo_top.v` | FPGA demo top, registered decoder outputs plus valid LED | Output axis space bounds |
+| `tagma_decoder_tb.v` | Exhaustive Verilator testbench over 11,172 code points | Not expressible |
+| `golden_anchors.hex` | 11,172 packed 29-bit reference vectors | Format documentable, decomposition not expressible |
+
+## Delivered fixtures
+
+`tests/fixtures/tagma/tagma_decoder.xif.yaml` models the valid input domain:
+field `code` over all 65,536 16-bit values, constrained by `ge 0xAC00` and
+`le 0xD7A3`. The expected result is 11,172 passed and 54,364 failed, which
+pins the boundary correction recorded in the syntagma verification devlog:
+the last valid syllable is U+D7A3, not U+D7AF, because 0xAC00 + 11171 = 0xD7A3.
+
+`tests/fixtures/tagma/tagma_demo_top.xif.yaml` models the output axis space:
+fields `i` in [0, 18], `m` in [0, 20], `f` in [0, 27], 11,172 combinations,
+all valid. The demo top validity LED uses the same predicate as the decoder
+domain, and its registered outputs are the same decoder function, so this
+fixture documents the codomain rather than adding a new predicate.
+
+Both fixtures are wired into `run.sh` fixture assertions,
+`tests/cli_test.rs`, and `tests/tagma_fixture.rs`.
+
+## Feasibility boundary
+
+The decoder decomposition `i = offset / 588`, `m = (offset % 588) / 28`,
+`f = offset % 28` requires integer division and modulo by constants. The 13
+constraint types (range, even, eq, neq, lt, gt, le, ge, oneof, cross, bitmask,
+enable_mask, enable_set) express relations between field values and constants,
+not arithmetic compositions of fields.
+
+Analytic conclusion, as of milestone 1: the functional contract of the
+decoder, of the demo top outputs, and of the golden anchor decomposition was
+not expressible in the model. The input domain contract and the output axis
+bounds were the largest expressible subsets.
+
+Milestone 2 closes the projection side of that gap: the `tagma_decode`
+projector computes the decomposition and packs it into the golden-anchor
+layout offset[28:15] i[14:10] m[9:5] f[4:0]. The decomposition is now a
+projection, not a constraint: pass/fail still expresses only the domain, and
+the axes are verified by comparing projections to the anchor contract.
+
+A naive field-product spec over (offset, i, m, f) parses and runs under the
+1B combination guard (124,813,584 combinations) but every combination passes,
+so it verifies no property.
+
+Sequential behavior (registered outputs, one-cycle latency) and Verilog
+testbench execution are outside the ev domain, which evaluates combinational
+encoding spaces. The testbench artifact is the reference for expected counts,
+not a spec target.
+
+## Coverage gate
+
+`scripts/coverage.sh`, wired into `run.sh --coverage` and `make coverage`,
+runs the instrumented suite with cargo-llvm-cov, then exercises the Spike,
+Yosys, and simulation backends with the instrumented binary (local tools or
+the ev Docker image), then merges all profraw data and fails the build when
+lines or regions fall below 80%. Measured on the committed suite: 83.35%
+lines and 82.34% regions across the full crate, including the backends. The
+gate runs in the CI coverage job.
+
+## Milestones
+
+Milestone 1 (this branch, delivered): fixture specs, `run.sh` assertions,
+CLI tests, lib-level fixture tests, the CI coverage gate, and this plan.
+
+Milestone 2 (issue #46, delivered on this branch): the `tagma_decode`
+projector, registered in `ProjectorRegistry` with the packed golden-anchor
+output, plus the `sv_projector` arm so generated SystemVerilog preserves the
+layout. Spot and full-domain tests pin the packing (projection of code k
+equals line k of the anchor file).
+
+Milestone 3 (issue #46, next): cross-check the ev projections against
+`syntagma/hw/rtl/golden_anchors.hex` line by line. The projector already
+emits the anchor layout, so this is a direct comparison, following the
+golden-anchor pattern of issues #25 and #28.
+
+Milestone 4 (issue #46, optional): an `ev synth` design-only mode for
+`tagma_decoder.v` so the generic synthesis report comes from the ev Yosys
+backend.
+
+## Verification results
+
+Measured with `ev verify` on the release build, text output:
+
+| Fixture | Total | Passed | Failed |
+|---|---|---|---|
+| tagma_decoder | 65,536 | 11,172 | 54,364 |
+| tagma_demo_top | 11,172 | 11,172 | 0 |
+
+The tagma_decode projections match the golden-anchor contract at the
+boundaries and over the full domain: code 0xAC00 projects to 0x00000000,
+0xAC01 to 0x00008001, 0xAC02 to 0x00010002, and 0xD7A3 to the packed last
+syllable (offset 11171, i 18, m 20, f 27).
+
+---
+
+## References
+
+- ev issue #47: Tagma hw RTL fixture specs: feasible verification YAML specs and plan
+- ev issue #46: Tagma decoder execution path verification: ev as an independent channel
+- syntagma issue #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: ev issues #25 and #28, `ssccs/poc/baremetal_riscv/sv`
+- Tagma whitepaper: https://doi.org/10.5281/zenodo.21302508

run.sh

@@ -8,6 +8,7 @@ set -euo pipefail
 #   ./run.sh --code       # fmt → clippy → build → test (strict)
 #   ./run.sh --fix        # auto-fix → build → test
 #   ./run.sh --verify     # Yosys synthesis + fixtures (binary must exist)
+#   ./run.sh --coverage   # Code coverage gate (cargo-llvm-cov, 80% thresholds)
 #   ./run.sh --demo       # Channel demo: ev ↔ SSCCS POC golden anchors
 #   ./run.sh --help
 #
@@ -21,7 +22,7 @@ EV_IMAGE="${EV_IMAGE:-ghcr.io/ssccsorg/ev:latest}"
 VERIFY_FAILED=0
 
 # Pre-process: auto-fmt for all build modes except --help and --demo.
-if [[ "${1:-}" != "--help" && "${1:-}" != "-h" && "${1:-}" != "--demo" ]]; then
+if [[ "${1:-}" != "--help" && "${1:-}" != "-h" && "${1:-}" != "--demo" && "${1:-}" != "--coverage" ]]; then
     cargo fmt --all
     cargo clippy --fix --allow-dirty 2>&1 || true
     cargo fix --allow-dirty 2>&1 || true
@@ -181,6 +182,8 @@ verify_large_fixtures() {
     _timed "ibex custom alu fixture (524k combos)" $EV verify --target "tests/fixtures/ibex/alu_ext.xif.yaml" 2>&1 | grep -E '(target:|total:|passed:|failed:)' || true
     _verify_check "ibex rv32imcb encoding"      92160  432128 "tests/fixtures/ibex/rv32imcb.xif.yaml"
     _verify_check "ibex rv32imcb imm ops"       55616   9920  "tests/fixtures/ibex/rv32imcb_imm.xif.yaml"
+    _verify_check "tagma decoder domain"        11172   54364 "tests/fixtures/tagma/tagma_decoder.xif.yaml"
+    _verify_check "tagma demo top outputs"      11172   0     "tests/fixtures/tagma/tagma_demo_top.xif.yaml"
     echo "=== structural enumeration bench ==="
     cargo bench --bench bench -- "struct_enum/ibex|struct_enum/cva6" 2>&1 | grep -E 'struct_enum|time:' | head -6
 }
@@ -235,6 +238,12 @@ case ${1:-} in
         echo "  Verification passed."
         echo "══════════════════════════════════════"
         ;;
+    --coverage)
+        echo "══════════════════════════════════════"
+        echo "  ev — code coverage gate"
+        echo "══════════════════════════════════════"
+        bash scripts/coverage.sh
+        ;;
     --demo)
         exec bash scripts/demo-ssccs-poc.sh
         ;;
@@ -243,8 +252,9 @@ case ${1:-} in
         echo "  (no arg)   Full pipeline: auto-fix → code → verify"
         echo "  --code     fmt → clippy → build → test (strict)"
         echo "  --fix      auto-fix → build → test"
-        echo "  --verify   Yosys + fixtures (binary needed)"
-        echo "  --demo     Channel demo: ev ↔ SSCCS POC (standalone)"
+        echo "  --verify     Yosys + fixtures (binary needed)"
+        echo "  --coverage   Code coverage gate (cargo-llvm-cov)"
+        echo "  --demo       Channel demo: ev ↔ SSCCS POC (standalone)"
         exit 0
         ;;
     *)

scripts/coverage.sh

@@ -0,0 +1,81 @@
+#!/usr/bin/env bash
+set -euo pipefail
+#
+# coverage.sh: ev code coverage gate (cargo-llvm-cov).
+#
+# Runs the instrumented test suite, then exercises the external-tool
+# backends (Spike, Yosys, simulation) with the instrumented binary so their
+# code is covered, then merges everything and enforces the 80% lines and
+# 80% regions thresholds. The backends run with local tools when present
+# and inside the ev Docker image otherwise.
+#
+# The two-step llvm-cov flow: `cargo llvm-cov --no-report` leaves the
+# profraw files in target/llvm-cov-target/, the external runs append their
+# profraw to the same directory, and `cargo llvm-cov report` merges all of
+# them. The merge glob is target/llvm-cov-target/*.profraw, so external
+# runs must write there (LLVM_PROFILE_FILE below).
+#
+# The whole instrumented build directory is removed before the suite. A
+# stale incremental build after a source change leaks old binary signatures
+# into the merge, producing mismatched-data warnings and distorted coverage
+# (observed after the PR #49 conflict resolution, which dropped the report
+# to ~51% before a full clean restored it).
+#
+# Usage: bash scripts/coverage.sh
+#
+
+cd "$(dirname "$0")/.."
+
+if ! command -v cargo-llvm-cov >/dev/null 2>&1; then
+    echo "ERROR: cargo-llvm-cov not found. Install it with:"
+    echo "  rustup component add llvm-tools-preview"
+    echo "  cargo install cargo-llvm-cov --locked"
+    exit 1
+fi
+
+EV_IMAGE="${EV_IMAGE:-ghcr.io/ssccsorg/ev:latest}"
+EV_COV=./target/llvm-cov-target/release/ev
+ALL_PASS=tests/fixtures/common/all_pass.xif.yaml
+PROFRAW_DIR=target/llvm-cov-target
+COVERAGE_MIN="${COVERAGE_MIN:-80}"
+
+echo "=== coverage: instrumented test suite ==="
+rm -rf "$PROFRAW_DIR"
+cargo llvm-cov --release --no-report
+
+echo "=== coverage: external backend runs (instrumented binary) ==="
+
+# Mock simulation backend, no external tools.
+echo "--- mock simulation ---"
+EV_SIM_BACKEND=mock LLVM_PROFILE_FILE="$PROFRAW_DIR/ev-ext-%p-%m.profraw" \
+    "$EV_COV" simulate --target "$ALL_PASS" >/dev/null
+
+# Yosys synthesis backend, local yosys or the ev image.
+echo "--- yosys synthesis ---"
+if command -v yosys >/dev/null 2>&1; then
+    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 --pull=always -v "$(pwd):/workspace" -w /workspace \
+        -e EV_SYNTH_BACKEND=yosys \
+        -e LLVM_PROFILE_FILE="/workspace/$PROFRAW_DIR/ev-ext-%p-%m.profraw" \
+        "$EV_IMAGE" bash -c "cd /workspace && EV_SYNTH_BACKEND=yosys ./target/llvm-cov-target/release/ev synth --target tests/fixtures/common/all_pass.xif.yaml" >/dev/null
+fi
+
+# Spike simulation backend, local spike + pk + riscv gcc or the ev image.
+echo "--- spike simulation ---"
+if command -v spike >/dev/null 2>&1 && command -v riscv64-unknown-elf-gcc >/dev/null 2>&1; then
+    EV_SIM_BACKEND=spike EV_PK_PATH="${EV_PK_PATH:-pk}" \
+        LLVM_PROFILE_FILE="$PROFRAW_DIR/ev-ext-%p-%m.profraw" \
+        "$EV_COV" simulate --target "$ALL_PASS" >/dev/null
+else
+    docker run --rm --pull=always -v "$(pwd):/workspace" -w /workspace \
+        -e EV_SIM_BACKEND=spike \
+        -e EV_PK_PATH=/usr/local/riscv64-unknown-elf/bin/pk \
+        -e LLVM_PROFILE_FILE="/workspace/$PROFRAW_DIR/ev-ext-%p-%m.profraw" \
+        "$EV_IMAGE" bash -c "cd /workspace && EV_SIM_BACKEND=spike EV_PK_PATH=/usr/local/riscv64-unknown-elf/bin/pk ./target/llvm-cov-target/release/ev simulate --target tests/fixtures/common/all_pass.xif.yaml" >/dev/null
+fi
+
+echo "=== coverage: merged report and thresholds ==="
+cargo llvm-cov report --release --fail-under-lines "$COVERAGE_MIN" --fail-under-regions "$COVERAGE_MIN"
+echo "fixture coverage: tagma decoder 11,172/11,172, tagma demo top 11,172/11,172, cva6 ref 196,608, ibex rv32imcb 92,160"

src/spec/mod.rs

@@ -196,4 +196,23 @@ pub enum ProjectorSpec {
     /// Classify parity of a single axis.
     #[serde(rename = "parity")]
     Parity { field: String },
+    /// Tagma 3-axis decoder projection.
+    ///
+    /// Packs the Hangul decomposition of the field value into the
+    /// golden-anchor layout offset[28:15] i[14:10] m[9:5] f[4:0], with
+    /// offset = code - base, i = offset / 588, m = (offset % 588) / 28,
+    /// f = offset % 28. Returns None for code points outside the valid
+    /// Hangul syllable block, matching the tagma_decoder domain.
+    #[serde(rename = "tagma_decode")]
+    TagmaDecode {
+        /// Field holding the 16-bit Hangul code point.
+        field: String,
+        /// Base of the Hangul syllable block; defaults to 0xAC00.
+        #[serde(default = "default_tagma_base")]
+        base: i64,
+    },
+}
+
+fn default_tagma_base() -> i64 {
+    0xAC00
 }