xaiger: when -dff use (* init *) for initial state

This commit is contained in:
Eddie Hung 2020-04-13 13:10:57 -07:00
parent 95763c8d18
commit 77f3abcdc3
1 changed files with 15 additions and 3 deletions

View File

@ -79,6 +79,7 @@ struct XAigerWriter
Module *module; Module *module;
SigMap sigmap; SigMap sigmap;
dict<SigBit, State> init_map;
pool<SigBit> input_bits, output_bits; pool<SigBit> input_bits, output_bits;
dict<SigBit, SigBit> not_map, alias_map; dict<SigBit, SigBit> not_map, alias_map;
dict<SigBit, pair<SigBit, SigBit>> and_map; dict<SigBit, pair<SigBit, SigBit>> and_map;
@ -157,7 +158,8 @@ struct XAigerWriter
if (wire->get_bool_attribute(ID::keep)) if (wire->get_bool_attribute(ID::keep))
sigmap.add(wire); sigmap.add(wire);
for (auto wire : module->wires()) for (auto wire : module->wires()) {
auto it = wire->attributes.find(ID::init);
for (int i = 0; i < GetSize(wire); i++) for (int i = 0; i < GetSize(wire); i++)
{ {
SigBit wirebit(wire, i); SigBit wirebit(wire, i);
@ -184,6 +186,16 @@ struct XAigerWriter
alias_map[wirebit] = bit; alias_map[wirebit] = bit;
output_bits.insert(wirebit); output_bits.insert(wirebit);
} }
if (it != wire->attributes.end()) {
auto s = it->second[i];
if (s != State::Sx) {
auto r = init_map.insert(std::make_pair(bit, it->second[i]));
if (!r.second && r.first->second != it->second[i])
log_error("Bit '%s' has a conflicting (* init *) value.\n", log_signal(bit));
}
}
}
} }
TimingInfo timing; TimingInfo timing;
@ -632,8 +644,8 @@ struct XAigerWriter
write_r_buffer(mergeability); write_r_buffer(mergeability);
else log_abort(); else log_abort();
Const init = cell->attributes.at(ID::abc9_init); SigBit Q = sigmap(cell->getPort(ID::Q));
log_assert(GetSize(init) == 1); State init = init_map.at(Q, State::Sx);
if (init == State::S1) if (init == State::S1)
write_s_buffer(1); write_s_buffer(1);
else if (init == State::S0) else if (init == State::S0)