1.20“ $past”构造

        SVA提供了一个内嵌的系统任务“$past”,它可以得到信号在几个时钟周期之前的值。在默认情况下,它提供信号在前一个时钟周期的值。结构的基本语法如下

$past (signal_name ,number of clock cycles)

        这个任务能够有效地验证设计到达当前时钟周期的状态所采用的通路是正确的。属性p19检验的是在给定的时钟上升沿,如果表达式(c&&d)为真,那么两个周期前,表达式(a&&b)为真。

property p19;
	@(posedge clk) (c && d) |-> ($past ((a  && b),2)==1'b1);
endproperty

a19: assert property(p19);

        图1-22显示了属性p19在模拟中的响应。表1-12总结了断言a19的状态和相关信号的采样值。断言在时钟周期1失败。在时钟周期1,信号“c”和信号“d”都为高,断言有一个有效的开始。于是检验器的后续算子需要比较两个周期前的表达式(a&&b)的值。但是由于不可能得到两个信号在时钟周期1之前两个周期的历史,信号的值被当作“x”,因此检验器在时钟周期1失败。

        检验在时钟周期5有一个真正的成功。在时钟周期5,由于信号“a”和信号“b”都为高,断言有一个成功的开始。后续算子检查在时钟周期3时表达式(a&&b)是否为真。正如期望的那样,在时钟周期3,信号“a”和信号“b”都被检测为高,因此检验成功。
        检验在时钟周期16失败。在时钟周期16,由于信号“a”和信号“b”都为高,断言也有一个成功的开始。后续算子检查在时钟周期3时表达式(a&&b)是否为真。信号“a”如期望的那样为高，但是信号“b”为低。这使得表达式(a&&b)为假,检验失败。


带时钟门控的$past构造

        $past构造可以由一个门控信号 (gating singal)控制。比如,在个给定的时钟沿,只有当门控信号的值为真时才检查后续算子的状况。使用门控信号的$past构造的基本语法如下

$past (signal_name, number of clock cycles ,gating signal);

        属性p20与属性p19相似。但是只有当门控信号“e”在任意给定的时钟上升沿有效时检验才被激活。

property p20;
	@(posedge clk) (c && d) |-> ($past ((a && b ),2,e)==1'b1);
endproperty

a20: assert property(p20);