3. Jasper用户界面与工程管理

Jasper 的日常使用并不是“打开一个软件然后点按钮”这么简单。它本质上是一套以 Tcl 命令为核心、以工程目录为载体的验证环境：图形界面（Jasper Apps）负责可视化与交互，命令行负责可复现的自动化，而工程目录负责把源码、脚本、编译产物和结果组织在一起。理解这三者的分工，是后续所有形式验证工作的基础。

Jasper Apps 界面构成

Jasper Apps 启动后，主窗口通常由几个固定区域组成。顶部是菜单栏与工具栏，提供 File、Edit、Compile、Window、Help 等入口；左侧是设计层次与属性浏览区，用于查看模块实例树、信号列表和属性状态；中部是主工作区，可切换显示源码、属性列表、波形、原理图等视图；底部是 Tcl 控制台（Console），所有图形操作最终都会在这里生成对应的 Tcl 命令，也可以直接输入命令执行。右侧或浮动窗口通常是属性/任务面板，显示当前选中对象的详细信息。

这种布局的关键价值在于“图形与命令一一对应”。在 Console 中可以看到每条操作对应的命令，例如点击编译按钮会生成 compile 相关命令，选中属性会生成 get_property_list 之类的查询。养成观察 Console 的习惯，能快速把界面操作转化为可脚本化的命令，这是从“会用界面”到“会做工程”的分水岭。

工程创建与目录组织

一个规范的 Jasper 工程通常包含以下目录结构（示例）：

my_jasper_proj/
├── rtl/                # 设计源码
│   ├── top.v
│   └── sub_module.v
├── props/              # 属性文件
│   ├── arbiter.sva
│   └── fifo.sva
├── scripts/            # Tcl 脚本
│   ├── setup.tcl
│   ├── compile.tcl
│   └── prove.tcl
├── work/               # 编译与运行产物
└── jasper.tcl          # 工程入口脚本

创建工程时，推荐用 new_project 或直接在目标目录下启动 Jasper，然后通过 set_property 设置工程属性。关键属性包括：project_root 指定工程根目录，source_files 指定 RTL 文件列表，include_dirs 指定头文件搜索路径，define 指定宏定义。这些属性决定了后续编译时工具如何解析设计。

文件组织上有一个常见原则：RTL、属性、脚本、产物分离。不要把编译生成的 work/ 目录提交到版本库，也不要把属性文件散落在 RTL 目录中。属性文件按功能模块命名（如 arbiter.sva、fifo.sva），便于定位和复用。

编译流程

Jasper 的编译流程可以概括为“读入设计 → 解析 → 建立模型 → 检查”。典型命令序列如下：

# 1. 清空当前工程状态
clear -all

# 2. 读入 RTL 文件
analyze -sv09 rtl/top.v
analyze -sv09 rtl/sub_module.v

# 3. 指定顶层模块并精化
elaborate -top top

# 4. 检查设计完整性
check_design -all

analyze 负责语法解析，把源文件读入内存；elaborate 负责把模块实例化关系展开，建立完整的层次模型；check_design 用于检查未连接端口、多驱动、组合环等常见问题。编译阶段如果报错，通常集中在语法错误、模块找不到、端口宽度不匹配这几类，Console 会给出文件名和行号，直接定位即可。

编译完成后，可以用 get_design_info 查看设计规模，用 get_instances 查看实例层次，确认顶层和子模块都被正确识别。这一步是后续属性绑定和证明的前提，如果设计模型不完整，后面的属性验证会直接失败或产生误导性结果。

常用命令分类

Jasper 命令数量很多，但日常高频使用的可以按功能归类。工程与设计类：clear、analyze、elaborate、check_design、get_design_info。属性类：create_property、get_property_list、assert、assume、cover。证明与调试类：prove、get_property_status、visualize、trace。脚本与流程类：source、set_property、get_property、puts、if/foreach 等 Tcl 控制结构。

其中 source 是把脚本文件加载进当前会话的关键命令，工程入口 jasper.tcl 通常就是一系列 source 和 set_property 的组合。把编译、属性加载、证明流程分别写成独立脚本，再用一个顶层脚本按顺序调用，是工程化管理的基本做法。

工程化实践建议

把上述内容落到实际项目中，建议遵循几条做法。第一，工程入口脚本 jasper.tcl 只做“编排”，不写具体实现，具体编译、属性加载、证明分别放在 scripts/ 下的独立脚本中，通过 source 调用。第二，属性文件与 RTL 模块一一对应，命名保持一致，例如 rtl/arbiter.v 对应 props/arbiter.sva，这样在属性失败时能快速定位到对应模块。第三，每次编译后先跑 check_design，确认设计模型干净，再加载属性，避免把设计问题误判为属性问题。第四，把常用命令封装成过程（proc），例如 proc load_and_compile {top} { ... }，减少重复输入，也便于团队统一流程。

掌握界面、目录、编译和命令这四块内容后，Jasper 工程就从“一次性的交互操作”变成了“可复现、可维护、可协作”的验证资产。后续的属性编写、证明调试和回归流程，都建立在这个工程骨架之上。