现在对前面几篇博客中介绍的断言进行分析，为了更好的理解，下面结合简单的代码段进行分析：

property  p1;
    @(posedge clk) a ##2 b;
endproperty

a1 : assert property(p1);

    针对这段代码段，可以做下总结：在每个时钟上升沿都检查信号“a”的电平，当a为高电平时，经过2个时钟周期后，检查信号“b”的电平，若b为高电平，则断言成功，若b为低电平，则断言失败；如果在时钟上升沿检测到信号a为低电平，断言直接失败并打印错误信息，但这并不是有效的错误信息，因为我们并不关心只检查信号“a”的电平。这个错误只是表明在时钟上升沿没有检测到有效的起始点。虽然这些错误是良性的，但在一段时间内将产生大量无效的错误信息。为了避免这些错误信息，可以利用SVA中的蕴含操作来忽略无效起始点的检查，并将断言默认为成功，称为“空成功”。

    蕴含等效于一个if-then结构，其左边称为“先行算子”，右边称为“后续算子”。只有当先行算子成功时，后续算子才能计算。如果先行算子不成功，那么该属性认为是成功即“空成功”。有一点要注意的，蕴含结构只能用在属性定义中。

蕴含包含交叠蕴含和非交叠蕴含两类。接下来分别介绍。

1、交叠蕴含

    交叠蕴含用符号“|->”表示，即当先行算子成功时，在同一个时钟周期内计算后续算子。如下测试代码：

/*******************************************************
作者   :  CrazyBird
文件   :  assert_test4.sv
日期   :  2015-5-7
功能   :  交叠蕴含
********************************************************/
`timescale 1ns/1ps
module  assert_test4(
    output reg  clk,
    output reg  a,
    output reg  b
    );
    
    //  产生时钟
    parameter   PERIOD = 10;
    
    initial
    begin
        clk = 0;
        forever #(PERIOD/2)
            clk = ~clk;  
    end
    
    //  产生激励
    initial
    begin
        a = 1;
        b = 1;
        repeat(20)@(negedge clk)
        begin
            a = {$random()}%2;
            b = {$random()}%2;
        end
        @(negedge clk);
        $stop;
    end
    
    //  建立属性
    property  p1;
        @(posedge clk) a |-> b;
    endproperty

    //  断言属性
    a1 : assert property(p1);

endmodule

    该代码在时钟上升沿检测信号“a”是否为高电平，若a为低电平，则断言默认成功即空成功；若a为高电平，则在同一个时钟上升沿检测信号“b”的电平，若b为高电平，则断言为真成功，否则断言失败。

仿真结果如下：

    红色光标处为其中一个断言空成功，红色下三角为断言失败的地方。

# ** Error: Assertion error.
#    Time: 45 ns Started: 45 ns  Scope: assert_test4.a1 File: D:/electron/modelsim/assert_test2/assert_test4.sv Line: 44
# ** Error: Assertion error.
#    Time: 75 ns Started: 75 ns  Scope: assert_test4.a1 File: D:/electron/modelsim/assert_test2/assert_test4.sv Line: 44
# ** Error: Assertion error.
#    Time: 85 ns Started: 85 ns  Scope: assert_test4.a1 File: D:/electron/modelsim/assert_test2/assert_test4.sv Line: 44
# ** Error: Assertion error.
#    Time: 95 ns Started: 95 ns  Scope: assert_test4.a1 File: D:/electron/modelsim/assert_test2/assert_test4.sv Line: 44
# ** Error: Assertion error.
#    Time: 165 ns Started: 165 ns  Scope: assert_test4.a1 File: D:/electron/modelsim/assert_test2/assert_test4.sv Line: 44

2、非交叠蕴含

    非交叠蕴含用符号“|=>”表示，即当先行算子成功时，在下一个时钟周期计算后续算子。如下测试代码：

/*******************************************************
作者   :  CrazyBird
文件   :  assert_test5.sv
日期   :  2015-5-7
功能   :  非交叠蕴含
********************************************************/
`timescale 1ns/1ps
module  assert_test5(
    output reg  clk,
    output reg  a,
    output reg  b
    );
    
    //  产生时钟
    parameter   PERIOD = 10;
    
    initial
    begin
        clk = 0;
        forever #(PERIOD/2)
            clk = ~clk;  
    end
    
    //  产生激励
    initial
    begin
        a = 1;
        b = 1;
        repeat(20)@(negedge clk)
        begin
            a = {$random()}%2;
            b = {$random()}%2;
        end
        @(negedge clk);
        $stop;
    end
    
    //  建立属性
    property  p1;
        @(posedge clk) a |=> b;
    endproperty

    //  断言属性
    a1 : assert property(p1);

endmodule

    该代码在时钟上升沿检测信号“a”是否为高电平，若a为低电平，则断言空成功；若a为高电平，则在下一个时钟上升沿检测信号“b”的电平，若b为高电平，则断言真成功，否则断言失败。

仿真结果如下：

# ** Error: Assertion error.
#    Time: 45 ns Started: 35 ns  Scope: assert_test5.a1 File: D:/electron/modelsim/assert_test2/assert_test5.sv Line: 44
# ** Error: Assertion error.
#    Time: 85 ns Started: 75 ns  Scope: assert_test5.a1 File: D:/electron/modelsim/assert_test2/assert_test5.sv Line: 44
# ** Error: Assertion error.
#    Time: 95 ns Started: 85 ns  Scope: assert_test5.a1 File: D:/electron/modelsim/assert_test2/assert_test5.sv Line: 44
# ** Error: Assertion error.
#    Time: 165 ns Started: 155 ns  Scope: assert_test5.a1 File: D:/electron/modelsim/assert_test2/assert_test5.sv Line: 44
# ** Error: Assertion error.
#    Time: 175 ns Started: 165 ns  Scope: assert_test5.a1 File: D:/electron/modelsim/assert_test2/assert_test5.sv Line: 44

    扩展一下，在避免无效错误信息出现的前提下，前面博文介绍的“a ##2 b”等价于”a |-> ##2 b”，这一块的验证自己动手做吧。

    待续~~~