SVA(system verilog assertions)基础

1甚么是断言：

  断言就是在摹拟进程中根据我们事前安排好的逻辑是否是产生了,如果产生断言成功，否则断言失败。

2断言的履行分为：豫备（preponed）视察(observed)响应(reactive).

3断言的分类：并发断言（基于时钟）和即时断言（基于语义）。

4SVA（system Verilogassertions）：块的建立：

序列：

  Sequencename_of_sequence;

    <test expression>

Endsequence

Property name _of_ property

 <test expression>

Or

<sequence>

Endproperty

Assertions _name: assert property (property_name) ortest_expression;

履行块：

Assertion_name:

      Assertproperty(property_name)

         <success message>

      Else

          <fail message>

注：保持序列独立于时钟，属性中定义时钟是好的编码风格。

5 SVA检测器的步骤：

建立布尔表达式->建立序列表达式->建立属性->断言属性；

6经常使用语句及函数：

 $rose()：检测信号上升沿

 $fell(): 检测信号降落沿

 $stable(); 检测信号是不是稳定。

  ##n：表示延迟N个时钟周期。

 ##[n1:n2]:延时在n1到n2个时钟周期以内。

 ##[n1:$]:延时在n1到无穷个时钟周期以内。

  not：检测属性不为真的情况（制止属性）

  |->:如果先行算子匹配在同1个时钟周期检测后续算子

 |=>:如果先行算子匹配在下1个时钟周期检测后续算子

 ended: 以序列的结尾作为多个序列的连接点

  xx？xx:xx：问号表达式与c相同。

 `define true 1:利用true表达式可实现序列延时n个周期。

 $past(signal_name, number of clock cycles，[gating signal]):用来检测n个时钟周期之前逻辑表达式的值。

  Signalor sequence [*n] 连续重复

  Signal[->n]：跟随重复(在其后必须有1个信号使得最后1次重复有效产生在其后逻辑产生之前的时钟周期)。

  Signal[=n]：非连续重复，重复次数为n

  and: 两个序列必须有相同的起始点。

  intersect:两个序列必须在相同时刻开始并且结束于同1时刻。

  or:其中1个序列成功便可。

  first_match:and or的序列中指定了时间窗，便可能同1检验具有多个匹配的情况。first_match确保只是用第1次序列匹配。

  throughout:(expression) throughout (sequence definition)保证某些条件在检测进程中1直为真。

  within:seq1 within seq2。seq1序列的检测必须包括在seq2的起始点和结束点。

 内建系统函数：

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

   $onehot0(expression):有1位或没有位为高。

   $isunknown(expression):检查表达式的任何位是不是为x或z。

   $countones(expression):计算向量中为高的位的数量。

disable iff (expression)  <property definition>: 当某些条件为真时则不进行检测。

matched: 可以用来检测第1个子序列的结束点。

expect:属性成功的检验

<cover_name>: cover property (property_name):cover会检测序列的：被尝试检测次数；属性成功次数；属性失败次数；属性空成功次数。

71个例子：

 sequences32a;

   @(posedgeclk)

     ((!a&&!b) ##1 (c[->3]) ##1 (a&&b)); //信号a和信号b均为低电平，经过1个时钟的延时后检测信号c是不是连续出现3次高电平，且c最后1次为高电平时，经过1个时钟延时信号a和信号b均为高电平。

endsequence

 sequences32b;

   @(posedgeclk)

     $fell(start) ##[5:10] $rose(start); //从start的降落沿开始，经过5⑴0个时钟周期start出现上升沿。即start保持低电平5⑴0个时钟周期。

endsequence

sequence s32;

   @(posedgeclk)

     s32a within s32b; //序列s32a 包括在 s32b中，即序列s32b的起始点和结束点包括s32a的起始点和结束点

endsequence

property p32;

   @(posedgeclk)

     $fell(start) |-> s32;//在start的降落沿立即检测s32.

endproperty

a32: assert property(p32);