Also fix write_aiger for UB

This commit is contained in:
Eddie Hung 2019-06-28 09:55:07 -07:00
parent 36e2eb06bb
commit 524af21317
1 changed files with 27 additions and 27 deletions

View File

@ -70,35 +70,35 @@ struct AigerWriter
int bit2aig(SigBit bit)
{
if (aig_map.count(bit) == 0)
{
aig_map[bit] = -1;
auto it = aig_map.find(bit);
if (it != aig_map.end()) {
log_assert(it->second >= 0);
return it->second;
}
if (initstate_bits.count(bit)) {
log_assert(initstate_ff > 0);
aig_map[bit] = initstate_ff;
} else
// NB: Cannot use iterator returned from aig_map.insert()
// since this function is called recursively
int a = -1;
if (not_map.count(bit)) {
int a = bit2aig(not_map.at(bit)) ^ 1;
aig_map[bit] = a;
a = bit2aig(not_map.at(bit)) ^ 1;
} else
if (and_map.count(bit)) {
auto args = and_map.at(bit);
int a0 = bit2aig(args.first);
int a1 = bit2aig(args.second);
aig_map[bit] = mkgate(a0, a1);
a = mkgate(a0, a1);
} else
if (alias_map.count(bit)) {
int a = bit2aig(alias_map.at(bit));
aig_map[bit] = a;
a = bit2aig(alias_map.at(bit));
}
if (bit == State::Sx || bit == State::Sz)
log_error("Design contains 'x' or 'z' bits. Use 'setundef' to replace those constants.\n");
}
log_assert(aig_map.at(bit) >= 0);
return aig_map.at(bit);
log_assert(a >= 0);
aig_map[bit] = a;
return a;
}
AigerWriter(Module *module, bool zinit_mode, bool imode, bool omode, bool bmode) : module(module), zinit_mode(zinit_mode), sigmap(module)