diff options
Diffstat (limited to 'src/temp/ivy')
-rw-r--r-- | src/temp/ivy/ivy.h | 30 | ||||
-rw-r--r-- | src/temp/ivy/ivyCheck.c | 6 | ||||
-rw-r--r-- | src/temp/ivy/ivyCut.c | 93 | ||||
-rw-r--r-- | src/temp/ivy/ivyDfs.c | 99 | ||||
-rw-r--r-- | src/temp/ivy/ivyFanout.c | 1 | ||||
-rw-r--r-- | src/temp/ivy/ivyIsop.c | 188 | ||||
-rw-r--r-- | src/temp/ivy/ivyMan.c | 29 | ||||
-rw-r--r-- | src/temp/ivy/ivyObj.c | 38 | ||||
-rw-r--r-- | src/temp/ivy/ivyRwrAlg.c | 4 | ||||
-rw-r--r-- | src/temp/ivy/ivyRwrPre.c | 94 | ||||
-rw-r--r-- | src/temp/ivy/ivySeq.c | 708 | ||||
-rw-r--r-- | src/temp/ivy/ivyTable.c | 4 | ||||
-rw-r--r-- | src/temp/ivy/ivyUtil.c | 73 | ||||
-rw-r--r-- | src/temp/ivy/module.make | 1 |
14 files changed, 1191 insertions, 177 deletions
diff --git a/src/temp/ivy/ivy.h b/src/temp/ivy/ivy.h index 8c5f130b..7fb054f7 100644 --- a/src/temp/ivy/ivy.h +++ b/src/temp/ivy/ivy.h @@ -80,6 +80,8 @@ struct Ivy_Obj_t_ // 24 bytes (32-bit) or 32 bytes (64-bit) int nRefs; // reference counter Ivy_Obj_t * pFanin0; // fanin Ivy_Obj_t * pFanin1; // fanin + Ivy_Obj_t * pFanout; // fanout + Ivy_Obj_t * pEquiv; // equivalent node }; // the AIG manager @@ -136,6 +138,9 @@ struct Ivy_Store_t_ Ivy_Cut_t pCuts[IVY_CUT_LIMIT]; // storage for cuts }; +#define IVY_LEAF_MASK 255 +#define IVY_LEAF_BITS 8 + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -170,9 +175,9 @@ static inline Ivy_Edge_t Ivy_EdgeNotCond( Ivy_Edge_t Edge, int fCond ) { ret static inline Ivy_Edge_t Ivy_EdgeFromNode( Ivy_Obj_t * pNode ) { return Ivy_EdgeCreate( Ivy_Regular(pNode)->Id, Ivy_IsComplement(pNode) ); } static inline Ivy_Obj_t * Ivy_EdgeToNode( Ivy_Man_t * p, Ivy_Edge_t Edge ){ return Ivy_NotCond( Ivy_ManObj(p, Ivy_EdgeId(Edge)), Ivy_EdgeIsComplement(Edge) ); } -static inline int Ivy_LeafCreate( int Id, int Lat ) { return (Id << 4) | Lat; } -static inline int Ivy_LeafId( int Leaf ) { return Leaf >> 4; } -static inline int Ivy_LeafLat( int Leaf ) { return Leaf & 15; } +static inline int Ivy_LeafCreate( int Id, int Lat ) { return (Id << IVY_LEAF_BITS) | Lat; } +static inline int Ivy_LeafId( int Leaf ) { return Leaf >> IVY_LEAF_BITS; } +static inline int Ivy_LeafLat( int Leaf ) { return Leaf & IVY_LEAF_MASK; } static inline int Ivy_ManPiNum( Ivy_Man_t * p ) { return p->nObjs[IVY_PI]; } static inline int Ivy_ManPoNum( Ivy_Man_t * p ) { return p->nObjs[IVY_PO]; } @@ -261,12 +266,16 @@ static inline int Ivy_ObjFanoutC( Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout static inline Ivy_Obj_t * Ivy_ObjCreateGhost( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type, Ivy_Init_t Init ) { Ivy_Obj_t * pGhost, * pTemp; + assert( Type != IVY_AND || !Ivy_ObjIsConst1(Ivy_Regular(p0)) ); + assert( p1 == NULL || !Ivy_ObjIsConst1(Ivy_Regular(p1)) ); + assert( Type == IVY_PI || Ivy_Regular(p0) != Ivy_Regular(p1) ); + assert( Type != IVY_LATCH || !Ivy_IsComplement(p0) ); +// assert( p1 == NULL || (!Ivy_ObjIsLatch(Ivy_Regular(p0)) || !Ivy_ObjIsLatch(Ivy_Regular(p1))) ); pGhost = Ivy_ManGhost(p); pGhost->Type = Type; pGhost->Init = Init; pGhost->pFanin0 = p0; pGhost->pFanin1 = p1; - assert( Type == IVY_PI || Ivy_ObjFanin0(pGhost) != Ivy_ObjFanin1(pGhost) ); if ( p1 && Ivy_ObjFaninId0(pGhost) > Ivy_ObjFaninId1(pGhost) ) pTemp = pGhost->pFanin0, pGhost->pFanin0 = pGhost->pFanin1, pGhost->pFanin1 = pTemp; return pGhost; @@ -384,6 +393,7 @@ extern Vec_Int_t * Ivy_ManDfsSeq( Ivy_Man_t * p, Vec_Int_t ** pvLatches ); extern void Ivy_ManCollectCone( Ivy_Obj_t * pObj, Vec_Ptr_t * vFront, Vec_Ptr_t * vCone ); extern Vec_Vec_t * Ivy_ManLevelize( Ivy_Man_t * p ); extern Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p ); +extern int Ivy_ManIsAcyclic( Ivy_Man_t * p ); /*=== ivyDsd.c ==========================================================*/ extern int Ivy_TruthDsd( unsigned uTruth, Vec_Int_t * vTree ); extern void Ivy_TruthDsdPrint( FILE * pFile, Vec_Int_t * vTree ); @@ -400,11 +410,14 @@ extern void Ivy_ObjCollectFanouts( Ivy_Man_t * p, Ivy_Obj_t * pObj, V extern Ivy_Obj_t * Ivy_ObjReadOneFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj ); extern Ivy_Obj_t * Ivy_ObjReadFirstFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj ); extern int Ivy_ObjFanoutNum( Ivy_Man_t * p, Ivy_Obj_t * pObj ); +/*=== ivyIsop.c ==========================================================*/ +extern int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover ); +extern void Ivy_TruthManStop(); /*=== ivyMan.c ==========================================================*/ extern Ivy_Man_t * Ivy_ManStart(); extern void Ivy_ManStop( Ivy_Man_t * p ); extern int Ivy_ManCleanup( Ivy_Man_t * p ); -extern int Ivy_ManPropagateBuffers( Ivy_Man_t * p ); +extern int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel ); extern void Ivy_ManPrintStats( Ivy_Man_t * p ); extern void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits ); /*=== ivyMem.c ==========================================================*/ @@ -425,8 +438,8 @@ extern void Ivy_ObjDisconnect( Ivy_Man_t * p, Ivy_Obj_t * pObj ); extern void Ivy_ObjPatchFanin0( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFaninNew ); extern void Ivy_ObjDelete( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop ); extern void Ivy_ObjDelete_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop ); -extern void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop ); -extern void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode ); +extern void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop, int fUpdateLevel ); +extern void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel ); /*=== ivyOper.c =========================================================*/ extern Ivy_Obj_t * Ivy_Oper( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1, Ivy_Type_t Type ); extern Ivy_Obj_t * Ivy_And( Ivy_Man_t * p, Ivy_Obj_t * p0, Ivy_Obj_t * p1 ); @@ -442,6 +455,8 @@ extern Ivy_Man_t * Ivy_ManResyn( Ivy_Man_t * p, int fUpdateLevel, int fVerbo extern int Ivy_ManSeqRewrite( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost ); extern int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost ); extern int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fVerbose ); +/*=== ivySeq.c =========================================================*/ +extern int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose ); /*=== ivyTable.c ========================================================*/ extern Ivy_Obj_t * Ivy_TableLookup( Ivy_Man_t * p, Ivy_Obj_t * pObj ); extern void Ivy_TableInsert( Ivy_Man_t * p, Ivy_Obj_t * pObj ); @@ -456,6 +471,7 @@ extern unsigned * Ivy_ManCutTruth( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Vec_In extern Vec_Int_t * Ivy_ManLatches( Ivy_Man_t * p ); extern int Ivy_ManLevels( Ivy_Man_t * p ); extern void Ivy_ManResetLevels( Ivy_Man_t * p ); +extern int Ivy_ObjMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pObj ); extern void Ivy_ObjUpdateLevel_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj ); extern void Ivy_ObjUpdateLevelR_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int ReqNew ); extern int Ivy_ObjIsMuxType( Ivy_Obj_t * pObj ); diff --git a/src/temp/ivy/ivyCheck.c b/src/temp/ivy/ivyCheck.c index 4331c07e..36222f72 100644 --- a/src/temp/ivy/ivyCheck.c +++ b/src/temp/ivy/ivyCheck.c @@ -107,8 +107,8 @@ int Ivy_ManCheck( Ivy_Man_t * p ) printf( "Ivy_ManCheck: The AIG has node \"%d\" with a wrong ordering of fanins.\n", pObj->Id ); return 0; } -// if ( Ivy_ObjLevel(pObj) != Ivy_ObjLevelNew(pObj) ) -// printf( "Ivy_ManCheck: Node with ID \"%d\" has level %d but should have level %d.\n", pObj->Id, Ivy_ObjLevel(pObj), Ivy_ObjLevelNew(pObj) ); + if ( Ivy_ObjLevel(pObj) != Ivy_ObjLevelNew(pObj) ) + printf( "Ivy_ManCheck: Node with ID \"%d\" has level %d but should have level %d.\n", pObj->Id, Ivy_ObjLevel(pObj), Ivy_ObjLevelNew(pObj) ); pObj2 = Ivy_TableLookup( p, pObj ); if ( pObj2 != pObj ) printf( "Ivy_ManCheck: Node with ID \"%d\" is not in the structural hashing table.\n", pObj->Id ); @@ -124,6 +124,8 @@ int Ivy_ManCheck( Ivy_Man_t * p ) printf( "Ivy_ManCheck: The number of nodes in the structural hashing table is wrong.\n" ); return 0; } + if ( !Ivy_ManIsAcyclic(p) ) + return 0; return 1; } diff --git a/src/temp/ivy/ivyCut.c b/src/temp/ivy/ivyCut.c index 7d1ec63a..56f872e9 100644 --- a/src/temp/ivy/ivyCut.c +++ b/src/temp/ivy/ivyCut.c @@ -24,6 +24,8 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static inline int Ivy_NodeCutHashValue( int NodeId ) { return 1 << (NodeId % 31); } + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -580,6 +582,88 @@ static inline int Ivy_NodeCutExtend( Ivy_Cut_t * pCut, int iNew ) /**Function************************************************************* + Synopsis [Returns 1 if the cut can be constructed; 0 otherwise.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Ivy_NodeCutPrescreen( Ivy_Cut_t * pCut, int Id0, int Id1 ) +{ + int i; + if ( pCut->nSize < pCut->nSizeMax ) + return 1; + for ( i = 0; i < pCut->nSize; i++ ) + if ( pCut->pArray[i] == Id0 || pCut->pArray[i] == Id1 ) + return 1; + return 0; +} + +/**Function************************************************************* + + Synopsis [Derives new cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Ivy_NodeCutDeriveNew( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int IdOld, int IdNew0, int IdNew1 ) +{ + unsigned uHash = 0; + int i, k; + assert( pCut->nSize > 0 ); + assert( IdNew0 < IdNew1 ); + for ( i = k = 0; i < pCut->nSize; i++ ) + { + if ( pCut->pArray[i] == IdOld ) + continue; + if ( IdNew0 <= pCut->pArray[i] ) + { + if ( IdNew0 < pCut->pArray[i] ) + { + pCutNew->pArray[ k++ ] = IdNew0; + uHash |= Ivy_NodeCutHashValue( IdNew0 ); + } + IdNew0 = 0x7FFFFFFF; + } + if ( IdNew1 <= pCut->pArray[i] ) + { + if ( IdNew1 < pCut->pArray[i] ) + { + pCutNew->pArray[ k++ ] = IdNew1; + uHash |= Ivy_NodeCutHashValue( IdNew1 ); + } + IdNew1 = 0x7FFFFFFF; + } + pCutNew->pArray[ k++ ] = pCut->pArray[i]; + uHash |= Ivy_NodeCutHashValue( pCut->pArray[i] ); + } + if ( IdNew0 < 0x7FFFFFFF ) + { + pCutNew->pArray[ k++ ] = IdNew0; + uHash |= Ivy_NodeCutHashValue( IdNew0 ); + } + if ( IdNew1 < 0x7FFFFFFF ) + { + pCutNew->pArray[ k++ ] = IdNew1; + uHash |= Ivy_NodeCutHashValue( IdNew1 ); + } + pCutNew->nSize = k; + pCutNew->uHash = uHash; + assert( pCutNew->nSize <= pCut->nSizeMax ); +// for ( i = 1; i < pCutNew->nSize; i++ ) +// assert( pCutNew->pArray[i-1] < pCutNew->pArray[i] ); + return 1; +} + +/**Function************************************************************* + Synopsis [Check if the cut exists.] Description [Returns 1 if the cut exists.] @@ -789,7 +873,7 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves Ivy_Cut_t CutNew, * pCutNew = &CutNew, * pCut; Ivy_Man_t * pMan = p; Ivy_Obj_t * pLeaf; - int i, k; + int i, k, iLeaf0, iLeaf1; assert( nLeaves <= IVY_CUT_INPUT ); @@ -818,6 +902,7 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves pLeaf = Ivy_ManObj( p, pCut->pArray[k] ); if ( Ivy_ObjIsCi(pLeaf) ) continue; +/* *pCutNew = *pCut; Ivy_NodeCutShrink( pCutNew, pLeaf->Id ); if ( !Ivy_NodeCutExtend( pCutNew, Ivy_ObjFaninId0(pLeaf) ) ) @@ -825,6 +910,12 @@ Ivy_Store_t * Ivy_NodeFindCutsAll( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves if ( Ivy_ObjIsNode(pLeaf) && !Ivy_NodeCutExtend( pCutNew, Ivy_ObjFaninId1(pLeaf) ) ) continue; Ivy_NodeCutHash( pCutNew ); +*/ + iLeaf0 = Ivy_ObjFaninId0(pLeaf); + iLeaf1 = Ivy_ObjFaninId1(pLeaf); + if ( !Ivy_NodeCutPrescreen( pCut, iLeaf0, iLeaf1 ) ) + continue; + Ivy_NodeCutDeriveNew( pCut, pCutNew, pCut->pArray[k], iLeaf0, iLeaf1 ); Ivy_NodeCutFindOrAddFilter( pCutStore, pCutNew ); if ( pCutStore->nCuts == IVY_CUT_LIMIT ) break; diff --git a/src/temp/ivy/ivyDfs.c b/src/temp/ivy/ivyDfs.c index fb938c42..30671baf 100644 --- a/src/temp/ivy/ivyDfs.c +++ b/src/temp/ivy/ivyDfs.c @@ -250,6 +250,105 @@ Vec_Int_t * Ivy_ManRequiredLevels( Ivy_Man_t * p ) return vLevelsR; } +/**Function************************************************************* + + Synopsis [Recursively detects combinational loops.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManIsAcyclic_rec( Ivy_Man_t * p, Ivy_Obj_t * pNode ) +{ + if ( Ivy_ObjIsCi(pNode) || Ivy_ObjIsConst1(pNode) ) + return 1; + assert( Ivy_ObjIsNode( pNode ) ); + // make sure the node is not visited + assert( !Ivy_ObjIsTravIdPrevious(p, pNode) ); + // check if the node is part of the combinational loop + if ( Ivy_ObjIsTravIdCurrent(p, pNode) ) + { + fprintf( stdout, "Manager contains combinational loop!\n" ); + fprintf( stdout, "Node \"%d\" is encountered twice on the following path:\n", Ivy_ObjId(pNode) ); + fprintf( stdout, " %d", Ivy_ObjId(pNode) ); + return 0; + } + // mark this node as a node on the current path + Ivy_ObjSetTravIdCurrent( p, pNode ); + // check if the fanin is visited + if ( !Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin0(pNode)) ) + { + // traverse the fanin's cone searching for the loop + if ( !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pNode)) ) + { + // return as soon as the loop is detected + fprintf( stdout, " <-- %d", Ivy_ObjId(Ivy_ObjFanin0(pNode)) ); + return 0; + } + } + // check if the fanin is visited + if ( !Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin1(pNode)) ) + { + // traverse the fanin's cone searching for the loop + if ( !Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin1(pNode)) ) + { + // return as soon as the loop is detected + fprintf( stdout, " <-- %d", Ivy_ObjId(Ivy_ObjFanin1(pNode)) ); + return 0; + } + } + // mark this node as a visited node + Ivy_ObjSetTravIdPrevious( p, pNode ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Detects combinational loops.] + + Description [This procedure is based on the idea suggested by Donald Chai. + As we traverse the network and visit the nodes, we need to distinquish + three types of nodes: (1) those that are visited for the first time, + (2) those that have been visited in this traversal but are currently not + on the traversal path, (3) those that have been visited and are currently + on the travesal path. When the node of type (3) is encountered, it means + that there is a combinational loop. To mark the three types of nodes, + two new values of the traversal IDs are used.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManIsAcyclic( Ivy_Man_t * p ) +{ + Ivy_Obj_t * pNode; + int fAcyclic, i; + // set the traversal ID for this DFS ordering + Ivy_ManIncrementTravId( p ); + Ivy_ManIncrementTravId( p ); + // pNode->TravId == pNet->nTravIds means "pNode is on the path" + // pNode->TravId == pNet->nTravIds - 1 means "pNode is visited but is not on the path" + // pNode->TravId < pNet->nTravIds - 1 means "pNode is not visited" + // traverse the network to detect cycles + fAcyclic = 1; + Ivy_ManForEachCo( p, pNode, i ) + { + if ( Ivy_ObjIsTravIdPrevious(p, Ivy_ObjFanin0(pNode)) ) + continue; + // traverse the output logic cone + if ( fAcyclic = Ivy_ManIsAcyclic_rec(p, Ivy_ObjFanin0(pNode)) ) + continue; + // stop as soon as the first loop is detected + fprintf( stdout, " (cone of CO \"%d\")\n", Ivy_ObjFaninId0(pNode) ); + break; + } + return fAcyclic; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/temp/ivy/ivyFanout.c b/src/temp/ivy/ivyFanout.c index 5911e051..2295516d 100644 --- a/src/temp/ivy/ivyFanout.c +++ b/src/temp/ivy/ivyFanout.c @@ -153,6 +153,7 @@ void Ivy_ObjDeleteFanout( Ivy_Man_t * p, Ivy_Obj_t * pObj, Ivy_Obj_t * pFanout ) assert( *ppSpot == pFanout ); *ppSpot = NULL; } +// printf( " %d", Ivy_ObjFanoutNum(p, pObj) ); } /**Function************************************************************* diff --git a/src/temp/ivy/ivyIsop.c b/src/temp/ivy/ivyIsop.c index f53e513d..2d0101a7 100644 --- a/src/temp/ivy/ivyIsop.c +++ b/src/temp/ivy/ivyIsop.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "ivy.h" +#include "mem.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -33,7 +34,8 @@ struct Ivy_Sop_t_ static Mem_Flex_t * s_Man = NULL; -static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes ); +static unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy_Sop_t * pcRes ); +static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t * pcRes ); //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -41,7 +43,7 @@ static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy /**Function************************************************************* - Synopsis [] + Synopsis [Deallocates memory used for computing ISOPs from TTs.] Description [] @@ -50,14 +52,15 @@ static unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy SeeAlso [] ***********************************************************************/ -void Ivy_TruthManStart() +void Ivy_TruthManStop() { - s_Man = Mem_FlexStart(); + Mem_FlexStop( s_Man, 0 ); + s_Man = NULL; } /**Function************************************************************* - Synopsis [] + Synopsis [Computes ISOP from TT.] Description [] @@ -66,15 +69,37 @@ void Ivy_TruthManStart() SeeAlso [] ***********************************************************************/ -void Ivy_TruthManStop() +int Ivy_TruthIsopOne( unsigned * puTruth, int nVars, Vec_Int_t * vCover ) { - Mem_FlexStop( s_Man, 0 ); - s_Man = NULL; + Ivy_Sop_t cRes, * pcRes = &cRes; + unsigned * pResult; + int i; + assert( nVars >= 0 && nVars < 16 ); + // if nVars < 5, make sure it does not depend on those vars + for ( i = nVars; i < 5; i++ ) + assert( !Extra_TruthVarInSupport(puTruth, 5, i) ); + // prepare memory manager + if ( s_Man == NULL ) + s_Man = Mem_FlexStart(); + else + Mem_FlexRestart( s_Man ); + // compute ISOP + pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes ); +// Extra_PrintBinary( stdout, puTruth, 1 << nVars ); printf( "\n" ); +// Extra_PrintBinary( stdout, pResult, 1 << nVars ); printf( "\n" ); + assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) ); +//printf( "%d ", Mem_FlexReadMemUsage(s_Man) ); +//printf( "%d ", pcRes->nCubes ); + // copy the truth table + Vec_IntClear( vCover ); + for ( i = 0; i < pcRes->nCubes; i++ ) + Vec_IntPush( vCover, pcRes->pCubes[i] ); + return 0; } /**Function************************************************************* - Synopsis [] + Synopsis [Computes ISOP from TT.] Description [] @@ -83,13 +108,51 @@ void Ivy_TruthManStop() SeeAlso [] ***********************************************************************/ -Vec_Int_t * Ivy_TruthIsop( unsigned * uTruth, int nVars ) +int Ivy_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vCover ) { + Ivy_Sop_t cRes, * pcRes = &cRes; + unsigned * pResult; + int i; + assert( nVars >= 0 && nVars < 16 ); + // if nVars < 5, make sure it does not depend on those vars + for ( i = nVars; i < 5; i++ ) + assert( !Extra_TruthVarInSupport(puTruth, 5, i) ); + // prepare memory manager + if ( s_Man == NULL ) + s_Man = Mem_FlexStart(); + else + Mem_FlexRestart( s_Man ); + // compute ISOP + pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes ); +// Extra_PrintBinary( stdout, puTruth, 1 << nVars ); printf( "\n" ); +// Extra_PrintBinary( stdout, pResult, 1 << nVars ); printf( "\n" ); + assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) ); +//printf( "%d ", Mem_FlexReadMemUsage(s_Man) ); +//printf( "%d ", pcRes->nCubes ); + // copy the truth table + Vec_IntClear( vCover ); + for ( i = 0; i < pcRes->nCubes; i++ ) + Vec_IntPush( vCover, pcRes->pCubes[i] ); + + // try other polarity + Mem_FlexRestart( s_Man ); + Extra_TruthNot( puTruth, puTruth, nVars ); + pResult = Ivy_TruthIsop_rec( puTruth, puTruth, nVars, pcRes ); + assert( Extra_TruthIsEqual( puTruth, pResult, nVars ) ); + Extra_TruthNot( puTruth, puTruth, nVars ); + if ( Vec_IntSize(vCover) < pcRes->nCubes ) + return 0; + + // copy the truth table + Vec_IntClear( vCover ); + for ( i = 0; i < pcRes->nCubes; i++ ) + Vec_IntPush( vCover, pcRes->pCubes[i] ); + return 1; } /**Function************************************************************* - Synopsis [Computes ISOP for 5 variables or less.] + Synopsis [Computes ISOP 6 variables or more.] Description [] @@ -103,54 +166,59 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy Ivy_Sop_t cRes0, cRes1, cRes2; Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2; unsigned * puRes0, * puRes1, * puRes2; - unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp0, * pTemp1; - int i, k, Var, nWords; - assert( nVars > 5 ); + unsigned * puOn0, * puOn1, * puOnDc0, * puOnDc1, * pTemp, * pTemp0, * pTemp1; + int i, k, Var, nWords, nWordsAll; assert( Extra_TruthIsImply( puOn, puOnDc, nVars ) ); + // allocate room for the resulting truth table + nWordsAll = Extra_TruthWordNum( nVars ); + pTemp = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * nWordsAll ); + // check for constants if ( Extra_TruthIsConst0( puOn, nVars ) ) { pcRes->nCubes = 0; pcRes->pCubes = NULL; - return puOn; + Extra_TruthClear( pTemp, nVars ); + return pTemp; } if ( Extra_TruthIsConst1( puOnDc, nVars ) ) { pcRes->nCubes = 1; pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 ); pcRes->pCubes[0] = 0; - return puOnDc; + Extra_TruthFill( pTemp, nVars ); + return pTemp; } + assert( nVars > 0 ); // find the topmost var for ( Var = nVars-1; Var >= 0; Var-- ) if ( Extra_TruthVarInSupport( puOn, nVars, Var ) || Extra_TruthVarInSupport( puOnDc, nVars, Var ) ) break; assert( Var >= 0 ); + // consider a simple case when one-word computation can be used if ( Var < 5 ) { - unsigned * puRes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 ); - *puRes = Ivy_TruthIsop5_rec( puOn[0], puOnDc[0], Var + 1, pcRes ); - return puRes; + unsigned uRes = Ivy_TruthIsop5_rec( puOn[0], puOnDc[0], Var+1, pcRes ); + for ( i = 0; i < nWordsAll; i++ ) + pTemp[i] = uRes; + return pTemp; } - nWords = Extra_TruthWordNum( Var+1 ); + assert( Var >= 5 ); + nWords = Extra_TruthWordNum( Var ); // cofactor - puOn0 = puOn; - puOn1 = puOn + nWords; - puOnDc0 = puOnDc; - puOnDc1 = puOnDc + nWords; - // intermediate copies - pTemp0 = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * nWords ); - pTemp1 = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * nWords ); + puOn0 = puOn; puOn1 = puOn + nWords; + puOnDc0 = puOnDc; puOnDc1 = puOnDc + nWords; + pTemp0 = pTemp; pTemp1 = pTemp + nWords; // solve for cofactors - Extra_TruthSharp( pTemp0, puOn0, puOnDc1, Var + 1 ); - puRes0 = Ivy_TruthIsop5_rec( pTemp0, uOnDc0, Var-1, pcRes0 ); - Extra_TruthSharp( pTemp0, puOn1, puOnDc0, Var + 1 ); - puRes1 = Ivy_TruthIsop5_rec( pTemp1, uOnDc1, Var-1, pcRes1 ); - Extra_TruthSharp( pTemp0, puOn0, puRes0, Var + 1 ); - Extra_TruthSharp( pTemp1, puOn1, puRes1, Var + 1 ); - Extra_TruthOr( pTemp0, pTemp0, pTemp1, Var + 1 ); - Extra_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var + 1 ); - puRes2 = Ivy_TruthIsop5_rec( pTemp0, pTemp1, Var-1, pcRes2 ); + Extra_TruthSharp( pTemp0, puOn0, puOnDc1, Var ); + puRes0 = Ivy_TruthIsop_rec( pTemp0, puOnDc0, Var, pcRes0 ); + Extra_TruthSharp( pTemp1, puOn1, puOnDc0, Var ); + puRes1 = Ivy_TruthIsop_rec( pTemp1, puOnDc1, Var, pcRes1 ); + Extra_TruthSharp( pTemp0, puOn0, puRes0, Var ); + Extra_TruthSharp( pTemp1, puOn1, puRes1, Var ); + Extra_TruthOr( pTemp0, pTemp0, pTemp1, Var ); + Extra_TruthAnd( pTemp1, puOnDc0, puOnDc1, Var ); + puRes2 = Ivy_TruthIsop_rec( pTemp0, pTemp1, Var, pcRes2 ); // create the resulting cover pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes; pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * pcRes->nCubes ); @@ -159,13 +227,21 @@ unsigned * Ivy_TruthIsop_rec( unsigned * puOn, unsigned * puOnDc, int nVars, Ivy pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1)); for ( i = 0; i < pcRes1->nCubes; i++ ) pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+0)); - for ( i = 0; i < pcRes1->nCubes; i++ ) + for ( i = 0; i < pcRes2->nCubes; i++ ) pcRes->pCubes[k++] = pcRes2->pCubes[i]; assert( k == pcRes->nCubes ); // create the resulting truth table - Extra_TruthSharp( pTemp0, Var, uRes0, uRes1, Var + 1 ); - Extra_TruthOr( pTemp0, pTemp0, uRes2, Var + 1 ); - return pTemp0; + Extra_TruthOr( pTemp0, puRes0, puRes2, Var ); + Extra_TruthOr( pTemp1, puRes1, puRes2, Var ); + // copy the table if needed + nWords <<= 1; + for ( i = 1; i < nWordsAll/nWords; i++ ) + for ( k = 0; k < nWords; k++ ) + pTemp[i*nWords + k] = pTemp[k]; + // verify in the end +// assert( Extra_TruthIsImply( puOn, pTemp, nVars ) ); +// assert( Extra_TruthIsImply( pTemp, puOnDc, nVars ) ); + return pTemp; } /**Function************************************************************* @@ -184,12 +260,11 @@ unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; Ivy_Sop_t cRes0, cRes1, cRes2; Ivy_Sop_t * pcRes0 = &cRes0, * pcRes1 = &cRes1, * pcRes2 = &cRes2; - unsigned uRes0, uRes1, uRes2; - unsigned uOn0, uOn1, uOnDc0, uOnDc1; + unsigned uOn0, uOn1, uOnDc0, uOnDc1, uRes0, uRes1, uRes2; int i, k, Var; assert( nVars <= 5 ); - assert( uOn & ~uOnDc == 0 ); - if ( Extra_TruthIsConst0( uOn == 0 ) + assert( (uOn & ~uOnDc) == 0 ); + if ( uOn == 0 ) { pcRes->nCubes = 0; pcRes->pCubes = NULL; @@ -202,6 +277,7 @@ unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t pcRes->pCubes[0] = 0; return 0xFFFFFFFF; } + assert( nVars > 0 ); // find the topmost var for ( Var = nVars-1; Var >= 0; Var-- ) if ( Extra_TruthVarInSupport( &uOn, 5, Var ) || @@ -209,16 +285,16 @@ unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t break; assert( Var >= 0 ); // cofactor - uOn0 = uOn1 = uOn; + uOn0 = uOn1 = uOn; uOnDc0 = uOnDc1 = uOnDc; - Extra_TruthCofactor0( &uOn0, 5, Var ); - Extra_TruthCofactor1( &uOn1, 5, Var ); - Extra_TruthCofactor0( &uOnDc0, 5, Var ); - Extra_TruthCofactor1( &uOnDc1, 5, Var ); + Extra_TruthCofactor0( &uOn0, Var + 1, Var ); + Extra_TruthCofactor1( &uOn1, Var + 1, Var ); + Extra_TruthCofactor0( &uOnDc0, Var + 1, Var ); + Extra_TruthCofactor1( &uOnDc1, Var + 1, Var ); // solve for cofactors - uRes0 = Ivy_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var-1, pcRes0 ); - uRes1 = Ivy_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var-1, pcRes1 ); - uRes2 = Ivy_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var-1, pcRes2 ); + uRes0 = Ivy_TruthIsop5_rec( uOn0 & ~uOnDc1, uOnDc0, Var, pcRes0 ); + uRes1 = Ivy_TruthIsop5_rec( uOn1 & ~uOnDc0, uOnDc1, Var, pcRes1 ); + uRes2 = Ivy_TruthIsop5_rec( (uOn0 & ~uRes0) | (uOn1 & ~uRes1), uOnDc0 & uOnDc1, Var, pcRes2 ); // create the resulting cover pcRes->nCubes = pcRes0->nCubes + pcRes1->nCubes + pcRes2->nCubes; pcRes->pCubes = (unsigned *)Mem_FlexEntryFetch( s_Man, 4 * pcRes->nCubes ); @@ -227,10 +303,14 @@ unsigned Ivy_TruthIsop5_rec( unsigned uOn, unsigned uOnDc, int nVars, Ivy_Sop_t pcRes->pCubes[k++] = pcRes0->pCubes[i] | (1 << ((Var<<1)+1)); for ( i = 0; i < pcRes1->nCubes; i++ ) pcRes->pCubes[k++] = pcRes1->pCubes[i] | (1 << ((Var<<1)+0)); - for ( i = 0; i < pcRes1->nCubes; i++ ) + for ( i = 0; i < pcRes2->nCubes; i++ ) pcRes->pCubes[k++] = pcRes2->pCubes[i]; assert( k == pcRes->nCubes ); - return (uRes0 & ~uMasks[Var]) | (uRes1 & uMasks[Var]) | uRes2; + // derive the final truth table + uRes2 |= (uRes0 & ~uMasks[Var]) | (uRes1 & uMasks[Var]); +// assert( (uOn & ~uRes2) == 0 ); +// assert( (uRes2 & ~uOnDc) == 0 ); + return uRes2; } diff --git a/src/temp/ivy/ivyMan.c b/src/temp/ivy/ivyMan.c index d1aca8a6..c5b66ad0 100644 --- a/src/temp/ivy/ivyMan.c +++ b/src/temp/ivy/ivyMan.c @@ -109,9 +109,10 @@ int Ivy_ManCleanup( Ivy_Man_t * p ) Ivy_Obj_t * pNode; int i, nNodesOld; nNodesOld = Ivy_ManNodeNum(p); - Ivy_ManForEachNode( p, pNode, i ) - if ( Ivy_ObjRefs(pNode) == 0 ) - Ivy_ObjDelete_rec( p, pNode, 1 ); + Ivy_ManForEachObj( p, pNode, i ) + if ( Ivy_ObjIsNode(pNode) || Ivy_ObjIsLatch(pNode) || Ivy_ObjIsBuf(pNode) ) + if ( Ivy_ObjRefs(pNode) == 0 ) + Ivy_ObjDelete_rec( p, pNode, 1 ); return nNodesOld - Ivy_ManNodeNum(p); } @@ -126,7 +127,7 @@ int Ivy_ManCleanup( Ivy_Man_t * p ) SeeAlso [] ***********************************************************************/ -int Ivy_ManPropagateBuffers( Ivy_Man_t * p ) +int Ivy_ManPropagateBuffers( Ivy_Man_t * p, int fUpdateLevel ) { Ivy_Obj_t * pNode; int nSteps; @@ -135,7 +136,7 @@ int Ivy_ManPropagateBuffers( Ivy_Man_t * p ) pNode = Vec_PtrEntryLast(p->vBufs); while ( Ivy_ObjIsBuf(pNode) ) pNode = Ivy_ObjReadFirstFanout( p, pNode ); - Ivy_NodeFixBufferFanins( p, pNode ); + Ivy_NodeFixBufferFanins( p, pNode, fUpdateLevel ); } // printf( "Number of steps = %d\n", nSteps ); return nSteps; @@ -200,6 +201,9 @@ void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits ) pObj = Ivy_ManPo( p, Ivy_ManPoNum(p) - nLatches + i ); pLatch = Ivy_Latch( p, Ivy_ObjChild0(pObj), Init ); Ivy_ObjDisconnect( p, pObj ); + // recycle the old PO object + Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL ); + Ivy_ManRecycleMemory( p, pObj ); // convert the corresponding PI to a buffer and connect it to the latch pObj = Ivy_ManPi( p, Ivy_ManPiNum(p) - nLatches + i ); pObj->Type = IVY_BUF; @@ -215,8 +219,21 @@ void Ivy_ManMakeSeq( Ivy_Man_t * p, int nLatches, int * pInits ) p->nObjs[IVY_PO] -= nLatches; p->nObjs[IVY_BUF] += nLatches; p->nDeleted -= 2 * nLatches; + // remove dangling nodes + Ivy_ManCleanup(p); +/* + // check for dangling nodes + Ivy_ManForEachObj( p, pObj, i ) + if ( !Ivy_ObjIsPi(pObj) && !Ivy_ObjIsPo(pObj) && !Ivy_ObjIsConst1(pObj) ) + { + assert( Ivy_ObjRefs(pObj) > 0 ); + assert( Ivy_ObjRefs(pObj) == Ivy_ObjFanoutNum(p, pObj) ); + } +*/ // perform hashing by propagating the buffers - Ivy_ManPropagateBuffers( p ); + Ivy_ManPropagateBuffers( p, 0 ); + // fix the levels + Ivy_ManResetLevels( p ); // check the resulting network if ( !Ivy_ManCheck(p) ) printf( "Ivy_ManMakeSeq(): The check has failed.\n" ); diff --git a/src/temp/ivy/ivyObj.c b/src/temp/ivy/ivyObj.c index de67c560..735d79c3 100644 --- a/src/temp/ivy/ivyObj.c +++ b/src/temp/ivy/ivyObj.c @@ -300,7 +300,7 @@ void Ivy_ObjDelete_rec( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fFreeTop ) SeeAlso [] ***********************************************************************/ -void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop ) +void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, int fDeleteOld, int fFreeTop, int fUpdateLevel ) { int nRefsOld; // the object to be replaced cannot be complemented @@ -315,26 +315,32 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in if ( Ivy_IsComplement(pObjNew) || Ivy_ObjIsLatch(pObjNew) || Ivy_ObjRefs(pObjNew) > 0 || Ivy_ObjIsPi(pObjNew) || Ivy_ObjIsConst1(pObjNew) ) pObjNew = Ivy_ObjCreate( p, Ivy_ObjCreateGhost(p, pObjNew, NULL, IVY_BUF, IVY_INIT_NONE) ); assert( !Ivy_IsComplement(pObjNew) ); - // if the new node's arrival time is different, recursively update arrival time of the fanouts - if ( p->vFanouts && !Ivy_ObjIsBuf(pObjNew) && pObjOld->Level != pObjNew->Level ) + if ( fUpdateLevel ) { - assert( Ivy_ObjIsNode(pObjOld) ); - pObjOld->Level = pObjNew->Level; - Ivy_ObjUpdateLevel_rec( p, pObjOld ); - } - // if the new node's required time has changed, recursively update required time of the fanins - if ( p->vRequired ) - { - int ReqNew = Vec_IntEntry(p->vRequired, pObjOld->Id); - if ( ReqNew < Vec_IntEntry(p->vRequired, pObjNew->Id) ) + // if the new node's arrival time is different, recursively update arrival time of the fanouts + if ( p->vFanouts && !Ivy_ObjIsBuf(pObjNew) && pObjOld->Level != pObjNew->Level ) + { + assert( Ivy_ObjIsNode(pObjOld) ); + pObjOld->Level = pObjNew->Level; + Ivy_ObjUpdateLevel_rec( p, pObjOld ); + } + // if the new node's required time has changed, recursively update required time of the fanins + if ( p->vRequired ) { - Vec_IntWriteEntry( p->vRequired, pObjNew->Id, ReqNew ); - Ivy_ObjUpdateLevelR_rec( p, pObjNew, ReqNew ); + int ReqNew = Vec_IntEntry(p->vRequired, pObjOld->Id); + if ( ReqNew < Vec_IntEntry(p->vRequired, pObjNew->Id) ) + { + Vec_IntWriteEntry( p->vRequired, pObjNew->Id, ReqNew ); + Ivy_ObjUpdateLevelR_rec( p, pObjNew, ReqNew ); + } } } // delete the old object if ( fDeleteOld ) Ivy_ObjDelete_rec( p, pObjOld, fFreeTop ); + // make sure object is pointing to itself + assert( Ivy_ObjFanin0(pObjNew) == NULL || pObjOld != Ivy_ObjFanin0(pObjNew) ); + assert( Ivy_ObjFanin1(pObjNew) == NULL || pObjOld != Ivy_ObjFanin1(pObjNew) ); // transfer the old object assert( Ivy_ObjRefs(pObjNew) == 0 ); nRefsOld = pObjOld->nRefs; @@ -370,7 +376,7 @@ void Ivy_ObjReplace( Ivy_Man_t * p, Ivy_Obj_t * pObjOld, Ivy_Obj_t * pObjNew, in SeeAlso [] ***********************************************************************/ -void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode ) +void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel ) { Ivy_Obj_t * pFanReal0, * pFanReal1, * pResult; if ( Ivy_ObjIsPo(pNode) ) @@ -394,7 +400,7 @@ void Ivy_NodeFixBufferFanins( Ivy_Man_t * p, Ivy_Obj_t * pNode ) else assert( 0 ); // perform the replacement - Ivy_ObjReplace( p, pNode, pResult, 1, 0 ); + Ivy_ObjReplace( p, pNode, pResult, 1, 0, fUpdateLevel ); } //////////////////////////////////////////////////////////////////////// diff --git a/src/temp/ivy/ivyRwrAlg.c b/src/temp/ivy/ivyRwrAlg.c index 234827ff..fc48deb0 100644 --- a/src/temp/ivy/ivyRwrAlg.c +++ b/src/temp/ivy/ivyRwrAlg.c @@ -80,7 +80,7 @@ int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost ) // the case of constant 0 cone if ( RetValue == -1 ) { - Ivy_ObjReplace( pObj, Ivy_ManConst0(p), 1, 0 ); + Ivy_ObjReplace( pObj, Ivy_ManConst0(p), 1, 0, 1 ); continue; } assert( Vec_PtrSize(vLeaves) > 2 ); @@ -94,7 +94,7 @@ int Ivy_ManRewriteAlg( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost ) if ( Ivy_ObjLevel(Ivy_Regular(pResult)) > LevelR && Ivy_ObjRefs(Ivy_Regular(pResult)) == 0 ) Ivy_ObjDelete_rec(Ivy_Regular(pResult), 1), CountUndo++; else - Ivy_ObjReplace( pObj, pResult, 1, 0 ), CountUsed++; + Ivy_ObjReplace( pObj, pResult, 1, 0, 1 ), CountUsed++; } printf( "Used = %d. Undo = %d.\n", CountUsed, CountUndo ); Vec_PtrFree( vFront ); diff --git a/src/temp/ivy/ivyRwrPre.c b/src/temp/ivy/ivyRwrPre.c index d2a1697e..537b64ff 100644 --- a/src/temp/ivy/ivyRwrPre.c +++ b/src/temp/ivy/ivyRwrPre.c @@ -27,9 +27,8 @@ //////////////////////////////////////////////////////////////////////// static unsigned Ivy_NodeGetTruth( Ivy_Obj_t * pObj, int * pNums, int nNums ); -static int Ivy_NodeMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pObj ); static int Ivy_NodeRewrite( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUpdateLevel, int fUseZeroCost ); -static Dec_Graph_t * Rwt_CutEvaluate( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, +static Dec_Graph_t * Rwt_CutEvaluate( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth ); static int Ivy_GraphToNetworkCount( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax, int LevelMax ); @@ -74,7 +73,7 @@ int Ivy_ManRewritePre( Ivy_Man_t * p, int fUpdateLevel, int fUseZeroCost, int fV Ivy_ManForEachNode( p, pNode, i ) { // fix the fanin buffer problem - Ivy_NodeFixBufferFanins( p, pNode ); + Ivy_NodeFixBufferFanins( p, pNode, 1 ); if ( Ivy_ObjIsBuf(pNode) ) continue; // stop if all nodes have been tried once @@ -120,8 +119,8 @@ Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart ); // fix the levels if ( fUpdateLevel ) Vec_IntFree( p->vRequired ), p->vRequired = NULL; -// else -// Ivy_ManResetLevels( p ); + else + Ivy_ManResetLevels( p ); // check if ( i = Ivy_ManCleanup(p) ) printf( "Cleanup after rewriting removed %d dangling nodes.\n", i ); @@ -182,7 +181,11 @@ clk = clock(); if ( Ivy_ObjIsBuf( Ivy_ManObj(pMan, pCut->pArray[i]) ) ) break; if ( i != pCut->nSize ) + { + p->nCutsBad++; continue; + } + p->nCutsGood++; // get the fanin permutation clk2 = clock(); uTruth = 0xFFFF & Ivy_NodeGetTruth( pNode, pCut->pArray, pCut->nSize ); // truth table @@ -211,7 +214,7 @@ clk2 = clock(); Ivy_ObjRefsInc( Ivy_Regular(pFanin) ); // label MFFC with current ID Ivy_ManIncrementTravId( pMan ); - nNodesSaved = Ivy_NodeMffcLabel( pMan, pNode ); + nNodesSaved = Ivy_ObjMffcLabel( pMan, pNode ); // unmark the fanin boundary Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i ) Ivy_ObjRefsDec( Ivy_Regular(pFanin) ); @@ -219,7 +222,7 @@ p->timeMffc += clock() - clk2; // evaluate the cut clk2 = clock(); - pGraph = Rwt_CutEvaluate( pMan, p, pNode, pCut, p->vFaninsCur, nNodesSaved, Required, &GainCur, uTruth ); + pGraph = Rwt_CutEvaluate( pMan, p, pNode, p->vFaninsCur, nNodesSaved, Required, &GainCur, uTruth ); p->timeEval += clock() - clk2; // check if the cut is better than the current best one @@ -289,75 +292,6 @@ p->timeRes += clock() - clk; return GainBest; } - -/**Function************************************************************* - - Synopsis [References/references the node and returns MFFC size.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ivy_NodeRefDeref( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fReference, int fLabel ) -{ - Ivy_Obj_t * pNode0, * pNode1; - int Counter; - // label visited nodes - if ( fLabel ) - Ivy_ObjSetTravIdCurrent( p, pNode ); - // skip the CI - if ( Ivy_ObjIsCi(pNode) ) - return 0; - assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsBuf(pNode) ); - // process the internal node - pNode0 = Ivy_ObjFanin0(pNode); - pNode1 = Ivy_ObjFanin1(pNode); - Counter = Ivy_ObjIsNode(pNode); - if ( fReference ) - { - if ( pNode0->nRefs++ == 0 ) - Counter += Ivy_NodeRefDeref( p, pNode0, fReference, fLabel ); - if ( pNode1 && pNode1->nRefs++ == 0 ) - Counter += Ivy_NodeRefDeref( p, pNode1, fReference, fLabel ); - } - else - { - assert( pNode0->nRefs > 0 ); - assert( pNode1 == NULL || pNode1->nRefs > 0 ); - if ( --pNode0->nRefs == 0 ) - Counter += Ivy_NodeRefDeref( p, pNode0, fReference, fLabel ); - if ( pNode1 && --pNode1->nRefs == 0 ) - Counter += Ivy_NodeRefDeref( p, pNode1, fReference, fLabel ); - } - return Counter; -} - -/**Function************************************************************* - - Synopsis [Computes the size of MFFC and labels nodes with the current TravId.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Ivy_NodeMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pNode ) -{ - int nConeSize1, nConeSize2; - assert( !Ivy_IsComplement( pNode ) ); - assert( Ivy_ObjIsNode( pNode ) ); - nConeSize1 = Ivy_NodeRefDeref( p, pNode, 0, 1 ); // dereference - nConeSize2 = Ivy_NodeRefDeref( p, pNode, 1, 0 ); // reference - assert( nConeSize1 == nConeSize2 ); - assert( nConeSize1 > 0 ); - return nConeSize1; -} - /**Function************************************************************* Synopsis [Computes the truth table.] @@ -418,7 +352,7 @@ unsigned Ivy_NodeGetTruth( Ivy_Obj_t * pObj, int * pNums, int nNums ) SeeAlso [] ***********************************************************************/ -Dec_Graph_t * Rwt_CutEvaluate( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth ) +Dec_Graph_t * Rwt_CutEvaluate( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int LevelMax, int * pGainBest, unsigned uTruth ) { Vec_Ptr_t * vSubgraphs; Dec_Graph_t * pGraphBest, * pGraphCur; @@ -596,12 +530,12 @@ void Ivy_GraphUpdateNetwork( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGr printf( "%d", Ivy_ObjRefs(Ivy_Regular(pRootNew)) ); printf( " " ); */ - Ivy_ObjReplace( p, pRoot, pRootNew, 1, 0 ); + Ivy_ObjReplace( p, pRoot, pRootNew, 1, 0, 1 ); // compare the gains nNodesNew = Ivy_ManNodeNum(p); assert( nGain <= nNodesOld - nNodesNew ); // propagate the buffer - Ivy_ManPropagateBuffers( p ); + Ivy_ManPropagateBuffers( p, 1 ); } /**Function************************************************************* @@ -649,7 +583,7 @@ void Ivy_GraphUpdateNetwork3( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pG printf( "%d", Ivy_ObjRefs(Ivy_Regular(pRootNew)) ); printf( " " ); */ - Ivy_ObjReplace( p, pRoot, pRootNew, 0, 0 ); + Ivy_ObjReplace( p, pRoot, pRootNew, 0, 0, 1 ); //printf( "Replace = %d. ", Ivy_ManNodeNum(p) ); // delete remaining dangling nodes diff --git a/src/temp/ivy/ivySeq.c b/src/temp/ivy/ivySeq.c index 1cfa8c4b..8fd1b63b 100644 --- a/src/temp/ivy/ivySeq.c +++ b/src/temp/ivy/ivySeq.c @@ -13,17 +13,28 @@ Affiliation [UC Berkeley] Date [Ver. 1.0. Started - May 11, 2006.] - + Revision [$Id: ivySeq.c,v 1.00 2006/05/11 00:00:00 alanmi Exp $] ***********************************************************************/ #include "ivy.h" +#include "deco.h" +#include "rwt.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +static int Ivy_NodeRewriteSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUseZeroCost ); +static void Ivy_GraphPrepare( Dec_Graph_t * pGraph, Ivy_Cut_t * pCut, Vec_Ptr_t * vFanins, char * pPerm ); +static unsigned Ivy_CutGetTruth( Ivy_Man_t * p, Ivy_Obj_t * pObj, int * pNums, int nNums ); +static Dec_Graph_t * Rwt_CutEvaluateSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, char * pPerm, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int * pGainBest, unsigned uTruth ); +static int Ivy_GraphToNetworkSeqCountSeq( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax ); +static Ivy_Obj_t * Ivy_GraphToNetworkSeq( Ivy_Man_t * p, Dec_Graph_t * pGraph ); +static void Ivy_GraphUpdateNetworkSeq( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain ); +static Ivy_Store_t * Ivy_CutComputeForNode( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeaves ); + static inline int Ivy_CutHashValue( int NodeId ) { return 1 << (NodeId % 31); } //////////////////////////////////////////////////////////////////////// @@ -32,6 +43,295 @@ static inline int Ivy_CutHashValue( int NodeId ) { return 1 << (NodeId % 31); } /**Function************************************************************* + Synopsis [Performs incremental rewriting of the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose ) +{ + Rwt_Man_t * pManRwt; + Ivy_Obj_t * pNode; + int i, nNodes, nGain; + int clk, clkStart = clock(); + // start the rewriting manager + pManRwt = Rwt_ManStart( 0 ); + p->pData = pManRwt; + if ( pManRwt == NULL ) + return 0; + // create fanouts + if ( p->vFanouts == NULL ) + Ivy_ManStartFanout( p ); + // resynthesize each node once + nNodes = Ivy_ManObjIdMax(p); + Ivy_ManForEachNode( p, pNode, i ) + { + assert( !Ivy_ObjIsBuf(pNode) ); + assert( !Ivy_ObjIsBuf(Ivy_ObjFanin0(pNode)) ); + assert( !Ivy_ObjIsBuf(Ivy_ObjFanin1(pNode)) ); + // fix the fanin buffer problem +// Ivy_NodeFixBufferFanins( p, pNode ); +// if ( Ivy_ObjIsBuf(pNode) ) +// continue; + // stop if all nodes have been tried once + if ( i > nNodes ) + break; + if ( i == 8648 ) + { + int x = 0; + } + // for each cut, try to resynthesize it + nGain = Ivy_NodeRewriteSeq( p, pManRwt, pNode, fUseZeroCost ); + if ( nGain > 0 || nGain == 0 && fUseZeroCost ) + { + Dec_Graph_t * pGraph = Rwt_ManReadDecs(pManRwt); + int fCompl = Rwt_ManReadCompl(pManRwt); + // complement the FF if needed +clk = clock(); + if ( fCompl ) Dec_GraphComplement( pGraph ); + Ivy_GraphUpdateNetworkSeq( p, pNode, pGraph, nGain ); + if ( fCompl ) Dec_GraphComplement( pGraph ); +Rwt_ManAddTimeUpdate( pManRwt, clock() - clk ); +/* + if ( !Ivy_ManIsAcyclic(p) ) + { + int x = 0; + } +*/ + } + } +Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart ); + // print stats + if ( fVerbose ) + Rwt_ManPrintStats( pManRwt ); + // delete the managers + Rwt_ManStop( pManRwt ); + p->pData = NULL; + // fix the levels + Ivy_ManResetLevels( p ); + // check + if ( !Ivy_ManCheck(p) ) + printf( "Ivy_ManRewritePre(): The check has failed.\n" ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Performs rewriting for one node.] + + Description [This procedure considers all the cuts computed for the node + and tries to rewrite each of them using the "forest" of different AIG + structures precomputed and stored in the RWR manager. + Determines the best rewriting and computes the gain in the number of AIG + nodes in the final network. In the end, p->vFanins contains information + about the best cut that can be used for rewriting, while p->pGraph gives + the decomposition dag (represented using decomposition graph data structure). + Returns gain in the number of nodes or -1 if node cannot be rewritten.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_NodeRewriteSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int fUseZeroCost ) +{ + int fVeryVerbose = 0; + Dec_Graph_t * pGraph; + Ivy_Store_t * pStore; + Ivy_Cut_t * pCut; + Ivy_Obj_t * pFanin; + unsigned uPhase, uTruthBest, uTruth; + char * pPerm; + int nNodesSaved, nNodesSaveCur; + int i, c, GainCur, GainBest = -1; + int clk, clk2; + + p->nNodesConsidered++; + // get the node's cuts +clk = clock(); + pStore = Ivy_CutComputeForNode( pMan, pNode, 5 ); +p->timeCut += clock() - clk; + + // go through the cuts +clk = clock(); + for ( c = 1; c < pStore->nCuts; c++ ) + { + pCut = pStore->pCuts + c; + // consider only 4-input cuts + if ( pCut->nSize != 4 ) + continue; + // skip the cuts with buffers + for ( i = 0; i < (int)pCut->nSize; i++ ) + if ( Ivy_ObjIsBuf( Ivy_ManObj(pMan, Ivy_LeafId(pCut->pArray[i])) ) ) + break; + if ( i != pCut->nSize ) + { + p->nCutsBad++; + continue; + } + p->nCutsGood++; + // get the fanin permutation +clk2 = clock(); + uTruth = 0xFFFF & Ivy_CutGetTruth( pMan, pNode, pCut->pArray, pCut->nSize ); // truth table +p->timeTruth += clock() - clk2; + pPerm = p->pPerms4[ p->pPerms[uTruth] ]; + uPhase = p->pPhases[uTruth]; + // collect fanins with the corresponding permutation/phase + Vec_PtrClear( p->vFaninsCur ); + Vec_PtrFill( p->vFaninsCur, (int)pCut->nSize, 0 ); + for ( i = 0; i < (int)pCut->nSize; i++ ) + { + pFanin = Ivy_ManObj( pMan, Ivy_LeafId( pCut->pArray[pPerm[i]] ) ); + assert( Ivy_ObjIsNode(pFanin) || Ivy_ObjIsCi(pFanin) || Ivy_ObjIsConst1(pFanin) ); + pFanin = Ivy_NotCond(pFanin, ((uPhase & (1<<i)) > 0) ); + Vec_PtrWriteEntry( p->vFaninsCur, i, pFanin ); + } +clk2 = clock(); + // mark the fanin boundary + Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i ) + Ivy_ObjRefsInc( Ivy_Regular(pFanin) ); + // label MFFC with current ID + Ivy_ManIncrementTravId( pMan ); + nNodesSaved = Ivy_ObjMffcLabel( pMan, pNode ); + // unmark the fanin boundary + Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i ) + Ivy_ObjRefsDec( Ivy_Regular(pFanin) ); +p->timeMffc += clock() - clk2; +/* +if ( pNode->Id == 8648 ) +{ + int i; + printf( "Trying cut : {" ); + for ( i = 0; i < pCut->nSize; i++ ) + printf( " %d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) ); +// printf( " }\n" ); + printf( " } " ); + Extra_PrintBinary( stdout, &uTruth, 16 ); printf( "\n" ); +} +*/ + + // evaluate the cut +clk2 = clock(); + pGraph = Rwt_CutEvaluateSeq( pMan, p, pNode, pCut, pPerm, p->vFaninsCur, nNodesSaved, &GainCur, uTruth ); +p->timeEval += clock() - clk2; + + + // check if the cut is better than the current best one + if ( pGraph != NULL && GainBest < GainCur ) + { + // save this form + nNodesSaveCur = nNodesSaved; + GainBest = GainCur; + p->pGraph = pGraph; + p->pCut = pCut; + p->pPerm = pPerm; + p->fCompl = ((uPhase & (1<<4)) > 0); + uTruthBest = uTruth; + // collect fanins in the + Vec_PtrClear( p->vFanins ); + Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i ) + Vec_PtrPush( p->vFanins, pFanin ); + } + } +p->timeRes += clock() - clk; + + if ( GainBest == -1 ) + return -1; + + // copy the leaves + Ivy_GraphPrepare( p->pGraph, p->pCut, p->vFanins, p->pPerm ); + + p->nScores[p->pMap[uTruthBest]]++; + p->nNodesGained += GainBest; + if ( fUseZeroCost || GainBest > 0 ) + p->nNodesRewritten++; + +/* + if ( GainBest > 0 ) + { + Ivy_Cut_t * pCut = p->pCut; + printf( "Useful cut : {" ); + for ( i = 0; i < pCut->nSize; i++ ) + printf( " %5d[%2d](%2d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]), + Ivy_ObjRefs( Ivy_ManObj(pMan, Ivy_LeafId(pCut->pArray[i])) ) ); + printf( " }\n" ); + } +*/ + + // report the progress + if ( fVeryVerbose && GainBest > 0 ) + { + printf( "Node %6d : ", Ivy_ObjId(pNode) ); + printf( "Fanins = %d. ", p->vFanins->nSize ); + printf( "Save = %d. ", nNodesSaveCur ); + printf( "Add = %d. ", nNodesSaveCur-GainBest ); + printf( "GAIN = %d. ", GainBest ); + printf( "Cone = %d. ", p->pGraph? Dec_GraphNodeNum(p->pGraph) : 0 ); + printf( "Class = %d. ", p->pMap[uTruthBest] ); + printf( "\n" ); + } + return GainBest; +} + + +/**Function************************************************************* + + Synopsis [Evaluates the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Rwt_CutEvaluateSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pRoot, Ivy_Cut_t * pCut, char * pPerm, Vec_Ptr_t * vFaninsCur, int nNodesSaved, int * pGainBest, unsigned uTruth ) +{ + Vec_Ptr_t * vSubgraphs; + Dec_Graph_t * pGraphBest, * pGraphCur; + Rwt_Node_t * pNode; + int nNodesAdded, GainBest, i; + // find the matching class of subgraphs + vSubgraphs = Vec_VecEntry( p->vClasses, p->pMap[uTruth] ); + p->nSubgraphs += vSubgraphs->nSize; + // determine the best subgraph + GainBest = -1; + Vec_PtrForEachEntry( vSubgraphs, pNode, i ) + { + // get the current graph + pGraphCur = (Dec_Graph_t *)pNode->pNext; + +// if ( pRoot->Id == 8648 ) +// Dec_GraphPrint( stdout, pGraphCur, NULL, NULL ); + // copy the leaves +// Vec_PtrForEachEntry( vFaninsCur, pFanin, k ) +// Dec_GraphNode(pGraphCur, k)->pFunc = pFanin; + Ivy_GraphPrepare( pGraphCur, pCut, vFaninsCur, pPerm ); + + // detect how many unlabeled nodes will be reused + nNodesAdded = Ivy_GraphToNetworkSeqCountSeq( pMan, pRoot, pGraphCur, nNodesSaved ); + if ( nNodesAdded == -1 ) + continue; + assert( nNodesSaved >= nNodesAdded ); + // count the gain at this node + if ( GainBest < nNodesSaved - nNodesAdded ) + { + GainBest = nNodesSaved - nNodesAdded; + pGraphBest = pGraphCur; + } + } + if ( GainBest == -1 ) + return NULL; + *pGainBest = GainBest; + return pGraphBest; +} + +/**Function************************************************************* + Synopsis [] Description [] @@ -41,8 +341,250 @@ static inline int Ivy_CutHashValue( int NodeId ) { return 1 << (NodeId % 31); } SeeAlso [] ***********************************************************************/ +void Ivy_GraphPrepare( Dec_Graph_t * pGraph, Ivy_Cut_t * pCut, Vec_Ptr_t * vFanins, char * pPerm ) +{ + Dec_Node_t * pNode, * pNode0, * pNode1; + int i; + assert( Dec_GraphLeaveNum(pGraph) == pCut->nSize ); + assert( Vec_PtrSize(vFanins) == pCut->nSize ); + // label the leaves with latch numbers + Dec_GraphForEachLeaf( pGraph, pNode, i ) + { + pNode->pFunc = Vec_PtrEntry( vFanins, i ); + pNode->nLat2 = Ivy_LeafLat( pCut->pArray[pPerm[i]] ); + } + // propagate latches through the nodes + Dec_GraphForEachNode( pGraph, pNode, i ) + { + // get the children of this node + pNode0 = Dec_GraphNode( pGraph, pNode->eEdge0.Node ); + pNode1 = Dec_GraphNode( pGraph, pNode->eEdge1.Node ); + // distribute the latches + pNode->nLat2 = IVY_MIN( pNode0->nLat2, pNode1->nLat2 ); + pNode->nLat0 = pNode0->nLat2 - pNode->nLat2; + pNode->nLat1 = pNode1->nLat2 - pNode->nLat2; + } +} + +/**Function************************************************************* + + Synopsis [Counts the number of new nodes added when using this graph.] + + Description [AIG nodes for the fanins should be assigned to pNode->pFunc + of the leaves of the graph before calling this procedure. + Returns -1 if the number of nodes and levels exceeded the given limit or + the number of levels exceeded the maximum allowed level.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_GraphToNetworkSeqCountSeq( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int NodeMax ) +{ + Dec_Node_t * pNode, * pNode0, * pNode1; + Ivy_Obj_t * pAnd, * pAnd0, * pAnd1; + int i, k, Counter, fCompl; + // check for constant function or a literal + if ( Dec_GraphIsConst(pGraph) || Dec_GraphIsVar(pGraph) ) + return 0; + // compute the AIG size after adding the internal nodes + Counter = 0; + Dec_GraphForEachNode( pGraph, pNode, i ) + { + // get the children of this node + pNode0 = Dec_GraphNode( pGraph, pNode->eEdge0.Node ); + pNode1 = Dec_GraphNode( pGraph, pNode->eEdge1.Node ); + // get the AIG nodes corresponding to the children + pAnd0 = pNode0->pFunc; + pAnd1 = pNode1->pFunc; + // skip the latches + for ( k = 0; pAnd0 && k < (int)pNode->nLat0; k++ ) + { + fCompl = Ivy_IsComplement(pAnd0); + pAnd0 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Regular(pAnd0), NULL, IVY_LATCH, IVY_INIT_DC) ); + if ( pAnd0 ) + pAnd0 = Ivy_NotCond( pAnd0, fCompl ); + } + for ( k = 0; pAnd1 && k < (int)pNode->nLat1; k++ ) + { + fCompl = Ivy_IsComplement(pAnd1); + pAnd1 = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, Ivy_Regular(pAnd1), NULL, IVY_LATCH, IVY_INIT_DC) ); + if ( pAnd1 ) + pAnd1 = Ivy_NotCond( pAnd1, fCompl ); + } + // get the new node + if ( pAnd0 && pAnd1 ) + { + // if they are both present, find the resulting node + pAnd0 = Ivy_NotCond( pAnd0, pNode->eEdge0.fCompl ); + pAnd1 = Ivy_NotCond( pAnd1, pNode->eEdge1.fCompl ); + assert( !Ivy_ObjIsLatch(Ivy_Regular(pAnd0)) || !Ivy_ObjIsLatch(Ivy_Regular(pAnd1)) ); + if ( Ivy_Regular(pAnd0) == Ivy_Regular(pAnd1) || Ivy_ObjIsConst1(Ivy_Regular(pAnd0)) || Ivy_ObjIsConst1(Ivy_Regular(pAnd1)) ) + pAnd = Ivy_And( p, pAnd0, pAnd1 ); + else + pAnd = Ivy_TableLookup( p, Ivy_ObjCreateGhost(p, pAnd0, pAnd1, IVY_AND, IVY_INIT_NONE) ); + // return -1 if the node is the same as the original root + if ( Ivy_Regular(pAnd) == pRoot ) + return -1; + } + else + pAnd = NULL; + // count the number of added nodes + if ( pAnd == NULL || Ivy_ObjIsTravIdCurrent(p, Ivy_Regular(pAnd)) ) + { + if ( ++Counter > NodeMax ) + return -1; + } + pNode->pFunc = pAnd; + } + return Counter; +} + + +/**Function************************************************************* + + Synopsis [Transforms the decomposition graph into the AIG.] + + Description [AIG nodes for the fanins should be assigned to pNode->pFunc + of the leaves of the graph before calling this procedure.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Ivy_Obj_t * Ivy_GraphToNetworkSeq( Ivy_Man_t * p, Dec_Graph_t * pGraph ) +{ + Ivy_Obj_t * pAnd0, * pAnd1; + Dec_Node_t * pNode; + int i, k; + // check for constant function + if ( Dec_GraphIsConst(pGraph) ) + return Ivy_NotCond( Ivy_ManConst1(p), Dec_GraphIsComplement(pGraph) ); + // check for a literal + if ( Dec_GraphIsVar(pGraph) ) + { + // get the variable node + pNode = Dec_GraphVar(pGraph); + // add the remaining latches + for ( k = 0; k < (int)pNode->nLat2; k++ ) + pNode->pFunc = Ivy_Latch( p, pNode->pFunc, IVY_INIT_DC ); + return Ivy_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) ); + } + // build the AIG nodes corresponding to the AND gates of the graph + Dec_GraphForEachNode( pGraph, pNode, i ) + { + pAnd0 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); + pAnd1 = Ivy_NotCond( Dec_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); + // add the latches + for ( k = 0; k < (int)pNode->nLat0; k++ ) + pAnd0 = Ivy_Latch( p, pAnd0, IVY_INIT_DC ); + for ( k = 0; k < (int)pNode->nLat1; k++ ) + pAnd1 = Ivy_Latch( p, pAnd1, IVY_INIT_DC ); + // create the node + pNode->pFunc = Ivy_And( p, pAnd0, pAnd1 ); + } + // add the remaining latches + for ( k = 0; k < (int)pNode->nLat2; k++ ) + pNode->pFunc = Ivy_Latch( p, pNode->pFunc, IVY_INIT_DC ); + // complement the result if necessary + return Ivy_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) ); +} + +/**Function************************************************************* + + Synopsis [Replaces MFFC of the node by the new factored form.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ivy_GraphUpdateNetworkSeq( Ivy_Man_t * p, Ivy_Obj_t * pRoot, Dec_Graph_t * pGraph, int nGain ) +{ + Ivy_Obj_t * pRootNew; + int nNodesNew, nNodesOld; + nNodesOld = Ivy_ManNodeNum(p); + // create the new structure of nodes + pRootNew = Ivy_GraphToNetworkSeq( p, pGraph ); + Ivy_ObjReplace( p, pRoot, pRootNew, 1, 0, 0 ); + // compare the gains + nNodesNew = Ivy_ManNodeNum(p); + assert( nGain <= nNodesOld - nNodesNew ); + // propagate the buffer + Ivy_ManPropagateBuffers( p, 0 ); +} + + + + + + + + + +/**Function************************************************************* + + Synopsis [Computes the truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Ivy_CutGetTruth_rec( Ivy_Man_t * p, int Leaf, int * pNums, int nNums ) +{ + static unsigned uMasks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; + unsigned uTruth0, uTruth1; + Ivy_Obj_t * pObj; + int i; + for ( i = 0; i < nNums; i++ ) + if ( Leaf == pNums[i] ) + return uMasks[i]; + pObj = Ivy_ManObj( p, Ivy_LeafId(Leaf) ); + if ( Ivy_ObjIsLatch(pObj) ) + { + assert( !Ivy_ObjFaninC0(pObj) ); + Leaf = Ivy_LeafCreate( Ivy_ObjFaninId0(pObj), Ivy_LeafLat(Leaf) + 1 ); + return Ivy_CutGetTruth_rec( p, Leaf, pNums, nNums ); + } + assert( Ivy_ObjIsNode(pObj) || Ivy_ObjIsBuf(pObj) ); + Leaf = Ivy_LeafCreate( Ivy_ObjFaninId0(pObj), Ivy_LeafLat(Leaf) ); + uTruth0 = Ivy_CutGetTruth_rec( p, Leaf, pNums, nNums ); + if ( Ivy_ObjFaninC0(pObj) ) + uTruth0 = ~uTruth0; + if ( Ivy_ObjIsBuf(pObj) ) + return uTruth0; + Leaf = Ivy_LeafCreate( Ivy_ObjFaninId1(pObj), Ivy_LeafLat(Leaf) ); + uTruth1 = Ivy_CutGetTruth_rec( p, Leaf, pNums, nNums ); + if ( Ivy_ObjFaninC1(pObj) ) + uTruth1 = ~uTruth1; + return uTruth0 & uTruth1; +} + + +/**Function************************************************************* + + Synopsis [Computes the truth table.] + Description [] + + SideEffects [] + SeeAlso [] + +***********************************************************************/ +unsigned Ivy_CutGetTruth( Ivy_Man_t * p, Ivy_Obj_t * pObj, int * pNums, int nNums ) +{ + assert( Ivy_ObjIsNode(pObj) ); + assert( nNums < 6 ); + return Ivy_CutGetTruth_rec( p, Ivy_LeafCreate(pObj->Id, 0), pNums, nNums ); +} @@ -50,6 +592,28 @@ static inline int Ivy_CutHashValue( int NodeId ) { return 1 << (NodeId % 31); } /**Function************************************************************* + Synopsis [Returns 1 if the cut can be constructed; 0 otherwise.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Ivy_CutPrescreen( Ivy_Cut_t * pCut, int Id0, int Id1 ) +{ + int i; + if ( pCut->nSize < pCut->nSizeMax ) + return 1; + for ( i = 0; i < pCut->nSize; i++ ) + if ( pCut->pArray[i] == Id0 || pCut->pArray[i] == Id1 ) + return 1; + return 0; +} + +/**Function************************************************************* + Synopsis [Derives new cut.] Description [] @@ -59,7 +623,7 @@ static inline int Ivy_CutHashValue( int NodeId ) { return 1 << (NodeId % 31); } SeeAlso [] ***********************************************************************/ -static inline int Ivy_CutDeriveNew( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int IdOld, int IdNew0, int IdNew1 ) +static inline int Ivy_CutDeriveNew2( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int IdOld, int IdNew0, int IdNew1 ) { unsigned uHash = 0; int i, k; @@ -126,6 +690,130 @@ static inline int Ivy_CutDeriveNew( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int I /**Function************************************************************* + Synopsis [Derives new cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Ivy_CutDeriveNew( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int IdOld, int IdNew0, int IdNew1 ) +{ + unsigned uHash = 0; + int i, k; + assert( pCut->nSize > 0 ); + assert( IdNew0 < IdNew1 ); + for ( i = k = 0; i < pCut->nSize; i++ ) + { + if ( pCut->pArray[i] == IdOld ) + continue; + if ( IdNew0 <= pCut->pArray[i] ) + { + if ( IdNew0 < pCut->pArray[i] ) + { + pCutNew->pArray[ k++ ] = IdNew0; + uHash |= Ivy_CutHashValue( IdNew0 ); + } + IdNew0 = 0x7FFFFFFF; + } + if ( IdNew1 <= pCut->pArray[i] ) + { + if ( IdNew1 < pCut->pArray[i] ) + { + pCutNew->pArray[ k++ ] = IdNew1; + uHash |= Ivy_CutHashValue( IdNew1 ); + } + IdNew1 = 0x7FFFFFFF; + } + pCutNew->pArray[ k++ ] = pCut->pArray[i]; + uHash |= Ivy_CutHashValue( pCut->pArray[i] ); + } + if ( IdNew0 < 0x7FFFFFFF ) + { + pCutNew->pArray[ k++ ] = IdNew0; + uHash |= Ivy_CutHashValue( IdNew0 ); + } + if ( IdNew1 < 0x7FFFFFFF ) + { + pCutNew->pArray[ k++ ] = IdNew1; + uHash |= Ivy_CutHashValue( IdNew1 ); + } + pCutNew->nSize = k; + pCutNew->uHash = uHash; + assert( pCutNew->nSize <= pCut->nSizeMax ); +// for ( i = 1; i < pCutNew->nSize; i++ ) +// assert( pCutNew->pArray[i-1] < pCutNew->pArray[i] ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Find the hash value of the cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline unsigned Ivy_NodeCutHash( Ivy_Cut_t * pCut ) +{ + int i; + pCut->uHash = 0; + for ( i = 0; i < pCut->nSize; i++ ) + pCut->uHash |= (1 << (pCut->pArray[i] % 31)); + return pCut->uHash; +} + +/**Function************************************************************* + + Synopsis [Derives new cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Ivy_CutDeriveNew3( Ivy_Cut_t * pCut, Ivy_Cut_t * pCutNew, int IdOld, int IdNew0, int IdNew1 ) +{ + int i, k; + assert( pCut->nSize > 0 ); + assert( IdNew0 < IdNew1 ); + for ( i = k = 0; i < pCut->nSize; i++ ) + { + if ( pCut->pArray[i] == IdOld ) + continue; + if ( IdNew0 <= pCut->pArray[i] ) + { + if ( IdNew0 < pCut->pArray[i] ) + pCutNew->pArray[ k++ ] = IdNew0; + IdNew0 = 0x7FFFFFFF; + } + if ( IdNew1 <= pCut->pArray[i] ) + { + if ( IdNew1 < pCut->pArray[i] ) + pCutNew->pArray[ k++ ] = IdNew1; + IdNew1 = 0x7FFFFFFF; + } + pCutNew->pArray[ k++ ] = pCut->pArray[i]; + } + if ( IdNew0 < 0x7FFFFFFF ) + pCutNew->pArray[ k++ ] = IdNew0; + if ( IdNew1 < 0x7FFFFFFF ) + pCutNew->pArray[ k++ ] = IdNew1; + pCutNew->nSize = k; + assert( pCutNew->nSize <= pCut->nSizeMax ); + Ivy_NodeCutHash( pCutNew ); + return 1; +} + +/**Function************************************************************* + Synopsis [Returns 1 if pDom is contained in pCut.] Description [] @@ -295,9 +983,12 @@ void Ivy_CutPrintForNodes( Ivy_Store_t * pCutStore ) ***********************************************************************/ static inline int Ivy_CutReadLeaf( Ivy_Obj_t * pFanin ) { + int iLeaf; assert( !Ivy_IsComplement(pFanin) ); if ( !Ivy_ObjIsLatch(pFanin) ) return Ivy_LeafCreate( pFanin->Id, 0 ); + iLeaf = Ivy_CutReadLeaf( Ivy_ObjFanin0(pFanin) ); + assert( Ivy_LeafLat(iLeaf) < IVY_LEAF_MASK ); return 1 + Ivy_CutReadLeaf( Ivy_ObjFanin0(pFanin) ); } @@ -345,13 +1036,20 @@ Ivy_Store_t * Ivy_CutComputeForNode( Ivy_Man_t * p, Ivy_Obj_t * pObj, int nLeave for ( k = 0; k < pCut->nSize; k++ ) { pLeaf = Ivy_ManObj( p, Ivy_LeafId(pCut->pArray[k]) ); - if ( Ivy_ObjIsCi(pLeaf) ) + if ( Ivy_ObjIsCi(pLeaf) || Ivy_ObjIsConst1(pLeaf) ) continue; assert( Ivy_ObjIsNode(pLeaf) ); nLats = Ivy_LeafLat(pCut->pArray[k]); + // get the fanins fanins - iLeaf0 = nLats + Ivy_CutReadLeaf( Ivy_ObjFanin0(pLeaf) ); - iLeaf1 = nLats + Ivy_CutReadLeaf( Ivy_ObjFanin1(pLeaf) ); + iLeaf0 = Ivy_CutReadLeaf( Ivy_ObjFanin0(pLeaf) ); + iLeaf1 = Ivy_CutReadLeaf( Ivy_ObjFanin1(pLeaf) ); + assert( nLats + Ivy_LeafLat(iLeaf0) < IVY_LEAF_MASK && nLats + Ivy_LeafLat(iLeaf1) < IVY_LEAF_MASK ); + iLeaf0 = nLats + iLeaf0; + iLeaf1 = nLats + iLeaf1; + if ( !Ivy_CutPrescreen( pCut, iLeaf0, iLeaf1 ) ) + continue; + // the given cut exist if ( iLeaf0 > iLeaf1 ) Temp = iLeaf0, iLeaf0 = iLeaf1, iLeaf1 = Temp; // create the new cut diff --git a/src/temp/ivy/ivyTable.c b/src/temp/ivy/ivyTable.c index f2617699..fe9c3570 100644 --- a/src/temp/ivy/ivyTable.c +++ b/src/temp/ivy/ivyTable.c @@ -74,8 +74,8 @@ Ivy_Obj_t * Ivy_TableLookup( Ivy_Man_t * p, Ivy_Obj_t * pObj ) return NULL; assert( Ivy_ObjIsLatch(pObj) || Ivy_ObjFaninId0(pObj) > 0 ); assert( Ivy_ObjFaninId1(pObj) == 0 || Ivy_ObjFaninId0(pObj) < Ivy_ObjFaninId1(pObj) ); -// if ( Ivy_ObjFanin0(pObj)->nRefs == 0 || (!Ivy_ObjIsLatch(pObj) && Ivy_ObjFanin1(pObj)->nRefs == 0) ) -// return NULL; + if ( Ivy_ObjFanin0(pObj)->nRefs == 0 || (Ivy_ObjChild1(pObj) && Ivy_ObjFanin1(pObj)->nRefs == 0) ) + return NULL; for ( i = Ivy_Hash(pObj, p->nTableSize); p->pTable[i]; i = (i+1) % p->nTableSize ) { pEntry = Ivy_ManObj( p, p->pTable[i] ); diff --git a/src/temp/ivy/ivyUtil.c b/src/temp/ivy/ivyUtil.c index 3b77bf41..77a55a39 100644 --- a/src/temp/ivy/ivyUtil.c +++ b/src/temp/ivy/ivyUtil.c @@ -265,7 +265,7 @@ int Ivy_ManLevels( Ivy_Man_t * p ) ***********************************************************************/ int Ivy_ManResetLevels_rec( Ivy_Obj_t * pObj ) { - if ( pObj->Level || Ivy_ObjIsCi(pObj) ) + if ( pObj->Level || Ivy_ObjIsCi(pObj) || Ivy_ObjIsConst1(pObj) ) return pObj->Level; if ( Ivy_ObjIsBuf(pObj) ) return pObj->Level = Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) ); @@ -292,12 +292,81 @@ void Ivy_ManResetLevels( Ivy_Man_t * p ) int i; Ivy_ManForEachObj( p, pObj, i ) pObj->Level = 0; - Ivy_ManForEachPo( p, pObj, i ) + Ivy_ManForEachCo( p, pObj, i ) Ivy_ManResetLevels_rec( Ivy_ObjFanin0(pObj) ); } /**Function************************************************************* + Synopsis [References/references the node and returns MFFC size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ObjRefDeref( Ivy_Man_t * p, Ivy_Obj_t * pNode, int fReference, int fLabel ) +{ + Ivy_Obj_t * pNode0, * pNode1; + int Counter; + // label visited nodes + if ( fLabel ) + Ivy_ObjSetTravIdCurrent( p, pNode ); + // skip the CI + if ( Ivy_ObjIsPi(pNode) ) + return 0; + assert( Ivy_ObjIsNode(pNode) || Ivy_ObjIsBuf(pNode) || Ivy_ObjIsLatch(pNode) ); + // process the internal node + pNode0 = Ivy_ObjFanin0(pNode); + pNode1 = Ivy_ObjFanin1(pNode); + Counter = Ivy_ObjIsNode(pNode); + if ( fReference ) + { + if ( pNode0->nRefs++ == 0 ) + Counter += Ivy_ObjRefDeref( p, pNode0, fReference, fLabel ); + if ( pNode1 && pNode1->nRefs++ == 0 ) + Counter += Ivy_ObjRefDeref( p, pNode1, fReference, fLabel ); + } + else + { + assert( pNode0->nRefs > 0 ); + assert( pNode1 == NULL || pNode1->nRefs > 0 ); + if ( --pNode0->nRefs == 0 ) + Counter += Ivy_ObjRefDeref( p, pNode0, fReference, fLabel ); + if ( pNode1 && --pNode1->nRefs == 0 ) + Counter += Ivy_ObjRefDeref( p, pNode1, fReference, fLabel ); + } + return Counter; +} + + +/**Function************************************************************* + + Synopsis [Labels MFFC with the current label.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ivy_ObjMffcLabel( Ivy_Man_t * p, Ivy_Obj_t * pNode ) +{ + int nConeSize1, nConeSize2; + assert( !Ivy_IsComplement( pNode ) ); + assert( Ivy_ObjIsNode( pNode ) ); + nConeSize1 = Ivy_ObjRefDeref( p, pNode, 0, 1 ); // dereference + nConeSize2 = Ivy_ObjRefDeref( p, pNode, 1, 0 ); // reference + assert( nConeSize1 == nConeSize2 ); + assert( nConeSize1 > 0 ); + return nConeSize1; +} + +/**Function************************************************************* + Synopsis [Recursively updates fanout levels.] Description [] diff --git a/src/temp/ivy/module.make b/src/temp/ivy/module.make index a8f6a824..e7ba865a 100644 --- a/src/temp/ivy/module.make +++ b/src/temp/ivy/module.make @@ -5,6 +5,7 @@ SRC += src/temp/ivy/ivyBalance.c \ src/temp/ivy/ivyDfs.c \ src/temp/ivy/ivyDsd.c \ src/temp/ivy/ivyFanout.c \ + src/temp/ivy/ivyIsop.c \ src/temp/ivy/ivyMan.c \ src/temp/ivy/ivyMem.c \ src/temp/ivy/ivyMulti.c \ |