The equivalence verdict in these three branches is taken from
Gia_ManAndNum(pNew) == 0 after Cec4_/Cec5_ManSimulateTest3. An AND-free GIA can
still have outputs that are constant 1 or CI literals, which are satisfiable, so
this reports "Networks are equivalent" for some non-equivalent pairs -- for
example `a & b` against `~(a & b)`, where the miter sweeps to constant 1.
Check the outputs as well: AND nodes remaining -> UNDECIDED as before; AND-free
with all outputs constant 0 -> equivalent as before; AND-free otherwise -> NOT
equivalent, which is decidable by inspection since such a miter is satisfiable.
`lutpack` aborts on some networks with
abc: src/opt/lpk/lpkAbcMux.c:192: Lpk_MuxSplit:
Assertion `iVarVac < (int)p->nVars' failed.
Reproducer (a 24.7k-LUT `sqrt` netlist produced by `if -K 10 -Z 6`, ~10 s):
read_blif sqrt-mapped.blif; lutpack
Lpk_MuxSplit() splits one component off a function and stores the new component
in a *vacant* fanin slot of the retained one:
p->uSupp = Kit_TruthSupport( Pol ? pTruth1 : pTruth0, p->nVars );
p->uSupp |= (1 << Var);
iVarVac = Kit_WordFindFirstBit( ~p->uSupp );
assert( iVarVac < (int)p->nVars );
A vacant slot is supposed to be guaranteed by Lpk_MuxAnalize(), which rejects a
candidate variable when
nSuppSizeL = max(nSuppSize0 + 2*!Polarity, nSuppSize1 + 2*Polarity) > p->nVars
but it reads nSuppSize0/nSuppSize1 out of the *cached* p->puSupps[]. When those
came from Lpk_ComputeSupports() they are not exact: that routine builds two
BDDs of the function in opposite variable orders and stitches the two support
estimates together at the cofactoring variable, and the result can be a strict
subset of the true cofactor support. Lpk_MuxAnalize() then admits a variable
whose split needs one slot more than the function has.
On the reproducer this happens for a 12-variable component at Var = 3,
Polarity = 1: the cached support of cofactor 1 is 0x3f7 (9 variables) while the
truth table's is 0xff7 (11). The guard sees 9 + 2 = 11 <= 12 and accepts;
the split then produces uSupp = 0xff7 | (1 << 3) = 0xfff, which is full.
Instrumenting the same run shows the estimate differs from the exact support in
484 of 101970 cofactor supports, and is narrower in 352 of them, so this is not
a one-off.
Rather than change the support estimator or weaken the assertion -- which
documents a real invariant of Lpk_MuxSplit() -- re-derive the single support the
split depends on, once the candidate has been chosen, and decline the MUX
decomposition when it does not fit. That is one cofactor and one support scan
per accepted candidate, not per candidate variable. On the reproducer lutpack
then completes and yields the same result as recomputing every cached support
from the truth table (24694 -> 24635 nodes, 237 levels in both cases).
ac_decomposition_impl::local_extend_to() replicates a truth table that really
depends on `real_num_vars` variables across the full `num_vars`-variable static
truth table. For real_num_vars < 6 it does so by folding the first word:
for ( auto i = real_num_vars; i < num_vars; ++i )
mask |= ( mask << ( 1 << i ) );
Once i reaches 6 the shift distance is 1 << 6 == 64, which is at least the width
of the 64-bit operand, so the shift has undefined behaviour. This is reached
whenever the cut being decomposed has more than six variables, i.e. in every
ordinary use of `if -K k -Z n` with k > 6; UBSan reports
ac_decomposition.hpp: runtime error: shift exponent 64 is too large for
64-bit type 'long unsigned int'
on, for example, `read adder.aig; strash; dch -f; if -K 11 -Z 6 -C 12`.
On x86 the shift is taken modulo 64 and the iteration happens to be a no-op, so
the observable behaviour today is correct, but that is not guaranteed by the
language and other targets shift in a saturating or unspecified way.
Variables 6 and above do not need the fold at all: the subsequent
std::fill() over the whole block array already replicates the word across every
block. Clamp the loop to the variables that live inside one word. No
behavioural change on x86.
bestPerm is only written inside the 'cost < best_cost' branch. When no
combination beats the initial best_cost -- which happens for an infeasible
free-set size -- the array is never written, yet the tail of the function still
evaluates permutations[bestPerm[i]]. That reads uninitialised stack and then
uses the value to index permutations[], so it is an out-of-bounds read as well.
Upstream results are unaffected in practice because the caller discards the
permutation on that path, but it is undefined behaviour and it becomes a hard
segfault as soon as the stack layout changes -- adding two members to the
decomposer object was enough to trigger it reliably.
Seeding the identity permutation in the existing initialisation loop is
sufficient and costs nothing.
Abc_NtkCompareSignals() sorts the PIs, POs and boxes of both networks by name
before comparing them. That is deliberate and is what lets fraig_store accept
two networks that use the same names in a different order.
When the names do not match, though, the comparison fails, Abc_NtkFraigStore()
resets the store and keeps the incoming network -- which by then has already
been sorted. The network that ends up in the store is a permutation of the one
the caller read in, and nothing reports it. The two lines printed on that path
say the store was reset; they do not say the interface changed.
Sorting is by name as a string, so numeric port names are where it shows up
worst: 1, 2, ..., 10 sort as 1, 10, 2, 3, ... With the EPFL cavlc benchmark and
its published reference netlist, whose ports are named "1".."10",
read_aiger cavlc.aig; strash; fraig_store
read_blif cavlc_size.blif; strash; fraig_store
fraig_restore; write_blif out.blif
gives an out.blif whose inputs are ordered 1, 10, 2, 3, ... instead of
1, 2, 3, ..., 10. It has the right number of inputs and outputs, it passes
Abc_NtkCheck(), and "cec -n out.blif cavlc.aig" reports a counterexample.
Save the three vectors before the comparison and put them back if it fails,
then rebuild vCis/vCos with Abc_NtkOrderCisCos(). The success path is
untouched, and so is every path where the names already agree -- those never
reach Abc_NtkCompareSignals(), since Abc_NodeCompareCiCo() has already
returned 1.
With GCC and Clang, look for the __SIZEOF_INT128__ define only defined
when __int128 is present before trying to use it.
This fixes build problem on all 32 bit Linux architectures.
Miodrag Milanovic
alanminko
Alan Mishchenko
Franz Reichl
Marcel Walter
agentic-synthesis
aiquoc
xiran
JingrenWang
Petter Reinholdtsen
Mahesh Madhav