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(+) 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 16:08:46 -0700 Subject: Be mindful that sigmap(wire) could have dupes when checking \init --- passes/sat/sat.cc | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/passes/sat/sat.cc b/passes/sat/sat.cc index 430bba1e8..93a4f225e 100644 --- a/passes/sat/sat.cc +++ b/passes/sat/sat.cc @@ -265,15 +265,18 @@ struct SatHelper RTLIL::SigSpec rhs = it.second->attributes.at("\\init"); log_assert(lhs.size() == rhs.size()); + dict seen_init; RTLIL::SigSpec removed_bits; for (int i = 0; i < lhs.size(); i++) { RTLIL::SigSpec bit = lhs.extract(i, 1); - if (rhs[i] == State::Sx || !satgen.initial_state.check_all(bit)) { + if (rhs[i] == State::Sx || !satgen.initial_state.check_all(bit) || seen_init.at(bit, rhs[i]) != rhs[i]) { removed_bits.append(bit); lhs.remove(i, 1); rhs.remove(i, 1); i--; } + else + seen_init[bit] = rhs[i]; } if (removed_bits.size()) -- cgit v1.2.3 From e730a595eeee1d9936a892c2477c99593d64bcfe Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Wed, 2 Oct 2019 17:48:55 -0700 Subject: Add test --- tests/various/peepopt.ys | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) 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 17:53:42 -0700 Subject: Refactor peepopt_dffmux and be sensitive to \init when trimming --- passes/pmgen/peepopt_dffmux.pmg | 95 +++++++++++++++++++++++++++-------------- 1 file changed, 63 insertions(+), 32 deletions(-) diff --git a/passes/pmgen/peepopt_dffmux.pmg b/passes/pmgen/peepopt_dffmux.pmg index c88a52226..2ec504cb4 100644 --- a/passes/pmgen/peepopt_dffmux.pmg +++ b/passes/pmgen/peepopt_dffmux.pmg @@ -8,21 +8,23 @@ match dff select GetSize(port(dff, \D)) > 1 endmatch +code sigD + sigD = port(dff, \D); +endcode + match rstmux select rstmux->type == $mux select GetSize(port(rstmux, \Y)) > 1 - index port(rstmux, \Y) === port(dff, \D) + index port(rstmux, \Y) === sigD choice BA {\B, \A} select port(rstmux, BA).is_fully_const() set rstmuxBA BA - optional + semioptional endmatch code sigD if (rstmux) sigD = port(rstmux, rstmuxBA == \B ? \A : \B); - else - sigD = port(dff, \D); endcode match cemux @@ -32,45 +34,70 @@ match cemux choice AB {\A, \B} index port(cemux, AB) === port(dff, \Q) set cemuxAB AB + semioptional endmatch code - SigSpec D = port(cemux, cemuxAB == \A ? \B : \A); - SigSpec Q = port(dff, \Q); + if (!cemux && !rstmux) + reject; +endcode + +code Const rst; - if (rstmux) + SigSpec D; + if (cemux) { + D = port(cemux, cemuxAB == \A ? \B : \A); + if (rstmux) + rst = port(rstmux, rstmuxBA).as_const(); + else + rst = Const(State::Sx, GetSize(D)); + } + else { + log_assert(rstmux); + D = port(rstmux, rstmuxBA == \B ? \A : \B); rst = port(rstmux, rstmuxBA).as_const(); + } + SigSpec Q = port(dff, \Q); int width = GetSize(D); - SigSpec &ceA = cemux->connections_.at(\A); - SigSpec &ceB = cemux->connections_.at(\B); - SigSpec &ceY = cemux->connections_.at(\Y); SigSpec &dffD = dff->connections_.at(\D); SigSpec &dffQ = dff->connections_.at(\Q); + Const init; + for (const auto &b : Q) { + auto it = b.wire->attributes.find(\init); + init.bits.push_back(it == b.wire->attributes.end() ? State::Sx : it->second[b.offset]); + } - if (D[width-1] == D[width-2]) { - did_something = true; + auto cmpx = [=](State lhs, State rhs) { + if (lhs == State::Sx || rhs == State::Sx) + return true; + return lhs == rhs; + }; - SigBit sign = D[width-1]; - bool is_signed = sign.wire; - int i; - for (i = width-1; i >= 2; i--) { - if (!is_signed) { - module->connect(Q[i], sign); - if (D[i-1] != sign || (rst.size() && rst[i-1] != rst[width-1])) - break; - } - else { - module->connect(Q[i], Q[i-1]); - if (D[i-2] != sign || (rst.size() && rst[i-1] != rst[width-1])) - break; - } + int i = width; + while (i > 2) { + i--; + if (D[i] != D[i-1]) + break; + if (!cmpx(rst[i], rst[i-1])) + break; + if (!cmpx(init[i], init[i-1])) + break; + if (!cmpx(rst[i], init[i])) + break; + module->connect(Q[i], Q[i-1]); + did_something = true; + } + if (i < width-1) { + if (cemux) { + SigSpec &ceA = cemux->connections_.at(\A); + SigSpec &ceB = cemux->connections_.at(\B); + SigSpec &ceY = cemux->connections_.at(\Y); + ceA.remove(i, width-i); + ceB.remove(i, width-i); + ceY.remove(i, width-i); + cemux->fixup_parameters(); } - - ceA.remove(i, width-i); - ceB.remove(i, width-i); - ceY.remove(i, width-i); - cemux->fixup_parameters(); dffD.remove(i, width-i); dffQ.remove(i, width-i); dff->fixup_parameters(); @@ -78,7 +105,11 @@ code log("dffcemux pattern in %s: dff=%s, cemux=%s; removed top %d bits.\n", log_id(module), log_id(dff), log_id(cemux), width-i); accept; } - else { + else if (cemux) { + SigSpec &ceA = cemux->connections_.at(\A); + SigSpec &ceB = cemux->connections_.at(\B); + SigSpec &ceY = cemux->connections_.at(\Y); + int count = 0; for (int i = width-1; i >= 0; i--) { if (D[i].wire) -- cgit v1.2.3 From f6fabc8fda1eb00b0227f1a91d85b837a0609728 Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Wed, 2 Oct 2019 18:03:45 -0700 Subject: Update test --- tests/various/peepopt.ys | 16 +++------------- 1 file changed, 3 insertions(+), 13 deletions(-) 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(-) 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 --- passes/pmgen/peepopt_dffmux.pmg | 49 ++++++++++++++++++++++------------------- tests/various/peepopt.ys | 4 ++-- 2 files changed, 28 insertions(+), 25 deletions(-) diff --git a/passes/pmgen/peepopt_dffmux.pmg b/passes/pmgen/peepopt_dffmux.pmg index 2ec504cb4..bfd155c58 100644 --- a/passes/pmgen/peepopt_dffmux.pmg +++ b/passes/pmgen/peepopt_dffmux.pmg @@ -74,9 +74,9 @@ code return lhs == rhs; }; - int i = width; - while (i > 2) { - i--; + int i = width-1; + while (i > 1) { + log_dump(i, D[i], D[i-1], rst[i], rst[i-1], init[i], init[i-1]); if (D[i] != D[i-1]) break; if (!cmpx(rst[i], rst[i-1])) @@ -86,26 +86,36 @@ code if (!cmpx(rst[i], init[i])) break; module->connect(Q[i], Q[i-1]); - did_something = true; + i--; } if (i < width-1) { + did_something = true; if (cemux) { SigSpec &ceA = cemux->connections_.at(\A); SigSpec &ceB = cemux->connections_.at(\B); SigSpec &ceY = cemux->connections_.at(\Y); - ceA.remove(i, width-i); - ceB.remove(i, width-i); - ceY.remove(i, width-i); + ceA.remove(i, width-1-i); + ceB.remove(i, width-1-i); + ceY.remove(i, width-1-i); cemux->fixup_parameters(); } - dffD.remove(i, width-i); - dffQ.remove(i, width-i); + if (rstmux) { + SigSpec &rstA = rstmux->connections_.at(\A); + SigSpec &rstB = rstmux->connections_.at(\B); + SigSpec &rstY = rstmux->connections_.at(\Y); + rstA.remove(i, width-1-i); + rstB.remove(i, width-1-i); + rstY.remove(i, width-1-i); + rstmux->fixup_parameters(); + } + dffD.remove(i, width-1-i); + dffQ.remove(i, width-1-i); dff->fixup_parameters(); - log("dffcemux pattern in %s: dff=%s, cemux=%s; removed top %d bits.\n", log_id(module), log_id(dff), log_id(cemux), width-i); - accept; + log("dffcemux pattern in %s: dff=%s, cemux=%s, rstmux=%s; removed top %d bits.\n", log_id(module), log_id(dff), log_id(cemux, "n/a"), log_id(rstmux, "n/a"), width-1-i); + width = i+1; } - else if (cemux) { + if (cemux) { SigSpec &ceA = cemux->connections_.at(\A); SigSpec &ceB = cemux->connections_.at(\B); SigSpec &ceY = cemux->connections_.at(\Y); @@ -114,15 +124,7 @@ code for (int i = width-1; i >= 0; i--) { if (D[i].wire) continue; - Wire *w = Q[i].wire; - auto it = w->attributes.find(\init); - State init; - if (it != w->attributes.end()) - init = it->second[Q[i].offset]; - else - init = State::Sx; - - if (init == State::Sx || init == D[i].data) { + if (cmpx(rst[i], D[i].data) && cmpx(init[i], D[i].data)) { count++; module->connect(Q[i], D[i]); ceA.remove(i); @@ -136,9 +138,10 @@ code did_something = true; cemux->fixup_parameters(); dff->fixup_parameters(); - log("dffcemux pattern in %s: dff=%s, cemux=%s; removed %d constant bits.\n", log_id(module), log_id(dff), log_id(cemux), count); + log("dffcemux pattern in %s: dff=%s, cemux=%s, rstmux=%s; removed %d constant bits.\n", log_id(module), log_id(dff), log_id(cemux), log_id(rstmux, "n/a"), count); } + } + if (did_something) accept; - } endcode 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 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(-) 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