luke/yosys
1
0
Fork 0
mirror of https://github.com/YosysHQ/yosys.git synced 2026-08-22 14:17:27 +02:00
Code Issues Packages Projects Releases Wiki Activity

Fix smt2 code generation for partially initialized memowy words, fixes #831

Browse Source 
Signed-off-by: Clifford Wolf <[email protected]>
This commit is contained in:
Clifford Wolf
2019-02-28 12:15:58 -08:00
parent 5e94a8a127
commit f570aa5e1d
1 changed files with 11 additions and 4 deletions
Download Patch File Download Diff File Expand all files Collapse all files
backends/smt2/smt2.cc
+11 -4
View File
@@ -1103,20 +1103,27 @@ struct Smt2Worker
break; break;
Const initword = init_data.extract(i*width, width, State::Sx); Const initword = init_data.extract(i*width, width, State::Sx);
Const initmask = initword;
bool gen_init_constr = false; bool gen_init_constr = false;
for (auto bit : initword.bits) for (int k = 0; k < GetSize(initword); k++) {
if (bit == State::S0 || bit == State::S1) if (initword[k] == State::S0 || initword[k] == State::S1) {
gen_init_constr = true; gen_init_constr = true;
initmask[k] = State::S1;
} else {
initmask[k] = State::S0;
initword[k] = State::S0;
}
}
if (gen_init_constr) if (gen_init_constr)
{ {
if (statebv) if (statebv)
/* FIXME */; /* FIXME */;
else else
init_list.push_back(stringf("(= (select (|%s#%d#0| state) #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(),
initword.as_string().c_str(), get_id(cell), i)); initmask.as_string().c_str(), initword.as_string().c_str(), get_id(cell), i));
} }
} }
} }