SystemVerilog断言学习笔记 - 图文 (4)

// 产生激励 initial begin a = 1; b = 1; repeat(20)@(negedge clk) begin a = {$random()}%2; b = {$random()}%2; end @(negedge clk); $stop; end //建立序列 sequence s1; a ##2 b; endsequence // 建立属性 property p1; @(posedge clk) s1; endproperty // 断言属性 a1 : assert property(p1); endmodule 按照代码的描述，其任务是检查信号a在给定的时钟上升沿是否为高电平。若a为低电平，断言直接失败；若a为高电平，则延迟2个时钟周期后检查b是否为高电平。若b为高电平，表示断言成功；若b为低电平，表示断言失败。 其仿真结果如下所示： # ** Error: Assertion error. # Time: 15 ns Started: 15 ns Scope: assert_test2.a1 File: D:/electron/modelsim/assert_test2/assert_test2.sv Line: 49 # ** Error: Assertion error. # Time: 45 ns Started: 25 ns Scope: assert_test2.a1 File: D:/electron/modelsim/assert_test2/assert_test2.sv Line: 49 # ** Error: Assertion error. # Time: 65 ns Started: 65 ns Scope: assert_test2.a1 File: D:/electron/modelsim/assert_test2/assert_test2.sv Line: 49 # ** Error: Assertion error. # Time: 75 ns Started: 55 ns Scope: assert_test2.a1 File: D:/electron/modelsim/assert_test2/assert_test2.sv Line: 49 # ** Error: Assertion error. # Time: 95 ns Started: 75 ns Scope: assert_test2.a1 File: D:/electron/modelsim/assert_test2/assert_test2.sv Line: 49 # ** Error: Assertion error. # Time: 115 ns Started: 115 ns Scope: assert_test2.a1 File: D:/electron/modelsim/assert_test2/assert_test2.sv Line: 49 # ** Error: Assertion error. # Time: 125 ns Started: 125 ns Scope: assert_test2.a1 File: D:/electron/modelsim/assert_test2/assert_test2.sv Line: 49 # ** Error: Assertion error. # Time: 125 ns Started: 105 ns Scope: assert_test2.a1 File: D:/electron/modelsim/assert_test2/assert_test2.sv Line: 49 # ** Error: Assertion error. # Time: 135 ns Started: 135 ns Scope: assert_test2.a1 File: D:/electron/modelsim/assert_test2/assert_test2.sv Line: 49 # ** Error: Assertion error. # Time: 145 ns Started: 145 ns Scope: assert_test2.a1 File: D:/electron/modelsim/assert_test2/assert_test2.sv Line: 49 # ** Error: Assertion error. # Time: 175 ns Started: 175 ns Scope: assert_test2.a1 File: D:/electron/modelsim/assert_test2/assert_test2.sv Line: 49 # ** Error: Assertion error. # Time: 175 ns Started: 155 ns Scope: assert_test2.a1 File: D:/electron/modelsim/assert_test2/assert_test2.sv Line: 49 # ** Error: Assertion error. # Time: 185 ns Started: 185 ns Scope: assert_test2.a1 File: D:/electron/modelsim/assert_test2/assert_test2.sv Line: 49 # ** Error: Assertion error. # Time: 195 ns Started: 195 ns Scope: assert_test2.a1 File: D:/electron/modelsim/assert_test2/assert_test2.sv Line: 49 待续~~~ 【SystemVerilog断言学习笔记6】禁止属性的使用 当我们期望属性永远为假时，可以用关键字―not‖来禁止属性，即当属性为真时断言失败。接下来验证―not‖是如何运作的。 测试代码： /******************************************************* 作者 : CrazyBird 文件 : assert_test2.sv 日期 : 2015-5-7 功能 : 禁止属性“not”的测试 ********************************************************/ `timescale 1ns/1ps module assert_test2( 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 // 建立序列 sequence s1; a ##2 b; endsequence // 建立属性 property p1; @(posedge clk) not(s1); endproperty // 断言属性 a1 : assert property(p1); endmodule 注意―not‖所在的位置，如果是下面的写法，编译将报错： // 建立序列 sequence s1; a ##2 b; endsequence // 建立属性 property p1; not(@(posedge clk) s1); endproperty 或者 // 建立序列 sequence s1; @(posedge clk) a ##2 b; endsequence // 建立属性 property p1; not(s1); endproperty 测试结果： # ** Error: Assertion error. # Time: 25 ns Started: 5 ns Scope: assert_test2.a1 File: D:/electron/modelsim/assert_test2/assert_test2.sv Line: 49 # ** Error: Assertion error. # Time: 55 ns Started: 35 ns Scope: assert_test2.a1 File: D:/electron/modelsim/assert_test2/assert_test2.sv Line: 49 # ** Error: Assertion error. # Time: 65 ns Started: 45 ns Scope: assert_test2.a1 File: D:/electron/modelsim/assert_test2/assert_test2.sv Line: 49 # ** Error: Assertion error. # Time: 105 ns Started: 85 ns Scope: assert_test2.a1 File: D:/electron/modelsim/assert_test2/assert_test2.sv Line: 49 # ** Error: Assertion error. # Time: 115 ns Started: 95 ns Scope: assert_test2.a1 File: D:/electron/modelsim/assert_test2/assert_test2.sv Line: 49 # ** Error: Assertion error. # Time: 185 ns Started: 165 ns Scope: assert_test2.a1 File: D:/electron/modelsim/assert_test2/assert_test2.sv Line: 49 很明显，当时钟上升沿到来时，若a为高电平，2个时钟周期后，若b也为高电平，则断言失败，且失败标注在序列的结束位置。当时钟上升沿到来时，若a为低电平，则断言直接成功；若a为高电平，2个时钟周期后b为低电平，则断言成功。这刚好跟―a ##2 b‖的属性相反，故验证了―not‖是可以禁止属性的。 待续~~~ 【SystemVerilog断言学习笔记7】蕴含操作 现在对前面几篇博客中介绍的断言进行分析，为了更好的理解，下面结合简单的代码段进行分析： 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,