【无标题】Open Verification Library Assertion检查

1 Assertion概述

断言概述
1.概念：通过在代码中插入对RTL的特征描述，检查RTL代码的关键行为是否和期望的一致（一般检查设计中的控制信号的完整性和数据的完整性），当异常出现时，断言语句会报警。通过这种方法可以快速的定位问题，为测试平台提供自检机制，提高验证效率。
2.目的：
• 为测试平台提供优秀的自检机制；
• 提高验证效率，减少调试时间；
• 提高测试的可控性和可观察性；
3.功能：
• 检查设计中控制信号的正确性；
• 检查设计中数据的完整性；

2 OVL概述

• 概念：Open Verification Library硬件验证库。在源代码设计的同时加入的更为细化的验证方案采用的库，通过在代码中插入ovl语句，可以在仿真验证中快速的定位出问题所在。
• 应用：Verilog HDL,VHDL,SystemC,System Verilog。
2.1 两个常用的OVL检测器
一个是assert_implication，一个是assert_never。

assert_implication

assert_implication [#(severity_level, property_type,
msg, category, coverage_level_1,
coverage_level_2, coverage_level_3)]
inst_name (
    clk, 
    reset_n, 
    antecedent_expr, 
    consequent_expr);
1
2
3
4
5
6
7
8

这个检查器会连续监测 antecedent_expr。
如果值为真，检查器将验证consequent_expr（下一个表达式） 是否为真，如果为真，那么不会报错。
当 antecedent_expr 为假的时候， consequent_expr 表达式将不会被检查，并且断言表明通过。
（severity_level表示严重级别，property_type表示属性类型,msg表示message，category表示种类）

assert_never

assert_never [#(severity_level, property_type, msg,
category)]
inst_name (
    clk, 
    reset_n,
    test_expr);
1
2
3
4
5
6

这个检查器会在每个时钟 clk 的上升沿连续的监测 test_expr。 它的检查目的 是： test_expr 的值永远不能为真。 test_expr 可以是任意有效的 verilog 表达式。 当 test_expr 为真的时候，检查器将会报错。

3 OVL使用案例

在cmsdk_apb4_eg_slave.v中使用断言

`ifdef ARM_APB_ASSERT_ON
 `include "std_ovl_defines.h"
  // ------------------------------------------------------------
  // Assertions
  // ------------------------------------------------------------
   // Check the reg_write_en signal generated
    assert_implication
    #(`OVL_ERROR,
      `OVL_ASSERT,
      "Error! register write signal was not generated! "
      )
     u_ovl_apb4_eg_slave_reg_write
     (.clk             (PCLK),
      .reset_n         (PRESETn),
      .antecedent_expr ( (PSEL & (~PENABLE) & PWRITE) ),
      .consequent_expr ( reg_write_en == 1'b1)
      );
  // Check the reg_read_en signal generated
    assert_implication
    #(`OVL_ERROR,
      `OVL_ASSERT,
      "Error! register read signal was not generated! "
      )
     u_ovl_apb4_eg_slave_reg_read
     (.clk             (PCLK),
      .reset_n         (PRESETn),
      .antecedent_expr ( (PSEL & (~PENABLE) & (~PWRITE)) ),
      .consequent_expr ( reg_read_en == 1'b1)
      );
  // Check register read and write operation won't assert at the same cycle
    assert_never
     #(`OVL_ERROR,
       `OVL_ASSERT,
       "Error! register read and write active at the same cycle!")
     u_ovl_apb4_eg_slave_rd_wr_illegal
     (.clk         (PCLK),
      .reset_n     (PRESETn),
      .test_expr   ((reg_write_en & reg_read_en))
      );
`endif
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40