Skip to content

Commit cd4b68e

Browse files
tautschnigtautschnig
committed
Updated liveness
1 parent 9b20d36 commit cd4b68e

File tree

220 files changed

+1487
-1288
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

220 files changed

+1487
-1288
lines changed

‎examples/Benchmarks/PWM_1.sv

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,33 @@
1-
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red, output reg lb_pulse, output reg ub_pulse);
22

33
localparam CBITS = 10; // Change pulse_wideR accordingly
44

55
wire [CBITS-1:0] pulse_wideR;
6-
assign pulse_wideR = {1'b0, sw[3:1], 6'd0}; // (CBTIS-4)
6+
assign pulse_wideR = {1'b0, sw[3:1], 1'b1, 5'd0}; // (CBTIS-5)
7+
assign lbR = {1'b0, 4'b0000, 1'b1, 5'd0};
8+
assign ubR = {1'b0, 4'b1111, 1'b1, 5'd0};
79

810
reg [CBITS-1:0] cnt_R;
911

1012
always @(posedge clk) begin
1113
cnt_R <= cnt_R + 1;
1214

1315
if (cnt_R < pulse_wideR)
14-
pulse_red = 1'b1;
16+
pulse_red = 1;
1517
else
16-
pulse_red = 1'b0;
17-
18+
pulse_red = 0;
19+
20+
if (cnt_R < lbR)
21+
lb_pulse = 1;
22+
else
23+
lb_pulse = 0;
24+
25+
if (cnt_R < ubR)
26+
ub_pulse = 1;
27+
else
28+
ub_pulse = 0;
1829
end
19-
p1: assert property (@(posedge clk) (always s_eventually pulse_red == 0)) ;
20-
// G F (pulse = F)
21-
// G F (pulse = F) is instantaneous for EBMC-BDD but G F (pulse = T) isn't
30+
31+
p1: assert property (@(posedge clk) s_eventually pulse_red == 0);
32+
// GF !p_red
2233
endmodule

‎examples/Benchmarks/PWM_10.sv

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,33 @@
1-
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red, output reg lb_pulse, output reg ub_pulse);
22

33
localparam CBITS = 19; // Change pulse_wideR accordingly
44

55
wire [CBITS-1:0] pulse_wideR;
6-
assign pulse_wideR = {1'b0, sw[3:1], 15'd0}; // (CBTIS-4)
6+
assign pulse_wideR = {1'b0, sw[3:1], 1'b1, 14'd0}; // (CBTIS-5)
7+
assign lbR = {1'b0, 4'b0000, 1'b1, 14'd0};
8+
assign ubR = {1'b0, 4'b1111, 1'b1, 14'd0};
79

810
reg [CBITS-1:0] cnt_R;
911

1012
always @(posedge clk) begin
1113
cnt_R <= cnt_R + 1;
1214

1315
if (cnt_R < pulse_wideR)
14-
pulse_red = 1'b1;
16+
pulse_red = 1;
1517
else
16-
pulse_red = 1'b0;
17-
18+
pulse_red = 0;
19+
20+
if (cnt_R < lbR)
21+
lb_pulse = 1;
22+
else
23+
lb_pulse = 0;
24+
25+
if (cnt_R < ubR)
26+
ub_pulse = 1;
27+
else
28+
ub_pulse = 0;
1829
end
19-
p1: assert property (@(posedge clk) (always s_eventually pulse_red == 0)) ;
20-
// G F (pulse = F)
21-
// G F (pulse = F) is instantaneous for EBMC-BDD but G F (pulse = T) isn't
30+
31+
p1: assert property (@(posedge clk) s_eventually pulse_red == 0);
32+
// GF !p_red
2233
endmodule

‎examples/Benchmarks/PWM_11.sv

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,33 @@
1-
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red, output reg lb_pulse, output reg ub_pulse);
22

33
localparam CBITS = 20; // Change pulse_wideR accordingly
44

55
wire [CBITS-1:0] pulse_wideR;
6-
assign pulse_wideR = {1'b0, sw[3:1], 16'd0}; // (CBTIS-4)
6+
assign pulse_wideR = {1'b0, sw[3:1], 1'b1, 15'd0}; // (CBTIS-5)
7+
assign lbR = {1'b0, 4'b0000, 1'b1, 15'd0};
8+
assign ubR = {1'b0, 4'b1111, 1'b1, 15'd0};
79

810
reg [CBITS-1:0] cnt_R;
911

1012
always @(posedge clk) begin
1113
cnt_R <= cnt_R + 1;
1214

1315
if (cnt_R < pulse_wideR)
14-
pulse_red = 1'b1;
16+
pulse_red = 1;
1517
else
16-
pulse_red = 1'b0;
17-
18+
pulse_red = 0;
19+
20+
if (cnt_R < lbR)
21+
lb_pulse = 1;
22+
else
23+
lb_pulse = 0;
24+
25+
if (cnt_R < ubR)
26+
ub_pulse = 1;
27+
else
28+
ub_pulse = 0;
1829
end
19-
p1: assert property (@(posedge clk) (always s_eventually pulse_red == 0)) ;
20-
// G F (pulse = F)
21-
// G F (pulse = F) is instantaneous for EBMC-BDD but G F (pulse = T) isn't
30+
31+
p1: assert property (@(posedge clk) s_eventually pulse_red == 0);
32+
// GF !p_red
2233
endmodule

‎examples/Benchmarks/PWM_12.sv

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,33 @@
1-
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red, output reg lb_pulse, output reg ub_pulse);
22

33
localparam CBITS = 21; // Change pulse_wideR accordingly
44

55
wire [CBITS-1:0] pulse_wideR;
6-
assign pulse_wideR = {1'b0, sw[3:1], 17'd0}; // (CBTIS-4)
6+
assign pulse_wideR = {1'b0, sw[3:1], 1'b1, 16'd0}; // (CBTIS-5)
7+
assign lbR = {1'b0, 4'b0000, 1'b1, 16'd0};
8+
assign ubR = {1'b0, 4'b1111, 1'b1, 16'd0};
79

810
reg [CBITS-1:0] cnt_R;
911

1012
always @(posedge clk) begin
1113
cnt_R <= cnt_R + 1;
1214

1315
if (cnt_R < pulse_wideR)
14-
pulse_red = 1'b1;
16+
pulse_red = 1;
1517
else
16-
pulse_red = 1'b0;
17-
18+
pulse_red = 0;
19+
20+
if (cnt_R < lbR)
21+
lb_pulse = 1;
22+
else
23+
lb_pulse = 0;
24+
25+
if (cnt_R < ubR)
26+
ub_pulse = 1;
27+
else
28+
ub_pulse = 0;
1829
end
19-
p1: assert property (@(posedge clk) (always s_eventually pulse_red == 0)) ;
20-
// G F (pulse = F)
21-
// G F (pulse = F) is instantaneous for EBMC-BDD but G F (pulse = T) isn't
30+
31+
p1: assert property (@(posedge clk) s_eventually pulse_red == 0);
32+
// GF !p_red
2233
endmodule

‎examples/Benchmarks/PWM_2.sv

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,33 @@
1-
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red, output reg lb_pulse, output reg ub_pulse);
22

33
localparam CBITS = 11; // Change pulse_wideR accordingly
44

55
wire [CBITS-1:0] pulse_wideR;
6-
assign pulse_wideR = {1'b0, sw[3:1], 7'd0}; // (CBTIS-4)
6+
assign pulse_wideR = {1'b0, sw[3:1], 1'b1, 6'd0}; // (CBTIS-5)
7+
assign lbR = {1'b0, 4'b0000, 1'b1, 6'd0};
8+
assign ubR = {1'b0, 4'b1111, 1'b1, 6'd0};
79

810
reg [CBITS-1:0] cnt_R;
911

1012
always @(posedge clk) begin
1113
cnt_R <= cnt_R + 1;
1214

1315
if (cnt_R < pulse_wideR)
14-
pulse_red = 1'b1;
16+
pulse_red = 1;
1517
else
16-
pulse_red = 1'b0;
17-
18+
pulse_red = 0;
19+
20+
if (cnt_R < lbR)
21+
lb_pulse = 1;
22+
else
23+
lb_pulse = 0;
24+
25+
if (cnt_R < ubR)
26+
ub_pulse = 1;
27+
else
28+
ub_pulse = 0;
1829
end
19-
p1: assert property (@(posedge clk) (always s_eventually pulse_red == 0)) ;
20-
// G F (pulse = F)
21-
// G F (pulse = F) is instantaneous for EBMC-BDD but G F (pulse = T) isn't
30+
31+
p1: assert property (@(posedge clk) s_eventually pulse_red == 0);
32+
// GF !p_red
2233
endmodule

‎examples/Benchmarks/PWM_3.sv

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,33 @@
1-
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red, output reg lb_pulse, output reg ub_pulse);
22

33
localparam CBITS = 12; // Change pulse_wideR accordingly
44

55
wire [CBITS-1:0] pulse_wideR;
6-
assign pulse_wideR = {1'b0, sw[3:1], 8'd0}; // (CBTIS-4)
6+
assign pulse_wideR = {1'b0, sw[3:1], 1'b1, 7'd0}; // (CBTIS-5)
7+
assign lbR = {1'b0, 4'b0000, 1'b1, 7'd0};
8+
assign ubR = {1'b0, 4'b1111, 1'b1, 7'd0};
79

810
reg [CBITS-1:0] cnt_R;
911

1012
always @(posedge clk) begin
1113
cnt_R <= cnt_R + 1;
1214

1315
if (cnt_R < pulse_wideR)
14-
pulse_red = 1'b1;
16+
pulse_red = 1;
1517
else
16-
pulse_red = 1'b0;
17-
18+
pulse_red = 0;
19+
20+
if (cnt_R < lbR)
21+
lb_pulse = 1;
22+
else
23+
lb_pulse = 0;
24+
25+
if (cnt_R < ubR)
26+
ub_pulse = 1;
27+
else
28+
ub_pulse = 0;
1829
end
19-
p1: assert property (@(posedge clk) (always s_eventually pulse_red == 0)) ;
20-
// G F (pulse = F)
21-
// G F (pulse = F) is instantaneous for EBMC-BDD but G F (pulse = T) isn't
30+
31+
p1: assert property (@(posedge clk) s_eventually pulse_red == 0);
32+
// GF !p_red
2233
endmodule

‎examples/Benchmarks/PWM_4.sv

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,33 @@
1-
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red, output reg lb_pulse, output reg ub_pulse);
22

33
localparam CBITS = 13; // Change pulse_wideR accordingly
44

55
wire [CBITS-1:0] pulse_wideR;
6-
assign pulse_wideR = {1'b0, sw[3:1], 9'd0}; // (CBTIS-4)
6+
assign pulse_wideR = {1'b0, sw[3:1], 1'b1, 8'd0}; // (CBTIS-5)
7+
assign lbR = {1'b0, 4'b0000, 1'b1, 8'd0};
8+
assign ubR = {1'b0, 4'b1111, 1'b1, 8'd0};
79

810
reg [CBITS-1:0] cnt_R;
911

1012
always @(posedge clk) begin
1113
cnt_R <= cnt_R + 1;
1214

1315
if (cnt_R < pulse_wideR)
14-
pulse_red = 1'b1;
16+
pulse_red = 1;
1517
else
16-
pulse_red = 1'b0;
17-
18+
pulse_red = 0;
19+
20+
if (cnt_R < lbR)
21+
lb_pulse = 1;
22+
else
23+
lb_pulse = 0;
24+
25+
if (cnt_R < ubR)
26+
ub_pulse = 1;
27+
else
28+
ub_pulse = 0;
1829
end
19-
p1: assert property (@(posedge clk) (always s_eventually pulse_red == 0)) ;
20-
// G F (pulse = F)
21-
// G F (pulse = F) is instantaneous for EBMC-BDD but G F (pulse = T) isn't
30+
31+
p1: assert property (@(posedge clk) s_eventually pulse_red == 0);
32+
// GF !p_red
2233
endmodule

‎examples/Benchmarks/PWM_5.sv

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,33 @@
1-
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red, output reg lb_pulse, output reg ub_pulse);
22

33
localparam CBITS = 14; // Change pulse_wideR accordingly
44

55
wire [CBITS-1:0] pulse_wideR;
6-
assign pulse_wideR = {1'b0, sw[3:1], 10'd0}; // (CBTIS-4)
6+
assign pulse_wideR = {1'b0, sw[3:1], 1'b1, 9'd0}; // (CBTIS-5)
7+
assign lbR = {1'b0, 4'b0000, 1'b1, 9'd0};
8+
assign ubR = {1'b0, 4'b1111, 1'b1, 9'd0};
79

810
reg [CBITS-1:0] cnt_R;
911

1012
always @(posedge clk) begin
1113
cnt_R <= cnt_R + 1;
1214

1315
if (cnt_R < pulse_wideR)
14-
pulse_red = 1'b1;
16+
pulse_red = 1;
1517
else
16-
pulse_red = 1'b0;
17-
18+
pulse_red = 0;
19+
20+
if (cnt_R < lbR)
21+
lb_pulse = 1;
22+
else
23+
lb_pulse = 0;
24+
25+
if (cnt_R < ubR)
26+
ub_pulse = 1;
27+
else
28+
ub_pulse = 0;
1829
end
19-
p1: assert property (@(posedge clk) (always s_eventually pulse_red == 0)) ;
20-
// G F (pulse = F)
21-
// G F (pulse = F) is instantaneous for EBMC-BDD but G F (pulse = T) isn't
30+
31+
p1: assert property (@(posedge clk) s_eventually pulse_red == 0);
32+
// GF !p_red
2233
endmodule

‎examples/Benchmarks/PWM_6.sv

Lines changed: 19 additions & 8 deletions
Original file line numberDiff line numberDiff line change
@@ -1,22 +1,33 @@
1-
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red, output reg lb_pulse, output reg ub_pulse);
22

33
localparam CBITS = 15; // Change pulse_wideR accordingly
44

55
wire [CBITS-1:0] pulse_wideR;
6-
assign pulse_wideR = {1'b0, sw[3:1], 11'd0}; // (CBTIS-4)
6+
assign pulse_wideR = {1'b0, sw[3:1], 1'b1, 10'd0}; // (CBTIS-5)
7+
assign lbR = {1'b0, 4'b0000, 1'b1, 10'd0};
8+
assign ubR = {1'b0, 4'b1111, 1'b1, 10'd0};
79

810
reg [CBITS-1:0] cnt_R;
911

1012
always @(posedge clk) begin
1113
cnt_R <= cnt_R + 1;
1214

1315
if (cnt_R < pulse_wideR)
14-
pulse_red = 1'b1;
16+
pulse_red = 1;
1517
else
16-
pulse_red = 1'b0;
17-
18+
pulse_red = 0;
19+
20+
if (cnt_R < lbR)
21+
lb_pulse = 1;
22+
else
23+
lb_pulse = 0;
24+
25+
if (cnt_R < ubR)
26+
ub_pulse = 1;
27+
else
28+
ub_pulse = 0;
1829
end
19-
p1: assert property (@(posedge clk) (always s_eventually pulse_red == 0)) ;
20-
// G F (pulse = F)
21-
// G F (pulse = F) is instantaneous for EBMC-BDD but G F (pulse = T) isn't
30+
31+
p1: assert property (@(posedge clk) s_eventually pulse_red == 0);
32+
// GF !p_red
2233
endmodule

0 commit comments

Comments
 (0)