summaryrefslogtreecommitdiff
path: root/backends/btor
diff options
context:
space:
mode:
authorRuben Undheim <ruben.undheim@gmail.com>2019-10-18 19:56:51 +0000
committerRuben Undheim <ruben.undheim@gmail.com>2019-10-18 19:56:51 +0000
commit1f6bb85359149a016811e7e7fef980c3d45211e7 (patch)
tree749672f9a104cbfb25bb02acad6cb731724b9d56 /backends/btor
parentff5734b20220e6fb4a3913cf5279ed94bb5156ea (diff)
New upstream version 0.9
Diffstat (limited to 'backends/btor')
-rw-r--r--backends/btor/btor.cc40
1 files changed, 35 insertions, 5 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index 55c49499..a507b120 100644
--- 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"
@@ -129,7 +134,13 @@ struct BtorWorker
void export_cell(Cell *cell)
{
- log_assert(cell_recursion_guard.count(cell) == 0);
+ if (cell_recursion_guard.count(cell)) {
+ string cell_list;
+ for (auto c : cell_recursion_guard)
+ cell_list += stringf("\n %s", log_id(c));
+ log_error("Found topological loop while processing cell %s. Active cells:%s\n", log_id(cell), cell_list.c_str());
+ }
+
cell_recursion_guard.insert(cell);
btorf_push(log_id(cell));
@@ -340,7 +351,7 @@ struct BtorWorker
if (cell->type == "$lt") btor_op = "lt";
if (cell->type == "$le") btor_op = "lte";
if (cell->type.in("$eq", "$eqx")) btor_op = "eq";
- if (cell->type.in("$ne", "$nex")) btor_op = "ne";
+ if (cell->type.in("$ne", "$nex")) btor_op = "neq";
if (cell->type == "$ge") btor_op = "gte";
if (cell->type == "$gt") btor_op = "gt";
log_assert(!btor_op.empty());
@@ -869,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));
+ }
}
}