luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Adding new synthesis scripts.

This commit is contained in:
Alan Mishchenko 2013-10-23 10:44:11 -07:00
parent 103fa663c7
commit 8ad1729aa9
5 changed files with 236 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
src/aig/gia/gia.h
View File

@ -937,6 +937,9 @@ 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_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 ===========================================================*/
extern unsigned * Gia_ManConvertAigToTruth( Gia_Man_t * p, Gia_Obj_t * pRoot, Vec_Int_t * vLeaves, Vec_Int_t * vTruth, Vec_Int_t * vVisited );
extern Gia_Man_t * Gia_ManPerformBidec( Gia_Man_t * p, int fVerbose );
@ -1062,6 +1065,8 @@ extern Gia_Man_t * Gia_ManFramesInitSpecial( Gia_Man_t * pAig, int nFram
/*=== giaFront.c ==========================================================*/
extern Gia_Man_t * Gia_ManFront( Gia_Man_t * p );
extern void Gia_ManFrontTest( Gia_Man_t * p );
/*=== giaFx.c ==========================================================*/
extern Gia_Man_t * Gia_ManPerformFx( Gia_Man_t * p, int nNewNodesMax, int LitCountMax, int fReverse, int fVerbose, int fVeryVerbose );
/*=== giaHash.c ===========================================================*/
extern void Gia_ManHashAlloc( Gia_Man_t * p );
extern void Gia_ManHashStart( Gia_Man_t * p );

70
src/aig/gia/giaBalance.c
View File

@ -965,7 +965,7 @@ Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax,
pNew1 = Dam_ManAreaBalanceInt( pNew, vCiLevels, nNewNodesMax, fVerbose, fVeryVerbose );
if ( fVerbose ) Gia_ManPrintStats( pNew1, NULL );
Gia_ManStop( pNew );
Vec_IntFree( vCiLevels );
Vec_IntFreeP( &vCiLevels );
// derive the final result
pNew2 = Gia_ManDupNoMuxes( pNew1 );
if ( fVerbose ) Gia_ManPrintStats( pNew2, NULL );
@ -984,7 +984,7 @@ Gia_Man_t * Gia_ManAreaBalance( Gia_Man_t * p, int fSimpleAnd, int nNewNodesMax,
SeeAlso []
***********************************************************************/
Gia_Man_t * Dam_ManAigSyn( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
Gia_Man_t * Gia_ManAigSyn2( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
{
Gia_Man_t * pNew, * pTemp;
Jf_Par_t Pars, * pPars = &Pars;
@ -1003,6 +1003,72 @@ Gia_Man_t * Dam_ManAigSyn( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
Gia_ManStop( pTemp );
return pNew;
}
Gia_Man_t * Gia_ManAigSyn3( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
{
Gia_Man_t * pNew, * pTemp;
Jf_Par_t Pars, * pPars = &Pars;
Jf_ManSetDefaultPars( pPars );
if ( fVerbose ) Gia_ManPrintStats( p, NULL );
// perform balancing
pNew = Gia_ManAreaBalance( p, 0, ABC_INFINITY, fVeryVerbose, 0 );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
// perform mapping
pPars->nLutSize = 6;
pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
// Gia_ManStop( pTemp );
// perform balancing
pNew = Gia_ManAreaBalance( pTemp = pNew, 0, ABC_INFINITY, fVeryVerbose, 0 );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
Gia_ManStop( pTemp );
// perform mapping
pPars->nLutSize = 4;
pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
// Gia_ManStop( pTemp );
// perform balancing
pNew = Gia_ManAreaBalance( pTemp = pNew, 0, ABC_INFINITY, fVeryVerbose, 0 );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
Gia_ManStop( pTemp );
return pNew;
}
Gia_Man_t * Gia_ManAigSyn4( Gia_Man_t * p, int fVerbose, int fVeryVerbose )
{
Gia_Man_t * pNew, * pTemp;
Jf_Par_t Pars, * pPars = &Pars;
Jf_ManSetDefaultPars( pPars );
if ( fVerbose ) Gia_ManPrintStats( p, NULL );
// perform balancing
pNew = Gia_ManAreaBalance( p, 0, ABC_INFINITY, fVeryVerbose, 0 );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
// perform mapping
pPars->nLutSize = 7;
pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
// Gia_ManStop( pTemp );
// perform extraction
pNew = Gia_ManPerformFx( pTemp = pNew, ABC_INFINITY, 0, 0, fVeryVerbose, 0 );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
Gia_ManStop( pTemp );
// perform balancing
pNew = Gia_ManAreaBalance( pTemp = pNew, 0, ABC_INFINITY, fVeryVerbose, 0 );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
Gia_ManStop( pTemp );
// perform mapping
pPars->nLutSize = 5;
pNew = Jf_ManPerformMapping( pTemp = pNew, pPars );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
// Gia_ManStop( pTemp );
// perform extraction
pNew = Gia_ManPerformFx( pTemp = pNew, ABC_INFINITY, 0, 0, fVeryVerbose, 0 );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
Gia_ManStop( pTemp );
// perform balancing
pNew = Gia_ManAreaBalance( pTemp = pNew, 0, ABC_INFINITY, fVeryVerbose, 0 );
if ( fVerbose ) Gia_ManPrintStats( pNew, NULL );
Gia_ManStop( pTemp );
return pNew;
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///

1
src/aig/gia/giaUtil.c
View File

@ -535,6 +535,7 @@ int Gia_ManSetLevels( Gia_Man_t * p, Vec_Int_t * vCiLevels )
int i;
if ( vCiLevels == NULL )
return Gia_ManLevelNum( p );
assert( Vec_IntSize(vCiLevels) == Gia_ManCiNum(p) );
Gia_ManCleanLevels( p, Gia_ManObjNum(p) );
p->nLevels = 0;
Gia_ManForEachCi( p, pObj, i )

164
src/base/abci/abc.c
View File

@ -352,6 +352,9 @@ static int Abc_CommandAbc9Bidec ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandAbc9Shrink ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Fx ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Balance ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Syn2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Syn3 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Syn4 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Miter ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Miter2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAbc9Append ( Abc_Frame_t * pAbc, int argc, char ** argv );
@ -912,6 +915,9 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "ABC9", "&shrink", Abc_CommandAbc9Shrink, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&fx", Abc_CommandAbc9Fx, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&b", Abc_CommandAbc9Balance, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&syn2", Abc_CommandAbc9Syn2, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&syn3", Abc_CommandAbc9Syn3, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&syn4", Abc_CommandAbc9Syn4, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&miter", Abc_CommandAbc9Miter, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&miter2", Abc_CommandAbc9Miter2, 0 );
Cmd_CommandAdd( pAbc, "ABC9", "&append", Abc_CommandAbc9Append, 0 );
@ -992,8 +998,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
// Dau_DsdTest();
}
// if ( Sdm_ManCanRead() )
// Sdm_ManRead();
if ( Sdm_ManCanRead() )
Sdm_ManRead();
}
/**Function*************************************************************
@ -27442,7 +27448,6 @@ usage:
***********************************************************************/
int Abc_CommandAbc9Fx( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Gia_ManPerformFx( Gia_Man_t * p, int nNewNodesMax, int LitCountMax, int fReverse, int fVerbose, int fVeryVerbose );
Gia_Man_t * pTemp;
int nNewNodesMax = 1000000;
int LitCountMax = 0;
@ -27604,6 +27609,159 @@ usage:
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Syn2( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
int c, fVerbose = 0;
int fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vwh" ) ) != EOF )
{
switch ( c )
{
case 'v':
fVerbose ^= 1;
break;
case 'w':
fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Syn2(): There is no AIG.\n" );
return 1;
}
pTemp = Gia_ManAigSyn2( pAbc->pGia, 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");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Syn3( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
int c, fVerbose = 0;
int fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vwh" ) ) != EOF )
{
switch ( c )
{
case 'v':
fVerbose ^= 1;
break;
case 'w':
fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Syn3(): There is no AIG.\n" );
return 1;
}
pTemp = Gia_ManAigSyn3( pAbc->pGia, fVerbose, fVeryVerbose );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &syn3 [-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");
return 1;
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Abc_CommandAbc9Syn4( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Gia_Man_t * pTemp;
int c, fVerbose = 0;
int fVeryVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "vwh" ) ) != EOF )
{
switch ( c )
{
case 'v':
fVerbose ^= 1;
break;
case 'w':
fVeryVerbose ^= 1;
break;
case 'h':
goto usage;
default:
goto usage;
}
}
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Syn4(): There is no AIG.\n" );
return 1;
}
pTemp = Gia_ManAigSyn4( pAbc->pGia, fVerbose, fVeryVerbose );
Abc_FrameUpdateGia( pAbc, pTemp );
return 0;
usage:
Abc_Print( -2, "usage: &syn4 [-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");
return 1;
}
/**Function*************************************************************
Synopsis []

3
src/sat/bmc/bmcBmcAnd.c
View File

@ -769,7 +769,6 @@ Abc_Cex_t * Gia_ManBmcCexGen( Bmc_Mna_t * pMan, Gia_Man_t * p, int iOut )
***********************************************************************/
int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
{
extern Gia_Man_t * Dam_ManAigSyn( Gia_Man_t * p, int fVerbose, int fVeryVerbose );
Bmc_Mna_t * p;
int nFramesMax, f, i=0, Lit, status, RetValue = -2;
abctime clk = Abc_Clock();
@ -784,7 +783,7 @@ int Gia_ManBmcPerform( Gia_Man_t * pGia, Bmc_AndPar_t * pPars )
if ( pPars->fUseSynth )
{
Gia_Man_t * pTemp = p->pFrames;
p->pFrames = Dam_ManAigSyn( pTemp, pPars->fVerbose, 0 );
p->pFrames = Gia_ManAigSyn2( pTemp, pPars->fVerbose, 0 );
Gia_ManStop( pTemp );
}
else if ( pPars->fVerbose )