SVA断言一二
断言相关知识点，随笔记录：
1.$past构造
（1）SVA内嵌系统函数$past可以得到信号在几个时钟周期之前的值。在默认情况下，它提供信号在前一个时钟周期的值。
（2）结构的基础语法：$past(signal_name,number of clk cyc)。
2.$past构造实例
property p19检验的是在给定的时钟上升沿，如果表达式（c&&d）为真，那么两个周期前，在表达式（a&&b）为真。
property p19：
@（posedge clk）（c&&d） |-> (&past（a&&b），2) == 1'b1);
endproperty
a19: assert property(p19);
3.带时钟门控的$past()构造
（1）$past构造可以由一个门控信号控制，比如在给定的时钟沿，只有当门控时钟为真时，才检查后续算子的情况；
（2）使用门控信号的$past构造的基本语法：$past(signal_name,number of clk cyc,gating signal)
4.带门控时钟的$past（）构造实例
property 20与property 19类似，但是只有门控信号e在任意给定的 时钟上升沿有效时，检验才被激活；
property 20；
@（posdge clk）（c&&d） |-> ($past((a&&b),2 ,e) == 1'b1);
endproperty
a20：assert property（p20）；
### 三、断言验证的高级用法与示例
断言验证（Assertion-Based Verification, ABV）在芯片和软件验证中扮演关键角色，尤其在提升验证深度和覆盖率方面具有显著优势。通过使用SystemVerilog断言（SVA）和覆盖属性，可以实现对设计行为的动态监控和错误捕获。
在芯片验证中，断言不仅用于捕捉设计错误，还可用于提供结构覆盖率。例如，通过定义覆盖属性，可以确保设计中的所有可能状态转换路径都被覆盖。以下是一个基于SystemVerilog的断言示例，用于验证一个简单的状态机行为：
```systemverilog
property p_state_transition;
@(posedge clk) disable iff (reset)
(current_state == IDLE) |=> (next_state == RUN);
endproperty
assert property (p_state_transition) else $error("State transition from IDLE to RUN failed");
```
该断言检查状态机是否能够从`IDLE`状态正确过渡到`RUN`状态。如果在仿真过程中未能满足该条件，断言将触发错误信息，提示设计者检查相关逻辑。
在更复杂的场景中，可以使用嵌套断言来验证多个条件的组合。例如，验证一个仲裁器在多个主设备请求时是否按照预期的优先级进行响应：
```systemverilog
property p_arbitration_priority;
@(posedge clk) disable iff (reset)
(req_0 && !req_1) |=> grant_0;
endproperty
assert property (p_arbitration_priority) else $error("Priority arbitration failed for req_0");
```
此断言确保当只有`req_0`被激活时，仲裁器应授予`grant_0`。这种断言结构可以扩展到更多请求信号，并结合优先级配置寄存器进行动态验证。
在软件验证方面，断言可用于验证关键数据结构的完整性。例如，在一个内存管理模块中，可以使用断言来确保内存分配和释放的正确性：
```c
assert(memory_block_is_valid(ptr));
```
该断言在运行时检查指针`ptr`所指向的内存块是否有效，若无效则触发断言失败，提示开发者检查内存管理逻辑。
为了提升验证的自动化程度，可以在验证平台中集成断言覆盖率分析。通过在回归测试中收集断言覆盖率，可以评估测试用例对设计行为的覆盖情况，并识别未被覆盖的边界条件或异常场景。例如：
```systemverilog
cover property (p_state_transition);
```
该语句用于在仿真过程中收集`p_state_transition`断言的覆盖数据，帮助验证工程师评估测试用例的有效性。
此外，断言还可以与参考模型结合使用，实现混合验证策略。例如，在验证一个通信协议时，可以使用断言检查协议状态机的时序行为，并结合参考模型验证数据传输的正确性：
```systemverilog
property p_protocol_timing;
@(posedge clk) disable iff (reset)
(start_signal) |-> ##[1:5] data_ready;
endproperty
assert property (p_protocol_timing) else $error("Protocol timing violation detected");
```
该断言确保在`start_signal`被激活后，`data_ready`信号应在1到5个时钟周期内变为高电平。若未满足该条件，断言将触发错误，提示协议实现存在时序问题。
在实际应用中，断言的高级用法还包括参数化断言、断言覆盖率驱动的测试生成等。例如，参数化断言可以用于验证不同配置下的设计行为：
```systemverilog
property p_configurable_arbitration(int unsigned priority_level);
@(posedge clk) disable iff (reset)
(req[priority_level]) |=> grant[priority_level];
endproperty
assert property (p_configurable_arbitration(2)) else $error("Arbitration failed for priority level 2");
```
该断言允许在不同优先级配置下验证仲裁器的行为，提升验证的灵活性和可重用性。
在验证平台中，断言还可以与覆盖率驱动的测试生成结合使用，以提高验证效率。例如，通过在测试平台中注入随机激励，并监控断言覆盖率，可以动态生成新的测试用例以覆盖未被验证的场景。
---