Skip to content

Commit 27ffa99

Browse files
tautschnigtautschnig
committed
Update examples
Added further designs and properties, and fixed syntax issues.
1 parent 0290dac commit 27ffa99

File tree

211 files changed

+3671
-399
lines changed

Some content is hidden

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

211 files changed

+3671
-399
lines changed

‎examples/Benchmarks/PWM_1.sv

Lines changed: 13 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,22 @@
1-
module PWM_TOP #(localparam CBITS = 10) (input clk, input [3:0] sw, output reg pulse);
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
2+
3+
localparam CBITS = 10; // Change pulse_wideR accordingly
24

3-
wire [CBITS-1:0] pulse_wide;
4-
assign pulse_wide = {1'b0, sw[3:1], 6'd0}; // (CBTIS-4)
5+
wire [CBITS-1:0] pulse_wideR;
6+
assign pulse_wideR = {1'b0, sw[3:1], 6'd0}; // (CBTIS-4)
57

6-
reg [CBITS-1:0] cntR;
8+
reg [CBITS-1:0] cnt_R;
79

810
always @(posedge clk) begin
9-
cntR <= cntR + 1;
11+
cnt_R <= cnt_R + 1;
1012

11-
if (cntR < pulse_wide)
12-
pulse = 1'b1;
13+
if (cnt_R < pulse_wideR)
14+
pulse_red = 1'b1;
1315
else
14-
pulse = 1'b0;
16+
pulse_red = 1'b0;
17+
1518
end
16-
p1: assert property (@(posedge clk) (always s_eventually pulse == 0)) ;
19+
p1: assert property (@(posedge clk) (always s_eventually pulse_red == 0)) ;
1720
// G F (pulse = F)
1821
// G F (pulse = F) is instantaneous for EBMC-BDD but G F (pulse = T) isn't
19-
endmodule
22+
endmodule

‎examples/Benchmarks/PWM_10.sv

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
2+
3+
localparam CBITS = 19; // Change pulse_wideR accordingly
4+
5+
wire [CBITS-1:0] pulse_wideR;
6+
assign pulse_wideR = {1'b0, sw[3:1], 15'd0}; // (CBTIS-4)
7+
8+
reg [CBITS-1:0] cnt_R;
9+
10+
always @(posedge clk) begin
11+
cnt_R <= cnt_R + 1;
12+
13+
if (cnt_R < pulse_wideR)
14+
pulse_red = 1'b1;
15+
else
16+
pulse_red = 1'b0;
17+
18+
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
22+
endmodule

‎examples/Benchmarks/PWM_11.sv

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
2+
3+
localparam CBITS = 20; // Change pulse_wideR accordingly
4+
5+
wire [CBITS-1:0] pulse_wideR;
6+
assign pulse_wideR = {1'b0, sw[3:1], 16'd0}; // (CBTIS-4)
7+
8+
reg [CBITS-1:0] cnt_R;
9+
10+
always @(posedge clk) begin
11+
cnt_R <= cnt_R + 1;
12+
13+
if (cnt_R < pulse_wideR)
14+
pulse_red = 1'b1;
15+
else
16+
pulse_red = 1'b0;
17+
18+
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
22+
endmodule

‎examples/Benchmarks/PWM_12.sv

Lines changed: 22 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,22 @@
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
2+
3+
localparam CBITS = 21; // Change pulse_wideR accordingly
4+
5+
wire [CBITS-1:0] pulse_wideR;
6+
assign pulse_wideR = {1'b0, sw[3:1], 17'd0}; // (CBTIS-4)
7+
8+
reg [CBITS-1:0] cnt_R;
9+
10+
always @(posedge clk) begin
11+
cnt_R <= cnt_R + 1;
12+
13+
if (cnt_R < pulse_wideR)
14+
pulse_red = 1'b1;
15+
else
16+
pulse_red = 1'b0;
17+
18+
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
22+
endmodule

‎examples/Benchmarks/PWM_2.sv

Lines changed: 13 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,22 @@
1-
module PWM_TOP #(localparam CBITS = 11) (input clk, input [3:0] sw, output reg pulse);
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
2+
3+
localparam CBITS = 11; // Change pulse_wideR accordingly
24

3-
wire [CBITS-1:0] pulse_wide;
4-
assign pulse_wide = {1'b0, sw[3:1], 7'd0}; // (CBTIS-4)
5+
wire [CBITS-1:0] pulse_wideR;
6+
assign pulse_wideR = {1'b0, sw[3:1], 7'd0}; // (CBTIS-4)
57

6-
reg [CBITS-1:0] cntR;
8+
reg [CBITS-1:0] cnt_R;
79

810
always @(posedge clk) begin
9-
cntR <= cntR + 1;
11+
cnt_R <= cnt_R + 1;
1012

11-
if (cntR < pulse_wide)
12-
pulse = 1'b1;
13+
if (cnt_R < pulse_wideR)
14+
pulse_red = 1'b1;
1315
else
14-
pulse = 1'b0;
16+
pulse_red = 1'b0;
17+
1518
end
16-
p1: assert property (@(posedge clk) (always s_eventually pulse == 0)) ;
19+
p1: assert property (@(posedge clk) (always s_eventually pulse_red == 0)) ;
1720
// G F (pulse = F)
1821
// G F (pulse = F) is instantaneous for EBMC-BDD but G F (pulse = T) isn't
19-
endmodule
22+
endmodule

‎examples/Benchmarks/PWM_3.sv

Lines changed: 13 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,22 @@
1-
module PWM_TOP #(localparam CBITS = 12) (input clk, input [3:0] sw, output reg pulse);
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
2+
3+
localparam CBITS = 12; // Change pulse_wideR accordingly
24

3-
wire [CBITS-1:0] pulse_wide;
4-
assign pulse_wide = {1'b0, sw[3:1], 8'd0}; // (CBTIS-4)
5+
wire [CBITS-1:0] pulse_wideR;
6+
assign pulse_wideR = {1'b0, sw[3:1], 8'd0}; // (CBTIS-4)
57

6-
reg [CBITS-1:0] cntR;
8+
reg [CBITS-1:0] cnt_R;
79

810
always @(posedge clk) begin
9-
cntR <= cntR + 1;
11+
cnt_R <= cnt_R + 1;
1012

11-
if (cntR < pulse_wide)
12-
pulse = 1'b1;
13+
if (cnt_R < pulse_wideR)
14+
pulse_red = 1'b1;
1315
else
14-
pulse = 1'b0;
16+
pulse_red = 1'b0;
17+
1518
end
16-
p1: assert property (@(posedge clk) (always s_eventually pulse == 0)) ;
19+
p1: assert property (@(posedge clk) (always s_eventually pulse_red == 0)) ;
1720
// G F (pulse = F)
1821
// G F (pulse = F) is instantaneous for EBMC-BDD but G F (pulse = T) isn't
19-
endmodule
22+
endmodule

‎examples/Benchmarks/PWM_4.sv

Lines changed: 13 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,22 @@
1-
module PWM_TOP #(localparam CBITS = 13) (input clk, input [3:0] sw, output reg pulse);
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
2+
3+
localparam CBITS = 13; // Change pulse_wideR accordingly
24

3-
wire [CBITS-1:0] pulse_wide;
4-
assign pulse_wide = {1'b0, sw[3:1], 9'd0}; // (CBTIS-4)
5+
wire [CBITS-1:0] pulse_wideR;
6+
assign pulse_wideR = {1'b0, sw[3:1], 9'd0}; // (CBTIS-4)
57

6-
reg [CBITS-1:0] cntR;
8+
reg [CBITS-1:0] cnt_R;
79

810
always @(posedge clk) begin
9-
cntR <= cntR + 1;
11+
cnt_R <= cnt_R + 1;
1012

11-
if (cntR < pulse_wide)
12-
pulse = 1'b1;
13+
if (cnt_R < pulse_wideR)
14+
pulse_red = 1'b1;
1315
else
14-
pulse = 1'b0;
16+
pulse_red = 1'b0;
17+
1518
end
16-
p1: assert property (@(posedge clk) (always s_eventually pulse == 0)) ;
19+
p1: assert property (@(posedge clk) (always s_eventually pulse_red == 0)) ;
1720
// G F (pulse = F)
1821
// G F (pulse = F) is instantaneous for EBMC-BDD but G F (pulse = T) isn't
19-
endmodule
22+
endmodule

‎examples/Benchmarks/PWM_5.sv

Lines changed: 13 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,22 @@
1-
module PWM_TOP #(localparam CBITS = 14) (input clk, input [3:0] sw, output reg pulse);
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
2+
3+
localparam CBITS = 14; // Change pulse_wideR accordingly
24

3-
wire [CBITS-1:0] pulse_wide;
4-
assign pulse_wide = {1'b0, sw[3:1], 10'd0}; // (CBTIS-4)
5+
wire [CBITS-1:0] pulse_wideR;
6+
assign pulse_wideR = {1'b0, sw[3:1], 10'd0}; // (CBTIS-4)
57

6-
reg [CBITS-1:0] cntR;
8+
reg [CBITS-1:0] cnt_R;
79

810
always @(posedge clk) begin
9-
cntR <= cntR + 1;
11+
cnt_R <= cnt_R + 1;
1012

11-
if (cntR < pulse_wide)
12-
pulse = 1'b1;
13+
if (cnt_R < pulse_wideR)
14+
pulse_red = 1'b1;
1315
else
14-
pulse = 1'b0;
16+
pulse_red = 1'b0;
17+
1518
end
16-
p1: assert property (@(posedge clk) (always s_eventually pulse == 0)) ;
19+
p1: assert property (@(posedge clk) (always s_eventually pulse_red == 0)) ;
1720
// G F (pulse = F)
1821
// G F (pulse = F) is instantaneous for EBMC-BDD but G F (pulse = T) isn't
19-
endmodule
22+
endmodule

‎examples/Benchmarks/PWM_6.sv

Lines changed: 13 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,22 @@
1-
module PWM_TOP #(localparam CBITS = 15) (input clk, input [3:0] sw, output reg pulse);
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
2+
3+
localparam CBITS = 15; // Change pulse_wideR accordingly
24

3-
wire [CBITS-1:0] pulse_wide;
4-
assign pulse_wide = {1'b0, sw[3:1], 11'd0}; // (CBTIS-4)
5+
wire [CBITS-1:0] pulse_wideR;
6+
assign pulse_wideR = {1'b0, sw[3:1], 11'd0}; // (CBTIS-4)
57

6-
reg [CBITS-1:0] cntR;
8+
reg [CBITS-1:0] cnt_R;
79

810
always @(posedge clk) begin
9-
cntR <= cntR + 1;
11+
cnt_R <= cnt_R + 1;
1012

11-
if (cntR < pulse_wide)
12-
pulse = 1'b1;
13+
if (cnt_R < pulse_wideR)
14+
pulse_red = 1'b1;
1315
else
14-
pulse = 1'b0;
16+
pulse_red = 1'b0;
17+
1518
end
16-
p1: assert property (@(posedge clk) (always s_eventually pulse == 0)) ;
19+
p1: assert property (@(posedge clk) (always s_eventually pulse_red == 0)) ;
1720
// G F (pulse = F)
1821
// G F (pulse = F) is instantaneous for EBMC-BDD but G F (pulse = T) isn't
19-
endmodule
22+
endmodule

‎examples/Benchmarks/PWM_7.sv

Lines changed: 13 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,22 @@
1-
module PWM_TOP #(localparam CBITS = 16) (input clk, input [3:0] sw, output reg pulse);
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
2+
3+
localparam CBITS = 16; // Change pulse_wideR accordingly
24

3-
wire [CBITS-1:0] pulse_wide;
4-
assign pulse_wide = {1'b0, sw[3:1], 12'd0}; // (CBTIS-4)
5+
wire [CBITS-1:0] pulse_wideR;
6+
assign pulse_wideR = {1'b0, sw[3:1], 12'd0}; // (CBTIS-4)
57

6-
reg [CBITS-1:0] cntR;
8+
reg [CBITS-1:0] cnt_R;
79

810
always @(posedge clk) begin
9-
cntR <= cntR + 1;
11+
cnt_R <= cnt_R + 1;
1012

11-
if (cntR < pulse_wide)
12-
pulse = 1'b1;
13+
if (cnt_R < pulse_wideR)
14+
pulse_red = 1'b1;
1315
else
14-
pulse = 1'b0;
16+
pulse_red = 1'b0;
17+
1518
end
16-
p1: assert property (@(posedge clk) (always s_eventually pulse == 0)) ;
19+
p1: assert property (@(posedge clk) (always s_eventually pulse_red == 0)) ;
1720
// G F (pulse = F)
1821
// G F (pulse = F) is instantaneous for EBMC-BDD but G F (pulse = T) isn't
19-
endmodule
22+
endmodule

‎examples/Benchmarks/PWM_8.sv

Lines changed: 13 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,22 @@
1-
module PWM_TOP #(localparam CBITS = 17) (input clk, input [3:0] sw, output reg pulse);
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
2+
3+
localparam CBITS = 17; // Change pulse_wideR accordingly
24

3-
wire [CBITS-1:0] pulse_wide;
4-
assign pulse_wide = {1'b0, sw[3:1], 13'd0}; // (CBTIS-4)
5+
wire [CBITS-1:0] pulse_wideR;
6+
assign pulse_wideR = {1'b0, sw[3:1], 13'd0}; // (CBTIS-4)
57

6-
reg [CBITS-1:0] cntR;
8+
reg [CBITS-1:0] cnt_R;
79

810
always @(posedge clk) begin
9-
cntR <= cntR + 1;
11+
cnt_R <= cnt_R + 1;
1012

11-
if (cntR < pulse_wide)
12-
pulse = 1'b1;
13+
if (cnt_R < pulse_wideR)
14+
pulse_red = 1'b1;
1315
else
14-
pulse = 1'b0;
16+
pulse_red = 1'b0;
17+
1518
end
16-
p1: assert property (@(posedge clk) (always s_eventually pulse == 0)) ;
19+
p1: assert property (@(posedge clk) (always s_eventually pulse_red == 0)) ;
1720
// G F (pulse = F)
1821
// G F (pulse = F) is instantaneous for EBMC-BDD but G F (pulse = T) isn't
19-
endmodule
22+
endmodule

‎examples/Benchmarks/PWM_9.sv

Lines changed: 13 additions & 10 deletions
Original file line numberDiff line numberDiff line change
@@ -1,19 +1,22 @@
1-
module PWM_TOP #(localparam CBITS = 18) (input clk, input [3:0] sw, output reg pulse);
1+
module PWM_TOP (input clk, input [3:0] sw, output reg pulse_red);
2+
3+
localparam CBITS = 18; // Change pulse_wideR accordingly
24

3-
wire [CBITS-1:0] pulse_wide;
4-
assign pulse_wide = {1'b0, sw[3:1], 14'd0}; // (CBTIS-4)
5+
wire [CBITS-1:0] pulse_wideR;
6+
assign pulse_wideR = {1'b0, sw[3:1], 14'd0}; // (CBTIS-4)
57

6-
reg [CBITS-1:0] cntR;
8+
reg [CBITS-1:0] cnt_R;
79

810
always @(posedge clk) begin
9-
cntR <= cntR + 1;
11+
cnt_R <= cnt_R + 1;
1012

11-
if (cntR < pulse_wide)
12-
pulse = 1'b1;
13+
if (cnt_R < pulse_wideR)
14+
pulse_red = 1'b1;
1315
else
14-
pulse = 1'b0;
16+
pulse_red = 1'b0;
17+
1518
end
16-
p1: assert property (@(posedge clk) (always s_eventually pulse == 0)) ;
19+
p1: assert property (@(posedge clk) (always s_eventually pulse_red == 0)) ;
1720
// G F (pulse = F)
1821
// G F (pulse = F) is instantaneous for EBMC-BDD but G F (pulse = T) isn't
19-
endmodule
22+
endmodule

‎examples/Benchmarks/delay_1-p2.sv

Lines changed: 18 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,18 @@
1+
module DELAY (input clk, input rst, output reg sig ,output reg err, output reg flg);
2+
localparam N = 750;
3+
localparam CBITS = 10;
4+
reg [CBITS-1 :0] cnt;
5+
always @(posedge clk) begin
6+
if (rst) cnt = 0;
7+
else cnt = cnt + 1;
8+
if (cnt > N) begin sig = 1;
9+
cnt = 0; end
10+
else sig = 0;
11+
if (cnt > N + 1) err = 1;
12+
else err = 0;
13+
if (cnt <= N) flg = 1;
14+
else flg = 0;
15+
end
16+
p2: assert property (@(posedge clk) (always s_eventually rst == 1) or (always s_eventually (sig == 1 and nexttime sig == 0))) ;
17+
// F G (rst = F) -> G F (sig = T & X (sig = F))
18+
endmodule

0 commit comments

Comments
 (0)