csrformal

在声明的假设下，对香山 CSR 的组合模块做 SMT 检查。case 是选点回归； EQ 是带假设的局部等价，不是「符合整本特权规范」。每条性质带规则 id 和原文哈希，规范改了可以标出该重审的结论。

当前能打红的确认级差异：menvcfg.STCE=0 时 RTL 未门控 vstimecmp （CSRPermit/S3 与 CSRPermit/EQ-permit 同红）。

csrformal is licensed under Mulan PSL v2.

适用范围

CSRPermitModule、TrapHandleModule 与 TrapEntry{M,HS}EventModule 精化后 registers=0，是纯组合。TrapEntry EQ 是 CSRPermit EQ 的方法移植， 同样是带假设的局部等价，不是「符合整本特权规范」。 输入是特权态、CSR 地址和一组 enable 位（TrapEntry 则是陷入前架构状态）。 SMT 在假设允许的自由位上穷尽，不是在全输入空间上证明整本规范。

自检：

• 假设集不可满足判 VACUOUS（失败），不是通过。
• spec-drift 比对被引用规则的原文；EQ 的条款在 extra_refs 里，必须进基线。
• spec-selfcheck 证明 permit() 与 permit_smt()、以及 TrapEntry 的 Python 次态与 SMT 公式，在同一套 eq_assumes 下一致。
• self-test 注入已知缺陷，要求意图对应的性质报反例。

规则追溯的案例见 规范漂移 demo。

安装

精化 / check / 变异回归仅 Linux。 SMT2 缓存用 fcntl 文件锁，不支持 Windows。list / lint / spec-selfcheck 是纯逻辑，不拦。请在 Linux 主机或 Docker 里跑精化；本仓库不为 Windows 重写流水线。

外部工具（不由本仓库安装）

工具	版本	用途	环境变量（未设则找 PATH）
yosys	0.68	SystemVerilog → SMT2	CSRFORMAL_YOSYS
firtool	1.135.0	CHIRRTL → SystemVerilog	CSRFORMAL_FIRTOOL
JDK + Scala 2.13 编译器	与 XiangShan 一致	精化 harness	CSRFORMAL_JAVA
gh	任意	解析规范仓库分支名（钉死 sha 时只需 curl 拉 tarball）	—（Docker 镜像不装；demo-spec-drift.sh 对照 main 请在宿主机跑，或传入 40 位 sha）

版本与获取方式见 scripts/versions.txt。本仓库不安装这些外部工具。

Python

pip install -r requirements.txt        # 只有 z3-solver

XiangShan 工作树与 classpath

精化需要一份已经 mill 编译过的 XiangShan 工作树（产物在 out/），用环境变量指向它，不要改源码里的路径：

export CSRFORMAL_XS_TREE=/path/to/compiled/XiangShan
# yosys / firtool 不在 PATH 里时：
export CSRFORMAL_YOSYS=/path/to/yosys
export CSRFORMAL_FIRTOOL=/path/to/firtool
# chisel-plugin 若不在 classpath 里：
export CSRFORMAL_CHISEL_PLUGIN=/path/to/chisel-plugin_2.13-*.jar

cp.txt 是本机 classpath（指向 $CSRFORMAL_XS_TREE/out/* 与 coursier 缓存）， 含绝对路径，不进仓库（已 gitignore）。生成：

./scripts/gen-cp.sh                 # 写出 ./cp.txt
# 或按 cp.txt.example 手工拼一份

换机器仍须自备预编译香山树。登记规模一节里的 XiangShan-b90dbba 是当时跑数用的提交，不是本机路径。

怎么跑

# 1) 静态自检：性质元数据是否齐全，引用的规则 id 是否存在于规范中
./bin/csrformal lint

# 2) 记录规范基线（默认钉恢复后的 menvcfg_stce_op2；不要对权威文件用 f20aa35）
./bin/csrformal spec-baseline

# 3) 跑全部模块的全部性质，出报告
./bin/csrformal check all

# 只跑一个模块 / 只跑一条性质（调试用）
./bin/csrformal check CSRPermitModule
./bin/csrformal check CSRPermitModule --only S3

# 4) 规范漂移检测
./bin/csrformal spec-drift --ref main --json out/reports/spec-drift.json
# 把「需要重新审阅」的性质喂回去重跑
./bin/csrformal check all --review out/reports/spec-drift.json

# 5) 规格自洽（permit / trap_entry 的 Python 与 SMT）
./bin/csrformal spec-selfcheck

# 6) 变异回归（阳性对照）
./bin/csrformal self-test --report out/reports/self-test.md

# 辅助
./bin/csrformal list                 # 列出全部性质
./bin/csrformal rules --text         # 列出被引用的规则 id 及原文
./bin/csrformal spike-cex out/reports/compliance.json   # 反例 + M 态阳性对照；缺二进制则跳过
./bin/csrformal spike-cex --controls-only               # 只跑对照（M 读 0x24D / HS 读 0x14D）

产物：

• out/reports/compliance.md —— 人可读的符合性报告（摘要 / 规则追溯表 / 反例详情 / 全量清单）
• out/reports/compliance.json —— 结构化结果，逐条给出结论、耗时、规则 id、反例取值
• out/<tag>/<rtl_id>/m.sv、c.smt2 —— 中间产物；<rtl_id> 是树路径 / commit / 关键 .scala 的指纹。换 CSRFORMAL_XS_TREE 或 commit 会自动换目录，不靠 --rebuild。

退出码：反例 / 真空 / 未知 / 错误 → 1；全部 HOLDS 为 0。 --review / --only 若匹配到 0 条性质（或变异体），拒绝当作通过（退出 1）。

登记规模（XiangShan-b90dbba @ b90dbba4）

• CSRPermitModule 156 条（case + 3 条 MONO + 1 条 EQ）
• TrapHandleModule 140 条
• TrapEntryMEventModule / TrapEntryHSEventModule 各 3 条 EQ （EQ-next：SIE/PP/cause；EQ-tval：tval2/GVA；EQ-tval-data： mem=memVA / inst=指令位 / zero=0。 epc / VS 后置，未验收。BP/SWC/HWE 与 fetch PC/PC+2（genTrapVA WARL）排除）
• TrapEntryDEventModule 精化后 registers≠0，跳过，不假装时序完整
• 当前红的是 CSRPermit/S3 与 CSRPermit/EQ-permit，反例都是 vstimecmp + menvcfg.STCE=0 一类。EQ 绿只表示「已建模条款 + 假设关掉的路径」 下 RTL 与规格一致，不等于符合整本规范。
• 精化缓存键含 RTL 树身份和 src/eqcheck/Elab2.scala。不要无故 --rebuild。 --rebuild 会连 harness class 一起重编。

规范漂移 demo

./bin/demo-spec-drift.sh

复现的是一起真实的规范编辑事故：

时间	事件
2025-12-16	riscv-isa-manual PR #2504（纯文本搬运）误删了 norm:menvcfg_stce_op2 里的 “or vstimecmp”
2026-06-24	提交 94a4b91a 按被删后的文本去掉 vstimecmp 门控，经 XiangShan PR #6243 进入 v3。PR #6129 Closed 未 merge（与 NEMU PR #1093 同时段提出，不是进树路径）
2026-08-20	riscv-isa-manual issue #3329 指出这是编辑事故
2026-08-24	PR #3344 恢复原文，当前 main 已是恢复后的文本

结果是 94a4b91a 按当时规范文本改的实现，被后来的规范勘误反转 （pc1 回滚的就是这份提交，不是未 merge 的 #6129）。demo 把一份旁路基线固定在 2026-06-14 （f20aa35，误删文本；不是 EQ 权威），再与当前 main 比对。权威基线 spec/baseline.json 钉在恢复后的原文（含 or vstimecmp）， spec-baseline 默认不会把权威文件拧回误删版。

[CHANGED] norm:menvcfg_stce_op2
  基线位置 priv/machine.adoc:2222  sha=59c33250aeb8103c
  当前位置 priv/machine.adoc:2223  sha=e56229e7534fd5f1
  词级差异（- 基线 / + 当前）
    + or `vstimecmp`
  受影响、需要重新审阅的性质
    * CSRPermit/EQ-permit
    * CSRPermit/S2
    * CSRPermit/S3
    * CSRPermit/S3b

demo 的第三步把这些性质拿去重跑当前 RTL，CSRPermit/S3 与 EQ 给出反例。

同一次比对还检出另外两条规则的文本变化：norm:hideleg_trans 删掉了一句关于平台中断的说明， norm:trap_unexp_hndl_rnmi 加了两个词。对应的 4 条性质被标为需重新审阅，重跑后仍然通过。 漂移检测只负责标出需要复核的范围，不给出结论。

变异回归（阳性对照）

./bin/csrformal self-test --report out/reports/self-test.md

13 个变体。2026-09-03 本机完整跑 13/13 符合预期（壁钟 114.7s）。 te1 只对 EQ-tval，te2 只对 EQ-tval-data（精确匹配，不再 startswith 串台）。tehs1 只改 HS 路径，没有它则 TrapEntryHS 三条 EQ 全绿不可信：

变体	类型	内容	结果
pc1	fix	回滚 94a4b91a：恢复 menvcfg.STCE 对 vstimecmp 的门控	FIXED（CSRPermit/S3 + EQ-permit）
m1	defect	mcounteren.TM 不再门控 vstimecmp	KILLED by S1b + EQ-permit
m2	defect	去掉 HU 态的 scounteren 检查	KILLED by C2 ×5
m3	defect	去掉 hstateen 对 sstateen 的门控	KILLED by E3 族 + EQ-permit（与 SE 规格重叠）
m4	defect	VS 计数器门控误用 scounteren 而非 hcounteren	KILLED by C3 ×5
t1	defect	hsEXVec 忽略 medeleg	KILLED by D2/D5 ×36
t2	defect	vsEXVec 忽略 hedeleg	KILLED by D4 ×18
t3	defect	handleTrapUnderHS 去掉 !isModeM	KILLED by D6 ×9
t5	defect	trapToHS 去掉 !vs_EX_DT	KILLED by DT2
pc3	defect	回滚 74fd4f59：VS 向量化入口 PC 用未映射的中断号	KILLED by V3 ×3
te1	defect	LS-GPF 的 mtval2 误用 trapPCGPA 而非 trapMemGPA	KILLED by TrapEntryM/EQ-tval
te2	defect	精确 tval 翻了 PC 与 memVA：mem 异常误写 trapPC	KILLED by TrapEntryM/EQ-tval-data
tehs1	defect	HS：LS-GPF 的 htval 误用 trapPCGPA 而非 trapMemGPA	KILLED by TrapEntryHS/EQ-tval

pc1 上一轮的类型是 defect（历史 bug 重放的阳性对照），依据是当时被误删了 “or vstimecmp” 的规范文本。规范恢复后该实现变成正确实现，因此改判为 fix 对照，职责是断言 F1 的建议改法 确实修好了这个 bug。若不改判，一条过期的阳性对照会持续以 SURVIVED 的形式报出。

架构

bin/csrformal              入口（bash → csrformal.cli）
bin/demo-spec-drift.sh     规范漂移自证 demo
csrformal/
  config.py                路径与外部工具配置（环境变量可覆盖）
  props.py                 Property / SpecRef 数据模型（含可选 prove_fn）
  spec_permit.py           CSRPermit 独立规格函数（等价性层；禁止抄 Chisel）
  spec_trap_entry.py       TrapEntry 陷入次态规格（别名表 + EQ；禁止抄 Chisel）
  specdb.py                规范规则库：adoc 锚点提取、原文哈希、基线、漂移比对
  elaborate.py             Chisel → CHIRRTL → SystemVerilog（含覆盖编译的硬校验）
  smt.py                   SV → SMT2 → z3（电路只 parse 一次，性质用 push/pop）
  runner.py                真空性门禁 + 求解 + 结构化结果
  report.py                Markdown / JSON 报告
  cli.py                   子命令
  spec_selfcheck.py        permit() 与 permit_smt() 自洽
  spike_oracle.py          反例定性（可选；缺 spike 跳过）
  modules/
    __init__.py            模块注册表（性质 + 源文件 + 变异体）
    csr_permit.py          CSRPermitModule 156 条（case + MONO + EQ）
    trap_handle.py         TrapHandleModule 的 140 条性质
    trap_entry.py          TrapEntry{M,HS} 的 EQ-next / EQ-tval / EQ-tval-data
src/eqcheck/Elab2.scala    最小精化 harness（把单个子模块当 top）
mutants-src/               变异体源码（base_* 与各变异版本）
spec/baseline.json         权威基线：恢复后的被引用规则原文
docs/spike-crosscheck.md   Spike 反例定性（未默认启用）

已验证的技术路径

1. firtool --btor2 不可用，不支持 n 元 comb.and。
2. 可工作路径：最小 harness 把目标模块当 top → firtool 出 SystemVerilog （必须加 --default-layer-specialization=disable）→ yosys read_verilog -sv → write_smt2 → z3。
3. 精化成本：TrapHandleModule 约 3 s、CSRPermitModule 约 4 s （MStatusModule 约 17 s、MipModule 约 54 s）。不需要整核精化。
4. 覆盖编译单个 .scala 时必须硬校验 scalac 退出码和产出的 .class 数量， elaborate.py 里两项都查。静默失败会让 classpath 悄悄回退到原始 class， 注入的缺陷不会进入 RTL，变异测试全部假通过。

registers=0

CSRPermitModule、TrapHandleModule 与 TrapEntry{M,HS}EventModule 精化后 registers=0，为纯组合逻辑，单周期求解即完整。 跨模块契约（irToVS ⇒ irToHS、intrVec ≤ 63、以及 TrapEntry 的 sstatus/mstatus 字段别名）未验证，作为假设处理，见「已知限制」。

怎么加一条新性质

编辑对应的 csrformal/modules/<模块>.py，用该文件里的 case() 助手加一行。 以 csr_permit.py 为例：

case("S9",                                        # pid（模块内唯一）
     "menvcfg.STCE=0 → HU 访问 stimecmp 抛 II",    # 一句话说明
     R["stce2"],                                  # 规范引用（见文件顶部的 R 表）
     "HU", RD, 0x14D, II,                         # 特权态、读/写、地址、期望输出
     menv=clr(ONES64, 63))                        # 相对 CLEAN 的偏离

三条硬要求：

1. 必须给 SpecRef，优先给 rule_id（norm: 开头的 asciidoc 锚点）。 没有对应锚点时（例如 AIA 在独立仓库、或性质是多条规则的组合）， 写 SpecRef(None, "出处", note="为什么没有 id")，不要凑 id —— 错误的 id 会让 spec-drift 比对错误的段落。
2. 假设集必须可满足。clean() 的整字默认值是「除被测位外全 1」， 要清某一位就用 clr() 传掩码，不要在 assumes 里另写一条相反的约束。 真空性门禁会兜底。
3. 加完跑一遍：

./bin/csrformal lint                          # 规则 id 是否存在
./bin/csrformal spec-baseline --ref main      # 新引用的规则要进基线
./bin/csrformal check <模块> --only S9

关系型性质（跨两份实例，例如特权单调性）直接构造 Property(kind="relational", free=[...])， free 里列出允许 A/B 取不同值的输入端口，其余输入由 runner 自动对齐。

等价性层和 case 层不是互相替换。case 钉死特权、地址、r/w，再用 clean() 关掉其它陷入源， SMT 只穷尽剩余自由位，职责是选点回归。等价性层（CSRPermit/EQ-permit）用独立规格函数 spec_permit.permit，在「已建模使能位自由、未覆盖路径按假设关掉」下证 (rtl.EX_II ↔ spec.II) ∧ (rtl.EX_VI ↔ spec.VI)；地址、特权、ren/wen 全部自由，不再钉 0x14D。 规格只来自特权规范 / SpecRef，禁止把 RTL 比较器翻译进去。本轮覆盖 Privilege、 只读写、Sstc、counteren、TVM，以及 Smstateen 的 SE/ENVCFG/CONTEXT/IMSIC/CSRIND （手册点名的 CSR）。未覆盖条款（XRet、FS/VS off、AIA 其余含 stateen.AIA、 Smcdeleg 间接窗口内容、custom/stateen.C、scountinhibit/scountovf） 必须写成可满足的假设关掉，否则会被无关路径打红。合取型主定理用 prove_fn 出 z3 公式， 条款的 rule_id 放 extra_refs，不要给合取硬凑一个 id。

怎么加一个新模块

以 InterruptFilter 为例，四步：

1. 确认 harness 能构造它。src/eqcheck/Elab2.scala 的 build() 里加一行 case "InterruptFilter" => new xiangshan.backend.fu.NewCSR.InterruptFilter （这一条已经在了）。若模块构造需要额外参数，在这里补。 删掉 out/_harness_classes/.ok 让它重编。

2. 先看端口。精化一次，用端口名写性质：

python3 -c "
import sys; sys.path.insert(0,'.')
from csrformal import elaborate, smt
sv = elaborate.elaborate('InterruptFilter','base_InterruptFilter')
c  = smt.Circuit(smt.sv_to_smt2(sv,'InterruptFilter','out/base_InterruptFilter/c.smt2'),'InterruptFilter')
print(sorted(c.ins)); print(sorted(c.outs)); print('regs',len(c.regs))
"

regs 不为 0 表示该模块有时序状态，单周期求解只覆盖组合部分， 必须在性质里说明；改用多周期展开本工具目前不支持。

3. 新建 csrformal/modules/interrupt_filter.py，导出 MODULE 与 PROPS （照抄 trap_handle.py 的结构：一个 CLEAN、一个 case() 助手、一张 R 规范引用表）。

4. 在 csrformal/modules/__init__.py 的 _build() 里登记一行 ModuleSpec(...)， 同时登记变异体。没有阳性对照，新模块的「全部通过」不可信。

变异体的做法：把 XiangShan/.../<Module>.scala 拷进 mutants-src/<id>_<Module>.scala， 改一处逻辑，在 ModuleSpec.mutants 里写清 expect_kill（pid 后缀精确匹配； 带下标的族用 D2 匹配 D2[...]。EQ-tval 不会吃到 EQ-tval-data）。

已知限制

1. 单周期组合逻辑。目前 CSRPermit / TrapHandle / TrapEntry{M,HS} 都是 registers=0，单周期即完整；但工具不支持时序展开， 有状态的模块加进来只能覆盖组合部分。扩展到 MStatus/Mip 等有状态模块需要 BMC/归纳，与当前组合 EQ 不是同一工程量级。
2. 跨模块契约是假设。TrapHandleModule 的输入 irToHS / irToVS / intrVec 由 InterruptFilter 产生，二者之间的约束（如 irToVS ⇒ irToHS）未被验证。
3. 43 条规则里有一部分性质没有规则 id：AIA 在独立仓库 riscv/riscv-aia， 没有 norm: 锚点体系；特权单调性是结构性元性质，不对应单条条文。 这些在报告的「规范规则追溯」一节里逐条列出了原因。
4. 未覆盖的模块：InterruptFilter（由另一项工作进行中）、XRetPermitModule （MRET/SRET/DRET/MNRET，与 debug 规范耦合）、MStatusModule、MipModule、 TrapEntryDEventModule（registers≠0，跳过）、TrapEntryVS/MN 的 EQ （VS/epc 后置，本轮未验收）。
5. 未覆盖的条款：异常优先级表（规范把若干异常放在同一优先级组、组内无序， 且把 load/store 地址不对齐相对页错误定为实现自定义，香山的差异落在规范 未约束的自由度内）、AIA iprio 窗口的奇偶规则、fp/vec 的 mstatus.FS/VS、 custom CSR 地址段。
6. 配置相关：结论基于 MinimalConfig（geilen=7），vgein 相关性质依赖该参数。
7. Spike 只做反例定性，不穷举。check --spike / spike-cex 未默认启用； 本机没有能跑的 spike 时跳过。spike-cex 会顺带跑 M 态读 0x24D 的阳性对照， 见 docs/spike-crosscheck.md。
8. spec-drift 只检测被引用规则的文本变化，不检测「规范新增了一条我们没写性质的规则」。
9. CSRPermit/EQ-permit 覆盖 Privilege、只读写、Sstc、counteren、TVM， 以及 Smstateen 的 SE/ENVCFG/CONTEXT/IMSIC/CSRIND。未覆盖条款靠假设关掉。 TrapEntryM/EQ-next 与 TrapEntryHS/EQ-next 只比 SIE/PP/cause。 EQ-tval 比 tval2（LS-GPF=GPA>>2，非 GPF=0）和 GVA（GPF=1，中断/ecall=0）。 EQ-tval-data 比精确 xtval：mem=memVA、inst=指令位、zero=0。 fetch 的 PC/PC+2 写在 spec_tval()，不进 prove（genTrapVA WARL； 试过低 39 位，反例是非法 satp.MODE / iMode，五道关不可达，不抄 Mux）。 isFetchMalAddr / isCrossPageIPF 不钉在假设里；data 条只在 implication 前件排除取指畸形覆盖通道。BP（0 或 PC）、SWC、HWE、 IGPF 的 tval2、非叶 PTE 排除。epc / VS 后置，未验收。 EQ 绿 ≠ 符合整本规范。假设太松会被无关条款打红，应收紧假设或扩规格， 不要抄比较器凑绿。

可复现性（两层）

层 1（不精化）：python -m compileall、./bin/csrformal list、lint、 spec-selfcheck。不需要 cp.txt，也不需要 yosys / firtool / 香山树。 GitHub Actions 和 Dockerfile 只覆盖这一层。

层 2（精化 / check / 变异回归）：需要已编译的 XiangShan 工作树、 CSRFORMAL_XS_TREE、本机 cp.txt，以及 scripts/versions.txt 里的 yosys / firtool / JDK。换机器做不到一键复现；CI 不跑 check CSRPermitModule。

Dockerfile 装 Python 与 z3-solver，并提示外部工具。镜像里通常没有 firtool 1.135.0 / yosys 0.68，也不装 gh（避免镜像膨胀）。 demo-spec-drift.sh 默认对照 main 时需要宿主机 gh；也可传入 40 位 sha。 缺 gh 时脚本会直接失败并说明原因。精化请用宿主机或 xs-env。此镜像未当作 「已验证可复现精化」的证据。

相关工作

• riscv-formal / SymbiYosys：检查 RVFI 指令迹，不是香山 Chisel CSR 子模块精化。
• Sail / Isla：可执行 ISA；香山 RTL 不从 Sail 生成。
• 本工具：从香山 Chisel 切片精化，性质带规范锚点哈希，并用 spec-drift 标出该重审的范围。EQ 是带假设的局部等价，不能替代上述工具。

参考

• 被测源码：已编译 XiangShan 工作树中的 src/main/scala/xiangshan/backend/fu/NewCSR/ （CSRPermitModule.scala、TrapHandleModule.scala、 CSREvents/TrapEntry{M,HS}Event.scala）
• 规范：riscv/riscv-isa-manual，src/priv/*.adoc
• License：Mulan PSL v2