SystemVerilog Assertions应用指南 Chapter1.33 在蕴含中使用 if/else

指南 Chapter1.33 在蕴含中使用 if/else"/>

SystemVerilog Assertions应用指南 Chapter1.33 在蕴含中使用 if/else

        SVA允许在使用蕴含的属性的后续算子中使用“if/else”语句。
        属性 p_if_else检査如果信号“ start”的下降沿被检测到,就是个有效开始,接着一个时钟周期后,信号“a”或者信号“b”为高。在现行算子成功匹配时,后续算子有两个可能的路径。
        1.如果信号“a”为高,那么信号“c”必须间歇地重复两次为高,且在下一个时钟周期,信号“e”必须为高。
        2.如果信号“a”不为高,那么信号“d”必须间歇地重复两次为高,且在下一个时钟周期,信号“f”必须为高。注意,在检验信号“a”的后续算子中有优先级。

property p_if_else;@(posedge clk)($fell(start) ##1 (a || b))  |->if(a)(c[->2] ##1 e)else (d[->2] ##1 f)
endpropertya_if_else : assert property (p_if_else);

        如果不用“ if/else”构造来重写这个属性,需要用三个单独的属性来实现。由于“ if/else”有优先级,两个信号导致了如下所示的三种不同的可能结果。

        可以发现,如果信号“a”和“b”都为高,那么会执行信号“a”的“if”块,因为它的优先级高。重写的三个属性如下所示。

property p_if_else_leaf1;@(posedge clk)($fell(start) #31 a) |-> (c[->2] ##1 e);
endpropertya_if_else_leaf1:assert property(p_if_else_leaf1);property p_if_else_leaf2;@(posedge clk)($fell(start) ##1 ) |-> (d[->2] ##1 f);
endpropertya_if_else_leaf2:assert property(p_if_else_leaf2);a_if_else_leaf2 :asser property(p_if_else_leaf2);property p_if_else_leaf3;@(posedge clk)($fell(start) ##1 (a && b) |-> (c[->2] ##1 e));
endpropertya_if_else_leaf3:asser property(p_if_else_leaf3);