Simplfy benchmark properties

1) This removes the redundant SVA always operator.

2) This adds a script for checking a ranking function on the benchmarks.

Author: kroening

examples/Benchmarks/check_ranking

@@ -0,0 +1,137 @@
+#!/bin/sh
+
+set -e
+
+ebmc PWM_1.sv --ranking-function "2**10-cntR"
+ebmc PWM_2.sv --ranking-function "2**11-cntR"
+ebmc PWM_3.sv --ranking-function "2**12-cntR"
+ebmc PWM_4.sv --ranking-function "2**13-cntR"
+ebmc PWM_5.sv --ranking-function "2**14-cntR"
+ebmc PWM_6.sv --ranking-function "2**15-cntR"
+ebmc PWM_7.sv --ranking-function "2**16-cntR"
+ebmc PWM_8.sv --ranking-function "2**17-cntR"
+ebmc PWM_9.sv --ranking-function "2**18-cntR"
+
+ebmc delay_1.sv --ranking-function "750-cnt"
+ebmc delay_2.sv --ranking-function "1250-cnt"
+ebmc delay_3.sv --ranking-function "2500-cnt"
+ebmc delay_4.sv --ranking-function "5000-cnt"
+ebmc delay_5.sv --ranking-function "7500-cnt"
+ebmc delay_6.sv --ranking-function "10000-cnt"
+ebmc delay_7.sv --ranking-function "12500-cnt"
+ebmc delay_8.sv --ranking-function "15000-cnt"
+ebmc delay_9.sv --ranking-function "17500-cnt"
+ebmc delay_10.sv --ranking-function "20000-cnt"
+ebmc delay_11.sv --ranking-function "22500-cnt"
+ebmc delay_12.sv --ranking-function "25000-cnt"
+ebmc delay_13.sv --ranking-function "50000-cnt"
+ebmc delay_14.sv --ranking-function "100000-cnt"
+ebmc delay_15.sv --ranking-function "200000-cnt"
+ebmc delay_16.sv --ranking-function "400000-cnt"
+
+ebmc gray_1.sv --ranking-function "2**8-cnt"
+ebmc gray_2.sv --ranking-function "2**9-cnt"
+ebmc gray_3.sv --ranking-function "2**10-cnt"
+ebmc gray_4.sv --ranking-function "2**11-cnt"
+ebmc gray_5.sv --ranking-function "2**12-cnt"
+ebmc gray_6.sv --ranking-function "2**13-cnt"
+ebmc gray_7.sv --ranking-function "2**14-cnt"
+ebmc gray_8.sv --ranking-function "2**15-cnt"
+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 lcd_1.sv --ranking-function "{3-state,500-cnt}"
+ebmc lcd_2.sv --ranking-function "{3-state,1000-cnt}"
+ebmc lcd_3.sv --ranking-function "{3-state,1500-cnt}"
+ebmc lcd_4.sv --ranking-function "{3-state,2500-cnt}"
+ebmc lcd_5.sv --ranking-function "{3-state,5000-cnt}"
+ebmc lcd_6.sv --ranking-function "{3-state,7500-cnt}"
+ebmc lcd_7.sv --ranking-function "{3-state,10000-cnt}"
+ebmc lcd_8.sv --ranking-function "{3-state,12500-cnt}"
+ebmc lcd_9.sv --ranking-function "{3-state,15000-cnt}"
+ebmc lcd_10.sv --ranking-function "{3-state,17500-cnt}"
+ebmc lcd_11.sv --ranking-function "{3-state,20000-cnt}"
+ebmc lcd_12.sv --ranking-function "{3-state,22500-cnt}"
+ebmc lcd_13.sv --ranking-function "{3-state,90000-cnt}"
+ebmc lcd_14.sv --ranking-function "{3-state,180000-cnt}"
+
+ebmc seven_seg_1.sv --ranking-function "250-cnt" --property SEVEN.property.p1
+ebmc seven_seg_2.sv --ranking-function "500-cnt" --property SEVEN.property.p1
+ebmc seven_seg_3.sv --ranking-function "750-cnt" --property SEVEN.property.p1
+ebmc seven_seg_4.sv --ranking-function "1000-cnt" --property SEVEN.property.p1
+ebmc seven_seg_5.sv --ranking-function "2500-cnt" --property SEVEN.property.p1
+ebmc seven_seg_6.sv --ranking-function "5000-cnt" --property SEVEN.property.p1
+ebmc seven_seg_7.sv --ranking-function "7500-cnt" --property SEVEN.property.p1
+ebmc seven_seg_8.sv --ranking-function "10000-cnt" --property SEVEN.property.p1
+ebmc seven_seg_9.sv --ranking-function "12500-cnt" --property SEVEN.property.p1
+ebmc seven_seg_10.sv --ranking-function "15000-cnt" --property SEVEN.property.p1
+ebmc seven_seg_11.sv --ranking-function "17500-cnt" --property SEVEN.property.p1
+ebmc seven_seg_12.sv --ranking-function "20000-cnt" --property SEVEN.property.p1
+ebmc seven_seg_16.sv --ranking-function "40000-cnt" --property SEVEN.property.p1
+ebmc seven_seg_17.sv --ranking-function "80000-cnt" --property SEVEN.property.p1
+ebmc seven_seg_18.sv --ranking-function "160000-cnt" --property SEVEN.property.p1
+
+ebmc thermocouple_1.sv --ranking-function "{2-state,2**5-cnt}"
+ebmc thermocouple_2.sv --ranking-function "{2-state,2**9-cnt}"
+ebmc thermocouple_3.sv --ranking-function "{2-state,2**10-cnt}"
+ebmc thermocouple_4.sv --ranking-function "{2-state,2**10-cnt}"
+ebmc thermocouple_5.sv --ranking-function "{2-state,2**11-cnt}"
+ebmc thermocouple_6.sv --ranking-function "{2-state,2**11-cnt}"
+ebmc thermocouple_7.sv --ranking-function "{2-state,2**12-cnt}"
+ebmc thermocouple_8.sv --ranking-function "{2-state,2**12-cnt}"
+ebmc thermocouple_9.sv --ranking-function "{2-state,2**13-cnt}"
+ebmc thermocouple_10.sv --ranking-function "{2-state,2**14-cnt}"
+ebmc thermocouple_11.sv --ranking-function "{2-state,2**14-cnt}"
+ebmc thermocouple_12.sv --ranking-function "{2-state,2**14-cnt}"
+ebmc thermocouple_13.sv --ranking-function "{2-state,2**15-cnt}"
+ebmc thermocouple_14.sv --ranking-function "{2-state,2**16-cnt}"
+ebmc thermocouple_15.sv --ranking-function "{2-state,2**17-cnt}"
+ebmc thermocouple_16.sv --ranking-function "{2-state,2**18-cnt}"
+ebmc thermocouple_17.sv --ranking-function "{2-state,2**19-cnt}"
+
+ebmc uart_transmit_1.sv --ranking-function "2**3-tx_cnt"
+ebmc uart_transmit_2.sv --ranking-function "2**4-tx_cnt"
+ebmc uart_transmit_3.sv --ranking-function "2**4-tx_cnt"
+ebmc uart_transmit_4.sv --ranking-function "2**4-tx_cnt"
+ebmc uart_transmit_5.sv --ranking-function "2**4-tx_cnt"
+ebmc uart_transmit_6.sv --ranking-function "2**4-tx_cnt"
+ebmc uart_transmit_7.sv --ranking-function "2**4-tx_cnt"
+ebmc uart_transmit_8.sv --ranking-function "2**4-tx_cnt"
+ebmc uart_transmit_9.sv --ranking-function "2**5-tx_cnt"
+ebmc uart_transmit_10.sv --ranking-function "2**5-tx_cnt"
+ebmc uart_transmit_11.sv --ranking-function "2**5-tx_cnt"
+ebmc uart_transmit_12.sv --ranking-function "2**6-tx_cnt"
+
+ebmc vga_1.sv --ranking-function "{2**5-v_cnt,2**7-h_cnt}"
+ebmc vga_2.sv --ranking-function "{2**6-v_cnt,2**8-h_cnt}"
+ebmc vga_3.sv --ranking-function "{2**6-v_cnt,2**8-h_cnt}"
+ebmc vga_4.sv --ranking-function "{2**7-v_cnt,2**9-h_cnt}"
+ebmc vga_5.sv --ranking-function "{2**8-v_cnt,2**9-h_cnt}"
+ebmc vga_6.sv --ranking-function "{2**8-v_cnt,2**9-h_cnt}"
+ebmc vga_7.sv --ranking-function "{2**8-v_cnt,2**10-h_cnt}"
+ebmc vga_8.sv --ranking-function "{2**9-v_cnt,2**10-h_cnt}"
+ebmc vga_9.sv --ranking-function "{2**9-v_cnt,2**11-h_cnt}"

examples/Benchmarks/delay_1.sv

@@ -7,6 +7,6 @@ module DELAY #(localparam N = 750, localparam CBITS = 10) (input clk, input rst,
       cnt = 0; end
     else sig = 0;
   end
-  p1: assert property  (@(posedge clk) ((always s_eventually rst == 1) or (always s_eventually sig == 1))) ;
+  p1: assert property (@(posedge clk) s_eventually rst || sig == 1) ;
   // F G (rst = F) -> G F (sig = T)
 endmodule

examples/Benchmarks/delay_10.sv

@@ -7,6 +7,6 @@ module DELAY #(localparam N = 20000, localparam CBITS = 15) (input clk, input rs
       cnt = 0; end
     else sig = 0;
   end
-  p1: assert property  (@(posedge clk) ((always s_eventually rst == 1) or (always s_eventually sig == 1))) ;
+  p1: assert property (@(posedge clk) s_eventually rst || sig == 1);
   // F G (rst = F) -> G F (sig = T)
 endmodule

examples/Benchmarks/delay_11.sv

@@ -7,6 +7,6 @@ module DELAY #(localparam N = 22500, localparam CBITS = 15) (input clk, input rs
       cnt = 0; end
     else sig = 0;
   end
-  p1: assert property  (@(posedge clk) ((always s_eventually rst == 1) or (always s_eventually sig == 1))) ;
+  p1: assert property (@(posedge clk) s_eventually rst || sig == 1);
   // F G (rst = F) -> G F (sig = T)
 endmodule

examples/Benchmarks/delay_12.sv

@@ -7,6 +7,6 @@ module DELAY #(localparam N = 25000, localparam CBITS = 15) (input clk, input rs
       cnt = 0; end
     else sig = 0;
   end
-  p1: assert property  (@(posedge clk) ((always s_eventually rst == 1) or (always s_eventually sig == 1))) ;
+  p1: assert property (@(posedge clk) s_eventually rst || sig == 1);
   // F G (rst = F) -> G F (sig = T)
 endmodule

examples/Benchmarks/delay_13.sv

@@ -7,6 +7,6 @@ module DELAY #(localparam N = 50000, localparam CBITS = 16) (input clk, input rs
       cnt = 0; end
     else sig = 0;
   end
-  p1: assert property  (@(posedge clk) ((always s_eventually rst == 1) or (always s_eventually sig == 1))) ;
+  p1: assert property (@(posedge clk) s_eventually rst || sig == 1);
   // F G (rst = F) -> G F (sig = T)
 endmodule

examples/Benchmarks/delay_14.sv

@@ -7,6 +7,6 @@ module DELAY #(localparam N = 100000, localparam CBITS = 17) (input clk, input r
       cnt = 0; end
     else sig = 0;
   end
-  p1: assert property  (@(posedge clk) ((always s_eventually rst == 1) or (always s_eventually sig == 1))) ;
+  p1: assert property (@(posedge clk) s_eventually rst || sig == 1);
   // F G (rst = F) -> G F (sig = T)
 endmodule

examples/Benchmarks/delay_15.sv

@@ -7,6 +7,6 @@ module DELAY #(localparam N = 200000, localparam CBITS = 18) (input clk, input r
       cnt = 0; end
     else sig = 0;
   end
-  p1: assert property  (@(posedge clk) ((always s_eventually rst == 1) or (always s_eventually sig == 1))) ;
+  p1: assert property (@(posedge clk) s_eventually rst || sig == 1);
   // F G (rst = F) -> G F (sig = T)
 endmodule

examples/Benchmarks/delay_16.sv

@@ -7,6 +7,6 @@ module DELAY #(localparam N = 400000, localparam CBITS = 19) (input clk, input r
       cnt = 0; end
     else sig = 0;
   end
-  p1: assert property  (@(posedge clk) ((always s_eventually rst == 1) or (always s_eventually sig == 1))) ;
+  p1: assert property (@(posedge clk) s_eventually rst || sig == 1);
   // F G (rst = F) -> G F (sig = T)
 endmodule

examples/Benchmarks/delay_2.sv

@@ -7,6 +7,6 @@ module DELAY #(localparam N = 1250, localparam CBITS = 11) (input clk, input rst
       cnt = 0; end
     else sig = 0;
   end
-  p1: assert property  (@(posedge clk) ((always s_eventually rst == 1) or (always s_eventually sig == 1))) ;
+  p1: assert property (@(posedge clk) s_eventually rst || sig == 1);
   // F G (rst = F) -> G F (sig = T)
 endmodule