systemverilog assertion

Posted hxing

tags:

篇首语:本文由小常识网(cha138.com)小编为大家整理,主要介绍了systemverilog assertion相关的知识,希望对你有一定的参考价值。

1.一般是单独写一个module 里面放assertion,  然后在验证平台顶层和RTL的实例化bind起来?

2. |->表示直接进行判断,|=>表示下一拍判断,一般一个断言最好只写一个蕴含。?

    $rose()表示该信号当前拍为1,上一拍为0,作用与 miso_oe && !past(miso_oe)一样。?

3.  (a [->1])  表示  a为高出现一次,(a [->2])  表示出现  a出现两次?

4.SVA应用指南:?

    a. $rose, $fell, $stable?

    b. 交叠蕴含:|->,非交叠蕴含:|=>,蕴含的先行算子没有发生时仿真不会报错,因此是空成功。??

    c.禁止属性:not

    d. 时间窗口,重叠的时序窗口在先行算子成功的同一个时钟沿开始计算?

    e. ended构造:基于序列的结束点来同步序列??

    f. $past构造:默认情况下它提供信号在前一个时钟周期的值??

        (c&&d) |-> ($past((a&&b),2)==1‘b1);  该属性检查c&&d为1时其前两个时钟周期a&&b为1。?

    g.重复运算符:?

连续重复运算符:   $rose(start) |-> ##2 (a[*3]) ##1 stop ##1 !stop;?

跟随重复运算符:   $rose(start) |-> ##2 (a[->3]) ##1 stop ##1 !stop;??

非连续重复运算符:   $rose(start) |-> ##2 (a[=3]) ##1 stop ##1 !stop;??

    h. and构造:用来逻辑地组合两个序列,当两个序列都成功时整个属性才成功?。也可以直接在property中使用。

    i. intersect构造:作用与and相同,不过要求两个序列的起始点和结束点都相同?

    j. or构造:只要一个序列成功,整个属性就成功????

  k. 蕴含只在时钟边沿检验前提条件一次,然后就开始检验后续算子部分,因此它不检测先行算子是否一直保持为真。为了保证某些条件在整个序列的验证过程中一直为真,可以使用“throughout”运算符。

    property p31;

            @(posedge clk)

            $fell(start) |->  (!start) throughout  (##1 (!a&&!b) ##1 (c[->3]) ##1 (a&&b));

    endproperty

在整个检查过程中start一直为低

    l.SVA 提供了几个内建的函数来检查一些最常用的设计条件:

        $onehot(检验在任意给定的时钟沿,表达式只有一位为高。

        $onehot0 检验在任意给定的时钟沿,表达式只有一位为高或者

没有任何位为高。

        $isunknown检验验表达式的任何位是否是 X或者 Z。

        $countones计算向量中为高的位的数量。

a33a :  assert  property(@(posedge clk) $onehot(state));

a33b :  assert  property(@(posedge clk) $onehot0(state));

a33c :  assert property(@(posedge clk) $isunknown(bus));

a33d :  assert  property(@(posedge clk) $countones(bus)> 1);

    m. 使用“intersect”控制序列的长度 :

这个intersect 的定义检查从序列的有效开始点(信号“a”为高),到序列成功的结束点(信号“c”为高),一共经过 2~5 个时钟周期。

        property p35;

                (@(posedge clk)

                1[*2:5]  intersect  (a ##[1:$] b ##[1:$] c));

        endproperty

    n.使用局部变量的SVA:  ($rose(enable), Ivar = a) |->  如果enable从0到1翻转了那么就执行赋值,否则不执行。

其他:嵌套的蕴含、disable iff构造。?

 

培训的笔记:

1.sv出现之前就有assertion,最早是软件上使用 

2.硬件的assertion比软件上更复杂 

3.他和sv其实挺独立的,所以sv的书不讲SVA 

4.systemverilog 应用指南,总共5章,细节可以参考此书。 

5.在tb中,激励和检查应该独立,所以assertion是做检查的工具。 

6.实际仿真中如果过多的使用$,会拖慢仿真速度。 

7.sequence和property可以做成参数化的,然后调用之。 

8.一个信号在特定时间内应该出现多少次:[*为严格的次数限制,[-> 

9.multi clock很少用 

10.cover的意思是assertion在其他地方已经做过检查,现在只需要cover一次。 

11.直接的assert()就是软件里面的用法,immediate assert,这一行执行完立刻消失。 

12. sequence更多的是像子模块,让代码模块化。 

13.assertion90%都是用于同步单时钟设计。理解这一点非常重要 

14.within运算符指前面的表达式所发生的时间必须是后面表达式的子集。 

15.即使某design有多个时钟,但是做assertion还是尽量用单个时钟,因为仿真器可能会对多时钟的延时判断有误,而且很难debug。 

16.assert用于检查该property有没有被违反。cover用于检查蕴含前面的触发条件有没有被满足过。 

17.initial和module等多数地方都可以放assertion。 

18.assertion module的端口最好与design的一样,这样在bind时直接用(.*)就可以。

以上是关于systemverilog assertion的主要内容,如果未能解决你的问题,请参考以下文章

请教systemverilog中的interface问题

SystemVerilog 编写FSM

systemverilog 断言中assume 和assert的区别

systemverilog 为啥要用$cast类型转换函数

参数化模块 (SystemVerilog)

vcs怎么编译产生随机激励的systemverilog语句