diff options
| author | Clifford Wolf <clifford@clifford.at> | 2018-12-08 06:21:31 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2018-12-08 06:21:31 +0100 |
| commit | ed3c57fad3616b981e54e2f209e7ee40ff87c8a7 (patch) | |
| tree | 21882fc83046bbfbbbca2229776c2818b198867f /backends/btor | |
| parent | 435776120a40ed06ea42ca63bcca231913507ac3 (diff) | |
| download | yosys-ed3c57fad3616b981e54e2f209e7ee40ff87c8a7.tar.gz yosys-ed3c57fad3616b981e54e2f209e7ee40ff87c8a7.tar.bz2 yosys-ed3c57fad3616b981e54e2f209e7ee40ff87c8a7.zip | |
Fix btor init value handling
Signed-off-by: Clifford Wolf <clifford@clifford.at>
Diffstat (limited to 'backends/btor')
| -rw-r--r-- | backends/btor/btor.cc | 22 |
1 files changed, 13 insertions, 9 deletions
diff --git a/backends/btor/btor.cc b/backends/btor/btor.cc index 58d2a8625..ab2702807 100644 --- a/backends/btor/btor.cc +++ b/backends/btor/btor.cc @@ -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)); |