From e41dcaa7594e501d24852ca29e3c699d85c394bf Mon Sep 17 00:00:00 2001
From: Clifford Wolf <clifford@clifford.at>
Date: Thu, 23 Nov 2017 08:28:29 +0100
Subject: Progress with new BTOR backend
---
backends/btor/btor.cc | 117 ++++++++++++++++++++++++++++++++++++++++++++++----
1 file changed, 109 insertions(+), 8 deletions(-)
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc
index ca106d387..77ae34797 100644
--- a/backends/btor/btor.cc
+++ b/backends/btor/btor.cc
@@ -53,6 +53,11 @@ struct BtorWorker
// bit to driving cell
dict<SigBit, Cell*> bit_cell;
+ // nids for constants
+ dict<Const, int> consts;
+
+ pool<Cell*> cell_recursion_guard;
+
int get_bv_sid(int width)
{
if (sorts_bv.count(width) == 0) {
@@ -63,7 +68,57 @@ struct BtorWorker
return sorts_bv.at(width);
}
- int get_sig_nid(SigSpec sig)
+ void export_cell(Cell *cell)
+ {
+ log_assert(cell_recursion_guard.count(cell) == 0);
+ cell_recursion_guard.insert(cell);
+
+ if (cell->type.in("$add", "$sub"))
+ {
+ string btor_op;
+ if (cell->type == "$add") btor_op = "add";
+ if (cell->type == "$sub") btor_op = "sub";
+ log_assert(!btor_op.empty());
+
+ int width = GetSize(cell->getPort("\\Y"));
+ width = std::max(width, GetSize(cell->getPort("\\A")));
+ width = std::max(width, GetSize(cell->getPort("\\B")));
+
+ bool a_signed = cell->hasParam("\\A_SIGNED") ? cell->getParam("\\A_SIGNED").as_bool() : false;
+ bool b_signed = cell->hasParam("\\B_SIGNED") ? cell->getParam("\\B_SIGNED").as_bool() : false;
+
+ int sid = get_bv_sid(width);
+ int nid_a = get_sig_nid(cell->getPort("\\A"), width, a_signed);
+ int nid_b = get_sig_nid(cell->getPort("\\B"), width, b_signed);
+
+ int nid = next_nid++;
+ f << stringf("%d %s %d %d %d\n", nid, btor_op.c_str(), sid, nid_a, nid_b);
+
+ SigSpec sig = sigmap(cell->getPort("\\Y"));
+
+ if (GetSize(sig) < width) {
+ int sid = get_bv_sid(GetSize(sig));
+ int nid2 = next_nid++;
+ f << stringf("%d slice %d %d %d 0\n", nid2, sid, nid, GetSize(sig)-1);
+ nid = nid2;
+ }
+
+ for (int i = 0; i < GetSize(sig); i++)
+ bit_nid[sig[i]] = make_pair(nid, i);
+
+ sig_nid[sig] = nid;
+ nid_width[nid] = GetSize(sig);
+
+ goto okay;
+ }
+
+ log_error("Unsupported cell type: %s\n", log_id(cell));
+
+ okay:
+ cell_recursion_guard.erase(cell);
+ }
+
+ int get_sig_nid(SigSpec sig, int to_width = -1, bool is_signed = false)
{
sigmap.apply(sig);
@@ -79,8 +134,33 @@ struct BtorWorker
if (bit_nid.count(bit) == 0)
{
- // FIXME
- log_abort();
+ if (bit.wire == nullptr)
+ {
+ Const c(bit.data);
+
+ while (i+GetSize(c) < GetSize(sig) && sig[i+GetSize(c)].wire == nullptr)
+ c.bits.push_back(sig[i+GetSize(c)].data);
+
+ if (consts.count(c) == 0) {
+ int sid = get_bv_sid(GetSize(c));
+ int nid = next_nid++;
+ f << stringf("%d const %d %s\n", nid, sid, c.as_string().c_str());
+ consts[c] = nid;
+ }
+
+ int nid = consts.at(c);
+
+ for (int j = 0; j < GetSize(c); j++)
+ nidbits.push_back(make_pair(nid, j));
+
+ i += GetSize(c)-1;
+ continue;
+ }
+ else
+ {
+ export_cell(bit_cell.at(bit));
+ log_assert(bit_nid.count(bit));
+ }
}
nidbits.push_back(bit_nid.at(bit));
@@ -124,7 +204,28 @@ struct BtorWorker
nid_width[nid] = width;
}
- return sig_nid.at(sig);
+ int nid = sig_nid.at(sig);
+
+ if (to_width >= 0 && to_width != GetSize(sig))
+ {
+ if (to_width < GetSize(sig))
+ {
+ int sid = get_bv_sid(to_width);
+ int nid2 = next_nid++;
+ f << stringf("%d slice %d %d %d 0\n", nid2, sid, nid, to_width-1);
+ nid = nid2;
+ }
+ else
+ {
+ int sid = get_bv_sid(to_width);
+ int nid2 = next_nid++;
+ f << stringf("%d %s %d %d %d\n", nid2, is_signed ? "sext" : "uext",
+ sid, nid, to_width - GetSize(sig));
+ nid = nid2;
+ }
+ }
+
+ return nid;
}
BtorWorker(std::ostream &f, RTLIL::Module *module, bool verbose) :
@@ -188,10 +289,10 @@ struct BtorBackend : public Backend {
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
- if (args[argidx] == "-verbose") {
- verbose = true;
- continue;
- }
+ // if (args[argidx] == "-verbose") {
+ // verbose = true;
+ // continue;
+ // }
break;
}
extra_args(f, filename, args, argidx);
--
cgit v1.2.3