第四章ARCH 架构建模

概述

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

Use Models

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

工作流程

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

Getting Started

加载模块

官方工作流图把这一步标为 Load/analyze/elaborate，对应命令是 check_arch -load。在 GUI 中对应 Arch. Model 按钮组里的 Load/Bind Spreadsheet/Murphi Module 按钮，默认选中 Load as top module。

用 Visualize 确认

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

自动生成的属性类型

• Row Covers：每行规格是否可达
• Full Checks：确保任何时刻至少有一行被引用（发现规格漏洞）
• Parallel Checks：确保任意两行不重叠（发现规格歧义）

下面是官方示例工程 example_jaspergold_apps/ARCH/ARCH_example.tcl 的完整流程：

clear -all
set_visualize_auto_check_props on

# Load the Archtectural Model
check_arch -load L1L2.xml

# Limit the proof time
set_prove_per_property_time_limit 10s
set_prove_time_limit 30s

# Prove the Arch Model
check_arch -prove

# Report results
report

# Visualize parts of the Arch Model
visualize -violation -property {<embedded>::L1L2.AST_table_L1_CMP_full} -new_window

注意自动生成的属性名形如 <embedded>::L1L2.AST_table_L1_CMP_full，由模型名和表格行/检查类型拼成。

除示例中的 check_arch -prove 外，官方工作流图中也给出了通用的证明命令：

# 证明所有 task 中的全部 assertion 和 cover
prove -all

# 证明指定 task
prove -task <task_name>

也可以在 Property Table 或 Source Browser 中多选属性后批量证明。

ARCH 文件格式

ARCH App 读入的是基于表格的模块描述，需要保存为 Microsoft Excel 2003 或 2004 XML 格式（官方示例即为 L1L2.xml）。表格内容包含：

• 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 的路由规则
• 任何可以用状态转换表或决策表描述的行为

三类自动属性的含义

三者都在检查规格表本身写得好不好，而不只是检查 RTL：

反例解读

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