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

Add support for memory initialization to write_btor 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2019-03-23 14:40:01 +01:00
parent e78f5a3055
commit 1eff8be8f0
1 changed files with 53 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

53
backends/btor/btor.cc
View File

@ -615,6 +615,7 @@ struct BtorWorker
{
int abits = cell->getParam("\\ABITS").as_int();
int width = cell->getParam("\\WIDTH").as_int();
int nwords = cell->getParam("\\SIZE").as_int();
int rdports = cell->getParam("\\RD_PORTS").as_int();
int wrports = cell->getParam("\\WR_PORTS").as_int();
@ -641,6 +642,52 @@ struct BtorWorker
int data_sid = get_bv_sid(width);
int bool_sid = get_bv_sid(1);
int sid = get_mem_sid(abits, width);
Const initdata = cell->getParam("\\INIT");
initdata.exts(nwords*width);
int nid_init_val = -1;
if (!initdata.is_fully_undef())
{
bool constword = true;
Const firstword = initdata.extract(0, width);
for (int i = 1; i < nwords; i++) {
Const thisword = initdata.extract(i*width, width);
if (thisword != firstword) {
constword = false;
break;
}
}
if (constword)
{
if (verbose)
btorf("; initval = %s\n", log_signal(firstword));
nid_init_val = get_sig_nid(firstword);
}
else
{
int 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);
if (thisword.is_fully_undef())
continue;
Const thisaddr(i, abits);
int nid_thisword = get_sig_nid(thisword);
int nid_thisaddr = get_sig_nid(thisaddr);
int last_nid_init_val = nid_init_val;
nid_init_val = next_nid++;
if (verbose)
btorf("; initval[%d] = %s\n", i, log_signal(thisword));
btorf("%d write %d %d %d %d\n", nid_init_val, sid, last_nid_init_val, nid_thisaddr, nid_thisword);
}
}
}
int nid = next_nid++;
int nid_head = nid;
@ -649,6 +696,12 @@ struct BtorWorker
else
btorf("%d state %d %s\n", nid, sid, log_id(cell));
if (nid_init_val >= 0)
{
int nid_init = next_nid++;
btorf("%d init %d %d %d\n", nid_init, sid, nid, nid_init_val);
}
if (asyncwr)
{
for (int port = 0; port < wrports; port++)