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

diff --git a/passes/equiv/equiv_induct.cc b/passes/equiv/equiv_induct.cc
index 596c938fc08f119f81942e37c7c4ad5be56f5470..37aec50cd42d8f7ba89b5b461d04539c93887af7 100644 (file)
--- 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 (file)
index 0000000..5d2c60d
--- /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