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

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”，这一块的验证自己动手做吧。

待续~~~