diff options
| author | Clifford Wolf <clifford@clifford.at> | 2016-12-01 12:00:00 +0100 |
|---|---|---|
| committer | Clifford Wolf <clifford@clifford.at> | 2016-12-01 12:00:00 +0100 |
| commit | 52c243cf05c331ef2c1ce01416e85f2fb8a70a33 (patch) | |
| tree | 05efe0d88821afe54c7e7837d6b1c53c0a6e8746 | |
| parent | 5fa1fa1e6f0dd731267f5e93d05f0223949d5c5c (diff) | |
| download | yosys-52c243cf05c331ef2c1ce01416e85f2fb8a70a33.tar.gz yosys-52c243cf05c331ef2c1ce01416e85f2fb8a70a33.tar.bz2 yosys-52c243cf05c331ef2c1ce01416e85f2fb8a70a33.zip | |
Added support for partially initialized regs to smt2 back-end
| -rw-r--r-- | backends/smt2/smt2.cc | 18 |
1 files changed, 15 insertions, 3 deletions
diff --git a/backends/smt2/smt2.cc b/backends/smt2/smt2.cc index 43479eb55..e0daae728 100644 --- a/backends/smt2/smt2.cc +++ b/backends/smt2/smt2.cc @@ -639,12 +639,24 @@ struct Smt2Worker if (wire->attributes.count("\\init")) { RTLIL::SigSpec sig = sigmap(wire); Const val = wire->attributes.at("\\init"); - val.bits.resize(GetSize(sig)); + val.bits.resize(GetSize(sig), State::Sx); if (bvmode && GetSize(sig) > 1) { - init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig).c_str(), val.as_string().c_str(), get_id(wire))); + Const mask(State::S1, GetSize(sig)); + bool use_mask = false; + for (int i = 0; i < GetSize(sig); i++) + if (val[i] != State::S0 && val[i] != State::S1) { + val[i] = State::S0; + mask[i] = State::S0; + use_mask = true; + } + if (use_mask) + init_list.push_back(stringf("(= (bvand %s #b%s) #b%s) ; %s", get_bv(sig).c_str(), mask.as_string().c_str(), val.as_string().c_str(), get_id(wire))); + else + init_list.push_back(stringf("(= %s #b%s) ; %s", get_bv(sig).c_str(), val.as_string().c_str(), get_id(wire))); } else { for (int i = 0; i < GetSize(sig); i++) - init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]).c_str(), val.bits[i] == State::S1 ? "true" : "false", get_id(wire))); + if (val[i] == State::S0 || val[i] == State::S1) + init_list.push_back(stringf("(= %s %s) ; %s", get_bool(sig[i]).c_str(), val[i] == State::S1 ? "true" : "false", get_id(wire))); } } |