system-verilog-assertions - 数据复用器 SVA 比较

Question

我在为这种情况设计断言（SVA）时遇到了麻烦。当 mux sel 被置位时，data_in 预计会稳定 2 个时钟；mux sel 被断言之前的时钟，以及 mux sel 被断言时的当前时钟。

现在 data_in 是一个宽向量/总线信号，因此总线的某些位在功能模式期间是 Z 和 X（这是预期的），而这些位可能在非功能模式期间携带值。

这意味着，设计 SVA 的方法是在 mux sel 被断言时逐位比较数据总线。

这是我的方法，但 SVA 失败了，不知道为什么。

generate 
for( genvar i=1 ; i<BUS_WIDTH ; i++ ) begin  
    always @ (posedge clk) begin  
       if(!$isunknown(data_in[i]) && reset) begin  
           data_in_temp_prev[i]      <= data_in[i];  
           if (mux_sel==1 && reset==1 && i>0) begin  
             SVA_TEST: assert property (data_in[i] == data_in_temp_prev[i-1]) else `uvm_error("TRIAL_SVA",$sformatf("datain expected to be stable for 2 clks prior to mux sel"));  
            end //if  
        end //if isunknown  
        else begin  
            din0_temp_prev[i] <= 0;  
        end  
     end //always  
end // for genvar  
endgenerate  

有关如何设计此 SVA 的任何建议？

谢谢。

Answer 1

我对 SVA 检查器的方法是对属性使用标准结构来避免各种问题。该结构始终使用带有“禁用 iff”的时钟属性，并始终使用隐含运算符，其中左侧是触发器，右侧是我们要验证的内容。以下是 LRM 的一个示例：

property abc(a, b, c);
  disable iff (c) @(posedge clk) a |=> b;
endproperty

与上面的答案类似，我会这样做：

property mux_compare;
    disable iff(!reset)  @(posedge clk)
    mux_sel===1 |->  
    !$isunknown(data_in[i]) || $stable(data_in) && data_in[i] == $past(data_in[i],2);  
endproperty: mux_compare

Answer 2

如果我正确理解了您的问题，那么对于此类问题，您不需要所有这些结构，请查看下面的示例并告诉我是否有帮助。

property mux_compare;
    disable iff(!reset)
        @(posedge mux_sel)
            !$isunknown(data_in)
        |->
        @(posedge clk)
            $stable(data_in) [*2];
endproperty: mux_compare