diff options
| -rw-r--r-- | src/aig/gia/gia.h | 3 | ||||
| -rw-r--r-- | src/aig/gia/giaDup.c | 13 | ||||
| -rw-r--r-- | src/aig/gia/giaIf.c | 58 | ||||
| -rw-r--r-- | src/aig/gia/giaTim.c | 104 | ||||
| -rw-r--r-- | src/base/abci/abc.c | 169 | ||||
| -rw-r--r-- | src/base/main/mainInt.h | 4 |
6 files changed, 342 insertions, 9 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index fa8a6026..0ac1c740 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1067,6 +1067,7 @@ extern Gia_Man_t * Gia_ManDupLastPis( Gia_Man_t * p, int nLastPis ); extern Gia_Man_t * Gia_ManDupFlip( Gia_Man_t * p, int * pInitState ); extern Gia_Man_t * Gia_ManDupCycled( Gia_Man_t * pAig, Abc_Cex_t * pCex, int nFrames ); extern Gia_Man_t * Gia_ManDup( Gia_Man_t * p ); +extern Gia_Man_t * Gia_ManDupWithAttributes( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupZero( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupPerm( Gia_Man_t * p, Vec_Int_t * vPiPerm ); extern Gia_Man_t * Gia_ManDupPermFlop( Gia_Man_t * p, Vec_Int_t * vFfPerm ); @@ -1180,6 +1181,7 @@ extern int Gia_ManLutFaninCount( Gia_Man_t * p ); extern int Gia_ManLutSizeMax( Gia_Man_t * p ); extern int Gia_ManLutNum( Gia_Man_t * p ); extern int Gia_ManLutLevel( Gia_Man_t * p ); +extern void Gia_ManLutParams( Gia_Man_t * p, int * pnCurLuts, int * pnCurEdges, int * pnCurLevels ); extern void Gia_ManSetRefsMapped( Gia_Man_t * p ); extern void Gia_ManSetIfParsDefault( void * pIfPars ); extern void Gia_ManMappingVerify( Gia_Man_t * p ); @@ -1313,6 +1315,7 @@ extern Gia_Man_t * Gia_ManDupNormalize( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupUnnormalize( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * vBoxPres ); extern int Gia_ManLevelWithBoxes( Gia_Man_t * p ); +extern int Gia_ManLutLevelWithBoxes( Gia_Man_t * p ); extern int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, void * pParsInit ); extern void * Gia_ManUpdateTimMan( Gia_Man_t * p, Vec_Int_t * vBoxPres ); extern Gia_Man_t * Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxPres ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index b54bdee0..37deb7fd 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -546,6 +546,19 @@ Gia_Man_t * Gia_ManDup( Gia_Man_t * p ) pNew->pCexSeq = Abc_CexDup( p->pCexSeq, Gia_ManRegNum(p) ); return pNew; } +Gia_Man_t * Gia_ManDupWithAttributes( Gia_Man_t * p ) +{ + Gia_Man_t * pNew = Gia_ManDup(p); + Gia_ManTransferMapping( pNew, p ); + Gia_ManTransferPacking( pNew, p ); + if ( p->pManTime ) + pNew->pManTime = Tim_ManDup( (Tim_Man_t *)p->pManTime, 0 ); + if ( p->pAigExtra ) + pNew->pAigExtra = Gia_ManDup( p->pAigExtra ); + if ( p->nAnd2Delay ) + pNew->nAnd2Delay = p->nAnd2Delay; + return pNew; +} /**Function************************************************************* diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index 6a2520eb..050966b1 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -183,6 +183,56 @@ int Gia_ManLutLevel( Gia_Man_t * p ) /**Function************************************************************* + Synopsis [Prints mapping statistics.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManLutParams( Gia_Man_t * p, int * pnCurLuts, int * pnCurEdges, int * pnCurLevels ) +{ + if ( p->pManTime && Tim_ManBoxNum((Tim_Man_t *)p->pManTime) ) + { + int i; + *pnCurLuts = 0; + *pnCurEdges = 0; + Gia_ManForEachLut( p, i ) + { + (*pnCurLuts)++; + (*pnCurEdges) += Gia_ObjLutSize(p, i); + } + *pnCurLevels = Gia_ManLutLevelWithBoxes( p ); + } + else + { + Gia_Obj_t * pObj; + int i, k, iFan; + int * pLevels = ABC_CALLOC( int, Gia_ManObjNum(p) ); + *pnCurLuts = 0; + *pnCurEdges = 0; + Gia_ManForEachLut( p, i ) + { + int Level = 0; + (*pnCurLuts)++; + (*pnCurEdges) += Gia_ObjLutSize(p, i); + Gia_LutForEachFanin( p, i, iFan, k ) + if ( Level < pLevels[iFan] ) + Level = pLevels[iFan]; + pLevels[i] = Level + 1; + } + *pnCurLevels = 0; + Gia_ManForEachCo( p, pObj, k ) + if ( *pnCurLevels < pLevels[Gia_ObjFaninId0p(p, pObj)] ) + *pnCurLevels = pLevels[Gia_ObjFaninId0p(p, pObj)]; + ABC_FREE( pLevels ); + } +} + +/**Function************************************************************* + Synopsis [Assigns levels.] Description [] @@ -395,7 +445,9 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p, char * pDumpFile ) Abc_Print( 1, "lev =%5d ", LevelMax ); Abc_Print( 1, "(%.2f) ", (float)Ave / Gia_ManCoNum(p) ); SetConsoleTextAttribute( hConsole, 7 ); // normal - Abc_Print( 1, "over =%5.1f %% ", 100.0 * Gia_ManComputeOverlap(p) / Gia_ManAndNum(p) ); +// Abc_Print( 1, "over =%5.1f %% ", 100.0 * Gia_ManComputeOverlap(p) / Gia_ManAndNum(p) ); + if ( p->pManTime && Tim_ManBoxNum((Tim_Man_t *)p->pManTime) ) + Abc_Print( 1, "levB =%5d ", Gia_ManLutLevelWithBoxes(p) ); Abc_Print( 1, "mem =%5.2f MB", 4.0*(Gia_ManObjNum(p) + 2*nLuts + nFanins)/(1<<20) ); Abc_Print( 1, "\n" ); } @@ -405,7 +457,9 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p, char * pDumpFile ) Abc_Print( 1, "%sedge =%8d%s ", "\033[1;32m", nFanins, "\033[0m" ); // green Abc_Print( 1, "%slev =%5d%s ", "\033[1;31m", LevelMax, "\033[0m" ); // red Abc_Print( 1, "%s(%.2f)%s ", "\033[1;31m", (float)Ave / Gia_ManCoNum(p), "\033[0m" ); - Abc_Print( 1, "over =%5.1f %% ", 100.0 * Gia_ManComputeOverlap(p) / Gia_ManAndNum(p) ); +// Abc_Print( 1, "over =%5.1f %% ", 100.0 * Gia_ManComputeOverlap(p) / Gia_ManAndNum(p) ); + if ( p->pManTime && Tim_ManBoxNum((Tim_Man_t *)p->pManTime) ) + Abc_Print( 1, "levB =%5d ", Gia_ManLutLevelWithBoxes(p) ); Abc_Print( 1, "mem =%5.2f MB", 4.0*(Gia_ManObjNum(p) + 2*nLuts + nFanins)/(1<<20) ); Abc_Print( 1, "\n" ); #endif diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c index 0e6a9252..290cae7d 100644 --- a/src/aig/gia/giaTim.c +++ b/src/aig/gia/giaTim.c @@ -486,6 +486,110 @@ int Gia_ManLevelWithBoxes( Gia_Man_t * p ) /**Function************************************************************* + Synopsis [Computes level with boxes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManLutLevelWithBoxes_rec( Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + int iObj, k, iFan, Level = 0; + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return 0; + Gia_ObjSetTravIdCurrent(p, pObj); + if ( Gia_ObjIsCi(pObj) ) + return 1; + assert( Gia_ObjIsAnd(pObj) ); + iObj = Gia_ObjId( p, pObj ); + Gia_LutForEachFanin( p, iObj, iFan, k ) + { + if ( Gia_ManLutLevelWithBoxes_rec( p, Gia_ManObj(p, iFan) ) ) + return 1; + Level = Abc_MaxInt( Level, Gia_ObjLevelId(p, iFan) ); + } + Gia_ObjSetLevelId( p, iObj, Level + 1 ); + return 0; +} +int Gia_ManLutLevelWithBoxes( Gia_Man_t * p ) +{ +// int nAnd2Delay = p->nAnd2Delay ? p->nAnd2Delay : 1; + Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime; + Gia_Obj_t * pObj, * pObjIn; + int i, k, j, curCi, curCo, LevelMax; + assert( Gia_ManRegNum(p) == 0 ); + // copy const and real PIs + Gia_ManCleanLevels( p, Gia_ManObjNum(p) ); + Gia_ObjSetLevel( p, Gia_ManConst0(p), 0 ); + Gia_ManIncrementTravId( p ); + Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) ); + for ( i = 0; i < Tim_ManPiNum(pManTime); i++ ) + { + pObj = Gia_ManPi( p, i ); +// Gia_ObjSetLevel( p, pObj, Tim_ManGetCiArrival(pManTime, i) / nAnd2Delay ); + Gia_ObjSetLevel( p, pObj, 0 ); + Gia_ObjSetTravIdCurrent( p, pObj ); + } + // create logic for each box + curCi = Tim_ManPiNum(pManTime); + curCo = 0; + for ( i = 0; i < Tim_ManBoxNum(pManTime); i++ ) + { + int nBoxInputs = Tim_ManBoxInputNum( pManTime, i ); + int nBoxOutputs = Tim_ManBoxOutputNum( pManTime, i ); + float * pDelayTable = Tim_ManBoxDelayTable( pManTime, i ); + // compute level for TFI of box inputs + for ( k = 0; k < nBoxInputs; k++ ) + { + pObj = Gia_ManPo( p, curCo + k ); + if ( Gia_ManLutLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) ) ) + { + printf( "Boxes are not in a topological order. Switching to level computation without boxes.\n" ); + return Gia_ManLevelNum( p ); + } + // set box input level + Gia_ObjSetCoLevel( p, pObj ); + } + // compute level for box outputs + for ( k = 0; k < nBoxOutputs; k++ ) + { + pObj = Gia_ManPi( p, curCi + k ); + Gia_ObjSetTravIdCurrent( p, pObj ); + // evaluate delay of this output + LevelMax = 0; + assert( nBoxInputs == (int)pDelayTable[1] ); + for ( j = 0; j < nBoxInputs && (pObjIn = Gia_ManPo(p, curCo + j)); j++ ) + if ( (int)pDelayTable[3+k*nBoxInputs+j] != -ABC_INFINITY ) +// LevelMax = Abc_MaxInt( LevelMax, Gia_ObjLevel(p, pObjIn) + ((int)pDelayTable[3+k*nBoxInputs+j] / nAnd2Delay) ); + LevelMax = Abc_MaxInt( LevelMax, Gia_ObjLevel(p, pObjIn) + 1 ); + // set box output level + Gia_ObjSetLevel( p, pObj, LevelMax ); + } + curCo += nBoxInputs; + curCi += nBoxOutputs; + } + // add remaining nodes + p->nLevels = 0; + for ( i = Tim_ManCoNum(pManTime) - Tim_ManPoNum(pManTime); i < Tim_ManCoNum(pManTime); i++ ) + { + pObj = Gia_ManPo( p, i ); + Gia_ManLutLevelWithBoxes_rec( p, Gia_ObjFanin0(pObj) ); + Gia_ObjSetCoLevel( p, pObj ); + p->nLevels = Abc_MaxInt( p->nLevels, Gia_ObjLevel(p, pObj) ); + } + curCo += Tim_ManPoNum(pManTime); + // verify counts + assert( curCi == Gia_ManPiNum(p) ); + assert( curCo == Gia_ManPoNum(p) ); +// printf( "Max level is %d.\n", p->nLevels ); + return p->nLevels; +} + +/**Function************************************************************* + Synopsis [Verify XAIG against its spec.] Description [] diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 51d1e878..019f7011 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -318,6 +318,8 @@ static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9Get ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Put ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Save ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Load ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Read ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9ReadBlif ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9ReadCBlif ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -903,6 +905,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&get", Abc_CommandAbc9Get, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&put", Abc_CommandAbc9Put, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&save", Abc_CommandAbc9Save, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&load", Abc_CommandAbc9Load, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&r", Abc_CommandAbc9Read, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&read_blif", Abc_CommandAbc9ReadBlif, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&read_cblif", Abc_CommandAbc9ReadCBlif, 0 ); @@ -1091,6 +1095,8 @@ void Abc_End( Abc_Frame_t * pAbc ) Gia_ManStop( Abc_FrameGetGlobalFrame()->pGia ); if ( Abc_FrameGetGlobalFrame()->pGia2 ) Gia_ManStop( Abc_FrameGetGlobalFrame()->pGia2 ); + if ( Abc_FrameGetGlobalFrame()->pGiaBest ) + Gia_ManStop( Abc_FrameGetGlobalFrame()->pGiaBest ); if ( Abc_NtkRecIsRunning3() ) Abc_NtkRecStop3(); } @@ -25420,6 +25426,129 @@ usage: /**Function************************************************************* + Synopsis [Compares to versions of the design and finds the best.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManCompareWithBest( Gia_Man_t * pBest, Gia_Man_t * p, int * pnBestLuts, int * pnBestEdges, int * pnBestLevels ) +{ + int nCurLuts, nCurEdges, nCurLevels; + Gia_ManLutParams( p, &nCurLuts, &nCurEdges, &nCurLevels ); + if ( pBest == NULL || + Gia_ManPiNum(pBest) != Gia_ManPiNum(p) || + Gia_ManPoNum(pBest) != Gia_ManPoNum(p) || + Gia_ManRegNum(pBest) != Gia_ManRegNum(p) || + strcmp(Gia_ManName(pBest), Gia_ManName(p)) || + (*pnBestLevels > nCurLevels) || + (*pnBestLevels == nCurLevels && *pnBestLuts > nCurLuts) || + (*pnBestLevels == nCurLevels && *pnBestLuts == nCurLuts && *pnBestEdges > nCurEdges) ) + { + *pnBestLuts = nCurLuts; + *pnBestEdges = nCurEdges; + *pnBestLevels = nCurLevels; + return 1; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Save( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + int c; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Empty network.\n" ); + return 1; + } + if ( !Gia_ManHasMapping(pAbc->pGia) ) + { + Abc_Print( -1, "GIA has not mapping.\n" ); + return 1; + } + if ( !Gia_ManCompareWithBest( pAbc->pGiaBest, pAbc->pGia, &pAbc->nBestLuts, &pAbc->nBestEdges, &pAbc->nBestLevels ) ) + return 0; + // save the design as best + Gia_ManStopP( &pAbc->pGiaBest ); + pAbc->pGiaBest = Gia_ManDupWithAttributes( pAbc->pGia ); + return 0; + +usage: + Abc_Print( -2, "usage: &save [-h]\n" ); + Abc_Print( -2, "\t compares and possibly saves AIG with mapping\n" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Load( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + int c; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + // restore from best + if ( pAbc->pGiaBest == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Load(): There is no best design saved.\n" ); + return 1; + } + Gia_ManStopP( &pAbc->pGia ); + pAbc->pGia = Gia_ManDupWithAttributes( pAbc->pGiaBest ); + return 0; + +usage: + Abc_Print( -2, "usage: &load [-h]\n" ); + Abc_Print( -2, "\t loads previously saved AIG with mapping" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -25507,10 +25636,10 @@ usage: int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gps_Par_t Pars, * pPars = &Pars; - int c; + int c, fBest = 0; memset( pPars, 0, sizeof(Gps_Par_t) ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Dtpcnlmash" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Dtpcnlmasbh" ) ) != EOF ) { switch ( c ) { @@ -25547,22 +25676,37 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->pDumpFile = argv[globalUtilOptind]; globalUtilOptind++; break; + case 'b': + fBest ^= 1; + break; case 'h': goto usage; default: goto usage; } } - if ( pAbc->pGia == NULL ) + if ( fBest ) { - Abc_Print( -1, "Abc_CommandAbc9Ps(): There is no AIG.\n" ); - return 1; + if ( pAbc->pGiaBest == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Ps(): There is no AIG.\n" ); + return 1; + } + Gia_ManPrintStats( pAbc->pGiaBest, pPars ); + } + else + { + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Ps(): There is no AIG.\n" ); + return 1; + } + Gia_ManPrintStats( pAbc->pGia, pPars ); } - Gia_ManPrintStats( pAbc->pGia, pPars ); return 0; usage: - Abc_Print( -2, "usage: &ps [-tpcnlmash] [-D file]\n" ); + Abc_Print( -2, "usage: &ps [-tpcnlmasbh] [-D file]\n" ); Abc_Print( -2, "\t prints stats of the current AIG\n" ); Abc_Print( -2, "\t-t : toggle printing BMC tents [default = %s]\n", pPars->fTents? "yes": "no" ); Abc_Print( -2, "\t-p : toggle printing switching activity [default = %s]\n", pPars->fSwitch? "yes": "no" ); @@ -25572,6 +25716,7 @@ usage: Abc_Print( -2, "\t-m : toggle printing MUX/XOR statistics [default = %s]\n", pPars->fMuxXor? "yes": "no" ); Abc_Print( -2, "\t-a : toggle printing miter statistics [default = %s]\n", pPars->fMiter? "yes": "no" ); Abc_Print( -2, "\t-s : skip mapping statistics even if mapped [default = %s]\n", pPars->fSkipMap? "yes": "no" ); + Abc_Print( -2, "\t-b : toggle printing saved AIG statistics [default = %s]\n", fBest? "yes": "no" ); Abc_Print( -2, "\t-D file : file name to dump statistics [default = none]\n" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -30646,6 +30791,11 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Empty GIA network.\n" ); return 1; } + if ( Gia_ManHasMapping(pAbc->pGia) ) + { + Abc_Print( -1, "Current AIG has mapping. Run \"&st\".\n" ); + return 1; + } if ( pPars->nLutSize == -1 ) { @@ -31650,6 +31800,11 @@ int Abc_CommandAbc9Lf( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Empty GIA network.\n" ); return 1; } + if ( Gia_ManHasMapping(pAbc->pGia) ) + { + Abc_Print( -1, "Current AIG has mapping. Run \"&st\".\n" ); + return 1; + } if ( pPars->nLutSizeMux && pPars->fUseMux7 ) { Abc_Print( -1, "Flags \"-M\" and \"-u\" are incompatible.\n" ); diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h index 73844c2b..c8276eeb 100644 --- a/src/base/main/mainInt.h +++ b/src/base/main/mainInt.h @@ -103,6 +103,10 @@ struct Abc_Frame_t_ // new code Gia_Man_t * pGia; // alternative current network as a light-weight AIG Gia_Man_t * pGia2; // copy of the above + Gia_Man_t * pGiaBest; // copy of the above + int nBestLuts; // best LUT count + int nBestEdges; // best edge count + int nBestLevels; // best level count Abc_Cex_t * pCex; // a counter-example to fail the current network Abc_Cex_t * pCex2; // copy of the above Vec_Ptr_t * vCexVec; // a vector of counter-examples if more than one PO fails |