From 5855024cccfbcb1919e3225f519bc9f0421c4056 Mon Sep 17 00:00:00 2001 From: Zachary Snow Date: Tue, 9 Apr 2019 12:28:32 -0400 Subject: support repeat loops with constant repeat counts outside of constant functions --- tests/sat/counters-repeat.v | 38 ++++++++++++++++++++++++++++++++++++++ tests/sat/counters-repeat.ys | 10 ++++++++++ 2 files changed, 48 insertions(+) create mode 100644 tests/sat/counters-repeat.v create mode 100644 tests/sat/counters-repeat.ys (limited to 'tests') diff --git a/tests/sat/counters-repeat.v b/tests/sat/counters-repeat.v new file mode 100644 index 000000000..2ea45499a --- /dev/null +++ b/tests/sat/counters-repeat.v @@ -0,0 +1,38 @@ +// coverage for repeat loops outside of constant functions + +module counter1(clk, rst, ping); + input clk, rst; + output ping; + reg [31:0] count; + + always @(posedge clk) begin + if (rst) + count <= 0; + else + count <= count + 1; + end + + assign ping = &count; +endmodule + +module counter2(clk, rst, ping); + input clk, rst; + output ping; + reg [31:0] count; + + integer i; + reg carry; + + always @(posedge clk) begin + carry = 1; + i = 0; + repeat (32) begin + count[i] <= !rst & (count[i] ^ carry); + carry = count[i] & carry; + i = i+1; + end + end + + assign ping = &count; +endmodule + diff --git a/tests/sat/counters-repeat.ys b/tests/sat/counters-repeat.ys new file mode 100644 index 000000000..b3dcfe08a --- /dev/null +++ b/tests/sat/counters-repeat.ys @@ -0,0 +1,10 @@ + +read_verilog counters-repeat.v +proc; opt + +expose -shared counter1 counter2 +miter -equiv -make_assert -make_outputs counter1 counter2 miter + +cd miter; flatten; opt +sat -verify -prove-asserts -tempinduct -set-at 1 in_rst 1 -seq 1 -show-inputs -show-outputs + -- cgit v1.2.3 From 4c831d72ef2d3a9f9b91d6fa27e09800ae09e869 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 19 Apr 2019 20:23:09 +0200 Subject: Add test for pmux2shiftx Signed-off-by: Clifford Wolf --- tests/various/pmux2shiftx.v | 28 ++++++++++++++++++++++++++++ tests/various/pmux2shiftx.ys | 24 ++++++++++++++++++++++++ 2 files changed, 52 insertions(+) create mode 100644 tests/various/pmux2shiftx.v create mode 100644 tests/various/pmux2shiftx.ys (limited to 'tests') diff --git a/tests/various/pmux2shiftx.v b/tests/various/pmux2shiftx.v new file mode 100644 index 000000000..ac61c5c0e --- /dev/null +++ b/tests/various/pmux2shiftx.v @@ -0,0 +1,28 @@ +module pmux2shiftx_test ( + input [2:0] S1, + input [5:0] S2, + input [9:0] A, B, C, D, D, E, F, + input [9:0] G, H, I, J, K, L, M, N, + output reg [9:0] X +); + always @* begin + case (S1) + 3'd0: X = A; + 3'd1: X = B; + 3'd2: X = C; + 3'd3: X = D; + 3'd4: X = E; + 3'd5: X = F; + 3'd6: X = G; + 3'd7: X = H; + endcase + case (S2) + 6'd46: X = I; + 6'd47: X = J; + 6'd48: X = K; + 6'd52: X = L; + 6'd53: X = M; + 6'd54: X = N; + endcase + end +endmodule diff --git a/tests/various/pmux2shiftx.ys b/tests/various/pmux2shiftx.ys new file mode 100644 index 000000000..16618ac0a --- /dev/null +++ b/tests/various/pmux2shiftx.ys @@ -0,0 +1,24 @@ +read_verilog pmux2shiftx.v +prep +design -save gold + +pmux2shiftx +opt +# show -width +select -assert-count 1 t:$mux +select -assert-count 1 t:$shift +select -assert-count 2 t:$shiftx +select -assert-count 1 t:$sub +design -stash gate + +design -import gold -as gold +design -import gate -as gate + +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -verify -prove-asserts -show-ports miter + +design -load gold +stat + +design -load gate +stat -- cgit v1.2.3 From 0070184ea9dea56d1dfd8268035bc01a3e340add Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Fri, 19 Apr 2019 23:37:11 +0200 Subject: Improvements in pmux2shiftx Signed-off-by: Clifford Wolf --- tests/various/pmux2shiftx.v | 38 ++++++++++++++++++++++---------------- tests/various/pmux2shiftx.ys | 12 ++++++++---- 2 files changed, 30 insertions(+), 20 deletions(-) (limited to 'tests') diff --git a/tests/various/pmux2shiftx.v b/tests/various/pmux2shiftx.v index ac61c5c0e..fec84187b 100644 --- a/tests/various/pmux2shiftx.v +++ b/tests/various/pmux2shiftx.v @@ -1,28 +1,34 @@ module pmux2shiftx_test ( input [2:0] S1, input [5:0] S2, - input [9:0] A, B, C, D, D, E, F, - input [9:0] G, H, I, J, K, L, M, N, + input [1:0] S3, + input [9:0] A, B, C, D, D, E, F, G, H, + input [9:0] I, J, K, L, M, N, O, P, Q, output reg [9:0] X ); always @* begin case (S1) - 3'd0: X = A; - 3'd1: X = B; - 3'd2: X = C; - 3'd3: X = D; - 3'd4: X = E; - 3'd5: X = F; - 3'd6: X = G; - 3'd7: X = H; + 3'd 0: X = A; + 3'd 1: X = B; + 3'd 2: X = C; + 3'd 3: X = D; + 3'd 4: X = E; + 3'd 5: X = F; + 3'd 6: X = G; + 3'd 7: X = H; endcase case (S2) - 6'd46: X = I; - 6'd47: X = J; - 6'd48: X = K; - 6'd52: X = L; - 6'd53: X = M; - 6'd54: X = N; + 6'd 45: X = I; + 6'd 47: X = J; + 6'd 49: X = K; + 6'd 55: X = L; + 6'd 57: X = M; + 6'd 59: X = N; + endcase + case (S3) + 2'd 1: X = O; + 2'd 2: X = P; + 2'd 3: X = Q; endcase end endmodule diff --git a/tests/various/pmux2shiftx.ys b/tests/various/pmux2shiftx.ys index 16618ac0a..f5e83171c 100644 --- a/tests/various/pmux2shiftx.ys +++ b/tests/various/pmux2shiftx.ys @@ -2,13 +2,17 @@ read_verilog pmux2shiftx.v prep design -save gold -pmux2shiftx +pmux2shiftx -density 70 50 + opt + +stat # show -width -select -assert-count 1 t:$mux -select -assert-count 1 t:$shift -select -assert-count 2 t:$shiftx select -assert-count 1 t:$sub +select -assert-count 2 t:$mux +select -assert-count 2 t:$shift +select -assert-count 3 t:$shiftx + design -stash gate design -import gold -as gold -- cgit v1.2.3 From 37728520a6d559a9f9a0082ddb3d596e8a634d97 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 20 Apr 2019 01:15:48 +0200 Subject: Improvements in "pmux2shiftx" Signed-off-by: Clifford Wolf --- tests/various/pmux2shiftx.ys | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tests') diff --git a/tests/various/pmux2shiftx.ys b/tests/various/pmux2shiftx.ys index f5e83171c..f84ae3869 100644 --- a/tests/various/pmux2shiftx.ys +++ b/tests/various/pmux2shiftx.ys @@ -2,7 +2,7 @@ read_verilog pmux2shiftx.v prep design -save gold -pmux2shiftx -density 70 50 +pmux2shiftx -min_density 70 50 opt -- cgit v1.2.3 From b3a3e08e389c8d10fbd8e0dc8b48e1e559dedf5d Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Sat, 20 Apr 2019 02:03:44 +0200 Subject: Improve "pmux2shiftx" Signed-off-by: Clifford Wolf --- tests/various/pmux2shiftx.ys | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tests') diff --git a/tests/various/pmux2shiftx.ys b/tests/various/pmux2shiftx.ys index f84ae3869..6bb9626eb 100644 --- a/tests/various/pmux2shiftx.ys +++ b/tests/various/pmux2shiftx.ys @@ -2,7 +2,7 @@ read_verilog pmux2shiftx.v prep design -save gold -pmux2shiftx -min_density 70 50 +pmux2shiftx -min_density 70 opt -- cgit v1.2.3 From a80e74dc2057b175a99d5cbc2926b712f0323010 Mon Sep 17 00:00:00 2001 From: Clifford Wolf Date: Mon, 22 Apr 2019 16:17:43 +0200 Subject: Updaye pmux2shiftx test Signed-off-by: Clifford Wolf --- tests/various/pmux2shiftx.ys | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tests') diff --git a/tests/various/pmux2shiftx.ys b/tests/various/pmux2shiftx.ys index 6bb9626eb..deb134083 100644 --- a/tests/various/pmux2shiftx.ys +++ b/tests/various/pmux2shiftx.ys @@ -9,8 +9,8 @@ opt stat # show -width select -assert-count 1 t:$sub -select -assert-count 2 t:$mux -select -assert-count 2 t:$shift +select -assert-count 1 t:$mux +select -assert-count 1 t:$shift select -assert-count 3 t:$shiftx design -stash gate -- cgit v1.2.3