diff --git a/src/aig/gia/giaDeep.c b/src/aig/gia/giaDeep.c index 3698c2cd7..bdd979eb2 100644 --- a/src/aig/gia/giaDeep.c +++ b/src/aig/gia/giaDeep.c @@ -43,7 +43,7 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManDeepSynOne( int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fVerbose ) +Gia_Man_t * Gia_ManDeepSynOne( int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fVerbose, Vec_Ptr_t * vGias ) { abctime nTimeToStop = TimeOut ? Abc_Clock() + TimeOut * CLOCKS_PER_SEC : 0; abctime clkStart = Abc_Clock(); @@ -100,6 +100,8 @@ Gia_Man_t * Gia_ManDeepSynOne( int nNoImpr, int TimeOut, int nAnds, int Seed, in pNew = Gia_ManDup( pTemp ); fChange = 1; iIterLast = i; + if ( vGias ) + Vec_PtrPush( vGias, Gia_ManDup(pTemp) ); } else if ( Gia_ManAndNum(pNew) + Gia_ManAndNum(pNew)/10 < Gia_ManAndNum(pTemp) ) { @@ -139,16 +141,19 @@ Gia_Man_t * Gia_ManDeepSynOne( int nNoImpr, int TimeOut, int nAnds, int Seed, in nAndsMin, nAnds, i, (float)1.0*(Abc_Clock() - clkStart)/CLOCKS_PER_SEC ); return pNew; } -Gia_Man_t * Gia_ManDeepSyn( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fVerbose ) +Gia_Man_t * Gia_ManDeepSyn( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fChoices, int fVerbose ) { + Vec_Ptr_t * vGias = fChoices ? Vec_PtrAlloc(100) : NULL; Gia_Man_t * pInit = Gia_ManDup(pGia); Gia_Man_t * pBest = Gia_ManDup(pGia); Gia_Man_t * pThis; int i; + if ( vGias ) + Vec_PtrPush( vGias, Gia_ManDup(pGia) ); for ( i = 0; i < nIters; i++ ) { Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), Gia_ManDup(pInit) ); - pThis = Gia_ManDeepSynOne( nNoImpr, TimeOut, nAnds, Seed+i, fUseTwo, fVerbose ); + pThis = Gia_ManDeepSynOne( nNoImpr, TimeOut, nAnds, Seed+i, fUseTwo, fVerbose, vGias ); if ( Gia_ManAndNum(pBest) > Gia_ManAndNum(pThis) ) { Gia_ManStop( pBest ); @@ -159,6 +164,18 @@ Gia_Man_t * Gia_ManDeepSyn( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeO } Gia_ManStop( pInit ); + if ( vGias) { + if ( Vec_PtrSize(vGias) > 1 ) { + extern Gia_Man_t * Gia_ManCreateChoicesArray( Vec_Ptr_t * vGias, int fVerbose ); + Gia_ManStopP( &pBest ); + pBest = Gia_ManCreateChoicesArray( vGias, fVerbose ); + } + // cleanup + Gia_Man_t * pTemp; + Vec_PtrForEachEntry( Gia_Man_t *, vGias, pTemp, i ) + Gia_ManStop( pTemp ); + Vec_PtrFree( vGias ); + } return pBest; } diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 8eb3e928f..c72582b05 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -4162,6 +4162,81 @@ 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_ManConst0(p)->Value = 0; + 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/aig/gia/giaStoch.c b/src/aig/gia/giaStoch.c index 53e491171..5484d0851 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,59 @@ 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 ) +Gia_Man_t * Gia_ManCreateChoicesArray( Vec_Ptr_t * vGias, int fVerbose ) +{ + 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) ); + Gia_Man_t * pTemp; int i; + 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, (Gia_Man_t *)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 ); + if ( fVerbose ) + Abc_PrintTime( 0, "Choice computation time", Abc_Clock() - clkStart ); + return pChoices; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +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 +1106,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 +1139,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 +1168,16 @@ 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 ) { + + Gia_Man_t * pChoices = Gia_ManCreateChoicesArray( vGias, fVerbose ); + Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pChoices ); + // cleanup + Gia_Man_t * pTemp; + Vec_PtrForEachEntry( Gia_Man_t *, vGias, pTemp, i ) + Gia_ManStop( pTemp ); + Vec_PtrFree( vGias ); + } } //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index fe655d1ed..7426fcf5a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -36140,21 +36140,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; @@ -36178,7 +36183,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 = pAbc->pGia->pSibls ? Gia_ManDupChoices(pAbc->pGia) : Gia_ManDup(pAbc->pGia); + else if ( fLeveled ) pTemp = Gia_ManDupLevelized( pAbc->pGia ); else if ( fNormal ) pTemp = Gia_ManDupOrderAiger( pAbc->pGia ); @@ -36188,9 +36195,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" ); @@ -53446,10 +53454,10 @@ usage: ***********************************************************************/ int Abc_CommandAbc9DeepSyn( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_ManDeepSyn( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fVerbose ); - Gia_Man_t * pTemp; int c, nIters = 1, nNoImpr = ABC_INFINITY, TimeOut = 0, nAnds = 0, Seed = 0, fUseTwo = 0, fVerbose = 0; + extern Gia_Man_t * Gia_ManDeepSyn( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fChoices, int fVerbose ); + Gia_Man_t * pTemp; int c, nIters = 1, nNoImpr = ABC_INFINITY, TimeOut = 0, nAnds = 0, Seed = 0, fUseTwo = 0, fChoices = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "IJTAStvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "IJTAStcvh" ) ) != EOF ) { switch ( c ) { @@ -53511,6 +53519,9 @@ int Abc_CommandAbc9DeepSyn( Abc_Frame_t * pAbc, int argc, char ** argv ) case 't': fUseTwo ^= 1; break; + case 'c': + fChoices ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -53525,12 +53536,12 @@ int Abc_CommandAbc9DeepSyn( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9DeepSyn(): There is no AIG.\n" ); return 0; } - pTemp = Gia_ManDeepSyn( pAbc->pGia, nIters, nNoImpr, TimeOut, nAnds, Seed, fUseTwo, fVerbose ); + pTemp = Gia_ManDeepSyn( pAbc->pGia, nIters, nNoImpr, TimeOut, nAnds, Seed, fUseTwo, fChoices, fVerbose ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: - Abc_Print( -2, "usage: &deepsyn [-IJTAS ] [-tvh]\n" ); + Abc_Print( -2, "usage: &deepsyn [-IJTAS ] [-tcvh]\n" ); Abc_Print( -2, "\t performs synthesis\n" ); Abc_Print( -2, "\t-I : the number of iterations [default = %d]\n", nIters ); Abc_Print( -2, "\t-J : the number of steps without improvements [default = %d]\n", nNoImpr ); @@ -53538,6 +53549,7 @@ usage: Abc_Print( -2, "\t-A : the number of nodes to stop (0 = no limit) [default = %d]\n", nAnds ); Abc_Print( -2, "\t-S : user-specified random seed (0 <= num <= 100) [default = %d]\n", Seed ); Abc_Print( -2, "\t-t : toggle using two-input LUTs [default = %s]\n", fUseTwo? "yes": "no" ); + Abc_Print( -2, "\t-c : toggle computing structural choices [default = %s]\n", fChoices? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -53708,10 +53720,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 ) { @@ -53784,6 +53796,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; @@ -53803,13 +53818,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]