From 61e74a103316421888004794e9e74dcac9d94dd2 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 16 Jun 2026 07:52:19 -0700 Subject: [PATCH] Update high-effort synthesis. --- src/aig/gia/giaDeep.c | 303 +++++++++++++++++++++++++++++++++++++++++- 1 file changed, 301 insertions(+), 2 deletions(-) diff --git a/src/aig/gia/giaDeep.c b/src/aig/gia/giaDeep.c index 9d2a2c875..9c506eab5 100644 --- a/src/aig/gia/giaDeep.c +++ b/src/aig/gia/giaDeep.c @@ -238,6 +238,229 @@ Gia_Man_t * Gia_ManRandSyn( Gia_Man_t * p, unsigned random_seed ) return pRes; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Gia_ManDeepSynParetoUpdate( Vec_Ptr_t * vPareto, Gia_Man_t * pCand, int nLevels, int nAnds ) +{ + Gia_Man_t * pBest = (Gia_Man_t *)Vec_PtrGetEntry( vPareto, nLevels ); + if ( pBest == NULL || Gia_ManAndNum(pBest) > nAnds ) + { + if ( pBest ) + Gia_ManStop( pBest ); + Vec_PtrSetEntry( vPareto, nLevels, Gia_ManDup(pCand) ); + } +} + +static void Gia_ManDeepSynParetoPrint( Vec_Ptr_t * vPareto ) +{ + Gia_Man_t * pTemp; + int i, fFirst = 1; + printf( "Pareto points:" ); + Vec_PtrForEachEntry( Gia_Man_t *, vPareto, pTemp, i ) + { + if ( pTemp == NULL ) + continue; + printf( "%s%d:%d", fFirst ? " " : " ", i, Gia_ManAndNum(pTemp) ); + fFirst = 0; + } + if ( fFirst ) + printf( " none" ); + printf( "\n" ); +} + +static void Gia_ManDeepSynParetoSave( Vec_Ptr_t * vPareto, char * pBase ) +{ + Gia_Man_t * pTemp; + char FileName[1000]; + int i; + if ( pBase == NULL ) + pBase = Extra_UtilStrsav( "gia" ); + Vec_PtrForEachEntry( Gia_Man_t *, vPareto, pTemp, i ) + { + if ( pTemp == NULL ) + continue; + sprintf( FileName, "%s_%d_%d.aig", pBase, i, Gia_ManAndNum(pTemp) ); + Gia_AigerWrite( pTemp, FileName, 0, 0, 0 ); + } + ABC_FREE( pBase ); +} + +Gia_Man_t * Gia_ManDeepSynOne2( int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fVerbose, Vec_Ptr_t * vGias, Vec_Ptr_t * vPareto ) +{ + abctime nTimeToStop = TimeOut ? Abc_Clock() + TimeOut * CLOCKS_PER_SEC : 0; + abctime clkStart = Abc_Clock(); + int s, i, k, IterMax = 100000, nLevelsMin = -1, nAndsMin = -1; + int nNoImprCount = 0; + Gia_Man_t * pTemp = Abc_FrameReadGia(Abc_FrameGetGlobalFrame()); + Gia_Man_t * pNew = Gia_ManDup( pTemp ); + (void)fUseTwo; + Abc_Random(1); + for ( s = 0; s < 10+Seed; s++ ) + Abc_Random(0); + nLevelsMin = Gia_ManLevelNum(pNew); + nAndsMin = Gia_ManAndNum(pNew); + for ( i = 0; i < IterMax; ) + { + unsigned Rand = Abc_Random(0); + int fDch = Rand & 1; + int fResyn = (Rand >> 1) % 3; + int fChange = 0; + char Command[2000]; + char pResyn[200]; + if ( fResyn == 0 ) + sprintf( pResyn, "&resyn3" ); + else if ( fResyn == 1 ) + sprintf( pResyn, "&resyn3rs" ); + else + sprintf( pResyn, "&resyn3; &resyn3rs" ); + sprintf( Command, "&dch%s; &if -y -K 6; %s", fDch ? " -f" : "", pResyn ); + if ( Abc_FrameIsBatchMode() ) + { + if ( Cmd_CommandExecute(Abc_FrameGetGlobalFrame(), Command) ) + { + Abc_Print( 1, "Something did not work out with the command \"%s\".\n", Command ); + return NULL; + } + } + else + { + Abc_FrameSetBatchMode( 1 ); + if ( Cmd_CommandExecute(Abc_FrameGetGlobalFrame(), Command) ) + { + Abc_Print( 1, "Something did not work out with the command \"%s\".\n", Command ); + return NULL; + } + Abc_FrameSetBatchMode( 0 ); + } + pTemp = Abc_FrameReadGia(Abc_FrameGetGlobalFrame()); + { + int nLevelTemp = Gia_ManLevelNum(pTemp); + int nAndsTemp = Gia_ManAndNum(pTemp); + if ( vPareto ) + Gia_ManDeepSynParetoUpdate( vPareto, pTemp, nLevelTemp, nAndsTemp ); + if ( nLevelsMin > nLevelTemp || (nLevelsMin == nLevelTemp && nAndsMin > nAndsTemp) ) + { + Gia_ManStop( pNew ); + pNew = Gia_ManDup( pTemp ); + nLevelsMin = nLevelTemp; + nAndsMin = nAndsTemp; + fChange = 1; + if ( vGias ) + Vec_PtrPush( vGias, Gia_ManDup(pTemp) ); + nNoImprCount = 0; + } + else + nNoImprCount++; + } + if ( fChange && fVerbose ) + { + printf( "Iter %6d : ", i ); + printf( "Time %8.2f sec : ", (float)1.0*(Abc_Clock() - clkStart)/CLOCKS_PER_SEC ); + printf( "Lev = %3d ", nLevelsMin ); + printf( "And = %6d ", nAndsMin ); + printf( "<== best : " ); + printf( "%s", Command ); + printf( "\n" ); + } + if ( nTimeToStop && Abc_Clock() > nTimeToStop ) + { + if ( !Abc_FrameIsBatchMode() ) + printf( "Runtime limit (%d sec) is reached after %d iterations.\n", TimeOut, i ); + break; + } + i++; + if ( nNoImprCount > nNoImpr ) + { + int nOuter = 1 + (Abc_Random(0) % 3); + int nKmax = nAnds ? nAnds : 6; + int nKmin = 3; + int nLuts[3]; + if ( nKmax < nKmin ) + nKmin = nKmax; + for ( k = 0; k < nOuter; k++ ) + nLuts[k] = nKmin + (Abc_Random(0) % (nKmax - nKmin + 1)); + if ( fVerbose ) + { + printf( "Completed %d iterations without improvement. Trying %d outer iterations with ", nNoImpr, nOuter ); + for ( k = 0; k < nOuter; k++ ) + printf( "%sK=%d", k ? ", " : "", nLuts[k] ); + printf( ". Time = %.2f sec\n", (float)1.0*(Abc_Clock() - clkStart)/CLOCKS_PER_SEC ); + } + nNoImprCount = 0; + for ( k = 0; k < nOuter && i < IterMax; k++ ) + { + int nLut = nLuts[k]; + int fOuterChange = 0; + sprintf( Command, "&dch; &if -K %d -m; &mfs; &st", nLut ); + if ( Abc_FrameIsBatchMode() ) + { + if ( Cmd_CommandExecute(Abc_FrameGetGlobalFrame(), Command) ) + { + Abc_Print( 1, "Something did not work out with the command \"%s\".\n", Command ); + return NULL; + } + } + else + { + Abc_FrameSetBatchMode( 1 ); + if ( Cmd_CommandExecute(Abc_FrameGetGlobalFrame(), Command) ) + { + Abc_Print( 1, "Something did not work out with the command \"%s\".\n", Command ); + return NULL; + } + Abc_FrameSetBatchMode( 0 ); + } + pTemp = Abc_FrameReadGia(Abc_FrameGetGlobalFrame()); + { + int nLevelTemp = Gia_ManLevelNum(pTemp); + int nAndsTemp = Gia_ManAndNum(pTemp); + if ( vPareto ) + Gia_ManDeepSynParetoUpdate( vPareto, pTemp, nLevelTemp, nAndsTemp ); + if ( nLevelsMin > nLevelTemp || (nLevelsMin == nLevelTemp && nAndsMin > nAndsTemp) ) + { + Gia_ManStop( pNew ); + pNew = Gia_ManDup( pTemp ); + nLevelsMin = nLevelTemp; + nAndsMin = nAndsTemp; + fOuterChange = 1; + if ( vGias ) + Vec_PtrPush( vGias, Gia_ManDup(pTemp) ); + } + } + if ( fOuterChange && fVerbose ) + { + printf( "Iter %6d : ", i ); + printf( "Time %8.2f sec : ", (float)1.0*(Abc_Clock() - clkStart)/CLOCKS_PER_SEC ); + printf( "Lev = %3d ", nLevelsMin ); + printf( "And = %6d ", nAndsMin ); + printf( "<== best : " ); + printf( "%s", Command ); + printf( "\n" ); + } + if ( nTimeToStop && Abc_Clock() > nTimeToStop ) + { + if ( !Abc_FrameIsBatchMode() ) + printf( "Runtime limit (%d sec) is reached after %d iterations.\n", TimeOut, i ); + return pNew; + } + i++; + } + } + } + if ( i == IterMax ) + printf( "Iteration limit (%d iters) is reached after %.2f seconds.\n", IterMax, (float)1.0*(Abc_Clock() - clkStart)/CLOCKS_PER_SEC ); + return pNew; +} + /**Function************************************************************* Synopsis [] @@ -251,7 +474,84 @@ Gia_Man_t * Gia_ManRandSyn( Gia_Man_t * p, unsigned random_seed ) ***********************************************************************/ Gia_Man_t * Gia_ManDeepSyn2( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fChoices, int fVerbose ) { - return Gia_ManDeepSyn( pGia, nIters, nNoImpr, TimeOut, nAnds, Seed, fUseTwo, fChoices, fVerbose ); + Vec_Ptr_t * vGias = fChoices ? Vec_PtrAlloc(100) : NULL; + Vec_Ptr_t * vPareto = fUseTwo ? Vec_PtrStart(100) : NULL; + char * pParetoBase = NULL; + Gia_Man_t * pInit; + Gia_Man_t * pBest; + Gia_Man_t * pThis; + int i, nBestLev, nBestAnd; + if ( !Abc_NtkRecIsRunning3() ) + { + Abc_Print( -1, "Gia_ManDeepSyn2(): LMS library is not loaded.\n" ); + Abc_Print( -1, "Download \"rec6Lib_final_filtered3_recanon.aig\" and run \"rec_start3 _/rec6Lib_final_filtered3_recanon.aig\".\n" ); + if ( vGias ) + Vec_PtrFree( vGias ); + if ( vPareto ) + Vec_PtrFree( vPareto ); + return Gia_ManDup( pGia ); + } + if ( vPareto ) + { + if ( pGia->pSpec && pGia->pSpec[0] ) + pParetoBase = Extra_FileNameGeneric( pGia->pSpec ); + else if ( pGia->pName && pGia->pName[0] ) + pParetoBase = Extra_FileNameGeneric( pGia->pName ); + else + pParetoBase = Extra_UtilStrsav( "gia" ); + } + pInit = Gia_ManDup(pGia); + pBest = Gia_ManDup(pGia); + nBestLev = Gia_ManLevelNum(pBest); + nBestAnd = Gia_ManAndNum(pBest); + if ( vPareto ) + Gia_ManDeepSynParetoUpdate( vPareto, pGia, nBestLev, nBestAnd ); + if ( vGias ) + Vec_PtrPush( vGias, Gia_ManDup(pGia) ); + for ( i = 0; i < nIters; i++ ) + { + if ( fVerbose ) + printf( "ITER %d (out of %d) running for %d seconds\n", i + 1, nIters, TimeOut ); + int nThisLev, nThisAnd; + Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), Gia_ManDup(pInit) ); + pThis = Gia_ManDeepSynOne2( nNoImpr, TimeOut, nAnds, Seed+i, fUseTwo, fVerbose, vGias, vPareto ); + nThisLev = Gia_ManLevelNum(pThis); + nThisAnd = Gia_ManAndNum(pThis); + if ( nBestLev > nThisLev || (nBestLev == nThisLev && nBestAnd > nThisAnd) ) + { + Gia_ManStop( pBest ); + pBest = pThis; + nBestLev = nThisLev; + nBestAnd = nThisAnd; + } + else + Gia_ManStop( pThis ); + if ( vPareto ) + Gia_ManDeepSynParetoPrint( vPareto ); + } + 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 ); + } + if ( vPareto ) + { + Gia_ManDeepSynParetoSave( vPareto, pParetoBase ); + Gia_Man_t * pTemp; + Vec_PtrForEachEntry( Gia_Man_t *, vPareto, pTemp, i ) + if ( pTemp ) + Gia_ManStop( pTemp ); + Vec_PtrFree( vPareto ); + } + return pBest; } //////////////////////////////////////////////////////////////////////// @@ -260,4 +560,3 @@ Gia_Man_t * Gia_ManDeepSyn2( Gia_Man_t * pGia, int nIters, int nNoImpr, int Time ABC_NAMESPACE_IMPL_END -