SVA概述

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig1,sig2;
initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end
initial begin
       sig1 = 1'b0; sig2 = 1'b1;
    #4 sig1 = 1'b1; #6 sig2 = 1'b0;
    #30 $stop;
end
// Normal Verilog format
always @(posedge sig1)
begin : v_f
    repeat(2)@(posedge clk);
    fork
        begin : p1
            @(negedge sig2) $info("== From Verilog ==");
            disable v_f;
        end
        begin : p2
            repeat(3) @(posedge clk);
            $info("== Verilog Fail ==");
            disable v_f;
        end
    join
end
// SVA format
property p0;
    @(posedge clk) $rose(sig1) |-> ##[2:3] $fell(sig2);
endproperty // p0

ap0 : assert property(p0) $info ("== From SVA == ");
             else $info("== SVA Fail ==");
cp0 : cover property(p0) $info("== Covered! ==");
endmodule    // top_tb

从上述仿真对比可以看到使用Verilog实现同样的检测，SVA完美的仅仅几行代码就能准确实现，同时还可以自动收集相应的覆盖率进行分析统计，并且在理解了词法结构后可读性很高。那么除了上述示例中展示出来的SVA特点之外，在设计验证过程中使用SVA还有哪些优点呢？这里先介绍一些特点，在后续的学习记录中将通过各种示例展示SVA的以下特点。

Ø 使用断言可以缩短研制周期；

Ø 使用断言可以使设计中存在的各种问题更容易被动态监测观察；

Ø 使用断言内嵌的覆盖率统计功能（cover）可以更加容易的获得对于功能的覆盖性；

Ø 断言不止可以用于单一时钟域的设计中，也可以用于多时钟域的设计中；

Ø 断言的可读性较一般描述语言更容易理解；

Ø 断言可以形成AIP，复用于其他项目；

Ø 开通过全局控制实现设计中断言的开关；

Ø 因为断言本身的特点，可以轻松的在进行断言检查的过程中实现覆盖率的统计；

具有这么多的优点，那么断言应该在电路研制的哪个环节添加呢？是在验证环节还是代码设计环节？一般情况下，不论是设计人员还是验证人员，在构建各自的设计时都需要增加嵌入一定的断言。对于设计人员来说，设计人员对于芯片的内部结构和逻辑更加了解，所以设计人员更适合在设计中插入断言。对于验证人员来说，验证人员因为需要访问芯片的各种接口，需要构建各种不同的测试用例，施加不同的激励，更适合在设计的就增加断言，实现对于接口和宏观功能的检查。综上所述，一般在一个电路的设计验证过程中可以在以下部位考虑增加断言设计。

Ø 模块内部的断言，例如设计中的状态机的状态跳转、特定的编码结构、存储器等；

Ø 模块间的接口时序，特别是具有特定协议要求的接口；

Ø 芯片端口的时序和具有特定的协议要求的接口；

Ø 功能性测试，特定的协议握手等；

Ø 在编写断言的过程中可以再次的审阅设计的正确性；

加入的断言根据使用的特点不同，可以分为如下图所示的几类。

其中Immediate Assertion为即时断言，即时断言本身又有一些细分，两者的主要区别在于断言析构时在同一个时间槽中处理的阶段不同。即时断言定义于过程性语句中，其行为一般不依赖于具体的时钟，当断言判断表达式中的任何信号发生变化，该检查都会被立即执行，可以理解该断言为不需要耗费时间的断言。Concurrent Assertion为并发断言，并发断言中的判断表达式是基于采样事件采样相关信号后才进行相应的处理，即其是采样事件敏感的，可以再过程块（procedural block）、模块（module）、接口（interface）和程序块（program）中定义使用，并且既可以用于动态仿真过程中，也可以用于静态仿真过程中（至于有些人说断言只能用于静态仿真表示不是很理解）。这里需要注意，在使用SVA的过程中，经常会遇到assume，其实在仿真的过程中，其作用域assert一样，只是在静态形式化验证过程中，assume可以对于判断条件中的各种信号起到约束的作用，从而可以有效地避免形式化验证过程中部分条件组合的空间爆炸问题，如下表示例所示。

那么在具体的应用过程中如何构建两种类型的断言呢？

即时断言一般存在于过程块中，并且其执行不受采样事件的影响，其使用方法较为简单，一般构建流程格式如下：

通过在即时断言中增加cover可以获得断言被执行的次数以及成功和失败的次数等信息，具体输出哪些信息不同的仿真器输出的数据结果可能会有差异。

从上述断言的构建流程可以看出，即时断言跟并发断言在语法结构上最显著的区别在于，即时断言不存在于property，而并发断言构建的过程中依赖于property。

即时断言

因为即时断言定义于过程块中，所以即时断言是不能出现在连续赋值语句中，如下例这种方式编译就会报错。

【示例】即时断言不能定义于连续赋值语句中

assign sig1 = assert(sig2 && sig3);    // illegal

示例中使用了“severity level system task”，其实在断言中不止可以使用示例中的$info还可以根据需要使用其他的函数或者任务，同时还可以给断言增加标号，从而可以提高仿真调试的效率。

【示例】不要在断言中增加可执行的RTL设计代码，虽然语法正确，但是因为assert模块通常会在综合时被忽略掉

`timescale 1 ns / 1 ps
module top_tb;
bit sig1,sig2,sig3,sig4;

initial begin
       sig1 = 1'b0;sig2 = 1'b0;sig4 = 1'b0;
    #1 sig1 = 1'b1;sig2 = 1'b1;
    #1 sig1 = 1'b0;sig2 = 1'b1;
    #1 sig1 = 1'b1;sig2 = 1'b0;
    #1 $stop;
end

always @(sig1&nbs***bsp;sig2)
begin
    sig3 = sig1 & sig2;
    assert_exp : assert(sig1 & sig2) $info("%m : Passed!"); 
                 else begin
                     $info("%m : Failed!");
                     sig4 = 1'b1;  // Not Suggested!
                 end
end
endmodule // top_tb

示例中，虽然断言的可执行分支中可以适用任何结构，但是出于可实现的原因，一般情况下不要在断言的可执行分之中使用意图要被实现的电路功能结构。

并发断言

并发断言与即时断言的根本不同点是并发断言是基于采样事件的，且其结构中存在即时断言不存在的property。并发断言主要用于存在时序关系的序列中。并发断言的构造流程如上文所述，下面在通过示例进行说明。

【示例】

`timescale 1 ns / 1 ps
module top_tb;
logic clk;
logic sig1,sig2,sig3;

initial begin
    clk = 1'b0;
    forever #1 clk = ~clk;
end
initial begin
       sig1 = 1'b0;sig2 = 1'b0;sig3 = 1'b0;
    #2 sig1 = 1'b1;
    #2 sig1 = 1'b0;sig2 = 1'b1;
    #4 sig3 = 1'b1;
    #4 $stop;
end
// 0 > pick spec
/*
  At posedge clk,if sig1 is high,
  that sig2 is high later one clk,
  and sig3 is high later two clk after sig2.
clk  : ____+---+____+---+____+---+____+---+____+---+____
sig1 : ____________+---+________________________________
sig2 : ____________________+----------------------------
sig3 : ______________________________________+----------
*/
// 1 > create sequence
sequence s;
    sig2 ##2 sig3;
endsequence // s
// 2 > create property
property p;
    @(posedge clk) sig1 |=> s;
endproperty // p
// 3 > assert property
a : assert property(p) $display("@%0t | PASSED!",$time);
    else $display("@0t | FAILED!",$time);
c : cover property(p) $display("Covered!");
endmodule // top_tb