diff options
Diffstat (limited to 'src')
81 files changed, 3051 insertions, 847 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" //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abcFanio.c b/src/base/abc/abcFanio.c index ff6d0590..c8536695 100644 --- a/src/base/abc/abcFanio.c +++ b/src/base/abc/abcFanio.c @@ -30,6 +30,45 @@ /**Function************************************************************* + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_IntPushMem( Extra_MmStep_t * pMemMan, Vec_Int_t * p, int Entry ) +{ + if ( p->nSize == p->nCap ) + { + int * pArray; + int i; + + if ( p->nSize == 0 ) + p->nCap = 1; + if ( pMemMan ) + pArray = (int *)Extra_MmStepEntryFetch( pMemMan, p->nCap * 8 ); + else + pArray = ALLOC( int, p->nCap * 2 ); + if ( p->pArray ) + { + for ( i = 0; i < p->nSize; i++ ) + pArray[i] = p->pArray[i]; + if ( pMemMan ) + Extra_MmStepEntryRecycle( pMemMan, (char *)p->pArray, p->nCap * 4 ); + else + free( p->pArray ); + } + p->nCap *= 2; + p->pArray = pArray; + } + p->pArray[p->nSize++] = Entry; +} + +/**Function************************************************************* + Synopsis [Creates fanout/fanin relationship between the nodes.] Description [] diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 571aa02c..22a8ad54 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -115,6 +115,7 @@ static int Abc_CommandIRewrite ( Abc_Frame_t * pAbc, int argc, char ** arg static int Abc_CommandDRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDRefactor ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDCompress2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandDChoice ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandDrwsat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIRewriteSeq ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandIResyn ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -283,6 +284,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "New AIG", "drw", Abc_CommandDRewrite, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "drf", Abc_CommandDRefactor, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "dcompress2", Abc_CommandDCompress2, 1 ); + Cmd_CommandAdd( pAbc, "New AIG", "dchoice", Abc_CommandDChoice, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "drwsat", Abc_CommandDrwsat, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "irws", Abc_CommandIRewriteSeq, 1 ); Cmd_CommandAdd( pAbc, "New AIG", "iresyn", Abc_CommandIResyn, 1 ); @@ -2977,8 +2979,8 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); - printf("This command will be available soon\n"); - return 0; +// printf("This command will be available soon\n"); +// return 0; // set defaults memset( pPars, 0, sizeof(Lpk_Par_t) ); @@ -6177,6 +6179,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Ntk_t * pNtk, * pNtkRes; int c; int nLevels; + int fVerbose; // extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ); // extern Abc_Ntk_t * Abc_NtkIvy( Abc_Ntk_t * pNtk ); // extern void Abc_NtkMaxFlowTest( Abc_Ntk_t * pNtk ); @@ -6187,15 +6190,17 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ); extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose ); + extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults + fVerbose = 0; nLevels = 1000; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Nh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Nvh" ) ) != EOF ) { switch ( c ) { @@ -6210,6 +6215,9 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nLevels < 0 ) goto usage; break; + case 'v': + fVerbose ^= 1; + break; case 'h': goto usage; default: @@ -6311,7 +6319,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) } // pNtkRes = Abc_NtkDar( pNtk ); - pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 ); +// pNtkRes = Abc_NtkDarRetime( pNtk, nLevels, 1 ); + pNtkRes = Abc_NtkPcmTest( pNtk, fVerbose ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); @@ -6323,6 +6332,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: fprintf( pErr, "usage: test [-h]\n" ); fprintf( pErr, "\t testbench for new procedures\n" ); + fprintf( pErr, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } @@ -7138,6 +7148,84 @@ usage: return 1; } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandDChoice( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pOut, * pErr; + Abc_Ntk_t * pNtk, * pNtkRes; + int fBalance, fVerbose, fUpdateLevel, c; + + extern Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose ); + + pNtk = Abc_FrameReadNtk(pAbc); + pOut = Abc_FrameReadOut(pAbc); + pErr = Abc_FrameReadErr(pAbc); + + // set defaults + fBalance = 1; + fUpdateLevel = 1; + fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "blvh" ) ) != EOF ) + { + switch ( c ) + { + case 'b': + fBalance ^= 1; + break; + case 'l': + fUpdateLevel ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pNtk == NULL ) + { + fprintf( pErr, "Empty network.\n" ); + return 1; + } + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "This command works only for strashed networks.\n" ); + return 1; + } + pNtkRes = Abc_NtkDChoice( pNtk, fBalance, fUpdateLevel, fVerbose ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Command has failed.\n" ); + return 0; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; + +usage: + fprintf( pErr, "usage: dchoice [-blvh]\n" ); + fprintf( pErr, "\t performs partitioned choicing using a new AIG package\n" ); + fprintf( pErr, "\t-b : toggle internal balancing [default = %s]\n", fBalance? "yes": "no" ); + fprintf( pErr, "\t-l : toggle updating level [default = %s]\n", fUpdateLevel? "yes": "no" ); + fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] @@ -11819,24 +11907,24 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - nFrames = 0; // if 0, iterates through frames + nFrames =16; fRetimeFirst = 1; fVerbose = 0; fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Krwvh" ) ) != EOF ) { switch ( c ) { - case 'F': + case 'K': if ( globalUtilOptind >= argc ) { - fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" ); goto usage; } nFrames = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nFrames <= 0 ) + if ( nFrames < 0 ) goto usage; break; case 'r': @@ -11872,9 +11960,9 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: dsec [-F num] [-rwvh] <file1> <file2>\n" ); + fprintf( pErr, "usage: dsec [-K num] [-rwvh] <file1> <file2>\n" ); fprintf( pErr, "\t performs inductive sequential equivalence checking\n" ); - fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames ); + fprintf( pErr, "\t-K num : the limit on the depth of induction [default = %d]\n", nFrames ); fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" ); @@ -11914,24 +12002,24 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) pErr = Abc_FrameReadErr(pAbc); // set defaults - nFrames = 0; // if 0, iterates through frames - fRetimeFirst = 1; - fVerbose = 0; - fVeryVerbose = 0; + nFrames = 16; + fRetimeFirst = 1; + fVerbose = 0; + fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Frwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Krwvh" ) ) != EOF ) { switch ( c ) { - case 'F': + case 'K': if ( globalUtilOptind >= argc ) { - fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); + fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" ); goto usage; } nFrames = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nFrames <= 0 ) + if ( nFrames < 0 ) goto usage; break; case 'r': @@ -11964,9 +12052,9 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: dprove [-F num] [-rwvh]\n" ); + fprintf( pErr, "usage: dprove [-K num] [-rwvh]\n" ); fprintf( pErr, "\t performs SEC on the sequential miter\n" ); - fprintf( pErr, "\t-F num : the number of time frames to use [default = %d]\n", nFrames ); + fprintf( pErr, "\t-K num : the limit on the depth of induction [default = %d]\n", nFrames ); fprintf( pErr, "\t-r : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" ); fprintf( pErr, "\t-v : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" ); fprintf( pErr, "\t-w : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index f8f7d20e..356a5565 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -67,6 +67,7 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters ) } // create the manager pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 ); + pMan->pName = Extra_UtilStrsav( pNtk->pName ); // save the number of registers if ( fRegisters ) pMan->nRegs = Abc_NtkLatchNum(pNtk); @@ -250,6 +251,7 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) Aig_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew); Aig_ManForEachPi( pMan, pObj, i ) pObj->pData = Abc_NtkCi(pNtkNew, i); + // rebuild the AIG vNodes = Aig_ManDfsChoices( pMan ); Vec_PtrForEachEntry( vNodes, pObj, i ) @@ -265,21 +267,8 @@ Abc_Ntk_t * Abc_NtkFromDarChoices( Abc_Ntk_t * pNtkOld, Aig_Man_t * pMan ) pAbcRepr->pData = pAbcObj; } } -printf( "Total = %d. Collected = %d.\n", Aig_ManNodeNum(pMan), Vec_PtrSize(vNodes) ); +//printf( "Total = %d. Collected = %d.\n", Aig_ManNodeNum(pMan), Vec_PtrSize(vNodes) ); Vec_PtrFree( vNodes ); -/* - { - Abc_Obj_t * pNode; - int k, Counter = 0; - Abc_NtkForEachNode( pNtkNew, pNode, k ) - if ( pNode->pData != 0 ) - { - int x = 0; - Counter++; - } - printf( "Choices = %d.\n", Counter ); - } -*/ // connect the PO nodes Aig_ManForEachPo( pMan, pObj, i ) Abc_ObjAddFanin( Abc_NtkCo(pNtkNew, i), (Abc_Obj_t *)Aig_ObjChild0Copy(pObj) ); @@ -496,11 +485,11 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in return NULL; Fra_ParamsDefault( pPars ); pPars->nBTLimitNode = nConfLimit; - pPars->fVerbose = fVerbose; - pPars->fProve = fProve; + pPars->fChoicing = fChoicing; pPars->fDoSparse = fDoSparse; pPars->fSpeculate = fSpeculate; - pPars->fChoicing = fChoicing; + pPars->fProve = fProve; + pPars->fVerbose = fVerbose; pMan = Fra_FraigPerform( pTemp = pMan, pPars ); if ( fChoicing ) pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan ); @@ -631,7 +620,7 @@ clk = clock(); ***********************************************************************/ Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose ) { - Aig_Man_t * pMan;//, * pTemp; + Aig_Man_t * pMan, * pTemp; Abc_Ntk_t * pNtkAig; int clk; assert( Abc_NtkIsStrash(pNtk) ); @@ -641,8 +630,8 @@ Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, // Aig_ManPrintStats( pMan ); clk = clock(); - pMan = Dar_ManCompress2( pMan, fBalance, fUpdateLevel, fVerbose ); -// Aig_ManStop( pTemp ); + pMan = Dar_ManCompress2( pTemp = pMan, fBalance, fUpdateLevel, fVerbose ); + Aig_ManStop( pTemp ); //PRT( "time", clock() - clk ); // Aig_ManPrintStats( pMan ); @@ -662,9 +651,35 @@ clk = clock(); SeeAlso [] ***********************************************************************/ +Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, int fVerbose ) +{ + Aig_Man_t * pMan, * pTemp; + Abc_Ntk_t * pNtkAig; + assert( Abc_NtkIsStrash(pNtk) ); + pMan = Abc_NtkToDar( pNtk, 0 ); + if ( pMan == NULL ) + return NULL; + pMan = Dar_ManChoice( pTemp = pMan, fBalance, fUpdateLevel, fVerbose ); + Aig_ManStop( pTemp ); + pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan ); + Aig_ManStop( pMan ); + return pNtkAig; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose ) { - Aig_Man_t * pMan;//, * pTemp; + Aig_Man_t * pMan, * pTemp; Abc_Ntk_t * pNtkAig; int clk; assert( Abc_NtkIsStrash(pNtk) ); @@ -674,8 +689,8 @@ Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose ) // Aig_ManPrintStats( pMan ); clk = clock(); - pMan = Dar_ManRwsat( pMan, fBalance, fVerbose ); -// Aig_ManStop( pTemp ); + pMan = Dar_ManRwsat( pTemp = pMan, fBalance, fVerbose ); + Aig_ManStop( pTemp ); //PRT( "time", clock() - clk ); // Aig_ManPrintStats( pMan ); @@ -1118,8 +1133,10 @@ Abc_Ntk_t * Abc_NtkDarLatchSweep( Abc_Ntk_t * pNtk, int fLatchSweep, int fVerbos Aig_ManSeqCleanup( pMan ); if ( fLatchSweep ) { - pMan = Aig_ManReduceLaches( pMan, fVerbose ); - pMan = Aig_ManConstReduce( pMan, fVerbose ); + if ( pMan->nRegs ) + pMan = Aig_ManReduceLaches( pMan, fVerbose ); + if ( pMan->nRegs ) + pMan = Aig_ManConstReduce( pMan, fVerbose ); } pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan ); Aig_ManStop( pMan ); diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c index 64cb2b38..be8a25f1 100644 --- a/src/base/abci/abcFraig.c +++ b/src/base/abci/abcFraig.c @@ -673,7 +673,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtkAdd ) } } Vec_PtrPush( vStore, pNtk ); - printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pNtk) ); +// printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pNtk) ); return 1; } @@ -704,9 +704,15 @@ Abc_Ntk_t * Abc_NtkFraigRestore() printf( "There are no network currently in storage.\n" ); return NULL; } - printf( "Currently stored %d networks will be fraiged.\n", Vec_PtrSize(vStore) ); +// printf( "Currently stored %d networks will be fraiged.\n", Vec_PtrSize(vStore) ); pNtk = Vec_PtrEntry( vStore, 0 ); + // swap the first and last network + // this should lead to the primary choice being "better" because of synthesis + pNtk = Vec_PtrPop( vStore ); + Vec_PtrPush( vStore, Vec_PtrEntry(vStore,0) ); + Vec_PtrWriteEntry( vStore, 0, pNtk ); + // to determine the number of simulation patterns // use the following strategy // at least 64 words (32 words random and 32 words dynamic) @@ -731,7 +737,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore() // perform partitioned computation of structural choices pFraig = Abc_NtkFraigPartitioned( vStore, &Params ); Abc_NtkFraigStoreClean(); -PRT( "Total choicing time", clock() - clk ); +//PRT( "Total choicing time", clock() - clk ); return pFraig; } diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c index a9c42ceb..bb56c22c 100644 --- a/src/base/abci/abcIf.c +++ b/src/base/abci/abcIf.c @@ -299,12 +299,8 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t } else { - extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph ); - // transform truth table into the decomposition tree - Kit_Graph_t * pGraph = Kit_TruthToGraph( If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), vCover ); - // derive the AIG for the decomposition tree - pNodeNew->pData = Kit_GraphToHop( pNtkNew->pManFunc, pGraph ); - Kit_GraphFree( pGraph ); + extern Hop_Obj_t * Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory ); + pNodeNew->pData = Kit_TruthToHop( pNtkNew->pManFunc, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), vCover ); } // complement the node if the cut was complemented if ( pCutBest->fCompl ) diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c index 6d4e480b..b839f812 100644 --- a/src/base/abci/abcQbf.c +++ b/src/base/abci/abcQbf.c @@ -140,7 +140,7 @@ clkV = clock() - clkV; printf( "AIG = %6d ", Abc_NtkNodeNum(pNtkSyn) ); Abc_NtkVectorPrintVars( pNtk, vPiValues, nPars ); printf( " " ); - PRTn( "Syn", clkS ); +// PRTn( "Syn", clkS ); PRT( "Ver", clkV ); } } diff --git a/src/base/io/ioWriteAiger.c b/src/base/io/ioWriteAiger.c index 958e3d96..e805fbc2 100644 --- a/src/base/io/ioWriteAiger.c +++ b/src/base/io/ioWriteAiger.c @@ -249,8 +249,8 @@ void Io_WriteAiger( Abc_Ntk_t * pNtk, char * pFileName, int fWriteSymbols ) // write the comment fprintf( pFile, "c\n" ); fprintf( pFile, "%s\n", pNtk->pName ); - fprintf( pFile, "This file in the AIGER format was written by ABC on %s\n", Extra_TimeStamp() ); - fprintf( pFile, "For information about the format, refer to %s\n", "http://fmv.jku.at/aiger" ); + fprintf( pFile, "This file was produced by ABC on %s\n", Extra_TimeStamp() ); + fprintf( pFile, "For information about AIGER format, refer to %s\n", "http://fmv.jku.at/aiger" ); fclose( pFile ); } diff --git a/src/map/fpga/fpgaLib.c b/src/map/fpga/fpgaLib.c index 8ac66cdc..e74def32 100644 --- a/src/map/fpga/fpgaLib.c +++ b/src/map/fpga/fpgaLib.c @@ -129,7 +129,7 @@ Fpga_LutLib_t * Fpga_LutLibCreate( char * FileName, int fVerbose ) printf( "Warning: Pin %d of LUT %d has delay %f. Pin delays should be non-negative numbers. Technology mapping may not work correctly.\n", k, i, p->pLutDelays[i][k] ); if ( k && p->pLutDelays[i][k-1] > p->pLutDelays[i][k] ) - printf( "Warning: Pin %d of LUT %d has delay %f. Pin %d of LUT %d has delay %f. Pin delays should be in non-degreasing order. Technology mapping may not work correctly.\n", + printf( "Warning: Pin %d of LUT %d has delay %f. Pin %d of LUT %d has delay %f. Pin delays should be in non-decreasing order. Technology mapping may not work correctly.\n", k-1, i, p->pLutDelays[i][k-1], k, i, p->pLutDelays[i][k] ); } diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c index 14267f8e..b713d80d 100644 --- a/src/map/if/ifMan.c +++ b/src/map/if/ifMan.c @@ -363,7 +363,7 @@ void If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId ) if ( p->pPars->fTruth ) { int i, nTruthWords; - nTruthWords = Extra_TruthWordNum( pCut->nLimit ); + nTruthWords = pCut->nLimit <= 5 ? 1 : (1 << (pCut->nLimit - 5)); for ( i = 0; i < nTruthWords; i++ ) If_CutTruth(pCut)[i] = 0xAAAAAAAA; } diff --git a/src/map/if/ifTime.c b/src/map/if/ifTime.c index d60d8a9d..60417c67 100644 --- a/src/map/if/ifTime.c +++ b/src/map/if/ifTime.c @@ -172,7 +172,7 @@ void If_CutPropagateRequired( If_Man_t * p, If_Cut_t * pCut, float ObjRequired ) /**Function************************************************************* - Synopsis [Sorts the pins in the degreasing order of delays.] + Synopsis [Sorts the pins in the decreasing order of delays.] Description [] diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c index c2f3196b..5587e3ff 100644 --- a/src/map/if/ifTruth.c +++ b/src/map/if/ifTruth.c @@ -30,6 +30,134 @@ /**Function************************************************************* + Synopsis [Several simple procedures working with truth tables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int If_TruthWordNum( int nVars ) { return nVars <= 5 ? 1 : (1 << (nVars - 5)); } +static inline void If_TruthNot( unsigned * pOut, unsigned * pIn, int nVars ) +{ + int w; + for ( w = If_TruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = ~pIn[w]; +} +static inline void If_TruthCopy( unsigned * pOut, unsigned * pIn, int nVars ) +{ + int w; + for ( w = If_TruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = pIn[w]; +} +static inline void If_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars ) +{ + int w; + for ( w = If_TruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = ~(pIn0[w] & pIn1[w]); +} +static inline void If_TruthAnd( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars ) +{ + int w; + for ( w = If_TruthWordNum(nVars)-1; w >= 0; w-- ) + pOut[w] = pIn0[w] & pIn1[w]; +} + +/**Function************************************************************* + + Synopsis [Swaps two adjacent variables in the truth table.] + + Description [Swaps var number Start and var number Start+1 (0-based numbers). + The input truth table is pIn. The output truth table is pOut.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int iVar ) +{ + static unsigned PMasks[4][3] = { + { 0x99999999, 0x22222222, 0x44444444 }, + { 0xC3C3C3C3, 0x0C0C0C0C, 0x30303030 }, + { 0xF00FF00F, 0x00F000F0, 0x0F000F00 }, + { 0xFF0000FF, 0x0000FF00, 0x00FF0000 } + }; + int nWords = If_TruthWordNum( nVars ); + int i, k, Step, Shift; + + assert( iVar < nVars - 1 ); + if ( iVar < 4 ) + { + Shift = (1 << iVar); + for ( i = 0; i < nWords; i++ ) + pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift); + } + else if ( iVar > 4 ) + { + Step = (1 << (iVar - 5)); + for ( k = 0; k < nWords; k += 4*Step ) + { + for ( i = 0; i < Step; i++ ) + pOut[i] = pIn[i]; + for ( i = 0; i < Step; i++ ) + pOut[Step+i] = pIn[2*Step+i]; + for ( i = 0; i < Step; i++ ) + pOut[2*Step+i] = pIn[Step+i]; + for ( i = 0; i < Step; i++ ) + pOut[3*Step+i] = pIn[3*Step+i]; + pIn += 4*Step; + pOut += 4*Step; + } + } + else // if ( iVar == 4 ) + { + for ( i = 0; i < nWords; i += 2 ) + { + pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16); + pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16); + } + } +} + +/**Function************************************************************* + + Synopsis [Expands the truth table according to the phase.] + + Description [The input and output truth tables are in pIn/pOut. The current number + of variables is nVars. The total number of variables in nVarsAll. The last argument + (Phase) contains shows where the variables should go.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase ) +{ + unsigned * pTemp; + int i, k, Var = nVars - 1, Counter = 0; + for ( i = nVarsAll - 1; i >= 0; i-- ) + if ( Phase & (1 << i) ) + { + for ( k = Var; k < i; k++ ) + { + If_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k ); + pTemp = pIn; pIn = pOut; pOut = pTemp; + Counter++; + } + Var--; + } + assert( Var == -1 ); + // swap if it was moved an even number of times + if ( !(Counter & 1) ) + If_TruthCopy( pOut, pIn, nVarsAll ); +} + +/**Function************************************************************* + Synopsis [Computes the stretching phase of the cut w.r.t. the merged cut.] Description [] @@ -39,7 +167,7 @@ SeeAlso [] ***********************************************************************/ -static inline unsigned Cut_TruthPhase( If_Cut_t * pCut, If_Cut_t * pCut1 ) +static inline unsigned If_CutTruthPhase( If_Cut_t * pCut, If_Cut_t * pCut1 ) { unsigned uPhase = 0; int i, k; @@ -73,22 +201,22 @@ void If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut // permute the first table if ( fCompl0 ^ pCut0->fCompl ) - Extra_TruthNot( p->puTemp[0], If_CutTruth(pCut0), pCut->nLimit ); + If_TruthNot( p->puTemp[0], If_CutTruth(pCut0), pCut->nLimit ); else - Extra_TruthCopy( p->puTemp[0], If_CutTruth(pCut0), pCut->nLimit ); - Extra_TruthStretch( p->puTemp[2], p->puTemp[0], pCut0->nLeaves, pCut->nLimit, Cut_TruthPhase(pCut, pCut0) ); + If_TruthCopy( p->puTemp[0], If_CutTruth(pCut0), pCut->nLimit ); + If_TruthStretch( p->puTemp[2], p->puTemp[0], pCut0->nLeaves, pCut->nLimit, If_CutTruthPhase(pCut, pCut0) ); // permute the second table if ( fCompl1 ^ pCut1->fCompl ) - Extra_TruthNot( p->puTemp[1], If_CutTruth(pCut1), pCut->nLimit ); + If_TruthNot( p->puTemp[1], If_CutTruth(pCut1), pCut->nLimit ); else - Extra_TruthCopy( p->puTemp[1], If_CutTruth(pCut1), pCut->nLimit ); - Extra_TruthStretch( p->puTemp[3], p->puTemp[1], pCut1->nLeaves, pCut->nLimit, Cut_TruthPhase(pCut, pCut1) ); + If_TruthCopy( p->puTemp[1], If_CutTruth(pCut1), pCut->nLimit ); + If_TruthStretch( p->puTemp[3], p->puTemp[1], pCut1->nLeaves, pCut->nLimit, If_CutTruthPhase(pCut, pCut1) ); // produce the resulting table assert( pCut->fCompl == 0 ); if ( pCut->fCompl ) - Extra_TruthNand( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit ); + If_TruthNand( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit ); else - Extra_TruthAnd( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit ); + If_TruthAnd( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit ); // perform // Kit_FactorTest( If_CutTruth(pCut), pCut->nLimit ); diff --git a/src/map/pcm/module.make b/src/map/pcm/module.make new file mode 100644 index 00000000..e69de29b --- /dev/null +++ b/src/map/pcm/module.make diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h index f23cc178..40b46bc5 100644 --- a/src/misc/vec/vec.h +++ b/src/misc/vec/vec.h @@ -25,12 +25,50 @@ extern "C" { #endif +#ifdef _WIN32 +#define inline __inline // compatible with MS VS 6.0 +#endif + //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// -#ifdef _WIN32 -#define inline __inline // compatible with MS VS 6.0 +// this include should be the first one in the list +// it is used to catch memory leaks on Windows +#include "leaks.h" + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +#ifndef ABS +#define ABS(a) ((a) < 0 ? -(a) : (a)) +#endif + +#ifndef MAX +#define MAX(a,b) ((a) > (b) ? (a) : (b)) +#endif + +#ifndef MIN +#define MIN(a,b) ((a) < (b) ? (a) : (b)) +#endif + +#ifndef ALLOC +#define ALLOC(type, num) ((type *) malloc(sizeof(type) * (num))) +#endif + +#ifndef FREE +#define FREE(obj) ((obj) ? (free((char *) (obj)), (obj) = 0) : 0) +#endif + +#ifndef REALLOC +#define REALLOC(type, obj, num) \ + ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \ + ((type *) malloc(sizeof(type) * (num)))) +#endif + +#ifndef PRT +#define PRT(a,t) printf("%s = ", (a)); printf("%6.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)) #endif #include "vecInt.h" @@ -49,10 +87,6 @@ extern "C" { //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// -/// MACRO DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -//////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// diff --git a/src/misc/vec/vecFlt.h b/src/misc/vec/vecFlt.h index 1c9980e9..6b36ce84 100644 --- a/src/misc/vec/vecFlt.h +++ b/src/misc/vec/vecFlt.h @@ -456,41 +456,6 @@ static inline void Vec_FltPush( Vec_Flt_t * p, float Entry ) SeeAlso [] ***********************************************************************/ -static inline void Vec_FltPushMem( Extra_MmStep_t * pMemMan, Vec_Flt_t * p, float Entry ) -{ - if ( p->nSize == p->nCap ) - { - float * pArray; - int i; - - if ( p->nSize == 0 ) - p->nCap = 1; - pArray = (float *)Extra_MmStepEntryFetch( pMemMan, p->nCap * 8 ); -// pArray = ALLOC( float, p->nCap * 2 ); - if ( p->pArray ) - { - for ( i = 0; i < p->nSize; i++ ) - pArray[i] = p->pArray[i]; - Extra_MmStepEntryRecycle( pMemMan, (char *)p->pArray, p->nCap * 4 ); -// free( p->pArray ); - } - p->nCap *= 2; - p->pArray = pArray; - } - p->pArray[p->nSize++] = Entry; -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ static inline void Vec_FltPushOrder( Vec_Flt_t * p, float Entry ) { int i; diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index df6f824c..d1321c62 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -26,7 +26,6 @@ //////////////////////////////////////////////////////////////////////// #include <stdio.h> -#include "extra.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// @@ -477,45 +476,6 @@ static inline void Vec_IntPushFirst( Vec_Int_t * p, int Entry ) /**Function************************************************************* - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Vec_IntPushMem( Extra_MmStep_t * pMemMan, Vec_Int_t * p, int Entry ) -{ - if ( p->nSize == p->nCap ) - { - int * pArray; - int i; - - if ( p->nSize == 0 ) - p->nCap = 1; - if ( pMemMan ) - pArray = (int *)Extra_MmStepEntryFetch( pMemMan, p->nCap * 8 ); - else - pArray = ALLOC( int, p->nCap * 2 ); - if ( p->pArray ) - { - for ( i = 0; i < p->nSize; i++ ) - pArray[i] = p->pArray[i]; - if ( pMemMan ) - Extra_MmStepEntryRecycle( pMemMan, (char *)p->pArray, p->nCap * 4 ); - else - free( p->pArray ); - } - p->nCap *= 2; - p->pArray = pArray; - } - p->pArray[p->nSize++] = Entry; -} - -/**Function************************************************************* - Synopsis [Inserts the entry while preserving the increasing order.] Description [] diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h index 38ac171d..ecf29f32 100644 --- a/src/misc/vec/vecStr.h +++ b/src/misc/vec/vecStr.h @@ -401,6 +401,27 @@ static inline void Vec_StrPush( Vec_Str_t * p, char Entry ) p->pArray[p->nSize++] = Entry; } +/**Function******************************************************************** + + Synopsis [Finds the smallest integer larger of equal than the logarithm.] + + Description [Returns [Log10(Num)].] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +static inline Vec_StrBase10Log( unsigned Num ) +{ + int Res; + assert( Num >= 0 ); + if ( Num == 0 ) return 0; + if ( Num == 1 ) return 1; + for ( Res = 0, Num--; Num; Num /= 10, Res++ ); + return Res; +} /* end of Extra_Base2Log */ + /**Function************************************************************* Synopsis [] @@ -425,7 +446,7 @@ static inline void Vec_StrPrintNum( Vec_Str_t * p, int Num ) Vec_StrPush( p, (char)('0' + Num) ); return; } - nDigits = Extra_Base10Log( Num ); + nDigits = Vec_StrBase10Log( Num ); Vec_StrGrow( p, p->nSize + nDigits ); for ( i = nDigits - 1; i >= 0; i-- ) { diff --git a/src/opt/lpk/lpkAbcDec.c b/src/opt/lpk/lpkAbcDec.c index 831097b0..e9f8d0df 100644 --- a/src/opt/lpk/lpkAbcDec.c +++ b/src/opt/lpk/lpkAbcDec.c @@ -17,7 +17,7 @@ Revision [$Id: lpkAbcDec.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] ***********************************************************************/ - + #include "lpkInt.h" //////////////////////////////////////////////////////////////////////// @@ -41,24 +41,29 @@ ***********************************************************************/ Abc_Obj_t * Lpk_ImplementFun( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Lpk_Fun_t * p ) { + extern Hop_Obj_t * Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory ); + unsigned * pTruth; Abc_Obj_t * pObjNew; int i; + // create the new node pObjNew = Abc_NtkCreateNode( pNtk ); for ( i = 0; i < (int)p->nVars; i++ ) Abc_ObjAddFanin( pObjNew, Vec_PtrEntry(vLeaves, p->pFanins[i]) ); Abc_ObjLevelNew( pObjNew ); - // create the logic function + // assign the node's function + pTruth = Lpk_FunTruth(p, 0); + if ( p->nVars == 0 ) { - extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph ); - // allocate memory for the ISOP - Vec_Int_t * vCover = Vec_IntAlloc( 0 ); - // transform truth table into the decomposition tree - Kit_Graph_t * pGraph = Kit_TruthToGraph( Lpk_FunTruth(p, 0), p->nVars, vCover ); - // derive the AIG for the decomposition tree - pObjNew->pData = Kit_GraphToHop( pNtk->pManFunc, pGraph ); - Kit_GraphFree( pGraph ); - Vec_IntFree( vCover ); + pObjNew->pData = Hop_NotCond( Hop_ManConst1(pNtk->pManFunc), !(pTruth[0] & 1) ); + return pObjNew; } + if ( p->nVars == 1 ) + { + pObjNew->pData = Hop_NotCond( Hop_ManPi(pNtk->pManFunc, 0), (pTruth[0] & 1) ); + return pObjNew; + } + // create the logic function + pObjNew->pData = Kit_TruthToHop( pNtk->pManFunc, pTruth, p->nVars, NULL ); return pObjNew; } @@ -85,6 +90,7 @@ Abc_Obj_t * Lpk_Implement( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, int nLeavesOld Vec_PtrWriteEntry( vLeaves, i, pRes ); Lpk_FunFree( pFun ); } + Vec_PtrShrink( vLeaves, nLeavesOld ); return pRes; } @@ -92,7 +98,9 @@ Abc_Obj_t * Lpk_Implement( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, int nLeavesOld Synopsis [Decomposes the function using recursive MUX decomposition.] - Description [] + Description [Returns the ID of the top-most decomposition node + implementing this function, or 0 if there is no decomposition satisfying + the constraints on area and delay.] SideEffects [] @@ -101,22 +109,78 @@ Abc_Obj_t * Lpk_Implement( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, int nLeavesOld ***********************************************************************/ int Lpk_Decompose_rec( Lpk_Fun_t * p ) { + Lpk_Res_t * pResMux, * pResDsd; Lpk_Fun_t * p2; - int VarPol; - assert( p->nAreaLim > 0 ); - if ( p->nVars <= p->nLutK ) - return 1; - // check if decomposition exists - VarPol = Lpk_MuxAnalize( p ); - if ( VarPol == -1 ) + // is only called for non-trivial blocks + assert( p->nLutK >= 3 && p->nLutK <= 6 ); + assert( p->nVars > p->nLutK ); + // skip if area bound is exceeded + if ( Lpk_LutNumLuts(p->nVars, p->nLutK) > (int)p->nAreaLim ) return 0; - // split and call recursively - p2 = Lpk_MuxSplit( p, VarPol ); - if ( !Lpk_Decompose_rec( p2 ) ) + // skip if delay bound is exceeded + if ( Lpk_SuppDelay(p->uSupp, p->pDelays) > (int)p->nDelayLim ) return 0; - return Lpk_Decompose_rec( p ); + // check MUX decomposition + pResMux = Lpk_MuxAnalize( p ); + assert( !pResMux || (pResMux->DelayEst <= (int)p->nDelayLim && pResMux->AreaEst <= (int)p->nAreaLim) ); + // accept MUX decomposition if it is "good" + if ( pResMux && pResMux->nSuppSizeS <= (int)p->nLutK && pResMux->nSuppSizeL <= (int)p->nLutK ) + pResDsd = NULL; + else + { + pResDsd = Lpk_DsdAnalize( p ); + assert( !pResDsd || (pResDsd->DelayEst <= (int)p->nDelayLim && pResDsd->AreaEst <= (int)p->nAreaLim) ); + } + if ( pResMux && pResDsd ) + { + // compare two decompositions + if ( pResMux->AreaEst < pResDsd->AreaEst || + (pResMux->AreaEst == pResDsd->AreaEst && pResMux->nSuppSizeL < pResDsd->nSuppSizeL) || + (pResMux->AreaEst == pResDsd->AreaEst && pResMux->nSuppSizeL == pResDsd->nSuppSizeL && pResMux->DelayEst < pResDsd->DelayEst) ) + pResDsd = NULL; + else + pResMux = NULL; + } + assert( pResMux == NULL || pResDsd == NULL ); + if ( pResMux ) + { + p2 = Lpk_MuxSplit( p, pResMux->pCofVars[0], pResMux->Polarity ); + if ( p2->nVars > p->nLutK && !Lpk_Decompose_rec( p2 ) ) + return 0; + if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( p ) ) + return 0; + return 1; + } + if ( pResDsd ) + { + p2 = Lpk_DsdSplit( p, pResDsd->pCofVars, pResDsd->nCofVars, pResDsd->BSVars ); + assert( p2->nVars <= (int)p->nLutK ); + if ( p->nVars > p->nLutK && !Lpk_Decompose_rec( p ) ) + return 0; + return 1; + } + return 0; } +/**Function************************************************************* + + Synopsis [Removes decomposed nodes from the array of fanins.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_DecomposeClean( Vec_Ptr_t * vLeaves, int nLeavesOld ) +{ + Lpk_Fun_t * pFunc; + int i; + Vec_PtrForEachEntryStart( vLeaves, pFunc, i, nLeavesOld ) + Lpk_FunFree( pFunc ); + Vec_PtrShrink( vLeaves, nLeavesOld ); +} /**Function************************************************************* @@ -131,22 +195,16 @@ int Lpk_Decompose_rec( Lpk_Fun_t * p ) ***********************************************************************/ Abc_Obj_t * Lpk_Decompose( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim ) { - Lpk_Fun_t * p; + Lpk_Fun_t * pFun; Abc_Obj_t * pObjNew = NULL; - int i, nLeaves; - // create the starting function - nLeaves = Vec_PtrSize( vLeaves ); - p = Lpk_FunCreate( pNtk, vLeaves, pTruth, nLutK, AreaLim, DelayLim ); - Lpk_FunSuppMinimize( p ); - // decompose the function - if ( Lpk_Decompose_rec(p) ) + int nLeaves = Vec_PtrSize( vLeaves ); + pFun = Lpk_FunCreate( pNtk, vLeaves, pTruth, nLutK, AreaLim, DelayLim ); + Lpk_FunSuppMinimize( pFun ); + if ( pFun->nVars <= pFun->nLutK ) + pObjNew = Lpk_ImplementFun( pNtk, vLeaves, pFun ); + else if ( Lpk_Decompose_rec(pFun) ) pObjNew = Lpk_Implement( pNtk, vLeaves, nLeaves ); - else - { - for ( i = Vec_PtrSize(vLeaves) - 1; i >= nLeaves; i-- ) - Lpk_FunFree( Vec_PtrEntry(vLeaves, i) ); - } - Vec_PtrShrink( vLeaves, nLeaves ); + Lpk_DecomposeClean( vLeaves, nLeaves ); return pObjNew; } diff --git a/src/opt/lpk/lpkAbcDsd.c b/src/opt/lpk/lpkAbcDsd.c index 8de8391f..f2e19945 100644 --- a/src/opt/lpk/lpkAbcDsd.c +++ b/src/opt/lpk/lpkAbcDsd.c @@ -30,9 +30,11 @@ /**Function************************************************************* - Synopsis [Returns the variable whose cofs have min sum of supp sizes.] + Synopsis [Cofactors TTs w.r.t. all vars and finds the best var.] - Description [] + Description [The best variable is the variable with the minimum + sum total of the support sizes of all truth tables. This procedure + computes and returns cofactors w.r.t. the best variable.] SideEffects [] @@ -42,6 +44,7 @@ int Lpk_FunComputeMinSuppSizeVar( Lpk_Fun_t * p, unsigned ** ppTruths, int nTruths, unsigned ** ppCofs ) { int i, Var, VarBest, nSuppSize0, nSuppSize1, nSuppTotalMin, nSuppTotalCur, nSuppMaxMin, nSuppMaxCur; + assert( nTruths > 0 ); VarBest = -1; Lpk_SuppForEachVar( p->uSupp, Var ) { @@ -85,7 +88,7 @@ int Lpk_FunComputeMinSuppSizeVar( Lpk_Fun_t * p, unsigned ** ppTruths, int nTrut SeeAlso [] ***********************************************************************/ -unsigned Lpk_ComputeBoundSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets ) +unsigned Lpk_ComputeBoundSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets, int nSizeMax ) { unsigned i, iLitFanin, uSupport, uSuppCur; Kit_DsdObj_t * pObj; @@ -99,7 +102,7 @@ unsigned Lpk_ComputeBoundSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets uSupport = 0; Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i ) { - uSupps[i] = Lpk_ComputeBoundSets_rec( p, iLitFanin, vSets ); + uSupps[i] = Lpk_ComputeBoundSets_rec( p, iLitFanin, vSets, nSizeMax ); uSupport |= uSupps[i]; } // create all subsets, except empty and full @@ -110,7 +113,8 @@ unsigned Lpk_ComputeBoundSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets for ( i = 0; i < pObj->nFans; i++ ) if ( s & (1 << i) ) uSuppCur |= uSupps[i]; - Vec_IntPush( vSets, uSuppCur ); + if ( Kit_WordCountOnes(uSuppCur) <= nSizeMax ) + Vec_IntPush( vSets, uSuppCur ); } return uSupport; } @@ -119,9 +123,10 @@ unsigned Lpk_ComputeBoundSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets uSupport = 0; Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i ) { - uSuppCur = Lpk_ComputeBoundSets_rec( p, iLitFanin, vSets ); + uSuppCur = Lpk_ComputeBoundSets_rec( p, iLitFanin, vSets, nSizeMax ); uSupport |= uSuppCur; - Vec_IntPush( vSets, uSuppCur ); + if ( Kit_WordCountOnes(uSuppCur) <= nSizeMax ) + Vec_IntPush( vSets, uSuppCur ); } return uSupport; } @@ -150,12 +155,15 @@ Vec_Int_t * Lpk_ComputeBoundSets( Kit_DsdNtk_t * p, int nSizeMax ) if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR ) { uSupport = ( 1 << Kit_DsdLit2Var(Kit_DsdNtkRoot(p)->pFans[0]) ); - Vec_IntPush( vSets, uSupport ); + if ( Kit_WordCountOnes(uSupport) <= nSizeMax ) + Vec_IntPush( vSets, uSupport ); return vSets; } - uSupport = Lpk_ComputeBoundSets_rec( p, p->Root, vSets ); + uSupport = Lpk_ComputeBoundSets_rec( p, p->Root, vSets, nSizeMax ); assert( (uSupport & 0xFFFF0000) == 0 ); - Vec_IntPush( vSets, uSupport ); + // add the total support of the network + if ( Kit_WordCountOnes(uSupport) <= nSizeMax ) + Vec_IntPush( vSets, uSupport ); // set the remaining variables Vec_IntForEachEntry( vSets, Number, i ) { @@ -176,7 +184,7 @@ Vec_Int_t * Lpk_ComputeBoundSets( Kit_DsdNtk_t * p, int nSizeMax ) SeeAlso [] ***********************************************************************/ -Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1 ) +Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nSizeMax ) { Vec_Int_t * vSets; int Entry0, Entry1, Entry; @@ -188,7 +196,8 @@ Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1 ) Entry = Entry0 | Entry1; if ( (Entry & (Entry >> 16)) ) continue; - Vec_IntPush( vSets, Entry ); + if ( Kit_WordCountOnes(Entry) <= nSizeMax ) + Vec_IntPush( vSets, Entry ); } return vSets; } @@ -266,14 +275,15 @@ void Lpk_FunFreeTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5 SeeAlso [] ***********************************************************************/ -Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p, int nCofDepth ) +void Lpk_DsdAnalizeOne( Lpk_Fun_t * p, int nCofDepth, Lpk_Res_t * pRes ) { - static Lpk_Res_t Res, * pRes = &Res; unsigned * ppTruths[5][16]; Vec_Int_t * pvBSets[4][8]; Kit_DsdNtk_t * pNtkDec, * pTemp; unsigned uBoundSet; int i, k, nVarsBS, nVarsRem, Delay, Area; + assert( nCofDepth >= 0 && nCofDepth < 4 ); + assert( nCofDepth < (int)p->nLutK - 1 ); Lpk_FunAllocTruthTables( p, nCofDepth, ppTruths ); // find the best cofactors memset( pRes, 0, sizeof(Lpk_Res_t) ); @@ -291,7 +301,7 @@ Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p, int nCofDepth ) // derive the set of feasible boundsets for ( i = nCofDepth - 1; i >= 0; i-- ) for ( k = 0; k < (1<<i); k++ ) - pvBSets[i][k] = Lpk_MergeBoundSets( pvBSets[i+1][2*k+0], pvBSets[i+1][2*k+1] ); + pvBSets[i][k] = Lpk_MergeBoundSets( pvBSets[i+1][2*k+0], pvBSets[i+1][2*k+1], p->nLutK - nCofDepth ); // compare the resulting boundsets Vec_IntForEachEntry( pvBSets[0][0], uBoundSet, i ) { @@ -299,12 +309,13 @@ Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p, int nCofDepth ) continue; assert( (uBoundSet & (uBoundSet >> 16)) == 0 ); nVarsBS = Kit_WordCountOnes( uBoundSet & 0xFFFF ); + assert( nVarsBS <= (int)p->nLutK - nCofDepth ); nVarsRem = p->nVars - nVarsBS + nCofDepth + 1; - Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays ); Area = 1 + Lpk_LutNumLuts( nVarsRem, p->nLutK ); - if ( Delay > (int)p->nDelayLim || Area > (int)p->nAreaLim ) + Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays ); + if ( Area > (int)p->nAreaLim || Delay > (int)p->nDelayLim ) continue; - if ( uBoundSet == 0 || pRes->DelayEst > Delay || pRes->DelayEst == Delay && pRes->nSuppSizeL > nVarsRem ) + if ( pRes->BSVars == 0 || pRes->DelayEst > Delay || pRes->DelayEst == Delay && pRes->nSuppSizeL > nVarsRem ) { pRes->nBSVars = nVarsBS; pRes->BSVars = uBoundSet; @@ -316,7 +327,60 @@ Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p, int nCofDepth ) } // free cofactor storage Lpk_FunFreeTruthTables( p, nCofDepth, ppTruths ); - return pRes; +} + +/**Function************************************************************* + + Synopsis [Performs DSD-based decomposition of the function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p ) +{ + static Lpk_Res_t Res0, * pRes0 = &Res0; + static Lpk_Res_t Res1, * pRes1 = &Res1; + static Lpk_Res_t Res2, * pRes2 = &Res2; + static Lpk_Res_t Res3, * pRes3 = &Res3; + memset( pRes0, 0, sizeof(Lpk_Res_t) ); + memset( pRes1, 0, sizeof(Lpk_Res_t) ); + memset( pRes2, 0, sizeof(Lpk_Res_t) ); + memset( pRes3, 0, sizeof(Lpk_Res_t) ); + assert( p->uSupp == Kit_BitMask(p->nVars) ); + + // try decomposition without cofactoring + Lpk_DsdAnalizeOne( p, 0, pRes0 ); + if ( pRes0->nBSVars == (int)p->nLutK && pRes0->AreaEst <= (int)p->nAreaLim && pRes0->DelayEst <= (int)p->nDelayLim ) + return pRes0; + + // cofactor 1 time + if ( p->nLutK >= 3 ) + Lpk_DsdAnalizeOne( p, 1, pRes1 ); + assert( pRes1->nBSVars <= (int)p->nLutK - 1 ); + if ( pRes1->nBSVars == (int)p->nLutK - 1 && pRes1->AreaEst <= (int)p->nAreaLim && pRes1->DelayEst <= (int)p->nDelayLim ) + return pRes1; + + // cofactor 2 times + if ( p->nLutK >= 4 ) + Lpk_DsdAnalizeOne( p, 2, pRes2 ); + assert( pRes2->nBSVars <= (int)p->nLutK - 2 ); + if ( pRes2->nBSVars == (int)p->nLutK - 2 && pRes2->AreaEst <= (int)p->nAreaLim && pRes2->DelayEst <= (int)p->nDelayLim ) + return pRes2; + + // cofactor 3 times + if ( p->nLutK >= 5 ) + Lpk_DsdAnalizeOne( p, 3, pRes3 ); + assert( pRes3->nBSVars <= (int)p->nLutK - 3 ); + if ( pRes3->nBSVars == (int)p->nLutK - 3 && pRes3->AreaEst <= (int)p->nAreaLim && pRes3->DelayEst <= (int)p->nDelayLim ) + return pRes3; + + // choose the best under these conditions + + return NULL; } /**Function************************************************************* @@ -332,19 +396,21 @@ Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p, int nCofDepth ) ***********************************************************************/ Lpk_Fun_t * Lpk_DsdSplit( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet ) { + Lpk_Fun_t * pNew; Kit_DsdMan_t * pDsdMan; Kit_DsdNtk_t * pNtkDec, * pTemp; unsigned * pTruth = Lpk_FunTruth( p, 0 ); unsigned * pTruth0 = Lpk_FunTruth( p, 1 ); unsigned * pTruth1 = Lpk_FunTruth( p, 2 ); - Lpk_Fun_t * pNew; unsigned * ppTruths[5][16]; char pBSVars[5]; - int i, k, nVars, nCofs; + int i, k, nVars, iVacVar, nCofs; // get the bound set variables nVars = Lpk_SuppToVars( uBoundSet, pBSVars ); + // get the vacuous variable + iVacVar = pBSVars[0]; // compute the cofactors - Lpk_FunAllocTruthTables( p, nCofVars, ppTruths ); + Lpk_FunAllocTruthTables( p, nCofVars + 1, ppTruths ); for ( i = 0; i < nCofVars; i++ ) for ( k = 0; k < (1<<i); k++ ) { @@ -353,38 +419,37 @@ Lpk_Fun_t * Lpk_DsdSplit( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned } // decompose each cofactor w.r.t. the bound set nCofs = (1<<nCofVars); - pDsdMan = Kit_DsdManAlloc( p->nVars, p->nVars * 4 ); + pDsdMan = Kit_DsdManAlloc( p->nVars, p->nVars * 2 ); for ( k = 0; k < nCofs; k++ ) { pNtkDec = Kit_DsdDecompose( ppTruths[nCofVars][k], p->nVars ); pNtkDec = Kit_DsdExpand( pTemp = pNtkDec ); Kit_DsdNtkFree( pTemp ); - Kit_DsdTruthPartialTwo( pDsdMan, pNtkDec, uBoundSet, pBSVars[0], ppTruths[nCofVars+1][k], ppTruths[nCofVars+1][nCofs+k] ); + Kit_DsdTruthPartialTwo( pDsdMan, pNtkDec, uBoundSet, iVacVar, ppTruths[nCofVars+1][k], ppTruths[nCofVars+1][nCofs+k] ); Kit_DsdNtkFree( pNtkDec ); } Kit_DsdManFree( pDsdMan ); - // compute the composition function - for ( i = nCofVars - 1; i >= 1; i-- ) + // compute the composition/decomposition functions (they will be in pTruth0/pTruth1) + for ( i = nCofVars; i >= 1; i-- ) for ( k = 0; k < (1<<i); k++ ) - Kit_TruthMuxVar( ppTruths[i][k], ppTruths[i+1][2*k+0], ppTruths[i+1][2*k+1], nVars, pCofVars[i] ); - // now the composition/decomposition functions are in pTruth0/pTruth1 + Kit_TruthMuxVar( ppTruths[i][k], ppTruths[i+1][2*k+0], ppTruths[i+1][2*k+1], nVars, pCofVars[i-1] ); // derive the new component pNew = Lpk_FunDup( p, pTruth1 ); // update the old component Kit_TruthCopy( pTruth, pTruth0, p->nVars ); p->uSupp = Kit_TruthSupport( pTruth0, p->nVars ); - p->pFanins[pBSVars[0]] = pNew->Id; - p->pDelays[pBSVars[0]] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays ); + p->pFanins[iVacVar] = pNew->Id; + p->pDelays[iVacVar] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays ); // support minimize both Lpk_FunSuppMinimize( p ); Lpk_FunSuppMinimize( pNew ); // update delay and area requirements - pNew->nDelayLim = p->nDelayLim - 1; + pNew->nDelayLim = p->pDelays[iVacVar]; pNew->nAreaLim = 1; p->nAreaLim = p->nAreaLim - 1; // free cofactor storage - Lpk_FunFreeTruthTables( p, nCofVars, ppTruths ); + Lpk_FunFreeTruthTables( p, nCofVars + 1, ppTruths ); return pNew; } diff --git a/src/opt/lpk/lpkAbcMux.c b/src/opt/lpk/lpkAbcMux.c index 6549e175..159cae96 100644 --- a/src/opt/lpk/lpkAbcMux.c +++ b/src/opt/lpk/lpkAbcMux.c @@ -48,7 +48,6 @@ void Lpk_FunComputeCofs( Lpk_Fun_t * p, int iVar ) Kit_TruthCofactor1New( pTruth1, pTruth, p->nVars, iVar ); } - /**Function************************************************************* Synopsis [Computes cofactors w.r.t. each variable.] @@ -85,18 +84,18 @@ void Lpk_FunComputeCofSupps( Lpk_Fun_t * p, unsigned * puSupps ) SeeAlso [] ***********************************************************************/ -int Lpk_MuxAnalize( Lpk_Fun_t * p ) +Lpk_Res_t * Lpk_MuxAnalize( Lpk_Fun_t * p ) { - unsigned puSupps[32] = {0}; - int nSuppSize0, nSuppSize1, Delay, Delay0, Delay1, DelayA, DelayB; - int Var, Area, Polarity, VarBest, AreaBest, PolarityBest, nSuppSizeBest; - - if ( p->nVars > p->nAreaLim * (p->nLutK - 1) + 1 ) - return -1; + static Lpk_Res_t Res, * pRes = &Res; + unsigned puSupps[32]; + int nSuppSize0, nSuppSize1, nSuppSizeBest; + int Var, Area, Polarity, Delay, Delay0, Delay1, DelayA, DelayB; + memset( pRes, 0, sizeof(Lpk_Res_t) ); + assert( p->uSupp == Kit_BitMask(p->nVars) ); // get cofactor supports for each variable Lpk_FunComputeCofSupps( p, puSupps ); - // derive the delay and area of each MUX-decomposition - VarBest = -1; + // derive the delay and area after MUX-decomp with each var - and find the best var + pRes->Variable = -1; Lpk_SuppForEachVar( p->uSupp, Var ) { nSuppSize0 = Kit_WordCountOnes(puSupps[2*Var+0]); @@ -124,20 +123,20 @@ int Lpk_MuxAnalize( Lpk_Fun_t * p ) Area = 1 + Lpk_LutNumLuts( nSuppSize1, p->nLutK ); Polarity = 0; } - else if ( nSuppSize0 <= (int)p->nLutK ) + else if ( nSuppSize1 <= (int)p->nLutK - 2 ) { DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays ); DelayB = Lpk_SuppDelay( puSupps[2*Var+0] , p->pDelays ); Delay = ABC_MAX( DelayA, DelayB + 1 ); - Area = 1 + Lpk_LutNumLuts( nSuppSize1+2, p->nLutK ); + Area = 1 + Lpk_LutNumLuts( nSuppSize0, p->nLutK ); Polarity = 1; } - else if ( nSuppSize1 <= (int)p->nLutK - 2 ) + else if ( nSuppSize0 <= (int)p->nLutK ) { DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<<Var), p->pDelays ); DelayB = Lpk_SuppDelay( puSupps[2*Var+0] , p->pDelays ); Delay = ABC_MAX( DelayA, DelayB + 1 ); - Area = 1 + Lpk_LutNumLuts( nSuppSize0, p->nLutK ); + Area = 1 + Lpk_LutNumLuts( nSuppSize1+2, p->nLutK ); Polarity = 1; } else if ( nSuppSize1 <= (int)p->nLutK ) @@ -171,15 +170,16 @@ int Lpk_MuxAnalize( Lpk_Fun_t * p ) continue; if ( Area > (int)p->nAreaLim ) continue; - if ( VarBest == -1 || AreaBest > Area || (AreaBest == Area && nSuppSizeBest > nSuppSize0+nSuppSize1) ) + if ( pRes->Variable == -1 || pRes->AreaEst > Area || (pRes->AreaEst == Area && nSuppSizeBest > nSuppSize0+nSuppSize1) ) { - VarBest = Var; - AreaBest = Area; - PolarityBest = Polarity; - nSuppSizeBest = nSuppSize0+nSuppSize1; + pRes->Variable = Var; + pRes->Polarity = Polarity; + pRes->AreaEst = Area; + pRes->DelayEst = Delay; + nSuppSizeBest = nSuppSize0+nSuppSize1; } } - return (VarBest == -1)? -1 : (2*VarBest + Polarity); + return pRes->Variable == -1 ? NULL : pRes; } /**Function************************************************************* @@ -193,60 +193,61 @@ int Lpk_MuxAnalize( Lpk_Fun_t * p ) SeeAlso [] ***********************************************************************/ -Lpk_Fun_t * Lpk_MuxSplit( Lpk_Fun_t * p, int VarPol ) +Lpk_Fun_t * Lpk_MuxSplit( Lpk_Fun_t * p, int Var, int Pol ) { Lpk_Fun_t * pNew; unsigned * pTruth = Lpk_FunTruth( p, 0 ); unsigned * pTruth0 = Lpk_FunTruth( p, 1 ); unsigned * pTruth1 = Lpk_FunTruth( p, 2 ); - int Var = VarPol / 2; - int Pol = VarPol % 2; int iVarVac; - assert( VarPol >= 0 && VarPol < 2 * (int)p->nVars ); + assert( Var >= 0 && Var < (int)p->nVars ); assert( p->nAreaLim >= 2 ); Lpk_FunComputeCofs( p, Var ); - if ( Pol == 0 ) + // derive the new component + pNew = Lpk_FunDup( p, Pol ? pTruth0 : pTruth1 ); + // update the support of the old component + p->uSupp = Kit_TruthSupport( Pol ? pTruth1 : pTruth0, p->nVars ); + p->uSupp |= (1 << Var); + // update the truth table of the old component + iVarVac = Kit_WordFindFirstBit( ~p->uSupp ); + assert( iVarVac < (int)p->nVars ); + Kit_TruthIthVar( pTruth, p->nVars, Var ); + if ( Pol ) + Kit_TruthMuxVar( pTruth, pTruth, pTruth1, p->nVars, iVarVac ); + else + Kit_TruthMuxVar( pTruth, pTruth0, pTruth, p->nVars, iVarVac ); + // set the decomposed variable + p->pFanins[iVarVac] = pNew->Id; + p->pDelays[iVarVac] = p->nDelayLim - 1; + // support minimize both + Lpk_FunSuppMinimize( p ); + Lpk_FunSuppMinimize( pNew ); + // update delay and area requirements + pNew->nDelayLim = p->nDelayLim - 1; + if ( p->nVars <= p->nLutK ) { - // derive the new component - pNew = Lpk_FunDup( p, pTruth1 ); - // update the old component - p->uSupp = Kit_TruthSupport( pTruth0, p->nVars ); - iVarVac = Kit_WordFindFirstBit( ~(p->uSupp | (1 << Var)) ); - assert( iVarVac < (int)p->nVars ); - Kit_TruthIthVar( pTruth, p->nVars, iVarVac ); - // update the truth table - Kit_TruthMux( pTruth, pTruth0, pTruth1, pTruth, p->nVars ); - p->pFanins[iVarVac] = pNew->Id; - p->pDelays[iVarVac] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays ); - // support minimize both - Lpk_FunSuppMinimize( p ); - Lpk_FunSuppMinimize( pNew ); - // update delay and area requirements - pNew->nDelayLim = p->nDelayLim - 1; - if ( p->nVars <= p->nLutK ) - { - pNew->nAreaLim = p->nAreaLim - 1; - p->nAreaLim = 1; - } - else if ( pNew->nVars <= pNew->nLutK ) - { - pNew->nAreaLim = 1; - p->nAreaLim = p->nAreaLim - 1; - } - else if ( p->nVars < pNew->nVars ) - { - pNew->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2; - p->nAreaLim = p->nAreaLim / 2 - p->nAreaLim % 2; - } - else // if ( pNew->nVars < p->nVars ) - { - pNew->nAreaLim = p->nAreaLim / 2 - p->nAreaLim % 2; - p->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2; - } + pNew->nAreaLim = p->nAreaLim - 1; + p->nAreaLim = 1; + } + else if ( pNew->nVars <= pNew->nLutK ) + { + pNew->nAreaLim = 1; + p->nAreaLim = p->nAreaLim - 1; + } + else if ( p->nVars < pNew->nVars ) + { + pNew->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2; + p->nAreaLim = p->nAreaLim / 2 - p->nAreaLim % 2; + } + else // if ( pNew->nVars < p->nVars ) + { + pNew->nAreaLim = p->nAreaLim / 2 - p->nAreaLim % 2; + p->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2; } return p; } + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/opt/lpk/lpkAbcUtil.c b/src/opt/lpk/lpkAbcUtil.c index 960ebded..681ec092 100644 --- a/src/opt/lpk/lpkAbcUtil.c +++ b/src/opt/lpk/lpkAbcUtil.c @@ -139,20 +139,20 @@ Lpk_Fun_t * Lpk_FunDup( Lpk_Fun_t * p, unsigned * pTruth ) ***********************************************************************/ void Lpk_FunSuppMinimize( Lpk_Fun_t * p ) { - int j, k, nVarsNew; + int i, k, nVarsNew; // compress the truth table if ( p->uSupp == Kit_BitMask(p->nVars) ) return; // minimize support nVarsNew = Kit_WordCountOnes(p->uSupp); Kit_TruthShrink( Lpk_FunTruth(p, 1), Lpk_FunTruth(p, 0), nVarsNew, p->nVars, p->uSupp, 1 ); - for ( j = k = 0; j < (int)p->nVars; j++ ) - if ( p->uSupp & (1 << j) ) - { - p->pFanins[k] = p->pFanins[j]; - p->pDelays[k] = p->pDelays[j]; - k++; - } + k = 0; + Lpk_SuppForEachVar( p->uSupp, i ) + { + p->pFanins[k] = p->pFanins[i]; + p->pDelays[k] = p->pDelays[i]; + k++; + } assert( k == nVarsNew ); p->nVars = k; p->uSupp = Kit_BitMask(p->nVars); diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c index fda5423e..37bfd956 100644 --- a/src/opt/lpk/lpkCore.c +++ b/src/opt/lpk/lpkCore.c @@ -361,17 +361,10 @@ p->timeTruth += clock() - clk; if ( p->pPars->fVeryVerbose ) { // char * pFileName; - int nSuppSize; - Kit_DsdNtk_t * pDsdNtk; - nSuppSize = Extra_TruthSupportSize(pTruth, pCut->nLeaves); + int nSuppSize = Extra_TruthSupportSize( pTruth, pCut->nLeaves ); printf( " C%02d: L= %2d/%2d V= %2d/%d N= %d W= %4.2f ", i, pCut->nLeaves, nSuppSize, pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight ); - - pDsdNtk = Kit_DsdDecompose( pTruth, pCut->nLeaves ); -// Kit_DsdVerify( pDsdNtk, pTruth, pCut->nLeaves ); - Kit_DsdPrint( stdout, pDsdNtk ); - Kit_DsdNtkFree( pDsdNtk ); -// Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves ); + Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves ); // pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ ); // printf( "Saved truth table in file \"%s\".\n", pFileName ); } diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c index d0908a6a..f5c0c66c 100644 --- a/src/opt/lpk/lpkCut.c +++ b/src/opt/lpk/lpkCut.c @@ -30,7 +30,7 @@ /**Function************************************************************* - Synopsis [Computes the truth able of one cut.] + Synopsis [Computes the truth table of one cut.] Description [] @@ -445,10 +445,17 @@ void Lpk_NodeCutsOne( Lpk_Man_t * p, Lpk_Cut_t * pCut, int Node ) memcpy( pCutNew->pNodes, pCut->pNodes, pCut->nNodes * sizeof(int) ); pCutNew->nNodes = pCut->nNodes; pCutNew->nNodesDup = pCut->nNodesDup; + // check if the node is already there + // if so, move the node to be the last for ( i = 0; i < (int)pCutNew->nNodes; i++ ) if ( pCutNew->pNodes[i] == Node ) + { + for ( k = i; k < (int)pCutNew->nNodes - 1; k++ ) + pCutNew->pNodes[k] = pCutNew->pNodes[k+1]; + pCutNew->pNodes[k] = Node; break; + } if ( i == (int)pCutNew->nNodes ) // new node { pCutNew->pNodes[ pCutNew->nNodes++ ] = Node; diff --git a/src/opt/lpk/lpkInt.h b/src/opt/lpk/lpkInt.h index 7022cc4a..32fb05b3 100644 --- a/src/opt/lpk/lpkInt.h +++ b/src/opt/lpk/lpkInt.h @@ -122,14 +122,14 @@ struct Lpk_Man_t_ typedef struct Lpk_Fun_t_ Lpk_Fun_t; struct Lpk_Fun_t_ { - Vec_Ptr_t * vNodes; // the array of all functions - unsigned int Id : 5; // the ID of this node + Vec_Ptr_t * vNodes; // the array of leaves and decomposition nodes + unsigned int Id : 8; // the ID of this node unsigned int nVars : 5; // the number of variables unsigned int nLutK : 4; // the number of LUT inputs - unsigned int nAreaLim : 8; // the area limit (the largest allowed) + unsigned int nAreaLim : 5; // the area limit (the largest allowed) unsigned int nDelayLim : 10; // the delay limit (the largest allowed) - char pFanins[16]; // the fanins of this function char pDelays[16]; // the delays of the inputs + char pFanins[16]; // the fanins of this function unsigned uSupp; // the support of this component unsigned pTruth[0]; // the truth table (contains room for three truth tables) }; @@ -146,6 +146,8 @@ struct Lpk_Res_t_ int nSuppSizeL; // support size of the larger (composition) function int DelayEst; // estimated delay of the decomposition int AreaEst; // estimated area of the decomposition + int Variable; // variable in MUX decomposition + int Polarity; // polarity in MUX decomposition }; static inline int Lpk_LutNumVars( int nLutsLim, int nLutK ) { return nLutsLim * (nLutK - 1) + 1; } @@ -177,11 +179,11 @@ static inline unsigned * Lpk_FunTruth( Lpk_Fun_t * p, int Num ) { assert( Num /*=== lpkAbcDec.c ============================================================*/ extern Abc_Obj_t * Lpk_Decompose( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim ); /*=== lpkAbcDsd.c ============================================================*/ -extern Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p, int nCofDepth ); +extern Lpk_Res_t * Lpk_DsdAnalize( Lpk_Fun_t * p ); extern Lpk_Fun_t * Lpk_DsdSplit( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet ); /*=== lpkAbcMux.c ============================================================*/ -extern int Lpk_MuxAnalize( Lpk_Fun_t * p ); -extern Lpk_Fun_t * Lpk_MuxSplit( Lpk_Fun_t * p, int VarPol ); +extern Lpk_Res_t * Lpk_MuxAnalize( Lpk_Fun_t * p ); +extern Lpk_Fun_t * Lpk_MuxSplit( Lpk_Fun_t * p, int Var, int Pol ); /*=== lpkAbcUtil.c ============================================================*/ extern Lpk_Fun_t * Lpk_FunAlloc( int nVars ); extern void Lpk_FunFree( Lpk_Fun_t * p ); diff --git a/src/opt/lpk/lpkMux.c b/src/opt/lpk/lpkMux.c index 7928f77e..ed046ad7 100644 --- a/src/opt/lpk/lpkMux.c +++ b/src/opt/lpk/lpkMux.c @@ -167,6 +167,8 @@ If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, I ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] ); Kit_DsdNtkFree( pTemp ); Kit_DsdTruthPartial( p->pDsdMan, ppNtks[0], pDec0, uSubset0 ); Kit_DsdTruthPartial( p->pDsdMan, ppNtks[1], pDec1, uSubset1 ); +// Kit_DsdTruthPartialTwo( p->pDsdMan, ppNtks[0], uSubset0, iVarReused, pCo0, pDec0 ); +// Kit_DsdTruthPartialTwo( p->pDsdMan, ppNtks[1], uSubset1, iVarReused, pCo1, pDec1 ); Kit_DsdNtkFree( ppNtks[0] ); Kit_DsdNtkFree( ppNtks[1] ); //Kit_DsdPrintFromTruth( pDec0, nVars ); @@ -218,6 +220,7 @@ If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, I Kit_TruthMuxVar( pCo1, pCo10, pCo11, nVars, iVarReused ); //Kit_DsdPrintFromTruth( pCo0, nVars ); //Kit_DsdPrintFromTruth( pCo1, nVars ); + // derive the composition function Kit_TruthMuxVar( pCo , pCo0 , pCo1 , nVars, iVar ); diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c index 19ff6f8b..512c5751 100644 --- a/src/sat/bsat/satSolver.c +++ b/src/sat/bsat/satSolver.c @@ -27,7 +27,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "satSolver.h" //#define SAT_USE_SYSTEM_MEMORY_MANAGEMENT -#define WATCHFLAG 1 //================================================================================================= // Debug: @@ -91,11 +90,9 @@ static inline void clause_setactivity(clause* c, float a) { *((float*)&c->lits[ //================================================================================================= // Encode literals in clause pointers: -static bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); } static clause* clause_from_lit (lit l) { return (clause*)((unsigned long)l + (unsigned long)l + 1); } +static bool clause_is_lit (clause* c) { return ((unsigned long)c & 1); } static lit clause_read_lit (clause* c) { return (lit)((unsigned long)c >> 1); } -static clause* clause_from_lit2(lit l) { return (clause*)(unsigned long)l; } -static lit clause_read_lit2(clause* c) { return (lit)(unsigned long)c; } //================================================================================================= // Simple helpers: @@ -111,15 +108,6 @@ static inline void vecp_remove(vecp* v, void* e) for (; j < vecp_size(v)-1; j++) ws[j] = ws[j+1]; vecp_resize(v,vecp_size(v)-1); } -static inline void vecp_remove2(vecp* v, void* e) -{ - void** ws = vecp_begin(v); - int j = 0; - for (; ws[j] != e ; j++); - assert(j < vecp_size(v)); - for (; j < vecp_size(v)-2; j++) ws[j] = ws[j+2]; - vecp_resize(v,vecp_size(v)-2); -} //================================================================================================= // Variable order functions: @@ -316,26 +304,8 @@ static clause* clause_new(sat_solver* s, lit* begin, lit* end, int learnt) //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c); //vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c); - if ( WATCHFLAG ) - { - if ( size == 2 ) - { - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)clause_from_lit(begin[1])); - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)clause_from_lit(begin[0])); - } - else - { - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)c); - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)clause_from_lit2(begin[1])); - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)c); - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)clause_from_lit2(begin[0])); - } - } - else - { - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1]))); - vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0]))); - } + vecp_push(sat_solver_read_wlist(s,lit_neg(begin[0])),(void*)(size > 2 ? c : clause_from_lit(begin[1]))); + vecp_push(sat_solver_read_wlist(s,lit_neg(begin[1])),(void*)(size > 2 ? c : clause_from_lit(begin[0]))); return c; } @@ -351,24 +321,8 @@ static void clause_remove(sat_solver* s, clause* c) //vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c); assert(lits[0] < s->size*2); - if ( WATCHFLAG ) - { - if ( clause_size(c) == 2 ) - { - vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)clause_from_lit(lits[1])); - vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)clause_from_lit(lits[0])); - } - else - { - vecp_remove2(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)c); - vecp_remove2(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)c); - } - } - else - { - vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1]))); - vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0]))); - } + vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[0])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[1]))); + vecp_remove(sat_solver_read_wlist(s,lit_neg(lits[1])),(void*)(clause_size(c) > 2 ? c : clause_from_lit(lits[0]))); if (clause_learnt(c)){ s->stats.learnts--; @@ -749,31 +703,6 @@ static void sat_solver_analyze(sat_solver* s, clause* c, veci* learnt) } -void sat_solver_check(sat_solver* s) -{ - int j, k; - lit Lit, First, *lits; - vecp* ws; - clause **begin, **end, **i; - for ( j = 0; j < s->size; j++ ) - for ( k = 0; k < 2; k++ ) - { - Lit = toLitCond( j, k ); - ws = sat_solver_read_wlist(s,Lit); - begin = (clause**)vecp_begin(ws); - end = begin + vecp_size(ws); - for (i = begin; i < end; i++) - { - if (clause_is_lit(*i)) - continue; - lits = clause_begin(*i); - First = clause_read_lit2(*(i+1)); - assert( First == lits[0] || First == lits[1] ); - i++; - } - } -} - clause* sat_solver_propagate(sat_solver* s) { lbool* values = s->assigns; @@ -787,19 +716,15 @@ clause* sat_solver_propagate(sat_solver* s) clause **begin = (clause**)vecp_begin(ws); clause **end = begin + vecp_size(ws); clause **i, **j; -// sat_solver_check(s); s->stats.propagations++; s->simpdb_props--; - + //printf("checking lit %d: "L_LIT"\n", veci_size(ws), L_lit(p)); - for (i = j = begin; i < end; i++) - { - if (clause_is_lit(*i)) - { + for (i = j = begin; i < end; ){ + if (clause_is_lit(*i)){ *j++ = *i; - if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))) - { + if (!enqueue(s,clause_read_lit(*i),clause_from_lit(p))){ confl = s->binary; (clause_begin(confl))[1] = lit_neg(p); (clause_begin(confl))[0] = clause_read_lit(*i++); @@ -808,27 +733,13 @@ clause* sat_solver_propagate(sat_solver* s) while (i < end) *j++ = *i++; } - } - else - { - lit false_lit, first; + }else{ + lit false_lit; lbool sig; - if ( WATCHFLAG ) - { - first = clause_read_lit2(*(i+1)); - sig = !lit_sign(first); sig += sig - 1; - if (values[lit_var(first)] == sig) - { - *j++ = *i++; - *j++ = *i; - continue; - } - } - lits = clause_begin(*i); - // Make sure the false literal is in data[1]: + // Make sure the false literal is data[1]: false_lit = lit_neg(p); if (lits[0] == false_lit){ lits[0] = lits[1]; @@ -837,95 +748,35 @@ clause* sat_solver_propagate(sat_solver* s) assert(lits[1] == false_lit); //printf("checking clause: "); printlits(lits, lits+clause_size(*i)); printf("\n"); - if ( WATCHFLAG ) - { -/* - // If 0th watch is true, then clause is already satisfied. - sig = !lit_sign(lits[0]); sig += sig - 1; - if (values[lit_var(lits[0])] == sig) - { - *j++ = *i++; - *j++ = *i; - continue; - } - else -*/ - { + // If 0th watch is true, then clause is already satisfied. + sig = !lit_sign(lits[0]); sig += sig - 1; + if (values[lit_var(lits[0])] == sig){ + *j++ = *i; + }else{ // Look for new watch: lit* stop = lits + clause_size(*i); lit* k; -// assert( lits[0] == first ); - for (k = lits + 2; k < stop; k++) - { + for (k = lits + 2; k < stop; k++){ lbool sig = lit_sign(*k); sig += sig - 1; - if (values[lit_var(*k)] != sig) - { + if (values[lit_var(*k)] != sig){ lits[1] = *k; *k = false_lit; -// vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i); - vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i++); - vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),clause_from_lit2(lits[0])); - break; - } + vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i); + goto next; } } - if ( k < stop ) - continue; *j++ = *i; // Clause is unit under assignment: - if (!enqueue(s,lits[0], *i)) - { + if (!enqueue(s,lits[0], *i)){ confl = *i++; - *j++ = clause_from_lit2(lits[0]); i++; // // Copy the remaining watches: while (i < end) *j++ = *i++; } - else - { - *j++ = clause_from_lit2(lits[0]); i++; // - } - } - } - else - { - // If 0th watch is true, then clause is already satisfied. - sig = !lit_sign(lits[0]); sig += sig - 1; - if (values[lit_var(lits[0])] == sig) - { - *j++ = *i; - } - else - { - // Look for new watch: - lit* stop = lits + clause_size(*i); - lit* k; - for (k = lits + 2; k < stop; k++) - { - lbool sig = lit_sign(*k); sig += sig - 1; - if (values[lit_var(*k)] != sig) - { - lits[1] = *k; - *k = false_lit; - vecp_push(sat_solver_read_wlist(s,lit_neg(lits[1])),*i); - break; - } - } - if ( k < stop ) - continue; - - *j++ = *i; - // Clause is unit under assignment: - if (!enqueue(s,lits[0], *i)) - { - confl = *i++; - // Copy the remaining watches: - while (i < end) - *j++ = *i++; - } - } } } + next: + i++; } s->stats.inspects += j - (clause**)vecp_begin(ws); @@ -944,7 +795,7 @@ void sat_solver_reducedb(sat_solver* s) double extra_lim = s->cla_inc / vecp_size(&s->learnts); // Remove any clause below this activity clause** learnts = (clause**)vecp_begin(&s->learnts); clause** reasons = s->reasons; -//printf( "Trying to reduce DB\n" ); + sat_solver_sort(vecp_begin(&s->learnts), vecp_size(&s->learnts), &clause_cmp); for (i = j = 0; i < vecp_size(&s->learnts) / 2; i++){ @@ -1037,10 +888,8 @@ static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_l } if (sat_solver_dlevel(s) == 0 && !s->fSkipSimplify) - { // Simplify the set of problem clauses: sat_solver_simplify(s); - } if (nof_learnts >= 0 && vecp_size(&s->learnts) - s->qtail >= nof_learnts) // Reduce the set of learnt clauses: @@ -1271,7 +1120,6 @@ bool sat_solver_simplify(sat_solver* s) if (s->qhead == s->simpdb_assigns || s->simpdb_props > 0) return true; -//printf( "Trying to simplify\n" ); reasons = s->reasons; for (type = 0; type < 2; type++){ |