From 745376d50553b75b64a332f63becd2a212f5c3b9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 16 Sep 2025 00:59:49 +0700 Subject: [PATCH 1/8] Reconstruction of structural choices. --- src/aig/gia/giaDup.c | 74 ++++++++++++++++++++++++++++++++++++++++++++ src/base/abci/abc.c | 24 +++++++++++--- 2 files changed, 94 insertions(+), 4 deletions(-) diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 8eb3e928f..d714b1ad6 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -4162,6 +4162,80 @@ Gia_Man_t * Gia_ManDupLevelized( Gia_Man_t * p ) return pNew; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDupChoicesTest( Gia_Man_t * p, Gia_Man_t * pNew ) +{ + Gia_ManCreateRefs( p ); + Gia_ManMarkFanoutDrivers( p ); + Gia_Obj_t * pObj; int i; + int ChoiceCounts[2][1000] = {{0}}; + Gia_ManForEachAnd( p, pObj, i ) + if ( Gia_ObjSibl(p, i) && pObj->fMark0 ) + { + Gia_Obj_t * pSibl, * pPrev; int Size = 1; + for ( pPrev = pObj, pSibl = Gia_ObjSiblObj(p, i); pSibl; pPrev = pSibl, pSibl = Gia_ObjSiblObj(p, Gia_ObjId(p, pSibl)) ) + Size++; + assert( Size < 1000 ); + ChoiceCounts[0][Size]++; + } + Gia_ManCleanMark0( p ); + int nSize = 1; + Gia_ManForEachAnd( pNew, pObj, i ) + if ( Gia_ObjRefNumId(p, i) == 0 ) + nSize++; + else if ( nSize > 1 ) { + assert( nSize < 1000 ); + ChoiceCounts[1][nSize]++; + nSize = 1; + } + printf( "Choice counting statistics:\n" ); + for ( i = 0; i < 1000; i++ ) + if ( ChoiceCounts[0][i] || ChoiceCounts[1][i] ) + printf( "%3d : %6d %6d\n", i, ChoiceCounts[0][i], ChoiceCounts[1][i] ); +} +void Gia_ManDupChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + if ( ~pObj->Value ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Gia_ManDupChoices_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManDupChoices_rec( pNew, p, Gia_ObjFanin1(pObj) ); + Gia_Obj_t * pSibl = Gia_ObjSiblObj(p, Gia_ObjId(p, pObj)); + if ( pSibl ) Gia_ManDupChoices_rec( pNew, p, pSibl ); + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( pSibl ) pNew->pSibls[Abc_Lit2Var(pObj->Value)] = Abc_Lit2Var(pObj->Value)-1; +} +Gia_Man_t * Gia_ManDupChoices( Gia_Man_t * p ) +{ + //Gia_ManPrintChoices( p ); + assert( p->pSibls ); + Gia_Obj_t * pObj; int i; + Gia_Man_t * pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + pNew->pSibls = ABC_CALLOC( int, Gia_ManObjNum(p) ); + Gia_ManFillValue(p); + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManForEachCo( p, pObj, i ) + Gia_ManDupChoices_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + //Gia_ManDupChoicesTest( p, pNew ); + return pNew; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 477d204c2..0931332e3 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -36126,21 +36126,26 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Dfs( Abc_Frame_t * pAbc, int argc, char ** argv ) { + extern Gia_Man_t * Gia_ManDupChoices( Gia_Man_t * p ); Gia_Man_t * pTemp; int c; int fNormal = 0; + int fChoices = 0; int fRevFans = 0; int fRevOuts = 0; int fLeveled = 0; int fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "nfolvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "ncfolvh" ) ) != EOF ) { switch ( c ) { case 'n': fNormal ^= 1; break; + case 'c': + fChoices ^= 1; + break; case 'f': fRevFans ^= 1; break; @@ -36164,7 +36169,9 @@ int Abc_CommandAbc9Dfs( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Dfs(): There is no AIG.\n" ); return 1; } - if ( fLeveled ) + if ( fChoices ) + pTemp = Gia_ManDupChoices( pAbc->pGia ); + else if ( fLeveled ) pTemp = Gia_ManDupLevelized( pAbc->pGia ); else if ( fNormal ) pTemp = Gia_ManDupOrderAiger( pAbc->pGia ); @@ -36174,9 +36181,10 @@ int Abc_CommandAbc9Dfs( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &dfs [-nfolvh]\n" ); + Abc_Print( -2, "usage: &dfs [-ncfolvh]\n" ); Abc_Print( -2, "\t orders objects in the DFS order\n" ); Abc_Print( -2, "\t-n : toggle using normalized ordering [default = %s]\n", fNormal? "yes": "no" ); + Abc_Print( -2, "\t-c : toggle using ordering for AIG with choices [default = %s]\n", fChoices? "yes": "no" ); Abc_Print( -2, "\t-f : toggle using reverse fanin traversal order [default = %s]\n", fRevFans? "yes": "no" ); Abc_Print( -2, "\t-o : toggle using reverse output traversal order [default = %s]\n", fRevOuts? "yes": "no" ); Abc_Print( -2, "\t-l : toggle using levelized order [default = %s]\n", fLeveled? "yes": "no" ); @@ -57706,6 +57714,14 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } +/* + Gia_Obj_t * pObj; int i; + Gia_ManCreateRefs(pAbc->pGia); + Gia_ManForEachAnd( pAbc->pGia, pObj, i ) + if ( !Gia_ObjIsLut(pAbc->pGia, i) && Gia_ObjRefNum(pAbc->pGia, pObj) > 1 ) + printf( "%d ", Gia_ObjRefNum(pAbc->pGia, pObj) ); + printf( "\n" ); + return 0; extern void cadical_solver_test(); cadical_solver_test(); @@ -57713,7 +57729,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void kissat_solver_test(); kissat_solver_test(); return 0; - +*/ if ( pAbc->pGia == NULL ) { Abc_Print( -1, "Abc_CommandAbc9Test(): There is no AIG.\n" ); From 08230e0c3127929348dbc579661c5f97c32f5d03 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 16 Sep 2025 02:33:08 +0700 Subject: [PATCH 2/8] Adding choice computaiton to &stochsyn. --- src/aig/gia/giaDup.c | 1 + src/aig/gia/giaStoch.c | 42 +++++++++++++++++++++++++++++++++++++++++- src/base/abci/abc.c | 19 ++++++++++++++----- 3 files changed, 56 insertions(+), 6 deletions(-) diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index d714b1ad6..c72582b05 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -4225,6 +4225,7 @@ Gia_Man_t * Gia_ManDupChoices( Gia_Man_t * p ) pNew->pSpec = Abc_UtilStrsav( p->pSpec ); pNew->pSibls = ABC_CALLOC( int, Gia_ManObjNum(p) ); Gia_ManFillValue(p); + Gia_ManConst0(p)->Value = 0; Gia_ManForEachCi( p, pObj, i ) pObj->Value = Gia_ManAppendCi(pNew); Gia_ManForEachCo( p, pObj, i ) diff --git a/src/aig/gia/giaStoch.c b/src/aig/gia/giaStoch.c index 53e491171..af6c5af7a 100644 --- a/src/aig/gia/giaStoch.c +++ b/src/aig/gia/giaStoch.c @@ -19,6 +19,8 @@ ***********************************************************************/ #include "gia.h" +#include "aig/gia/giaAig.h" +#include "proof/dch/dch.h" #include "base/main/main.h" #include "base/cmd/cmd.h" @@ -1029,13 +1031,14 @@ Vec_Wec_t * Gia_ManStochOutputs( Gia_Man_t * p, Vec_Wec_t * vAnds ) SeeAlso [] ***********************************************************************/ -void Gia_ManStochSyn( int nSuppMax, int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript, int nProcs, int fDelayOpt ) +void Gia_ManStochSyn( int nSuppMax, int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript, int nProcs, int fDelayOpt, int fChoices ) { abctime nTimeToStop = TimeOut ? Abc_Clock() + TimeOut * CLOCKS_PER_SEC : 0; abctime clkStart = Abc_Clock(); int fMapped = Gia_ManHasMapping(Abc_FrameReadGia(Abc_FrameGetGlobalFrame())); int nLutEnd, nLutBeg = fMapped ? Gia_ManLutNum(Abc_FrameReadGia(Abc_FrameGetGlobalFrame())) : 0; int i, nEnd, nBeg = Gia_ManAndNum(Abc_FrameReadGia(Abc_FrameGetGlobalFrame())); + Vec_Ptr_t * vGias = fChoices ? Vec_PtrAlloc( nIters ) : NULL; Abc_Random(1); for ( i = 0; i < 10+Seed; i++ ) Abc_Random(0); @@ -1058,6 +1061,7 @@ void Gia_ManStochSyn( int nSuppMax, int nMaxSize, int nIters, int TimeOut, int S Vec_Ptr_t * vAigs = Gia_ManDupDivide( pGia, vIns, vAnds, vOuts, pScript, nProcs, TimeOut, fDelayOpt ); Gia_Man_t * pNew = Gia_ManDupStitchMap( pGia, vIns, vAnds, vOuts, vAigs ); int fMapped = Gia_ManHasMapping(pGia) && Gia_ManHasMapping(pNew); + if ( vGias ) Vec_PtrPush( vGias, Gia_ManDup(pNew) ); Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew ); if ( fVerbose ) printf( "Iteration %3d : Using %3d partitions. Reducing %6d to %6d %s. ", @@ -1090,6 +1094,7 @@ void Gia_ManStochSyn( int nSuppMax, int nMaxSize, int nIters, int TimeOut, int S Vec_Int_t * vGains = Gia_StochProcess( vAigs, pScript, nProcs, TimeOut, 0 ); int nPartsInit = fOverlap ? Gia_ManFilterPartitions( pGia, vIns, vNodes, vOuts, vAigs, vGains, fDelayOpt ) : Vec_PtrSize(vIns); Gia_Man_t * pNew = Gia_ManDupInsertWindows( pGia, vIns, vOuts, vAigs ); Gia_ManStaticFanoutStop(pGia); + if ( vGias ) Vec_PtrPush( vGias, Gia_ManDup(pNew) ); Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew ); if ( fVerbose ) printf( "Iteration %3d : Using %3d -> %3d partitions. Reducing node count from %6d to %6d. ", @@ -1118,6 +1123,41 @@ void Gia_ManStochSyn( int nSuppMax, int nMaxSize, int nIters, int TimeOut, int S fMapped ? nLutBeg - nLutEnd : nBeg - nEnd, fMapped ? "LUTs" : "nodes", 100.0*(nBeg - nEnd)/Abc_MaxInt(nBeg, 1), nIters ); if ( fVerbose ) Abc_PrintTime( 0, "Total time", Abc_Clock() - clkStart ); + if ( vGias ) { + abctime clkStart = Abc_Clock(); + // swap around the first and the last + Gia_Man_t * pTemp = (Gia_Man_t *)Vec_PtrPop( vGias ); + Vec_PtrPush( vGias, Vec_PtrEntry(vGias,0) ); + Vec_PtrWriteEntry( vGias, 0, pTemp ); + if ( fVerbose ) { + printf( "Choicing will be performed with %d AIGs:\n", Vec_PtrSize(vGias) ); + Vec_PtrForEachEntry( Gia_Man_t *, vGias, pTemp, i ) + Gia_ManPrintStats( pTemp, NULL ); + } + Dch_Pars_t Pars, * pPars = &Pars; + Dch_ManSetDefaultParams( pPars ); + // derive the miter + Gia_Man_t * pMiter = Gia_ManChoiceMiter( vGias ); + Aig_Man_t * pAux, * pMan = Gia_ManToAigSkip( pMiter, Vec_PtrSize(vGias) ); + Gia_ManStop( pMiter ); + pMan = Dch_ComputeChoices( pAux = pMan, pPars ); + Aig_ManStop( pAux ); + // reconstruct the network + extern Vec_Ptr_t * Gia_ManOrderPios( Aig_Man_t * p, Gia_Man_t * pOrder ); + Vec_Ptr_t * vPios = Gia_ManOrderPios( pMan, Vec_PtrEntry(vGias,0) ); + pMan = Aig_ManDupDfsGuided( pAux = pMan, vPios ); + Aig_ManStop( pAux ); + Vec_PtrFree( vPios ); + // convert to GIA + Gia_Man_t * pChoices = Gia_ManFromAigChoices( pMan ); + Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pChoices ); + // cleanup + Vec_PtrForEachEntry( Gia_Man_t *, vGias, pTemp, i ) + Gia_ManStop( pTemp ); + Vec_PtrFree( vGias ); + if ( fVerbose ) + Abc_PrintTime( 0, "Choice computation time", Abc_Clock() - clkStart ); + } } //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 0931332e3..daf00dc3b 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -53698,10 +53698,10 @@ usage: ***********************************************************************/ int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Gia_ManStochSyn( int nSuppMax, int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript, int nProcs, int fDelayOpt ); - int c, nSuppMax = 0, nMaxSize = 1000, nIters = 10, TimeOut = 0, Seed = 0, nProcs = 1, fDelayOpt = 0, fVerbose = 0; char * pScript; + extern void Gia_ManStochSyn( int nSuppMax, int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript, int nProcs, int fDelayOpt, int fChoices ); + int c, nSuppMax = 0, nMaxSize = 1000, nIters = 10, TimeOut = 0, Seed = 0, nProcs = 1, fDelayOpt = 0, fChoices = 0, fVerbose = 0; char * pScript; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "NMITSPdvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "NMITSPdcvh" ) ) != EOF ) { switch ( c ) { @@ -53774,6 +53774,9 @@ int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'd': fDelayOpt ^= 1; break; + case 'c': + fChoices ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -53793,13 +53796,18 @@ int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv ) printf( "Expecting a synthesis script in quotes on the command line (for example: \"&st; &dch; &if\").\n" ); goto usage; } + if ( fChoices && nIters < 2 ) + { + printf( "The number of iterations should be more than 1.\n" ); + goto usage; + } pScript = Abc_UtilStrsav( argv[globalUtilOptind] ); - Gia_ManStochSyn( nSuppMax, nMaxSize, nIters, TimeOut, Seed, fVerbose, pScript, nProcs, fDelayOpt ); + Gia_ManStochSyn( nSuppMax, nMaxSize, nIters, TimeOut, Seed, fVerbose, pScript, nProcs, fDelayOpt, fChoices ); ABC_FREE( pScript ); return 0; usage: - Abc_Print( -2, "usage: &stochsyn [-NMITSP ] [-dvh]