write_xaiger2: fix function argument evaluation order

This commit is contained in:
Lofty 2026-03-31 10:22:17 +01:00
parent 162eeea29a
commit 568a31c83a
1 changed files with 35 additions and 12 deletions

View File

@ -197,7 +197,9 @@ struct Index {
Lit OR(Lit a, Lit b)
{
return NOT(AND(NOT(a), NOT(b)));
Lit not_a = NOT(a);
Lit not_b = NOT(b);
return NOT(AND(not_a, not_b));
}
Lit MUX(Lit a, Lit b, Lit s)
@ -211,17 +213,24 @@ struct Index {
return b;
}
return OR(AND(a, NOT(s)), AND(b, s));
Lit not_s = NOT(s);
Lit a_active = AND(a, not_s);
Lit b_active = AND(b, s);
return OR(a_active, b_active);
}
Lit XOR(Lit a, Lit b)
{
return OR(AND(a, NOT(b)), AND(NOT(a), b));
Lit not_a = NOT(a);
Lit not_b = NOT(b);
Lit a_and_not_b = AND(a, not_b);
Lit not_a_and_b = AND(not_a, b);
return OR(a_and_not_b, not_a_and_b);
}
Lit XNOR(Lit a, Lit b)
{
return NOT(OR(AND(a, NOT(b)), AND(NOT(a), b)));
return NOT(XOR(a, b));
}
Lit CARRY(Lit a, Lit b, Lit c)
@ -233,7 +242,10 @@ struct Index {
return AND(a, b);
}
}
return OR(AND(a, b), AND(c, OR(a, b)));
Lit a_or_b = OR(a, b);
Lit a_or_b_and_c = AND(c, a_or_b);
Lit a_and_b = AND(a, b);
return OR(a_and_b, a_or_b_and_c);
}
Lit REDUCE(std::vector<Lit> lits, bool op_xor=false)
@ -381,7 +393,7 @@ struct Index {
} else if (cell->type.in(ID($xor), ID($_XOR_))) {
return XOR(a, b);
} else if (cell->type.in(ID($xnor), ID($_XNOR_))) {
return NOT(XOR(a, b));
return XNOR(a, b);
} else if (cell->type.in(ID($_ANDNOT_))) {
return AND(a, NOT(b));
} else if (cell->type.in(ID($_ORNOT_))) {
@ -401,7 +413,9 @@ struct Index {
if (oport == ID::Y) {
return XOR(ab, c);
} else /* oport == ID::X */ {
return OR(AND(a, b), AND(c, ab));
Lit a_and_b = AND(a, b);
Lit c_and_ab = AND(c, ab);
return OR(a_and_b, c_and_ab);
}
} else if (cell->type.in(ID($_AOI3_), ID($_OAI3_), ID($_AOI4_), ID($_OAI4_))) {
Lit c, d;
@ -412,10 +426,15 @@ struct Index {
else
d = cell->type == ID($_AOI3_) ? CTRUE : CFALSE;
if (/* aoi */ cell->type.in(ID($_AOI3_), ID($_AOI4_)))
return NOT(OR(AND(a, b), AND(c, d)));
else
return NOT(AND(OR(a, b), OR(c, d)));
if (/* aoi */ cell->type.in(ID($_AOI3_), ID($_AOI4_))) {
Lit a_and_b = AND(a, b);
Lit c_and_d = AND(c, d);
return NOT(OR(a_and_b, c_and_d));
} else {
Lit a_or_b = OR(a, b);
Lit c_or_d = OR(c, d);
return NOT(AND(a_or_b, c_or_d));
}
} else {
log_abort();
}
@ -436,7 +455,11 @@ struct Index {
sels.push_back(NOT(s));
}
return OR(AND(REDUCE(sels), a), NOT(REDUCE(bar)));
Lit reduce_sels = REDUCE(sels);
Lit reduce_sels_and_a = AND(reduce_sels, a);
Lit reduce_bar = NOT(REDUCE(bar));
return OR(reduce_sels_and_a, reduce_bar);
} else if (cell->type == ID($bmux)) {
SigSpec aport = cell->getPort(ID::A);
SigSpec sport = cell->getPort(ID::S);