Update high-effort synthesis.

This commit is contained in:
Alan Mishchenko 2026-06-16 07:52:19 -07:00
parent 2d835aabf0
commit 61e74a1033
1 changed files with 301 additions and 2 deletions

View File

@ -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