diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2006-02-20 08:01:00 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2006-02-20 08:01:00 -0800 |
commit | 8eef7f8326e715ea4e9e84f46487cf4657601c25 (patch) | |
tree | 03a394e5a245bd3c0ed0b6397275c5b029adfb41 /src/base | |
parent | 77d7377442c28fd5c65144d7ea23938600967b2b (diff) | |
download | abc-8eef7f8326e715ea4e9e84f46487cf4657601c25.tar.gz abc-8eef7f8326e715ea4e9e84f46487cf4657601c25.tar.bz2 abc-8eef7f8326e715ea4e9e84f46487cf4657601c25.zip |
Version abc60220
Diffstat (limited to 'src/base')
49 files changed, 3074 insertions, 1218 deletions
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 7ace4880..e36f133e 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -410,6 +410,8 @@ extern bool Abc_AigCheck( Abc_Aig_t * pMan ); extern int Abc_AigGetLevelNum( Abc_Ntk_t * pNtk ); extern Abc_Obj_t * Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ); extern Abc_Obj_t * Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ); +extern Abc_Obj_t * Abc_AigXorLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1, int * pType ); +extern Abc_Obj_t * Abc_AigMuxLookup( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * pT, Abc_Obj_t * pE, int * pType ); extern Abc_Obj_t * Abc_AigOr( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ); extern Abc_Obj_t * Abc_AigXor( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ); extern Abc_Obj_t * Abc_AigMiter( Abc_Aig_t * pMan, Vec_Ptr_t * vPairs ); @@ -425,7 +427,7 @@ extern void Abc_AigSetNodePhases( Abc_Ntk_t * pNtk ); /*=== abcAttach.c ==========================================================*/ extern int Abc_NtkAttach( Abc_Ntk_t * pNtk ); /*=== abcBalance.c ==========================================================*/ -extern Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective ); +extern Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective, bool fUpdateLevel ); /*=== abcCheck.c ==========================================================*/ extern bool Abc_NtkCheck( Abc_Ntk_t * pNtk ); extern bool Abc_NtkCheckRead( Abc_Ntk_t * pNtk ); @@ -435,7 +437,7 @@ extern bool Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * /*=== abcCollapse.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose ); /*=== abcCut.c ==========================================================*/ -extern void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj ); +extern void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fMulti ); extern void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fMulti ); extern void Abc_NodeGetCutsSeq( void * p, Abc_Obj_t * pObj, int fFirst ); extern void * Abc_NodeReadCuts( void * p, Abc_Obj_t * pObj ); @@ -559,8 +561,9 @@ extern void Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkStartRead( char * pName ); extern void Abc_NtkFinalizeRead( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ); -extern Abc_Ntk_t * Abc_NtkCreateOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis ); -extern Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues ); +extern Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNodeName, int fUseAllCis ); +extern Abc_Ntk_t * Abc_NtkCreateMffc( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNodeName ); +extern Abc_Ntk_t * Abc_NtkCreateTarget( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues ); extern Abc_Ntk_t * Abc_NtkCreateFromNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode ); extern Abc_Ntk_t * Abc_NtkCreateWithNode( char * pSop ); extern void Abc_NtkDelete( Abc_Ntk_t * pNtk ); @@ -575,6 +578,8 @@ extern void Abc_NtkPrintFactor( FILE * pFile, Abc_Ntk_t * pNtk, in extern void Abc_NodePrintFactor( FILE * pFile, Abc_Obj_t * pNode, int fUseRealNames ); extern void Abc_NtkPrintLevel( FILE * pFile, Abc_Ntk_t * pNtk, int fProfile, int fListNodes ); extern void Abc_NodePrintLevel( FILE * pFile, Abc_Obj_t * pNode ); +/*=== abcProve.c ==========================================================*/ +extern int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fUseRewrite, int fUseFraig, int fVerbose ); /*=== abcReconv.c ==========================================================*/ extern Abc_ManCut_t * Abc_NtkManCutStart( int nNodeSizeMax, int nConeSizeMax, int nNodeFanStop, int nConeFanStop ); extern void Abc_NtkManCutStop( Abc_ManCut_t * p ); @@ -590,13 +595,14 @@ extern int Abc_NodeMffcSize( Abc_Obj_t * pNode ); extern int Abc_NodeMffcSizeSupp( Abc_Obj_t * pNode ); extern int Abc_NodeMffcSizeStop( Abc_Obj_t * pNode ); extern int Abc_NodeMffcLabel( Abc_Obj_t * pNode ); -extern int Abc_NodeMffcLabelFast( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); -extern Vec_Ptr_t * Abc_NodeMffcCollect( Abc_Obj_t * pNode ); +extern void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp ); +extern int Abc_NodeDeref_rec( Abc_Obj_t * pNode ); +extern int Abc_NodeRef_rec( Abc_Obj_t * pNode ); /*=== abcRenode.c ==========================================================*/ extern Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple ); extern DdNode * Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld ); /*=== abcSat.c ==========================================================*/ -extern int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ); +extern int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fVerbose ); extern solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk ); /*=== abcSop.c ==========================================================*/ extern char * Abc_SopRegister( Extra_MmFlex_t * pMan, char * pName ); @@ -681,6 +687,7 @@ extern int Abc_NtkLogicMakeSimpleCos( Abc_Ntk_t * pNtk, bool fDup extern void Abc_VecObjPushUniqueOrderByLevel( Vec_Ptr_t * p, Abc_Obj_t * pNode ); extern bool Abc_NodeIsExorType( Abc_Obj_t * pNode ); extern bool Abc_NodeIsMuxType( Abc_Obj_t * pNode ); +extern bool Abc_NodeIsMuxControlType( Abc_Obj_t * pNode ); extern Abc_Obj_t * Abc_NodeRecognizeMux( Abc_Obj_t * pNode, Abc_Obj_t ** ppNodeT, Abc_Obj_t ** ppNodeE ); 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 ); diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c index 167e7552..e5f39127 100644 --- a/src/base/abc/abcAig.c +++ b/src/base/abc/abcAig.c @@ -54,7 +54,6 @@ struct Abc_Aig_t_ int nBins; // the size of the table int nEntries; // the total number of entries in the table Vec_Ptr_t * vNodes; // the temporary array of nodes - Vec_Ptr_t * vStackDelete; // the nodes to be deleted Vec_Ptr_t * vStackReplaceOld; // the nodes to be replaced Vec_Ptr_t * vStackReplaceNew; // the nodes to be used for replacement Vec_Vec_t * vLevels; // the nodes to be updated @@ -83,8 +82,7 @@ static Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_O static void Abc_AigAndDelete( Abc_Aig_t * pMan, Abc_Obj_t * pThis ); static void Abc_AigResize( Abc_Aig_t * pMan ); // incremental AIG procedures -static void Abc_AigReplace_int( Abc_Aig_t * pMan, int fUpdateLevel ); -static void Abc_AigDelete_int( Abc_Aig_t * pMan ); +static void Abc_AigReplace_int( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int fUpdateLevel ); static void Abc_AigUpdateLevel_int( Abc_Aig_t * pMan ); static void Abc_AigUpdateLevelR_int( Abc_Aig_t * pMan ); static void Abc_AigRemoveFromLevelStructure( Vec_Vec_t * vStruct, Abc_Obj_t * pNode ); @@ -116,7 +114,6 @@ Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig ) pMan->pBins = ALLOC( Abc_Obj_t *, pMan->nBins ); memset( pMan->pBins, 0, sizeof(Abc_Obj_t *) * pMan->nBins ); pMan->vNodes = Vec_PtrAlloc( 100 ); - pMan->vStackDelete = Vec_PtrAlloc( 100 ); pMan->vStackReplaceOld = Vec_PtrAlloc( 100 ); pMan->vStackReplaceNew = Vec_PtrAlloc( 100 ); pMan->vLevels = Vec_VecAlloc( 100 ); @@ -139,13 +136,11 @@ Abc_Aig_t * Abc_AigAlloc( Abc_Ntk_t * pNtkAig ) ***********************************************************************/ void Abc_AigFree( Abc_Aig_t * pMan ) { - assert( Vec_PtrSize( pMan->vStackDelete ) == 0 ); assert( Vec_PtrSize( pMan->vStackReplaceOld ) == 0 ); assert( Vec_PtrSize( pMan->vStackReplaceNew ) == 0 ); // free the table Vec_VecFree( pMan->vLevels ); Vec_VecFree( pMan->vLevelsR ); - Vec_PtrFree( pMan->vStackDelete ); Vec_PtrFree( pMan->vStackReplaceOld ); Vec_PtrFree( pMan->vStackReplaceNew ); Vec_PtrFree( pMan->vNodes ); @@ -166,18 +161,21 @@ void Abc_AigFree( Abc_Aig_t * pMan ) ***********************************************************************/ int Abc_AigCleanup( Abc_Aig_t * pMan ) { + Vec_Ptr_t * vDangles; Abc_Obj_t * pAnd; - int i, Counter; + int i, nNodesOld; + nNodesOld = pMan->nEntries; // collect the AND nodes that do not fanout - assert( Vec_PtrSize( pMan->vStackDelete ) == 0 ); + vDangles = Vec_PtrAlloc( 100 ); for ( i = 0; i < pMan->nBins; i++ ) Abc_AigBinForEachEntry( pMan->pBins[i], pAnd ) if ( Abc_ObjFanoutNum(pAnd) == 0 ) - Vec_PtrPush( pMan->vStackDelete, pAnd ); + Vec_PtrPush( vDangles, pAnd ); // process the dangling nodes and their MFFCs - for ( Counter = 0; Vec_PtrSize(pMan->vStackDelete) > 0; Counter++ ) - Abc_AigDelete_int( pMan ); - return Counter; + Vec_PtrForEachEntry( vDangles, pAnd, i ) + Abc_AigDeleteNode( pMan, pAnd ); + Vec_PtrFree( vDangles ); + return nNodesOld - pMan->nEntries; } /**Function************************************************************* @@ -383,6 +381,74 @@ Abc_Obj_t * Abc_AigAndLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 ) /**Function************************************************************* + Synopsis [Returns the gate implementing EXOR of the two arguments if it exists.] + + Description [The argument nodes can be complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_AigXorLookup( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1, int * pType ) +{ + Abc_Obj_t * pNode1, * pNode2, * pNode; + // set the flag to zero + if ( pType ) *pType = 0; + // check the case of XOR(a,b) = OR(ab, a'b')' + if ( (pNode1 = Abc_AigAndLookup(pMan, Abc_ObjNot(p0), Abc_ObjNot(p1))) && + (pNode2 = Abc_AigAndLookup(pMan, p0, p1)) ) + { + pNode = Abc_AigAndLookup( pMan, Abc_ObjNot(pNode1), Abc_ObjNot(pNode2) ); + if ( pNode && pType ) *pType = 1; + return pNode; + } + // check the case of XOR(a,b) = OR(a'b, ab') + if ( (pNode1 = Abc_AigAndLookup(pMan, p0, Abc_ObjNot(p1))) && + (pNode2 = Abc_AigAndLookup(pMan, Abc_ObjNot(p0), p1)) ) + { + pNode = Abc_AigAndLookup( pMan, Abc_ObjNot(pNode1), Abc_ObjNot(pNode2) ); + return pNode? Abc_ObjNot(pNode) : NULL; + } + return NULL; +} + +/**Function************************************************************* + + Synopsis [Returns the gate implementing EXOR of the two arguments if it exists.] + + Description [The argument nodes can be complemented.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Abc_AigMuxLookup( Abc_Aig_t * pMan, Abc_Obj_t * pC, Abc_Obj_t * pT, Abc_Obj_t * pE, int * pType ) +{ + Abc_Obj_t * pNode1, * pNode2, * pNode; + // set the flag to zero + if ( pType ) *pType = 0; + // check the case of MUX(c,t,e) = OR(ct', c'e')' + if ( (pNode1 = Abc_AigAndLookup(pMan, pC, Abc_ObjNot(pT))) && + (pNode2 = Abc_AigAndLookup(pMan, Abc_ObjNot(pC), Abc_ObjNot(pE))) ) + { + pNode = Abc_AigAndLookup( pMan, Abc_ObjNot(pNode1), Abc_ObjNot(pNode2) ); + if ( pNode && pType ) *pType = 1; + return pNode; + } + // check the case of MUX(c,t,e) = OR(ct, c'e) + if ( (pNode1 = Abc_AigAndLookup(pMan, pC, pT)) && + (pNode2 = Abc_AigAndLookup(pMan, Abc_ObjNot(pC), pE)) ) + { + pNode = Abc_AigAndLookup( pMan, Abc_ObjNot(pNode1), Abc_ObjNot(pNode2) ); + return pNode? Abc_ObjNot(pNode) : NULL; + } + return NULL; +} + +/**Function************************************************************* + Synopsis [Deletes an AIG node from the hash table.] Description [] @@ -662,11 +728,16 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, bool { assert( Vec_PtrSize(pMan->vStackReplaceOld) == 0 ); assert( Vec_PtrSize(pMan->vStackReplaceNew) == 0 ); - assert( Vec_PtrSize(pMan->vStackDelete) == 0 ); Vec_PtrPush( pMan->vStackReplaceOld, pOld ); Vec_PtrPush( pMan->vStackReplaceNew, pNew ); + assert( !Abc_ObjIsComplement(pOld) ); + // process the replacements while ( Vec_PtrSize(pMan->vStackReplaceOld) ) - Abc_AigReplace_int( pMan, fUpdateLevel ); + { + pOld = Vec_PtrPop( pMan->vStackReplaceOld ); + pNew = Vec_PtrPop( pMan->vStackReplaceNew ); + Abc_AigReplace_int( pMan, pOld, pNew, fUpdateLevel ); + } if ( fUpdateLevel ) { Abc_AigUpdateLevel_int( pMan ); @@ -685,14 +756,10 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, bool SeeAlso [] ***********************************************************************/ -void Abc_AigReplace_int( Abc_Aig_t * pMan, int fUpdateLevel ) +void Abc_AigReplace_int( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int fUpdateLevel ) { - Abc_Obj_t * pOld, * pNew, * pFanin1, * pFanin2, * pFanout, * pFanoutNew, * pFanoutFanout; - int k, v, iFanin; - // get the pair of nodes to replace - assert( Vec_PtrSize(pMan->vStackReplaceOld) > 0 ); - pOld = Vec_PtrPop( pMan->vStackReplaceOld ); - pNew = Vec_PtrPop( pMan->vStackReplaceNew ); + Abc_Obj_t * pFanin1, * pFanin2, * pFanout, * pFanoutNew, * pFanoutFanout; + int k, v, iFanin; // make sure the old node is regular and has fanouts // (the new node can be complemented and can have fanouts) assert( !Abc_ObjIsComplement(pOld) ); @@ -775,88 +842,58 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan, int fUpdateLevel ) SeeAlso [] ***********************************************************************/ -void Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pOld ) -{ - assert( Vec_PtrSize(pMan->vStackDelete) == 0 ); - Vec_PtrPush( pMan->vStackDelete, pOld ); - while ( Vec_PtrSize(pMan->vStackDelete) ) - Abc_AigDelete_int( pMan ); -} - -/**Function************************************************************* - - Synopsis [Performs internal deletion step.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_AigDelete_int( Abc_Aig_t * pMan ) +void Abc_AigDeleteNode( Abc_Aig_t * pMan, Abc_Obj_t * pNode ) { - Vec_Ptr_t * vNodes; - Abc_Obj_t * pRoot, * pObj; - int k; - // get the node to delete - assert( Vec_PtrSize(pMan->vStackDelete) > 0 ); - pRoot = Vec_PtrPop( pMan->vStackDelete ); + Abc_Obj_t * pNode0, * pNode1, * pTemp; + int i, k; // make sure the node is regular and dangling - assert( !Abc_ObjIsComplement(pRoot) ); - assert( Abc_ObjIsNode(pRoot) ); - assert( Abc_ObjFaninNum(pRoot) == 2 ); - assert( Abc_ObjFanoutNum(pRoot) == 0 ); - - // collect the MFFC - vNodes = Abc_NodeMffcCollect( pRoot ); - - // if reverse levels are specified, schedule fanins of MFFC for updating - // currently, we do not do it because we do not know the correct level of the fanins - // also, it is unlikely that this will make a difference since we are - // processing the network forward while at this point fanins are left behind... -/* - if ( pObj->pNtk->vLevelsR ) - Vec_PtrForEachEntry( vNodes, pObj, k ) + assert( !Abc_ObjIsComplement(pNode) ); + assert( Abc_ObjIsNode(pNode) ); + assert( Abc_ObjFaninNum(pNode) == 2 ); + assert( Abc_ObjFanoutNum(pNode) == 0 ); + + // when deleting an old node that is scheduled for replacement, remove it from the replacement queue + Vec_PtrForEachEntry( pMan->vStackReplaceOld, pTemp, i ) + if ( pNode == pTemp ) { - Abc_Obj_t * pFanin; - if ( Abc_ObjIsCi(pObj) ) - continue; - pFanin = Abc_ObjFanin0(pObj); - if ( pFanin->fMarkB == 0 ) - { - pFanin->fMarkB = 1; - Vec_VecPush( pMan->vLevelsR, Abc_NodeReadReverseLevel(pFanin), pFanin ); - } - pFanin = Abc_ObjFanin1(pObj); - if ( pFanin->fMarkB == 0 ) + // remove the entry from the replacement array + for ( k = i; k < pMan->vStackReplaceOld->nSize - 1; k++ ) { - pFanin->fMarkB = 1; - Vec_VecPush( pMan->vLevelsR, Abc_NodeReadReverseLevel(pFanin), pFanin ); + pMan->vStackReplaceOld->pArray[k] = pMan->vStackReplaceOld->pArray[k+1]; + pMan->vStackReplaceNew->pArray[k] = pMan->vStackReplaceNew->pArray[k+1]; } + pMan->vStackReplaceOld->nSize--; + pMan->vStackReplaceNew->nSize--; } -*/ - // delete the nodes in MFFC - Vec_PtrForEachEntry( vNodes, pObj, k ) - { - if ( Abc_ObjIsCi(pObj) ) - continue; - assert( Abc_ObjFanoutNum(pObj) == 0 ); - // remove the node from the table - Abc_AigAndDelete( pMan, pObj ); - // if the node is in the level structure, remove it - if ( pObj->fMarkA ) - Abc_AigRemoveFromLevelStructure( pMan->vLevels, pObj ); - if ( pObj->fMarkB ) - Abc_AigRemoveFromLevelStructureR( pMan->vLevelsR, pObj ); - // remove the node from the network - Abc_NtkDeleteObj( pObj ); - } - Vec_PtrFree( vNodes ); + // when deleting a new node that should replace another node, do not delete + Vec_PtrForEachEntry( pMan->vStackReplaceNew, pTemp, i ) + if ( pNode == Abc_ObjRegular(pTemp) ) + return; + + // remember the node's fanins + pNode0 = Abc_ObjFanin0( pNode ); + pNode1 = Abc_ObjFanin1( pNode ); + + // remove the node from the table + Abc_AigAndDelete( pMan, pNode ); + // if the node is in the level structure, remove it + if ( pNode->fMarkA ) + Abc_AigRemoveFromLevelStructure( pMan->vLevels, pNode ); + if ( pNode->fMarkB ) + Abc_AigRemoveFromLevelStructureR( pMan->vLevelsR, pNode ); + // remove the node from the network + Abc_NtkDeleteObj( pNode ); + + // call recursively for the fanins + if ( Abc_ObjIsNode(pNode0) && pNode0->vFanouts.nSize == 0 ) + Abc_AigDeleteNode( pMan, pNode0 ); + if ( Abc_ObjIsNode(pNode1) && pNode1->vFanouts.nSize == 0 ) + Abc_AigDeleteNode( pMan, pNode1 ); } + /**Function************************************************************* Synopsis [Updates the level of the node after it has changed.] diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c index b366890f..ccbd2c85 100644 --- a/src/base/abc/abcNames.c +++ b/src/base/abc/abcNames.c @@ -306,7 +306,7 @@ Vec_Ptr_t * Abc_NodeGetFaninNames( Abc_Obj_t * pNode ) int i; vNodes = Vec_PtrAlloc( 100 ); Abc_ObjForEachFanin( pNode, pFanin, i ) - Vec_PtrPush( vNodes, util_strsav(Abc_ObjName(pFanin)) ); + Vec_PtrPush( vNodes, Extra_UtilStrsav(Abc_ObjName(pFanin)) ); return vNodes; } @@ -341,7 +341,7 @@ Vec_Ptr_t * Abc_NodeGetFakeNames( int nNames ) Buffer[1] = '0' + i/26; Buffer[2] = 0; } - Vec_PtrPush( vNames, util_strsav(Buffer) ); + Vec_PtrPush( vNames, Extra_UtilStrsav(Buffer) ); } return vNames; } diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index 82367c09..31b4c5f4 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -117,8 +117,8 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_ // start the network pNtkNew = Abc_NtkAlloc( Type, Func ); // duplicate the name and the spec - pNtkNew->pName = util_strsav(pNtk->pName); - pNtkNew->pSpec = util_strsav(pNtk->pSpec); + pNtkNew->pName = Extra_UtilStrsav(pNtk->pName); + pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec); // clean the node copy fields Abc_NtkForEachNode( pNtk, pObj, i ) pObj->pCopy = NULL; @@ -235,8 +235,8 @@ Abc_Ntk_t * Abc_NtkStartRead( char * pName ) // allocate the empty network pNtkNew = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP ); // set the specs - pNtkNew->pName = util_strsav( Extra_FileNameGeneric(pName) ); - pNtkNew->pSpec = util_strsav( pName ); + pNtkNew->pName = Extra_FileNameGeneric(pName); + pNtkNew->pSpec = Extra_UtilStrsav(pName); return pNtkNew; } @@ -359,7 +359,7 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ) /**Function************************************************************* - Synopsis [Creates the network composed of one output.] + Synopsis [Creates the network composed of one logic cone.] Description [] @@ -368,22 +368,22 @@ Abc_Ntk_t * Abc_NtkDup( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkCreateOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAllCis ) +Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNodeName, int fUseAllCis ) { - Vec_Ptr_t * vNodes; Abc_Ntk_t * pNtkNew; - Abc_Obj_t * pObj, * pFanin; + Vec_Ptr_t * vNodes; + Abc_Obj_t * pObj, * pFanin, * pNodeCoNew; char Buffer[1000]; int i, k; assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) ); - assert( Abc_ObjIsCo(pNode) ); + assert( Abc_ObjIsNode(pNode) ); // start the network pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc ); // set the name - sprintf( Buffer, "%s_%s", pNtk->pName, Abc_ObjName(pNode) ); - pNtkNew->pName = util_strsav(Buffer); + sprintf( Buffer, "%s_%s", pNtk->pName, pNodeName ); + pNtkNew->pName = Extra_UtilStrsav(Buffer); // establish connection between the constant nodes Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew); @@ -399,7 +399,9 @@ Abc_Ntk_t * Abc_NtkCreateOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAl Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) ); } } - + // add the PO corresponding to this output + pNodeCoNew = Abc_NtkCreatePo( pNtkNew ); + Abc_NtkLogicStoreName( pNodeCoNew, pNodeName ); // copy the nodes Vec_PtrForEachEntry( vNodes, pObj, i ) { @@ -415,15 +417,83 @@ Abc_Ntk_t * Abc_NtkCreateOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAl Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy ); } } + // connect the internal nodes to the new CO + Abc_ObjAddFanin( pNodeCoNew, pNode->pCopy ); Vec_PtrFree( vNodes ); - // add the PO corresponding to this output - pNode->pCopy = Abc_NtkCreatePo( pNtkNew ); - Abc_ObjAddFanin( pNode->pCopy, Abc_ObjFanin0(pNode)->pCopy ); - Abc_NtkLogicStoreName( pNode->pCopy, Abc_ObjName(pNode) ); + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Creates the network composed of MFFC of one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkCreateMffc( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, char * pNodeName ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObj, * pFanin, * pNodeCoNew; + Vec_Ptr_t * vCone, * vSupp; + char Buffer[1000]; + int i, k; + + assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) ); + assert( Abc_ObjIsNode(pNode) ); + + // start the network + pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc ); + // set the name + sprintf( Buffer, "%s_%s", pNtk->pName, pNodeName ); + pNtkNew->pName = Extra_UtilStrsav(Buffer); + + // establish connection between the constant nodes + Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew); + + // collect the nodes in MFFC + vCone = Vec_PtrAlloc( 100 ); + vSupp = Vec_PtrAlloc( 100 ); + Abc_NodeDeref_rec( pNode ); + Abc_NodeMffsConeSupp( pNode, vCone, vSupp ); + Abc_NodeRef_rec( pNode ); + // create the PIs + Vec_PtrForEachEntry( vSupp, pObj, i ) + { + pObj->pCopy = Abc_NtkCreatePi(pNtkNew); + Abc_NtkLogicStoreName( pObj->pCopy, Abc_ObjName(pObj) ); + } + // create the PO + pNodeCoNew = Abc_NtkCreatePo( pNtkNew ); + Abc_NtkLogicStoreName( pNodeCoNew, pNodeName ); + // copy the nodes + Vec_PtrForEachEntry( vCone, pObj, i ) + { + // if it is an AIG, add to the hash table + if ( Abc_NtkIsStrash(pNtk) ) + { + pObj->pCopy = Abc_AigAnd( pNtkNew->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) ); + } + else + { + Abc_NtkDupObj( pNtkNew, pObj ); + Abc_ObjForEachFanin( pObj, pFanin, k ) + Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy ); + } + } + // connect the topmost node + Abc_ObjAddFanin( pNodeCoNew, pNode->pCopy ); + Vec_PtrFree( vCone ); + Vec_PtrFree( vSupp ); if ( !Abc_NtkCheck( pNtkNew ) ) - fprintf( stdout, "Abc_NtkCreateOutput(): Network check has failed.\n" ); + fprintf( stdout, "Abc_NtkCreateMffc(): Network check has failed.\n" ); return pNtkNew; } @@ -438,7 +508,7 @@ Abc_Ntk_t * Abc_NtkCreateOutput( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode, int fUseAl SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues ) +Abc_Ntk_t * Abc_NtkCreateTarget( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * vValues ) { Vec_Ptr_t * vNodes; Abc_Ntk_t * pNtkNew; @@ -450,7 +520,7 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * // start the network Abc_NtkCleanCopy( pNtk ); pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG ); - pNtkNew->pName = util_strsav(pNtk->pName); + pNtkNew->pName = Extra_UtilStrsav(pNtk->pName); // collect the nodes in the TFI of the output vNodes = Abc_NtkDfsNodes( pNtk, (Abc_Obj_t **)vRoots->pArray, vRoots->nSize ); @@ -483,7 +553,7 @@ Abc_Ntk_t * Abc_NtkCreateCone( Abc_Ntk_t * pNtk, Vec_Ptr_t * vRoots, Vec_Int_t * Abc_ObjAddFanin( pNodePo, pFinal ); Abc_NtkLogicStoreName( pNodePo, "miter" ); if ( !Abc_NtkCheck( pNtkNew ) ) - fprintf( stdout, "Abc_NtkCreateCone(): Network check has failed.\n" ); + fprintf( stdout, "Abc_NtkCreateTarget(): Network check has failed.\n" ); return pNtkNew; } @@ -505,7 +575,7 @@ Abc_Ntk_t * Abc_NtkCreateFromNode( Abc_Ntk_t * pNtk, Abc_Obj_t * pNode ) int i; // start the network pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc ); - pNtkNew->pName = util_strsav(Abc_ObjName(pNode)); + pNtkNew->pName = Extra_UtilStrsav(Abc_ObjName(pNode)); // add the PIs corresponding to the fanins of the node Abc_ObjForEachFanin( pNode, pFanin, i ) { @@ -544,7 +614,7 @@ Abc_Ntk_t * Abc_NtkCreateWithNode( char * pSop ) int i, nVars; // start the network pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_SOP ); - pNtkNew->pName = util_strsav("ex"); + pNtkNew->pName = Extra_UtilStrsav("ex"); // create PIs Vec_PtrPush( pNtkNew->vObjs, NULL ); nVars = Abc_SopGetVarNum( pSop ); diff --git a/src/base/abc/abcRefs.c b/src/base/abc/abcRefs.c index 5d0c68d1..808bfae8 100644 --- a/src/base/abc/abcRefs.c +++ b/src/base/abc/abcRefs.c @@ -24,10 +24,8 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t * vNodes ); -static int Abc_NodeMffcCountSupp( Vec_Ptr_t * vNodes ); +static int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel ); static int Abc_NodeRefDerefStop( Abc_Obj_t * pNode, bool fReference ); -static int Abc_NodeDeref( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -52,8 +50,8 @@ int Abc_NodeMffcSize( Abc_Obj_t * pNode ) assert( Abc_ObjIsNode( pNode ) ); if ( Abc_ObjFaninNum(pNode) == 0 ) return 0; - nConeSize1 = Abc_NodeRefDeref( pNode, 0, 0, NULL ); // dereference - nConeSize2 = Abc_NodeRefDeref( pNode, 1, 0, NULL ); // reference + nConeSize1 = Abc_NodeRefDeref( pNode, 0, 0 ); // dereference + nConeSize2 = Abc_NodeRefDeref( pNode, 1, 0 ); // reference assert( nConeSize1 == nConeSize2 ); assert( nConeSize1 > 0 ); return nConeSize1; @@ -61,36 +59,6 @@ int Abc_NodeMffcSize( Abc_Obj_t * pNode ) /**Function************************************************************* - Synopsis [Returns the MFFC size.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NodeMffcSizeSupp( Abc_Obj_t * pNode ) -{ - Vec_Ptr_t * vNodes; - int nSuppSize, nConeSize1, nConeSize2; - assert( Abc_NtkIsStrash(pNode->pNtk) ); - assert( !Abc_ObjIsComplement( pNode ) ); - assert( Abc_ObjIsNode( pNode ) ); - if ( Abc_ObjFaninNum(pNode) == 0 ) - return 0; - vNodes = Vec_PtrAlloc( 10 ); - nConeSize1 = Abc_NodeRefDeref( pNode, 0, 0, vNodes ); // dereference - nSuppSize = Abc_NodeMffcCountSupp(vNodes); - nConeSize2 = Abc_NodeRefDeref( pNode, 1, 0, NULL ); // reference - assert( nConeSize1 == nConeSize2 ); - assert( nConeSize1 > 0 ); - Vec_PtrFree(vNodes); - return nSuppSize; -} - -/**Function************************************************************* - Synopsis [Returns the MFFC size while stopping at the complemented edges.] Description [] @@ -129,12 +97,13 @@ int Abc_NodeMffcSizeStop( Abc_Obj_t * pNode ) int Abc_NodeMffcLabel( Abc_Obj_t * pNode ) { int nConeSize1, nConeSize2; + assert( Abc_NtkIsStrash(pNode->pNtk) ); assert( !Abc_ObjIsComplement( pNode ) ); assert( Abc_ObjIsNode( pNode ) ); if ( Abc_ObjFaninNum(pNode) == 0 ) return 0; - nConeSize1 = Abc_NodeRefDeref( pNode, 0, 1, NULL ); // dereference - nConeSize2 = Abc_NodeRefDeref( pNode, 1, 0, NULL ); // reference + nConeSize1 = Abc_NodeRefDeref( pNode, 0, 1 ); // dereference + nConeSize2 = Abc_NodeRefDeref( pNode, 1, 0 ); // reference assert( nConeSize1 == nConeSize2 ); assert( nConeSize1 > 0 ); return nConeSize1; @@ -142,88 +111,64 @@ int Abc_NodeMffcLabel( Abc_Obj_t * pNode ) /**Function************************************************************* - Synopsis [Returns the MFFC size.] + Synopsis [References/references the node and returns MFFC size.] - Description [Profiling shows that this procedure runs the same as - the above one, not faster.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -int Abc_NodeMffcLabelFast( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) +int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel ) { - Abc_Obj_t * pTemp; - int nConeSize, i; - - assert( !Abc_ObjIsComplement( pNode ) ); - assert( Abc_ObjIsNode( pNode ) ); - if ( Abc_ObjFaninNum(pNode) == 0 ) + Abc_Obj_t * pNode0, * pNode1; + int Counter; + // label visited nodes + if ( fLabel ) + Abc_NodeSetTravIdCurrent( pNode ); + // skip the CI + if ( Abc_ObjIsCi(pNode) ) return 0; - - Vec_PtrClear( vNodes ); - nConeSize = Abc_NodeDeref( pNode, vNodes ); - // label the nodes with the current ID and ref their children - Vec_PtrForEachEntry( vNodes, pTemp, i ) + // process the internal node + pNode0 = Abc_ObjFanin0(pNode); + pNode1 = Abc_ObjFanin1(pNode); + Counter = 1; + if ( fReference ) + { + if ( pNode0->vFanouts.nSize++ == 0 ) + Counter += Abc_NodeRefDeref( pNode0, fReference, fLabel ); + if ( pNode1->vFanouts.nSize++ == 0 ) + Counter += Abc_NodeRefDeref( pNode1, fReference, fLabel ); + } + else { - Abc_NodeSetTravIdCurrent( pTemp ); - if ( Abc_ObjIsCi(pTemp) ) - continue; - Abc_ObjFanin0(pTemp)->vFanouts.nSize++; - Abc_ObjFanin1(pTemp)->vFanouts.nSize++; + assert( pNode0->vFanouts.nSize > 0 ); + assert( pNode1->vFanouts.nSize > 0 ); + if ( --pNode0->vFanouts.nSize == 0 ) + Counter += Abc_NodeRefDeref( pNode0, fReference, fLabel ); + if ( --pNode1->vFanouts.nSize == 0 ) + Counter += Abc_NodeRefDeref( pNode1, fReference, fLabel ); } - return nConeSize; + return Counter; } -/**Function************************************************************* - - Synopsis [Collects the nodes in MFFC in the topological order.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Abc_NodeMffcCollect( Abc_Obj_t * pNode ) -{ - Vec_Ptr_t * vNodes; - int nConeSize1, nConeSize2; - assert( !Abc_ObjIsComplement( pNode ) ); - assert( Abc_ObjIsNode( pNode ) ); - vNodes = Vec_PtrAlloc( 8 ); - if ( Abc_ObjFaninNum(pNode) == 0 ) - return vNodes; - nConeSize1 = Abc_NodeRefDeref( pNode, 0, 0, vNodes ); // dereference - nConeSize2 = Abc_NodeRefDeref( pNode, 1, 0, NULL ); // reference - assert( nConeSize1 == nConeSize2 ); - assert( nConeSize1 > 0 ); - return vNodes; -} /**Function************************************************************* Synopsis [References/references the node and returns MFFC size.] - Description [] + Description [Stops at the complemented edges.] SideEffects [] SeeAlso [] ***********************************************************************/ -int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t * vNodes ) +int Abc_NodeRefDerefStop( Abc_Obj_t * pNode, bool fReference ) { Abc_Obj_t * pNode0, * pNode1; int Counter; - // label visited nodes - if ( fLabel ) - Abc_NodeSetTravIdCurrent( pNode ); - // collect visited nodes - if ( vNodes ) - Vec_PtrPush( vNodes, pNode ); // skip the CI if ( Abc_ObjIsCi(pNode) ) return 0; @@ -233,26 +178,29 @@ int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t Counter = 1; if ( fReference ) { - if ( pNode0->vFanouts.nSize++ == 0 ) - Counter += Abc_NodeRefDeref( pNode0, fReference, fLabel, vNodes ); - if ( pNode1->vFanouts.nSize++ == 0 ) - Counter += Abc_NodeRefDeref( pNode1, fReference, fLabel, vNodes ); + if ( pNode0->vFanouts.nSize++ == 0 && !Abc_ObjFaninC0(pNode) ) + Counter += Abc_NodeRefDerefStop( pNode0, fReference ); + if ( pNode1->vFanouts.nSize++ == 0 && !Abc_ObjFaninC1(pNode) ) + Counter += Abc_NodeRefDerefStop( pNode1, fReference ); } else { assert( pNode0->vFanouts.nSize > 0 ); assert( pNode1->vFanouts.nSize > 0 ); - if ( --pNode0->vFanouts.nSize == 0 ) - Counter += Abc_NodeRefDeref( pNode0, fReference, fLabel, vNodes ); - if ( --pNode1->vFanouts.nSize == 0 ) - Counter += Abc_NodeRefDeref( pNode1, fReference, fLabel, vNodes ); + if ( --pNode0->vFanouts.nSize == 0 && !Abc_ObjFaninC0(pNode) ) + Counter += Abc_NodeRefDerefStop( pNode0, fReference ); + if ( --pNode1->vFanouts.nSize == 0 && !Abc_ObjFaninC1(pNode) ) + Counter += Abc_NodeRefDerefStop( pNode1, fReference ); } return Counter; } + + + /**Function************************************************************* - Synopsis [References/references the node and returns MFFC supp size.] + Synopsis [Dereferences the node's MFFC.] Description [] @@ -261,53 +209,24 @@ int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fReference, bool fLabel, Vec_Ptr_t SeeAlso [] ***********************************************************************/ -int Abc_NodeMffcCountSupp( Vec_Ptr_t * vNodes ) +int Abc_NodeDeref_rec( Abc_Obj_t * pNode ) { - Abc_Obj_t * pNode, * pNode0, * pNode1; - int i, Counter = 0; - Vec_PtrForEachEntry( vNodes, pNode, i ) - { - if ( Abc_ObjIsCi(pNode) ) - { - if ( pNode->fMarkB == 0 ) - { - pNode->fMarkB = 1; - Counter++; - } - continue; - } - pNode0 = Abc_ObjFanin0(pNode); - if ( pNode0->vFanouts.nSize > 0 && pNode0->fMarkB == 0 ) - { - pNode0->fMarkB = 1; - Counter++; - } - pNode1 = Abc_ObjFanin1(pNode); - if ( pNode1->vFanouts.nSize > 0 && pNode1->fMarkB == 0 ) - { - pNode1->fMarkB = 1; - Counter++; - } - } - Vec_PtrForEachEntry( vNodes, pNode, i ) + Abc_Obj_t * pFanin; + int i, Counter = 1; + if ( Abc_ObjIsCi(pNode) ) + return 0; + Abc_ObjForEachFanin( pNode, pFanin, i ) { - if ( Abc_ObjIsCi(pNode) ) - { - pNode->fMarkB = 0; - continue; - } - pNode0 = Abc_ObjFanin0(pNode); - pNode0->fMarkB = 0; - pNode1 = Abc_ObjFanin1(pNode); - pNode1->fMarkB = 0; + assert( pFanin->vFanouts.nSize > 0 ); + if ( --pFanin->vFanouts.nSize == 0 ) + Counter += Abc_NodeDeref_rec( pFanin ); } return Counter; - } /**Function************************************************************* - Synopsis [References/references the node and returns MFFC size.] + Synopsis [References the node's MFFC.] Description [] @@ -316,69 +235,98 @@ int Abc_NodeMffcCountSupp( Vec_Ptr_t * vNodes ) SeeAlso [] ***********************************************************************/ -int Abc_NodeDeref( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) +int Abc_NodeRef_rec( Abc_Obj_t * pNode ) { - Abc_Obj_t * pNode0, * pNode1; - int Counter; - // collect visited nodes - Vec_PtrPush( vNodes, pNode ); - // skip the CI + Abc_Obj_t * pFanin; + int i, Counter = 1; if ( Abc_ObjIsCi(pNode) ) return 0; - // process the internal node - pNode0 = Abc_ObjFanin0(pNode); - pNode1 = Abc_ObjFanin1(pNode); - assert( pNode0->vFanouts.nSize > 0 ); - assert( pNode1->vFanouts.nSize > 0 ); - Counter = 1; - if ( --pNode0->vFanouts.nSize == 0 ) - Counter += Abc_NodeDeref( pNode0, vNodes ); - if ( --pNode1->vFanouts.nSize == 0 ) - Counter += Abc_NodeDeref( pNode1, vNodes ); + Abc_ObjForEachFanin( pNode, pFanin, i ) + { + if ( pFanin->vFanouts.nSize++ == 0 ) + Counter += Abc_NodeRef_rec( pFanin ); + } return Counter; } /**Function************************************************************* - Synopsis [References/references the node and returns MFFC size.] + Synopsis [Collects the internal and boundary nodes in the derefed MFFC.] - Description [Stops at the complemented edges.] + Description [] SideEffects [] SeeAlso [] ***********************************************************************/ -int Abc_NodeRefDerefStop( Abc_Obj_t * pNode, bool fReference ) +void Abc_NodeMffsConeSupp_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp, int fTopmost ) { - Abc_Obj_t * pNode0, * pNode1; - int Counter; - // skip the CI - if ( Abc_ObjIsCi(pNode) ) - return 0; - // process the internal node - pNode0 = Abc_ObjFanin0(pNode); - pNode1 = Abc_ObjFanin1(pNode); - Counter = 1; - if ( fReference ) - { - if ( pNode0->vFanouts.nSize++ == 0 && !Abc_ObjFaninC0(pNode) ) - Counter += Abc_NodeRefDerefStop( pNode0, fReference ); - if ( pNode1->vFanouts.nSize++ == 0 && !Abc_ObjFaninC1(pNode) ) - Counter += Abc_NodeRefDerefStop( pNode1, fReference ); - } - else + Abc_Obj_t * pFanin; + int i; + // skip visited nodes + if ( Abc_NodeIsTravIdCurrent(pNode) ) + return; + Abc_NodeSetTravIdCurrent(pNode); + // add to the new support nodes + if ( !fTopmost && (Abc_ObjIsCi(pNode) || pNode->vFanouts.nSize > 0) ) { - assert( pNode0->vFanouts.nSize > 0 ); - assert( pNode1->vFanouts.nSize > 0 ); - if ( --pNode0->vFanouts.nSize == 0 && !Abc_ObjFaninC0(pNode) ) - Counter += Abc_NodeRefDerefStop( pNode0, fReference ); - if ( --pNode1->vFanouts.nSize == 0 && !Abc_ObjFaninC1(pNode) ) - Counter += Abc_NodeRefDerefStop( pNode1, fReference ); + Vec_PtrPush( vSupp, pNode ); + return; } - return Counter; + // recur on the children + Abc_ObjForEachFanin( pNode, pFanin, i ) + Abc_NodeMffsConeSupp_rec( pFanin, vCone, vSupp, 0 ); + // collect the internal node + Vec_PtrPush( vCone, pNode ); +} + +/**Function************************************************************* + + Synopsis [Collects the support of the derefed MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * vCone, Vec_Ptr_t * vSupp ) +{ + assert( Abc_ObjIsNode(pNode) ); + assert( !Abc_ObjIsComplement(pNode) ); + Vec_PtrClear( vCone ); + Vec_PtrClear( vSupp ); + Abc_NtkIncrementTravId( pNode->pNtk ); + Abc_NodeMffsConeSupp_rec( pNode, vCone, vSupp, 1 ); +} + +/**Function************************************************************* + + Synopsis [Collects the support of the derefed MFFC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode ) +{ + Vec_Ptr_t * vCone, * vSupp; + vCone = Vec_PtrAlloc( 100 ); + vSupp = Vec_PtrAlloc( 100 ); + Abc_NodeDeref_rec( pNode ); + Abc_NodeMffsConeSupp( pNode, vCone, vSupp ); + Abc_NodeRef_rec( pNode ); + printf( "Cone = %6d. Supp = %6d. \n", Vec_PtrSize(vCone), Vec_PtrSize(vSupp) ); + Vec_PtrFree( vCone ); + Vec_PtrFree( vSupp ); } + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 1e52e4a6..122cf589 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -28,8 +28,6 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static int Abc_NodeRefDeref( Abc_Obj_t * pNode, bool fFanouts, bool fReference ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -605,6 +603,35 @@ bool Abc_NodeIsMuxType( Abc_Obj_t * pNode ) /**Function************************************************************* + Synopsis [Returns 1 if the node is the control type of the MUX.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +bool Abc_NodeIsMuxControlType( Abc_Obj_t * pNode ) +{ + Abc_Obj_t * pNode0, * pNode1; + // check that the node is regular + assert( !Abc_ObjIsComplement(pNode) ); + // skip the node that do not have two fanouts + if ( Abc_ObjFanoutNum(pNode) != 2 ) + return 0; + // get the fanouts + pNode0 = Abc_ObjFanout( pNode, 0 ); + pNode1 = Abc_ObjFanout( pNode, 1 ); + // if they have more than one fanout, we are not interested + if ( Abc_ObjFanoutNum(pNode0) != 1 || Abc_ObjFanoutNum(pNode1) != 1 ) + return 0; + // if the fanouts have the same fanout, this is MUX or EXOR (or a redundant gate (CA)(CB)) + return Abc_ObjFanout0(pNode0) == Abc_ObjFanout0(pNode1); +} + +/**Function************************************************************* + Synopsis [Recognizes what nodes are control and data inputs of a MUX.] Description [If the node is a MUX, returns the control variable C. diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 119f8cdf..d2422b64 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -62,6 +62,7 @@ static int Abc_CommandDisjoint ( Abc_Frame_t * pAbc, int argc, char ** argv static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandRestructure ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandLogic ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -80,6 +81,7 @@ static int Abc_CommandExdcGet ( Abc_Frame_t * pAbc, int argc, char ** argv static int Abc_CommandExdcSet ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandCut ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandXyz ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandEspresso ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandFraig ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -110,6 +112,7 @@ static int Abc_CommandSeqCleanup ( Abc_Frame_t * pAbc, int argc, char ** argv static int Abc_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSec ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandProve ( Abc_Frame_t * pAbc, int argc, char ** argv ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -161,6 +164,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "refactor", Abc_CommandRefactor, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "restructure", Abc_CommandRestructure, 1 ); // Cmd_CommandAdd( pAbc, "Various", "logic", Abc_CommandLogic, 1 ); Cmd_CommandAdd( pAbc, "Various", "miter", Abc_CommandMiter, 1 ); @@ -171,14 +175,15 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "muxes", Abc_CommandMuxes, 1 ); Cmd_CommandAdd( pAbc, "Various", "sat", Abc_CommandSat, 0 ); Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 ); - Cmd_CommandAdd( pAbc, "Various", "one_output", Abc_CommandOneOutput, 1 ); - Cmd_CommandAdd( pAbc, "Various", "one_node", Abc_CommandOneNode, 1 ); + Cmd_CommandAdd( pAbc, "Various", "cone", Abc_CommandOneOutput, 1 ); + Cmd_CommandAdd( pAbc, "Various", "node", Abc_CommandOneNode, 1 ); Cmd_CommandAdd( pAbc, "Various", "short_names", Abc_CommandShortNames, 0 ); Cmd_CommandAdd( pAbc, "Various", "exdc_free", Abc_CommandExdcFree, 1 ); Cmd_CommandAdd( pAbc, "Various", "exdc_get", Abc_CommandExdcGet, 1 ); Cmd_CommandAdd( pAbc, "Various", "exdc_set", Abc_CommandExdcSet, 1 ); Cmd_CommandAdd( pAbc, "Various", "cut", Abc_CommandCut, 0 ); Cmd_CommandAdd( pAbc, "Various", "xyz", Abc_CommandXyz, 1 ); + Cmd_CommandAdd( pAbc, "Various", "espresso", Abc_CommandEspresso, 1 ); Cmd_CommandAdd( pAbc, "Various", "test", Abc_CommandTest, 0 ); Cmd_CommandAdd( pAbc, "Fraiging", "fraig", Abc_CommandFraig, 1 ); @@ -209,6 +214,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Verification", "cec", Abc_CommandCec, 0 ); Cmd_CommandAdd( pAbc, "Verification", "sec", Abc_CommandSec, 0 ); + Cmd_CommandAdd( pAbc, "Verification", "prove", Abc_CommandProve, 1 ); // Rwt_Man4ExploreStart(); // Map_Var3Print(); @@ -258,8 +264,8 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv ) // set the defaults fShort = 1; fFactor = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "sfh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "sfh" ) ) != EOF ) { switch ( c ) { @@ -321,8 +327,8 @@ int Abc_CommandPrintExdc( Abc_Frame_t * pAbc, int argc, char ** argv ) // set the defaults fShort = 1; fPrintDc = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "sdh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "sdh" ) ) != EOF ) { switch ( c ) { @@ -407,8 +413,8 @@ int Abc_CommandPrintIo( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -425,18 +431,18 @@ int Abc_CommandPrintIo( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( argc > util_optind + 1 ) + if ( argc > globalUtilOptind + 1 ) { fprintf( pErr, "Wrong number of auguments.\n" ); goto usage; } - if ( argc == util_optind + 1 ) + if ( argc == globalUtilOptind + 1 ) { - pNode = Abc_NtkFindNode( pNtk, argv[util_optind] ); + pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] ); if ( pNode == NULL ) { - fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] ); + fprintf( pErr, "Cannot find node \"%s\".\n", argv[globalUtilOptind] ); return 1; } Abc_NodePrintFanio( pOut, pNode ); @@ -476,8 +482,8 @@ int Abc_CommandPrintLatch( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -526,8 +532,8 @@ int Abc_CommandPrintFanio( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -580,8 +586,8 @@ int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fUseRealNames = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "nh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "nh" ) ) != EOF ) { switch ( c ) { @@ -607,18 +613,18 @@ int Abc_CommandPrintFactor( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( argc > util_optind + 1 ) + if ( argc > globalUtilOptind + 1 ) { fprintf( pErr, "Wrong number of auguments.\n" ); goto usage; } - if ( argc == util_optind + 1 ) + if ( argc == globalUtilOptind + 1 ) { - pNode = Abc_NtkFindNode( pNtk, argv[util_optind] ); + pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] ); if ( pNode == NULL ) { - fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] ); + fprintf( pErr, "Cannot find node \"%s\".\n", argv[globalUtilOptind] ); return 1; } Abc_NodePrintFactor( pOut, pNode, fUseRealNames ); @@ -664,8 +670,8 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fListNodes = 0; fProfile = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "nph" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "nph" ) ) != EOF ) { switch ( c ) { @@ -694,18 +700,18 @@ int Abc_CommandPrintLevel( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( argc > util_optind + 1 ) + if ( argc > globalUtilOptind + 1 ) { fprintf( pErr, "Wrong number of auguments.\n" ); goto usage; } - if ( argc == util_optind + 1 ) + if ( argc == globalUtilOptind + 1 ) { - pNode = Abc_NtkFindNode( pNtk, argv[util_optind] ); + pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] ); if ( pNode == NULL ) { - fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] ); + fprintf( pErr, "Cannot find node \"%s\".\n", argv[globalUtilOptind] ); return 1; } Abc_NodePrintLevel( pOut, pNode ); @@ -752,8 +758,8 @@ int Abc_CommandPrintSupport( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fVerbose = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) { switch ( c ) { @@ -829,8 +835,8 @@ int Abc_CommandPrintSymms( Abc_Frame_t * pAbc, int argc, char ** argv ) fUseBdds = 0; fNaive = 0; fVerbose = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "bnvh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "bnvh" ) ) != EOF ) { switch ( c ) { @@ -906,8 +912,8 @@ int Abc_CommandPrintUnate( Abc_Frame_t * pAbc, int argc, char ** argv ) fUseBdds = 1; fUseNaive = 0; fVerbose = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "bnvh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "bnvh" ) ) != EOF ) { switch ( c ) { @@ -978,19 +984,19 @@ int Abc_CommandPrintAuto( Abc_Frame_t * pAbc, int argc, char ** argv ) Output = -1; fNaive = 0; fVerbose = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "Onvh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Onvh" ) ) != EOF ) { switch ( c ) { case 'O': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-O\" should be followed by an integer.\n" ); goto usage; } - Output = atoi(argv[util_optind]); - util_optind++; + Output = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( Output < 0 ) goto usage; break; @@ -1058,8 +1064,8 @@ int Abc_CommandPrintKMap( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fUseRealNames = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "nh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "nh" ) ) != EOF ) { switch ( c ) { @@ -1084,12 +1090,12 @@ int Abc_CommandPrintKMap( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Visualizing Karnaugh map works for BDD logic networks (run \"bdd\").\n" ); return 1; } - if ( argc > util_optind + 1 ) + if ( argc > globalUtilOptind + 1 ) { fprintf( pErr, "Wrong number of auguments.\n" ); goto usage; } - if ( argc == util_optind ) + if ( argc == globalUtilOptind ) { pNode = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) ); if ( !Abc_ObjIsNode(pNode) ) @@ -1100,10 +1106,10 @@ int Abc_CommandPrintKMap( Abc_Frame_t * pAbc, int argc, char ** argv ) } else { - pNode = Abc_NtkFindNode( pNtk, argv[util_optind] ); + pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] ); if ( pNode == NULL ) { - fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] ); + fprintf( pErr, "Cannot find node \"%s\".\n", argv[globalUtilOptind] ); return 1; } } @@ -1145,8 +1151,8 @@ int Abc_CommandPrintGates( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fUseLibrary = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "lh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF ) { switch ( c ) { @@ -1208,8 +1214,8 @@ int Abc_CommandPrintSharing( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fUseLibrary = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "lh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF ) { switch ( c ) { @@ -1269,8 +1275,8 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -1293,12 +1299,12 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( argc > util_optind + 1 ) + if ( argc > globalUtilOptind + 1 ) { fprintf( pErr, "Wrong number of auguments.\n" ); goto usage; } - if ( argc == util_optind ) + if ( argc == globalUtilOptind ) { pNode = Abc_ObjFanin0( Abc_NtkPo(pNtk, 0) ); if ( !Abc_ObjIsNode(pNode) ) @@ -1309,10 +1315,10 @@ int Abc_CommandShowBdd( Abc_Frame_t * pAbc, int argc, char ** argv ) } else { - pNode = Abc_NtkFindNode( pNtk, argv[util_optind] ); + pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] ); if ( pNode == NULL ) { - fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] ); + fprintf( pErr, "Cannot find node \"%s\".\n", argv[globalUtilOptind] ); return 1; } } @@ -1359,30 +1365,30 @@ int Abc_CommandShowCut( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults nNodeSizeMax = 10; nConeSizeMax = ABC_INFINITY; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "NCh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "NCh" ) ) != EOF ) { switch ( c ) { case 'N': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); goto usage; } - nNodeSizeMax = atoi(argv[util_optind]); - util_optind++; + nNodeSizeMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( nNodeSizeMax < 0 ) goto usage; break; case 'C': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); goto usage; } - nConeSizeMax = atoi(argv[util_optind]); - util_optind++; + nConeSizeMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( nConeSizeMax < 0 ) goto usage; break; @@ -1404,16 +1410,16 @@ int Abc_CommandShowCut( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Visualizing cuts only works for AIGs (run \"strash\").\n" ); return 1; } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { fprintf( pErr, "Wrong number of auguments.\n" ); goto usage; } - pNode = Abc_NtkFindNode( pNtk, argv[util_optind] ); + pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] ); if ( pNode == NULL ) { - fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] ); + fprintf( pErr, "Cannot find node \"%s\".\n", argv[globalUtilOptind] ); return 1; } Abc_NodeShowCut( pNode, nNodeSizeMax, nConeSizeMax ); @@ -1459,8 +1465,8 @@ int Abc_CommandShowAig( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fMulti = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "mh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "mh" ) ) != EOF ) { switch ( c ) { @@ -1533,8 +1539,8 @@ int Abc_CommandShowNtk( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fGateNames = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "gh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "gh" ) ) != EOF ) { switch ( c ) { @@ -1595,8 +1601,8 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -1671,8 +1677,8 @@ int Abc_CommandStrash( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fAllNodes = 0; fCleanup = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "ach" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ach" ) ) != EOF ) { switch ( c ) { @@ -1733,19 +1739,24 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; bool fDuplicate; bool fSelective; + bool fUpdateLevel; pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - fDuplicate = 0; - fSelective = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "dsh" ) ) != EOF ) + fDuplicate = 0; + fSelective = 0; + fUpdateLevel = 1; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ldsh" ) ) != EOF ) { switch ( c ) { + case 'l': + fUpdateLevel ^= 1; + break; case 'd': fDuplicate ^= 1; break; @@ -1773,7 +1784,7 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv ) // get the new network if ( Abc_NtkIsStrash(pNtk) ) { - pNtkRes = Abc_NtkBalance( pNtk, fDuplicate, fSelective ); + pNtkRes = Abc_NtkBalance( pNtk, fDuplicate, fSelective, fUpdateLevel ); } else { @@ -1783,7 +1794,7 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Strashing before balancing has failed.\n" ); return 1; } - pNtkRes = Abc_NtkBalance( pNtkTemp, fDuplicate, fSelective ); + pNtkRes = Abc_NtkBalance( pNtkTemp, fDuplicate, fSelective, fUpdateLevel ); Abc_NtkDelete( pNtkTemp ); } @@ -1798,8 +1809,9 @@ int Abc_CommandBalance( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: balance [-dsh]\n" ); + fprintf( pErr, "usage: balance [-ldsh]\n" ); fprintf( pErr, "\t transforms the current network into a well-balanced AIG\n" ); + fprintf( pErr, "\t-l : toggle minimizing the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" ); fprintf( pErr, "\t-d : toggle duplication of logic [default = %s]\n", fDuplicate? "yes": "no" ); fprintf( pErr, "\t-s : toggle duplication on the critical paths [default = %s]\n", fSelective? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); @@ -1836,30 +1848,30 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv ) fCnf = 0; fMulti = 0; fSimple = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "TFmcsh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "TFmcsh" ) ) != EOF ) { switch ( c ) { case 'T': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" ); goto usage; } - nThresh = atoi(argv[util_optind]); - util_optind++; + nThresh = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( nThresh < 0 ) goto usage; break; case 'F': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } - nFaninMax = atoi(argv[util_optind]); - util_optind++; + nFaninMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( nFaninMax < 0 ) goto usage; break; @@ -1938,8 +1950,8 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -1993,8 +2005,8 @@ int Abc_CommandSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -2062,30 +2074,30 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) p->fUse0 = 0; p->fUseCompl = 1; p->fVerbose = 0; - util_getopt_reset(); - while ( (c = util_getopt(argc, argv, "LNsdzcvh")) != EOF ) + Extra_UtilGetoptReset(); + while ( (c = Extra_UtilGetopt(argc, argv, "LNsdzcvh")) != EOF ) { switch (c) { case 'L': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-L\" should be followed by an integer.\n" ); goto usage; } - p->nPairsMax = atoi(argv[util_optind]); - util_optind++; + p->nPairsMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( p->nPairsMax < 0 ) goto usage; break; case 'N': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); goto usage; } - p->nNodesExt = atoi(argv[util_optind]); - util_optind++; + p->nNodesExt = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( p->nNodesExt < 0 ) goto usage; break; @@ -2184,8 +2196,8 @@ int Abc_CommandDisjoint( Abc_Frame_t * pAbc, int argc, char ** argv ) fVerbose = 0; fPrint = 0; fShort = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "grvpsh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "grvpsh" ) ) != EOF ) { switch ( c ) { @@ -2309,8 +2321,8 @@ int Abc_CommandRewrite( Abc_Frame_t * pAbc, int argc, char ** argv ) fPrecompute = 0; fUseZeros = 0; fVerbose = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "lxzvh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "lxzvh" ) ) != EOF ) { switch ( c ) { @@ -2371,7 +2383,7 @@ usage: fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; -} +} /**Function************************************************************* @@ -2404,34 +2416,34 @@ int Abc_CommandRefactor( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults nNodeSizeMax = 10; nConeSizeMax = 16; - fUpdateLevel = 0; + fUpdateLevel = 1; fUseZeros = 0; fUseDcs = 0; fVerbose = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "NClzdvh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "NClzdvh" ) ) != EOF ) { switch ( c ) { case 'N': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); goto usage; } - nNodeSizeMax = atoi(argv[util_optind]); - util_optind++; + nNodeSizeMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( nNodeSizeMax < 0 ) goto usage; break; case 'C': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); goto usage; } - nConeSizeMax = atoi(argv[util_optind]); - util_optind++; + nConeSizeMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( nConeSizeMax < 0 ) goto usage; break; @@ -2497,6 +2509,109 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandRestructure( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int nCutMax; + bool fUpdateLevel; + bool fUseZeros; + bool fVerbose; + extern int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + nCutMax = 5; + fUpdateLevel = 0; + fUseZeros = 0; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Klzvh" ) ) != EOF ) + { + switch ( c ) + { + case 'K': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); + goto usage; + } + nCutMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nCutMax < 0 ) + goto usage; + break; + case 'l': + fUpdateLevel ^= 1; + break; + case 'z': + fUseZeros ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( nCutMax < 4 || nCutMax > CUT_SIZE_MAX ) + { + fprintf( pErr, "Can only compute the cuts for %d <= K <= %d.\n", 4, CUT_SIZE_MAX ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command can only be applied to an AIG (run \"strash\").\n" ); + return 1; + } + if ( Abc_NtkGetChoiceNum(pNtk) ) + { + fprintf( pErr, "AIG resynthesis cannot be applied to AIGs with choice nodes.\n" ); + return 1; + } + + // modify the current network + if ( !Abc_NtkRestructure( pNtk, nCutMax, fUpdateLevel, fUseZeros, fVerbose ) ) + { + fprintf( pErr, "Refactoring has failed.\n" ); + return 1; + } + return 0; + +usage: + fprintf( pErr, "usage: restructure [-K num] [-lzvh]\n" ); + fprintf( pErr, "\t performs technology-independent restructuring of the AIG\n" ); + fprintf( pErr, "\t-K num : the max cut size (%d <= num <= %d) [default = %d]\n", CUT_SIZE_MIN, CUT_SIZE_MAX, nCutMax ); + fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" ); + fprintf( pErr, "\t-z : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "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; +} + /**Function************************************************************* @@ -2520,8 +2635,8 @@ int Abc_CommandLogic( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -2591,8 +2706,8 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fComb = 1; fCheck = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF ) { switch ( c ) { @@ -2604,8 +2719,8 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) } } - pArgvNew = argv + util_optind; - nArgcNew = argc - util_optind; + pArgvNew = argv + globalUtilOptind; + nArgcNew = argc - globalUtilOptind; if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) return 1; @@ -2662,19 +2777,19 @@ int Abc_CommandFrames( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fInitial = 0; nFrames = 5; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "Fih" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Fih" ) ) != EOF ) { switch ( c ) { case 'F': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } - nFrames = atoi(argv[util_optind]); - util_optind++; + nFrames = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( nFrames <= 0 ) goto usage; break; @@ -2744,8 +2859,8 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -2804,8 +2919,8 @@ int Abc_CommandBdd( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -2866,8 +2981,8 @@ int Abc_CommandReorder( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fVerbose = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) { switch ( c ) { @@ -2926,8 +3041,8 @@ int Abc_CommandMuxes( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -2987,29 +3102,43 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; int RetValue; int fVerbose; - int nSeconds; + int nConfLimit; + int nImpLimit; + int clk; pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - fVerbose = 0; - nSeconds = 20; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "Tvh" ) ) != EOF ) + fVerbose = 0; + nConfLimit = 100000; + nImpLimit = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "CIvh" ) ) != EOF ) { switch ( c ) { - case 'T': - if ( util_optind >= argc ) + case 'C': + if ( globalUtilOptind >= argc ) { - fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); goto usage; } - nSeconds = atoi(argv[util_optind]); - util_optind++; - if ( nSeconds < 0 ) + nConfLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfLimit < 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nImpLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nImpLimit < 0 ) goto usage; break; case 'v': @@ -3038,46 +3167,42 @@ int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } -/* - if ( !Abc_NtkIsLogic(pNtk) ) - { - fprintf( stdout, "This command can only be applied to logic network (run \"renode -c\").\n" ); - return 0; - } - if ( Abc_NtkIsMappedLogic(pNtk) ) - Abc_NtkUnmap(pNtk); - if ( Abc_NtkIsSopLogic(pNtk) ) - Abc_NtkSopToBdd(pNtk); -*/ if ( Abc_NtkIsStrash(pNtk) ) { - RetValue = Abc_NtkMiterSat( pNtk, nSeconds, fVerbose ); + clk = clock(); + RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, fVerbose ); if ( RetValue == -1 ) - printf( "The miter is UNDECIDED (SAT solver timed out).\n" ); + printf( "UNDECIDED " ); else if ( RetValue == 0 ) - printf( "The miter is SATISFIABLE.\n" ); + printf( "SATISFIABLE " ); else - printf( "The miter is UNSATISFIABLE.\n" ); + printf( "UNSATISFIABLE " ); + //printf( "\n" ); + PRT( "Time", clock() - clk ); } else { Abc_Ntk_t * pTemp; pTemp = Abc_NtkStrash( pNtk, 0, 0 ); - RetValue = Abc_NtkMiterSat( pTemp, nSeconds, fVerbose ); + clk = clock(); + RetValue = Abc_NtkMiterSat( pTemp, nConfLimit, nImpLimit, fVerbose ); if ( RetValue == -1 ) - printf( "The miter is UNDECIDED (SAT solver timed out).\n" ); + printf( "UNDECIDED " ); else if ( RetValue == 0 ) - printf( "The miter is SATISFIABLE.\n" ); + printf( "SATISFIABLE " ); else - printf( "The miter is UNSATISFIABLE.\n" ); + printf( "UNSATISFIABLE " ); + //printf( "\n" ); + PRT( "Time", clock() - clk ); Abc_NtkDelete( pTemp ); } return 0; usage: - fprintf( pErr, "usage: sat [-T num] [-vh]\n" ); + fprintf( pErr, "usage: sat [-C num] [-I num] [-vh]\n" ); fprintf( pErr, "\t solves the combinational miter\n" ); - fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds ); + fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); + fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit ); fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -3109,8 +3234,8 @@ int Abc_CommandExtSeqDcs( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fVerbose = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "vh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) { switch ( c ) { @@ -3169,9 +3294,10 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; - Abc_Obj_t * pNode; + Abc_Obj_t * pNode, * pNodeCo; int c; int fUseAllCis; + int fUseMffc; int Output; pNtk = Abc_FrameReadNtk(pAbc); @@ -3180,23 +3306,26 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fUseAllCis = 0; + fUseMffc = 0; Output = -1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "Oah" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Omah" ) ) != EOF ) { switch ( c ) { case 'O': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-O\" should be followed by an integer.\n" ); goto usage; } - Output = atoi(argv[util_optind]); - util_optind++; + Output = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( Output < 0 ) goto usage; break; + case 'm': + fUseMffc ^= 1; case 'a': fUseAllCis ^= 1; break; @@ -3219,27 +3348,31 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( argc > util_optind + 1 ) + if ( argc > globalUtilOptind + 1 ) { fprintf( pErr, "Wrong number of auguments.\n" ); goto usage; } - if ( argc == util_optind + 1 ) + if ( argc == globalUtilOptind + 1 ) { - pNode = Abc_NtkFindCo( pNtk, argv[util_optind] ); + pNodeCo = Abc_NtkFindCo( pNtk, argv[globalUtilOptind] ); + pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] ); if ( pNode == NULL ) { - fprintf( pErr, "Cannot find CO node \"%s\".\n", argv[util_optind] ); + fprintf( pErr, "Cannot find node \"%s\".\n", argv[globalUtilOptind] ); return 1; } - pNtkRes = Abc_NtkCreateOutput( pNtk, pNode, fUseAllCis ); + if ( fUseMffc ) + pNtkRes = Abc_NtkCreateMffc( pNtk, pNode, argv[globalUtilOptind] ); + else + pNtkRes = Abc_NtkCreateCone( pNtk, pNode, argv[globalUtilOptind], fUseAllCis ); } else { if ( Output == -1 ) { - fprintf( pErr, "The output is not specified.\n" ); + fprintf( pErr, "The node is not specified.\n" ); return 1; } if ( Output >= Abc_NtkCoNum(pNtk) ) @@ -3247,11 +3380,17 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "The 0-based output number (%d) is larger than the number of outputs (%d).\n", Output, Abc_NtkCoNum(pNtk) ); return 1; } - pNtkRes = Abc_NtkCreateOutput( pNtk, Abc_NtkCo(pNtk,Output), fUseAllCis ); + pNodeCo = Abc_NtkCo( pNtk, Output ); + if ( fUseMffc ) + pNtkRes = Abc_NtkCreateMffc( pNtk, Abc_ObjFanin0(pNodeCo), Abc_ObjName(pNodeCo) ); + else + pNtkRes = Abc_NtkCreateCone( pNtk, Abc_ObjFanin0(pNodeCo), Abc_ObjName(pNodeCo), fUseAllCis ); } + if ( pNodeCo && Abc_ObjFaninC0(pNodeCo) ) + printf( "The extracted cone represents the complement function of the CO.\n" ); if ( pNtkRes == NULL ) { - fprintf( pErr, "Splitting one output has failed.\n" ); + fprintf( pErr, "Writing the logic cone of one node has failed.\n" ); return 1; } // replace the current network @@ -3259,12 +3398,13 @@ int Abc_CommandOneOutput( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: one_output [-O num] [-ah] <name>\n" ); - fprintf( pErr, "\t replaces the current network by the logic cone of one output\n" ); + fprintf( pErr, "usage: cone [-O num] [-amh] <name>\n" ); + fprintf( pErr, "\t replaces the current network by one logic cone\n" ); fprintf( pErr, "\t-a : toggle writing all CIs or structral support only [default = %s]\n", fUseAllCis? "all": "structural" ); + fprintf( pErr, "\t-m : toggle writing only MFFC or complete TFI cone [default = %s]\n", fUseMffc? "MFFC": "TFI cone" ); fprintf( pErr, "\t-h : print the command usage\n"); - fprintf( pErr, "\t-O num : (optional) the 0-based number of the output\n"); - fprintf( pErr, "\tname : (optional) the name of the output\n"); + fprintf( pErr, "\t-O num : (optional) the 0-based number of the CO to extract\n"); + fprintf( pErr, "\tname : (optional) the name of the node to extract\n"); return 1; } @@ -3291,8 +3431,8 @@ int Abc_CommandOneNode( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -3315,16 +3455,16 @@ int Abc_CommandOneNode( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { fprintf( pErr, "Wrong number of auguments.\n" ); goto usage; } - pNode = Abc_NtkFindNode( pNtk, argv[util_optind] ); + pNode = Abc_NtkFindNode( pNtk, argv[globalUtilOptind] ); if ( pNode == NULL ) { - fprintf( pErr, "Cannot find node \"%s\".\n", argv[util_optind] ); + fprintf( pErr, "Cannot find node \"%s\".\n", argv[globalUtilOptind] ); return 1; } @@ -3340,7 +3480,7 @@ int Abc_CommandOneNode( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: one_node [-h] <name>\n" ); + fprintf( pErr, "usage: node [-h] <name>\n" ); fprintf( pErr, "\t replaces the current network by the network composed of one node\n" ); fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\tname : the node name\n"); @@ -3371,8 +3511,8 @@ int Abc_CommandShortNames( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -3420,8 +3560,8 @@ int Abc_CommandExdcFree( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -3480,8 +3620,8 @@ int Abc_CommandExdcGet( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -3538,8 +3678,8 @@ int Abc_CommandExdcSet( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -3556,13 +3696,13 @@ int Abc_CommandExdcSet( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { goto usage; } // get the input file name - FileName = argv[util_optind]; + FileName = argv[globalUtilOptind]; if ( (pFile = fopen( FileName, "r" )) == NULL ) { fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName ); @@ -3639,30 +3779,30 @@ int Abc_CommandCut( Abc_Frame_t * pAbc, int argc, char ** argv ) pParams->fDrop = 0; // drop cuts on the fly pParams->fMulti = 0; // use multi-input AND-gates pParams->fVerbose = 0; // the verbosiness flag - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "KMtfdmvoh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "KMtfdmvoh" ) ) != EOF ) { switch ( c ) { case 'K': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" ); goto usage; } - pParams->nVarsMax = atoi(argv[util_optind]); - util_optind++; + pParams->nVarsMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( pParams->nVarsMax < 0 ) goto usage; break; case 'M': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-M\" should be followed by an integer.\n" ); goto usage; } - pParams->nKeepMax = atoi(argv[util_optind]); - util_optind++; + pParams->nKeepMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( pParams->nKeepMax < 0 ) goto usage; break; @@ -3729,7 +3869,7 @@ usage: fprintf( pErr, "\t-t : toggle truth table computation [default = %s]\n", pParams->fTruth? "yes": "no" ); fprintf( pErr, "\t-f : toggle filtering of duplicated/dominated [default = %s]\n", pParams->fFilter? "yes": "no" ); fprintf( pErr, "\t-d : toggle dropping when fanouts are done [default = %s]\n", pParams->fDrop? "yes": "no" ); - fprintf( pErr, "\t-m : toggle using multi-input AND-gates [default = %s]\n", pParams->fMulti? "yes": "no" ); + fprintf( pErr, "\t-m : toggle computing only factor-cuts [default = %s]\n", pParams->fMulti? "yes": "no" ); fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", pParams->fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; @@ -3767,30 +3907,30 @@ int Abc_CommandScut( Abc_Frame_t * pAbc, int argc, char ** argv ) pParams->fFilter = 1; // filter dominated cuts pParams->fSeq = 1; // compute sequential cuts pParams->fVerbose = 0; // the verbosiness flag - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "KMtvh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "KMtvh" ) ) != EOF ) { switch ( c ) { case 'K': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" ); goto usage; } - pParams->nVarsMax = atoi(argv[util_optind]); - util_optind++; + pParams->nVarsMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( pParams->nVarsMax < 0 ) goto usage; break; case 'M': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-M\" should be followed by an integer.\n" ); goto usage; } - pParams->nKeepMax = atoi(argv[util_optind]); - util_optind++; + pParams->nKeepMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( pParams->nKeepMax < 0 ) goto usage; break; @@ -3868,19 +4008,19 @@ int Abc_CommandXyz( Abc_Frame_t * pAbc, int argc, char ** argv ) fVerbose = 0; fUseInvs = 1; nFaninMax = 128; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "Nivh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Nivh" ) ) != EOF ) { switch ( c ) { case 'N': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" ); goto usage; } - nFaninMax = atoi(argv[util_optind]); - util_optind++; + nFaninMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( nFaninMax < 0 ) goto usage; break; @@ -3931,6 +4071,66 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandEspresso( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk; + int c; + int fVerbose; + extern void Abc_NtkEspresso( Abc_Ntk_t * pNtk, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsLogic(pNtk) ) + { + fprintf( pErr, "SOP minimization is possible for logic networks (run \"renode\").\n" ); + return 1; + } + Abc_NtkEspresso( pNtk, fVerbose ); + return 0; + +usage: + fprintf( pErr, "usage: espresso [-vh]\n" ); + fprintf( pErr, "\t minimizes SOPs of the local functions using Espresso\n" ); + fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* @@ -3948,15 +4148,15 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) FILE * pOut, * pErr; Abc_Ntk_t * pNtk, * pNtkRes; int c; -// extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ); + extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -3984,8 +4184,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // run the command // pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 ); -// pNtkRes = Abc_NtkNewAig( pNtk ); - pNtkRes = NULL; + pNtkRes = Abc_NtkNewAig( pNtk ); +// pNtkRes = NULL; if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -4044,41 +4244,41 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) pParams->fTryProve = 0; // tries to solve the final miter pParams->fVerbose = 0; // the verbosiness flag pParams->fVerboseP = 0; // the verbosiness flag - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "RDBrscpvaeh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "RDBrscpvaeh" ) ) != EOF ) { switch ( c ) { case 'R': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-R\" should be followed by an integer.\n" ); goto usage; } - pParams->nPatsRand = atoi(argv[util_optind]); - util_optind++; + pParams->nPatsRand = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( pParams->nPatsRand < 0 ) goto usage; break; case 'D': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-D\" should be followed by an integer.\n" ); goto usage; } - pParams->nPatsDyna = atoi(argv[util_optind]); - util_optind++; + pParams->nPatsDyna = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( pParams->nPatsDyna < 0 ) goto usage; break; case 'B': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-B\" should be followed by an integer.\n" ); goto usage; } - pParams->nBTLimit = atoi(argv[util_optind]); - util_optind++; + pParams->nBTLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( pParams->nBTLimit < 0 ) goto usage; break; @@ -4189,8 +4389,8 @@ int Abc_CommandFraigTrust( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fDuplicate = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "dh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF ) { switch ( c ) { @@ -4253,8 +4453,8 @@ int Abc_CommandFraigStore( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fDuplicate = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "dh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF ) { switch ( c ) { @@ -4314,8 +4514,8 @@ int Abc_CommandFraigRestore( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fDuplicate = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "dh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF ) { switch ( c ) { @@ -4378,8 +4578,8 @@ int Abc_CommandFraigClean( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fDuplicate = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "dh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF ) { switch ( c ) { @@ -4432,8 +4632,8 @@ int Abc_CommandFraigSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) fUseInv = 1; fExdc = 0; fVerbose = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "ievh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ievh" ) ) != EOF ) { switch ( c ) { @@ -4521,19 +4721,19 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) fSweep = 1; fSwitching = 0; fVerbose = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "Daspvh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Daspvh" ) ) != EOF ) { switch ( c ) { case 'D': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-D\" should be followed by a floating point number.\n" ); goto usage; } - DelayTarget = (float)atof(argv[util_optind]); - util_optind++; + DelayTarget = (float)atof(argv[globalUtilOptind]); + globalUtilOptind++; if ( DelayTarget <= 0.0 ) goto usage; break; @@ -4576,7 +4776,7 @@ int Abc_CommandMap( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Strashing before mapping has failed.\n" ); return 1; } - pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0 ); + pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0, 1 ); Abc_NtkDelete( pNtkRes ); if ( pNtk == NULL ) { @@ -4652,8 +4852,8 @@ int Abc_CommandUnmap( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -4713,8 +4913,8 @@ int Abc_CommandAttach( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -4776,8 +4976,8 @@ int Abc_CommandSuperChoice( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -4853,8 +5053,8 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) fSwitching = 0; fVerbose = 0; DelayTarget =-1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "apvhD" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "apvhD" ) ) != EOF ) { switch ( c ) { @@ -4870,13 +5070,13 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'h': goto usage; case 'D': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-D\" should be followed by a floating point number.\n" ); goto usage; } - DelayTarget = (float)atof(argv[util_optind]); - util_optind++; + DelayTarget = (float)atof(argv[globalUtilOptind]); + globalUtilOptind++; if ( DelayTarget <= 0.0 ) goto usage; break; @@ -4906,7 +5106,7 @@ int Abc_CommandFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Strashing before FPGA mapping has failed.\n" ); return 1; } - pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0 ); + pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0, 1 ); Abc_NtkDelete( pNtkRes ); if ( pNtk == NULL ) { @@ -4985,8 +5185,8 @@ int Abc_CommandPga( Abc_Frame_t * pAbc, int argc, char ** argv ) pParams->fSwitching = 0; pParams->fDropCuts = 0; pParams->fVerbose = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "fapdvh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "fapdvh" ) ) != EOF ) { switch ( c ) { @@ -5029,7 +5229,7 @@ int Abc_CommandPga( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Strashing before FPGA mapping has failed.\n" ); return 1; } - pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0 ); + pNtk = Abc_NtkBalance( pNtkRes = pNtk, 0, 0, 1 ); Abc_NtkDelete( pNtkRes ); if ( pNtk == NULL ) { @@ -5106,8 +5306,8 @@ int Abc_CommandInit( Abc_Frame_t * pAbc, int argc, char ** argv ) fOnes = 0; fRandom = 0; fDontCare = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "zordh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "zordh" ) ) != EOF ) { switch ( c ) { @@ -5211,19 +5411,19 @@ int Abc_CommandPipe( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults nLatches = 5; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "Lh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Lh" ) ) != EOF ) { switch ( c ) { case 'L': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-L\" should be followed by a positive integer.\n" ); goto usage; } - nLatches = atoi(argv[util_optind]); - util_optind++; + nLatches = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( nLatches < 0 ) goto usage; break; @@ -5286,8 +5486,8 @@ int Abc_CommandSeq( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -5364,8 +5564,8 @@ int Abc_CommandUnseq( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults fShare = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "sh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "sh" ) ) != EOF ) { switch ( c ) { @@ -5445,19 +5645,19 @@ int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv ) fInitial = 1; fVerbose = 0; nMaxIters = 15; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "Ifbivh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Ifbivh" ) ) != EOF ) { switch ( c ) { case 'I': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-I\" should be followed by a positive integer.\n" ); goto usage; } - nMaxIters = atoi(argv[util_optind]); - util_optind++; + nMaxIters = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( nMaxIters < 0 ) goto usage; break; @@ -5568,19 +5768,19 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults nMaxIters = 15; fVerbose = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "Ivh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF ) { switch ( c ) { case 'I': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-I\" should be followed by a positive integer.\n" ); goto usage; } - nMaxIters = atoi(argv[util_optind]); - util_optind++; + nMaxIters = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( nMaxIters < 0 ) goto usage; break; @@ -5625,7 +5825,7 @@ int Abc_CommandSeqFpga( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0, 0 ); + pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0, 0, 1 ); Abc_NtkDelete( pNtkRes ); if ( pNtkNew == NULL ) { @@ -5692,19 +5892,19 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults nMaxIters = 15; fVerbose = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "Ivh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF ) { switch ( c ) { case 'I': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-I\" should be followed by a positive integer.\n" ); goto usage; } - nMaxIters = atoi(argv[util_optind]); - util_optind++; + nMaxIters = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( nMaxIters < 0 ) goto usage; break; @@ -5749,7 +5949,7 @@ int Abc_CommandSeqMap( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0, 0 ); + pNtkNew = Abc_NtkBalance( pNtkRes = pNtkNew, 0, 0, 1 ); Abc_NtkDelete( pNtkRes ); if ( pNtkNew == NULL ) { @@ -5824,19 +6024,19 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv ) fExdc = 1; fImp = 0; fVerbose = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "Feivh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Feivh" ) ) != EOF ) { switch ( c ) { case 'F': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } - nFrames = atoi(argv[util_optind]); - util_optind++; + nFrames = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( nFrames <= 0 ) goto usage; break; @@ -5927,8 +6127,8 @@ int Abc_CommandSeqCleanup( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -5983,8 +6183,10 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv ) int fSat; int fVerbose; int nSeconds; + int nConfLimit; + int nImpLimit; - extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds ); + extern void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nImpLimit ); extern void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose ); @@ -5996,22 +6198,46 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv ) fSat = 0; fVerbose = 0; nSeconds = 20; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "Tsvh" ) ) != EOF ) + nConfLimit = 10000; + nImpLimit = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "TCIsvh" ) ) != EOF ) { switch ( c ) { case 'T': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" ); goto usage; } - nSeconds = atoi(argv[util_optind]); - util_optind++; + nSeconds = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( nSeconds < 0 ) goto usage; break; + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfLimit < 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nImpLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nImpLimit < 0 ) + goto usage; + break; case 's': fSat ^= 1; break; @@ -6023,14 +6249,14 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv ) } } - pArgvNew = argv + util_optind; - nArgcNew = argc - util_optind; + pArgvNew = argv + globalUtilOptind; + nArgcNew = argc - globalUtilOptind; if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) return 1; // perform equivalence checking if ( fSat ) - Abc_NtkCecSat( pNtk1, pNtk2, nSeconds ); + Abc_NtkCecSat( pNtk1, pNtk2, nConfLimit, nImpLimit ); else Abc_NtkCecFraig( pNtk1, pNtk2, nSeconds, fVerbose ); @@ -6039,9 +6265,11 @@ int Abc_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: cec [-T num] [-svh] <file1> <file2>\n" ); + fprintf( pErr, "usage: cec [-T num] [-C num] [-I num] [-svh] <file1> <file2>\n" ); fprintf( pErr, "\t performs combinational equivalence checking\n" ); fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds ); + fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); + fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit ); fprintf( pErr, "\t-s : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); @@ -6075,8 +6303,10 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) int fVerbose; int nFrames; int nSeconds; + int nConfLimit; + int nImpLimit; - extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames ); + extern void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nImpLimit, int nFrames ); extern void Abc_NtkSecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames, int fVerbose ); @@ -6089,33 +6319,57 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) fVerbose = 0; nFrames = 3; nSeconds = 20; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "FTsvh" ) ) != EOF ) + nConfLimit = 10000; + nImpLimit = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "FTCIsvh" ) ) != EOF ) { switch ( c ) { case 'F': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); goto usage; } - nFrames = atoi(argv[util_optind]); - util_optind++; + nFrames = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( nFrames <= 0 ) goto usage; break; case 'T': - if ( util_optind >= argc ) + if ( globalUtilOptind >= argc ) { fprintf( pErr, "Command line switch \"-T\" should be followed by an integer.\n" ); goto usage; } - nSeconds = atoi(argv[util_optind]); - util_optind++; + nSeconds = atoi(argv[globalUtilOptind]); + globalUtilOptind++; if ( nSeconds < 0 ) goto usage; break; + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfLimit < 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nImpLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nImpLimit < 0 ) + goto usage; + break; case 'v': fVerbose ^= 1; break; @@ -6127,14 +6381,14 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) } } - pArgvNew = argv + util_optind; - nArgcNew = argc - util_optind; + pArgvNew = argv + globalUtilOptind; + nArgcNew = argc - globalUtilOptind; if ( !Abc_NtkPrepareTwoNtks( pErr, pNtk, pArgvNew, nArgcNew, &pNtk1, &pNtk2, &fDelete1, &fDelete2 ) ) return 1; // perform equivalence checking if ( fSat ) - Abc_NtkSecSat( pNtk1, pNtk2, nSeconds, nFrames ); + Abc_NtkSecSat( pNtk1, pNtk2, nConfLimit, nImpLimit, nFrames ); else Abc_NtkSecFraig( pNtk1, pNtk2, nSeconds, nFrames, fVerbose ); @@ -6143,13 +6397,15 @@ int Abc_CommandSec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: sec [-F num] [-T num] [-svh] <file1> <file2>\n" ); + fprintf( pErr, "usage: sec [-F num] [-T num] [-C num] [-I num] [-svh] <file1> <file2>\n" ); fprintf( pErr, "\t performs bounded sequential equivalence checking\n" ); fprintf( pErr, "\t-s : toggle \"SAT only\" and \"FRAIG + SAT\" [default = %s]\n", fSat? "SAT only": "FRAIG + SAT" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames ); fprintf( pErr, "\t-T num : approximate runtime limit in seconds [default = %d]\n", nSeconds ); + fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); + fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit ); fprintf( pErr, "\tfile1 : (optional) the file with the first network\n"); fprintf( pErr, "\tfile2 : (optional) the file with the second network\n"); fprintf( pErr, "\t if no files are given, uses the current network and its spec\n"); @@ -6157,6 +6413,137 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkTemp; + int c; + int RetValue; + int fVerbose; + int fRewrite; + int fFraig; + int nConfLimit; + int nImpLimit; + int clk; + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fVerbose = 0; + fRewrite = 1; + fFraig = 1; + nConfLimit = 300000; + nImpLimit = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "CIrfvh" ) ) != EOF ) + { + switch ( c ) + { + case 'C': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nConfLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nConfLimit < 0 ) + goto usage; + break; + case 'I': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nImpLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nImpLimit < 0 ) + goto usage; + break; + case 'r': + fRewrite ^= 1; + break; + case 'f': + fFraig ^= 1; + 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_NtkLatchNum(pNtk) > 0 ) + { + fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" ); + return 0; + } + if ( Abc_NtkCoNum(pNtk) != 1 ) + { + fprintf( stdout, "Currently can only solve the miter with one output.\n" ); + return 0; + } + if ( Abc_NtkIsSeq(pNtk) ) + { + fprintf( stdout, "This command cannot be applied to the sequential AIG.\n" ); + return 0; + } + + clk = clock(); + + if ( Abc_NtkIsStrash(pNtk) ) + pNtkTemp = Abc_NtkDup( pNtk ); + else + pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 ); + + RetValue = Abc_NtkMiterProve( &pNtkTemp, nConfLimit, nImpLimit, fRewrite, fFraig, fVerbose ); + if ( RetValue == -1 ) + printf( "UNDECIDED " ); + else if ( RetValue == 0 ) + printf( "SATISFIABLE " ); + else + printf( "UNSATISFIABLE " ); + //printf( "\n" ); + + PRT( "Time", clock() - clk ); + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkTemp ); + return 0; + +usage: + fprintf( pErr, "usage: prove [-C num] [-I num] [-rfvh]\n" ); + fprintf( pErr, "\t solves combinational miter by rewriting, FRAIGing, and SAT\n" ); + fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n", nConfLimit ); + fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit ); + fprintf( pErr, "\t-r : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" ); + fprintf( pErr, "\t-f : toggle the use of FRAIGing [default = %s]\n", fFraig? "yes": "no" ); + fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c index effae853..919ea3b2 100644 --- a/src/base/abci/abcBalance.c +++ b/src/base/abci/abcBalance.c @@ -24,8 +24,8 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate, bool fSelective ); -static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Level, bool fDuplicate, bool fSelective ); +static void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate, bool fSelective, bool fUpdateLevel ); +static Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Vec_t * vStorage, int Level, bool fDuplicate, bool fSelective, bool fUpdateLevel ); static Vec_Ptr_t * Abc_NodeBalanceCone( Abc_Obj_t * pNode, Vec_Vec_t * vSuper, int Level, int fDuplicate, bool fSelective ); static int Abc_NodeBalanceCone_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vSuper, bool fFirst, bool fDuplicate, bool fSelective ); static void Abc_NtkMarkCriticalNodes( Abc_Ntk_t * pNtk ); @@ -45,7 +45,7 @@ static void Abc_NtkMarkCriticalNodes( Abc_Ntk_t * pNtk ); SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective ) +Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective, bool fUpdateLevel ) { Abc_Ntk_t * pNtkAig; assert( Abc_NtkIsStrash(pNtk) ); @@ -57,7 +57,7 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective ) } // perform balancing pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); - Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate, fSelective ); + Abc_NtkBalancePerform( pNtk, pNtkAig, fDuplicate, fSelective, fUpdateLevel ); Abc_NtkFinalize( pNtk, pNtkAig ); // undo the required times if ( fSelective ) @@ -88,7 +88,7 @@ Abc_Ntk_t * Abc_NtkBalance( Abc_Ntk_t * pNtk, bool fDuplicate, bool fSelective ) SeeAlso [] ***********************************************************************/ -void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate, bool fSelective ) +void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplicate, bool fSelective, bool fUpdateLevel ) { int fCheck = 1; ProgressBar * pProgress; @@ -107,7 +107,7 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica Extra_ProgressBarUpdate( pProgress, i, NULL ); // strash the driver node pDriver = Abc_ObjFanin0(pNode); - Abc_NodeBalance_rec( pNtkAig, pDriver, vStorage, 0, fDuplicate, fSelective ); + Abc_NodeBalance_rec( pNtkAig, pDriver, vStorage, 0, fDuplicate, fSelective, fUpdateLevel ); } Extra_ProgressBarStop( pProgress ); Vec_VecFree( vStorage ); @@ -115,38 +115,93 @@ void Abc_NtkBalancePerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkAig, bool fDuplica /**Function************************************************************* - Synopsis [Randomizes the node positions.] + Synopsis [Finds the left bound on the next candidate to be paired.] - Description [] + Description [The nodes in the array are in the decreasing order of levels. + The last node in the array has the smallest level. By default it would be paired + with the next node on the left. However, it may be possible to pair it with some + other node on the left, in such a way that the new node is shared. This procedure + finds the index of the left-most node, which can be paired with the last node.] SideEffects [] SeeAlso [] ***********************************************************************/ -void Abc_NodeBalanceRandomize( Vec_Ptr_t * vSuper ) +int Abc_NodeBalanceFindLeft( Vec_Ptr_t * vSuper ) { - Abc_Obj_t * pNode1, * pNode2; - int i, Signature; + Abc_Obj_t * pNodeRight, * pNodeLeft; + int Current; + // if two or less nodes, pair with the first if ( Vec_PtrSize(vSuper) < 3 ) + return 0; + // set the pointer to the one before the last + Current = Vec_PtrSize(vSuper) - 2; + pNodeRight = Vec_PtrEntry( vSuper, Current ); + // go through the nodes to the left of this one + for ( Current--; Current >= 0; Current-- ) + { + // get the next node on the left + pNodeLeft = Vec_PtrEntry( vSuper, Current ); + // if the level of this node is different, quit the loop + if ( Abc_ObjRegular(pNodeLeft)->Level != Abc_ObjRegular(pNodeRight)->Level ) + break; + } + Current++; + // get the node, for which the equality holds + pNodeLeft = Vec_PtrEntry( vSuper, Current ); + assert( Abc_ObjRegular(pNodeLeft)->Level == Abc_ObjRegular(pNodeRight)->Level ); + return Current; +} + +/**Function************************************************************* + + Synopsis [Moves closer to the end the node that is best for sharing.] + + Description [If there is no node with sharing, randomly chooses one of + the legal nodes.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeBalancePermute( Abc_Ntk_t * pNtkNew, Vec_Ptr_t * vSuper, int LeftBound ) +{ + Abc_Obj_t * pNode1, * pNode2, * pNode3; + int RightBound, i; + // get the right bound + RightBound = Vec_PtrSize(vSuper) - 2; + assert( LeftBound <= RightBound ); + if ( LeftBound == RightBound ) return; - pNode1 = Vec_PtrEntry( vSuper, Vec_PtrSize(vSuper)-2 ); - pNode2 = Vec_PtrEntry( vSuper, Vec_PtrSize(vSuper)-3 ); - if ( Abc_ObjRegular(pNode1)->Level != Abc_ObjRegular(pNode2)->Level ) - return; - // some reordering will be performed - Signature = rand(); - for ( i = Vec_PtrSize(vSuper)-2; i > 0; i-- ) + // get the two last nodes + pNode1 = Vec_PtrEntry( vSuper, RightBound + 1 ); + pNode2 = Vec_PtrEntry( vSuper, RightBound ); + // find the first node that can be shared + for ( i = RightBound; i >= LeftBound; i-- ) + { + pNode3 = Vec_PtrEntry( vSuper, i ); + if ( Abc_AigAndLookup( pNtkNew->pManFunc, pNode1, pNode3 ) ) + { + if ( pNode3 == pNode2 ) + return; + Vec_PtrWriteEntry( vSuper, i, pNode2 ); + Vec_PtrWriteEntry( vSuper, RightBound, pNode3 ); + return; + } + } +/* + // we did not find the node to share, randomize choice { - pNode1 = Vec_PtrEntry( vSuper, i ); - pNode2 = Vec_PtrEntry( vSuper, i-1 ); - if ( Abc_ObjRegular(pNode1)->Level != Abc_ObjRegular(pNode2)->Level ) + int Choice = rand() % (RightBound - LeftBound + 1); + pNode3 = Vec_PtrEntry( vSuper, LeftBound + Choice ); + if ( pNode3 == pNode2 ) return; - if ( Signature & (1 << (i % 10)) ) - continue; - Vec_PtrWriteEntry( vSuper, i, pNode2 ); - Vec_PtrWriteEntry( vSuper, i-1, pNode1 ); + Vec_PtrWriteEntry( vSuper, LeftBound + Choice, pNode2 ); + Vec_PtrWriteEntry( vSuper, RightBound, pNode3 ); } +*/ } /**Function************************************************************* @@ -160,12 +215,12 @@ void Abc_NodeBalanceRandomize( Vec_Ptr_t * vSuper ) SeeAlso [] ***********************************************************************/ -Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_Vec_t * vStorage, int Level, bool fDuplicate, bool fSelective ) +Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_Vec_t * vStorage, int Level, bool fDuplicate, bool fSelective, bool fUpdateLevel ) { Abc_Aig_t * pMan = pNtkNew->pManFunc; Abc_Obj_t * pNodeNew, * pNode1, * pNode2; Vec_Ptr_t * vSuper; - int i; + int i, LeftBound; assert( !Abc_ObjIsComplement(pNodeOld) ); // return if the result if known if ( pNodeOld->pCopy ) @@ -181,7 +236,7 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_ // for each old node, derive the new well-balanced node for ( i = 0; i < vSuper->nSize; i++ ) { - pNodeNew = Abc_NodeBalance_rec( pNtkNew, Abc_ObjRegular(vSuper->pArray[i]), vStorage, Level + 1, fDuplicate, fSelective ); + pNodeNew = Abc_NodeBalance_rec( pNtkNew, Abc_ObjRegular(vSuper->pArray[i]), vStorage, Level + 1, fDuplicate, fSelective, fUpdateLevel ); vSuper->pArray[i] = Abc_ObjNotCond( pNodeNew, Abc_ObjIsComplement(vSuper->pArray[i]) ); } if ( vSuper->nSize < 2 ) @@ -192,8 +247,10 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_ assert( vSuper->nSize > 1 ); while ( vSuper->nSize > 1 ) { - // randomize the node positions -// Abc_NodeBalanceRandomize( vSuper ); + // find the left bound on the node to be paired + LeftBound = (!fUpdateLevel)? 0 : Abc_NodeBalanceFindLeft( vSuper ); + // find the node that can be shared (if no such node, randomize choice) + Abc_NodeBalancePermute( pNtkNew, vSuper, LeftBound ); // pull out the last two nodes pNode1 = Vec_PtrPop(vSuper); pNode2 = Vec_PtrPop(vSuper); diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcClpBdd.c index 59c76e09..59c76e09 100644 --- a/src/base/abci/abcCollapse.c +++ b/src/base/abci/abcClpBdd.c diff --git a/src/base/abci/abcClpSop.c b/src/base/abci/abcClpSop.c new file mode 100644 index 00000000..de92243f --- /dev/null +++ b/src/base/abci/abcClpSop.c @@ -0,0 +1,53 @@ +/**CFile**************************************************************** + + FileName [abcCollapse.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Collapsing the network into two-levels.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcCollapse.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Collapses the network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkCollapseSop( Abc_Ntk_t * pNtk, int fVerbose ) +{ + Abc_Ntk_t * pNtkNew; + pNtkNew = NULL; + return pNtkNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c index 3e34602d..1ee9a712 100644 --- a/src/base/abci/abcCut.c +++ b/src/base/abci/abcCut.c @@ -57,10 +57,41 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) extern void Abc_NtkBalanceDetach( Abc_Ntk_t * pNtk ); assert( Abc_NtkIsStrash(pNtk) ); - +/* if ( pParams->fMulti ) - Abc_NtkBalanceAttach(pNtk); - + { + Abc_Obj_t * pNode, * pNodeA, * pNodeB, * pNodeC; + int nFactors; + // lebel the nodes, which will be the roots of factor-cuts + // mark the multiple-fanout nodes + Abc_AigForEachAnd( pNtk, pNode, i ) + if ( pNode->vFanouts.nSize > 1 ) + pNode->fMarkB = 1; + // unmark the control inputs of MUXes and inputs of EXOR gates + Abc_AigForEachAnd( pNtk, pNode, i ) + { + if ( !Abc_NodeIsMuxType(pNode) ) + continue; + + pNodeC = Abc_NodeRecognizeMux( pNode, &pNodeA, &pNodeB ); + // if real children are used, skip + if ( Abc_ObjFanin0(pNode)->vFanouts.nSize > 1 || Abc_ObjFanin1(pNode)->vFanouts.nSize > 1 ) + continue; + + if ( pNodeC->vFanouts.nSize == 2 ) + pNodeC->fMarkB = 0; + if ( Abc_ObjRegular(pNodeA) == Abc_ObjRegular(pNodeB) && Abc_ObjRegular(pNodeA)->vFanouts.nSize == 2 ) + Abc_ObjRegular(pNodeA)->fMarkB = 0; + } + // mark the PO drivers +// Abc_NtkForEachCo( pNtk, pNode, i ) +// Abc_ObjFanin0(pNode)->fMarkB = 1; + nFactors = 0; + Abc_AigForEachAnd( pNtk, pNode, i ) + nFactors += pNode->fMarkB; + printf( "Total nodes = %6d. Total factors = %6d.\n", Abc_NtkNodeNum(pNtk), nFactors ); + } +*/ // start the manager pParams->nIdsMax = Abc_NtkObjNumMax( pNtk ); p = Cut_ManStart( pParams ); @@ -104,8 +135,13 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams ) } Vec_PtrFree( vNodes ); Vec_IntFree( vChoices ); +/* if ( pParams->fMulti ) - Abc_NtkBalanceDetach(pNtk); + { + Abc_NtkForEachObj( pNtk, pNode, i ) + pNode->fMarkB = 0; + } +*/ PRT( "Total", clock() - clk ); //Abc_NtkPrintCuts_( p, pNtk, 0 ); // Cut_ManPrintStatsToFile( p, pNtk->pSpec, clock() - clk ); @@ -282,14 +318,14 @@ printf( "Converged after %d iterations.\n", nIters ); SeeAlso [] ***********************************************************************/ -void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj ) +void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fMulti ) { void * pList; if ( pList = Abc_NodeReadCuts( p, pObj ) ) return pList; - Abc_NodeGetCutsRecursive( p, Abc_ObjFanin0(pObj) ); - Abc_NodeGetCutsRecursive( p, Abc_ObjFanin1(pObj) ); - return Abc_NodeGetCuts( p, pObj, 0 ); + Abc_NodeGetCutsRecursive( p, Abc_ObjFanin0(pObj), fMulti ); + Abc_NodeGetCutsRecursive( p, Abc_ObjFanin1(pObj), fMulti ); + return Abc_NodeGetCuts( p, pObj, fMulti ); } /**Function************************************************************* @@ -305,7 +341,8 @@ void * Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj ) ***********************************************************************/ void * Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fMulti ) { - int fTriv = (!fMulti) || (pObj->pCopy != NULL); +// int fTriv = (!fMulti) || pObj->fMarkB; + int fTriv = (!fMulti) || (pObj->vFanouts.nSize > 1 && !Abc_NodeIsMuxControlType(pObj)); assert( Abc_NtkIsStrash(pObj->pNtk) ); assert( Abc_ObjFaninNum(pObj) == 2 ); return Cut_NodeComputeCuts( p, pObj->Id, Abc_ObjFaninId0(pObj), Abc_ObjFaninId1(pObj), diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c index a73ab2b5..9dd5ea3a 100644 --- a/src/base/abci/abcDsd.c +++ b/src/base/abci/abcDsd.c @@ -446,7 +446,7 @@ void Abc_NodeDecompDsdAndMux( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes, Dsd_Manager /**Function************************************************************* - Synopsis [Performs decomposition of one node.] + Synopsis [Checks if the node should be decomposed by DSD.] Description [] diff --git a/src/base/abci/abcEspresso.c b/src/base/abci/abcEspresso.c new file mode 100644 index 00000000..ee6598c9 --- /dev/null +++ b/src/base/abci/abcEspresso.c @@ -0,0 +1,244 @@ +/**CFile**************************************************************** + + FileName [abcEspresso.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Procedures to minimize SOPs using Espresso.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcEspresso.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "espresso.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static void Abc_NodeEspresso( Abc_Obj_t * pNode ); +static pset_family Abc_SopToEspresso( char * pSop ); +static char * Abc_SopFromEspresso( Extra_MmFlex_t * pMan, pset_family Cover ); +static pset_family Abc_EspressoMinimize( pset_family pOnset, pset_family pDcset ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Minimizes SOP representations using Espresso.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkEspresso( Abc_Ntk_t * pNtk, int fVerbose ) +{ + Abc_Obj_t * pNode; + int i; + assert( Abc_NtkIsLogic(pNtk) ); + // convert the network to have SOPs + if ( Abc_NtkHasMapping(pNtk) ) + Abc_NtkUnmap(pNtk); + else if ( Abc_NtkHasBdd(pNtk) ) + Abc_NtkBddToSop(pNtk); + // minimize SOPs of all nodes + Abc_NtkForEachNode( pNtk, pNode, i ) + if ( i ) Abc_NodeEspresso( pNode ); +} + +/**Function************************************************************* + + Synopsis [Minimizes SOP representation of one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeEspresso( Abc_Obj_t * pNode ) +{ + extern void define_cube_size( int n ); + pset_family Cover; + int fCompl; + + assert( Abc_ObjIsNode(pNode) ); + // define the cube for this node + define_cube_size( Abc_ObjFaninNum(pNode) ); + // create the Espresso cover + fCompl = Abc_SopIsComplement( pNode->pData ); + Cover = Abc_SopToEspresso( pNode->pData ); + // perform minimization + Cover = Abc_EspressoMinimize( Cover, NULL ); // deletes also cover + // convert back onto the node's SOP representation + pNode->pData = Abc_SopFromEspresso( pNode->pNtk->pManFunc, Cover ); + if ( fCompl ) Abc_SopComplement( pNode->pData ); + sf_free(Cover); +} + +/**Function************************************************************* + + Synopsis [Converts SOP in ABC into SOP representation in Espresso.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +pset_family Abc_SopToEspresso( char * pSop ) +{ + char * pCube; + pset_family Cover; + pset set; + int nCubes, nVars, Value, v; + + if ( pSop == NULL ) + return NULL; + + nVars = Abc_SopGetVarNum(pSop); + nCubes = Abc_SopGetCubeNum(pSop); + assert( cube.size == 2 * nVars ); + + if ( Abc_SopIsConst0(pSop) ) + { + Cover = sf_new(0, cube.size); + return Cover; + } + if ( Abc_SopIsConst1(pSop) ) + { + Cover = sf_new(1, cube.size); + set = GETSET(Cover, Cover->count++); + set_copy( set, cube.fullset ); + return Cover; + } + + // create the cover + Cover = sf_new(nCubes, cube.size); + // fill in the cubes + Abc_SopForEachCube( pSop, nVars, pCube ) + { + set = GETSET(Cover, Cover->count++); + set_copy( set, cube.fullset ); + Abc_CubeForEachVar( pCube, Value, v ) + { + if ( Value == '0' ) + set_remove(set, 2*v+1); + else if ( Value == '1' ) + set_remove(set, 2*v); + } + } + return Cover; +} + +/**Function************************************************************* + + Synopsis [Converts SOP representation in Espresso into SOP in ABC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Abc_SopFromEspresso( Extra_MmFlex_t * pMan, pset_family Cover ) +{ + pset set; + char * pSop, * pCube; + int Lit, nVars, nCubes, i, k; + + nVars = Cover->sf_size/2; + nCubes = Cover->count; + + pSop = Abc_SopStart( pMan, nCubes, nVars ); + + // go through the cubes + i = 0; + Abc_SopForEachCube( pSop, nVars, pCube ) + { + set = GETSET(Cover, i++); + for ( k = 0; k < nVars; k++ ) + { + Lit = GETINPUT(set, k); + if ( Lit == ZERO ) + pCube[k] = '0'; + else if ( Lit == ONE ) + pCube[k] = '1'; + } + } + return pSop; +} + + +/**Function************************************************************* + + Synopsis [Minimizes the cover using Espresso.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +pset_family Abc_EspressoMinimize( pset_family pOnset, pset_family pDcset ) +{ + pset_family pOffset; + int fNewDcset, i; + int fSimple = 0; + int fSparse = 0; + + if ( fSimple ) + { + for ( i = 0; i < cube.num_vars; i++ ) + pOnset = d1merge( pOnset, i ); + pOnset = sf_contain( pOnset ); + return pOnset; + } + + // create the dcset + fNewDcset = (pDcset == NULL); + if ( pDcset == NULL ) + pDcset = sf_new( 1, cube.size ); + pDcset->wsize = pOnset->wsize; + pDcset->sf_size = pOnset->sf_size; + + // derive the offset + if ( pDcset->sf_size == 0 || pDcset->count == 0 ) + pOffset = complement(cube1list(pOnset)); + else + pOffset = complement(cube2list(pOnset, pDcset)); + + // perform minimization + skip_make_sparse = !fSparse; + pOnset = espresso( pOnset, pDcset, pOffset ); + + // free covers + sf_free( pOffset ); + if ( fNewDcset ) + sf_free( pDcset ); + return pOnset; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c index d59f21a0..4aae6ba5 100644 --- a/src/base/abci/abcFraig.c +++ b/src/base/abci/abcFraig.c @@ -26,7 +26,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ); +extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ); static Abc_Ntk_t * Abc_NtkFromFraig2( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ); static Abc_Obj_t * Abc_NodeFromFraig_rec( Abc_Ntk_t * pNtkNew, Fraig_Node_t * pNodeFraig ); static void Abc_NtkFromFraig2_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNode, Vec_Ptr_t * vNodeReprs ); diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c index 128e054a..39bf15aa 100644 --- a/src/base/abci/abcMap.c +++ b/src/base/abci/abcMap.c @@ -105,7 +105,7 @@ clk = clock(); Map_ManFree( pMan ); return NULL; } - Map_ManPrintStatsToFile( pNtk->pSpec, Map_ManReadAreaFinal(pMan), Map_ManReadRequiredGlo(pMan), clock()-clk ); +// Map_ManPrintStatsToFile( pNtk->pSpec, Map_ManReadAreaFinal(pMan), Map_ManReadRequiredGlo(pMan), clock()-clk ); // reconstruct the network after mapping pNtkNew = Abc_NtkFromMap( pMan, pNtk ); diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index 44130a20..30fc3a79 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -90,7 +90,7 @@ Abc_Ntk_t * Abc_NtkMiterInt( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb ) // start the new network pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG ); sprintf( Buffer, "%s_%s_miter", pNtk1->pName, pNtk2->pName ); - pNtkMiter->pName = util_strsav(Buffer); + pNtkMiter->pName = Extra_UtilStrsav(Buffer); // perform strashing Abc_NtkMiterPrepare( pNtk1, pNtk2, pNtkMiter, fComb ); @@ -308,7 +308,7 @@ Abc_Ntk_t * Abc_NtkMiterForCofactors( Abc_Ntk_t * pNtk, int Out, int In1, int In // start the new network pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG ); sprintf( Buffer, "%s_miter", Abc_ObjName(Abc_NtkCo(pNtk, Out)) ); - pNtkMiter->pName = util_strsav(Buffer); + pNtkMiter->pName = Extra_UtilStrsav(Buffer); // get the root output pRoot = Abc_NtkCo( pNtk, Out ); @@ -372,7 +372,7 @@ Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist ) // start the new network pNtkMiter = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG ); - pNtkMiter->pName = util_strsav( Abc_ObjName(Abc_NtkCo(pNtk, 0)) ); + pNtkMiter->pName = Extra_UtilStrsav( Abc_ObjName(Abc_NtkCo(pNtk, 0)) ); // get the root output pRoot = Abc_NtkCo( pNtk, 0 ); @@ -384,14 +384,16 @@ Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist ) // add the first cofactor Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot ); // save the output - pOutput1 = Abc_ObjFanin0(pRoot)->pCopy; +// pOutput1 = Abc_ObjFanin0(pRoot)->pCopy; + pOutput1 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot)->pCopy, Abc_ObjFaninC0(pRoot) ); // set the second cofactor Abc_NtkCi(pNtk, In)->pCopy = Abc_NtkConst1( pNtkMiter ); // add the second cofactor Abc_NtkMiterAddCone( pNtk, pNtkMiter, pRoot ); // save the output - pOutput2 = Abc_ObjFanin0(pRoot)->pCopy; +// pOutput2 = Abc_ObjFanin0(pRoot)->pCopy; + pOutput2 = Abc_ObjNotCond( Abc_ObjFanin0(pRoot)->pCopy, Abc_ObjFaninC0(pRoot) ); // create the miter of the two outputs if ( fExist ) @@ -461,7 +463,7 @@ int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter ) assert( Abc_NtkIsStrash(pMiter) ); Abc_NtkForEachPo( pMiter, pNodePo, i ) { - pChild = Abc_ObjChild0( Abc_NtkPo(pMiter,i) ); + pChild = Abc_ObjChild0( pNodePo ); if ( Abc_ObjIsNode(Abc_ObjRegular(pChild)) && Abc_NodeIsConst(pChild) ) { assert( Abc_ObjRegular(pChild) == Abc_NtkConst1(pMiter) ); @@ -552,7 +554,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial ) // start the new network pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG ); sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames ); - pNtkFrames->pName = util_strsav(Buffer); + pNtkFrames->pName = Extra_UtilStrsav(Buffer); // create new latches (or their initial values) and remember them in the new latches if ( !fInitial ) { @@ -682,7 +684,7 @@ Abc_Ntk_t * Abc_NtkFrames2( Abc_Ntk_t * pNtk, int nFrames, int fInitial, AddFram // start the new network pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG ); sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames ); - pNtkFrames->pName = util_strsav(Buffer); + pNtkFrames->pName = Extra_UtilStrsav(Buffer); // create new latches (or their initial values) and remember them in the new latches if ( !fInitial ) { diff --git a/src/base/abci/abcNewAig.c b/src/base/abci/abcNewAig.c index 33f58135..ce76195a 100644 --- a/src/base/abci/abcNewAig.c +++ b/src/base/abci/abcNewAig.c @@ -56,9 +56,11 @@ Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ) { Aig_Man_t * pMan; Abc_Ntk_t * pNtkAig; - Aig_ProofType_t RetValue; +// Aig_ProofType_t RetValue; int fCleanup = 1; int nNodes; + extern void Aig_MffcTest( Aig_Man_t * pMan ); + assert( !Abc_NtkIsNetlist(pNtk) ); assert( !Abc_NtkIsSeq(pNtk) ); @@ -70,6 +72,10 @@ Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ) // convert to the AIG manager pMan = Abc_NtkToAig( pNtk ); + + Aig_MffcTest( pMan ); + +/* // execute a command in the AIG manager RetValue = Aig_FraigProve( pMan ); if ( RetValue == AIG_PROOF_SAT ) @@ -80,6 +86,7 @@ Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ) printf( "Undecided.\n" ); else assert( 0 ); +*/ // convert from the AIG manager pNtkAig = Abc_NtkFromAig( pNtk, pMan ); @@ -173,6 +180,8 @@ Aig_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld ) Abc_NtkConst1(pNtkOld)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan); Abc_NtkForEachCi( pNtkOld, pObj, i ) pObj->pCopy = (Abc_Obj_t *)Aig_NodeCreatePi(pMan); + Abc_NtkForEachCo( pNtkOld, pObj, i ) + pObj->pCopy = (Abc_Obj_t *)Aig_NodeCreatePo(pMan); // perform the conversion of the internal nodes Abc_NtkStrashPerformAig( pNtkOld, pMan ); // create the POs @@ -180,7 +189,7 @@ Aig_Man_t * Abc_NtkToAig( Abc_Ntk_t * pNtkOld ) { pFanin = (Aig_Node_t *)Abc_ObjFanin0(pObj)->pCopy; pFanin = Aig_NotCond( pFanin, Abc_ObjFaninC0(pObj) ); - pObj->pCopy = (Abc_Obj_t *)Aig_NodeCreatePo( pMan, pFanin ); + Aig_NodeConnectPo( pMan, (Aig_Node_t *)pObj->pCopy, pFanin ); } return pMan; } diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c index 6257bd08..b961ec15 100644 --- a/src/base/abci/abcNtbdd.c +++ b/src/base/abci/abcNtbdd.c @@ -79,7 +79,7 @@ Abc_Ntk_t * Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo // start the network pNtk = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD ); - pNtk->pName = util_strsav(pNamePo); + pNtk->pName = Extra_UtilStrsav(pNamePo); // make sure the new manager has enough inputs Cudd_bddIthVar( pNtk->pManFunc, Vec_PtrSize(vNamesPi) ); // add the PIs corresponding to the names diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c new file mode 100644 index 00000000..18ee9a3f --- /dev/null +++ b/src/base/abci/abcProve.c @@ -0,0 +1,232 @@ +/**CFile**************************************************************** + + FileName [abcProve.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [Proves the miter using AIG rewriting, FRAIGing, and SAT solving.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcProve.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "fraig.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern int Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, int fVerbose ); +extern int Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose ); +extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk ); + +static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue ); +static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Attempts to solve the miter using a number of tricks.] + + Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT. Returns + a simplified version of the original network (or a constant 0 network). + In case the network is not a constant zero and a SAT assignment is found, + pNtk->pModel contains a satisfying assignment.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fUseRewrite, int fUseFraig, int fVerbose ) +{ + Abc_Ntk_t * pNtk, * pNtkTemp; + int nConfsStart = 1000, nImpsStart = 0, nBTLimitStart = 2; + int nConfs, nImps, nBTLimit, RetValue; + int nIter = 0, clk, timeStart = clock(); + + // get the starting network + pNtk = *ppNtk; + assert( Abc_NtkIsStrash(pNtk) ); + assert( Abc_NtkPoNum(pNtk) == 1 ); + + // set the initial limits + nConfs = !nConfLimit? nConfsStart : ABC_MIN( nConfsStart, nConfLimit ); + nImps = !nImpLimit ? nImpsStart : ABC_MIN( nImpsStart , nImpLimit ); + nBTLimit = nBTLimitStart; + + if ( fVerbose ) + printf( "Global resource limits: ConfsLim = %6d. ImpsLim = %d.\n", nConfLimit, nImpLimit ); + + // if SAT only, solve without iteration + if ( !fUseRewrite && !fUseFraig ) + { + clk = clock(); + RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, 0 ); + Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose ); + *ppNtk = pNtk; + return RetValue; + } + + // check the current resource limits + do { + nIter++; + + if ( fVerbose ) + printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter, nConfs, nBTLimit ); + + // try brute-force SAT + clk = clock(); + RetValue = Abc_NtkMiterSat( pNtk, nConfs, nImps, 0 ); + Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose ); + if ( RetValue >= 0 ) + break; + + if ( fUseRewrite ) + { + clk = clock(); + + // try rewriting + Abc_NtkRewrite( pNtk, 0, 0, 0 ); + if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 ) + break; + Abc_NtkRefactor( pNtk, 10, 16, 0, 0, 0, 0 ); + if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 ) + break; + pNtk = Abc_NtkBalance( pNtkTemp = pNtk, 0, 0, 0 ); Abc_NtkDelete( pNtkTemp ); + if ( (RetValue = Abc_NtkMiterIsConstant(pNtk)) >= 0 ) + break; + + Abc_NtkMiterPrint( pNtk, "Rewriting ", clk, fVerbose ); + } + + if ( fUseFraig ) + { + // try FRAIGing + clk = clock(); + pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, nBTLimit, &RetValue ); Abc_NtkDelete( pNtkTemp ); + Abc_NtkMiterPrint( pNtk, "FRAIGing ", clk, fVerbose ); + if ( RetValue >= 0 ) + break; + } + + // increase resource limits + nConfs = ABC_MIN( nConfs * 3 / 2, 1000000000 ); + nImps = ABC_MIN( nImps * 3 / 2, 1000000000 ); + nBTLimit = ABC_MIN( nBTLimit * 8, 1000000000 ); + + // timeout at 5 minutes + if ( clock() - timeStart >= 300 * CLOCKS_PER_SEC ) + break; + if ( nIter == 4 ) + break; + } + while ( (nConfLimit == 0 || nConfs <= nConfLimit) && + (nImpLimit == 0 || nImps <= nImpLimit ) ); + + // try to prove it using brute force SAT + if ( RetValue < 0 ) + { + clk = clock(); + RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, 0 ); + Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose ); + } + + *ppNtk = pNtk; + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Attempts to solve the miter using a number of tricks.] + + Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue ) +{ + Abc_Ntk_t * pNtkNew; + Fraig_Params_t Params, * pParams = &Params; + Fraig_Man_t * pMan; + int nWords1, nWords2, nWordsMin, RetValue; + int * pModel; + + // to determine the number of simulation patterns + // use the following strategy + // at least 64 words (32 words random and 32 words dynamic) + // no more than 256M for one circuit (128M + 128M) + nWords1 = 32; + nWords2 = (1<<27) / (Abc_NtkNodeNum(pNtk) + Abc_NtkCiNum(pNtk)); + nWordsMin = ABC_MIN( nWords1, nWords2 ); + + // set the FRAIGing parameters + Fraig_ParamsSetDefault( pParams ); + pParams->nPatsRand = nWordsMin * 32; // the number of words of random simulation info + pParams->nPatsDyna = nWordsMin * 32; // the number of words of dynamic simulation info + pParams->nBTLimit = nBTLimit; // the max number of backtracks + pParams->nSeconds = -1; // the runtime limit + pParams->fTryProve = 0; // do not try to prove the final miter + pParams->fDoSparse = 1; // try proving sparse functions + pParams->fVerbose = 0; + + // transform the target into a fraig + pMan = Abc_NtkToFraig( pNtk, pParams, 0, 0 ); + Fraig_ManProveMiter( pMan ); + RetValue = Fraig_ManCheckMiter( pMan ); + + // save model + if ( RetValue == 0 ) + { + pModel = Fraig_ManReadModel( pMan ); + FREE( pNtk->pModel ); + pNtk->pModel = ALLOC( int, Abc_NtkCiNum(pNtk) ); + memcpy( pNtk->pModel, pModel, sizeof(int) * Abc_NtkCiNum(pNtk) ); + } + // create the network + pNtkNew = Abc_NtkFromFraig( pMan, pNtk ); + // delete the fraig manager + Fraig_ManFree( pMan ); + *pRetValue = RetValue; + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Attempts to solve the miter using a number of tricks.] + + Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose ) +{ + if ( !fVerbose ) + return; + printf( "Nodes = %7d. Levels = %4d. ", Abc_NtkNodeNum(pNtk), Abc_AigGetLevelNum(pNtk) ); + PRT( pString, clock() - clk ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c index ea2f808c..cfb05aee 100644 --- a/src/base/abci/abcRenode.c +++ b/src/base/abci/abcRenode.c @@ -407,7 +407,7 @@ void Abc_NtkRenodeSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax ) continue; if ( pNode->fMarkA == 0 ) continue; - // continue cutting branches ntil it meets the fanin limit + // continue cutting branches until it meets the fanin limit while ( Abc_NtkRenodeLimit(pNode, vCone, nFaninMax) ); assert( vCone->nSize <= nFaninMax ); } diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c new file mode 100644 index 00000000..0b4c80c8 --- /dev/null +++ b/src/base/abci/abcRestruct.c @@ -0,0 +1,1026 @@ +/**CFile**************************************************************** + + FileName [abcRestruct.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Network and node package.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: abcRestruct.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "abc.h" +#include "dec.h" +#include "dsd.h" +#include "cut.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Abc_ManRst_t_ Abc_ManRst_t; +struct Abc_ManRst_t_ +{ + // the network + Abc_Ntk_t * pNtk; // the network for restructuring + // user specified parameters + int nCutMax; // the limit on the size of the supernode + int fUpdateLevel; // turns on watching the number of levels + int fUseZeros; // turns on zero-cost replacements + int fVerbose; // the verbosity flag + // internal data structures + DdManager * dd; // the BDD manager + Dsd_Manager_t * pManDsd; // the DSD manager + Vec_Ptr_t * vVisited; // temporary + Vec_Ptr_t * vLeaves; // temporary + Vec_Ptr_t * vDecs; // temporary + // node statistics + int nLastGain; + int nCutsConsidered; + int nCutsExplored; + int nNodesConsidered; + int nNodesRestructured; + int nNodesGained; + // runtime statistics + int timeCut; + int timeBdd; + int timeDsd; + int timeEval; + int timeRes; + int timeNtk; + int timeTotal; +}; + +static Dec_Graph_t * Abc_NodeRestructure( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_t * pCutList ); +static Dec_Graph_t * Abc_NodeRestructureCut( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_t * pCut ); +static Dec_Graph_t * Abc_NodeEvaluateDsd( Abc_ManRst_t * pManRst, Dsd_Node_t * pNodeDsd, Abc_Obj_t * pRoot, int Required, int nNodesSaved, int * pnNodesAdded ); + +static Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fMulti ); +static Abc_ManRst_t * Abc_NtkManRstStart( int nCutMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose ); +static void Abc_NtkManRstStop( Abc_ManRst_t * p ); +static void Abc_NtkManRstPrintStats( Abc_ManRst_t * p ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Implements AIG restructuring.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkRestructure( Abc_Ntk_t * pNtk, int nCutMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose ) +{ + ProgressBar * pProgress; + Abc_ManRst_t * pManRst; + Cut_Man_t * pManCut; + Cut_Cut_t * pCutList; + Dec_Graph_t * pGraph; + Abc_Obj_t * pNode; + int clk, clkStart = clock(); + int fMulti = 1; + int i, nNodes; + + assert( Abc_NtkIsStrash(pNtk) ); + // cleanup the AIG + Abc_AigCleanup(pNtk->pManFunc); + Abc_NtkCleanCopy(pNtk); + + // compute the reverse levels if level update is requested + if ( fUpdateLevel ) + Abc_NtkStartReverseLevels( pNtk ); + + // start the restructuring manager + pManRst = Abc_NtkManRstStart( nCutMax, fUpdateLevel, fUseZeros, fVerbose ); + pManRst->pNtk = pNtk; + // start the cut manager +clk = clock(); + pManCut = Abc_NtkStartCutManForRestruct( pNtk, nCutMax, fMulti ); +pManRst->timeCut += clock() - clk; +// pNtk->pManCut = pManCut; + + // resynthesize each node once + nNodes = Abc_NtkObjNumMax(pNtk); + pProgress = Extra_ProgressBarStart( stdout, nNodes ); + Abc_NtkForEachNode( pNtk, pNode, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + // skip the constant node + if ( Abc_NodeIsConst(pNode) ) + continue; + // skip the node if it is inside the tree +// if ( Abc_ObjFanoutNum(pNode) < 2 ) +// continue; + // skip the nodes with too many fanouts + if ( Abc_ObjFanoutNum(pNode) > 1000 ) + continue; + // stop if all nodes have been tried once + if ( i >= nNodes ) + break; + // get the cuts for the given node +clk = clock(); + pCutList = Abc_NodeGetCutsRecursive( pManCut, pNode, fMulti ); +pManRst->timeCut += clock() - clk; + // evaluate these cuts +clk = clock(); + pGraph = Abc_NodeRestructure( pManRst, pNode, pCutList ); +pManRst->timeRes += clock() - clk; + if ( pGraph == NULL ) + continue; + // acceptable replacement found, update the graph +clk = clock(); + Dec_GraphUpdateNetwork( pNode, pGraph, fUpdateLevel, pManRst->nLastGain ); +pManRst->timeNtk += clock() - clk; + Dec_GraphFree( pGraph ); + } + Extra_ProgressBarStop( pProgress ); +pManRst->timeTotal = clock() - clkStart; + + // print statistics of the manager +// if ( fVerbose ) + Abc_NtkManRstPrintStats( pManRst ); + // delete the managers + Cut_ManStop( pManCut ); + Abc_NtkManRstStop( pManRst ); + // put the nodes into the DFS order and reassign their IDs + Abc_NtkReassignIds( pNtk ); +// Abc_AigCheckFaninOrder( pNtk->pManFunc ); + // fix the levels + if ( fUpdateLevel ) + Abc_NtkStopReverseLevels( pNtk ); + else + Abc_NtkGetLevelNum( pNtk ); + // check + if ( !Abc_NtkCheck( pNtk ) ) + { + printf( "Abc_NtkRefactor: The network check has failed.\n" ); + return 0; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_RestructNodeDivisors( Abc_ManRst_t * p, Abc_Obj_t * pRoot ) +{ + Abc_Obj_t * pNode, * pFanin, * pFanout; + int i, k; + // start with the leaves + Vec_PtrClear( p->vDecs ); + Vec_PtrForEachEntry( p->vLeaves, pNode, i ) + { + Vec_PtrPush( p->vDecs, pNode ); + assert( pNode->fMarkC == 0 ); + pNode->fMarkC = 1; + } + // explore the fanouts + Vec_PtrForEachEntry( p->vDecs, pNode, i ) + { + // if the fanout has both fanins in the set, add it + Abc_ObjForEachFanout( pNode, pFanout, k ) + { + if ( pFanout->fMarkC || Abc_ObjIsPo(pFanout) ) + continue; + if ( Abc_ObjFanin0(pFanout)->fMarkC && Abc_ObjFanin1(pFanout)->fMarkC ) + { + Vec_PtrPush( p->vDecs, pFanout ); + pFanout->fMarkC = 1; + } + } + } + // unmark the nodes + Vec_PtrForEachEntry( p->vDecs, pNode, i ) + pNode->fMarkC = 0; + // print the nodes + Vec_PtrForEachEntryStart( p->vDecs, pNode, i, Vec_PtrSize(p->vLeaves) ) + { + printf( "%2d %s = ", i, Abc_NodeIsTravIdCurrent(pNode)? "*" : " " ); + // find the first fanin + Vec_PtrForEachEntry( p->vDecs, pFanin, k ) + if ( Abc_ObjFanin0(pNode) == pFanin ) + break; + if ( k < Vec_PtrSize(p->vLeaves) ) + printf( "%c", 'a' + k ); + else + printf( "%d", k ); + printf( "%s ", Abc_ObjFaninC0(pNode)? "\'" : "" ); + // find the second fanin + Vec_PtrForEachEntry( p->vDecs, pFanin, k ) + if ( Abc_ObjFanin1(pNode) == pFanin ) + break; + if ( k < Vec_PtrSize(p->vLeaves) ) + printf( "%c", 'a' + k ); + else + printf( "%d", k ); + printf( "%s ", Abc_ObjFaninC1(pNode)? "\'" : "" ); + printf( "\n" ); + } +} + + +/**Function************************************************************* + + Synopsis [Starts the cut manager for rewriting.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_NodeRestructure( Abc_ManRst_t * p, Abc_Obj_t * pNode, Cut_Cut_t * pCutList ) +{ + Dec_Graph_t * pGraph; + Cut_Cut_t * pCut; + int nCuts; + p->nNodesConsidered++; + + // count the number of cuts with four inputs or more + nCuts = 0; + for ( pCut = pCutList; pCut; pCut = pCut->pNext ) + nCuts += (int)(pCut->nLeaves > 3); + printf( "-----------------------------------\n" ); + printf( "Node %6d : Factor-cuts = %5d.\n", pNode->Id, nCuts ); + + // go through the interesting cuts + for ( pCut = pCutList; pCut; pCut = pCut->pNext ) + { + if ( pCut->nLeaves < 4 ) + continue; + if ( pGraph = Abc_NodeRestructureCut( p, pNode, pCut ) ) + return pGraph; + } + return NULL; +} + +/**Function************************************************************* + + Synopsis [Starts the cut manager for rewriting.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_NodeRestructureCut( Abc_ManRst_t * p, Abc_Obj_t * pRoot, Cut_Cut_t * pCut ) +{ + Dec_Graph_t * pGraph; + Dsd_Node_t * pNodeDsd; + Abc_Obj_t * pLeaf; + DdNode * bFunc; + int nNodesSaved, nNodesAdded; + int Required, nMaxSize, clk, i; + int fVeryVerbose = 0; + + p->nCutsConsidered++; + + // get the required time for the node + Required = p->fUpdateLevel? Abc_NodeReadRequiredLevel(pRoot) : ABC_INFINITY; + + // collect the leaves of the cut + Vec_PtrClear( p->vLeaves ); + for ( i = 0; i < (int)pCut->nLeaves; i++ ) + { + pLeaf = Abc_NtkObj(pRoot->pNtk, pCut->pLeaves[i]); + if ( pLeaf == NULL ) // the so-called "bad cut phenomenon" is due to removed nodes + return NULL; + Vec_PtrPush( p->vLeaves, pLeaf ); + } +clk = clock(); + // collect the internal nodes of the cut + Abc_NodeConeCollect( &pRoot, 1, p->vLeaves, p->vVisited, 0 ); + // derive the BDD of the cut + bFunc = Abc_NodeConeBdd( p->dd, p->dd->vars, pRoot, p->vLeaves, p->vVisited ); Cudd_Ref( bFunc ); +p->timeBdd += clock() - clk; + + // consider the special case, when the function is a constant + if ( Cudd_IsConstant(bFunc) ) + { + p->nLastGain = Abc_NodeMffcSize( pRoot ); + p->nNodesGained += p->nLastGain; + p->nNodesRestructured++; + Cudd_RecursiveDeref( p->dd, bFunc ); + if ( Cudd_IsComplement(bFunc) ) + return Dec_GraphCreateConst0(); + return Dec_GraphCreateConst1(); + } + +clk = clock(); + // try disjoint support decomposition + pNodeDsd = Dsd_DecomposeOne( p->pManDsd, bFunc ); +p->timeDsd += clock() - clk; + + + // skip nodes with non-decomposable blocks + Dsd_TreeNodeGetInfoOne( pNodeDsd, NULL, &nMaxSize ); + if ( nMaxSize > 3 ) + { + Cudd_RecursiveDeref( p->dd, bFunc ); + return NULL; + } +/* + // skip nodes that cannot be improved + if ( Vec_PtrSize(p->vVisited) <= Dsd_TreeGetAigCost(pNodeDsd) ) + { + Cudd_RecursiveDeref( p->dd, bFunc ); + return NULL; + } +*/ + + p->nCutsExplored++; + + // mark the fanin boundary + // (can mark only essential fanins, belonging to bNodeFunc!) + Vec_PtrForEachEntry( p->vLeaves, pLeaf, i ) + pLeaf->vFanouts.nSize++; + // label MFFC with current traversal ID + Abc_NtkIncrementTravId( pRoot->pNtk ); + nNodesSaved = Abc_NodeMffcLabel( pRoot ); + // unmark the fanin boundary and set the fanins as leaves in the form + Vec_PtrForEachEntry( p->vLeaves, pLeaf, i ) + pLeaf->vFanouts.nSize--; + + + printf( "%5d : Cut-size = %d. Old AIG = %2d. New AIG = %2d. Old MFFC = %2d.\n", + pRoot->Id, pCut->nLeaves, Vec_PtrSize(p->vVisited), Dsd_TreeGetAigCost(pNodeDsd), + nNodesSaved ); + Dsd_NodePrint( stdout, pNodeDsd ); + + Abc_RestructNodeDivisors( p, pRoot ); + + if ( pRoot->Id == 433 ) + { + int x = 0; + } + + // detect how many new nodes will be added (while taking into account reused nodes) +clk = clock(); + pGraph = Abc_NodeEvaluateDsd( p, pNodeDsd, pRoot, Required, nNodesSaved, &nNodesAdded ); +// pGraph = NULL; +p->timeEval += clock() - clk; + + // quit if there is no improvement + if ( nNodesAdded == -1 || nNodesAdded == nNodesSaved && !p->fUseZeros ) + { + Cudd_RecursiveDeref( p->dd, bFunc ); + if ( pGraph ) Dec_GraphFree( pGraph ); + return NULL; + } + + + // print stats + printf( "%5d : Cut-size = %d. Old AIG = %2d. New AIG = %2d. Old MFFC = %2d. New MFFC = %2d. Gain = %d.\n", + pRoot->Id, pCut->nLeaves, Vec_PtrSize(p->vVisited), Dsd_TreeGetAigCost(pNodeDsd), + nNodesSaved, nNodesAdded, (nNodesAdded == -1)? 0 : nNodesSaved-nNodesAdded ); +// Dsd_NodePrint( stdout, pNodeDsd ); +// Dec_GraphPrint( stdout, pGraph, NULL, NULL ); + + + // compute the total gain in the number of nodes + p->nLastGain = nNodesSaved - nNodesAdded; + p->nNodesGained += p->nLastGain; + p->nNodesRestructured++; + + // report the progress + if ( fVeryVerbose ) + { + printf( "Node %6s : ", Abc_ObjName(pRoot) ); + printf( "Cone = %2d. ", p->vLeaves->nSize ); + printf( "BDD = %2d. ", Cudd_DagSize(bFunc) ); + printf( "FF = %2d. ", 1 + Dec_GraphNodeNum(pGraph) ); + printf( "MFFC = %2d. ", nNodesSaved ); + printf( "Add = %2d. ", nNodesAdded ); + printf( "GAIN = %2d. ", p->nLastGain ); + printf( "\n" ); + } + Cudd_RecursiveDeref( p->dd, bFunc ); + return pGraph; +} + + +/**Function************************************************************* + + Synopsis [Moves closer to the end the node that is best for sharing.] + + Description [If the flag is set, tries to find an EXOR, otherwise, tries + to find an OR.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeEdgeDsdPermute( Dec_Graph_t * pGraph, Abc_ManRst_t * pManRst, Vec_Int_t * vEdges, int fExor ) +{ + Dec_Edge_t eNode1, eNode2, eNode3; + Abc_Obj_t * pNode1, * pNode2, * pNode3, * pTemp; + int LeftBound = 0, RightBound, i; + // get the right bound + RightBound = Vec_IntSize(vEdges) - 2; + assert( LeftBound <= RightBound ); + if ( LeftBound == RightBound ) + return; + // get the two last nodes + eNode1 = Dec_IntToEdge( Vec_IntEntry(vEdges, RightBound + 1) ); + eNode2 = Dec_IntToEdge( Vec_IntEntry(vEdges, RightBound ) ); + pNode1 = Dec_GraphNode( pGraph, eNode1.Node )->pFunc; + pNode2 = Dec_GraphNode( pGraph, eNode2.Node )->pFunc; + pNode1 = !pNode1? NULL : Abc_ObjNotCond( pNode1, eNode1.fCompl ); + pNode2 = !pNode2? NULL : Abc_ObjNotCond( pNode2, eNode2.fCompl ); + // quit if the last node does not exist + if ( pNode1 == NULL ) + return; + // find the first node that can be shared + for ( i = RightBound; i >= LeftBound; i-- ) + { + // get the third node + eNode3 = Dec_IntToEdge( Vec_IntEntry(vEdges, i) ); + pNode3 = Dec_GraphNode( pGraph, eNode3.Node )->pFunc; + pNode3 = !pNode3? NULL : Abc_ObjNotCond( pNode3, eNode3.fCompl ); + if ( pNode3 == NULL ) + continue; + // check if the node exists + if ( fExor ) + { + if ( pNode1 && pNode3 ) + { + pTemp = Abc_AigXorLookup( pManRst->pNtk->pManFunc, pNode1, pNode3, NULL ); + if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) ) + continue; + + if ( pNode3 == pNode2 ) + return; + Vec_IntWriteEntry( vEdges, i, Dec_EdgeToInt(eNode2) ); + Vec_IntWriteEntry( vEdges, RightBound, Dec_EdgeToInt(eNode3) ); + return; + } + } + else + { + if ( pNode1 && pNode3 ) + { + pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, Abc_ObjNot(pNode1), Abc_ObjNot(pNode3) ); + if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) ) + continue; + + if ( eNode3.Node == eNode2.Node ) + return; + Vec_IntWriteEntry( vEdges, i, Dec_EdgeToInt(eNode2) ); + Vec_IntWriteEntry( vEdges, RightBound, Dec_EdgeToInt(eNode3) ); + return; + } + } + } +} + +/**Function************************************************************* + + Synopsis [Adds the new edge in the given order.] + + Description [Similar to Vec_IntPushOrder, except in decreasing order.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NodeEdgeDsdPushOrdered( Dec_Graph_t * pGraph, Vec_Int_t * vEdges, int Edge ) +{ + int i, NodeOld, NodeNew; + vEdges->nSize++; + for ( i = vEdges->nSize-2; i >= 0; i-- ) + { + NodeOld = Dec_IntToEdge(vEdges->pArray[i]).Node; + NodeNew = Dec_IntToEdge(Edge).Node; + // use <= because we are trying to push the new (non-existent) nodes as far as possible + if ( Dec_GraphNode(pGraph, NodeOld)->Level <= Dec_GraphNode(pGraph, NodeNew)->Level ) + vEdges->pArray[i+1] = vEdges->pArray[i]; + else + break; + } + vEdges->pArray[i+1] = Edge; +} + +/**Function************************************************************* + + Synopsis [Evaluation one DSD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Edge_t Abc_NodeEvaluateDsd_rec( Dec_Graph_t * pGraph, Abc_ManRst_t * pManRst, Dsd_Node_t * pNodeDsd, int Required, int nNodesSaved, int * pnNodesAdded ) +{ + Dec_Edge_t eNode1, eNode2, eNode3, eResult, eQuit = { 0, 2006 }; + Abc_Obj_t * pNode1, * pNode2, * pNode3, * pNode4, * pTemp; + Dsd_Node_t * pChildDsd; + Dsd_Type_t DecType; + Vec_Int_t * vEdges; + int Level1, Level2, Level3, Level4; + int i, Index, fCompl, Type; + + // remove the complemented attribute + fCompl = Dsd_IsComplement( pNodeDsd ); + pNodeDsd = Dsd_Regular( pNodeDsd ); + + // consider the trivial case + DecType = Dsd_NodeReadType( pNodeDsd ); + if ( DecType == DSD_NODE_BUF ) + { + Index = Dsd_NodeReadFunc(pNodeDsd)->index; + assert( Index < Dec_GraphLeaveNum(pGraph) ); + eResult = Dec_EdgeCreate( Index, fCompl ); + return eResult; + } + assert( DecType == DSD_NODE_OR || DecType == DSD_NODE_EXOR || DecType == DSD_NODE_PRIME ); + + // solve the problem for the children + vEdges = Vec_IntAlloc( Dsd_NodeReadDecsNum(pNodeDsd) ); + Dsd_NodeForEachChild( pNodeDsd, i, pChildDsd ) + { + eResult = Abc_NodeEvaluateDsd_rec( pGraph, pManRst, pChildDsd, Required, nNodesSaved, pnNodesAdded ); + if ( eResult.Node == eQuit.Node ) // infeasible + { + Vec_IntFree( vEdges ); + return eQuit; + } + // order the inputs only if this is OR or EXOR + if ( DecType == DSD_NODE_PRIME ) + Vec_IntPush( vEdges, Dec_EdgeToInt(eResult) ); + else + Abc_NodeEdgeDsdPushOrdered( pGraph, vEdges, Dec_EdgeToInt(eResult) ); + } + // the edges are sorted by the level of their nodes in decreasing order + + + // consider special cases + if ( DecType == DSD_NODE_OR ) + { + // try to balance the nodes by delay + assert( Vec_IntSize(vEdges) > 1 ); + while ( Vec_IntSize(vEdges) > 1 ) + { + // permute the last two entries + if ( Vec_IntSize(vEdges) > 2 ) + Abc_NodeEdgeDsdPermute( pGraph, pManRst, vEdges, 0 ); + // get the two last nodes + eNode1 = Dec_IntToEdge( Vec_IntPop(vEdges) ); + eNode2 = Dec_IntToEdge( Vec_IntPop(vEdges) ); + pNode1 = Dec_GraphNode( pGraph, eNode1.Node )->pFunc; + pNode2 = Dec_GraphNode( pGraph, eNode2.Node )->pFunc; + pNode1 = !pNode1? NULL : Abc_ObjNotCond( pNode1, eNode1.fCompl ); + pNode2 = !pNode2? NULL : Abc_ObjNotCond( pNode2, eNode2.fCompl ); + // check if the new node exists + pNode3 = NULL; + if ( pNode1 && pNode2 ) + { + pNode3 = Abc_AigAndLookup( pManRst->pNtk->pManFunc, Abc_ObjNot(pNode1), Abc_ObjNot(pNode2) ); + pNode3 = !pNode3? NULL : Abc_ObjNot(pNode3); + } + // create the new node + eNode3 = Dec_GraphAddNodeOr( pGraph, eNode1, eNode2 ); + // set level + Level1 = Dec_GraphNode( pGraph, eNode1.Node )->Level; + Level2 = Dec_GraphNode( pGraph, eNode2.Node )->Level; + Dec_GraphNode( pGraph, eNode3.Node )->Level = 1 + ABC_MAX(Level1, Level2); + // get the new node if possible + if ( pNode3 ) + { + Dec_GraphNode( pGraph, eNode3.Node )->pFunc = Abc_ObjNotCond(pNode3, eNode3.fCompl); + Level3 = Dec_GraphNode( pGraph, eNode3.Node )->Level; + assert( Required == ABC_INFINITY || Level3 == (int)Abc_ObjRegular(pNode3)->Level ); + } + if ( !pNode3 || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pNode3)) ) + { + (*pnNodesAdded)++; + if ( *pnNodesAdded > nNodesSaved ) + { + Vec_IntFree( vEdges ); + return eQuit; + } + } + // add the resulting node to the form + Abc_NodeEdgeDsdPushOrdered( pGraph, vEdges, Dec_EdgeToInt(eNode3) ); + } + // get the last node + eResult = Dec_IntToEdge( Vec_IntPop(vEdges) ); + Vec_IntFree( vEdges ); + // complement the graph if the node was complemented + eResult.fCompl ^= fCompl; + return eResult; + } + if ( DecType == DSD_NODE_EXOR ) + { + // try to balance the nodes by delay + assert( Vec_IntSize(vEdges) > 1 ); + while ( Vec_IntSize(vEdges) > 1 ) + { + // permute the last two entries + if ( Vec_IntSize(vEdges) > 2 ) + Abc_NodeEdgeDsdPermute( pGraph, pManRst, vEdges, 1 ); + // get the two last nodes + eNode1 = Dec_IntToEdge( Vec_IntPop(vEdges) ); + eNode2 = Dec_IntToEdge( Vec_IntPop(vEdges) ); + pNode1 = Dec_GraphNode( pGraph, eNode1.Node )->pFunc; + pNode2 = Dec_GraphNode( pGraph, eNode2.Node )->pFunc; + pNode1 = !pNode1? NULL : Abc_ObjNotCond( pNode1, eNode1.fCompl ); + pNode2 = !pNode2? NULL : Abc_ObjNotCond( pNode2, eNode2.fCompl ); + // check if the new node exists + Type = 0; + pNode3 = NULL; + if ( pNode1 && pNode2 ) + pNode3 = Abc_AigXorLookup( pManRst->pNtk->pManFunc, pNode1, pNode2, &Type ); + // create the new node + eNode3 = Dec_GraphAddNodeXor( pGraph, eNode1, eNode2, Type ); // should have the same structure as in AIG + // set level + Level1 = Dec_GraphNode( pGraph, eNode1.Node )->Level; + Level2 = Dec_GraphNode( pGraph, eNode2.Node )->Level; + Dec_GraphNode( pGraph, eNode3.Node )->Level = 2 + ABC_MAX(Level1, Level2); + // get the new node if possible + if ( pNode3 ) + { + Dec_GraphNode( pGraph, eNode3.Node )->pFunc = Abc_ObjNotCond(pNode3, eNode3.fCompl); + Level3 = Dec_GraphNode( pGraph, eNode3.Node )->Level; + assert( Required == ABC_INFINITY || Level3 == (int)Abc_ObjRegular(pNode3)->Level ); + } + if ( !pNode3 || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pNode3)) ) + { + (*pnNodesAdded)++; + if ( !pNode1 || !pNode2 ) + (*pnNodesAdded) += 2; + else if ( Type == 0 ) + { + pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, pNode1, Abc_ObjNot(pNode2) ); + if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) ) + (*pnNodesAdded)++; + pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, Abc_ObjNot(pNode1), pNode2 ); + if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) ) + (*pnNodesAdded)++; + } + else + { + pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, Abc_ObjNot(pNode1), Abc_ObjNot(pNode2) ); + if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) ) + (*pnNodesAdded)++; + pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, pNode1, pNode2 ); + if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) ) + (*pnNodesAdded)++; + } + if ( *pnNodesAdded > nNodesSaved ) + { + Vec_IntFree( vEdges ); + return eQuit; + } + } + // add the resulting node to the form + Abc_NodeEdgeDsdPushOrdered( pGraph, vEdges, Dec_EdgeToInt(eNode3) ); + } + // get the last node + eResult = Dec_IntToEdge( Vec_IntPop(vEdges) ); + Vec_IntFree( vEdges ); + // complement the graph if the node is complemented + eResult.fCompl ^= fCompl; + return eResult; + } + if ( DecType == DSD_NODE_PRIME ) + { + DdNode * bLocal, * bVar, * bCofT, * bCofE; + bLocal = Dsd_TreeGetPrimeFunction( pManRst->dd, pNodeDsd ); Cudd_Ref( bLocal ); +//Extra_bddPrint( pManRst->dd, bLocal ); + + bVar = pManRst->dd->vars[0]; + bCofE = Cudd_Cofactor( pManRst->dd, bLocal, Cudd_Not(bVar) ); Cudd_Ref( bCofE ); + bCofT = Cudd_Cofactor( pManRst->dd, bLocal, bVar ); Cudd_Ref( bCofT ); + if ( !Extra_bddIsVar(bCofE) || !Extra_bddIsVar(bCofT) ) + { + Cudd_RecursiveDeref( pManRst->dd, bCofE ); + Cudd_RecursiveDeref( pManRst->dd, bCofT ); + bVar = pManRst->dd->vars[1]; + bCofE = Cudd_Cofactor( pManRst->dd, bLocal, Cudd_Not(bVar) ); Cudd_Ref( bCofE ); + bCofT = Cudd_Cofactor( pManRst->dd, bLocal, bVar ); Cudd_Ref( bCofT ); + if ( !Extra_bddIsVar(bCofE) || !Extra_bddIsVar(bCofT) ) + { + Cudd_RecursiveDeref( pManRst->dd, bCofE ); + Cudd_RecursiveDeref( pManRst->dd, bCofT ); + bVar = pManRst->dd->vars[2]; + bCofE = Cudd_Cofactor( pManRst->dd, bLocal, Cudd_Not(bVar) ); Cudd_Ref( bCofE ); + bCofT = Cudd_Cofactor( pManRst->dd, bLocal, bVar ); Cudd_Ref( bCofT ); + if ( !Extra_bddIsVar(bCofE) || !Extra_bddIsVar(bCofT) ) + { + Cudd_RecursiveDeref( pManRst->dd, bCofE ); + Cudd_RecursiveDeref( pManRst->dd, bCofT ); + Cudd_RecursiveDeref( pManRst->dd, bLocal ); + Vec_IntFree( vEdges ); + return eQuit; + } + } + } + Cudd_RecursiveDeref( pManRst->dd, bLocal ); + // we found the control variable (bVar) and the var-cofactors (bCofT, bCofE) + + // find the graph nodes + eNode1 = Dec_IntToEdge( Vec_IntEntry(vEdges, bVar->index) ); + eNode2 = Dec_IntToEdge( Vec_IntEntry(vEdges, Cudd_Regular(bCofT)->index) ); + eNode3 = Dec_IntToEdge( Vec_IntEntry(vEdges, Cudd_Regular(bCofE)->index) ); + // add the complements to the graph nodes + eNode2.fCompl ^= Cudd_IsComplement(bCofT); + eNode3.fCompl ^= Cudd_IsComplement(bCofE); + + // because the cofactors are vars, we can just as well deref them here + Cudd_RecursiveDeref( pManRst->dd, bCofE ); + Cudd_RecursiveDeref( pManRst->dd, bCofT ); + + // find the ABC nodes + pNode1 = Dec_GraphNode( pGraph, eNode1.Node )->pFunc; + pNode2 = Dec_GraphNode( pGraph, eNode2.Node )->pFunc; + pNode3 = Dec_GraphNode( pGraph, eNode3.Node )->pFunc; + pNode1 = !pNode1? NULL : Abc_ObjNotCond( pNode1, eNode1.fCompl ); + pNode2 = !pNode2? NULL : Abc_ObjNotCond( pNode2, eNode2.fCompl ); + pNode3 = !pNode3? NULL : Abc_ObjNotCond( pNode3, eNode3.fCompl ); + + // check if the new node exists + Type = 0; + pNode4 = NULL; + if ( pNode1 && pNode2 && pNode3 ) + pNode4 = Abc_AigMuxLookup( pManRst->pNtk->pManFunc, pNode1, pNode2, pNode3, &Type ); + + // create the new node + eResult = Dec_GraphAddNodeMux( pGraph, eNode1, eNode2, eNode3, Type ); // should have the same structure as AIG + + // set level + Level1 = Dec_GraphNode( pGraph, eNode1.Node )->Level; + Level2 = Dec_GraphNode( pGraph, eNode2.Node )->Level; + Level3 = Dec_GraphNode( pGraph, eNode3.Node )->Level; + Dec_GraphNode( pGraph, eResult.Node )->Level = 2 + ABC_MAX( ABC_MAX(Level1, Level2), Level3 ); + // get the new node if possible + if ( pNode4 ) + { + Dec_GraphNode( pGraph, eResult.Node )->pFunc = Abc_ObjNotCond(pNode4, eResult.fCompl); + Level4 = Dec_GraphNode( pGraph, eResult.Node )->Level; + assert( Required == ABC_INFINITY || Level4 == (int)Abc_ObjRegular(pNode4)->Level ); + } + if ( !pNode4 || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pNode4)) ) + { + (*pnNodesAdded)++; + if ( Type == 0 ) + { + if ( !pNode1 || !pNode2 ) + (*pnNodesAdded)++; + else + { + pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, pNode1, pNode2 ); + if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) ) + (*pnNodesAdded)++; + } + if ( !pNode1 || !pNode3 ) + (*pnNodesAdded)++; + else + { + pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, Abc_ObjNot(pNode1), pNode3 ); + if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) ) + (*pnNodesAdded)++; + } + } + else + { + if ( !pNode1 || !pNode2 ) + (*pnNodesAdded)++; + else + { + pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, pNode1, Abc_ObjNot(pNode2) ); + if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) ) + (*pnNodesAdded)++; + } + if ( !pNode1 || !pNode3 ) + (*pnNodesAdded)++; + else + { + pTemp = Abc_AigAndLookup( pManRst->pNtk->pManFunc, Abc_ObjNot(pNode1), Abc_ObjNot(pNode3) ); + if ( !pTemp || Abc_NodeIsTravIdCurrent(Abc_ObjRegular(pTemp)) ) + (*pnNodesAdded)++; + } + } + if ( *pnNodesAdded > nNodesSaved ) + { + Vec_IntFree( vEdges ); + return eQuit; + } + } + + Vec_IntFree( vEdges ); + // complement the graph if the node was complemented + eResult.fCompl ^= fCompl; + return eResult; + } + Vec_IntFree( vEdges ); + return eQuit; +} + +/**Function************************************************************* + + Synopsis [Evaluation one DSD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_NodeEvaluateDsd( Abc_ManRst_t * pManRst, Dsd_Node_t * pNodeDsd, Abc_Obj_t * pRoot, int Required, int nNodesSaved, int * pnNodesAdded ) +{ + Dec_Graph_t * pGraph; + Dec_Edge_t gEdge; + Abc_Obj_t * pLeaf; + Dec_Node_t * pNode; + int i; + + // create the graph and set the leaves + pGraph = Dec_GraphCreate( Vec_PtrSize(pManRst->vLeaves) ); + Dec_GraphForEachLeaf( pGraph, pNode, i ) + { + pLeaf = Vec_PtrEntry( pManRst->vLeaves, i ); + pNode->pFunc = pLeaf; + pNode->Level = pLeaf->Level; + } + + // create the decomposition structure from the DSD + *pnNodesAdded = 0; + gEdge = Abc_NodeEvaluateDsd_rec( pGraph, pManRst, pNodeDsd, Required, nNodesSaved, pnNodesAdded ); + if ( gEdge.Node > 1000 ) // infeasible + { + *pnNodesAdded = -1; + Dec_GraphFree( pGraph ); + return NULL; + } + + // quit if the root node is the same + pLeaf = Dec_GraphNode( pGraph, gEdge.Node )->pFunc; + if ( Abc_ObjRegular(pLeaf) == pRoot ) + { + *pnNodesAdded = -1; + Dec_GraphFree( pGraph ); + return NULL; + } + + Dec_GraphSetRoot( pGraph, gEdge ); + return pGraph; +} + + + +/**Function************************************************************* + + Synopsis [Starts the cut manager for rewriting.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Cut_Man_t * Abc_NtkStartCutManForRestruct( Abc_Ntk_t * pNtk, int nCutMax, int fMulti ) +{ + static Cut_Params_t Params, * pParams = &Params; + Cut_Man_t * pManCut; + Abc_Obj_t * pObj; + int i; + // start the cut manager + memset( pParams, 0, sizeof(Cut_Params_t) ); + pParams->nVarsMax = nCutMax; // the max cut size ("k" of the k-feasible cuts) + pParams->nKeepMax = 250; // the max number of cuts kept at a node + pParams->fTruth = 0; // compute truth tables + pParams->fFilter = 1; // filter dominated cuts + pParams->fSeq = 0; // compute sequential cuts + pParams->fDrop = 0; // drop cuts on the fly + pParams->fMulti = fMulti; // compute factor-cuts + pParams->fVerbose = 0; // the verbosiness flag + pParams->nIdsMax = Abc_NtkObjNumMax( pNtk ); + pManCut = Cut_ManStart( pParams ); + if ( pParams->fDrop ) + Cut_ManSetFanoutCounts( pManCut, Abc_NtkFanoutCounts(pNtk) ); + // set cuts for PIs + Abc_NtkForEachCi( pNtk, pObj, i ) + if ( Abc_ObjFanoutNum(pObj) > 0 ) + Cut_NodeSetTriv( pManCut, pObj->Id ); + return pManCut; +} + +/**Function************************************************************* + + Synopsis [Starts the resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_ManRst_t * Abc_NtkManRstStart( int nCutMax, bool fUpdateLevel, bool fUseZeros, bool fVerbose ) +{ + Abc_ManRst_t * p; + p = ALLOC( Abc_ManRst_t, 1 ); + memset( p, 0, sizeof(Abc_ManRst_t) ); + // set the parameters + p->nCutMax = nCutMax; + p->fUpdateLevel = fUpdateLevel; + p->fUseZeros = fUseZeros; + p->fVerbose = fVerbose; + // start the BDD manager + p->dd = Cudd_Init( p->nCutMax, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + Cudd_zddVarsFromBddVars( p->dd, 2 ); + // start the DSD manager + p->pManDsd = Dsd_ManagerStart( p->dd, p->dd->size, 0 ); + // other temp datastructures + p->vVisited = Vec_PtrAlloc( 100 ); + p->vLeaves = Vec_PtrAlloc( 100 ); + p->vDecs = Vec_PtrAlloc( 100 ); + return p; +} + +/**Function************************************************************* + + Synopsis [Stops the resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkManRstStop( Abc_ManRst_t * p ) +{ + Dsd_ManagerStop( p->pManDsd ); + Extra_StopManager( p->dd ); + Vec_PtrFree( p->vDecs ); + Vec_PtrFree( p->vLeaves ); + Vec_PtrFree( p->vVisited ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Stops the resynthesis manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkManRstPrintStats( Abc_ManRst_t * p ) +{ + printf( "Refactoring statistics:\n" ); + printf( "Nodes considered = %8d.\n", p->nNodesConsidered ); + printf( "Cuts considered = %8d.\n", p->nCutsConsidered ); + printf( "Cuts explored = %8d.\n", p->nCutsExplored ); + printf( "Nodes restructured = %8d.\n", p->nNodesRestructured ); + printf( "Calculated gain = %8d.\n", p->nNodesGained ); + PRT( "Cuts ", p->timeCut ); + PRT( "Resynthesis", p->timeRes ); + PRT( " BDD ", p->timeBdd ); + PRT( " DSD ", p->timeDsd ); + PRT( " Eval ", p->timeEval ); + PRT( "AIG update ", p->timeNtk ); + PRT( "TOTAL ", p->timeTotal ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcRewrite.c b/src/base/abci/abcRewrite.c index b3b30d9a..f3360421 100644 --- a/src/base/abci/abcRewrite.c +++ b/src/base/abci/abcRewrite.c @@ -96,6 +96,14 @@ Rwr_ManAddTimeCuts( pManRwr, clock() - clk ); { Dec_Graph_t * pGraph = Rwr_ManReadDecs(pManRwr); int fCompl = Rwr_ManReadCompl(pManRwr); +/* + if ( nGain > 0 ) + { // print stats on the MFFC + extern void Abc_NodeMffsConeSuppPrint( Abc_Obj_t * pNode ); + printf( "Node %6d : Gain = %4d ", pNode->Id, nGain ); + Abc_NodeMffsConeSuppPrint( pNode ); + } +*/ // complement the FF if needed if ( fCompl ) Dec_GraphComplement( pGraph ); clk = clock(); diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c index 9c650aa9..5376444b 100644 --- a/src/base/abci/abcSat.c +++ b/src/base/abci/abcSat.c @@ -24,13 +24,7 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars ); -static int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ); - -static solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk ); - static Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk ); - static nMuxes; //////////////////////////////////////////////////////////////////////// @@ -48,13 +42,13 @@ static nMuxes; SeeAlso [] ***********************************************************************/ -int Abc_NtkMiterSat_OldAndRusty( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ) +int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fVerbose ) { solver * pSat; lbool status; int RetValue, clk; - assert( Abc_NtkIsBddLogic(pNtk) ); + assert( Abc_NtkIsStrash(pNtk) ); assert( Abc_NtkLatchNum(pNtk) == 0 ); if ( Abc_NtkPoNum(pNtk) > 1 ) @@ -84,7 +78,7 @@ int Abc_NtkMiterSat_OldAndRusty( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ) clk = clock(); if ( fVerbose ) pSat->verbosity = 1; - status = solver_solve( pSat, NULL, NULL, nSeconds ); + status = solver_solve( pSat, NULL, NULL, nConfLimit, nImpLimit ); if ( status == l_Undef ) { // printf( "The problem timed out.\n" ); @@ -107,277 +101,6 @@ int Abc_NtkMiterSat_OldAndRusty( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ) // if the problem is SAT, get the counterexample if ( status == l_True ) { - Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk ); - pNtk->pModel = solver_get_model( pSat, vCiIds->pArray, vCiIds->nSize ); - Vec_IntFree( vCiIds ); - } - // free the solver - solver_delete( pSat ); - return RetValue; -} - -/**Function************************************************************* - - Synopsis [Sets up the SAT solver.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk ) -{ - solver * pSat; - Extra_MmFlex_t * pMmFlex; - Abc_Obj_t * pNode; - Vec_Str_t * vCube; - Vec_Int_t * vVars; - char * pSop0, * pSop1; - int i, clk = clock(); - - assert( Abc_NtkIsBddLogic(pNtk) ); - - // start the data structures - pSat = solver_new(); - pMmFlex = Extra_MmFlexStart(); - vCube = Vec_StrAlloc( 100 ); - vVars = Vec_IntAlloc( 100 ); - - // add clauses for each internal nodes - Abc_NtkForEachNode( pNtk, pNode, i ) - { - // derive SOPs for both phases of the node - Abc_NodeBddToCnf( pNode, pMmFlex, vCube, &pSop0, &pSop1 ); - // add the clauses to the solver - if ( !Abc_NodeAddClauses( pSat, pSop0, pSop1, pNode, vVars ) ) - { - solver_delete( pSat ); - return NULL; - } - } - // add clauses for the POs - if ( !Abc_NodeAddClausesTop( pSat, Abc_NtkPo(pNtk, Abc_NtkPoNum(pNtk)-1), vVars ) ) - { - solver_delete( pSat ); - return NULL; - } -// Asat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 0 ); - - PRT( "Creating solver", clock() - clk ); - - // delete - Vec_StrFree( vCube ); - Vec_IntFree( vVars ); - Extra_MmFlexStop( pMmFlex, 0 ); - return pSat; -} - -/**Function************************************************************* - - Synopsis [Adds clauses for the internal node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NodeAddClauses( solver * pSat, char * pSop0, char * pSop1, Abc_Obj_t * pNode, Vec_Int_t * vVars ) -{ - Abc_Obj_t * pFanin; - int i, c, nFanins; - char * pCube; - - nFanins = Abc_ObjFaninNum( pNode ); - assert( nFanins == Abc_SopGetVarNum( pSop0 ) ); - - if ( nFanins == 0 ) - { - vVars->nSize = 0; - if ( Abc_SopIsConst1(pSop1) ) - Vec_IntPush( vVars, toLit(pNode->Id) ); - else - Vec_IntPush( vVars, neg(toLit(pNode->Id)) ); - return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); - } - - // add clauses for the negative phase - for ( c = 0; ; c++ ) - { - // get the cube - pCube = pSop0 + c * (nFanins + 3); - if ( *pCube == 0 ) - break; - // add the clause - vVars->nSize = 0; - Abc_ObjForEachFanin( pNode, pFanin, i ) - { - if ( pCube[i] == '0' ) - Vec_IntPush( vVars, toLit(pFanin->Id) ); - else if ( pCube[i] == '1' ) - Vec_IntPush( vVars, neg(toLit(pFanin->Id)) ); - } - Vec_IntPush( vVars, neg(toLit(pNode->Id)) ); - if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) - return 0; - } - - // add clauses for the positive phase - for ( c = 0; ; c++ ) - { - // get the cube - pCube = pSop1 + c * (nFanins + 3); - if ( *pCube == 0 ) - break; - // add the clause - vVars->nSize = 0; - Abc_ObjForEachFanin( pNode, pFanin, i ) - { - if ( pCube[i] == '0' ) - Vec_IntPush( vVars, toLit(pFanin->Id) ); - else if ( pCube[i] == '1' ) - Vec_IntPush( vVars, neg(toLit(pFanin->Id)) ); - } - Vec_IntPush( vVars, toLit(pNode->Id) ); - if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) - return 0; - } - return 1; -} - -/**Function************************************************************* - - Synopsis [Adds clauses for the PO node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NodeAddClausesTop( solver * pSat, Abc_Obj_t * pNode, Vec_Int_t * vVars ) -{ - Abc_Obj_t * pFanin; - - pFanin = Abc_ObjFanin0(pNode); - if ( Abc_ObjFaninC0(pNode) ) - { - vVars->nSize = 0; - Vec_IntPush( vVars, toLit(pFanin->Id) ); - Vec_IntPush( vVars, toLit(pNode->Id) ); - if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) - return 0; - - vVars->nSize = 0; - Vec_IntPush( vVars, neg(toLit(pFanin->Id)) ); - Vec_IntPush( vVars, neg(toLit(pNode->Id)) ); - if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) - return 0; - } - else - { - vVars->nSize = 0; - Vec_IntPush( vVars, neg(toLit(pFanin->Id)) ); - Vec_IntPush( vVars, toLit(pNode->Id) ); - if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) - return 0; - - vVars->nSize = 0; - Vec_IntPush( vVars, toLit(pFanin->Id) ); - Vec_IntPush( vVars, neg(toLit(pNode->Id)) ); - if ( !solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ) ) - return 0; - } - - vVars->nSize = 0; - Vec_IntPush( vVars, toLit(pNode->Id) ); - return solver_addclause( pSat, vVars->pArray, vVars->pArray + vVars->nSize ); -} - - - - - - - - - - - -/**Function************************************************************* - - Synopsis [Attempts to solve the miter using an internal SAT solver.] - - Description [Returns -1 if timed out; 0 if SAT; 1 if UNSAT.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nSeconds, int fVerbose ) -{ - solver * pSat; - lbool status; - int RetValue, clk; - - assert( Abc_NtkIsStrash(pNtk) ); - assert( Abc_NtkLatchNum(pNtk) == 0 ); - - if ( Abc_NtkPoNum(pNtk) > 1 ) - fprintf( stdout, "Warning: The miter has %d outputs. SAT will try to prove all of them.\n", Abc_NtkPoNum(pNtk) ); - - // load clauses into the solver - clk = clock(); - pSat = Abc_NtkMiterSatCreate2( pNtk ); - if ( pSat == NULL ) - return 1; -// printf( "Created SAT problem with %d variable and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) ); -// PRT( "Time", clock() - clk ); - - // simplify the problem - clk = clock(); - status = solver_simplify(pSat); -// printf( "Simplified the problem to %d variables and %d clauses. ", solver_nvars(pSat), solver_nclauses(pSat) ); -// PRT( "Time", clock() - clk ); - if ( status == 0 ) - { - solver_delete( pSat ); -// printf( "The problem is UNSATISFIABLE after simplification.\n" ); - return 1; - } - - // solve the miter - clk = clock(); - if ( fVerbose ) - pSat->verbosity = 1; - status = solver_solve( pSat, NULL, NULL, nSeconds ); - if ( status == l_Undef ) - { -// printf( "The problem timed out.\n" ); - RetValue = -1; - } - else if ( status == l_True ) - { -// printf( "The problem is SATISFIABLE.\n" ); - RetValue = 0; - } - else if ( status == l_False ) - { -// printf( "The problem is UNSATISFIABLE.\n" ); - RetValue = 1; - } - else - assert( 0 ); - PRT( "SAT solver time", clock() - clk ); - - // if the problem is SAT, get the counterexample - if ( status == l_True ) - { // Vec_Int_t * vCiIds = Abc_NtkGetCiIds( pNtk ); Vec_Int_t * vCiIds = Abc_NtkGetCiSatVarNums( pNtk ); pNtk->pModel = solver_get_model( pSat, vCiIds->pArray, vCiIds->nSize ); @@ -411,7 +134,6 @@ Vec_Int_t * Abc_NtkGetCiSatVarNums( Abc_Ntk_t * pNtk ) } - /**Function************************************************************* @@ -669,7 +391,7 @@ void Abc_NtkCollectSupergate( Abc_Obj_t * pNode, int fStopAtMux, Vec_Ptr_t * vNo SeeAlso [] ***********************************************************************/ -int Abc_NtkMiterSatCreate2Int( solver * pSat, Abc_Ntk_t * pNtk ) +int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk ) { Abc_Obj_t * pNode, * pFanin, * pNodeC, * pNodeT, * pNodeE; Vec_Ptr_t * vNodes, * vSuper; @@ -787,7 +509,7 @@ int Abc_NtkMiterSatCreate2Int( solver * pSat, Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk ) +solver * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk ) { solver * pSat; Abc_Obj_t * pNode; @@ -796,7 +518,7 @@ solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk ) nMuxes = 0; pSat = solver_new(); - RetValue = Abc_NtkMiterSatCreate2Int( pSat, pNtk ); + RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk ); Abc_NtkForEachObj( pNtk, pNode, i ) pNode->fMarkA = 0; // Asat_SolverWriteDimacs( pSat, "temp_sat.cnf", NULL, NULL, 1 ); @@ -805,8 +527,8 @@ solver * Abc_NtkMiterSatCreate2( Abc_Ntk_t * pNtk ) solver_delete(pSat); return NULL; } - printf( "The number of MUXes detected = %d (%5.2f %% of logic). ", nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) ); - PRT( "Creating solver", clock() - clk ); +// printf( "Ands = %6d. Muxes = %6d (%5.2f %%). ", Abc_NtkNodeNum(pNtk), nMuxes, 300.0*nMuxes/Abc_NtkNodeNum(pNtk) ); +// PRT( "Creating solver", clock() - clk ); return pSat; } diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c index 00370002..34757145 100644 --- a/src/base/abci/abcUnreach.c +++ b/src/base/abci/abcUnreach.c @@ -285,7 +285,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn // start the new network pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD ); - pNtkNew->pName = util_strsav( "exdc" ); + pNtkNew->pName = Extra_UtilStrsav( "exdc" ); pNtkNew->pSpec = NULL; // create PIs corresponding to LOs diff --git a/src/base/abci/abcVanEijk.c b/src/base/abci/abcVanEijk.c index f8d659a0..d719df4f 100644 --- a/src/base/abci/abcVanEijk.c +++ b/src/base/abci/abcVanEijk.c @@ -517,13 +517,13 @@ Abc_Ntk_t * Abc_NtkVanEijkFrames( Abc_Ntk_t * pNtk, Vec_Ptr_t * vCorresp, int nF pNtkFrames = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG ); if ( fShortNames ) { - pNtkFrames->pName = util_strsav(pNtk->pName); - pNtkFrames->pSpec = util_strsav(pNtk->pSpec); + pNtkFrames->pName = Extra_UtilStrsav(pNtk->pName); + pNtkFrames->pSpec = Extra_UtilStrsav(pNtk->pSpec); } else { sprintf( Buffer, "%s_%d_frames", pNtk->pName, nFrames + fAddLast ); - pNtkFrames->pName = util_strsav(Buffer); + pNtkFrames->pName = Extra_UtilStrsav(Buffer); } // map the constant nodes Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkFrames); @@ -722,7 +722,7 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses ) // start the network pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc ); - pNtkNew->pName = util_strsav("exdc"); + pNtkNew->pName = Extra_UtilStrsav("exdc"); pNtkNew->pSpec = NULL; // map the constant nodes diff --git a/src/base/abci/abcVanImp.c b/src/base/abci/abcVanImp.c index 693d0af7..1805378c 100644 --- a/src/base/abci/abcVanImp.c +++ b/src/base/abci/abcVanImp.c @@ -878,7 +878,7 @@ Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_I // start the network pNtkNew = Abc_NtkAlloc( pNtk->ntkType, pNtk->ntkFunc ); - pNtkNew->pName = util_strsav( "exdc" ); + pNtkNew->pName = Extra_UtilStrsav( "exdc" ); pNtkNew->pSpec = NULL; // map the constant nodes diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 99392e48..5c7b525e 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -46,7 +46,7 @@ static void Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, SeeAlso [] ***********************************************************************/ -void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds ) +void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nImpLimit ) { Abc_Ntk_t * pMiter; Abc_Ntk_t * pCnf; @@ -87,7 +87,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds ) } // solve the CNF using the SAT solver - RetValue = Abc_NtkMiterSat( pCnf, nSeconds, 0 ); + RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0 ); if ( RetValue == -1 ) printf( "Networks are undecided (SAT solver timed out).\n" ); else if ( RetValue == 0 ) @@ -184,7 +184,7 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV SeeAlso [] ***********************************************************************/ -void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFrames ) +void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nImpLimit, int nFrames ) { Abc_Ntk_t * pMiter; Abc_Ntk_t * pFrames; @@ -244,7 +244,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int nFra } // solve the CNF using the SAT solver - RetValue = Abc_NtkMiterSat( pCnf, nSeconds, 0 ); + RetValue = Abc_NtkMiterSat( pCnf, nConfLimit, nImpLimit, 0 ); if ( RetValue == -1 ) printf( "Networks are undecided (SAT solver timed out).\n" ); else if ( RetValue == 0 ) diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 5b15641b..3ca188b7 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -2,9 +2,11 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcAttach.c \ src/base/abci/abcAuto.c \ src/base/abci/abcBalance.c \ - src/base/abci/abcCollapse.c \ + src/base/abci/abcClpBdd.c \ + src/base/abci/abcClpSop.c \ src/base/abci/abcCut.c \ src/base/abci/abcDsd.c \ + src/base/abci/abcEspresso.c \ src/base/abci/abcFpga.c \ src/base/abci/abcFraig.c \ src/base/abci/abcFxu.c \ @@ -13,6 +15,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcNtbdd.c \ src/base/abci/abcPga.c \ src/base/abci/abcPrint.c \ + src/base/abci/abcProve.c \ src/base/abci/abcReconv.c \ src/base/abci/abcRefactor.c \ src/base/abci/abcRenode.c \ diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index b2a90806..21dba247 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -142,8 +142,8 @@ int CmdCommandTime( Abc_Frame_t * pAbc, int argc, char **argv ) { int c; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -154,7 +154,7 @@ int CmdCommandTime( Abc_Frame_t * pAbc, int argc, char **argv ) } } - if ( argc != util_optind ) + if ( argc != globalUtilOptind ) { goto usage; } @@ -188,8 +188,8 @@ int CmdCommandEcho( Abc_Frame_t * pAbc, int argc, char **argv ) int c; int n = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "hn" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "hn" ) ) != EOF ) { switch ( c ) { @@ -204,7 +204,7 @@ int CmdCommandEcho( Abc_Frame_t * pAbc, int argc, char **argv ) } } - for ( i = util_optind; i < argc; i++ ) + for ( i = globalUtilOptind; i < argc; i++ ) fprintf( pAbc->Out, "%s ", argv[i] ); if ( n ) fprintf( pAbc->Out, "\n" ); @@ -234,8 +234,8 @@ int CmdCommandQuit( Abc_Frame_t * pAbc, int argc, char **argv ) { int c; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "hs" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "hs" ) ) != EOF ) { switch ( c ) { @@ -250,7 +250,7 @@ int CmdCommandQuit( Abc_Frame_t * pAbc, int argc, char **argv ) } } - if ( argc != util_optind ) + if ( argc != globalUtilOptind ) goto usage; return -1; @@ -294,8 +294,8 @@ int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv ) int i, c, num, size; num = 20; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -309,8 +309,8 @@ int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv ) goto usage; // get the number of commands to print - if ( argc == util_optind + 1 ) - num = atoi(argv[util_optind]); + if ( argc == globalUtilOptind + 1 ) + num = atoi(argv[globalUtilOptind]); // print the commands size = pAbc->aHistory->nSize; num = ( num < size ) ? num : size; @@ -342,8 +342,8 @@ int CmdCommandAlias( Abc_Frame_t * pAbc, int argc, char **argv ) char *key, *value; int c; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -399,8 +399,8 @@ int CmdCommandUnalias( Abc_Frame_t * pAbc, int argc, char **argv ) char *key, *value; int c; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -450,8 +450,8 @@ int CmdCommandHelp( Abc_Frame_t * pAbc, int argc, char **argv ) int c; fPrintAll = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "ah" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ah" ) ) != EOF ) { switch ( c ) { @@ -468,7 +468,7 @@ int CmdCommandHelp( Abc_Frame_t * pAbc, int argc, char **argv ) } } - if ( argc != util_optind ) + if ( argc != globalUtilOptind ) goto usage; CmdCommandPrint( pAbc, fPrintAll ); @@ -503,8 +503,8 @@ int CmdCommandSource( Abc_Frame_t * pAbc, int argc, char **argv ) interactive = silent = prompt = echo = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "hipsx" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "hipsx" ) ) != EOF ) { switch ( c ) { @@ -529,12 +529,12 @@ int CmdCommandSource( Abc_Frame_t * pAbc, int argc, char **argv ) } /* added to avoid core-dumping when no script file is specified */ - if ( argc == util_optind ) + if ( argc == globalUtilOptind ) { goto usage; } - lp_file_index = util_optind; + lp_file_index = globalUtilOptind; lp_count = 0; /* @@ -568,7 +568,7 @@ int CmdCommandSource( Abc_Frame_t * pAbc, int argc, char **argv ) } else { - prompt_string = NIL( char ); + prompt_string = NULL; } /* clear errors -- e.g., EOF reached from stdin */ @@ -602,7 +602,7 @@ int CmdCommandSource( Abc_Frame_t * pAbc, int argc, char **argv ) fprintf( pAbc->Out, "abc - > %s", line ); } command = CmdHistorySubstitution( pAbc, line, &did_subst ); - if ( command == NIL( char ) ) + if ( command == NULL ) { status = 1; break; @@ -620,8 +620,8 @@ int CmdCommandSource( Abc_Frame_t * pAbc, int argc, char **argv ) } if ( interactive && *line != '\0' ) { - Cmd_HistoryAddCommand( pAbc, util_strsav(line) ); - if ( pAbc->Hst != NIL( FILE ) ) + Cmd_HistoryAddCommand( pAbc, Extra_UtilStrsav(line) ); + if ( pAbc->Hst != NULL ) { fprintf( pAbc->Hst, "%s\n", line ); ( void ) fflush( pAbc->Hst ); @@ -674,8 +674,8 @@ int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv ) char *flag_value, *key, *value; int c; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -703,9 +703,9 @@ int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv ) FREE( value ); } - flag_value = argc == 2 ? util_strsav( "" ) : util_strsav( argv[2] ); -// flag_value = argc == 2 ? NULL : util_strsav(argv[2]); - st_insert( pAbc->tFlags, util_strsav(argv[1]), flag_value ); + flag_value = argc == 2 ? Extra_UtilStrsav( "" ) : Extra_UtilStrsav( argv[2] ); +// flag_value = argc == 2 ? NULL : Extra_UtilStrsav(argv[2]); + st_insert( pAbc->tFlags, Extra_UtilStrsav(argv[1]), flag_value ); if ( strcmp( argv[1], "abcout" ) == 0 ) { @@ -713,7 +713,7 @@ int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv ) fclose( pAbc->Out ); if ( strcmp( flag_value, "" ) == 0 ) flag_value = "-"; - pAbc->Out = CmdFileOpen( pAbc, flag_value, "w", NIL( char * ), 0 ); + pAbc->Out = CmdFileOpen( pAbc, flag_value, "w", NULL, 0 ); if ( pAbc->Out == NULL ) pAbc->Out = stdout; #if HAVE_SETVBUF @@ -726,7 +726,7 @@ int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv ) fclose( pAbc->Err ); if ( strcmp( flag_value, "" ) == 0 ) flag_value = "-"; - pAbc->Err = CmdFileOpen( pAbc, flag_value, "w", NIL( char * ), 0 ); + pAbc->Err = CmdFileOpen( pAbc, flag_value, "w", NULL, 0 ); if ( pAbc->Err == NULL ) pAbc->Err = stderr; #if HAVE_SETVBUF @@ -735,15 +735,15 @@ int CmdCommandSetVariable( Abc_Frame_t * pAbc, int argc, char **argv ) } if ( strcmp( argv[1], "history" ) == 0 ) { - if ( pAbc->Hst != NIL( FILE ) ) + if ( pAbc->Hst != NULL ) fclose( pAbc->Hst ); if ( strcmp( flag_value, "" ) == 0 ) - pAbc->Hst = NIL( FILE ); + pAbc->Hst = NULL; else { - pAbc->Hst = CmdFileOpen( pAbc, flag_value, "w", NIL( char * ), 0 ); + pAbc->Hst = CmdFileOpen( pAbc, flag_value, "w", NULL, 0 ); if ( pAbc->Hst == NULL ) - pAbc->Hst = NIL( FILE ); + pAbc->Hst = NULL; } } return 0; @@ -774,8 +774,8 @@ int CmdCommandUnsetVariable( Abc_Frame_t * pAbc, int argc, char **argv ) char *key, *value; int c; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -867,8 +867,8 @@ int CmdCommandRecall( Abc_Frame_t * pAbc, int argc, char **argv ) } - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -979,8 +979,8 @@ int CmdCommandEmpty( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; } - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -1021,7 +1021,7 @@ int CmdCommandUndo( Abc_Frame_t * pAbc, int argc, char **argv ) Abc_Ntk_t * pNtkTemp; int id, c; - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -1032,12 +1032,12 @@ int CmdCommandUndo( Abc_Frame_t * pAbc, int argc, char **argv ) goto usage; } } - if (util_optind <= argc) { + if (globalUtilOptind <= argc) { pNtkTemp = pAbc->pNtk; pAbc->pNtk = pAbc->pNtkSaved; pAbc->pNtkSaved = pNtkTemp; } - id = atoi(argv[util_optind]); + id = atoi(argv[globalUtilOptind]); pNtkTemp = Cmd_HistoryGetSnapshot(pAbc, id); if (!pNtkTemp) fprintf( pAbc->Err, "Snapshot %d does not exist\n", id); @@ -1095,8 +1095,8 @@ int CmdCommandLs( Abc_Frame_t * pAbc, int argc, char **argv ) int fPrintedNewLine; char c; - util_getopt_reset(); - while ( (c = util_getopt(argc, argv, "lb") ) != EOF ) + Extra_UtilGetoptReset(); + while ( (c = Extra_UtilGetopt(argc, argv, "lb") ) != EOF ) { switch (c) { @@ -1294,7 +1294,7 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv ) if ( pNtk->pSpec ) { FREE( pNtkNew->pSpec ); - pNtkNew->pSpec = util_strsav( pNtk->pSpec ); + pNtkNew->pSpec = Extra_UtilStrsav( pNtk->pSpec ); } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew ); @@ -1430,7 +1430,7 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv ) if ( pNtk->pSpec ) { FREE( pNtkNew->pSpec ); - pNtkNew->pSpec = util_strsav( pNtk->pSpec ); + pNtkNew->pSpec = Extra_UtilStrsav( pNtk->pSpec ); } // replace the current network Abc_FrameReplaceCurrentNetwork( pAbc, pNtkNew ); diff --git a/src/base/cmd/cmdAlias.c b/src/base/cmd/cmdAlias.c index beb7a566..0ec3feea 100644 --- a/src/base/cmd/cmdAlias.c +++ b/src/base/cmd/cmdAlias.c @@ -45,11 +45,11 @@ void CmdCommandAliasAdd( Abc_Frame_t * pAbc, char * sName, int argc, char ** arg int fStatus, i; pAlias = ALLOC(Abc_Alias, 1); - pAlias->sName = util_strsav(sName); + pAlias->sName = Extra_UtilStrsav(sName); pAlias->argc = argc; pAlias->argv = ALLOC(char *, pAlias->argc); for(i = 0; i < argc; i++) - pAlias->argv[i] = util_strsav(argv[i]); + pAlias->argv[i] = Extra_UtilStrsav(argv[i]); fStatus = st_insert( pAbc->tAliases, pAlias->sName, (char *) pAlias ); assert(!fStatus); } diff --git a/src/base/cmd/cmdApi.c b/src/base/cmd/cmdApi.c index cc3d5806..7167e22b 100644 --- a/src/base/cmd/cmdApi.c +++ b/src/base/cmd/cmdApi.c @@ -57,8 +57,8 @@ void Cmd_CommandAdd( Abc_Frame_t * pAbc, char * sGroup, char * sName, void * pFu // create the new command pCommand = ALLOC( Abc_Command, 1 ); - pCommand->sName = util_strsav( sName ); - pCommand->sGroup = util_strsav( sGroup ); + pCommand->sName = Extra_UtilStrsav( sName ); + pCommand->sGroup = Extra_UtilStrsav( sGroup ); pCommand->pFunc = pFunc; pCommand->fChange = fChanges; fStatus = st_insert( pAbc->tCommands, sName, (char *)pCommand ); diff --git a/src/base/cmd/cmdFlag.c b/src/base/cmd/cmdFlag.c index 267f8e06..993f2a49 100644 --- a/src/base/cmd/cmdFlag.c +++ b/src/base/cmd/cmdFlag.c @@ -35,8 +35,7 @@ Description [The command parser maintains a table of named values. These are manipulated using the 'set' and 'unset' commands. The value of the - named flag is returned, or NIL(char) is returned if the flag has not been - set.] + named flag is returned, or NULL is returned if the flag has not been set.] SideEffects [] @@ -65,9 +64,9 @@ void Cmd_FlagUpdateValue( Abc_Frame_t * pAbc, char * key, char * value ) if ( !key ) return; if ( value ) - newValue = util_strsav(value); + newValue = Extra_UtilStrsav(value); else - newValue = util_strsav(""); + newValue = Extra_UtilStrsav(""); // newValue = NULL; if ( st_delete(pAbc->tFlags, &key, &oldValue) ) FREE(oldValue); diff --git a/src/base/cmd/cmdHist.c b/src/base/cmd/cmdHist.c index dae293d7..12750d16 100644 --- a/src/base/cmd/cmdHist.c +++ b/src/base/cmd/cmdHist.c @@ -47,7 +47,7 @@ void Cmd_HistoryAddCommand( Abc_Frame_t * p, char * command ) strcpy( Buffer, command ); if ( command[strlen(command)-1] != '\n' ) strcat( Buffer, "\n" ); - Vec_PtrPush( p->aHistory, util_strsav(Buffer) ); + Vec_PtrPush( p->aHistory, Extra_UtilStrsav(Buffer) ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/base/cmd/cmdUtils.c b/src/base/cmd/cmdUtils.c index 9b7fb49f..47e54bb3 100644 --- a/src/base/cmd/cmdUtils.c +++ b/src/base/cmd/cmdUtils.c @@ -121,10 +121,10 @@ int CmdCommandDispatch( Abc_Frame_t * pAbc, int argc, char **argv ) } // execute the command - clk = util_cpu_time(); + clk = Extra_CpuTime(); pFunc = (int (*)(Abc_Frame_t *, int, char **))pCommand->pFunc; fError = (*pFunc)( pAbc, argc, argv ); - pAbc->TimeCommand += (util_cpu_time() - clk); + pAbc->TimeCommand += (Extra_CpuTime() - clk); // automatic execution of arbitrary command after each command // usually this is a passive command ... @@ -270,7 +270,7 @@ int CmdApplyAlias( Abc_Frame_t * pAbc, int *argcp, char ***argvp, int *loop ) } for ( i = 1; i <= added; i++ ) { - argv[i] = NIL( char ); + argv[i] = NULL; } argc += added; } @@ -278,7 +278,7 @@ int CmdApplyAlias( Abc_Frame_t * pAbc, int *argcp, char ***argvp, int *loop ) for ( i = 0, offset = 0; i < alias->argc; i++, offset++ ) { arg = CmdHistorySubstitution( pAbc, alias->argv[i], &did_subst ); - if ( arg == NIL( char ) ) + if ( arg == NULL ) { *argcp = argc; *argvp = argv; @@ -383,11 +383,11 @@ FILE * CmdFileOpen( Abc_Frame_t * pAbc, char *sFileName, char *sMode, char **pFi if (strcmp(sFileName, "-") == 0) { if (strcmp(sMode, "w") == 0) { - sRealName = util_strsav( "stdout" ); + sRealName = Extra_UtilStrsav( "stdout" ); pFile = stdout; } else { - sRealName = util_strsav( "stdin" ); + sRealName = Extra_UtilStrsav( "stdin" ); pFile = stdin; } } @@ -403,24 +403,24 @@ FILE * CmdFileOpen( Abc_Frame_t * pAbc, char *sFileName, char *sMode, char **pFi sPathAll = NULL; } else if ( sPathUsr == NULL ) { - sPathAll = util_strsav( sPathLib ); + sPathAll = Extra_UtilStrsav( sPathLib ); } else if ( sPathLib == NULL ) { - sPathAll = util_strsav( sPathUsr ); + sPathAll = Extra_UtilStrsav( sPathUsr ); } else { sPathAll = ALLOC( char, strlen(sPathLib)+strlen(sPathUsr)+5 ); sprintf( sPathAll, "%s:%s",sPathUsr, sPathLib ); } - if ( sPathAll != NIL(char) ) { - sRealName = util_file_search(sFileName, sPathAll, "r"); + if ( sPathAll != NULL ) { + sRealName = Extra_UtilFileSearch(sFileName, sPathAll, "r"); FREE( sPathAll ); } } - if (sRealName == NIL(char)) { - sRealName = util_tilde_expand(sFileName); + if (sRealName == NULL) { + sRealName = Extra_UtilTildeExpand(sFileName); } - if ((pFile = fopen(sRealName, sMode)) == NIL(FILE)) { + if ((pFile = fopen(sRealName, sMode)) == NULL) { if (! silent) { perror(sRealName); } diff --git a/src/base/io/io.c b/src/base/io/io.c index 69b60000..2725eb8a 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -120,8 +120,8 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; fCheck = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF ) { switch ( c ) { @@ -135,13 +135,13 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv ) } } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { goto usage; } // get the input file name - FileName = argv[util_optind]; + FileName = argv[globalUtilOptind]; if ( (pFile = fopen( FileName, "r" )) == NULL ) { fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName ); @@ -192,8 +192,8 @@ int IoCommandReadBaf( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; fCheck = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF ) { switch ( c ) { @@ -207,13 +207,13 @@ int IoCommandReadBaf( Abc_Frame_t * pAbc, int argc, char ** argv ) } } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { goto usage; } // get the input file name - FileName = argv[util_optind]; + FileName = argv[globalUtilOptind]; if ( (pFile = fopen( FileName, "r" )) == NULL ) { fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName ); @@ -265,8 +265,8 @@ int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; fCheck = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF ) { switch ( c ) { @@ -280,13 +280,13 @@ int IoCommandReadBlif( Abc_Frame_t * pAbc, int argc, char ** argv ) } } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { goto usage; } // get the input file name - FileName = argv[util_optind]; + FileName = argv[globalUtilOptind]; if ( (pFile = fopen( FileName, "r" )) == NULL ) { fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName ); @@ -346,8 +346,8 @@ int IoCommandReadBench( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; fCheck = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF ) { switch ( c ) { @@ -361,13 +361,13 @@ int IoCommandReadBench( Abc_Frame_t * pAbc, int argc, char ** argv ) } } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { goto usage; } // get the input file name - FileName = argv[util_optind]; + FileName = argv[globalUtilOptind]; if ( (pFile = fopen( FileName, "r" )) == NULL ) { fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName ); @@ -426,8 +426,8 @@ int IoCommandReadEdif( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; fCheck = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF ) { switch ( c ) { @@ -441,13 +441,13 @@ int IoCommandReadEdif( Abc_Frame_t * pAbc, int argc, char ** argv ) } } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { goto usage; } // get the input file name - FileName = argv[util_optind]; + FileName = argv[globalUtilOptind]; if ( (pFile = fopen( FileName, "r" )) == NULL ) { fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName ); @@ -506,8 +506,8 @@ int IoCommandReadEqn( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; fCheck = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF ) { switch ( c ) { @@ -521,13 +521,13 @@ int IoCommandReadEqn( Abc_Frame_t * pAbc, int argc, char ** argv ) } } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { goto usage; } // get the input file name - FileName = argv[util_optind]; + FileName = argv[globalUtilOptind]; if ( (pFile = fopen( FileName, "r" )) == NULL ) { fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName ); @@ -586,8 +586,8 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; fCheck = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF ) { switch ( c ) { @@ -601,13 +601,13 @@ int IoCommandReadVerilog( Abc_Frame_t * pAbc, int argc, char ** argv ) } } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { goto usage; } // get the input file name - FileName = argv[util_optind]; + FileName = argv[globalUtilOptind]; if ( (pFile = fopen( FileName, "r" )) == NULL ) { fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName ); @@ -666,8 +666,8 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; fCheck = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "ch" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "ch" ) ) != EOF ) { switch ( c ) { @@ -681,13 +681,13 @@ int IoCommandReadPla( Abc_Frame_t * pAbc, int argc, char ** argv ) } } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { goto usage; } // get the input file name - FileName = argv[util_optind]; + FileName = argv[globalUtilOptind]; if ( (pFile = fopen( FileName, "r" )) == NULL ) { fprintf( pAbc->Err, "Cannot open input file \"%s\". ", FileName ); @@ -745,8 +745,8 @@ int IoCommandReadTruth( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; fHex = 0; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "xh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "xh" ) ) != EOF ) { switch ( c ) { @@ -760,16 +760,16 @@ int IoCommandReadTruth( Abc_Frame_t * pAbc, int argc, char ** argv ) } } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { goto usage; } // convert truth table to SOP if ( fHex ) - pSopCover = Abc_SopFromTruthHex(argv[util_optind]); + pSopCover = Abc_SopFromTruthHex(argv[globalUtilOptind]); else - pSopCover = Abc_SopFromTruthBin(argv[util_optind]); + pSopCover = Abc_SopFromTruthBin(argv[globalUtilOptind]); if ( pSopCover == NULL ) { fprintf( pAbc->Err, "Reading truth table has failed.\n" ); @@ -814,8 +814,8 @@ int IoCommandWriteBaf( Abc_Frame_t * pAbc, int argc, char **argv ) char * FileName; int c; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "lh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF ) { switch ( c ) { @@ -833,11 +833,11 @@ int IoCommandWriteBaf( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { goto usage; } - FileName = argv[util_optind]; + FileName = argv[globalUtilOptind]; // check the network type if ( !Abc_NtkIsStrash(pNtk) ) @@ -875,8 +875,8 @@ int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv ) int c; fWriteLatches = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "lh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF ) { switch ( c ) { @@ -897,11 +897,11 @@ int IoCommandWriteBlif( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { goto usage; } - FileName = argv[util_optind]; + FileName = argv[globalUtilOptind]; // check the network type if ( !Abc_NtkIsLogic(pNtk) && !Abc_NtkIsStrash(pNtk) && !Abc_NtkIsSeq(pNtk) ) @@ -941,8 +941,8 @@ int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv ) int c; fWriteLatches = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "lh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "lh" ) ) != EOF ) { switch ( c ) { @@ -963,12 +963,12 @@ int IoCommandWriteBench( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { goto usage; } // get the input file name - FileName = argv[util_optind]; + FileName = argv[globalUtilOptind]; if ( !Abc_NtkIsStrash(pNtk) ) { @@ -1012,8 +1012,8 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv ) char * FileName; int c; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -1026,17 +1026,22 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv ) if ( pAbc->pNtkCur == NULL ) { - fprintf( pAbc->Out, "Empty network.\n" ); + printf( "Empty network.\n" ); return 0; } + if ( !Abc_NtkIsStrash(pAbc->pNtkCur) ) + { + printf( "This command can only be applied to an AIG (run \"strash\").\n" ); + return 1; + } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { goto usage; } // get the input file name - FileName = argv[util_optind]; + FileName = argv[globalUtilOptind]; // write the file if ( !Io_WriteCnf( pAbc->pNtkCur, FileName ) ) { @@ -1070,8 +1075,8 @@ int IoCommandWriteDot( Abc_Frame_t * pAbc, int argc, char **argv ) Vec_Ptr_t * vNodes; int c; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -1094,13 +1099,13 @@ int IoCommandWriteDot( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { goto usage; } // get the input file name - FileName = argv[util_optind]; + FileName = argv[globalUtilOptind]; // write the file vNodes = Abc_NtkCollectObjects( pAbc->pNtkCur ); Io_WriteDotAig( pAbc->pNtkCur, vNodes, NULL, FileName, 0 ); @@ -1132,8 +1137,8 @@ int IoCommandWriteEqn( Abc_Frame_t * pAbc, int argc, char **argv ) char * FileName; int c; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -1151,7 +1156,7 @@ int IoCommandWriteEqn( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { goto usage; } @@ -1163,7 +1168,7 @@ int IoCommandWriteEqn( Abc_Frame_t * pAbc, int argc, char **argv ) } // get the input file name - FileName = argv[util_optind]; + FileName = argv[globalUtilOptind]; // write the file // get rid of complemented covers if present if ( Abc_NtkIsSopLogic(pNtk) ) @@ -1203,8 +1208,8 @@ int IoCommandWriteGml( Abc_Frame_t * pAbc, int argc, char **argv ) char * FileName; int c; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -1227,13 +1232,13 @@ int IoCommandWriteGml( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { goto usage; } // get the input file name - FileName = argv[util_optind]; + FileName = argv[globalUtilOptind]; // write the file Io_WriteGml( pAbc->pNtkCur, FileName ); return 0; @@ -1264,8 +1269,8 @@ int IoCommandWriteList( Abc_Frame_t * pAbc, int argc, char **argv ) int c; fUseHost = 1; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "nh" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "nh" ) ) != EOF ) { switch ( c ) { @@ -1291,13 +1296,13 @@ int IoCommandWriteList( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { goto usage; } // get the input file name - FileName = argv[util_optind]; + FileName = argv[globalUtilOptind]; // write the file Io_WriteList( pAbc->pNtkCur, FileName, fUseHost ); return 0; @@ -1328,8 +1333,8 @@ int IoCommandWritePla( Abc_Frame_t * pAbc, int argc, char **argv ) char * FileName; int c; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -1359,12 +1364,12 @@ int IoCommandWritePla( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { goto usage; } // get the input file name - FileName = argv[util_optind]; + FileName = argv[globalUtilOptind]; // derive the netlist pNtkTemp = Abc_NtkLogicToNetlist(pNtk); @@ -1402,8 +1407,8 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv ) char * FileName; int c; - util_getopt_reset(); - while ( ( c = util_getopt( argc, argv, "h" ) ) != EOF ) + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) { switch ( c ) { @@ -1421,12 +1426,12 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv ) return 0; } - if ( argc != util_optind + 1 ) + if ( argc != globalUtilOptind + 1 ) { goto usage; } // get the input file name - FileName = argv[util_optind]; + FileName = argv[globalUtilOptind]; // derive the netlist pNtkTemp = Abc_NtkLogicToNetlist(pNtk); diff --git a/src/base/io/ioReadBaf.c b/src/base/io/ioReadBaf.c index 2d6c3ca6..e2aa2109 100644 --- a/src/base/io/ioReadBaf.c +++ b/src/base/io/ioReadBaf.c @@ -74,8 +74,8 @@ Abc_Ntk_t * Io_ReadBaf( char * pFileName, int fCheck ) // allocate the empty AIG pNtkNew = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG ); - pNtkNew->pName = util_strsav( pName ); - pNtkNew->pSpec = util_strsav( pFileName ); + pNtkNew->pName = Extra_UtilStrsav( pName ); + pNtkNew->pSpec = Extra_UtilStrsav( pFileName ); // prepare the array of nodes vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds ); diff --git a/src/base/io/ioReadBlif.c b/src/base/io/ioReadBlif.c index c05f444e..39b85a10 100644 --- a/src/base/io/ioReadBlif.c +++ b/src/base/io/ioReadBlif.c @@ -230,7 +230,7 @@ Vec_Ptr_t * Io_ReadBlifGetTokens( Io_ReadBlif_t * p ) vTokens->nSize--; // load them into the new array for ( i = 0; i < vTokens->nSize; i++ ) - Vec_PtrPush( p->vNewTokens, util_strsav(vTokens->pArray[i]) ); + Vec_PtrPush( p->vNewTokens, Extra_UtilStrsav(vTokens->pArray[i]) ); // load as long as there is the line break while ( 1 ) @@ -249,12 +249,12 @@ Vec_Ptr_t * Io_ReadBlifGetTokens( Io_ReadBlif_t * p ) vTokens->nSize--; // load them into the new array for ( i = 0; i < vTokens->nSize; i++ ) - Vec_PtrPush( p->vNewTokens, util_strsav(vTokens->pArray[i]) ); + Vec_PtrPush( p->vNewTokens, Extra_UtilStrsav(vTokens->pArray[i]) ); continue; } // otherwise, load them and break for ( i = 0; i < vTokens->nSize; i++ ) - Vec_PtrPush( p->vNewTokens, util_strsav(vTokens->pArray[i]) ); + Vec_PtrPush( p->vNewTokens, Extra_UtilStrsav(vTokens->pArray[i]) ); break; } return p->vNewTokens; @@ -294,8 +294,8 @@ Abc_Ntk_t * Io_ReadBlifNetwork( Io_ReadBlif_t * p ) pModelName = vTokens->pArray[1]; // allocate the empty network p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP ); - p->pNtk->pName = util_strsav( pModelName ); - p->pNtk->pSpec = util_strsav( p->pFileName ); + p->pNtk->pName = Extra_UtilStrsav( pModelName ); + p->pNtk->pSpec = Extra_UtilStrsav( p->pFileName ); } else p->pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP ); @@ -681,7 +681,7 @@ int Io_ReadBlifNetworkInputArrival( Io_ReadBlif_t * p, Vec_Ptr_t * vTokens ) return 1; } // set the arrival time - Abc_NtkTimeSetArrival( p->pNtk, pNet->Id, (float)TimeRise, (float)TimeFall ); + Abc_NtkTimeSetArrival( p->pNtk, Abc_ObjFanin0(pNet)->Id, (float)TimeRise, (float)TimeFall ); return 0; } diff --git a/src/base/io/ioReadEdif.c b/src/base/io/ioReadEdif.c index f100a45f..3bdf2567 100644 --- a/src/base/io/ioReadEdif.c +++ b/src/base/io/ioReadEdif.c @@ -181,7 +181,7 @@ Abc_Ntk_t * Io_ReadEdifNetwork( Extra_FileReader_t * p ) else if ( strcmp( vTokens->pArray[0], "design" ) == 0 ) { free( pNtk->pName ); - pNtk->pName = util_strsav( vTokens->pArray[3] ); + pNtk->pName = Extra_UtilStrsav( vTokens->pArray[3] ); break; } } diff --git a/src/base/io/ioReadEqn.c b/src/base/io/ioReadEqn.c index a5a46f40..4fb313f4 100644 --- a/src/base/io/ioReadEqn.c +++ b/src/base/io/ioReadEqn.c @@ -145,7 +145,7 @@ Abc_Ntk_t * Io_ReadEqnNetwork( Extra_FileReader_t * p ) continue; } // determine unique variables - pCubesCopy = util_strsav( pCubesCopy ); + pCubesCopy = Extra_UtilStrsav( pCubesCopy ); // find the names of the fanins of this node Io_ReadEqnStrCutAt( pCubesCopy, "!*+", 1, vVars ); // create the node diff --git a/src/base/io/ioReadVerilog.c b/src/base/io/ioReadVerilog.c index 58071e39..a4610cac 100644 --- a/src/base/io/ioReadVerilog.c +++ b/src/base/io/ioReadVerilog.c @@ -272,8 +272,8 @@ Abc_Ntk_t * Io_ReadVerNetwork( Io_ReadVer_t * p ) // allocate the empty network pNtk = Abc_NtkAlloc( ABC_NTK_NETLIST, ABC_FUNC_SOP ); - pNtk->pName = util_strsav( pModelName ); - pNtk->pSpec = util_strsav( p->pFileName ); + pNtk->pName = Extra_UtilStrsav( pModelName ); + pNtk->pSpec = Extra_UtilStrsav( p->pFileName ); // create constant nodes and nets Abc_NtkFindOrCreateNet( pNtk, "1'b0" ); @@ -334,7 +334,7 @@ Abc_Ntk_t * Io_ReadVerNetwork( Io_ReadVer_t * p ) } // add the tri-state element to the skipped ones sprintf( Buffer, "%s %s", vTokens->pArray[0], vTokens->pArray[1] ); - Vec_PtrPush( p->vSkipped, util_strsav(Buffer) ); + Vec_PtrPush( p->vSkipped, Extra_UtilStrsav(Buffer) ); } Extra_ProgressBarStop( pProgress ); diff --git a/src/base/io/ioUtil.c b/src/base/io/ioUtil.c index e817bee8..fc37bc3f 100644 --- a/src/base/io/ioUtil.c +++ b/src/base/io/ioUtil.c @@ -223,7 +223,7 @@ FILE * Io_FileOpen( const char * FileName, const char * PathVar, const char * Mo { char ActualFileName[4096]; FILE * fp = 0; - t = util_strsav( c ); + t = Extra_UtilStrsav( c ); for (i = strtok( t, ":" ); i != 0; i = strtok( 0, ":") ) { #ifdef WIN32 diff --git a/src/base/io/ioWriteCnf.c b/src/base/io/ioWriteCnf.c index f2131257..9e5ceb9f 100644 --- a/src/base/io/ioWriteCnf.c +++ b/src/base/io/ioWriteCnf.c @@ -42,19 +42,19 @@ int Io_WriteCnf( Abc_Ntk_t * pNtk, char * pFileName ) { solver * pSat; - if ( !Abc_NtkIsBddLogic(pNtk) ) + if ( !Abc_NtkIsStrash(pNtk) ) { - fprintf( stdout, "Io_WriteCnf(): Currently can only process logic networks with BDDs.\n" ); + fprintf( stdout, "Io_WriteCnf(): Currently can only process AIGs.\n" ); return 0; } if ( Abc_NtkPoNum(pNtk) != 1 ) { - fprintf( stdout, "Io_WriteCnf(): Currently can only solve the miter (the network with one PO).\n" ); + fprintf( stdout, "Io_WriteCnf(): Currently can only process the miter (the network with one PO).\n" ); return 0; } if ( Abc_NtkLatchNum(pNtk) != 0 ) { - fprintf( stdout, "Io_WriteCnf(): Currently can only solve the miter for combinational circuits.\n" ); + fprintf( stdout, "Io_WriteCnf(): Currently can only process the miter for combinational circuits.\n" ); return 0; } // create solver with clauses diff --git a/src/base/main/main.c b/src/base/main/main.c index a9f27bf8..1c6cbcb0 100644 --- a/src/base/main/main.c +++ b/src/base/main/main.c @@ -75,21 +75,21 @@ int main( int argc, char * argv[] ) sprintf( sReadCmd, "read" ); sprintf( sWriteCmd, "write" ); - util_getopt_reset(); - while ((c = util_getopt(argc, argv, "c:hf:F:o:st:T:x")) != EOF) { + Extra_UtilGetoptReset(); + while ((c = Extra_UtilGetopt(argc, argv, "c:hf:F:o:st:T:x")) != EOF) { switch(c) { case 'c': - strcpy( sCommandUsr, util_optarg ); + strcpy( sCommandUsr, globalUtilOptarg ); fBatch = 1; break; case 'f': - sprintf(sCommandUsr, "source %s", util_optarg); + sprintf(sCommandUsr, "source %s", globalUtilOptarg); fBatch = 1; break; case 'F': - sprintf(sCommandUsr, "source -x %s", util_optarg); + sprintf(sCommandUsr, "source -x %s", globalUtilOptarg); fBatch = 1; break; @@ -98,7 +98,7 @@ int main( int argc, char * argv[] ) break; case 'o': - sOutFile = util_optarg; + sOutFile = globalUtilOptarg; fFinalWrite = 1; break; @@ -107,12 +107,12 @@ int main( int argc, char * argv[] ) break; case 't': - if ( TypeCheck( pAbc, util_optarg ) ) + if ( TypeCheck( pAbc, globalUtilOptarg ) ) { - if ( !strcmp(util_optarg, "none") == 0 ) + if ( !strcmp(globalUtilOptarg, "none") == 0 ) { fInitRead = 1; - sprintf( sReadCmd, "read_%s", util_optarg ); + sprintf( sReadCmd, "read_%s", globalUtilOptarg ); } } else { @@ -122,12 +122,12 @@ int main( int argc, char * argv[] ) break; case 'T': - if ( TypeCheck( pAbc, util_optarg ) ) + if ( TypeCheck( pAbc, globalUtilOptarg ) ) { - if (!strcmp(util_optarg, "none") == 0) + if (!strcmp(globalUtilOptarg, "none") == 0) { fFinalWrite = 1; - sprintf( sWriteCmd, "write_%s", util_optarg); + sprintf( sWriteCmd, "write_%s", globalUtilOptarg); } } else { @@ -151,14 +151,14 @@ int main( int argc, char * argv[] ) { pAbc->fBatchMode = 1; - if (argc - util_optind == 0) + if (argc - globalUtilOptind == 0) { sInFile = NULL; } - else if (argc - util_optind == 1) + else if (argc - globalUtilOptind == 1) { fInitRead = 1; - sInFile = argv[util_optind]; + sInFile = argv[globalUtilOptind]; } else { @@ -221,10 +221,7 @@ int main( int argc, char * argv[] ) // if the memory should be freed, quit packages if ( fStatus < 0 ) { - // perform uninitializations - Abc_FrameEnd( pAbc ); - // stop the framework - Abc_FrameDeallocate( pAbc ); + Abc_Stop(); } return 0; @@ -250,16 +247,12 @@ usage: void Abc_Start() { Abc_Frame_t * pAbc; - // added to detect memory leaks: #ifdef _DEBUG _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF ); #endif - - // get global frame (singleton pattern) - // will be initialized on first call + // start the glocal frame pAbc = Abc_FrameGetGlobalFrame(); - // source the resource file // Abc_UtilsSource( pAbc ); } @@ -278,17 +271,11 @@ void Abc_Start() void Abc_Stop() { Abc_Frame_t * pAbc; - int fStatus = 0; - - // if the memory should be freed, quit packages - if ( fStatus == -2 ) - { - pAbc = Abc_FrameGetGlobalFrame(); - // perform uninitializations - Abc_FrameEnd( pAbc ); - // stop the framework - Abc_FrameDeallocate( pAbc ); - } + pAbc = Abc_FrameGetGlobalFrame(); + // perform uninitializations + Abc_FrameEnd( pAbc ); + // stop the framework + Abc_FrameDeallocate( pAbc ); } /**Function******************************************************************** diff --git a/src/base/main/main.h b/src/base/main/main.h index c5f311aa..d5a463f5 100644 --- a/src/base/main/main.h +++ b/src/base/main/main.h @@ -40,17 +40,10 @@ typedef struct Abc_Frame_t_ Abc_Frame_t; // it is used to catch memory leaks on Windows #include "leaks.h" -// standard includes -#include <stdio.h> -#include <string.h> - -// includes from GLU -#include "util.h" -#include "st.h" - // data structure packages #include "extra.h" #include "vec.h" +#include "st.h" // core packages #include "abc.h" diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c index e9e243af..b3208740 100644 --- a/src/base/main/mainFrame.c +++ b/src/base/main/mainFrame.c @@ -48,8 +48,8 @@ int Abc_FrameReadNtkStoreSize() { return s_GlobalFrame->nSt void * Abc_FrameReadLibLut() { return s_GlobalFrame->pLibLut; } void * Abc_FrameReadLibGen() { return s_GlobalFrame->pLibGen; } void * Abc_FrameReadLibSuper() { return s_GlobalFrame->pLibSuper; } -void * Abc_FrameReadManDd() { return s_GlobalFrame->dd; } -void * Abc_FrameReadManDec() { return s_GlobalFrame->pManDec; } +void * Abc_FrameReadManDd() { if ( s_GlobalFrame->dd == NULL ) s_GlobalFrame->dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); return s_GlobalFrame->dd; } +void * Abc_FrameReadManDec() { if ( s_GlobalFrame->pManDec == NULL ) s_GlobalFrame->pManDec = Dec_ManStart(); return s_GlobalFrame->pManDec; } char * Abc_FrameReadFlag( char * pFlag ) { return Cmd_FlagReadByName( s_GlobalFrame, pFlag ); } void Abc_FrameSetNtkStore( Abc_Ntk_t * pNtk ) { s_GlobalFrame->pStored = pNtk; } @@ -97,7 +97,8 @@ bool Abc_FrameIsFlagEnabled( char * pFlag ) Abc_Frame_t * Abc_FrameAllocate() { Abc_Frame_t * p; - + extern void define_cube_size( int n ); + extern void set_espresso_flags(); // allocate and clean p = ALLOC( Abc_Frame_t, 1 ); memset( p, 0, sizeof(Abc_Frame_t) ); @@ -111,8 +112,8 @@ Abc_Frame_t * Abc_FrameAllocate() p->nSteps = 1; p->fBatchMode = 0; // initialize decomposition manager - p->pManDec = Dec_ManStart(); - p->dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); + define_cube_size(20); + set_espresso_flags(); return p; } @@ -130,11 +131,13 @@ Abc_Frame_t * Abc_FrameAllocate() ***********************************************************************/ void Abc_FrameDeallocate( Abc_Frame_t * p ) { - Dec_ManStop( p->pManDec ); - Extra_StopManager( p->dd ); + extern void undefine_cube_size(); + undefine_cube_size(); + if ( p->pManDec ) Dec_ManStop( p->pManDec ); + if ( p->dd ) Extra_StopManager( p->dd ); Abc_FrameDeleteAllNetworks( p ); free( p ); - p = NULL; + s_GlobalFrame = NULL; } /**Function************************************************************* diff --git a/src/base/main/mainUtils.c b/src/base/main/mainUtils.c index aa8b63d0..3d0bdc33 100644 --- a/src/base/main/mainUtils.c +++ b/src/base/main/mainUtils.c @@ -139,8 +139,8 @@ void Abc_UtilsSource( Abc_Frame_t * pAbc ) // If .rc is present in both the home and current directories, then read // it from the home directory. Otherwise, read it from wherever it's located. - sPath1 = util_file_search(".rc", "~/", "r"); - sPath2 = util_file_search(".rc", ".", "r"); + sPath1 = Extra_UtilFileSearch(".rc", "~/", "r"); + sPath2 = Extra_UtilFileSearch(".rc", ".", "r"); if ( sPath1 && sPath2 ) { /* ~/.rc == .rc : Source the file only once */ diff --git a/src/base/seq/seqAigCore.c b/src/base/seq/seqAigCore.c index ed2a33fc..e74f3fa7 100644 --- a/src/base/seq/seqAigCore.c +++ b/src/base/seq/seqAigCore.c @@ -343,7 +343,7 @@ int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int } // get the miter cone - pNtkMiter = Abc_NtkCreateCone( pNtkProb, pNtkProb->vCos, vValues ); + pNtkMiter = Abc_NtkCreateTarget( pNtkProb, pNtkProb->vCos, vValues ); Abc_NtkDelete( pNtkProb ); Vec_IntFree( vValues ); @@ -358,7 +358,7 @@ int Seq_NtkImplementRetimingBackward( Abc_Ntk_t * pNtk, Vec_Ptr_t * vMoves, int // solve the miter clk = clock(); // RetValue = Abc_NtkMiterSat_OldAndRusty( pNtkCnf, 30, 0 ); - RetValue = Abc_NtkMiterSat( pNtkCnf, 30, 0 ); + RetValue = Abc_NtkMiterSat( pNtkCnf, 500000, 50000000, 0 ); if ( fVerbose ) if ( clock() - clk > 100 ) { diff --git a/src/base/seq/seqCreate.c b/src/base/seq/seqCreate.c index d94e8e82..b0c2e084 100644 --- a/src/base/seq/seqCreate.c +++ b/src/base/seq/seqCreate.c @@ -88,8 +88,8 @@ Abc_Ntk_t * Abc_NtkAigToSeq( Abc_Ntk_t * pNtk ) // start the network pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG ); // duplicate the name and the spec - pNtkNew->pName = util_strsav(pNtk->pName); - pNtkNew->pSpec = util_strsav(pNtk->pSpec); + pNtkNew->pName = Extra_UtilStrsav(pNtk->pName); + pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec); // map the constant nodes Abc_NtkCleanCopy( pNtk ); diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c index b4795039..4aba069d 100644 --- a/src/base/seq/seqRetCore.c +++ b/src/base/seq/seqRetCore.c @@ -112,8 +112,8 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose ) // start the network pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG ); // duplicate the name and the spec - pNtkNew->pName = util_strsav(pNtk->pName); - pNtkNew->pSpec = util_strsav(pNtk->pSpec); + pNtkNew->pName = Extra_UtilStrsav(pNtk->pName); + pNtkNew->pSpec = Extra_UtilStrsav(pNtk->pSpec); // map the constant nodes Abc_NtkCleanCopy( pNtk ); |