ARM架构验证Co-Simulation盲区系统化分析方法论

背景：在前序工作《ARM架构验证中ISA仿真无法覆盖的测试点分析》中，我们通过关键词扫描（P0/P1/P2）识别了40个co-simulation blind spot。过程中发现了一个核心问题——EPDn盲区被遗漏了。根因是关键词”TLB miss”不在扫描模式中。这触发了更深层的思考：关键词扫描永远有漏，我们需要一个不依赖特定关键词的系统化方法论。

本文定义从架构规范结构出发的盲区分析方法：从关键词驱动的第一层扫描，到架构不变式驱动的第二层结构扫描，再到章节深度分析的第三层。这套方法论的目标是让盲区发现过程可重复、可审计、可改进。

1.1 通用条件

一个架构行为是 co-simulation blind spot 当且仅当：

架构规范将行为的定义建立在 ISA 仿真器无法复现的微架构状态或事件之上。

即：规范定义的行为路径选择依赖一个条件 C，ISA 总是取路径 P1（因为 ISA 没有 μarch 状态），而 RTL 可以取 P2（因为 RTL 有 μarch 状态），且 P1 与 P2 产生软件可观察的差异。

1.2 三个具体表现形式

#	形式	描述	示例
1	State caching	架构允许某个检查结果被 TLB/cache 缓存，ISA 无缓存→每次重做检查	Permission fault 缓存、EPDn
2	Event sensitivity	行为触发条件为 μarch 事件（mispredict、TLB miss、speculative access）	Speculative AF 更新、debug+speculation
3	Timing dependence	行为或结果依赖于物理时间/周期数	PMU 事件计数、RNDR NZCV

1.3 可观察差异三角

每个盲区候选需要验证以下三个角：

                +-- fault vs no fault (异常与否)
                |
ISA vs RTL  --> +-- data value (数据值)
  差异          |
                +-- syndrome encoding (错误信息编码、ESR_ELx 等)

只有至少一个角产生 ISA/RTL 差异，才是真正盲区。

2. 整体方法论架构

第一层: Keyword Scanning
  → 快速广泛覆盖
  → 局限: 漏掉未知关键词
  
第二层: Structural Pattern Scanning  
  → 系统完备覆盖
  → 基于规范自身的结构化模式

第三层: Chapter Deep-Dive
  → 逐章节人工分析
  → 覆盖前两层都漏掉的边缘情况

每层输出如下：

第一层输出: keyword_hits.json (P0/P1/P2 分类)
    ↓ 过滤已覆盖项
第二层输出: structural_patterns.json (序列/cached/条件触发)
    ↓ 合并去重
第三层输出: final_blindspots.json (带 impact 评估)
    ↓ 写入 blog

3. 第一层：Keyword-Based Scanning

3.1 原理

定义一组关键词，用正则表达式搜索 ARM ARM PDF。每个 hit 标记一个潜在盲区。

3.2 关键词分类体系

P0（高精度盲区指示词——命中几乎总是盲点）

类别	关键词	目标盲区类型
推测执行	mispredict	推测执行的 ISA 不可见性
推测效果	speculative access / speculative load / speculative store	推测性架构状态修改
TLB 冲突	TLB conflict abort	中间 TLB 结构
TLB 缓存	cached in TLB	TLB stale entry 问题
周期计数	cycle count / cycle counting	时序依赖行为
随机数	random number / RNDR	不可预测结果
SVE FF	first fault / first-fault	SVE first-fault 加载
Trace atoms	trace atom / atom element	ETE/TRBE
Debug+spec	breakpoint + committed / watchpoint + speculative	Debug 与推测交互

P1（需要上下文判断——命中可能需要人工确认）

类别	关键词	目标盲区类型
Cache/TLB hit/miss	cache hit / cache miss / TLB hit / TLB miss	缓存相关盲区
Cache 维护	cache maintenance	Cache 维护操作
推测执行	speculative instruction / speculative execution	推测上下文
Refill	cache refill / TLB refill	fill 行为
指令顺序	instruction order / order of instructions	内存顺序
异常返回顺序	exception return address	ERET 相关顺序
随机值	random value / UNKNOWN / unpredictable	未指定值
非错误访问	non-fault access / non-fault load	NFU 加载
SVE FF	first-fault	SVE first-fault

P2（PMU 微架构事件名——PMU 专用）

所有 _ARCHITECTED 宏和标准 PMU 事件名：L1D_CACHE_REFILL、STALL_FRONTEND、MEM_ACCESS、BUS_ACCESS 等。

3.3 执行步骤

1. 将 ARM ARM PDF 按章节分文件
2. 对每个 PDF 运行正则扫描
3. 每类关键词的结果写入 JSON
4. 标记已覆盖章节（D13/D14/D17/D18/D4-D6/D19/D2/D8/D7/K1 等）
5. 未覆盖章节的 hits 进入 deep-dive 分析

3.4 已知局限

模式完整性: 一个类别可能只覆盖了部分关键词（如 cache_tlb_hit_miss 漏掉了 TLB hit/miss）
上下文敏感: 同一关键词在不同语境含义不同（如 “UNKNOWN” 可能是 reset 状态的合法描述）
跨类别盲区: 有些盲区由多个关键词组合产生（如 debug + speculation，需要两个模式同时命中同一段落）

4. 第二层：Structural Pattern Scanning

这是本方法论的核心改进。第一层扫描依赖关键词，而第二层扫描依赖 ARM ARM 规范自身的结构化模式。

4.1 核心理念

ARM ARM 在描述盲区易感行为时，使用了固定的语言模式。这些模式本身就是盲区指示器。识别这些模式，比记忆所有关键词更系统、更完备。

4.2 三种结构化模式

方法 A：Step-by-Step Sequence Audit（序列分析）

目标：分析规范中的编号行为序列，识别哪些步骤被 μarch 缓存绕过。

适用对象：ARM ARM 中以编号列表形式出现的行为序列。

已知序列：

D8.15.4 MMU fault checking sequence（15 steps）
D8.15 FETCH descriptor sequence

执行步骤：

1. 找到章节中的编号序列
2. 对每一步 Sn，问：
   a. Sn 的检查是在 translation table walk 时做吗？
   b. Sn 的结果被缓存在 TLB entry 中吗？
   c. 如果是 → TLB hit 时 Sn 被绕过
   d. Sn 被绕过是否产生可观察差异？（fault/no fault、data、syndrome）
3. 枚举所有影响 Sn 的 control field（寄存器和页表字段）
4. 对每个 control field：软件改变该字段后，TLB stale entry 是否导致 Sn 结果不同？
5. 如果是 → CONFIRMED BLIND SPOT

示例（D8.15.4 Step 2）：

Step 2: Check IA maps to TTBR
  - TLB cached? YES (TLB entry proves valid mapping)
  - Control fields: TCR_ELx.EPD0/EPD1
  - Software changes EPDn → TLB has stale mapping → ISA misses EPDn=1,
    RTL hits TLB → bypasses EPDn check → BLIND SPOT ✓

D8.15.4 完整序列分析表：

Step	检查内容	TLB 缓存?	已覆盖?
1	Alignment check	否(每次检查)	非盲区
2	IA→TTBR mapping (EPDn)	是	✅ 1.8
3	TTBR address size	是	⭕ 候选
4	Fetch descriptor	walk-time only	非盲区
5	Descriptor valid	是	⭕ 候选
6	Descriptor address size	是	⭕ 候选
7	Descriptor type (table/block/page)	是	非盲区(只影响walk)
8	BBML1 nT check	是	⭕ 候选
9	AF bit check	是	✅ 部分
10	AF HW update	walk-time only	✅ 推测AF
11	Get OA and OA space	是(缓存)	非盲区
12	OA alignment	是	⭕ 候选
13	OA space access permissions	是	✅ 1.1
14	Dirty state HW update	walk-time only	⭕ 候选
15	Return OA and attributes	是(缓存)	非盲区

⭕ 候选中，还需要确认对应的 control field 是否可以被软件独立修改（在TLB fill 之后修改）。

方法 B：”permitted to be cached in a TLB” Registry Audit（Cached 清单审计）

目标：ARM ARM 使用固定的语言 "X is permitted to be cached in a TLB" 系统性地标注哪些字段可以被 TLB 缓存。每一个这样的声明都是 blind spot 候选——因为 ISA 没有缓存，总是重新读取 X。

适用对象：D8、D24 中所有 permitted to be cached in a TLB 声明。

执行步骤：

1. 提取所有 "X is permitted to be cached in a TLB" 及 "X is not permitted to be cached in a TLB"
2. 消除已覆盖项（Permission fault、CnP、Conflict Abort、非缓存fault）
3. 对剩余项分析：
   a. X 被软件修改后，TLB 中旧 entry 是否继续使用 X 的旧值？
   b. 使用旧值是否导致与 ISA 走不同路径？
   c. 差异是否软件可观察？
   d. 是否存在一个合理的 test scenario 能触发？
4. 每项一个 BLIND SPOT / NOT_A_BLIND_SPOT 判定

D8 已知清单节选：

字段	可缓存?	盲区状态
Translation table entry (正常)	YES	基础机制
Permission fault entry	YES	✅ 已覆盖
SCTLR_ELx.WXN	YES	✅ 已覆盖
PSTATE.PAN + Base permissions	YES	⭕ 待分析
PrivWXN / UnprivWXN	YES	✅ 已覆盖
POE field	NO	非盲区
E0POE field	NO	非盲区
POIndex	YES	⭕ 待分析
SCR_EL3.SIF	YES	✅ 已覆盖
HAFT (AF/Dirty HW mgmt)	YES	⭕ 待分析
AMAIR2_ELx.Attr<n>	YES	⭕ 待分析
HCR_EL2.E2H	YES	✅ 已覆盖
HCR_EL2.{NV, NV1}	YES(impl-def)	⭕ 待分析
TTBR_ELx.CnP	YES	✅ 已覆盖
PTTWI	YES	⭕ 待分析

分析方法模板：

Field: SCTLR_ELx.WXN
Spec: "WXN is permitted to be cached in a TLB"
Blind Spot Scenario:
  1. TLB fill → entry 缓存了 WXN=0 时的权限
  2. 软件设置 WXN=1 → 要求写权限不能同时有执行权限
  3. 再次访问同一 VA
     RTL: TLB hit → 用 entry 中缓存的旧权限 → 执行可能仍被允许
     ISA: 无 TLB → 重新检查 WXN=1 → 执行被阻止
Impact: HIGH（直接决定访问能否成功）

方法 C：Conditional Trigger Analysis（条件触发器分析）

目标：搜索以 μarch 事件为触发条件的架构声明。

核心洞察：ISA 没有 μarch 状态，所以所有以 μarch 状态为条件的声明，ISA 总是取同一个分支。

可搜索的条件短语列表：

条件短语	代表盲区	发现方式
“when a TLB miss occurs”	EPDn, NFDn, E0PDn	全文搜索 `tlb miss`
“as a result of speculation”	Debug watchpoint + speculation	P0 `debug_spec`
“on a TLB hit”	伪代码中的条件分支	全文搜索 `tlb hit`
“permitted to” (as μarch permission)	多种 μarch 可选行为	方法 B 已覆盖
“on a mispredict”	Trace atom 修复	P0 `trace_atom`

执行步骤：

1. 对每个条件短语 P，全文搜索所有 PDF
2. 对每个匹配，问：
   a. ISA 总是取哪个分支？(总是 TLB miss / 总是 committed / 总是非推测)
   b. RTL 能否取另一个分支？(TLB hit / 推测执行等)
   c. 两个分支产生不同的可观察结果？
3. 每项一个判定

5. 第三层：Chapter Deep-Dive（章节深度分析）

5.1 适用场景

前两层扫描完成后，对每个章节做一次人工深度阅读，捕获前两层遗漏的盲区。

5.2 执行步骤

1. 对目标章节，阅读其所有 subsection title
2. 对每个 subsection，标注其功能（寄存器描述、行为序列、fault 条件等）
3. 对行为描述类 subsection，应用第二层方法 A/B/C
4. 对寄存器描述类 subsection，提取所有 "permitted to be cached" 声明
5. 对 fault 条件类 subsection，列出所有 fault 类型和触发条件
6. 每个 fault 触发条件，问：ISA 对该条件的建模是否与 RTL 一致？

6. 完整执行流程

6.1 对新章节的探索流程

Start: 新章节 X
  │
  ├── Step 1: 推导 X 领域的盲区充分条件
  │     例: TLB → "缓存状态绕过检查"
  │     例: Cache → "ISA 无 cache 结构"
  │     例: Debug → "ISA 不推测执行"
  │     例: PMU → "ISA 无 μarch 事件"
  │
  ├── Step 2: 第一层 Keyword Scan
  │     - 对 X 运行 P0/P1/P2 所有模式
  │     - 输出 x_p0_hits.json, x_p1_hits.json
  │
  ├── Step 3: 第二层 Structure Scan
  │     - A: 找 X 中编号序列，逐步骤分析
  │     - B: 找 X 中 "permitted to be cached" 声明
  │     - C: 找 X 中 μarch 条件短语匹配
  │     - 输出 x_structural_hits.json
  │
  ├── Step 4: 交叉验证
  │     - 消除关键词和结构扫描的重叠
  │     - 对每个候选做可观察差异三角验证
  │
  └── Step 5: Impact 评估
        - HIGH: 直接导致 co-sim mismatch，场景常见
        - MEDIUM: 需要特定配置/场景才能触发
        - LOW: 边界情况，几乎不影响主流验证

7. EPDn 漏检案例分析

用本方法论回溯 EPDn 的漏检原因和正确检测路径，说明方法论改进的必要性。

漏检原因

第一层 cache_tlb_hit_miss 模式只实现了 cache hit/miss，没有 TLB hit/miss
EPDn 未被任何其他模式覆盖
D8 被标记为 “P0 已覆盖”，没有重新做第二层扫描

正确检测路径

路径 1（方法 A - 序列分析）：

D8.15.4 Step 2 分析:
  → Step 2 检查被 TLB hit 绕过
  → 枚举影响 Step 2 的 control field: EPDn
  → 分析 EPDn 修改后的 stale entry 行为
  → BLIND SPOT ✓

路径 2（方法 C - 条件触发）：

全文搜索 "when a TLB miss occurs"
  → 匹配 D8 + D24 中 EPDn, E0PDn, NFDn 的描述
  → 对每个分析: ISA 总是 TLB miss → 控制字段总是生效
  → RTL 可能 TLB hit → 控制字段被绕过
  → BLIND SPOT ✓

路径 3（第一层加强）：

1
2
3

在 cache_tlb_hit_miss 中加入 "tlb hit" 和 "tlb miss"
  → 重新扫描 D8 → 命中 EPDn 描述
  → deep-dive 分析 → BLIND SPOT ✓

方法论价值

EPDn 案例验证了方法论的核心主张：第二层结构扫描发现的盲区，第一层关键词扫描可能遗漏；但第一层补全后的关键词可以覆盖第二层发现的同类盲区。两层互为补充，交叉验证。

8. 后续工作指引

按本方法论继续探索新盲区时：

新领域优先用第二层：不要先列关键词。先推导该领域的盲区充分条件，然后找规范中对应的结构化模式。
第一层补全常规：同时对已知 P0/P1 模式做完整性检查——确认每个模式的 regex 是否覆盖了所有相关术语。
交叉验证：第二层发现的每个候选盲区，回头用第一层关键词确认——如果关键词能命中但不是盲区，调整关键词。如果第二层发现了关键词没命中的盲区，补全关键词。
方法论本身迭代：如果在深度分析中发现新的结构化模式，加入第二层的方法集。

关联阅读：《ARM架构验证中ISA仿真无法覆盖的测试点分析（完整版）》——应用本方法论产出的 40 个具体 blind spot 清单及分析。

1. Co-Simulation Blind Spot 的充分条件

1.1 通用条件

1.2 三个具体表现形式

1.3 可观察差异三角

2. 整体方法论架构

3. 第一层：Keyword-Based Scanning

3.1 原理

3.2 关键词分类体系

P0（高精度盲区指示词——命中几乎总是盲点）

P1（需要上下文判断——命中可能需要人工确认）

P2（PMU 微架构事件名——PMU 专用）

3.3 执行步骤

3.4 已知局限

4. 第二层：Structural Pattern Scanning

4.1 核心理念

4.2 三种结构化模式

方法 A：Step-by-Step Sequence Audit（序列分析）

方法 B：”permitted to be cached in a TLB” Registry Audit（Cached 清单审计）

方法 C：Conditional Trigger Analysis（条件触发器分析）

5. 第三层：Chapter Deep-Dive（章节深度分析）

5.1 适用场景

5.2 执行步骤

6. 完整执行流程

6.1 对新章节的探索流程

7. EPDn 漏检案例分析

漏检原因

正确检测路径

方法论价值

8. 后续工作指引