summaryrefslogtreecommitdiff
path: root/backends/smt2
diff options
context:
space:
mode:
Diffstat (limited to 'backends/smt2')
-rw-r--r--backends/smt2/smt2.cc237
1 files changed, 157 insertions, 80 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 3d872c63..af3d0ad3 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -32,7 +32,7 @@ struct Smt2Worker
CellTypes ct;
SigMap sigmap;
RTLIL::Module *module;
- bool bvmode, verbose;
+ bool bvmode, memmode, verbose;
int idcounter;
std::vector<std::string> decls, trans;
@@ -41,10 +41,11 @@ struct Smt2Worker
pool<Cell*> recursive_cells, registers;
std::map<RTLIL::SigBit, std::pair<int, int>> fcache;
+ std::map<Cell*, int> memarrays;
std::map<int, int> bvsizes;
- Smt2Worker(RTLIL::Module *module, bool bvmode, bool verbose) :
- ct(module->design), sigmap(module), module(module), bvmode(bvmode), verbose(verbose), idcounter(0)
+ Smt2Worker(RTLIL::Module *module, bool bvmode, bool memmode, bool verbose) :
+ ct(module->design), sigmap(module), module(module), bvmode(bvmode), memmode(memmode), verbose(verbose), idcounter(0)
{
decls.push_back(stringf("(declare-sort |%s_s| 0)\n", log_id(module)));
@@ -316,6 +317,7 @@ struct Smt2Worker
if (exported_cells.count(cell))
return;
+
exported_cells.insert(cell);
recursive_cells.insert(cell);
@@ -345,89 +347,121 @@ struct Smt2Worker
// FIXME: $lut
- if (!bvmode)
- log_error("Unsupported cell type %s for cell %s.%s. (Maybe this cell type would be supported in -bv mode?)\n",
- log_id(cell->type), log_id(module), log_id(cell));
-
- if (cell->type == "$dff")
+ if (bvmode)
{
- registers.insert(cell);
- decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
- log_id(module), idcounter, log_id(module), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q"))));
- register_bv(cell->getPort("\\Q"), idcounter++);
- recursive_cells.erase(cell);
- return;
+ if (cell->type == "$dff")
+ {
+ registers.insert(cell);
+ decls.push_back(stringf("(declare-fun |%s#%d| (|%s_s|) (_ BitVec %d)) ; %s\n",
+ log_id(module), idcounter, log_id(module), GetSize(cell->getPort("\\Q")), log_signal(cell->getPort("\\Q"))));
+ register_bv(cell->getPort("\\Q"), idcounter++);
+ recursive_cells.erase(cell);
+ return;
+ }
+
+ if (cell->type == "$and") return export_bvop(cell, "(bvand A B)");
+ if (cell->type == "$or") return export_bvop(cell, "(bvor A B)");
+ if (cell->type == "$xor") return export_bvop(cell, "(bvxor A B)");
+ if (cell->type == "$xnor") return export_bvop(cell, "(bvxnor A B)");
+
+ if (cell->type == "$shl") return export_bvop(cell, "(bvshl A B)", 's');
+ if (cell->type == "$shr") return export_bvop(cell, "(bvlshr A B)", 's');
+ if (cell->type == "$sshl") return export_bvop(cell, "(bvshl A B)", 's');
+ if (cell->type == "$sshr") return export_bvop(cell, "(bvLshr A B)", 's');
+
+ // FIXME: $shift $shiftx
+
+ if (cell->type == "$lt") return export_bvop(cell, "(bvUlt A B)", 'b');
+ if (cell->type == "$le") return export_bvop(cell, "(bvUle A B)", 'b');
+ if (cell->type == "$ge") return export_bvop(cell, "(bvUge A B)", 'b');
+ if (cell->type == "$gt") return export_bvop(cell, "(bvUgt A B)", 'b');
+
+ if (cell->type == "$ne") return export_bvop(cell, "(distinct A B)", 'b');
+ if (cell->type == "$nex") return export_bvop(cell, "(distinct A B)", 'b');
+ if (cell->type == "$eq") return export_bvop(cell, "(= A B)", 'b');
+ if (cell->type == "$eqx") return export_bvop(cell, "(= A B)", 'b');
+
+ if (cell->type == "$not") return export_bvop(cell, "(bvnot A)");
+ if (cell->type == "$pos") return export_bvop(cell, "A");
+ if (cell->type == "$neg") return export_bvop(cell, "(bvneg A)");
+
+ if (cell->type == "$add") return export_bvop(cell, "(bvadd A B)");
+ if (cell->type == "$sub") return export_bvop(cell, "(bvsub A B)");
+ if (cell->type == "$mul") return export_bvop(cell, "(bvmul A B)");
+ if (cell->type == "$div") return export_bvop(cell, "(bvUdiv A B)", 'd');
+ if (cell->type == "$mod") return export_bvop(cell, "(bvUrem A B)", 'd');
+
+ if (cell->type == "$reduce_and") return export_reduce(cell, "(and A)", true);
+ if (cell->type == "$reduce_or") return export_reduce(cell, "(or A)", false);
+ if (cell->type == "$reduce_xor") return export_reduce(cell, "(xor A)", false);
+ if (cell->type == "$reduce_xnor") return export_reduce(cell, "(not (xor A))", false);
+ if (cell->type == "$reduce_bool") return export_reduce(cell, "(or A)", false);
+
+ if (cell->type == "$logic_not") return export_reduce(cell, "(not (or A))", false);
+ if (cell->type == "$logic_and") return export_reduce(cell, "(and (or A) (or B))", false);
+ if (cell->type == "$logic_or") return export_reduce(cell, "(or A B)", false);
+
+ if (cell->type == "$mux" || cell->type == "$pmux")
+ {
+ int width = GetSize(cell->getPort("\\Y"));
+ std::string processed_expr = get_bv(cell->getPort("\\A"));
+
+ RTLIL::SigSpec sig_b = cell->getPort("\\B");
+ RTLIL::SigSpec sig_s = cell->getPort("\\S");
+ get_bv(sig_b);
+ get_bv(sig_s);
+
+ for (int i = 0; i < GetSize(sig_s); i++)
+ processed_expr = stringf("(ite %s %s %s)", get_bool(sig_s[i]).c_str(),
+ get_bv(sig_b.extract(i*width, width)).c_str(), processed_expr.c_str());
+
+ if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "",
+ log_id(cell));
+ RTLIL::SigSpec sig = sigmap(cell->getPort("\\Y"));
+ decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+ log_id(module), idcounter, log_id(module), width, processed_expr.c_str(), log_signal(sig)));
+ register_bv(sig, idcounter++);
+ recursive_cells.erase(cell);
+ return;
+ }
+
+ // FIXME: $slice $concat
}
- if (cell->type == "$and") return export_bvop(cell, "(bvand A B)");
- if (cell->type == "$or") return export_bvop(cell, "(bvor A B)");
- if (cell->type == "$xor") return export_bvop(cell, "(bvxor A B)");
- if (cell->type == "$xnor") return export_bvop(cell, "(bvxnor A B)");
-
- if (cell->type == "$shl") return export_bvop(cell, "(bvshl A B)", 's');
- if (cell->type == "$shr") return export_bvop(cell, "(bvlshr A B)", 's');
- if (cell->type == "$sshl") return export_bvop(cell, "(bvshl A B)", 's');
- if (cell->type == "$sshr") return export_bvop(cell, "(bvLshr A B)", 's');
-
- // FIXME: $shift $shiftx
-
- if (cell->type == "$lt") return export_bvop(cell, "(bvUlt A B)", 'b');
- if (cell->type == "$le") return export_bvop(cell, "(bvUle A B)", 'b');
- if (cell->type == "$ge") return export_bvop(cell, "(bvUge A B)", 'b');
- if (cell->type == "$gt") return export_bvop(cell, "(bvUgt A B)", 'b');
-
- if (cell->type == "$ne") return export_bvop(cell, "(distinct A B)", 'b');
- if (cell->type == "$nex") return export_bvop(cell, "(distinct A B)", 'b');
- if (cell->type == "$eq") return export_bvop(cell, "(= A B)", 'b');
- if (cell->type == "$eqx") return export_bvop(cell, "(= A B)", 'b');
-
- if (cell->type == "$not") return export_bvop(cell, "(bvnot A)");
- if (cell->type == "$pos") return export_bvop(cell, "A");
- if (cell->type == "$neg") return export_bvop(cell, "(bvneg A)");
-
- if (cell->type == "$add") return export_bvop(cell, "(bvadd A B)");
- if (cell->type == "$sub") return export_bvop(cell, "(bvsub A B)");
- if (cell->type == "$mul") return export_bvop(cell, "(bvmul A B)");
- if (cell->type == "$div") return export_bvop(cell, "(bvUdiv A B)", 'd');
- if (cell->type == "$mod") return export_bvop(cell, "(bvUrem A B)", 'd');
-
- if (cell->type == "$reduce_and") return export_reduce(cell, "(and A)", true);
- if (cell->type == "$reduce_or") return export_reduce(cell, "(or A)", false);
- if (cell->type == "$reduce_xor") return export_reduce(cell, "(xor A)", false);
- if (cell->type == "$reduce_xnor") return export_reduce(cell, "(not (xor A))", false);
- if (cell->type == "$reduce_bool") return export_reduce(cell, "(or A)", false);
-
- if (cell->type == "$logic_not") return export_reduce(cell, "(not (or A))", false);
- if (cell->type == "$logic_and") return export_reduce(cell, "(and (or A) (or B))", false);
- if (cell->type == "$logic_or") return export_reduce(cell, "(or A B)", false);
-
- if (cell->type == "$mux" || cell->type == "$pmux")
+ if (memmode && cell->type == "$mem")
{
- int width = GetSize(cell->getPort("\\Y"));
- std::string processed_expr = get_bv(cell->getPort("\\A"));
+ int arrayid = idcounter++;
+ memarrays[cell] = arrayid;
- RTLIL::SigSpec sig_b = cell->getPort("\\B");
- RTLIL::SigSpec sig_s = cell->getPort("\\S");
- get_bv(sig_b);
- get_bv(sig_s);
+ int abits = cell->getParam("\\ABITS").as_int();
+ int width = cell->getParam("\\WIDTH").as_int();
+ int rd_ports = cell->getParam("\\RD_PORTS").as_int();
- for (int i = 0; i < GetSize(sig_s); i++)
- processed_expr = stringf("(ite %s %s %s)", get_bool(sig_s[i]).c_str(),
- get_bv(sig_b.extract(i*width, width)).c_str(), processed_expr.c_str());
+ decls.push_back(stringf("(declare-fun |%s#%d#0| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
+ log_id(module), arrayid, log_id(module), abits, width, log_id(cell)));
- if (verbose) log("%*s-> import cell: %s\n", 2+2*GetSize(recursive_cells), "",
- log_id(cell));
- RTLIL::SigSpec sig = sigmap(cell->getPort("\\Y"));
- decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
- log_id(module), idcounter, log_id(module), width, processed_expr.c_str(), log_signal(sig)));
- register_bv(sig, idcounter++);
+ log_cell(cell);
+
+ for (int i = 0; i < rd_ports; i++)
+ {
+ std::string addr = get_bv(cell->getPort("\\RD_ADDR").extract(abits*i, abits));
+ SigSpec data_sig = cell->getPort("\\RD_DATA").extract(width*i, width);
+
+ if (cell->getParam("\\RD_CLK_ENABLE").extract(i).as_bool())
+ log_error("Read port %d (%s) of memory %s.%s is clocked. This is not supported by \"write_smt2\"! "
+ "Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(data_sig), log_id(cell), log_id(module));
+
+ decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (select (|%s#%d#0| state) %s)) ; %s\n",
+ log_id(module), idcounter, log_id(module), width, log_id(module), arrayid, addr.c_str(), log_signal(data_sig)));
+ register_bv(data_sig, idcounter++);
+ }
+
+ registers.insert(cell);
recursive_cells.erase(cell);
return;
}
- // FIXME: $slice $concat
-
- log_error("Unsupported cell type %s for cell %s.%s.\n",
+ log_error("Unsupported cell type %s for cell %s.%s. (Maybe this cell type would be supported in -bv or -mem mode?)\n",
log_id(cell->type), log_id(module), log_id(cell));
}
@@ -490,17 +524,49 @@ struct Smt2Worker
if (verbose) log("=> export logic driving registers [iteration %d]\n", iter);
- for (auto cell : this_regs) {
- if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_") {
+ for (auto cell : this_regs)
+ {
+ if (cell->type == "$_DFF_P_" || cell->type == "$_DFF_N_")
+ {
std::string expr_d = get_bool(cell->getPort("\\D"));
std::string expr_q = get_bool(cell->getPort("\\Q"), "next_state");
trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), log_id(cell), log_signal(cell->getPort("\\Q"))));
}
- if (cell->type == "$dff") {
+
+ if (cell->type == "$dff")
+ {
std::string expr_d = get_bv(cell->getPort("\\D"));
std::string expr_q = get_bv(cell->getPort("\\Q"), "next_state");
trans.push_back(stringf(" (= %s %s) ; %s %s\n", expr_d.c_str(), expr_q.c_str(), log_id(cell), log_signal(cell->getPort("\\Q"))));
}
+
+ if (cell->type == "$mem")
+ {
+ int arrayid = memarrays.at(cell);
+
+ int abits = cell->getParam("\\ABITS").as_int();
+ int width = cell->getParam("\\WIDTH").as_int();
+ int wr_ports = cell->getParam("\\WR_PORTS").as_int();
+
+ for (int i = 0; i < wr_ports; i++)
+ {
+ std::string addr = get_bv(cell->getPort("\\WR_ADDR").extract(abits*i, abits));
+ std::string data = get_bv(cell->getPort("\\WR_DATA").extract(width*i, width));
+ std::string mask = get_bv(cell->getPort("\\WR_EN").extract(width*i, width));
+
+ data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))",
+ data.c_str(), mask.c_str(), log_id(module), arrayid, i, addr.c_str(), mask.c_str());
+
+ decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) "
+ "(store (|%s#%d#%d| state) %s %s)) ; %s\n",
+ log_id(module), arrayid, i+1, log_id(module), abits, width,
+ log_id(module), arrayid, i, addr.c_str(), data.c_str(), log_id(cell)));
+ }
+
+ std::string expr_d = stringf("(|%s#%d#%d| state)", log_id(module), arrayid, wr_ports);
+ std::string expr_q = stringf("(|%s#%d#0| next_state)", log_id(module), arrayid);
+ trans.push_back(stringf(" (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), log_id(cell)));
+ }
}
}
@@ -591,6 +657,12 @@ struct Smt2Backend : public Backend {
log(" option set multi-bit wires are represented using the BitVec sort and\n");
log(" support for coarse grain cells (incl. arithmetic) is enabled.\n");
log("\n");
+ log(" -mem\n");
+ log(" enable support for memories (via ArraysEx theory). this option\n");
+ log(" also implies -bv. only $mem cells without merged registers in\n");
+ log(" read ports are supported. call \"memory\" with -nordff to make sure\n");
+ log(" that no registers are merged into $mem read ports.\n");
+ log("\n");
log(" -tpl <template_file>\n");
log(" use the given template file. the line containing only the token '%%%%'\n");
log(" is replaced with the regular output of this command.\n");
@@ -647,7 +719,7 @@ struct Smt2Backend : public Backend {
virtual void execute(std::ostream *&f, std::string filename, std::vector<std::string> args, RTLIL::Design *design)
{
std::ifstream template_f;
- bool bvmode = false, verbose = false;
+ bool bvmode = false, memmode = false, verbose = false;
log_header("Executing SMT2 backend.\n");
@@ -664,6 +736,11 @@ struct Smt2Backend : public Backend {
bvmode = true;
continue;
}
+ if (args[argidx] == "-mem") {
+ bvmode = true;
+ memmode = true;
+ continue;
+ }
if (args[argidx] == "-verbose") {
verbose = true;
continue;
@@ -693,7 +770,7 @@ struct Smt2Backend : public Backend {
log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));
- Smt2Worker worker(module, bvmode, verbose);
+ Smt2Worker worker(module, bvmode, memmode, verbose);
worker.run();
worker.write(*f);
}
generated by cgit v1.2.3 (git 2.25.1) at 2024-04-19 20:45:57 +0000