From c28d4b804720c2cf0086e921748219150e9631b5 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Wed, 2 Oct 2019 14:52:40 -0700 Subject: Add test that is expecting to fail --- tests/sat/initval.ys | 20 ++++++++++++++++++++ 1 file changed, 20 insertions(+) (limited to 'tests') diff --git a/tests/sat/initval.ys b/tests/sat/initval.ys index 2079d2f34..1627a37e3 100644 --- a/tests/sat/initval.ys +++ b/tests/sat/initval.ys @@ -2,3 +2,23 @@ read_verilog -sv initval.v proc;; sat -seq 10 -prove-asserts + +read_verilog < Date: Wed, 2 Oct 2019 17:48:55 -0700 Subject: Add test --- tests/various/peepopt.ys | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) (limited to 'tests') diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys index 6bca62e2b..dc0acf3ca 100644 --- a/tests/various/peepopt.ys +++ b/tests/various/peepopt.ys @@ -173,3 +173,34 @@ select -assert-count 1 t:$dff r:WIDTH=2 %i select -assert-count 2 t:$mux select -assert-count 2 t:$mux r:WIDTH=2 %i select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D + +#################### + +design -reset +read_verilog < Date: Wed, 2 Oct 2019 18:03:45 -0700 Subject: Update test --- tests/various/peepopt.ys | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) (limited to 'tests') diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys index dc0acf3ca..734a22408 100644 --- a/tests/various/peepopt.ys +++ b/tests/various/peepopt.ys @@ -188,19 +188,9 @@ endmodule EOT proc -#equiv_opt -assert peepopt - -design -save gold -peepopt -design -stash gate -design -import gold -as gold -design -import gate -as gate -miter -equiv -flatten -make_assert -make_outputs gold gate miter -sat -seq 1 -verify -prove-asserts -show-ports miter - +equiv_opt -assert peepopt design -load postopt -wreduce -select -assert-count 1 t:$dff r:WIDTH=2 %i +select -assert-count 1 t:$dff r:WIDTH=4 %i select -assert-count 2 t:$mux -select -assert-count 2 t:$mux r:WIDTH=2 %i +select -assert-count 2 t:$mux r:WIDTH=4 %i select -assert-count 0 t:$logic_not t:$dff t:$mux %% t:* %D -- cgit v1.2.3 From e4bd5aaebf7e329236b10c93eac9ad113231f00e Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Wed, 2 Oct 2019 18:12:25 -0700 Subject: Fix test --- tests/various/peepopt.ys | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) (limited to 'tests') diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys index 734a22408..1f18f1c74 100644 --- a/tests/various/peepopt.ys +++ b/tests/various/peepopt.ys @@ -188,8 +188,18 @@ endmodule EOT proc -equiv_opt -assert peepopt -design -load postopt +#equiv_opt -assert peepopt + +design -save gold +peepopt +wreduce +design -stash gate +design -import gold -as gold +design -import gate -as gate +miter -equiv -flatten -make_assert -make_outputs gold gate miter +sat -seq 1 -verify -prove-asserts -show-ports miter + +design -load gate select -assert-count 1 t:$dff r:WIDTH=4 %i select -assert-count 2 t:$mux select -assert-count 2 t:$mux r:WIDTH=4 %i -- cgit v1.2.3 From e9645c7fa7fc349afad103ff8736699bb4dc0412 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Wed, 2 Oct 2019 21:26:26 -0700 Subject: Fix broken CI, check reset even for constants, trim rstmux --- 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 1f18f1c74..4b130578b 100644 --- a/tests/various/peepopt.ys +++ b/tests/various/peepopt.ys @@ -131,8 +131,8 @@ EOT proc equiv_opt -assert peepopt 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 1 t:$dff r:WIDTH=4 %i +select -assert-count 1 t:$mux r:WIDTH=4 %i select -assert-count 0 t:$dff t:$mux %% t:* %D #################### -- cgit v1.2.3 From 5d680590d6bccd929ed3909248dbb73fb3876e65 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 3 Oct 2019 10:30:33 -0700 Subject: Use equiv_opt -async2sync for xilinx --- tests/xilinx/latches.ys | 4 +--- 1 file changed, 1 insertion(+), 3 deletions(-) (limited to 'tests') diff --git a/tests/xilinx/latches.ys b/tests/xilinx/latches.ys index ac1102896..bd1dffd21 100644 --- a/tests/xilinx/latches.ys +++ b/tests/xilinx/latches.ys @@ -2,9 +2,7 @@ read_verilog latches.v proc flatten -equiv_opt -assert -run :prove -map +/xilinx/cells_sim.v synth_xilinx # equivalency check -async2sync -equiv_opt -assert -run prove: -map +/xilinx/cells_sim.v synth_xilinx # equivalency check +equiv_opt -async2sync -assert -map +/xilinx/cells_sim.v synth_xilinx # equivalency check design -load preopt synth_xilinx -- cgit v1.2.3 From bd5889640bbcbb11c80360893fcf17d9399cef8a Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 3 Oct 2019 10:45:53 -0700 Subject: Disable equiv check for ice40 latches --- tests/ice40/latches.ys | 9 +++------ 1 file changed, 3 insertions(+), 6 deletions(-) (limited to 'tests') diff --git a/tests/ice40/latches.ys b/tests/ice40/latches.ys index f3562559e..708734e44 100644 --- a/tests/ice40/latches.ys +++ b/tests/ice40/latches.ys @@ -1,14 +1,11 @@ read_verilog latches.v -design -save read proc -async2sync # converts latches to a 'sync' variant clocked by a 'super'-clock flatten -synth_ice40 -equiv_opt -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check -design -load postopt # load the post-opt design (otherwise equiv_opt loads the pre-opt design) +# Can't run any sort of equivalence check because latches are blown to LUTs +#equiv_opt -async2sync -assert -map +/ice40/cells_sim.v synth_ice40 # equivalency check -design -load read +#design -load preopt synth_ice40 cd top select -assert-count 4 t:SB_LUT4 -- cgit v1.2.3 From 045f34403889b69f3ac3ac08d96e5cf1fae787d1 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Thu, 3 Oct 2019 11:11:50 -0700 Subject: Use `sat -tempinduct` and comments for why equiv_opt not sufficient --- tests/various/peepopt.ys | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) (limited to 'tests') diff --git a/tests/various/peepopt.ys b/tests/various/peepopt.ys index 4b130578b..ee5ad8a1a 100644 --- a/tests/various/peepopt.ys +++ b/tests/various/peepopt.ys @@ -188,6 +188,13 @@ endmodule EOT proc +# NB: equiv_opt uses equiv_induct which covers +# only the induction half of temporal induction +# --- missing the base-case half +# This makes it akin to `sat -tempinduct-inductonly` +# instead of `sat -tempinduct-baseonly` or +# `sat -tempinduct` which is necessary for this +# testcase #equiv_opt -assert peepopt design -save gold @@ -197,7 +204,7 @@ design -stash gate design -import gold -as gold design -import gate -as gate miter -equiv -flatten -make_assert -make_outputs gold gate miter -sat -seq 1 -verify -prove-asserts -show-ports miter +sat -tempinduct -verify -prove-asserts -show-ports miter design -load gate select -assert-count 1 t:$dff r:WIDTH=4 %i -- cgit v1.2.3 From 5c68da4150f8e5367138f2c7187f707b20cc19db Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Sat, 5 Oct 2019 09:27:12 -0700 Subject: Missing 'accept' at end of ice40_wrapcarry, spotted by @cliffordwolf --- tests/ice40/wrapcarry.ys | 22 ++++++++++++++++++++++ 1 file changed, 22 insertions(+) create mode 100644 tests/ice40/wrapcarry.ys (limited to 'tests') diff --git a/tests/ice40/wrapcarry.ys b/tests/ice40/wrapcarry.ys new file mode 100644 index 000000000..10c029e68 --- /dev/null +++ b/tests/ice40/wrapcarry.ys @@ -0,0 +1,22 @@ +read_verilog < Date: Tue, 8 Oct 2019 12:41:26 -0700 Subject: Revert "Add test that is expecting to fail" This reverts commit c28d4b804720c2cf0086e921748219150e9631b5. --- tests/sat/initval.ys | 20 -------------------- 1 file changed, 20 deletions(-) (limited to 'tests') diff --git a/tests/sat/initval.ys b/tests/sat/initval.ys index 1627a37e3..2079d2f34 100644 --- a/tests/sat/initval.ys +++ b/tests/sat/initval.ys @@ -2,23 +2,3 @@ read_verilog -sv initval.v proc;; sat -seq 10 -prove-asserts - -read_verilog <