Merge pull request #1146 from diffblue/i2c_SVA

fixup i2c_*.sv SVA

Author: tautschnig

examples/Benchmarks/i2c_11.sv

@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 4500, localparam CBITS = 15) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	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)
 endmodule

examples/Benchmarks/i2c_12.sv

@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 5000, localparam CBITS = 15) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	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)
 endmodule

examples/Benchmarks/i2c_13.sv

@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 5500, localparam CBITS = 15) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	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)
 endmodule

examples/Benchmarks/i2c_14.sv

@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 6000, localparam CBITS = 15) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	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)
 endmodule

examples/Benchmarks/i2c_15.sv

@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 6500, localparam CBITS = 15) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	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)
 endmodule

examples/Benchmarks/i2c_16.sv

@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 7000, localparam CBITS = 15) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	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)
 endmodule

examples/Benchmarks/i2c_17.sv

@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 10000, localparam CBITS = 16) (input clk
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	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)
 endmodule

examples/Benchmarks/i2c_18.sv

@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 17500, localparam CBITS = 17) (input clk
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	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)
 endmodule

examples/Benchmarks/i2c_19.sv

@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 35000, localparam CBITS = 18) (input clk
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	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)
 endmodule

examples/Benchmarks/i2c_20.sv

@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 70000, localparam CBITS = 19) (input clk
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	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)
 endmodule

examples/Benchmarks/i2c_3.sv

@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 500, localparam CBITS = 11) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	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)
 endmodule

examples/Benchmarks/i2c_4.sv

@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 1000, localparam CBITS = 12) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	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)
 endmodule

examples/Benchmarks/i2c_5.sv

@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 1500, localparam CBITS = 13) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	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)
 endmodule

examples/Benchmarks/i2c_6.sv

@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 2000, localparam CBITS = 13) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	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)
 endmodule

examples/Benchmarks/i2c_7.sv

@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 2500, localparam CBITS = 14) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	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)
 endmodule

examples/Benchmarks/i2c_8.sv

@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 3000, localparam CBITS = 14) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	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)
 endmodule

examples/Benchmarks/i2c_9.sv

@@ -33,6 +33,6 @@ module i2cStrech #(localparam divider = 3500, localparam CBITS = 14) (input clk,
 			data_clk = 0;
 		end
 	end
-	p1: assert property  (@(posedge clk) ((always s_eventually (rst == 1 or scl_not_ena == 1)) or (always s_eventually stretch == 1))) ;
+	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)
 endmodule