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

Fix btor init value handling 

Signed-off-by: Clifford Wolf <clifford@clifford.at>
This commit is contained in:
Clifford Wolf 2018-12-08 06:21:31 +01:00
parent 435776120a
commit ed3c57fad3
1 changed files with 13 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

22
backends/btor/btor.cc
View File

@ -506,6 +506,18 @@ struct BtorWorker
}
}
Const initval;
for (int i = 0; i < GetSize(sig_q); i++)
if (initbits.count(sig_q[i]))
initval.bits.push_back(initbits.at(sig_q[i]) ? State::S1 : State::S0);
else
initval.bits.push_back(State::Sx);
int nid_init_val = -1;
if (!initval.is_fully_undef())
nid_init_val = get_sig_nid(initval);
int sid = get_bv_sid(GetSize(sig_q));
int nid = next_nid++;
@ -514,15 +526,7 @@ struct BtorWorker
else
btorf("%d state %d %s\n", nid, sid, log_id(symbol));
Const initval;
for (int i = 0; i < GetSize(sig_q); i++)
if (initbits.count(sig_q[i]))
initval.bits.push_back(initbits.at(sig_q[i]) ? State::S1 : State::S0);
else
initval.bits.push_back(State::Sx);
if (!initval.is_fully_undef()) {
int nid_init_val = get_sig_nid(initval);
if (nid_init_val >= 0) {
int nid_init = next_nid++;
if (verbose)
btorf("; initval = %s\n", log_signal(initval));