NutShell Cache RTL 验证工程

本仓库对公开的 NutShell Cache.v 快照执行真实 RTL 验证。主路径由 Picker/Verilator、 Toffee Bundle、事务环境、独立参考模型与 Scoreboard、受约束随机场景、故障注入和覆盖门禁组成。覆盖结论只从本次 RTL 事务与 Verilator 数据库生成。

正式报告

ucagent验证报告.pdf

该 PDF 是本项目唯一正式验证报告。

当前可复现状态

最近一次完整 make verify 的机器可读结论为：

主回归：132 passed，4 strict-xfailed；
RTL 事务证据：882 条；
功能覆盖：23/23；交叉覆盖：23/23；Toffee 覆盖：18/18；
完整需求映射：10 FG、48 FC、144 CK，131 项运行证据闭合、7 项已知 RTL 问题、6 项不可达配置、0 项 TEST_GAP；
行覆盖：整体 98.30%，核心 Cache.v 98.19%；
故障注入：7 个事务/边界检查通过，6/6 个 RTL 源码变异被正常场景检出；
总门禁：PASS。

这些数字分别来自 reports/regression/regression.json、 reports/coverage/coverage_gate.json、reports/bugs/bug_matrix.json 和 reports/verification_summary.json。reports/verification_session.json 保存本轮唯一 run_id、RTL/源码/测试输入哈希；顶层门禁拒绝混用不同轮次的 PASS 文件。提交前应重新运行命令，不应把 README 当作最新执行证据。

一键复现

Picker 是生成 DUT 的独立编译工具，不属于 Python/Conda 包。首次在干净环境运行时，先以固定 commit 构建到仓库忽略的 .tools/ 目录；脚本结束后无需手工填写本机路径：

conda env create -f environment.yml
conda activate ucagent-cache
make setup
make bootstrap_picker
make verify

如果 PATH 中已经安装了同一版本的 Picker，可以跳过 make bootstrap_picker。项目要求的 Picker 版本为 0.9.0-master-301c403-2026-05-12，对应源码 commit 301c40375407498b24a30a35d5c9fe0b710db0f7；make check_toolchain 会核验 Picker、 Verilator 和 Python 的准确版本，而不只检查命令是否存在。

分阶段运行命令为：

make check_toolchain
make gen_dut
make verify

make verify 会依次检查工具、校验或生成 DUT、清空旧证据、运行主回归与 CRV/stress、合并全部 Verilator 覆盖数据库、生成三类功能报告和完整 FG/FC/CK 映射、执行硬门禁、构建 RTL 变异并运行总门禁。

工程入口

src/nutshell_cache_vip/：事务、Driver、Monitor、Adapter、Memory/MMIO Agent、独立 Cache 状态模型、Scoreboard、Toffee 与证据记录器。
tests/：定向场景、真实 RTL CRV、stress、coherence 和故障检测。
scripts/：工具检查、DUT/变异构建、覆盖生成与总门禁。
rtl/：固定 RTL 快照、来源哈希和唯一接口映射。
reports/：当前机器可读结果，不保存重复快照。
ucagent/baseline/：冻结的 UCAgent 原型和运行元数据；最终实现不直接执行其中模板。

运行 make human_refinement 可从冻结 manifest、实际源码和当前 PASS 报告重新生成 reports/analysis/human_refinement_ab.json。该文件分别报告结构耦合、通用 CRV 约束收敛、 24 对 24 笔等预算对照和执行证据，不计算主观综合分；对照范围和输入 SHA-256 均写在 JSON 内。

设计和证据说明见架构、验证计划、证据模型、工程修正记录与复现说明。

已知边界

当前 RTL 的 coherence probe 命令与握手可复现，但 payload data 返回陈旧/非缓存值，由两个 strict-xfail 用例持续保留。该 DCache 快照还在 CacheStage3 中断言只允许 ICache 执行 cache flush，因此不能把 DCache 全量失效声明为可达功能。顶层也没有 L2 prefetch 接口。CPU response 在 ready 拉低时还会抑制 valid，而不是保持 valid/payload，由定向与 seed-controlled 两个 strict-xfail 分别固定最小复现和随机压力复现。详细依据见 docs/verification-plan.md。