SVA 断言概要

基于《SystemVerilog Assertions应用指南》内容，提炼核心，绘制思维导图，简化学习成本。

SVA1

• 书籍推荐
  • 《SystemVerilog Assertions应用指南》
    • 1.3小节：SV中的调度阶段划分，要能在波形上正确说出“从上一个周期得来的采样值”和“当前周期采样值”1.7小节：掌握边缘表达式，$rose() $fell() $stable()1.14小节：蕴含操作符的使用1.15小节：时序窗口，固定延迟、可变延迟1.21小节：重复运算符1.39小节：连接SVA和设计
• 分类
  • 并发断言
    • 基于时钟
      • 当前时钟采样的是上一时钟的稳定状态值
    • 过程块（procedural block）模块（module）接口（interface）程序（program）
    • 静态（形式）验证动态（模拟）验证
  • 即时断言
    • 不是时序相关，是立即被求值
    • 只能放在过程块（procedural block）
    • 只能动态仿真
  • 区别
    • 并发断言有关键词：property（属性）
• SVA 块
  • 序列(sequence)
    • sequence name_of_sequence; <test expression>; endsequence
  • 属性(property)
    • property name_of_property; <test expression>; or <complex sequence expressions>; endproperty
  • 断言(assert)
    • assertion_name： assert property (property_name);
    • 编写代码时，我们总是会做出一些假设，断言就是用于在代码中捕捉这些假设，可以将断言看作是异常处理的一种高级形式。断言表示为一些布尔表达式，程序员相信在程序中的某个特定点该表达式值为真。
  • 运行步骤
    • ①建立布尔表达式：boolean exp
    • ②建立序列表达式：sequence
    • ③建立属性：property
    • ④断言属性：assert
      • 序列和属性只有在被断言才能起作用
• 内建/嵌函数
  • 时序逻辑
    • 判断独立的一根信号的行为
      • 信号上升：$rose( a );
      • 信号下降：$fell( a );
      • 信号保持：$stable( a );
      • @ (posedge clk) A事件; 当clk上升沿时，如果发生A事件，断言将报警。
• 调度
  • 预备 Preponed
  • 观察 Observed
  • 响应 Reactive
• 功能覆盖率（不展开）
• 时钟定义
  • 在序列、属性，甚至一个断言的语句中都可以定义时钟注不可重复定义时钟
  • 序列中定义时钟
    • sequence s5; @(posedge clk) a ##2 b; endsequence property p5; s5; endproperty a5 ： assert property(p5);
  • 属性中定义时钟
    • sequence s5a; a ##2 b; endsequence property p5a; @(posedge clk) s5a; endproperty a5a ： assert property(p5a);
  • 断言语句中定义时钟
    • sequence s5b; a ##2 b; endsequence a5b ： assert property(@(posedge clk) s5b);
  • 通常在属性中定义时钟，保持序列独立于时钟这样可以提高序列的可重用性
• 序列相关
  • 用序列做表达式
    • 嵌套序列
      • sequence s3_lib (a，b); a || b; endsequence
        • 序列中定义形参
        • sequence s3_lib_inst1; s3_lib (req1，req2); endsequence
  • 序列中添加时序关系
    • 属性中也可以添加吗？
    • “##”表示时钟延时
      • sequence s4; @(posedge clk) a ##2 b; endsequence
        • a为高电平时，序列开始检测2时钟后b的状态为高，当前输出1
  • 序列开始的位置
    • 第一个表达式“##”前的部分成立的采样点
  • 序列成功的位置
    • 整个表达式都成立的采样点
  • 成功的序列总标注在序列开始的地方而不是序列成功的地方
• 序列的种类
  • 简单序列
    • 检测一个信号的状态
      • sequence s1; @(posedge clk) a; endsequence
  • 边沿定义的序列
    • 检测边沿跳变状态
      • sequence s2; @(posedge clk) $rose(a); endsequence
    • 内嵌函数
      • 信号保持：$stable( a );
      • 信号下降：$fell( a );
      • 信号上升：$rose( a );
      • @ (posedge clk) A事件; 当clk上升沿时，如果发生A事件，断言将报警。
  • 逻辑关系的序列
    • 检测信号之间逻辑关系后的状态
      • sequence s3; @(posedge clk) a || b; endsequence
• 显示
  • assertion_name : assert property(property_name) <success message> ; else <fail message>;

SVA2

• 蕴含（implication）
  • 可能的影响(或作用、结果)
  • 等效：if-then语句左边：“先行算子”(antecedent)右侧：“后续算子”(consequent)
    • 当先行算子成功时，后续算子才会被计算
  • 只能在属性中使用
    • 表达式和序列可以作为算子
  • 分类
    • 交叠蕴含
      • 解释
        • 表示在同一个时钟周期计算后续算子表达式
      • 符号：“|->”
        • property p8; @(posedge clk) a |-> b; endproperty a8 ： assert property(p8);
    • 非交叠蕴含
      • 解释
        • 如果先行算子匹配，那么在下一个时钟周期计算后续算子表达式
        • 后续算子表达式的计算总是有一个时钟周期的延迟
      • 符号：“|=>”
        • property p9; @(posedge clk) a |=> b; endproperty a9 ： assert property(p9);
    • 带延迟的蕴含
      • 固定延时
        • 例如“|-> ##2”
          • property p10; @(posedge clk) a |-> ##2 b; endproperty a10 ： assert property(p10);
      • 可变延时
        • 例如“|-> ##[1:3]”
          • 时序窗口表达式左手边的值必须小于右手边的值
          • property p12; @(posedge clk) (a && b) |-> ##[1:3] c; endproperty a12 ： assert property(p12);
            • (a && b) |-> ##1 c 或 (a && b) |-> ##2 c 或 (a && b) |-> ##3 c
              • 属性有三个机会成功。所有三个线程具有相同的起始点，但是一旦第一个成功的线程将使整个属性成功。
      • 无限时序窗口
        • 例如：“##[0：$] ”
          • 不太建议用
          • property p14; @(posedge clk) a |-> ##[1：$] b ##[0：$] c; endproperty a14 ： assert property(p14);
    • 序列作为先行算子的蕴含
      • sequence s11a; @(posedge clk) (a && b) ##1 c; endsequence sequence s11b; @(posedge clk) ##2 !d; endsequence property p11; s11a |-> s11b; endpeoperty
        • 开始时间是（a&&b）=1的时刻d的采样时间是在(a && b) ##1 c成功后的2个clk的时刻
  • 断言结果
    • 真成功：先行和后行算子都成功
    • 空成功：先行算子不成功