ranking function for i2c benchmarks

This adds a lexicographic ranking function for the i2c benchmarks.

Author: kroening

examples/Benchmarks/check_ranking

@@ -41,28 +41,26 @@ ebmc gray_9.sv --ranking-function "2**16-cnt"
 ebmc gray_10.sv --ranking-function "2**17-cnt"
 ebmc gray_11.sv --ranking-function "2**18-cnt"
 
-if false ; then
-ebmc i2c_1.sv --ranking-function "2**9-cnt"
-ebmc i2c_2.sv --ranking-function "2**10-cnt"
-ebmc i2c_3.sv --ranking-function "2**11-cnt"
-ebmc i2c_4.sv --ranking-function "2**12-cnt"
-ebmc i2c_5.sv --ranking-function "2**13-cnt"
-ebmc i2c_6.sv --ranking-function "2**14-cnt"
-ebmc i2c_7.sv --ranking-function "2**15-cnt"
-ebmc i2c_8.sv --ranking-function "2**16-cnt"
-ebmc i2c_9.sv --ranking-function "2**17-cnt"
-ebmc i2c_10.sv --ranking-function "2**18-cnt"
-ebmc i2c_11.sv --ranking-function "2**19-cnt"
-ebmc i2c_12.sv --ranking-function "2**10-cnt"
-ebmc i2c_13.sv --ranking-function "2**10-cnt"
-ebmc i2c_14.sv --ranking-function "2**10-cnt"
-ebmc i2c_15.sv --ranking-function "2**10-cnt"
-ebmc i2c_16.sv --ranking-function "2**10-cnt"
-ebmc i2c_17.sv --ranking-function "2**10-cnt"
-ebmc i2c_18.sv --ranking-function "2**10-cnt"
-ebmc i2c_19.sv --ranking-function "2**10-cnt"
-ebmc i2c_20.sv --ranking-function "2**19-cnt"
-fi
+ebmc i2c_1.sv --ranking-function "{cnt>=divider*4 ? 3 : scl_clk==0 && cnt>=3*divider-1 ? 2 : scl_clk ? 1 : 0, divider*4-cnt}"
+ebmc i2c_2.sv --ranking-function "{cnt>=divider*4 ? 3 : scl_clk==0 && cnt>=3*divider-1 ? 2 : scl_clk ? 1 : 0, divider*4-cnt}"
+ebmc i2c_3.sv --ranking-function "{cnt>=divider*4 ? 3 : scl_clk==0 && cnt>=3*divider-1 ? 2 : scl_clk ? 1 : 0, divider*4-cnt}"
+ebmc i2c_4.sv --ranking-function "{cnt>=divider*4 ? 3 : scl_clk==0 && cnt>=3*divider-1 ? 2 : scl_clk ? 1 : 0, divider*4-cnt}"
+ebmc i2c_5.sv --ranking-function "{cnt>=divider*4 ? 3 : scl_clk==0 && cnt>=3*divider-1 ? 2 : scl_clk ? 1 : 0, divider*4-cnt}"
+ebmc i2c_6.sv --ranking-function "{cnt>=divider*4 ? 3 : scl_clk==0 && cnt>=3*divider-1 ? 2 : scl_clk ? 1 : 0, divider*4-cnt}"
+ebmc i2c_7.sv --ranking-function "{cnt>=divider*4 ? 3 : scl_clk==0 && cnt>=3*divider-1 ? 2 : scl_clk ? 1 : 0, divider*4-cnt}"
+ebmc i2c_8.sv --ranking-function "{cnt>=divider*4 ? 3 : scl_clk==0 && cnt>=3*divider-1 ? 2 : scl_clk ? 1 : 0, divider*4-cnt}"
+ebmc i2c_9.sv --ranking-function "{cnt>=divider*4 ? 3 : scl_clk==0 && cnt>=3*divider-1 ? 2 : scl_clk ? 1 : 0, divider*4-cnt}"
+ebmc i2c_10.sv --ranking-function "{cnt>=divider*4 ? 3 : scl_clk==0 && cnt>=3*divider-1 ? 2 : scl_clk ? 1 : 0, divider*4-cnt}"
+ebmc i2c_11.sv --ranking-function "{cnt>=divider*4 ? 3 : scl_clk==0 && cnt>=3*divider-1 ? 2 : scl_clk ? 1 : 0, divider*4-cnt}"
+ebmc i2c_12.sv --ranking-function "{cnt>=divider*4 ? 3 : scl_clk==0 && cnt>=3*divider-1 ? 2 : scl_clk ? 1 : 0, divider*4-cnt}"
+ebmc i2c_13.sv --ranking-function "{cnt>=divider*4 ? 3 : scl_clk==0 && cnt>=3*divider-1 ? 2 : scl_clk ? 1 : 0, divider*4-cnt}"
+ebmc i2c_14.sv --ranking-function "{cnt>=divider*4 ? 3 : scl_clk==0 && cnt>=3*divider-1 ? 2 : scl_clk ? 1 : 0, divider*4-cnt}"
+ebmc i2c_15.sv --ranking-function "{cnt>=divider*4 ? 3 : scl_clk==0 && cnt>=3*divider-1 ? 2 : scl_clk ? 1 : 0, divider*4-cnt}"
+ebmc i2c_16.sv --ranking-function "{cnt>=divider*4 ? 3 : scl_clk==0 && cnt>=3*divider-1 ? 2 : scl_clk ? 1 : 0, divider*4-cnt}"
+ebmc i2c_17.sv --ranking-function "{cnt>=divider*4 ? 3 : scl_clk==0 && cnt>=3*divider-1 ? 2 : scl_clk ? 1 : 0, divider*4-cnt}"
+ebmc i2c_18.sv --ranking-function "{cnt>=divider*4 ? 3 : scl_clk==0 && cnt>=3*divider-1 ? 2 : scl_clk ? 1 : 0, divider*4-cnt}"
+ebmc i2c_19.sv --ranking-function "{cnt>=divider*4 ? 3 : scl_clk==0 && cnt>=3*divider-1 ? 2 : scl_clk ? 1 : 0, divider*4-cnt}"
+ebmc i2c_20.sv --ranking-function "{cnt>=divider*4 ? 3 : scl_clk==0 && cnt>=3*divider-1 ? 2 : scl_clk ? 1 : 0, divider*4-cnt}"
 
 ebmc lcd_1.sv --ranking-function "{3-state,500-cnt}"
 ebmc lcd_2.sv --ranking-function "{3-state,1000-cnt}"

examples/Benchmarks/i2c_1.sv

@@ -37,4 +37,14 @@ module i2cStrech #(localparam divider = 125, localparam CBITS = 9) (input clk, i
 	p1: assert property (@(posedge clk) s_eventually rst == 1 || scl_not_ena == 1 || stretch == 1);
 	//F G (rst = F & scl_not_ena = F) -> G F (stretch = T)
 
+wire [8:0] rank1 =
+  cnt>=divider*4 ? 3 :  // 500
+  !scl_clk && cnt>=3*divider-1 ? 2 :
+  scl_clk        ? 1 :
+                   0 ;
+
+wire [8:0] rank2 = 500 - cnt;
+
+wire [31:0] rank = {rank1, rank2};
+
 endmodule