diff options
| author | clairexen <claire@symbioticeda.com> | 2020-07-28 12:56:22 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-28 12:56:22 +0200 |
| commit | 66afed6f55be9c32eb2a1eef921633b302efa9c4 (patch) | |
| tree | 3bd90b24e40dd45430bb2e67b99130c8c5fe11b5 | |
| parent | a2fb84fd0c5f57b601b6a3c4cee0b409d74b5d21 (diff) | |
| parent | a1a0abf52afe397e11b63bfc67e82aaf7bf9f498 (diff) | |
| download | yosys-66afed6f55be9c32eb2a1eef921633b302efa9c4.tar.gz yosys-66afed6f55be9c32eb2a1eef921633b302efa9c4.tar.bz2 yosys-66afed6f55be9c32eb2a1eef921633b302efa9c4.zip | |
Merge pull request #2306 from YosysHQ/mwk/equiv_induct-undef
equiv_induct: Fix up assumption for $equiv cells in -undef mode.
| -rw-r--r-- | passes/equiv/equiv_induct.cc | 4 | ||||
| -rw-r--r-- | tests/various/equiv_opt_undef.ys | 35 |
2 files changed, 38 insertions, 1 deletions
diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc index 596c938fc..37aec50cd 100644 --- a/passes/equiv/equiv_induct.cc +++ b/passes/equiv/equiv_induct.cc @@ -65,8 +65,10 @@ struct EquivInductWorker int ez_a = satgen.importSigBit(bit_a, step); int ez_b = satgen.importSigBit(bit_b, step); int cond = ez->IFF(ez_a, ez_b); - if (satgen.model_undef) + if (satgen.model_undef) { + cond = ez->AND(cond, ez->NOT(satgen.importUndefSigBit(bit_b, step))); cond = ez->OR(cond, satgen.importUndefSigBit(bit_a, step)); + } ez_equal_terms.push_back(cond); } } diff --git a/tests/various/equiv_opt_undef.ys b/tests/various/equiv_opt_undef.ys new file mode 100644 index 000000000..5d2c60d0a --- /dev/null +++ b/tests/various/equiv_opt_undef.ys @@ -0,0 +1,35 @@ +read_ilang << EOT + +module \top + wire $a + wire $b + wire input 1 \D + wire input 2 \EN + wire output 3 \Q + cell $mux $x + parameter \WIDTH 1 + connect \A \Q + connect \B \D + connect \S \EN + connect \Y $a + end + cell $ff $y + parameter \WIDTH 1 + connect \D $a + connect \Q $b + end + cell $and $z + parameter \A_SIGNED 0 + parameter \A_WIDTH 1 + parameter \B_SIGNED 0 + parameter \B_WIDTH 1 + parameter \Y_WIDTH 1 + connect \A $b + connect \B 1'x + connect \Y \Q + end +end + +EOT + +equiv_opt -assert -undef ls |