diff options
Diffstat (limited to 'src/aig')
56 files changed, 2336 insertions, 363 deletions
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h index 3a617117..d5c2a4db 100644 --- a/src/aig/aig/aig.h +++ b/src/aig/aig/aig.h @@ -85,6 +85,7 @@ struct Aig_Obj_t_ // 8 words // the AIG manager struct Aig_Man_t_ { + char * pName; // the design name // AIG nodes Vec_Ptr_t * vPis; // the array of PIs Vec_Ptr_t * vPos; // the array of POs @@ -148,13 +149,16 @@ struct Aig_Man_t_ #define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)) #endif -static inline int Aig_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); } -static inline int Aig_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); } -static inline int Aig_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; } -static inline void Aig_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); } -static inline void Aig_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); } -static inline unsigned Aig_InfoMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); } -static inline unsigned Aig_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); } +static inline int Aig_Base2Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; } +static inline int Aig_Base10Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; } +static inline char * Aig_UtilStrsav( char * s ) { return s ? strcpy(ALLOC(char, strlen(s)+1), s) : NULL; } +static inline int Aig_BitWordNum( int nBits ) { return (nBits>>5) + ((nBits&31) > 0); } +static inline int Aig_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); } +static inline int Aig_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; } +static inline void Aig_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); } +static inline void Aig_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); } +static inline unsigned Aig_InfoMask( int nVar ) { return (~(unsigned)0) >> (32-nVar); } +static inline unsigned Aig_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); } static inline int Aig_WordCountOnes( unsigned uWord ) { uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555); @@ -178,7 +182,7 @@ static inline int Aig_ManLatchNum( Aig_Man_t * p ) { return p->nO static inline int Aig_ManNodeNum( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]+p->nObjs[AIG_OBJ_EXOR]; } static inline int Aig_ManGetCost( Aig_Man_t * p ) { return p->nObjs[AIG_OBJ_AND]+3*p->nObjs[AIG_OBJ_EXOR]; } static inline int Aig_ManObjNum( Aig_Man_t * p ) { return p->nCreated - p->nDeleted; } -static inline int Aig_ManObjIdMax( Aig_Man_t * p ) { return Vec_PtrSize(p->vObjs); } +static inline int Aig_ManObjNumMax( Aig_Man_t * p ) { return Vec_PtrSize(p->vObjs); } static inline int Aig_ManRegNum( Aig_Man_t * p ) { return p->nRegs; } static inline Aig_Obj_t * Aig_ManConst0( Aig_Man_t * p ) { return Aig_Not(p->pConst1); } @@ -200,8 +204,9 @@ static inline int Aig_ObjIsAnd( Aig_Obj_t * pObj ) { return pObj- static inline int Aig_ObjIsExor( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_EXOR; } static inline int Aig_ObjIsLatch( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_LATCH; } static inline int Aig_ObjIsNode( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR; } -static inline int Aig_ObjIsTerm( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_PI || pObj->Type == AIG_OBJ_PO || pObj->Type == AIG_OBJ_CONST1; } -static inline int Aig_ObjIsHash( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR || pObj->Type == AIG_OBJ_LATCH; } +static inline int Aig_ObjIsTerm( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_PI || pObj->Type == AIG_OBJ_PO || pObj->Type == AIG_OBJ_CONST1; } +static inline int Aig_ObjIsHash( Aig_Obj_t * pObj ) { return pObj->Type == AIG_OBJ_AND || pObj->Type == AIG_OBJ_EXOR || pObj->Type == AIG_OBJ_LATCH; } +static inline int Aig_ObjIsChoice( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquivs && p->pEquivs[pObj->Id] && pObj->nRefs > 0; } static inline int Aig_ObjIsMarkA( Aig_Obj_t * pObj ) { return pObj->fMarkA; } static inline void Aig_ObjSetMarkA( Aig_Obj_t * pObj ) { pObj->fMarkA = 1; } @@ -234,6 +239,7 @@ static inline int Aig_ObjLevel( Aig_Obj_t * pObj ) { return pObj- static inline int Aig_ObjLevelNew( Aig_Obj_t * pObj ) { return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; } static inline void Aig_ObjClean( Aig_Obj_t * pObj ) { memset( pObj, 0, sizeof(Aig_Obj_t) ); } static inline Aig_Obj_t * Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj ) { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); } +static inline Aig_Obj_t * Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj ) { return p->pEquivs? p->pEquivs[pObj->Id] : NULL; } static inline int Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin ) { if ( Aig_ObjFanin0(pObj) == pFanin ) return 0; @@ -362,6 +368,7 @@ extern Vec_Ptr_t * Aig_ManDfs( Aig_Man_t * p ); extern Vec_Ptr_t * Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes ); extern Vec_Ptr_t * Aig_ManDfsChoices( Aig_Man_t * p ); extern Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p ); +extern int Aig_ManLevelNum( Aig_Man_t * p ); extern int Aig_ManCountLevels( Aig_Man_t * p ); extern int Aig_DagSize( Aig_Obj_t * pObj ); extern int Aig_SupportSize( Aig_Man_t * p, Aig_Obj_t * pObj ); @@ -428,14 +435,15 @@ extern void Aig_ObjOrderAdvance( Aig_Man_t * p ); extern Vec_Ptr_t * Aig_ManSupports( Aig_Man_t * pMan ); extern Vec_Ptr_t * Aig_ManPartitionSmart( Aig_Man_t * p, int nPartSizeLimit, int fVerbose, Vec_Ptr_t ** pvPartSupps ); extern Vec_Ptr_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize ); +extern Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize ); /*=== aigRepr.c =========================================================*/ extern void Aig_ManReprStart( Aig_Man_t * p, int nIdMax ); extern void Aig_ManReprStop( Aig_Man_t * p ); extern void Aig_ObjCreateRepr( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 ); extern void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p ); -extern Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p ); +extern Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered ); extern Aig_Man_t * Aig_ManRehash( Aig_Man_t * p ); -extern void Aig_ManCreateChoices( Aig_Man_t * p ); +extern void Aig_ManMarkValidChoices( Aig_Man_t * p ); /*=== aigRet.c ========================================================*/ extern Aig_Man_t * Rtm_ManRetime( Aig_Man_t * p, int fForward, int nStepsMax, int fVerbose ); /*=== aigScl.c ==========================================================*/ diff --git a/src/aig/aig/aigCheck.c b/src/aig/aig/aigCheck.c index dc01f779..f4a6bf6b 100644 --- a/src/aig/aig/aigCheck.c +++ b/src/aig/aig/aigCheck.c @@ -1,5 +1,5 @@ /**CFile**************************************************************** - + FileName [aigCheck.c] SystemName [ABC: Logic synthesis and verification system.] diff --git a/src/aig/aig/aigDfs.c b/src/aig/aig/aigDfs.c index 86509322..9cfaf69c 100644 --- a/src/aig/aig/aigDfs.c +++ b/src/aig/aig/aigDfs.c @@ -243,6 +243,27 @@ Vec_Ptr_t * Aig_ManDfsReverse( Aig_Man_t * p ) SeeAlso [] ***********************************************************************/ +int Aig_ManLevelNum( Aig_Man_t * p ) +{ + Aig_Obj_t * pObj; + int i, LevelsMax; + LevelsMax = 0; + Aig_ManForEachPo( p, pObj, i ) + LevelsMax = AIG_MAX( LevelsMax, (int)Aig_ObjFanin0(pObj)->Level ); + return LevelsMax; +} + +/**Function************************************************************* + + Synopsis [Computes the max number of levels in the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Aig_ManCountLevels( Aig_Man_t * p ) { Vec_Ptr_t * vNodes; diff --git a/src/aig/aig/aigFanout.c b/src/aig/aig/aigFanout.c index 9aff0fd5..d0beb128 100644 --- a/src/aig/aig/aigFanout.c +++ b/src/aig/aig/aigFanout.c @@ -57,7 +57,7 @@ void Aig_ManFanoutStart( Aig_Man_t * p ) assert( Aig_ManBufNum(p) == 0 ); // allocate fanout datastructure assert( p->pFanData == NULL ); - p->nFansAlloc = 2 * Aig_ManObjIdMax(p); + p->nFansAlloc = 2 * Aig_ManObjNumMax(p); if ( p->nFansAlloc < (1<<12) ) p->nFansAlloc = (1<<12); p->pFanData = ALLOC( int, 5 * p->nFansAlloc ); diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c index 076cc420..30a7991a 100644 --- a/src/aig/aig/aigMan.c +++ b/src/aig/aig/aigMan.c @@ -87,7 +87,8 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p ) Aig_Obj_t * pObj; int i; // create the new manager - pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 ); + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); // create the PIs Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); Aig_ManForEachPi( p, pObj, i ) @@ -134,7 +135,8 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered ) Aig_Obj_t * pObj; int i; // create the new manager - pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 ); + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); pNew->nRegs = p->nRegs; pNew->nAsserts = p->nAsserts; // create the PIs @@ -187,7 +189,8 @@ Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * Aig_Obj_t * pObj; int i; // create the new manager - pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 ); + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); // create the PIs Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); @@ -240,6 +243,7 @@ void Aig_ManStop( Aig_Man_t * p ) if ( p->vBufs ) Vec_PtrFree( p->vBufs ); if ( p->vLevelR ) Vec_IntFree( p->vLevelR ); if ( p->vLevels ) Vec_VecFree( p->vLevels ); + FREE( p->pName ); FREE( p->pObjCopies ); FREE( p->pReprs ); FREE( p->pEquivs ); @@ -298,7 +302,7 @@ void Aig_ManPrintStats( Aig_Man_t * p ) // printf( "Cre = %6d. ", p->nCreated ); // printf( "Del = %6d. ", p->nDeleted ); // printf( "Lev = %3d. ", Aig_ManCountLevels(p) ); - printf( "Max = %7d. ", Aig_ManObjIdMax(p) ); + printf( "Max = %7d. ", Aig_ManObjNumMax(p) ); printf( "Lev = %3d. ", Aig_ManLevels(p) ); printf( "\n" ); } diff --git a/src/aig/aig/aigOrder.c b/src/aig/aig/aigOrder.c index 8aef67c8..62aeca6e 100644 --- a/src/aig/aig/aigOrder.c +++ b/src/aig/aig/aigOrder.c @@ -46,7 +46,7 @@ void Aig_ManOrderStart( Aig_Man_t * p ) assert( Aig_ManBufNum(p) == 0 ); // allocate order datastructure assert( p->pOrderData == NULL ); - p->nOrderAlloc = 2 * Aig_ManObjIdMax(p); + p->nOrderAlloc = 2 * Aig_ManObjNumMax(p); if ( p->nOrderAlloc < (1<<12) ) p->nOrderAlloc = (1<<12); p->pOrderData = ALLOC( unsigned, 2 * p->nOrderAlloc ); diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c index 08cf9975..4c879ee8 100644 --- a/src/aig/aig/aigPart.c +++ b/src/aig/aig/aigPart.c @@ -445,7 +445,7 @@ int Aig_ManPartitionSmartFindPart( Vec_Ptr_t * vPartSuppsAll, Vec_Ptr_t * vParts if ( Vec_IntSize(vPartSupp) < 100 ) Repulse = 1; else - Repulse = 1+Extra_Base2Log(Vec_IntSize(vPartSupp)-100); + Repulse = 1+Aig_Base2Log(Vec_IntSize(vPartSupp)-100); Value = Attract/Repulse; if ( ValueBest < Value ) { @@ -484,7 +484,7 @@ void Aig_ManPartitionPrint( Aig_Man_t * p, Vec_Ptr_t * vPartsAll, Vec_Ptr_t * vP break; } assert( Counter == Aig_ManPoNum(p) ); - printf( "\nTotal = %d. Outputs = %d.\n", Counter, Aig_ManPoNum(p) ); +// printf( "\nTotal = %d. Outputs = %d.\n", Counter, Aig_ManPoNum(p) ); } /**Function************************************************************* @@ -719,18 +719,22 @@ Vec_Ptr_t * Aig_ManPartitionNaive( Aig_Man_t * p, int nPartSize ) SeeAlso [] ***********************************************************************/ -Aig_Obj_t * Aig_ManDupPart_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj ) +Aig_Obj_t * Aig_ManDupPart_rec( Aig_Man_t * pNew, Aig_Man_t * pOld, Aig_Obj_t * pObj, Vec_Int_t * vSuppMap ) { assert( !Aig_IsComplement(pObj) ); - if ( Aig_ObjIsTravIdCurrent(p, pObj) ) + if ( Aig_ObjIsTravIdCurrent(pOld, pObj) ) return pObj->pData; + Aig_ObjSetTravIdCurrent(pOld, pObj); + if ( Aig_ObjIsPi(pObj) ) + { + assert( Vec_IntSize(vSuppMap) == Aig_ManPiNum(pNew) ); + Vec_IntPush( vSuppMap, (int)pObj->pNext ); + return pObj->pData = Aig_ObjCreatePi(pNew); + } assert( Aig_ObjIsNode(pObj) ); - Aig_ManDupPart_rec( pNew, p, Aig_ObjFanin0(pObj) ); - Aig_ManDupPart_rec( pNew, p, Aig_ObjFanin1(pObj) ); - pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); - assert( !Aig_ObjIsTravIdCurrent(p, pObj) ); // loop detection - Aig_ObjSetTravIdCurrent(p, pObj); - return pObj->pData; + Aig_ManDupPart_rec( pNew, pOld, Aig_ObjFanin0(pObj), vSuppMap ); + Aig_ManDupPart_rec( pNew, pOld, Aig_ObjFanin1(pObj), vSuppMap ); + return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ); } /**Function************************************************************* @@ -744,43 +748,60 @@ Aig_Obj_t * Aig_ManDupPart_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pOb SeeAlso [] ***********************************************************************/ -Vec_Ptr_t * Aig_ManDupPart( Aig_Man_t * pNew, Aig_Man_t * p, Vec_Int_t * vPart, Vec_Int_t * vPartSupp, int fInverse ) +Vec_Ptr_t * Aig_ManDupPart( Aig_Man_t * pNew, Aig_Man_t * pOld, Vec_Int_t * vPart, Vec_Int_t * vSuppMap, int fInverse ) { - Vec_Ptr_t * vOutputs; - Aig_Obj_t * pObj, * pObjNew; - int Entry, k; + Vec_Ptr_t * vOutsTotal; + Aig_Obj_t * pObj; + int Entry, i; // create the PIs - Aig_ManIncrementTravId( p ); - Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) ); - Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); + Aig_ManIncrementTravId( pOld ); + Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew); + Aig_ObjSetTravIdCurrent( pOld, Aig_ManConst1(pOld) ); if ( !fInverse ) { - Vec_IntForEachEntry( vPartSupp, Entry, k ) + Vec_IntForEachEntry( vSuppMap, Entry, i ) { - pObj = Aig_ManPi( p, Entry ); - pObj->pData = Aig_ManPi( pNew, k ); - Aig_ObjSetTravIdCurrent( p, pObj ); + pObj = Aig_ManPi( pOld, Entry ); + pObj->pData = Aig_ManPi( pNew, i ); + Aig_ObjSetTravIdCurrent( pOld, pObj ); } } else { - Vec_IntForEachEntry( vPartSupp, Entry, k ) + Vec_IntForEachEntry( vSuppMap, Entry, i ) { - pObj = Aig_ManPi( p, k ); + pObj = Aig_ManPi( pOld, i ); pObj->pData = Aig_ManPi( pNew, Entry ); - Aig_ObjSetTravIdCurrent( p, pObj ); + Aig_ObjSetTravIdCurrent( pOld, pObj ); } + vSuppMap = NULL; // should not be useful } // create the internal nodes - vOutputs = Vec_PtrAlloc( Vec_IntSize(vPart) ); - Vec_IntForEachEntry( vPart, Entry, k ) + vOutsTotal = Vec_PtrAlloc( Vec_IntSize(vPart) ); + if ( !fInverse ) { - pObj = Aig_ManPo( p, Entry ); - pObjNew = Aig_ManDupPart_rec( pNew, p, Aig_ObjFanin0(pObj) ); - pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) ); - Vec_PtrPush( vOutputs, pObjNew ); + Vec_IntForEachEntry( vPart, Entry, i ) + { + pObj = Aig_ManPo( pOld, Entry ); + Aig_ManDupPart_rec( pNew, pOld, Aig_ObjFanin0(pObj), vSuppMap ); + Vec_PtrPush( vOutsTotal, Aig_ObjChild0Copy(pObj) ); + } + } + else + { + Aig_ManForEachObj( pOld, pObj, i ) + { + if ( Aig_ObjIsPo(pObj) ) + { + Aig_ManDupPart_rec( pNew, pOld, Aig_ObjFanin0(pObj), vSuppMap ); + Vec_PtrPush( vOutsTotal, Aig_ObjChild0Copy(pObj) ); + } + else if ( Aig_ObjIsNode(pObj) && pObj->nRefs == 0 ) + Aig_ManDupPart_rec( pNew, pOld, pObj, vSuppMap ); + + } } - return vOutputs; + return vOutsTotal; } /**Function************************************************************* @@ -814,6 +835,7 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi vPartSupp = Vec_PtrEntry( vPartSupps, i ); // create the new miter pNew = Aig_ManStart( 1000 ); +// pNew->pName = Extra_UtilStrsav( p1->pName ); // create the PIs for ( k = 0; k < Vec_IntSize(vPartSupp); k++ ) Aig_ObjCreatePi( pNew ); @@ -822,6 +844,8 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi vNodes2 = Aig_ManDupPart( pNew, p2, vPart, vPartSupp, 0 ); // create the miter pMiter = Aig_MiterTwo( pNew, vNodes1, vNodes2 ); + Vec_PtrFree( vNodes1 ); + Vec_PtrFree( vNodes2 ); // create the output Aig_ObjCreatePo( pNew, pMiter ); // clean up @@ -847,90 +871,115 @@ Vec_Ptr_t * Aig_ManMiterPartitioned( Aig_Man_t * p1, Aig_Man_t * p2, int nPartSi ***********************************************************************/ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize ) { - Aig_Man_t * pChoice, * pNew, * pAig, * p; - Aig_Obj_t * pObj; - Vec_Ptr_t * vMiters, * vNodes; - Vec_Ptr_t * vParts, * vPartSupps; + extern int Cmd_CommandExecute( void * pAbc, char * sCommand ); + extern void * Abc_FrameGetGlobalFrame(); + extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax ); + + Vec_Ptr_t * vOutsTotal, * vOuts; + Aig_Man_t * pAigTotal, * pAigPart, * pAig; Vec_Int_t * vPart, * vPartSupp; + Vec_Ptr_t * vParts; + Aig_Obj_t * pObj; + void ** ppData; int i, k, m; - // partition the first AIG + // partition the first AIG in the array assert( Vec_PtrSize(vAigs) > 1 ); pAig = Vec_PtrEntry( vAigs, 0 ); - vParts = Aig_ManPartitionSmart( pAig, nPartSize, 0, &vPartSupps ); + vParts = Aig_ManPartitionSmart( pAig, nPartSize, 0, NULL ); - // derive the AIG partitions - vMiters = Vec_PtrAlloc( Vec_PtrSize(vParts) ); - for ( i = 0; i < Vec_PtrSize(vParts); i++ ) - { - // get partitions and their support - vPart = Vec_PtrEntry( vParts, i ); - vPartSupp = Vec_PtrEntry( vPartSupps, i ); - // create the new miter - pNew = Aig_ManStart( 1000 ); - // create the PIs - for ( k = 0; k < Vec_IntSize(vPartSupp); k++ ) - Aig_ObjCreatePi( pNew ); - // copy the components - Vec_PtrForEachEntry( vAigs, p, k ) - { - vNodes = Aig_ManDupPart( pNew, p, vPart, vPartSupp, 0 ); - Vec_PtrForEachEntry( vNodes, pObj, m ) - Aig_ObjCreatePo( pNew, pObj ); - Vec_PtrFree( vNodes ); - } - // add to the partitions - Vec_PtrPush( vMiters, pNew ); - } + // start the total fraiged AIG + pAigTotal = Aig_ManStartFrom( pAig ); + Aig_ManReprStart( pAigTotal, Vec_PtrSize(vAigs) * Aig_ManObjNumMax(pAig) ); + vOutsTotal = Vec_PtrStart( Aig_ManPoNum(pAig) ); - // perform choicing for each derived AIG - Vec_PtrForEachEntry( vMiters, pNew, i ) - { - extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig ); - pNew = Fra_FraigChoice( p = pNew ); - Vec_PtrWriteEntry( vMiters, i, pNew ); - Aig_ManStop( p ); - } + // set the PI numbers + Vec_PtrForEachEntry( vAigs, pAig, i ) + Aig_ManForEachPi( pAig, pObj, k ) + pObj->pNext = (Aig_Obj_t *)k; - // combine the resulting AIGs - pNew = Aig_ManStartFrom( pAig ); - Vec_PtrForEachEntry( vMiters, p, i ) + Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" ); + + // create the total fraiged AIG + vPartSupp = Vec_IntAlloc( 100 ); // maps part PI num into total PI num + Vec_PtrForEachEntry( vParts, vPart, i ) { - // get partitions and their support - vPart = Vec_PtrEntry( vParts, i ); - vPartSupp = Vec_PtrEntry( vPartSupps, i ); - // copy the component - vNodes = Aig_ManDupPart( pNew, p, vPart, vPartSupp, 1 ); - assert( Vec_PtrSize(vNodes) == Vec_PtrSize(vParts) * Vec_PtrSize(vAigs) ); - // create choice node - for ( k = 0; k < Vec_PtrSize(vParts); k++ ) + // derive the partition AIG + pAigPart = Aig_ManStart( 5000 ); +// pAigPart->pName = Extra_UtilStrsav( pAigPart->pName ); + Vec_IntClear( vPartSupp ); + Vec_PtrForEachEntry( vAigs, pAig, k ) { - for ( m = 0; m < Vec_PtrSize(vAigs); m++ ) + vOuts = Aig_ManDupPart( pAigPart, pAig, vPart, vPartSupp, 0 ); + if ( k == 0 ) { - pObj = Aig_ObjChild0( Vec_PtrEntry(vNodes, k * Vec_PtrSize(vAigs) + m) ); - break; + Vec_PtrForEachEntry( vOuts, pObj, m ) + Aig_ObjCreatePo( pAigPart, pObj ); } - Aig_ObjCreatePo( pNew, pObj ); + Vec_PtrFree( vOuts ); + } + // derive the total AIG from the partitioned AIG + vOuts = Aig_ManDupPart( pAigTotal, pAigPart, vPart, vPartSupp, 1 ); + // add to the outputs + Vec_PtrForEachEntry( vOuts, pObj, k ) + { + assert( Vec_PtrEntry( vOutsTotal, Vec_IntEntry(vPart,k) ) == NULL ); + Vec_PtrWriteEntry( vOutsTotal, Vec_IntEntry(vPart,k), pObj ); } - Vec_PtrFree( vNodes ); + Vec_PtrFree( vOuts ); + // store contents of pData pointers + ppData = ALLOC( void *, Aig_ManObjNumMax(pAigPart) ); + Aig_ManForEachObj( pAigPart, pObj, k ) + ppData[k] = pObj->pData; + // report the process + printf( "Fraiging part %4d (out of %4d) PI = %5d. PO = %5d. And = %6d. Lev = %4d.\r", + i+1, Vec_PtrSize(vParts), Aig_ManPiNum(pAigPart), Aig_ManPoNum(pAigPart), + Aig_ManNodeNum(pAigPart), Aig_ManLevelNum(pAigPart) ); + // compute equivalence classes (to be stored in pNew->pReprs) + pAig = Fra_FraigChoice( pAigPart, 1000 ); + Aig_ManStop( pAig ); + // reset the pData pointers + Aig_ManForEachObj( pAigPart, pObj, k ) + pObj->pData = ppData[k]; + free( ppData ); + // transfer representatives to the total AIG + if ( pAigPart->pReprs ) + Aig_ManTransferRepr( pAigTotal, pAigPart ); + Aig_ManStop( pAigPart ); } + printf( " \r" ); Vec_VecFree( (Vec_Vec_t *)vParts ); - Vec_VecFree( (Vec_Vec_t *)vPartSupps ); + Vec_IntFree( vPartSupp ); - // trasfer representatives - Aig_ManReprStart( pNew, Aig_ManObjIdMax(pNew)+1 ); - Vec_PtrForEachEntry( vMiters, p, i ) - { - Aig_ManTransferRepr( pNew, p ); - Aig_ManStop( p ); - } - Vec_PtrFree( vMiters ); + Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" ); + + // clear the PI numbers + Vec_PtrForEachEntry( vAigs, pAig, i ) + Aig_ManForEachPi( pAig, pObj, k ) + pObj->pNext = NULL; +/* + // collect the missing outputs (outputs whose driver is not a node) + pAig = Vec_PtrEntry( vAigs, 0 ); + Aig_ManConst1(pAig)->pData = Aig_ManConst1(pAigTotal); + Aig_ManForEachPi( pAig, pObj, i ) + pAig->pData = Aig_ManPi( pAigTotal, i ); + Aig_ManForEachPo( pAig, pObj, i ) + if ( !Aig_ObjIsNode(Aig_ObjFanin0(pObj)) ) + { + assert( Vec_PtrEntry( vOutsTotal, i ) == NULL ); + Vec_PtrWriteEntry( vOutsTotal, i, Aig_ObjChild0Copy(pObj) ); + } +*/ + // add the outputs in the same order + Vec_PtrForEachEntry( vOutsTotal, pObj, i ) + Aig_ObjCreatePo( pAigTotal, pObj ); + Vec_PtrFree( vOutsTotal ); // derive the result of choicing - pChoice = Aig_ManRehash( pNew ); - if ( pChoice != pNew ) - Aig_ManStop( pNew ); - return pChoice; + pAig = Aig_ManRehash( pAigTotal ); + // create the equivalent nodes lists + Aig_ManMarkValidChoices( pAig ); + return pAig; } diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c index cea3c438..787ede49 100644 --- a/src/aig/aig/aigRepr.c +++ b/src/aig/aig/aigRepr.c @@ -164,11 +164,13 @@ static inline void Aig_ObjClearRepr( Aig_Man_t * p, Aig_Obj_t * pNode ) SeeAlso [] ***********************************************************************/ -static inline Aig_Obj_t * Aig_ObjFindReprTrans( Aig_Man_t * p, Aig_Obj_t * pNode ) +static inline Aig_Obj_t * Aig_ObjFindReprTransitive( Aig_Man_t * p, Aig_Obj_t * pNode ) { - Aig_Obj_t * pPrev, * pRepr; - for ( pPrev = NULL, pRepr = Aig_ObjFindRepr(p, pNode); pRepr; pPrev = pRepr, pRepr = Aig_ObjFindRepr(p, pRepr) ); - return pPrev; + Aig_Obj_t * pNext, * pRepr; + if ( (pRepr = Aig_ObjFindRepr(p, pNode)) ) + while ( (pNext = Aig_ObjFindRepr(p, pRepr)) ) + pRepr = pNext; + return pRepr; } /**Function************************************************************* @@ -203,14 +205,22 @@ static inline Aig_Obj_t * Aig_ObjChild1Repr( Aig_Man_t * p, Aig_Obj_t * pObj ) { SeeAlso [] ***********************************************************************/ -void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * p ) +void Aig_ManTransferRepr( Aig_Man_t * pNew, Aig_Man_t * pOld ) { Aig_Obj_t * pObj, * pRepr; int k; assert( pNew->pReprs != NULL ); + // extend storage to fix pNew + if ( pNew->nReprsAlloc < Aig_ManObjNumMax(pNew) ) + { + int nReprsAllocNew = 2 * Aig_ManObjNumMax(pNew); + pNew->pReprs = REALLOC( Aig_Obj_t *, pNew->pReprs, nReprsAllocNew ); + memset( pNew->pReprs + pNew->nReprsAlloc, 0, sizeof(Aig_Obj_t *) * (nReprsAllocNew-pNew->nReprsAlloc) ); + pNew->nReprsAlloc = nReprsAllocNew; + } // go through the nodes which have representatives - Aig_ManForEachObj( p, pObj, k ) - if ( (pRepr = Aig_ObjFindRepr(p, pObj)) ) + Aig_ManForEachObj( pOld, pObj, k ) + if ( (pRepr = Aig_ObjFindRepr(pOld, pObj)) ) Aig_ObjSetRepr( pNew, Aig_Regular(pRepr->pData), Aig_Regular(pObj->pData) ); } @@ -251,16 +261,15 @@ Aig_Obj_t * Aig_ManDupRepr_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pOb SeeAlso [] ***********************************************************************/ -Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p ) +Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p, int fOrdered ) { - int fOrdered = 0; Aig_Man_t * pNew; Aig_Obj_t * pObj; int i; // start the HOP package - pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 ); + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); pNew->nRegs = p->nRegs; - Aig_ManReprStart( pNew, Aig_ManObjIdMax(p)+1 ); // map the const and primary inputs Aig_ManCleanData( p ); Aig_ManConst1(p)->pData = Aig_ManConst1(pNew); @@ -303,7 +312,7 @@ int Aig_ManRemapRepr( Aig_Man_t * p ) int i, nFanouts = 0; Aig_ManForEachNode( p, pObj, i ) { - pRepr = Aig_ObjFindReprTrans( p, pObj ); + pRepr = Aig_ObjFindReprTransitive( p, pObj ); if ( pRepr == NULL ) continue; assert( pRepr->Id < pObj->Id ); @@ -379,10 +388,14 @@ int Aig_ObjCheckTfi( Aig_Man_t * p, Aig_Obj_t * pNew, Aig_Obj_t * pOld ) Aig_Man_t * Aig_ManRehash( Aig_Man_t * p ) { Aig_Man_t * pTemp; + int i, nFanouts; assert( p->pReprs != NULL ); - while ( Aig_ManRemapRepr( p ) ) + for ( i = 0; nFanouts = Aig_ManRemapRepr( p ); i++ ) { - p = Aig_ManDupRepr( pTemp = p ); +// printf( "Iter = %3d. Fanouts = %6d. Nodes = %7d.\n", i+1, nFanouts, Aig_ManNodeNum(p) ); + p = Aig_ManDupRepr( pTemp = p, 1 ); + Aig_ManReprStart( p, Aig_ManObjNumMax(p) ); + Aig_ManTransferRepr( p, pTemp ); Aig_ManStop( pTemp ); } return p; @@ -390,7 +403,7 @@ Aig_Man_t * Aig_ManRehash( Aig_Man_t * p ) /**Function************************************************************* - Synopsis [Creates choices.] + Synopsis [Marks the nodes that are Creates choices.] Description [The input AIG is assumed to have representatives assigned.] @@ -399,15 +412,15 @@ Aig_Man_t * Aig_ManRehash( Aig_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Aig_ManCreateChoices( Aig_Man_t * p ) +void Aig_ManMarkValidChoices( Aig_Man_t * p ) { Aig_Obj_t * pObj, * pRepr; int i; assert( p->pReprs != NULL ); // create equivalent nodes in the manager assert( p->pEquivs == NULL ); - p->pEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjIdMax(p) + 1 ); - memset( p->pEquivs, 0, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(p) + 1) ); + p->pEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p) ); + memset( p->pEquivs, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p) ); // make the choice nodes Aig_ManForEachNode( p, pObj, i ) { diff --git a/src/aig/aig/aigRet.c b/src/aig/aig/aigRet.c index 38fcc719..3efe20f0 100644 --- a/src/aig/aig/aigRet.c +++ b/src/aig/aig/aigRet.c @@ -275,10 +275,12 @@ void Rtm_PrintEdge( Rtm_Man_t * p, Rtm_Edg_t * pEdge ) { unsigned LData = pEdge->LData; printf( "%d : ", pEdge->nLats ); +/* if ( pEdge->nLats > 10 ) Extra_PrintBinary( stdout, p->pExtra + pEdge->LData, 2*(pEdge->nLats+1) ); else Extra_PrintBinary( stdout, &LData, 2*(pEdge->nLats+1) ); +*/ printf( "\n" ); } @@ -804,7 +806,7 @@ Aig_Man_t * Rtm_ManToAig( Rtm_Man_t * pRtm ) pObjNew = Aig_ManPi( pNew, pLatches[2*pObjRtm->Id + k] + m ); pObjNew = Aig_NotCond( pObjNew, Val == RTM_VAL_ONE ); } - assert( Aig_Regular(pObjNew)->nRefs > 0 ); +// assert( Aig_Regular(pObjNew)->nRefs > 0 ); } free( pLatches ); pNew->nRegs = nLatches; @@ -947,6 +949,7 @@ clk = clock(); // get the new manager pNew = Rtm_ManToAig( pRtm ); + pNew->pName = Aig_UtilStrsav( p->pName ); Rtm_ManFree( pRtm ); // group the registers clk = clock(); diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c index f8989446..166377bf 100644 --- a/src/aig/aig/aigScl.c +++ b/src/aig/aig/aigScl.c @@ -46,7 +46,8 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap ) Aig_Obj_t * pObj, * pObjMapped; int i; // create the new manager - pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 ); + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); pNew->nRegs = p->nRegs; pNew->nAsserts = p->nAsserts; // create the PIs @@ -285,7 +286,7 @@ Vec_Ptr_t * Aig_ManReduceLachesOnce( Aig_Man_t * p ) Aig_ManForEachPiSeq( p, pObj, i ) Vec_PtrPush( vMap, pObj ); // create mapping of fanin nodes into the corresponding latch outputs - pMapping = ALLOC( int, 2 * (Aig_ManObjIdMax(p) + 1) ); + pMapping = ALLOC( int, 2 * Aig_ManObjNumMax(p) ); Aig_ManForEachLiLoSeq( p, pObjLi, pObjLo, i ) { pFanin = Aig_ObjFanin0(pObjLi); @@ -358,6 +359,8 @@ Aig_Man_t * Aig_ManReduceLaches( Aig_Man_t * p, int fVerbose ) printf( "REnd = %5d. NEnd = %6d. ", Aig_ManRegNum(p), Aig_ManNodeNum(p) ); printf( "\n" ); } + if ( p->nRegs == 0 ) + break; } return p; } diff --git a/src/aig/aig/aigShow.c b/src/aig/aig/aigShow.c index c93c0c7a..96b0e37f 100644 --- a/src/aig/aig/aigShow.c +++ b/src/aig/aig/aigShow.c @@ -128,7 +128,7 @@ void Aig_WriteDotAig( Aig_Man_t * pMan, char * pFileName, int fHaig, Vec_Ptr_t * fprintf( pFile, "%s", "AIG structure visualized by ABC" ); fprintf( pFile, "\\n" ); fprintf( pFile, "Benchmark \\\"%s\\\". ", "aig" ); - fprintf( pFile, "Time was %s. ", Extra_TimeStamp() ); +// fprintf( pFile, "Time was %s. ", Extra_TimeStamp() ); fprintf( pFile, "\"\n" ); fprintf( pFile, " ];\n" ); fprintf( pFile, "}" ); diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c index ba359c09..94593d70 100644 --- a/src/aig/aig/aigTable.c +++ b/src/aig/aig/aigTable.c @@ -74,7 +74,7 @@ void Aig_TableResize( Aig_Man_t * p ) { Aig_Obj_t * pEntry, * pNext; Aig_Obj_t ** pTableOld, ** ppPlace; - int nTableSizeOld, Counter, nEntries, i, clk; + int nTableSizeOld, Counter, i, clk; clk = clock(); // save the old table pTableOld = p->pTable; @@ -97,10 +97,9 @@ clk = clock(); pEntry->pNext = NULL; Counter++; } - nEntries = Aig_ManNodeNum(p); - assert( Counter == nEntries ); - printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize ); - PRT( "Time", clock() - clk ); + assert( Counter == Aig_ManNodeNum(p) ); +// printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize ); +// PRT( "Time", clock() - clk ); // replace the table and the parameters free( pTableOld ); } diff --git a/src/aig/aig/aigTiming.c b/src/aig/aig/aigTiming.c index 14ee4f2c..a5da4513 100644 --- a/src/aig/aig/aigTiming.c +++ b/src/aig/aig/aigTiming.c @@ -147,7 +147,7 @@ void Aig_ManStartReverseLevels( Aig_Man_t * p, int nMaxLevelIncrease ) p->nLevelMax = Aig_ManLevels(p) + nMaxLevelIncrease; // start the reverse levels p->vLevelR = Vec_IntAlloc( 0 ); - Vec_IntFill( p->vLevelR, 1 + Aig_ManObjIdMax(p), 0 ); + Vec_IntFill( p->vLevelR, Aig_ManObjNumMax(p), 0 ); // compute levels in reverse topological order vNodes = Aig_ManDfsReverse( p ); Vec_PtrForEachEntry( vNodes, pObj, i ) diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c index 4d99e254..86cd02ce 100644 --- a/src/aig/aig/aigUtil.c +++ b/src/aig/aig/aigUtil.c @@ -679,7 +679,7 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName ) pObj->pData = (void *)Counter++; Vec_PtrForEachEntry( vNodes, pObj, i ) pObj->pData = (void *)Counter++; - nDigits = Extra_Base10Log( Counter ); + nDigits = Aig_Base10Log( Counter ); // write the file pFile = fopen( pFileName, "w" ); fprintf( pFile, "# BLIF file written by procedure Aig_ManDumpBlif() in ABC\n" ); diff --git a/src/aig/bar/bar.c b/src/aig/bar/bar.c new file mode 100644 index 00000000..8c215b48 --- /dev/null +++ b/src/aig/bar/bar.c @@ -0,0 +1,177 @@ +/**CFile**************************************************************** + + FileName [bar.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [extra] + + Synopsis [Progress bar.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: bar.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include "bar.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +struct Bar_Progress_t_ +{ + int nItemsNext; // the number of items for the next update of the progress bar + int nItemsTotal; // the total number of items + int posTotal; // the total number of positions + int posCur; // the current position + FILE * pFile; // the output stream +}; + +static void Bar_ProgressShow( Bar_Progress_t * p, char * pString ); +static void Bar_ProgressClean( Bar_Progress_t * p ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Starts the progress bar.] + + Description [The first parameter is the output stream (pFile), where + the progress is printed. The current printing position should be the + first one on the given line. The second parameters is the total + number of items that correspond to 100% position of the progress bar.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Bar_Progress_t * Bar_ProgressStart( FILE * pFile, int nItemsTotal ) +{ + Bar_Progress_t * p; +// extern int Abc_FrameShowProgress( void * p ); +// extern void * Abc_FrameGetGlobalFrame(); +// if ( !Abc_FrameShowProgress(Abc_FrameGetGlobalFrame()) ) return NULL; + p = (Bar_Progress_t *) malloc(sizeof(Bar_Progress_t)); + memset( p, 0, sizeof(Bar_Progress_t) ); + p->pFile = pFile; + p->nItemsTotal = nItemsTotal; + p->posTotal = 78; + p->posCur = 1; + p->nItemsNext = (int)((7.0+p->posCur)*p->nItemsTotal/p->posTotal); + Bar_ProgressShow( p, NULL ); + return p; +} + +/**Function************************************************************* + + Synopsis [Updates the progress bar.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bar_ProgressUpdate_int( Bar_Progress_t * p, int nItemsCur, char * pString ) +{ + if ( p == NULL ) return; + if ( nItemsCur < p->nItemsNext ) + return; + if ( nItemsCur >= p->nItemsTotal ) + { + p->posCur = 78; + p->nItemsNext = 0x7FFFFFFF; + } + else + { + p->posCur += 7; + p->nItemsNext = (int)((7.0+p->posCur)*p->nItemsTotal/p->posTotal); + } + Bar_ProgressShow( p, pString ); +} + + +/**Function************************************************************* + + Synopsis [Stops the progress bar.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bar_ProgressStop( Bar_Progress_t * p ) +{ + if ( p == NULL ) return; + Bar_ProgressClean( p ); + free( p ); +} + +/**Function************************************************************* + + Synopsis [Prints the progress bar of the given size.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bar_ProgressShow( Bar_Progress_t * p, char * pString ) +{ + int i; + if ( p == NULL ) return; + if ( pString ) + fprintf( p->pFile, "%s ", pString ); + for ( i = (pString? strlen(pString) + 1 : 0); i < p->posCur; i++ ) + fprintf( p->pFile, "-" ); + if ( i == p->posCur ) + fprintf( p->pFile, ">" ); + for ( i++ ; i <= p->posTotal; i++ ) + fprintf( p->pFile, " " ); + fprintf( p->pFile, "\r" ); + fflush( stdout ); +} + +/**Function************************************************************* + + Synopsis [Cleans the progress bar before quitting.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bar_ProgressClean( Bar_Progress_t * p ) +{ + int i; + if ( p == NULL ) return; + for ( i = 0; i <= p->posTotal; i++ ) + fprintf( p->pFile, " " ); + fprintf( p->pFile, "\r" ); + fflush( stdout ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/bar/bar.h b/src/aig/bar/bar.h new file mode 100644 index 00000000..814fbe6f --- /dev/null +++ b/src/aig/bar/bar.h @@ -0,0 +1,74 @@ +/**CFile**************************************************************** + + FileName [bar.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Progress bar.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: bar.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __BAR_H__ +#define __BAR_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +#ifdef _WIN32 +#define inline __inline // compatible with MS VS 6.0 +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +#define BAR_PROGRESS_USE 1 + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Bar_Progress_t_ Bar_Progress_t; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== bar.c ==========================================================*/ +extern Bar_Progress_t * Bar_ProgressStart( FILE * pFile, int nItemsTotal ); +extern void Bar_ProgressStop( Bar_Progress_t * p ); +extern void Bar_ProgressUpdate_int( Bar_Progress_t * p, int nItemsCur, char * pString ); + +static inline void Bar_ProgressUpdate( Bar_Progress_t * p, int nItemsCur, char * pString ) { + if ( BAR_PROGRESS_USE && p && (nItemsCur < *((int*)p)) ) return; Bar_ProgressUpdate_int(p, nItemsCur, pString); } + + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/bar/module.make b/src/aig/bar/module.make new file mode 100644 index 00000000..26161ba1 --- /dev/null +++ b/src/aig/bar/module.make @@ -0,0 +1 @@ +SRC += src/aig/bar/bar.c diff --git a/src/aig/cnf/cnfMap.c b/src/aig/cnf/cnfMap.c index ad728412..d966df15 100644 --- a/src/aig/cnf/cnfMap.c +++ b/src/aig/cnf/cnfMap.c @@ -100,8 +100,8 @@ void Cnf_DeriveMapping( Cnf_Man_t * p ) Dar_Cut_t * pCut, * pCutBest; int i, k, AreaFlow, * pAreaFlows; // allocate area flows - pAreaFlows = ALLOC( int, Aig_ManObjIdMax(p->pManAig) + 1 ); - memset( pAreaFlows, 0, sizeof(int) * (Aig_ManObjIdMax(p->pManAig) + 1) ); + pAreaFlows = ALLOC( int, Aig_ManObjNumMax(p->pManAig) ); + memset( pAreaFlows, 0, sizeof(int) * Aig_ManObjNumMax(p->pManAig) ); // visit the nodes in the topological order and update their best cuts vSuper = Vec_PtrAlloc( 100 ); Aig_ManForEachNode( p->pManAig, pObj, i ) diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c index 6faa08d2..45a3efad 100644 --- a/src/aig/cnf/cnfWrite.c +++ b/src/aig/cnf/cnfWrite.c @@ -214,8 +214,8 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals; // create room for variable numbers - pCnf->pVarNums = ALLOC( int, 1+Aig_ManObjIdMax(p->pManAig) ); - memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Aig_ManObjIdMax(p->pManAig)) ); + pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(p->pManAig) ); + memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p->pManAig) ); // assign variables to the last (nOutputs) POs Number = 1; if ( nOutputs ) @@ -246,7 +246,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) for ( k = 0; k < (int)pCut->nFanins; k++ ) { pVars[k] = pCnf->pVarNums[ pCut->pFanins[k] ]; - assert( pVars[k] <= Aig_ManObjIdMax(p->pManAig) ); + assert( pVars[k] <= Aig_ManObjNumMax(p->pManAig) ); } // positive polarity of the cut @@ -285,7 +285,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs ) // write the constant literal OutVar = pCnf->pVarNums[ Aig_ManConst1(p->pManAig)->Id ]; - assert( OutVar <= Aig_ManObjIdMax(p->pManAig) ); + assert( OutVar <= Aig_ManObjNumMax(p->pManAig) ); *pClas++ = pLits; *pLits++ = 2 * OutVar; @@ -353,8 +353,8 @@ Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs ) pCnf->pClauses[nClauses] = pCnf->pClauses[0] + nLiterals; // create room for variable numbers - pCnf->pVarNums = ALLOC( int, 1+Aig_ManObjIdMax(p) ); - memset( pCnf->pVarNums, 0xff, sizeof(int) * (1+Aig_ManObjIdMax(p)) ); + pCnf->pVarNums = ALLOC( int, Aig_ManObjNumMax(p) ); + memset( pCnf->pVarNums, 0xff, sizeof(int) * Aig_ManObjNumMax(p) ); // assign variables to the last (nOutputs) POs Number = 1; if ( nOutputs ) @@ -403,7 +403,7 @@ Cnf_Dat_t * Cnf_DeriveSimple( Aig_Man_t * p, int nOutputs ) // write the constant literal OutVar = pCnf->pVarNums[ Aig_ManConst1(p)->Id ]; - assert( OutVar <= Aig_ManObjIdMax(p) ); + assert( OutVar <= Aig_ManObjNumMax(p) ); *pClas++ = pLits; *pLits++ = 2 * OutVar; diff --git a/src/aig/csw/cswMan.c b/src/aig/csw/cswMan.c index 2af1a844..c3061dee 100644 --- a/src/aig/csw/cswMan.c +++ b/src/aig/csw/cswMan.c @@ -57,11 +57,11 @@ Csw_Man_t * Csw_ManStart( Aig_Man_t * pMan, int nCutsMax, int nLeafMax, int fVer p->pManRes = Aig_ManStartFrom( pMan ); assert( Aig_ManPiNum(p->pManAig) == Aig_ManPiNum(p->pManRes) ); // allocate room for cuts and equivalent nodes - p->pnRefs = ALLOC( int, Aig_ManObjIdMax(pMan) + 1 ); - p->pEquiv = ALLOC( Aig_Obj_t *, Aig_ManObjIdMax(pMan) + 1 ); - p->pCuts = ALLOC( Csw_Cut_t *, Aig_ManObjIdMax(pMan) + 1 ); - memset( p->pCuts, 0, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(pMan) + 1) ); - memset( p->pnRefs, 0, sizeof(int) * (Aig_ManObjIdMax(pMan) + 1) ); + p->pnRefs = ALLOC( int, Aig_ManObjNumMax(pMan) ); + p->pEquiv = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pMan) ); + p->pCuts = ALLOC( Csw_Cut_t *, Aig_ManObjNumMax(pMan) ); + memset( p->pCuts, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pMan) ); + memset( p->pnRefs, 0, sizeof(int) * Aig_ManObjNumMax(pMan) ); // allocate memory manager p->nTruthWords = Aig_TruthWordNum(nLeafMax); p->nCutSize = sizeof(Csw_Cut_t) + sizeof(int) * nLeafMax + sizeof(unsigned) * p->nTruthWords; diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h index 923ffc12..1f25e767 100644 --- a/src/aig/dar/dar.h +++ b/src/aig/dar/dar.h @@ -86,8 +86,10 @@ extern void Dar_ManDefaultRefParams( Dar_RefPar_t * pPars ); extern int Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars ); /*=== darScript.c ========================================================*/ extern Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig ); -extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose ); extern Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose ); +extern Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose ); +extern Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose ); +extern Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose ); #ifdef __cplusplus } diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c index 9c0997b8..d4266103 100644 --- a/src/aig/dar/darBalance.c +++ b/src/aig/dar/darBalance.c @@ -53,7 +53,8 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel ) Vec_Vec_t * vStore; int i; // create the new manager - pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 ); + pNew = Aig_ManStart( Aig_ManObjNumMax(p) ); + pNew->pName = Aig_UtilStrsav( p->pName ); pNew->nRegs = p->nRegs; pNew->nAsserts = p->nAsserts; // map the PI nodes diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c index dec9bff7..5e1c0fad 100644 --- a/src/aig/dar/darCore.c +++ b/src/aig/dar/darCore.c @@ -65,7 +65,7 @@ void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars ) int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars ) { Dar_Man_t * p; - ProgressBar * pProgress; + Bar_Progress_t * pProgress; Dar_Cut_t * pCut; Aig_Obj_t * pObj, * pObjNew; int i, k, nNodesOld, nNodeBefore, nNodeAfter, Required; @@ -88,15 +88,15 @@ int Dar_ManRewrite( Aig_Man_t * pAig, Dar_RwrPar_t * pPars ) p->nNodesInit = Aig_ManNodeNum(pAig); nNodesOld = Vec_PtrSize( pAig->vObjs ); - pProgress = Extra_ProgressBarStart( stdout, nNodesOld ); + pProgress = Bar_ProgressStart( stdout, nNodesOld ); Aig_ManForEachObj( pAig, pObj, i ) -// pProgress = Extra_ProgressBarStart( stdout, 100 ); +// pProgress = Bar_ProgressStart( stdout, 100 ); // Aig_ManOrderStart( pAig ); // Aig_ManForEachNodeInOrder( pAig, pObj ) { -// Extra_ProgressBarUpdate( pProgress, 100*pAig->nAndPrev/pAig->nAndTotal, NULL ); +// Bar_ProgressUpdate( pProgress, 100*pAig->nAndPrev/pAig->nAndTotal, NULL ); - Extra_ProgressBarUpdate( pProgress, i, NULL ); + Bar_ProgressUpdate( pProgress, i, NULL ); if ( !Aig_ObjIsNode(pObj) ) continue; if ( i > nNodesOld ) @@ -167,7 +167,7 @@ p->timeCuts += clock() - clk; p->timeTotal = clock() - clkStart; p->timeOther = p->timeTotal - p->timeCuts - p->timeEval; - Extra_ProgressBarStop( pProgress ); + Bar_ProgressStop( pProgress ); p->nCutMemUsed = Aig_MmFixedReadMemUsage(p->pMemCuts)/(1<<20); Dar_ManCutsFree( p ); // put the nodes into the DFS order and reassign their IDs diff --git a/src/aig/dar/darInt.h b/src/aig/dar/darInt.h index b14d5c30..97331416 100644 --- a/src/aig/dar/darInt.h +++ b/src/aig/dar/darInt.h @@ -38,6 +38,7 @@ extern "C" { #include "vec.h" #include "aig.h" #include "dar.h" +#include "bar.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -148,6 +149,9 @@ extern Aig_Obj_t * Dar_LibBuildBest( Dar_Man_t * p ); extern Dar_Man_t * Dar_ManStart( Aig_Man_t * pAig, Dar_RwrPar_t * pPars ); extern void Dar_ManStop( Dar_Man_t * p ); extern void Dar_ManPrintStats( Dar_Man_t * p ); +/*=== darPrec.c ============================================================*/ +extern char ** Dar_Permutations( int n ); +extern void Dar_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms, unsigned char ** puMap ); #ifdef __cplusplus } diff --git a/src/aig/dar/darLib.c b/src/aig/dar/darLib.c index e159f35a..14a47cee 100644 --- a/src/aig/dar/darLib.c +++ b/src/aig/dar/darLib.c @@ -129,8 +129,8 @@ Dar_Lib_t * Dar_LibAlloc( int nObjs ) p->pObjs = ALLOC( Dar_LibObj_t, nObjs ); memset( p->pObjs, 0, sizeof(Dar_LibObj_t) * nObjs ); // allocate canonical data - p->pPerms4 = Extra_Permutations( 4 ); - Extra_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap ); + p->pPerms4 = Dar_Permutations( 4 ); + Dar_Truth4VarNPN( &p->puCanons, &p->pPhases, &p->pPerms, &p->pMap ); // start the elementary objects p->iObj = 4; for ( i = 0; i < 4; i++ ) @@ -570,8 +570,8 @@ void Dar_LibStart() int clk = clock(); assert( s_DarLib == NULL ); s_DarLib = Dar_LibRead(); - printf( "The 4-input library started with %d nodes and %d subgraphs. ", s_DarLib->nObjs - 4, s_DarLib->nSubgrTotal ); - PRT( "Time", clock() - clk ); +// printf( "The 4-input library started with %d nodes and %d subgraphs. ", s_DarLib->nObjs - 4, s_DarLib->nSubgrTotal ); +// PRT( "Time", clock() - clk ); } /**Function************************************************************* diff --git a/src/aig/dar/darPrec.c b/src/aig/dar/darPrec.c new file mode 100644 index 00000000..c3e62389 --- /dev/null +++ b/src/aig/dar/darPrec.c @@ -0,0 +1,388 @@ +/**CFile**************************************************************** + + FileName [darPrec.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [DAG-aware AIG rewriting.] + + Synopsis [Truth table precomputation.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: darPrec.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "darInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + +/**Function************************************************************* + + Synopsis [Allocated one-memory-chunk array.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void ** Dar_ArrayAlloc( int nCols, int nRows, int Size ) +{ + char ** pRes; + char * pBuffer; + int i; + assert( nCols > 0 && nRows > 0 && Size > 0 ); + pBuffer = ALLOC( char, nCols * (sizeof(void *) + nRows * Size) ); + pRes = (char **)pBuffer; + pRes[0] = pBuffer + nCols * sizeof(void *); + for ( i = 1; i < nCols; i++ ) + pRes[i] = pRes[0] + i * nRows * Size; + return pRes; +} + +/**Function******************************************************************** + + Synopsis [Computes the factorial.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Dar_Factorial( int n ) +{ + int i, Res = 1; + for ( i = 1; i <= n; i++ ) + Res *= i; + return Res; +} + +/**Function******************************************************************** + + Synopsis [Fills in the array of permutations.] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Dar_Permutations_rec( char ** pRes, int nFact, int n, char Array[] ) +{ + char ** pNext; + int nFactNext; + int iTemp, iCur, iLast, k; + + if ( n == 1 ) + { + pRes[0][0] = Array[0]; + return; + } + + // get the next factorial + nFactNext = nFact / n; + // get the last entry + iLast = n - 1; + + for ( iCur = 0; iCur < n; iCur++ ) + { + // swap Cur and Last + iTemp = Array[iCur]; + Array[iCur] = Array[iLast]; + Array[iLast] = iTemp; + + // get the pointer to the current section + pNext = pRes + (n - 1 - iCur) * nFactNext; + + // set the last entry + for ( k = 0; k < nFactNext; k++ ) + pNext[k][iLast] = Array[iLast]; + + // call recursively for this part + Dar_Permutations_rec( pNext, nFactNext, n - 1, Array ); + + // swap them back + iTemp = Array[iCur]; + Array[iCur] = Array[iLast]; + Array[iLast] = iTemp; + } +} + +/**Function******************************************************************** + + Synopsis [Computes the set of all permutations.] + + Description [The number of permutations in the array is n!. The number of + entries in each permutation is n. Therefore, the resulting array is a + two-dimentional array of the size: n! x n. To free the resulting array, + call free() on the pointer returned by this procedure.] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +char ** Dar_Permutations( int n ) +{ + char Array[50]; + char ** pRes; + int nFact, i; + // allocate memory + nFact = Dar_Factorial( n ); + pRes = (char **)Dar_ArrayAlloc( nFact, n, sizeof(char) ); + // fill in the permutations + for ( i = 0; i < n; i++ ) + Array[i] = i; + Dar_Permutations_rec( pRes, nFact, n, Array ); + // print the permutations +/* + { + int i, k; + for ( i = 0; i < nFact; i++ ) + { + printf( "{" ); + for ( k = 0; k < n; k++ ) + printf( " %d", pRes[i][k] ); + printf( " }\n" ); + } + } +*/ + return pRes; +} + +/**Function************************************************************* + + Synopsis [Permutes the given vector of minterms.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_TruthPermute_int( int * pMints, int nMints, char * pPerm, int nVars, int * pMintsP ) +{ + int m, v; + // clean the storage for minterms + memset( pMintsP, 0, sizeof(int) * nMints ); + // go through minterms and add the variables + for ( m = 0; m < nMints; m++ ) + for ( v = 0; v < nVars; v++ ) + if ( pMints[m] & (1 << v) ) + pMintsP[m] |= (1 << pPerm[v]); +} + +/**Function************************************************************* + + Synopsis [Permutes the function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Dar_TruthPermute( unsigned Truth, char * pPerms, int nVars, int fReverse ) +{ + unsigned Result; + int * pMints; + int * pMintsP; + int nMints; + int i, m; + + assert( nVars < 6 ); + nMints = (1 << nVars); + pMints = ALLOC( int, nMints ); + pMintsP = ALLOC( int, nMints ); + for ( i = 0; i < nMints; i++ ) + pMints[i] = i; + + Dar_TruthPermute_int( pMints, nMints, pPerms, nVars, pMintsP ); + + Result = 0; + if ( fReverse ) + { + for ( m = 0; m < nMints; m++ ) + if ( Truth & (1 << pMintsP[m]) ) + Result |= (1 << m); + } + else + { + for ( m = 0; m < nMints; m++ ) + if ( Truth & (1 << m) ) + Result |= (1 << pMintsP[m]); + } + + free( pMints ); + free( pMintsP ); + + return Result; +} + +/**Function************************************************************* + + Synopsis [Changes the phase of the function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Dar_TruthPolarize( unsigned uTruth, int Polarity, int nVars ) +{ + // elementary truth tables + static unsigned Signs[5] = { + 0xAAAAAAAA, // 1010 1010 1010 1010 1010 1010 1010 1010 + 0xCCCCCCCC, // 1010 1010 1010 1010 1010 1010 1010 1010 + 0xF0F0F0F0, // 1111 0000 1111 0000 1111 0000 1111 0000 + 0xFF00FF00, // 1111 1111 0000 0000 1111 1111 0000 0000 + 0xFFFF0000 // 1111 1111 1111 1111 0000 0000 0000 0000 + }; + unsigned uTruthRes, uCof0, uCof1; + int nMints, Shift, v; + assert( nVars < 6 ); + nMints = (1 << nVars); + uTruthRes = uTruth; + for ( v = 0; v < nVars; v++ ) + if ( Polarity & (1 << v) ) + { + uCof0 = uTruth & ~Signs[v]; + uCof1 = uTruth & Signs[v]; + Shift = (1 << v); + uCof0 <<= Shift; + uCof1 >>= Shift; + uTruth = uCof0 | uCof1; + } + return uTruth; +} + +/**Function************************************************************* + + Synopsis [Computes NPN canonical forms for 4-variable functions.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_Truth4VarNPN( unsigned short ** puCanons, char ** puPhases, char ** puPerms, unsigned char ** puMap ) +{ + unsigned short * uCanons; + unsigned char * uMap; + unsigned uTruth, uPhase, uPerm; + char ** pPerms4, * uPhases, * uPerms; + int nFuncs, nClasses; + int i, k; + + nFuncs = (1 << 16); + uCanons = ALLOC( unsigned short, nFuncs ); + uPhases = ALLOC( char, nFuncs ); + uPerms = ALLOC( char, nFuncs ); + uMap = ALLOC( unsigned char, nFuncs ); + memset( uCanons, 0, sizeof(unsigned short) * nFuncs ); + memset( uPhases, 0, sizeof(char) * nFuncs ); + memset( uPerms, 0, sizeof(char) * nFuncs ); + memset( uMap, 0, sizeof(unsigned char) * nFuncs ); + pPerms4 = Dar_Permutations( 4 ); + + nClasses = 1; + nFuncs = (1 << 15); + for ( uTruth = 1; uTruth < (unsigned)nFuncs; uTruth++ ) + { + // skip already assigned + if ( uCanons[uTruth] ) + { + assert( uTruth > uCanons[uTruth] ); + uMap[~uTruth & 0xFFFF] = uMap[uTruth] = uMap[uCanons[uTruth]]; + continue; + } + uMap[uTruth] = nClasses++; + for ( i = 0; i < 16; i++ ) + { + uPhase = Dar_TruthPolarize( uTruth, i, 4 ); + for ( k = 0; k < 24; k++ ) + { + uPerm = Dar_TruthPermute( uPhase, pPerms4[k], 4, 0 ); + if ( uCanons[uPerm] == 0 ) + { + uCanons[uPerm] = uTruth; + uPhases[uPerm] = i; + uPerms[uPerm] = k; + + uPerm = ~uPerm & 0xFFFF; + uCanons[uPerm] = uTruth; + uPhases[uPerm] = i | 16; + uPerms[uPerm] = k; + } + else + assert( uCanons[uPerm] == uTruth ); + } + uPhase = Dar_TruthPolarize( ~uTruth & 0xFFFF, i, 4 ); + for ( k = 0; k < 24; k++ ) + { + uPerm = Dar_TruthPermute( uPhase, pPerms4[k], 4, 0 ); + if ( uCanons[uPerm] == 0 ) + { + uCanons[uPerm] = uTruth; + uPhases[uPerm] = i; + uPerms[uPerm] = k; + + uPerm = ~uPerm & 0xFFFF; + uCanons[uPerm] = uTruth; + uPhases[uPerm] = i | 16; + uPerms[uPerm] = k; + } + else + assert( uCanons[uPerm] == uTruth ); + } + } + } + uPhases[(1<<16)-1] = 16; + assert( nClasses == 222 ); + free( pPerms4 ); + if ( puCanons ) + *puCanons = uCanons; + else + free( uCanons ); + if ( puPhases ) + *puPhases = uPhases; + else + free( uPhases ); + if ( puPerms ) + *puPerms = uPerms; + else + free( uPerms ); + if ( puMap ) + *puMap = uMap; + else + free( uMap ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c index b304fe34..a5435862 100644 --- a/src/aig/dar/darRefact.c +++ b/src/aig/dar/darRefact.c @@ -309,7 +309,7 @@ Aig_Obj_t * Dar_RefactBuildGraph( Aig_Man_t * pAig, Vec_Ptr_t * vCut, Kit_Graph_ if ( Kit_GraphIsVar(pGraph) ) return Aig_NotCond( Kit_GraphVar(pGraph)->pFunc, Kit_GraphIsComplement(pGraph) ); // build the AIG nodes corresponding to the AND gates of the graph -//printf( "Building (current number %d):\n", Aig_ManObjIdMax(pAig) ); +//printf( "Building (current number %d):\n", Aig_ManObjNumMax(pAig) ); Kit_GraphForEachNode( pGraph, pNode, i ) { pAnd0 = Aig_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c index 2fe39860..9eb5e280 100644 --- a/src/aig/dar/darScript.c +++ b/src/aig/dar/darScript.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "darInt.h" +#include "ioa.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -63,8 +64,8 @@ Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig ) SeeAlso [] ***********************************************************************/ -Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose ) -//alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l" +Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose ) +//alias rwsat "st; rw -l; b -l; rw -l; rf -l" { Aig_Man_t * pTemp; @@ -74,18 +75,14 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, Dar_ManDefaultRwrParams( pParsRwr ); Dar_ManDefaultRefParams( pParsRef ); - pParsRwr->fUpdateLevel = fUpdateLevel; - pParsRef->fUpdateLevel = fUpdateLevel; + pParsRwr->fUpdateLevel = 0; + pParsRef->fUpdateLevel = 0; pParsRwr->fVerbose = fVerbose; pParsRef->fVerbose = fVerbose; - // balance - if ( fBalance ) - { -// pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); -// Aig_ManStop( pTemp ); - } + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); // rewrite Dar_ManRewrite( pAig, pParsRwr ); @@ -98,9 +95,9 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, Aig_ManStop( pTemp ); // balance -// if ( fBalance ) + if ( fBalance ) { - pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); + pAig = Dar_ManBalance( pTemp = pAig, 0 ); Aig_ManStop( pTemp ); } @@ -109,28 +106,54 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, pAig = Aig_ManDup( pTemp = pAig, 0 ); Aig_ManStop( pTemp ); - pParsRwr->fUseZeros = 1; - pParsRef->fUseZeros = 1; - - // rewrite - Dar_ManRewrite( pAig, pParsRwr ); - pAig = Aig_ManDup( pTemp = pAig, 0 ); - Aig_ManStop( pTemp ); + return pAig; +} + + +/**Function************************************************************* + + Synopsis [Reproduces script "compress".] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dar_ManCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose ) +//alias compress2 "b -l; rw -l; rwz -l; b -l; rwz -l; b -l" +{ + Aig_Man_t * pTemp; + + Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr; + Dar_RefPar_t ParsRef, * pParsRef = &ParsRef; + + Dar_ManDefaultRwrParams( pParsRwr ); + Dar_ManDefaultRefParams( pParsRef ); + + pParsRwr->fUpdateLevel = fUpdateLevel; + pParsRef->fUpdateLevel = fUpdateLevel; + + pParsRwr->fVerbose = fVerbose; + pParsRef->fVerbose = fVerbose; + + pAig = Aig_ManDup( pAig, 0 ); // balance if ( fBalance ) { - pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); - Aig_ManStop( pTemp ); +// pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); +// Aig_ManStop( pTemp ); } - // refactor - Dar_ManRefactor( pAig, pParsRef ); + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); pAig = Aig_ManDup( pTemp = pAig, 0 ); Aig_ManStop( pTemp ); - // rewrite - Dar_ManRewrite( pAig, pParsRwr ); + // refactor + Dar_ManRefactor( pAig, pParsRef ); pAig = Aig_ManDup( pTemp = pAig, 0 ); Aig_ManStop( pTemp ); @@ -140,6 +163,15 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); Aig_ManStop( pTemp ); } + + pParsRwr->fUseZeros = 1; + pParsRef->fUseZeros = 1; + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + return pAig; } @@ -149,13 +181,13 @@ Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, Description [] - SideEffects [This procedure does not tighten level during restructuring.] + SideEffects [] SeeAlso [] ***********************************************************************/ -Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose ) -//alias rwsat "st; rw -l; b -l; rw -l; rf -l" +Aig_Man_t * Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose ) +//alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l" { Aig_Man_t * pTemp; @@ -165,11 +197,20 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose ) Dar_ManDefaultRwrParams( pParsRwr ); Dar_ManDefaultRefParams( pParsRef ); - pParsRwr->fUpdateLevel = 0; - pParsRef->fUpdateLevel = 0; + pParsRwr->fUpdateLevel = fUpdateLevel; + pParsRef->fUpdateLevel = fUpdateLevel; pParsRwr->fVerbose = fVerbose; pParsRef->fVerbose = fVerbose; + + pAig = Aig_ManDup( pAig, 0 ); + + // balance + if ( fBalance ) + { +// pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); +// Aig_ManStop( pTemp ); + } // rewrite Dar_ManRewrite( pAig, pParsRwr ); @@ -182,20 +223,144 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose ) Aig_ManStop( pTemp ); // balance +// if ( fBalance ) + { + pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); + Aig_ManStop( pTemp ); + } + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + pParsRwr->fUseZeros = 1; + pParsRef->fUseZeros = 1; + + // rewrite + Dar_ManRewrite( pAig, pParsRwr ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + + // balance if ( fBalance ) { - pAig = Dar_ManBalance( pTemp = pAig, 0 ); + pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); Aig_ManStop( pTemp ); } + // refactor + Dar_ManRefactor( pAig, pParsRef ); + pAig = Aig_ManDup( pTemp = pAig, 0 ); + Aig_ManStop( pTemp ); + // rewrite Dar_ManRewrite( pAig, pParsRwr ); pAig = Aig_ManDup( pTemp = pAig, 0 ); Aig_ManStop( pTemp ); + // balance + if ( fBalance ) + { + pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel ); + Aig_ManStop( pTemp ); + } return pAig; } +/**Function************************************************************* + + Synopsis [Reproduces script "compress2".] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose ) +//alias resyn "b; rw; rwz; b; rwz; b" +//alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b" +{ + Vec_Ptr_t * vAigs; + vAigs = Vec_PtrAlloc( 3 ); + pAig = Aig_ManDup(pAig, 0); + Vec_PtrPush( vAigs, pAig ); + pAig = Dar_ManCompress (pAig, 0, fUpdateLevel, fVerbose); + Vec_PtrPush( vAigs, pAig ); + pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, fVerbose); + Vec_PtrPush( vAigs, pAig ); + return vAigs; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Dar_ManChoiceSynthesisExt() +{ + Vec_Ptr_t * vAigs; + Aig_Man_t * pMan; + vAigs = Vec_PtrAlloc( 3 ); + pMan = Ioa_ReadAiger( "i10_1.aig", 1 ); + Vec_PtrPush( vAigs, pMan ); + pMan = Ioa_ReadAiger( "i10_2.aig", 1 ); + Vec_PtrPush( vAigs, pMan ); + pMan = Ioa_ReadAiger( "i10_3.aig", 1 ); + Vec_PtrPush( vAigs, pMan ); + return vAigs; +} + +/**Function************************************************************* + + Synopsis [Reproduces script "compress2".] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Dar_ManChoice( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose ) +{ + Aig_Man_t * pMan, * pTemp; + Vec_Ptr_t * vAigs; + int i, clk; + +clk = clock(); +// vAigs = Dar_ManChoiceSynthesisExt(); + vAigs = Dar_ManChoiceSynthesis( pAig, fBalance, fUpdateLevel, fVerbose ); + + // swap the first and last network + // this should lead to the primary choice being "better" because of synthesis + pMan = Vec_PtrPop( vAigs ); + Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) ); + Vec_PtrWriteEntry( vAigs, 0, pMan ); + +if ( fVerbose ) +{ +PRT( "Synthesis time", clock() - clk ); +} +clk = clock(); + pMan = Aig_ManChoicePartitioned( vAigs, 300 ); + Vec_PtrForEachEntry( vAigs, pTemp, i ) + Aig_ManStop( pTemp ); + Vec_PtrFree( vAigs ); +if ( fVerbose ) +{ +PRT( "Choicing time ", clock() - clk ); +} + return pMan; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/dar/module.make b/src/aig/dar/module.make index 09b45171..0a1f7687 100644 --- a/src/aig/dar/module.make +++ b/src/aig/dar/module.make @@ -4,6 +4,7 @@ SRC += src/aig/dar/darBalance.c \ src/aig/dar/darData.c \ src/aig/dar/darLib.c \ src/aig/dar/darMan.c \ + src/aig/dar/darPrec.c \ src/aig/dar/darRefact.c \ src/aig/dar/darResub.c \ src/aig/dar/darScript.c \ diff --git a/src/aig/ec/module.make b/src/aig/ec/module.make deleted file mode 100644 index d6d908e7..00000000 --- a/src/aig/ec/module.make +++ /dev/null @@ -1 +0,0 @@ -SRC += diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h index 931e0930..cd6bdfd4 100644 --- a/src/aig/fra/fra.h +++ b/src/aig/fra/fra.h @@ -39,6 +39,7 @@ extern "C" { #include "aig.h" #include "dar.h" #include "satSolver.h" +#include "bar.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -126,6 +127,7 @@ struct Fra_Man_t_ // mapping AIG into FRAIG int nFramesAll; // the number of timeframes used Aig_Obj_t ** pMemFraig; // memory allocated for points to the fraig nodes + int nSizeAlloc; // allocated size of the arrays for timeframe nodes // equivalence classes Fra_Cla_t * pCla; // representation of (candidate) equivalent nodes // simulation info @@ -144,7 +146,7 @@ struct Fra_Man_t_ sint64 nInsLimitGlobal; // resource limit Vec_Ptr_t ** pMemFanins; // the arrays of fanins for some FRAIG nodes int * pMemSatNums; // the array of SAT numbers for some FRAIG nodes - int nSizeAlloc; // allocated size of the arrays + int nMemAlloc; // allocated size of the arrays for FRAIG varnums and fanins Vec_Ptr_t * vTimeouts; // the nodes, for which equivalence checking timed out // statistics int nSimRounds; @@ -240,7 +242,7 @@ extern void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pO extern void Fra_FraigSweep( Fra_Man_t * pManAig ); extern int Fra_FraigMiterStatus( Aig_Man_t * p ); extern Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars ); -extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig ); +extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax ); extern Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax ); /*=== fraImp.c ========================================================*/ extern Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr ); @@ -259,7 +261,7 @@ extern Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int n extern void Fra_ParamsDefault( Fra_Par_t * pParams ); extern void Fra_ParamsDefaultSeq( Fra_Par_t * pParams ); extern Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams ); -extern void Fra_ManClean( Fra_Man_t * p ); +extern void Fra_ManClean( Fra_Man_t * p, int nNodesMax ); extern Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p ); extern void Fra_ManFinalizeComb( Fra_Man_t * p ); extern void Fra_ManStop( Fra_Man_t * p ); diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c index 648d08c4..1df25c0a 100644 --- a/src/aig/fra/fraBmc.c +++ b/src/aig/fra/fraBmc.c @@ -187,8 +187,8 @@ Fra_Bmc_t * Fra_BmcStart( Aig_Man_t * pAig, int nPref, int nDepth ) p->nPref = nPref; p->nDepth = nDepth; p->nFramesAll = nPref + nDepth; - p->pObjToFrames = ALLOC( Aig_Obj_t *, p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) ); - memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) ); + p->pObjToFrames = ALLOC( Aig_Obj_t *, p->nFramesAll * Aig_ManObjNumMax(pAig) ); + memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * Aig_ManObjNumMax(pAig) ); return p; } @@ -231,7 +231,8 @@ Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p ) int i, k, f; // start the fraig package - pAigFrames = Aig_ManStart( (Aig_ManObjIdMax(p->pAig) + 1) * p->nFramesAll ); + pAigFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFramesAll ); + pAigFrames->pName = Aig_UtilStrsav( p->pAig->pName ); // create PI nodes for the frames for ( f = 0; f < p->nFramesAll; f++ ) Bmc_ObjSetFrames( Aig_ManConst1(p->pAig), f, Aig_ManConst1(pAigFrames) ); diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c index 3e3392c7..a03fa6e5 100644 --- a/src/aig/fra/fraClass.c +++ b/src/aig/fra/fraClass.c @@ -60,8 +60,8 @@ Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig ) p = ALLOC( Fra_Cla_t, 1 ); memset( p, 0, sizeof(Fra_Cla_t) ); p->pAig = pAig; - p->pMemRepr = ALLOC( Aig_Obj_t *, (Aig_ManObjIdMax(pAig) + 1) ); - memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(pAig) + 1) ); + p->pMemRepr = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) ); + memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAig) ); p->vClasses = Vec_PtrAlloc( 100 ); p->vClasses1 = Vec_PtrAlloc( 100 ); p->vClassesTemp = Vec_PtrAlloc( 100 ); @@ -112,8 +112,8 @@ void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed ) { Aig_Obj_t * pObj; int i; - Aig_ManReprStart( p->pAig, Aig_ManObjIdMax(p->pAig) + 1 ); - memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * (Aig_ManObjIdMax(p->pAig) + 1) ); + Aig_ManReprStart( p->pAig, Aig_ManObjNumMax(p->pAig) ); + memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) ); if ( Vec_PtrSize(p->vClasses1) == 0 && Vec_PtrSize(p->vClasses) == 0 ) { Aig_ManForEachObj( p->pAig, pObj, i ) @@ -277,7 +277,7 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr ) int i, k, nTableSize, nEntries, nNodes, iEntry; // allocate the hash table hashing simulation info into nodes - nTableSize = Aig_PrimeCudd( Aig_ManObjIdMax(p->pAig) + 1 ); + nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig) ); ppTable = ALLOC( Aig_Obj_t *, nTableSize ); ppNexts = ALLOC( Aig_Obj_t *, nTableSize ); memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize ); @@ -643,8 +643,8 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p ) // perform combinational simulation pComb = Fra_SmlSimulateComb( p->pAig, 32 ); // compute the weight of each node in the classes - pWeights = ALLOC( int, Aig_ManObjIdMax(p->pAig) + 1 ); - memset( pWeights, 0, sizeof(int) * (Aig_ManObjIdMax(p->pAig) + 1) ); + pWeights = ALLOC( int, Aig_ManObjNumMax(p->pAig) ); + memset( pWeights, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) ); Aig_ManForEachObj( p->pAig, pObj, i ) { pRepr = Fra_ClassObjRepr( pObj ); @@ -798,9 +798,10 @@ Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK ) assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) ); assert( nFramesK > 0 ); // start the fraig package - pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pAig) + 1) * nFramesAll ); + pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * nFramesAll ); + pManFraig->pName = Aig_UtilStrsav( p->pAig->pName ); // allocate place for the node mapping - ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjIdMax(p->pAig) + 1 ); + ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) ); Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) ); // create latches for the first frame Aig_ManForEachLoSeq( p->pAig, pObj, i ) diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c index 94beb61a..b390edbe 100644 --- a/src/aig/fra/fraCore.c +++ b/src/aig/fra/fraCore.c @@ -267,7 +267,7 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj ) ***********************************************************************/ void Fra_FraigSweep( Fra_Man_t * p ) { - ProgressBar * pProgress; + Bar_Progress_t * pProgress; Aig_Obj_t * pObj, * pObjNew; int i, k = 0, Pos = 0; // fraig latch outputs @@ -280,10 +280,10 @@ void Fra_FraigSweep( Fra_Man_t * p ) if ( p->pPars->fLatchCorr ) return; // fraig internal nodes - pProgress = Extra_ProgressBarStart( stdout, Aig_ManObjIdMax(p->pManAig) ); + pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pManAig) ); Aig_ManForEachNode( p->pManAig, pObj, i ) { - Extra_ProgressBarUpdate( pProgress, i, NULL ); + Bar_ProgressUpdate( pProgress, i, NULL ); // derive and remember the new fraig node pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj,p->pPars->nFramesK), Fra_ObjChild1Fra(pObj,p->pPars->nFramesK) ); Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjNew ); @@ -296,7 +296,7 @@ void Fra_FraigSweep( Fra_Man_t * p ) if ( p->pPars->fUseImps ) Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos ); } - Extra_ProgressBarStop( pProgress ); + Bar_ProgressStop( pProgress ); // try to prove the outputs of the miter p->nNodesMiter = Aig_ManNodeNum(p->pManFraig); // Fra_MiterStatus( p->pManFraig ); @@ -331,8 +331,8 @@ clk = clock(); p->pManFraig = Fra_ManPrepareComb( p ); p->pSml = Fra_SmlStart( pManAig, 0, 1, pPars->nSimWords ); Fra_SmlSimulate( p, 0 ); - if ( p->pPars->fChoicing ) - Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 ); +// if ( p->pPars->fChoicing ) +// Aig_ManReprStart( p->pManFraig, Aig_ManObjNumMax(p->pManAig) ); // collect initial states p->nLitsBeg = Fra_ClassesCountLits( p->pCla ); p->nNodesBeg = Aig_ManNodeNum(pManAig); @@ -346,10 +346,12 @@ clk = clock(); Fra_ManFinalizeComb( p ); if ( p->pPars->fChoicing ) { - int clk2 = clock(); +int clk2 = clock(); Fra_ClassesCopyReprs( p->pCla, p->vTimeouts ); - pManAigNew = Aig_ManDupRepr( p->pManAig ); - Aig_ManCreateChoices( pManAigNew ); + pManAigNew = Aig_ManDupRepr( p->pManAig, 1 ); + Aig_ManReprStart( pManAigNew, Aig_ManObjNumMax(pManAigNew) ); + Aig_ManTransferRepr( pManAigNew, p->pManAig ); + Aig_ManMarkValidChoices( pManAigNew ); Aig_ManStop( p->pManFraig ); p->pManFraig = NULL; p->timeTrav += clock() - clk2; @@ -359,14 +361,6 @@ p->timeTrav += clock() - clk2; Aig_ManCleanup( p->pManFraig ); pManAigNew = p->pManFraig; p->pManFraig = NULL; -/* - Fra_ClassesCopyReprs( p->pCla, p->vTimeouts ); - pManAigNew = Aig_ManDupRepr( p->pManAig ); -// Aig_ManCreateChoices( pManAigNew ); - Aig_ManCleanup( pManAigNew ); - Aig_ManStop( p->pManFraig ); - p->pManFraig = NULL; -*/ } p->timeTotal = clock() - clk; // collect final stats @@ -388,16 +382,16 @@ p->timeTotal = clock() - clk; SeeAlso [] ***********************************************************************/ -Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig ) +Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax ) { Fra_Par_t Pars, * pPars = &Pars; Fra_ParamsDefault( pPars ); - pPars->nBTLimitNode = 1000; - pPars->fVerbose = 0; - pPars->fProve = 0; + pPars->nBTLimitNode = nConfMax; + pPars->fChoicing = 1; pPars->fDoSparse = 1; pPars->fSpeculate = 0; - pPars->fChoicing = 1; + pPars->fProve = 0; + pPars->fVerbose = 0; return Fra_FraigPerform( pManAig, pPars ); } @@ -418,11 +412,11 @@ Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax ) Fra_Par_t Pars, * pPars = &Pars; Fra_ParamsDefault( pPars ); pPars->nBTLimitNode = nConfMax; - pPars->fVerbose = 0; - pPars->fProve = 0; + pPars->fChoicing = 0; pPars->fDoSparse = 1; pPars->fSpeculate = 0; - pPars->fChoicing = 0; + pPars->fProve = 0; + pPars->fVerbose = 0; pFraig = Fra_FraigPerform( pManAig, pPars ); return pFraig; } diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c index 5e4b8c28..d8bf4e48 100644 --- a/src/aig/fra/fraImp.c +++ b/src/aig/fra/fraImp.c @@ -64,8 +64,8 @@ static inline int * Fra_SmlCountOnes( Fra_Sml_t * p ) { Aig_Obj_t * pObj; int i, * pnBits; - pnBits = ALLOC( int, Aig_ManObjIdMax(p->pAig) + 1 ); - memset( pnBits, 0, sizeof(int) * (Aig_ManObjIdMax(p->pAig) + 1) ); + pnBits = ALLOC( int, Aig_ManObjNumMax(p->pAig) ); + memset( pnBits, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) ); Aig_ManForEachObj( p->pAig, pObj, i ) pnBits[i] = Fra_SmlCountOnesOne( p, i ); return pnBits; @@ -325,7 +325,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0; int CostMin = AIG_INFINITY, CostMax = 0; int i, k, Imp, CostRange, clk = clock(); - assert( Aig_ManObjIdMax(p->pManAig) + 1 < (1 << 15) ); + assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) ); assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit ); // normalize both managers pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords ); diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c index 53dbdbb6..14fba9ba 100644 --- a/src/aig/fra/fraInd.c +++ b/src/aig/fra/fraInd.c @@ -133,7 +133,8 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p ) assert( Aig_ManRegNum(p->pManAig) < Aig_ManPiNum(p->pManAig) ); // start the fraig package - pManFraig = Aig_ManStart( (Aig_ManObjIdMax(p->pManAig) + 1) * p->nFramesAll ); + pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) * p->nFramesAll ); + pManFraig->pName = Aig_UtilStrsav( p->pManAig->pName ); pManFraig->nRegs = p->pManAig->nRegs; // create PI nodes for the frames for ( f = 0; f < p->nFramesAll; f++ ) @@ -194,7 +195,7 @@ void Fra_FramesAddMore( Aig_Man_t * p, int nFrames ) Aig_ManForEachObj( p, pObj, i ) pObj->pData = pObj; // iterate and add objects - nNodesOld = Aig_ManObjIdMax(p); + nNodesOld = Aig_ManObjNumMax(p); pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p) ); for ( f = 0; f < nFrames; f++ ) { @@ -372,11 +373,14 @@ PRT( "Time", clock() - clk ); if ( p->pSat == NULL ) printf( "Fra_FraigInduction(): Adding implicationsn to CNF led to a conflict.\n" ); } - + // set the pointers to the manager Aig_ManForEachObj( p->pManFraig, pObj, i ) pObj->pData = p; + // prepare solver for fraiging the last timeframe + Fra_ManClean( p, Aig_ManObjNumMax(p->pManFraig) + Aig_ManNodeNum(p->pManAig) ); + // transfer PI/LO variable numbers Aig_ManForEachObj( p->pManFraig, pObj, i ) { @@ -402,12 +406,14 @@ PRT( "Time", clock() - clk ); p->nSatCallsRecent = 0; p->nSatCallsSkipped = 0; Fra_FraigSweep( p ); + // remove FRAIG and SAT solver + Aig_ManStop( p->pManFraig ); p->pManFraig = NULL; + sat_solver_delete( p->pSat ); p->pSat = NULL; + memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll ); // printf( "Recent SAT called = %d. Skipped = %d.\n", p->nSatCallsRecent, p->nSatCallsSkipped ); assert( p->vTimeouts == NULL ); if ( p->vTimeouts ) printf( "Fra_FraigInduction(): SAT solver timed out!\n" ); - // cleanup - Fra_ManClean( p ); // check if refinement has happened // p->pCla->fRefinement = (int)(nLitsOld != Fra_ClassesCountLits(p->pCla)); if ( p->pCla->fRefinement && @@ -435,7 +441,7 @@ clk2 = clock(); // Fra_ClassesPrint( p->pCla, 1 ); Fra_ClassesSelectRepr( p->pCla ); Fra_ClassesCopyReprs( p->pCla, p->vTimeouts ); - pManAigNew = Aig_ManDupRepr( pManAig ); + pManAigNew = Aig_ManDupRepr( pManAig, 0 ); // add implications to the manager if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) ) Fra_ImpRecordInManager( p, pManAigNew ); diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c index c3b5504e..e73d610f 100644 --- a/src/aig/fra/fraLcr.c +++ b/src/aig/fra/fraLcr.c @@ -509,7 +509,7 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC Fra_Man_t * pTemp; Aig_Man_t * pAigPart, * pAigNew = NULL; Vec_Int_t * vPart; - Aig_Obj_t * pObj = Aig_ManObj(pAig, 2078); +// Aig_Obj_t * pObj = Aig_ManObj(pAig, 2078); int i, nIter, clk = clock(), clk2, clk3; if ( Aig_ManNodeNum(pAig) == 0 ) { @@ -622,7 +622,7 @@ clk2 = clock(); if ( fReprSelect ) Fra_ClassesSelectRepr( p->pCla ); Fra_ClassesCopyReprs( p->pCla, NULL ); - pAigNew = Aig_ManDupRepr( p->pAig ); + pAigNew = Aig_ManDupRepr( p->pAig, 0 ); Aig_ManSeqCleanup( pAigNew ); // Aig_ManCountMergeRegs( pAigNew ); p->timeUpdate += clock() - clk2; diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c index 97282e98..f505b0c2 100644 --- a/src/aig/fra/fraMan.c +++ b/src/aig/fra/fraMan.c @@ -42,20 +42,20 @@ void Fra_ParamsDefault( Fra_Par_t * pPars ) { memset( pPars, 0, sizeof(Fra_Par_t) ); - pPars->nSimWords = 32; // the number of words in the simulation info - pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached - pPars->fPatScores = 0; // enables simulation pattern scoring - pPars->MaxScore = 25; // max score after which resimulation is used - pPars->fDoSparse = 1; // skips sparse functions -// pPars->dActConeRatio = 0.05; // the ratio of cone to be bumped -// pPars->dActConeBumpMax = 5.0; // the largest bump of activity - pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped - pPars->dActConeBumpMax = 10.0; // the largest bump of activity - pPars->nBTLimitNode = 100; // conflict limit at a node - pPars->nBTLimitMiter = 500000; // conflict limit at an output - pPars->nFramesK = 0; // the number of timeframes to unroll - pPars->fConeBias = 1; - pPars->fRewrite = 0; + pPars->nSimWords = 32; // the number of words in the simulation info + pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached + pPars->fPatScores = 0; // enables simulation pattern scoring + pPars->MaxScore = 25; // max score after which resimulation is used + pPars->fDoSparse = 1; // skips sparse functions +// pPars->dActConeRatio = 0.05; // the ratio of cone to be bumped +// pPars->dActConeBumpMax = 5.0; // the largest bump of activity + pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped + pPars->dActConeBumpMax = 10.0; // the largest bump of activity + pPars->nBTLimitNode = 100; // conflict limit at a node + pPars->nBTLimitMiter = 500000; // conflict limit at an output + pPars->nFramesK = 0; // the number of timeframes to unroll + pPars->fConeBias = 1; + pPars->fRewrite = 0; } /**Function************************************************************* @@ -72,20 +72,20 @@ void Fra_ParamsDefault( Fra_Par_t * pPars ) void Fra_ParamsDefaultSeq( Fra_Par_t * pPars ) { memset( pPars, 0, sizeof(Fra_Par_t) ); - pPars->nSimWords = 1; // the number of words in the simulation info - pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached - pPars->fPatScores = 0; // enables simulation pattern scoring - pPars->MaxScore = 25; // max score after which resimulation is used - pPars->fDoSparse = 1; // skips sparse functions - pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped - pPars->dActConeBumpMax = 10.0; // the largest bump of activity - pPars->nBTLimitNode =10000000; // conflict limit at a node - pPars->nBTLimitMiter = 500000; // conflict limit at an output - pPars->nFramesK = 1; // the number of timeframes to unroll - pPars->fConeBias = 0; - pPars->fRewrite = 0; - pPars->fLatchCorr = 0; -} + pPars->nSimWords = 1; // the number of words in the simulation info + pPars->dSimSatur = 0.005; // the ratio of refined classes when saturation is reached + pPars->fPatScores = 0; // enables simulation pattern scoring + pPars->MaxScore = 25; // max score after which resimulation is used + pPars->fDoSparse = 1; // skips sparse functions + pPars->dActConeRatio = 0.3; // the ratio of cone to be bumped + pPars->dActConeBumpMax = 10.0; // the largest bump of activity + pPars->nBTLimitNode = 10000000; // conflict limit at a node + pPars->nBTLimitMiter = 500000; // conflict limit at an output + pPars->nFramesK = 1; // the number of timeframes to unroll + pPars->fConeBias = 0; + pPars->fRewrite = 0; + pPars->fLatchCorr = 0; +} /**Function************************************************************* @@ -108,7 +108,7 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars ) memset( p, 0, sizeof(Fra_Man_t) ); p->pPars = pPars; p->pManAig = pManAig; - p->nSizeAlloc = Aig_ManObjIdMax( pManAig ) + 1; + p->nSizeAlloc = Aig_ManObjNumMax( pManAig ); p->nFramesAll = pPars->nFramesK + 1; // allocate storage for sim pattern p->nPatWords = Aig_BitWordNum( (Aig_ManPiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) ); @@ -119,10 +119,6 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars ) // allocate other members p->pMemFraig = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll ); memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll ); - p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nSizeAlloc * p->nFramesAll + 10000 ); - memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nSizeAlloc * p->nFramesAll + 10000 ); - p->pMemSatNums = ALLOC( int, p->nSizeAlloc * p->nFramesAll + 10000 ); - memset( p->pMemSatNums, 0, sizeof(int) * p->nSizeAlloc * p->nFramesAll + 10000 ); // set random number generator srand( 0xABCABC ); // set the pointer to the manager @@ -142,24 +138,24 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars ) SeeAlso [] ***********************************************************************/ -void Fra_ManClean( Fra_Man_t * p ) +void Fra_ManClean( Fra_Man_t * p, int nNodesMax ) { - int i, Limit; - - Limit = Aig_ManObjIdMax(p->pManFraig) + 1; - for ( i = 0; i < Limit; i++ ) + int i; + // remove old arrays + for ( i = 0; i < p->nMemAlloc; i++ ) if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 ) Vec_PtrFree( p->pMemFanins[i] ); - - memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll ); - memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * Limit ); - memset( p->pMemSatNums, 0, sizeof(int) * Limit ); - - Aig_ManStop( p->pManFraig ); - p->pManFraig = NULL; - - sat_solver_delete( p->pSat ); - p->pSat = NULL; + // realloc for the new size + if ( p->nMemAlloc < nNodesMax ) + { + int nMemAllocNew = nNodesMax + 5000; + p->pMemFanins = REALLOC( Vec_Ptr_t *, p->pMemFanins, nMemAllocNew ); + p->pMemSatNums = REALLOC( int, p->pMemSatNums, nMemAllocNew ); + p->nMemAlloc = nMemAllocNew; + } + // prepare for the new run + memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc ); + memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc ); } /**Function************************************************************* @@ -180,7 +176,8 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p ) int i; assert( p->pManFraig == NULL ); // start the fraig package - pManFraig = Aig_ManStart( Aig_ManObjIdMax(p->pManAig) + 1 ); + pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) ); + pManFraig->pName = Aig_UtilStrsav( p->pManAig->pName ); pManFraig->nRegs = p->pManAig->nRegs; pManFraig->nAsserts = p->pManAig->nAsserts; // set the pointers to the available fraig nodes @@ -190,6 +187,12 @@ Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p ) // set the pointers to the manager Aig_ManForEachObj( pManFraig, pObj, i ) pObj->pData = p; + // allocate memory for mapping FRAIG nodes into SAT numbers and fanins + p->nMemAlloc = p->nSizeAlloc; + p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nMemAlloc ); + memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc ); + p->pMemSatNums = ALLOC( int, p->nMemAlloc ); + memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc ); // make sure the satisfying assignment is node assigned assert( pManFraig->pData == NULL ); return pManFraig; @@ -231,7 +234,6 @@ void Fra_ManFinalizeComb( Fra_Man_t * p ) ***********************************************************************/ void Fra_ManStop( Fra_Man_t * p ) { - int i; if ( p->pPars->fVerbose ) Fra_ManPrint( p ); // save mapping from original nodes into FRAIG nodes @@ -242,9 +244,7 @@ void Fra_ManStop( Fra_Man_t * p ) p->pManAig->pObjCopies = p->pMemFraig; p->pMemFraig = NULL; } - for ( i = 0; i < p->nSizeAlloc; i++ ) - if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 ) - Vec_PtrFree( p->pMemFanins[i] ); + Fra_ManClean( p, 0 ); if ( p->vTimeouts ) Vec_PtrFree( p->vTimeouts ); if ( p->vPiVars ) Vec_PtrFree( p->vPiVars ); if ( p->pSat ) sat_solver_delete( p->pSat ); @@ -271,14 +271,14 @@ void Fra_ManStop( Fra_Man_t * p ) ***********************************************************************/ void Fra_ManPrint( Fra_Man_t * p ) { - double nMemory = 1.0*Aig_ManObjIdMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20); + double nMemory = 1.0*Aig_ManObjNumMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20); printf( "SimWord = %d. Round = %d. Mem = %0.2f Mb. LitBeg = %d. LitEnd = %d. (%6.2f %%).\n", p->pPars->nSimWords, p->pSml->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/(p->nLitsBeg?p->nLitsBeg:1) ); printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. C-lim = %d. ImpRatio = %6.2f %%\n", p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->pPars->nBTLimitNode, Fra_ImpComputeStateSpaceRatio(p) ); printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", - p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg, - p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg ); + p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1), + p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) ); if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat ); PRT( "AIG simulation ", p->pSml->timeSim ); PRT( "AIG traversal ", p->timeTrav ); diff --git a/src/aig/fra/fraPart.c b/src/aig/fra/fraPart.c index 23b6dd1d..691b2b3d 100644 --- a/src/aig/fra/fraPart.c +++ b/src/aig/fra/fraPart.c @@ -41,7 +41,7 @@ ***********************************************************************/ void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim ) { - ProgressBar * pProgress; + Bar_Progress_t * pProgress; Vec_Vec_t * vSupps, * vSuppsIn; Vec_Ptr_t * vSuppsNew; Vec_Int_t * vSupNew, * vSup, * vSup2, * vTemp;//, * vSupIn; @@ -86,10 +86,10 @@ clk = clock(); vSuppsNew = Vec_PtrAlloc( Aig_ManPoNum(p) ); vOverNew = Vec_IntAlloc( Aig_ManPoNum(p) ); vQuantNew = Vec_IntAlloc( Aig_ManPoNum(p) ); - pProgress = Extra_ProgressBarStart( stdout, Aig_ManPoNum(p) ); + pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(p) ); Aig_ManForEachPo( p, pObj, i ) { - Extra_ProgressBarUpdate( pProgress, i, NULL ); + Bar_ProgressUpdate( pProgress, i, NULL ); // get old supports vSup = Vec_VecEntry( vSupps, i ); if ( Vec_IntSize(vSup) < 2 ) @@ -152,7 +152,7 @@ clk = clock(); printf( "\n" ); */ } - Extra_ProgressBarStop( pProgress ); + Bar_ProgressStop( pProgress ); PRT( "Scanning", clock() - clk ); // print cumulative statistics diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c index bc8ef08a..e1cc4c32 100644 --- a/src/aig/fra/fraSat.c +++ b/src/aig/fra/fraSat.c @@ -18,6 +18,7 @@ ***********************************************************************/ +#include <math.h> #include "fra.h" //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 88c552dc..0146ac5a 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -19,6 +19,7 @@ ***********************************************************************/ #include "fra.h" +#include "ioa.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -100,7 +101,7 @@ PRT( "Time", clock() - clkTotal ); SeeAlso [] ***********************************************************************/ -int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fRetimeFirst, int fVerbose, int fVeryVerbose ) +int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fVerbose, int fVeryVerbose ) { Aig_Man_t * pNew, * pTemp; int nFrames, RetValue, nIter, clk, clkTotal = clock(); @@ -116,7 +117,9 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fRetimeFirst, int fVerbose, // perform sequential cleanup clk = clock(); + if ( pNew->nRegs ) pNew = Aig_ManReduceLaches( pNew, 0 ); + if ( pNew->nRegs ) pNew = Aig_ManConstReduce( pNew, 0 ); if ( fVerbose ) { @@ -126,7 +129,7 @@ PRT( "Time", clock() - clk ); } // perform forward retiming - if ( fRetimeFirst ) + if ( fRetimeFirst && pNew->nRegs ) { clk = clock(); pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 ); @@ -141,6 +144,8 @@ PRT( "Time", clock() - clk ); // run latch correspondence clk = clock(); + if ( pNew->nRegs ) + { pNew = Aig_ManDup( pTemp = pNew, 1 ); Aig_ManStop( pTemp ); pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, fVeryVerbose, &nIter ); @@ -151,6 +156,7 @@ clk = clock(); nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); PRT( "Time", clock() - clk ); } + } // perform fraiging clk = clock(); @@ -166,7 +172,7 @@ PRT( "Time", clock() - clk ); // perform seq sweeping while increasing the number of frames RetValue = Fra_FraigMiterStatus( pNew ); if ( RetValue == -1 ) - for ( nFrames = 1; ; nFrames *= 2 ) + for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 ) { clk = clock(); pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter ); @@ -203,19 +209,35 @@ clk = clock(); Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) ); PRT( "Time", clock() - clk ); } + if ( pNew->nRegs ) + pNew = Aig_ManConstReduce( pNew, 0 ); } + // get the miter status RetValue = Fra_FraigMiterStatus( pNew ); - Aig_ManStop( pNew ); // report the miter if ( RetValue == 1 ) + { printf( "Networks are equivalent. " ); +PRT( "Time", clock() - clkTotal ); + } else if ( RetValue == 0 ) + { printf( "Networks are NOT EQUIVALENT. " ); +PRT( "Time", clock() - clkTotal ); + } else + { + static int Counter = 1; + char pFileName[1000]; printf( "Networks are UNDECIDED. " ); PRT( "Time", clock() - clkTotal ); + sprintf( pFileName, "sm%03d.aig", Counter++ ); + Ioa_WriteAiger( pNew, pFileName, 0 ); + printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName ); + } + Aig_ManStop( pNew ); return RetValue; } diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c index 0b93fb73..d6f6d74a 100644 --- a/src/aig/fra/fraSim.c +++ b/src/aig/fra/fraSim.c @@ -703,7 +703,7 @@ printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize( Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame ) { Fra_Sml_t * p; - p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * (Aig_ManObjIdMax(pAig) + 1) * (nPref + nFrames) * nWordsFrame ); + p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame ); memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame ); p->pAig = pAig; p->nPref = nPref; diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h index 37096473..c5815a2c 100644 --- a/src/aig/hop/hop.h +++ b/src/aig/hop/hop.h @@ -121,6 +121,8 @@ static inline int Hop_TruthWordNum( int nVars ) { return nVars static inline int Hop_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; } static inline void Hop_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); } static inline void Hop_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); } +static inline int Hop_Base2Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n >>= 1, r++ ); return r; } +static inline int Hop_Base10Log( unsigned n ) { int r; assert( n >= 0 ); if ( n < 2 ) return n; for ( r = 0, n--; n; n /= 10, r++ ); return r; } static inline Hop_Obj_t * Hop_Regular( Hop_Obj_t * p ) { return (Hop_Obj_t *)((unsigned long)(p) & ~01); } static inline Hop_Obj_t * Hop_Not( Hop_Obj_t * p ) { return (Hop_Obj_t *)((unsigned long)(p) ^ 01); } @@ -268,12 +270,12 @@ static inline void Hop_ManRecycleMemory( Hop_Man_t * p, Hop_Obj_t * pEntry ) /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -/*=== aigBalance.c ========================================================*/ +/*=== hopBalance.c ========================================================*/ extern Hop_Man_t * Hop_ManBalance( Hop_Man_t * p, int fUpdateLevel ); extern Hop_Obj_t * Hop_NodeBalanceBuildSuper( Hop_Man_t * p, Vec_Ptr_t * vSuper, Hop_Type_t Type, int fUpdateLevel ); -/*=== aigCheck.c ========================================================*/ +/*=== hopCheck.c ========================================================*/ extern int Hop_ManCheck( Hop_Man_t * p ); -/*=== aigDfs.c ==========================================================*/ +/*=== hopDfs.c ==========================================================*/ extern Vec_Ptr_t * Hop_ManDfs( Hop_Man_t * p ); extern Vec_Ptr_t * Hop_ManDfsNode( Hop_Man_t * p, Hop_Obj_t * pNode ); extern int Hop_ManCountLevels( Hop_Man_t * p ); @@ -282,16 +284,16 @@ extern int Hop_DagSize( Hop_Obj_t * pObj ); extern void Hop_ConeUnmark_rec( Hop_Obj_t * pObj ); extern Hop_Obj_t * Hop_Transfer( Hop_Man_t * pSour, Hop_Man_t * pDest, Hop_Obj_t * pObj, int nVars ); extern Hop_Obj_t * Hop_Compose( Hop_Man_t * p, Hop_Obj_t * pRoot, Hop_Obj_t * pFunc, int iVar ); -/*=== aigMan.c ==========================================================*/ +/*=== hopMan.c ==========================================================*/ extern Hop_Man_t * Hop_ManStart(); extern Hop_Man_t * Hop_ManDup( Hop_Man_t * p ); extern void Hop_ManStop( Hop_Man_t * p ); extern int Hop_ManCleanup( Hop_Man_t * p ); extern void Hop_ManPrintStats( Hop_Man_t * p ); -/*=== aigMem.c ==========================================================*/ +/*=== hopMem.c ==========================================================*/ extern void Hop_ManStartMemory( Hop_Man_t * p ); extern void Hop_ManStopMemory( Hop_Man_t * p ); -/*=== aigObj.c ==========================================================*/ +/*=== hopObj.c ==========================================================*/ extern Hop_Obj_t * Hop_ObjCreatePi( Hop_Man_t * p ); extern Hop_Obj_t * Hop_ObjCreatePo( Hop_Man_t * p, Hop_Obj_t * pDriver ); extern Hop_Obj_t * Hop_ObjCreate( Hop_Man_t * p, Hop_Obj_t * pGhost ); @@ -301,7 +303,7 @@ extern void Hop_ObjDelete( Hop_Man_t * p, Hop_Obj_t * pObj ); extern void Hop_ObjDelete_rec( Hop_Man_t * p, Hop_Obj_t * pObj ); extern Hop_Obj_t * Hop_ObjRepr( Hop_Obj_t * pObj ); extern void Hop_ObjCreateChoice( Hop_Obj_t * pOld, Hop_Obj_t * pNew ); -/*=== aigOper.c =========================================================*/ +/*=== hopOper.c =========================================================*/ extern Hop_Obj_t * Hop_IthVar( Hop_Man_t * p, int i ); extern Hop_Obj_t * Hop_Oper( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1, Hop_Type_t Type ); extern Hop_Obj_t * Hop_And( Hop_Man_t * p, Hop_Obj_t * p0, Hop_Obj_t * p1 ); @@ -313,13 +315,13 @@ extern Hop_Obj_t * Hop_Miter( Hop_Man_t * p, Vec_Ptr_t * vPairs ); extern Hop_Obj_t * Hop_CreateAnd( Hop_Man_t * p, int nVars ); extern Hop_Obj_t * Hop_CreateOr( Hop_Man_t * p, int nVars ); extern Hop_Obj_t * Hop_CreateExor( Hop_Man_t * p, int nVars ); -/*=== aigTable.c ========================================================*/ +/*=== hopTable.c ========================================================*/ extern Hop_Obj_t * Hop_TableLookup( Hop_Man_t * p, Hop_Obj_t * pGhost ); extern void Hop_TableInsert( Hop_Man_t * p, Hop_Obj_t * pObj ); extern void Hop_TableDelete( Hop_Man_t * p, Hop_Obj_t * pObj ); extern int Hop_TableCountEntries( Hop_Man_t * p ); extern void Hop_TableProfile( Hop_Man_t * p ); -/*=== aigUtil.c =========================================================*/ +/*=== hopUtil.c =========================================================*/ extern void Hop_ManIncrementTravId( Hop_Man_t * p ); extern void Hop_ManCleanData( Hop_Man_t * p ); extern void Hop_ObjCleanData_rec( Hop_Obj_t * pObj ); diff --git a/src/aig/hop/hopTable.c b/src/aig/hop/hopTable.c index 8e61ef36..76390054 100644 --- a/src/aig/hop/hopTable.c +++ b/src/aig/hop/hopTable.c @@ -28,8 +28,8 @@ static unsigned long Hop_Hash( Hop_Obj_t * pObj, int TableSize ) { unsigned long Key = Hop_ObjIsExor(pObj) * 1699; - Key ^= (long)Hop_ObjFanin0(pObj) * 7937; - Key ^= (long)Hop_ObjFanin1(pObj) * 2971; + Key ^= Hop_ObjFanin0(pObj)->Id * 7937; + Key ^= Hop_ObjFanin1(pObj)->Id * 2971; Key ^= Hop_ObjFaninC0(pObj) * 911; Key ^= Hop_ObjFaninC1(pObj) * 353; return Key % TableSize; diff --git a/src/aig/hop/hopUtil.c b/src/aig/hop/hopUtil.c index 34f689f6..87fdb15e 100644 --- a/src/aig/hop/hopUtil.c +++ b/src/aig/hop/hopUtil.c @@ -523,7 +523,7 @@ void Hop_ManDumpBlif( Hop_Man_t * p, char * pFileName ) pObj->pData = (void *)Counter++; Vec_PtrForEachEntry( vNodes, pObj, i ) pObj->pData = (void *)Counter++; - nDigits = Extra_Base10Log( Counter ); + nDigits = Hop_Base10Log( Counter ); // write the file pFile = fopen( pFileName, "w" ); fprintf( pFile, "# BLIF file written by procedure Hop_ManDumpBlif() in ABC\n" ); diff --git a/src/aig/ioa/ioa.h b/src/aig/ioa/ioa.h new file mode 100644 index 00000000..3458d12e --- /dev/null +++ b/src/aig/ioa/ioa.h @@ -0,0 +1,80 @@ +/**CFile**************************************************************** + + FileName [ioa.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [AIG package.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: ioa.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __IOA_H__ +#define __IOA_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include <stdio.h> +#include <stdlib.h> +#include <string.h> +#include <assert.h> +#include <time.h> + +#include "vec.h" +#include "bar.h" +#include "aig.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// ITERATORS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== ioaReadAig.c ========================================================*/ +extern Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck ); +/*=== ioaWriteAig.c =======================================================*/ +extern void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols ); +/*=== ioaUtil.c =======================================================*/ +extern int Ioa_FileSize( char * pFileName ); +extern char * Ioa_FileNameGeneric( char * FileName ); +extern char * Ioa_TimeStamp(); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/aig/ioa/ioaReadAig.c b/src/aig/ioa/ioaReadAig.c new file mode 100644 index 00000000..937e446f --- /dev/null +++ b/src/aig/ioa/ioaReadAig.c @@ -0,0 +1,312 @@ +/**CFile**************************************************************** + + FileName [ioaReadAiger.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Command processing package.] + + Synopsis [Procedures to read binary AIGER format developed by + Armin Biere, Johannes Kepler University (http://fmv.jku.at/)] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - December 16, 2006.] + + Revision [$Id: ioaReadAiger.c,v 1.00 2006/12/16 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ioa.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +unsigned Ioa_ReadAigerDecode( char ** ppPos ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Reads the AIG in the binary AIGER format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Aig_Man_t * Ioa_ReadAiger( char * pFileName, int fCheck ) +{ + Bar_Progress_t * pProgress; + FILE * pFile; + Vec_Ptr_t * vNodes, * vDrivers;//, * vTerms; + Aig_Obj_t * pObj, * pNode0, * pNode1; + Aig_Man_t * pManNew; + int nTotal, nInputs, nOutputs, nLatches, nAnds, nFileSize, i;//, iTerm, nDigits; + char * pContents, * pDrivers, * pSymbols, * pCur, * pName;//, * pType; + unsigned uLit0, uLit1, uLit; + + // read the file into the buffer + nFileSize = Ioa_FileSize( pFileName ); + pFile = fopen( pFileName, "rb" ); + pContents = ALLOC( char, nFileSize ); + fread( pContents, nFileSize, 1, pFile ); + fclose( pFile ); + + // check if the input file format is correct + if ( strncmp(pContents, "aig", 3) != 0 ) + { + fprintf( stdout, "Wrong input file format.\n" ); + return NULL; + } + + // read the file type + pCur = pContents; while ( *pCur++ != ' ' ); + // read the number of objects + nTotal = atoi( pCur ); while ( *pCur++ != ' ' ); + // read the number of inputs + nInputs = atoi( pCur ); while ( *pCur++ != ' ' ); + // read the number of latches + nLatches = atoi( pCur ); while ( *pCur++ != ' ' ); + // read the number of outputs + nOutputs = atoi( pCur ); while ( *pCur++ != ' ' ); + // read the number of nodes + nAnds = atoi( pCur ); while ( *pCur++ != '\n' ); + // check the parameters + if ( nTotal != nInputs + nLatches + nAnds ) + { + fprintf( stdout, "The paramters are wrong.\n" ); + return NULL; + } + + // allocate the empty AIG + pManNew = Aig_ManStart( nAnds ); + pName = Ioa_FileNameGeneric( pFileName ); + pManNew->pName = Aig_UtilStrsav( pName ); +// pManNew->pSpec = Ioa_UtilStrsav( pFileName ); + free( pName ); + + // prepare the array of nodes + vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds ); + Vec_PtrPush( vNodes, Aig_ManConst0(pManNew) ); + + // create the PIs + for ( i = 0; i < nInputs + nLatches; i++ ) + { + pObj = Aig_ObjCreatePi(pManNew); + Vec_PtrPush( vNodes, pObj ); + } +/* + // create the POs + for ( i = 0; i < nOutputs + nLatches; i++ ) + { + pObj = Aig_ObjCreatePo(pManNew); + } +*/ + // create the latches + pManNew->nRegs = nLatches; +/* + nDigits = Ioa_Base10Log( nLatches ); + for ( i = 0; i < nLatches; i++ ) + { + pObj = Aig_ObjCreateLatch(pManNew); + Aig_LatchSetInit0( pObj ); + pNode0 = Aig_ObjCreateBi(pManNew); + pNode1 = Aig_ObjCreateBo(pManNew); + Aig_ObjAddFanin( pObj, pNode0 ); + Aig_ObjAddFanin( pNode1, pObj ); + Vec_PtrPush( vNodes, pNode1 ); + // assign names to latch and its input +// Aig_ObjAssignName( pObj, Aig_ObjNameDummy("_L", i, nDigits), NULL ); +// printf( "Creating latch %s with input %d and output %d.\n", Aig_ObjName(pObj), pNode0->Id, pNode1->Id ); + } +*/ + + // remember the beginning of latch/PO literals + pDrivers = pCur; + + // scroll to the beginning of the binary data + for ( i = 0; i < nLatches + nOutputs; ) + if ( *pCur++ == '\n' ) + i++; + + // create the AND gates + pProgress = Bar_ProgressStart( stdout, nAnds ); + for ( i = 0; i < nAnds; i++ ) + { + Bar_ProgressUpdate( pProgress, i, NULL ); + uLit = ((i + 1 + nInputs + nLatches) << 1); + uLit1 = uLit - Ioa_ReadAigerDecode( &pCur ); + uLit0 = uLit1 - Ioa_ReadAigerDecode( &pCur ); +// assert( uLit1 > uLit0 ); + pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), uLit0 & 1 ); + pNode1 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit1 >> 1), uLit1 & 1 ); + assert( Vec_PtrSize(vNodes) == i + 1 + nInputs + nLatches ); + Vec_PtrPush( vNodes, Aig_And(pManNew, pNode0, pNode1) ); + } + Bar_ProgressStop( pProgress ); + + // remember the place where symbols begin + pSymbols = pCur; + + // read the latch driver literals + vDrivers = Vec_PtrAlloc( nLatches + nOutputs ); + pCur = pDrivers; +// Aig_ManForEachLatchInput( pManNew, pObj, i ) + for ( i = 0; i < nLatches; i++ ) + { + uLit0 = atoi( pCur ); while ( *pCur++ != '\n' ); + pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); +// Aig_ObjAddFanin( pObj, pNode0 ); + Vec_PtrPush( vDrivers, pNode0 ); + } + // read the PO driver literals +// Aig_ManForEachPo( pManNew, pObj, i ) + for ( i = 0; i < nOutputs; i++ ) + { + uLit0 = atoi( pCur ); while ( *pCur++ != '\n' ); + pNode0 = Aig_NotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); +// Aig_ObjAddFanin( pObj, pNode0 ); + Vec_PtrPush( vDrivers, pNode0 ); + } + + + // create the POs + for ( i = 0; i < nOutputs; i++ ) + Aig_ObjCreatePo( pManNew, Vec_PtrEntry(vDrivers, nLatches + i) ); + for ( i = 0; i < nLatches; i++ ) + Aig_ObjCreatePo( pManNew, Vec_PtrEntry(vDrivers, i) ); + Vec_PtrFree( vDrivers ); + +/* + // read the names if present + pCur = pSymbols; + if ( *pCur != 'c' ) + { + int Counter = 0; + while ( pCur < pContents + nFileSize && *pCur != 'c' ) + { + // get the terminal type + pType = pCur; + if ( *pCur == 'i' ) + vTerms = pManNew->vPis; + else if ( *pCur == 'l' ) + vTerms = pManNew->vBoxes; + else if ( *pCur == 'o' ) + vTerms = pManNew->vPos; + else + { + fprintf( stdout, "Wrong terminal type.\n" ); + return NULL; + } + // get the terminal number + iTerm = atoi( ++pCur ); while ( *pCur++ != ' ' ); + // get the node + if ( iTerm >= Vec_PtrSize(vTerms) ) + { + fprintf( stdout, "The number of terminal is out of bound.\n" ); + return NULL; + } + pObj = Vec_PtrEntry( vTerms, iTerm ); + if ( *pType == 'l' ) + pObj = Aig_ObjFanout0(pObj); + // assign the name + pName = pCur; while ( *pCur++ != '\n' ); + // assign this name + *(pCur-1) = 0; + Aig_ObjAssignName( pObj, pName, NULL ); + if ( *pType == 'l' ) + { + Aig_ObjAssignName( Aig_ObjFanin0(pObj), Aig_ObjName(pObj), "L" ); + Aig_ObjAssignName( Aig_ObjFanin0(Aig_ObjFanin0(pObj)), Aig_ObjName(pObj), "_in" ); + } + // mark the node as named + pObj->pCopy = (Aig_Obj_t *)Aig_ObjName(pObj); + } + + // assign the remaining names + Aig_ManForEachPi( pManNew, pObj, i ) + { + if ( pObj->pCopy ) continue; + Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL ); + Counter++; + } + Aig_ManForEachLatchOutput( pManNew, pObj, i ) + { + if ( pObj->pCopy ) continue; + Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL ); + Aig_ObjAssignName( Aig_ObjFanin0(pObj), Aig_ObjName(pObj), "L" ); + Aig_ObjAssignName( Aig_ObjFanin0(Aig_ObjFanin0(pObj)), Aig_ObjName(pObj), "_in" ); + Counter++; + } + Aig_ManForEachPo( pManNew, pObj, i ) + { + if ( pObj->pCopy ) continue; + Aig_ObjAssignName( pObj, Aig_ObjName(pObj), NULL ); + Counter++; + } + if ( Counter ) + printf( "Ioa_ReadAiger(): Added %d default names for nameless I/O/register objects.\n", Counter ); + } + else + { +// printf( "Ioa_ReadAiger(): I/O/register names are not given. Generating short names.\n" ); + Aig_ManShortNames( pManNew ); + } +*/ + + // skipping the comments + free( pContents ); + Vec_PtrFree( vNodes ); + + // remove the extra nodes + Aig_ManCleanup( pManNew ); + + // check the result + if ( fCheck && !Aig_ManCheck( pManNew ) ) + { + printf( "Ioa_ReadAiger: The network check has failed.\n" ); + Aig_ManStop( pManNew ); + return NULL; + } + return pManNew; +} + + +/**Function************************************************************* + + Synopsis [Extracts one unsigned AIG edge from the input buffer.] + + Description [This procedure is a slightly modified version of Armin Biere's + procedure "unsigned decode (FILE * file)". ] + + SideEffects [Updates the current reading position.] + + SeeAlso [] + +***********************************************************************/ +unsigned Ioa_ReadAigerDecode( char ** ppPos ) +{ + unsigned x = 0, i = 0; + unsigned char ch; + +// while ((ch = getnoneofch (file)) & 0x80) + while ((ch = *(*ppPos)++) & 0x80) + x |= (ch & 0x7f) << (7 * i++); + + return x | (ch << (7 * i)); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ioa/ioaUtil.c b/src/aig/ioa/ioaUtil.c new file mode 100644 index 00000000..79dcca1e --- /dev/null +++ b/src/aig/ioa/ioaUtil.c @@ -0,0 +1,117 @@ +/**CFile**************************************************************** + + FileName [ioaUtil.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Command processing package.] + + Synopsis [Procedures to read binary AIGER format developed by + Armin Biere, Johannes Kepler University (http://fmv.jku.at/)] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - December 16, 2006.] + + Revision [$Id: ioaUtil.c,v 1.00 2006/12/16 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ioa.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns the file size.] + + Description [The file should be closed.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ioa_FileSize( char * pFileName ) +{ + FILE * pFile; + int nFileSize; + pFile = fopen( pFileName, "r" ); + if ( pFile == NULL ) + { + printf( "Ioa_FileSize(): The file is unavailable (absent or open).\n" ); + return 0; + } + fseek( pFile, 0, SEEK_END ); + nFileSize = ftell( pFile ); + fclose( pFile ); + return nFileSize; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Ioa_FileNameGeneric( char * FileName ) +{ + char * pDot; + char * pUnd; + char * pRes; + + // find the generic name of the file + pRes = Aig_UtilStrsav( FileName ); + // find the pointer to the "." symbol in the file name +// pUnd = strstr( FileName, "_" ); + pUnd = NULL; + pDot = strstr( FileName, "." ); + if ( pUnd ) + pRes[pUnd - FileName] = 0; + else if ( pDot ) + pRes[pDot - FileName] = 0; + return pRes; +} + +/**Function************************************************************* + + Synopsis [Returns the time stamp.] + + Description [The file should be closed.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +char * Ioa_TimeStamp() +{ + static char Buffer[100]; + char * TimeStamp; + time_t ltime; + // get the current time + time( <ime ); + TimeStamp = asctime( localtime( <ime ) ); + TimeStamp[ strlen(TimeStamp) - 1 ] = 0; + strcpy( Buffer, TimeStamp ); + return Buffer; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ioa/ioaWriteAig.c b/src/aig/ioa/ioaWriteAig.c new file mode 100644 index 00000000..74462bbd --- /dev/null +++ b/src/aig/ioa/ioaWriteAig.c @@ -0,0 +1,291 @@ +/**CFile**************************************************************** + + FileName [ioaWriteAiger.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Command processing package.] + + Synopsis [Procedures to write binary AIGER format developed by + Armin Biere, Johannes Kepler University (http://fmv.jku.at/)] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - December 16, 2006.] + + Revision [$Id: ioaWriteAiger.c,v 1.00 2006/12/16 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "ioa.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/* + The following is taken from the AIGER format description, + which can be found at http://fmv.jku.at/aiger +*/ + + +/* + The AIGER And-Inverter Graph (AIG) Format Version 20061129 + ---------------------------------------------------------- + Armin Biere, Johannes Kepler University, 2006 + + This report describes the AIG file format as used by the AIGER library. + The purpose of this report is not only to motivate and document the + format, but also to allow independent implementations of writers and + readers by giving precise and unambiguous definitions. + + ... + +Introduction + + The name AIGER contains as one part the acronym AIG of And-Inverter + Graphs and also if pronounced in German sounds like the name of the + 'Eiger', a mountain in the Swiss alps. This choice should emphasize the + origin of this format. It was first openly discussed at the Alpine + Verification Meeting 2006 in Ascona as a way to provide a simple, compact + file format for a model checking competition affiliated to CAV 2007. + + ... + +Binary Format Definition + + The binary format is semantically a subset of the ASCII format with a + slightly different syntax. The binary format may need to reencode + literals, but translating a file in binary format into ASCII format and + then back in to binary format will result in the same file. + + The main differences of the binary format to the ASCII format are as + follows. After the header the list of input literals and all the + current state literals of a latch can be omitted. Furthermore the + definitions of the AND gates are binary encoded. However, the symbol + table and the comment section are as in the ASCII format. + + The header of an AIGER file in binary format has 'aig' as format + identifier, but otherwise is identical to the ASCII header. The standard + file extension for the binary format is therefore '.aig'. + + A header for the binary format is still in ASCII encoding: + + aig M I L O A + + Constants, variables and literals are handled in the same way as in the + ASCII format. The first simplifying restriction is on the variable + indices of inputs and latches. The variable indices of inputs come first, + followed by the pseudo-primary inputs of the latches and then the variable + indices of all LHS of AND gates: + + input variable indices 1, 2, ... , I + latch variable indices I+1, I+2, ... , (I+L) + AND variable indices I+L+1, I+L+2, ... , (I+L+A) == M + + The corresponding unsigned literals are + + input literals 2, 4, ... , 2*I + latch literals 2*I+2, 2*I+4, ... , 2*(I+L) + AND literals 2*(I+L)+2, 2*(I+L)+4, ... , 2*(I+L+A) == 2*M + + All literals have to be defined, and therefore 'M = I + L + A'. With this + restriction it becomes possible that the inputs and the current state + literals of the latches do not have to be listed explicitly. Therefore, + after the header only the list of 'L' next state literals follows, one per + latch on a single line, and then the 'O' outputs, again one per line. + + In the binary format we assume that the AND gates are ordered and respect + the child parent relation. AND gates with smaller literals on the LHS + come first. Therefore we can assume that the literals on the right-hand + side of a definition of an AND gate are smaller than the LHS literal. + Furthermore we can sort the literals on the RHS, such that the larger + literal comes first. A definition thus consists of three literals + + lhs rhs0 rhs1 + + with 'lhs' even and 'lhs > rhs0 >= rhs1'. Also the variable indices are + pairwise different to avoid combinational self loops. Since the LHS + indices of the definitions are all consecutive (as even integers), + the binary format does not have to keep 'lhs'. In addition, we can use + the order restriction and only write the differences 'delta0' and 'delta1' + instead of 'rhs0' and 'rhs1', with + + delta0 = lhs - rhs0, delta1 = rhs0 - rhs1 + + The differences will all be strictly positive, and in practice often very + small. We can take advantage of this fact by the simple little-endian + encoding of unsigned integers of the next section. After the binary delta + encoding of the RHSs of all AND gates, the optional symbol table and + optional comment section start in the same format as in the ASCII case. + + ... + +*/ + +static unsigned Ioa_ObjMakeLit( int Var, int fCompl ) { return (Var << 1) | fCompl; } +static unsigned Ioa_ObjAigerNum( Aig_Obj_t * pObj ) { return (unsigned)pObj->pData; } +static void Ioa_ObjSetAigerNum( Aig_Obj_t * pObj, unsigned Num ) { pObj->pData = (void *)Num; } + +int Ioa_WriteAigerEncode( char * pBuffer, int Pos, unsigned x ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Writes the AIG in the binary AIGER format.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Ioa_WriteAiger( Aig_Man_t * pMan, char * pFileName, int fWriteSymbols ) +{ + Bar_Progress_t * pProgress; + FILE * pFile; + Aig_Obj_t * pObj, * pDriver; + int i, nNodes, Pos, nBufferSize; + unsigned char * pBuffer; + unsigned uLit0, uLit1, uLit; + +// assert( Aig_ManIsStrash(pMan) ); + // start the output stream + pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + fprintf( stdout, "Ioa_WriteAiger(): Cannot open the output file \"%s\".\n", pFileName ); + return; + } +/* + Aig_ManForEachLatch( pMan, pObj, i ) + if ( !Aig_LatchIsInit0(pObj) ) + { + fprintf( stdout, "Ioa_WriteAiger(): Cannot write AIGER format with non-0 latch init values. Run \"zero\".\n" ); + return; + } +*/ + // set the node numbers to be used in the output file + nNodes = 0; + Ioa_ObjSetAigerNum( Aig_ManConst1(pMan), nNodes++ ); + Aig_ManForEachPi( pMan, pObj, i ) + Ioa_ObjSetAigerNum( pObj, nNodes++ ); + Aig_ManForEachNode( pMan, pObj, i ) + Ioa_ObjSetAigerNum( pObj, nNodes++ ); + + // write the header "M I L O A" where M = I + L + A + fprintf( pFile, "aig %u %u %u %u %u\n", + Aig_ManPiNum(pMan) + Aig_ManNodeNum(pMan), + Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan), + Aig_ManRegNum(pMan), + Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan), + Aig_ManNodeNum(pMan) ); + + // if the driver node is a constant, we need to complement the literal below + // because, in the AIGER format, literal 0/1 is represented as number 0/1 + // while, in ABC, constant 1 node has number 0 and so literal 0/1 will be 1/0 + + // write latch drivers + Aig_ManForEachLiSeq( pMan, pObj, i ) + { + pDriver = Aig_ObjFanin0(pObj); + fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) ); + } + + // write PO drivers + Aig_ManForEachPoSeq( pMan, pObj, i ) + { + pDriver = Aig_ObjFanin0(pObj); + fprintf( pFile, "%u\n", Ioa_ObjMakeLit( Ioa_ObjAigerNum(pDriver), Aig_ObjFaninC0(pObj) ^ (Ioa_ObjAigerNum(pDriver) == 0) ) ); + } + + // write the nodes into the buffer + Pos = 0; + nBufferSize = 6 * Aig_ManNodeNum(pMan) + 100; // skeptically assuming 3 chars per one AIG edge + pBuffer = ALLOC( char, nBufferSize ); + pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(pMan) ); + Aig_ManForEachNode( pMan, pObj, i ) + { + Bar_ProgressUpdate( pProgress, i, NULL ); + uLit = Ioa_ObjMakeLit( Ioa_ObjAigerNum(pObj), 0 ); + uLit0 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj) ); + uLit1 = Ioa_ObjMakeLit( Ioa_ObjAigerNum(Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj) ); + assert( uLit0 < uLit1 ); + Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit - uLit1 ); + Pos = Ioa_WriteAigerEncode( pBuffer, Pos, uLit1 - uLit0 ); + if ( Pos > nBufferSize - 10 ) + { + printf( "Ioa_WriteAiger(): AIGER generation has failed because the allocated buffer is too small.\n" ); + fclose( pFile ); + return; + } + } + assert( Pos < nBufferSize ); + Bar_ProgressStop( pProgress ); + + // write the buffer + fwrite( pBuffer, 1, Pos, pFile ); + free( pBuffer ); +/* + // write the symbol table + if ( fWriteSymbols ) + { + // write PIs + Aig_ManForEachPi( pMan, pObj, i ) + fprintf( pFile, "i%d %s\n", i, Aig_ObjName(pObj) ); + // write latches + Aig_ManForEachLatch( pMan, pObj, i ) + fprintf( pFile, "l%d %s\n", i, Aig_ObjName(Aig_ObjFanout0(pObj)) ); + // write POs + Aig_ManForEachPo( pMan, pObj, i ) + fprintf( pFile, "o%d %s\n", i, Aig_ObjName(pObj) ); + } +*/ + // write the comment + fprintf( pFile, "c\n" ); + fprintf( pFile, "%s\n", pMan->pName ); + fprintf( pFile, "This file was produced by the AIG package in ABC on %s\n", Ioa_TimeStamp() ); + fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" ); + fclose( pFile ); +} + +/**Function************************************************************* + + Synopsis [Adds one unsigned AIG edge to the output buffer.] + + Description [This procedure is a slightly modified version of Armin Biere's + procedure "void encode (FILE * file, unsigned x)" ] + + SideEffects [Returns the current writing position.] + + SeeAlso [] + +***********************************************************************/ +int Ioa_WriteAigerEncode( char * pBuffer, int Pos, unsigned x ) +{ + unsigned char ch; + while (x & ~0x7f) + { + ch = (x & 0x7f) | 0x80; +// putc (ch, file); + pBuffer[Pos++] = ch; + x >>= 7; + } + ch = x; +// putc (ch, file); + pBuffer[Pos++] = ch; + return Pos; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/ioa/module.make b/src/aig/ioa/module.make new file mode 100644 index 00000000..66b4a0d5 --- /dev/null +++ b/src/aig/ioa/module.make @@ -0,0 +1,3 @@ +SRC += src/aig/ioa/ioaReadAig.c \ + src/aig/ioa/ioaWriteAig.c \ + src/aig/ioa/ioaUtil.c diff --git a/src/aig/ivy/ivy.h b/src/aig/ivy/ivy.h index 6aa7fa9f..ed19d67c 100644 --- a/src/aig/ivy/ivy.h +++ b/src/aig/ivy/ivy.h @@ -30,6 +30,7 @@ extern "C" { //////////////////////////////////////////////////////////////////////// #include <stdio.h> +#include "extra.h" #include "vec.h" //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h index c08bead2..2ad9a6f0 100644 --- a/src/aig/kit/kit.h +++ b/src/aig/kit/kit.h @@ -35,6 +35,7 @@ extern "C" { #include <assert.h> #include <time.h> #include "vec.h" +#include "extra.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -488,7 +489,7 @@ extern Kit_DsdNtk_t * Kit_DsdDecomposeMux( unsigned * pTruth, int nVars, int nD extern void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars ); extern void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk ); extern int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk ); -extern void Kit_DsdGetSupports( Kit_DsdNtk_t * p ); +extern unsigned Kit_DsdGetSupports( Kit_DsdNtk_t * p ); extern Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p ); extern Kit_DsdNtk_t * Kit_DsdShrink( Kit_DsdNtk_t * p, int pPrios[] ); extern void Kit_DsdRotate( Kit_DsdNtk_t * p, int pFreqs[] ); @@ -510,6 +511,9 @@ extern unsigned Kit_GraphToTruth( Kit_Graph_t * pGraph ); extern Kit_Graph_t * Kit_TruthToGraph( unsigned * pTruth, int nVars, Vec_Int_t * vMemory ); extern int Kit_GraphLeafDepth_rec( Kit_Graph_t * pGraph, Kit_Node_t * pNode, Kit_Node_t * pLeaf ); /*=== kitHop.c ==========================================================*/ +//extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph ); +//extern Hop_Obj_t * Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory ); +//extern Hop_Obj_t * Kit_CoverToHop( Hop_Man_t * pMan, Vec_Int_t * vCover, int nVars, Vec_Int_t * vMemory ); /*=== kitIsop.c ==========================================================*/ extern int Kit_TruthIsop( unsigned * puTruth, int nVars, Vec_Int_t * vMemory, int fTryBoth ); /*=== kitSop.c ==========================================================*/ diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c index 354ab6ef..9c61bb6f 100644 --- a/src/aig/kit/kitDsd.c +++ b/src/aig/kit/kitDsd.c @@ -319,7 +319,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i { Kit_DsdObj_t * pObj; unsigned * pTruthRes, * pTruthPrime, * pTruthMint, * pTruthFans[16]; - unsigned i, m, iLit, nMints, fCompl, fPartial = 0; + unsigned i, m, iLit, nMints, fCompl, nPartial = 0; // get the node with this ID pObj = Kit_DsdNtkObj( pNtk, Id ); @@ -364,7 +364,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i else { pTruthFans[i] = NULL; - fPartial = 1; + nPartial = 1; } } else @@ -401,7 +401,7 @@ unsigned * Kit_DsdTruthComputeNode_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, i } assert( pObj->Type == KIT_DSD_PRIME ); - if ( uSupp && fPartial ) + if ( uSupp && nPartial ) { // find the only non-empty component Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) @@ -463,6 +463,169 @@ unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned /**Function************************************************************* + Synopsis [Derives the truth table of the DSD node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Kit_DsdTruthComputeNodeTwo_rec( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, int Id, unsigned uSupp, int iVar, unsigned * pTruthDec ) +{ + Kit_DsdObj_t * pObj; + unsigned * pTruthRes, * pTruthPrime, * pTruthMint, * pTruthFans[16]; + unsigned i, m, iLit, nMints, fCompl, uSuppCur, uSuppFan, nPartial; + int pfBoundSet[16]; + assert( uSupp > 0 ); + + // get the node with this ID + pObj = Kit_DsdNtkObj( pNtk, Id ); + pTruthRes = Vec_PtrEntry( p->vTtNodes, Id ); + if ( pObj == NULL ) + { + assert( Id < pNtk->nVars ); + return pTruthRes; + } + assert( pObj->Type != KIT_DSD_CONST1 ); + assert( pObj->Type != KIT_DSD_VAR ); + + // count the number of intersecting fanins + // collect the total support of the intersecting fanins + nPartial = 0; + uSuppFan = 0; + Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) + { + uSuppCur = Kit_DsdLitSupport(pNtk, iLit); + if ( uSupp & uSuppCur ) + { + nPartial++; + uSuppFan |= uSuppCur; + } + } + + // if there is no intersection, or full intersection, use simple procedure + if ( nPartial == 0 || nPartial == pObj->nFans ) + return Kit_DsdTruthComputeNode_rec( p, pNtk, Id, 0 ); + + // if support of the component includes some other variables + // we need to continue constructing it as usual by the two-function procedure + if ( uSuppFan != (uSuppFan & uSupp) ) + { + assert( nPartial == 1 ); +// return Kit_DsdTruthComputeNodeTwo_rec( p, pNtk, Id, uSupp, iVar, pTruthDec ); + Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) + { + if ( uSupp & Kit_DsdLitSupport(pNtk, iLit) ) + pTruthFans[i] = Kit_DsdTruthComputeNodeTwo_rec( p, pNtk, Kit_DsdLit2Var(iLit), uSupp, iVar, pTruthDec ); + else + pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), 0 ); + } + + // create composition/decomposition functions + if ( pObj->Type == KIT_DSD_AND ) + { + Kit_TruthFill( pTruthRes, pNtk->nVars ); + Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) + Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) ); + return pTruthRes; + } + if ( pObj->Type == KIT_DSD_XOR ) + { + Kit_TruthClear( pTruthRes, pNtk->nVars ); + fCompl = 0; + Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) + { + fCompl ^= Kit_DsdLitIsCompl(iLit); + Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars ); + } + if ( fCompl ) + Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars ); + return pTruthRes; + } + assert( pObj->Type == KIT_DSD_PRIME ); + } + else + { + assert( uSuppFan == (uSuppFan & uSupp) ); + assert( nPartial < pObj->nFans ); + // the support of the insecting component(s) is contained in the bound-set + // and yet there are components that are not contained in the bound set + + // solve the fanins and collect info, which components belong to the bound set + Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) + { + pTruthFans[i] = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(iLit), 0 ); + pfBoundSet[i] = (int)((uSupp & Kit_DsdLitSupport(pNtk, iLit)) > 0); + } + + // create composition/decomposition functions + if ( pObj->Type == KIT_DSD_AND ) + { + Kit_TruthIthVar( pTruthRes, pNtk->nVars, iVar ); + Kit_TruthFill( pTruthDec, pNtk->nVars ); + Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) + if ( pfBoundSet[i] ) + Kit_TruthAndPhase( pTruthDec, pTruthDec, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) ); + else + Kit_TruthAndPhase( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars, 0, Kit_DsdLitIsCompl(iLit) ); + return pTruthRes; + } + if ( pObj->Type == KIT_DSD_XOR ) + { + Kit_TruthIthVar( pTruthRes, pNtk->nVars, iVar ); + Kit_TruthClear( pTruthDec, pNtk->nVars ); + fCompl = 0; + Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) + { + fCompl ^= Kit_DsdLitIsCompl(iLit); + if ( pfBoundSet[i] ) + Kit_TruthXor( pTruthDec, pTruthDec, pTruthFans[i], pNtk->nVars ); + else + Kit_TruthXor( pTruthRes, pTruthRes, pTruthFans[i], pNtk->nVars ); + } + if ( fCompl ) + Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars ); + return pTruthRes; + } + assert( pObj->Type == KIT_DSD_PRIME ); + assert( nPartial == 1 ); + + // find the only non-empty component + Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) + if ( pfBoundSet[i] ) + break; + assert( i < pObj->nFans ); + + // save this component as the decomposed function + Kit_TruthCopy( pTruthDec, pTruthFans[i], pNtk->nVars ); + // set the corresponding component to be the new variable + Kit_TruthIthVar( pTruthFans[i], pNtk->nVars, iVar ); + } + + // get the truth table of the prime node + pTruthPrime = Kit_DsdObjTruth( pObj ); + // get storage for the temporary minterm + pTruthMint = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes); + + // go through the minterms + nMints = (1 << pObj->nFans); + Kit_TruthClear( pTruthRes, pNtk->nVars ); + for ( m = 0; m < nMints; m++ ) + { + if ( !Kit_TruthHasBit(pTruthPrime, m) ) + continue; + Kit_TruthFill( pTruthMint, pNtk->nVars ); + Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) + Kit_TruthAndPhase( pTruthMint, pTruthMint, pTruthFans[i], pNtk->nVars, 0, ((m & (1<<i)) == 0) ^ Kit_DsdLitIsCompl(iLit) ); + Kit_TruthOr( pTruthRes, pTruthRes, pTruthMint, pNtk->nVars ); + } + return pTruthRes; +} + +/**Function************************************************************* + Synopsis [Derives the truth table of the DSD network.] Description [] @@ -472,22 +635,37 @@ unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned SeeAlso [] ***********************************************************************/ -void Kit_DsdTruthComputeTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar ) +unsigned * Kit_DsdTruthComputeTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthDec ) { - unsigned * pTruthRes; + unsigned * pTruthRes, uSuppAll; int i; - // if support is specified, request that supports are available - if ( uSupp ) - Kit_DsdGetSupports( pNtk ); - // assign elementary truth tables + assert( uSupp > 0 ); assert( pNtk->nVars <= p->nVars ); + // compute support of all nodes + uSuppAll = Kit_DsdGetSupports( pNtk ); + // consider special case - there is no overlap + if ( (uSupp & uSuppAll) == 0 ) + { + Kit_TruthClear( pTruthDec, pNtk->nVars ); + return Kit_DsdTruthCompute( p, pNtk, 0 ); + } + // consider special case - support is fully contained + if ( (uSupp & uSuppAll) == uSuppAll ) + { + pTruthRes = Kit_DsdTruthCompute( p, pNtk, 0 ); + Kit_TruthCopy( pTruthDec, pTruthRes, pNtk->nVars ); + Kit_TruthIthVar( pTruthRes, pNtk->nVars, iVar ); + return pTruthRes; + } + // assign elementary truth tables for ( i = 0; i < (int)pNtk->nVars; i++ ) Kit_TruthCopy( Vec_PtrEntry(p->vTtNodes, i), Vec_PtrEntry(p->vTtElems, i), p->nVars ); // compute truth table for each node - pTruthRes = Kit_DsdTruthComputeNode_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root), uSupp ); + pTruthRes = Kit_DsdTruthComputeNodeTwo_rec( p, pNtk, Kit_DsdLit2Var(pNtk->Root), uSupp, iVar, pTruthDec ); // complement the truth table if needed if ( Kit_DsdLitIsCompl(pNtk->Root) ) Kit_TruthNot( pTruthRes, pTruthRes, pNtk->nVars ); + return pTruthRes; } /**Function************************************************************* @@ -522,10 +700,11 @@ void Kit_DsdTruth( Kit_DsdNtk_t * pNtk, unsigned * pTruthRes ) SeeAlso [] ***********************************************************************/ -void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp ) +void Kit_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthCo, unsigned * pTruthDec ) { - unsigned * pTruth = Kit_DsdTruthCompute( p, pNtk, uSupp ); - Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars ); + unsigned * pTruth = Kit_DsdTruthComputeTwo( p, pNtk, uSupp, iVar, pTruthDec ); + if ( pTruthCo ) + Kit_TruthCopy( pTruthCo, pTruth, pNtk->nVars ); } /**Function************************************************************* @@ -539,16 +718,29 @@ void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTru SeeAlso [] ***********************************************************************/ -void Kit_DsdTruthPartialTwo( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned uSupp, int iVar, unsigned * pTruthCo, unsigned * pTruthDec ) +void Kit_DsdTruthPartial( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruthRes, unsigned uSupp ) { - unsigned * pTruth; - Kit_DsdObj_t * pRoot; - Kit_DsdTruthComputeTwo( p, pNtk, uSupp, iVar ); - pRoot = Kit_DsdNtkRoot( pNtk ); - pTruth = Vec_PtrEntry( p->vTtNodes, 2*pRoot->Id+0 ); - Kit_TruthCopy( pTruthCo, pTruth, p->nVars ); - pTruth = Vec_PtrEntry( p->vTtNodes, 2*pRoot->Id+1 ); - Kit_TruthCopy( pTruthDec, pTruth, p->nVars ); + unsigned * pTruth = Kit_DsdTruthCompute( p, pNtk, uSupp ); + Kit_TruthCopy( pTruthRes, pTruth, pNtk->nVars ); +/* + // verification + { + // compute the same function using different procedure + unsigned * pTruthTemp = Vec_PtrEntry(p->vTtNodes, pNtk->nVars + pNtk->nNodes + 1); + pNtk->pSupps = NULL; + Kit_DsdTruthComputeTwo( p, pNtk, uSupp, -1, pTruthTemp ); +// if ( !Kit_TruthIsEqual( pTruthTemp, pTruthRes, pNtk->nVars ) ) + if ( !Kit_TruthIsEqualWithPhase( pTruthTemp, pTruthRes, pNtk->nVars ) ) + { + printf( "Verification FAILED!\n" ); + Kit_DsdPrint( stdout, pNtk ); + Kit_DsdPrintFromTruth( pTruthRes, pNtk->nVars ); + Kit_DsdPrintFromTruth( pTruthTemp, pNtk->nVars ); + } +// else +// printf( "Verification successful.\n" ); + } +*/ } /**Function************************************************************* @@ -1090,9 +1282,10 @@ unsigned Kit_DsdGetSupports_rec( Kit_DsdNtk_t * p, int iLit ) SeeAlso [] ***********************************************************************/ -void Kit_DsdGetSupports( Kit_DsdNtk_t * p ) +unsigned Kit_DsdGetSupports( Kit_DsdNtk_t * p ) { Kit_DsdObj_t * pRoot; + unsigned uSupport; assert( p->pSupps == NULL ); p->pSupps = ALLOC( unsigned, p->nNodes ); // consider simple special cases @@ -1100,16 +1293,17 @@ void Kit_DsdGetSupports( Kit_DsdNtk_t * p ) if ( pRoot->Type == KIT_DSD_CONST1 ) { assert( p->nNodes == 1 ); - p->pSupps[0] = 0; + uSupport = p->pSupps[0] = 0; } if ( pRoot->Type == KIT_DSD_VAR ) { assert( p->nNodes == 1 ); - p->pSupps[0] = Kit_DsdLitSupport( p, pRoot->pFans[0] ); + uSupport = p->pSupps[0] = Kit_DsdLitSupport( p, pRoot->pFans[0] ); } else - Kit_DsdGetSupports_rec( p, p->Root ); - assert( p->pSupps[0] <= 0xFFFF ); + uSupport = Kit_DsdGetSupports_rec( p, p->Root ); + assert( uSupport <= 0xFFFF ); + return uSupport; } /**Function************************************************************* @@ -1697,7 +1891,7 @@ void Kit_DsdVerify( Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars ) { Kit_DsdMan_t * p; unsigned * pTruthC; - p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk) ); + p = Kit_DsdManAlloc( nVars, Kit_DsdNtkObjNum(pNtk)+2 ); pTruthC = Kit_DsdTruthCompute( p, pNtk, 0 ); if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) ) printf( "Verification failed.\n" ); diff --git a/src/aig/kit/kitHop.c b/src/aig/kit/kitHop.c index 95461c4e..f914fbab 100644 --- a/src/aig/kit/kitHop.c +++ b/src/aig/kit/kitHop.c @@ -29,7 +29,6 @@ /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// - /**Function************************************************************* Synopsis [Transforms the decomposition graph into the AIG.] @@ -87,6 +86,36 @@ Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph ) /**Function************************************************************* + Synopsis [Strashed onen logic nodes using its truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Hop_Obj_t * Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory ) +{ + Hop_Obj_t * pObj; + Kit_Graph_t * pGraph; + // transform truth table into the decomposition tree + if ( vMemory == NULL ) + { + vMemory = Vec_IntAlloc( 0 ); + pGraph = Kit_TruthToGraph( pTruth, nVars, vMemory ); + Vec_IntFree( vMemory ); + } + else + pGraph = Kit_TruthToGraph( pTruth, nVars, vMemory ); + // derive the AIG for the decomposition tree + pObj = Kit_GraphToHop( pMan, pGraph ); + Kit_GraphFree( pGraph ); + return pObj; +} + +/**Function************************************************************* + Synopsis [Strashes one logic node using its SOP.] Description [] diff --git a/src/aig/kit/kitTruth.c b/src/aig/kit/kitTruth.c index d41e5d4e..d196b455 100644 --- a/src/aig/kit/kitTruth.c +++ b/src/aig/kit/kitTruth.c @@ -845,7 +845,7 @@ void Kit_TruthForallSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned /**Function************************************************************* - Synopsis [Computes negative cofactor of the function.] + Synopsis [Multiplexes two functions with the given variable.] Description [] diff --git a/src/aig/rwt/rwt.h b/src/aig/rwt/rwt.h index 42a57ad6..9199ff2a 100644 --- a/src/aig/rwt/rwt.h +++ b/src/aig/rwt/rwt.h @@ -30,6 +30,7 @@ extern "C" { //////////////////////////////////////////////////////////////////////// #include "mem.h" +#include "extra.h" #include "vec.h" //////////////////////////////////////////////////////////////////////// |