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：检测属性不为真的情况（禁止属性）

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

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

 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]：跟随重复(在其后必须有一个信号使得最后一次重复有效发生在其后逻辑发生之前的时钟周期)。

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

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

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

  or:其中一个序列成功即可。

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

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

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

 内建系统函数：

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

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

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

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

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

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

expect:属性成功的检验

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

7一个例子：

 sequences32a;

   @(posedgeclk)

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

endsequence

 sequences32b;

   @(posedgeclk)

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

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);

SVA(system verilog assertions)基础