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.

🏆 第八届 CCF 开源创新大赛决赛人工智能方向一等奖

Award: First Prize (AI Track) — 8th CCF Open Source Innovation Competition Finals

This project was awarded the First Prize in the AI Direction at the finals of the 8th CCF Open Source Innovation Competition (第八届 CCF 开源创新大赛决赛人工智能方向一等奖).

Reviewer Quick Start

Reproduce: make reproduce
- Expected: 166 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: 166 passed / 4 xfailed (170 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