crazybird

【SystemVerilog断言学习笔记7】蕴含操作

0
阅读(4355) 评论(4)

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

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为高电平,则断言为真成功,否则断言失败。

仿真结果如下:

10

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

# ** 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

11

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为高电平,则断言真成功,否则断言失败。

仿真结果如下:

12

# ** 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

13

 

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

 

    待续~~~

  1. @2004111

  2. @liuyu17500

  3. 谢谢,学习中
  4. 楼主写的很好,很受启发啊