FPGA仿真中SystemVerilog断言（SVA）实战应用指南：以4位计数器为例

1天前

Quick Start 快速上手

准备环境：安装 Vivado 2024.2 或更新版本（完整支持 SystemVerilog 断言），并确保仿真器（如 Vivado Simulator 或 Questa）已正确配置。
创建工程：新建一个 Vivado 工程，添加一个 RTL 源文件（如 counter.sv）和一个测试平台文件（如 tb_counter.sv）。
编写 RTL：实现一个 4 位计数器，带异步复位和使能信号。
添加断言：在测试平台中编写一个 SVA 断言，检查计数器在使能有效时每个时钟周期递增 1。
运行仿真：在 Vivado 中启动仿真，观察断言是否通过。
验证结果：查看仿真日志，确认断言无失败（Failure）报告；若有失败，根据错误信息定位并修复 RTL。

前置条件与环境

项目	推荐值	说明	替代方案
器件/板卡	Xilinx Artix-7 XC7A35T	用于综合与上板验证，仿真无需板卡	任何支持 SVA 的 FPGA 器件
EDA 版本	Vivado 2024.2	完整支持 SystemVerilog 断言（SVA）	Vivado 2023.x 或 Questa 2024.x
仿真器	Vivado Simulator (xsim)	内置于 Vivado，支持 SVA 仿真	Questa、VCS、ModelSim
时钟/复位	时钟 100 MHz，异步复位低有效	标准同步设计基础	根据目标板调整频率
接口依赖	无特殊硬件接口	仅需仿真环境	—
约束文件	无（仿真阶段不需要 XDC）	上板时才需要物理约束	—

目标与验收标准

功能点：在仿真中，SVA 断言能正确检测到 RTL 行为是否违反预期协议（如计数器递增、握手信号时序）。
性能指标：断言不应影响仿真速度（通常影响可忽略，但需避免过度复杂的断言逻辑）。
验收标准：仿真日志中所有断言均通过（Pass），无任何 Failure 报告；若故意注入错误，断言应准确触发失败。

实施步骤

步骤 1：创建 Vivado 工程并添加源文件

打开 Vivado 2024.2，点击“Create Project”，选择工程路径与名称（例如 sva_counter_demo）。
在“Add Sources”阶段，选择“Add or create design sources”，然后点击“Create File”，新建文件 counter.sv（类型选 SystemVerilog）。
同样方式，在“Add or create simulation sources”中新建测试平台文件 tb_counter.sv（类型选 SystemVerilog）。
完成工程创建向导，进入 Vivado 主界面。

步骤 2：编写 RTL 代码（counter.sv）

// counter.sv - 4位计数器，带异步复位和使能
module counter (
    input  logic       clk,
    input  logic       rst_n,   // 异步复位，低有效
    input  logic       en,      // 使能信号
    output logic [3:0] count
);

    always_ff @(posedge clk or negedge rst_n) begin
        if (!rst_n)
            count &lt;= 4'b0;
        else if (en)
            count &lt;= count + 1'b1;
        // 当 en=0 时，count 保持
    end

endmodule

逐行说明

第 1 行：注释，指明文件功能——4 位计数器，带异步复位和使能。
第 2 行：模块声明，名称为 counter。
第 3 行：输入端口 clk，类型为 logic。
第 4 行：输入端口 rst_n，异步复位，低电平有效。
第 5 行：输入端口 en，使能信号。
第 6 行：输出端口 count，4 位宽，类型 logic。
第 8 行：always_ff 块，敏感列表为时钟上升沿或复位下降沿（异步复位）。
第 9 行：复位条件判断——若 rst_n 为低，则执行复位。
第 10 行：复位操作：count 赋值为 4 位二进制 0。
第 11 行：非复位时，判断使能 en 是否为高。
第 12 行：使能有效时，count 自增 1。
第 13 行：注释说明当 en=0 时，count 保持当前值。
第 15 行：模块结束。

步骤 3：编写测试平台并添加 SVA 断言（tb_counter.sv）

// tb_counter.sv - 测试平台，含 SVA 断言
`timescale 1ns / 1ps

module tb_counter;

    // 信号声明
    logic        clk;
    logic        rst_n;
    logic        en;
    logic [3:0]  count;
    logic [3:0]  expected_count;

    // 实例化 DUT
    counter u_dut (
        .clk  (clk),
        .rst_n(rst_n),
        .en   (en),
        .count(count)
    );

    // 时钟生成：周期 10ns（100 MHz）
    initial begin
        clk = 0;
        forever #5 clk = ~clk;
    end

    // 测试序列
    initial begin
        // 初始化
        rst_n = 0;
        en    = 0;
        #20;
        rst_n = 1;
        #10;
        en = 1;
        // 运行 20 个时钟周期
        #200;
        en = 0;
        #50;
        $finish;
    end

    // SVA 断言：使能有效时，每个时钟周期 count 递增 1
    // 使用 expected_count 辅助验证
    always_ff @(posedge clk or negedge rst_n) begin
        if (!rst_n)
            expected_count &lt;= 0;
        else if (en)
            expected_count &lt;= expected_count + 1'b1;
    end

    // 断言：count 必须等于 expected_count
    assert_count_equal: assert property (
        @(posedge clk) disable iff (!rst_n)
        (en) |-&gt; (count == expected_count)
    ) else $error("断言失败：count=%0d, expected=%0d at time %0t", count, expected_count, $time);

endmodule

逐行说明

第 1 行：注释，指明文件为测试平台，包含 SVA 断言。
第 2 行：时间尺度定义：timescale 1ns / 1ps，仿真精度 1ps。
第 4 行：测试平台模块声明，名称为 tb_counter。
第 7 行：声明 clk 信号，类型 logic。
第 8 行：声明 rst_n 信号。
第 9 行：声明 en 信号。
第 10 行：声明 count 信号，4 位宽，连接 DUT 输出。
第 11 行：声明 expected_count 信号，用于辅助断言验证。
第 13 行：实例化 DUT（counter 模块），命名为 u_dut。
第 14 行：连接 clk 端口。
第 15 行：连接 rst_n 端口。
第 16 行：连接 en 端口。
第 17 行：连接 count 端口。
第 18 行：实例化结束。
第 20 行：时钟生成块开始。
第 21 行：初始化 clk 为 0。
第 22 行：每 5ns 翻转时钟，周期 10ns（100 MHz）。
第 24 行：测试序列块开始。
第 26 行：复位信号置低（有效）。
第 27 行：使能信号置低。
第 28 行：等待 20ns。
第 29 行：释放复位（rst_n 置高）。
第 30 行：等待 10ns。
第 31 行：使能信号置高。
第 32 行：等待 200ns（20 个时钟周期）。
第 33 行：使能信号置低。
第 34 行：等待 50ns。
第 35 行：结束仿真。
第 37 行：注释，说明 SVA 断言的作用。
第 39 行：always_ff 块，用于生成 expected_count，模拟理想计数器行为。
第 40 行：复位条件判断。
第 41 行：复位时 expected_count 清零。
第 42 行：使能有效时，expected_count 自增 1。
第 45 行：断言声明，标签为 assert_count_equal。
第 46 行：assert property 关键字，定义属性。
第 47 行：时钟事件为 posedge clk，disable iff (!rst_n) 表示复位时禁用断言。
第 48 行：断言逻辑：当 en 为高时，count 必须等于 expected_count。
第 49 行：断言失败时的错误报告，打印实际值和期望值及仿真时间。
第 51 行：模块结束。

步骤 4：运行仿真并查看断言结果

在 Vivado 左侧 Flow Navigator 中，选择“SIMULATION” → “Run Simulation” → “Run Behavioral Simulation”。
仿真启动后，Vivado 会自动打开波形窗口。在 Tcl Console 或仿真日志中，查看断言报告。
若断言通过，日志中会显示类似“Info: assert_count_equal: passed”的信息；若失败，则显示“Error: 断言失败：count=..., expected=...”。
可故意修改 RTL（例如将 count <= count + 1'b1 改为 count <= count + 2）重新仿真，验证断言能正确捕获错误。

验证结果

按照上述步骤运行仿真后，预期输出如下（以 Vivado Simulator 日志为例）：

run -all
# Info: assert_count_equal: passed at time 50000 ps
# Info: assert_count_equal: passed at time 60000 ps
# ... (每个时钟周期均通过)
# $finish called at time 300000 ps

若故意注入错误（如修改 RTL 递增步长为 2），断言会报告失败：

# Error: 断言失败：count=2, expected=1 at time 60000 ps
# Error: 断言失败：count=4, expected=2 at time 70000 ps

排障指南

断言未触发：检查测试平台中是否在适当时间点使能了 en 信号；确认 disable iff 条件是否正确（如复位信号极性）。
断言始终失败：对比 count 与 expected_count 的波形，确认 RTL 逻辑是否与预期一致；检查时钟域是否对齐。
仿真速度变慢：避免在断言中使用过于复杂的序列（如 ##[1:$] 无限延迟）；减少不必要的 $error 打印。
断言语法错误：确认 Vivado 版本支持 SystemVerilog 断言（2024.2 及以上）；检查文件扩展名是否为 .sv。

扩展应用

多断言协同：可添加更多断言，例如检查计数器溢出行为（count == 4'hF 时下一周期回绕到 0）。
形式化验证集成：将 SVA 断言用于形式化验证工具（如 JasperGold），实现静态时序属性检查。
覆盖率驱动：结合 SVA 的 cover property 语句，收集断言覆盖点，评估验证完备性。
复杂协议验证：将本示例中的基本断言扩展至 AXI、APB 等总线协议，检查握手信号（VALID/READY）的时序关系。

参考资源

IEEE Std 1800-2017: SystemVerilog Language Reference Manual, Chapter 16 (Assertions).
Xilinx UG900: Vivado Design Suite User Guide - Logic Simulation.
Mentor Graphics (Siemens) Questa User Manual: Assertion-Based Verification.

附录：完整代码清单

counter.sv

// counter.sv - 4位计数器，带异步复位和使能
module counter (
    input  logic       clk,
    input  logic       rst_n,
    input  logic       en,
    output logic [3:0] count
);

    always_ff @(posedge clk or negedge rst_n) begin
        if (!rst_n)
            count &lt;= 4'b0;
        else if (en)
            count &lt;= count + 1'b1;
    end

endmodule

tb_counter.sv

// tb_counter.sv - 测试平台，含 SVA 断言
`timescale 1ns / 1ps

module tb_counter;

    logic        clk;
    logic        rst_n;
    logic        en;
    logic [3:0]  count;
    logic [3:0]  expected_count;

    counter u_dut (
        .clk  (clk),
        .rst_n(rst_n),
        .en   (en),
        .count(count)
    );

    initial begin
        clk = 0;
        forever #5 clk = ~clk;
    end

    initial begin
        rst_n = 0;
        en    = 0;
        #20;
        rst_n = 1;
        #10;
        en = 1;
        #200;
        en = 0;
        #50;
        $finish;
    end

    always_ff @(posedge clk or negedge rst_n) begin
        if (!rst_n)
            expected_count &lt;= 0;
        else if (en)
            expected_count &lt;= expected_count + 1'b1;
    end

    assert_count_equal: assert property (
        @(posedge clk) disable iff (!rst_n)
        (en) |-&gt; (count == expected_count)
    ) else $error("断言失败：count=%0d, expected=%0d at time %0t", count, expected_count, $time);

endmodule