equiv_induct: Fix up assumption for $equiv cells in -undef mode.

Before this fix, equiv_induct only assumed that one of the following is
true:

- defined value of A is equal to defined value of B
- A is undefined

This lets through valuations where A is defined, B is undefined, and
the defined (meaningless) value of B happens to match the defined value
of A.  Instead, tighten this up to OR of the following:

- defined value of A is equal to defined value of B, and B is not
  undefined
- A is undefined

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