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

1 files changed, 35 insertions, 0 deletions

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