NeurIPS 2025 SystemVerilog benchmarks

Author: kroening

examples/NeurIPS2025/Liveness/PWM_1-l1.sv

@@ -0,0 +1,35 @@
+module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red, output reg lb_pulse, output reg ub_pulse);
+
+  localparam CBITS = 10;    // Change pulse_wideR accordingly
+  
+  wire [CBITS-1:0] pulse_wideR;
+  assign pulse_wideR = {1'b0, sw[3:1], 1'b1, 5'd0};     // (CBTIS-5)
+  assign lbR = {1'b0, 4'b0000, 1'b1, 5'd0};
+  assign ubR = {1'b0, 4'b1111, 1'b1, 5'd0};
+
+  reg [CBITS-1:0] cnt_R;
+
+  always @(posedge clk) begin
+    cnt_R <= cnt_R + 1;
+    
+    if (cnt_R < pulse_wideR)
+      pulse_red = 1;
+    else
+      pulse_red = 0;
+
+    if (cnt_R < lbR)
+      lb_pulse = 1;
+    else
+      lb_pulse = 0;
+    
+    if (cnt_R < ubR)
+      ub_pulse = 1;
+    else
+      ub_pulse = 0;
+  end
+
+
+  // LTLSPEC G F Verilog.PWM_TOP.pulse_red = FALSE
+  assert property (@(posedge clk) always s_eventually pulse_red == 0);
+
+endmodule

examples/NeurIPS2025/Liveness/PWM_10-l1.sv

@@ -0,0 +1,35 @@
+module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red, output reg lb_pulse, output reg ub_pulse);
+
+  localparam CBITS = 19;    // Change pulse_wideR accordingly
+  
+  wire [CBITS-1:0] pulse_wideR;
+  assign pulse_wideR = {1'b0, sw[3:1], 1'b1, 14'd0};     // (CBTIS-5)
+  assign lbR = {1'b0, 4'b0000, 1'b1, 14'd0};
+  assign ubR = {1'b0, 4'b1111, 1'b1, 14'd0};
+
+  reg [CBITS-1:0] cnt_R;
+
+  always @(posedge clk) begin
+    cnt_R <= cnt_R + 1;
+    
+    if (cnt_R < pulse_wideR)
+      pulse_red = 1;
+    else
+      pulse_red = 0;
+
+    if (cnt_R < lbR)
+      lb_pulse = 1;
+    else
+      lb_pulse = 0;
+    
+    if (cnt_R < ubR)
+      ub_pulse = 1;
+    else
+      ub_pulse = 0;
+  end
+
+
+  // LTLSPEC G F Verilog.PWM_TOP.pulse_red = FALSE
+  assert property (@(posedge clk) always s_eventually pulse_red == 0);
+
+endmodule

examples/NeurIPS2025/Liveness/PWM_11-l1.sv

@@ -0,0 +1,35 @@
+module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red, output reg lb_pulse, output reg ub_pulse);
+
+  localparam CBITS = 20;    // Change pulse_wideR accordingly
+  
+  wire [CBITS-1:0] pulse_wideR;
+  assign pulse_wideR = {1'b0, sw[3:1], 1'b1, 15'd0};     // (CBTIS-5)
+  assign lbR = {1'b0, 4'b0000, 1'b1, 15'd0};
+  assign ubR = {1'b0, 4'b1111, 1'b1, 15'd0};
+
+  reg [CBITS-1:0] cnt_R;
+
+  always @(posedge clk) begin
+    cnt_R <= cnt_R + 1;
+    
+    if (cnt_R < pulse_wideR)
+      pulse_red = 1;
+    else
+      pulse_red = 0;
+
+    if (cnt_R < lbR)
+      lb_pulse = 1;
+    else
+      lb_pulse = 0;
+    
+    if (cnt_R < ubR)
+      ub_pulse = 1;
+    else
+      ub_pulse = 0;
+  end
+
+
+  // LTLSPEC G F Verilog.PWM_TOP.pulse_red = FALSE
+  assert property (@(posedge clk) always s_eventually pulse_red == 0);
+
+endmodule

examples/NeurIPS2025/Liveness/PWM_12-l1.sv

@@ -0,0 +1,35 @@
+module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red, output reg lb_pulse, output reg ub_pulse);
+
+  localparam CBITS = 21;    // Change pulse_wideR accordingly
+  
+  wire [CBITS-1:0] pulse_wideR;
+  assign pulse_wideR = {1'b0, sw[3:1], 1'b1, 16'd0};     // (CBTIS-5)
+  assign lbR = {1'b0, 4'b0000, 1'b1, 16'd0};
+  assign ubR = {1'b0, 4'b1111, 1'b1, 16'd0};
+
+  reg [CBITS-1:0] cnt_R;
+
+  always @(posedge clk) begin
+    cnt_R <= cnt_R + 1;
+    
+    if (cnt_R < pulse_wideR)
+      pulse_red = 1;
+    else
+      pulse_red = 0;
+
+    if (cnt_R < lbR)
+      lb_pulse = 1;
+    else
+      lb_pulse = 0;
+    
+    if (cnt_R < ubR)
+      ub_pulse = 1;
+    else
+      ub_pulse = 0;
+  end
+
+
+  // LTLSPEC G F Verilog.PWM_TOP.pulse_red = FALSE
+  assert property (@(posedge clk) always s_eventually pulse_red == 0);
+
+endmodule

examples/NeurIPS2025/Liveness/PWM_2-l1.sv

@@ -0,0 +1,35 @@
+module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red, output reg lb_pulse, output reg ub_pulse);
+
+  localparam CBITS = 11;    // Change pulse_wideR accordingly
+  
+  wire [CBITS-1:0] pulse_wideR;
+  assign pulse_wideR = {1'b0, sw[3:1], 1'b1, 6'd0};     // (CBTIS-5)
+  assign lbR = {1'b0, 4'b0000, 1'b1, 6'd0};
+  assign ubR = {1'b0, 4'b1111, 1'b1, 6'd0};
+
+  reg [CBITS-1:0] cnt_R;
+
+  always @(posedge clk) begin
+    cnt_R <= cnt_R + 1;
+    
+    if (cnt_R < pulse_wideR)
+      pulse_red = 1;
+    else
+      pulse_red = 0;
+
+    if (cnt_R < lbR)
+      lb_pulse = 1;
+    else
+      lb_pulse = 0;
+    
+    if (cnt_R < ubR)
+      ub_pulse = 1;
+    else
+      ub_pulse = 0;
+  end
+
+
+  // LTLSPEC G F Verilog.PWM_TOP.pulse_red = FALSE
+  assert property (@(posedge clk) always s_eventually pulse_red == 0);
+
+endmodule

examples/NeurIPS2025/Liveness/PWM_3-l1.sv

@@ -0,0 +1,35 @@
+module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red, output reg lb_pulse, output reg ub_pulse);
+
+  localparam CBITS = 12;    // Change pulse_wideR accordingly
+  
+  wire [CBITS-1:0] pulse_wideR;
+  assign pulse_wideR = {1'b0, sw[3:1], 1'b1, 7'd0};     // (CBTIS-5)
+  assign lbR = {1'b0, 4'b0000, 1'b1, 7'd0};
+  assign ubR = {1'b0, 4'b1111, 1'b1, 7'd0};
+
+  reg [CBITS-1:0] cnt_R;
+
+  always @(posedge clk) begin
+    cnt_R <= cnt_R + 1;
+    
+    if (cnt_R < pulse_wideR)
+      pulse_red = 1;
+    else
+      pulse_red = 0;
+
+    if (cnt_R < lbR)
+      lb_pulse = 1;
+    else
+      lb_pulse = 0;
+    
+    if (cnt_R < ubR)
+      ub_pulse = 1;
+    else
+      ub_pulse = 0;
+  end
+
+
+  // LTLSPEC G F Verilog.PWM_TOP.pulse_red = FALSE
+  assert property (@(posedge clk) always s_eventually pulse_red == 0);
+
+endmodule

examples/NeurIPS2025/Liveness/PWM_4-l1.sv

@@ -0,0 +1,35 @@
+module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red, output reg lb_pulse, output reg ub_pulse);
+
+  localparam CBITS = 13;    // Change pulse_wideR accordingly
+  
+  wire [CBITS-1:0] pulse_wideR;
+  assign pulse_wideR = {1'b0, sw[3:1], 1'b1, 8'd0};     // (CBTIS-5)
+  assign lbR = {1'b0, 4'b0000, 1'b1, 8'd0};
+  assign ubR = {1'b0, 4'b1111, 1'b1, 8'd0};
+
+  reg [CBITS-1:0] cnt_R;
+
+  always @(posedge clk) begin
+    cnt_R <= cnt_R + 1;
+    
+    if (cnt_R < pulse_wideR)
+      pulse_red = 1;
+    else
+      pulse_red = 0;
+
+    if (cnt_R < lbR)
+      lb_pulse = 1;
+    else
+      lb_pulse = 0;
+    
+    if (cnt_R < ubR)
+      ub_pulse = 1;
+    else
+      ub_pulse = 0;
+  end
+
+
+  // LTLSPEC G F Verilog.PWM_TOP.pulse_red = FALSE
+  assert property (@(posedge clk) always s_eventually pulse_red == 0);
+
+endmodule

examples/NeurIPS2025/Liveness/PWM_5-l1.sv

@@ -0,0 +1,35 @@
+module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red, output reg lb_pulse, output reg ub_pulse);
+
+  localparam CBITS = 14;    // Change pulse_wideR accordingly
+  
+  wire [CBITS-1:0] pulse_wideR;
+  assign pulse_wideR = {1'b0, sw[3:1], 1'b1, 9'd0};     // (CBTIS-5)
+  assign lbR = {1'b0, 4'b0000, 1'b1, 9'd0};
+  assign ubR = {1'b0, 4'b1111, 1'b1, 9'd0};
+
+  reg [CBITS-1:0] cnt_R;
+
+  always @(posedge clk) begin
+    cnt_R <= cnt_R + 1;
+    
+    if (cnt_R < pulse_wideR)
+      pulse_red = 1;
+    else
+      pulse_red = 0;
+
+    if (cnt_R < lbR)
+      lb_pulse = 1;
+    else
+      lb_pulse = 0;
+    
+    if (cnt_R < ubR)
+      ub_pulse = 1;
+    else
+      ub_pulse = 0;
+  end
+
+
+  // LTLSPEC G F Verilog.PWM_TOP.pulse_red = FALSE
+  assert property (@(posedge clk) always s_eventually pulse_red == 0);
+
+endmodule

examples/NeurIPS2025/Liveness/PWM_6-l1.sv

@@ -0,0 +1,35 @@
+module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red, output reg lb_pulse, output reg ub_pulse);
+
+  localparam CBITS = 15;    // Change pulse_wideR accordingly
+  
+  wire [CBITS-1:0] pulse_wideR;
+  assign pulse_wideR = {1'b0, sw[3:1], 1'b1, 10'd0};     // (CBTIS-5)
+  assign lbR = {1'b0, 4'b0000, 1'b1, 10'd0};
+  assign ubR = {1'b0, 4'b1111, 1'b1, 10'd0};
+
+  reg [CBITS-1:0] cnt_R;
+
+  always @(posedge clk) begin
+    cnt_R <= cnt_R + 1;
+    
+    if (cnt_R < pulse_wideR)
+      pulse_red = 1;
+    else
+      pulse_red = 0;
+
+    if (cnt_R < lbR)
+      lb_pulse = 1;
+    else
+      lb_pulse = 0;
+    
+    if (cnt_R < ubR)
+      ub_pulse = 1;
+    else
+      ub_pulse = 0;
+  end
+
+
+  // LTLSPEC G F Verilog.PWM_TOP.pulse_red = FALSE
+  assert property (@(posedge clk) always s_eventually pulse_red == 0);
+
+endmodule

examples/NeurIPS2025/Liveness/PWM_7-l1.sv

@@ -0,0 +1,35 @@
+module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red, output reg lb_pulse, output reg ub_pulse);
+
+  localparam CBITS = 16;    // Change pulse_wideR accordingly
+  
+  wire [CBITS-1:0] pulse_wideR;
+  assign pulse_wideR = {1'b0, sw[3:1], 1'b1, 11'd0};     // (CBTIS-5)
+  assign lbR = {1'b0, 4'b0000, 1'b1, 11'd0};
+  assign ubR = {1'b0, 4'b1111, 1'b1, 11'd0};
+
+  reg [CBITS-1:0] cnt_R;
+
+  always @(posedge clk) begin
+    cnt_R <= cnt_R + 1;
+    
+    if (cnt_R < pulse_wideR)
+      pulse_red = 1;
+    else
+      pulse_red = 0;
+
+    if (cnt_R < lbR)
+      lb_pulse = 1;
+    else
+      lb_pulse = 0;
+    
+    if (cnt_R < ubR)
+      ub_pulse = 1;
+    else
+      ub_pulse = 0;
+  end
+
+
+  // LTLSPEC G F Verilog.PWM_TOP.pulse_red = FALSE
+  assert property (@(posedge clk) always s_eventually pulse_red == 0);
+
+endmodule