在某些设计情况中,如果一些条件为真,则我们不想执行检验。换句话说,这就像是一个异步的复位,使得检验在当前时刻不工作。SVA提供了关键词“ disable iff来实现这种检验器的异步复位。“ disable iff”的基本语法如下。

disable iff (expression) <property definition>

        属性p34检查在有效开始后,信号“a”重复两次,且1个周期之后,信号“b”重复两次,再过一个时钟周期,信号“ start”为低。在整个序列过程中,如果“ reset”被检测为高,检验器会停止并默认地发出一个空成功的信号。

module disableiff;

logic clk, reset, start;
logic a,b,c;

initial $vcdpluson();

initial
begin
clk=1'b0; reset=1'b0; start = 1'b0;
repeat(2) @(posedge clk);
reset = 1'b1; a=1'b0; b=1'b0; c=1'b0;
repeat(2) @(posedge clk) reset = 1'b0; start = 1'b1; 

@(posedge clk) a=1'b1;
@(posedge clk) a=1'b0;
repeat(2) @(posedge clk);
@(posedge clk) a=1'b1;
@(posedge clk) a=1'b0;
repeat(2) @(posedge clk);
@(posedge clk) b=1'b1;
@(posedge clk) b=1'b0;
repeat(2) @(posedge clk);
@(posedge clk) b=1'b1;
@(posedge clk) b=1'b0;
repeat(1) @(posedge clk);
start = 1'b0;
repeat(2) @(posedge clk);start = 1'b1;

@(posedge clk) a=1'b1;
@(posedge clk) a=1'b0;
repeat(2) @(posedge clk);
@(posedge clk) a=1'b1;
@(posedge clk) a=1'b0;
repeat(2) @(posedge clk);
@(posedge clk) b=1'b1; reset = 1'b1;
@(posedge clk) b=1'b0;
repeat(2) @(posedge clk);
@(posedge clk) b=1'b1;
@(posedge clk) b=1'b0;
repeat(1) @(posedge clk);
start = 1'b0;
repeat(2) @(posedge clk);

$finish();
end

property p34;
	 @(posedge clk) disable iff (reset) $rose(start) |=> a[=2] ##1 b[=2] ##1 !start ;
endproperty

a34: assert property(p34);

initial forever clk = #25 ~clk;

endmodule

        图1-36显示了属性p34在模拟中的响应。标记1标出了一个有效的开始,在有效开始后,信号“a”重复为高两次,接着信号“b”重复为高两次,然后信号“ start”如期望的为低。
        在整个序列的过程中,信号“ reset”如期望的始终不被激活,因此检验在标记1e处成功。第二个有效开始由标记2s标出。在有效开始后,信号“a”重复为高两次,接着复位信号“reet”在信号“b”重复两次之前被激活。这使得检查失效,属性得到一个空成功。