mirror of
https://github.com/YosysHQ/yosys
synced 2025-11-04 05:19:11 +00:00
btor: Use Mem helper.
This commit is contained in:
Marcelina Kościelnicka
parent
f272c8b407
commit
2d340cd355
1 changed files with 116 additions and 107 deletions
|
|
@ -27,6 +27,7 @@
|
|||
#include "kernel/sigtools.h"
|
||||
#include "kernel/celltypes.h"
|
||||
#include "kernel/log.h"
|
||||
#include "kernel/mem.h"
|
||||
#include <string>
|
||||
|
||||
USING_YOSYS_NAMESPACE
|
||||
|
|
@ -68,12 +69,15 @@ struct BtorWorker
|
|||
|
||||
// ff inputs that need to be evaluated (<nid>, <ff_cell>)
|
||||
vector<pair<int, Cell*>> ff_todo;
|
||||
vector<pair<int, Mem*>> mem_todo;
|
||||
|
||||
pool<Cell*> cell_recursion_guard;
|
||||
vector<int> bad_properties;
|
||||
dict<SigBit, bool> initbits;
|
||||
pool<Wire*> statewires;
|
||||
pool<string> srcsymbols;
|
||||
vector<Mem> memories;
|
||||
dict<Cell*, Mem*> mem_cells;
|
||||
|
||||
string indent, info_filename;
|
||||
vector<string> info_lines;
|
||||
|
|
@ -704,49 +708,45 @@ struct BtorWorker
|
|||
goto okay;
|
||||
}
|
||||
|
||||
if (cell->type == ID($mem))
|
||||
if (cell->type.in(ID($mem), ID($memrd), ID($memwr), ID($meminit)))
|
||||
{
|
||||
int abits = cell->getParam(ID::ABITS).as_int();
|
||||
int width = cell->getParam(ID::WIDTH).as_int();
|
||||
int nwords = cell->getParam(ID::SIZE).as_int();
|
||||
int rdports = cell->getParam(ID::RD_PORTS).as_int();
|
||||
int wrports = cell->getParam(ID::WR_PORTS).as_int();
|
||||
Mem *mem = mem_cells[cell];
|
||||
|
||||
Const wr_clk_en = cell->getParam(ID::WR_CLK_ENABLE);
|
||||
Const rd_clk_en = cell->getParam(ID::RD_CLK_ENABLE);
|
||||
int abits = ceil_log2(mem->size);
|
||||
|
||||
bool asyncwr = wr_clk_en.is_fully_zero();
|
||||
bool asyncwr = false;
|
||||
bool syncwr = false;
|
||||
|
||||
if (!asyncwr && !wr_clk_en.is_fully_ones())
|
||||
for (auto &port : mem->wr_ports) {
|
||||
if (port.clk_enable)
|
||||
syncwr = true;
|
||||
else
|
||||
asyncwr = true;
|
||||
}
|
||||
|
||||
if (asyncwr && syncwr)
|
||||
log_error("Memory %s.%s has mixed async/sync write ports.\n",
|
||||
log_id(module), log_id(cell));
|
||||
log_id(module), log_id(mem->memid));
|
||||
|
||||
if (!rd_clk_en.is_fully_zero())
|
||||
log_error("Memory %s.%s has sync read ports.\n",
|
||||
log_id(module), log_id(cell));
|
||||
for (auto &port : mem->rd_ports)
|
||||
if (port.clk_enable)
|
||||
log_error("Memory %s.%s has sync read ports.\n",
|
||||
log_id(module), log_id(mem->memid));
|
||||
|
||||
SigSpec sig_rd_addr = sigmap(cell->getPort(ID::RD_ADDR));
|
||||
SigSpec sig_rd_data = sigmap(cell->getPort(ID::RD_DATA));
|
||||
|
||||
SigSpec sig_wr_addr = sigmap(cell->getPort(ID::WR_ADDR));
|
||||
SigSpec sig_wr_data = sigmap(cell->getPort(ID::WR_DATA));
|
||||
SigSpec sig_wr_en = sigmap(cell->getPort(ID::WR_EN));
|
||||
|
||||
int data_sid = get_bv_sid(width);
|
||||
int data_sid = get_bv_sid(mem->width);
|
||||
int bool_sid = get_bv_sid(1);
|
||||
int sid = get_mem_sid(abits, width);
|
||||
int sid = get_mem_sid(abits, mem->width);
|
||||
|
||||
Const initdata = cell->getParam(ID::INIT);
|
||||
initdata.exts(nwords*width);
|
||||
int nid_init_val = -1;
|
||||
|
||||
if (!initdata.is_fully_undef())
|
||||
if (!mem->inits.empty())
|
||||
{
|
||||
Const initdata = mem->get_init_data();
|
||||
bool constword = true;
|
||||
Const firstword = initdata.extract(0, width);
|
||||
Const firstword = initdata.extract(0, mem->width);
|
||||
|
||||
for (int i = 1; i < nwords; i++) {
|
||||
Const thisword = initdata.extract(i*width, width);
|
||||
for (int i = 1; i < mem->size; i++) {
|
||||
Const thisword = initdata.extract(i*mem->width, mem->width);
|
||||
if (thisword != firstword) {
|
||||
constword = false;
|
||||
break;
|
||||
|
|
@ -764,8 +764,8 @@ struct BtorWorker
|
|||
nid_init_val = next_nid++;
|
||||
btorf("%d state %d\n", nid_init_val, sid);
|
||||
|
||||
for (int i = 0; i < nwords; i++) {
|
||||
Const thisword = initdata.extract(i*width, width);
|
||||
for (int i = 0; i < mem->size; i++) {
|
||||
Const thisword = initdata.extract(i*mem->width, mem->width);
|
||||
if (thisword.is_fully_undef())
|
||||
continue;
|
||||
Const thisaddr(i, abits);
|
||||
|
|
@ -784,10 +784,10 @@ struct BtorWorker
|
|||
int nid = next_nid++;
|
||||
int nid_head = nid;
|
||||
|
||||
if (cell->name[0] == '$')
|
||||
if (mem->memid[0] == '$')
|
||||
btorf("%d state %d\n", nid, sid);
|
||||
else
|
||||
btorf("%d state %d %s\n", nid, sid, log_id(cell));
|
||||
btorf("%d state %d %s\n", nid, sid, log_id(mem->memid));
|
||||
|
||||
if (nid_init_val >= 0)
|
||||
{
|
||||
|
|
@ -797,15 +797,14 @@ struct BtorWorker
|
|||
|
||||
if (asyncwr)
|
||||
{
|
||||
for (int port = 0; port < wrports; port++)
|
||||
for (auto &port : mem->wr_ports)
|
||||
{
|
||||
SigSpec wa = sig_wr_addr.extract(port*abits, abits);
|
||||
SigSpec wd = sig_wr_data.extract(port*width, width);
|
||||
SigSpec we = sig_wr_en.extract(port*width, width);
|
||||
SigSpec wa = port.addr;
|
||||
wa.extend_u0(abits);
|
||||
|
||||
int wa_nid = get_sig_nid(wa);
|
||||
int wd_nid = get_sig_nid(wd);
|
||||
int we_nid = get_sig_nid(we);
|
||||
int wd_nid = get_sig_nid(port.data);
|
||||
int we_nid = get_sig_nid(port.en);
|
||||
|
||||
int nid2 = next_nid++;
|
||||
btorf("%d read %d %d %d\n", nid2, data_sid, nid_head, wa_nid);
|
||||
|
|
@ -835,22 +834,22 @@ struct BtorWorker
|
|||
}
|
||||
}
|
||||
|
||||
for (int port = 0; port < rdports; port++)
|
||||
for (auto &port : mem->rd_ports)
|
||||
{
|
||||
SigSpec ra = sig_rd_addr.extract(port*abits, abits);
|
||||
SigSpec rd = sig_rd_data.extract(port*width, width);
|
||||
SigSpec ra = port.addr;
|
||||
ra.extend_u0(abits);
|
||||
|
||||
int ra_nid = get_sig_nid(ra);
|
||||
int rd_nid = next_nid++;
|
||||
|
||||
btorf("%d read %d %d %d\n", rd_nid, data_sid, nid_head, ra_nid);
|
||||
|
||||
add_nid_sig(rd_nid, rd);
|
||||
add_nid_sig(rd_nid, port.data);
|
||||
}
|
||||
|
||||
if (!asyncwr)
|
||||
{
|
||||
ff_todo.push_back(make_pair(nid, cell));
|
||||
mem_todo.push_back(make_pair(nid, mem));
|
||||
}
|
||||
else
|
||||
{
|
||||
|
|
@ -1065,6 +1064,15 @@ struct BtorWorker
|
|||
if (!info_filename.empty())
|
||||
infof("name %s\n", log_id(module));
|
||||
|
||||
memories = Mem::get_all_memories(module);
|
||||
|
||||
dict<IdString, Mem*> mem_dict;
|
||||
for (auto &mem : memories)
|
||||
mem_dict[mem.memid] = &mem;
|
||||
for (auto cell : module->cells())
|
||||
if (cell->type.in(ID($mem), ID($memwr), ID($memrd), ID($meminit)))
|
||||
mem_cells[cell] = mem_dict[cell->parameters.at(ID::MEMID).decode_string()];
|
||||
|
||||
btorf_push("inputs");
|
||||
|
||||
for (auto wire : module->wires())
|
||||
|
|
@ -1201,7 +1209,7 @@ struct BtorWorker
|
|||
continue;
|
||||
}
|
||||
|
||||
while (!ff_todo.empty())
|
||||
while (!ff_todo.empty() || !mem_todo.empty())
|
||||
{
|
||||
vector<pair<int, Cell*>> todo;
|
||||
todo.swap(ff_todo);
|
||||
|
|
@ -1213,71 +1221,72 @@ struct BtorWorker
|
|||
|
||||
btorf_push(stringf("next %s", log_id(cell)));
|
||||
|
||||
if (cell->type == ID($mem))
|
||||
{
|
||||
int abits = cell->getParam(ID::ABITS).as_int();
|
||||
int width = cell->getParam(ID::WIDTH).as_int();
|
||||
int wrports = cell->getParam(ID::WR_PORTS).as_int();
|
||||
|
||||
SigSpec sig_wr_addr = sigmap(cell->getPort(ID::WR_ADDR));
|
||||
SigSpec sig_wr_data = sigmap(cell->getPort(ID::WR_DATA));
|
||||
SigSpec sig_wr_en = sigmap(cell->getPort(ID::WR_EN));
|
||||
|
||||
int data_sid = get_bv_sid(width);
|
||||
int bool_sid = get_bv_sid(1);
|
||||
int sid = get_mem_sid(abits, width);
|
||||
int nid_head = nid;
|
||||
|
||||
for (int port = 0; port < wrports; port++)
|
||||
{
|
||||
SigSpec wa = sig_wr_addr.extract(port*abits, abits);
|
||||
SigSpec wd = sig_wr_data.extract(port*width, width);
|
||||
SigSpec we = sig_wr_en.extract(port*width, width);
|
||||
|
||||
int wa_nid = get_sig_nid(wa);
|
||||
int wd_nid = get_sig_nid(wd);
|
||||
int we_nid = get_sig_nid(we);
|
||||
|
||||
int nid2 = next_nid++;
|
||||
btorf("%d read %d %d %d\n", nid2, data_sid, nid_head, wa_nid);
|
||||
|
||||
int nid3 = next_nid++;
|
||||
btorf("%d not %d %d\n", nid3, data_sid, we_nid);
|
||||
|
||||
int nid4 = next_nid++;
|
||||
btorf("%d and %d %d %d\n", nid4, data_sid, nid2, nid3);
|
||||
|
||||
int nid5 = next_nid++;
|
||||
btorf("%d and %d %d %d\n", nid5, data_sid, wd_nid, we_nid);
|
||||
|
||||
int nid6 = next_nid++;
|
||||
btorf("%d or %d %d %d\n", nid6, data_sid, nid5, nid4);
|
||||
|
||||
int nid7 = next_nid++;
|
||||
btorf("%d write %d %d %d %d\n", nid7, sid, nid_head, wa_nid, nid6);
|
||||
|
||||
int nid8 = next_nid++;
|
||||
btorf("%d redor %d %d\n", nid8, bool_sid, we_nid);
|
||||
|
||||
int nid9 = next_nid++;
|
||||
btorf("%d ite %d %d %d %d\n", nid9, sid, nid8, nid7, nid_head);
|
||||
|
||||
nid_head = nid9;
|
||||
}
|
||||
|
||||
int nid2 = next_nid++;
|
||||
btorf("%d next %d %d %d%s\n", nid2, sid, nid, nid_head, getinfo(cell).c_str());
|
||||
}
|
||||
else
|
||||
{
|
||||
SigSpec sig = sigmap(cell->getPort(ID::D));
|
||||
int nid_q = get_sig_nid(sig);
|
||||
int sid = get_bv_sid(GetSize(sig));
|
||||
btorf("%d next %d %d %d%s\n", next_nid++, sid, nid, nid_q, getinfo(cell).c_str());
|
||||
}
|
||||
SigSpec sig = sigmap(cell->getPort(ID::D));
|
||||
int nid_q = get_sig_nid(sig);
|
||||
int sid = get_bv_sid(GetSize(sig));
|
||||
btorf("%d next %d %d %d%s\n", next_nid++, sid, nid, nid_q, getinfo(cell).c_str());
|
||||
|
||||
btorf_pop(stringf("next %s", log_id(cell)));
|
||||
}
|
||||
|
||||
vector<pair<int, Mem*>> mtodo;
|
||||
mtodo.swap(mem_todo);
|
||||
|
||||
for (auto &it : mtodo)
|
||||
{
|
||||
int nid = it.first;
|
||||
Mem *mem = it.second;
|
||||
|
||||
btorf_push(stringf("next %s", log_id(mem->memid)));
|
||||
|
||||
int abits = ceil_log2(mem->size);
|
||||
|
||||
int data_sid = get_bv_sid(mem->width);
|
||||
int bool_sid = get_bv_sid(1);
|
||||
int sid = get_mem_sid(abits, mem->width);
|
||||
int nid_head = nid;
|
||||
|
||||
for (auto &port : mem->wr_ports)
|
||||
{
|
||||
SigSpec wa = port.addr;
|
||||
wa.extend_u0(abits);
|
||||
|
||||
int wa_nid = get_sig_nid(wa);
|
||||
int wd_nid = get_sig_nid(port.data);
|
||||
int we_nid = get_sig_nid(port.en);
|
||||
|
||||
int nid2 = next_nid++;
|
||||
btorf("%d read %d %d %d\n", nid2, data_sid, nid_head, wa_nid);
|
||||
|
||||
int nid3 = next_nid++;
|
||||
btorf("%d not %d %d\n", nid3, data_sid, we_nid);
|
||||
|
||||
int nid4 = next_nid++;
|
||||
btorf("%d and %d %d %d\n", nid4, data_sid, nid2, nid3);
|
||||
|
||||
int nid5 = next_nid++;
|
||||
btorf("%d and %d %d %d\n", nid5, data_sid, wd_nid, we_nid);
|
||||
|
||||
int nid6 = next_nid++;
|
||||
btorf("%d or %d %d %d\n", nid6, data_sid, nid5, nid4);
|
||||
|
||||
int nid7 = next_nid++;
|
||||
btorf("%d write %d %d %d %d\n", nid7, sid, nid_head, wa_nid, nid6);
|
||||
|
||||
int nid8 = next_nid++;
|
||||
btorf("%d redor %d %d\n", nid8, bool_sid, we_nid);
|
||||
|
||||
int nid9 = next_nid++;
|
||||
btorf("%d ite %d %d %d %d\n", nid9, sid, nid8, nid7, nid_head);
|
||||
|
||||
nid_head = nid9;
|
||||
}
|
||||
|
||||
int nid2 = next_nid++;
|
||||
btorf("%d next %d %d %d%s\n", nid2, sid, nid, nid_head, (mem->cell ? getinfo(mem->cell) : getinfo(mem->mem)).c_str());
|
||||
|
||||
btorf_pop(stringf("next %s", log_id(mem->memid)));
|
||||
}
|
||||
}
|
||||
|
||||
while (!bad_properties.empty())
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue