16.15Disable iff用法

转自:https://blog.csdn.net/qq_43464337/article/details/121835094

16.15 Disable iff 解析

        默认disable iff可以在生成块或者module，interface，program声明中声明，其在默认disable iff声明的范围（作用域）和子范围（子作用域）中，为所有并发断言提供了一种默认禁用情况。默认禁用iff可以在生成块或模块、接口或程序声明中声明。此外，默认值扩展到任何嵌套的模块、接口或程序声明，以及嵌套的生成块。但是，如果嵌套模块、接口、程序声明或生成块本身有一个默认disable iff声明，则默认disable iff用嵌套声明或生成块应用，并从外部覆盖任何默认disable iff。使用作用域解析的disable iff声明中引用的任何信号，都将从声明的作用域解析。

        默认disable iff声明的作用，与声明在该范围内的位置无关，同一模块、接口、程序声明或生成块中多个默认disable iff声明应为错误，该作用域不会扩展到模块、接口、程序声明的任何实例。

        在下面这个例子中，模块m1将rst1声明为默认禁用条件，在嵌套模块m2中没有默认disable iff声明，默认禁用条件rst1适用于m1的整个声明和m2的嵌套声明，因此，断言a1和a2的推断禁用条件都是rst1。

1.  module m1;
2. bit clk, rst1;
3. default disable iff rst1;
4. a1: assert property (@(posedge clk) p1); // property p1 is
5. // defined elsewhere
6. ...
7. module m2;
8. bit rst2;
9. ...
10. a2: assert property (@(posedge clk) p2); // property p2 is
11. // defined elsewhere
12. endmodule
13. ...
14. endmodule

        在嵌套模块m2中有默认disable iff声明，则在m2中此默认禁用条件覆盖了在m1中声明的默认禁用条件。因此，下面这个例子a1的推断禁用条件是rst1，但a2的推断禁用条件是rst2。

1. module m1;
2. bit clk, rst1;
3. default disable iff rst1;
4. a1: assert property (@(posedge clk) p1); // property p1 is
5. // defined elsewhere
6. ...
7. module m2;
8. bit rst2;
9. default disable iff rst2;
10. ...
11. a2: assert property (@(posedge clk) p2); // property p2 is
12. // defined elsewhere
13. endmodule
14. ...
15. endmodule

       以下规则适用于禁用条件的解决方案：

（1）如果断言有一个disable iff分句，则应使用这个分句中指定的禁用条件，并忽略此断言的任何默认disable iff声明；

（2）如果断言不包含一个disable iff分句，但这个断言在默认disable iff声明的作用域中，则这个断言的禁用条件从默认disable iff声明推断出来；

（3）否则，不执行推断（这等价于禁用条件推断为0）。

        下面两个例子说明了这些规则的应用：

1. module examples_with_default (input logic a, b, clk, rst, rst1);
2. default disable iff rst;
3. property p1;
4. disable iff (rst1) a |=> b;
5. endproperty
6. // Disable condition is rst1 - explicitly specified within a1
7. a1 : assert property (@(posedge clk) disable iff (rst1) a |=> b);
8. // Disable condition is rst1 - explicitly specified within p1
9. a2 : assert property (@(posedge clk) p1);
10. // Disable condition is rst - no explicit specification, inferred from
11. // default disable iff declaration
12. a3 : assert property (@(posedge clk) a |=> b);
13. // Disable condition is 1'b0. This is the only way to
14. // cancel the effect of default disable.
15. a4 : assert property (@(posedge clk) disable iff (1'b0) a |=> b);
16. endmodule
17. module examples_without_default (input logic a, b, clk, rst);
18. property p2;
19. disable iff (rst) a |=> b;
20. endproperty
21. // Disable condition is rst - explicitly specified within a5
22. a5 : assert property (@(posedge clk) disable iff (rst) a |=> b);
23. // Disable condition is rst - explicitly specified within p2
24. a6 : assert property (@ (posedge clk) p2);
25. // No disable condition
26. a7 : assert property (@ (posedge clk) a |=> b);
27. endmodule