From 0cee66e7591b6315f9e7dce91b789c1f6b53138f Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Wed, 4 Sep 2019 12:34:44 -0700 Subject: Add peepopt_dffmuxext tests --- tests/simple/peepopt.v | 8 ++++++++ 1 file changed, 8 insertions(+) (limited to 'tests') diff --git a/tests/simple/peepopt.v b/tests/simple/peepopt.v index 1bf427897..b4d113dba 100644 --- a/tests/simple/peepopt.v +++ b/tests/simple/peepopt.v @@ -11,3 +11,11 @@ wire [3:0] t; assign t = i * 3; assign o = t / 3; endmodule + +module peepopt_dffmuxext_signed(input clk, ce, input signed [1:0] i, output reg signed [3:0] o); + always @(posedge clk) if (ce) o <= i; +endmodule + +module peepopt_dffmuxext_unsigned(input clk, ce, input [1:0] i, output reg [3:0] o); + always @(posedge clk) if (ce) o <= i; +endmodule -- cgit v1.2.3 From 6fe1ca633d90fb238d2671dba3d7f772c263a497 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Wed, 4 Sep 2019 15:20:04 -0700 Subject: abc9 followed by clean otherwise netlist could be invalid for sim --- tests/simple_abc9/run-test.sh | 1 + 1 file changed, 1 insertion(+) (limited to 'tests') diff --git a/tests/simple_abc9/run-test.sh b/tests/simple_abc9/run-test.sh index 0d4262005..4d15a3253 100755 --- a/tests/simple_abc9/run-test.sh +++ b/tests/simple_abc9/run-test.sh @@ -25,5 +25,6 @@ exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v EXTRA_FLAGS="-n 300 -p '\ synth -run coarse; \ opt -full; \ techmap; abc9 -lut 4 -box ../abc.box; \ + clean; \ check -assert; \ select -assert-none t:${DOLLAR}_NOT_ t:${DOLLAR}_AND_ %%'" -- cgit v1.2.3 From 11f623cbe0057ee752f2545eb7100966afb08676 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 5 Sep 2019 08:25:09 -0700 Subject: Revert "abc9 followed by clean otherwise netlist could be invalid for sim" This reverts commit 6fe1ca633d90fb238d2671dba3d7f772c263a497. --- tests/simple_abc9/run-test.sh | 1 - 1 file changed, 1 deletion(-) (limited to 'tests') diff --git a/tests/simple_abc9/run-test.sh b/tests/simple_abc9/run-test.sh index 4d15a3253..0d4262005 100755 --- a/tests/simple_abc9/run-test.sh +++ b/tests/simple_abc9/run-test.sh @@ -25,6 +25,5 @@ exec ${MAKE:-make} -f ../tools/autotest.mk $seed *.v EXTRA_FLAGS="-n 300 -p '\ synth -run coarse; \ opt -full; \ techmap; abc9 -lut 4 -box ../abc.box; \ - clean; \ check -assert; \ select -assert-none t:${DOLLAR}_NOT_ t:${DOLLAR}_AND_ %%'" -- cgit v1.2.3 From ef0681ea4ca0b34689cbf14d5a4478e2785600d9 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 5 Sep 2019 08:43:22 -0700 Subject: simple/peepopt.v tests to various/peepopt.ys with equiv_opt & select --- tests/simple/peepopt.v | 21 ---------------- tests/various/peepopt.ys | 63 ++++++++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 63 insertions(+), 21 deletions(-) delete mode 100644 tests/simple/peepopt.v create mode 100644 tests/various/peepopt.ys (limited to 'tests') diff --git a/tests/simple/peepopt.v b/tests/simple/peepopt.v deleted file mode 100644 index b4d113dba..000000000 --- a/tests/simple/peepopt.v +++ /dev/null @@ -1,21 +0,0 @@ -module peepopt_shiftmul_0 #(parameter N=3, parameter W=3) (input [N*W-1:0] i, input [$clog2(N)-1:0] s, output [W-1:0] o); -assign o = i[s*W+:W]; -endmodule - -module peepopt_shiftmul_1 (output y, input [2:0] w); -assign y = 1'b1 >> (w * (3'b110)); -endmodule - -module peepopt_muldiv_0(input [1:0] i, output [1:0] o); -wire [3:0] t; -assign t = i * 3; -assign o = t / 3; -endmodule - -module peepopt_dffmuxext_signed(input clk, ce, input signed [1:0] i, output reg signed [3:0] o); - always @(posedge clk) if (ce) o <= i; -endmodule - -module peepopt_dffmuxext_unsigned(input clk, ce, input [1:0] i, output reg [3:0] o); - always @(posedge clk) if (ce) o <= i; -endmodule diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys new file mode 100644 index 000000000..91db22423 --- /dev/null +++ b/tests/various/peepopt.ys @@ -0,0 +1,63 @@ +read_verilog <> (w * (3'b110)); +endmodule +EOT + +prep -nokeepdc +equiv_opt peepopt +design -load postopt +clean +select -assert-count 1 t:$shr +select -assert-count 1 t:$mul +select -assert-count 0 t:$shr t:$mul %% t:* %D + +#################### + +design -reset +read_verilog < Date: Fri, 6 Sep 2019 22:48:04 -0700 Subject: Usee equiv_opt -assert --- tests/various/peepopt.ys | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'tests') diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys index 91db22423..a476133a2 100644 --- a/tests/various/peepopt.ys +++ b/tests/various/peepopt.ys @@ -5,7 +5,7 @@ endmodule EOT prep -nokeepdc -equiv_opt peepopt +equiv_opt -assert peepopt design -load postopt clean select -assert-count 1 t:$shiftx @@ -21,7 +21,7 @@ endmodule EOT prep -nokeepdc -equiv_opt peepopt +equiv_opt -assert peepopt design -load postopt clean select -assert-count 1 t:$shr @@ -40,7 +40,7 @@ endmodule EOT prep -nokeepdc -equiv_opt peepopt +equiv_opt -assert peepopt design -load postopt clean select -assert-count 0 t:* -- cgit v1.2.3 From e2c2d784c8217e4bcf29fb6b156b6a8285036b80 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 6 Sep 2019 22:48:23 -0700 Subject: Make one check $shift(x)? only; change testcase to be 8b --- tests/various/peepopt.ys | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tests') diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys index a476133a2..dcf3cacbd 100644 --- a/tests/various/peepopt.ys +++ b/tests/various/peepopt.ys @@ -16,7 +16,7 @@ select -assert-count 0 t:$shiftx t:* %D design -reset read_verilog <> (w * (3'b110)); +assign y = 1'b1 >> (w * (8'b110)); endmodule EOT @@ -25,7 +25,7 @@ equiv_opt -assert peepopt design -load postopt clean select -assert-count 1 t:$shr -select -assert-count 1 t:$mul +select -assert-count 0 t:$mul select -assert-count 0 t:$shr t:$mul %% t:* %D #################### -- cgit v1.2.3 From 97e1520b13231c8170cec73774eee7a22c5dc065 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 6 Sep 2019 22:50:03 -0700 Subject: Missing equiv_opt -assert --- tests/various/peepopt.ys | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tests') diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys index dcf3cacbd..33555264d 100644 --- a/tests/various/peepopt.ys +++ b/tests/various/peepopt.ys @@ -55,7 +55,7 @@ endmodule EOT prep -nokeepdc -equiv_opt peepopt +equiv_opt -assert peepopt design -load postopt clean select -assert-count 1 t:$dff r:WIDTH=2 %i -- cgit v1.2.3 From 580faae8ad608981ef6ef6a99ca6b771dc0368ae Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Wed, 11 Sep 2019 00:07:17 -0700 Subject: Add unsigned case --- tests/various/peepopt.ys | 17 +++++++++++++++++ 1 file changed, 17 insertions(+) (limited to 'tests') diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys index 33555264d..e930015a4 100644 --- a/tests/various/peepopt.ys +++ b/tests/various/peepopt.ys @@ -47,6 +47,23 @@ select -assert-count 0 t:* #################### +design -reset +read_verilog < Date: Wed, 11 Sep 2019 00:14:06 -0700 Subject: proc instead of prep --- tests/various/peepopt.ys | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tests') diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys index e930015a4..2a660d5c9 100644 --- a/tests/various/peepopt.ys +++ b/tests/various/peepopt.ys @@ -54,7 +54,7 @@ module peepopt_dffmuxext_unsigned(input clk, ce, input [1:0] i, output reg [3:0] endmodule EOT -prep -nokeepdc +proc equiv_opt -assert peepopt design -load postopt clean @@ -71,7 +71,7 @@ module peepopt_dffmuxext_signed(input clk, ce, input signed [1:0] i, output reg endmodule EOT -prep -nokeepdc +proc equiv_opt -assert peepopt design -load postopt clean -- cgit v1.2.3 From f46ef47893b4d2cb01fc5914fe0ee89d206f686f Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Wed, 11 Sep 2019 13:22:41 -0700 Subject: Add more tests --- tests/various/peepopt.ys | 32 ++++++++++++++++++++++++++++++++ 1 file changed, 32 insertions(+) (limited to 'tests') diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys index 2a660d5c9..8dce679ff 100644 --- a/tests/various/peepopt.ys +++ b/tests/various/peepopt.ys @@ -78,3 +78,35 @@ clean select -assert-count 1 t:$dff r:WIDTH=2 %i select -assert-count 1 t:$mux r:WIDTH=2 %i select -assert-count 0 t:$dff t:$mux %% t:* %D + +################### + +design -reset +read_verilog < Date: Wed, 11 Sep 2019 13:36:37 -0700 Subject: Cope with presence of reset muxes too --- tests/various/peepopt.ys | 39 +++++++++++++++++++++++++++++++++++++++ 1 file changed, 39 insertions(+) (limited to 'tests') diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys index 8dce679ff..886c8cd9d 100644 --- a/tests/various/peepopt.ys +++ b/tests/various/peepopt.ys @@ -110,3 +110,42 @@ design -load postopt select -assert-count 1 t:$dff r:WIDTH=5 %i select -assert-count 1 t:$mux r:WIDTH=5 %i select -assert-count 0 t:$dff t:$mux %% t:* %D + +#################### + +design -reset +read_verilog < Date: Fri, 13 Sep 2019 16:33:18 -0700 Subject: Revert "Make one check $shift(x)? only; change testcase to be 8b" This reverts commit e2c2d784c8217e4bcf29fb6b156b6a8285036b80. --- tests/various/peepopt.ys | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'tests') diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys index 886c8cd9d..abee9cc0a 100644 --- a/tests/various/peepopt.ys +++ b/tests/various/peepopt.ys @@ -16,7 +16,7 @@ select -assert-count 0 t:$shiftx t:* %D design -reset read_verilog <> (w * (8'b110)); +assign y = 1'b1 >> (w * (3'b110)); endmodule EOT @@ -25,7 +25,7 @@ equiv_opt -assert peepopt design -load postopt clean select -assert-count 1 t:$shr -select -assert-count 0 t:$mul +select -assert-count 1 t:$mul select -assert-count 0 t:$shr t:$mul %% t:* %D #################### -- cgit v1.2.3 From a2eee9ebefc6e8089c815b4355bc64d1ac3396b5 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Fri, 13 Sep 2019 16:41:10 -0700 Subject: Add counter-example from @cliffordwolf --- tests/various/peepopt.ys | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) (limited to 'tests') diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys index abee9cc0a..7c1c3b5bc 100644 --- a/tests/various/peepopt.ys +++ b/tests/various/peepopt.ys @@ -30,6 +30,30 @@ select -assert-count 0 t:$shr t:$mul %% t:* %D #################### +design -reset +read_verilog <> (S*3); +endmodule +EOT + +prep +design -save gold +peepopt +design -stash gate + +design -import gold -as gold peepopt_shiftmul_2 +design -import gate -as gate peepopt_shiftmul_2 + +miter -equiv -make_assert -make_outputs -ignore_gold_x -flatten gold gate miter +sat -show-public -enable_undef -prove-asserts miter +select -assert-count 1 t:$shr +select -assert-count 1 t:$mul +select -assert-count 0 t:$shr t:$mul %% t:* %D +exit + +#################### + design -reset read_verilog < Date: Fri, 13 Sep 2019 18:19:07 -0700 Subject: Oops --- tests/various/peepopt.ys | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'tests') diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys index 7c1c3b5bc..6bca62e2b 100644 --- a/tests/various/peepopt.ys +++ b/tests/various/peepopt.ys @@ -47,10 +47,10 @@ design -import gate -as gate peepopt_shiftmul_2 miter -equiv -make_assert -make_outputs -ignore_gold_x -flatten gold gate miter sat -show-public -enable_undef -prove-asserts miter +cd gate select -assert-count 1 t:$shr select -assert-count 1 t:$mul select -assert-count 0 t:$shr t:$mul %% t:* %D -exit #################### -- cgit v1.2.3