aboutsummaryrefslogtreecommitdiffstats
path: root/backends/smt2/smt2.cc
diff options
context:
space:
mode:
Diffstat (limited to 'backends/smt2/smt2.cc')
-rw-r--r--backends/smt2/smt2.cc498
1 files changed, 299 insertions, 199 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc
index 526b36352..a928419a1 100644
--- a/backends/smt2/smt2.cc
+++ b/backends/smt2/smt2.cc
@@ -1,7 +1,7 @@
/*
* yosys -- Yosys Open SYnthesis Suite
*
- * Copyright (C) 2012 Clifford Wolf <clifford@clifford.at>
+ * Copyright (C) 2012 Claire Xenia Wolf <claire@yosyshq.com>
*
* Permission to use, copy, modify, and/or distribute this software for any
* purpose with or without fee is hereby granted, provided that the above
@@ -22,6 +22,7 @@
#include "kernel/sigtools.h"
#include "kernel/celltypes.h"
#include "kernel/log.h"
+#include "kernel/mem.h"
#include <string>
USING_YOSYS_NAMESPACE
@@ -40,12 +41,15 @@ struct Smt2Worker
std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver;
std::set<RTLIL::Cell*> exported_cells, hiercells, hiercells_queue;
pool<Cell*> recursive_cells, registers;
+ std::vector<Mem> memories;
+ dict<Cell*, Mem*> mem_cells;
+ std::set<Mem*> memory_queue;
pool<SigBit> clock_posedge, clock_negedge;
vector<string> ex_state_eq, ex_input_eq;
std::map<RTLIL::SigBit, std::pair<int, int>> fcache;
- std::map<Cell*, int> memarrays;
+ std::map<Mem*, int> memarrays;
std::map<int, int> bvsizes;
dict<IdString, char*> ids;
@@ -116,12 +120,74 @@ struct Smt2Worker
makebits(stringf("%s_is", get_id(module)));
+ dict<IdString, Mem*> mem_dict;
+ memories = Mem::get_all_memories(module);
+ for (auto &mem : memories)
+ {
+ mem.narrow();
+ mem_dict[mem.memid] = &mem;
+ for (auto &port : mem.wr_ports)
+ {
+ if (port.clk_enable) {
+ SigSpec clk = sigmap(port.clk);
+ for (int i = 0; i < GetSize(clk); i++)
+ {
+ if (clk[i].wire == nullptr)
+ continue;
+ if (port.clk_polarity)
+ clock_posedge.insert(clk[i]);
+ else
+ clock_negedge.insert(clk[i]);
+ }
+ }
+ for (auto bit : sigmap(port.en))
+ noclock.insert(bit);
+ for (auto bit : sigmap(port.addr))
+ noclock.insert(bit);
+ for (auto bit : sigmap(port.data))
+ noclock.insert(bit);
+ }
+ for (auto &port : mem.rd_ports)
+ {
+ if (port.clk_enable) {
+ SigSpec clk = sigmap(port.clk);
+ for (int i = 0; i < GetSize(clk); i++)
+ {
+ if (clk[i].wire == nullptr)
+ continue;
+ if (port.clk_polarity)
+ clock_posedge.insert(clk[i]);
+ else
+ clock_negedge.insert(clk[i]);
+ }
+ }
+ for (auto bit : sigmap(port.en))
+ noclock.insert(bit);
+ for (auto bit : sigmap(port.addr))
+ noclock.insert(bit);
+ for (auto bit : sigmap(port.data))
+ noclock.insert(bit);
+ Cell *driver = port.cell ? port.cell : mem.cell;
+ for (auto bit : sigmap(port.data)) {
+ if (bit_driver.count(bit))
+ log_error("Found multiple drivers for %s.\n", log_signal(bit));
+ bit_driver[bit] = driver;
+ }
+ }
+ }
+
for (auto cell : module->cells())
for (auto &conn : cell->connections())
{
if (GetSize(conn.second) == 0)
continue;
+ // Handled above.
+ if (cell->is_mem_cell()) {
+ mem_cells[cell] = mem_dict[cell->parameters.at(ID::MEMID).decode_string()];
+ continue;
+ }
+
bool is_input = ct.cell_input(cell->type, conn.first);
bool is_output = ct.cell_output(cell->type, conn.first);
@@ -135,24 +201,6 @@ struct Smt2Worker
log_error("Unsupported or unknown directionality on port %s of cell %s.%s (%s).\n",
log_id(conn.first), log_id(module), log_id(cell), log_id(cell->type));
- if (cell->type.in(ID($mem)) && conn.first.in(ID::RD_CLK, ID::WR_CLK))
- {
- SigSpec clk = sigmap(conn.second);
- for (int i = 0; i < GetSize(clk); i++)
- {
- if (clk[i].wire == nullptr)
- continue;
-
- if (cell->getParam(conn.first == ID::RD_CLK ? ID::RD_CLK_ENABLE : ID::WR_CLK_ENABLE)[i] != State::S1)
- continue;
-
- if (cell->getParam(conn.first == ID::RD_CLK ? ID::RD_CLK_POLARITY : ID::WR_CLK_POLARITY)[i] == State::S1)
- clock_posedge.insert(clk[i]);
- else
- clock_negedge.insert(clk[i]);
- }
- }
- else
if (cell->type.in(ID($dff), ID($_DFF_P_), ID($_DFF_N_)) && conn.first.in(ID::CLK, ID::C))
{
bool posedge = (cell->type == ID($_DFF_N_)) || (cell->type == ID($dff) && cell->getParam(ID::CLK_POLARITY).as_bool());
@@ -647,27 +695,35 @@ struct Smt2Worker
// FIXME: $slice $concat
}
- if (memmode && cell->type == ID($mem))
+ if (memmode && cell->is_mem_cell())
{
+ Mem *mem = mem_cells[cell];
+
+ if (memarrays.count(mem)) {
+ recursive_cells.erase(cell);
+ return;
+ }
+
int arrayid = idcounter++;
- memarrays[cell] = arrayid;
-
- int abits = cell->getParam(ID::ABITS).as_int();
- int width = cell->getParam(ID::WIDTH).as_int();
- int rd_ports = cell->getParam(ID::RD_PORTS).as_int();
- int wr_ports = cell->getParam(ID::WR_PORTS).as_int();
-
- bool async_read = false;
- if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_ones()) {
- if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_zero())
- log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module));
- async_read = true;
+ memarrays[mem] = arrayid;
+
+ int abits = ceil_log2(mem->size);
+
+ bool has_sync_wr = false;
+ bool has_async_wr = false;
+ for (auto &port : mem->wr_ports) {
+ if (port.clk_enable)
+ has_sync_wr = true;
+ else
+ has_async_wr = true;
}
+ if (has_async_wr && has_sync_wr)
+ log_error("Memory %s.%s has mixed clocked/nonclocked write ports. This is not supported by \"write_smt2\".\n", log_id(cell), log_id(module));
- decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(cell), abits, width, rd_ports, wr_ports, async_read ? "async" : "sync"));
+ decls.push_back(stringf("; yosys-smt2-memory %s %d %d %d %d %s\n", get_id(mem->memid), abits, mem->width, GetSize(mem->rd_ports), GetSize(mem->wr_ports), has_async_wr ? "async" : "sync"));
string memstate;
- if (async_read) {
+ if (has_async_wr) {
memstate = stringf("%s#%d#final", get_id(module), arrayid);
} else {
memstate = stringf("%s#%d#0", get_id(module), arrayid);
@@ -675,80 +731,79 @@ struct Smt2Worker
if (statebv)
{
- int mem_size = cell->getParam(ID::SIZE).as_int();
- int mem_offset = cell->getParam(ID::OFFSET).as_int();
-
- makebits(memstate, width*mem_size, get_id(cell));
+ makebits(memstate, mem->width*mem->size, get_id(mem->memid));
decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (_ BitVec %d) (|%s| state))\n",
- get_id(module), get_id(cell), get_id(module), width*mem_size, memstate.c_str()));
+ get_id(module), get_id(mem->memid), get_id(module), mem->width*mem->size, memstate.c_str()));
- for (int i = 0; i < rd_ports; i++)
+ for (int i = 0; i < GetSize(mem->rd_ports); i++)
{
- SigSpec addr_sig = cell->getPort(ID::RD_ADDR).extract(abits*i, abits);
- SigSpec data_sig = cell->getPort(ID::RD_DATA).extract(width*i, width);
+ auto &port = mem->rd_ports[i];
+ SigSpec addr_sig = port.addr;
+ addr_sig.extend_u0(abits);
std::string addr = get_bv(addr_sig);
- if (cell->getParam(ID::RD_CLK_ENABLE).extract(i).as_bool())
+ if (port.clk_enable)
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));
+ "Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(port.data), log_id(mem->memid), log_id(module));
decls.push_back(stringf("(define-fun |%s_m:R%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
- get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
+ get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
std::string read_expr = "#b";
- for (int k = 0; k < width; k++)
+ for (int k = 0; k < mem->width; k++)
read_expr += "0";
- for (int k = 0; k < mem_size; k++)
+ for (int k = 0; k < mem->size; k++)
read_expr = stringf("(ite (= (|%s_m:R%dA %s| state) #b%s) ((_ extract %d %d) (|%s| state))\n %s)",
- get_id(module), i, get_id(cell), Const(k+mem_offset, abits).as_string().c_str(),
- width*(k+1)-1, width*k, memstate.c_str(), read_expr.c_str());
+ get_id(module), i, get_id(mem->memid), Const(k+mem->start_offset, abits).as_string().c_str(),
+ mem->width*(k+1)-1, mem->width*k, memstate.c_str(), read_expr.c_str());
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d)\n %s) ; %s\n",
- get_id(module), idcounter, get_id(module), width, read_expr.c_str(), log_signal(data_sig)));
+ get_id(module), idcounter, get_id(module), mem->width, read_expr.c_str(), log_signal(port.data)));
decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n",
- get_id(module), i, get_id(cell), get_id(module), width, get_id(module), idcounter));
+ get_id(module), i, get_id(mem->memid), get_id(module), mem->width, get_id(module), idcounter));
- register_bv(data_sig, idcounter++);
+ register_bv(port.data, idcounter++);
}
}
else
{
if (statedt)
dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
- memstate.c_str(), abits, width, get_id(cell)));
+ memstate.c_str(), abits, mem->width, get_id(mem->memid)));
else
decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
- memstate.c_str(), get_id(module), abits, width, get_id(cell)));
+ memstate.c_str(), get_id(module), abits, mem->width, get_id(mem->memid)));
decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (Array (_ BitVec %d) (_ BitVec %d)) (|%s| state))\n",
- get_id(module), get_id(cell), get_id(module), abits, width, memstate.c_str()));
+ get_id(module), get_id(mem->memid), get_id(module), abits, mem->width, memstate.c_str()));
- for (int i = 0; i < rd_ports; i++)
+ for (int i = 0; i < GetSize(mem->rd_ports); i++)
{
- SigSpec addr_sig = cell->getPort(ID::RD_ADDR).extract(abits*i, abits);
- SigSpec data_sig = cell->getPort(ID::RD_DATA).extract(width*i, width);
+ auto &port = mem->rd_ports[i];
+ SigSpec addr_sig = port.addr;
+ addr_sig.extend_u0(abits);
std::string addr = get_bv(addr_sig);
- if (cell->getParam(ID::RD_CLK_ENABLE).extract(i).as_bool())
+ if (port.clk_enable)
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));
+ "Call \"memory\" with -nordff to avoid this error.\n", i, log_signal(port.data), log_id(mem->memid), log_id(module));
decls.push_back(stringf("(define-fun |%s_m:R%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
- get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
+ get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
decls.push_back(stringf("(define-fun |%s#%d| ((state |%s_s|)) (_ BitVec %d) (select (|%s| state) (|%s_m:R%dA %s| state))) ; %s\n",
- get_id(module), idcounter, get_id(module), width, memstate.c_str(), get_id(module), i, get_id(cell), log_signal(data_sig)));
+ get_id(module), idcounter, get_id(module), mem->width, memstate.c_str(), get_id(module), i, get_id(mem->memid), log_signal(port.data)));
decls.push_back(stringf("(define-fun |%s_m:R%dD %s| ((state |%s_s|)) (_ BitVec %d) (|%s#%d| state))\n",
- get_id(module), i, get_id(cell), get_id(module), width, get_id(module), idcounter));
+ get_id(module), i, get_id(mem->memid), get_id(module), mem->width, get_id(module), idcounter));
- register_bv(data_sig, idcounter++);
+ register_bv(port.data, idcounter++);
}
}
- registers.insert(cell);
+ memory_queue.insert(mem);
recursive_cells.erase(cell);
return;
}
@@ -801,6 +856,18 @@ struct Smt2Worker
return;
}
+ if (cell->type.in(ID($dffe), ID($sdff), ID($sdffe), ID($sdffce)) || cell->type.str().substr(0, 6) == "$_SDFF" || (cell->type.str().substr(0, 6) == "$_DFFE" && cell->type.str().size() == 10)) {
+ log_error("Unsupported cell type %s for cell %s.%s -- please run `dffunmap` before `write_smt2`.\n",
+ log_id(cell->type), log_id(module), log_id(cell));
+ }
+ if (cell->type.in(ID($adff), ID($adffe), ID($aldff), ID($aldffe), ID($dffsr), ID($dffsre)) || cell->type.str().substr(0, 5) == "$_DFF" || cell->type.str().substr(0, 7) == "$_ALDFF") {
+ log_error("Unsupported cell type %s for cell %s.%s -- please run `async2sync; dffunmap` or `clk2fflogic` before `write_smt2`.\n",
+ log_id(cell->type), log_id(module), log_id(cell));
+ }
+ if (cell->type.in(ID($sr), ID($dlatch), ID($adlatch), ID($dlatchsr)) || cell->type.str().substr(0, 8) == "$_DLATCH" || cell->type.str().substr(0, 5) == "$_SR_") {
+ log_error("Unsupported cell type %s for cell %s.%s -- please run `clk2fflogic` before `write_smt2`.\n",
+ log_id(cell->type), log_id(module), log_id(cell));
+ }
log_error("Unsupported cell type %s for cell %s.%s.\n",
log_id(cell->type), log_id(module), log_id(cell));
}
@@ -822,40 +889,51 @@ struct Smt2Worker
for (auto bit : SigSpec(wire))
if (reg_bits.count(bit))
is_register = true;
- if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\')) {
+ if (wire->port_id || is_register || wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic())) {
RTLIL::SigSpec sig = sigmap(wire);
+ std::vector<std::string> comments;
if (wire->port_input)
- decls.push_back(stringf("; yosys-smt2-input %s %d\n", get_id(wire), wire->width));
+ comments.push_back(stringf("; yosys-smt2-input %s %d\n", get_id(wire), wire->width));
if (wire->port_output)
- decls.push_back(stringf("; yosys-smt2-output %s %d\n", get_id(wire), wire->width));
+ comments.push_back(stringf("; yosys-smt2-output %s %d\n", get_id(wire), wire->width));
if (is_register)
- decls.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width));
- if (wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name[0] == '\\'))
- decls.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width));
+ comments.push_back(stringf("; yosys-smt2-register %s %d\n", get_id(wire), wire->width));
+ if (wire->get_bool_attribute(ID::keep) || (wiresmode && wire->name.isPublic()))
+ comments.push_back(stringf("; yosys-smt2-wire %s %d\n", get_id(wire), wire->width));
if (GetSize(wire) == 1 && (clock_posedge.count(sig) || clock_negedge.count(sig)))
- decls.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
+ comments.push_back(stringf("; yosys-smt2-clock %s%s%s\n", get_id(wire),
clock_posedge.count(sig) ? " posedge" : "", clock_negedge.count(sig) ? " negedge" : ""));
if (bvmode && GetSize(sig) > 1) {
+ std::string sig_bv = get_bv(sig);
+ if (!comments.empty())
+ decls.insert(decls.end(), comments.begin(), comments.end());
decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) (_ BitVec %d) %s)\n",
- get_id(module), get_id(wire), get_id(module), GetSize(sig), get_bv(sig).c_str()));
+ get_id(module), get_id(wire), get_id(module), GetSize(sig), sig_bv.c_str()));
if (wire->port_input)
ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))",
get_id(module), get_id(wire), get_id(module), get_id(wire)));
} else {
- for (int i = 0; i < GetSize(sig); i++)
+ std::vector<std::string> sig_bool;
+ for (int i = 0; i < GetSize(sig); i++) {
+ sig_bool.push_back(get_bool(sig[i]));
+ }
+ if (!comments.empty())
+ decls.insert(decls.end(), comments.begin(), comments.end());
+ for (int i = 0; i < GetSize(sig); i++) {
if (GetSize(sig) > 1) {
decls.push_back(stringf("(define-fun |%s_n %s %d| ((state |%s_s|)) Bool %s)\n",
- get_id(module), get_id(wire), i, get_id(module), get_bool(sig[i]).c_str()));
+ get_id(module), get_id(wire), i, get_id(module), sig_bool[i].c_str()));
if (wire->port_input)
ex_input_eq.push_back(stringf(" (= (|%s_n %s %d| state) (|%s_n %s %d| other_state))",
get_id(module), get_id(wire), i, get_id(module), get_id(wire), i));
} else {
decls.push_back(stringf("(define-fun |%s_n %s| ((state |%s_s|)) Bool %s)\n",
- get_id(module), get_id(wire), get_id(module), get_bool(sig[i]).c_str()));
+ get_id(module), get_id(wire), get_id(module), sig_bool[i].c_str()));
if (wire->port_input)
ex_input_eq.push_back(stringf(" (= (|%s_n %s| state) (|%s_n %s| other_state))",
get_id(module), get_id(wire), get_id(module), get_id(wire)));
}
+ }
}
}
}
@@ -966,7 +1044,7 @@ struct Smt2Worker
}
}
- for (int iter = 1; !registers.empty(); iter++)
+ for (int iter = 1; !registers.empty() || !memory_queue.empty(); iter++)
{
pool<Cell*> this_regs;
this_regs.swap(registers);
@@ -999,152 +1077,156 @@ struct Smt2Worker
if (cell->type == ID($anyconst))
ex_state_eq.push_back(stringf("(= %s %s)", get_bv(cell->getPort(ID::Y)).c_str(), get_bv(cell->getPort(ID::Y), "other_state").c_str()));
}
+ }
- if (cell->type == ID($mem))
- {
- int arrayid = memarrays.at(cell);
+ std::set<Mem*> this_mems;
+ this_mems.swap(memory_queue);
+
+ for (auto mem : this_mems)
+ {
+ int arrayid = memarrays.at(mem);
- int abits = cell->getParam(ID::ABITS).as_int();
- int width = cell->getParam(ID::WIDTH).as_int();
- int wr_ports = cell->getParam(ID::WR_PORTS).as_int();
+ int abits = ceil_log2(mem->size);;
- bool async_read = false;
- string initial_memstate, final_memstate;
+ bool has_sync_wr = false;
+ bool has_async_wr = false;
+ for (auto &port : mem->wr_ports) {
+ if (port.clk_enable)
+ has_sync_wr = true;
+ else
+ has_async_wr = true;
+ }
- if (!cell->getParam(ID::WR_CLK_ENABLE).is_fully_ones()) {
- log_assert(cell->getParam(ID::WR_CLK_ENABLE).is_fully_zero());
- async_read = true;
- initial_memstate = stringf("%s#%d#0", get_id(module), arrayid);
- final_memstate = stringf("%s#%d#final", get_id(module), arrayid);
+ string initial_memstate, final_memstate;
+
+ if (has_async_wr) {
+ log_assert(!has_sync_wr);
+ initial_memstate = stringf("%s#%d#0", get_id(module), arrayid);
+ final_memstate = stringf("%s#%d#final", get_id(module), arrayid);
+ }
+
+ if (statebv)
+ {
+ if (has_async_wr) {
+ makebits(final_memstate, mem->width*mem->size, get_id(mem->memid));
}
- if (statebv)
+ for (int i = 0; i < GetSize(mem->wr_ports); i++)
{
- int mem_size = cell->getParam(ID::SIZE).as_int();
- int mem_offset = cell->getParam(ID::OFFSET).as_int();
-
- if (async_read) {
- makebits(final_memstate, width*mem_size, get_id(cell));
+ auto &port = mem->wr_ports[i];
+ SigSpec addr_sig = port.addr;
+ addr_sig.extend_u0(abits);
+
+ std::string addr = get_bv(addr_sig);
+ std::string data = get_bv(port.data);
+ std::string mask = get_bv(port.en);
+
+ decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+ get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
+ addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(mem->memid));
+
+ decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+ get_id(module), i, get_id(mem->memid), get_id(module), mem->width, data.c_str(), log_signal(port.data)));
+ data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(mem->memid));
+
+ decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+ get_id(module), i, get_id(mem->memid), get_id(module), mem->width, mask.c_str(), log_signal(port.en)));
+ mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(mem->memid));
+
+ std::string data_expr;
+
+ for (int k = mem->size-1; k >= 0; k--) {
+ std::string new_data = stringf("(bvor (bvand %s %s) (bvand ((_ extract %d %d) (|%s#%d#%d| state)) (bvnot %s)))",
+ data.c_str(), mask.c_str(), mem->width*(k+1)-1, mem->width*k, get_id(module), arrayid, i, mask.c_str());
+ data_expr += stringf("\n (ite (= %s #b%s) %s ((_ extract %d %d) (|%s#%d#%d| state)))",
+ addr.c_str(), Const(k+mem->start_offset, abits).as_string().c_str(), new_data.c_str(),
+ mem->width*(k+1)-1, mem->width*k, get_id(module), arrayid, i);
}
- for (int i = 0; i < wr_ports; i++)
- {
- SigSpec addr_sig = cell->getPort(ID::WR_ADDR).extract(abits*i, abits);
- SigSpec data_sig = cell->getPort(ID::WR_DATA).extract(width*i, width);
- SigSpec mask_sig = cell->getPort(ID::WR_EN).extract(width*i, width);
+ decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (_ BitVec %d) (concat%s)) ; %s\n",
+ get_id(module), arrayid, i+1, get_id(module), mem->width*mem->size, data_expr.c_str(), get_id(mem->memid)));
+ }
+ }
+ else
+ {
+ if (has_async_wr) {
+ if (statedt)
+ dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
+ initial_memstate.c_str(), abits, mem->width, get_id(mem->memid)));
+ else
+ decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
+ initial_memstate.c_str(), get_id(module), abits, mem->width, get_id(mem->memid)));
+ }
- std::string addr = get_bv(addr_sig);
- std::string data = get_bv(data_sig);
- std::string mask = get_bv(mask_sig);
+ for (int i = 0; i < GetSize(mem->wr_ports); i++)
+ {
+ auto &port = mem->wr_ports[i];
+ SigSpec addr_sig = port.addr;
+ addr_sig.extend_u0(abits);
- decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
- get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
- addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(cell));
+ std::string addr = get_bv(addr_sig);
+ std::string data = get_bv(port.data);
+ std::string mask = get_bv(port.en);
- decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
- get_id(module), i, get_id(cell), get_id(module), width, data.c_str(), log_signal(data_sig)));
- data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(cell));
+ decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+ get_id(module), i, get_id(mem->memid), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
+ addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(mem->memid));
- decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
- get_id(module), i, get_id(cell), get_id(module), width, mask.c_str(), log_signal(mask_sig)));
- mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(cell));
+ decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+ get_id(module), i, get_id(mem->memid), get_id(module), mem->width, data.c_str(), log_signal(port.data)));
+ data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(mem->memid));
- std::string data_expr;
+ decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
+ get_id(module), i, get_id(mem->memid), get_id(module), mem->width, mask.c_str(), log_signal(port.en)));
+ mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(mem->memid));
- for (int k = mem_size-1; k >= 0; k--) {
- std::string new_data = stringf("(bvor (bvand %s %s) (bvand ((_ extract %d %d) (|%s#%d#%d| state)) (bvnot %s)))",
- data.c_str(), mask.c_str(), width*(k+1)-1, width*k, get_id(module), arrayid, i, mask.c_str());
- data_expr += stringf("\n (ite (= %s #b%s) %s ((_ extract %d %d) (|%s#%d#%d| state)))",
- addr.c_str(), Const(k+mem_offset, abits).as_string().c_str(), new_data.c_str(),
- width*(k+1)-1, width*k, get_id(module), arrayid, i);
- }
+ data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))",
+ data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str());
- decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (_ BitVec %d) (concat%s)) ; %s\n",
- get_id(module), arrayid, i+1, get_id(module), width*mem_size, data_expr.c_str(), get_id(cell)));
- }
+ 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",
+ get_id(module), arrayid, i+1, get_id(module), abits, mem->width,
+ get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(mem->memid)));
}
- else
- {
- if (async_read) {
- if (statedt)
- dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
- initial_memstate.c_str(), abits, width, get_id(cell)));
- else
- decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
- initial_memstate.c_str(), get_id(module), abits, width, get_id(cell)));
- }
-
- for (int i = 0; i < wr_ports; i++)
- {
- SigSpec addr_sig = cell->getPort(ID::WR_ADDR).extract(abits*i, abits);
- SigSpec data_sig = cell->getPort(ID::WR_DATA).extract(width*i, width);
- SigSpec mask_sig = cell->getPort(ID::WR_EN).extract(width*i, width);
+ }
- std::string addr = get_bv(addr_sig);
- std::string data = get_bv(data_sig);
- std::string mask = get_bv(mask_sig);
+ std::string expr_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, GetSize(mem->wr_ports));
+ std::string expr_q = stringf("(|%s#%d#0| next_state)", get_id(module), arrayid);
+ trans.push_back(stringf(" (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), get_id(mem->memid)));
+ ex_state_eq.push_back(stringf("(= (|%s#%d#0| state) (|%s#%d#0| other_state))", get_id(module), arrayid, get_id(module), arrayid));
- decls.push_back(stringf("(define-fun |%s_m:W%dA %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
- get_id(module), i, get_id(cell), get_id(module), abits, addr.c_str(), log_signal(addr_sig)));
- addr = stringf("(|%s_m:W%dA %s| state)", get_id(module), i, get_id(cell));
+ if (has_async_wr)
+ hier.push_back(stringf(" (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(mem->memid)));
- decls.push_back(stringf("(define-fun |%s_m:W%dD %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
- get_id(module), i, get_id(cell), get_id(module), width, data.c_str(), log_signal(data_sig)));
- data = stringf("(|%s_m:W%dD %s| state)", get_id(module), i, get_id(cell));
+ Const init_data = mem->get_init_data();
- decls.push_back(stringf("(define-fun |%s_m:W%dM %s| ((state |%s_s|)) (_ BitVec %d) %s) ; %s\n",
- get_id(module), i, get_id(cell), get_id(module), width, mask.c_str(), log_signal(mask_sig)));
- mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(cell));
+ for (int i = 0; i < mem->size; i++)
+ {
+ if (i*mem->width >= GetSize(init_data))
+ break;
- data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))",
- data.c_str(), mask.c_str(), get_id(module), arrayid, i, addr.c_str(), mask.c_str());
+ Const initword = init_data.extract(i*mem->width, mem->width, State::Sx);
+ Const initmask = initword;
+ bool gen_init_constr = false;
- 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",
- get_id(module), arrayid, i+1, get_id(module), abits, width,
- get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(cell)));
+ for (int k = 0; k < GetSize(initword); k++) {
+ if (initword[k] == State::S0 || initword[k] == State::S1) {
+ gen_init_constr = true;
+ initmask[k] = State::S1;
+ } else {
+ initmask[k] = State::S0;
+ initword[k] = State::S0;
}
}
- std::string expr_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, wr_ports);
- std::string expr_q = stringf("(|%s#%d#0| next_state)", get_id(module), arrayid);
- trans.push_back(stringf(" (= %s %s) ; %s\n", expr_d.c_str(), expr_q.c_str(), get_id(cell)));
- ex_state_eq.push_back(stringf("(= (|%s#%d#0| state) (|%s#%d#0| other_state))", get_id(module), arrayid, get_id(module), arrayid));
-
- if (async_read)
- hier.push_back(stringf(" (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(cell)));
-
- Const init_data = cell->getParam(ID::INIT);
- int memsize = cell->getParam(ID::SIZE).as_int();
-
- for (int i = 0; i < memsize; i++)
+ if (gen_init_constr)
{
- if (i*width >= GetSize(init_data))
- break;
-
- Const initword = init_data.extract(i*width, width, State::Sx);
- Const initmask = initword;
- bool gen_init_constr = false;
-
- for (int k = 0; k < GetSize(initword); k++) {
- if (initword[k] == State::S0 || initword[k] == State::S1) {
- gen_init_constr = true;
- initmask[k] = State::S1;
- } else {
- initmask[k] = State::S0;
- initword[k] = State::S0;
- }
- }
-
- if (gen_init_constr)
- {
- if (statebv)
- /* FIXME */;
- else
- init_list.push_back(stringf("(= (bvand (select (|%s#%d#0| state) #b%s) #b%s) #b%s) ; %s[%d]",
- get_id(module), arrayid, Const(i, abits).as_string().c_str(),
- initmask.as_string().c_str(), initword.as_string().c_str(), get_id(cell), i));
- }
+ if (statebv)
+ /* FIXME */;
+ else
+ init_list.push_back(stringf("(= (bvand (select (|%s#%d#0| state) #b%s) #b%s) #b%s) ; %s[%d]",
+ get_id(module), arrayid, Const(i, abits).as_string().c_str(),
+ initmask.as_string().c_str(), initword.as_string().c_str(), get_id(mem->memid), i));
}
}
}
@@ -1387,8 +1469,12 @@ struct Smt2Backend : public Backend {
log(" use the given template file. the line containing only the token '%%%%'\n");
log(" is replaced with the regular output of this command.\n");
log("\n");
+ log(" -solver-option <option> <value>\n");
+ log(" emit a `; yosys-smt2-solver-option` directive for yosys-smtbmc to write\n");
+ log(" the given option as a `(set-option ...)` command in the SMT-LIBv2.\n");
+ log("\n");
log("[1] For more information on SMT-LIBv2 visit http://smt-lib.org/ or read David\n");
- log("R. Cok's tutorial: http://www.grammatech.com/resources/smt/SMTLIBTutorial.pdf\n");
+ log("R. Cok's tutorial: https://smtlib.github.io/jSMTLIB/SMTLIBTutorial.pdf\n");
log("\n");
log("---------------------------------------------------------------------------\n");
log("\n");
@@ -1441,9 +1527,15 @@ struct Smt2Backend : public Backend {
std::ifstream template_f;
bool bvmode = true, memmode = true, wiresmode = false, verbose = false, statebv = false, statedt = false;
bool forallmode = false;
+ dict<std::string, std::string> solver_options;
log_header(design, "Executing SMT2 backend.\n");
+ log_push();
+ Pass::call(design, "bmuxmap");
+ Pass::call(design, "demuxmap");
+ log_pop();
+
size_t argidx;
for (argidx = 1; argidx < args.size(); argidx++)
{
@@ -1484,6 +1576,11 @@ struct Smt2Backend : public Backend {
verbose = true;
continue;
}
+ if (args[argidx] == "-solver-option" && argidx+2 < args.size()) {
+ solver_options.emplace(args[argidx+1], args[argidx+2]);
+ argidx += 2;
+ continue;
+ }
break;
}
extra_args(f, filename, args, argidx);
@@ -1514,6 +1611,9 @@ struct Smt2Backend : public Backend {
if (statedt)
*f << stringf("; yosys-smt2-stdt\n");
+ for (auto &it : solver_options)
+ *f << stringf("; yosys-smt2-solver-option %s %s\n", it.first.c_str(), it.second.c_str());
+
std::vector<RTLIL::Module*> sorted_modules;
// extract module dependencies
@@ -1562,7 +1662,7 @@ struct Smt2Backend : public Backend {
for (auto module : sorted_modules)
{
- if (module->get_blackbox_attribute() || module->has_memories_warn() || module->has_processes_warn())
+ if (module->get_blackbox_attribute() || module->has_processes_warn())
continue;
log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));
generated by cgit v1.2.3 (git 2.25.1) at 2025-04-05 21:26:28 +0000