Systemverilog之SVA（一）

标签：断言 sequence clk SVA property Systemverilog 时钟

  前言

systemverilog assertion作为systemverilog引入的重要特性，在功能仿真及形式验证中有着重要的作用。相较于Verilog传统的checker，SVA作为声明性的语言，使用简单易于管理；在时序检测，协议监控上有着非常便捷的优势。文章参考《A Practical Guide for Systemverilog Assertions》。

1 SVA的执行原则

sva中所采用的变量在进入时隙的Preponed区域进行采样，在Observed区域进行断言的评估，而评估结果将在Reactive区域进行响应。由于DUT的执行更新是在active，inactive，NAB区域进行，因而断言诊断在时序图上“滞后了一个时钟周期”。

2 SVA分类

SVA有立即断言（Immediate asseration）与并发断言（Concurrent asseration）。

2.1 并发断言

并发断言基于时钟周期进行，可以放置于procedural block、module、interface及program中。在静态(形式）验证及动态仿真工具中均可以应用。

简单的并发断言示例如下：

a_cc:assert property ((@posedge clk) not(a&&b));

a_cc将在每个时钟上升沿进行断言检测，若a和b同时为高，则断言失败。

2.2 立即断言

立即断言基于事件，必须放置在程序块中，只能用于动态仿真，没有时间的概念。立即断言与并发断言关键字区分在于“property”。简单的立即断言示例如下：

always_comb
begin
     a_ia :assert(a&&b);
end

像Verilog的连续赋值块，当a或b变化时，a_ia会执行，当a和b都为高时断言成功，否则断言失败。

3 SVA（并发断言）的建立

由于代码功能块实现往往跨越多个时钟周期或多个信号组合，SVA提供了sequence关键字，sequence原语如下：

sequence name_of_sequence;
   <test_expression>;
endsequence

多个sequence可以组合成更复杂的序列，SVA提供property关键字以组织复杂序列，其原语如下：

property name_of_property;
   <test expression>; or
   <complex sequence expression>;
endproperty

propertys属性必须在仿真过程中通过关键字assert进行使能检测，assert原语为：

assertion_name:assert property (property_name);

SVA构建流程如下：

3.1 sequence

简单的sequence示例如下：

sequence s1;
  @(posedge clk) a;
endsequence   

s1将在每个上升沿检测a是否为1，若是，则断言成功，否则断言失败。

3.1.1 带有边沿定义的序列

SVA提供带有边沿检测的原语序列用于监控边沿变化：

$rose(boolean expression or signal_name):当信号的LSB从低变为高时返回真。

$fell(boolean expression or signal_name):当信号的LSB从高变为低时返回真。

$stable(boolean expression or signal_name):信号不发生变化时返回真。

示例：

sequence s2;
 @(posedge clk) $rose(a);
endsequence

s2将在每个时钟上升沿检查a是否跳变为1.检测结果如下图：

注意图中在时刻1处a跳转为1，但在时刻2处方断言成功。原因在于信号的改变发生在上升沿之后，断言的采样发生在时隙的prepond区域，有一个时钟的延迟。

3.1.2 带有边沿定义的序列

序列可通过带有形式参数的参数列表进行复用。设计中的一些公共属性（如独热码状态机，奇偶校验等）可设置带参数的序列库进行重用。

示例：

sequence s3_lib(a,b);
      a||b;
endsequence
#s3_lib可复用在任何两个信号中
sequence s3_lib_inst1;
 s3_lib(req1,req2);
endsequence

3.1.3 跨时钟周期的序列

在SVA中，时钟延迟用符号“##”表示。##3代表三个时钟周期。

示例：

sequence s4;
   @(posedge clk) a ##2 b;
endsequence

s4在每个时钟沿检测a是否为高，若是则检测两个时钟周期后b是否为高，若是则断言成功

注意：s4序列检测起始和结束时间并不在同一时刻。若a断言失败，则起始和结束时间相同，否则不同。同时断言成功与否标注在序列的开始时刻。

3.2 时钟的定义

SVA在仿真过程中，sequence和property本身是不做任何事的，要想是他们有效，必须通过assert进行声明。

SVA时钟可以在sequence，property甚至assert中进行定义，但应注意：

时钟最好在property中进行定义而不要在sequence中定义，从而保证sequence的独立性，也方便复用。

可以在assert中同时定义时钟和使用sequence，但不允许同时定义时钟和使用property。

示例

sequence s5a;
 a ##2 b;
endsequence
property p5;
 @(posedge clk) s5;
endproperty
a5: assert property (p5);
#或省略property
a5b: assert property (@(posedge clk) s5a);

3.3 禁止属性的定义

属性property也可以被定义为不希望发生，即若property中序列发生，则断言失败，可以使用关键词not进行声明。

示例：

sequence s6;
 @(posedge clk) a##2 b;
endsequence
property p6;
 not s6;
endproperty
a6: assert property (p6);

上例中若在某时钟沿a为高点平，且两个时钟后b为高电平则断言失败，否则断言成功。

4 响应块（action block）

默认情况下，SVA在断言失败的情况下会打印失败信息，而断言成功则不打印。可通过响应块自定义断言处理状况。响应块定义原语如下：

assertion_name:

assert property (property_name)

<sucess message>;

else

<fail message>;

在仿真过程中，可通过响应块控制仿真及功能覆盖率收集等。

5 蕴含操作符

上述断言中，SVA会在每个时钟沿进行检测，若不符合情况则断言失败，但有时往往关注某信号发生变化后的时序关系，这将导致大量并非我们所关心的断言失败情况产生。为避免这种情况，SVA引入蕴含操作符(Implication)来起一个门控作用。

蕴含操作符类似于if-then结构。蕴含操作符左侧称之为先验部分（antecedent），右侧称之为后验结果(consequent)。若先验部分验证成功，后验结果才进行检查，否则若先验部分验证失败，则认为是“伪成功”。蕴含操作符用于property中，不可用于sequence中！

蕴含操作符包含：交叠蕴含操作符和非交叠蕴含操作符。

5.1 交叠蕴含操作符（Overlapped implication）

交叠蕴含操作符符号为 |->

交叠蕴含操作符中，若先验部分验证成功，则后验结果在同一时钟进行验证。如下例所示,若某时钟处a变为高电平，则同一时刻b也应为高电平。

property p8;
 @(posedge clk) a |-> b
endproperty
a8:assert property (p8);

时刻1、6为伪成功。

5.2 非交叠蕴含操作符（Non-overlapped implication）

非交叠蕴含操作符符号为|=>。

非交叠蕴含操作符在先验部分验证匹配后，在下个时钟沿才进行后验部分的检查匹配。相对于蕴含操作符后验部分有一个时钟的滞后。如下例所示，在时钟边沿a为高电平则一个时钟后b也应为高电平。

property p9;
 @(posedge clk) a |=> b;
endporperty
a9:assert property(p9);

5.3 序列作为先验部分

在蕴含操作中，先验部分不仅可使用变量，也可使用序列。使用序列作为先验部分，在序列验证成功后则进行后验部分的验证匹配。

sequence s11a;
  @(posedge clk) (a&&b) ##1 c;
endsequence
sequence s11b;
 @(posedge clk) ##2 !d;
endsequence
property p11;
 s11a |->s11b;
endproperty
a11:assert property(p11);

（后验序列的计时起点为先验序列结束时刻。由于s11a有一个时钟周期延迟，因而检测！d在（a&&b）三个时钟周期后进行)。

6 SVA检查中的时间窗口

之前示例中时钟延时往往是固定格式的，SVA允许时间窗的引入，其表示形式为##[minperiod : max_period],表示后续部分在min_period到max_period个时钟周期内验证成功则断言通过。示例如下：

property p12;
   @(posedge clk) a&&b |-> ##[1:3] c;
endproperty
a12: assert property(p12);

上述断言在时钟沿处若a和b同时为高，则在1至3个时钟周期后c应为高电平。

延时时间上线可以设置为$表示不设上限，将一直检测到断言成功或仿真结束为止。

7 SVA检查之ended

默认情况下，多重sequence的组合是以个sequence的起始时间作为同步标志的，SVA提供ended结构以sequence的结束时间作为序列同步点。ended的用法如下：

sequence_name.ended

若使用ended，则sequence必须定义时钟。关键字ended存储一个反映在指定时钟处序列是否匹配成功的布尔值。该布尔值尽在同一时钟内有效。

下述四种属性检查定义相同：

sequence s1;
 @(posedge clk) a##1 b;
endsequence
sequence s2;
 @(posedge clk) c ##1 d;
endsequence
property p1;
s1|=>s2; //s1的成功匹配点滞后一时钟周期是s2匹配的起点
endproperty
property p2;
s1|=>##1 s2.ended; //s1成功匹配点滞后两个时钟周期是s2成功匹配点，即s1匹配成功则再过两个时钟周期s2必须匹配成功
endproperty
property p3;
s1.ended|=>s2; //s1的成功匹配点滞后一时钟周期是s2匹配的起点
endproperty
property p4;
s1.ended|=> ##1 s2.ended;//s1成功匹配点滞后两个时钟周期是s2成功匹配点，即s1匹配成功则再过两个时钟周期s2必须匹配成功
endproperty

8 SVA参数（parameter）列表

SVA允许在sequence或property中使用parameter参数以重定义或适用于不同的场景。

module generic_chk(input logic a,b,clk);
parameter delay=1;
property p16;
  @(posedge clk) a|->##delay b;
endproperty
a16:assert property(p16);
endmodule
module top();
 logic a,b,c,d;
generic_chk#(.delay(2))i1(input logic a,b,clk);
generic_chk i2(input logic c,d,clk);
endmoule

9 选择运算符

SVA允许使用选择运算符？：如下例所示：

property p17;
     @(posedge clk) c? d==a:d==b;
endporperty

p17在上升沿检测c点评，为高时判定d是否等于a，为低时判定d是否等于b。

10 真值表达式

真值表达式： `ture （需自己定义 `defien true 1）

使用true表达式，可以在时间上延长SVA检验器，能够使序列的结束点延长一个时钟周期，这可以用来实现同步检测多个属性且需要同时成功检测的复杂协议。

`ddefine true 1
sequence s18a;
  @(posedge clk) a ##1 b;
endsequence
sequence s18a_ext;
  @(posedge clk) a##1 b ##1 `true;
endsequence;
sequence s18b;
 @(posedge clk) c##1 d;
endsequence;
property p18;
  s18a.ended |->##2 s18b.ended;
endproperty
property p18_ext;
  s18a_ext.ended |=>s18b.ended;
endproperty
a18 :assert property(p18);
a18_ext: assert property(p18_ext);

上例中a18、a18_ext作用相同，均检测序列 a##1 b ##1 c ##1 d;

11 前向检测

SVA提供内建任务$past用于获取之前时钟沿某处的值。其原语为：

$past(signalname,numberof_clock_cycles)

默认缺省情况下，SVA提供前一个时钟沿处的信号值。

示例：

property p19;
 @(posedge clk) (c&&d)|->($past((a&&b),2)==1);
endproperty;
a19:assert property(p19);

a19检测在时钟沿处若c和d同时为1，则在前溯第二个时钟沿处a和b应为1。

$past允许使用带有时钟门控信号的检测匹配。

$past(signal_name,number_of_clock_cycles,gating_signal);

property p20;
  @(posedge clk) (c&&d)|->($past((a&&b),2,enable)==1);
endproperty
a20:assert property(p20);

a20同a19类似，不过若c和d同时为1，则前溯第二个时钟沿处使能信号enable必须为高且a和b必须为高。

标签：断言,sequence,clk,SVA,property,Systemverilog,时钟
From： https://www.cnblogs.com/amxiang/p/16749377.html