打开VC Formal GUI并加载设计后，执行形式验证的核心流程是：**设置约束 -> 加载属性 -> 启动证明引擎 -> 分析结果**。以下是详细步骤和操作示例。 ### 1. 关键操作界面与功能区 在VCF GUI中，主要使用以下窗口和标签页： | 界面区域 | 功能说明 | 关键用途 | | :--- | :--- | :--- | | **主工作区 (Main Workspace)** | 显示设计层次、源码、波形等。 | 查看设计结构，编辑约束和属性。 | | **约束管理器 (Constraint Manager)** | 管理时钟、复位、输入假设(assume)。 | **定义`create_clock`, `create_reset`，添加输入约束。** | | **断言浏览器 (Assertion Browser)** | 列出所有加载的SVA属性。 | 查看断言状态（未启动/运行中/通过/失败），启动证明。 | | **日志与报告窗口 (Log/Report)** | 显示工具运行输出和证明报告。 | 查看证明进度、反例生成信息和最终结果。 | | **波形查看器 (Waveform Viewer)** | 显示反例波形。 | 调试失败断言，分析违反场景。 | ### 2. 详细执行步骤（GUI操作） #### **步骤 1: 设置时序约束（时钟与复位）** 这是形式验证理解设计时序的基础[ref_1]。必须在证明前完成。 1. 在菜单栏选择 **“Constraints” -> “New Clock”**。 2. 在弹出的对话框中： * `Clock Name`: 输入时钟名称，如 `sys_clk`。 * `Period`: 输入时钟周期，如 `10` (单位通常为ns)。 * `Ports`: 点击浏览按钮，从设计端口列表中选择你的时钟端口（如 `clk`）。 3. 点击 **“Apply”**。同样方法，选择 **“Constraints” -> “New Reset”** 创建复位约束。对于低有效异步复位，设置 `Sense` 为 `Low`，`Type` 为 `Async`。 #### **步骤 2: 加载形式验证属性 (SVA)** 属性定义了要验证的具体行为。 1. 将你的SVA属性写入一个`.sva`或`.sv`文件。例如，创建一个 `clock_check.sva` 文件，内容如下： ```systemverilog // 检查复位释放后，时钟信号是否会发生跳变（即开始工作） property p_clk_activity_after_reset; @(posedge rst_n) // 当复位释放（假设上升沿释放）时 |-> s_eventually (clk != $past(clk)); // 最终，时钟值应与上一个周期不同 endproperty // 将属性绑定到设计实例 bind my_top_module assert property (p_clk_activity_after_reset); ``` 2. 在VCF GUI中，选择 **“File” -> “Read”**，然后选择你的 `.sva` 文件。加载后，属性会出现在 **“Assertion Browser”** 中。 #### **步骤 3: （可选）添加输入假设 (Assume)** 为了缩小搜索空间、避免不现实的场景，可以为设计的输入信号添加约束。 1. 在 **“Constraint Manager”** 中，找到需要约束的输入端口。 2. 右键点击该端口，选择 **“Add Assume”**。 3. 在弹出的表达式编辑器中，写入约束条件。例如，约束一个使能信号 `en` 在复位后一直为高：`assume property (@(posedge clk) (rst_n) |-> (en))`。 #### **步骤 4: 启动形式证明引擎** 1. 在 **“Assertion Browser”** 中，选中你想要验证的属性（如 `p_clk_activity_after_reset`）。 2. 右键点击选中的属性，选择 **“Prove”** 或点击工具栏上的 **“Prove”** 按钮。 3. 在弹出的证明设置对话框中，可以设置**超时时间**（例如300秒）和**证明深度**。对于简单的时钟检查，使用默认设置通常即可。 4. 点击 **“Start”**。工具将开始形式证明，**“Log”** 窗口会显示实时进度。 #### **步骤 5: 分析与调试结果** 证明完成后，状态会在 **“Assertion Browser”** 中更新。 | 结果状态 | 含义与后续操作 | | :--- | :--- | | **PROVEN (通过)** | 属性在所有可能的输入序列和状态下都成立。验证目标达成。 | | **FALSIFIED (失败)** | 工具找到了一个反例，证明属性可能不成立。**这是调试的关键**。 | | **UNPROVEN (未证明)** | 在给定的时间和资源内，工具无法确定属性是否成立[ref_1]。 | * **如果断言失败 (FALSIFIED)**： 1. 在 **“Assertion Browser”** 中，右键点击失败的断言，选择 **“Show Counterexample”**。 2. **波形查看器**会自动打开，显示导致断言失败的具体信号时序。重点关注复位(`rst_n`)、时钟(`clk`)以及相关控制信号在失败时刻附近的行为。 3. 通过分析波形，可以定位是设计错误、约束不足还是属性编写有误。 * **如果断言未证明 (UNPROVEN)**： 1. 尝试增加证明时间或证明深度。 2. 检查并添加更多合理的输入约束 (`assume`)，排除无关状态空间。 3. 使用 **“Sequential Depth”** 分析工具，查看状态空间的大小和瓶颈。 ### 3. 通过TCL控制台执行（GUI内高效方式） 在VCF GUI中，通常集成了TCL控制台。对于重复性任务或复杂流程，直接在控制台输入命令更高效。以下是等效于上述GUI操作的TCL命令序列： ```tcl # 在VCF GUI的TCL控制台中执行 # 1. 设置时钟和复位约束（与GUI操作等效） create_clock -name sys_clk -period 10 [get_ports clk] create_reset -name sys_rst -sense low -async [get_ports rst_n] # 2. 加载SVA属性文件 read_sva -binding {./clock_check.sva} # 3. （可选）运行一段初始化模拟，帮助工具找到有效起始状态 sim_run -all -time 100 # 4. 启动证明，指定超时时间 fv_prove -task prove -timeout 300 # 5. 生成报告 report_fv -status {FALSIFIED UNPROVEN} -output ./debug_report.rpt ``` ### 4. 验证“复位后时钟正常”的完整示例流程 假设你的设计顶层模块为 `chip_top`，时钟端口为 `i_clk`，异步低有效复位端口为 `i_rst_n`。 1. **准备SVA文件 (`clock_post_reset.sva`)**: ```systemverilog module clock_checker; property p_clk_ok_after_rst; // 当复位释放后，在有限时间内，时钟必须出现上升沿和下降沿（即完整周期） @(posedge i_rst_n) // 复位释放的边沿 |-> strong(##[1:100] ($rose(i_clk) && $fell(i_clk))); // 在1到100个周期内，必须看到一个上升沿和一个下降沿 endproperty a_clk_post_rst: assert property (p_clk_ok_after_rst) else $error("Clock failed to start after reset!"); endmodule bind chip_top clock_checker inst_clock_checker (); ``` 2. **在VCF GUI中操作**: * 加载设计后，在 **“Constraint Manager”** 为 `i_clk` 创建周期为10ns的时钟，为 `i_rst_n` 创建低有效异步复位。 * **“File” -> “Read”** 加载 `clock_post_reset.sva`。 * 在 **“Assertion Browser”** 中找到 `a_clk_post_rst`，右键选择 **“Prove”**。 * 证明完成后，若失败，则通过 **“Show Counterexample”** 查看波形，检查 `i_clk` 在 `i_rst_n` 变高后为何没有产生边沿。常见原因包括：时钟门控使能信号未有效、PLL锁定信号未拉高、或复位逻辑存在缺陷。 通过以上步骤，你可以在VC Formal GUI中完成从加载设计到执行并分析一个具体形式验证任务的全过程。关键在于**精确的约束定义**和**准确的属性描述**，这是获得有意义验证结果的前提[ref_1]。