第四章ARCH 架构建模

概述

架构建模 App使用表格格式描述设计的高层架构行为，JasperGold 自动解析并生成形式属性进行验证，无需手写 SVA。

Use Models

• 高层需求验证：从架构文档直接验证 RTL 实现
• 架构一致性检查：验证 RTL 符合架构规格
• 设计文档可执行化：将表格规格转化为可验证的形式模型

工作流程

1. 以 ARCH 格式编写架构行为表
2. 加载 RTL 和 ARCH 文件
3. Visualize 确认加载正确
4. 自动生成属性并证明
5. 调试反例

Getting Started

加载模块

# 加载 ARCH 文件
analyze -arch arch_table.csv
elaborate -top top_module

用 Visualize 确认

在运行证明前，通过 Visualize 检查架构模型是否正确加载，信号映射是否正确。

自动生成的属性类型

• Row Covers：每行规格是否可达
• Full Checks：完整的行为一致性检查
• Parallel Checks：并行检查独立行

# 证明所有属性
prove -all

# 证明单个属性
prove -property arch_row_3

# 从 Source Browser 批量选择
# 在 GUI 中选择多行并点击 Prove

ARCH 文件格式

ARCH 文件使用表格格式（CSV 或 TSV），包含：

• Keywords：特殊关键字定义信号、条件、动作
• Row 1：信号名称和方向
• Row 2：信号类型/位宽
• Row 3：初始值/复位值
• Row 4+：行为规则行（条件 → 预期结果）

详细的 ARCH 格式语法参见附录：Architectural Modeling App Format。

调试反例

当 Full Check 失败时，JasperGold 生成反例波形，显示哪一行架构规格被违反以及具体信号值。

ARCH 架构建模界面

架构建模验证方法论

ARCH 的独特价值

传统 FPV 用 SVA 写断言，描述"某个属性必须成立"。ARCH 用表格描述完整的行为模型，自动生成全量属性，更适合：

• 缓存一致性协议（MESI/MOESI 状态转换）
• 通信协议（请求-响应-确认序列）
• arbiters/routers 的路由规则
• 任何可以用状态转换表或决策表描述的行为

三类自动属性的含义

反例解读

ARCH 失败时，反例显示哪一行（Row）的条件被违反。这直接对应到协议定义中的某条规则，定位效率比 SVA 反例高得多。