From 811cd6c3ae3cdfa073a84a68f2513942e94e0a00 Mon Sep 17 00:00:00 2001
From: TH Lee <lee@ssccs.org>
Date: Sun, 23 Aug 2026 12:45:48 +0200
Subject: [PATCH 1/9] feat: add tagma decoder and demo top fixture specs #47

---
 README.md                                    |  4 +-
 docs/devlog/2026-08-23-tagma-hw-fixtures.md  | 97 ++++++++++++++++++++
 run.sh                                       |  2 +
 tests/cli_test.rs                            | 41 +++++++++
 tests/fixtures/tagma/tagma_decoder.xif.yaml  | 40 ++++++++
 tests/fixtures/tagma/tagma_demo_top.xif.yaml | 26 ++++++
 6 files changed, 209 insertions(+), 1 deletion(-)
 create mode 100644 docs/devlog/2026-08-23-tagma-hw-fixtures.md
 create mode 100644 tests/fixtures/tagma/tagma_decoder.xif.yaml
 create mode 100644 tests/fixtures/tagma/tagma_demo_top.xif.yaml

diff --git a/README.md b/README.md
index 6cd2b6f..a7a8f60 100644
--- a/README.md
+++ b/README.md
@@ -176,6 +176,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 |
 
@@ -190,7 +192,7 @@ Valid counts below are the `evaluate_all` results on the committed fixtures
 | Speedup (same-language baseline, this machine) | ~550x |
 | 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 | 92 (73 lib + 14 CLI + 5 structural), all passing |
+| Tests | 94 (73 lib + 16 CLI + 5 structural), all passing |
 | Simulation backends | Mock (default), Spike (`EV_SIM_BACKEND=spike`) |
 
 Benchmark methodology and reproducibility: both pipelines are Rust, the same
diff --git a/docs/devlog/2026-08-23-tagma-hw-fixtures.md b/docs/devlog/2026-08-23-tagma-hw-fixtures.md
new file mode 100644
index 0000000..eb6ebaa
--- /dev/null
+++ b/docs/devlog/2026-08-23-tagma-hw-fixtures.md
@@ -0,0 +1,97 @@
+# 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 and
+`tests/cli_test.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: the functional contract of the decoder, of the demo top
+outputs, and of the golden anchor decomposition is not expressible in the
+current model. The input domain contract and the output axis bounds are the
+largest expressible subsets.
+
+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. The golden anchor contract therefore stays in the
+domain of the Python consistency gate and the Verilator golden testbench
+until the extension lands.
+
+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.
+
+## Milestones
+
+Milestone 1 (this branch): fixture specs, `run.sh` assertions, CLI tests, and
+this plan.
+
+Milestone 2 (issue #46): a decode projector or an arithmetic constraint so
+the decomposition becomes expressible. This is the main engine extension.
+
+Milestone 3 (issue #46): cross-check the ev enumeration against
+`syntagma/hw/rtl/golden_anchors.hex` through 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.
+
+Recommendation: ship Milestone 1 now. Milestone 2 is the prerequisite for any
+functional cross-check inside ev.
+
+## 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 |
+
+---
+
+## 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
diff --git a/run.sh b/run.sh
index fcb1287..c566243 100644
--- a/run.sh
+++ b/run.sh
@@ -182,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
 }
diff --git a/tests/cli_test.rs b/tests/cli_test.rs
index 3fdac06..fbc8cad 100644
--- a/tests/cli_test.rs
+++ b/tests/cli_test.rs
@@ -152,6 +152,47 @@ fn verify_cva6_xif_mac_fixture() {
     );
 }
 
+#[test]
+fn verify_tagma_decoder_domain_fixture() {
+    let output = Command::new(env!("CARGO_BIN_EXE_ev"))
+        .arg("verify")
+        .arg("--target")
+        .arg("tests/fixtures/tagma/tagma_decoder.xif.yaml")
+        .output()
+        .expect("failed to run ev verify on tagma_decoder fixture");
+    // The decoder domain has 54,364 invalid code points, so the exit code is non-zero.
+    assert!(
+        !output.status.success(),
+        "tagma_decoder fixture should exit non-zero"
+    );
+    let stdout = String::from_utf8_lossy(&output.stdout);
+    assert!(
+        stdout.contains("passed: 11172") && stdout.contains("failed: 54364"),
+        "should report the 11,172 valid syllables: {}",
+        stdout
+    );
+}
+
+#[test]
+fn verify_tagma_demo_top_fixture() {
+    let output = Command::new(env!("CARGO_BIN_EXE_ev"))
+        .arg("verify")
+        .arg("--target")
+        .arg("tests/fixtures/tagma/tagma_demo_top.xif.yaml")
+        .output()
+        .expect("failed to run ev verify on tagma_demo_top fixture");
+    assert!(
+        output.status.success(),
+        "tagma_demo_top fixture should pass"
+    );
+    let stdout = String::from_utf8_lossy(&output.stdout);
+    assert!(
+        stdout.contains("All combinations passed"),
+        "demo top output space should pass entirely: {}",
+        stdout
+    );
+}
+
 #[test]
 #[ignore = "medium: 16K combos via CLI. Use release build or struct_enum for speed."]
 fn verify_cva6_xif_ref_r4_fixture() {
diff --git a/tests/fixtures/tagma/tagma_decoder.xif.yaml b/tests/fixtures/tagma/tagma_decoder.xif.yaml
new file mode 100644
index 0000000..86e4811
--- /dev/null
+++ b/tests/fixtures/tagma/tagma_decoder.xif.yaml
@@ -0,0 +1,40 @@
+# Tagma 3-axis decoder input domain contract.
+#
+# Models the valid input domain of the combinational decoder in
+# syntagma/hw/rtl/tagma_decoder.v: a 16-bit Hangul syllable code point is
+# valid exactly when it falls in [0xAC00, 0xD7A3].
+#
+# Decoder contract (Tagma whitepaper, https://doi.org/10.5281/zenodo.21302508):
+#   code in [0xAC00, 0xD7A3]  (11,172 valid syllables)
+#   offset = code - 0xAC00
+#   i = offset / 588           (initial, 0..18)
+#   m = (offset % 588) / 28    (medial, 0..20)
+#   f = offset % 28            (final, 0..27)
+#
+# ev verifies the domain boundary: exactly 11,172 of the 65,536 16-bit
+# values pass. This pins the boundary correction recorded in the syntagma
+# verification devlog: the last valid syllable is U+D7A3, not U+D7AF
+# (0xAC00 + 11171 = 0xD7A3).
+#
+# The axis decomposition itself requires integer division and modulo by
+# constants, which the current constraint set cannot express. The plan
+# devlog 2026-08-23-tagma-hw-fixtures.md records the extension proposal
+# under ev issue #46.
+#
+# Verification space: 65,536 raw combinations
+# Valid: 11,172 (the Hangul syllable block), Failed: 54,364
+
+target: tagma_decoder
+fields:
+  code:
+    range: [0, 65535]
+constraints:
+  - type: ge
+    field: "code"
+    value: 0xAC00
+  - type: le
+    field: "code"
+    value: 0xD7A3
+projector:
+  type: identity
+  field: "code"
diff --git a/tests/fixtures/tagma/tagma_demo_top.xif.yaml b/tests/fixtures/tagma/tagma_demo_top.xif.yaml
new file mode 100644
index 0000000..098d36d
--- /dev/null
+++ b/tests/fixtures/tagma/tagma_demo_top.xif.yaml
@@ -0,0 +1,26 @@
+# Tagma FPGA demo top output space contract.
+#
+# Models the registered output space of syntagma/hw/rtl/tagma_demo_top.v:
+# the three decoder axes i, m, f. The demo top registers the combinational
+# decoder outputs on the board clock; the axis codomain is exactly the
+# product of the axis ranges, so every valid axis triple is produced by
+# exactly one code point.
+#
+# The validity LED predicate ((code >= 0xAC00) && (code <= 0xD7A3)) is the
+# same boolean condition verified by the tagma_decoder fixture. Sequential
+# behavior (registered outputs, one-cycle latency) is outside the ev
+# verification domain, which evaluates combinational encoding spaces only.
+#
+# Verification space: 19 x 21 x 28 = 11,172 raw combinations
+# Valid: 11,172 (every axis triple is reachable)
+
+target: tagma_demo_top
+fields:
+  i:
+    range: [0, 18]
+  m:
+    range: [0, 20]
+  f:
+    range: [0, 27]
+projector:
+  type: sum

From 46e60a1b7c7182d12a85492c430161a9ac72da8d Mon Sep 17 00:00:00 2001
From: TH Lee <lee@ssccs.org>
Date: Sun, 23 Aug 2026 14:08:30 +0200
Subject: [PATCH 2/9] test: add lib-level tagma fixture tests #47

---
 README.md                                   |  2 +-
 docs/devlog/2026-08-23-tagma-hw-fixtures.md |  4 +-
 tests/tagma_fixture.rs                      | 81 +++++++++++++++++++++
 3 files changed, 84 insertions(+), 3 deletions(-)
 create mode 100644 tests/tagma_fixture.rs

diff --git a/README.md b/README.md
index a7a8f60..1cf1e10 100644
--- a/README.md
+++ b/README.md
@@ -192,7 +192,7 @@ Valid counts below are the `evaluate_all` results on the committed fixtures
 | Speedup (same-language baseline, this machine) | ~550x |
 | 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 | 94 (73 lib + 16 CLI + 5 structural), all passing |
+| Tests | 96 (73 lib + 16 CLI + 2 tagma + 5 structural), all passing |
 | Simulation backends | Mock (default), Spike (`EV_SIM_BACKEND=spike`) |
 
 Benchmark methodology and reproducibility: both pipelines are Rust, the same
diff --git a/docs/devlog/2026-08-23-tagma-hw-fixtures.md b/docs/devlog/2026-08-23-tagma-hw-fixtures.md
index eb6ebaa..a82c97b 100644
--- a/docs/devlog/2026-08-23-tagma-hw-fixtures.md
+++ b/docs/devlog/2026-08-23-tagma-hw-fixtures.md
@@ -30,8 +30,8 @@ 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 and
-`tests/cli_test.rs`.
+Both fixtures are wired into `run.sh` fixture assertions,
+`tests/cli_test.rs`, and `tests/tagma_fixture.rs`.
 
 ## Feasibility boundary
 
diff --git a/tests/tagma_fixture.rs b/tests/tagma_fixture.rs
new file mode 100644
index 0000000..4eab5f9
--- /dev/null
+++ b/tests/tagma_fixture.rs
@@ -0,0 +1,81 @@
+//! Lib-level regression tests for the Tagma hardware fixture specs.
+//!
+//! The CLI tests in cli_test.rs exercise the same fixtures through the
+//! spawned binary, which the coverage instrumentation does not see. These
+//! tests evaluate the fixtures in-process through the public library API,
+//! so the ge/le constraint path, the YAML parse of the hex boundary
+//! constants, and the domain counts are covered by the instrumented suite.
+
+use ev::spec::VerificationSpec;
+use ev::verify::compose::expand_all;
+use ev::verify::evaluate::evaluate_all;
+use ev::verify::registry::{ConstraintRegistry, ProjectorRegistry};
+
+fn load_fixture(path: &str) -> VerificationSpec {
+    VerificationSpec::from_yaml(std::path::Path::new(path))
+        .unwrap_or_else(|e| panic!("failed to load fixture {path}: {e}"))
+}
+
+/// The decoder accepts exactly the 11,172 Hangul syllables in
+/// [0xAC00, 0xD7A3]. The boundary assertion pins the correction recorded in
+/// the syntagma verification devlog: the last valid syllable is U+D7A3, not
+/// U+D7AF (0xAC00 + 11171 = 0xD7A3).
+#[test]
+fn tagma_decoder_domain_boundary() {
+    let spec = load_fixture("tests/fixtures/tagma/tagma_decoder.xif.yaml");
+    let combos = expand_all(&spec).expect("domain expansion must succeed");
+    assert_eq!(
+        combos.len(),
+        65_536,
+        "all 16-bit code points are raw candidates"
+    );
+
+    let results = evaluate_all(
+        &spec,
+        combos,
+        &ConstraintRegistry::default(),
+        &ProjectorRegistry::default(),
+    );
+    let valid: Vec<i64> = results
+        .into_iter()
+        .filter(|r| r.passed)
+        .map(|r| r.combination.values[0])
+        .collect();
+
+    assert_eq!(
+        valid.len(),
+        11_172,
+        "exactly the Hangul syllable block is valid"
+    );
+    assert_eq!(
+        *valid.first().expect("non-empty"),
+        0xAC00,
+        "first valid code point"
+    );
+    assert_eq!(
+        *valid.last().expect("non-empty"),
+        0xD7A3,
+        "last valid code point is U+D7A3"
+    );
+}
+
+/// The demo top output space is the product of the axis ranges: every axis
+/// triple is reachable, so the 11,172 combinations all pass.
+#[test]
+fn tagma_demo_top_output_space() {
+    let spec = load_fixture("tests/fixtures/tagma/tagma_demo_top.xif.yaml");
+    let combos = expand_all(&spec).expect("domain expansion must succeed");
+    assert_eq!(combos.len(), 11_172, "19 x 21 x 28 axis triples");
+
+    let results = evaluate_all(
+        &spec,
+        combos,
+        &ConstraintRegistry::default(),
+        &ProjectorRegistry::default(),
+    );
+    assert_eq!(results.len(), 11_172);
+    assert!(
+        results.iter().all(|r| r.passed),
+        "every axis triple is reachable"
+    );
+}

From 53e007dc07944125aa45ee72ed1c42d2f94b6c82 Mon Sep 17 00:00:00 2001
From: TH Lee <lee@ssccs.org>
Date: Sun, 23 Aug 2026 14:27:14 +0200
Subject: [PATCH 3/9] ci: add llvm-cov coverage gate with 80% thresholds #47

---
 .github/workflows/build-ev.yml              | 19 +++++++++++++++++++
 Makefile                                    | 11 ++++++++++-
 README.md                                   |  2 ++
 docs/devlog/2026-08-23-tagma-hw-fixtures.md | 13 +++++++++++--
 run.sh                                      | 14 +++++++++++---
 5 files changed, 53 insertions(+), 6 deletions(-)

diff --git a/.github/workflows/build-ev.yml b/.github/workflows/build-ev.yml
index 29aa584..45c513a 100644
--- a/.github/workflows/build-ev.yml
+++ b/.github/workflows/build-ev.yml
@@ -71,3 +71,22 @@ 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
+    steps:
+      - uses: actions/checkout@v6
+
+      - uses: dtolnay/rust-toolchain@stable
+        with:
+          components: clippy, rustfmt, llvm-tools-preview
+
+      - uses: Swatinem/rust-cache@v2
+
+      - name: Install cargo-llvm-cov
+        env:
+          RUSTFLAGS: ""
+        run: cargo install cargo-llvm-cov --locked
+
+      - name: Coverage gate
+        run: bash run.sh --coverage
diff --git a/Makefile b/Makefile
index d13156d..311ed2f 100644
--- a/Makefile
+++ b/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,14 @@ check:
 	cargo build --release
 	cargo test --release
 
+# Code coverage gate (cargo-llvm-cov). The Spike, Yosys, and simulation
+# backends are excluded: they require external tools at runtime and are
+# exercised by the integration pipeline instead. Thresholds leave headroom
+# over the measured 85.67% lines / 84.72% regions on the committed suite.
+coverage:
+	cargo llvm-cov --release --fail-under-lines 80 --fail-under-regions 80 \
+		--ignore-filename-regex "synth/backends|synth/sim"
+	@echo "fixture coverage: tagma decoder 11,172/11,172, tagma demo top 11,172/11,172, cva6 ref 196,608, ibex rv32imcb 92,160"
+
 clean:
 	cargo clean
diff --git a/README.md b/README.md
index 1cf1e10..9261cde 100644
--- a/README.md
+++ b/README.md
@@ -58,6 +58,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:
@@ -193,6 +194,7 @@ Valid counts below are the `evaluate_all` results on the committed fixtures
 | 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 | 96 (73 lib + 16 CLI + 2 tagma + 5 structural), all passing |
+| Coverage gate | 80% lines / 80% regions (llvm-cov, backends excluded) |
 | Simulation backends | Mock (default), Spike (`EV_SIM_BACKEND=spike`) |
 
 Benchmark methodology and reproducibility: both pipelines are Rust, the same
diff --git a/docs/devlog/2026-08-23-tagma-hw-fixtures.md b/docs/devlog/2026-08-23-tagma-hw-fixtures.md
index a82c97b..5ba0c3c 100644
--- a/docs/devlog/2026-08-23-tagma-hw-fixtures.md
+++ b/docs/devlog/2026-08-23-tagma-hw-fixtures.md
@@ -57,10 +57,19 @@ 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
+
+`make coverage` runs the instrumented suite with cargo-llvm-cov and fails the
+build when lines or regions fall below 80%. The Spike, Yosys, and simulation
+backends are excluded from the measurement because they require external
+tools at runtime; the integration pipeline exercises them. Measured on the
+committed suite: 85.67% lines, 84.72% regions (backends excluded). The gate
+is wired into the CI coverage job and into `run.sh --coverage`.
+
 ## Milestones
 
-Milestone 1 (this branch): fixture specs, `run.sh` assertions, CLI tests, and
-this plan.
+Milestone 1 (this branch): fixture specs, `run.sh` assertions, CLI tests,
+lib-level fixture tests, the CI coverage gate, and this plan.
 
 Milestone 2 (issue #46): a decode projector or an arithmetic constraint so
 the decomposition becomes expressible. This is the main engine extension.
diff --git a/run.sh b/run.sh
index c566243..64be1b7 100644
--- a/run.sh
+++ b/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
@@ -238,6 +239,12 @@ case ${1:-} in
         echo "  Verification passed."
         echo "══════════════════════════════════════"
         ;;
+    --coverage)
+        echo "══════════════════════════════════════"
+        echo "  ev — code coverage gate"
+        echo "══════════════════════════════════════"
+        make coverage
+        ;;
     --demo)
         exec bash scripts/demo-ssccs-poc.sh
         ;;
@@ -246,8 +253,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
         ;;
     *)

From 798774db87b7f5fc277b6b8c2f34aec1050d78ab Mon Sep 17 00:00:00 2001
From: TH Lee <lee@ssccs.org>
Date: Sun, 23 Aug 2026 14:40:06 +0200
Subject: [PATCH 4/9] ci: cover spike and yosys backends in the coverage gate
 #47

---
 .github/workflows/build-ev.yml              |  9 +++
 Makefile                                    | 12 ++--
 README.md                                   |  2 +-
 docs/devlog/2026-08-23-tagma-hw-fixtures.md | 13 ++--
 run.sh                                      |  2 +-
 scripts/coverage.sh                         | 67 +++++++++++++++++++++
 6 files changed, 90 insertions(+), 15 deletions(-)
 create mode 100755 scripts/coverage.sh

diff --git a/.github/workflows/build-ev.yml b/.github/workflows/build-ev.yml
index 45c513a..0965ab5 100644
--- a/.github/workflows/build-ev.yml
+++ b/.github/workflows/build-ev.yml
@@ -74,6 +74,8 @@ jobs:
 
   coverage:
     runs-on: ubuntu-latest
+    env:
+      EV_IMAGE: ${{ env.REGISTRY }}/${{ env.IMAGE_NAME }}:latest
     steps:
       - uses: actions/checkout@v6
 
@@ -83,6 +85,13 @@ jobs:
 
       - 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: ""
diff --git a/Makefile b/Makefile
index 311ed2f..2b8dc5c 100644
--- a/Makefile
+++ b/Makefile
@@ -18,14 +18,12 @@ check:
 	cargo build --release
 	cargo test --release
 
-# Code coverage gate (cargo-llvm-cov). The Spike, Yosys, and simulation
-# backends are excluded: they require external tools at runtime and are
-# exercised by the integration pipeline instead. Thresholds leave headroom
-# over the measured 85.67% lines / 84.72% regions on the committed suite.
+# 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:
-	cargo llvm-cov --release --fail-under-lines 80 --fail-under-regions 80 \
-		--ignore-filename-regex "synth/backends|synth/sim"
-	@echo "fixture coverage: tagma decoder 11,172/11,172, tagma demo top 11,172/11,172, cva6 ref 196,608, ibex rv32imcb 92,160"
+	bash run.sh --coverage
 
 clean:
 	cargo clean
diff --git a/README.md b/README.md
index 9261cde..ba107a9 100644
--- a/README.md
+++ b/README.md
@@ -194,7 +194,7 @@ Valid counts below are the `evaluate_all` results on the committed fixtures
 | 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 | 96 (73 lib + 16 CLI + 2 tagma + 5 structural), all passing |
-| Coverage gate | 80% lines / 80% regions (llvm-cov, backends excluded) |
+| 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: both pipelines are Rust, the same
diff --git a/docs/devlog/2026-08-23-tagma-hw-fixtures.md b/docs/devlog/2026-08-23-tagma-hw-fixtures.md
index 5ba0c3c..f9eb4f7 100644
--- a/docs/devlog/2026-08-23-tagma-hw-fixtures.md
+++ b/docs/devlog/2026-08-23-tagma-hw-fixtures.md
@@ -59,12 +59,13 @@ not a spec target.
 
 ## Coverage gate
 
-`make coverage` runs the instrumented suite with cargo-llvm-cov and fails the
-build when lines or regions fall below 80%. The Spike, Yosys, and simulation
-backends are excluded from the measurement because they require external
-tools at runtime; the integration pipeline exercises them. Measured on the
-committed suite: 85.67% lines, 84.72% regions (backends excluded). The gate
-is wired into the CI coverage job and into `run.sh --coverage`.
+`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
 
diff --git a/run.sh b/run.sh
index 64be1b7..b9e6159 100644
--- a/run.sh
+++ b/run.sh
@@ -243,7 +243,7 @@ case ${1:-} in
         echo "══════════════════════════════════════"
         echo "  ev — code coverage gate"
         echo "══════════════════════════════════════"
-        make coverage
+        bash scripts/coverage.sh
         ;;
     --demo)
         exec bash scripts/demo-ssccs-poc.sh
diff --git a/scripts/coverage.sh b/scripts/coverage.sh
new file mode 100755
index 0000000..ea05dd6
--- /dev/null
+++ b/scripts/coverage.sh
@@ -0,0 +1,67 @@
+#!/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).
+#
+# Usage: bash scripts/coverage.sh
+#
+
+cd "$(dirname "$0")/.."
+
+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
+
+echo "=== coverage: instrumented test suite ==="
+rm -f "$PROFRAW_DIR"/*.profraw
+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 -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 -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 80 --fail-under-regions 80
+echo "fixture coverage: tagma decoder 11,172/11,172, tagma demo top 11,172/11,172, cva6 ref 196,608, ibex rv32imcb 92,160"

From cc723cf54aa42ef464b158a62aabd5b85b3da1bc Mon Sep 17 00:00:00 2001
From: TH Lee <lee@ssccs.org>
Date: Sun, 23 Aug 2026 15:05:02 +0200
Subject: [PATCH 5/9] ci: harden coverage gate with tool check and threshold
 variable #47

---
 README.md           |  1 +
 scripts/coverage.sh | 10 +++++++++-
 2 files changed, 10 insertions(+), 1 deletion(-)

diff --git a/README.md b/README.md
index ba107a9..be0130f 100644
--- a/README.md
+++ b/README.md
@@ -246,6 +246,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)
diff --git a/scripts/coverage.sh b/scripts/coverage.sh
index ea05dd6..7da833a 100755
--- a/scripts/coverage.sh
+++ b/scripts/coverage.sh
@@ -20,10 +20,18 @@ set -euo pipefail
 
 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 -f "$PROFRAW_DIR"/*.profraw
@@ -63,5 +71,5 @@ else
 fi
 
 echo "=== coverage: merged report and thresholds ==="
-cargo llvm-cov report --release --fail-under-lines 80 --fail-under-regions 80
+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"

From b10eab7ef01f424131afa0723ed239ba765788df Mon Sep 17 00:00:00 2001
From: TH Lee <lee@ssccs.org>
Date: Sun, 23 Aug 2026 15:20:19 +0200
Subject: [PATCH 6/9] feat: add tagma_decode projector for the decoder
 decomposition #46

---
 README.md                                   | 15 +++-
 docs/devlog/2026-08-23-tagma-hw-fixtures.md | 44 ++++++-----
 scripts/coverage.sh                         |  7 +-
 src/spec/mod.rs                             | 19 +++++
 src/synth/mod.rs                            |  9 +++
 src/verify/registry.rs                      | 43 +++++++++++
 tests/cli_test.rs                           | 17 +++++
 tests/fixtures/tagma/tagma_decoder.xif.yaml | 12 +--
 tests/tagma_fixture.rs                      | 82 ++++++++++++++++++++-
 9 files changed, 222 insertions(+), 26 deletions(-)

diff --git a/README.md b/README.md
index be0130f..c0f064f 100644
--- a/README.md
+++ b/README.md
@@ -152,12 +152,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`.
 
@@ -193,7 +203,8 @@ Valid counts below are the `evaluate_all` results on the committed fixtures
 | Speedup (same-language baseline, this machine) | ~550x |
 | 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 | 96 (73 lib + 16 CLI + 2 tagma + 5 structural), all passing |
+| Projector types | 4 (sum, identity, parity, tagma_decode) |
+| Tests | 100 (73 lib + 17 CLI + 5 tagma + 5 structural), all passing |
 | Coverage gate | 80% lines / 80% regions (llvm-cov, all modules incl. Spike/Yosys backends) |
 | Simulation backends | Mock (default), Spike (`EV_SIM_BACKEND=spike`) |
 
diff --git a/docs/devlog/2026-08-23-tagma-hw-fixtures.md b/docs/devlog/2026-08-23-tagma-hw-fixtures.md
index f9eb4f7..eaa757d 100644
--- a/docs/devlog/2026-08-23-tagma-hw-fixtures.md
+++ b/docs/devlog/2026-08-23-tagma-hw-fixtures.md
@@ -41,16 +41,20 @@ 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: the functional contract of the decoder, of the demo top
-outputs, and of the golden anchor decomposition is not expressible in the
-current model. The input domain contract and the output axis bounds are the
-largest expressible subsets.
+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. The golden anchor contract therefore stays in the
-domain of the Python consistency gate and the Verilator golden testbench
-until the extension lands.
+so it verifies no property.
 
 Sequential behavior (registered outputs, one-cycle latency) and Verilog
 testbench execution are outside the ev domain, which evaluates combinational
@@ -69,23 +73,24 @@ gate runs in the CI coverage job.
 
 ## Milestones
 
-Milestone 1 (this branch): fixture specs, `run.sh` assertions, CLI tests,
-lib-level fixture tests, the CI coverage gate, and this plan.
+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): a decode projector or an arithmetic constraint so
-the decomposition becomes expressible. This is the main engine extension.
+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): cross-check the ev enumeration against
-`syntagma/hw/rtl/golden_anchors.hex` through the golden-anchor pattern of
-issues #25 and #28.
+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.
 
-Recommendation: ship Milestone 1 now. Milestone 2 is the prerequisite for any
-functional cross-check inside ev.
-
 ## Verification results
 
 Measured with `ev verify` on the release build, text output:
@@ -95,6 +100,11 @@ Measured with `ev verify` on the release build, text output:
 | 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
diff --git a/scripts/coverage.sh b/scripts/coverage.sh
index 7da833a..7239a3e 100755
--- a/scripts/coverage.sh
+++ b/scripts/coverage.sh
@@ -15,6 +15,10 @@ set -euo pipefail
 # them. The merge glob is target/llvm-cov-target/*.profraw, so external
 # runs must write there (LLVM_PROFILE_FILE below).
 #
+# The instrumented bin is removed before the suite so a stale build from
+# before a source edit cannot leak old signatures into the merge, which
+# produces mismatched-data warnings and distorted coverage.
+#
 # Usage: bash scripts/coverage.sh
 #
 
@@ -34,7 +38,8 @@ PROFRAW_DIR=target/llvm-cov-target
 COVERAGE_MIN="${COVERAGE_MIN:-80}"
 
 echo "=== coverage: instrumented test suite ==="
-rm -f "$PROFRAW_DIR"/*.profraw
+cargo llvm-cov clean --profraw-only
+rm -f "$EV_COV"
 cargo llvm-cov --release --no-report
 
 echo "=== coverage: external backend runs (instrumented binary) ==="
diff --git a/src/spec/mod.rs b/src/spec/mod.rs
index ca8cf29..8318cfc 100644
--- a/src/spec/mod.rs
+++ b/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
 }
diff --git a/src/synth/mod.rs b/src/synth/mod.rs
index b33cbae..9ea3f4d 100644
--- a/src/synth/mod.rs
+++ b/src/synth/mod.rs
@@ -199,6 +199,15 @@ fn sv_projector(proj: &crate::spec::ProjectorSpec, field_names: &[&String]) -> S
         crate::spec::ProjectorSpec::Parity { field } => {
             format!("{}[0]", field)
         }
+        crate::spec::ProjectorSpec::TagmaDecode { field, base } => {
+            // Golden-anchor packed layout: offset[28:15] i[14:10] m[9:5] f[4:0].
+            // offset = code - base, i = offset / 588, m = (offset % 588) / 28, f = offset % 28.
+            format!(
+                "(({f} - {base}) << 15) | ((({f} - {base}) / 588) << 10) | (((({f} - {base}) % 588) / 28) << 5) | (({f} - {base}) % 28)",
+                f = field,
+                base = base
+            )
+        }
     }
 }
 
diff --git a/src/verify/registry.rs b/src/verify/registry.rs
index 5cfe092..318e59b 100644
--- a/src/verify/registry.rs
+++ b/src/verify/registry.rs
@@ -602,6 +602,14 @@ impl Default for ProjectorRegistry {
                 panic!("parity builder called on non-parity spec")
             }
         });
+        reg.register("tagma_decode", |spec, axis_of| {
+            if let ProjectorSpec::TagmaDecode { field, base } = spec {
+                let axis = axis_of[field];
+                Box::new(TagmaDecodeEval { axis, base: *base })
+            } else {
+                panic!("tagma_decode builder called on non-tagma_decode spec")
+            }
+        });
         reg
     }
 }
@@ -611,6 +619,7 @@ fn spec_projector_name(spec: &ProjectorSpec) -> &str {
         ProjectorSpec::Sum => "sum",
         ProjectorSpec::Identity { .. } => "identity",
         ProjectorSpec::Parity { .. } => "parity",
+        ProjectorSpec::TagmaDecode { .. } => "tagma_decode",
     }
 }
 
@@ -644,3 +653,37 @@ impl Evaluator for ParityEval {
         point.coordinates().get_axis(self.axis).map(|v| v & 1)
     }
 }
+
+/// Tagma decoder constants: the Hangul syllable block U+AC00..U+D7A3
+/// decomposes as offset = code - 0xAC00, i = offset / 588, m = (offset %
+/// 588) / 28, f = offset % 28 (588 = 21 * 28).
+const TAGMA_STRIDE_INIT: i64 = 588;
+const TAGMA_STRIDE_MED: i64 = 28;
+const TAGMA_N_INIT: i64 = 19;
+const TAGMA_N_MED: i64 = 21;
+const TAGMA_N_FIN: i64 = 28;
+
+/// Tagma 3-axis decoder evaluator: packs the decomposition into the
+/// golden-anchor layout offset[28:15] i[14:10] m[9:5] f[4:0].
+#[derive(Debug, Clone)]
+struct TagmaDecodeEval {
+    axis: usize,
+    base: i64,
+}
+
+impl Evaluator for TagmaDecodeEval {
+    fn evaluate(&self, point: &Point) -> Option<i64> {
+        let code = point.coordinates().get_axis(self.axis)?;
+        let offset = code - self.base;
+        if offset < 0 {
+            return None;
+        }
+        let i = offset / TAGMA_STRIDE_INIT;
+        let m = (offset % TAGMA_STRIDE_INIT) / TAGMA_STRIDE_MED;
+        let f = offset % TAGMA_STRIDE_MED;
+        if i >= TAGMA_N_INIT || m >= TAGMA_N_MED || f >= TAGMA_N_FIN {
+            return None;
+        }
+        Some((offset << 15) | (i << 10) | (m << 5) | f)
+    }
+}
diff --git a/tests/cli_test.rs b/tests/cli_test.rs
index fbc8cad..7b38b7a 100644
--- a/tests/cli_test.rs
+++ b/tests/cli_test.rs
@@ -259,6 +259,23 @@ fn synth_json_with_mock_backend() {
     );
 }
 
+#[test]
+fn synth_tagma_decoder_with_mock_backend() {
+    let output = Command::new(env!("CARGO_BIN_EXE_ev"))
+        .arg("synth")
+        .arg("--target")
+        .arg("tests/fixtures/tagma/tagma_decoder.xif.yaml")
+        .env("EV_SYNTH_BACKEND", "mock")
+        .output()
+        .expect("failed to run ev synth on tagma fixture");
+    assert!(
+        output.status.success(),
+        "ev synth should exit 0 on the tagma fixture"
+    );
+    let stdout = String::from_utf8_lossy(&output.stdout);
+    assert!(stdout.contains("[ok]"), "synthesis should show ok status");
+}
+
 #[test]
 #[ignore = "33M combos via CLI (old pipeline). struct_enum does it in ~200ms; pending CLI integration."]
 fn verify_cva6_xif_ref_fixture() {
diff --git a/tests/fixtures/tagma/tagma_decoder.xif.yaml b/tests/fixtures/tagma/tagma_decoder.xif.yaml
index 86e4811..d1b8a92 100644
--- a/tests/fixtures/tagma/tagma_decoder.xif.yaml
+++ b/tests/fixtures/tagma/tagma_decoder.xif.yaml
@@ -16,10 +16,11 @@
 # verification devlog: the last valid syllable is U+D7A3, not U+D7AF
 # (0xAC00 + 11171 = 0xD7A3).
 #
-# The axis decomposition itself requires integer division and modulo by
-# constants, which the current constraint set cannot express. The plan
-# devlog 2026-08-23-tagma-hw-fixtures.md records the extension proposal
-# under ev issue #46.
+# The tagma_decode projector (issue #46, milestone 2) packs the axis
+# decomposition of every passing code point into the golden-anchor layout
+# offset[28:15] i[14:10] m[9:5] f[4:0], so the projection of code k equals
+# line k of syntagma/hw/rtl/golden_anchors.hex. Pass/fail itself remains a
+# domain check: the decomposition is a projection, not a constraint.
 #
 # Verification space: 65,536 raw combinations
 # Valid: 11,172 (the Hangul syllable block), Failed: 54,364
@@ -36,5 +37,6 @@ constraints:
     field: "code"
     value: 0xD7A3
 projector:
-  type: identity
+  type: tagma_decode
   field: "code"
+  base: 0xAC00
diff --git a/tests/tagma_fixture.rs b/tests/tagma_fixture.rs
index 4eab5f9..38257b9 100644
--- a/tests/tagma_fixture.rs
+++ b/tests/tagma_fixture.rs
@@ -4,9 +4,11 @@
 //! spawned binary, which the coverage instrumentation does not see. These
 //! tests evaluate the fixtures in-process through the public library API,
 //! so the ge/le constraint path, the YAML parse of the hex boundary
-//! constants, and the domain counts are covered by the instrumented suite.
+//! constants, the tagma_decode projector, and the domain counts are covered
+//! by the instrumented suite.
 
 use ev::spec::VerificationSpec;
+use ev::synth::GenerateRtl;
 use ev::verify::compose::expand_all;
 use ev::verify::evaluate::evaluate_all;
 use ev::verify::registry::{ConstraintRegistry, ProjectorRegistry};
@@ -16,6 +18,26 @@ fn load_fixture(path: &str) -> VerificationSpec {
         .unwrap_or_else(|e| panic!("failed to load fixture {path}: {e}"))
 }
 
+/// (code, projection) pairs for every passing combination, in domain order.
+fn valid_code_projection_pairs(spec: &VerificationSpec) -> Vec<(i64, i64)> {
+    let combos = expand_all(spec).expect("domain expansion must succeed");
+    evaluate_all(
+        spec,
+        combos,
+        &ConstraintRegistry::default(),
+        &ProjectorRegistry::default(),
+    )
+    .into_iter()
+    .filter(|r| r.passed)
+    .map(|r| {
+        (
+            r.combination.values[0],
+            r.projection.expect("valid code points must project"),
+        )
+    })
+    .collect()
+}
+
 /// The decoder accepts exactly the 11,172 Hangul syllables in
 /// [0xAC00, 0xD7A3]. The boundary assertion pins the correction recorded in
 /// the syntagma verification devlog: the last valid syllable is U+D7A3, not
@@ -79,3 +101,61 @@ fn tagma_demo_top_output_space() {
         "every axis triple is reachable"
     );
 }
+
+/// The tagma_decode projector packs the decomposition into the golden-anchor
+/// layout offset[28:15] i[14:10] m[9:5] f[4:0]. Literal spot values pin the
+/// packing without re-deriving it from the same formula.
+#[test]
+fn tagma_decode_projection_spot_values() {
+    let spec = load_fixture("tests/fixtures/tagma/tagma_decoder.xif.yaml");
+    let pairs = valid_code_projection_pairs(&spec);
+    assert_eq!(pairs.len(), 11_172);
+
+    // code 0xAC00: offset 0, i 0, m 0, f 0.
+    assert_eq!(pairs[0], (0xAC00, 0));
+    // code 0xAC00 + 587: offset 587, i 0, m 20, f 27 (last medial of the first initial).
+    // i 0 contributes no bits to the pack (bit 10..14 are zero).
+    assert_eq!(pairs[587], (0xAC00 + 587, (587 << 15) | (20 << 5) | 27));
+    // code 0xD7A3: offset 11171, i 18, m 20, f 27 (last syllable).
+    assert_eq!(
+        pairs[11_171],
+        (0xD7A3, (11_171 << 15) | (18 << 10) | (20 << 5) | 27)
+    );
+}
+
+/// Over the whole valid domain, the projector equals the golden-anchor
+/// contract: line k packs offset k with the i/m/f decomposition of k.
+#[test]
+fn tagma_decode_projection_full_domain() {
+    let spec = load_fixture("tests/fixtures/tagma/tagma_decoder.xif.yaml");
+    let pairs = valid_code_projection_pairs(&spec);
+    assert_eq!(pairs.len(), 11_172);
+
+    for (k, (code, proj)) in pairs.iter().enumerate() {
+        let k = k as i64;
+        assert_eq!(*code, 0xAC00 + k, "code at offset {k}");
+        let expected = (k << 15) | ((k / 588) << 10) | (((k % 588) / 28) << 5) | (k % 28);
+        assert_eq!(*proj, expected, "packed projection at offset {k}");
+    }
+}
+
+/// The SV generator must emit the packed decode expression for the
+/// tagma_decode projector, so the golden-anchor layout is preserved in the
+/// generated RTL.
+#[test]
+fn tagma_decode_sv_generation() {
+    let spec = load_fixture("tests/fixtures/tagma/tagma_decoder.xif.yaml");
+    let sv_path = ev::synth::SvGenerator
+        .generate(&spec)
+        .expect("sv generation");
+    let sv = std::fs::read_to_string(&sv_path).expect("read generated sv");
+
+    assert!(
+        sv.contains("((code - 44032) << 15)"),
+        "generated SV must pack the offset into bits 28:15"
+    );
+    assert!(
+        sv.contains("/ 588") && sv.contains("% 588") && sv.contains("% 28"),
+        "generated SV must express the Tagma decomposition"
+    );
+}

From 59f4cef3ea97c88c649733f26cbf83dc8f3e17d3 Mon Sep 17 00:00:00 2001
From: TH Lee <lee@ssccs.org>
Date: Sun, 23 Aug 2026 15:30:55 +0200
Subject: [PATCH 7/9] test: un-ignore cva6 xif r4 CLI fixture test #47

---
 README.md         | 2 +-
 tests/cli_test.rs | 1 -
 2 files changed, 1 insertion(+), 2 deletions(-)

diff --git a/README.md b/README.md
index c0f064f..3a0d187 100644
--- a/README.md
+++ b/README.md
@@ -204,7 +204,7 @@ Valid counts below are the `evaluate_all` results on the committed fixtures
 | 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) |
 | Projector types | 4 (sum, identity, parity, tagma_decode) |
-| Tests | 100 (73 lib + 17 CLI + 5 tagma + 5 structural), all passing |
+| Tests | 101 (73 lib + 18 CLI + 5 tagma + 5 structural), all passing |
 | Coverage gate | 80% lines / 80% regions (llvm-cov, all modules incl. Spike/Yosys backends) |
 | Simulation backends | Mock (default), Spike (`EV_SIM_BACKEND=spike`) |
 
diff --git a/tests/cli_test.rs b/tests/cli_test.rs
index 7b38b7a..3e6c33d 100644
--- a/tests/cli_test.rs
+++ b/tests/cli_test.rs
@@ -194,7 +194,6 @@ fn verify_tagma_demo_top_fixture() {
 }
 
 #[test]
-#[ignore = "medium: 16K combos via CLI. Use release build or struct_enum for speed."]
 fn verify_cva6_xif_ref_r4_fixture() {
     let output = Command::new(env!("CARGO_BIN_EXE_ev"))
         .arg("verify")

From 0685f8b53cdbd681e18dbc02978c2dab5399201a Mon Sep 17 00:00:00 2001
From: TH Lee <lee@ssccs.org>
Date: Sun, 23 Aug 2026 16:03:05 +0200
Subject: [PATCH 8/9] fix: address inline review on coverage pull policy, sv
 comment, and README reconciliation #47

---
 README.md           | 42 ++++++++++++++++++++++--------------------
 scripts/coverage.sh |  4 ++--
 src/synth/mod.rs    |  3 +++
 3 files changed, 27 insertions(+), 22 deletions(-)

diff --git a/README.md b/README.md
index 3a0d187..f3ac9b9 100644
--- a/README.md
+++ b/README.md
@@ -3,11 +3,11 @@
 Exhaustive verification CLI for RISC-V custom instruction extensions.
 Apache 2.0.
 
-33.5 million combinations evaluated deterministically: 10.4 s with the
-standard pipeline, 19.0 ms with the Tagma-based structural enumeration
-(~550x, same-language baseline). The CVA6 fixtures are derived from the
-hardware decoder mask table (commit `6544a714c`); the Spike backend
-cross-checks the constraint model and instruction-word assembly in C.
+33.5 million combinations verified deterministically in about 0.2 s (release)
+through the structural enumeration pipeline, which is the CLI default since
+issue #42. The CVA6 fixtures are derived from the hardware decoder mask
+table (commit `6544a714c`); the Spike backend cross-checks the constraint
+model and instruction-word assembly in C.
 
 ## What It Does
 
@@ -20,10 +20,11 @@ cross) that are encoded directly into the enumeration space, and runtime
 constraints (eq, neq, lt, gt, le, ge, even) that are checked per combination.
 Only structurally valid combinations are ever generated.
 
-A single command enumerates and evaluates 33.5 million combinations against the
-CVA6 CV-X-IF encoding space derived from the hardware decoder mask table
-(`cva6/core/cvxif_example/include/cvxif_instr_pkg.sv` at commit `6544a714c`),
-and produces the result in 19.0 milliseconds:
+A single command verifies the 33.5 million combination CVA6 CV-X-IF encoding
+space derived from the hardware decoder mask table
+(`cva6/core/cvxif_example/include/cvxif_instr_pkg.sv` at commit `6544a714c`)
+in about 0.2 seconds, by enumerating only the structurally valid
+combinations:
 
 ```bash
 ev verify --target tests/fixtures/cva6/xif_ref.xif.yaml
@@ -196,22 +197,23 @@ Valid counts below are the `evaluate_all` results on the committed fixtures
 
 | Metric | Value |
 |--------|-------|
-| Raw combinations evaluated (CVA6 full) | 33,554,432 |
+| Raw combinations verified (CVA6 full) | 33,554,432 (counted, not enumerated) |
 | Valid combinations identified (CVA6 full) | 196,608 |
-| Standard pipeline time (evaluate_all, release) | 10.4 s |
-| Structural pipeline time (struct_enum, release) | 19.0 ms |
-| Speedup (same-language baseline, this machine) | ~550x |
+| CLI verify time (CVA6 full, structural pipeline, release) | ~0.2 s |
+| Previous CLI time (expand_all, release) | 10.4 s |
+| 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) |
 | Projector types | 4 (sum, identity, parity, tagma_decode) |
-| Tests | 101 (73 lib + 18 CLI + 5 tagma + 5 structural), all passing |
+| 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: both pipelines are Rust, the same
-release profile, measured by criterion; the speedup is the O(N) vs O(V)
-enumeration-strategy gain, not a language effect. Reproduce with
-`cargo bench -- cva6_full` on the committed fixtures.
+Benchmark methodology and reproducibility: the structural pipeline is the
+CLI default; the raw total is computed from the field domains without
+enumeration, and only structurally valid combinations are generated and
+evaluated. Reproduce with `cargo bench -- cva6_full` on the committed
+fixtures.
 
 ## Architecture
 
@@ -220,8 +222,8 @@ src/
   main.rs           CLI (clap: verify, simulate, synth)
   spec/             VerificationSpec, FieldSpec, ConstraintSpec, ProjectorSpec
   verify/
-    compose.rs      Domain expansion + structural enumeration
-    evaluate.rs     Constraint evaluation + projection + CoordSpace validation
+    compose.rs      Domain expansion + structural enumeration + raw total
+    evaluate.rs     Constraint evaluation + projection + structural pipeline
     registry.rs     ConstraintRegistry + ProjectorRegistry (pluggable builder)
   report/
     reporter.rs     ReporterCapable trait + TextReporter + CsvReporter
diff --git a/scripts/coverage.sh b/scripts/coverage.sh
index 7239a3e..ad64bac 100755
--- a/scripts/coverage.sh
+++ b/scripts/coverage.sh
@@ -55,7 +55,7 @@ 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 -v "$(pwd):/workspace" -w /workspace \
+    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
@@ -68,7 +68,7 @@ if command -v spike >/dev/null 2>&1 && command -v riscv64-unknown-elf-gcc >/dev/
         LLVM_PROFILE_FILE="$PROFRAW_DIR/ev-ext-%p-%m.profraw" \
         "$EV_COV" simulate --target "$ALL_PASS" >/dev/null
 else
-    docker run --rm -v "$(pwd):/workspace" -w /workspace \
+    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" \
diff --git a/src/synth/mod.rs b/src/synth/mod.rs
index 9ea3f4d..21c55a6 100644
--- a/src/synth/mod.rs
+++ b/src/synth/mod.rs
@@ -202,6 +202,9 @@ fn sv_projector(proj: &crate::spec::ProjectorSpec, field_names: &[&String]) -> S
         crate::spec::ProjectorSpec::TagmaDecode { field, base } => {
             // Golden-anchor packed layout: offset[28:15] i[14:10] m[9:5] f[4:0].
             // offset = code - base, i = offset / 588, m = (offset % 588) / 28, f = offset % 28.
+            // The expression is only meaningful for code >= base. SystemVerilog
+            // division and modulo on negative operands are tool-dependent, and
+            // the generated assertion module is exercised on the valid domain.
             format!(
                 "(({f} - {base}) << 15) | ((({f} - {base}) / 588) << 10) | (((({f} - {base}) % 588) / 28) << 5) | (({f} - {base}) % 28)",
                 f = field,

From b2ca5effd120a6b24cf41daa30ba70c9f483bba8 Mon Sep 17 00:00:00 2001
From: TH Lee <lee@ssccs.org>
Date: Sun, 23 Aug 2026 16:07:50 +0200
Subject: [PATCH 9/9] fix: full-clean instrumented build dir in coverage gate
 #47

---
 scripts/coverage.sh | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/scripts/coverage.sh b/scripts/coverage.sh
index ad64bac..9498323 100755
--- a/scripts/coverage.sh
+++ b/scripts/coverage.sh
@@ -15,9 +15,11 @@ set -euo pipefail
 # them. The merge glob is target/llvm-cov-target/*.profraw, so external
 # runs must write there (LLVM_PROFILE_FILE below).
 #
-# The instrumented bin is removed before the suite so a stale build from
-# before a source edit cannot leak old signatures into the merge, which
-# produces mismatched-data warnings and distorted coverage.
+# 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
 #
@@ -38,8 +40,7 @@ PROFRAW_DIR=target/llvm-cov-target
 COVERAGE_MIN="${COVERAGE_MIN:-80}"
 
 echo "=== coverage: instrumented test suite ==="
-cargo llvm-cov clean --profraw-only
-rm -f "$EV_COV"
+rm -rf "$PROFRAW_DIR"
 cargo llvm-cov --release --no-report
 
 echo "=== coverage: external backend runs (instrumented binary) ==="