From 85207c7568dd2edac04e97ecdf59c2d684d1cb91 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 18 Mar 2008 08:01:00 -0700 Subject: Version abc80318 --- src/aig/aig/aig.h | 1 + src/aig/aig/aigPart.c | 140 +++++++++++++++++++++++++++++++++++++++++++++++++ src/base/abci/abc.c | 38 ++++++++++++-- src/base/abci/abcDar.c | 25 +++++++++ 4 files changed, 201 insertions(+), 3 deletions(-) diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index bd77c0a4..33f7b2a0 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -526,6 +526,7 @@ extern Vec_Ptr_t * Aig_ManPartitionSmartRegisters( Aig_Man_t * pAig, int nSu extern Vec_Ptr_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize ); extern Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSize ); extern Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nConfMax, int nLevelMax, int fVerbose ); +extern Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfMax, int nLevelMax, int fVerbose ); /*=== aigPartReg.c =========================================================*/ extern Vec_Ptr_t * Aig_ManRegPartitionSimple( Aig_Man_t * pAig, int nPartSize, int nOverSize ); extern Vec_Ptr_t * Aig_ManRegPartitionSmart( Aig_Man_t * pAig, int nPartSize ); diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c index df5792b2..1fb93eb7 100644 --- a/src/aig/aig/aigPart.c +++ b/src/aig/aig/aigPart.c @@ -1020,6 +1020,75 @@ Vec_Ptr_t * Aig_ManDupPart( Aig_Man_t * pNew, Aig_Man_t * pOld, Vec_Int_t * vPar return vOutsTotal; } +/**Function************************************************************* + + Synopsis [Adds internal nodes in the topological order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Aig_ManDupPartAll_rec( Aig_Man_t * pNew, Aig_Man_t * pOld, Aig_Obj_t * pObj ) +{ + Aig_Obj_t * pObjNew; + assert( !Aig_IsComplement(pObj) ); + if ( Aig_ObjIsTravIdCurrent(pOld, pObj) ) + return; + Aig_ObjSetTravIdCurrent(pOld, pObj); + if ( Aig_ObjIsPi(pObj) ) + pObjNew = Aig_ObjCreatePi(pNew); + else if ( Aig_ObjIsPo(pObj) ) + { + Aig_ManDupPartAll_rec( pNew, pOld, Aig_ObjFanin0(pObj) ); + pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) ); + } + else + { + assert( Aig_ObjIsNode(pObj) ); + Aig_ManDupPartAll_rec( pNew, pOld, Aig_ObjFanin0(pObj) ); + Aig_ManDupPartAll_rec( pNew, pOld, Aig_ObjFanin1(pObj) ); + pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); + } + pObj->pData = pObjNew; + pObjNew->pData = pObj; +} + +/**Function************************************************************* + + Synopsis [Adds internal nodes in the topological order.] + + Description [Returns the array of new outputs.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManDupPartAll( Aig_Man_t * pOld, Vec_Int_t * vPart ) +{ + Aig_Man_t * pNew; + Aig_Obj_t * pObj, * pObjNew; + int i, Entry; + Aig_ManIncrementTravId( pOld ); + pNew = Aig_ManStart( 5000 ); + // map constant nodes + pObj = Aig_ManConst1(pOld); + pObjNew = Aig_ManConst1(pNew); + pObj->pData = pObjNew; + pObjNew->pData = pObj; + Aig_ObjSetTravIdCurrent(pOld, pObj); + // map all other nodes + Vec_IntForEachEntry( vPart, Entry, i ) + { + pObj = Aig_ManPo( pOld, Entry ); + Aig_ManDupPartAll_rec( pNew, pOld, pObj ); + } + return pNew; +} + /**Function************************************************************* Synopsis [Create partitioned miter of the two AIGs.] @@ -1205,6 +1274,77 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon return pAig; } +/**Function************************************************************* + + Synopsis [Performs partitioned choice computation.] + + Description [Assumes that each output in the second AIG cannot have + more supp vars than the same output in the first AIG.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Aig_ManFraigPartitioned( Aig_Man_t * pAig, int nPartSize, int nConfMax, int nLevelMax, int fVerbose ) +{ + extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax ); + + Aig_Man_t * pAigPart, * pAigTemp; + Vec_Int_t * vPart; + Vec_Ptr_t * vParts; + Aig_Obj_t * pObj; + void ** ppData; + int i, k; + + // partition the outputs of the AIG + vParts = Aig_ManPartitionNaive( pAig, nPartSize ); + + // start the equivalence classes + Aig_ManReprStart( pAig, Aig_ManObjNumMax(pAig) ); + + // set the PI numbers + Aig_ManForEachPi( pAig, pObj, k ) + pObj->pNext = (Aig_Obj_t *)(long)k; + + // create the total fraiged AIG + Vec_PtrForEachEntry( vParts, vPart, i ) + { + // derive the partition AIG + pAigPart = Aig_ManDupPartAll( pAig, vPart ); + // store contents of pData pointers + ppData = ALLOC( void *, Aig_ManObjNumMax(pAigPart) ); + Aig_ManForEachObj( pAigPart, pObj, k ) + ppData[k] = pObj->pData; + // report the process + if ( fVerbose ) + printf( "Part %4d (out of %4d) PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r", + i+1, Vec_PtrSize(vParts), Aig_ManPiNum(pAigPart), Aig_ManPoNum(pAigPart), + Aig_ManNodeNum(pAigPart), Aig_ManLevelNum(pAigPart) ); + // compute equivalence classes (to be stored in pNew->pReprs) + pAigTemp = Fra_FraigChoice( pAigPart, nConfMax, nLevelMax ); + Aig_ManStop( pAigTemp ); + // reset the pData pointers + Aig_ManForEachObj( pAigPart, pObj, k ) + pObj->pData = ppData[k]; + free( ppData ); + // transfer representatives to the total AIG + if ( pAigPart->pReprs ) + Aig_ManTransferRepr( pAig, pAigPart ); + Aig_ManStop( pAigPart ); + } + if ( fVerbose ) + printf( " \r" ); + Vec_VecFree( (Vec_Vec_t *)vParts ); + + // clear the PI numbers + Aig_ManForEachPi( pAig, pObj, k ) + pObj->pNext = NULL; + + // derive the result of choicing + return Aig_ManDupRepr( pAig, 0 ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 91133b2a..7178cc0a 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -8458,23 +8458,39 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk, * pNtkRes; int c, fProve, fVerbose, fDoSparse; int nConfLimit; + int nPartSize; + int nLevelMax; extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fTransfer, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkDarFraigPart( Abc_Ntk_t * pNtk, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults + nPartSize = 0; + nLevelMax = 0; nConfLimit = 100; fDoSparse = 0; fProve = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Cspvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "PCLspvh" ) ) != EOF ) { switch ( c ) { + case 'P': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" ); + goto usage; + } + nPartSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nPartSize < 0 ) + goto usage; + break; case 'C': if ( globalUtilOptind >= argc ) { @@ -8486,6 +8502,17 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nConfLimit < 0 ) goto usage; break; + case 'L': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" ); + goto usage; + } + nLevelMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLevelMax < 0 ) + goto usage; + break; case 's': fDoSparse ^= 1; break; @@ -8512,7 +8539,10 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fVerbose ); + if ( nPartSize > 0 ) + pNtkRes = Abc_NtkDarFraigPart( pNtk, nPartSize, nConfLimit, nLevelMax, fVerbose ); + else + pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fDoSparse, fProve, 0, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -8523,9 +8553,11 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: ifraig [-C num] [-spvh]\n" ); + fprintf( pErr, "usage: ifraig [-P num] [-C num] [-L num] [-spvh]\n" ); fprintf( pErr, "\t performs fraiging using a new method\n" ); + fprintf( pErr, "\t-P num : partition size (0 = partitioning is not used) [default = %d]\n", nPartSize ); fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); + fprintf( pErr, "\t-L num : limit on node level to fraig (0 = fraig all nodes) [default = %d]\n", nLevelMax ); fprintf( pErr, "\t-s : toggle considering sparse functions [default = %s]\n", fDoSparse? "yes": "no" ); fprintf( pErr, "\t-p : toggle proving the miter outputs [default = %s]\n", fProve? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 78f43aac..e1b3828e 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -593,6 +593,31 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in return pNtkAig; } +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarFraigPart( Abc_Ntk_t * pNtk, int nPartSize, int nConfLimit, int nLevelMax, int fVerbose ) +{ + Abc_Ntk_t * pNtkAig; + Aig_Man_t * pMan, * pTemp; + pMan = Abc_NtkToDar( pNtk, 0 ); + if ( pMan == NULL ) + return NULL; + pMan = Aig_ManFraigPartitioned( pTemp = pMan, nPartSize, nConfLimit, nLevelMax, fVerbose ); + Aig_ManStop( pTemp ); + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + Aig_ManStop( pMan ); + return pNtkAig; +} + /**Function************************************************************* Synopsis [Gives the current ABC network to AIG manager for processing.] -- cgit v1.2.3