From 77f3abcdc30e21b4359c2b07c20b63bdac5993bf Mon Sep 17 00:00:00 2001 From: Eddie Hung Date: Mon, 13 Apr 2020 13:10:57 -0700 Subject: xaiger: when -dff use (* init *) for initial state --- backends/aiger/xaiger.cc | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) (limited to 'backends') diff --git a/backends/aiger/xaiger.cc b/backends/aiger/xaiger.cc index 2e2ca7018..5d15df310 100644 --- a/backends/aiger/xaiger.cc +++ b/backends/aiger/xaiger.cc @@ -79,6 +79,7 @@ struct XAigerWriter Module *module; SigMap sigmap; + dict init_map; pool input_bits, output_bits; dict not_map, alias_map; dict> and_map; @@ -157,7 +158,8 @@ struct XAigerWriter if (wire->get_bool_attribute(ID::keep)) 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++) { SigBit wirebit(wire, i); @@ -184,7 +186,17 @@ struct XAigerWriter alias_map[wirebit] = bit; 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; @@ -632,8 +644,8 @@ struct XAigerWriter write_r_buffer(mergeability); else log_abort(); - Const init = cell->attributes.at(ID::abc9_init); - log_assert(GetSize(init) == 1); + SigBit Q = sigmap(cell->getPort(ID::Q)); + State init = init_map.at(Q, State::Sx); if (init == State::S1) write_s_buffer(1); else if (init == State::S0) -- cgit v1.2.3