#include "kernel/sigtools.h"
#include "kernel/celltypes.h"
#include "kernel/log.h"
+#include "kernel/mem.h"
#include <string>
USING_YOSYS_NAMESPACE
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;
makebits(stringf("%s_is", get_id(module)));
+ dict<IdString, Mem*> mem_dict;
+ memories = Mem::get_all_memories(module);
+ for (auto &mem : memories)
+ {
+ 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->type.in(ID($mem), ID($memrd), ID($memwr), ID($meminit))) {
+ 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);
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());
// FIXME: $slice $concat
}
- if (memmode && cell->type == ID($mem))
+ if (memmode && cell->type.in(ID($mem), ID($memrd), ID($memwr), ID($meminit)))
{
+ 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);
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;
}
}
}
- 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);
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 = ceil_log2(mem->size);;
- 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();
+ 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;
+ }
- bool async_read = false;
- string initial_memstate, final_memstate;
+ string initial_memstate, final_memstate;
- 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);
+ 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));
}
}
}
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));
projects / yosys.git / commitdiff