SVA中内嵌了信号边沿检测函数，方便用户监视信号从一个时钟周期到另一个时钟周期的跳变。其中，有三个非常有用的内嵌函数如下：

（1）$rose(boolean expression or signal_name)：当表达式/信号的最低位由0变为1时返回真；

    针对上述的描述，可以得出两个结论：
（1）这三个内嵌函数是工作在时钟边沿上的；
（2）这三个内嵌函数只检测信号的最低位，而忽略其他位。

    接下来，带着这两个结论以及运用上一篇博客对SVA块的建立步骤对三个内嵌函数进行验证。

1、$rose()函数的验证

    为了验证内嵌函数$rose()是工作在时钟边沿上的，这里给出一个简单的反例即不受时钟控制：

/*******************************************************
作者   :  CrazyBird
文件   :  rose_test.sv
日期   :  2015-5-6
功能   :  $rose()函数的验证
********************************************************/
`timescale 1ns/1ps
module rose_test(
    output reg        clk,
    output reg  [1:0] a
    );
    //  时钟的产生
    parameter PERIOD = 10;
  
    initial
    begin
        clk = 0;
        forever #(PERIOD/2)
        clk = ~clk;
    end
  
    //  激励的产生
    initial
    begin
        a = 0;
        repeat(20)@(negedge clk)
        begin
        a = {$random()}%2**2;
        end
        @(negedge clk);
        $stop;
    end
  
    //  断言
    always_comb
    begin
        a_ia : assert($rose(a));
    end
  
endmodule

    对该程序进行编译将出现以下错误：

    从错误中可以看出，$rose()函数是时钟敏感的。改正后的代码如下所示：

/*******************************************************
作者   :  CrazyBird
文件   :  rose_test.sv
日期   :  2015-5-6
功能   :  $rose()函数的验证
********************************************************/
`timescale 1ns/1ps
module rose_test(
    output reg        clk,
    output reg  [1:0] a
    );
    //  时钟的产生
    parameter PERIOD = 10;
  
    initial
    begin
        clk = 0;
        forever #(PERIOD/2)
        clk = ~clk;
    end
  
    //  激励的产生
    initial
    begin
        a = 0;
        repeat(20)@(negedge clk)
        begin
        a = {$random()}%2**2;
        end
        @(negedge clk);
        $stop;
    end
  
    //  序列的建立
    sequence s1;
        @(posedge clk) $rose(a);        //  受时钟边沿控制，正确
        //$rose(a);                     //  不受时钟控制，错误
    endsequence
    //  属性的建立
    property p1;
        s1;
    endproperty
    //  断言属性
    a_cc: assert property(p1);
  
endmodule

    对改正后的代码进行仿真，可得到如下的时序图：

    其中，红色光标所在处表示断言成功，而红色下三角表示断言失败。可以很容易分析到，断言成功的地方肯定是当前时刻信号的最低位是高电平，上一时刻信号的最低位是低电平。断言失败的地方信号的最低位要么当前时刻是低电平，上一时刻是高电平，要么当前时刻和上一时刻的电平没有发生变化，不管其他位是如何变化的。从而验证了内嵌函数$rose()只检测信号的最低位，而忽略其他位。

    对于内嵌函数$fell()和$stable()的验证与$rose()类似，同样可以验证“内嵌函数是工作在时钟边沿上的”和“内嵌函数只检测信号的最低位，而忽略其他位”这两个结论的正确性。下面只给出他们的仿真结果。

2、$fell()的验证

3、$stable()的验证

先介绍到这吧，待续~~