Adding more features to the synthesis script &syn2.

This commit is contained in:
Alan Mishchenko 2014-06-14 19:03:05 -07:00
parent 0ac22c9e1d
commit cf993a9d90
5 changed files with 56 additions and 17 deletions

View File

@ -969,7 +969,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 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_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 ===========================================================*/

View File

@ -1017,14 +1017,22 @@ void Gia_ManAigTransferPiLevels( Gia_Man_t * pNew, Gia_Man_t * p )
SeeAlso []
***********************************************************************/
Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fOldAlgo, int fCoarsen, int fCutMin, int nRelaxRatio, int fVerbose, int fVeryVerbose )
{
Gia_Man_t * pNew, * pTemp;
Jf_Par_t Pars, * pPars = &Pars;
Lf_ManSetDefaultPars( pPars );
// pPars->fVerbose = 1;
pPars->fCoarsen = 1;
pPars->nRelaxRatio = 20;
if ( fOldAlgo )
{
Jf_ManSetDefaultPars( pPars );
pPars->fCutMin = fCutMin;
}
else
{
Lf_ManSetDefaultPars( pPars );
pPars->fCoarsen = fCoarsen;
pPars->fCutMin = fCutMin;
pPars->nRelaxRatio = nRelaxRatio;
}
if ( fVerbose ) Gia_ManPrintStats( p, NULL );
if ( Gia_ManAndNum(p) == 0 )
return Gia_ManDup(p);
@ -1033,7 +1041,10 @@ Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
Gia_ManAigTransferPiLevels( pNew, p );
// perform mapping
pNew = Lf_ManPerformMapping( pTemp = pNew, pPars );
if ( fOldAlgo )
pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
else
pNew = Lf_ManPerformMapping( pTemp = pNew, pPars );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
// Gia_ManStop( pTemp );
// perform balancing

View File

@ -27707,12 +27707,36 @@ int Abc_CommandAbc9Syn2( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
int c, fVerbose = 0;
int fOldAlgo = 0;
int fCoarsen = 1;
int fCutMin = 0;
int nRelaxRatio = 20;
int fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Rakmvwh" ) ) != EOF )
{
switch ( c )
{
case 'R':
if ( globalUtilOptind >= argc )
{
Abc_Print( 1, "Command line switch \"-R\" should be followed by a floating point number.\n" );
return 0;
}
nRelaxRatio = atoi(argv[globalUtilOptind]);
globalUtilOptind++;
if ( nRelaxRatio < 0 )
goto usage;
break;
case 'a':
fOldAlgo ^= 1;
break;
case 'k':
fCoarsen ^= 1;
break;
case 'm':
fCutMin ^= 1;
break;
case 'v':
fVerbose ^= 1;
break;
@ -27730,16 +27754,20 @@ 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, fVerbose, fVeryVerbose );
pTemp = Gia_ManAigSyn2( pAbc->pGia, fOldAlgo, fCoarsen, fCutMin, nRelaxRatio, fVerbose, fVeryVerbose );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &syn2 [-lvh]\n" );
Abc_Print( -2, "\t performs AIG optimization\n" );
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-h : print the command usage\n");
Abc_Print( -2, "usage: &syn2 [-R num] [-akmlvh]\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-h : print the command usage\n");
return 1;
}

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, pPars->fVerbose, 0 );
p->pFrames = Gia_ManAigSyn2( pTemp, 1, 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, pPars->fVerbose, 0 ); Gia_ManStop( pTemp );
p->pFrames = Gia_ManAigSyn2( pTemp = p->pFrames, 1, 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, 0, 0 );
pGia = Gia_ManAigSyn2( pTemp = pGia, 1, 0, 0, 0, 0, 0 );
Gia_ManStop( pTemp );
pAig = Gia_ManToAig( pGia, 0 );
Gia_ManStop( pGia );