SystemVerilog Assertions

LittlBee

1308人浏览 · 2025-07-16 09:56:40

LittlBee · 2025-07-16 09:56:40 发布

SystemVerilog Assertions（SVA），是一种基于SystemVerilog的断言语言，广泛用于硬件验证。它允许用户以声明式的方式描述硬件设计的预期行为。主要在一下场景中使用：

形式验证：通过数学方法验证设计的正确性。
仿真验证：在仿真中检查设计是否符合预期行为。
调试：帮助定位设计中的错误。
覆盖率分析：通过断言覆盖率评估验证的完整性。

一、SVA基本概念

SVA的核心是一个属性（property）和一个断言（assertion），它们通过特定的语法构造出设计的行为。同时还有一些其他高级的用法，例如，sequence，coverage等。

1.1 断言（Assertions）

作为SVA的核心功能，其主要用于对设计表现出的行为是否符合预期的检查。断言可以直接调用属性，并在仿真中检查属性。语法如下：

assert_name: assert property (property_name) [action_block];

assert_name：断言标签。
property：引用的属性。
action_block：断言成功或失败执行的操作，通常是打印信息。

1.2 属性（Properties）

属性是SVA中用来描述设计行为的逻辑表达式，可以包含时间序列、布尔表达式和操作符。属性可以单独定义，然后在断言中引用。语法如下：

property property_name;
    @(clock_edge) expression |-> consequent;
endproperty

clock_edge：指定时钟边沿，可以是posedge clk，也可个negedge clk；
expression：触发条件，描述行为发生的前提。
|->：推到运算符，表示如果条件成立后，后续的条件必须成立。
consequent：预期的结果，描述expression成立后应该发生的行为。

1.3 序列（Sequences）

序列是SVA中描述事件或信号随时间变化的模式。序列可以是简单的信号组合，也可以是复杂的多周期时间关系。语法如下：

sequence sequence_name;
    expression [##n expression];
endsequence

1.4 时钟（Clocking）

SVA中的并发断言通常与时钟信号相关联，用于定义时间步进和采样点。时钟控制断言的评估时机。

1.5 覆盖（Coverage）

SVA支持覆盖率分析，用于检查验证过程中是否所有预期的行为都被触发。语法如下：

cover property (@(posedge clk) req ##1 ack) 
               $display("cov hit: req followed by ack");

二、SVA的主要类型

SVA主要分为立即断言和并发断言。

2.1 立即断言（immediate assertion）

立即断言是在仿真执行到某一行代码时，立即检查条件是否成立。语法如下：

assert (expression) [action_block];

expression：需要进行检查的条件。
action_block：成功或失败执行的动作。可以使用也可以不使用，一般为打印信息。

立即断言适合检查瞬时条件，不适合复杂的时序关系。

2.2 并发断言（concurrent assertion）

并发断言是SVA的核心功能。它是基于时钟边沿检测时序逻辑的行为。它在仿真过程中持续检测监控信号的时序关系。并发断言的语法：

assert property (@(posedge clk) expression |-> consequent) 
                           else $error("Error message");

三、SVA时序运算符

SVA 提供了丰富的时序运算符，用于描述信号之间的复杂时序关系。以下是常用的时序运算符：

3.1 基本时序运算符

##n：延迟 n 个时钟周期。
示例：a |-> ##2 b 表示如果 a 为真，则 2 个时钟周期后 b 必须为真。
##[m:n]：延迟 m 到 n 个时钟周期。
示例：a |-> ##[1:3] b 表示 a 为真后，1 到 3 个周期内 b 必须为真。

3.2 重复运算符

[*n]：信号连续重复 n 次。
示例：req |-> req[*3] ##1 ack 表示 req 连续高 3 个周期后，ack 必须在下一个周期为高。
[*m:n]：信号重复 m 到 n 次。
示例：req |-> req[*2:4] ##1 ack 表示 req 连续高 2 到 4 次后，ack 必须为高。
[=n]：信号非连续重复 n 次。
示例：req |-> req[=2] ##1 ack 表示 req 在任意时间点出现 2 次后，ack 必须为高

3.3 逻辑运算符

and：两个条件同时成立。
示例：a && b 表示 a 和 b 都为真。
or：两个条件之一成立。
示例：a || b 表示 a 或 b 为真。
not：条件不成立。
示例：not a 表示 a 不为真。

3.4 推导运算符

|->：重叠推导，前件成立后，后件在同一周期或之后必须成立。
示例：req |-> ack 表示如果 req 为真，ack 必须在同一周期为真。
|=>>：非重叠推导，前件成立后，后件在下一个周期必须成立。
示例：req |=> ack 表示如果 req 为真，ack 必须在下一个周期为真。

四、注意事项

4.1 定义清晰

属性和断言的命名应该清晰且具有意义，能够明确其功能。如果对应property直接命名为pro1，根本无法知道描述的是什么功能。但是如果命名为check_req_ack，则可以清晰知道是在对req和ack进行检测。

4.2 避免复杂

断言定义太复杂，会增加调试难度，甚至无法进行调试。对于复杂场景，建议拆成若干个简单的断言进行检测。

4.3 时钟和复位

需要确保断言绑定在正确的时钟信号上。同时需要考虑复位时，需要进行的动作。也可以使用disable iff（reset）在复位时，禁用断言。

4.4 覆盖率分析

可以用断言分析覆盖场景。确保测试用例覆盖所有的关键场景。

五、一些示例

以下是基于apb接口的一些SVA示例。

    property setup_to_access;
        @(posedge clk) disable iff (!rst_n)
            $rose(apb_psel) && !apb_penable |=> apb_psel && apb_penable;
    endproperty
    assert property (setup_to_access) else
        `uvm_error("sva", "SETUP to ACCESS transition failed!");

    property access_signal_stable;
        @(posedge clk) disable iff (!rst_n)
            (apb_psel && apb_penable && !apb_pready) |=>
            $stable(apb_paddr) && $stable(apb_pwrite) && $stable(apb_pwdata);
    endproperty
    assert property (access_signal_stable) else
        `uvm_error("sva", "PADDR, PWRITE, or PWDATA changed during ACCESS phase!");

    property penable_only_with_psel;
        @(posedge clk) disable iff (!rst_n)
            apb_penable |-> apb_psel;
    endproperty
    assert property (penable_only_with_psel) else
        `uvm_error("sva", "PENABLE active without PSEL!");

    property transfer_completion;
        @(posedge clk) disable iff (!rst_n)
            (apb_psel && apb_penable && apb_pready) |=> !apb_penable;
    endproperty
    assert property (transfer_completion) else
        `uvm_error("sva", "PENABLE not deasserted after PREADY!");

    property write_data_valid;
        @(posedge clk) disable iff (!rst_n)
            (apb_psel && apb_penable && apb_pready && apb_pwrite) |-> !$isunknown(apb_pwdata);
    endproperty
    assert property (write_data_valid) else
        `uvm_error("sva", "PWDATA contains X/Z during write transfer!");

    property read_data_valid;
        @(posedge clk) disable iff (!rst_n)
            (apb_psel && apb_penable && apb_pready && !apb_pwrite) |-> !$isunknown(apb_prdata);
    endproperty
    assert property (read_data_valid) else
        `uvm_error("sva", "PRDATA contains X/Z during read transfer!");

    property idle_state;
        @(posedge clk) disable iff (!rst_n)
            !apb_psel |-> !apb_penable;
    endproperty
    assert property (idle_state) else
        `uvm_error("sva", "PENABLE is high during IDLE state!");

    property reset_behavior;
        @(posedge clk)
            !rst_n |-> !apb_psel && !apb_penable && !apb_pready;
    endproperty
    assert property (reset_behavior) else
        `uvm_error("sva", "PSEL, PENABLE, or PREADY not low during reset!");