第一章第一个实验：跑通 FPV

本章通过官方提供的示例工程，快速体验 JasperGold FPV 的完整流程。示例设计是一个简单的 SoC 互联结构，包含 arbiter（仲裁器）、bridge（桥接）、ingress/egress（入/出端口）和 port_select（端口选择）模块。

运行示例

进入示例目录后，执行以下命令：

cd doc/example_jaspergold_apps/FPV
jg -fpv FPV_verilog_sva_example.tcl -proj ~/jgproject

JasperGold 将启动 GUI，加载设计并运行证明。

Tcl 脚本逐行解读

示例脚本 FPV_verilog_sva_example.tcl 展示了 FPV 的标准流程：

example_jaspergold_apps/FPV/FPV_verilog_sva_example.tcl

# ----------------------------------------
#  Copyright (c) 2017 Cadence Design Systems, Inc. All Rights
#  Reserved.  Unpublished -- rights reserved under the copyright 
#  laws of the United States.
# ----------------------------------------

# Analyze design under verification files
set ROOT_PATH ../designs/reference_design/verilog_sva
set RTL_PATH ${ROOT_PATH}/source/design
set PROP_PATH ${ROOT_PATH}/source/properties

analyze -verilog \
  ${RTL_PATH}/arbiter.v \
  ${RTL_PATH}/port_select.v \
  ${RTL_PATH}/bridge.v \
  ${RTL_PATH}/egress.v \
  ${RTL_PATH}/ingress.v \
  ${RTL_PATH}/top.v

# Analyze property files
analyze -sva \
  ${PROP_PATH}/bindings.sva \
  ${PROP_PATH}/v_arbiter.sva \
  ${PROP_PATH}/v_bridge.sva \
  ${PROP_PATH}/v_ingress.sva \
  ${PROP_PATH}/v_egress.sva \
  ${PROP_PATH}/v_port_select.sva
  
# Elaborate design and properties
elaborate -top top

# Set up Clocks and Resets
clock clk
reset ~rstN

# Get design information to check general complexity
get_design_info

# Prove properties
# 1st pass: Quick validation of properties with default engines
set_max_trace_length 10
prove -all
#
# 2nd pass: Validation of remaining properties with different engine
set_max_trace_length 50
set_prove_per_property_time_limit 30s
set_engine_mode {K I N} 
prove -all

# Report proof results
report

步骤解析

1. 设置路径

set ROOT_PATH ../designs/reference_design/verilog_sva
set RTL_PATH ${{ROOT_PATH}}/source/design
set PROP_PATH ${{ROOT_PATH}}/source/properties

定义 RTL 源文件路径和属性（SVA）文件路径。

2. 分析 RTL 设计

analyze -verilog \
  ${{RTL_PATH}}/arbiter.v \
  ${{RTL_PATH}}/port_select.v \
  ${{RTL_PATH}}/bridge.v \
  ${{RTL_PATH}}/egress.v \
  ${{RTL_PATH}}/ingress.v \
  ${{RTL_PATH}}/top.v

analyze 命令读取并编译 Verilog 源文件。支持的语言选项包括 -verilog、-vhdl、-sva、-psl。

3. 分析属性文件

analyze -sva \
  ${{PROP_PATH}}/bindings.sva \
  ${{PROP_PATH}}/v_arbiter.sva \
  ...

SVA 属性文件包含断言定义。bindings.sva 使用 SystemVerilog 的 bind 语句将断言模块绑定到 RTL 模块上：

example_jaspergold_apps/.../bindings.sva

bind arbiter
  v_arbiter i_arbiter (
  .clk(clk), .rstN(rstN),
  .gnt(gnt), .req(req),
  .int_ready(int_ready), .int_valid(int_valid), .trans_started(trans_started)
);

bind bridge
  v_bridge i_bridge (
  .clk(clk), .rstN(rstN),
  .fifo_full(fifo_full), .wr_ptr(wr_ptr),
  .fifo_empty(fifo_empty), .rd_ptr(rd_ptr),
  .int_datavalid(int_datavalid), .int_datardy(int_datardy),
  .int_ready(int_ready), .int_valid(int_valid)
);

bind egress
  v_egress i_egress (
  .clk(clk), .rstN(rstN),
  .eg_valid(eg_valid),
  .eg_ready(eg_ready),
  .int_datavalid(int_datavalid),
  .int_datardy(int_datardy)
);

bind ingress
  v_ingress i_ingress (
  .clk(clk), .rstN(rstN),
  .rd_ready(rd_ready), .wr_rd(wr_rd), .valid(valid), .ready(ready),
  .int_valid(int_valid), .int_ready(int_ready), .int_read_done(int_read_done)
);

bind port_select
  v_port_select i_port_select (
  .clk(clk),
  .int_ready0(int_ready0), .int_ready1(int_ready1),
  .int_ready2(int_ready2), .int_ready3(int_ready3),
  .ig_sel(ig_sel), .int_size(int_size),
  .int_size0(int_size0), .int_size1(int_size1),
  .int_size2(int_size2), .int_size3(int_size3)
);


// ------------------------------------------------------
// Copyright (c) 2017 Cadence Design Systems, Inc.
//
// All rights reserved.
//
// Jasper Design Automation Proprietary and Confidential.
// -------------------------------------------------------

bind 允许在不修改 RTL 源码的情况下，将断言模块实例化到目标模块内部。

4. 细化设计

elaborate -top top

elaborate 命令对设计进行细化（elaboration），解析层次结构、连接关系，准备证明数据库。-top 指定顶层模块。

5. 指定时钟和复位

clock clk
reset ~rstN

clock clk：声明全局时钟信号 clk
reset ~rstN：声明全局复位信号，~ 表示低有效复位

6. 获取设计信息

get_design_info

输出设计复杂度信息（状态数、寄存器数等），帮助评估证明难度。

7. 第一轮证明（快速验证）

set_max_trace_length 10
prove -all

先用较短的 trace length（10 个时钟周期）和默认引擎快速验证，可以较快发现浅层 bug。

8. 第二轮证明（深度验证）

set_max_trace_length 50
set_prove_per_property_time_limit 30s
set_engine_mode {{K I N}}
prove -all

对第一轮未 proven 的属性，加大 trace length 到 50，设置单属性时间限制 30 秒，并切换到引擎组合 K（K-Induction）、I（Interpolation）、N（BMC）进行更深度的证明。

9. 报告结果

report

输出所有属性的证明结果摘要。

这就是 FPV 的标准流程：分析 → 细化 → 时钟/复位 → 证明 → 分析结果。后续章节将详细讲解每个步骤。

界面截图

本章要点总结

跑完第一个实验后，你应该已经理解了以下核心概念：

FPV 的标准流程：analyze → elaborate → clock/reset → prove → report，所有 App 共享这个基本框架
两轮证明策略：先快后深，第一轮发现浅层 bug，第二轮深度证明
bind 机制：断言通过 bind 绑定到 RTL 实例，不需要修改 RTL 源码
Property Table：绿色 ✓ proven / 红色 ✗ failed / 黄色 bounded，这是所有 App 通用的结果展示方式

下一步：第二篇深入讲解 FPV 的环境搭建、SVA 断言编写、约束建模和结果分析。掌握这些核心技能后，第三篇的专项 App 就是在 FPV 基础上针对特定场景的自动化封装。

来源文档

jaspergold_apps_userguide.pdf
example_jaspergold_apps/FPV/