diff options
Diffstat (limited to 'src')
58 files changed, 2301 insertions, 3849 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 33345577..f44a8022 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -344,8 +344,8 @@ static inline bool Abc_ObjIsPo( Abc_Obj_t * pObj ) { return pO static inline bool Abc_ObjIsBi( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_BI; } static inline bool Abc_ObjIsBo( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_BO; } static inline bool Abc_ObjIsAssert( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_ASSERT; } -static inline bool Abc_ObjIsCi( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_BI; } -static inline bool Abc_ObjIsCo( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_BO || pObj->Type == ABC_OBJ_ASSERT; } +static inline bool Abc_ObjIsCi( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_PI || pObj->Type == ABC_OBJ_BO; } +static inline bool Abc_ObjIsCo( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_PO || pObj->Type == ABC_OBJ_BI || pObj->Type == ABC_OBJ_ASSERT; } static inline bool Abc_ObjIsTerm( Abc_Obj_t * pObj ) { return Abc_ObjIsCi(pObj) || Abc_ObjIsCo(pObj); } static inline bool Abc_ObjIsNet( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_NET; } static inline bool Abc_ObjIsNode( Abc_Obj_t * pObj ) { return pObj->Type == ABC_OBJ_NODE; } @@ -547,6 +547,7 @@ extern void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFani extern Abc_Obj_t * Abc_ObjInsertBetween( Abc_Obj_t * pNodeIn, Abc_Obj_t * pNodeOut, Abc_ObjType_t Type ); extern void Abc_ObjTransferFanout( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew ); extern void Abc_ObjReplace( Abc_Obj_t * pObjOld, Abc_Obj_t * pObjNew ); +extern int Abc_ObjFanoutFaninNum( Abc_Obj_t * pFanout, Abc_Obj_t * pFanin ); /*=== abcFraig.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc ); extern void * Abc_NtkToFraig( Abc_Ntk_t * pNtk, void * pParams, int fAllNodes, int fExdc ); @@ -573,6 +574,7 @@ extern bool Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch ); extern int Abc_NtkCountSelfFeedLatches( Abc_Ntk_t * pNtk ); extern int Abc_NtkRemoveSelfFeedLatches( Abc_Ntk_t * pNtk ); extern Vec_Int_t * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk ); +extern void Abc_NtkInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues ); /*=== abcLib.c ==========================================================*/ extern Abc_Lib_t * Abc_LibCreate( char * pName ); extern void Abc_LibFree( Abc_Lib_t * pLib ); @@ -599,6 +601,7 @@ extern void Abc_ObjRecycle( Abc_Obj_t * pObj ); extern Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ); extern void Abc_NtkDeleteObj( Abc_Obj_t * pObj ); extern void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj, int fOnlyNodes ); +extern void Abc_NtkDeleteAll_rec( Abc_Obj_t * pObj ); extern Abc_Obj_t * Abc_NtkDupObj( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pObj, int fCopyName ); extern Abc_Obj_t * Abc_NtkDupBox( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pBox, int fCopyName ); extern Abc_Obj_t * Abc_NtkCloneObj( Abc_Obj_t * pNode ); @@ -808,6 +811,7 @@ extern Abc_Obj_t * Abc_NodeRecognizeMux( Abc_Obj_t * pNode, Abc_Obj_t ** extern int Abc_NtkPrepareTwoNtks( FILE * pErr, Abc_Ntk_t * pNtk, char ** argv, int argc, Abc_Ntk_t ** ppNtk1, Abc_Ntk_t ** ppNtk2, int * pfDelete1, int * pfDelete2 ); extern void Abc_NodeCollectFanins( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); extern void Abc_NodeCollectFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); +extern Vec_Ptr_t * Abc_NtkCollectLatches( Abc_Ntk_t * pNtk ); extern int Abc_NodeCompareLevelsIncrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 ); extern int Abc_NodeCompareLevelsDecrease( Abc_Obj_t ** pp1, Abc_Obj_t ** pp2 ); extern Vec_Int_t * Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk ); diff --git a/src/base/abc/abcCheck.c b/src/base/abc/abcCheck.c index d0c1deef..eb5a8400 100644 --- a/src/base/abc/abcCheck.c +++ b/src/base/abc/abcCheck.c @@ -20,7 +20,7 @@ #include "abc.h" #include "main.h" -#include "seq.h" +//#include "seq.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c index d9985737..a8edfbeb 100644 --- a/src/base/abc/abcDfs.c +++ b/src/base/abc/abcDfs.c @@ -638,6 +638,10 @@ int Abc_NtkGetLevelNum_rec( Abc_Obj_t * pNode ) Abc_Obj_t * pFanin; int i, Level; assert( !Abc_ObjIsNet(pNode) ); + if ( pNode->Id == 27278 ) + { + int x = 0; + } // skip the PI if ( Abc_ObjIsCi(pNode) ) return 0; diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c index 0581b35d..a988062f 100644 --- a/src/base/abc/abcFanio.c +++ b/src/base/abc/abcFanio.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "abc.h" -#include "seqInt.h" +//#include "seqInt.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -128,7 +128,7 @@ void Abc_ObjRemoveFanins( Abc_Obj_t * pObj ) void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFaninNew ) { Abc_Obj_t * pFaninNewR = Abc_ObjRegular(pFaninNew); - int iFanin, nLats;//, fCompl; + int iFanin;//, nLats;//, fCompl; assert( !Abc_ObjIsComplement(pObj) ); assert( !Abc_ObjIsComplement(pFaninOld) ); assert( pFaninOld != pFaninNewR ); @@ -153,8 +153,8 @@ void Abc_ObjPatchFanin( Abc_Obj_t * pObj, Abc_Obj_t * pFaninOld, Abc_Obj_t * pFa if ( Abc_ObjIsComplement(pFaninNew) ) Abc_ObjXorFaninC( pObj, iFanin ); - if ( Abc_NtkIsSeq(pObj->pNtk) && (nLats = Seq_ObjFaninL(pObj, iFanin)) ) - Seq_ObjSetFaninL( pObj, iFanin, nLats ); +// if ( Abc_NtkIsSeq(pObj->pNtk) && (nLats = Seq_ObjFaninL(pObj, iFanin)) ) +// Seq_ObjSetFaninL( pObj, iFanin, nLats ); // update the fanout of the fanin if ( !Vec_IntRemove( &pFaninOld->vFanouts, pObj->Id ) ) { @@ -223,8 +223,7 @@ void Abc_ObjTransferFanout( Abc_Obj_t * pNodeFrom, Abc_Obj_t * pNodeTo ) int nFanoutsOld, i; assert( !Abc_ObjIsComplement(pNodeFrom) ); assert( !Abc_ObjIsComplement(pNodeTo) ); - assert( Abc_ObjIsNode(pNodeFrom) || Abc_ObjIsCi(pNodeFrom) ); - assert( !Abc_ObjIsPo(pNodeTo) ); + assert( !Abc_ObjIsPo(pNodeFrom) && !Abc_ObjIsPo(pNodeTo) ); assert( pNodeFrom->pNtk == pNodeTo->pNtk ); assert( pNodeFrom != pNodeTo ); assert( Abc_ObjFanoutNum(pNodeFrom) > 0 ); @@ -264,6 +263,27 @@ void Abc_ObjReplace( Abc_Obj_t * pNodeOld, Abc_Obj_t * pNodeNew ) Abc_NtkDeleteObj( pNodeOld ); } +/**Function************************************************************* + + Synopsis [Returns the index of the fanin in the fanin list of the fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_ObjFanoutFaninNum( Abc_Obj_t * pFanout, Abc_Obj_t * pFanin ) +{ + Abc_Obj_t * pObj; + int i; + Abc_ObjForEachFanin( pFanout, pObj, i ) + if ( pObj == pFanin ) + return i; + return -1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abc/abcLatch.c b/src/base/abc/abcLatch.c index 7bc5e264..e475fd2a 100644 --- a/src/base/abc/abcLatch.c +++ b/src/base/abc/abcLatch.c @@ -46,9 +46,9 @@ bool Abc_NtkLatchIsSelfFeed_rec( Abc_Obj_t * pLatch, Abc_Obj_t * pLatchRoot ) if ( pLatch == pLatchRoot ) return 1; pFanin = Abc_ObjFanin0(Abc_ObjFanin0(pLatch)); - if ( !Abc_ObjIsBi(pFanin) || !Abc_ObjIsLatch(Abc_ObjFanin0(pFanin)) ) + if ( !Abc_ObjIsBo(pFanin) || !Abc_ObjIsLatch(Abc_ObjFanin0(pFanin)) ) return 0; - return Abc_NtkLatchIsSelfFeed_rec( Abc_ObjFanin0(pFanin), pLatchRoot ); + return Abc_NtkLatchIsSelfFeed_rec( Abc_ObjFanin0(pFanin), pLatch ); } /**Function************************************************************* @@ -67,7 +67,7 @@ bool Abc_NtkLatchIsSelfFeed( Abc_Obj_t * pLatch ) Abc_Obj_t * pFanin; assert( Abc_ObjIsLatch(pLatch) ); pFanin = Abc_ObjFanin0(Abc_ObjFanin0(pLatch)); - if ( !Abc_ObjIsBi(pFanin) || !Abc_ObjIsLatch(Abc_ObjFanin0(pFanin)) ) + if ( !Abc_ObjIsBo(pFanin) || !Abc_ObjIsLatch(Abc_ObjFanin0(pFanin)) ) return 0; return Abc_NtkLatchIsSelfFeed_rec( Abc_ObjFanin0(pFanin), pLatch ); } @@ -183,13 +183,32 @@ void Abc_NtkLatchPipe( Abc_Ntk_t * pNtk, int nLatches ) ***********************************************************************/ Vec_Int_t * Abc_NtkCollectLatchValues( Abc_Ntk_t * pNtk ) { - Vec_Int_t * vArray; + Vec_Int_t * vValues; + Abc_Obj_t * pLatch; + int i; + vValues = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) ); + Abc_NtkForEachLatch( pNtk, pLatch, i ) + Vec_IntPush( vValues, Abc_LatchIsInit1(pLatch) ); + return vValues; +} + +/**Function************************************************************* + + Synopsis [Strashes one logic node using its SOP.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues ) +{ Abc_Obj_t * pLatch; int i; - vArray = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) ); Abc_NtkForEachLatch( pNtk, pLatch, i ) - Vec_IntPush( vArray, Abc_LatchIsInit1(pLatch) ); - return vArray; + pLatch->pData = (void *)(vValues? (Vec_IntEntry(vValues,i)? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC); } diff --git a/src/base/abc/abcLib.c b/src/base/abc/abcLib.c index be0d34b7..218df6ef 100644 --- a/src/base/abc/abcLib.c +++ b/src/base/abc/abcLib.c @@ -148,11 +148,11 @@ int Abc_LibDeriveBlackBoxes( Abc_Ntk_t * pNtk, Abc_Lib_t * pLib ) { // go through the fanin nets Abc_ObjForEachFanin( pObj, pFanin, k ) - Abc_ObjInsertBetween( pFanin, pObj, ABC_OBJ_BO ); + Abc_ObjInsertBetween( pFanin, pObj, ABC_OBJ_BI ); // go through the fanout nets Abc_ObjForEachFanout( pObj, pFanout, k ) { - Abc_ObjInsertBetween( pObj, pFanout, ABC_OBJ_BI ); + Abc_ObjInsertBetween( pObj, pFanout, ABC_OBJ_BO ); // if the name is not given assign name if ( pFanout->pData == NULL ) { diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c index 30fab9a3..5ea9b369 100644 --- a/src/base/abc/abcNetlist.c +++ b/src/base/abc/abcNetlist.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "abc.h" -#include "seq.h" +//#include "seq.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index 96f489bd..a3ce5145 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -22,7 +22,7 @@ #include "abcInt.h" #include "main.h" #include "mio.h" -#include "seqInt.h" +//#include "seqInt.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -343,7 +343,7 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ) Abc_NtkDupObj(pNtkNew, pObj, 0); // reconnect all objects (no need to transfer attributes on edges) Abc_NtkForEachObj( pNtk, pObj, i ) - if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBi(pObj) ) + if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBo(pObj) ) Abc_ObjForEachFanin( pObj, pFanin, k ) Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy ); } @@ -357,6 +357,92 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ) /**Function************************************************************* + Synopsis [Duplicate the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDouble( Abc_Ntk_t * pNtk ) +{ + char Buffer[500]; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj, * pFanin; + int i, k; + assert( Abc_NtkIsLogic(pNtk) ); + + // start the network + pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc, 1 ); + sprintf( Buffer, "%s%s", pNtk->pName, "_doubled" ); + pNtkNew->pName = Extra_UtilStrsav(Buffer); + + // clean the node copy fields + Abc_NtkCleanCopy( pNtk ); + // clone CIs/CIs/boxes + Abc_NtkForEachPi( pNtk, pObj, i ) + Abc_NtkDupObj( pNtkNew, pObj, 0 ); + Abc_NtkForEachPo( pNtk, pObj, i ) + Abc_NtkDupObj( pNtkNew, pObj, 0 ); + Abc_NtkForEachAssert( pNtk, pObj, i ) + Abc_NtkDupObj( pNtkNew, pObj, 0 ); + Abc_NtkForEachBox( pNtk, pObj, i ) + Abc_NtkDupBox( pNtkNew, pObj, 0 ); + // copy the internal nodes + // duplicate the nets and nodes (CIs/COs/latches already dupped) + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( pObj->pCopy == NULL ) + Abc_NtkDupObj(pNtkNew, pObj, 0); + // reconnect all objects (no need to transfer attributes on edges) + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBo(pObj) ) + Abc_ObjForEachFanin( pObj, pFanin, k ) + Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy ); + + // clean the node copy fields + Abc_NtkCleanCopy( pNtk ); + // clone CIs/CIs/boxes + Abc_NtkForEachPi( pNtk, pObj, i ) + Abc_NtkDupObj( pNtkNew, pObj, 0 ); + Abc_NtkForEachPo( pNtk, pObj, i ) + Abc_NtkDupObj( pNtkNew, pObj, 0 ); + Abc_NtkForEachAssert( pNtk, pObj, i ) + Abc_NtkDupObj( pNtkNew, pObj, 0 ); + Abc_NtkForEachBox( pNtk, pObj, i ) + Abc_NtkDupBox( pNtkNew, pObj, 0 ); + // copy the internal nodes + // duplicate the nets and nodes (CIs/COs/latches already dupped) + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( pObj->pCopy == NULL ) + Abc_NtkDupObj(pNtkNew, pObj, 0); + // reconnect all objects (no need to transfer attributes on edges) + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBo(pObj) ) + Abc_ObjForEachFanin( pObj, pFanin, k ) + Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy ); + + // assign names + Abc_NtkForEachCi( pNtk, pObj, i ) + { + Abc_ObjAssignName( Abc_NtkCi(pNtkNew, i), "1_", Abc_ObjName(pObj) ); + Abc_ObjAssignName( Abc_NtkCi(pNtkNew, Abc_NtkCiNum(pNtk) + i), "2_", Abc_ObjName(pObj) ); + } + Abc_NtkForEachCo( pNtk, pObj, i ) + { + Abc_ObjAssignName( Abc_NtkCo(pNtkNew, i), "1_", Abc_ObjName(pObj) ); + Abc_ObjAssignName( Abc_NtkCo(pNtkNew, Abc_NtkCoNum(pNtk) + i), "2_", Abc_ObjName(pObj) ); + } + + // perform the final check + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkDup(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + Synopsis [Attaches the second network at the bottom of the first.] Description [Returns the first network. Deletes the second network.] diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c index ca86565a..dc3ff73c 100644 --- a/src/base/abc/abcObj.c +++ b/src/base/abc/abcObj.c @@ -129,10 +129,10 @@ Abc_Obj_t * Abc_NtkCreateObj( Abc_Ntk_t * pNtk, Abc_ObjType_t Type ) Vec_PtrPush( pNtk->vCos, pObj ); break; case ABC_OBJ_BI: - if ( pNtk->vCis ) Vec_PtrPush( pNtk->vCis, pObj ); + if ( pNtk->vCos ) Vec_PtrPush( pNtk->vCos, pObj ); break; case ABC_OBJ_BO: - if ( pNtk->vCos ) Vec_PtrPush( pNtk->vCos, pObj ); + if ( pNtk->vCis ) Vec_PtrPush( pNtk->vCis, pObj ); break; case ABC_OBJ_ASSERT: Vec_PtrPush( pNtk->vAsserts, pObj ); @@ -171,11 +171,11 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj ) Abc_Ntk_t * pNtk = pObj->pNtk; Vec_Ptr_t * vNodes; int i; + assert( !Abc_ObjIsComplement(pObj) ); // remove from the table of names if ( Nm_ManFindNameById(pObj->pNtk->pManName, pObj->Id) ) Nm_ManDeleteIdName(pObj->pNtk->pManName, pObj->Id); // delete fanins and fanouts - assert( !Abc_ObjIsComplement(pObj) ); vNodes = Vec_PtrAlloc( 100 ); Abc_NodeCollectFanouts( pObj, vNodes ); for ( i = 0; i < vNodes->nSize; i++ ) @@ -210,10 +210,10 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj ) Vec_PtrRemove( pNtk->vCos, pObj ); break; case ABC_OBJ_BI: - if ( pNtk->vCis ) Vec_PtrRemove( pNtk->vCis, pObj ); + if ( pNtk->vCos ) Vec_PtrRemove( pNtk->vCos, pObj ); break; case ABC_OBJ_BO: - if ( pNtk->vCos ) Vec_PtrRemove( pNtk->vCos, pObj ); + if ( pNtk->vCis ) Vec_PtrRemove( pNtk->vCis, pObj ); break; case ABC_OBJ_ASSERT: Vec_PtrRemove( pNtk->vAsserts, pObj ); @@ -253,7 +253,6 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj ) ***********************************************************************/ void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj, int fOnlyNodes ) { - Abc_Ntk_t * pNtk = pObj->pNtk; Vec_Ptr_t * vNodes; int i; assert( !Abc_ObjIsComplement(pObj) ); @@ -280,6 +279,33 @@ void Abc_NtkDeleteObj_rec( Abc_Obj_t * pObj, int fOnlyNodes ) /**Function************************************************************* + Synopsis [Deletes the node and MFFC of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkDeleteAll_rec( Abc_Obj_t * pObj ) +{ + Vec_Ptr_t * vNodes; + int i; + assert( !Abc_ObjIsComplement(pObj) ); + assert( Abc_ObjFanoutNum(pObj) == 0 ); + // delete fanins and fanouts + vNodes = Vec_PtrAlloc( 100 ); + Abc_NodeCollectFanins( pObj, vNodes ); + Abc_NtkDeleteObj( pObj ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + if ( Abc_ObjFanoutNum(pObj) == 0 ) + Abc_NtkDeleteAll_rec( pObj ); + Vec_PtrFree( vNodes ); +} + +/**Function************************************************************* + Synopsis [Duplicate the Obj.] Description [] @@ -401,7 +427,7 @@ Abc_Obj_t * Abc_NtkFindNode( Abc_Ntk_t * pNtk, char * pName ) Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_PO ); if ( Num >= 0 ) return Abc_ObjFanin0( Abc_NtkObj( pNtk, Num ) ); - Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_BO ); + Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_BI ); if ( Num >= 0 ) return Abc_ObjFanin0( Abc_NtkObj( pNtk, Num ) ); Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_NODE ); @@ -474,7 +500,7 @@ Abc_Obj_t * Abc_NtkFindCi( Abc_Ntk_t * pNtk, char * pName ) Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_PI ); if ( Num >= 0 ) return Abc_NtkObj( pNtk, Num ); - Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_BI ); + Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_BO ); if ( Num >= 0 ) return Abc_NtkObj( pNtk, Num ); return NULL; @@ -498,7 +524,7 @@ Abc_Obj_t * Abc_NtkFindCo( Abc_Ntk_t * pNtk, char * pName ) Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_PO ); if ( Num >= 0 ) return Abc_NtkObj( pNtk, Num ); - Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_BO ); + Num = Nm_ManFindIdByName( pNtk->pManName, pName, ABC_OBJ_BI ); if ( Num >= 0 ) return Abc_NtkObj( pNtk, Num ); return NULL; diff --git a/src/base/abc/abcShow.c b/src/base/abc/abcShow.c index 8ed653a9..fa921391 100644 --- a/src/base/abc/abcShow.c +++ b/src/base/abc/abcShow.c @@ -259,7 +259,8 @@ void Abc_NtkShow( Abc_Ntk_t * pNtk, int fGateNames ) char FileNameDot[200]; int i; - assert( !Abc_NtkHasAig(pNtk) ); + assert( !Abc_NtkIsStrash(pNtk) ); + Abc_NtkLogicToSop( pNtk, 0 ); // create the file name Abc_ShowGetFileName( pNtk->pName, FileNameDot ); // check that the file can be opened @@ -273,7 +274,8 @@ void Abc_NtkShow( Abc_Ntk_t * pNtk, int fGateNames ) // collect all nodes in the network vNodes = Vec_PtrAlloc( 100 ); Abc_NtkForEachObj( pNtk, pNode, i ) - Vec_PtrPush( vNodes, pNode ); +// if ( !Abc_ObjIsBi(pNode) && !Abc_ObjIsBo(pNode) ) + Vec_PtrPush( vNodes, pNode ); // write the DOT file Io_WriteDotNtk( pNtk, vNodes, NULL, FileNameDot, fGateNames ); Vec_PtrFree( vNodes ); diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index d5a4b5cb..fa1cd69a 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -22,7 +22,7 @@ #include "main.h" #include "mio.h" #include "dec.h" -#include "seq.h" +//#include "seq.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -1038,6 +1038,28 @@ void Abc_NodeCollectFanouts( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) /**Function************************************************************* + Synopsis [Collects all latches in the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Abc_NtkCollectLatches( Abc_Ntk_t * pNtk ) +{ + Vec_Ptr_t * vLatches; + Abc_Obj_t * pObj; + int i; + vLatches = Vec_PtrAlloc( 10 ); + Abc_NtkForEachObj( pNtk, pObj, i ) + Vec_PtrPush( vLatches, pObj ); + return vLatches; +} + +/**Function************************************************************* + Synopsis [Procedure used for sorting the nodes in increasing order of levels.] Description [] diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 5d6af56d..dffe4b99 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -25,7 +25,7 @@ #include "fpga.h" #include "pga.h" #include "cut.h" -#include "seq.h" +//#include "seq.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -92,6 +92,8 @@ static int Abc_CommandEspresso ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandGen ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandXyz ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandXsim ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandCycle ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDouble ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIStrash ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -138,6 +140,7 @@ static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDebug ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTraceStart ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTraceCheck ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -201,7 +204,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "resub", Abc_CommandResubstitute, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "rr", Abc_CommandRr, 1 ); -// Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 ); + Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 ); Cmd_CommandAdd( pAbc, "Various", "miter", Abc_CommandMiter, 1 ); Cmd_CommandAdd( pAbc, "Various", "demiter", Abc_CommandDemiter, 1 ); Cmd_CommandAdd( pAbc, "Various", "orpos", Abc_CommandOrPos, 1 ); @@ -225,6 +228,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "gen", Abc_CommandGen, 0 ); Cmd_CommandAdd( pAbc, "Various", "xyz", Abc_CommandXyz, 1 ); Cmd_CommandAdd( pAbc, "Various", "xsim", Abc_CommandXsim, 0 ); + Cmd_CommandAdd( pAbc, "Various", "cycle", Abc_CommandCycle, 1 ); + Cmd_CommandAdd( pAbc, "Various", "double", Abc_CommandDouble, 1 ); Cmd_CommandAdd( pAbc, "Various", "test", Abc_CommandTest, 0 ); Cmd_CommandAdd( pAbc, "New AIG", "istrash", Abc_CommandIStrash, 1 ); @@ -257,7 +262,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "FPGA mapping", "pga", Abc_CommandPga, 1 ); // Cmd_CommandAdd( pAbc, "Sequential", "scut", Abc_CommandScut, 0 ); -// Cmd_CommandAdd( pAbc, "Sequential", "init", Abc_CommandInit, 1 ); + Cmd_CommandAdd( pAbc, "Sequential", "init", Abc_CommandInit, 1 ); // Cmd_CommandAdd( pAbc, "Sequential", "pipe", Abc_CommandPipe, 1 ); // Cmd_CommandAdd( pAbc, "Sequential", "seq", Abc_CommandSeq, 1 ); // Cmd_CommandAdd( pAbc, "Sequential", "unseq", Abc_CommandUnseq, 1 ); @@ -271,6 +276,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "sat", Abc_CommandSat, 0 ); Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 ); + Cmd_CommandAdd( pAbc, "Verification", "debug", Abc_CommandDebug, 0 ); // Cmd_CommandAdd( pAbc, "Verification", "trace_start", Abc_CommandTraceStart, 0 ); // Cmd_CommandAdd( pAbc, "Verification", "trace_check", Abc_CommandTraceCheck, 0 ); @@ -3089,14 +3095,14 @@ int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( !Abc_NtkIsNetlist( pNtk ) ) + if ( !Abc_NtkIsStrash( pNtk ) ) { - fprintf( pErr, "This command is only applicable to netlists.\n" ); + fprintf( pErr, "This command is only applicable to strashed networks.\n" ); return 1; } // get the new network - pNtkRes = Abc_NtkNetlistToLogic( pNtk ); + pNtkRes = Abc_NtkAigToLogicSop( pNtk ); if ( pNtkRes == NULL ) { fprintf( pErr, "Converting to a logic network has failed.\n" ); @@ -3108,7 +3114,7 @@ int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( pErr, "usage: logic [-h]\n" ); - fprintf( pErr, "\t transforms a netlist into a logic network\n" ); + fprintf( pErr, "\t transforms an AIG into a logic network with SOPs\n" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -5115,6 +5121,169 @@ usage: SeeAlso [] ***********************************************************************/ +int Abc_CommandCycle( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int nFrames; + int fVerbose; + extern void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fVerbose ); + extern void Abc_NtkCycleInitStateSop( Abc_Ntk_t * pNtk, int nFrames, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nFrames = 50; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nFrames = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFrames < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( !Abc_NtkIsStrash(pNtk) && !Abc_NtkIsSopLogic(pNtk) ) + { + fprintf( pErr, "Only works for strashed networks or logic SOP networks.\n" ); + return 1; + } + + if ( Abc_NtkIsStrash(pNtk) ) + Abc_NtkCycleInitState( pNtk, nFrames, fVerbose ); + else + Abc_NtkCycleInitStateSop( pNtk, nFrames, fVerbose ); + return 0; + +usage: + fprintf( pErr, "usage: cycle [-F num] [-vh]\n" ); + fprintf( pErr, "\t cycles sequiential circuit for the given number of timeframes\n" ); + fprintf( pErr, "\t to derive a new initial state (which may be on the envelope)\n" ); + fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames ); + fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandDouble( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int c; + int nFrames; + int fVerbose; + extern Abc_Ntk_t * Abc_NtkDouble( Abc_Ntk_t * pNtk ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nFrames = 50; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'F': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nFrames = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nFrames < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + + if ( !Abc_NtkIsSopLogic(pNtk) ) + { + fprintf( pErr, "Only works for logic SOP networks.\n" ); + return 1; + } + + pNtkRes = Abc_NtkDouble( pNtk ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Command has failed.\n" ); + return 0; + } + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: double [-vh]\n" ); + fprintf( pErr, "\t puts together two parallel copies of the current network\n" ); +// fprintf( pErr, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames ); + fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; @@ -5692,10 +5861,10 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; - int c, fProve, fVerbose; + int c, fProve, fVerbose, fDoSparse; int nConfLimit; - extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fProve, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -5703,10 +5872,11 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults nConfLimit = 100; + fDoSparse = 0; fProve = 0; fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Cpvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Cspvh" ) ) != EOF ) { switch ( c ) { @@ -5721,6 +5891,9 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nConfLimit < 0 ) goto usage; break; + case 's': + fDoSparse ^= 1; + break; case 'p': fProve ^= 1; break; @@ -5744,7 +5917,7 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fProve, fVerbose ); + pNtkRes = Abc_NtkIvyFraig( pNtk, nConfLimit, fDoSparse, fProve, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -5755,10 +5928,11 @@ int Abc_CommandIFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: ifraig [-C num] [-pvh]\n" ); + fprintf( pErr, "usage: ifraig [-C num] [-spvh]\n" ); fprintf( pErr, "\t performs fraiging using a new method\n" ); fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); - fprintf( pErr, "\t-p : toggle proving miter outputs [default = %s]\n", fProve? "yes": "no" ); + 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" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -6133,17 +6307,17 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) memset( pParams, 0, sizeof(Fraig_Params_t) ); pParams->nPatsRand = 2048; // the number of words of random simulation info pParams->nPatsDyna = 2048; // the number of words of dynamic simulation info - pParams->nBTLimit = 99; // the max number of backtracks to perform - pParams->fFuncRed = 1; // performs only one level hashing - pParams->fFeedBack = 1; // enables solver feedback - pParams->fDist1Pats = 1; // enables distance-1 patterns - pParams->fDoSparse = 0; // performs equiv tests for sparse functions - pParams->fChoicing = 0; // enables recording structural choices - pParams->fTryProve = 0; // tries to solve the final miter - pParams->fVerbose = 0; // the verbosiness flag - pParams->fVerboseP = 0; // the verbosiness flag + pParams->nBTLimit = 100; // the max number of backtracks to perform + pParams->fFuncRed = 1; // performs only one level hashing + pParams->fFeedBack = 1; // enables solver feedback + pParams->fDist1Pats = 1; // enables distance-1 patterns + pParams->fDoSparse = 0; // performs equiv tests for sparse functions + pParams->fChoicing = 0; // enables recording structural choices + pParams->fTryProve = 0; // tries to solve the final miter + pParams->fVerbose = 0; // the verbosiness flag + pParams->fVerboseP = 0; // the verbosiness flag Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "RDBrscpvaeh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "RDCrscpvaeh" ) ) != EOF ) { switch ( c ) { @@ -6169,10 +6343,10 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pParams->nPatsDyna < 0 ) goto usage; break; - case 'B': + case 'C': if ( globalUtilOptind >= argc ) { - fprintf( pErr, "Command line switch \"-B\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); goto usage; } pParams->nBTLimit = atoi(argv[globalUtilOptind]); @@ -6247,15 +6421,15 @@ 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] [-B num] [-rscpvah]\n" ); + fprintf( pErr, "usage: fraig [-R num] [-D num] [-C num] [-rscpvah]\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 ); - fprintf( pErr, "\t-B num : number of backtracks for one SAT problem [default = %s]\n", pParams->nBTLimit==-1? "infinity" : Buffer ); + fprintf( pErr, "\t-C num : number of backtracks for one SAT problem [default = %s]\n", pParams->nBTLimit==-1? "infinity" : Buffer ); fprintf( pErr, "\t-r : toggle functional reduction [default = %s]\n", pParams->fFuncRed? "yes": "no" ); fprintf( pErr, "\t-s : toggle considering sparse functions [default = %s]\n", pParams->fDoSparse? "yes": "no" ); fprintf( pErr, "\t-c : toggle accumulation of choices [default = %s]\n", pParams->fChoicing? "yes": "no" ); - fprintf( pErr, "\t-p : toggle proving the final miter [default = %s]\n", pParams->fTryProve? "yes": "no" ); + fprintf( pErr, "\t-p : toggle proving the miter outputs [default = %s]\n", pParams->fTryProve? "yes": "no" ); 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" ); @@ -7699,7 +7873,8 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Abc_NtkAigToSeq( pNtk ); +// pNtkRes = Abc_NtkAigToSeq( pNtk ); + pNtkRes = NULL; if ( pNtkRes == NULL ) { fprintf( pErr, "Converting to sequential AIG has failed.\n" ); @@ -7772,7 +7947,8 @@ int Abc_CommandUnseq( Abc_Frame_t * pAbc, int argc, char ** argv ) // Seq_NtkShareFanouts(pNtk); // get the new network - pNtkRes = Abc_NtkSeqToLogicSop( pNtk ); +// pNtkRes = Abc_NtkSeqToLogicSop( pNtk ); + pNtkRes = NULL; if ( pNtkRes == NULL ) { fprintf( pErr, "Converting sequential AIG into an SOP logic network has failed.\n" ); @@ -7804,24 +7980,26 @@ usage: int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; - Abc_Ntk_t * pNtk, * pNtkTemp; + Abc_Ntk_t * pNtk, * pNtkRes; int c, nMaxIters; - int fInitial; + int fForward; + int fBackward; int fVerbose; int Mode; - extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fVerbose ); + extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - Mode = 3; - fInitial = 1; - fVerbose = 1; + Mode = 5; + fForward = 0; + fBackward = 0; + fVerbose = 1; nMaxIters = 15; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Mvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Mfbvh" ) ) != EOF ) { switch ( c ) { @@ -7836,6 +8014,12 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( Mode < 0 ) goto usage; break; + case 'f': + fForward ^= 1; + break; + case 'b': + fBackward ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -7852,6 +8036,12 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } + if ( fForward && fBackward ) + { + fprintf( pErr, "Only one switch \"-f\" or \"-b\" can be selected at a time.\n" ); + return 1; + } + if ( !Abc_NtkLatchNum(pNtk) ) { fprintf( pErr, "The network has no latches. Retiming is not performed.\n" ); @@ -7865,8 +8055,13 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Retiming with choice nodes is not implemented.\n" ); return 0; } - pNtk = Abc_NtkAigToLogicSop( pNtkTemp = pNtk ); - Abc_NtkDelete( pNtkTemp ); + // convert the network into an SOP network + pNtkRes = Abc_NtkAigToLogicSop( pNtk ); + // perform the retiming + Abc_NtkRetime( pNtkRes, Mode, fForward, fBackward, fVerbose ); + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; } // get the network in the SOP form @@ -7883,19 +8078,21 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) } // perform the retiming - Abc_NtkRetime( pNtk, Mode, fVerbose ); + Abc_NtkRetime( pNtk, Mode, fForward, fBackward, fVerbose ); return 0; usage: - fprintf( pErr, "usage: retime [-M num] [-vh]\n" ); + fprintf( pErr, "usage: retime [-M num] [-fbvh]\n" ); fprintf( pErr, "\t retimes the current network using one of the algorithms:\n" ); fprintf( pErr, "\t 1: most forward retiming\n" ); fprintf( pErr, "\t 2: most backward retiming\n" ); - fprintf( pErr, "\t 3: min-area retiming\n" ); - fprintf( pErr, "\t 4: min-delay retiming\n" ); - fprintf( pErr, "\t 5: min-area under min-delay constraint retiming\n" ); + fprintf( pErr, "\t 3: forward and backward min-area retiming\n" ); + fprintf( pErr, "\t 4: forward and backward min-delay retiming\n" ); + fprintf( pErr, "\t 5: mode 3 followed by mode 4\n" ); fprintf( pErr, "\t-M num : the retiming algorithm to use [default = %d]\n", Mode ); - fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-f : enables forward-only retiming in modes 3,4,5 [default = %s]\n", fForward? "yes": "no" ); + fprintf( pErr, "\t-b : enables backward-only retiming in modes 3,4,5 [default = %s]\n", fBackward? "yes": "no" ); + fprintf( pErr, "\t-v : enables verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; // fprintf( pErr, "\t-I num : max number of iterations of l-value computation [default = %d]\n", nMaxIters ); @@ -7971,10 +8168,11 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } */ - if ( Abc_NtkIsStrash(pNtk) ) - pNtkNew = Abc_NtkAigToSeq(pNtk); - else - pNtkNew = Abc_NtkDup(pNtk); +// if ( Abc_NtkIsStrash(pNtk) ) +// pNtkNew = Abc_NtkAigToSeq(pNtk); +// else +// pNtkNew = Abc_NtkDup(pNtk); + pNtkNew = NULL; } else { @@ -7995,7 +8193,8 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) } // convert into a sequential AIG - pNtkNew = Abc_NtkAigToSeq( pNtkRes = pNtkNew ); +// pNtkNew = Abc_NtkAigToSeq( pNtkRes = pNtkNew ); + pNtkNew = NULL; Abc_NtkDelete( pNtkRes ); if ( pNtkNew == NULL ) { @@ -8007,7 +8206,8 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Seq_NtkFpgaMapRetime( pNtkNew, nMaxIters, fVerbose ); +// pNtkRes = Seq_NtkFpgaMapRetime( pNtkNew, nMaxIters, fVerbose ); + pNtkRes = NULL; if ( pNtkRes == NULL ) { // fprintf( pErr, "Sequential FPGA mapping has failed.\n" ); @@ -8095,10 +8295,11 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } */ - if ( Abc_NtkIsStrash(pNtk) ) - pNtkNew = Abc_NtkAigToSeq(pNtk); - else - pNtkNew = Abc_NtkDup(pNtk); +// if ( Abc_NtkIsStrash(pNtk) ) +// pNtkNew = Abc_NtkAigToSeq(pNtk); +// else +// pNtkNew = Abc_NtkDup(pNtk); + pNtkNew = NULL; } else { @@ -8119,7 +8320,8 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv ) } // convert into a sequential AIG - pNtkNew = Abc_NtkAigToSeq( pNtkRes = pNtkNew ); +// pNtkNew = Abc_NtkAigToSeq( pNtkRes = pNtkNew ); + pNtkNew = NULL; Abc_NtkDelete( pNtkRes ); if ( pNtkNew == NULL ) { @@ -8131,7 +8333,8 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv ) } // get the new network - pNtkRes = Seq_MapRetime( pNtkNew, nMaxIters, fVerbose ); +// pNtkRes = Seq_MapRetime( pNtkNew, nMaxIters, fVerbose ); + pNtkRes = NULL; if ( pNtkRes == NULL ) { // fprintf( pErr, "Sequential FPGA mapping has failed.\n" ); @@ -8481,7 +8684,7 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) int nInsLimit; extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nInsLimit, int nFrames ); - extern void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose ); + extern int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); @@ -8904,6 +9107,63 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandDebug( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + extern void Abc_NtkAutoDebug( Abc_Ntk_t * pNtk, int (*pFuncError) (Abc_Ntk_t *) ); + extern int Abc_NtkRetimeDebug( Abc_Ntk_t * pNtk ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsLogic(pNtk) ) + { + fprintf( pErr, "This command is applicable to logic networks.\n" ); + return 1; + } + + Abc_NtkAutoDebug( pNtk, Abc_NtkRetimeDebug ); + return 0; + +usage: + fprintf( pErr, "usage: debug [-h]\n" ); + fprintf( pErr, "\t performs automated debugging of the given procedure\n" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* @@ -9101,7 +9361,8 @@ int Abc_CommandHoward( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } - result = Seq_NtkHoward( pNtk, fVerbose ); +// result = Seq_NtkHoward( pNtk, fVerbose ); + result = 0; if (result < 0) { fprintf( pErr, "Analysis failed.\n" ); @@ -9178,7 +9439,7 @@ int Abc_CommandSkewForward( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } - Seq_NtkSkewForward( pNtk, target, fMinimize ); +// Seq_NtkSkewForward( pNtk, target, fMinimize ); return 1; diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c index 7024a970..c021728a 100644 --- a/src/base/abci/abcCut.c +++ b/src/base/abci/abcCut.c @@ -20,7 +20,7 @@ #include "abc.h" #include "cut.h" -#include "seqInt.h" +//#include "seqInt.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -401,6 +401,7 @@ void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree ) ***********************************************************************/ void Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fTriv ) { +/* int CutSetNum; assert( Abc_NtkIsSeq(pObj->pNtk) ); assert( Abc_ObjFaninNum(pObj) == 2 ); @@ -408,6 +409,7 @@ void Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fTriv ) CutSetNum = pObj->fMarkC ? (int)pObj->pCopy : -1; Cut_NodeComputeCutsSeq( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj), Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj), Seq_ObjFaninL0(pObj), Seq_ObjFaninL1(pObj), fTriv, CutSetNum ); +*/ } /**Function************************************************************* diff --git a/src/base/abci/abcDebug.c b/src/base/abci/abcDebug.c new file mode 100644 index 00000000..4d37c496 --- /dev/null +++ b/src/base/abci/abcDebug.c @@ -0,0 +1,198 @@ +/**CFile**************************************************************** + + FileName [abcDebug.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Automated debugging procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcDebug.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static int Abc_NtkCountFaninsTotal( Abc_Ntk_t * pNtk ); +static Abc_Ntk_t * Abc_NtkAutoDebugModify( Abc_Ntk_t * pNtk, int ObjNum, int fConst1 ); + +extern void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Takes a network and a procedure to test.] + + Description [The network demonstrates the bug in the procedure. + Procedure should return 1 if the bug is demonstrated.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkAutoDebug( Abc_Ntk_t * pNtk, int (*pFuncError) (Abc_Ntk_t *) ) +{ + Abc_Ntk_t * pNtkMod; + char * pFileName = "bug_found.blif"; + int i, nSteps, nIter, ModNum, RandNum = 1, clk, clkTotal = clock(); + assert( Abc_NtkIsLogic(pNtk) ); + srand( 0x123123 ); + // create internal copy of the network + pNtk = Abc_NtkDup(pNtk); + if ( !(*pFuncError)( pNtk ) ) + { + printf( "The original network does not cause the bug. Quitting.\n" ); + Abc_NtkDelete( pNtk ); + return; + } + // perform incremental modifications + for ( nIter = 0; ; nIter++ ) + { + clk = clock(); + // count how many ways of modifying the network exists + nSteps = 2 * Abc_NtkCountFaninsTotal(pNtk); + // try modifying the network as many times + RandNum ^= rand(); + for ( i = 0; i < nSteps; i++ ) + { + // get the shifted number of bug + ModNum = (i + RandNum) % nSteps; + // get the modified network + pNtkMod = Abc_NtkAutoDebugModify( pNtk, ModNum/2, ModNum%2 ); + // write the network + Io_WriteBlifLogic( pNtk, "bug_temp.blif", 1 ); + // check if the bug is still there + if ( (*pFuncError)( pNtkMod ) ) // bug is still there + { + Abc_NtkDelete( pNtk ); + pNtk = pNtkMod; + break; + } + else // no bug + Abc_NtkDelete( pNtkMod ); + } + printf( "Iteration %6d : Nodes = %6d. Steps = %6d. Error step = %3d. ", nIter, Abc_NtkObjNum(pNtk), nSteps, i ); + PRT( "Time", clock() - clk ); + if ( i == nSteps ) // could not modify it while preserving the bug + break; + } + // write out the final network + Io_WriteBlifLogic( pNtk, pFileName, 1 ); + printf( "Final network written into file \"%s\". ", pFileName ); + PRT( "Total time", clock() - clkTotal ); + Abc_NtkDelete( pNtk ); +} + +/**Function************************************************************* + + Synopsis [Counts the total number of fanins.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkCountFaninsTotal( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj, * pFanin; + int i, k, Counter = 0; + Abc_NtkForEachObj( pNtk, pObj, i ) + Abc_ObjForEachFanin( pObj, pFanin, k ) + { + if ( Abc_NodeIsConst(pFanin) ) + continue; + Counter++; + } + return Counter; +} + +/**Function************************************************************* + + Synopsis [Returns the node and fanin to be modified.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkFindGivenFanin( Abc_Ntk_t * pNtk, int Step, Abc_Obj_t ** ppObj, Abc_Obj_t ** ppFanin ) +{ + Abc_Obj_t * pObj, * pFanin; + int i, k, Counter = 0; + Abc_NtkForEachObj( pNtk, pObj, i ) + Abc_ObjForEachFanin( pObj, pFanin, k ) + { + if ( Abc_NodeIsConst(pFanin) ) + continue; + if ( Counter++ == Step ) + { + *ppObj = pObj; + *ppFanin = pFanin; + return 1; + } + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Perform modification with the given number.] + + Description [Modification consists of replacing the node by a constant.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkAutoDebugModify( Abc_Ntk_t * pNtkInit, int Step, int fConst1 ) +{ + Abc_Ntk_t * pNtk; + Abc_Obj_t * pObj, * pFanin, * pConst; + // copy the network + pNtk = Abc_NtkDup( pNtkInit ); + assert( Abc_NtkNodeNum(pNtk) == Abc_NtkNodeNum(pNtkInit) ); + // find the object number + Abc_NtkFindGivenFanin( pNtk, Step, &pObj, &pFanin ); + // consider special case + if ( Abc_ObjIsPo(pObj) && Abc_NodeIsConst(pFanin) ) + { + Abc_NtkDeleteAll_rec( pObj ); + return pNtk; + } + // plug in a constant node + pConst = fConst1? Abc_NtkCreateNodeConst1(pNtk) : Abc_NtkCreateNodeConst0(pNtk); + Abc_ObjTransferFanout( pFanin, pConst ); + Abc_NtkDeleteAll_rec( pFanin ); + + Abc_NtkSweep( pNtk, 0 ); + Abc_NtkCleanupSeq( pNtk, 0 ); + Abc_NtkLogicToSop( pNtk, 0 ); + Abc_NtkCycleInitStateSop( pNtk, 20, 0 ); + return pNtk; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c index 446eb0cc..30ed21cf 100644 --- a/src/base/abci/abcIvy.c +++ b/src/base/abci/abcIvy.c @@ -84,7 +84,7 @@ Ivy_Man_t * Abc_NtkIvyBefore( Abc_Ntk_t * pNtk, int fSeq, int fUseDc ) } if ( fSeq && Abc_NtkCountSelfFeedLatches(pNtk) ) { - printf( "Warning: The network has %d self-feeding latches. Quitting.\n", Abc_NtkCountSelfFeedLatches(pNtk) ); + printf( "Warning: The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtk) ); // return NULL; } // print warning about choice nodes @@ -369,7 +369,7 @@ Abc_Ntk_t * Abc_NtkIvySat( Abc_Ntk_t * pNtk, int nConfLimit, int fVerbose ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fProve, int fVerbose ) +Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, int fProve, int fVerbose ) { Ivy_FraigParams_t Params, * pParams = &Params; Abc_Ntk_t * pNtkAig; @@ -379,8 +379,9 @@ Abc_Ntk_t * Abc_NtkIvyFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fProve, int f return NULL; Ivy_FraigParamsDefault( pParams ); pParams->nBTLimitNode = nConfLimit; - pParams->fVerbose = fVerbose; - pParams->fProve = fProve; + pParams->fVerbose = fVerbose; + pParams->fProve = fProve; + pParams->fDoSparse = fDoSparse; pMan = Ivy_FraigPerform( pTemp = pMan, pParams ); Ivy_ManStop( pTemp ); pNtkAig = Abc_NtkIvyAfter( pNtk, pMan, 0, 0 ); @@ -668,8 +669,8 @@ Abc_Ntk_t * Abc_NtkFromAigSeq( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan, int fHaig Ivy_ManForEachNodeVec( pMan, vLatches, pNode, i ) { pObjNew = Abc_NtkCreateLatch( pNtk ); - pFaninNew0 = Abc_NtkCreateBo( pNtk ); - pFaninNew1 = Abc_NtkCreateBi( pNtk ); + pFaninNew0 = Abc_NtkCreateBi( pNtk ); + pFaninNew1 = Abc_NtkCreateBo( pNtk ); Abc_ObjAddFanin( pObjNew, pFaninNew0 ); Abc_ObjAddFanin( pFaninNew1, pObjNew ); if ( fHaig || Ivy_ObjInit(pNode) == IVY_INIT_DC ) diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c index a1f6b9f9..f99f7bce 100644 --- a/src/base/abci/abcNtbdd.c +++ b/src/base/abci/abcNtbdd.c @@ -343,7 +343,7 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly */ // reset references Abc_NtkForEachObj( pNtk, pObj, i ) - if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBi(pObj) ) + if ( !Abc_ObjIsBox(pObj) && !Abc_ObjIsBo(pObj) ) Abc_ObjForEachFanin( pObj, pFanin, k ) pFanin->vFanouts.nSize++; diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index 6af12afd..bdca4a8e 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -22,7 +22,7 @@ #include "dec.h" #include "main.h" #include "mio.h" -#include "seq.h" +//#include "seq.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -142,7 +142,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) fprintf( pTable, "\n" ); fclose( pTable ); } -*/ +*/ /* // print the statistic into a file @@ -162,14 +162,22 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) /* // print the statistic into a file { + static int Counter = 0; + extern int timeRetime; FILE * pTable; - pTable = fopen( "stats.txt", "a+" ); - fprintf( pTable, "%s ", pNtk->pName ); + Counter++; + pTable = fopen( "sap/stats_retime.txt", "a+" ); + fprintf( pTable, "%s ", pNtk->pName ); + fprintf( pTable, "%d ", Abc_NtkNodeNum(pNtk) ); fprintf( pTable, "%d ", Abc_NtkLatchNum(pNtk) ); - fprintf( pTable, "\n" ); + fprintf( pTable, "%d ", Abc_NtkGetLevelNum(pNtk) ); + fprintf( pTable, "%.2f ", (float)(timeRetime)/(float)(CLOCKS_PER_SEC) ); + if ( Counter % 4 == 0 ) + fprintf( pTable, "\n" ); fclose( pTable ); } */ + /* s_TotalNodes += Abc_NtkNodeNum(pNtk); printf( "Total nodes = %6d %6.2f Mb Changes = %6d.\n", @@ -254,8 +262,18 @@ void Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk ) InitNums[Init]++; pFanin = Abc_ObjFanin0(Abc_ObjFanin0(pLatch)); - if ( !Abc_ObjIsNode(pFanin) || !Abc_NodeIsConst(pFanin) ) - continue; + if ( Abc_NtkIsLogic(pNtk) ) + { + if ( !Abc_NodeIsConst(pFanin) ) + continue; + } + else if ( Abc_NtkIsStrash(pNtk) ) + { + if ( !Abc_AigNodeIsConst(pFanin) ) + continue; + } + else + assert( 0 ); // the latch input is a constant node Counter0++; diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c index 61be3dee..9fcc6979 100644 --- a/src/base/abci/abcResub.c +++ b/src/base/abci/abcResub.c @@ -147,9 +147,9 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, bool fUpd if ( fUpdateLevel ) Abc_NtkStartReverseLevels( pNtk ); -// if ( Abc_NtkLatchNum(pNtk) ) -// Abc_NtkForEachLatch(pNtk, pNode, i) -// pNode->pNext = pNode->pData; + if ( Abc_NtkLatchNum(pNtk) ) + Abc_NtkForEachLatch(pNtk, pNode, i) + pNode->pNext = pNode->pData; // resynthesize each node once nNodes = Abc_NtkObjNumMax(pNtk); @@ -221,9 +221,9 @@ pManRes->timeTotal = clock() - clkStart; Abc_NtkForEachObj( pNtk, pNode, i ) pNode->pData = NULL; -// if ( Abc_NtkLatchNum(pNtk) ) -// Abc_NtkForEachLatch(pNtk, pNode, i) -// pNode->pData = pNode->pNext, pNode->pNext = NULL; + if ( Abc_NtkLatchNum(pNtk) ) + Abc_NtkForEachLatch(pNtk, pNode, i) + pNode->pData = pNode->pNext, pNode->pNext = NULL; // put the nodes into the DFS order and reassign their IDs Abc_NtkReassignIds( pNtk ); diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c index 076bee46..db926d17 100644 --- a/src/base/abci/abcSweep.c +++ b/src/base/abci/abcSweep.c @@ -860,7 +860,7 @@ int Abc_NtkReplaceAutonomousLogic( Abc_Ntk_t * pNtk ) continue; // skip constants and latches fed by constants if ( Abc_NtkCheckConstant_rec(pFanin) != -1 || - (Abc_ObjIsBi(pFanin) && Abc_NtkCheckConstant_rec(Abc_ObjFanin0(Abc_ObjFanin0(pFanin))) != -1) ) + (Abc_ObjIsBo(pFanin) && Abc_NtkCheckConstant_rec(Abc_ObjFanin0(Abc_ObjFanin0(pFanin))) != -1) ) { Abc_NtkSetTravId_rec( pFanin ); continue; @@ -874,6 +874,7 @@ int Abc_NtkReplaceAutonomousLogic( Abc_Ntk_t * pNtk ) Vec_PtrForEachEntry( vNodes, pNode, i ) { pFanin = Abc_NtkCreatePi(pNtk); + Abc_ObjAssignName( pFanin, Abc_ObjName(pFanin), NULL ); Abc_NodeSetTravIdCurrent( pFanin ); Abc_ObjTransferFanout( pNode, pFanin ); } diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c index cced1c47..e4873986 100644 --- a/src/base/abci/abcUnreach.c +++ b/src/base/abci/abcUnreach.c @@ -95,7 +95,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose ) pNtk->pManGlob = NULL; // make sure that everything is okay - if ( !Abc_NtkCheck( pNtk->pExdc ) ) + if ( pNtk->pExdc && !Abc_NtkCheck( pNtk->pExdc ) ) { printf( "Abc_NtkExtractSequentialDcs: The network check has failed.\n" ); Abc_NtkDelete( pNtk->pExdc ); diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 594cc2d6..ad58e35c 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -286,7 +286,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI SeeAlso [] ***********************************************************************/ -void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose ) +int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose ) { Fraig_Params_t Params; Fraig_Man_t * pMan; @@ -299,7 +299,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF if ( pMiter == NULL ) { printf( "Miter computation has failed.\n" ); - return; + return 0; } RetValue = Abc_NtkMiterIsConstant( pMiter ); if ( RetValue == 0 ) @@ -310,13 +310,13 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pMiter->pModel, nFrames ); FREE( pMiter->pModel ); Abc_NtkDelete( pMiter ); - return; + return 0; } if ( RetValue == 1 ) { Abc_NtkDelete( pMiter ); printf( "Networks are equivalent after structural hashing.\n" ); - return; + return 1; } // create the timeframes @@ -325,7 +325,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF if ( pFrames == NULL ) { printf( "Frames computation has failed.\n" ); - return; + return 0; } RetValue = Abc_NtkMiterIsConstant( pFrames ); if ( RetValue == 0 ) @@ -336,13 +336,13 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF // Abc_NtkVerifyReportErrorSeq( pNtk1, pNtk2, pFrames->pModel, nFrames ); FREE( pFrames->pModel ); Abc_NtkDelete( pFrames ); - return; + return 0; } if ( RetValue == 1 ) { Abc_NtkDelete( pFrames ); printf( "Networks are equivalent after framing.\n" ); - return; + return 1; } // convert the miter into a FRAIG @@ -372,6 +372,7 @@ void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nF Fraig_ManFree( pMan ); // delete the miter Abc_NtkDelete( pFrames ); + return RetValue == 1; } /**Function************************************************************* diff --git a/src/base/abci/abcXsim.c b/src/base/abci/abcXsim.c index 1d56ba36..d17ab1dd 100644 --- a/src/base/abci/abcXsim.c +++ b/src/base/abci/abcXsim.c @@ -24,9 +24,9 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -#define XVS0 1 -#define XVS1 2 -#define XVSX 3 +#define XVS0 ABC_INIT_ZERO +#define XVS1 ABC_INIT_ONE +#define XVSX ABC_INIT_DC static inline void Abc_ObjSetXsim( Abc_Obj_t * pObj, int Value ) { pObj->pCopy = (void *)Value; } static inline int Abc_ObjGetXsim( Abc_Obj_t * pObj ) { return (int)pObj->pCopy; } @@ -157,6 +157,49 @@ void Abc_NtkXValueSimulate( Abc_Ntk_t * pNtk, int nFrames, int fInputs, int fVer } } +/**Function************************************************************* + + Synopsis [Cycles the circuit to create a new initial state.] + + Description [Simulates the circuit with random input for the given + number of timeframes to get a better initial state.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkCycleInitState( Abc_Ntk_t * pNtk, int nFrames, int fVerbose ) +{ + Abc_Obj_t * pObj; + int i, f; + assert( Abc_NtkIsStrash(pNtk) ); + srand( 0x12341234 ); + // initialize the values + Abc_ObjSetXsim( Abc_AigConst1(pNtk), XVS1 ); + Abc_NtkForEachPi( pNtk, pObj, i ) + Abc_ObjSetXsim( pObj, Abc_XsimRand2() ); + Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_LatchIsInit1(pObj)? XVS1 : XVS0 ); + // simulate for the given number of timeframes + for ( f = 0; f < nFrames; f++ ) + { + Abc_AigForEachAnd( pNtk, pObj, i ) + Abc_ObjSetXsim( pObj, Abc_XsimAnd(Abc_ObjGetXsimFanin0(pObj), Abc_ObjGetXsimFanin1(pObj)) ); + Abc_NtkForEachCo( pNtk, pObj, i ) + Abc_ObjSetXsim( pObj, Abc_ObjGetXsimFanin0(pObj) ); + // assign input values + Abc_NtkForEachPi( pNtk, pObj, i ) + Abc_ObjSetXsim( pObj, Abc_XsimRand2() ); + // transfer the latch values + Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_ObjSetXsim( Abc_ObjFanout0(pObj), Abc_ObjGetXsim(Abc_ObjFanin0(pObj)) ); + } + // set the final values + Abc_NtkForEachLatch( pNtk, pObj, i ) + pObj->pData = (void *)Abc_ObjGetXsim(Abc_ObjFanout0(pObj)); +} + /////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 50a40393..7db26629 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -6,6 +6,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcClpBdd.c \ src/base/abci/abcClpSop.c \ src/base/abci/abcCut.c \ + src/base/abci/abcDebug.c \ src/base/abci/abcDsd.c \ src/base/abci/abcEspresso.c \ src/base/abci/abcExtract.c \ diff --git a/src/base/io/io.c b/src/base/io/io.c index 9c1b94ab..7a661664 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -40,6 +40,7 @@ static int IoCommandReadTruth ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteBaf ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteBlif ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteBench ( Abc_Frame_t * pAbc, int argc, char **argv ); +static int IoCommandWriteCellNet( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteCnf ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteDot ( Abc_Frame_t * pAbc, int argc, char **argv ); static int IoCommandWriteEqn ( Abc_Frame_t * pAbc, int argc, char **argv ); @@ -84,6 +85,7 @@ void Io_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "I/O", "write_baf", IoCommandWriteBaf, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_blif", IoCommandWriteBlif, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_bench", IoCommandWriteBench, 0 ); + Cmd_CommandAdd( pAbc, "I/O", "write_cellnet", IoCommandWriteCellNet, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_cnf", IoCommandWriteCnf, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_dot", IoCommandWriteDot, 0 ); Cmd_CommandAdd( pAbc, "I/O", "write_eqn", IoCommandWriteEqn, 0 ); @@ -1189,6 +1191,68 @@ usage: SeeAlso [] ***********************************************************************/ +int IoCommandWriteCellNet( Abc_Frame_t * pAbc, int argc, char **argv ) +{ + Abc_Ntk_t * pNtk; + char * FileName; + int c; + extern void Io_WriteCellNet( Abc_Ntk_t * pNtk, char * pFileName ); + + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + + pNtk = pAbc->pNtkCur; + if ( pNtk == NULL ) + { + fprintf( pAbc->Out, "Empty network.\n" ); + return 0; + } + + if ( argc != globalUtilOptind + 1 ) + { + goto usage; + } + // get the input file name + FileName = argv[globalUtilOptind]; + + if ( !Abc_NtkIsLogic(pNtk) ) + { + fprintf( pAbc->Out, "The network should be a logic network (if it an AIG, use command \"logic\")\n" ); + return 0; + } + + // derive the netlist + Io_WriteCellNet( pNtk, FileName ); + return 0; + +usage: + fprintf( pAbc->Err, "usage: write_cellnet [-h] <file>\n" ); + fprintf( pAbc->Err, "\t write the network is the cellnet format\n" ); + fprintf( pAbc->Err, "\t-h : print the help massage\n" ); + fprintf( pAbc->Err, "\tfile : the name of the file to write\n" ); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv ) { char * FileName; diff --git a/src/base/io/ioReadBaf.c b/src/base/io/ioReadBaf.c index 15d75ba8..a6e0c2e2 100644 --- a/src/base/io/ioReadBaf.c +++ b/src/base/io/ioReadBaf.c @@ -100,10 +100,10 @@ Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck ) pObj = Abc_NtkCreateLatch(pNtkNew); Abc_ObjAssignName( pObj, pCur, NULL ); while ( *pCur++ ); - pNode0 = Abc_NtkCreateBo(pNtkNew); + pNode0 = Abc_NtkCreateBi(pNtkNew); Abc_ObjAssignName( pNode0, pCur, NULL ); while ( *pCur++ ); - pNode1 = Abc_NtkCreateBi(pNtkNew); + pNode1 = Abc_NtkCreateBo(pNtkNew); Abc_ObjAssignName( pNode1, pCur, NULL ); while ( *pCur++ ); Vec_PtrPush( vNodes, pNode1 ); diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c index aa7f82e3..72dd2b52 100644 --- a/src/base/io/ioReadBench.c +++ b/src/base/io/ioReadBench.c @@ -142,6 +142,8 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p ) Abc_ObjSetData( pNode, Abc_SopCreateBuf(pNtk->pManFunc) ); else if ( strcmp(pType, "NOT") == 0 ) Abc_ObjSetData( pNode, Abc_SopCreateInv(pNtk->pManFunc) ); + else if ( strncmp(pType, "MUX", 3) == 0 ) + Abc_ObjSetData( pNode, Abc_SopRegister(pNtk->pManFunc, "1-0 1\n-11 1\n") ); else { printf( "Cannot determine gate type \"%s\" in line %d.\n", pType, Extra_FileReaderGetLineNumber(p, 0) ); diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c index 8b7e015b..d7f456ff 100644 --- a/src/base/io/ioReadBlif.c +++ b/src/base/io/ioReadBlif.c @@ -354,7 +354,7 @@ int Io_ReadBlifNetworkAsserts( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens ) ***********************************************************************/ int Io_ReadBlifNetworkLatch( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens ) -{ +{ Abc_Ntk_t * pNtk = p->pNtkCur; Abc_Obj_t * pLatch; int ResetValue; diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c index f2f07b14..dff27dd1 100644 --- a/src/base/io/ioUtil.c +++ b/src/base/io/ioUtil.c @@ -120,13 +120,13 @@ Abc_Obj_t * Io_ReadCreateLatch( Abc_Ntk_t * pNtk, char * pNetLI, char * pNetLO ) // get the LI net pNet = Abc_NtkFindOrCreateNet( pNtk, pNetLI ); // add the BO terminal - pTerm = Abc_NtkCreateBo( pNtk ); + pTerm = Abc_NtkCreateBi( pNtk ); Abc_ObjAddFanin( pTerm, pNet ); // add the latch box pLatch = Abc_NtkCreateLatch( pNtk ); Abc_ObjAddFanin( pLatch, pTerm ); // add the BI terminal - pTerm = Abc_NtkCreateBi( pNtk ); + pTerm = Abc_NtkCreateBo( pNtk ); Abc_ObjAddFanin( pTerm, pLatch ); // get the LO net pNet = Abc_NtkFindOrCreateNet( pNtk, pNetLO ); diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c index 05539c40..3cc3fcfe 100644 --- a/src/base/io/ioWriteDot.c +++ b/src/base/io/ioWriteDot.c @@ -19,7 +19,9 @@ ***********************************************************************/ #include "io.h" -#include "seqInt.h" +#include "main.h" +#include "mio.h" +//#include "seqInt.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -292,6 +294,10 @@ void Io_WriteDotAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho { if ( Abc_ObjFaninNum(pNode) == 0 ) continue; + + if ( Abc_ObjIsBo(pNode) ) + continue; + if ( fMulti && Abc_ObjIsNode(pNode) ) { Vec_Ptr_t * vSuper; @@ -305,6 +311,10 @@ void Io_WriteDotAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho pFanin = Abc_ObjRegular(pFanin); if ( !pFanin->fMarkC ) continue; + + if ( Abc_ObjIsBi(pFanin) ) + continue; + fprintf( pFile, "Node%d", pNode->Id ); fprintf( pFile, " -> " ); fprintf( pFile, "Node%d%s", pFanin->Id, (Abc_ObjIsLatch(pFanin)? "_out":"") ); @@ -316,7 +326,7 @@ void Io_WriteDotAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho continue; } // generate the edge from this node to the next - if ( Abc_ObjFanin0(pNode)->fMarkC ) + if ( Abc_ObjFanin0(pNode)->fMarkC && !Abc_ObjIsBi(Abc_ObjFanin0(pNode)) ) { fprintf( pFile, "Node%d%s", pNode->Id, (Abc_ObjIsLatch(pNode)? "_in":"") ); fprintf( pFile, " -> " ); @@ -331,7 +341,7 @@ void Io_WriteDotAig( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho if ( Abc_ObjFaninNum(pNode) == 1 ) continue; // generate the edge from this node to the next - if ( Abc_ObjFanin1(pNode)->fMarkC ) + if ( Abc_ObjFanin1(pNode)->fMarkC && !Abc_ObjIsBi(Abc_ObjFanin1(pNode)) ) { fprintf( pFile, "Node%d", pNode->Id ); fprintf( pFile, " -> " ); @@ -392,7 +402,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho int LevelMin, LevelMax, fHasCos, Level, i, k, fHasBdds; int Limit = 300; - assert( !Abc_NtkHasAig(pNtk) ); + assert( !Abc_NtkIsStrash(pNtk) ); if ( vNodes->nSize < 1 ) { @@ -606,7 +616,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho fprintf( pFile, " rank = same;\n" ); // the labeling node of this level fprintf( pFile, " Level%d;\n", LevelMin ); - // generat the PO nodes + // generate the PO nodes Vec_PtrForEachEntry( vNodes, pNode, i ) { if ( !Abc_ObjIsCi(pNode) ) @@ -653,6 +663,11 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho { if ( !Abc_ObjFanin0(pNode)->fMarkC ) continue; + + // added to fix the bug after adding boxes + if ( Abc_ObjIsBo(pNode) || Abc_ObjIsBi(pFanin) ) + continue; + // generate the edge from this node to the next fprintf( pFile, "Node%d%s", pNode->Id, (Abc_ObjIsLatch(pNode)? "_in":"") ); fprintf( pFile, " -> " ); diff --git a/src/base/io/ioWriteList.c b/src/base/io/ioWriteList.c index c2bea884..a92c2eff 100644 --- a/src/base/io/ioWriteList.c +++ b/src/base/io/ioWriteList.c @@ -19,7 +19,7 @@ ***********************************************************************/ #include "io.h" -#include "seqInt.h" +//#include "seqInt.h" /* -------- Original Message -------- @@ -159,7 +159,8 @@ void Io_WriteListEdge( FILE * pFile, Abc_Obj_t * pObj ) { fprintf( pFile, " %s", Abc_ObjName(pFanout) ); fprintf( pFile, " ([%s_to_", Abc_ObjName(pObj) ); - fprintf( pFile, "%s] = %d)", Abc_ObjName(pFanout), Seq_ObjFanoutL(pObj, pFanout) ); +// fprintf( pFile, "%s] = %d)", Abc_ObjName(pFanout), Seq_ObjFanoutL(pObj, pFanout) ); + fprintf( pFile, "%s] = %d)", Abc_ObjName(pFanout), 0 ); if ( i != Abc_ObjFanoutNum(pObj) - 1 ) fprintf( pFile, "," ); } @@ -204,6 +205,83 @@ void Io_WriteListHost( FILE * pFile, Abc_Ntk_t * pNtk ) } +/**Function************************************************************* + + Synopsis [Writes the adjacency list for a sequential AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Io_WriteCellNet( Abc_Ntk_t * pNtk, char * pFileName ) +{ + FILE * pFile; + Abc_Obj_t * pObj, * pFanout; + int i, k; + + assert( Abc_NtkIsLogic(pNtk) ); + + // start the output stream + pFile = fopen( pFileName, "w" ); + if ( pFile == NULL ) + { + fprintf( stdout, "Io_WriteCellNet(): Cannot open the output file \"%s\".\n", pFileName ); + return; + } + + fprintf( pFile, "# CellNet file for network \"%s\" written by ABC on %s\n", pNtk->pName, Extra_TimeStamp() ); + + // the only tricky part with writing is handling latches: + // each latch comes with (a) single-input latch-input node, (b) latch proper, (c) single-input latch-output node + // we arbitrarily decide to use the interger ID of the latch-input node to represent the latch in the file + // (this ID is used for both the cell and the net driven by that cell) + + // write the PIs + Abc_NtkForEachPi( pNtk, pObj, i ) + fprintf( pFile, "cell %d is 0\n", pObj->Id ); + // write the POs + Abc_NtkForEachPo( pNtk, pObj, i ) + fprintf( pFile, "cell %d is 1\n", pObj->Id ); + // write the latches (use the ID of latch input) + Abc_NtkForEachLatch( pNtk, pObj, i ) + fprintf( pFile, "cell %d is 2\n", Abc_ObjFanin0(pObj)->Id ); + // write the logic nodes + Abc_NtkForEachNode( pNtk, pObj, i ) + fprintf( pFile, "cell %d is %d\n", pObj->Id, 3+Abc_ObjFaninNum(pObj) ); + + // write the nets driven by PIs + Abc_NtkForEachPi( pNtk, pObj, i ) + { + fprintf( pFile, "net %d %d 0", pObj->Id, pObj->Id ); + Abc_ObjForEachFanout( pObj, pFanout, k ) + fprintf( pFile, " %d %d", pFanout->Id, 1 + Abc_ObjFanoutFaninNum(pFanout, pObj) ); + fprintf( pFile, "\n" ); + } + // write the nets driven by latches + Abc_NtkForEachLatch( pNtk, pObj, i ) + { + fprintf( pFile, "net %d %d 0", Abc_ObjFanin0(pObj)->Id, Abc_ObjFanin0(pObj)->Id ); + pObj = Abc_ObjFanout0(pObj); + Abc_ObjForEachFanout( pObj, pFanout, k ) + fprintf( pFile, " %d %d", pFanout->Id, 1 + Abc_ObjFanoutFaninNum(pFanout, pObj) ); + fprintf( pFile, "\n" ); + } + // write the nets driven by nodes + Abc_NtkForEachNode( pNtk, pObj, i ) + { + fprintf( pFile, "net %d %d 0", pObj->Id, pObj->Id ); + Abc_ObjForEachFanout( pObj, pFanout, k ) + fprintf( pFile, " %d %d", pFanout->Id, 1 + Abc_ObjFanoutFaninNum(pFanout, pObj) ); + fprintf( pFile, "\n" ); + } + + fprintf( pFile, "\n" ); + fclose( pFile ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/misc/nm/nmTable.c b/src/misc/nm/nmTable.c index b209becd..94e46f04 100644 --- a/src/misc/nm/nmTable.c +++ b/src/misc/nm/nmTable.c @@ -110,6 +110,7 @@ int Nm_ManTableDelete( Nm_Man_t * p, int ObjId ) { Nm_Entry_t ** ppSpot, * pEntry, * pPrev; int fRemoved; + p->nEntries--; // remove the entry from the table Id->Name assert( Nm_ManTableLookupId(p, ObjId) != NULL ); ppSpot = p->pBinsI2N + Nm_HashNumber(ObjId, p->nBins); diff --git a/src/opt/ret/module.make b/src/opt/ret/module.make index 9ac0bf1f..c65021c4 100644 --- a/src/opt/ret/module.make +++ b/src/opt/ret/module.make @@ -1,8 +1,7 @@ -SRC += src/opt/dec/retArea.c \ - src/opt/dec/retBwd.c \ - src/opt/dec/retCore.c \ - src/opt/dec/retDelay.c \ - src/opt/dec/retFlow.c \ - src/opt/dec/retFwd.c \ - src/opt/dec/retInit.c +SRC += src/opt/ret/retArea.c \ + src/opt/ret/retCore.c \ + src/opt/ret/retDelay.c \ + src/opt/ret/retFlow.c \ + src/opt/ret/retIncrem.c \ + src/opt/ret/retInit.c diff --git a/src/opt/ret/retArea.c b/src/opt/ret/retArea.c index 7f93b87b..41d19592 100644 --- a/src/opt/ret/retArea.c +++ b/src/opt/ret/retArea.c @@ -50,38 +50,36 @@ extern Abc_Ntk_t * Abc_NtkAttachBottom( Abc_Ntk_t * pNtkTop, Abc_Ntk_t * pNtkBot SeeAlso [] ***********************************************************************/ -int Abc_NtkRetimeMinArea( Abc_Ntk_t * pNtk, int fVerbose ) +int Abc_NtkRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBackwardOnly, int fVerbose ) { - Abc_Ntk_t * pNtkTotal = NULL, * pNtkBottom, * pNtkMiter; - Vec_Int_t * vValues; + Abc_Ntk_t * pNtkTotal = NULL, * pNtkBottom; + Vec_Int_t * vValuesNew = NULL, * vValues; int nLatches = Abc_NtkLatchNum(pNtk); + assert( !fForwardOnly || !fBackwardOnly ); // there should not be black boxes assert( Abc_NtkIsSopLogic(pNtk) ); assert( Abc_NtkLatchNum(pNtk) == Vec_PtrSize(pNtk->vBoxes) ); // reorder CI/CO/latch inputs Abc_NtkOrderCisCos( pNtk ); // perform forward retiming - vValues = Abc_NtkCollectLatchValues( pNtk ); // Abc_NtkRetimeMinAreaFwd( pNtk, fVerbose ); - pNtkTotal = Abc_NtkRetimeMinAreaBwd( pNtk, fVerbose ); - -// while ( Abc_NtkRetimeMinAreaFwd( pNtk, fVerbose ) ); +// pNtkTotal = Abc_NtkRetimeMinAreaBwd( pNtk, fVerbose ); + if ( !fBackwardOnly ) + while ( Abc_NtkRetimeMinAreaFwd( pNtk, fVerbose ) ); + // remember initial values + vValues = Abc_NtkCollectLatchValues( pNtk ); // perform backward retiming -// while ( pNtkBottom = Abc_NtkRetimeMinAreaBwd( pNtk, fVerbose ) ) -// pNtkTotal = Abc_NtkAttachBottom( pNtkTotal, pNtkBottom ); + if ( !fForwardOnly ) +// pNtkTotal = Abc_NtkRetimeMinAreaBwd( pNtk, fVerbose ); + while ( pNtkBottom = Abc_NtkRetimeMinAreaBwd( pNtk, fVerbose ) ) + pNtkTotal = Abc_NtkAttachBottom( pNtkTotal, pNtkBottom ); // compute initial values - if ( pNtkTotal ) - { - // convert the target network to AIG - Abc_NtkLogicToAig( pNtkTotal ); - // get the miter - pNtkMiter = Abc_NtkCreateTarget( pNtkTotal, pNtkTotal->vCos, vValues ); - Abc_NtkDelete( pNtkTotal ); - // get the initial values - Abc_NtkRetimeInitialValues( pNtk, pNtkMiter, fVerbose ); - Abc_NtkDelete( pNtkMiter ); - } - Vec_IntFree( vValues ); + vValuesNew = Abc_NtkRetimeInitialValues( pNtkTotal, vValues, fVerbose ); + if ( pNtkTotal ) Abc_NtkDelete( pNtkTotal ); + // insert new initial values + Abc_NtkInsertLatchValues( pNtk, vValuesNew ); + if ( vValuesNew ) Vec_IntFree( vValuesNew ); + if ( vValues ) Vec_IntFree( vValues ); // fix the COs Abc_NtkLogicMakeSimpleCos( pNtk, 0 ); // check for correctness @@ -311,46 +309,6 @@ void Abc_NtkRetimeMinAreaRemoveBuffers( Abc_Ntk_t * pNtk, Vec_Ptr_t * vBuffers ) /**Function************************************************************* - Synopsis [Computes the results of simulating one node.] - - Description [Assumes that fanins have pCopy set to the input values.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_ObjSopSimulate( Abc_Obj_t * pObj ) -{ - char * pCube, * pSop = pObj->pData; - int nVars, Value, v, ResOr, ResAnd, ResVar; - assert( pSop && !Abc_SopIsExorType(pSop) ); - // simulate the SOP of the node - ResOr = 0; - nVars = Abc_SopGetVarNum(pSop); - Abc_SopForEachCube( pSop, nVars, pCube ) - { - ResAnd = 1; - Abc_CubeForEachVar( pCube, Value, v ) - { - if ( Value == '0' ) - ResVar = 1 ^ ((int)Abc_ObjFanin(pObj, v)->pCopy); - else if ( Value == '1' ) - ResVar = (int)Abc_ObjFanin(pObj, v)->pCopy; - else - continue; - ResAnd &= ResVar; - } - ResOr |= ResAnd; - } - // complement the result if necessary - if ( !Abc_SopGetPhase(pSop) ) - ResOr ^= 1; - return ResOr; -} - -/**Function************************************************************* - Synopsis [Compute initial values.] Description [] @@ -369,7 +327,7 @@ int Abc_NtkRetimeMinAreaInitValue_rec( Abc_Obj_t * pObj ) return (int)pObj->pCopy; Abc_NodeSetTravIdCurrent(pObj); // consider the case of a latch output - if ( Abc_ObjIsBi(pObj) ) + if ( Abc_ObjIsBo(pObj) ) { assert( Abc_ObjIsLatch(Abc_ObjFanin0(pObj)) ); pObj->pCopy = (void *)Abc_NtkRetimeMinAreaInitValue_rec( Abc_ObjFanin0(pObj) ); @@ -431,8 +389,11 @@ Abc_Obj_t * Abc_NtkRetimeMinAreaConstructNtk_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t return pObj->pCopy; Abc_NodeSetTravIdCurrent(pObj); // consider the case of a latch output - if ( Abc_ObjIsBo(pObj) ) - return Abc_NtkRetimeMinAreaConstructNtk_rec( pNtkNew, Abc_ObjFanin0(pObj) ); + if ( Abc_ObjIsBi(pObj) ) + { + pObj->pCopy = Abc_NtkRetimeMinAreaConstructNtk_rec( pNtkNew, Abc_ObjFanin0(pObj) ); + return pObj->pCopy; + } assert( Abc_ObjIsNode(pObj) ); // visit the fanins Abc_ObjForEachFanin( pObj, pFanin, i ) @@ -462,7 +423,7 @@ Abc_Ntk_t * Abc_NtkRetimeMinAreaConstructNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMin int i; // create new network pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 ); - // set mapping of new latches into the PIs of the network + // map new latches into PIs of the new network Abc_NtkIncrementTravId(pNtk); Vec_PtrForEachEntry( vMinCut, pObj, i ) { @@ -475,6 +436,9 @@ Abc_Ntk_t * Abc_NtkRetimeMinAreaConstructNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMin pObjNew = Abc_NtkRetimeMinAreaConstructNtk_rec( pNtkNew, Abc_ObjFanin0(pObj) ); Abc_ObjAddFanin( Abc_NtkCreatePo(pNtkNew), pObjNew ); } + // unmark the nodes in the cut + Vec_PtrForEachEntry( vMinCut, pObj, i ) + Abc_NodeSetTravIdPrevious( pObj ); // assign dummy node names Abc_NtkAddDummyPiNames( pNtkNew ); Abc_NtkAddDummyPoNames( pNtkNew ); @@ -485,6 +449,76 @@ Abc_Ntk_t * Abc_NtkRetimeMinAreaConstructNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMin /**Function************************************************************* + Synopsis [Mark the inside of the min-cut with current traversal ID.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkRetimeMinAreaMarkInside_rec( Abc_Obj_t * pObj, int fForward ) +{ + Abc_Obj_t * pNext; + int i; + // skip visited nodes + if ( Abc_NodeIsTravIdCurrent(pObj) ) + return; + Abc_NodeSetTravIdCurrent( pObj ); + // make sure we never reach PIs/POs/latches + if ( Abc_ObjIsPi(pObj) || Abc_ObjIsPo(pObj) || Abc_ObjIsLatch(pObj) ) + printf( "Abc_NtkRetimeMinAreaMarkInside(): The set of nodes is not a cut. Internal error!!!\n" ); + // continue to explore the cone + if ( fForward ) + { + Abc_ObjForEachFanout( pObj, pNext, i ) + Abc_NtkRetimeMinAreaMarkInside_rec( pNext, fForward ); + } + else + { + Abc_ObjForEachFanin( pObj, pNext, i ) + Abc_NtkRetimeMinAreaMarkInside_rec( pNext, fForward ); + } +} + +/**Function************************************************************* + + Synopsis [Marks the inside of the min-cut with current traversal ID.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkRetimeMinAreaMarkInside( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMinCut, int fForward ) +{ + Abc_Obj_t * pObj; + int i; + // mark the mincut + Abc_NtkIncrementTravId(pNtk); + Vec_PtrForEachEntry( vMinCut, pObj, i ) + Abc_NodeSetTravIdCurrent( pObj ); + // mark the area inside of the cut + if ( fForward ) + { + Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_NtkRetimeMinAreaMarkInside_rec( Abc_ObjFanout0(pObj), fForward ); + } + else + { + Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_NtkRetimeMinAreaMarkInside_rec( Abc_ObjFanin0(pObj), fForward ); + // unmark the nodes in the cut + Vec_PtrForEachEntry( vMinCut, pObj, i ) + Abc_NodeSetTravIdPrevious( pObj ); + } +} + +/**Function************************************************************* + Synopsis [Updates the network after backward retiming.] Description [] @@ -496,9 +530,11 @@ Abc_Ntk_t * Abc_NtkRetimeMinAreaConstructNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMin ***********************************************************************/ void Abc_NtkRetimeMinAreaUpdateLatches( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMinCut, int fForward ) { - Vec_Ptr_t * vCis, * vCos, * vBoxes, * vBoxesNew, * vFanouts; - Abc_Obj_t * pObj, * pLatch, * pLatchIn, * pLatchOut, * pFanout; + Vec_Ptr_t * vCis, * vCos, * vBoxes, * vBoxesNew, * vNodes; + Abc_Obj_t * pObj, * pLatch, * pLatchIn, * pLatchOut, * pNext; int i, k; + // mark the inside of min-cut with new trav ID + Abc_NtkRetimeMinAreaMarkInside( pNtk, vMinCut, fForward ); // create new latches Vec_PtrShrink( pNtk->vCis, Abc_NtkCiNum(pNtk) - Abc_NtkLatchNum(pNtk) ); Vec_PtrShrink( pNtk->vCos, Abc_NtkCoNum(pNtk) - Abc_NtkLatchNum(pNtk) ); @@ -511,8 +547,7 @@ void Abc_NtkRetimeMinAreaUpdateLatches( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMinCut, i if ( !Abc_ObjIsLatch(pObj) ) Vec_PtrPush( vBoxesNew, pObj ); // create or reuse latches - Abc_NtkIncrementTravId(pNtk); - vFanouts = Vec_PtrAlloc( 100 ); + vNodes = Vec_PtrAlloc( 100 ); Vec_PtrForEachEntry( vMinCut, pObj, i ) { if ( Abc_ObjIsCi(pObj) && fForward ) @@ -520,7 +555,7 @@ void Abc_NtkRetimeMinAreaUpdateLatches( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMinCut, i pLatchOut = pObj; pLatch = Abc_ObjFanin0(pLatchOut); pLatchIn = Abc_ObjFanin0(pLatch); - assert( Abc_ObjIsBi(pLatchOut) && Abc_ObjIsLatch(pLatch) && Abc_ObjIsBo(pLatchIn) ); + assert( Abc_ObjIsBo(pLatchOut) && Abc_ObjIsLatch(pLatch) && Abc_ObjIsBi(pLatchIn) ); // mark the latch as reused Abc_NodeSetTravIdCurrent( pLatch ); } @@ -529,15 +564,15 @@ void Abc_NtkRetimeMinAreaUpdateLatches( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMinCut, i pLatchIn = pObj; pLatch = Abc_ObjFanout0(pLatchIn); pLatchOut = Abc_ObjFanout0(pLatch); - assert( Abc_ObjIsBi(pLatchOut) && Abc_ObjIsLatch(pLatch) && Abc_ObjIsBo(pLatchIn) ); + assert( Abc_ObjIsBo(pLatchOut) && Abc_ObjIsLatch(pLatch) && Abc_ObjIsBi(pLatchIn) ); // mark the latch as reused Abc_NodeSetTravIdCurrent( pLatch ); } else { - pLatchOut = Abc_NtkCreateBi(pNtk); + pLatchOut = Abc_NtkCreateBo(pNtk); pLatch = Abc_NtkCreateLatch(pNtk); - pLatchIn = Abc_NtkCreateBo(pNtk); + pLatchIn = Abc_NtkCreateBi(pNtk); Abc_ObjAssignName( pLatchOut, Abc_ObjName(pLatchOut), NULL ); Abc_ObjAssignName( pLatchIn, Abc_ObjName(pLatchIn), NULL ); // connect @@ -545,16 +580,20 @@ void Abc_NtkRetimeMinAreaUpdateLatches( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMinCut, i Abc_ObjAddFanin( pLatch, pLatchIn ); if ( fForward ) { - Abc_ObjTransferFanout( pObj, pLatchOut ); pLatch->pData = (void *)(pObj->pCopy? ABC_INIT_ONE : ABC_INIT_ZERO); + // redirect edges to the unvisited fanouts of the node + Abc_NodeCollectFanouts( pObj, vNodes ); + Vec_PtrForEachEntry( vNodes, pNext, k ) + if ( !Abc_NodeIsTravIdCurrent(pNext) ) + Abc_ObjPatchFanin( pNext, pObj, pLatchOut ); } else { - // redirect unmarked edges - Abc_NodeCollectFanouts( pObj, vFanouts ); - Vec_PtrForEachEntry( vFanouts, pFanout, k ) - if ( !pFanout->fMarkA ) - Abc_ObjPatchFanin( pFanout, pObj, pLatchOut ); + // redirect edges to the visited fanouts of the node + Abc_NodeCollectFanouts( pObj, vNodes ); + Vec_PtrForEachEntry( vNodes, pNext, k ) + if ( Abc_NodeIsTravIdCurrent(pNext) ) + Abc_ObjPatchFanin( pNext, pObj, pLatchOut ); } // connect latch to the node Abc_ObjAddFanin( pLatchIn, pObj ); @@ -563,7 +602,7 @@ void Abc_NtkRetimeMinAreaUpdateLatches( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMinCut, i Vec_PtrPush( vBoxesNew, pLatch ); Vec_PtrPush( vCos, pLatchIn ); } - Vec_PtrFree( vFanouts ); + Vec_PtrFree( vNodes ); // remove useless latches Vec_PtrForEachEntry( vBoxes, pObj, i ) { @@ -574,7 +613,8 @@ void Abc_NtkRetimeMinAreaUpdateLatches( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMinCut, i pLatchOut = Abc_ObjFanout0(pObj); pLatch = pObj; pLatchIn = Abc_ObjFanin0(pObj); - Abc_ObjTransferFanout( pLatchOut, Abc_ObjFanin0(pLatchIn) ); + if ( Abc_ObjFanoutNum(pLatchOut) > 0 ) + Abc_ObjTransferFanout( pLatchOut, Abc_ObjFanin0(pLatchIn) ); Abc_NtkDeleteObj( pLatchOut ); Abc_NtkDeleteObj( pObj ); Abc_NtkDeleteObj( pLatchIn ); diff --git a/src/opt/ret/retBwd.c b/src/opt/ret/retBwd.c deleted file mode 100644 index 7eefc4e0..00000000 --- a/src/opt/ret/retBwd.c +++ /dev/null @@ -1,65 +0,0 @@ -/**CFile**************************************************************** - - FileName [retBwd.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Retiming package.] - - Synopsis [Most backward retiming.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - Oct 31, 2006.] - - Revision [$Id: retBwd.c,v 1.00 2006/10/31 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "retInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkRetimeBackward( Abc_Ntk_t * pNtk, int fVerbose ) -{ - printf( "Not implemented.\n" ); - return 0; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/opt/ret/retCore.c b/src/opt/ret/retCore.c index 541f5962..8ef4e79b 100644 --- a/src/opt/ret/retCore.c +++ b/src/opt/ret/retCore.c @@ -24,6 +24,8 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +int timeRetime = 0; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -39,36 +41,74 @@ SeeAlso [] ***********************************************************************/ -int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fVerbose ) +int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fVerbose ) { - int RetValue; + int nLatches = Abc_NtkLatchNum(pNtk); + int nLevels = Abc_NtkGetLevelNum(pNtk); + int RetValue = 0, clkTotal = clock(); assert( Mode > 0 && Mode < 6 ); + assert( !fForwardOnly || !fBackwardOnly ); // perform forward retiming switch ( Mode ) { case 1: // forward - RetValue = Abc_NtkRetimeForward( pNtk, fVerbose ); + RetValue = Abc_NtkRetimeIncremental( pNtk, 1, 0, fVerbose ); break; case 2: // backward - RetValue = Abc_NtkRetimeBackward( pNtk, fVerbose ); + RetValue = Abc_NtkRetimeIncremental( pNtk, 0, 0, fVerbose ); break; case 3: // min-area - RetValue = Abc_NtkRetimeMinArea( pNtk, fVerbose ); + RetValue = Abc_NtkRetimeMinArea( pNtk, fForwardOnly, fBackwardOnly, fVerbose ); break; case 4: // min-delay - RetValue = Abc_NtkRetimeMinDelay( pNtk, fVerbose ); + if ( !fBackwardOnly ) + RetValue += Abc_NtkRetimeIncremental( pNtk, 1, 1, fVerbose ); + if ( !fForwardOnly ) + RetValue += Abc_NtkRetimeIncremental( pNtk, 0, 1, fVerbose ); break; case 5: // min-area + min-delay - RetValue = Abc_NtkRetimeMinArea( pNtk, fVerbose ); - RetValue += Abc_NtkRetimeMinDelay( pNtk, fVerbose ); + RetValue = Abc_NtkRetimeMinArea( pNtk, fForwardOnly, fBackwardOnly, fVerbose ); + if ( !fBackwardOnly ) + RetValue += Abc_NtkRetimeIncremental( pNtk, 1, 1, fVerbose ); + if ( !fForwardOnly ) + RetValue += Abc_NtkRetimeIncremental( pNtk, 0, 1, fVerbose ); break; default: printf( "Unknown retiming option.\n" ); break; } + if ( fVerbose ) + { + printf( "Reduction in area = %3d. Reduction in delay = %3d. ", + nLatches - Abc_NtkLatchNum(pNtk), nLevels - Abc_NtkGetLevelNum(pNtk) ); + PRT( "Total runtime", clock() - clkTotal ); + } + timeRetime = clock() - clkTotal; return RetValue; } +/**Function************************************************************* + + Synopsis [Used for automated debugging.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRetimeDebug( Abc_Ntk_t * pNtk ) +{ + extern int Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose ); + Abc_Ntk_t * pNtkRet; + assert( Abc_NtkIsLogic(pNtk) ); + Abc_NtkLogicToSop( pNtk, 0 ); + pNtkRet = Abc_NtkDup( pNtk ); + Abc_NtkRetime( pNtkRet, 3, 0, 1, 0 ); + return !Abc_NtkSecFraig( pNtk, pNtkRet, 10000, 3, 0 ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/ret/retDelay.c b/src/opt/ret/retDelay.c index b7ccc570..d2d87447 100644 --- a/src/opt/ret/retDelay.c +++ b/src/opt/ret/retDelay.c @@ -24,30 +24,44 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static int Abc_NtkRetimeMinDelayTry( Abc_Ntk_t * pNtk, int fForward, int fInitial, int nIterLimit, int * pIterBest, int fVerbose ); +static int Abc_NtkRetimeTiming( Abc_Ntk_t * pNtk, int fForward, Vec_Ptr_t * vCritical ); +static int Abc_NtkRetimeTiming_rec( Abc_Obj_t * pObj, int fForward ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [] + Synopsis [Retimes incrementally for minimum delay.] - Description [] + Description [This procedure cannot be called in the application code + because it assumes that the network is preprocessed by removing LIs/LOs.] SideEffects [] SeeAlso [] ***********************************************************************/ -int Abc_NtkRetimeMinDelay( Abc_Ntk_t * pNtk, int fVerbose ) +int Abc_NtkRetimeMinDelay( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkCopy, int nIterLimit, int fForward, int fVerbose ) { - printf( "Not implemented.\n" ); - return 0; + int IterBest, DelayBest; + int IterBest2, DelayBest2; + // try to find the best delay iteration on a copy + DelayBest = Abc_NtkRetimeMinDelayTry( pNtkCopy, fForward, 0, nIterLimit, &IterBest, fVerbose ); + if ( IterBest == 0 ) + return 1; + // perform the given number of iterations on the original network + DelayBest2 = Abc_NtkRetimeMinDelayTry( pNtk, fForward, 1, IterBest, &IterBest2, fVerbose ); + assert( DelayBest == DelayBest2 ); + assert( IterBest == IterBest2 ); + return 1; } /**Function************************************************************* - Synopsis [] + Synopsis [Returns the best delay and the number of best iteration.] Description [] @@ -56,7 +70,217 @@ int Abc_NtkRetimeMinDelay( Abc_Ntk_t * pNtk, int fVerbose ) SeeAlso [] ***********************************************************************/ +int Abc_NtkRetimeMinDelayTry( Abc_Ntk_t * pNtk, int fForward, int fInitial, int nIterLimit, int * pIterBest, int fVerbose ) +{ + Abc_Ntk_t * pNtkNew = NULL; + Vec_Ptr_t * vCritical; + Vec_Int_t * vValues; + Abc_Obj_t * pObj; + int i, k, IterBest, DelayCur, DelayBest, DelayStart; + // transfer intitial values + if ( fInitial ) + { + if ( fForward ) + Abc_NtkRetimeTranferToCopy( pNtk ); + else + { + // save initial value of the latches + vValues = Abc_NtkRetimeCollectLatchValues( pNtk ); + // start the network for initial value computation + pNtkNew = Abc_NtkRetimeBackwardInitialStart( pNtk ); + } + } + // find the best iteration + DelayBest = ABC_INFINITY; IterBest = 0; + vCritical = Vec_PtrAlloc( 100 ); + for ( i = 0; ; i++ ) + { + // perform moves for the timing-critical nodes + DelayCur = Abc_NtkRetimeTiming( pNtk, fForward, vCritical ); + if ( i == 0 ) + DelayStart = DelayCur; + // record this position if it has the best delay + if ( DelayBest > DelayCur ) + { + DelayBest = DelayCur; + IterBest = i; + } + // quit after timing analysis + if ( i == nIterLimit ) + break; + // try retiming to improve the delay + Vec_PtrForEachEntry( vCritical, pObj, k ) + if ( Abc_NtkRetimeNodeIsEnabled(pObj, fForward) ) + Abc_NtkRetimeNode( pObj, fForward, fInitial ); + } + Vec_PtrFree( vCritical ); + // transfer the initial state back to the latches + if ( fInitial ) + { + if ( fForward ) + Abc_NtkRetimeTranferFromCopy( pNtk ); + else + { + Abc_NtkRetimeBackwardInitialFinish( pNtk, pNtkNew, vValues, fVerbose ); + Abc_NtkDelete( pNtkNew ); + Vec_IntFree( vValues ); + } + } + if ( !fInitial && fVerbose ) + printf( "%s : Starting delay = %3d. Final delay = %3d. IterBest = %2d (out of %2d).\n", + fForward? "Forward " : "Backward", DelayStart, DelayBest, IterBest, nIterLimit ); + *pIterBest = IterBest; + return DelayBest; +} + +/**Function************************************************************* + + Synopsis [Returns the set of timing-critical nodes.] + Description [Performs static timing analysis on the network. Uses + unit-delay model.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRetimeTiming( Abc_Ntk_t * pNtk, int fForward, Vec_Ptr_t * vCritical ) +{ + Vec_Ptr_t * vLatches; + Abc_Obj_t * pObj, * pNext; + int i, k, LevelCur, LevelMax = 0; + // mark all objects except nodes + Abc_NtkIncrementTravId(pNtk); + vLatches = Vec_PtrAlloc( Abc_NtkLatchNum(pNtk) ); + Abc_NtkForEachObj( pNtk, pObj, i ) + { + if ( Abc_ObjIsLatch(pObj) ) + Vec_PtrPush( vLatches, pObj ); + if ( Abc_ObjIsNode(pObj) ) + continue; + pObj->Level = 0; + Abc_NodeSetTravIdCurrent( pObj ); + } + // perform analysis from CIs/COs + if ( fForward ) + { + Vec_PtrForEachEntry( vLatches, pObj, i ) + { + Abc_ObjForEachFanout( pObj, pNext, k ) + { + LevelCur = Abc_NtkRetimeTiming_rec( pNext, fForward ); + if ( LevelMax < LevelCur ) + LevelMax = LevelCur; + } + } + Abc_NtkForEachPi( pNtk, pObj, i ) + { + Abc_ObjForEachFanout( pObj, pNext, k ) + { + LevelCur = Abc_NtkRetimeTiming_rec( pNext, fForward ); + if ( LevelMax < LevelCur ) + LevelMax = LevelCur; + } + } + } + else + { + Vec_PtrForEachEntry( vLatches, pObj, i ) + { + LevelCur = Abc_NtkRetimeTiming_rec( Abc_ObjFanin0(pObj), fForward ); + if ( LevelMax < LevelCur ) + LevelMax = LevelCur; + } + Abc_NtkForEachPo( pNtk, pObj, i ) + { + LevelCur = Abc_NtkRetimeTiming_rec( Abc_ObjFanin0(pObj), fForward ); + if ( LevelMax < LevelCur ) + LevelMax = LevelCur; + } + } + // collect timing critical nodes, which should be retimed forward/backward + Vec_PtrClear( vCritical ); + Abc_NtkIncrementTravId(pNtk); + if ( fForward ) + { + Vec_PtrForEachEntry( vLatches, pObj, i ) + { + Abc_ObjForEachFanout( pObj, pNext, k ) + { + if ( Abc_NodeIsTravIdCurrent(pNext) ) + continue; + if ( LevelMax != (int)pNext->Level ) + continue; + // new critical node + Vec_PtrPush( vCritical, pNext ); + Abc_NodeSetTravIdCurrent( pNext ); + } + } + } + else + { + Vec_PtrForEachEntry( vLatches, pObj, i ) + { + Abc_ObjForEachFanin( pObj, pNext, k ) + { + if ( Abc_NodeIsTravIdCurrent(pNext) ) + continue; + if ( LevelMax != (int)pNext->Level ) + continue; + // new critical node + Vec_PtrPush( vCritical, pNext ); + Abc_NodeSetTravIdCurrent( pNext ); + } + } + } + Vec_PtrFree( vLatches ); + return LevelMax; +} + +/**Function************************************************************* + + Synopsis [Recursively performs timing analysis.] + + Description [Performs static timing analysis on the network. Uses + unit-delay model.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRetimeTiming_rec( Abc_Obj_t * pObj, int fForward ) +{ + Abc_Obj_t * pNext; + int i, LevelCur, LevelMax = 0; + // skip visited nodes + if ( Abc_NodeIsTravIdCurrent(pObj) ) + return pObj->Level; + Abc_NodeSetTravIdCurrent(pObj); + // visit the next nodes + if ( fForward ) + { + Abc_ObjForEachFanout( pObj, pNext, i ) + { + LevelCur = Abc_NtkRetimeTiming_rec( pNext, fForward ); + if ( LevelMax < LevelCur ) + LevelMax = LevelCur; + } + } + else + { + Abc_ObjForEachFanin( pObj, pNext, i ) + { + LevelCur = Abc_NtkRetimeTiming_rec( pNext, fForward ); + if ( LevelMax < LevelCur ) + LevelMax = LevelCur; + } + } +// printf( "Node %3d -> Level %3d.\n", pObj->Id, LevelMax + 1 ); + pObj->Level = LevelMax + 1; + return pObj->Level; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/opt/ret/retFlow.c b/src/opt/ret/retFlow.c index 9b8393f3..642a1f69 100644 --- a/src/opt/ret/retFlow.c +++ b/src/opt/ret/retFlow.c @@ -126,9 +126,12 @@ Vec_Ptr_t * Abc_NtkMaxFlow( Abc_Ntk_t * pNtk, int fForward, int fVerbose ) printf( "Abc_NtkMaxFlow() error! The computed min-cut is not a cut!\n" ); // report the results + if ( fVerbose ) + { printf( "Latches = %6d. %s max-flow = %6d. Min-cut = %6d. ", Abc_NtkLatchNum(pNtk), fForward? "Forward " : "Backward", Flow, Vec_PtrSize(vMinCut) ); PRT( "Time", clock() - clk ); + } // Abc_NtkMaxFlowPrintCut( vMinCut ); return vMinCut; @@ -377,6 +380,15 @@ int Abc_NtkMaxFlowVerifyCut( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMinCut, int fForward return 0; } } +/* + { + // count the volume of the cut + int Counter = 0; + Abc_NtkForEachObj( pNtk, pObj, i ) + Counter += Abc_NodeIsTravIdCurrent( pObj ); + printf( "Volume = %d.\n", Counter ); + } +*/ return 1; } diff --git a/src/opt/ret/retFwd.c b/src/opt/ret/retFwd.c deleted file mode 100644 index c33abc30..00000000 --- a/src/opt/ret/retFwd.c +++ /dev/null @@ -1,65 +0,0 @@ -/**CFile**************************************************************** - - FileName [retFwd.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Retiming package.] - - Synopsis [Most forward retiming.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - Oct 31, 2006.] - - Revision [$Id: retFwd.c,v 1.00 2006/10/31 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "retInt.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkRetimeForward( Abc_Ntk_t * pNtk, int fVerbose ) -{ - printf( "Not implemented.\n" ); - return 0; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/opt/ret/retIncrem.c b/src/opt/ret/retIncrem.c new file mode 100644 index 00000000..d2ad6a72 --- /dev/null +++ b/src/opt/ret/retIncrem.c @@ -0,0 +1,460 @@ +/**CFile**************************************************************** + + FileName [retIncrem.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Retiming package.] + + Synopsis [Incremental retiming in one direction.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - Oct 31, 2006.] + + Revision [$Id: retIncrem.c,v 1.00 2006/10/31 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "retInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static st_table * Abc_NtkRetimePrepareLatches( Abc_Ntk_t * pNtk ); +static int Abc_NtkRetimeFinalizeLatches( Abc_Ntk_t * pNtk, st_table * tLatches, int nIdMaxStart ); +static int Abc_NtkRetimeOneWay( Abc_Ntk_t * pNtk, int fForward, int fVerbose ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Performs retiming in one direction.] + + Description [Currently does not retime over black boxes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRetimeIncremental( Abc_Ntk_t * pNtk, int fForward, int fMinDelay, int fVerbose ) +{ + Abc_Ntk_t * pNtkCopy = NULL; + Vec_Ptr_t * vBoxes; + st_table * tLatches; + int nLatches = Abc_NtkLatchNum(pNtk); + int nIdMaxStart = Abc_NtkObjNumMax(pNtk); + int RetValue, nIterLimit; + if ( Abc_NtkNodeNum(pNtk) == 0 ) + return 0; + // reorder CI/CO/latch inputs + Abc_NtkOrderCisCos( pNtk ); + if ( fMinDelay ) + { + nIterLimit = 2 * Abc_NtkGetLevelNum(pNtk); + pNtkCopy = Abc_NtkDup( pNtk ); + tLatches = Abc_NtkRetimePrepareLatches( pNtkCopy ); + st_free_table( tLatches ); + } + // collect latches and remove CIs/COs + tLatches = Abc_NtkRetimePrepareLatches( pNtk ); + // save boxes + vBoxes = pNtk->vBoxes; pNtk->vBoxes = NULL; + // perform the retiming + if ( fMinDelay ) + Abc_NtkRetimeMinDelay( pNtk, pNtkCopy, nIterLimit, fForward, fVerbose ); + else + Abc_NtkRetimeOneWay( pNtk, fForward, fVerbose ); + if ( fMinDelay ) + Abc_NtkDelete( pNtkCopy ); + // share the latches + Abc_NtkRetimeShareLatches( pNtk ); + // restore boxes + pNtk->vBoxes = vBoxes; + // finalize the latches + RetValue = Abc_NtkRetimeFinalizeLatches( pNtk, tLatches, nIdMaxStart ); + st_free_table( tLatches ); + if ( RetValue == 0 ) + return 0; + // fix the COs + Abc_NtkLogicMakeSimpleCos( pNtk, 0 ); + // check for correctness + if ( !Abc_NtkCheck( pNtk ) ) + fprintf( stdout, "Abc_NtkRetimeForward(): Network check has failed.\n" ); + // return the number of latches saved + return nLatches - Abc_NtkLatchNum(pNtk); +} + +/**Function************************************************************* + + Synopsis [Prepares the network for retiming.] + + Description [Hash latches into their number in the original network.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +st_table * Abc_NtkRetimePrepareLatches( Abc_Ntk_t * pNtk ) +{ + st_table * tLatches; + Abc_Obj_t * pLatch, * pLatchIn, * pLatchOut, * pFanin; + int i, nOffSet = Abc_NtkBoxNum(pNtk) - Abc_NtkLatchNum(pNtk); + // collect latches and remove CIs/COs + tLatches = st_init_table( st_ptrcmp, st_ptrhash ); + Abc_NtkForEachLatch( pNtk, pLatch, i ) + { + // map latch into its true number + st_insert( tLatches, (void *)pLatch, (void *)(i-nOffSet) ); + // disconnect LI + pLatchIn = Abc_ObjFanin0(pLatch); + pFanin = Abc_ObjFanin0(pLatchIn); + Abc_ObjTransferFanout( pLatchIn, pFanin ); + Abc_ObjDeleteFanin( pLatchIn, pFanin ); + // disconnect LO + pLatchOut = Abc_ObjFanout0(pLatch); + pFanin = Abc_ObjFanin0(pLatchOut); + Abc_ObjTransferFanout( pLatchOut, pFanin ); + Abc_ObjDeleteFanin( pLatchOut, pFanin ); + } + return tLatches; +} + +/**Function************************************************************* + + Synopsis [Finalizes the latches after retiming.] + + Description [Reuses the LIs/LOs for old latches.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRetimeFinalizeLatches( Abc_Ntk_t * pNtk, st_table * tLatches, int nIdMaxStart ) +{ + Vec_Ptr_t * vCisOld, * vCosOld, * vBoxesOld, * vCisNew, * vCosNew, * vBoxesNew; + Abc_Obj_t * pObj, * pLatch, * pLatchIn, * pLatchOut; + int i, Index; + // create new arrays + vCisOld = pNtk->vCis; pNtk->vCis = NULL; vCisNew = Vec_PtrAlloc( 100 ); + vCosOld = pNtk->vCos; pNtk->vCos = NULL; vCosNew = Vec_PtrAlloc( 100 ); + vBoxesOld = pNtk->vBoxes; pNtk->vBoxes = NULL; vBoxesNew = Vec_PtrAlloc( 100 ); + // copy boxes and their CIs/COs + Vec_PtrForEachEntryStop( vCisOld, pObj, i, Vec_PtrSize(vCisOld) - st_count(tLatches) ) + Vec_PtrPush( vCisNew, pObj ); + Vec_PtrForEachEntryStop( vCosOld, pObj, i, Vec_PtrSize(vCosOld) - st_count(tLatches) ) + Vec_PtrPush( vCosNew, pObj ); + Vec_PtrForEachEntryStop( vBoxesOld, pObj, i, Vec_PtrSize(vBoxesOld) - st_count(tLatches) ) + Vec_PtrPush( vBoxesNew, pObj ); + // go through the latches + Abc_NtkForEachObj( pNtk, pLatch, i ) + { + if ( !Abc_ObjIsLatch(pLatch) ) + continue; + if ( Abc_ObjId(pLatch) >= (unsigned)nIdMaxStart ) + { + // this is a new latch + pLatchIn = Abc_NtkCreateBi(pNtk); + pLatchOut = Abc_NtkCreateBo(pNtk); + Abc_ObjAssignName( pLatchIn, Abc_ObjName(pLatchIn), NULL ); + Abc_ObjAssignName( pLatchOut, Abc_ObjName(pLatchOut), NULL ); + } + else + { + // this is an old latch + // get its number in the original order + if ( !st_lookup( tLatches, (char *)pLatch, (char **)&Index ) ) + { + printf( "Abc_NtkRetimeFinalizeLatches(): Internal error.\n" ); + return 0; + } + assert( pLatch == Vec_PtrEntry(vBoxesOld, Vec_PtrSize(vBoxesOld) - st_count(tLatches) + Index) ); + // reconnect with the old LIs/LOs + pLatchIn = Vec_PtrEntry( vCosOld, Vec_PtrSize(vCosOld) - st_count(tLatches) + Index ); + pLatchOut = Vec_PtrEntry( vCisOld, Vec_PtrSize(vCisOld) - st_count(tLatches) + Index ); + } + // connect + Abc_ObjAddFanin( pLatchIn, Abc_ObjFanin0(pLatch) ); + Abc_ObjPatchFanin( pLatch, Abc_ObjFanin0(pLatch), pLatchIn ); + Abc_ObjTransferFanout( pLatch, pLatchOut ); + Abc_ObjAddFanin( pLatchOut, pLatch ); + // add to the arrays + Vec_PtrPush( vCisNew, pLatchOut ); + Vec_PtrPush( vCosNew, pLatchIn ); + Vec_PtrPush( vBoxesNew, pLatch ); + } + // free useless Cis/Cos + Vec_PtrForEachEntry( vCisOld, pObj, i ) + if ( !Abc_ObjIsPi(pObj) && Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 ) + Abc_NtkDeleteObj(pObj); + Vec_PtrForEachEntry( vCosOld, pObj, i ) + if ( !Abc_ObjIsPo(pObj) && Abc_ObjFaninNum(pObj) == 0 && Abc_ObjFanoutNum(pObj) == 0 ) + Abc_NtkDeleteObj(pObj); + // set the new arrays + pNtk->vCis = vCisNew; Vec_PtrFree( vCisOld ); + pNtk->vCos = vCosNew; Vec_PtrFree( vCosOld ); + pNtk->vBoxes = vBoxesNew; Vec_PtrFree( vBoxesOld ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Performs retiming one way, forward or backward.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRetimeOneWay( Abc_Ntk_t * pNtk, int fForward, int fVerbose ) +{ + Abc_Ntk_t * pNtkNew; + Vec_Int_t * vValues; + Abc_Obj_t * pObj; + int i, fChanges, nTotalMoves = 0, nTotalMovesLimit = 5000; + if ( fForward ) + Abc_NtkRetimeTranferToCopy( pNtk ); + else + { + // save initial values of the latches + vValues = Abc_NtkRetimeCollectLatchValues( pNtk ); + // start the network for initial value computation + pNtkNew = Abc_NtkRetimeBackwardInitialStart( pNtk ); + } + // try to move latches forward whenever possible + do { + fChanges = 0; + Abc_NtkForEachObj( pNtk, pObj, i ) + { + if ( !Abc_ObjIsNode(pObj) ) + continue; + if ( Abc_NtkRetimeNodeIsEnabled( pObj, fForward ) ) + { + Abc_NtkRetimeNode( pObj, fForward, 1 ); + fChanges = 1; + nTotalMoves++; + if ( nTotalMoves >= nTotalMovesLimit ) + { + printf( "Stopped after %d latch moves.\n", nTotalMoves ); + break; + } + } + } + } while ( fChanges && nTotalMoves < nTotalMovesLimit ); + // transfer the initial state back to the latches + if ( fForward ) + Abc_NtkRetimeTranferFromCopy( pNtk ); + else + { + Abc_NtkRetimeBackwardInitialFinish( pNtk, pNtkNew, vValues, fVerbose ); + Abc_NtkDelete( pNtkNew ); + Vec_IntFree( vValues ); + } + return 0; +} + + +/**Function************************************************************* + + Synopsis [Returns 1 if retiming forward/backward is possible.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRetimeNodeIsEnabled( Abc_Obj_t * pObj, int fForward ) +{ + Abc_Obj_t * pNext; + int i; + assert( Abc_ObjIsNode(pObj) ); + if ( fForward ) + { + Abc_ObjForEachFanin( pObj, pNext, i ) + if ( !Abc_ObjIsLatch(pNext) ) + return 0; + } + else + { + Abc_ObjForEachFanout( pObj, pNext, i ) + if ( !Abc_ObjIsLatch(pNext) ) + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Retimes the node backward or forward.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkRetimeNode( Abc_Obj_t * pObj, int fForward, int fInitial ) +{ + Abc_Ntk_t * pNtkNew = NULL; + Vec_Ptr_t * vNodes; + Abc_Obj_t * pNext, * pLatch; + int i; + vNodes = Vec_PtrAlloc( 10 ); + if ( fForward ) + { + // compute the initial value + if ( fInitial ) + pObj->pCopy = (void *)Abc_ObjSopSimulate( pObj ); + // collect fanins + Abc_NodeCollectFanins( pObj, vNodes ); + // make the node point to the fanins fanins + Vec_PtrForEachEntry( vNodes, pNext, i ) + { + assert( Abc_ObjIsLatch(pNext) ); + Abc_ObjPatchFanin( pObj, pNext, Abc_ObjFanin0(pNext) ); + if ( Abc_ObjFanoutNum(pNext) == 0 ) + Abc_NtkDeleteObj(pNext); + } + // add a new latch on top + pNext = Abc_NtkCreateLatch(pObj->pNtk); + Abc_ObjTransferFanout( pObj, pNext ); + Abc_ObjAddFanin( pNext, pObj ); + // set the initial value + if ( fInitial ) + pNext->pCopy = pObj->pCopy; + } + else + { + // compute the initial value + if ( fInitial ) + { + pNtkNew = Abc_ObjFanout0(pObj)->pCopy->pNtk; + Abc_NtkDupObj( pNtkNew, pObj, 0 ); + Abc_ObjForEachFanout( pObj, pNext, i ) + { + assert( Abc_ObjFaninNum(pNext->pCopy) == 0 ); + Abc_ObjAddFanin( pNext->pCopy, pObj->pCopy ); + } + } + // collect fanouts + Abc_NodeCollectFanouts( pObj, vNodes ); + // make the fanouts fanouts point to the node + Vec_PtrForEachEntry( vNodes, pNext, i ) + { + assert( Abc_ObjIsLatch(pNext) ); + Abc_ObjTransferFanout( pNext, pObj ); + Abc_NtkDeleteObj( pNext ); + } + // add new latches to the fanins + Abc_ObjForEachFanin( pObj, pNext, i ) + { + pLatch = Abc_NtkCreateLatch(pObj->pNtk); + Abc_ObjPatchFanin( pObj, pNext, pLatch ); + Abc_ObjAddFanin( pLatch, pNext ); + // create buffer isomorphic to this latch + if ( fInitial ) + { + pLatch->pCopy = Abc_NtkCreateNodeBuf( pNtkNew, NULL ); + Abc_ObjAddFanin( pObj->pCopy, pLatch->pCopy ); + } + } + } + Vec_PtrFree( vNodes ); +} + +/**Function************************************************************* + + Synopsis [Returns the number of compatible fanout latches.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRetimeCheckCompatibleLatchFanouts( Abc_Obj_t * pObj ) +{ + Abc_Obj_t * pFanout; + int i, nLatches = 0, Init = -1; + Abc_ObjForEachFanout( pObj, pFanout, i ) + { + if ( !Abc_ObjIsLatch(pFanout) ) + continue; + if ( Init == -1 ) + { + Init = (int)pObj->pData; + nLatches++; + } + else if ( Init == (int)pObj->pData ) + nLatches++; + } + return nLatches; +} + +/**Function************************************************************* + + Synopsis [Retimes the node backward or forward.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkRetimeShareLatches( Abc_Ntk_t * pNtk ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pFanin, * pLatch, * pLatchTop, * pLatchCur; + int i, k; + vNodes = Vec_PtrAlloc( 10 ); + // consider latch fanins + Abc_NtkForEachObj( pNtk, pLatch, i ) + { + if ( !Abc_ObjIsLatch(pLatch) ) + continue; + pFanin = Abc_ObjFanin0(pLatch); + if ( Abc_NtkRetimeCheckCompatibleLatchFanouts(pFanin) <= 1 ) + continue; + // get the first latch + Abc_ObjForEachFanout( pFanin, pLatchTop, k ) + if ( Abc_ObjIsLatch(pLatchTop) ) + break; + assert( Abc_ObjIsLatch(pLatchTop) ); + // redirect compatible fanout latches to the first latch + Abc_NodeCollectFanouts( pFanin, vNodes ); + Vec_PtrForEachEntry( vNodes, pLatchCur, k ) + { + if ( pLatchCur == pLatchTop ) + continue; + if ( !Abc_ObjIsLatch(pLatchCur) ) + continue; + if ( pLatchCur->pData != pLatchTop->pData ) + continue; + // redirect the fanouts + Abc_ObjTransferFanout( pLatchCur, pLatchTop ); + Abc_NtkDeleteObj(pLatchCur); + } + } + Vec_PtrFree( vNodes ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/ret/retInit.c b/src/opt/ret/retInit.c index 169d5a63..3eb80da1 100644 --- a/src/opt/ret/retInit.c +++ b/src/opt/ret/retInit.c @@ -1,12 +1,12 @@ /**CFile**************************************************************** - FileName [ret_.c] + FileName [retInit.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Retiming package.] - Synopsis [] + Synopsis [Initial state computation for backward retiming.] Author [Alan Mishchenko] @@ -14,7 +14,7 @@ Date [Ver. 1.0. Started - Oct 31, 2006.] - Revision [$Id: ret_.c,v 1.00 2006/10/31 00:00:00 alanmi Exp $] + Revision [$Id: retInit.c,v 1.00 2006/10/31 00:00:00 alanmi Exp $] ***********************************************************************/ @@ -24,6 +24,8 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static int Abc_NtkRetimeVerifyModel( Abc_Ntk_t * pNtkCone, Vec_Int_t * vValues, int * pModel ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -39,29 +41,306 @@ SeeAlso [] ***********************************************************************/ -void Abc_NtkRetimeInitialValues( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, int fVerbose ) +Vec_Int_t * Abc_NtkRetimeInitialValues( Abc_Ntk_t * pNtkCone, Vec_Int_t * vValues, int fVerbose ) { - Abc_Obj_t * pLatch; - int * pModel, RetValue, clk, i; + Vec_Int_t * vSolution; + Abc_Ntk_t * pNtkMiter, * pNtkLogic; + int RetValue, clk; + if ( pNtkCone == NULL ) + return Vec_IntDup( vValues ); + // convert the target network to AIG + pNtkLogic = Abc_NtkDup( pNtkCone ); + Abc_NtkLogicToAig( pNtkLogic ); + // get the miter + pNtkMiter = Abc_NtkCreateTarget( pNtkLogic, pNtkLogic->vCos, vValues ); if ( fVerbose ) - printf( "The number of ANDs in the AIG = %5d.\n", Abc_NtkNodeNum(pNtkMiter) ); + printf( "The miter for initial state computation has %d AIG nodes. ", Abc_NtkNodeNum(pNtkMiter) ); // solve the miter -clk = clock(); + clk = clock(); RetValue = Abc_NtkMiterSat( pNtkMiter, (sint64)500000, (sint64)50000000, 0, 0, NULL, NULL ); -if ( fVerbose && clock() - clk > 100 ) -{ -PRT( "SAT solving time", clock() - clk ); -} + if ( fVerbose ) + { PRT( "SAT solving time", clock() - clk ); } // analyze the result if ( RetValue == 1 ) printf( "Abc_NtkRetimeInitialValues(): The problem is unsatisfiable. DC latch values are used.\n" ); else if ( RetValue == -1 ) printf( "Abc_NtkRetimeInitialValues(): The SAT problem timed out. DC latch values are used.\n" ); + else if ( !Abc_NtkRetimeVerifyModel( pNtkCone, vValues, pNtkMiter->pModel ) ) + printf( "Abc_NtkRetimeInitialValues(): The computed counter-example is incorrect.\n" ); // set the values of the latches - pModel = pNtkMiter->pModel; pNtkMiter->pModel = NULL; - Abc_NtkForEachLatch( pNtk, pLatch, i ) - pLatch->pData = (void *)(pModel? (pModel[i]? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC); - FREE( pModel ); + vSolution = RetValue? NULL : Vec_IntAllocArray( pNtkMiter->pModel, Abc_NtkPiNum(pNtkLogic) ); + pNtkMiter->pModel = NULL; + Abc_NtkDelete( pNtkMiter ); + Abc_NtkDelete( pNtkLogic ); + return vSolution; +} + +/**Function************************************************************* + + Synopsis [Computes the results of simulating one node.] + + Description [Assumes that fanins have pCopy set to the input values.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_ObjSopSimulate( Abc_Obj_t * pObj ) +{ + char * pCube, * pSop = pObj->pData; + int nVars, Value, v, ResOr, ResAnd, ResVar; + assert( pSop && !Abc_SopIsExorType(pSop) ); + // simulate the SOP of the node + ResOr = 0; + nVars = Abc_SopGetVarNum(pSop); + Abc_SopForEachCube( pSop, nVars, pCube ) + { + ResAnd = 1; + Abc_CubeForEachVar( pCube, Value, v ) + { + if ( Value == '0' ) + ResVar = 1 ^ ((int)Abc_ObjFanin(pObj, v)->pCopy); + else if ( Value == '1' ) + ResVar = (int)Abc_ObjFanin(pObj, v)->pCopy; + else + continue; + ResAnd &= ResVar; + } + ResOr |= ResAnd; + } + // complement the result if necessary + if ( !Abc_SopGetPhase(pSop) ) + ResOr ^= 1; + return ResOr; +} + +/**Function************************************************************* + + Synopsis [Verifies the counter-example.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRetimeVerifyModel( Abc_Ntk_t * pNtkCone, Vec_Int_t * vValues, int * pModel ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pObj; + int i, Counter = 0; + assert( Abc_NtkIsSopLogic(pNtkCone) ); + // set the PIs + Abc_NtkForEachPi( pNtkCone, pObj, i ) + pObj->pCopy = (void *)pModel[i]; + // simulate the internal nodes + vNodes = Abc_NtkDfs( pNtkCone, 0 ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + pObj->pCopy = (void *)Abc_ObjSopSimulate( pObj ); + Vec_PtrFree( vNodes ); + // compare the outputs + Abc_NtkForEachPo( pNtkCone, pObj, i ) + pObj->pCopy = Abc_ObjFanin0(pObj)->pCopy; + Abc_NtkForEachPo( pNtkCone, pObj, i ) + Counter += (Vec_IntEntry(vValues, i) != (int)pObj->pCopy); + if ( Counter > 0 ) + printf( "%d outputs (out of %d) have a value mismatch.\n", Counter, Abc_NtkPoNum(pNtkCone) ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Transfer latch initial values to pCopy.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkRetimeTranferToCopy( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + int i; + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( Abc_ObjIsLatch(pObj) ) + pObj->pCopy = (void *)Abc_LatchIsInit1(pObj); +} + +/**Function************************************************************* + + Synopsis [Transfer latch initial values from pCopy.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkRetimeTranferFromCopy( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + int i; + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( Abc_ObjIsLatch(pObj) ) + pObj->pData = (void *)(pObj->pCopy? ABC_INIT_ONE : ABC_INIT_ZERO); +} + +/**Function************************************************************* + + Synopsis [Transfer latch initial values to pCopy.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Abc_NtkRetimeCollectLatchValues( Abc_Ntk_t * pNtk ) +{ + Vec_Int_t * vValues; + Abc_Obj_t * pObj; + int i; + vValues = Vec_IntAlloc( Abc_NtkLatchNum(pNtk) ); + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( Abc_ObjIsLatch(pObj) ) + Vec_IntPush( vValues, Abc_LatchIsInit1(pObj) ); + return vValues; +} + +/**Function************************************************************* + + Synopsis [Transfer latch initial values from pCopy.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkRetimeInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues ) +{ + Abc_Obj_t * pObj; + int i, Counter = 0; + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( Abc_ObjIsLatch(pObj) ) + pObj->pCopy = (void *)Counter++; + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( Abc_ObjIsLatch(pObj) ) + pObj->pData = (void *)(vValues? (Vec_IntEntry(vValues,(int)pObj->pCopy)? ABC_INIT_ONE : ABC_INIT_ZERO) : ABC_INIT_DC); +} + +/**Function************************************************************* + + Synopsis [Transfer latch initial values to pCopy.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkRetimeBackwardInitialStart( Abc_Ntk_t * pNtk ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj; + int i; + // create the network used for the initial state computation + pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP, 1 ); + // create POs corresponding to the initial values + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( Abc_ObjIsLatch(pObj) ) + pObj->pCopy = Abc_NtkCreatePo(pNtkNew); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Transfer latch initial values to pCopy.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkRetimeBackwardInitialFinish( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, Vec_Int_t * vValuesOld, int fVerbose ) +{ + Vec_Int_t * vValuesNew; + Abc_Obj_t * pObj; + int i; + // create PIs corresponding to the initial values + Abc_NtkForEachObj( pNtk, pObj, i ) + if ( Abc_ObjIsLatch(pObj) ) + Abc_ObjAddFanin( pObj->pCopy, Abc_NtkCreatePi(pNtkNew) ); + pObj = Abc_NtkPo(pNtkNew, 0); + // assign dummy node names + Abc_NtkAddDummyPiNames( pNtkNew ); + Abc_NtkAddDummyPoNames( pNtkNew ); + // check the network + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkRetimeBackwardInitialFinish(): Network check has failed.\n" ); + // derive new initial values + vValuesNew = Abc_NtkRetimeInitialValues( pNtkNew, vValuesOld, fVerbose ); + // insert new initial values + Abc_NtkRetimeInsertLatchValues( pNtk, vValuesNew ); + if ( vValuesNew ) Vec_IntFree( vValuesNew ); +} + + +/**Function************************************************************* + + Synopsis [Cycles the circuit to create a new initial state.] + + Description [Simulates the circuit with random input for the given + number of timeframes to get a better initial state.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkCycleInitStateSop( Abc_Ntk_t * pNtk, int nFrames, int fVerbose ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pObj; + int i, f; + assert( Abc_NtkIsSopLogic(pNtk) ); + srand( 0x12341234 ); + // initialize the values + Abc_NtkForEachPi( pNtk, pObj, i ) + pObj->pCopy = (void *)(rand() & 1); + Abc_NtkForEachLatch( pNtk, pObj, i ) + pObj->pCopy = (void *)Abc_LatchIsInit1(pObj); + // simulate for the given number of timeframes + vNodes = Abc_NtkDfs( pNtk, 0 ); + for ( f = 0; f < nFrames; f++ ) + { + // simulate internal nodes + Vec_PtrForEachEntry( vNodes, pObj, i ) + pObj->pCopy = (void *)Abc_ObjSopSimulate( pObj ); + // bring the results to the COs + Abc_NtkForEachCo( pNtk, pObj, i ) + pObj->pCopy = Abc_ObjFanin0(pObj)->pCopy; + // assign PI values + Abc_NtkForEachPi( pNtk, pObj, i ) + pObj->pCopy = (void *)(rand() & 1); + // transfer the latch values + Abc_NtkForEachLatch( pNtk, pObj, i ) + Abc_ObjFanout0(pObj)->pCopy = Abc_ObjFanin0(pObj)->pCopy; + } + Vec_PtrFree( vNodes ); + // set the final values + Abc_NtkForEachLatch( pNtk, pObj, i ) + pObj->pData = (void *)(Abc_ObjFanout0(pObj)->pCopy ? ABC_INIT_ONE : ABC_INIT_ZERO); } //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/ret/retInt.h b/src/opt/ret/retInt.h index 2cb465fa..9b3aa00a 100644 --- a/src/opt/ret/retInt.h +++ b/src/opt/ret/retInt.h @@ -44,20 +44,28 @@ //////////////////////////////////////////////////////////////////////// /*=== retArea.c ========================================================*/ -extern int Abc_NtkRetimeMinArea( Abc_Ntk_t * pNtk, int fVerbose ); -/*=== retBwd.c ========================================================*/ -extern int Abc_NtkRetimeBackward( Abc_Ntk_t * pNtk, int fVerbose ); +extern int Abc_NtkRetimeMinArea( Abc_Ntk_t * pNtk, int fForwardOnly, int fBackwardOnly, int fVerbose ); /*=== retCore.c ========================================================*/ -extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fVerbose ); +extern int Abc_NtkRetime( Abc_Ntk_t * pNtk, int Mode, int fForwardOnly, int fBackwardOnly, int fVerbose ); /*=== retDelay.c ========================================================*/ -extern int Abc_NtkRetimeMinDelay( Abc_Ntk_t * pNtk, int fVerbose ); +extern int Abc_NtkRetimeMinDelay( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkCopy, int nIterLimit, int fForward, int fVerbose ); +/*=== retDirect.c ========================================================*/ +extern int Abc_NtkRetimeIncremental( Abc_Ntk_t * pNtk, int fForward, int fMinDelay, int fVerbose ); +extern void Abc_NtkRetimeShareLatches( Abc_Ntk_t * pNtk ); +extern int Abc_NtkRetimeNodeIsEnabled( Abc_Obj_t * pObj, int fForward ); +extern void Abc_NtkRetimeNode( Abc_Obj_t * pObj, int fForward, int fInitial ); /*=== retFlow.c ========================================================*/ extern void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk ); extern Vec_Ptr_t * Abc_NtkMaxFlow( Abc_Ntk_t * pNtk, int fForward, int fVerbose ); -/*=== retFwd.c ========================================================*/ -extern int Abc_NtkRetimeForward( Abc_Ntk_t * pNtk, int fVerbose ); /*=== retInit.c ========================================================*/ -extern void Abc_NtkRetimeInitialValues( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkMiter, int fVerbose ); +extern Vec_Int_t * Abc_NtkRetimeInitialValues( Abc_Ntk_t * pNtkSat, Vec_Int_t * vValues, int fVerbose ); +extern int Abc_ObjSopSimulate( Abc_Obj_t * pObj ); +extern void Abc_NtkRetimeTranferToCopy( Abc_Ntk_t * pNtk ); +extern void Abc_NtkRetimeTranferFromCopy( Abc_Ntk_t * pNtk ); +extern Vec_Int_t * Abc_NtkRetimeCollectLatchValues( Abc_Ntk_t * pNtk ); +extern void Abc_NtkRetimeInsertLatchValues( Abc_Ntk_t * pNtk, Vec_Int_t * vValues ); +extern Abc_Ntk_t * Abc_NtkRetimeBackwardInitialStart( Abc_Ntk_t * pNtk ); +extern void Abc_NtkRetimeBackwardInitialFinish( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew, Vec_Int_t * vValuesOld, int fVerbose ); #endif diff --git a/src/temp/aig-alan.tar.gz b/src/temp/aig-alan.tar.gz Binary files differdeleted file mode 100644 index b61827ad..00000000 --- a/src/temp/aig-alan.tar.gz +++ /dev/null diff --git a/src/temp/esop/esop.h b/src/temp/esop/esop.h deleted file mode 100644 index 5f95f371..00000000 --- a/src/temp/esop/esop.h +++ /dev/null @@ -1,723 +0,0 @@ -/**CFile**************************************************************** - - FileName [esop.h] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Cover manipulation package.] - - Synopsis [Internal declarations.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: esop.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef __ESOP_H__ -#define __ESOP_H__ - -#ifdef __cplusplus -extern "C" { -#endif - -#include <stdio.h> -#include "vec.h" -#include "mem.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Esop_Man_t_ Esop_Man_t; -typedef struct Esop_Cube_t_ Esop_Cube_t; -typedef struct Mem_Fixed_t_ Mem_Fixed_t; - -struct Esop_Man_t_ -{ - int nVars; // the number of vars - int nWords; // the number of words - Mem_Fixed_t * pMemMan1; // memory manager for cubes - Mem_Fixed_t * pMemMan2; // memory manager for cubes - Mem_Fixed_t * pMemMan4; // memory manager for cubes - Mem_Fixed_t * pMemMan8; // memory manager for cubes - // temporary cubes - Esop_Cube_t * pOne0; // tautology cube - Esop_Cube_t * pOne1; // tautology cube - Esop_Cube_t * pTriv0; // trivial cube - Esop_Cube_t * pTriv1; // trivial cube - Esop_Cube_t * pTemp; // cube for computing the distance - Esop_Cube_t * pBubble; // cube used as a separator - // temporary storage for the new cover - int nCubes; // the number of cubes - Esop_Cube_t ** ppStore; // storage for cubes by number of literals -}; - -struct Esop_Cube_t_ -{ - Esop_Cube_t * pNext; // the pointer to the next cube in the cover - unsigned nVars : 10; // the number of variables - unsigned nWords : 12; // the number of machine words - unsigned nLits : 10; // the number of literals in the cube - unsigned uData[1]; // the bit-data for the cube -}; - -#define ALLOC(type, num) ((type *) malloc(sizeof(type) * (num))) -#define FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0) -#define REALLOC(type, obj, num) \ - ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \ - ((type *) malloc(sizeof(type) * (num)))) - -// iterators through the entries in the linked lists of cubes -#define Esop_CoverForEachCube( pCover, pCube ) \ - for ( pCube = pCover; \ - pCube; \ - pCube = pCube->pNext ) -#define Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 ) \ - for ( pCube = pCover, \ - pCube2 = pCube? pCube->pNext: NULL; \ - pCube; \ - pCube = pCube2, \ - pCube2 = pCube? pCube->pNext: NULL ) -#define Esop_CoverForEachCubePrev( pCover, pCube, ppPrev ) \ - for ( pCube = pCover, \ - ppPrev = &(pCover); \ - pCube; \ - ppPrev = &pCube->pNext, \ - pCube = pCube->pNext ) - - -// macros to get hold of bits and values in the cubes -static inline int Esop_CubeHasBit( Esop_Cube_t * p, int i ) { return (p->uData[i >> 5] & (1<<(i & 31))) > 0; } -static inline void Esop_CubeSetBit( Esop_Cube_t * p, int i ) { p->uData[i >> 5] |= (1<<(i & 31)); } -static inline void Esop_CubeXorBit( Esop_Cube_t * p, int i ) { p->uData[i >> 5] ^= (1<<(i & 31)); } -static inline int Esop_CubeGetVar( Esop_Cube_t * p, int Var ) { return 3 & (p->uData[(Var<<1)>>5] >> ((Var<<1) & 31)); } -static inline void Esop_CubeXorVar( Esop_Cube_t * p, int Var, int Value ) { p->uData[(Var<<1)>>5] ^= (Value<<((Var<<1) & 31)); } -static inline int Esop_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); } - -/*=== esopMem.c ===========================================================*/ -extern Mem_Fixed_t * Mem_FixedStart( int nEntrySize ); -extern void Mem_FixedStop( Mem_Fixed_t * p, int fVerbose ); -extern char * Mem_FixedEntryFetch( Mem_Fixed_t * p ); -extern void Mem_FixedEntryRecycle( Mem_Fixed_t * p, char * pEntry ); -extern void Mem_FixedRestart( Mem_Fixed_t * p ); -extern int Mem_FixedReadMemUsage( Mem_Fixed_t * p ); -/*=== esopMin.c ===========================================================*/ -extern void Esop_EsopMinimize( Esop_Man_t * p ); -extern void Esop_EsopAddCube( Esop_Man_t * p, Esop_Cube_t * pCube ); -/*=== esopMan.c ===========================================================*/ -extern Esop_Man_t * Esop_ManAlloc( int nVars ); -extern void Esop_ManClean( Esop_Man_t * p, int nSupp ); -extern void Esop_ManFree( Esop_Man_t * p ); -/*=== esopUtil.c ===========================================================*/ -extern void Esop_CubeWrite( FILE * pFile, Esop_Cube_t * pCube ); -extern void Esop_CoverWrite( FILE * pFile, Esop_Cube_t * pCover ); -extern void Esop_CoverWriteStore( FILE * pFile, Esop_Man_t * p ); -extern void Esop_CoverWriteFile( Esop_Cube_t * pCover, char * pName, int fEsop ); -extern void Esop_CoverCheck( Esop_Man_t * p ); -extern int Esop_CubeCheck( Esop_Cube_t * pCube ); -extern Esop_Cube_t * Esop_CoverCollect( Esop_Man_t * p, int nSuppSize ); -extern void Esop_CoverExpand( Esop_Man_t * p, Esop_Cube_t * pCover ); -extern int Esop_CoverSuppVarNum( Esop_Man_t * p, Esop_Cube_t * pCover ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Creates the cube.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Esop_Cube_t * Esop_CubeAlloc( Esop_Man_t * p ) -{ - Esop_Cube_t * pCube; - if ( p->nWords <= 1 ) - pCube = (Esop_Cube_t *)Mem_FixedEntryFetch( p->pMemMan1 ); - else if ( p->nWords <= 2 ) - pCube = (Esop_Cube_t *)Mem_FixedEntryFetch( p->pMemMan2 ); - else if ( p->nWords <= 4 ) - pCube = (Esop_Cube_t *)Mem_FixedEntryFetch( p->pMemMan4 ); - else if ( p->nWords <= 8 ) - pCube = (Esop_Cube_t *)Mem_FixedEntryFetch( p->pMemMan8 ); - pCube->pNext = NULL; - pCube->nVars = p->nVars; - pCube->nWords = p->nWords; - pCube->nLits = 0; - memset( pCube->uData, 0xff, sizeof(unsigned) * p->nWords ); - return pCube; -} - -/**Function************************************************************* - - Synopsis [Creates the cube representing elementary var.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Esop_Cube_t * Esop_CubeAllocVar( Esop_Man_t * p, int iVar, int fCompl ) -{ - Esop_Cube_t * pCube; - pCube = Esop_CubeAlloc( p ); - Esop_CubeXorBit( pCube, iVar*2+fCompl ); - pCube->nLits = 1; - return pCube; -} - -/**Function************************************************************* - - Synopsis [Creates the cube.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Esop_Cube_t * Esop_CubeDup( Esop_Man_t * p, Esop_Cube_t * pCopy ) -{ - Esop_Cube_t * pCube; - pCube = Esop_CubeAlloc( p ); - memcpy( pCube->uData, pCopy->uData, sizeof(unsigned) * p->nWords ); - pCube->nLits = pCopy->nLits; - return pCube; -} - -/**Function************************************************************* - - Synopsis [Recycles the cube.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Esop_CubeRecycle( Esop_Man_t * p, Esop_Cube_t * pCube ) -{ - if ( pCube->nWords <= 1 ) - Mem_FixedEntryRecycle( p->pMemMan1, (char *)pCube ); - else if ( pCube->nWords <= 2 ) - Mem_FixedEntryRecycle( p->pMemMan2, (char *)pCube ); - else if ( pCube->nWords <= 4 ) - Mem_FixedEntryRecycle( p->pMemMan4, (char *)pCube ); - else if ( pCube->nWords <= 8 ) - Mem_FixedEntryRecycle( p->pMemMan8, (char *)pCube ); -} - -/**Function************************************************************* - - Synopsis [Recycles the cube cover.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Esop_CoverRecycle( Esop_Man_t * p, Esop_Cube_t * pCover ) -{ - Esop_Cube_t * pCube, * pCube2; - if ( pCover == NULL ) - return; - if ( pCover->nWords <= 1 ) - Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 ) - Mem_FixedEntryRecycle( p->pMemMan1, (char *)pCube ); - else if ( pCover->nWords <= 2 ) - Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 ) - Mem_FixedEntryRecycle( p->pMemMan2, (char *)pCube ); - else if ( pCover->nWords <= 4 ) - Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 ) - Mem_FixedEntryRecycle( p->pMemMan4, (char *)pCube ); - else if ( pCover->nWords <= 8 ) - Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 ) - Mem_FixedEntryRecycle( p->pMemMan8, (char *)pCube ); -} - -/**Function************************************************************* - - Synopsis [Recycles the cube cover.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Esop_Cube_t * Esop_CoverDup( Esop_Man_t * p, Esop_Cube_t * pCover ) -{ - Esop_Cube_t * pCube, * pCubeNew; - Esop_Cube_t * pCoverNew = NULL, ** ppTail = &pCoverNew; - Esop_CoverForEachCube( pCover, pCube ) - { - pCubeNew = Esop_CubeDup( p, pCube ); - *ppTail = pCubeNew; - ppTail = &pCubeNew->pNext; - } - *ppTail = NULL; - return pCoverNew; -} - - -/**Function************************************************************* - - Synopsis [Counts the number of cubes in the cover.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Esop_CubeCountLits( Esop_Cube_t * pCube ) -{ - unsigned uData; - int Count = 0, i, w; - for ( w = 0; w < (int)pCube->nWords; w++ ) - { - uData = pCube->uData[w] ^ (pCube->uData[w] >> 1); - for ( i = 0; i < 32; i += 2 ) - if ( uData & (1 << i) ) - Count++; - } - return Count; -} - -/**Function************************************************************* - - Synopsis [Counts the number of cubes in the cover.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Esop_CubeGetLits( Esop_Cube_t * pCube, Vec_Int_t * vLits ) -{ - unsigned uData; - int i, w; - Vec_IntClear( vLits ); - for ( w = 0; w < (int)pCube->nWords; w++ ) - { - uData = pCube->uData[w] ^ (pCube->uData[w] >> 1); - for ( i = 0; i < 32; i += 2 ) - if ( uData & (1 << i) ) - Vec_IntPush( vLits, w*16 + i/2 ); - } -} - -/**Function************************************************************* - - Synopsis [Counts the number of cubes in the cover.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Esop_CoverCountCubes( Esop_Cube_t * pCover ) -{ - Esop_Cube_t * pCube; - int Count = 0; - Esop_CoverForEachCube( pCover, pCube ) - Count++; - return Count; -} - - -/**Function************************************************************* - - Synopsis [Checks if two cubes are disjoint.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Esop_CubesDisjoint( Esop_Cube_t * pCube0, Esop_Cube_t * pCube1 ) -{ - unsigned uData; - int i; - assert( pCube0->nVars == pCube1->nVars ); - for ( i = 0; i < (int)pCube0->nWords; i++ ) - { - uData = pCube0->uData[i] & pCube1->uData[i]; - uData = (uData | (uData >> 1)) & 0x55555555; - if ( uData != 0x55555555 ) - return 1; - } - return 0; -} - -/**Function************************************************************* - - Synopsis [Collects the disjoint variables of the two cubes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Esop_CoverGetDisjVars( Esop_Cube_t * pThis, Esop_Cube_t * pCube, Vec_Int_t * vVars ) -{ - unsigned uData; - int i, w; - Vec_IntClear( vVars ); - for ( w = 0; w < (int)pCube->nWords; w++ ) - { - uData = pThis->uData[w] & (pThis->uData[w] >> 1) & 0x55555555; - uData &= (pCube->uData[w] ^ (pCube->uData[w] >> 1)); - if ( uData == 0 ) - continue; - for ( i = 0; i < 32; i += 2 ) - if ( uData & (1 << i) ) - Vec_IntPush( vVars, w*16 + i/2 ); - } -} - -/**Function************************************************************* - - Synopsis [Checks if two cubes are disjoint.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Esop_CubesDistOne( Esop_Cube_t * pCube0, Esop_Cube_t * pCube1, Esop_Cube_t * pTemp ) -{ - unsigned uData; - int i, fFound = 0; - for ( i = 0; i < (int)pCube0->nWords; i++ ) - { - uData = pCube0->uData[i] ^ pCube1->uData[i]; - if ( uData == 0 ) - { - if ( pTemp ) pTemp->uData[i] = 0; - continue; - } - if ( fFound ) - return 0; - uData = (uData | (uData >> 1)) & 0x55555555; - if ( (uData & (uData-1)) > 0 ) // more than one 1 - return 0; - if ( pTemp ) pTemp->uData[i] = uData | (uData << 1); - fFound = 1; - } - if ( fFound == 0 ) - { - printf( "\n" ); - Esop_CubeWrite( stdout, pCube0 ); - Esop_CubeWrite( stdout, pCube1 ); - printf( "Error: Esop_CubesDistOne() looks at two equal cubes!\n" ); - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Checks if two cubes are disjoint.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Esop_CubesDistTwo( Esop_Cube_t * pCube0, Esop_Cube_t * pCube1, int * pVar0, int * pVar1 ) -{ - unsigned uData;//, uData2; - int i, k, Var0 = -1, Var1 = -1; - for ( i = 0; i < (int)pCube0->nWords; i++ ) - { - uData = pCube0->uData[i] ^ pCube1->uData[i]; - if ( uData == 0 ) - continue; - if ( Var0 >= 0 && Var1 >= 0 ) // more than two 1s - return 0; - uData = (uData | (uData >> 1)) & 0x55555555; - if ( (Var0 >= 0 || Var1 >= 0) && (uData & (uData-1)) > 0 ) - return 0; - for ( k = 0; k < 32; k += 2 ) - if ( uData & (1 << k) ) - { - if ( Var0 == -1 ) - Var0 = 16 * i + k/2; - else if ( Var1 == -1 ) - Var1 = 16 * i + k/2; - else - return 0; - } - /* - if ( Var0 >= 0 ) - { - uData &= 0xFFFF; - uData2 = (uData >> 16); - if ( uData && uData2 ) - return 0; - if ( uData ) - { - } - uData }= uData2; - uData &= 0x - } - */ - } - if ( Var0 >= 0 && Var1 >= 0 ) - { - *pVar0 = Var0; - *pVar1 = Var1; - return 1; - } - if ( Var0 == -1 || Var1 == -1 ) - { - printf( "\n" ); - Esop_CubeWrite( stdout, pCube0 ); - Esop_CubeWrite( stdout, pCube1 ); - printf( "Error: Esop_CubesDistTwo() looks at two equal cubes or dist1 cubes!\n" ); - } - return 0; -} - -/**Function************************************************************* - - Synopsis [Makes the produce of two cubes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Esop_Cube_t * Esop_CubesProduct( Esop_Man_t * p, Esop_Cube_t * pCube0, Esop_Cube_t * pCube1 ) -{ - Esop_Cube_t * pCube; - int i; - assert( pCube0->nVars == pCube1->nVars ); - pCube = Esop_CubeAlloc( p ); - for ( i = 0; i < p->nWords; i++ ) - pCube->uData[i] = pCube0->uData[i] & pCube1->uData[i]; - pCube->nLits = Esop_CubeCountLits( pCube ); - return pCube; -} - -/**Function************************************************************* - - Synopsis [Makes the produce of two cubes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Esop_Cube_t * Esop_CubesXor( Esop_Man_t * p, Esop_Cube_t * pCube0, Esop_Cube_t * pCube1 ) -{ - Esop_Cube_t * pCube; - int i; - assert( pCube0->nVars == pCube1->nVars ); - pCube = Esop_CubeAlloc( p ); - for ( i = 0; i < p->nWords; i++ ) - pCube->uData[i] = pCube0->uData[i] ^ pCube1->uData[i]; - pCube->nLits = Esop_CubeCountLits( pCube ); - return pCube; -} - -/**Function************************************************************* - - Synopsis [Makes the produce of two cubes.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Esop_CubesAreEqual( Esop_Cube_t * pCube0, Esop_Cube_t * pCube1 ) -{ - int i; - for ( i = 0; i < (int)pCube0->nWords; i++ ) - if ( pCube0->uData[i] != pCube1->uData[i] ) - return 0; - return 1; -} - -/**Function************************************************************* - - Synopsis [Returns 1 if pCube1 is contained in pCube0, bitwise.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Esop_CubeIsContained( Esop_Cube_t * pCube0, Esop_Cube_t * pCube1 ) -{ - int i; - for ( i = 0; i < (int)pCube0->nWords; i++ ) - if ( (pCube0->uData[i] & pCube1->uData[i]) != pCube1->uData[i] ) - return 0; - return 1; -} - -/**Function************************************************************* - - Synopsis [Transforms the cube into the result of merging.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Esop_CubesTransform( Esop_Cube_t * pCube, Esop_Cube_t * pDist, Esop_Cube_t * pMask ) -{ - int w; - for ( w = 0; w < (int)pCube->nWords; w++ ) - { - pCube->uData[w] = pCube->uData[w] ^ pDist->uData[w]; - pCube->uData[w] |= (pDist->uData[w] & ~pMask->uData[w]); - } -} - -/**Function************************************************************* - - Synopsis [Transforms the cube into the result of distance-1 merging.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Esop_CubesTransformOr( Esop_Cube_t * pCube, Esop_Cube_t * pDist ) -{ - int w; - for ( w = 0; w < (int)pCube->nWords; w++ ) - pCube->uData[w] |= pDist->uData[w]; -} - - - -/**Function************************************************************* - - Synopsis [Sorts the cover in the increasing number of literals.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Esop_CoverExpandRemoveEqual( Esop_Man_t * p, Esop_Cube_t * pCover ) -{ - Esop_Cube_t * pCube, * pCube2, * pThis; - if ( pCover == NULL ) - { - Esop_ManClean( p, p->nVars ); - return; - } - Esop_ManClean( p, pCover->nVars ); - Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 ) - { - // go through the linked list - Esop_CoverForEachCube( p->ppStore[pCube->nLits], pThis ) - if ( Esop_CubesAreEqual( pCube, pThis ) ) - { - Esop_CubeRecycle( p, pCube ); - break; - } - if ( pThis != NULL ) - continue; - pCube->pNext = p->ppStore[pCube->nLits]; - p->ppStore[pCube->nLits] = pCube; - p->nCubes++; - } -} - -/**Function************************************************************* - - Synopsis [Returns 1 if the given cube is contained in one of the cubes of the cover.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Esop_CoverContainsCube( Esop_Man_t * p, Esop_Cube_t * pCube ) -{ - Esop_Cube_t * pThis; - int i; -/* - // this cube cannot be equal to any cube - Esop_CoverForEachCube( p->ppStore[pCube->nLits], pThis ) - { - if ( Esop_CubesAreEqual( pCube, pThis ) ) - { - Esop_CubeWrite( stdout, pCube ); - assert( 0 ); - } - } -*/ - // try to find a containing cube - for ( i = 0; i <= (int)pCube->nLits; i++ ) - Esop_CoverForEachCube( p->ppStore[i], pThis ) - { - // skip the bubble - if ( pThis != p->pBubble && Esop_CubeIsContained( pThis, pCube ) ) - return 1; - } - return 0; -} - -#ifdef __cplusplus -} -#endif - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/temp/esop/esopMan.c b/src/temp/esop/esopMan.c deleted file mode 100644 index 5c411349..00000000 --- a/src/temp/esop/esopMan.c +++ /dev/null @@ -1,117 +0,0 @@ -/**CFile**************************************************************** - - FileName [esopMan.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Cover manipulation package.] - - Synopsis [SOP manipulation.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: esopMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "esop.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Starts the minimization manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Esop_Man_t * Esop_ManAlloc( int nVars ) -{ - Esop_Man_t * pMan; - // start the manager - pMan = ALLOC( Esop_Man_t, 1 ); - memset( pMan, 0, sizeof(Esop_Man_t) ); - pMan->nVars = nVars; - pMan->nWords = Esop_BitWordNum( nVars * 2 ); - pMan->pMemMan1 = Mem_FixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (1 - 1) ); - pMan->pMemMan2 = Mem_FixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (2 - 1) ); - pMan->pMemMan4 = Mem_FixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (4 - 1) ); - pMan->pMemMan8 = Mem_FixedStart( sizeof(Esop_Cube_t) + sizeof(unsigned) * (8 - 1) ); - // allocate storage for the temporary cover - pMan->ppStore = ALLOC( Esop_Cube_t *, pMan->nVars + 1 ); - // create tautology cubes - Esop_ManClean( pMan, nVars ); - pMan->pOne0 = Esop_CubeAlloc( pMan ); - pMan->pOne1 = Esop_CubeAlloc( pMan ); - pMan->pTemp = Esop_CubeAlloc( pMan ); - pMan->pBubble = Esop_CubeAlloc( pMan ); pMan->pBubble->uData[0] = 0; - // create trivial cubes - Esop_ManClean( pMan, 1 ); - pMan->pTriv0 = Esop_CubeAllocVar( pMan, 0, 0 ); - pMan->pTriv1 = Esop_CubeAllocVar( pMan, 0, 0 ); - Esop_ManClean( pMan, nVars ); - return pMan; -} - -/**Function************************************************************* - - Synopsis [Cleans the minimization manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Esop_ManClean( Esop_Man_t * p, int nSupp ) -{ - // set the size of the cube manager - p->nVars = nSupp; - p->nWords = Esop_BitWordNum(2*nSupp); - // clean the storage - memset( p->ppStore, 0, sizeof(Esop_Cube_t *) * (nSupp + 1) ); - p->nCubes = 0; -} - -/**Function************************************************************* - - Synopsis [Stops the minimization manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Esop_ManFree( Esop_Man_t * p ) -{ - Mem_FixedStop ( p->pMemMan1, 0 ); - Mem_FixedStop ( p->pMemMan2, 0 ); - Mem_FixedStop ( p->pMemMan4, 0 ); - Mem_FixedStop ( p->pMemMan8, 0 ); - free( p->ppStore ); - free( p ); -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/temp/esop/esopMin.c b/src/temp/esop/esopMin.c deleted file mode 100644 index 7a460f8e..00000000 --- a/src/temp/esop/esopMin.c +++ /dev/null @@ -1,299 +0,0 @@ -/**CFile**************************************************************** - - FileName [esopMin.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Cover manipulation package.] - - Synopsis [ESOP manipulation.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: esopMin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "esop.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static void Esop_EsopRewrite( Esop_Man_t * p ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [ESOP minimization procedure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Esop_EsopMinimize( Esop_Man_t * p ) -{ - int nCubesInit, nCubesOld, nIter; - if ( p->nCubes < 3 ) - return; - nIter = 0; - nCubesInit = p->nCubes; - do { - nCubesOld = p->nCubes; - Esop_EsopRewrite( p ); - nIter++; - } - while ( 100.0*(nCubesOld - p->nCubes)/nCubesOld > 3.0 ); - -// printf( "%d:%d->%d ", nIter, nCubesInit, p->nCubes ); -} - -/**Function************************************************************* - - Synopsis [Performs one round of rewriting using distance 2 cubes.] - - Description [The weakness of this procedure is that it tries each cube - with only one distance-2 cube. If this pair does not lead to improvement - the cube is inserted into the cover anyhow, and we try another pair. - A possible improvement would be to try this cube with all distance-2 - cubes, until an improvement is found, or until all such cubes are tried.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Esop_EsopRewrite( Esop_Man_t * p ) -{ - Esop_Cube_t * pCube, ** ppPrev; - Esop_Cube_t * pThis, ** ppPrevT; - int v00, v01, v10, v11, Var0, Var1, Index, nCubesOld; - int nPairs = 0; - - // insert the bubble before the first cube - p->pBubble->pNext = p->ppStore[0]; - p->ppStore[0] = p->pBubble; - p->pBubble->nLits = 0; - - // go through the cubes - while ( 1 ) - { - // get the index of the bubble - Index = p->pBubble->nLits; - - // find the bubble - Esop_CoverForEachCubePrev( p->ppStore[Index], pCube, ppPrev ) - if ( pCube == p->pBubble ) - break; - assert( pCube == p->pBubble ); - - // remove the bubble, get the next cube after the bubble - *ppPrev = p->pBubble->pNext; - pCube = p->pBubble->pNext; - if ( pCube == NULL ) - for ( Index++; Index <= p->nVars; Index++ ) - if ( p->ppStore[Index] ) - { - ppPrev = &(p->ppStore[Index]); - pCube = p->ppStore[Index]; - break; - } - // stop if there is no more cubes - if ( pCube == NULL ) - break; - - // find the first dist2 cube - Esop_CoverForEachCubePrev( pCube->pNext, pThis, ppPrevT ) - if ( Esop_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) - break; - if ( pThis == NULL && Index < p->nVars ) - Esop_CoverForEachCubePrev( p->ppStore[Index+1], pThis, ppPrevT ) - if ( Esop_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) - break; - if ( pThis == NULL && Index < p->nVars - 1 ) - Esop_CoverForEachCubePrev( p->ppStore[Index+2], pThis, ppPrevT ) - if ( Esop_CubesDistTwo( pCube, pThis, &Var0, &Var1 ) ) - break; - // continue if there is no dist2 cube - if ( pThis == NULL ) - { - // insert the bubble after the cube - p->pBubble->pNext = pCube->pNext; - pCube->pNext = p->pBubble; - p->pBubble->nLits = pCube->nLits; - continue; - } - nPairs++; - - // remove the cubes, insert the bubble instead of pCube - *ppPrevT = pThis->pNext; - *ppPrev = p->pBubble; - p->pBubble->pNext = pCube->pNext; - p->pBubble->nLits = pCube->nLits; - p->nCubes -= 2; - - // Exorlink-2: - // A{v00} B{v01} + A{v10} B{v11} = - // A{v00+v10} B{v01} + A{v10} B{v01+v11} = - // A{v00} B{v01+v11} + A{v00+v10} B{v11} - - // save the dist2 parameters - v00 = Esop_CubeGetVar( pCube, Var0 ); - v01 = Esop_CubeGetVar( pCube, Var1 ); - v10 = Esop_CubeGetVar( pThis, Var0 ); - v11 = Esop_CubeGetVar( pThis, Var1 ); -//printf( "\n" ); -//Esop_CubeWrite( stdout, pCube ); -//Esop_CubeWrite( stdout, pThis ); - - // derive the first pair of resulting cubes - Esop_CubeXorVar( pCube, Var0, v10 ); - pCube->nLits -= (v00 != 3); - pCube->nLits += ((v00 ^ v10) != 3); - Esop_CubeXorVar( pThis, Var1, v01 ); - pThis->nLits -= (v11 != 3); - pThis->nLits += ((v01 ^ v11) != 3); - - // add the cubes - nCubesOld = p->nCubes; - Esop_EsopAddCube( p, pCube ); - Esop_EsopAddCube( p, pThis ); - // check if the cubes were absorbed - if ( p->nCubes < nCubesOld + 2 ) - continue; - - // pull out both cubes - assert( pThis == p->ppStore[pThis->nLits] ); - p->ppStore[pThis->nLits] = pThis->pNext; - assert( pCube == p->ppStore[pCube->nLits] ); - p->ppStore[pCube->nLits] = pCube->pNext; - p->nCubes -= 2; - - // derive the second pair of resulting cubes - Esop_CubeXorVar( pCube, Var0, v10 ); - pCube->nLits -= ((v00 ^ v10) != 3); - pCube->nLits += (v00 != 3); - Esop_CubeXorVar( pCube, Var1, v11 ); - pCube->nLits -= (v01 != 3); - pCube->nLits += ((v01 ^ v11) != 3); - - Esop_CubeXorVar( pThis, Var0, v00 ); - pThis->nLits -= (v10 != 3); - pThis->nLits += ((v00 ^ v10) != 3); - Esop_CubeXorVar( pThis, Var1, v01 ); - pThis->nLits -= ((v01 ^ v11) != 3); - pThis->nLits += (v11 != 3); - - // add them anyhow - Esop_EsopAddCube( p, pCube ); - Esop_EsopAddCube( p, pThis ); - } -// printf( "Pairs = %d ", nPairs ); -} - -/**Function************************************************************* - - Synopsis [Adds the cube to storage.] - - Description [Returns 0 if the cube is added or removed. Returns 1 - if the cube is glued with some other cube and has to be added again. - Do not forget to clean the storage!] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Esop_EsopAddCubeInt( Esop_Man_t * p, Esop_Cube_t * pCube ) -{ - Esop_Cube_t * pThis, ** ppPrev; - // try to find the identical cube - Esop_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev ) - { - if ( Esop_CubesAreEqual( pCube, pThis ) ) - { - *ppPrev = pThis->pNext; - Esop_CubeRecycle( p, pCube ); - Esop_CubeRecycle( p, pThis ); - p->nCubes--; - return 0; - } - } - // find a distance-1 cube if it exists - if ( pCube->nLits < pCube->nVars ) - Esop_CoverForEachCubePrev( p->ppStore[pCube->nLits+1], pThis, ppPrev ) - { - if ( Esop_CubesDistOne( pCube, pThis, p->pTemp ) ) - { - *ppPrev = pThis->pNext; - Esop_CubesTransform( pCube, pThis, p->pTemp ); - pCube->nLits++; - Esop_CubeRecycle( p, pThis ); - p->nCubes--; - return 1; - } - } - Esop_CoverForEachCubePrev( p->ppStore[pCube->nLits], pThis, ppPrev ) - { - if ( Esop_CubesDistOne( pCube, pThis, p->pTemp ) ) - { - *ppPrev = pThis->pNext; - Esop_CubesTransform( pCube, pThis, p->pTemp ); - pCube->nLits--; - Esop_CubeRecycle( p, pThis ); - p->nCubes--; - return 1; - } - } - if ( pCube->nLits > 0 ) - Esop_CoverForEachCubePrev( p->ppStore[pCube->nLits-1], pThis, ppPrev ) - { - if ( Esop_CubesDistOne( pCube, pThis, p->pTemp ) ) - { - *ppPrev = pThis->pNext; - Esop_CubesTransform( pCube, pThis, p->pTemp ); - Esop_CubeRecycle( p, pThis ); - p->nCubes--; - return 1; - } - } - // add the cube - pCube->pNext = p->ppStore[pCube->nLits]; - p->ppStore[pCube->nLits] = pCube; - p->nCubes++; - return 0; -} - -/**Function************************************************************* - - Synopsis [Adds the cube to storage.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Esop_EsopAddCube( Esop_Man_t * p, Esop_Cube_t * pCube ) -{ - assert( pCube != p->pBubble ); - assert( (int)pCube->nLits == Esop_CubeCountLits(pCube) ); - while ( Esop_EsopAddCubeInt( p, pCube ) ); -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/temp/esop/esopUtil.c b/src/temp/esop/esopUtil.c deleted file mode 100644 index 7230cc87..00000000 --- a/src/temp/esop/esopUtil.c +++ /dev/null @@ -1,277 +0,0 @@ -/**CFile**************************************************************** - - FileName [esopUtil.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Cover manipulation package.] - - Synopsis [Utilities.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: esopUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "esop.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Esop_CubeWrite( FILE * pFile, Esop_Cube_t * pCube ) -{ - int i; - assert( (int)pCube->nLits == Esop_CubeCountLits(pCube) ); - for ( i = 0; i < (int)pCube->nVars; i++ ) - if ( Esop_CubeHasBit(pCube, i*2) ) - { - if ( Esop_CubeHasBit(pCube, i*2+1) ) - fprintf( pFile, "-" ); - else - fprintf( pFile, "0" ); - } - else - { - if ( Esop_CubeHasBit(pCube, i*2+1) ) - fprintf( pFile, "1" ); - else - fprintf( pFile, "?" ); - } - fprintf( pFile, " 1\n" ); -// fprintf( pFile, " %d\n", pCube->nLits ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Esop_CoverWrite( FILE * pFile, Esop_Cube_t * pCover ) -{ - Esop_Cube_t * pCube; - Esop_CoverForEachCube( pCover, pCube ) - Esop_CubeWrite( pFile, pCube ); - printf( "\n" ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Esop_CoverWriteStore( FILE * pFile, Esop_Man_t * p ) -{ - Esop_Cube_t * pCube; - int i; - for ( i = 0; i <= p->nVars; i++ ) - { - Esop_CoverForEachCube( p->ppStore[i], pCube ) - { - printf( "%2d : ", i ); - if ( pCube == p->pBubble ) - { - printf( "Bubble\n" ); - continue; - } - Esop_CubeWrite( pFile, pCube ); - } - } - printf( "\n" ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Esop_CoverWriteFile( Esop_Cube_t * pCover, char * pName, int fEsop ) -{ - char Buffer[1000]; - Esop_Cube_t * pCube; - FILE * pFile; - int i; - sprintf( Buffer, "%s.%s", pName, fEsop? "esop" : "pla" ); - for ( i = strlen(Buffer) - 1; i >= 0; i-- ) - if ( Buffer[i] == '<' || Buffer[i] == '>' ) - Buffer[i] = '_'; - pFile = fopen( Buffer, "w" ); - fprintf( pFile, "# %s cover for output %s generated by ABC\n", fEsop? "ESOP":"SOP", pName ); - fprintf( pFile, ".i %d\n", pCover? pCover->nVars : 0 ); - fprintf( pFile, ".o %d\n", 1 ); - fprintf( pFile, ".p %d\n", Esop_CoverCountCubes(pCover) ); - if ( fEsop ) fprintf( pFile, ".type esop\n" ); - Esop_CoverForEachCube( pCover, pCube ) - Esop_CubeWrite( pFile, pCube ); - fprintf( pFile, ".e\n" ); - fclose( pFile ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Esop_CoverCheck( Esop_Man_t * p ) -{ - Esop_Cube_t * pCube; - int i; - for ( i = 0; i <= p->nVars; i++ ) - Esop_CoverForEachCube( p->ppStore[i], pCube ) - assert( i == (int)pCube->nLits ); -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Esop_CubeCheck( Esop_Cube_t * pCube ) -{ - int i; - for ( i = 0; i < (int)pCube->nVars; i++ ) - if ( Esop_CubeGetVar( pCube, i ) == 0 ) - return 0; - return 1; -} - -/**Function************************************************************* - - Synopsis [Converts the cover from the sorted structure.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Esop_Cube_t * Esop_CoverCollect( Esop_Man_t * p, int nSuppSize ) -{ - Esop_Cube_t * pCov = NULL, ** ppTail = &pCov; - Esop_Cube_t * pCube, * pCube2; - int i; - for ( i = 0; i <= nSuppSize; i++ ) - { - Esop_CoverForEachCubeSafe( p->ppStore[i], pCube, pCube2 ) - { - assert( i == (int)pCube->nLits ); - *ppTail = pCube; - ppTail = &pCube->pNext; - assert( pCube->uData[0] ); // not a bubble - } - } - *ppTail = NULL; - return pCov; -} - -/**Function************************************************************* - - Synopsis [Sorts the cover in the increasing number of literals.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Esop_CoverExpand( Esop_Man_t * p, Esop_Cube_t * pCover ) -{ - Esop_Cube_t * pCube, * pCube2; - Esop_ManClean( p, p->nVars ); - Esop_CoverForEachCubeSafe( pCover, pCube, pCube2 ) - { - pCube->pNext = p->ppStore[pCube->nLits]; - p->ppStore[pCube->nLits] = pCube; - p->nCubes++; - } -} - -/**Function************************************************************* - - Synopsis [Sorts the cover in the increasing number of literals.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Esop_CoverSuppVarNum( Esop_Man_t * p, Esop_Cube_t * pCover ) -{ - Esop_Cube_t * pCube; - int i, Counter; - if ( pCover == NULL ) - return 0; - // clean the cube - for ( i = 0; i < (int)pCover->nWords; i++ ) - p->pTemp->uData[i] = ~((unsigned)0); - // add the bit data - Esop_CoverForEachCube( pCover, pCube ) - for ( i = 0; i < (int)pCover->nWords; i++ ) - p->pTemp->uData[i] &= pCube->uData[i]; - // count the vars - Counter = 0; - for ( i = 0; i < (int)pCover->nVars; i++ ) - Counter += ( Esop_CubeGetVar(p->pTemp, i) != 3 ); - return Counter; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/temp/esop/module.make b/src/temp/esop/module.make deleted file mode 100644 index 1003ccc1..00000000 --- a/src/temp/esop/module.make +++ /dev/null @@ -1,3 +0,0 @@ -SRC += src/temp/esop/esopMan.c \ - src/temp/esop/esopMin.c \ - src/temp/esop/esopUtil.c diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h index eb5f50e4..a8c8b289 100644 --- a/src/temp/ivy/ivy.h +++ b/src/temp/ivy/ivy.h @@ -136,6 +136,7 @@ struct Ivy_FraigParams_t_ double dActConeBumpMax; // the largest bump in activity int fProve; // prove the miter outputs int fVerbose; // verbose output + int fDoSparse; // skip sparse functions int nBTLimitNode; // conflict limit at a node int nBTLimitMiter; // conflict limit at an output int nBTLimitGlobal; // conflict limit global diff --git a/src/temp/ivy/ivyFraig.c b/src/temp/ivy/ivyFraig.c index 694d5a30..209ff8e7 100644 --- a/src/temp/ivy/ivyFraig.c +++ b/src/temp/ivy/ivyFraig.c @@ -216,6 +216,7 @@ void Ivy_FraigParamsDefault( Ivy_FraigParams_t * pParams ) pParams->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached pParams->fPatScores = 0; // enables simulation pattern scoring pParams->MaxScore = 25; // max score after which resimulation is used + pParams->fDoSparse = 1; // skips sparse functions // pParams->dActConeRatio = 0.05; // the ratio of cone to be bumped // pParams->dActConeBumpMax = 5.0; // the largest bump of activity pParams->dActConeRatio = 0.3; // the ratio of cone to be bumped @@ -1227,6 +1228,69 @@ int Ivy_FraigRefineClass_rec( Ivy_FraigMan_t * p, Ivy_Obj_t * pClass ) RetValue = Ivy_FraigRefineClass_rec( p, pClassNew ); return RetValue + 1; } + +/**Function************************************************************* + + Synopsis [Creates the counter-example from the successful pattern.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_FraigCheckOutputSimsSavePattern( Ivy_FraigMan_t * p, Ivy_Obj_t * pObj ) +{ + Ivy_FraigSim_t * pSims; + int i, k, BestPat, * pModel; + // find the word of the pattern + pSims = Ivy_ObjSim(pObj); + for ( i = 0; i < p->nSimWords; i++ ) + if ( pSims->pData[i] ) + break; + assert( i < p->nSimWords ); + // find the bit of the pattern + for ( k = 0; k < 32; k++ ) + if ( pSims->pData[i] & (1 << k) ) + break; + assert( k < 32 ); + // determine the best pattern + BestPat = i * 32 + k; + // fill in the counter-example data + pModel = ALLOC( int, Ivy_ManPiNum(p->pManFraig) ); + Ivy_ManForEachPi( p->pManAig, pObj, i ) + pModel[i] = Ivy_InfoHasBit(Ivy_ObjSim(pObj)->pData, BestPat); + // set the model + assert( p->pManFraig->pData == NULL ); + p->pManFraig->pData = pModel; + return; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the one of the output is already non-constant 0.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_FraigCheckOutputSims( Ivy_FraigMan_t * p ) +{ + Ivy_Obj_t * pObj; + int i; + Ivy_ManForEachPo( p->pManAig, pObj, i ) + if ( !Ivy_NodeHasZeroSim( p, Ivy_ObjFanin0(pObj) ) ) + { + // create the counter-example from this pattern + Ivy_FraigCheckOutputSimsSavePattern( p, Ivy_ObjFanin0(pObj) ); + return 1; + } + return 0; +} /**Function************************************************************* @@ -1244,6 +1308,13 @@ int Ivy_FraigRefineClasses( Ivy_FraigMan_t * p ) { Ivy_Obj_t * pClass, * pClass2; int clk, RetValue, Counter = 0; + // check if some outputs already became non-constant + // this is a special case when computation can be stopped!!! + if ( p->pParams->fProve ) + Ivy_FraigCheckOutputSims( p ); + if ( p->pManFraig->pData ) + return 0; + // refine the classed clk = clock(); Ivy_FraigForEachEquivClassSafe( p->lClasses.pHead, pClass, pClass2 ) { @@ -1447,27 +1518,6 @@ void Ivy_FraigSavePattern3( Ivy_FraigMan_t * p ) /**Function************************************************************* - Synopsis [Returns 1 if the one of the output is already non-constant 0.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ivy_FraigCheckOutputSims( Ivy_FraigMan_t * p ) -{ - Ivy_Obj_t * pObj; - int i; - Ivy_ManForEachPo( p->pManAig, pObj, i ) - if ( !Ivy_NodeHasZeroSim( p, Ivy_ObjFanin0(pObj) ) ) - return 1; - return 0; -} - -/**Function************************************************************* - Synopsis [Performs simulation of the manager.] Description [] @@ -1490,11 +1540,15 @@ void Ivy_FraigSimulate( Ivy_FraigMan_t * p ) Ivy_FraigAssignDist1( p, p->pPatWords ); Ivy_FraigSimulateOne( p ); nChanges = Ivy_FraigRefineClasses( p ); + if ( p->pManFraig->pData ) + return; //printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) ); Ivy_FraigSavePattern1( p ); Ivy_FraigAssignDist1( p, p->pPatWords ); Ivy_FraigSimulateOne( p ); nChanges = Ivy_FraigRefineClasses( p ); + if ( p->pManFraig->pData ) + return; //printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) ); // refine classes by random simulation do { @@ -1502,13 +1556,11 @@ void Ivy_FraigSimulate( Ivy_FraigMan_t * p ) Ivy_FraigSimulateOne( p ); nClasses = p->lClasses.nItems; nChanges = Ivy_FraigRefineClasses( p ); + if ( p->pManFraig->pData ) + return; //printf( "Refined classes = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) ); } while ( (double)nChanges / nClasses > p->pParams->dSimSatur ); // Ivy_FraigPrintSimClasses( p ); - - // check if some outputs already became non-constant -// if ( Ivy_FraigCheckOutputSims(p) ) -// printf( "Special case: One of the POs is already non-const zero.\n" ); } @@ -1620,6 +1672,8 @@ void Ivy_FraigResimulate( Ivy_FraigMan_t * p ) if ( p->pParams->fPatScores ) Ivy_FraigCleanPatScores( p ); nChanges = Ivy_FraigRefineClasses( p ); + if ( p->pManFraig->pData ) + return; if ( nChanges < 1 ) printf( "Error: A counter-example did not refine classes!\n" ); assert( nChanges >= 1 ); @@ -1635,6 +1689,8 @@ void Ivy_FraigResimulate( Ivy_FraigMan_t * p ) Ivy_FraigSimulateOne( p ); Ivy_FraigCleanPatScores( p ); nChanges = Ivy_FraigRefineClasses( p ); + if ( p->pManFraig->pData ) + return; //printf( "Refined class!!! = %5d. Changes = %4d. Pairs = %6d.\n", p->lClasses.nItems, nChanges, Ivy_FraigCountPairsClasses(p) ); if ( nChanges == 0 ) break; @@ -1765,6 +1821,14 @@ void Ivy_FraigMiterProve( Ivy_FraigMan_t * p ) memset( p->pManFraig->pData, 0, sizeof(int) * Ivy_ManPiNum(p->pManFraig) ); break; } +/* + // check the representative of this node + pRepr = Ivy_ObjClassNodeRepr(Ivy_ObjFanin0(pObj)); + if ( Ivy_Regular(pRepr) != p->pManAig->pConst1 ) + printf( "Representative is not constant 1.\n" ); + else + printf( "Representative is constant 1.\n" ); +*/ // try to prove the output constant 0 RetValue = Ivy_FraigNodeIsConst( p, Ivy_Regular(pObjNew) ); if ( RetValue == 1 ) // proved equivalent @@ -1816,7 +1880,11 @@ p->nClassesBeg = p->lClasses.nItems; Ivy_ManForEachNode( p->pManAig, pObj, i ) { Extra_ProgressBarUpdate( p->pProgress, k++, NULL ); - pObj->pEquiv = Ivy_FraigAnd( p, pObj ); + // default to simple strashing if simulation detected a counter-example for a PO + if ( p->pManFraig->pData ) + pObj->pEquiv = Ivy_And( p->pManFraig, Ivy_ObjChild0Equiv(pObj), Ivy_ObjChild1Equiv(pObj) ); + else + pObj->pEquiv = Ivy_FraigAnd( p, pObj ); assert( pObj->pEquiv != NULL ); // pTemp = Ivy_Regular(pObj->pEquiv); // assert( Ivy_Regular(pObj->pEquiv)->Type ); @@ -1826,7 +1894,7 @@ p->nClassesEnd = p->lClasses.nItems; // try to prove the outputs of the miter p->nNodesMiter = Ivy_ManNodeNum(p->pManFraig); // Ivy_FraigMiterStatus( p->pManFraig ); - if ( p->pParams->fProve ) + if ( p->pParams->fProve && p->pManFraig->pData == NULL ) Ivy_FraigMiterProve( p ); // add the POs Ivy_ManForEachPo( p->pManAig, pObj, i ) @@ -1860,7 +1928,7 @@ p->nClassesEnd = p->lClasses.nItems; ***********************************************************************/ Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld ) -{ +{ Ivy_Obj_t * pObjNew, * pFanin0New, * pFanin1New, * pObjReprNew; int RetValue; // get the fraiged fanins @@ -1869,8 +1937,13 @@ Ivy_Obj_t * Ivy_FraigAnd( Ivy_FraigMan_t * p, Ivy_Obj_t * pObjOld ) // get the candidate fraig node pObjNew = Ivy_And( p->pManFraig, pFanin0New, pFanin1New ); // get representative of this class - if ( Ivy_ObjClassNodeRepr(pObjOld) == NULL ) // this is a unique node + if ( Ivy_ObjClassNodeRepr(pObjOld) == NULL || // this is a unique node + (!p->pParams->fDoSparse && Ivy_ObjClassNodeRepr(pObjOld) == p->pManAig->pConst1) ) // this is a sparse node { +// if ( Ivy_ObjClassNodeRepr(pObjOld) == p->pManAig->pConst1 ) +// { +// int x = 0; +// } assert( Ivy_Regular(pFanin0New) != Ivy_Regular(pFanin1New) ); assert( pObjNew != Ivy_Regular(pFanin0New) ); assert( pObjNew != Ivy_Regular(pFanin1New) ); diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c index 8099b834..ac58cb61 100644 --- a/src/temp/ivy/ivyMan.c +++ b/src/temp/ivy/ivyMan.c @@ -411,7 +411,7 @@ int Ivy_ManLatchIsSelfFeed( Ivy_Obj_t * pLatch ) int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel ) { Ivy_Obj_t * pNode; - int LimitFactor = 100; + int LimitFactor = 5; int NodeBeg = Ivy_ManNodeNum(p); int nSteps; for ( nSteps = 0; Vec_PtrSize(p->vBufs) > 0; nSteps++ ) @@ -430,7 +430,8 @@ int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel ) Ivy_NodeFixBufferFanins( p, pNode, fUpdateLevel ); if ( nSteps > NodeBeg * LimitFactor ) { - printf( "This circuit cannot be forward retimed completely. Structural hashing is not finished after %d forward latch moves.\n", NodeBeg * LimitFactor ); + printf( "Structural hashing is not finished after %d forward latch moves.\n", NodeBeg * LimitFactor ); + printf( "This circuit cannot be forward-retimed completely. Quitting.\n" ); break; } } diff --git a/src/temp/player/module.make b/src/temp/player/module.make deleted file mode 100644 index 5185f56e..00000000 --- a/src/temp/player/module.make +++ /dev/null @@ -1,4 +0,0 @@ -SRC += src/temp/player/playerToAbc.c \ - src/temp/player/playerCore.c \ - src/temp/player/playerMan.c \ - src/temp/player/playerUtil.c diff --git a/src/temp/player/player.h b/src/temp/player/player.h deleted file mode 100644 index a4ee5650..00000000 --- a/src/temp/player/player.h +++ /dev/null @@ -1,113 +0,0 @@ -/**CFile**************************************************************** - - FileName [player.h] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [PLA decomposition package.] - - Synopsis [External declarations.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: player.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#ifndef __XYZ_H__ -#define __XYZ_H__ - -#ifdef __cplusplus -extern "C" { -#endif - -#include "ivy.h" -#include "esop.h" -#include "vec.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -typedef struct Pla_Man_t_ Pla_Man_t; -typedef struct Pla_Obj_t_ Pla_Obj_t; - -// storage for node information -struct Pla_Obj_t_ -{ - unsigned fFixed : 1; // fixed node - unsigned Depth : 31; // the depth in terms of LUTs/PLAs - int nRefs; // the number of references - Vec_Int_t vSupp[2]; // supports in two frames - Esop_Cube_t * pCover[2]; // esops in two frames -}; - -// storage for additional information -struct Pla_Man_t_ -{ - // general characteristics - int nLutMax; // the number of vars - int nPlaMax; // the number of vars - int nCubesMax; // the limit on the number of cubes in the intermediate covers - Ivy_Man_t * pManAig; // the AIG manager - Pla_Obj_t * pPlaStrs; // memory for structures - Esop_Man_t * pManMin; // the cube manager - // arrays to map local variables - Vec_Int_t * vComTo0; // mapping of common variables into first fanin - Vec_Int_t * vComTo1; // mapping of common variables into second fanin - Vec_Int_t * vPairs0; // the first var in each pair of common vars - Vec_Int_t * vPairs1; // the second var in each pair of common vars - Vec_Int_t * vTriv0; // trival support of the first node - Vec_Int_t * vTriv1; // trival support of the second node - // statistics - int nNodes; // the number of nodes processed - int nNodesLut; // the number of nodes processed - int nNodesPla; // the number of nodes processed - int nNodesBoth; // the number of nodes processed - int nNodesDeref; // the number of nodes processed -}; - -#define PLAYER_FANIN_LIMIT 128 - -#define PLA_MIN(a,b) (((a) < (b))? (a) : (b)) -#define PLA_MAX(a,b) (((a) > (b))? (a) : (b)) - -#define PLA_EMPTY ((Esop_Cube_t *)1) - -static inline Pla_Man_t * Ivy_ObjPlaMan( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { return (Pla_Man_t *)p->pData; } -static inline Pla_Obj_t * Ivy_ObjPlaStr( Ivy_Man_t * p, Ivy_Obj_t * pObj ) { return ((Pla_Man_t *)p->pData)->pPlaStrs + pObj->Id; } - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/*=== playerToAbc.c ==============================================================*/ -extern void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fRewriting, int fSynthesis, int fVerbose ); -/*=== playerCore.c =============================================================*/ -extern Pla_Man_t * Pla_ManDecompose( Ivy_Man_t * p, int nLutMax, int nPlaMax, int fVerbose ); -/*=== playerMan.c ==============================================================*/ -extern Pla_Man_t * Pla_ManAlloc( Ivy_Man_t * p, int nLutMax, int nPlaMax ); -extern void Pla_ManFree( Pla_Man_t * p ); -extern void Pla_ManFreeStr( Pla_Man_t * p, Pla_Obj_t * pStr ); -/*=== playerUtil.c =============================================================*/ -extern int Pla_ManMergeTwoSupports( Pla_Man_t * p, Vec_Int_t * vSupp0, Vec_Int_t * vSupp1, Vec_Int_t * vSupp ); -extern Esop_Cube_t * Pla_ManAndTwoCovers( Pla_Man_t * p, Esop_Cube_t * pCover0, Esop_Cube_t * pCover1, int nSupp, int fStopAtLimit ); -extern Esop_Cube_t * Pla_ManExorTwoCovers( Pla_Man_t * p, Esop_Cube_t * pCover0, Esop_Cube_t * pCover1, int nSupp, int fStopAtLimit ); -extern void Pla_ManComputeStats( Ivy_Man_t * pAig, Vec_Int_t * vNodes ); - -#ifdef __cplusplus -} -#endif - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - - diff --git a/src/temp/player/playerAbc.c b/src/temp/player/playerAbc.c deleted file mode 100644 index dcbca462..00000000 --- a/src/temp/player/playerAbc.c +++ /dev/null @@ -1,228 +0,0 @@ -/**CFile**************************************************************** - - FileName [playerAbc.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [PLAyer decomposition package.] - - Synopsis [Bridge between ABC and PLAyer.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - May 20, 2006.] - - Revision [$Id: playerAbc.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "player.h" -#include "abc.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static Ivy_Man_t * Ivy_ManFromAbc( Abc_Ntk_t * p ); -static Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtkOld, Ivy_Man_t * p ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -#if 0 - -/**Function************************************************************* - - Synopsis [Gives the current ABC network to PLAyer for processing.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fVerbose ) -{ - int fUseRewriting = 1; - Ivy_Man_t * pMan, * pManExt; - Abc_Ntk_t * pNtkAig; - - if ( !Abc_NtkIsStrash(pNtk) ) - return NULL; - // convert to the new AIG manager - pMan = Ivy_ManFromAbc( pNtk ); - // check the correctness of conversion - if ( !Ivy_ManCheck( pMan ) ) - { - printf( "Abc_NtkPlayer: Internal AIG check has failed.\n" ); - Ivy_ManStop( pMan ); - return NULL; - } - if ( fVerbose ) - Ivy_ManPrintStats( pMan ); - if ( fUseRewriting ) - { - // simplify - pMan = Ivy_ManResyn( pManExt = pMan, 1, 0 ); - Ivy_ManStop( pManExt ); - if ( fVerbose ) - Ivy_ManPrintStats( pMan ); - } - // perform decomposition/mapping into PLAs/LUTs - pManExt = Pla_ManDecompose( pMan, nLutMax, nPlaMax, fVerbose ); - Ivy_ManStop( pMan ); - pMan = pManExt; - if ( fVerbose ) - Ivy_ManPrintStats( pMan ); - // convert from the extended AIG manager into an SOP network - pNtkAig = Ivy_ManToAbc( pNtk, pMan ); - Ivy_ManStop( pMan ); - // chech the resulting network - if ( !Abc_NtkCheck( pNtkAig ) ) - { - printf( "Abc_NtkPlayer: The network check has failed.\n" ); - Abc_NtkDelete( pNtkAig ); - return NULL; - } - return pNtkAig; -} - -/**Function************************************************************* - - Synopsis [Converts from strashed AIG in ABC into strash AIG in IVY.] - - Description [Assumes DFS ordering of nodes in the AIG of ABC.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ivy_Man_t * Ivy_ManFromAbc( Abc_Ntk_t * pNtk ) -{ - Ivy_Man_t * pMan; - Abc_Obj_t * pObj; - int i; - // create the manager - pMan = Ivy_ManStart( Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk), Abc_NtkNodeNum(pNtk) + 10 ); - // create the PIs - Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Ivy_ManConst1(pMan); - Abc_NtkForEachCi( pNtk, pObj, i ) - pObj->pCopy = (Abc_Obj_t *)Ivy_ManPi(pMan, i); - // perform the conversion of the internal nodes - Abc_AigForEachAnd( pNtk, pObj, i ) - pObj->pCopy = (Abc_Obj_t *)Ivy_And( (Ivy_Obj_t *)Abc_ObjChild0Copy(pObj), (Ivy_Obj_t *)Abc_ObjChild1Copy(pObj) ); - // create the POs - Abc_NtkForEachCo( pNtk, pObj, i ) - Ivy_ObjConnect( Ivy_ManPo(pMan, i), (Ivy_Obj_t *)Abc_ObjChild0Copy(pObj) ); - Ivy_ManCleanup( pMan ); - return pMan; -} - -/**Function************************************************************* - - Synopsis [Converts AIG manager after PLA/LUT mapping into a logic ABC network.] - - Description [The AIG manager contains nodes with extended functionality. - Node types are in pObj->Type. Node fanins are in pObj->vFanins. Functions - of LUT nodes are in pMan->vTruths.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtkOld, Ivy_Man_t * pMan ) -{ - Abc_Ntk_t * pNtkNew; - Vec_Int_t * vIvyNodes, * vIvyFanins, * vTruths = pMan->vTruths; - Abc_Obj_t * pObj, * pObjNew, * pFaninNew; - Ivy_Obj_t * pIvyNode, * pIvyFanin; - int pCompls[PLAYER_FANIN_LIMIT]; - int i, k, Fanin, nFanins; - // start the new ABC network - pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_LOGIC, ABC_FUNC_SOP ); - // transfer the pointers to the basic nodes - Ivy_ManCleanTravId(pMan); - Ivy_ManConst1(pMan)->TravId = Abc_AigConst1(pNtkNew)->Id; - Abc_NtkForEachCi( pNtkNew, pObjNew, i ) - Ivy_ManPi(pMan, i)->TravId = pObjNew->Id; - // construct the logic network isomorphic to logic network in the AIG manager - vIvyNodes = Ivy_ManDfsExt( pMan ); - Ivy_ManForEachNodeVec( pMan, vIvyNodes, pIvyNode, i ) - { - // get fanins of the old node - vIvyFanins = Ivy_ObjGetFanins( pIvyNode ); - nFanins = Vec_IntSize(vIvyFanins); - // create the new node - pObjNew = Abc_NtkCreateNode( pNtkNew ); - Vec_IntForEachEntry( vIvyFanins, Fanin, k ) - { - pIvyFanin = Ivy_ObjObj( pIvyNode, Ivy_EdgeId(Fanin) ); - pFaninNew = Abc_NtkObj( pNtkNew, pIvyFanin->TravId ); - Abc_ObjAddFanin( pObjNew, pFaninNew ); - pCompls[k] = Ivy_EdgeIsComplement(Fanin); - assert( Ivy_ObjIsAndMulti(pIvyNode) || nFanins == 1 || pCompls[k] == 0 ); // EXOR/LUT cannot have complemented fanins - } - assert( k <= PLAYER_FANIN_LIMIT ); - // create logic function of the node - if ( Ivy_ObjIsAndMulti(pIvyNode) ) - pObjNew->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, nFanins, pCompls ); - else if ( Ivy_ObjIsExorMulti(pIvyNode) ) - pObjNew->pData = Abc_SopCreateXorSpecial( pNtkNew->pManFunc, nFanins ); - else if ( Ivy_ObjIsLut(pIvyNode) ) - pObjNew->pData = Abc_SopCreateFromTruth( pNtkNew->pManFunc, nFanins, Ivy_ObjGetTruth(pIvyNode) ); - else assert( 0 ); - assert( Abc_SopGetVarNum(pObjNew->pData) == nFanins ); - pIvyNode->TravId = pObjNew->Id; - } -//Pla_ManComputeStats( pMan, vIvyNodes ); - Vec_IntFree( vIvyNodes ); - // connect the PO nodes - Abc_NtkForEachCo( pNtkOld, pObj, i ) - { - // get the old fanin of the PO node - vIvyFanins = Ivy_ObjGetFanins( Ivy_ManPo(pMan, i) ); - Fanin = Vec_IntEntry( vIvyFanins, 0 ); - pIvyFanin = Ivy_ManObj( pMan, Ivy_EdgeId(Fanin) ); - // get the new ABC node corresponding to the old fanin - pFaninNew = Abc_NtkObj( pNtkNew, pIvyFanin->TravId ); - if ( Ivy_EdgeIsComplement(Fanin) ) // complement - { -// pFaninNew = Abc_NtkCreateNodeInv(pNtkNew, pFaninNew); - if ( Abc_ObjIsCi(pFaninNew) ) - pFaninNew = Abc_NtkCreateNodeInv(pNtkNew, pFaninNew); - else - { - // clone the node - pObjNew = Abc_NtkCloneObj( pFaninNew ); - // set complemented functions - pObjNew->pData = Abc_SopRegister( pNtkNew->pManFunc, pFaninNew->pData ); - Abc_SopComplement(pObjNew->pData); - // return the new node - pFaninNew = pObjNew; - } - assert( Abc_SopGetVarNum(pFaninNew->pData) == Abc_ObjFaninNum(pFaninNew) ); - } - Abc_ObjAddFanin( pObj->pCopy, pFaninNew ); - } - // remove dangling nodes - Abc_NtkForEachNode(pNtkNew, pObj, i) - if ( Abc_ObjFanoutNum(pObj) == 0 ) - Abc_NtkDeleteObj(pObj); - // fix CIs feeding directly into COs - Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 ); - return pNtkNew; -} - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/temp/player/playerBuild.c b/src/temp/player/playerBuild.c deleted file mode 100644 index e878f19c..00000000 --- a/src/temp/player/playerBuild.c +++ /dev/null @@ -1,283 +0,0 @@ -/**CFile**************************************************************** - - FileName [playerBuild.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [PLA decomposition package.] - - Synopsis [] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - May 11, 2006.] - - Revision [$Id: playerBuild.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "player.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static Ivy_Obj_t * Pla_ManToAig_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld ); -static Ivy_Obj_t * Ivy_ManToAigCube( Ivy_Man_t * pNew, Ivy_Obj_t * pObj, Esop_Cube_t * pCube, Vec_Int_t * vSupp ); -static Ivy_Obj_t * Ivy_ManToAigConst( Ivy_Man_t * pNew, int fConst1 ); -static int Pla_ManToAigLutFuncs( Ivy_Man_t * pNew, Ivy_Man_t * pOld ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -#if 0 - -/**Function************************************************************* - - Synopsis [Constructs the AIG manager (IVY) for the network after mapping.] - - Description [Uses extended node types (multi-input AND, multi-input EXOR, LUT).] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ivy_Man_t * Pla_ManToAig( Ivy_Man_t * pOld ) -{ - Ivy_Man_t * pNew; - Ivy_Obj_t * pObjOld, * pObjNew; - int i; - // start the new manager - pNew = Ivy_ManStart( Ivy_ManPiNum(pOld), Ivy_ManPoNum(pOld), 2*Ivy_ManNodeNum(pOld) + 10 ); - pNew->fExtended = 1; - // transfer the const/PI numbers - Ivy_ManCleanTravId(pOld); - Ivy_ManConst1(pOld)->TravId = Ivy_ManConst1(pNew)->Id; - Ivy_ManForEachPi( pOld, pObjOld, i ) - pObjOld->TravId = Ivy_ManPi(pNew, i)->Id; - // recursively construct the network - Ivy_ManForEachPo( pOld, pObjOld, i ) - { - pObjNew = Pla_ManToAig_rec( pNew, Ivy_ObjFanin0(pObjOld) ); - Ivy_ObjStartFanins( Ivy_ManPo(pNew, i), 1 ); - Ivy_ObjAddFanin( Ivy_ManPo(pNew, i), Ivy_EdgeCreate(pObjNew->Id, Ivy_ObjFaninC0(pObjOld)) ); - } - // compute the LUT functions - Pla_ManToAigLutFuncs( pNew, pOld ); - return pNew; -} - -/**Function************************************************************* - - Synopsis [Recursively construct the new node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ivy_Obj_t * Pla_ManToAig_rec( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld ) -{ - Pla_Man_t * p = Ivy_ObjMan(pObjOld)->pData; - Vec_Int_t * vSupp; - Esop_Cube_t * pCover, * pCube; - Ivy_Obj_t * pFaninOld, * pFaninNew, * pObjNew; - Pla_Obj_t * pStr; - int Entry, nCubes, ObjNewId, i; - // skip the node if it is a constant or already processed - if ( Ivy_ObjIsConst1(pObjOld) || pObjOld->TravId ) - return Ivy_ManObj( pNew, pObjOld->TravId ); - assert( Ivy_ObjIsAnd(pObjOld) || Ivy_ObjIsExor(pObjOld) ); - // get the support and the cover - pStr = Ivy_ObjPlaStr( pNew, pObjOld ); - if ( Vec_IntSize( &pStr->vSupp[0] ) <= p->nLutMax ) - { - vSupp = &pStr->vSupp[0]; - pCover = PLA_EMPTY; - } - else - { - vSupp = &pStr->vSupp[1]; - pCover = pStr->pCover[1]; - assert( pCover != PLA_EMPTY ); - } - // process the fanins - Vec_IntForEachEntry( vSupp, Entry, i ) - Pla_ManToAig_rec( pNew, Ivy_ObjObj(pObjOld, Entry) ); - // consider the case of a LUT - if ( pCover == PLA_EMPTY ) - { - pObjNew = Ivy_ObjCreateExt( pNew, IVY_LUT ); - Ivy_ObjStartFanins( pObjNew, p->nLutMax ); - // remember new object ID in case it changes - ObjNewId = pObjNew->Id; - Vec_IntForEachEntry( vSupp, Entry, i ) - { - pFaninOld = Ivy_ObjObj( pObjOld, Entry ); - Ivy_ObjAddFanin( Ivy_ManObj(pNew, ObjNewId), Ivy_EdgeCreate(pFaninOld->TravId, 0) ); - } - // get the new object - pObjNew = Ivy_ManObj(pNew, ObjNewId); - } - else - { - // for each cube, construct the node - nCubes = Esop_CoverCountCubes( pCover ); - if ( nCubes == 0 ) - pObjNew = Ivy_ManToAigConst( pNew, 0 ); - else if ( nCubes == 1 ) - pObjNew = Ivy_ManToAigCube( pNew, pObjOld, pCover, vSupp ); - else - { - pObjNew = Ivy_ObjCreateExt( pNew, IVY_EXORM ); - Ivy_ObjStartFanins( pObjNew, p->nLutMax ); - // remember new object ID in case it changes - ObjNewId = pObjNew->Id; - Esop_CoverForEachCube( pCover, pCube ) - { - pFaninNew = Ivy_ManToAigCube( pNew, pObjOld, pCube, vSupp ); - Ivy_ObjAddFanin( Ivy_ManObj(pNew, ObjNewId), Ivy_EdgeCreate(pFaninNew->Id, 0) ); - } - // get the new object - pObjNew = Ivy_ManObj(pNew, ObjNewId); - } - } - pObjOld->TravId = pObjNew->Id; - pObjNew->TravId = pObjOld->Id; - return pObjNew; -} - - -/**Function************************************************************* - - Synopsis [Returns constant 1 node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ivy_Obj_t * Ivy_ManToAigConst( Ivy_Man_t * pNew, int fConst1 ) -{ - Ivy_Obj_t * pObjNew; - pObjNew = Ivy_ObjCreateExt( pNew, IVY_ANDM ); - Ivy_ObjStartFanins( pObjNew, 1 ); - Ivy_ObjAddFanin( pObjNew, Ivy_EdgeCreate(0, !fConst1) ); - return pObjNew; -} - -/**Function************************************************************* - - Synopsis [Derives the decomposed network.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ivy_Obj_t * Ivy_ManToAigCube( Ivy_Man_t * pNew, Ivy_Obj_t * pObjOld, Esop_Cube_t * pCube, Vec_Int_t * vSupp ) -{ - Ivy_Obj_t * pObjNew, * pFaninOld; - int i, Value; - // if tautology cube, create constant 1 node - if ( pCube->nLits == 0 ) - return Ivy_ManToAigConst( pNew, 1 ); - // create AND node - pObjNew = Ivy_ObjCreateExt( pNew, IVY_ANDM ); - Ivy_ObjStartFanins( pObjNew, pCube->nLits ); - // add fanins - for ( i = 0; i < (int)pCube->nVars; i++ ) - { - Value = Esop_CubeGetVar( pCube, i ); - assert( Value != 0 ); - if ( Value == 3 ) - continue; - pFaninOld = Ivy_ObjObj( pObjOld, Vec_IntEntry(vSupp, i) ); - Ivy_ObjAddFanin( pObjNew, Ivy_EdgeCreate( pFaninOld->TravId, Value==1 ) ); - } - assert( Ivy_ObjFaninNum(pObjNew) == (int)pCube->nLits ); - return pObjNew; -} - - -/**Function************************************************************* - - Synopsis [Recursively construct the new node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Pla_ManToAigLutFuncs( Ivy_Man_t * pNew, Ivy_Man_t * pOld ) -{ - Vec_Int_t * vSupp, * vFanins, * vNodes, * vTemp; - Ivy_Obj_t * pObjOld, * pObjNew; - unsigned * pComputed, * pTruth; - int i, k, Counter = 0; - // create mapping from the LUT nodes into truth table indices - assert( pNew->vTruths == NULL ); - vNodes = Vec_IntAlloc( 100 ); - vTemp = Vec_IntAlloc( 100 ); - pNew->vTruths = Vec_IntStart( Ivy_ManObjIdNext(pNew) ); - Ivy_ManForEachObj( pNew, pObjNew, i ) - { - if ( Ivy_ObjIsLut(pObjNew) ) - Vec_IntWriteEntry( pNew->vTruths, i, 8 * Counter++ ); - else - Vec_IntWriteEntry( pNew->vTruths, i, -1 ); - } - // allocate memory - pNew->pMemory = ALLOC( unsigned, 8 * Counter ); - memset( pNew->pMemory, 0, sizeof(unsigned) * 8 * Counter ); - // derive truth tables - Ivy_ManForEachObj( pNew, pObjNew, i ) - { - if ( !Ivy_ObjIsLut(pObjNew) ) - continue; - pObjOld = Ivy_ManObj( pOld, pObjNew->TravId ); - vSupp = Ivy_ObjPlaStr(pNew, pObjOld)->vSupp; - assert( Vec_IntSize(vSupp) <= 8 ); - pTruth = Ivy_ObjGetTruth( pObjNew ); - pComputed = Ivy_ManCutTruth( pNew, pObjOld, vSupp, vNodes, vTemp ); - // check if the truth table is constant 0 - for ( k = 0; k < 8; k++ ) - if ( pComputed[k] ) - break; - if ( k == 8 ) - { - // create inverter - for ( k = 0; k < 8; k++ ) - pComputed[k] = 0x55555555; - // point it to the constant 1 node - vFanins = Ivy_ObjGetFanins( pObjNew ); - Vec_IntClear( vFanins ); - Vec_IntPush( vFanins, Ivy_EdgeCreate(0, 1) ); - } - memcpy( pTruth, pComputed, sizeof(unsigned) * 8 ); -// Extra_PrintBinary( stdout, pTruth, 16 ); printf( "\n" ); - } - Vec_IntFree( vTemp ); - Vec_IntFree( vNodes ); - return Counter; -} - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/temp/player/playerCore.c b/src/temp/player/playerCore.c deleted file mode 100644 index b87f39d4..00000000 --- a/src/temp/player/playerCore.c +++ /dev/null @@ -1,376 +0,0 @@ -/**CFile**************************************************************** - - FileName [playerCore.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [PLA decomposition package.] - - Synopsis [] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - May 11, 2006.] - - Revision [$Id: playerCore.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "player.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static int Pla_ManDecomposeInt( Pla_Man_t * p ); -static int Pla_ManDecomposeNode( Pla_Man_t * p, Ivy_Obj_t * pObj ); -static void Pla_NodeGetSuppsAndCovers( Pla_Man_t * p, Ivy_Obj_t * pObj, int Level, - Vec_Int_t ** pvSuppA, Vec_Int_t ** pvSuppB, Esop_Cube_t ** pvCovA, Esop_Cube_t ** pvCovB ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Performs decomposition/mapping into PLAs and K-LUTs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Pla_Man_t * Pla_ManDecompose( Ivy_Man_t * pAig, int nLutMax, int nPlaMax, int fVerbose ) -{ - Pla_Man_t * p; - p = Pla_ManAlloc( pAig, nLutMax, nPlaMax ); - if ( !Pla_ManDecomposeInt( p ) ) - { - printf( "Decomposition/mapping failed.\n" ); - Pla_ManFree( p ); - return NULL; - } - return p; -} - -/**Function************************************************************* - - Synopsis [Performs decomposition/mapping into PLAs and K-LUTs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Pla_ManDecomposeInt( Pla_Man_t * p ) -{ - Ivy_Man_t * pAig = p->pManAig; - Ivy_Obj_t * pObj; - Pla_Obj_t * pStr; - int i; - - // prepare the PI structures - Ivy_ManForEachPi( pAig, pObj, i ) - { - pStr = Ivy_ObjPlaStr( pAig, pObj ); - pStr->fFixed = 1; - pStr->Depth = 0; - pStr->nRefs = (unsigned)pObj->nRefs; - pStr->pCover[0] = PLA_EMPTY; - pStr->pCover[1] = PLA_EMPTY; - } - - // assuming DFS ordering of nodes in the manager - Ivy_ManForEachNode( pAig, pObj, i ) - if ( !Pla_ManDecomposeNode(p, pObj) ) - return 0; - return 1; -} - -/**Function************************************************************* - - Synopsis [Records decomposition statistics for one node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Pla_ManCountDecNodes( Pla_Man_t * p, Pla_Obj_t * pStr ) -{ - if ( Vec_IntSize(pStr->vSupp) <= p->nLutMax && pStr->pCover[1] != PLA_EMPTY ) - p->nNodesBoth++; - else if ( Vec_IntSize(pStr->vSupp) <= p->nLutMax ) - p->nNodesLut++; - else if ( pStr->pCover[1] != PLA_EMPTY ) - p->nNodesPla++; -} - -/**Function************************************************************* - - Synopsis [Performs decomposition/mapping for one node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Pla_ManDecomposeNode( Pla_Man_t * p, Ivy_Obj_t * pObj ) -{ - Pla_Obj_t * pStr, * pStr0, * pStr1; - Vec_Int_t * vSuppA, * vSuppB, * vSupp0, * vSupp1; - Esop_Cube_t * pCovA, * pCovB; - int nSuppSize1, nSuppSize2; - - assert( pObj->nRefs > 0 ); - p->nNodes++; - - // get the structures - pStr = Ivy_ObjPlaStr( p->pManAig, pObj ); - pStr0 = Ivy_ObjPlaStr( p->pManAig, Ivy_ObjFanin0( pObj ) ); - pStr1 = Ivy_ObjPlaStr( p->pManAig, Ivy_ObjFanin1( pObj ) ); - vSupp0 = &pStr->vSupp[0]; - vSupp1 = &pStr->vSupp[1]; - pStr->pCover[0] = PLA_EMPTY; - pStr->pCover[1] = PLA_EMPTY; - - // process level 1 - Pla_NodeGetSuppsAndCovers( p, pObj, 1, &vSuppA, &vSuppB, &pCovA, &pCovB ); - nSuppSize1 = Pla_ManMergeTwoSupports( p, vSuppA, vSuppB, vSupp0 ); - if ( nSuppSize1 > p->nPlaMax || pCovA == PLA_EMPTY || pCovB == PLA_EMPTY ) - pStr->pCover[0] = PLA_EMPTY; - else if ( Ivy_ObjIsAnd(pObj) ) - pStr->pCover[0] = Pla_ManAndTwoCovers( p, pCovA, pCovB, nSuppSize1, 1 ); - else - pStr->pCover[0] = Pla_ManExorTwoCovers( p, pCovA, pCovB, nSuppSize1, 1 ); - - // process level 2 - if ( PLA_MAX(pStr0->Depth, pStr1->Depth) > 1 ) - { - Pla_NodeGetSuppsAndCovers( p, pObj, 2, &vSuppA, &vSuppB, &pCovA, &pCovB ); - nSuppSize2 = Pla_ManMergeTwoSupports( p, vSuppA, vSuppB, vSupp1 ); - if ( nSuppSize2 > p->nPlaMax || pCovA == PLA_EMPTY || pCovB == PLA_EMPTY ) - pStr->pCover[1] = PLA_EMPTY; - else if ( Ivy_ObjIsAnd(pObj) ) - pStr->pCover[1] = Pla_ManAndTwoCovers( p, pCovA, pCovB, nSuppSize2, 1 ); - else - pStr->pCover[1] = Pla_ManExorTwoCovers( p, pCovA, pCovB, nSuppSize2, 1 ); - } - - // determine the level of this node - pStr->nRefs = (unsigned)pObj->nRefs; - pStr->Depth = PLA_MAX( pStr0->Depth, pStr1->Depth ); - pStr->Depth = pStr->Depth? pStr->Depth : 1; - if ( nSuppSize1 > p->nLutMax && pStr->pCover[1] == PLA_EMPTY ) - { - pStr->Depth++; - // free second level - if ( pStr->pCover[1] != PLA_EMPTY ) - Esop_CoverRecycle( p->pManMin, pStr->pCover[1] ); - vSupp1->nCap = 0; - vSupp1->nSize = 0; - FREE( vSupp1->pArray ); - pStr->pCover[1] = PLA_EMPTY; - // move first to second - pStr->vSupp[1] = pStr->vSupp[0]; - pStr->pCover[1] = pStr->pCover[0]; - vSupp0->nCap = 0; - vSupp0->nSize = 0; - vSupp0->pArray = NULL; - pStr->pCover[0] = PLA_EMPTY; - // get zero level - Pla_NodeGetSuppsAndCovers( p, pObj, 0, &vSuppA, &vSuppB, &pCovA, &pCovB ); - nSuppSize2 = Pla_ManMergeTwoSupports( p, vSuppA, vSuppB, vSupp0 ); - assert( nSuppSize2 == 2 ); - if ( pCovA == PLA_EMPTY || pCovB == PLA_EMPTY ) - pStr->pCover[0] = PLA_EMPTY; - else if ( Ivy_ObjIsAnd(pObj) ) - pStr->pCover[0] = Pla_ManAndTwoCovers( p, pCovA, pCovB, nSuppSize2, 0 ); - else - pStr->pCover[0] = Pla_ManExorTwoCovers( p, pCovA, pCovB, nSuppSize2, 0 ); - // count stats - if ( pStr0->fFixed == 0 ) Pla_ManCountDecNodes( p, pStr0 ); - if ( pStr1->fFixed == 0 ) Pla_ManCountDecNodes( p, pStr1 ); - // mark the nodes - pStr0->fFixed = 1; - pStr1->fFixed = 1; - } - else if ( pStr0->Depth < pStr1->Depth ) - { - if ( pStr0->fFixed == 0 ) Pla_ManCountDecNodes( p, pStr0 ); - pStr0->fFixed = 1; - } - else // if ( pStr0->Depth > pStr1->Depth ) - { - if ( pStr1->fFixed == 0 ) Pla_ManCountDecNodes( p, pStr1 ); - pStr1->fFixed = 1; - } - assert( pStr->Depth ); - - // free some of the covers to save memory - assert( pStr0->nRefs > 0 ); - assert( pStr1->nRefs > 0 ); - pStr0->nRefs--; - pStr1->nRefs--; - - if ( pStr0->nRefs == 0 && !pStr0->fFixed ) - Pla_ManFreeStr( p, pStr0 ), p->nNodesDeref++; - if ( pStr1->nRefs == 0 && !pStr1->fFixed ) - Pla_ManFreeStr( p, pStr1 ), p->nNodesDeref++; - - return 1; -} - -/**Function************************************************************* - - Synopsis [Returns pointers to the support arrays on the given level.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Pla_NodeGetSuppsAndCovers( Pla_Man_t * p, Ivy_Obj_t * pObj, int Level, - Vec_Int_t ** pvSuppA, Vec_Int_t ** pvSuppB, Esop_Cube_t ** pvCovA, Esop_Cube_t ** pvCovB ) -{ - Ivy_Obj_t * pFan0, * pFan1; - Pla_Obj_t * pStr, * pStr0, * pStr1; - Esop_Cube_t * pCovA, * pCovB; - int fCompl0, fCompl1; - assert( Level >= 0 && Level <= 2 ); - // get the complemented attributes - fCompl0 = Ivy_ObjFaninC0( pObj ); - fCompl1 = Ivy_ObjFaninC1( pObj ); - // get the fanins - pFan0 = Ivy_ObjFanin0( pObj ); - pFan1 = Ivy_ObjFanin1( pObj ); - // get the structures - pStr = Ivy_ObjPlaStr( p->pManAig, pObj ); - pStr0 = Ivy_ObjPlaStr( p->pManAig, pFan0 ); - pStr1 = Ivy_ObjPlaStr( p->pManAig, pFan1 ); - // make sure the fanins are processed - assert( Ivy_ObjIsPi(pFan0) || pStr0->Depth > 0 ); - assert( Ivy_ObjIsPi(pFan1) || pStr1->Depth > 0 ); - // prepare the return values depending on the level - Vec_IntWriteEntry( p->vTriv0, 0, pFan0->Id ); - Vec_IntWriteEntry( p->vTriv1, 0, pFan1->Id ); - *pvSuppA = p->vTriv0; - *pvSuppB = p->vTriv1; - pCovA = p->pManMin->pTriv0; - pCovB = p->pManMin->pTriv1; - if ( Level == 1 ) - { - if ( pStr0->Depth == pStr1->Depth ) - { - if ( pStr0->Depth > 0 ) - { - *pvSuppA = &pStr0->vSupp[0]; - *pvSuppB = &pStr1->vSupp[0]; - pCovA = pStr0->pCover[0]; - pCovB = pStr1->pCover[0]; - } - } - else if ( pStr0->Depth < pStr1->Depth ) - { - *pvSuppB = &pStr1->vSupp[0]; - pCovB = pStr1->pCover[0]; - } - else // if ( pStr0->Depth > pStr1->Depth ) - { - *pvSuppA = &pStr0->vSupp[0]; - pCovA = pStr0->pCover[0]; - } - } - else if ( Level == 2 ) - { - if ( pStr0->Depth == pStr1->Depth ) - { - *pvSuppA = &pStr0->vSupp[1]; - *pvSuppB = &pStr1->vSupp[1]; - pCovA = pStr0->pCover[1]; - pCovB = pStr1->pCover[1]; - } - else if ( pStr0->Depth + 1 == pStr1->Depth ) - { - *pvSuppA = &pStr0->vSupp[0]; - *pvSuppB = &pStr1->vSupp[1]; - pCovA = pStr0->pCover[0]; - pCovB = pStr1->pCover[1]; - } - else if ( pStr0->Depth == pStr1->Depth + 1 ) - { - *pvSuppA = &pStr0->vSupp[1]; - *pvSuppB = &pStr1->vSupp[0]; - pCovA = pStr0->pCover[1]; - pCovB = pStr1->pCover[0]; - } - else if ( pStr0->Depth < pStr1->Depth ) - { - *pvSuppB = &pStr1->vSupp[1]; - pCovB = pStr1->pCover[1]; - } - else // if ( pStr0->Depth > pStr1->Depth ) - { - *pvSuppA = &pStr0->vSupp[1]; - pCovA = pStr0->pCover[1]; - } - } - // complement the first if needed - if ( pCovA == PLA_EMPTY || !fCompl0 ) - *pvCovA = pCovA; - else if ( pCovA && pCovA->nLits == 0 ) // topmost one is the tautology cube - *pvCovA = pCovA->pNext; - else - *pvCovA = p->pManMin->pOne0, p->pManMin->pOne0->pNext = pCovA; - // complement the second if needed - if ( pCovB == PLA_EMPTY || !fCompl1 ) - *pvCovB = pCovB; - else if ( pCovB && pCovB->nLits == 0 ) // topmost one is the tautology cube - *pvCovB = pCovB->pNext; - else - *pvCovB = p->pManMin->pOne1, p->pManMin->pOne1->pNext = pCovB; -} - - -/* - if ( pObj->Id == 1371 ) - { - int k; - printf( "Zero : " ); - for ( k = 0; k < vSuppA->nSize; k++ ) - printf( "%d ", vSuppA->pArray[k] ); - printf( "\n" ); - printf( "One : " ); - for ( k = 0; k < vSuppB->nSize; k++ ) - printf( "%d ", vSuppB->pArray[k] ); - printf( "\n" ); - printf( "Node : " ); - for ( k = 0; k < vSupp0->nSize; k++ ) - printf( "%d ", vSupp0->pArray[k] ); - printf( "\n" ); - printf( "\n" ); - printf( "\n" ); - Esop_CoverWrite( stdout, pCovA ); - printf( "\n" ); - Esop_CoverWrite( stdout, pCovB ); - printf( "\n" ); - } -*/ - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/temp/player/playerMan.c b/src/temp/player/playerMan.c deleted file mode 100644 index 32eacc9b..00000000 --- a/src/temp/player/playerMan.c +++ /dev/null @@ -1,125 +0,0 @@ -/**CFile**************************************************************** - - FileName [playerMan.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [PLA decomposition package.] - - Synopsis [] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - May 11, 2006.] - - Revision [$Id: playerMan.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "player.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Allocates the PLA/LUT mapping manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Pla_Man_t * Pla_ManAlloc( Ivy_Man_t * pAig, int nLutMax, int nPlaMax ) -{ - Pla_Man_t * pMan; - assert( !(nLutMax < 2 || nLutMax > 8 || nPlaMax < 8 || nPlaMax > 128) ); - // start the manager - pMan = ALLOC( Pla_Man_t, 1 ); - memset( pMan, 0, sizeof(Pla_Man_t) ); - pMan->nLutMax = nLutMax; - pMan->nPlaMax = nPlaMax; - pMan->nCubesMax = 2 * nPlaMax; // higher limit, later reduced - pMan->pManAig = pAig; - // set up the temporaries - pMan->vComTo0 = Vec_IntAlloc( 2 * nPlaMax ); - pMan->vComTo1 = Vec_IntAlloc( 2 * nPlaMax ); - pMan->vPairs0 = Vec_IntAlloc( nPlaMax ); - pMan->vPairs1 = Vec_IntAlloc( nPlaMax ); - pMan->vTriv0 = Vec_IntAlloc( 1 ); Vec_IntPush( pMan->vTriv0, -1 ); - pMan->vTriv1 = Vec_IntAlloc( 1 ); Vec_IntPush( pMan->vTriv1, -1 ); - // allocate memory for object structures - pMan->pPlaStrs = ALLOC( Pla_Obj_t, Ivy_ManObjIdMax(pAig)+1 ); - memset( pMan->pPlaStrs, 0, sizeof(Pla_Obj_t) * (Ivy_ManObjIdMax(pAig)+1) ); - // create the cube manager - pMan->pManMin = Esop_ManAlloc( nPlaMax ); - // save the resulting manager - assert( pAig->pData == NULL ); - pAig->pData = pMan; - return pMan; -} - -/**Function************************************************************* - - Synopsis [Frees the PLA/LUT mapping manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Pla_ManFree( Pla_Man_t * p ) -{ - Pla_Obj_t * pStr; - int i; - Esop_ManFree( p->pManMin ); - Vec_IntFree( p->vTriv0 ); - Vec_IntFree( p->vTriv1 ); - Vec_IntFree( p->vComTo0 ); - Vec_IntFree( p->vComTo1 ); - Vec_IntFree( p->vPairs0 ); - Vec_IntFree( p->vPairs1 ); - for ( i = 0, pStr = p->pPlaStrs; i <= Ivy_ManObjIdMax(p->pManAig); i++, pStr++ ) - FREE( pStr->vSupp[0].pArray ), FREE( pStr->vSupp[1].pArray ); - free( p->pPlaStrs ); - free( p ); -} - -/**Function************************************************************* - - Synopsis [Cleans the PLA/LUT structure of the node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Pla_ManFreeStr( Pla_Man_t * p, Pla_Obj_t * pStr ) -{ - if ( pStr->pCover[0] != PLA_EMPTY ) Esop_CoverRecycle( p->pManMin, pStr->pCover[0] ); - if ( pStr->pCover[1] != PLA_EMPTY ) Esop_CoverRecycle( p->pManMin, pStr->pCover[1] ); - if ( pStr->vSupp[0].pArray ) free( pStr->vSupp[0].pArray ); - if ( pStr->vSupp[1].pArray ) free( pStr->vSupp[1].pArray ); - memset( pStr, 0, sizeof(Pla_Obj_t) ); - pStr->pCover[0] = PLA_EMPTY; - pStr->pCover[1] = PLA_EMPTY; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/temp/player/playerToAbc.c b/src/temp/player/playerToAbc.c deleted file mode 100644 index 81032826..00000000 --- a/src/temp/player/playerToAbc.c +++ /dev/null @@ -1,523 +0,0 @@ -/**CFile**************************************************************** - - FileName [playerToAbc.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [PLAyer decomposition package.] - - Synopsis [Bridge between ABC and PLAyer.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - May 20, 2006.] - - Revision [$Id: playerToAbc.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "player.h" -#include "abc.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -static Ivy_Man_t * Ivy_ManFromAbc( Abc_Ntk_t * p ); -static Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, Pla_Man_t * p, int fFastMode ); -static Abc_Obj_t * Ivy_ManToAbc_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Pla_Man_t * p, Ivy_Obj_t * pObjIvy, Vec_Int_t * vNodes, Vec_Int_t * vTemp ); -static Abc_Obj_t * Ivy_ManToAbcFast_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj_t * pObjIvy, Vec_Int_t * vNodes, Vec_Int_t * vTemp ); -static Abc_Obj_t * Ivy_ManToAigCube( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj_t * pObjIvy, Esop_Cube_t * pCube, Vec_Int_t * vSupp ); -static int Abc_NtkPlayerCost( Abc_Ntk_t * pNtk, int RankCost, int fVerbose ); - -static inline void Abc_ObjSetIvy2Abc( Ivy_Man_t * p, int IvyId, Abc_Obj_t * pObjAbc ) { assert(Vec_PtrEntry(p->pCopy, IvyId) == NULL); assert(!Abc_ObjIsComplement(pObjAbc)); Vec_PtrWriteEntry( p->pCopy, IvyId, pObjAbc ); } -static inline Abc_Obj_t * Abc_ObjGetIvy2Abc( Ivy_Man_t * p, int IvyId ) { return Vec_PtrEntry( p->pCopy, IvyId ); } - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Applies PLA/LUT mapping to the ABC network.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void * Abc_NtkPlayer( void * pNtk, int nLutMax, int nPlaMax, int RankCost, int fFastMode, int fRewriting, int fSynthesis, int fVerbose ) -{ - Pla_Man_t * p; - Ivy_Man_t * pMan, * pManExt; - Abc_Ntk_t * pNtkNew; - if ( !Abc_NtkIsStrash(pNtk) ) - return NULL; - // convert to the new AIG manager - pMan = Ivy_ManFromAbc( pNtk ); - // check the correctness of conversion - if ( !Ivy_ManCheck( pMan ) ) - { - printf( "Abc_NtkPlayer: Internal AIG check has failed.\n" ); - Ivy_ManStop( pMan ); - return NULL; - } - if ( fVerbose ) - Ivy_ManPrintStats( pMan ); - if ( fRewriting ) - { - // simplify - pMan = Ivy_ManResyn0( pManExt = pMan, 1, 0 ); - Ivy_ManStop( pManExt ); - if ( fVerbose ) - Ivy_ManPrintStats( pMan ); - } - if ( fSynthesis ) - { - // simplify - pMan = Ivy_ManResyn( pManExt = pMan, 1, 0 ); - Ivy_ManStop( pManExt ); - if ( fVerbose ) - Ivy_ManPrintStats( pMan ); - } - // perform decomposition - if ( fFastMode ) - { - // perform mapping into LUTs - Ivy_FastMapPerform( pMan, nLutMax, 1, fVerbose ); - // convert from the extended AIG manager into an SOP network - pNtkNew = Ivy_ManToAbc( pNtk, pMan, NULL, fFastMode ); -// pNtkNew = NULL; - Ivy_FastMapStop( pMan ); - } - else - { - assert( nLutMax >= 2 && nLutMax <= 8 ); - // perform decomposition/mapping into PLAs/LUTs - p = Pla_ManDecompose( pMan, nLutMax, nPlaMax, fVerbose ); - // convert from the extended AIG manager into an SOP network - pNtkNew = Ivy_ManToAbc( pNtk, pMan, p, fFastMode ); - Pla_ManFree( p ); - } - Ivy_ManStop( pMan ); - // chech the resulting network - if ( pNtkNew && !Abc_NtkCheck( pNtkNew ) ) - { - printf( "Abc_NtkPlayer: The network check has failed.\n" ); - Abc_NtkDelete( pNtkNew ); - return NULL; - } -// Abc_NtkPlayerCost( pNtkNew, RankCost, fVerbose ); - return pNtkNew; -} - -/**Function************************************************************* - - Synopsis [Converts from strashed AIG in ABC into strash AIG in IVY.] - - Description [Assumes DFS ordering of nodes in the AIG of ABC.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Ivy_Man_t * Ivy_ManFromAbc( Abc_Ntk_t * pNtk ) -{ - Ivy_Man_t * pMan; - Abc_Obj_t * pObj; - int i; - // create the manager - pMan = Ivy_ManStart(); - // create the PIs - Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Ivy_ManConst1(pMan); - Abc_NtkForEachCi( pNtk, pObj, i ) - pObj->pCopy = (Abc_Obj_t *)Ivy_ObjCreatePi(pMan); - // perform the conversion of the internal nodes - Abc_AigForEachAnd( pNtk, pObj, i ) - pObj->pCopy = (Abc_Obj_t *)Ivy_And( pMan, (Ivy_Obj_t *)Abc_ObjChild0Copy(pObj), (Ivy_Obj_t *)Abc_ObjChild1Copy(pObj) ); - // create the POs - Abc_NtkForEachCo( pNtk, pObj, i ) - Ivy_ObjCreatePo( pMan, (Ivy_Obj_t *)Abc_ObjChild0Copy(pObj) ); - Ivy_ManCleanup( pMan ); - return pMan; -} - -/**Function************************************************************* - - Synopsis [Constructs the ABC network after mapping.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Ivy_ManToAbc( Abc_Ntk_t * pNtk, Ivy_Man_t * pMan, Pla_Man_t * p, int fFastMode ) -{ - Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pObjAbc, * pObj; - Ivy_Obj_t * pObjIvy; - Vec_Int_t * vNodes, * vTemp; - int i; - // start mapping from Ivy into Abc - pMan->pCopy = Vec_PtrStart( Ivy_ManObjIdMax(pMan) + 1 ); - // start the new ABC network - pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); - // transfer the pointers to the basic nodes - Abc_ObjSetIvy2Abc( pMan, Ivy_ManConst1(pMan)->Id, Abc_NtkCreateNodeConst1(pNtkNew) ); - Abc_NtkForEachCi( pNtkNew, pObjAbc, i ) - Abc_ObjSetIvy2Abc( pMan, Ivy_ManPi(pMan, i)->Id, pObjAbc ); - // recursively construct the network - vNodes = Vec_IntAlloc( 100 ); - vTemp = Vec_IntAlloc( 100 ); - Ivy_ManForEachPo( pMan, pObjIvy, i ) - { - // get the new ABC node corresponding to the old fanin of the PO in IVY - if ( fFastMode ) - pObjAbc = Ivy_ManToAbcFast_rec( pNtkNew, pMan, Ivy_ObjFanin0(pObjIvy), vNodes, vTemp ); - else - pObjAbc = Ivy_ManToAbc_rec( pNtkNew, pMan, p, Ivy_ObjFanin0(pObjIvy), vNodes, vTemp ); - // consider the case of complemented fanin of the PO - if ( Ivy_ObjFaninC0(pObjIvy) ) // complement - { - if ( Abc_ObjIsCi(pObjAbc) ) - pObjAbc = Abc_NtkCreateNodeInv( pNtkNew, pObjAbc ); - else - { - // clone the node - pObj = Abc_NtkCloneObj( pObjAbc ); - // set complemented functions - pObj->pData = Abc_SopRegister( pNtkNew->pManFunc, pObjAbc->pData ); - Abc_SopComplement(pObj->pData); - // return the new node - pObjAbc = pObj; - } - assert( Abc_SopGetVarNum(pObjAbc->pData) == Abc_ObjFaninNum(pObjAbc) ); - } - Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), pObjAbc ); - } - Vec_IntFree( vTemp ); - Vec_IntFree( vNodes ); - Vec_PtrFree( pMan->pCopy ); - pMan->pCopy = NULL; - // remove dangling nodes -// Abc_NtkForEachNode( pNtkNew, pObjAbc, i ) -// if ( Abc_ObjFanoutNum(pObjAbc) == 0 ) -// Abc_NtkDeleteObj(pObjAbc); - Abc_NtkCleanup( pNtkNew, 0 ); - // fix CIs feeding directly into COs - Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 ); - return pNtkNew; -} - -/**Function************************************************************* - - Synopsis [Recursively construct the new node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Obj_t * Ivy_ManToAbc_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Pla_Man_t * p, Ivy_Obj_t * pObjIvy, Vec_Int_t * vNodes, Vec_Int_t * vTemp ) -{ - Vec_Int_t * vSupp; - Esop_Cube_t * pCover, * pCube; - Abc_Obj_t * pObjAbc, * pFaninAbc; - Pla_Obj_t * pStr; - int Entry, nCubes, i; - unsigned * puTruth; - // skip the node if it is a constant or already processed - pObjAbc = Abc_ObjGetIvy2Abc( pMan, pObjIvy->Id ); - if ( pObjAbc ) - return pObjAbc; - assert( Ivy_ObjIsAnd(pObjIvy) || Ivy_ObjIsExor(pObjIvy) ); - // get the support and the cover - pStr = Ivy_ObjPlaStr( pMan, pObjIvy ); - if ( Vec_IntSize( &pStr->vSupp[0] ) <= p->nLutMax ) - { - vSupp = &pStr->vSupp[0]; - pCover = PLA_EMPTY; - } - else - { - vSupp = &pStr->vSupp[1]; - pCover = pStr->pCover[1]; - assert( pCover != PLA_EMPTY ); - } - // create new node and its fanins - Vec_IntForEachEntry( vSupp, Entry, i ) - Ivy_ManToAbc_rec( pNtkNew, pMan, p, Ivy_ManObj(pMan, Entry), vNodes, vTemp ); - // consider the case of a LUT - if ( pCover == PLA_EMPTY ) - { - pObjAbc = Abc_NtkCreateNode( pNtkNew ); - Vec_IntForEachEntry( vSupp, Entry, i ) - Abc_ObjAddFanin( pObjAbc, Abc_ObjGetIvy2Abc(pMan, Entry) ); - // check if the truth table is constant 0 - puTruth = Ivy_ManCutTruth( pMan, pObjIvy, vSupp, vNodes, vTemp ); - // if the function is constant 0, create constant 0 node - if ( Extra_TruthIsConst0(puTruth, 8) ) - { - pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL ); - pObjAbc = Abc_NtkCreateNodeConst0( pNtkNew ); - } - else if ( Extra_TruthIsConst1(puTruth, 8) ) - { - pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL ); - pObjAbc = Abc_NtkCreateNodeConst1( pNtkNew ); - } - else - { - int fCompl = Ivy_TruthIsop( puTruth, Vec_IntSize(vSupp), vNodes, 1 ); - if ( vNodes->nSize == -1 ) - printf( "Ivy_ManToAbc_rec(): Internal error.\n" ); - pObjAbc->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, Vec_IntSize(vSupp), vNodes ); - if ( fCompl ) Abc_SopComplement(pObjAbc->pData); -// printf( "Cover contains %d cubes.\n", Vec_IntSize(vNodes) ); -// pObjAbc->pData = Abc_SopCreateFromTruth( pNtkNew->pManFunc, Vec_IntSize(vSupp), puTruth ); - } - } - else - { - // for each cube, construct the node - nCubes = Esop_CoverCountCubes( pCover ); - if ( nCubes == 0 ) - pObjAbc = Abc_NtkCreateNodeConst0( pNtkNew ); - else if ( nCubes == 1 ) - pObjAbc = Ivy_ManToAigCube( pNtkNew, pMan, pObjIvy, pCover, vSupp ); - else - { - pObjAbc = Abc_NtkCreateNode( pNtkNew ); - Esop_CoverForEachCube( pCover, pCube ) - { - pFaninAbc = Ivy_ManToAigCube( pNtkNew, pMan, pObjIvy, pCube, vSupp ); - Abc_ObjAddFanin( pObjAbc, pFaninAbc ); - } - pObjAbc->pData = Abc_SopCreateXorSpecial( pNtkNew->pManFunc, Abc_ObjFaninNum(pObjAbc) ); - } - } - Abc_ObjSetIvy2Abc( pMan, pObjIvy->Id, pObjAbc ); - return pObjAbc; -} - -/**Function************************************************************* - - Synopsis [Derives the decomposed network.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Obj_t * Ivy_ManToAigCube( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj_t * pObjIvy, Esop_Cube_t * pCube, Vec_Int_t * vSupp ) -{ - int pCompls[PLAYER_FANIN_LIMIT]; - Abc_Obj_t * pObjAbc, * pFaninAbc; - int i, k, Value; - // if tautology cube, create constant 1 node - if ( pCube->nLits == 0 ) - return Abc_NtkCreateNodeConst1(pNtkNew); - // create AND node - pObjAbc = Abc_NtkCreateNode( pNtkNew ); - for ( i = k = 0; i < (int)pCube->nVars; i++ ) - { - Value = Esop_CubeGetVar( pCube, i ); - assert( Value != 0 ); - if ( Value == 3 ) - continue; - pFaninAbc = Abc_ObjGetIvy2Abc( pMan, Vec_IntEntry(vSupp, i) ); - pFaninAbc = Abc_ObjNotCond( pFaninAbc, Value==1 ); - Abc_ObjAddFanin( pObjAbc, Abc_ObjRegular(pFaninAbc) ); - pCompls[k++] = Abc_ObjIsComplement(pFaninAbc); - } - pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Abc_ObjFaninNum(pObjAbc), pCompls ); - assert( Abc_ObjFaninNum(pObjAbc) == (int)pCube->nLits ); - return pObjAbc; -} - - - - -/**Function************************************************************* - - Synopsis [Recursively construct the new node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Obj_t * Ivy_ManToAbcFast_rec( Abc_Ntk_t * pNtkNew, Ivy_Man_t * pMan, Ivy_Obj_t * pObjIvy, Vec_Int_t * vNodes, Vec_Int_t * vTemp ) -{ - Vec_Int_t Supp, * vSupp = &Supp; - Abc_Obj_t * pObjAbc, * pFaninAbc; - int i, Entry; - unsigned * puTruth; - // skip the node if it is a constant or already processed - pObjAbc = Abc_ObjGetIvy2Abc( pMan, pObjIvy->Id ); - if ( pObjAbc ) - return pObjAbc; - assert( Ivy_ObjIsAnd(pObjIvy) || Ivy_ObjIsExor(pObjIvy) ); - // get the support of K-LUT - Ivy_FastMapReadSupp( pMan, pObjIvy, vSupp ); - // create new ABC node and its fanins - pObjAbc = Abc_NtkCreateNode( pNtkNew ); - Vec_IntForEachEntry( vSupp, Entry, i ) - { - pFaninAbc = Ivy_ManToAbcFast_rec( pNtkNew, pMan, Ivy_ManObj(pMan, Entry), vNodes, vTemp ); - Abc_ObjAddFanin( pObjAbc, pFaninAbc ); - } - // check if the truth table is constant 0 - puTruth = Ivy_ManCutTruth( pMan, pObjIvy, vSupp, vNodes, vTemp ); - // if the function is constant 0, create constant 0 node - if ( Extra_TruthIsConst0(puTruth, 8) ) - { - pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL ); - pObjAbc = Abc_NtkCreateNodeConst0( pNtkNew ); - } - else if ( Extra_TruthIsConst1(puTruth, 8) ) - { - pObjAbc->pData = Abc_SopCreateAnd( pNtkNew->pManFunc, Vec_IntSize(vSupp), NULL ); - pObjAbc = Abc_NtkCreateNodeConst1( pNtkNew ); - } - else - { - int fCompl = Ivy_TruthIsop( puTruth, Vec_IntSize(vSupp), vNodes, 1 ); - if ( vNodes->nSize == -1 ) - printf( "Ivy_ManToAbcFast_rec(): Internal error.\n" ); - pObjAbc->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, Vec_IntSize(vSupp), vNodes ); - if ( fCompl ) Abc_SopComplement(pObjAbc->pData); - } - Abc_ObjSetIvy2Abc( pMan, pObjIvy->Id, pObjAbc ); - return pObjAbc; -} - - -/**Function************************************************************* - - Synopsis [Computes cost of the node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Abc_NodePlayerCost( int nFanins ) -{ - if ( nFanins <= 4 ) - return 1; - if ( nFanins <= 6 ) - return 2; - if ( nFanins <= 8 ) - return 4; - if ( nFanins <= 16 ) - return 8; - if ( nFanins <= 32 ) - return 16; - if ( nFanins <= 64 ) - return 32; - if ( nFanins <= 128 ) - return 64; - assert( 0 ); - return 0; -} - -/**Function************************************************************* - - Synopsis [Computes the number of ranks needed for one level.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline int Abc_NtkPlayerCostOneLevel( int nCost, int RankCost ) -{ - return (nCost / RankCost) + ((nCost % RankCost) > 0); -} - -/**Function************************************************************* - - Synopsis [Computes the cost function for the network (number of ranks).] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkPlayerCost( Abc_Ntk_t * pNtk, int RankCost, int fVerbose ) -{ - Abc_Obj_t * pObj; - int * pLevelCosts, * pLevelCostsR; - int Cost, CostTotal, CostTotalR, nRanksTotal, nRanksTotalR; - int nFanins, nLevels, LevelR, i; - // compute the reverse levels - Abc_NtkStartReverseLevels( pNtk ); - // compute the costs for each level - nLevels = Abc_NtkGetLevelNum( pNtk ); - pLevelCosts = ALLOC( int, nLevels + 1 ); - pLevelCostsR = ALLOC( int, nLevels + 1 ); - memset( pLevelCosts, 0, sizeof(int) * (nLevels + 1) ); - memset( pLevelCostsR, 0, sizeof(int) * (nLevels + 1) ); - Abc_NtkForEachNode( pNtk, pObj, i ) - { - nFanins = Abc_ObjFaninNum(pObj); - if ( nFanins == 0 ) - continue; - Cost = Abc_NodePlayerCost( nFanins ); - LevelR = Vec_IntEntry( pNtk->vLevelsR, pObj->Id ); - pLevelCosts[ pObj->Level ] += Cost; - pLevelCostsR[ LevelR ] += Cost; - } - // compute the total cost - CostTotal = CostTotalR = nRanksTotal = nRanksTotalR = 0; - for ( i = 0; i <= nLevels; i++ ) - { - CostTotal += pLevelCosts[i]; - CostTotalR += pLevelCostsR[i]; - nRanksTotal += Abc_NtkPlayerCostOneLevel( pLevelCosts[i], RankCost ); - nRanksTotalR += Abc_NtkPlayerCostOneLevel( pLevelCostsR[i], RankCost ); - } - assert( CostTotal == CostTotalR ); - // print out statistics - if ( fVerbose ) - { - for ( i = 1; i <= nLevels; i++ ) - { - printf( "Level %2d : Cost = %7d. Ranks = %6.3f. Cost = %7d. Ranks = %6.3f.\n", i, - pLevelCosts[i], ((double)pLevelCosts[i])/RankCost, - pLevelCostsR[nLevels+1-i], ((double)pLevelCostsR[nLevels+1-i])/RankCost ); - } - printf( "TOTAL : Cost = %7d. Ranks = %6d. RanksR = %5d. RanksBest = %5d.\n", - CostTotal, nRanksTotal, nRanksTotalR, nLevels ); - } - free( pLevelCosts ); - free( pLevelCostsR ); - return nRanksTotal; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - diff --git a/src/temp/player/playerUtil.c b/src/temp/player/playerUtil.c deleted file mode 100644 index 1c8aeec2..00000000 --- a/src/temp/player/playerUtil.c +++ /dev/null @@ -1,353 +0,0 @@ -/**CFile**************************************************************** - - FileName [playerUtil.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [PLA decomposition package.] - - Synopsis [] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - May 11, 2006.] - - Revision [$Id: playerUtil.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "player.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Merges two supports.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Pla_ManMergeTwoSupports( Pla_Man_t * p, Vec_Int_t * vSupp0, Vec_Int_t * vSupp1, Vec_Int_t * vSupp ) -{ - int k0, k1; - - assert( vSupp0->nSize && vSupp1->nSize ); - - Vec_IntFill( p->vComTo0, vSupp0->nSize + vSupp1->nSize, -1 ); - Vec_IntFill( p->vComTo1, vSupp0->nSize + vSupp1->nSize, -1 ); - Vec_IntClear( p->vPairs0 ); - Vec_IntClear( p->vPairs1 ); - - vSupp->nSize = 0; - vSupp->nCap = vSupp0->nSize + vSupp1->nSize; - vSupp->pArray = ALLOC( int, vSupp->nCap ); - - for ( k0 = k1 = 0; k0 < vSupp0->nSize && k1 < vSupp1->nSize; ) - { - if ( vSupp0->pArray[k0] == vSupp1->pArray[k1] ) - { - Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 ); - Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 ); - Vec_IntPush( p->vPairs0, k0 ); - Vec_IntPush( p->vPairs1, k1 ); - Vec_IntPush( vSupp, vSupp0->pArray[k0] ); - k0++; k1++; - } - else if ( vSupp0->pArray[k0] < vSupp1->pArray[k1] ) - { - Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 ); - Vec_IntPush( vSupp, vSupp0->pArray[k0] ); - k0++; - } - else - { - Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 ); - Vec_IntPush( vSupp, vSupp1->pArray[k1] ); - k1++; - } - } - for ( ; k0 < vSupp0->nSize; k0++ ) - { - Vec_IntWriteEntry( p->vComTo0, vSupp->nSize, k0 ); - Vec_IntPush( vSupp, vSupp0->pArray[k0] ); - } - for ( ; k1 < vSupp1->nSize; k1++ ) - { - Vec_IntWriteEntry( p->vComTo1, vSupp->nSize, k1 ); - Vec_IntPush( vSupp, vSupp1->pArray[k1] ); - } -/* - printf( "Zero : " ); - for ( k = 0; k < vSupp0->nSize; k++ ) - printf( "%d ", vSupp0->pArray[k] ); - printf( "\n" ); - - printf( "One : " ); - for ( k = 0; k < vSupp1->nSize; k++ ) - printf( "%d ", vSupp1->pArray[k] ); - printf( "\n" ); - - printf( "Sum : " ); - for ( k = 0; k < vSupp->nSize; k++ ) - printf( "%d ", vSupp->pArray[k] ); - printf( "\n" ); - printf( "\n" ); -*/ - return Vec_IntSize(vSupp); -} - - -/**Function************************************************************* - - Synopsis [Computes the produce of two covers.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Esop_Cube_t * Pla_ManAndTwoCovers( Pla_Man_t * p, Esop_Cube_t * pCover0, Esop_Cube_t * pCover1, int nSupp, int fStopAtLimit ) -{ - Esop_Cube_t * pCube, * pCube0, * pCube1; - Esop_Cube_t * pCover; - int i, Val0, Val1; - assert( pCover0 != PLA_EMPTY && pCover1 != PLA_EMPTY ); - - // clean storage - assert( nSupp <= p->nPlaMax ); - Esop_ManClean( p->pManMin, nSupp ); - // go through the cube pairs - Esop_CoverForEachCube( pCover0, pCube0 ) - Esop_CoverForEachCube( pCover1, pCube1 ) - { - // go through the support variables of the cubes - for ( i = 0; i < p->vPairs0->nSize; i++ ) - { - Val0 = Esop_CubeGetVar( pCube0, p->vPairs0->pArray[i] ); - Val1 = Esop_CubeGetVar( pCube1, p->vPairs1->pArray[i] ); - if ( (Val0 & Val1) == 0 ) - break; - } - // check disjointness - if ( i < p->vPairs0->nSize ) - continue; - - if ( fStopAtLimit && p->pManMin->nCubes > p->nCubesMax ) - { - pCover = Esop_CoverCollect( p->pManMin, nSupp ); -//Esop_CoverWriteFile( pCover, "large", 1 ); - Esop_CoverRecycle( p->pManMin, pCover ); - return PLA_EMPTY; - } - - // create the product cube - pCube = Esop_CubeAlloc( p->pManMin ); - - // add the literals - pCube->nLits = 0; - for ( i = 0; i < nSupp; i++ ) - { - if ( p->vComTo0->pArray[i] == -1 ) - Val0 = 3; - else - Val0 = Esop_CubeGetVar( pCube0, p->vComTo0->pArray[i] ); - - if ( p->vComTo1->pArray[i] == -1 ) - Val1 = 3; - else - Val1 = Esop_CubeGetVar( pCube1, p->vComTo1->pArray[i] ); - - if ( (Val0 & Val1) == 3 ) - continue; - - Esop_CubeXorVar( pCube, i, (Val0 & Val1) ^ 3 ); - pCube->nLits++; - } - // add the cube to storage - Esop_EsopAddCube( p->pManMin, pCube ); - } - - // minimize the cover - Esop_EsopMinimize( p->pManMin ); - pCover = Esop_CoverCollect( p->pManMin, nSupp ); - - // quit if the cover is too large - if ( fStopAtLimit && Esop_CoverCountCubes(pCover) > p->nPlaMax ) - { - Esop_CoverRecycle( p->pManMin, pCover ); - return PLA_EMPTY; - } -// if ( pCover && pCover->nWords > 4 ) -// printf( "%d", pCover->nWords ); -// else -// printf( "." ); - return pCover; -} - -/**Function************************************************************* - - Synopsis [Computes the EXOR of two covers.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Esop_Cube_t * Pla_ManExorTwoCovers( Pla_Man_t * p, Esop_Cube_t * pCover0, Esop_Cube_t * pCover1, int nSupp, int fStopAtLimit ) -{ - Esop_Cube_t * pCube, * pCube0, * pCube1; - Esop_Cube_t * pCover; - int i, Val0, Val1; - assert( pCover0 != PLA_EMPTY && pCover1 != PLA_EMPTY ); - - // clean storage - assert( nSupp <= p->nPlaMax ); - Esop_ManClean( p->pManMin, nSupp ); - Esop_CoverForEachCube( pCover0, pCube0 ) - { - // create the cube - pCube = Esop_CubeAlloc( p->pManMin ); - pCube->nLits = 0; - for ( i = 0; i < p->vComTo0->nSize; i++ ) - { - if ( p->vComTo0->pArray[i] == -1 ) - continue; - Val0 = Esop_CubeGetVar( pCube0, p->vComTo0->pArray[i] ); - if ( Val0 == 3 ) - continue; - Esop_CubeXorVar( pCube, i, Val0 ^ 3 ); - pCube->nLits++; - } - if ( fStopAtLimit && p->pManMin->nCubes > p->nCubesMax ) - { - pCover = Esop_CoverCollect( p->pManMin, nSupp ); - Esop_CoverRecycle( p->pManMin, pCover ); - return PLA_EMPTY; - } - // add the cube to storage - Esop_EsopAddCube( p->pManMin, pCube ); - } - Esop_CoverForEachCube( pCover1, pCube1 ) - { - // create the cube - pCube = Esop_CubeAlloc( p->pManMin ); - pCube->nLits = 0; - for ( i = 0; i < p->vComTo1->nSize; i++ ) - { - if ( p->vComTo1->pArray[i] == -1 ) - continue; - Val1 = Esop_CubeGetVar( pCube1, p->vComTo1->pArray[i] ); - if ( Val1 == 3 ) - continue; - Esop_CubeXorVar( pCube, i, Val1 ^ 3 ); - pCube->nLits++; - } - if ( fStopAtLimit && p->pManMin->nCubes > p->nCubesMax ) - { - pCover = Esop_CoverCollect( p->pManMin, nSupp ); - Esop_CoverRecycle( p->pManMin, pCover ); - return PLA_EMPTY; - } - // add the cube to storage - Esop_EsopAddCube( p->pManMin, pCube ); - } - - // minimize the cover - Esop_EsopMinimize( p->pManMin ); - pCover = Esop_CoverCollect( p->pManMin, nSupp ); - - // quit if the cover is too large - if ( fStopAtLimit && Esop_CoverCountCubes(pCover) > p->nPlaMax ) - { - Esop_CoverRecycle( p->pManMin, pCover ); - return PLA_EMPTY; - } - return pCover; -} - -#if 0 - -/**Function************************************************************* - - Synopsis [Computes area/delay of the mapping.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Pla_ManComputeStats( Ivy_Man_t * p, Vec_Int_t * vNodes ) -{ - Ivy_Obj_t * pObj, * pFanin; - Vec_Int_t * vFanins; - int Area, Delay, Fanin, nFanins, i, k; - - Delay = Area = 0; - // compute levels and area - Ivy_ManForEachPi( p, pObj, i ) - pObj->Level = 0; - Ivy_ManForEachNodeVec( p, vNodes, pObj, i ) - { - // compute level of the node - pObj->Level = 0; - vFanins = Ivy_ObjGetFanins( pObj ); - Vec_IntForEachEntry( vFanins, Fanin, k ) - { - pFanin = Ivy_ManObj(p, Ivy_EdgeId(Fanin)); - pObj->Level = IVY_MAX( pObj->Level, pFanin->Level ); - } - pObj->Level += 1; - // compute area of the node - nFanins = Ivy_ObjFaninNum( pObj ); - if ( nFanins <= 4 ) - Area += 1; - else if ( nFanins <= 6 ) - Area += 2; - else if ( nFanins <= 8 ) - Area += 4; - else if ( nFanins <= 16 ) - Area += 8; - else if ( nFanins <= 32 ) - Area += 16; - else if ( nFanins <= 64 ) - Area += 32; - else if ( nFanins <= 128 ) - Area += 64; - else - assert( 0 ); - } - Ivy_ManForEachPo( p, pObj, i ) - { - Fanin = Ivy_ObjReadFanin(pObj, 0); - pFanin = Ivy_ManObj( p, Ivy_EdgeId(Fanin) ); - pObj->Level = pFanin->Level; - Delay = IVY_MAX( Delay, (int)pObj->Level ); - } - printf( "Area = %d. Delay = %d.\n", Area, Delay ); -} - -#endif - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |