From 480e33e308d66a782c1cf669cd85440519348c7a Mon Sep 17 00:00:00 2001 From: Trevor Hansen Date: Tue, 1 Sep 2026 16:58:34 +1000 Subject: [PATCH 1/2] aig, gia: reduce the structural hash key without a divide Aig_Hash() and Gia_ManHashOne() both end in "Key % TableSize", with TableSize read out of the manager on every call: a hardware divide by a runtime value on the hottest path either package has. Profiled over a bit-blasted query, Aig_TableInsert(), Aig_TableLookup() and Aig_TableResize() are between 66% and 80% of AIG construction, and Gia_ManHashAnd() with Gia_ManHashResize() is 86% of the GIA one. Reduce the key with two multiplies instead. Multiply it by an odd 64-bit constant and take the high half of the product, which every input bit has had an effect on, then map that onto the table by multiplying by the table size and taking the high half again. The mixing steps above are untouched, and so is every table size: Abc_PrimeCudd() still chooses it, the growth policy keeps its trigger and its factor, and no table allocates a byte it did not allocate before. A power-of-two table indexed by a mask is the shorter way to drop the divide, and it is not available here. nTableSize and pTable are public fields of Aig_Man_t, and a client that knows how many nodes it is about to build can swap in a table of its own sizing -- which one does, with a prime. A mask then collapses the table onto the buckets the size's set bits reach: over the keys of one such blast, a table of 2,191,451 buckets holding 1,890,878 keys used 512 of them, mean chain 3,693, and the blast did not finish. The reduction here leaves 1,266,734 buckets occupied against the 1,266,744 a uniform hash predicts, and costs 1.432 probes per lookup against the remainder's 1.430. A lookup decides identity by comparing fanins inside the chain walk, and a key is in the table at most once, so neither the bucket a node lands in nor the order within a chain can change which node is found. Checked rather than assumed: across six conversion levels of a bit-blasting client over 52 large queries, and its default settings over 25 fuzzer outputs, all 337 comparisons give a byte-identical CNF. What this does not buy is time. Interleaved against the same build without it on an unloaded machine, three large queries move that client's own bit-blasting timer by +0.33%, -0.28% and +0.93% at the AIG level and by +0.76%, +1.21% and -1.27% at the GIA level, every one of them inside the run-to-run spread, while retired instructions rise between 0.01% and 0.25%. The divide sits on the dependency path to the bucket load, but that load misses cache often enough to hide it. The same three queries do respond to the load factor: sizing the client's table four times larger takes 22% to 26% off the same timer, for 5.6% more peak memory. --- src/aig/aig/aigTable.c | 17 ++++++++++++++--- src/aig/gia/giaHash.c | 11 +++++++++-- 2 files changed, 23 insertions(+), 5 deletions(-) diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c index 6c2463b4d..f3e8ac544 100644 --- a/src/aig/aig/aigTable.c +++ b/src/aig/aig/aigTable.c @@ -36,14 +36,25 @@ ABC_NAMESPACE_IMPL_START // terms multiply a 0/1 flag by a small constant. Doing those two in unsigned // arithmetic is defined for every Id and keeps the result a function of the // operands alone. -static unsigned long Aig_Hash( Aig_Obj_t * pObj, int TableSize ) +// +// The mixed key is reduced to a bucket with two multiplies rather than with a +// remainder, which is a hardware divide by a runtime value on the hottest path +// this package has. The key is multiplied by an odd 64-bit constant and the +// high half of the product taken, which every input bit has had an effect on; +// that is then mapped onto the table by multiplying it by the table size and +// taking the high half again. Neither step needs the size to be a power of +// two: nTableSize is a public field and a client may size the table itself. +#define AIG_HASH_MULT ABC_CONST(0x9E3779B97F4A7C15) + +static unsigned Aig_Hash( Aig_Obj_t * pObj, int TableSize ) { - unsigned long Key = Aig_ObjIsExor(pObj) * 1699; + unsigned Key = Aig_ObjIsExor(pObj) * 1699, Hash; Key ^= (unsigned)Aig_ObjFanin0(pObj)->Id * 7937u; Key ^= (unsigned)Aig_ObjFanin1(pObj)->Id * 2971u; Key ^= Aig_ObjFaninC0(pObj) * 911; Key ^= Aig_ObjFaninC1(pObj) * 353; - return Key % TableSize; + Hash = (unsigned)(((word)Key * AIG_HASH_MULT) >> 32); + return (unsigned)(((word)Hash * (word)(unsigned)TableSize) >> 32); } // returns the place where this node is stored (or should be stored) diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c index 063cfd31a..e796e0bde 100644 --- a/src/aig/gia/giaHash.c +++ b/src/aig/gia/giaHash.c @@ -31,6 +31,12 @@ ABC_NAMESPACE_IMPL_START /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// +// The mixed key is reduced to a bucket with two multiplies rather than with a +// remainder, for the reason given over Aig_Hash() in aigTable.c: a remainder +// by a runtime table size is a hardware divide on every lookup and every +// insert, and this reduction needs no power-of-two table to avoid it. +#define GIA_HASH_MULT ABC_CONST(0x9E3779B97F4A7C15) + /**Function************************************************************* Synopsis [Returns the place where this node is stored (or should be stored).] @@ -44,12 +50,13 @@ ABC_NAMESPACE_IMPL_START ***********************************************************************/ static inline int Gia_ManHashOne( int iLit0, int iLit1, int iLitC, int TableSize ) { - unsigned Key = iLitC * 2011; + unsigned Key = iLitC * 2011, Hash; Key += Abc_Lit2Var(iLit0) * 7937; Key += Abc_Lit2Var(iLit1) * 2971; Key += Abc_LitIsCompl(iLit0) * 911; Key += Abc_LitIsCompl(iLit1) * 353; - return (int)(Key % TableSize); + Hash = (unsigned)(((word)Key * GIA_HASH_MULT) >> 32); + return (int)(((word)Hash * (word)(unsigned)TableSize) >> 32); } static inline int * Gia_ManHashFind( Gia_Man_t * p, int iLit0, int iLit1, int iLitC ) { From 3c0b4033ebd6e5e5e4dc00a126208057aed78de5 Mon Sep 17 00:00:00 2001 From: Trevor Hansen Date: Tue, 1 Sep 2026 17:05:43 +1000 Subject: [PATCH 2/2] aig: rebuild the strash table from vObjs on resize Aig_TableResize walked the old bucket chains to refill the new array, so both arrays were live across the resize and the transient was their sum. Every node the table holds is also in vObjs -- the invariant the Counter assert has always stated -- and the hash is recomputed from the fanins either way, so the rebuild can sweep vObjs instead: the old array is freed before the new one is allocated, the transient becomes the larger of the two rather than their sum, and the sweep reads nodes sequentially where chain-chasing did not. Chain order changes, which lookups cannot observe (each key exists at most once); the emitted CNF is byte-identical across the hard-set sample on both generators that drive this table. Peak RSS on real queries is unchanged, because the last resize fires mid-blast at about two thirds of the final node count and the process peak comes later -- the bound matters for callers whose footprint peaks at the resize, and the sequential sweep and earlier free are worth having regardless. --- src/aig/aig/aigTable.c | 36 ++++++++++++++++-------------------- 1 file changed, 16 insertions(+), 20 deletions(-) diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c index f3e8ac544..a0818b3a8 100644 --- a/src/aig/aig/aigTable.c +++ b/src/aig/aig/aigTable.c @@ -87,38 +87,34 @@ static Aig_Obj_t ** Aig_TableFind( Aig_Man_t * p, Aig_Obj_t * pObj ) ***********************************************************************/ void Aig_TableResize( Aig_Man_t * p ) { - Aig_Obj_t * pEntry, * pNext; - Aig_Obj_t ** pTableOld, ** ppPlace; - int nTableSizeOld, Counter, i; - abctime clk; + Aig_Obj_t * pEntry; + Aig_Obj_t ** ppPlace; + int Counter, i; assert( p->pTable != NULL ); -clk = Abc_Clock(); - // save the old table - pTableOld = p->pTable; - nTableSizeOld = p->nTableSize; - // get the new table - p->nTableSize = Abc_PrimeCudd( 2 * Aig_ManNodeNum(p) ); + // The table is rebuilt from vObjs rather than from the old buckets, so + // the old array can be freed before the new one is allocated: the + // resize transient is max(old, new) instead of their sum, and the + // sweep reads the nodes sequentially where chain-chasing did not. + // Membership is unchanged -- the table holds exactly the AND and EXOR + // nodes, which is the invariant the Counter assert below has always + // stated, and the hash is recomputed from each node's fanins either + // way. Stale pNext values from the freed chains are never read: a + // node's pNext is only walked once it is in the new table, and it is + // nulled at insertion. + ABC_FREE( p->pTable ); + p->nTableSize = Abc_PrimeCudd( 2 * Aig_ManNodeNum(p) ); p->pTable = ABC_ALLOC( Aig_Obj_t *, p->nTableSize ); memset( p->pTable, 0, sizeof(Aig_Obj_t *) * p->nTableSize ); - // rehash the entries from the old table Counter = 0; - for ( i = 0; i < nTableSizeOld; i++ ) - for ( pEntry = pTableOld[i], pNext = pEntry? pEntry->pNext : NULL; - pEntry; pEntry = pNext, pNext = pEntry? pEntry->pNext : NULL ) + Aig_ManForEachNode( p, pEntry, i ) { - // get the place where this entry goes in the table ppPlace = Aig_TableFind( p, pEntry ); assert( *ppPlace == NULL ); // should not be there - // add the entry to the list *ppPlace = pEntry; pEntry->pNext = NULL; Counter++; } assert( Counter == Aig_ManNodeNum(p) ); -// printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize ); -// ABC_PRT( "Time", Abc_Clock() - clk ); - // replace the table and the parameters - ABC_FREE( pTableOld ); } /**Function*************************************************************