riscv
/
yosys
mirror of https://github.com/YosysHQ/yosys.git
1
0
Fork 0
Code Issues Projects Releases Wiki Activity

smt2: Use Mem helper.

This commit is contained in:
Marcelina Kościelnicka 2020-10-18 03:09:45 +02:00
parent ec483b7c3b
commit f272c8b407
1 changed files with 253 additions and 195 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

310
backends/smt2/smt2.cc
View File

@ -22,6 +22,7 @@
#include "kernel/sigtools.h" #include "kernel/sigtools.h"
#include "kernel/celltypes.h" #include "kernel/celltypes.h"
#include "kernel/log.h" #include "kernel/log.h"
#include "kernel/mem.h"
#include <string> #include <string>
USING_YOSYS_NAMESPACE USING_YOSYS_NAMESPACE
@ -40,12 +41,15 @@ struct Smt2Worker
std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver; std::map<RTLIL::SigBit, RTLIL::Cell*> bit_driver;
std::set<RTLIL::Cell*> exported_cells, hiercells, hiercells_queue; std::set<RTLIL::Cell*> exported_cells, hiercells, hiercells_queue;
pool<Cell*> recursive_cells, registers; 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; pool<SigBit> clock_posedge, clock_negedge;
vector<string> ex_state_eq, ex_input_eq; vector<string> ex_state_eq, ex_input_eq;
std::map<RTLIL::SigBit, std::pair<int, int>> fcache; std::map<RTLIL::SigBit, std::pair<int, int>> fcache;
std::map<Cell*, int> memarrays; std::map<Mem*, int> memarrays;
std::map<int, int> bvsizes; std::map<int, int> bvsizes;
dict<IdString, char*> ids; dict<IdString, char*> ids;
@ -116,12 +120,73 @@ struct Smt2Worker
makebits(stringf("%s_is", get_id(module))); 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 cell : module->cells())
for (auto &conn : cell->connections()) for (auto &conn : cell->connections())
{ {
if (GetSize(conn.second) == 0) if (GetSize(conn.second) == 0)
continue; 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_input = ct.cell_input(cell->type, conn.first);
bool is_output = ct.cell_output(cell->type, conn.first); bool is_output = ct.cell_output(cell->type, conn.first);
@ -135,24 +200,6 @@ struct Smt2Worker
log_error("Unsupported or unknown directionality on port %s of cell %s.%s (%s).\n", 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)); 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)) 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()); bool posedge = (cell->type == ID($_DFF_N_)) || (cell->type == ID($dff) && cell->getParam(ID::CLK_POLARITY).as_bool());
@ -647,27 +694,35 @@ struct Smt2Worker
// FIXME: $slice $concat // FIXME: $slice $concat
} }
if (memmode && cell->type == ID($mem)) if (memmode && cell->type.in(ID($mem), ID($memrd), ID($memwr), ID($meminit)))
{ {
int arrayid = idcounter++; Mem *mem = mem_cells[cell];
memarrays[cell] = arrayid;
int abits = cell->getParam(ID::ABITS).as_int(); if (memarrays.count(mem)) {
int width = cell->getParam(ID::WIDTH).as_int(); recursive_cells.erase(cell);
int rd_ports = cell->getParam(ID::RD_PORTS).as_int(); return;
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;
} }
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")); int arrayid = idcounter++;
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(mem->memid), abits, mem->width, GetSize(mem->rd_ports), GetSize(mem->wr_ports), has_async_wr ? "async" : "sync"));
string memstate; string memstate;
if (async_read) { if (has_async_wr) {
memstate = stringf("%s#%d#final", get_id(module), arrayid); memstate = stringf("%s#%d#final", get_id(module), arrayid);
} else { } else {
memstate = stringf("%s#%d#0", get_id(module), arrayid); memstate = stringf("%s#%d#0", get_id(module), arrayid);
@ -675,80 +730,79 @@ struct Smt2Worker
if (statebv) if (statebv)
{ {
int mem_size = cell->getParam(ID::SIZE).as_int(); makebits(memstate, mem->width*mem->size, get_id(mem->memid));
int mem_offset = cell->getParam(ID::OFFSET).as_int();
makebits(memstate, width*mem_size, get_id(cell));
decls.push_back(stringf("(define-fun |%s_m %s| ((state |%s_s|)) (_ BitVec %d) (|%s| state))\n", 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); auto &port = mem->rd_ports[i];
SigSpec data_sig = cell->getPort(ID::RD_DATA).extract(width*i, width); SigSpec addr_sig = port.addr;
addr_sig.extend_u0(abits);
std::string addr = get_bv(addr_sig); 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\"! " 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", 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"; std::string read_expr = "#b";
for (int k = 0; k < width; k++) for (int k = 0; k < mem->width; k++)
read_expr += "0"; 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)", 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(), get_id(module), i, get_id(mem->memid), Const(k+mem->start_offset, abits).as_string().c_str(),
width*(k+1)-1, width*k, memstate.c_str(), read_expr.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", 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", 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 else
{ {
if (statedt) if (statedt)
dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", 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 else
decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", 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", 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); auto &port = mem->rd_ports[i];
SigSpec data_sig = cell->getPort(ID::RD_DATA).extract(width*i, width); SigSpec addr_sig = port.addr;
addr_sig.extend_u0(abits);
std::string addr = get_bv(addr_sig); 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\"! " 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", 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", 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", 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); recursive_cells.erase(cell);
return; return;
} }
@ -977,7 +1031,7 @@ struct Smt2Worker
} }
} }
for (int iter = 1; !registers.empty(); iter++) for (int iter = 1; !registers.empty() || !memory_queue.empty(); iter++)
{ {
pool<Cell*> this_regs; pool<Cell*> this_regs;
this_regs.swap(registers); this_regs.swap(registers);
@ -1010,130 +1064,135 @@ struct Smt2Worker
if (cell->type == ID($anyconst)) 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())); 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)) std::set<Mem*> this_mems;
this_mems.swap(memory_queue);
for (auto mem : this_mems)
{ {
int arrayid = memarrays.at(cell); int arrayid = memarrays.at(mem);
int abits = cell->getParam(ID::ABITS).as_int(); int abits = ceil_log2(mem->size);;
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()) { if (has_async_wr) {
log_assert(cell->getParam(ID::WR_CLK_ENABLE).is_fully_zero()); log_assert(!has_sync_wr);
async_read = true;
initial_memstate = stringf("%s#%d#0", get_id(module), arrayid); initial_memstate = stringf("%s#%d#0", get_id(module), arrayid);
final_memstate = stringf("%s#%d#final", get_id(module), arrayid); final_memstate = stringf("%s#%d#final", get_id(module), arrayid);
} }
if (statebv) if (statebv)
{ {
int mem_size = cell->getParam(ID::SIZE).as_int(); if (has_async_wr) {
int mem_offset = cell->getParam(ID::OFFSET).as_int(); makebits(final_memstate, mem->width*mem->size, get_id(mem->memid));
if (async_read) {
makebits(final_memstate, width*mem_size, get_id(cell));
} }
for (int i = 0; i < wr_ports; i++) for (int i = 0; i < GetSize(mem->wr_ports); i++)
{ {
SigSpec addr_sig = cell->getPort(ID::WR_ADDR).extract(abits*i, abits); auto &port = mem->wr_ports[i];
SigSpec data_sig = cell->getPort(ID::WR_DATA).extract(width*i, width); SigSpec addr_sig = port.addr;
SigSpec mask_sig = cell->getPort(ID::WR_EN).extract(width*i, width); addr_sig.extend_u0(abits);
std::string addr = get_bv(addr_sig); std::string addr = get_bv(addr_sig);
std::string data = get_bv(data_sig); std::string data = get_bv(port.data);
std::string mask = get_bv(mask_sig); 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", 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))); 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(cell)); 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", 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))); 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(cell)); 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", 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))); 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(cell)); mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(mem->memid));
std::string data_expr; std::string data_expr;
for (int k = mem_size-1; k >= 0; k--) { 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)))", 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.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)))", 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(), addr.c_str(), Const(k+mem->start_offset, abits).as_string().c_str(), new_data.c_str(),
width*(k+1)-1, width*k, get_id(module), arrayid, i); mem->width*(k+1)-1, mem->width*k, get_id(module), arrayid, i);
} }
decls.push_back(stringf("(define-fun |%s#%d#%d| ((state |%s_s|)) (_ BitVec %d) (concat%s)) ; %s\n", 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))); get_id(module), arrayid, i+1, get_id(module), mem->width*mem->size, data_expr.c_str(), get_id(mem->memid)));
} }
} }
else else
{ {
if (async_read) { if (has_async_wr) {
if (statedt) if (statedt)
dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", dtmembers.push_back(stringf(" (|%s| (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n",
initial_memstate.c_str(), abits, width, get_id(cell))); initial_memstate.c_str(), abits, mem->width, get_id(mem->memid)));
else else
decls.push_back(stringf("(declare-fun |%s| (|%s_s|) (Array (_ BitVec %d) (_ BitVec %d))) ; %s\n", 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))); initial_memstate.c_str(), get_id(module), abits, mem->width, get_id(mem->memid)));
} }
for (int i = 0; i < wr_ports; i++) for (int i = 0; i < GetSize(mem->wr_ports); i++)
{ {
SigSpec addr_sig = cell->getPort(ID::WR_ADDR).extract(abits*i, abits); auto &port = mem->wr_ports[i];
SigSpec data_sig = cell->getPort(ID::WR_DATA).extract(width*i, width); SigSpec addr_sig = port.addr;
SigSpec mask_sig = cell->getPort(ID::WR_EN).extract(width*i, width); addr_sig.extend_u0(abits);
std::string addr = get_bv(addr_sig); std::string addr = get_bv(addr_sig);
std::string data = get_bv(data_sig); std::string data = get_bv(port.data);
std::string mask = get_bv(mask_sig); 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", 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))); 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(cell)); 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", 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))); 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(cell)); 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", 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))); 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(cell)); mask = stringf("(|%s_m:W%dM %s| state)", get_id(module), i, get_id(mem->memid));
data = stringf("(bvor (bvand %s %s) (bvand (select (|%s#%d#%d| state) %s) (bvnot %s)))", 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()); 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|)) (Array (_ BitVec %d) (_ BitVec %d)) " 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", "(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+1, get_id(module), abits, mem->width,
get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(cell))); get_id(module), arrayid, i, addr.c_str(), data.c_str(), get_id(mem->memid)));
} }
} }
std::string expr_d = stringf("(|%s#%d#%d| state)", get_id(module), arrayid, wr_ports); 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); 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))); 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)); 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) if (has_async_wr)
hier.push_back(stringf(" (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(cell))); hier.push_back(stringf(" (= %s (|%s| state)) ; %s\n", expr_d.c_str(), final_memstate.c_str(), get_id(mem->memid)));
Const init_data = cell->getParam(ID::INIT); Const init_data = mem->get_init_data();
int memsize = cell->getParam(ID::SIZE).as_int();
for (int i = 0; i < memsize; i++) for (int i = 0; i < mem->size; i++)
{ {
if (i*width >= GetSize(init_data)) if (i*mem->width >= GetSize(init_data))
break; break;
Const initword = init_data.extract(i*width, width, State::Sx); Const initword = init_data.extract(i*mem->width, mem->width, State::Sx);
Const initmask = initword; Const initmask = initword;
bool gen_init_constr = false; bool gen_init_constr = false;
@ -1154,8 +1213,7 @@ struct Smt2Worker
else else
init_list.push_back(stringf("(= (bvand (select (|%s#%d#0| state) #b%s) #b%s) #b%s) ; %s[%d]", 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(), 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)); initmask.as_string().c_str(), initword.as_string().c_str(), get_id(mem->memid), i));
}
} }
} }
} }
@ -1586,7 +1644,7 @@ struct Smt2Backend : public Backend {
for (auto module : sorted_modules) 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; continue;
log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module)); log("Creating SMT-LIBv2 representation of module %s.\n", log_id(module));