关于断言的部分用法

时间:2025/7/11 9:53:56来源：https://blog.csdn.net/pgl512228/article/details/141990450 浏览次数:0次

1、带变量的断言

systemVerilog assertion 中variable delay的使用，##[variable]，带变量的延时(可变延时)_assertion中的延时-CSDN博客

2、until 的使用

systemVerilog assertion 中until的使用_verilog until-CSDN博客

3、throughout的使用

常用于断言和假设中的时间约束。它的主要作用是检查在一段时间内一个信号是否一直保持特定的状态。

assert property (@(posedge clk) (A throughout B ##[3] C));

这表示 A 必须在 B 持续有效的时间内为真，并且在 B 有效后的 3 个时钟周期内 C 也必须为真。

4、利用generate同时产生多个断言

module test_assertions (input logic clk,  // 时钟信号input logic rst_n,  // 复位信号，低电平有效input wire [10:0] A,  // 信号 A，11 位宽input wire [10:0] B   // 信号 B，11 位宽
);// 定义一个名为 'test_assert' 的属性，用于验证两个信号之间的关系property test_assert(signal_a, signal_b);@(posedge clk);  // 在时钟上升沿触发disable iff(rst_n === 1'b0)  // 当 rst_n 低电平时，禁用该属性$rose(signal_a) |-> ##4 signal_b;  // 如果 signal_a 上升沿触发，则 4 个时钟周期后 signal_b 应为高电平endproperty// 使用 generate 块生成断言测试genvar i;  // 定义生成变量 igenerate// 对 A 和 B 的每一位信号生成相应的断言for (i = 0; i <= 10; i++) begin: ASSERT_TEST// 对 A[i] 和 B[i] 应用 test_assert 属性test_assert_a: assert property(test_assert(A[i], B[i]));endendgenerateendmodule

模块接口信号：
- clk 是时钟信号，驱动断言的触发。
- rst_n 是复位信号，低电平时禁用断言。
- A 和 B 是 11 位宽的信号，表示要进行验证的信号集。
property 块：
- @(posedge clk)：确保断言在时钟上升沿时触发。
- disable iff(rst_n === 1'b0)：当 rst_n 低电平（复位有效）时，禁用断言。
- $rose(signal_a) |-> ##4 signal_b：当 signal_a 在时钟边沿上升时，4 个时钟周期之后 signal_b 应为高电平。
generate 块：
- 通过 genvar i 和 for 循环，分别对信号 A 和 B 的每个位进行断言验证。
- assert property(test_assert(A[i], B[i])) 对 A 和 B 的每个位执行断言检查。