system verilog的断言assertion_system verilog assertion

1.什么是断言？

 断言通常被称为序列监视器或者序列检验器；是对设计应当如何执行特定行为的描述，是一种嵌入设计检查。如果检查的属性（property）不是我们期望的表现，那么在我们期望事件序列的故障上会产生警告或者错误提示。

断言用来检查模拟序列行为或者激励生成的正确性，断言作为功能验证的一种重要手段，可以脱离测试用例而覆盖测试点，所以断言覆盖率可以是功能覆盖率的一部分，完善的断言能为全面的功能覆盖率尺度打下良好的基础。

2.可以添加什么类型的断言？

设计层面：设计意图相关的断言；

接口层面：模块接口相关断言、芯片功能意图相关断言、芯片接口相关断言；

性能层面：读取的缓存延迟、数据包处理延迟。如果超过设计时限则请求断言。

3.断言的目的是？

 

 3.断言添加的位置

断言可以嵌入到RTL中：和普通设计语句一样，分布在rtl中，在综合时会被忽略；

在设计模型中，但是独立成块：仿真时和设计一起执行综合要忽略；

在设计模型外部独立的模块文件。

4.断言的两种类型

4.1即时断言（immediate assertions）:在当时时刻断定信号的数值情况；

语法

label: asser (expression) actin_block;

必须放到过程块中（task/function/always）

例如

asser_foo:assert (foo)$display("%m pass");
            else $display("%m failed"); //名字：assert(判断语句)若真执行语句1，否则执行语句2

4.2并发断言（concyrrent assertions）：在多个周期断定序列顺序。

并发断言是检查跨越多个时钟周期的事件序列。

仅在有时钟周期的情况下出现，

测试表达式是基于所涉及的采样值在时钟边缘计算的；

可以放在过程块、模块、接口或程序定义中

区别并发断言和即时断言的关键字是property

例子

always @ (posedge clk)
        if (state == fetch)
        ap_req_grant:assert property (p_req_gnt) passed_count++;
        property p_req_gnt;
            @(posedge clk) request ##3 grant ##1 !request ##1 !grant;
         endproperty:p_req_gnt

主要区别是与clk有无关系。

5.断言的结构

断言assertion（属性property（序列sequence））

6.断言基本语法

  6.1信号间的组合逻辑关系

   （1）常见的有&&，||，！，^

        (2)a?b:c    a事件成功后，触发b，a不成功出发c。

  6.2 再时序逻辑中判断独立的一根信号的行为：

                $rose(a)   ---  信号上升；

                $fell()    --   信号下降

                $stable(a)   --信号值不变

   6.3 再时序逻辑中判断多个事件/信号的行为关系

                intersect(a,b)     --        a和b两个事件同时产生，同时约束

                a within b         --        b事件发生的时间段内包含a事件发生的时间段

                a ## 2b        --        a事件发生的两个时间单位内b事件会发生

                a##[1:3] b        --        a事件发生过后1-3个时间单位内b会发生

                a##[1:$] b         --        a事件发生后的3个周期后B会发生

                c throughout (a##2 b)         --        在a成立到b成立的过程中，c一直成立

                

                @（posedge clk） a |-> b        --        clk上升沿，a事件发生，同时b发生。

                @（posedge clk） a.end|->b        --        clk上升沿，a发生结束后，b发生

                @（posedge clk） a |=>b        --        clk上升沿，a发生后，b在下一个clk发生

                @（posedge clk） a|=> ##2        --        clk上升沿，a发生后，b在下三个时钟沿发生

                @（posedge clk）a [*3]         --        a在连续的3个时钟沿都成立

                @（posedge clk）a [*1:3]         --        a在连续的1~3个时钟沿都成立

                @（posedge clk）a [->*3]         --        a在非连续的3个时钟沿都成立

         6.4 多时钟域的联合断言：能表示多个时钟域的之间的信号关系

                多时钟序列由单时钟序列通过延迟符号 ##1 连接而成。表示从第一个时钟序列的结束点，到第二个单时钟序列的起始点。

        6.5        总线的断言函数

                $onehot(expression):  在给定的时钟沿，表达式只有一位为高

                $onehot0(expression):  在给定的时钟沿，表达式只有一位为低，或没有高位

例子

property p5
    @(posedge clk) $ rose (start)|->##2 (a[*3])##2 stop ##1 !stop;
    endpriperty
 
 
其中a[*3]可以展开成：a##1 a ##1 a;