Improve BTOR2 handling of undriven wires

Signed-off-by: Clifford Wolf <clifford@clifford.at>

diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 511a1194271cf54ed820087c54cb5e012178b3c4..a507b120b88e7a00012dc17aa582b33898dedc5b 100644 (file)
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -17,6 +17,11 @@
  *
  */
 
+// [[CITE]] Btor2 , BtorMC and Boolector 3.0
+// Aina Niemetz, Mathias Preiner, Clifford Wolf, Armin Biere
+// Computer Aided Verification - 30th International Conference, CAV 2018
+// https://cs.stanford.edu/people/niemetz/publication/2018/niemetzpreinerwolfbiere-cav18/
+
 #include "kernel/rtlil.h"
 #include "kernel/register.h"
 #include "kernel/sigtools.h"
@@ -875,9 +880,28 @@ struct BtorWorker
                                        else
                                        {
                                                if (bit_cell.count(bit) == 0)
-                                                       log_error("No driver for signal bit %s.\n", log_signal(bit));
-                                               export_cell(bit_cell.at(bit));
-                                               log_assert(bit_nid.count(bit));
+                                               {
+                                                       SigSpec s = bit;
+
+                                                       while (i+GetSize(s) < GetSize(sig) && sig[i+GetSize(s)].wire != nullptr &&
+                                                                       bit_cell.count(sig[i+GetSize(s)]) == 0)
+                                                               s.append(sig[i+GetSize(s)]);
+
+                                                       log_warning("No driver for signal %s.\n", log_signal(s));
+
+                                                       int sid = get_bv_sid(GetSize(s));
+                                                       int nid = next_nid++;
+                                                       btorf("%d input %d %s\n", nid, sid);
+                                                       nid_width[nid] = GetSize(s);
+
+                                                       i += GetSize(s)-1;
+                                                       continue;
+                                               }
+                                               else
+                                               {
+                                                       export_cell(bit_cell.at(bit));
+                                                       log_assert(bit_nid.count(bit));
+                                               }
                                        }
                                }