Track1 NutShell Cache Verification Workspace

This workspace is for the CCF Track1 UCAgent competition task: verifying the NutShell Cache with UCAgent-assisted, human-reviewed verification engineering.

Reviewer Quick Start

Reproduce: make reproduce
- Expected: 164 tests PASS + 4 documented xfails + coverage collection + bug injection + recovery (perf + LFSR=0 formal proof tests run separately via make perf-summary and pytest tests/directed/test_lfsr_zero_unreachable.py)
Coverage Reports:
- Funcov: open build/reports/cache_coverage.html — 28 groups, 38 points, 113/113 bins hit
- CRV standalone (Python-only, no RTL): cat reports/crv_standalone_summary.md — 28/28 intent bins, 10/10 seeds independently close
- Performance (4 workloads): cat reports/perf_summary.md — 790 cache transactions, 71.65% overall hit rate, p50 = 2 cycles (hit) / 5 cycles (miss), no DUT stall

Key Documents (recommended reading order):

Doc	Purpose
`docs/ai_collaboration_report.md`	AI-human collaboration log, defects table, prompt strategy
`docs/env_defect_register.md`	16 environment defects (ENV-001..016) — 3 are human-review inversions of AI conclusions
`docs/coverage_waiver_rationale.md`	Coverage waiver analysis
`docs/requirements_traceability_matrix.md`	Requirements traceability matrix
`SKILL.md`	UCAgent / Claude Code re-run skill for this repo

UCAgent re-run (one command):

bash scripts/clean_room_check.sh         # env facts + make clean && make reproduce
make crv-standalone                      # ms-scale, no Verilator needed
make perf-summary                        # 4-workload characterization + reports/
pytest tests/directed/test_lfsr_zero_unreachable.py -v
                                         # LFSR=0 formal proof (about 30s, $10^8$ scan)

Status

UCAgent and Claude Code CLI are available on this machine.
The selected DUT is Picker’s Cache example RTL at rtl/dut/Cache.v.
Picker exports the selected DUT as Python class DUTCache in build/picker_cache/.
16 UCAgent stages (0-15) + Round-2 remediation (stages 0-7) completed with Claude Code backend through MCP server.
Full regression: 164 passed / 4 xfailed (168 collected; see Coverage table below for the breakdown).
Aug 7 additions: tests/directed/test_burst_spec_complete.py adds DIR-024a..d (11 cases, 10 pass + 1 strict-xfail — covers burst spec completeness); tests/perf/ adds PERF-001..004 (5 cases); tests/directed/test_lfsr_zero_unreachable.py adds LFSR=0 formal proof (3 cases).
Line / branch / expression coverage: 100% (with structural waivers for provably-unreachable lines).
Functional coverage: 113 bins / 28 groups / 38 points, 113/113 bins hit (grate 100%, no orphan or dangling vPlan links).
Toggle coverage: 90.06% multi-seed (2803 misses / 28203), meeting the ≥88% target.
Bug injection: 10 scenarios (BUG-001..010), all detected by scoreboard; recovery path passes. BUG-006 is a real RTL bug.
Scoreboard: 15 check methods (multi-beat, protocol timing, PREFETCH/READ_BURST, consistency).
make reproduce verified end-to-end (regression + coverage + bug-injection-fail + recovery).
Human review: All UCAgent-generated code was reviewed and corrected by a human engineer before committing. See docs/ai_collaboration_report.md for the full human review log.

DUT Overview

The top-level Cache (Verilog module Cache) is a 4-way set-associative L1 cache with a 3-stage pipeline (s1/s2/s3). Address decomposition: tag = addr[31:13], index = addr[12:6], wordIndex = addr[5:3].

Interfaces:

CPU side: io_in_req_* (request: addr/size/cmd/wmask/wdata/user), io_in_resp_* (response: cmd/rdata/user), io_flush[1:0], io_empty.
Memory backend: io_out_mem_req_* / io_out_mem_resp_* (downstream memory), io_out_coh_req_* / io_out_coh_resp_* (coherence probes), io_mmio_req_* / io_mmio_resp_* (MMIO bypass).

Key behaviors: hit/miss with hitVec + waymask; invalid-way-first then LFSR replacement; meta/data forwarding from write buses; MMIO range detection; flush-done via io_empty; PopCount(waymask) <= 1 assertion.

Test Suite

Suite	Tests	Coverage
smoke	1	Basic read miss/refill, read hit, write hit
directed	120 collected cases	Write masks, word offsets, refill beats, replacement (LFSR + invalid-first), MMIO bypass + semantics (incl. all-8-words no-pollution), pipeline drain, coherence probe (+probe×dirty), write miss, clean eviction, dirty writeback, user passthrough, READ_BURST, PREFETCH, cycle-exact forwarding, pipeline interaction, toggle closure, write-hit mask×offset, spec-conformance xfails, refill profile, hit latency, hit throughput, SRAM arbiter, LFSR reset seed
corner	7	Memory request backpressure, CPU response backpressure, handshake backpressure (probe/MMIO), reset during traffic (refill-wait + dirty-writeback), post-reset state invalidation (tag + dirty)
random	21	Constrained random traffic + 10-seed multi-seed sweep + toggle-diversity
perf	5 tests (PERF-001..004 + smoke)	`tests/perf/test_perf_workloads.py`: 4 parametrized workloads (read-heavy / write-heavy / mixed-7r3w / burst-heavy). Sibling `StepRis` observer (`tests/perf/perf_collector.py`) — does not modify `CacheMonitor` or `CacheCoverage`. Latency histogram + hit/miss per workload → `reports/perf_summary.{json,md}` (closes `final_report §8.2 §4`)
lfsr_zero	3 tests	`tests/directed/test_lfsr_zero_unreachable.py`: model-level formal proof that the `victimWaymask_lfsr == 0` predicate (`Cache.v:240`) is unreachable from the seeded initial state. Canonical $10^8$ advances run + parametrized $10^6$ / $10^7$ . Promotes the Category (R) waiver from docstring to executable sentinel (closes `final_report §8.2 §5`).
injected_bug	10 scenarios	Reference-model bit-flip, dirty-writeback bypass, address corruption, dirty-bit loss, refill order scramble, PREFETCH response leakage, READ_BURST beat corruption, writeback cmd encoding, flush-probe consistency, refill word corruption

Coverage

Metric	Result
Line coverage	100.0% (1345/1345) (with structural waivers)
Branch coverage	100.0% (458/458)
Expression coverage	100.0% (131/131)
Functional coverage	113 bins, 113 hit + 0 waived (28 groups / 38 points, grate 100)
Toggle coverage	90.06% multi-seed (2803 misses / 28203)
CRV standalone (Python-only)	28/28 intent bins, 10/10 seeds independently close (`reports/crv_standalone_summary.md`)
Performance (non-functional)	Hit-path latency 2 cyc / Miss-path latency 5 cyc across 4 workloads (`reports/perf_summary.md`); closes final_report §8.2 §4

UCAgent Integration

All 16 completed UCAgent stages (0-15) drove Claude Code through the MCP server:

Stage 0: Workspace audit and DUT interface analysis
Stage 1: Verification environment build (env, monitor, scoreboard, utils)
Stage 2: Backpressure directed tests
Stage 3: CRV and functional coverage bootstrap
Stage 4: Directed test expansion (8 test files)
Stage 5: Dirty writeback coverage closure
Stage 6: Bug injection evidence (5 scenarios)
Stage 7: Coherence probe test
Stage 8: Flush behavior test
Stage 9: Scoreboard enhancement
Stage 10: Scoreboard enhancement verification
Stage 11: Line coverage closure
Stage 12: Branch coverage closure
Stage 13: Toggle coverage improvement
Stage 14: Expression coverage closure
Stage 15: Functional coverage closure

Working Directories

./
├── LICENSE (Apache 2.0)
├── Makefile
├── README.md
├── top.md
├── configs/
│   ├── internal.yaml
│   └── ucagent_track1_cache.yaml
├── docs/
│   ├── verification_plan.md
│   ├── ai_collaboration_report.md
│   ├── coverage_report.md
│   ├── coverage_waiver_rationale.md
│   ├── bug_tracking.md
│   ├── test_points.md
│   ├── requirements_traceability_matrix.md
│   ├── known_rtl_bugs.md
│   └── reproducibility_evidence.md
├── rtl/dut/
├── src/
│   ├── env/
│   ├── generator/
│   ├── monitor/
│   ├── scoreboard/
│   └── utils/
├── tests/
│   ├── smoke/
│   ├── corner/
│   ├── directed/
│   ├── random/
│   └── injected_bug/
└── scripts/

Quick Start

# One-click full reproduction
make reproduce

# Quick verify: clean -> export -> smoke
make quick

# Run a specific UCAgent stage
make stage STAGE=0

# Full regression
make test

# Coverage collection
make coverage-multi

# Performance characterization (4 workloads)
make perf-summary

# Bug injection
make bug-inject    # Expected: failure (bug detected)
make bug-recover   # Expected: pass (recovery path)

Environment

Python: .venv/bin/python (3.11, pytest, toffee)
Picker: configured via scripts/env.sh (PICKER_HOME, PYTHONPATH)
All tests use the Toffee framework + Picker DUT (DUTCache)
UCAgent: /Users/zzy/Workspace/ucagent/.venv/bin/ucagent
Claude Code: MCP backend at http://127.0.0.1:5002/mcp