diff --git a/src/opt/eslim/eslimCirMan.cpp b/src/opt/eslim/eslimCirMan.cpp index 5f9c5007d..f0dccccf2 100644 --- a/src/opt/eslim/eslimCirMan.cpp +++ b/src/opt/eslim/eslimCirMan.cpp @@ -506,6 +506,22 @@ namespace eSLIM { fan1negated = (fan1negated != is_node_negated[(pe->fanins[0])->node_id]); fan2negated = (fan2negated != is_node_negated[(pe->fanins[1])->node_id]); + // We need to remove gates with duplicate fanins. + // We do not use simplifyDuplicateFanins as it does not propagate duplicate fanins. + if (fan1 == fan2) { + if ((fan1negated != fan2negated ) || is_xor) { + assert (!negate_and); + node_ids[node_id] = const_false_id; + is_node_negated[node_id] = negate_and; + return const_false_id; + } else { + node_ids[node_id] = fan1; + // Gates are assumed to be normal -> x = !a && !a (x = !a || !a) is not possible. + is_node_negated[node_id] = is_node_negated[(pe->fanins[1])->node_id]; + return fan1; + } + } + int id; if (is_xor) { id = Gia_ManAppendXor(pGia, Abc_LitNotCond(fan1, fan1negated), Abc_LitNotCond(fan2, fan2negated)); @@ -523,7 +539,7 @@ namespace eSLIM { Gia_Man_t* eSLIMCirMan::eSLIMCirManToGia() { - simplifyDuplicateFanins(); + // simplifyDuplicateFanins(); Gia_Man_t * pNew = Gia_ManStart( getNofObjs() ); std::vector node_ids(nodes.size(), 0); @@ -536,15 +552,6 @@ namespace eSLIM { } for (int i = nof_pis + 1; i < nodes.size() - nof_pos; i++) { - // It is possible (but rather unlikley) that a gate has only a single fanin - // For instance it is possible that internally a gate has duplicate fanins. - // simplifyDuplicateFanins removes duplicate fanins - if (nodes[i]->getNFanins() == 1) { - eSLIMCirObj* pe = getpObj(i); - node_ids[i] = node_ids[(pe->fanins[0])->node_id]; - is_node_negated[i] = pe->tt == 1; - continue; - } assert(nodes[i]->getNFanins() == 2); addGiaGate( pNew, i, node_ids, is_node_negated ); } diff --git a/src/opt/eslim/relationSynthesiser.cpp b/src/opt/eslim/relationSynthesiser.cpp index 70a488d83..7fd507fe9 100644 --- a/src/opt/eslim/relationSynthesiser.cpp +++ b/src/opt/eslim/relationSynthesiser.cpp @@ -532,7 +532,12 @@ namespace eSLIM { std::vector clause (gate_output_variables[i].begin(), gate_output_variables[i].end()); clause.reserve(max_size - i + 1); for (int j = i + 1; j < max_size; j++) { - clause.push_back(selection_variables[j][subcir.inputs.size() + i]); + // clause.push_back(selection_variables[j][subcir.inputs.size() + i]); + int isused = getNewVariable(); + // The gate is used by another (active) gate. + solver.addClause({-isused, selection_variables[j][subcir.inputs.size() + i]}); + solver.addClause({-isused, gate_activation_variables[j]}); + clause.push_back(isused); } clause.push_back(-gate_activation_variables[i]); solver.addClause(clause);