SV-assertion

断言(assert)是一种描述性语言,通过描述的期望结果来进行仿真验证。

断言有一个更加基础的信息,我们称为属性(property),属性可以作为断言结果,功能覆盖点,形式检查和约束随机激励生成

断言相比较与testcase的仿真验证,对设计的可见度要求比较高,可以帮助快速定位错误的根源,断言可以分布在设计各个部位。

在项目中使用断言,有两种方式(eda tool中都支持):

  1) 使用预建的断言库,如OVL,

  2) 使用SVA,PSL等断言语言来自己描述。(PSL是完全独立的断言语言,SVA被继承在SV语言中),

SVA的语言层次结构:

  SV-assertion

assertion分为:

  1) immediate assert,基于simulation event semantics;

      assert/assume/cover (expression)  action_block;

  2) concurrent assert,基于clock semantics;

      assert/assume/cover (expression)  action_block;

  action_block的声明:

      statement | [statement] else statement

  immediate assert的action block紧跟着assert执行,就像在procedual block中,(比如active或者NBA region)

    可以放在任何procedual中,initial,always,task,function。

  concurrent assert的action block,在当前assert的reactive region执行,所以action block中使用$sampled()采样信号值,表示evaluate时的信号值

assertion中的property,可以用来描述design的某一个行为,必须被例化在assert,assume,cover等编译选项后

        包含在module,interface,package,program,clocking,$unit中。

      sequence,用来描述high level property的abort condition或者common start point,一系列的boolean expression。

在sva中,一个property代表一个thread,表示一系列event的sequence,可能持续多个cycle。

  在property没有start的时候,thread不会起来,之后的check是不会被evaluation的。被认为是true的。

  当该property执行结束或者结果已经出错,property在这个时间点结束

SV引入了 |->表示overlapping的操作,resulting sequence (consequent) 与causing sequence (antecedent) 在同一个cycle完成。

      |=>表示non-overlapping的操作,resulting sequence在causing sequence的下一个cycle开始。

sequence:随着时间增加的SV boolean expression

SV-assertion

  可以声明有formal args,local var;

  method方法有:ended,matched,triggered,这三个方法都表示sequence的结束;

  尽量使用named sequence,来增加代码的可读性。

  sequence支持的操作符:

    SV-assertion

注意:1) sequence中的formal args是untyped的;formal args可以是一个signal,sequence,sequence method

   2) sequence中的local var是不能用作setup delay或者repetition ranges的

property:可以包含formal args,可以有local var;

    SV-assertion

    property支持的操作符:

      SV-assertion

注意:1) 一个property_spec不是一个sequence,但是一个sequence可以是一个property_spec

   2) formal args可以带default value。

SVA中支持的assertion 语句以及function:

  SV-assertion

  SV-assertion

  SV-assertion

SVA中各个运算符之间的操作,可以是expression,sequence,property。

  expression的优先级与logic operate部分相同。

  sequence之间的优先级:

    SV-assertion

  property之间的优先级:

    SV-assertion

verilog中的#表示延时,delay,##号表示延时若干个clock cycles。

如果implication operator中,antecedent fail,property被hold为vacuous success。

property中的not operator不可以和implication operator一同使用,一般只用在sequence组成的property,表示从不true的序列。

sequence中的first_match操作符,用来消除可能发生overlap的assert result:

  1.如果property中只由一个sequence组成,则包含一个implicit first_match。

    property p_seq;   (a##1 b ##[0:5] c); endproperty

  2.consequent sequence中默认包含一个implicit first_match

    property p_seq;  a=>b##[1:2] c ## [0:4] d; endproperty

    property p_seq;  a=>## [0:3] qABC.ended; endproperty

  first_match主要用在antecedent的sequence中,一个sequence的ended是可以多触发的

    property p_seq; first_match(a##[2:3]b) |-> c;  endproperty

    property p_seq; first_match(qABC.ended) |-> c; endproperty

重复操作符,可以用于sequence和expression中。

  consecutive repetitive,  seq[*n], exp[*n]

  non-consecutive repetive,   seq[=n],  exp[=n]

  goto repetitive,non-consecutive exact repetitive, seq[->n],exp[->n]

throughtout, condition over sequence。用来保证boolean condition在sequence有效期间是正确的。

   property p_seq; @(posedge clk)  $rose(req) |-> ##[1:4] enable throughout (ack ##[1:$] done); endproperty

      其中enable throughout (ack ##[1:$] done)表示一个sequence;

      ##[1:4] seq表示一个sequence;

intersect, length-match sequence 表示两个sequence从同一个clock tick 开始并且在同一个clock tick结束。

within, 表示一个sequence在另一个sequence有效中完成。

and, not-length-matching sequence,两个sequence同时开始,但是不需要同时结束。

sequence  method:

  ended,主要用在sequence在single clock assertion中的endpoint;

    ended method方法,在observe region之外是没有意义的,所以只能用在assert evaluation。

    property p_seq;  @(psoedge clk) dmaWriteBlock(dma_done).ended |-> ##[1:5] cpu_interrupt; endproperty

  matched,主要用在sequence在multi_clocks assertion中的endpoint;

    将ended的结果进行latch and multi-clock sync,只在第一个clock的observe region有效

    sequence q_1(a, b);     @(posedge clk)   $rose(a) ##[2:3] b;     endsequence

    sequence q_2;       @(posedge sysclk)   c##1 q_1(a,b).matched[->1]##1 d; endsequence

  triggered,Level-sensitive control,主要用在disable iff,或者wait sequence.triggered中。

值采样函数,$stable(exp),表示该exp的值与上一个clock tick的值相同。

  property p_seq;    $fell(req_n) |=> ack ##1 $stable(ack)[*0:100] ##1data_valid;   endproperty。

assertion-ctrl system task;

  $asserton,  $assertoff,  $assertkill。

assert cover中,可以收集assert更多的结果,主要分为coverage for properties,coverage for sequences。

  1.coverage for properties, Number of times attempted, succeeded, failed, vacuous success.

  2.coverage for sequence, Number of times attempted, matched.

assert中的clock定义:

  1. sequence中定义,

    顶层的clock定义不影响该sequence中的clock定义

    assert property中仍需要定义clock,该sequence中定义的clock不会变为property clock

  2. concurrent property中定义,

  3. procedual block中inferred clock,

  4. 本身property定义在clocking block中,

    clocking block中的input output delay并不影响assert的执行,input,output delay只是对circuit delay的建模。

  5. 定义default clocking,

  6,声明assert的时候显式指定, assert property (@posedge clk) p_seq);

    如果此时property中也定义了clock,两个clock必须相同

上一篇:启动MYSQL密码审计插件


下一篇:简单快速的Android打渠道包的方法