验证与设计不同，尤其是初学者，验证会成为一盘散沙——无规可循。然而 为了能够实现验证平台的重用，需要标准的验证语言和标准的验证库。这样一来 在验证的过程中只需要调用验证库中的库单元就可以实现验证的重用。所以为了 解决验证的混乱局面，特此依据 Synopsys 的 SVL 库进行翻译，该库与 OVL 的 使用方式相同，每次的检查对象仅需要例化对应的库单元就可以实现。 其原文来自于 Synopsys 的 SystemVerilog 检查库的讲解文档，翻译难免有错 和生硬的地方，所以请参照相应文件进行阅读。 最后将 Serikanth Vijayaraghavan 和 Meyyappan Ramanathan 编著的《A Practical Guide for SystemVerilog Assertions》的第一章翻译放置在附录 A 中，以 供阅者参考。 SystemVerilog 断言(SVA)是数字电路验证中一种强大的工具，它允许设计者在硬件级别定义期望的行为，从而确保系统按照预期运行。Synopsys的SVA检查库是这个领域的一个重要资源，提供了丰富的预定义检查器，用于简化和标准化验证过程。 1. **SVA检查器库概述** SystemVerilog断言库提供了大量的预定义检查器，这些检查器覆盖了常见的错误检测场景，如数据路径错误、时序问题和协议违规等。它们是基于SystemVerilog的属性和行为语句构建的，可以方便地在验证环境中插入和配置。 2. **全局控制（Global Controls）** 全局控制是影响所有断言的设置，例如，`assertproperty`的超时限制或者全局的严重级别。这些控制可以设置在验证环境的高层次，使得整个验证平台能共享统一的策略。 3. **检查器触发条件** 每个检查器都有一个特定的触发条件，比如时钟边沿、数据变化或者其他事件。这些条件由用户指定，当满足条件时，检查器将被激活并评估断言是否为真。 4. **带有VMM报告性质的检查器** VMM（Virtual Memory Model）是一种流行的验证方法学，它引入了详细的报告机制。当检查器与VMM结合使用时，可以提供更丰富的错误信息，包括错误的位置、时间和其他相关上下文。 5. **定制报告** 用户可以根据需求定制检查失败时的报告信息，包括错误消息、严重级别和类别，以提高调试效率。 6. **共享语法** - **severity_level**：定义断言失败时的严重程度，如error、warning或info。 - **options**：可以用来控制断言的行为，例如禁用或启用某些特性。 - **property_type**：指定断言的类型，例如序列、静态或定时。 - **msg**：自定义的错误消息，显示在检查失败时。 - **category**：分类断言，有助于组织和筛选错误报告。 - **coverage_level_i**：用于覆盖率收集，评估断言的覆盖情况。 - **inst_name**：断言实例的名称，有助于追踪和调试。 - **clk**：关联的时钟信号，用于时序相关的断言。 - **reset_n**：复位信号，通常与断言的初始化和重置行为相关联。 7. **使用示例** 在实际应用中，用户可以通过实例化检查器模块，并设置其参数来使用这些检查器。例如，可以创建一个`always @(posedge clk)`来触发一个数据路径完整性检查，当数据异常时，检查器将报告错误并可能触发覆盖率收集。 Synopsys SVA检查库为设计者提供了强大且灵活的验证手段，通过标准化的库单元和丰富的控制选项，能够有效地管理和组织复杂的验证流程。学习和理解这些检查器的使用，对于提升验证质量和效率至关重要。参考《A Practical Guide for SystemVerilog Assertions》等相关资料，可以进一步深入理解和应用SystemVerilog断言。

包含SystemVerilog的图书SystemVerilog for Verification（第3版）以及最新版IEEE标准；SystemVerilog Assertions的图书A Practical Guide for SystemVerilog Assertions；UVM1.2源码、官方手册、最新版IEEE标准以及图书A practical guide to adopting the universal verfication methodology(UVM)。

一份非常好的 SVA 资料，详细介绍怎样写出好的 assertion。资料的最后部分以 sync_fifo 为例子，详细介绍了 assertion 的写法

 论文分析了步进频率探地雷达距离旁瓣的产生机理及其影响，对传统的线性加权法抑制距离旁瓣效果进行了对比分析，包括时域加权和频域加权，理论和实验结果表明：线性加权法在抑制距离旁瓣的同时容易造成分辨率下降。因此，本文提出基于SVA的步进频率探地雷达距离旁瓣抑制方法，它是一种非线性加权方法，能对时域波形主瓣和旁瓣自适应地选择加权函数，达到保留主瓣抑制旁瓣的目的。仿真结果表明，该方法可以有效地抑制步进频率探地雷达距离旁瓣，旁瓣抑制比提高20 dB，并且具有频谱外推的效果，主瓣展宽仅为5%，相同条件下，采用Hamming窗线性加权则主瓣展宽为50%。

Eduard Cerny, Surrendra Dudani, John Havlicek, Dmitry Korchemny (auth.) - SVA_ The Power of Assertions in SystemVerilog-Springer International Publishing (2015)

SYSTEMVERILOG ASSERTIONS FOR FORMAL VERIFICATION

System-Verilog-Assertions(SVA)-简介,断言，形式验证

Ashok B. Mehta (auth.) - SystemVerilog Assertions and Functional Coverage_ Guide to Language, Methodology and Applications-Springer International Publishing 非常好的学习验证的中文资料，尤其是assertion 。极力推荐。

旁瓣抑制中的SVA和超分辨率SUPER-SVA算法的matlab代码.该算法在雷达成像领域应用较为广泛，可以在不损失主瓣性能的条件下，抑制旁瓣幅度。

这本书是为设计和验证工程师准备的。花了一个完整的部分来说明其原因和实用性拥有由设计工程师和宏级编写的微观级别的断言由验证工程师编写的断言。设计师只编写RTL并把它扔给验证工程师检查的日子一去不复返了。