diff options
Diffstat (limited to 'src/base/abci')
-rw-r--r-- | src/base/abci/abc.c | 56 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 209 | ||||
-rw-r--r-- | src/base/abci/abcFraig.c | 4 | ||||
-rw-r--r-- | src/base/abci/abcPart.c | 55 |
4 files changed, 258 insertions, 66 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 1e0fed0c..d5321e6d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -330,7 +330,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) // Kit_TruthCountMintermsPrecomp(); // Kit_DsdPrecompute4Vars(); - Dar_LibStart(); +// Dar_LibStart(); } /**Function************************************************************* @@ -346,7 +346,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) ***********************************************************************/ void Abc_End() { - Dar_LibStop(); +// Dar_LibStop(); Abc_NtkFraigStoreClean(); // Rwt_Man4ExplorePrint(); @@ -5931,7 +5931,7 @@ usage: int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; - Abc_Ntk_t * pNtk;//, * pNtkRes; + Abc_Ntk_t * pNtk, * pNtkRes; int c; int nLevels; // extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ); @@ -5940,6 +5940,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern int Pr_ManProofTest( char * pFileName ); extern void Abc_NtkCompareSupports( Abc_Ntk_t * pNtk ); extern void Abc_NtkCompareCones( Abc_Ntk_t * pNtk ); + extern Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -6049,8 +6050,21 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // Abc_Ntk4VarTable( pNtk ); // Dat_NtkGenerateArrays( pNtk ); - return 0; + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "Network should be strashed. Command has failed.\n" ); + return 1; + } + pNtkRes = Abc_NtkDar( pNtk ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Command has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; usage: fprintf( pErr, "usage: test [-h]\n" ); fprintf( pErr, "\t testbench for new procedures\n" ); @@ -7286,6 +7300,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) int fAllNodes; int fExdc; int c; + int fPartition = 0; pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -7307,7 +7322,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) pParams->fVerbose = 0; // the verbosiness flag pParams->fVerboseP = 0; // the verbosiness flag Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "RDCrscpvaeh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "RDCrscptvaeh" ) ) != EOF ) { switch ( c ) { @@ -7360,6 +7375,9 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'v': pParams->fVerbose ^= 1; break; + case 't': + fPartition ^= 1; + break; case 'a': fAllNodes ^= 1; break; @@ -7388,13 +7406,28 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) pParams->fVerboseP = pParams->fTryProve; // get the new network - if ( Abc_NtkIsStrash(pNtk) ) - pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc ); + if ( fPartition ) + { + pNtkRes = Abc_NtkDup( pNtk ); + if ( Abc_NtkIsStrash(pNtk) ) + Abc_NtkFraigPartitionedTime( pNtk, &Params ); + else + { + pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 ); + Abc_NtkFraigPartitionedTime( pNtk, &Params ); + Abc_NtkDelete( pNtk ); + } + } else { - pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 ); - pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc ); - Abc_NtkDelete( pNtk ); + if ( Abc_NtkIsStrash(pNtk) ) + pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc ); + else + { + pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 ); + pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc ); + Abc_NtkDelete( pNtk ); + } } if ( pNtkRes == NULL ) { @@ -7411,7 +7444,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: sprintf( Buffer, "%d", pParams->nBTLimit ); - fprintf( pErr, "usage: fraig [-R num] [-D num] [-C num] [-rscpvah]\n" ); + fprintf( pErr, "usage: fraig [-R num] [-D num] [-C num] [-rscpvtah]\n" ); fprintf( pErr, "\t transforms a logic network into a functionally reduced AIG\n" ); fprintf( pErr, "\t-R num : number of random patterns (127 < num < 32769) [default = %d]\n", pParams->nPatsRand ); fprintf( pErr, "\t-D num : number of systematic patterns (127 < num < 32769) [default = %d]\n", pParams->nPatsDyna ); @@ -7423,6 +7456,7 @@ usage: fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pParams->fVerbose? "yes": "no" ); fprintf( pErr, "\t-e : toggle functional sweeping using EXDC [default = %s]\n", fExdc? "yes": "no" ); fprintf( pErr, "\t-a : toggle between all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "dfs" ); + fprintf( pErr, "\t-t : toggle using partitioned representation [default = %s]\n", fPartition? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 0863061b..81278515 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -25,62 +25,12 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk ); -static Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [Gives the current ABC network to AIG manager for processing.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ) -{ - Abc_Ntk_t * pNtkAig; - Dar_Man_t * pMan;//, * pTemp; - assert( Abc_NtkIsStrash(pNtk) ); - // convert to the AIG manager - pMan = Abc_NtkToDar( pNtk ); - if ( pMan == NULL ) - return NULL; - if ( !Dar_ManCheck( pMan ) ) - { - printf( "Abc_NtkDar: AIG check has failed.\n" ); - Dar_ManStop( pMan ); - return NULL; - } - // perform balance - Dar_ManPrintStats( pMan ); -// Dar_ManDumpBlif( pMan, "aig_temp.blif" ); - pMan->pPars = Dar_ManDefaultParams(); - Dar_ManRewrite( pMan ); - Dar_ManPrintStats( pMan ); - // convert from the AIG manager - pNtkAig = Abc_NtkFromDar( pNtk, pMan ); - if ( pNtkAig == NULL ) - return NULL; - Dar_ManStop( pMan ); - // make sure everything is okay - if ( !Abc_NtkCheck( pNtkAig ) ) - { - printf( "Abc_NtkDar: The network check has failed.\n" ); - Abc_NtkDelete( pNtkAig ); - return NULL; - } - return pNtkAig; -} - -/**Function************************************************************* - Synopsis [Converts the network from the AIG manager into ABC.] Description [] @@ -96,7 +46,7 @@ Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk ) Abc_Obj_t * pObj; int i; // create the manager - pMan = Dar_ManStart( Abc_NtkNodeNum(pNtk) ); + pMan = Dar_ManStart( Abc_NtkNodeNum(pNtk) + 100 ); // transfer the pointers to the basic nodes Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Dar_ManConst1(pMan); Abc_NtkForEachCi( pNtk, pObj, i ) @@ -122,14 +72,14 @@ Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtk, Dar_Man_t * pMan ) +Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan ) { Vec_Ptr_t * vNodes; Abc_Ntk_t * pNtkNew; Dar_Obj_t * pObj; int i; // perform strashing - pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); + pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); // transfer the pointers to the basic nodes Dar_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew); Dar_ManForEachPi( pMan, pObj, i ) @@ -147,6 +97,159 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtk, Dar_Man_t * pMan ) return pNtkNew; } +/**Function************************************************************* + + Synopsis [Converts the network from the AIG manager into ABC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan ) +{ + Vec_Ptr_t * vNodes; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1; + Dar_Obj_t * pObj; + int i; +// assert( Dar_ManLatchNum(pMan) > 0 ); + // perform strashing + pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); + // transfer the pointers to the basic nodes + Dar_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew); + Dar_ManForEachPi( pMan, pObj, i ) + pObj->pData = Abc_NtkPi(pNtkNew, i); + // create latches of the new network + Dar_ManForEachObj( pMan, pObj, i ) + { + if ( !Dar_ObjIsLatch(pObj) ) + continue; + pObjNew = Abc_NtkCreateLatch( pNtkNew ); + pFaninNew0 = Abc_NtkCreateBi( pNtkNew ); + pFaninNew1 = Abc_NtkCreateBo( pNtkNew ); + Abc_ObjAddFanin( pObjNew, pFaninNew0 ); + Abc_ObjAddFanin( pFaninNew1, pObjNew ); + Abc_LatchSetInit0( pObjNew ); + pObj->pData = Abc_ObjFanout0( pObjNew ); + } + Abc_NtkAddDummyBoxNames( pNtkNew ); + // rebuild the AIG + vNodes = Dar_ManDfs( pMan ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + // add the first fanin + pObj->pData = pFaninNew0 = (Abc_Obj_t *)Dar_ObjChild0Copy(pObj); + if ( Dar_ObjIsBuf(pObj) ) + continue; + // add the second fanin + pFaninNew1 = (Abc_Obj_t *)Dar_ObjChild1Copy(pObj); + // create the new node + if ( Dar_ObjIsExor(pObj) ) + pObj->pData = pObjNew = Abc_AigXor( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 ); + else + pObj->pData = pObjNew = Abc_AigAnd( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 ); + } + Vec_PtrFree( vNodes ); + // connect the PO nodes + Dar_ManForEachPo( pMan, pObj, i ) + { + pFaninNew = (Abc_Obj_t *)Dar_ObjChild0Copy( pObj ); + Abc_ObjAddFanin( Abc_NtkPo(pNtkNew, i), pFaninNew ); + } + // connect the latches + Dar_ManForEachObj( pMan, pObj, i ) + { + if ( !Dar_ObjIsLatch(pObj) ) + continue; + pFaninNew = (Abc_Obj_t *)Dar_ObjChild0Copy( pObj ); + Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0(pObj->pData)), pFaninNew ); + } + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkFromIvySeq(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Collect latch values.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pLatch; + int i, * pArray; + pArray = ALLOC( int, Abc_NtkLatchNum(pNtk) ); + Abc_NtkForEachLatch( pNtk, pLatch, i ) + pArray[i] = Abc_LatchIsInit1(pLatch); + return pArray; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ) +{ + Abc_Ntk_t * pNtkAig; + Dar_Man_t * pMan;//, * pTemp; + int * pArray; + + assert( Abc_NtkIsStrash(pNtk) ); + // convert to the AIG manager + pMan = Abc_NtkToDar( pNtk ); + if ( pMan == NULL ) + return NULL; + if ( !Dar_ManCheck( pMan ) ) + { + printf( "Abc_NtkDar: AIG check has failed.\n" ); + Dar_ManStop( pMan ); + return NULL; + } + // perform balance + Dar_ManPrintStats( pMan ); + + pArray = Abc_NtkGetLatchValues(pNtk); + Dar_ManSeqStrash( pMan, Abc_NtkLatchNum(pNtk), pArray ); + free( pArray ); + +// Dar_ManDumpBlif( pMan, "aig_temp.blif" ); +// pMan->pPars = Dar_ManDefaultParams(); +// Dar_ManRewrite( pMan ); + Dar_ManPrintStats( pMan ); + // convert from the AIG manager + if ( Dar_ManLatchNum(pMan) ) + pNtkAig = Abc_NtkFromDarSeq( pNtk, pMan ); + else + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + if ( pNtkAig == NULL ) + return NULL; + Dar_ManStop( pMan ); + // make sure everything is okay + if ( !Abc_NtkCheck( pNtkAig ) ) + { + printf( "Abc_NtkDar: The network check has failed.\n" ); + Abc_NtkDelete( pNtkAig ); + return NULL; + } + return pNtkAig; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c index 30e49af2..fa6771b3 100644 --- a/src/base/abci/abcFraig.c +++ b/src/base/abci/abcFraig.c @@ -687,7 +687,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk ) // set the number of networks stored Abc_FrameSetNtkStoreSize( Abc_FrameReadNtkStoreSize() + 1 ); } -// printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld ); + printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld ); return 1; } @@ -734,7 +734,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore() Fraig_ParamsSetDefault( &Params ); Params.nPatsRand = nWordsMin * 32; // the number of words of random simulation info Params.nPatsDyna = nWordsMin * 32; // the number of words of dynamic simulation info - Params.nBTLimit = 99; // the max number of backtracks to perform + Params.nBTLimit = 999999; // the max number of backtracks to perform Params.fFuncRed = 1; // performs only one level hashing Params.fFeedBack = 1; // enables solver feedback Params.fDist1Pats = 1; // enables distance-1 patterns diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c index 748868de..787e3f88 100644 --- a/src/base/abci/abcPart.c +++ b/src/base/abci/abcPart.c @@ -698,12 +698,67 @@ Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams ) // derive the final network pNtkFraig = Abc_NtkPartStitchChoices( pNtk, vFraigs ); Vec_PtrForEachEntry( vFraigs, pNtkAig, i ) + { +// Abc_NtkPrintStats( stdout, pNtkAig, 0 ); Abc_NtkDelete( pNtkAig ); + } Vec_PtrFree( vFraigs ); return pNtkFraig; } +/**Function************************************************************* + + Synopsis [Stitches together several networks with choice nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFraigPartitionedTime( Abc_Ntk_t * pNtk, void * pParams ) +{ + extern int Cmd_CommandExecute( void * pAbc, char * sCommand ); + extern void * Abc_FrameGetGlobalFrame(); + + Vec_Vec_t * vParts; + Vec_Ptr_t * vFraigs, * vOne; + Abc_Ntk_t * pNtkAig, * pNtkFraig; + int i; + int clk = clock(); + + // perform partitioning + assert( Abc_NtkIsStrash(pNtk) ); +// vParts = Abc_NtkPartitionNaive( pNtk, 20 ); + vParts = Abc_NtkPartitionSmart( pNtk, 0, 0 ); + + Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" ); + + // fraig each partition + vFraigs = Vec_PtrAlloc( Vec_VecSize(vParts) ); + Vec_VecForEachLevel( vParts, vOne, i ) + { + pNtkAig = Abc_NtkCreateConeArray( pNtk, vOne, 0 ); + pNtkFraig = Abc_NtkFraig( pNtkAig, pParams, 0, 0 ); + Vec_PtrPush( vFraigs, pNtkFraig ); + Abc_NtkDelete( pNtkAig ); + + printf( "Finished part %d (out of %d)\r", i+1, Vec_VecSize(vParts) ); + } + Vec_VecFree( vParts ); + + Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" ); + + // derive the final network + Vec_PtrForEachEntry( vFraigs, pNtkAig, i ) + Abc_NtkDelete( pNtkAig ); + Vec_PtrFree( vFraigs ); + + PRT( "Partitioned fraiging time", clock() - clk ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// |