Skip to content

Commit 720eb68

Browse files
tautschnigtautschnig
committed
Add blinking-led example
1 parent 7470aaa commit 720eb68

25 files changed

+475
-0
lines changed

‎examples/Benchmarks/blink_1.sv

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module BLINK #(localparam CBITS = 8) (input clk, input rst, output reg led, output reg flg);
2+
reg [CBITS-1:0] cnt;
3+
reg mode;
4+
always@(posedge clk, posedge rst) begin
5+
if (rst) begin
6+
cnt <= 0;
7+
mode <= 0;
8+
end
9+
else begin
10+
cnt <= cnt + 1;
11+
if (cnt == 0)
12+
mode <= ~mode;
13+
flg = (cnt == 0);
14+
led = mode;
15+
end
16+
end
17+
p1: assert property (@(posedge clk) s_eventually !rst -> led);
18+
// F G (rst = F) -> G F (led = T)
19+
endmodule

‎examples/Benchmarks/blink_10.sv

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module BLINK #(localparam CBITS = 17) (input clk, input rst, output reg led, output reg flg);
2+
reg [CBITS-1:0] cnt;
3+
reg mode;
4+
always@(posedge clk, posedge rst) begin
5+
if (rst) begin
6+
cnt <= 0;
7+
mode <= 0;
8+
end
9+
else begin
10+
cnt <= cnt + 1;
11+
if (cnt == 0)
12+
mode <= ~mode;
13+
flg = (cnt == 0);
14+
led = mode;
15+
end
16+
end
17+
p1: assert property (@(posedge clk) s_eventually !rst -> led);
18+
// F G (rst = F) -> G F (led = T)
19+
endmodule

‎examples/Benchmarks/blink_11.sv

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module BLINK #(localparam CBITS = 18) (input clk, input rst, output reg led, output reg flg);
2+
reg [CBITS-1:0] cnt;
3+
reg mode;
4+
always@(posedge clk, posedge rst) begin
5+
if (rst) begin
6+
cnt <= 0;
7+
mode <= 0;
8+
end
9+
else begin
10+
cnt <= cnt + 1;
11+
if (cnt == 0)
12+
mode <= ~mode;
13+
flg = (cnt == 0);
14+
led = mode;
15+
end
16+
end
17+
p1: assert property (@(posedge clk) s_eventually !rst -> led);
18+
// F G (rst = F) -> G F (led = T)
19+
endmodule

‎examples/Benchmarks/blink_12.sv

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module BLINK #(localparam CBITS = 19) (input clk, input rst, output reg led, output reg flg);
2+
reg [CBITS-1:0] cnt;
3+
reg mode;
4+
always@(posedge clk, posedge rst) begin
5+
if (rst) begin
6+
cnt <= 0;
7+
mode <= 0;
8+
end
9+
else begin
10+
cnt <= cnt + 1;
11+
if (cnt == 0)
12+
mode <= ~mode;
13+
flg = (cnt == 0);
14+
led = mode;
15+
end
16+
end
17+
p1: assert property (@(posedge clk) s_eventually !rst -> led);
18+
// F G (rst = F) -> G F (led = T)
19+
endmodule

‎examples/Benchmarks/blink_13.sv

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module BLINK #(localparam CBITS = 20) (input clk, input rst, output reg led, output reg flg);
2+
reg [CBITS-1:0] cnt;
3+
reg mode;
4+
always@(posedge clk, posedge rst) begin
5+
if (rst) begin
6+
cnt <= 0;
7+
mode <= 0;
8+
end
9+
else begin
10+
cnt <= cnt + 1;
11+
if (cnt == 0)
12+
mode <= ~mode;
13+
flg = (cnt == 0);
14+
led = mode;
15+
end
16+
end
17+
p1: assert property (@(posedge clk) s_eventually !rst -> led);
18+
// F G (rst = F) -> G F (led = T)
19+
endmodule

‎examples/Benchmarks/blink_14.sv

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module BLINK #(localparam CBITS = 21) (input clk, input rst, output reg led, output reg flg);
2+
reg [CBITS-1:0] cnt;
3+
reg mode;
4+
always@(posedge clk, posedge rst) begin
5+
if (rst) begin
6+
cnt <= 0;
7+
mode <= 0;
8+
end
9+
else begin
10+
cnt <= cnt + 1;
11+
if (cnt == 0)
12+
mode <= ~mode;
13+
flg = (cnt == 0);
14+
led = mode;
15+
end
16+
end
17+
p1: assert property (@(posedge clk) s_eventually !rst -> led);
18+
// F G (rst = F) -> G F (led = T)
19+
endmodule

‎examples/Benchmarks/blink_15.sv

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module BLINK #(localparam CBITS = 22) (input clk, input rst, output reg led, output reg flg);
2+
reg [CBITS-1:0] cnt;
3+
reg mode;
4+
always@(posedge clk, posedge rst) begin
5+
if (rst) begin
6+
cnt <= 0;
7+
mode <= 0;
8+
end
9+
else begin
10+
cnt <= cnt + 1;
11+
if (cnt == 0)
12+
mode <= ~mode;
13+
flg = (cnt == 0);
14+
led = mode;
15+
end
16+
end
17+
p1: assert property (@(posedge clk) s_eventually !rst -> led);
18+
// F G (rst = F) -> G F (led = T)
19+
endmodule

‎examples/Benchmarks/blink_16.sv

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module BLINK #(localparam CBITS = 23) (input clk, input rst, output reg led, output reg flg);
2+
reg [CBITS-1:0] cnt;
3+
reg mode;
4+
always@(posedge clk, posedge rst) begin
5+
if (rst) begin
6+
cnt <= 0;
7+
mode <= 0;
8+
end
9+
else begin
10+
cnt <= cnt + 1;
11+
if (cnt == 0)
12+
mode <= ~mode;
13+
flg = (cnt == 0);
14+
led = mode;
15+
end
16+
end
17+
p1: assert property (@(posedge clk) s_eventually !rst -> led);
18+
// F G (rst = F) -> G F (led = T)
19+
endmodule

‎examples/Benchmarks/blink_17.sv

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module BLINK #(localparam CBITS = 24) (input clk, input rst, output reg led, output reg flg);
2+
reg [CBITS-1:0] cnt;
3+
reg mode;
4+
always@(posedge clk, posedge rst) begin
5+
if (rst) begin
6+
cnt <= 0;
7+
mode <= 0;
8+
end
9+
else begin
10+
cnt <= cnt + 1;
11+
if (cnt == 0)
12+
mode <= ~mode;
13+
flg = (cnt == 0);
14+
led = mode;
15+
end
16+
end
17+
p1: assert property (@(posedge clk) s_eventually !rst -> led);
18+
// F G (rst = F) -> G F (led = T)
19+
endmodule

‎examples/Benchmarks/blink_18.sv

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module BLINK #(localparam CBITS = 25) (input clk, input rst, output reg led, output reg flg);
2+
reg [CBITS-1:0] cnt;
3+
reg mode;
4+
always@(posedge clk, posedge rst) begin
5+
if (rst) begin
6+
cnt <= 0;
7+
mode <= 0;
8+
end
9+
else begin
10+
cnt <= cnt + 1;
11+
if (cnt == 0)
12+
mode <= ~mode;
13+
flg = (cnt == 0);
14+
led = mode;
15+
end
16+
end
17+
p1: assert property (@(posedge clk) s_eventually !rst -> led);
18+
// F G (rst = F) -> G F (led = T)
19+
endmodule

‎examples/Benchmarks/blink_19.sv

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module BLINK #(localparam CBITS = 26) (input clk, input rst, output reg led, output reg flg);
2+
reg [CBITS-1:0] cnt;
3+
reg mode;
4+
always@(posedge clk, posedge rst) begin
5+
if (rst) begin
6+
cnt <= 0;
7+
mode <= 0;
8+
end
9+
else begin
10+
cnt <= cnt + 1;
11+
if (cnt == 0)
12+
mode <= ~mode;
13+
flg = (cnt == 0);
14+
led = mode;
15+
end
16+
end
17+
p1: assert property (@(posedge clk) s_eventually !rst -> led);
18+
// F G (rst = F) -> G F (led = T)
19+
endmodule

‎examples/Benchmarks/blink_2.sv

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module BLINK #(localparam CBITS = 9) (input clk, input rst, output reg led, output reg flg);
2+
reg [CBITS-1:0] cnt;
3+
reg mode;
4+
always@(posedge clk, posedge rst) begin
5+
if (rst) begin
6+
cnt <= 0;
7+
mode <= 0;
8+
end
9+
else begin
10+
cnt <= cnt + 1;
11+
if (cnt == 0)
12+
mode <= ~mode;
13+
flg = (cnt == 0);
14+
led = mode;
15+
end
16+
end
17+
p1: assert property (@(posedge clk) s_eventually !rst -> led);
18+
// F G (rst = F) -> G F (led = T)
19+
endmodule

‎examples/Benchmarks/blink_20.sv

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module BLINK #(localparam CBITS = 27) (input clk, input rst, output reg led, output reg flg);
2+
reg [CBITS-1:0] cnt;
3+
reg mode;
4+
always@(posedge clk, posedge rst) begin
5+
if (rst) begin
6+
cnt <= 0;
7+
mode <= 0;
8+
end
9+
else begin
10+
cnt <= cnt + 1;
11+
if (cnt == 0)
12+
mode <= ~mode;
13+
flg = (cnt == 0);
14+
led = mode;
15+
end
16+
end
17+
p1: assert property (@(posedge clk) s_eventually !rst -> led);
18+
// F G (rst = F) -> G F (led = T)
19+
endmodule

‎examples/Benchmarks/blink_21.sv

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module BLINK #(localparam CBITS = 28) (input clk, input rst, output reg led, output reg flg);
2+
reg [CBITS-1:0] cnt;
3+
reg mode;
4+
always@(posedge clk, posedge rst) begin
5+
if (rst) begin
6+
cnt <= 0;
7+
mode <= 0;
8+
end
9+
else begin
10+
cnt <= cnt + 1;
11+
if (cnt == 0)
12+
mode <= ~mode;
13+
flg = (cnt == 0);
14+
led = mode;
15+
end
16+
end
17+
p1: assert property (@(posedge clk) s_eventually !rst -> led);
18+
// F G (rst = F) -> G F (led = T)
19+
endmodule

‎examples/Benchmarks/blink_22.sv

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module BLINK #(localparam CBITS = 29) (input clk, input rst, output reg led, output reg flg);
2+
reg [CBITS-1:0] cnt;
3+
reg mode;
4+
always@(posedge clk, posedge rst) begin
5+
if (rst) begin
6+
cnt <= 0;
7+
mode <= 0;
8+
end
9+
else begin
10+
cnt <= cnt + 1;
11+
if (cnt == 0)
12+
mode <= ~mode;
13+
flg = (cnt == 0);
14+
led = mode;
15+
end
16+
end
17+
p1: assert property (@(posedge clk) s_eventually !rst -> led);
18+
// F G (rst = F) -> G F (led = T)
19+
endmodule

‎examples/Benchmarks/blink_23.sv

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module BLINK #(localparam CBITS = 30) (input clk, input rst, output reg led, output reg flg);
2+
reg [CBITS-1:0] cnt;
3+
reg mode;
4+
always@(posedge clk, posedge rst) begin
5+
if (rst) begin
6+
cnt <= 0;
7+
mode <= 0;
8+
end
9+
else begin
10+
cnt <= cnt + 1;
11+
if (cnt == 0)
12+
mode <= ~mode;
13+
flg = (cnt == 0);
14+
led = mode;
15+
end
16+
end
17+
p1: assert property (@(posedge clk) s_eventually !rst -> led);
18+
// F G (rst = F) -> G F (led = T)
19+
endmodule

‎examples/Benchmarks/blink_24.sv

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module BLINK #(localparam CBITS = 31) (input clk, input rst, output reg led, output reg flg);
2+
reg [CBITS-1:0] cnt;
3+
reg mode;
4+
always@(posedge clk, posedge rst) begin
5+
if (rst) begin
6+
cnt <= 0;
7+
mode <= 0;
8+
end
9+
else begin
10+
cnt <= cnt + 1;
11+
if (cnt == 0)
12+
mode <= ~mode;
13+
flg = (cnt == 0);
14+
led = mode;
15+
end
16+
end
17+
p1: assert property (@(posedge clk) s_eventually !rst -> led);
18+
// F G (rst = F) -> G F (led = T)
19+
endmodule

‎examples/Benchmarks/blink_25.sv

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module BLINK #(localparam CBITS = 32) (input clk, input rst, output reg led, output reg flg);
2+
reg [CBITS-1:0] cnt;
3+
reg mode;
4+
always@(posedge clk, posedge rst) begin
5+
if (rst) begin
6+
cnt <= 0;
7+
mode <= 0;
8+
end
9+
else begin
10+
cnt <= cnt + 1;
11+
if (cnt == 0)
12+
mode <= ~mode;
13+
flg = (cnt == 0);
14+
led = mode;
15+
end
16+
end
17+
p1: assert property (@(posedge clk) s_eventually !rst -> led);
18+
// F G (rst = F) -> G F (led = T)
19+
endmodule

‎examples/Benchmarks/blink_3.sv

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module BLINK #(localparam CBITS = 10) (input clk, input rst, output reg led, output reg flg);
2+
reg [CBITS-1:0] cnt;
3+
reg mode;
4+
always@(posedge clk, posedge rst) begin
5+
if (rst) begin
6+
cnt <= 0;
7+
mode <= 0;
8+
end
9+
else begin
10+
cnt <= cnt + 1;
11+
if (cnt == 0)
12+
mode <= ~mode;
13+
flg = (cnt == 0);
14+
led = mode;
15+
end
16+
end
17+
p1: assert property (@(posedge clk) s_eventually !rst -> led);
18+
// F G (rst = F) -> G F (led = T)
19+
endmodule

‎examples/Benchmarks/blink_4.sv

Lines changed: 19 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,19 @@
1+
module BLINK #(localparam CBITS = 11) (input clk, input rst, output reg led, output reg flg);
2+
reg [CBITS-1:0] cnt;
3+
reg mode;
4+
always@(posedge clk, posedge rst) begin
5+
if (rst) begin
6+
cnt <= 0;
7+
mode <= 0;
8+
end
9+
else begin
10+
cnt <= cnt + 1;
11+
if (cnt == 0)
12+
mode <= ~mode;
13+
flg = (cnt == 0);
14+
led = mode;
15+
end
16+
end
17+
p1: assert property (@(posedge clk) s_eventually !rst -> led);
18+
// F G (rst = F) -> G F (led = T)
19+
endmodule

0 commit comments

Comments
 (0)