Systemverilog断言属于验证方法中的一种，断言(assertions)就是对设计属性(行为)的描述，如果一个属性不是我们期望的那样，那么断言就会失败。assertions与verilog相比，verilog是一种过程性语言。它的设计目的是硬件描述，它可以很好的控制时序，但是描述复杂的时序关系，代码较为冗长，assertions是一种描述性语言，设计目的为仿真验证，可以有很多内嵌的函数来测试特定的时序关系和自动收集覆盖率数据。

      SVA分为并发断言和即时断言两种。并发断言是基于时钟周期的，在时钟边沿计算表达式，它可以放在模块(module)，接口(interface)，或程序块(program)的定义中，以关键词“property”来定义，可以在静态验证工具和动态验证工具中使用。即时断言是基于事件的变化，表达式的计算像verilog中的组合逻辑赋值一样，是立即被求值的，与时序无关，必须放在过程块中定义。

       并发assertions：     property   a2b_p;           //描述属性

                                                      @(posedge sclk)   $rose(a) |->[2:4] $rose(b);

                                       endproperty

                                       a2b_a:   assert property(a2b_p);      //assert property SVA的关键字表示并发断言

                                       a2b_c:   cover  property(a2b_p);      //覆盖语句

       由Modelsim 6.1b中的仿真波形来看：断言信号为高阻态表示没有被激活，断言信号为1表示断言被激活，正在检查时序属性，倒三角表示断言在此刻失败，正三角表示断言在此刻成功。其中a和b的上升沿相比较sclk会表现出晚一个时钟被采样，也就是说在sclk=1时，a为0，sclk=2时，a为1，则sclk=3时，SV才会知道a来了一个上升沿。

        断言的组成与时序建立过程：断言的建立过程为"编写布尔表达式----->编写序列(sequence)------>编写属性(property)------>编写断言(assert property)和覆盖语句(cover property)"。其中的sequence是SVA中的关键字，来完成时序模型的建立----可以表达同一时钟沿被求值的布尔表达式，也可以是经过几个时钟周期计算得到的事件。

        断言应用中的两个例子：

        1)简单的逻辑值检测建模：         sequence   s1_s；

                                                                    @(posedge  sclk)   a;

                                                           endsequence

                                                            a1_a:   assert  property(s1_s);

                                                                           $display("");     else   $diaplay("");

                                                            c1_c:    cover  property(s1_c);

这个断言表示在每个sclk中a都必须为高电平，采用sequence关键字，并且可以自定义显示内容$display。

                                                            sequence  s2_s;

                                                                        @(posedge sclk)   a ##2 b;

                                                            endsequence

表示信号a在某个时钟为高电平，两个时钟周期后，信号b也必须为高电平，此时断言才会成功，如果a不是高电平，则断言也是失败。

       2)信号边沿检查，SVA提供了三个函数$rose()，$fell()，$stable()。

                                    sequence   rose_s;

                                             @(posedge sclk)  $rose(a);

                                    endsequence

                                    sequence  fell_s;

                                             @(posedge sclk)   $fell(a);

                                    endsequence

                                    sequence  stable_s;

                                              @(posedge sclk)   $stable(a);

                                    endsequence

rose_a用于检测信号a的上升沿，它只在“a在当前时钟周期是高电平，在上一个时钟周期是低电平或不定态x”情况下才成功。fell_a用于检测信号a的下降沿，它只在“a在当前时钟周期是低电平，在上一个时钟周期是高电平和不定态x”情况下才成功。stable_a用于检测信号a不变的情况。

       3)为了有效的控制时序建模的起点，引入了蕴含操作符(implication)，只能应用在"属性"property中。其中可以分为两类：交叠蕴含操作符(overlapped implication，|——>)和非交叠蕴含操作符(non_overlapped implication，|——>)。操作符左边项为"先行算子"，右边项为"后序算子"，其中先行算子是约束条件。在交叠蕴含操作符中，先行算子匹配后，后序算子在下一个时钟周期开始计算。在非交叠蕴含操作符中，先行算子匹配，后序算子在同一个时钟周期计算。

      序列的重复操作符分为3类：连续重复"[*m]","[*3]"表示a被连续重复3次，"a[*1:3]"表示a被连续重复1--3次。两次重复之间只有一个时钟间隔。跳转重复操作符"[->m]"，"a[->3]"表示a被跳转重复3次，"a[*1:3]"表示a被跳转重复1--3次，每次重复之间可以任意时钟间隔。非连续重复操作符"[=m]"，"a[=3]"表示a被非连续重复3次，非连续重复每次重复之前可以有任意时钟周期，并且最后一次重复后可以有任意个时钟周期。

                                          property   cons_rep_p;

                                                   @(posedge  sclk)  $rose(a) |-> ##1 b[*3]  ##1  c;

                                          endproperty

                                          property   gotorep_p;

                                                    @(posedge sclk)  $rose(a) |-> ##1 b[->3] ##1 c;

                                          endproperty

                                          property   non_cons_rep_p;

                                                    @(posedge sclk)  $rose(a) |-> ##1 b[=3]   ##1 c;

                                          endproperty

cons_rep_p表示在信号a出现上升沿，后一个时钟，信号b连续三次为高电平，再推迟一个时钟后，信号c为高电平，断言成功。