第六章Executable Specification
概述
Executable Specification GUI 可以与任何 JasperGold App 配合使用，用于：
- 以可执行文档描述设计特性和行为
- 创建报告增强设计理解
- 研究 RTL 变更对行为和结构的影响
它将文档和形式验证结合起来，使设计规格本身成为可执行的验证资产。
用表格做验证的思路
什么场景适合 Executable Spec
Executable Spec 特别适合规则明确、可以用表格描述的设计规范：
- 协议表格：总线协议（AXI/AHB/Wishbone）的VALID/READY 时序关系表
- 状态机转换表：状态转移条件和动作（比画状态机图更精确）
- 寄存器映射表：地址/访问类型/复位值表（CSR App 底层就是这个原理）
- 指令集表：处理器指令编码和行为表
和手写 SVA 的对比
| 维度 | 手写 SVA | Executable Spec |
|---|---|---|
| 门槛 | 需要学习 SVA 语法 | 填表即可，不需要断言经验 |
| 可读性 | 代码形式，只有写的人懂 | 表格形式，架构师也能 review |
| 覆盖度 | 取决于写断言的人想到了什么 | 自动生成全面的属性（Row/Full/Parallel） |
| 灵活性 | 可以描述任意复杂的时序 | 适合表格化的规则，复杂时序不如 SVA |
Executable Spec 将文档和验证合二为一：设计规格本身就是可执行的验证环境，规格更新后验证自动更新，不存在"文档和实现不一致"的问题。
来源文档
jaspergold_apps_userguide.pdf Ch.11