stv0g/yosys
1
0
Fork 0
Code Issues Pull requests Releases Wiki Activity

Added support for partially initialized regs to smt2 back-end

Browse source
This commit is contained in:
Clifford Wolf 2016-12-01 12:00:00 +01:00
parent 5fa1fa1e6f
commit 52c243cf05
1 changed files with 15 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

18
backends/smt2/smt2.cc
View file

@ -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)));
}
}