Adding delay optimization to synthesis script &syn2.

This commit is contained in:
Alan Mishchenko 2014-08-08 12:45:28 -07:00
parent 35b816dd57
commit 68ce0bc1c1
8 changed files with 123 additions and 22 deletions

View File

@ -88,6 +88,10 @@ LINK32=link.exe
# PROP Default_Filter "cpp;c;cxx;rc;def;r;odl;idl;hpj;bat"
# Begin Source File
SOURCE=.\src\aig\gia\giaBalance.c
# End Source File
# Begin Source File
SOURCE=.\src\base\main\main.c
# End Source File
# End Group

View File

@ -1021,7 +1021,7 @@ extern void Gia_AigerWriteSimple( Gia_Man_t * pInit, char * pFile
/*=== giaBalance.c ===========================================================*/
extern Gia_Man_t * Gia_ManBalance( Gia_Man_t * p, int fSimpleAnd, int fVerbose );
extern Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax, int fVerbose, int fVeryVerbose );
extern Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fOldAlgo, int fCoarsen, int fCutMin, int nRelaxRatio, int fVerbose, int fVeryVerbose );
extern Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fOldAlgo, int fCoarsen, int fCutMin, int nRelaxRatio, int fDelayMin, int fVerbose, int fVeryVerbose );
extern Gia_Man_t * Gia_ManAigSyn3( Gia_Man_t * p, int fVerbose, int fVeryVerbose );
extern Gia_Man_t * Gia_ManAigSyn4( Gia_Man_t * p, int fVerbose, int fVeryVerbose );
/*=== giaBidec.c ===========================================================*/
@ -1186,6 +1186,7 @@ extern void Gia_ManMappingVerify( Gia_Man_t * p );
extern void Gia_ManTransferMapping( Gia_Man_t * pGia, Gia_Man_t * p );
extern Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pIfPars, int fNormalized );
extern Gia_Man_t * Gia_ManPerformSopBalance( Gia_Man_t * p, int nCutNum, int nRelaxRatio, int fVerbose );
extern Gia_Man_t * Gia_ManPerformDsdBalance( Gia_Man_t * p, int nCutNum, int nRelaxRatio, int fVerbose );
/*=== giaJf.c ===========================================================*/
extern void Jf_ManSetDefaultPars( Jf_Par_t * pPars );
extern Gia_Man_t * Jf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars );

View File

@ -1017,7 +1017,7 @@ void Gia_ManAigTransferPiLevels( Gia_Man_t * pNew, Gia_Man_t * p )
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fOldAlgo, int fCoarsen, int fCutMin, int nRelaxRatio, int fVerbose, int fVeryVerbose )
Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fOldAlgo, int fCoarsen, int fCutMin, int nRelaxRatio, int fDelayMin, int fVerbose, int fVeryVerbose )
{
Gia_Man_t * pNew, * pTemp;
Jf_Par_t Pars, * pPars = &Pars;
@ -1029,18 +1029,65 @@ Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fOldAlgo, int fCoarsen, int fCutM
else
{
Lf_ManSetDefaultPars( pPars );
pPars->fCoarsen = fCoarsen;
pPars->fCutMin = fCutMin;
pPars->fCoarsen = fCoarsen;
pPars->nRelaxRatio = nRelaxRatio;
pPars->nAreaTuner = 1;
pPars->nCutNum = 4;
}
if ( fVerbose ) Gia_ManPrintStats( p, NULL );
p = Gia_ManDup( pTemp = p );
Gia_ManAigTransferPiLevels( p, pTemp );
if ( Gia_ManAndNum(p) == 0 )
return Gia_ManDup(p);
return p;
// delay optimization
if ( fDelayMin )
{
int Area0, Area1, Delay0, Delay1;
int fCutMin = pPars->fCutMin;
int fCoarsen = pPars->fCoarsen;
int nRelaxRatio = pPars->nRelaxRatio;
pPars->fCutMin = 0;
pPars->fCoarsen = 0;
pPars->nRelaxRatio = 0;
// perform mapping
if ( fOldAlgo )
Jf_ManPerformMapping( p, pPars );
else
Lf_ManPerformMapping( p, pPars );
Area0 = (int)pPars->Area;
Delay0 = (int)pPars->Delay;
// perform balancing
pNew = Gia_ManPerformDsdBalance( p, 4, 0, 0 );
// perform mapping again
if ( fOldAlgo )
Jf_ManPerformMapping( pNew, pPars );
else
Lf_ManPerformMapping( pNew, pPars );
Area1 = (int)pPars->Area;
Delay1 = (int)pPars->Delay;
// choose the best result
if ( Delay1 < Delay0 - 1 || (Delay1 == Delay0 + 1 && 100.0 * (Area1 - Area0) / Area1 < 3.0) )
{
Gia_ManAigTransferPiLevels( pNew, p );
Gia_ManStop( p );
p = pNew;
}
else
{
Gia_ManStop( pNew );
Vec_IntFreeP( &p->vMapping );
}
// reset params
pPars->fCutMin = fCutMin;
pPars->fCoarsen = fCoarsen;
pPars->nRelaxRatio = nRelaxRatio;
}
// perform balancing
pNew = Gia_ManAreaBalance( p, 0, ABC_INFINITY, fVeryVerbose, 0 );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
Gia_ManAigTransferPiLevels( pNew, p );
Gia_ManStop( p );
// perform mapping
if ( fOldAlgo )
pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );

View File

@ -1758,6 +1758,38 @@ Gia_Man_t * Gia_ManPerformSopBalance( Gia_Man_t * p, int nCutNum, int nRelaxRati
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
}
Gia_Man_t * Gia_ManPerformDsdBalance( Gia_Man_t * p, int nCutNum, int nRelaxRatio, int fVerbose )
{
Gia_Man_t * pNew;
If_Man_t * pIfMan;
If_Par_t Pars, * pPars = &Pars;
If_ManSetDefaultPars( pPars );
pPars->nCutsMax = nCutNum;
pPars->nRelaxRatio = nRelaxRatio;
pPars->fVerbose = fVerbose;
pPars->nLutSize = 6;
pPars->fDsdBalance = 1;
pPars->fUseDsd = 1;
pPars->fCutMin = 1;
pPars->fTruth = 1;
pPars->fExpRed = 0;
if ( Abc_FrameReadManDsd() == NULL )
Abc_FrameSetManDsd( If_DsdManAlloc(pPars->nLutSize, 0) );
// perform mapping
pIfMan = Gia_ManToIf( p, pPars );
pIfMan->pIfDsdMan = (If_DsdMan_t *)Abc_FrameReadManDsd();
if ( pPars->fDsdBalance )
If_DsdManAllocIsops( pIfMan->pIfDsdMan, pPars->nLutSize );
If_ManPerformMapping( pIfMan );
pNew = Gia_ManFromIfAig( pIfMan );
If_ManStop( pIfMan );
// transfer name
assert( pNew->pName == NULL );
pNew->pName = Abc_UtilStrsav( p->pName );
pNew->pSpec = Abc_UtilStrsav( p->pSpec );
Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
return pNew;
}
/**Function*************************************************************

View File

@ -10603,16 +10603,16 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
// Nf_ManPrepareLibraryTest();
// return 0;
}
/*
if ( pNtk )
{
extern Abc_Ntk_t * Abc_NtkBarBufsOnOffTest( Abc_Ntk_t * pNtk );
Abc_Ntk_t * pNtkRes = Abc_NtkBarBufsOnOffTest( pNtk );
// extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fNewAlgo, int fVerbose );
// extern Abc_Ntk_t * Abc_NtkBarBufsOnOffTest( Abc_Ntk_t * pNtk );
// Abc_Ntk_t * pNtkRes = Abc_NtkBarBufsOnOffTest( pNtk );
extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fNewAlgo, int fVerbose );
// extern Abc_Ntk_t * Abc_NtkPcmTestAig( Abc_Ntk_t * pNtk, int fVerbose );
// Abc_Ntk_t * pNtkRes;
Abc_Ntk_t * pNtkRes;
// if ( Abc_NtkIsLogic(pNtk) )
// pNtkRes = Abc_NtkPcmTest( pNtk, fNewAlgo, fVerbose );
pNtkRes = Abc_NtkPcmTest( pNtk, fNewAlgo, fVerbose );
// else
// pNtkRes = Abc_NtkPcmTestAig( pNtk, fVerbose );
if ( pNtkRes == NULL )
@ -10622,6 +10622,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
}
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
}
*/
return 0;
usage:
Abc_Print( -2, "usage: test [-CKDNM] [-aovwh] <file_name>\n" );
@ -27936,9 +27937,10 @@ int Abc_CommandAbc9Syn2( Abc_Frame_t * pAbc, int argc, char ** argv )
int fCoarsen = 1;
int fCutMin = 0;
int nRelaxRatio = 20;
int fDelayMin = 1;
int fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Rakmvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Rakmdvwh" ) ) != EOF )
{
switch ( c )
{
@ -27962,6 +27964,9 @@ int Abc_CommandAbc9Syn2( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'm':
fCutMin ^= 1;
break;
case 'd':
fDelayMin ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -27979,19 +27984,29 @@ int Abc_CommandAbc9Syn2( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9Syn2(): There is no AIG.\n" );
return 1;
}
pTemp = Gia_ManAigSyn2( pAbc->pGia, fOldAlgo, fCoarsen, fCutMin, nRelaxRatio, fVerbose, fVeryVerbose );
if ( fDelayMin )
{
If_DsdMan_t * p = (If_DsdMan_t *)Abc_FrameReadManDsd();
if ( p && If_DsdManVarNum(p) < 6 )
{
printf( "DSD manager has incompatible number of variables. Delay minimization is not performed.\n" );
fDelayMin = 0;
}
}
pTemp = Gia_ManAigSyn2( pAbc->pGia, fOldAlgo, fCoarsen, fCutMin, nRelaxRatio, fDelayMin, fVerbose, fVeryVerbose );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &syn2 [-R num] [-akmlvh]\n" );
Abc_Print( -2, "usage: &syn2 [-R num] [-akmdvh]\n" );
Abc_Print( -2, "\t performs AIG optimization\n" );
Abc_Print( -2, "\t-R num : the delay relaxation ratio (num >= 0) [default = %d]\n", nRelaxRatio );
Abc_Print( -2, "\t-a : toggles using the old algorithm [default = %s]\n", fOldAlgo? "yes": "no" );
Abc_Print( -2, "\t-k : toggles coarsening the subject graph [default = %s]\n", fCoarsen? "yes": "no" );
Abc_Print( -2, "\t-m : toggles cut minimization [default = %s]\n", fCutMin? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggle printing additional information [default = %s]\n", fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-R num : the delay relaxation ratio (num >= 0) [default = %d]\n", nRelaxRatio );
Abc_Print( -2, "\t-a : toggles using the old algorithm [default = %s]\n", fOldAlgo? "yes": "no" );
Abc_Print( -2, "\t-k : toggles coarsening the subject graph [default = %s]\n", fCoarsen? "yes": "no" );
Abc_Print( -2, "\t-m : toggles cut minimization [default = %s]\n", fCutMin? "yes": "no" );
Abc_Print( -2, "\t-d : toggles additional delay optimization [default = %s]\n", fDelayMin? "yes": "no" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-w : toggles printing additional information [default = %s]\n", fVeryVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}

View File

@ -593,6 +593,8 @@ Dar_Lib_t * Dar_LibRead()
void Dar_LibStart()
{
// abctime clk = Abc_Clock();
if ( s_DarLib != NULL )
return;
assert( s_DarLib == NULL );
s_DarLib = Dar_LibRead();
// printf( "The 4-input library started with %d nodes and %d subgraphs. ", s_DarLib->nObjs - 4, s_DarLib->nSubgrTotal );

View File

@ -786,7 +786,7 @@ int Gia_ManBmcPerform_old_cnf( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
if ( pPars->fUseSynth )
{
Gia_Man_t * pTemp = p->pFrames;
p->pFrames = Gia_ManAigSyn2( pTemp, 1, 0, 0, 0, pPars->fVerbose, 0 );
p->pFrames = Gia_ManAigSyn2( pTemp, 1, 0, 0, 0, 0, pPars->fVerbose, 0 );
Gia_ManStop( pTemp );
}
else if ( pPars->fVerbose )
@ -970,7 +970,7 @@ int Gia_ManBmcPerformInt( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
}
if ( pPars->fUseSynth )
{
p->pFrames = Gia_ManAigSyn2( pTemp = p->pFrames, 1, 0, 0, 0, pPars->fVerbose, 0 ); Gia_ManStop( pTemp );
p->pFrames = Gia_ManAigSyn2( pTemp = p->pFrames, 1, 0, 0, 0, 0, pPars->fVerbose, 0 ); Gia_ManStop( pTemp );
}
else if ( pPars->fVerbose )
Gia_ManPrintStats( p->pFrames, NULL );

View File

@ -140,7 +140,7 @@ Aig_Man_t * Gia_ManMultiProveSyn( Aig_Man_t * p, int fVerbose, int fVeryVerbose
Aig_Man_t * pAig;
Gia_Man_t * pGia, * pTemp;
pGia = Gia_ManFromAig( p );
pGia = Gia_ManAigSyn2( pTemp = pGia, 1, 0, 0, 0, 0, 0 );
pGia = Gia_ManAigSyn2( pTemp = pGia, 1, 0, 0, 0, 0, 0, 0 );
Gia_ManStop( pTemp );
pAig = Gia_ManToAig( pGia, 0 );
Gia_ManStop( pGia );