From d47752011d94805850f8713258634d1bde5e639f Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 8 Jun 2007 08:01:00 -0700 Subject: [PATCH] Version abc70608 --- abc.dsp | 4 + src/aig/dar/dar.h | 38 +-- src/aig/dar/darCheck.c | 13 +- src/aig/dar/darCore.c | 4 +- src/aig/dar/darDfs.c | 55 ++-- src/aig/dar/darMan.c | 26 +- src/aig/dar/darObj.c | 55 +++- src/aig/dar/darOper.c | 64 ++++- src/aig/dar/darSeq.c | 471 +++++++++++++++++++++++++++++++++ src/aig/dar/darTable.c | 29 +- src/base/abc/abcDfs.c | 3 + src/base/abc/abcNtk.c | 2 +- src/base/abci/abc.c | 56 +++- src/base/abci/abcDar.c | 209 +++++++++++---- src/base/abci/abcFraig.c | 4 +- src/base/abci/abcPart.c | 55 ++++ src/base/io/ioReadAiger.c | 13 +- src/base/io/ioReadBench.c | 8 +- src/base/io/ioWriteVerilog.c | 10 +- src/base/io/ioWriteVerilog.zip | Bin 0 -> 3662 bytes src/base/ver/ver.h | 1 + src/base/ver/verCore.c | 173 ++++++++---- src/base/ver/verCore.zip | Bin 14163 -> 14624 bytes src/map/if/ifUtil.c | 20 ++ 24 files changed, 1103 insertions(+), 210 deletions(-) create mode 100644 src/aig/dar/darSeq.c create mode 100644 src/base/io/ioWriteVerilog.zip diff --git a/abc.dsp b/abc.dsp index bb02cf328..cfc19378b 100644 --- a/abc.dsp +++ b/abc.dsp @@ -858,6 +858,10 @@ SOURCE=.\src\aig\dar\darOper.c # End Source File # Begin Source File +SOURCE=.\src\aig\dar\darSeq.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\dar\darTable.c # End Source File # Begin Source File diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h index 7c77bea5c..9bb79262a 100644 --- a/src/aig/dar/dar.h +++ b/src/aig/dar/dar.h @@ -65,7 +65,8 @@ typedef enum { DAR_AIG_BUF, // 4: buffer node DAR_AIG_AND, // 5: AND node DAR_AIG_EXOR, // 6: EXOR node - DAR_AIG_VOID // 7: unused object + DAR_AIG_LATCH, // 7: latch + DAR_AIG_VOID // 8: unused object } Dar_Type_t; // the parameters @@ -179,11 +180,13 @@ static inline Dar_Obj_t * Dar_ManObj( Dar_Man_t * p, int i ) { return p->vO static inline int Dar_ManPiNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_PI]; } static inline int Dar_ManPoNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_PO]; } +static inline int Dar_ManBufNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_BUF]; } static inline int Dar_ManAndNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_AND]; } static inline int Dar_ManExorNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_EXOR]; } -static inline int Dar_ManNodeNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_AND]+p->nObjs[DAR_AIG_EXOR];} +static inline int Dar_ManLatchNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_LATCH]; } +static inline int Dar_ManNodeNum( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_AND]+p->nObjs[DAR_AIG_EXOR]; } static inline int Dar_ManGetCost( Dar_Man_t * p ) { return p->nObjs[DAR_AIG_AND]+3*p->nObjs[DAR_AIG_EXOR]; } -static inline int Dar_ManObjNum( Dar_Man_t * p ) { return p->nCreated - p->nDeleted; } +static inline int Dar_ManObjNum( Dar_Man_t * p ) { return p->nCreated - p->nDeleted; } static inline Dar_Type_t Dar_ObjType( Dar_Obj_t * pObj ) { return (Dar_Type_t)pObj->Type; } static inline int Dar_ObjIsNone( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_NONE; } @@ -193,19 +196,20 @@ static inline int Dar_ObjIsPo( Dar_Obj_t * pObj ) { return pObj- static inline int Dar_ObjIsBuf( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_BUF; } static inline int Dar_ObjIsAnd( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_AND; } static inline int Dar_ObjIsExor( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_EXOR; } +static inline int Dar_ObjIsLatch( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_LATCH; } static inline int Dar_ObjIsNode( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_AND || pObj->Type == DAR_AIG_EXOR; } -static inline int Dar_ObjIsTerm( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_PI || pObj->Type == DAR_AIG_PO || pObj->Type == DAR_AIG_CONST1; } -static inline int Dar_ObjIsHash( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_AND || pObj->Type == DAR_AIG_EXOR; } +static inline int Dar_ObjIsTerm( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_PI || pObj->Type == DAR_AIG_PO || pObj->Type == DAR_AIG_CONST1; } +static inline int Dar_ObjIsHash( Dar_Obj_t * pObj ) { return pObj->Type == DAR_AIG_AND || pObj->Type == DAR_AIG_EXOR || pObj->Type == DAR_AIG_LATCH; } static inline int Dar_ObjIsMarkA( Dar_Obj_t * pObj ) { return pObj->fMarkA; } static inline void Dar_ObjSetMarkA( Dar_Obj_t * pObj ) { pObj->fMarkA = 1; } static inline void Dar_ObjClearMarkA( Dar_Obj_t * pObj ) { pObj->fMarkA = 0; } -static inline void Dar_ObjSetTravId( Dar_Obj_t * pObj, int TravId ) { pObj->pData = (void *)TravId; } -static inline void Dar_ObjSetTravIdCurrent( Dar_Man_t * p, Dar_Obj_t * pObj ) { pObj->pData = (void *)p->nTravIds; } -static inline void Dar_ObjSetTravIdPrevious( Dar_Man_t * p, Dar_Obj_t * pObj ) { pObj->pData = (void *)(p->nTravIds - 1); } -static inline int Dar_ObjIsTravIdCurrent( Dar_Man_t * p, Dar_Obj_t * pObj ) { return (int )((int)pObj->pData == p->nTravIds); } -static inline int Dar_ObjIsTravIdPrevious( Dar_Man_t * p, Dar_Obj_t * pObj ) { return (int )((int)pObj->pData == p->nTravIds - 1); } +static inline void Dar_ObjSetTravId( Dar_Obj_t * pObj, int TravId ) { pObj->TravId = TravId; } +static inline void Dar_ObjSetTravIdCurrent( Dar_Man_t * p, Dar_Obj_t * pObj ) { pObj->TravId = p->nTravIds; } +static inline void Dar_ObjSetTravIdPrevious( Dar_Man_t * p, Dar_Obj_t * pObj ) { pObj->TravId = p->nTravIds - 1; } +static inline int Dar_ObjIsTravIdCurrent( Dar_Man_t * p, Dar_Obj_t * pObj ) { return (int)(pObj->TravId == p->nTravIds); } +static inline int Dar_ObjIsTravIdPrevious( Dar_Man_t * p, Dar_Obj_t * pObj ) { return (int)(pObj->TravId == p->nTravIds - 1); } static inline int Dar_ObjTravId( Dar_Obj_t * pObj ) { return (int)pObj->pData; } static inline int Dar_ObjPhase( Dar_Obj_t * pObj ) { return pObj->fPhase; } @@ -247,7 +251,7 @@ static inline Dar_Obj_t * Dar_ObjCreateGhost( Dar_Man_t * p, Dar_Obj_t * p0, Da assert( Type == DAR_AIG_PI || Dar_Regular(p0) != Dar_Regular(p1) ); pGhost = Dar_ManGhost(p); pGhost->Type = Type; - if ( Dar_Regular(p0)->Id < Dar_Regular(p1)->Id ) + if ( p1 == NULL || Dar_Regular(p0)->Id < Dar_Regular(p1)->Id ) { pGhost->pFanin0 = p0; pGhost->pFanin1 = p1; @@ -274,7 +278,8 @@ static inline Dar_Obj_t * Dar_ManFetchMemory( Dar_Man_t * p ) static inline void Dar_ManRecycleMemory( Dar_Man_t * p, Dar_Obj_t * pEntry ) { extern void Dar_MmFixedEntryRecycle( Dar_MmFixed_t * p, char * pEntry ); - pEntry->Type = DAR_AIG_NONE; // distinquishes dead node from live node + p->nDeleted++; + pEntry->Type = DAR_AIG_NONE; // distinquishes a dead node from a live node Dar_MmFixedEntryRecycle( p->pMemObjs, (char *)pEntry ); } @@ -291,7 +296,7 @@ static inline void Dar_ManRecycleMemory( Dar_Man_t * p, Dar_Obj_t * pEntry ) Vec_PtrForEachEntry( p->vPos, pObj, i ) // iterator over all objects, including those currently not used #define Dar_ManForEachObj( p, pObj, i ) \ - Vec_PtrForEachEntry( p->vObjs, pObj, i ) + Vec_PtrForEachEntry( p->vObjs, pObj, i ) if ( (pObj) == NULL ) {} else //////////////////////////////////////////////////////////////////////// /// FUNCTION DECLARATIONS /// @@ -313,7 +318,6 @@ extern Vec_Int_t * Dar_LibReadNodes(); extern Vec_Int_t * Dar_LibReadOuts(); /*=== darDfs.c ==========================================================*/ extern Vec_Ptr_t * Dar_ManDfs( Dar_Man_t * p ); -extern Vec_Ptr_t * Dar_ManDfsNode( Dar_Man_t * p, Dar_Obj_t * pNode ); extern int Dar_ManCountLevels( Dar_Man_t * p ); extern void Dar_ManCreateRefs( Dar_Man_t * p ); extern int Dar_DagSize( Dar_Obj_t * pObj ); @@ -342,11 +346,13 @@ extern void Dar_ObjConnect( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_ extern void Dar_ObjDisconnect( Dar_Man_t * p, Dar_Obj_t * pObj ); extern void Dar_ObjDelete( Dar_Man_t * p, Dar_Obj_t * pObj ); extern void Dar_ObjDelete_rec( Dar_Man_t * p, Dar_Obj_t * pObj, int fFreeTop ); -extern void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew ); +extern void Dar_ObjPatchFanin0( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pFaninNew ); +extern void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew, int fNodesOnly ); /*=== darOper.c =========================================================*/ extern Dar_Obj_t * Dar_IthVar( Dar_Man_t * p, int i ); extern Dar_Obj_t * Dar_Oper( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1, Dar_Type_t Type ); extern Dar_Obj_t * Dar_And( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1 ); +extern Dar_Obj_t * Dar_Latch( Dar_Man_t * p, Dar_Obj_t * pObj, int fInitOne ); extern Dar_Obj_t * Dar_Or( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1 ); extern Dar_Obj_t * Dar_Exor( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1 ); extern Dar_Obj_t * Dar_Mux( Dar_Man_t * p, Dar_Obj_t * pC, Dar_Obj_t * p1, Dar_Obj_t * p0 ); @@ -355,6 +361,8 @@ extern Dar_Obj_t * Dar_Miter( Dar_Man_t * p, Vec_Ptr_t * vPairs ); extern Dar_Obj_t * Dar_CreateAnd( Dar_Man_t * p, int nVars ); extern Dar_Obj_t * Dar_CreateOr( Dar_Man_t * p, int nVars ); extern Dar_Obj_t * Dar_CreateExor( Dar_Man_t * p, int nVars ); +/*=== darSeq.c ========================================================*/ +extern int Dar_ManSeqStrash( Dar_Man_t * p, int nLatches, int * pInits ); /*=== darTable.c ========================================================*/ extern Dar_Obj_t * Dar_TableLookup( Dar_Man_t * p, Dar_Obj_t * pGhost ); extern void Dar_TableInsert( Dar_Man_t * p, Dar_Obj_t * pObj ); diff --git a/src/aig/dar/darCheck.c b/src/aig/dar/darCheck.c index 6cfba787e..5c7a2390d 100644 --- a/src/aig/dar/darCheck.c +++ b/src/aig/dar/darCheck.c @@ -89,15 +89,24 @@ int Dar_ManCheck( Dar_Man_t * p ) } } // count the total number of nodes - if ( Dar_ManObjNum(p) != 1 + Dar_ManPiNum(p) + Dar_ManPoNum(p) + Dar_ManAndNum(p) + Dar_ManExorNum(p) ) + if ( Dar_ManObjNum(p) != 1 + Dar_ManPiNum(p) + Dar_ManPoNum(p) + Dar_ManBufNum(p) + Dar_ManAndNum(p) + Dar_ManExorNum(p) + Dar_ManLatchNum(p) ) { printf( "Dar_ManCheck: The number of created nodes is wrong.\n" ); + printf( "C1 = %d. Pi = %d. Po = %d. Buf = %d. And = %d. Xor = %d. Lat = %d. Total = %d.\n", + 1, Dar_ManPiNum(p), Dar_ManPoNum(p), Dar_ManBufNum(p), Dar_ManAndNum(p), Dar_ManExorNum(p), Dar_ManLatchNum(p), + 1 + Dar_ManPiNum(p) + Dar_ManPoNum(p) + Dar_ManBufNum(p) + Dar_ManAndNum(p) + Dar_ManExorNum(p) + Dar_ManLatchNum(p) ); + printf( "Created = %d. Deleted = %d. Existing = %d.\n", + p->nCreated, p->nDeleted, p->nCreated - p->nDeleted ); return 0; } // count the number of nodes in the table - if ( Dar_TableCountEntries(p) != Dar_ManAndNum(p) + Dar_ManExorNum(p) ) + if ( Dar_TableCountEntries(p) != Dar_ManAndNum(p) + Dar_ManExorNum(p) + Dar_ManLatchNum(p) ) { printf( "Dar_ManCheck: The number of nodes in the structural hashing table is wrong.\n" ); + printf( "Entries = %d. And = %d. Xor = %d. Lat = %d. Total = %d.\n", + Dar_TableCountEntries(p), Dar_ManAndNum(p), Dar_ManExorNum(p), Dar_ManLatchNum(p), + Dar_ManAndNum(p) + Dar_ManExorNum(p) + Dar_ManLatchNum(p) ); + return 0; } // if ( !Dar_ManIsAcyclic(p) ) diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c index 9f0f58f6a..d56cca459 100644 --- a/src/aig/dar/darCore.c +++ b/src/aig/dar/darCore.c @@ -76,7 +76,7 @@ int Dar_ManRewrite( Dar_Man_t * p ) pObjNew = Dar_LibBuildBest( p ); pObjNew = Dar_NotCond( pObjNew, pObjNew->fPhase ^ pObj->fPhase ); // remove the old nodes - Dar_ObjReplace( p, pObj, pObjNew ); + Dar_ObjReplace( p, pObj, pObjNew, 1 ); // compare the gains nNodeAfter = Dar_ManNodeNum( p ); assert( p->GainBest == nNodeBefore - nNodeAfter ); @@ -99,6 +99,8 @@ int Dar_ManRewrite( Dar_Man_t * p ) return 1; } + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/dar/darDfs.c b/src/aig/dar/darDfs.c index 1c2ab0576..bdb23c9d0 100644 --- a/src/aig/dar/darDfs.c +++ b/src/aig/dar/darDfs.c @@ -39,15 +39,18 @@ SeeAlso [] ***********************************************************************/ -void Dar_ManDfs_rec( Dar_Obj_t * pObj, Vec_Ptr_t * vNodes ) +void Dar_ManDfs_rec( Dar_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vNodes ) { assert( !Dar_IsComplement(pObj) ); - if ( !Dar_ObjIsNode(pObj) || Dar_ObjIsMarkA(pObj) ) + if ( pObj == NULL ) return; - Dar_ManDfs_rec( Dar_ObjFanin0(pObj), vNodes ); - Dar_ManDfs_rec( Dar_ObjFanin1(pObj), vNodes ); - assert( !Dar_ObjIsMarkA(pObj) ); // loop detection - Dar_ObjSetMarkA(pObj); + if ( Dar_ObjIsTravIdCurrent(p, pObj) ) + return; + assert( Dar_ObjIsNode(pObj) || Dar_ObjIsBuf(pObj) ); + Dar_ManDfs_rec( p, Dar_ObjFanin0(pObj), vNodes ); + Dar_ManDfs_rec( p, Dar_ObjFanin1(pObj), vNodes ); + assert( !Dar_ObjIsTravIdCurrent(p, pObj) ); // loop detection + Dar_ObjSetTravIdCurrent(p, pObj); Vec_PtrPush( vNodes, pObj ); } @@ -67,35 +70,21 @@ Vec_Ptr_t * Dar_ManDfs( Dar_Man_t * p ) Vec_Ptr_t * vNodes; Dar_Obj_t * pObj; int i; + Dar_ManIncrementTravId( p ); + // mark constant and PIs + Dar_ObjSetTravIdCurrent( p, Dar_ManConst1(p) ); + Dar_ManForEachPi( p, pObj, i ) + Dar_ObjSetTravIdCurrent( p, pObj ); + // if there are latches, mark them + if ( Dar_ManLatchNum(p) > 0 ) + Dar_ManForEachObj( p, pObj, i ) + if ( Dar_ObjIsLatch(pObj) ) + Dar_ObjSetTravIdCurrent( p, pObj ); + // go through the nodes vNodes = Vec_PtrAlloc( Dar_ManNodeNum(p) ); Dar_ManForEachObj( p, pObj, i ) - Dar_ManDfs_rec( pObj, vNodes ); - Dar_ManForEachObj( p, pObj, i ) - Dar_ObjClearMarkA(pObj); - return vNodes; -} - -/**Function************************************************************* - - Synopsis [Collects internal nodes in the DFS order.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Ptr_t * Dar_ManDfsNode( Dar_Man_t * p, Dar_Obj_t * pNode ) -{ - Vec_Ptr_t * vNodes; - Dar_Obj_t * pObj; - int i; - assert( !Dar_IsComplement(pNode) ); - vNodes = Vec_PtrAlloc( 16 ); - Dar_ManDfs_rec( pNode, vNodes ); - Vec_PtrForEachEntry( vNodes, pObj, i ) - Dar_ObjClearMarkA(pObj); + if ( Dar_ObjIsNode(pObj) || Dar_ObjIsBuf(pObj) ) + Dar_ManDfs_rec( p, pObj, vNodes ); return vNodes; } diff --git a/src/aig/dar/darMan.c b/src/aig/dar/darMan.c index bbac1360f..1b40bb39b 100644 --- a/src/aig/dar/darMan.c +++ b/src/aig/dar/darMan.c @@ -55,6 +55,7 @@ Dar_Man_t * Dar_ManStart( int nNodesMax ) // allocate arrays for nodes p->vPis = Vec_PtrAlloc( 100 ); p->vPos = Vec_PtrAlloc( 100 ); + p->vObjs = Vec_PtrAlloc( 1000 ); // prepare the internal memory manager p->pMemObjs = Dar_MmFixedStart( sizeof(Dar_Obj_t), nNodesMax ); p->pMemCuts = Dar_MmFlexStart(); @@ -66,7 +67,7 @@ Dar_Man_t * Dar_ManStart( int nNodesMax ) p->pConst1 = Dar_ManFetchMemory( p ); p->pConst1->Type = DAR_AIG_CONST1; p->pConst1->fPhase = 1; - p->nCreated = 1; + p->nObjs[DAR_AIG_CONST1]++; // start the table p->nTableSize = nNodesMax; p->pTable = ALLOC( Dar_Obj_t *, p->nTableSize ); @@ -100,10 +101,10 @@ void Dar_ManStop( Dar_Man_t * p ) // Dar_TableProfile( p ); Dar_MmFixedStop( p->pMemObjs, 0 ); Dar_MmFlexStop( p->pMemCuts, 0 ); - if ( p->vPis ) Vec_PtrFree( p->vPis ); - if ( p->vPos ) Vec_PtrFree( p->vPos ); - if ( p->vObjs ) Vec_PtrFree( p->vObjs ); - if ( p->vRequired ) Vec_IntFree( p->vRequired ); + if ( p->vPis ) Vec_PtrFree( p->vPis ); + if ( p->vPos ) Vec_PtrFree( p->vPos ); + if ( p->vObjs ) Vec_PtrFree( p->vObjs ); + if ( p->vRequired ) Vec_IntFree( p->vRequired ); if ( p->vLeavesBest ) Vec_PtrFree( p->vLeavesBest ); free( p->pTable ); free( p ); @@ -151,12 +152,15 @@ int Dar_ManCleanup( Dar_Man_t * p ) ***********************************************************************/ void Dar_ManPrintStats( Dar_Man_t * p ) { - printf( "PI/PO = %d/%d. ", Dar_ManPiNum(p), Dar_ManPoNum(p) ); - printf( "A = %7d. ", Dar_ManAndNum(p) ); - printf( "X = %5d. ", Dar_ManExorNum(p) ); - printf( "Cre = %7d. ", p->nCreated ); - printf( "Del = %7d. ", p->nDeleted ); - printf( "Lev = %3d. ", Dar_ManCountLevels(p) ); + printf( "PI/PO/Lat = %5d/%5d/%5d ", Dar_ManPiNum(p), Dar_ManPoNum(p), Dar_ManLatchNum(p) ); + printf( "A = %6d. ", Dar_ManAndNum(p) ); + if ( Dar_ManExorNum(p) ) + printf( "X = %5d. ", Dar_ManExorNum(p) ); + if ( Dar_ManBufNum(p) ) + printf( "B = %3d. ", Dar_ManBufNum(p) ); + printf( "Cre = %6d. ", p->nCreated ); + printf( "Del = %6d. ", p->nDeleted ); +// printf( "Lev = %3d. ", Dar_ManCountLevels(p) ); printf( "\n" ); } diff --git a/src/aig/dar/darObj.c b/src/aig/dar/darObj.c index faf9336e9..2db13c714 100644 --- a/src/aig/dar/darObj.c +++ b/src/aig/dar/darObj.c @@ -89,7 +89,7 @@ Dar_Obj_t * Dar_ObjCreate( Dar_Man_t * p, Dar_Obj_t * pGhost ) { Dar_Obj_t * pObj; assert( !Dar_IsComplement(pGhost) ); - assert( Dar_ObjIsNode(pGhost) ); + assert( Dar_ObjIsHash(pGhost) ); assert( pGhost == &p->Ghost ); // get memory for the new object pObj = Dar_ManFetchMemory( p ); @@ -116,7 +116,7 @@ Dar_Obj_t * Dar_ObjCreate( Dar_Man_t * p, Dar_Obj_t * pGhost ) void Dar_ObjConnect( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pFan0, Dar_Obj_t * pFan1 ) { assert( !Dar_IsComplement(pObj) ); - assert( Dar_ObjIsNode(pObj) ); + assert( !Dar_ObjIsPi(pObj) ); // add the first fanin pObj->pFanin0 = pFan0; pObj->pFanin1 = pFan1; @@ -137,7 +137,7 @@ void Dar_ObjConnect( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pFan0, Dar_Obj pObj->fPhase = Dar_ObjFaninPhase(pFan0); } // add the node to the structural hash table - if ( Dar_ObjIsNode(pObj) ) + if ( Dar_ObjIsHash(pObj) ) Dar_TableInsert( p, pObj ); } @@ -161,7 +161,7 @@ void Dar_ObjDisconnect( Dar_Man_t * p, Dar_Obj_t * pObj ) if ( pObj->pFanin1 != NULL ) Dar_ObjDeref(Dar_ObjFanin1(pObj)); // remove the node from the structural hash table - if ( Dar_ObjIsNode(pObj) ) + if ( Dar_ObjIsHash(pObj) ) Dar_TableDelete( p, pObj ); // add the first fanin pObj->pFanin0 = NULL; @@ -184,7 +184,7 @@ void Dar_ObjDelete( Dar_Man_t * p, Dar_Obj_t * pObj ) assert( !Dar_IsComplement(pObj) ); assert( !Dar_ObjIsTerm(pObj) ); assert( Dar_ObjRefs(pObj) == 0 ); - p->nDeleted++; + p->nObjs[pObj->Type]--; Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL ); Dar_ManRecycleMemory( p, pObj ); } @@ -206,11 +206,10 @@ void Dar_ObjDelete_rec( Dar_Man_t * p, Dar_Obj_t * pObj, int fFreeTop ) assert( !Dar_IsComplement(pObj) ); if ( Dar_ObjIsConst1(pObj) || Dar_ObjIsPi(pObj) ) return; - assert( Dar_ObjIsNode(pObj) ); + assert( !Dar_ObjIsPo(pObj) ); pFanin0 = Dar_ObjFanin0(pObj); pFanin1 = Dar_ObjFanin1(pObj); Dar_ObjDisconnect( p, pObj ); - p->nObjs[pObj->Type]--; if ( fFreeTop ) Dar_ObjDelete( p, pObj ); if ( pFanin0 && !Dar_ObjIsNone(pFanin0) && Dar_ObjRefs(pFanin0) == 0 ) @@ -219,6 +218,33 @@ void Dar_ObjDelete_rec( Dar_Man_t * p, Dar_Obj_t * pObj, int fFreeTop ) Dar_ObjDelete_rec( p, pFanin1, 1 ); } +/**Function************************************************************* + + Synopsis [Replaces the first fanin of the node by the new fanin.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ObjPatchFanin0( Dar_Man_t * p, Dar_Obj_t * pObj, Dar_Obj_t * pFaninNew ) +{ + Dar_Obj_t * pFaninOld; + assert( !Dar_IsComplement(pObj) ); + pFaninOld = Dar_ObjFanin0(pObj); + // decrement ref and remove fanout + Dar_ObjDeref( pFaninOld ); + // update the fanin + pObj->pFanin0 = pFaninNew; + // increment ref and add fanout + Dar_ObjRef( Dar_Regular(pFaninNew) ); + // get rid of old fanin + if ( !Dar_ObjIsPi(pFaninOld) && !Dar_ObjIsConst1(pFaninOld) && Dar_ObjRefs(pFaninOld) == 0 ) + Dar_ObjDelete_rec( p, pFaninOld, 1 ); +} + /**Function************************************************************* Synopsis [Replaces one object by another.] @@ -232,27 +258,27 @@ void Dar_ObjDelete_rec( Dar_Man_t * p, Dar_Obj_t * pObj, int fFreeTop ) SeeAlso [] ***********************************************************************/ -void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew ) +void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew, int fNodesOnly ) { Dar_Obj_t * pObjNewR = Dar_Regular(pObjNew); // the object to be replaced cannot be complemented assert( !Dar_IsComplement(pObjOld) ); // the object to be replaced cannot be a terminal assert( !Dar_ObjIsPi(pObjOld) && !Dar_ObjIsPo(pObjOld) ); - // the object to be used cannot be a buffer + // the object to be used cannot be a buffer or a PO assert( !Dar_ObjIsBuf(pObjNewR) && !Dar_ObjIsPo(pObjNewR) ); // the object cannot be the same assert( pObjOld != pObjNewR ); // make sure object is not pointing to itself - assert( pObjOld != Dar_ObjFanin0(pObjNewR) ); +// assert( pObjOld != Dar_ObjFanin0(pObjNewR) ); assert( pObjOld != Dar_ObjFanin1(pObjNewR) ); - // delete the old node + // recursively delete the old node - but leave the object there Dar_ObjDelete_rec( p, pObjOld, 0 ); // if the new object is complemented or already used, create a buffer - if ( Dar_IsComplement(pObjNew) || Dar_ObjRefs(pObjNew) > 0 || !Dar_ObjIsNode(pObjNew) ) + p->nObjs[pObjOld->Type]--; + if ( Dar_IsComplement(pObjNew) || Dar_ObjRefs(pObjNew) > 0 || (fNodesOnly && !Dar_ObjIsNode(pObjNew)) ) { pObjOld->Type = DAR_AIG_BUF; - p->nObjs[pObjOld->Type]++; Dar_ObjConnect( p, pObjOld, pObjNew, NULL ); } else @@ -261,9 +287,10 @@ void Dar_ObjReplace( Dar_Man_t * p, Dar_Obj_t * pObjOld, Dar_Obj_t * pObjNew ) Dar_Obj_t * pFanin1 = pObjNew->pFanin1; pObjOld->Type = pObjNew->Type; Dar_ObjDisconnect( p, pObjNew ); - Dar_ObjDelete( p, pObjNew ); Dar_ObjConnect( p, pObjOld, pFanin0, pFanin1 ); + Dar_ObjDelete( p, pObjNew ); } + p->nObjs[pObjOld->Type]++; } //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/dar/darOper.c b/src/aig/dar/darOper.c index 8921fe335..cfb89e312 100644 --- a/src/aig/dar/darOper.c +++ b/src/aig/dar/darOper.c @@ -87,6 +87,43 @@ Dar_Obj_t * Dar_Oper( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1, Dar_Type_t return NULL; } +/**Function************************************************************* + + Synopsis [Creates the canonical form of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dar_Obj_t * Dar_CanonPair_rec( Dar_Man_t * p, Dar_Obj_t * pGhost ) +{ + Dar_Obj_t * pResult, * pLat0, * pLat1; + int fCompl0, fCompl1; + Dar_Type_t Type; + assert( Dar_ObjIsNode(pGhost) ); + // consider the case when the pair is canonical + if ( !Dar_ObjIsLatch(Dar_ObjFanin0(pGhost)) || !Dar_ObjIsLatch(Dar_ObjFanin1(pGhost)) ) + { + if ( pResult = Dar_TableLookup( p, pGhost ) ) + return pResult; + return Dar_ObjCreate( p, pGhost ); + } + /// remember the latches + pLat0 = Dar_ObjFanin0(pGhost); + pLat1 = Dar_ObjFanin1(pGhost); + // remember type and compls + Type = Dar_ObjType(pGhost); + fCompl0 = Dar_ObjFaninC0(pGhost); + fCompl1 = Dar_ObjFaninC1(pGhost); + // call recursively + pResult = Dar_Oper( p, Dar_NotCond(Dar_ObjChild0(pLat0), fCompl0), Dar_NotCond(Dar_ObjChild0(pLat1), fCompl1), Type ); + // build latch on top of this + return Dar_Latch( p, pResult, (Type == DAR_AIG_AND)? fCompl0 & fCompl1 : fCompl0 ^ fCompl1 ); +} + /**Function************************************************************* Synopsis [Performs canonicization step.] @@ -114,11 +151,30 @@ Dar_Obj_t * Dar_And( Dar_Man_t * p, Dar_Obj_t * p0, Dar_Obj_t * p1 ) // check if it can be an EXOR gate // if ( Dar_ObjIsExorType( p0, p1, &pFan0, &pFan1 ) ) // return Dar_Exor( p, pFan0, pFan1 ); - // check the table pGhost = Dar_ObjCreateGhost( p, p0, p1, DAR_AIG_AND ); - if ( pResult = Dar_TableLookup( p, pGhost ) ) - return pResult; - return Dar_ObjCreate( p, pGhost ); + pResult = Dar_CanonPair_rec( p, pGhost ); + return pResult; +} + +/**Function************************************************************* + + Synopsis [Creates the canonical form of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dar_Obj_t * Dar_Latch( Dar_Man_t * p, Dar_Obj_t * pObj, int fInitOne ) +{ + Dar_Obj_t * pGhost, * pResult; + pGhost = Dar_ObjCreateGhost( p, Dar_NotCond(pObj, fInitOne), NULL, DAR_AIG_LATCH ); + pResult = Dar_TableLookup( p, pGhost ); + if ( pResult == NULL ) + pResult = Dar_ObjCreate( p, pGhost ); + return Dar_NotCond( pResult, fInitOne ); } /**Function************************************************************* diff --git a/src/aig/dar/darSeq.c b/src/aig/dar/darSeq.c new file mode 100644 index 000000000..bf3807f4c --- /dev/null +++ b/src/aig/dar/darSeq.c @@ -0,0 +1,471 @@ +/**CFile**************************************************************** + + FileName [darSeq.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [DAG-aware AIG rewriting.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: darSeq.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "dar.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Converts combinational AIG manager into a sequential one.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ManSeqStrashConvert( Dar_Man_t * p, int nLatches, int * pInits ) +{ + Dar_Obj_t * pObjLi, * pObjLo, * pLatch; + int i; + // collect the POs to be converted into latches + for ( i = 0; i < nLatches; i++ ) + { + // get the corresponding PI/PO pair + pObjLi = Dar_ManPo( p, Dar_ManPoNum(p) - nLatches + i ); + pObjLo = Dar_ManPi( p, Dar_ManPiNum(p) - nLatches + i ); + // create latch + pLatch = Dar_Latch( p, Dar_ObjChild0(pObjLi), pInits? pInits[i] : 0 ); + // recycle the old PO object + Dar_ObjDisconnect( p, pObjLi ); + Vec_PtrWriteEntry( p->vObjs, pObjLi->Id, NULL ); + Dar_ManRecycleMemory( p, pObjLi ); + // convert the corresponding PI to be a buffer and connect it to the latch + pObjLo->Type = DAR_AIG_BUF; + Dar_ObjConnect( p, pObjLo, pLatch, NULL ); + } + // shrink the arrays + Vec_PtrShrink( p->vPis, Dar_ManPiNum(p) - nLatches ); + Vec_PtrShrink( p->vPos, Dar_ManPoNum(p) - nLatches ); + // update the counters of different objects + p->nObjs[DAR_AIG_PI] -= nLatches; + p->nObjs[DAR_AIG_PO] -= nLatches; + p->nObjs[DAR_AIG_BUF] += nLatches; +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ManDfsSeq_rec( Dar_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + assert( !Dar_IsComplement(pObj) ); + if ( pObj == NULL ) + return; + if ( Dar_ObjIsTravIdCurrent( p, pObj ) ) + return; + Dar_ObjSetTravIdCurrent( p, pObj ); + if ( Dar_ObjIsPi(pObj) ) + return; + Dar_ManDfsSeq_rec( p, Dar_ObjFanin0(pObj), vNodes ); + Dar_ManDfsSeq_rec( p, Dar_ObjFanin1(pObj), vNodes ); + Vec_PtrPush( vNodes, pObj ); +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Dar_ManDfsSeq( Dar_Man_t * p ) +{ + Vec_Ptr_t * vNodes; + Dar_Obj_t * pObj; + int i; + Dar_ManIncrementTravId( p ); + vNodes = Vec_PtrAlloc( Dar_ManNodeNum(p) ); + Dar_ManForEachPo( p, pObj, i ) + Dar_ManDfsSeq_rec( p, Dar_ObjFanin0(pObj), vNodes ); + return vNodes; +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ManDfsUnreach_rec( Dar_Man_t * p, Dar_Obj_t * pObj, Vec_Ptr_t * vNodes ) +{ + assert( !Dar_IsComplement(pObj) ); + if ( pObj == NULL ) + return; + if ( Dar_ObjIsTravIdPrevious(p, pObj) || Dar_ObjIsTravIdCurrent(p, pObj) ) + return; + Dar_ObjSetTravIdPrevious( p, pObj ); // assume unknown + Dar_ManDfsUnreach_rec( p, Dar_ObjFanin0(pObj), vNodes ); + Dar_ManDfsUnreach_rec( p, Dar_ObjFanin1(pObj), vNodes ); + if ( Dar_ObjIsTravIdPrevious(p, Dar_ObjFanin0(pObj)) && + (Dar_ObjFanin1(pObj) == NULL || Dar_ObjIsTravIdPrevious(p, Dar_ObjFanin1(pObj))) ) + Vec_PtrPush( vNodes, pObj ); + else + Dar_ObjSetTravIdCurrent( p, pObj ); +} + +/**Function************************************************************* + + Synopsis [Collects internal nodes unreachable from PIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Ptr_t * Dar_ManDfsUnreach( Dar_Man_t * p ) +{ + Vec_Ptr_t * vNodes; + Dar_Obj_t * pObj, * pFanin; + int i, k;//, RetValue; + // collect unreachable nodes + Dar_ManIncrementTravId( p ); + Dar_ManIncrementTravId( p ); + // mark the constant and PIs + Dar_ObjSetTravIdPrevious( p, Dar_ManConst1(p) ); + Dar_ManForEachPi( p, pObj, i ) + Dar_ObjSetTravIdCurrent( p, pObj ); + // curr marks visited nodes reachable from PIs + // prev marks visited nodes unreachable or unknown + + // collect the unreachable nodes + vNodes = Vec_PtrAlloc( 32 ); + Dar_ManForEachPo( p, pObj, i ) + Dar_ManDfsUnreach_rec( p, Dar_ObjFanin0(pObj), vNodes ); + + // refine resulting nodes + do + { + k = 0; + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + assert( Dar_ObjIsTravIdPrevious(p, pObj) ); + if ( Dar_ObjIsLatch(pObj) || Dar_ObjIsBuf(pObj) ) + { + pFanin = Dar_ObjFanin0(pObj); + assert( Dar_ObjIsTravIdPrevious(p, pFanin) || Dar_ObjIsTravIdCurrent(p, pFanin) ); + if ( Dar_ObjIsTravIdCurrent(p, pFanin) ) + { + Dar_ObjSetTravIdCurrent( p, pObj ); + continue; + } + } + else // AND gate + { + assert( Dar_ObjIsNode(pObj) ); + pFanin = Dar_ObjFanin0(pObj); + assert( Dar_ObjIsTravIdPrevious(p, pFanin) || Dar_ObjIsTravIdCurrent(p, pFanin) ); + if ( Dar_ObjIsTravIdCurrent(p, pFanin) ) + { + Dar_ObjSetTravIdCurrent( p, pObj ); + continue; + } + pFanin = Dar_ObjFanin1(pObj); + assert( Dar_ObjIsTravIdPrevious(p, pFanin) || Dar_ObjIsTravIdCurrent(p, pFanin) ); + if ( Dar_ObjIsTravIdCurrent(p, pFanin) ) + { + Dar_ObjSetTravIdCurrent( p, pObj ); + continue; + } + } + // write it back + Vec_PtrWriteEntry( vNodes, k++, pObj ); + } + Vec_PtrShrink( vNodes, k ); + } + while ( k < i ); + + if ( Vec_PtrSize(vNodes) > 0 ) + printf( "Found %d unreachable.\n", Vec_PtrSize(vNodes) ); + return vNodes; + +/* + // the resulting array contains all unreachable nodes except const 1 + if ( Vec_PtrSize(vNodes) == 0 ) + { + Vec_PtrFree( vNodes ); + return 0; + } + RetValue = Vec_PtrSize(vNodes); + + // mark these nodes + Dar_ManIncrementTravId( p ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + Dar_ObjSetTravIdCurrent( p, pObj ); + Vec_PtrFree( vNodes ); + return RetValue; +*/ +} + + +/**Function************************************************************* + + Synopsis [Removes nodes that do not fanout into POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar_ManRemoveUnmarked( Dar_Man_t * p ) +{ + Vec_Ptr_t * vNodes; + Dar_Obj_t * pObj; + int i, RetValue; + // collect unmarked nodes + vNodes = Vec_PtrAlloc( 100 ); + Dar_ManForEachObj( p, pObj, i ) + { + if ( Dar_ObjIsTerm(pObj) ) + continue; + if ( Dar_ObjIsTravIdCurrent(p, pObj) ) + continue; +//Dar_ObjPrintVerbose( pObj, 0 ); + Dar_ObjDisconnect( p, pObj ); + Vec_PtrPush( vNodes, pObj ); + } + if ( Vec_PtrSize(vNodes) == 0 ) + { + Vec_PtrFree( vNodes ); + return 0; + } + // remove the dangling objects + RetValue = Vec_PtrSize(vNodes); + Vec_PtrForEachEntry( vNodes, pObj, i ) + Dar_ObjDelete( p, pObj ); + printf( "Removes %d dangling.\n", Vec_PtrSize(vNodes) ); + Vec_PtrFree( vNodes ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline Dar_Obj_t * Dar_ObjReal_rec( Dar_Obj_t * pObj ) +{ + Dar_Obj_t * pObjNew, * pObjR = Dar_Regular(pObj); + if ( !Dar_ObjIsBuf(pObjR) ) + return pObj; + pObjNew = Dar_ObjReal_rec( Dar_ObjChild0(pObjR) ); + return Dar_NotCond( pObjNew, Dar_IsComplement(pObj) ); +} + +/**Function************************************************************* + + Synopsis [Rehashes the nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar_ManSeqRehashOne( Dar_Man_t * p, Vec_Ptr_t * vNodes, Vec_Ptr_t * vUnreach ) +{ + Dar_Obj_t * pObj, * pObjNew, * pFanin0, * pFanin1; + int i, RetValue = 0; + // mark the unreachable nodes + Dar_ManIncrementTravId( p ); + Vec_PtrForEachEntry( vUnreach, pObj, i ) + Dar_ObjSetTravIdCurrent(p, pObj); + // go through the nodes while skipping unreachable + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + // skip nodes unreachable from the PIs + if ( Dar_ObjIsTravIdCurrent(p, pObj) ) + continue; + // process the node + if ( Dar_ObjIsPo(pObj) ) + { + if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) ) + continue; + pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) ); + Dar_ObjPatchFanin0( p, pObj, pFanin0 ); + continue; + } + if ( Dar_ObjIsLatch(pObj) ) + { + if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) ) + continue; + pObjNew = Dar_ObjReal_rec( Dar_ObjChild0(pObj) ); + pObjNew = Dar_Latch( p, pObjNew, 0 ); + Dar_ObjReplace( p, pObj, pObjNew, 1 ); + RetValue = 1; + continue; + } + if ( Dar_ObjIsNode(pObj) ) + { + if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) && !Dar_ObjIsBuf(Dar_ObjFanin1(pObj)) ) + continue; + pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) ); + pFanin1 = Dar_ObjReal_rec( Dar_ObjChild1(pObj) ); + pObjNew = Dar_And( p, pFanin0, pFanin1 ); + Dar_ObjReplace( p, pObj, pObjNew, 1 ); + RetValue = 1; + continue; + } + } + return RetValue; +} + +/**Function************************************************************* + + Synopsis [If AIG contains buffers, this procedure removes them.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Dar_ManRemoveBuffers( Dar_Man_t * p ) +{ + Dar_Obj_t * pObj, * pObjNew, * pFanin0, * pFanin1; + int i; + if ( Dar_ManBufNum(p) == 0 ) + return; + Dar_ManForEachObj( p, pObj, i ) + { + if ( Dar_ObjIsPo(pObj) ) + { + if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) ) + continue; + pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) ); + Dar_ObjPatchFanin0( p, pObj, pFanin0 ); + } + else if ( Dar_ObjIsLatch(pObj) ) + { + if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) ) + continue; + pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) ); + pObjNew = Dar_Latch( p, pFanin0, 0 ); + Dar_ObjReplace( p, pObj, pObjNew, 0 ); + } + else if ( Dar_ObjIsAnd(pObj) ) + { + if ( !Dar_ObjIsBuf(Dar_ObjFanin0(pObj)) && !Dar_ObjIsBuf(Dar_ObjFanin1(pObj)) ) + continue; + pFanin0 = Dar_ObjReal_rec( Dar_ObjChild0(pObj) ); + pFanin1 = Dar_ObjReal_rec( Dar_ObjChild1(pObj) ); + pObjNew = Dar_And( p, pFanin0, pFanin1 ); + Dar_ObjReplace( p, pObj, pObjNew, 0 ); + } + } + assert( Dar_ManBufNum(p) == 0 ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dar_ManSeqStrash( Dar_Man_t * p, int nLatches, int * pInits ) +{ + Vec_Ptr_t * vNodes, * vUnreach; + Dar_Obj_t * pObj; + int i; + int RetValue = 1; + // create latches out of the additional PI/PO pairs + Dar_ManSeqStrashConvert( p, nLatches, pInits ); + // iteratively rehash the network + while ( RetValue ) + { + Dar_ManPrintStats( p ); + + Dar_ManForEachObj( p, pObj, i ) + assert( pObj->Type > 0 ); + + // mark nodes unreachable from the PIs + vUnreach = Dar_ManDfsUnreach( p ); + // collect nodes reachable from the POs + vNodes = Dar_ManDfsSeq( p ); + // remove nodes unreachable from the POs + Dar_ManRemoveUnmarked( p ); + // continue rehashing as long as there are changes + RetValue = Dar_ManSeqRehashOne( p, vNodes, vUnreach ); + Vec_PtrFree( vNodes ); + Vec_PtrFree( vUnreach ); + } + // perform the final cleanup + Dar_ManIncrementTravId( p ); + vNodes = Dar_ManDfsSeq( p ); + Dar_ManRemoveUnmarked( p ); + Vec_PtrFree( vNodes ); + // remove buffers if they are left +// Dar_ManRemoveBuffers( p ); + // clean up + if ( !Dar_ManCheck( p ) ) + { + printf( "Dar_ManSeqStrash: The network check has failed.\n" ); + return 0; + } + return 1; + +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/aig/dar/darTable.c b/src/aig/dar/darTable.c index 8b4bfaf3e..af9956ec0 100644 --- a/src/aig/dar/darTable.c +++ b/src/aig/dar/darTable.c @@ -39,8 +39,15 @@ static unsigned long Dar_Hash( Dar_Obj_t * pObj, int TableSize ) static Dar_Obj_t ** Dar_TableFind( Dar_Man_t * p, Dar_Obj_t * pObj ) { Dar_Obj_t ** ppEntry; - assert( Dar_ObjChild0(pObj) && Dar_ObjChild1(pObj) ); - assert( Dar_ObjFanin0(pObj)->Id < Dar_ObjFanin1(pObj)->Id ); + if ( Dar_ObjIsLatch(pObj) ) + { + assert( Dar_ObjChild0(pObj) && Dar_ObjChild1(pObj) == NULL ); + } + else + { + assert( Dar_ObjChild0(pObj) && Dar_ObjChild1(pObj) ); + assert( Dar_ObjFanin0(pObj)->Id < Dar_ObjFanin1(pObj)->Id ); + } for ( ppEntry = p->pTable + Dar_Hash(pObj, p->nTableSize); *ppEntry; ppEntry = &(*ppEntry)->pNext ) if ( *ppEntry == pObj ) return ppEntry; @@ -70,10 +77,20 @@ Dar_Obj_t * Dar_TableLookup( Dar_Man_t * p, Dar_Obj_t * pGhost ) { Dar_Obj_t * pEntry; assert( !Dar_IsComplement(pGhost) ); - assert( Dar_ObjChild0(pGhost) && Dar_ObjChild1(pGhost) ); - assert( Dar_ObjFanin0(pGhost)->Id < Dar_ObjFanin1(pGhost)->Id ); - if ( !Dar_ObjRefs(Dar_ObjFanin0(pGhost)) || !Dar_ObjRefs(Dar_ObjFanin1(pGhost)) ) - return NULL; + if ( pGhost->Type == DAR_AIG_LATCH ) + { + assert( Dar_ObjChild0(pGhost) && Dar_ObjChild1(pGhost) == NULL ); + if ( !Dar_ObjRefs(Dar_ObjFanin0(pGhost)) ) + return NULL; + } + else + { + assert( pGhost->Type == DAR_AIG_AND ); + assert( Dar_ObjChild0(pGhost) && Dar_ObjChild1(pGhost) ); + assert( Dar_ObjFanin0(pGhost)->Id < Dar_ObjFanin1(pGhost)->Id ); + if ( !Dar_ObjRefs(Dar_ObjFanin0(pGhost)) || !Dar_ObjRefs(Dar_ObjFanin1(pGhost)) ) + return NULL; + } for ( pEntry = p->pTable[Dar_Hash(pGhost, p->nTableSize)]; pEntry; pEntry = pEntry->pNext ) { if ( Dar_ObjChild0(pEntry) == Dar_ObjChild0(pGhost) && diff --git a/src/base/abc/abcDfs.c b/src/base/abc/abcDfs.c index b682f8aec..39e985c0e 100644 --- a/src/base/abc/abcDfs.c +++ b/src/base/abc/abcDfs.c @@ -55,7 +55,10 @@ void Abc_NtkDfs_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vNodes ) assert( Abc_ObjIsNode( pNode ) || Abc_ObjIsBox( pNode ) ); // visit the transitive fanin of the node Abc_ObjForEachFanin( pNode, pFanin, i ) + { +// pFanin = Abc_ObjFanin( pNode, Abc_ObjFaninNum(pNode)-1-i ); Abc_NtkDfs_rec( Abc_ObjFanin0Ntk(pFanin), vNodes ); + } // add the node after the fanins have been added Vec_PtrPush( vNodes, pNode ); } diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index ce187f607..7d8d0f0fd 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -987,7 +987,7 @@ void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk ) Abc_Obj_t * pNet, * pNode; int i; - if ( Abc_NtkNodeNum(pNtk) == 0 ) + if ( Abc_NtkNodeNum(pNtk) == 0 && Abc_NtkBoxNum(pNtk) == 0 ) return; // check for non-driven nets diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 1e0fed0cf..d5321e6d1 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -330,7 +330,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) // Kit_TruthCountMintermsPrecomp(); // Kit_DsdPrecompute4Vars(); - Dar_LibStart(); +// Dar_LibStart(); } /**Function************************************************************* @@ -346,7 +346,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) ***********************************************************************/ void Abc_End() { - Dar_LibStop(); +// Dar_LibStop(); Abc_NtkFraigStoreClean(); // Rwt_Man4ExplorePrint(); @@ -5931,7 +5931,7 @@ usage: int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) { FILE * pOut, * pErr; - Abc_Ntk_t * pNtk;//, * pNtkRes; + Abc_Ntk_t * pNtk, * pNtkRes; int c; int nLevels; // extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk ); @@ -5940,6 +5940,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // extern int Pr_ManProofTest( char * pFileName ); extern void Abc_NtkCompareSupports( Abc_Ntk_t * pNtk ); extern void Abc_NtkCompareCones( Abc_Ntk_t * pNtk ); + extern Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -6049,8 +6050,21 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) // Abc_Ntk4VarTable( pNtk ); // Dat_NtkGenerateArrays( pNtk ); - return 0; + if ( !Abc_NtkIsStrash(pNtk) ) + { + fprintf( pErr, "Network should be strashed. Command has failed.\n" ); + return 1; + } + pNtkRes = Abc_NtkDar( pNtk ); + if ( pNtkRes == NULL ) + { + fprintf( pErr, "Command has failed.\n" ); + return 1; + } + // replace the current network + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; usage: fprintf( pErr, "usage: test [-h]\n" ); fprintf( pErr, "\t testbench for new procedures\n" ); @@ -7286,6 +7300,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) int fAllNodes; int fExdc; int c; + int fPartition = 0; pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -7307,7 +7322,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) pParams->fVerbose = 0; // the verbosiness flag pParams->fVerboseP = 0; // the verbosiness flag Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "RDCrscpvaeh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "RDCrscptvaeh" ) ) != EOF ) { switch ( c ) { @@ -7360,6 +7375,9 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'v': pParams->fVerbose ^= 1; break; + case 't': + fPartition ^= 1; + break; case 'a': fAllNodes ^= 1; break; @@ -7388,13 +7406,28 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) pParams->fVerboseP = pParams->fTryProve; // get the new network - if ( Abc_NtkIsStrash(pNtk) ) - pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc ); + if ( fPartition ) + { + pNtkRes = Abc_NtkDup( pNtk ); + if ( Abc_NtkIsStrash(pNtk) ) + Abc_NtkFraigPartitionedTime( pNtk, &Params ); + else + { + pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 ); + Abc_NtkFraigPartitionedTime( pNtk, &Params ); + Abc_NtkDelete( pNtk ); + } + } else { - pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 ); - pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc ); - Abc_NtkDelete( pNtk ); + if ( Abc_NtkIsStrash(pNtk) ) + pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc ); + else + { + pNtk = Abc_NtkStrash( pNtk, fAllNodes, !fAllNodes, 0 ); + pNtkRes = Abc_NtkFraig( pNtk, &Params, fAllNodes, fExdc ); + Abc_NtkDelete( pNtk ); + } } if ( pNtkRes == NULL ) { @@ -7411,7 +7444,7 @@ int Abc_CommandFraig( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: sprintf( Buffer, "%d", pParams->nBTLimit ); - fprintf( pErr, "usage: fraig [-R num] [-D num] [-C num] [-rscpvah]\n" ); + fprintf( pErr, "usage: fraig [-R num] [-D num] [-C num] [-rscpvtah]\n" ); fprintf( pErr, "\t transforms a logic network into a functionally reduced AIG\n" ); fprintf( pErr, "\t-R num : number of random patterns (127 < num < 32769) [default = %d]\n", pParams->nPatsRand ); fprintf( pErr, "\t-D num : number of systematic patterns (127 < num < 32769) [default = %d]\n", pParams->nPatsDyna ); @@ -7423,6 +7456,7 @@ usage: fprintf( pErr, "\t-v : toggle verbose output [default = %s]\n", pParams->fVerbose? "yes": "no" ); fprintf( pErr, "\t-e : toggle functional sweeping using EXDC [default = %s]\n", fExdc? "yes": "no" ); fprintf( pErr, "\t-a : toggle between all nodes and DFS nodes [default = %s]\n", fAllNodes? "all": "dfs" ); + fprintf( pErr, "\t-t : toggle using partitioned representation [default = %s]\n", fPartition? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index 0863061b8..812785156 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -25,60 +25,10 @@ /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -static Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk ); -static Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -/**Function************************************************************* - - Synopsis [Gives the current ABC network to AIG manager for processing.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ) -{ - Abc_Ntk_t * pNtkAig; - Dar_Man_t * pMan;//, * pTemp; - assert( Abc_NtkIsStrash(pNtk) ); - // convert to the AIG manager - pMan = Abc_NtkToDar( pNtk ); - if ( pMan == NULL ) - return NULL; - if ( !Dar_ManCheck( pMan ) ) - { - printf( "Abc_NtkDar: AIG check has failed.\n" ); - Dar_ManStop( pMan ); - return NULL; - } - // perform balance - Dar_ManPrintStats( pMan ); -// Dar_ManDumpBlif( pMan, "aig_temp.blif" ); - pMan->pPars = Dar_ManDefaultParams(); - Dar_ManRewrite( pMan ); - Dar_ManPrintStats( pMan ); - // convert from the AIG manager - pNtkAig = Abc_NtkFromDar( pNtk, pMan ); - if ( pNtkAig == NULL ) - return NULL; - Dar_ManStop( pMan ); - // make sure everything is okay - if ( !Abc_NtkCheck( pNtkAig ) ) - { - printf( "Abc_NtkDar: The network check has failed.\n" ); - Abc_NtkDelete( pNtkAig ); - return NULL; - } - return pNtkAig; -} - /**Function************************************************************* Synopsis [Converts the network from the AIG manager into ABC.] @@ -96,7 +46,7 @@ Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk ) Abc_Obj_t * pObj; int i; // create the manager - pMan = Dar_ManStart( Abc_NtkNodeNum(pNtk) ); + pMan = Dar_ManStart( Abc_NtkNodeNum(pNtk) + 100 ); // transfer the pointers to the basic nodes Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Dar_ManConst1(pMan); Abc_NtkForEachCi( pNtk, pObj, i ) @@ -122,14 +72,14 @@ Dar_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk ) SeeAlso [] ***********************************************************************/ -Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtk, Dar_Man_t * pMan ) +Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan ) { Vec_Ptr_t * vNodes; Abc_Ntk_t * pNtkNew; Dar_Obj_t * pObj; int i; // perform strashing - pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG ); + pNtkNew = Abc_NtkStartFrom( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); // transfer the pointers to the basic nodes Dar_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew); Dar_ManForEachPi( pMan, pObj, i ) @@ -147,6 +97,159 @@ Abc_Ntk_t * Abc_NtkFromDar( Abc_Ntk_t * pNtk, Dar_Man_t * pMan ) return pNtkNew; } +/**Function************************************************************* + + Synopsis [Converts the network from the AIG manager into ABC.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkFromDarSeq( Abc_Ntk_t * pNtkOld, Dar_Man_t * pMan ) +{ + Vec_Ptr_t * vNodes; + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pObjNew, * pFaninNew, * pFaninNew0, * pFaninNew1; + Dar_Obj_t * pObj; + int i; +// assert( Dar_ManLatchNum(pMan) > 0 ); + // perform strashing + pNtkNew = Abc_NtkStartFromNoLatches( pNtkOld, ABC_NTK_STRASH, ABC_FUNC_AIG ); + // transfer the pointers to the basic nodes + Dar_ManConst1(pMan)->pData = Abc_AigConst1(pNtkNew); + Dar_ManForEachPi( pMan, pObj, i ) + pObj->pData = Abc_NtkPi(pNtkNew, i); + // create latches of the new network + Dar_ManForEachObj( pMan, pObj, i ) + { + if ( !Dar_ObjIsLatch(pObj) ) + continue; + pObjNew = Abc_NtkCreateLatch( pNtkNew ); + pFaninNew0 = Abc_NtkCreateBi( pNtkNew ); + pFaninNew1 = Abc_NtkCreateBo( pNtkNew ); + Abc_ObjAddFanin( pObjNew, pFaninNew0 ); + Abc_ObjAddFanin( pFaninNew1, pObjNew ); + Abc_LatchSetInit0( pObjNew ); + pObj->pData = Abc_ObjFanout0( pObjNew ); + } + Abc_NtkAddDummyBoxNames( pNtkNew ); + // rebuild the AIG + vNodes = Dar_ManDfs( pMan ); + Vec_PtrForEachEntry( vNodes, pObj, i ) + { + // add the first fanin + pObj->pData = pFaninNew0 = (Abc_Obj_t *)Dar_ObjChild0Copy(pObj); + if ( Dar_ObjIsBuf(pObj) ) + continue; + // add the second fanin + pFaninNew1 = (Abc_Obj_t *)Dar_ObjChild1Copy(pObj); + // create the new node + if ( Dar_ObjIsExor(pObj) ) + pObj->pData = pObjNew = Abc_AigXor( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 ); + else + pObj->pData = pObjNew = Abc_AigAnd( pNtkNew->pManFunc, pFaninNew0, pFaninNew1 ); + } + Vec_PtrFree( vNodes ); + // connect the PO nodes + Dar_ManForEachPo( pMan, pObj, i ) + { + pFaninNew = (Abc_Obj_t *)Dar_ObjChild0Copy( pObj ); + Abc_ObjAddFanin( Abc_NtkPo(pNtkNew, i), pFaninNew ); + } + // connect the latches + Dar_ManForEachObj( pMan, pObj, i ) + { + if ( !Dar_ObjIsLatch(pObj) ) + continue; + pFaninNew = (Abc_Obj_t *)Dar_ObjChild0Copy( pObj ); + Abc_ObjAddFanin( Abc_ObjFanin0(Abc_ObjFanin0(pObj->pData)), pFaninNew ); + } + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkFromIvySeq(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Collect latch values.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int * Abc_NtkGetLatchValues( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pLatch; + int i, * pArray; + pArray = ALLOC( int, Abc_NtkLatchNum(pNtk) ); + Abc_NtkForEachLatch( pNtk, pLatch, i ) + pArray[i] = Abc_LatchIsInit1(pLatch); + return pArray; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ) +{ + Abc_Ntk_t * pNtkAig; + Dar_Man_t * pMan;//, * pTemp; + int * pArray; + + assert( Abc_NtkIsStrash(pNtk) ); + // convert to the AIG manager + pMan = Abc_NtkToDar( pNtk ); + if ( pMan == NULL ) + return NULL; + if ( !Dar_ManCheck( pMan ) ) + { + printf( "Abc_NtkDar: AIG check has failed.\n" ); + Dar_ManStop( pMan ); + return NULL; + } + // perform balance + Dar_ManPrintStats( pMan ); + + pArray = Abc_NtkGetLatchValues(pNtk); + Dar_ManSeqStrash( pMan, Abc_NtkLatchNum(pNtk), pArray ); + free( pArray ); + +// Dar_ManDumpBlif( pMan, "aig_temp.blif" ); +// pMan->pPars = Dar_ManDefaultParams(); +// Dar_ManRewrite( pMan ); + Dar_ManPrintStats( pMan ); + // convert from the AIG manager + if ( Dar_ManLatchNum(pMan) ) + pNtkAig = Abc_NtkFromDarSeq( pNtk, pMan ); + else + pNtkAig = Abc_NtkFromDar( pNtk, pMan ); + if ( pNtkAig == NULL ) + return NULL; + Dar_ManStop( pMan ); + // make sure everything is okay + if ( !Abc_NtkCheck( pNtkAig ) ) + { + printf( "Abc_NtkDar: The network check has failed.\n" ); + Abc_NtkDelete( pNtkAig ); + return NULL; + } + return pNtkAig; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abcFraig.c b/src/base/abci/abcFraig.c index 30e49af27..fa6771b35 100644 --- a/src/base/abci/abcFraig.c +++ b/src/base/abci/abcFraig.c @@ -687,7 +687,7 @@ int Abc_NtkFraigStore( Abc_Ntk_t * pNtk ) // set the number of networks stored Abc_FrameSetNtkStoreSize( Abc_FrameReadNtkStoreSize() + 1 ); } -// printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld ); + printf( "The number of AIG nodes added to storage = %5d.\n", Abc_NtkNodeNum(pStore) - nAndsOld ); return 1; } @@ -734,7 +734,7 @@ Abc_Ntk_t * Abc_NtkFraigRestore() Fraig_ParamsSetDefault( &Params ); Params.nPatsRand = nWordsMin * 32; // the number of words of random simulation info Params.nPatsDyna = nWordsMin * 32; // the number of words of dynamic simulation info - Params.nBTLimit = 99; // the max number of backtracks to perform + Params.nBTLimit = 999999; // the max number of backtracks to perform Params.fFuncRed = 1; // performs only one level hashing Params.fFeedBack = 1; // enables solver feedback Params.fDist1Pats = 1; // enables distance-1 patterns diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c index 748868de8..787e3f886 100644 --- a/src/base/abci/abcPart.c +++ b/src/base/abci/abcPart.c @@ -698,12 +698,67 @@ Abc_Ntk_t * Abc_NtkFraigPartitioned( Abc_Ntk_t * pNtk, void * pParams ) // derive the final network pNtkFraig = Abc_NtkPartStitchChoices( pNtk, vFraigs ); Vec_PtrForEachEntry( vFraigs, pNtkAig, i ) + { +// Abc_NtkPrintStats( stdout, pNtkAig, 0 ); Abc_NtkDelete( pNtkAig ); + } Vec_PtrFree( vFraigs ); return pNtkFraig; } +/**Function************************************************************* + + Synopsis [Stitches together several networks with choice nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_NtkFraigPartitionedTime( Abc_Ntk_t * pNtk, void * pParams ) +{ + extern int Cmd_CommandExecute( void * pAbc, char * sCommand ); + extern void * Abc_FrameGetGlobalFrame(); + + Vec_Vec_t * vParts; + Vec_Ptr_t * vFraigs, * vOne; + Abc_Ntk_t * pNtkAig, * pNtkFraig; + int i; + int clk = clock(); + + // perform partitioning + assert( Abc_NtkIsStrash(pNtk) ); +// vParts = Abc_NtkPartitionNaive( pNtk, 20 ); + vParts = Abc_NtkPartitionSmart( pNtk, 0, 0 ); + + Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "unset progressbar" ); + + // fraig each partition + vFraigs = Vec_PtrAlloc( Vec_VecSize(vParts) ); + Vec_VecForEachLevel( vParts, vOne, i ) + { + pNtkAig = Abc_NtkCreateConeArray( pNtk, vOne, 0 ); + pNtkFraig = Abc_NtkFraig( pNtkAig, pParams, 0, 0 ); + Vec_PtrPush( vFraigs, pNtkFraig ); + Abc_NtkDelete( pNtkAig ); + + printf( "Finished part %d (out of %d)\r", i+1, Vec_VecSize(vParts) ); + } + Vec_VecFree( vParts ); + + Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "set progressbar" ); + + // derive the final network + Vec_PtrForEachEntry( vFraigs, pNtkAig, i ) + Abc_NtkDelete( pNtkAig ); + Vec_PtrFree( vFraigs ); + + PRT( "Partitioned fraiging time", clock() - clk ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c index a54a00fe2..fe519476d 100644 --- a/src/base/io/ioReadAiger.c +++ b/src/base/io/ioReadAiger.c @@ -96,7 +96,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) // prepare the array of nodes vNodes = Vec_PtrAlloc( 1 + nInputs + nLatches + nAnds ); - Vec_PtrPush( vNodes, Abc_AigConst1(pNtkNew) ); + Vec_PtrPush( vNodes, Abc_ObjNot( Abc_AigConst1(pNtkNew) ) ); // create the PIs for ( i = 0; i < nInputs; i++ ) @@ -122,6 +122,8 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) Vec_PtrPush( vNodes, pNode1 ); // assign names to latch and its input Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL ); + + printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id ); } // remember the beginning of latch/PO literals @@ -156,14 +158,17 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) Abc_NtkForEachLatchInput( pNtkNew, pObj, i ) { uLit0 = atoi( pCur ); while ( *pCur++ != '\n' ); - pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ^ (uLit0 < 2) ); + pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); Abc_ObjAddFanin( pObj, pNode0 ); + + printf( "Adding input %d to latch input %d.\n", pNode0->Id, pObj->Id ); + } // read the PO driver literals Abc_NtkForEachPo( pNtkNew, pObj, i ) { uLit0 = atoi( pCur ); while ( *pCur++ != '\n' ); - pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) ^ (uLit0 < 2) ); + pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) ); Abc_ObjAddFanin( pObj, pNode0 ); } @@ -204,7 +209,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck ) Abc_ObjAssignName( Abc_ObjFanin0(Abc_ObjFanin0(pObj)), Abc_ObjName(pObj), "L" ); // mark the node as named pObj->pCopy = (Abc_Obj_t *)Abc_ObjName(pObj); - } + } // skipping the comments free( pContents ); Vec_PtrFree( vNodes ); diff --git a/src/base/io/ioReadBench.c b/src/base/io/ioReadBench.c index 2730ba69b..ba622e40d 100644 --- a/src/base/io/ioReadBench.c +++ b/src/base/io/ioReadBench.c @@ -118,7 +118,13 @@ Abc_Ntk_t * Io_ReadBenchNetwork( Extra_FileReader_t * p ) if ( strncmp(pType, "DFF", 3) == 0 ) // works for both DFF and DFFRSE { pNode = Io_ReadCreateLatch( pNtk, vTokens->pArray[2], vTokens->pArray[0] ); - Abc_LatchSetInit0( pNode ); +// Abc_LatchSetInit0( pNode ); + if ( pType[3] == '0' ) + Abc_LatchSetInit0( pNode ); + else if ( pType[3] == '1' ) + Abc_LatchSetInit1( pNode ); + else + Abc_LatchSetInitDc( pNode ); } else if ( strcmp(pType, "LUT") == 0 ) { diff --git a/src/base/io/ioWriteVerilog.c b/src/base/io/ioWriteVerilog.c index a02d53fd5..a4eeb78f5 100644 --- a/src/base/io/ioWriteVerilog.c +++ b/src/base/io/ioWriteVerilog.c @@ -113,7 +113,12 @@ void Io_WriteVerilogInt( FILE * pFile, Abc_Ntk_t * pNtk ) { // write inputs and outputs // fprintf( pFile, "module %s ( gclk,\n ", Abc_NtkName(pNtk) ); - fprintf( pFile, "module %s ( \n ", Abc_NtkName(pNtk) ); + fprintf( pFile, "module %s ( ", Abc_NtkName(pNtk) ); + // add the clock signal if it does not exist + if ( Abc_NtkLatchNum(pNtk) > 0 && Nm_ManFindIdByName(pNtk->pManName, "clock", ABC_OBJ_PI) == -1 ) + fprintf( pFile, "clock, " ); + // write other primary inputs + fprintf( pFile, "\n " ); if ( Abc_NtkPiNum(pNtk) > 0 ) { Io_WriteVerilogPis( pFile, pNtk, 3 ); @@ -435,7 +440,8 @@ void Io_WriteVerilogLatches( FILE * pFile, Abc_Ntk_t * pNtk ) return; // write the latches // fprintf( pFile, " always @(posedge %s) begin\n", Io_WriteVerilogGetName(Abc_ObjFanout0(Abc_NtkPi(pNtk,0))) ); - fprintf( pFile, " always begin\n" ); +// fprintf( pFile, " always begin\n" ); + fprintf( pFile, " always @ (posedge clock) begin\n" ); Abc_NtkForEachLatch( pNtk, pLatch, i ) { fprintf( pFile, " %s", Io_WriteVerilogGetName(Abc_ObjName(Abc_ObjFanout0(Abc_ObjFanout0(pLatch)))) ); diff --git a/src/base/io/ioWriteVerilog.zip b/src/base/io/ioWriteVerilog.zip new file mode 100644 index 0000000000000000000000000000000000000000..19e68a892b5a03b77442b3eb2e39b76ee6906c00 GIT binary patch literal 3662 zcmV-U4zcl2O9KQH00ICA0H9#7HVVQ`7|aa-0LWAT01yBG0BLVma%psBR%LQ&Y;R{S zW9?jfQ{y-i|9huuzJoTmEHQ*kn7z5GBg@v5MWmQOzKkzE!Hnagf8 zjW;x8M1M|zev@oATTSvYq(R6WvO#{Cc#OPkHQ>M2t7zm8?2-$lh`oO3I9ntu*Ty9h zYRO(NTK{?!;lF#{K4?mV7Xx+{-@F zjh;Vyv7nEnL<&A{_V*5VKJ0wz9CbgE(oaNbK|DQwCPL5wn_T+bAszobxmq1BtdoPz z;XYX-W3-kA*}1UKyW#LW#7FRjSnX00$6U-J(IDIlm151L<}Z@kuN*9Ef%HDG{vyd8 z(hy8m+;;_zF8;&pa4s^)qET3T{sdK`tgk(w0X)w1e#=5cz`I^9mWl`Y)BUaYMhOgtNbb^%T+5E<82DiG?c`G!P9;uV>^~fEu!~1&RI!EG!6Apr*>mMDr4VZi7}y_bR`+c4IcdG)FE8>DtMr7ne`n{Jct z=fgw8^m@_!MCiasjiPyaKEy3BT9Tz6l0L1ih|?NQtC3WLk{QNxRBMX_*?%W8t`Smv z_ymM@;qvFcr3YsmECwfRs!0;4g-4r ziH{gS`emr8TRo*gNTpLnnw=Xi0ykJ_a+Df-{o{NyBNuir83jwCi~o`ER4B=<(8`IGDsaR zR+;a5w(AQP*&aT+U4~l`kJPVJ3R+{g66-(r0E1LEr|?K%6kyaJWwn3@pp<>v9X3ue z->Jpp$Vf*!fOY}oBx#iP1Rkj4NOK20u!jVV4!jhY1P_Vh!#W|DvTGhefHW3OP{xqm z$w(7@O=)H~pw({Xlh;z7Zt;ju=3IT&)byLW!H`^))p$3nx~*i4#TZd$Sz z{F`Jyi7(I|K=wvUyFfNdoN33S=X1={lQAHqDFI2CU4#6TGUVLojm+@31}=Ov7pCF; z;^A{c1EF>joHEMUh%~bSPOuN_%>wv}8heGo`CQVPM#=^*^9H|6k;6VvCh2 zMxmO;Ie9uBNV?Jtz1ZOIvi1fJ;^IO=>8_3VLD()C0(F)n$iF($Z%toppgJ z;wr9aFH|WEfG%c@@UPC|rd<R)SGaJfgyPD#`tOB+n|~K@>t-87ZDXa{UT|Q*ZbeHsBa?N7< zjfJXLR=Pc1>!gF$Yokpa-2JkDRt7>a5vsg4`@s zbeEhpNJ>(Ykr_q!+vPb^S?zdaE_D9AX0sE8FDW0oizNl^To>v~8wA+V&p|7?n9n9R zFl>CKb|EIC3oug9s6-h`bpXpP*+!0YPQw;Xf>a&_?&qwLv)ElrdGeyl3dfQsq|#)j z*C@zb;Jei}yL8n?0S+KhRGW<*{+?gYQp8)o@bP>v|}iBMwV) zw`#d!k+Iy0vQ4`ev=8P7ZhRNaVX8&bJ3WejTBMpf0Yii|76eopHlaJi4#o9n+1 z6-pJD@{^f8nc1Jm%=ACeDXMt7+fmN7#1lfeWC80xwq$(ngWBd?Tm}RWvgbB;=IyHO z+)VCm+#FtdzMak#w9u;W{$-I{5_rlNp7MnU%ommjpW1RC8G=^6n^JfMv#Bk$G%`rACF;LY_!nyQT=9( z8jVwS3@~Dl#2m_ll~%s<9ii4RCLvV~u^K>I){LWrKX1c`?Ftgl3~Hz#<%hg2lr6wy z=8Pq1i#=3F_E^9O4e)p#5AllSC3Po}Uz|tODP@)~J3ujF6qOmz)#6>G^WXMA9Faf% zsL=ALyPplqF9Jq~N#l_fYqJGaG9J^!ji)|Uv#Lf@(SWS`>h(M_w`QIqM3X=@-8@~r zXtnP#&DrLGHwdb7Z_tAo%x^v%^OX#3iT+gG?ZQI|7yk95^Q)CFYsP*RZ|LBE`0DbI zU4kODO*iJk;jVw(F4<9xkLO5G)h*xo<7rD=y^<}$H@wgBYH!^p7u<#gdF8({fK*PshFHbC*?1a5?Ht85WQ`fQPEvS=Q_$)pZEK@ao0= z0s*;TjbRR3ZwqDPe+$`6OZinrvxvYfAsm>b;m8Z_Yiw*{F11x_kirx0IR>qQD-gMJ z@X6r*9hLWGxz{he+Az&D-*f-`kY5BexcR`S^OlD4R_J?row&Ay;FM%}HpF1^m`4*c zqEtCWP^LLJ1>{=+DSj(Ni>UcA_ol6nV?;Jz1O;Yh1_Ub`Yl8GO<|yelV#ZLgD$B;d zteGHG1&CxDKftS-dJcLqqXFTGhzI0S+|%i1JHa=}B)bml(JSnRjAd%o6$;YLGMh>c z7s~{Pvy2t&d%+pWBN&Ha@*~}vZqX(q{)mXwY2~`wmGG-X3eid(O~QnBRD`X$1u#7` zL#m8n72U)syOpbBBv2|HIqkTRTGz8z(kdSrGVNj^7M0q!DdiXP#`g+xb|Wd_*&sHF=V7bQ?kbQLOH z!}ynT0KWgkU^Cb6WW_*}{E@BQ39uWSylS=1lAF&uu#dJ>vKyI_VzT({djh7eJedti z5+XH?eq~}nFHx>i(6v?#e}kyDSxa74uSWxHlTFkwK=_(E%Kl&LS{l049@Of<~>8?BZuD@06+RAtRr|KF% z!%3g78m%r>zfU8!7Hg)HHaAH-mvP%bESwsE2ya|vBdUeg7hDFidV0DVZ9i2Myzb7| zH_zmKD>b`zini*iTC9>)vNames = Vec_PtrAlloc( 100 ); p->vStackFn = Vec_PtrAlloc( 100 ); p->vStackOp = Vec_IntAlloc( 100 ); + p->vPerm = Vec_IntAlloc( 100 ); // create the design library and assign the technology library p->pDesign = Abc_LibCreate( pFileName ); p->pDesign->pLibrary = pGateLib; @@ -136,6 +137,7 @@ void Ver_ParseStop( Ver_Man_t * p ) Vec_PtrFree( p->vNames ); Vec_PtrFree( p->vStackFn ); Vec_IntFree( p->vStackOp ); + Vec_IntFree( p->vPerm ); free( p ); } @@ -1193,6 +1195,12 @@ int Ver_ParseAssign( Ver_Man_t * pMan, Abc_Ntk_t * pNtk ) pFunc = (Hop_Obj_t *)Mio_LibraryReadConst1(Abc_FrameReadLibGen()); else { + // "assign foo = \bar ;" + if ( *pEquation == '\\' ) + { + pEquation++; + pEquation[strlen(pEquation) - 1] = 0; + } if ( Ver_ParseFindNet(pNtk, pEquation) == NULL ) { sprintf( pMan->sError, "Cannot read Verilog with non-trivial assignments in the mapped netlist." ); @@ -1356,6 +1364,29 @@ int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t Ga return 1; } +/**Function************************************************************* + + Synopsis [Returns the index of the given pin the gate.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Ver_FindGateInput( Mio_Gate_t * pGate, char * pName ) +{ + Mio_Pin_t * pGatePin; + int i; + for ( i = 0, pGatePin = Mio_GateReadPins(pGate); pGatePin != NULL; pGatePin = Mio_PinReadNext(pGatePin), i++ ) + if ( strcmp(pName, Mio_PinReadName(pGatePin)) == 0 ) + return i; + if ( strcmp(pName, Mio_GateReadOutName(pGate)) == 0 ) + return i; + return -1; +} + /**Function************************************************************* Synopsis [Parses one directive.] @@ -1369,10 +1400,10 @@ int Ver_ParseGateStandard( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Ver_GateType_t Ga ***********************************************************************/ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate ) { - Mio_Pin_t * pGatePin; Ver_Stream_t * p = pMan->pReader; Abc_Obj_t * pNetActual, * pNode; char * pWord, Symbol; + int Input, i, nFanins = Mio_GateReadInputs(pGate); // convert from the blackbox into the network with local functions representated by gates if ( 1 != pMan->fMapped ) @@ -1404,7 +1435,7 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate ) pNode->pData = pGate; // parse pairs of formal/actural inputs - pGatePin = Mio_GateReadPins(pGate); + Vec_IntClear( pMan->vPerm ); while ( 1 ) { // process one pair of formal/actual parameters @@ -1420,24 +1451,13 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate ) if ( pWord == NULL ) return 0; - // make sure that the formal name is the same as the gate's - if ( Mio_GateReadInputs(pGate) == Abc_ObjFaninNum(pNode) ) + // find the corresponding pin of the gate + Input = Ver_FindGateInput( pGate, pWord ); + if ( Input == -1 ) { - if ( strcmp(pWord, Mio_GateReadOutName(pGate)) ) - { - sprintf( pMan->sError, "Formal output name listed %s is different from the name of the gate output %s.", pWord, Mio_GateReadOutName(pGate) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } - } - else - { - if ( strcmp(pWord, Mio_PinReadName(pGatePin)) ) - { - sprintf( pMan->sError, "Formal input name listed %s is different from the name of the corresponding pin %s.", pWord, Mio_PinReadName(pGatePin) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; - } + sprintf( pMan->sError, "Formal input name %s cannot be found in the gate %s.", pWord, Mio_GateReadOutName(pGate) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; } // open the paranthesis @@ -1482,10 +1502,13 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate ) } // add the fanin - if ( Mio_GateReadInputs(pGate) == Abc_ObjFaninNum(pNode) ) - Abc_ObjAddFanin( pNetActual, pNode ); // fanout - else + if ( Input < nFanins ) + { + Vec_IntPush( pMan->vPerm, Input ); Abc_ObjAddFanin( pNode, pNetActual ); // fanin + } + else + Abc_ObjAddFanin( pNetActual, pNode ); // fanout // check if it is the end of gate Ver_ParseSkipComments( pMan ); @@ -1501,13 +1524,10 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate ) return 0; } Ver_ParseSkipComments( pMan ); - - // get the next pin - pGatePin = Mio_PinReadNext(pGatePin); } // check that the gate as the same number of input - if ( !(Abc_ObjFaninNum(pNode) == Mio_GateReadInputs(pGate) && Abc_ObjFanoutNum(pNode) == 1) ) + if ( !(Abc_ObjFaninNum(pNode) == nFanins && Abc_ObjFanoutNum(pNode) == 1) ) { sprintf( pMan->sError, "Parsing of gate %s has failed.", Mio_GateReadName(pGate) ); Ver_ParsePrintErrorMessage( pMan ); @@ -1522,6 +1542,20 @@ int Ver_ParseGate( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Mio_Gate_t * pGate ) Ver_ParsePrintErrorMessage( pMan ); return 0; } + + // check if we need to permute the inputs + Vec_IntForEachEntry( pMan->vPerm, Input, i ) + if ( Input != i ) + break; + if ( i < Vec_IntSize(pMan->vPerm) ) + { + // add the fanin numnbers to the end of the permuation array + for ( i = 0; i < nFanins; i++ ) + Vec_IntPush( pMan->vPerm, Abc_ObjFaninId(pNode, i) ); + // write the fanin numbers into their corresponding places (according to the gate) + for ( i = 0; i < nFanins; i++ ) + Vec_IntWriteEntry( &pNode->vFanins, Vec_IntEntry(pMan->vPerm, i), Vec_IntEntry(pMan->vPerm, i+nFanins) ); + } return 1; } @@ -1546,6 +1580,7 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) Abc_Obj_t * pNode; char * pWord, Symbol; int fCompl, fFormalIsGiven; + int i, k, Bit, Limit, nMsb, nLsb, fQuit, flag; // gate the name of the box pWord = Ver_ParseGetName( pMan ); @@ -1613,8 +1648,6 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) // consider the case of vector-inputs if ( Symbol == '{' ) { - int i, k, Bit, Limit, nMsb, nLsb, fQuit; - // skip this char Ver_StreamPopChar(p); @@ -1673,7 +1706,8 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) pNetActual = Ver_ParseFindNet( pNtk, pWord ); if ( pNetActual == NULL ) { - if ( !strncmp(pWord, "Open_", 5) ) + if ( !strncmp(pWord, "Open_", 5) || + !strncmp(pWord, "dct_unconnected", 15) ) pNetActual = Abc_NtkCreateNet( pNtk ); else { @@ -1697,7 +1731,8 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) pNetActual = Ver_ParseFindNet( pNtk, Buffer ); if ( pNetActual == NULL ) { - if ( !strncmp(pWord, "Open_", 5) ) + if ( !strncmp(pWord, "Open_", 5) || + !strncmp(pWord, "dct_unconnected", 15) ) pNetActual = Abc_NtkCreateNet( pNtk ); else { @@ -1738,34 +1773,72 @@ int Ver_ParseBox( Ver_Man_t * pMan, Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkBox ) if ( pWord[0] == 0 ) { pNetActual = Abc_NtkCreateNet( pNtk ); + Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) ); } else { -/* - // check if the name is complemented - fCompl = (pWord[0] == '~'); - if ( fCompl ) - { - pWord++; - if ( pNtk->pData == NULL ) - pNtk->pData = Extra_MmFlexStart(); - } -*/ // get the actual net + flag=0; pNetActual = Ver_ParseFindNet( pNtk, pWord ); - if ( pNetActual == NULL ) + if ( pNetActual == NULL ) { - if ( !strncmp(pWord, "Open_", 5) ) - pNetActual = Abc_NtkCreateNet( pNtk ); - else + Ver_ParseLookupSuffix( pMan, pWord, &nMsb, &nLsb ); + if ( nMsb == -1 && nLsb == -1 ) { - sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) ); - Ver_ParsePrintErrorMessage( pMan ); - return 0; + Ver_ParseSignalSuffix( pMan, pWord, &nMsb, &nLsb ); + if ( nMsb == -1 && nLsb == -1 ) + { + if ( !strncmp(pWord, "Open_", 5) || + !strncmp(pWord, "dct_unconnected", 15) ) + { + pNetActual = Abc_NtkCreateNet( pNtk ); + Vec_PtrPush( pBundle->vNetsActual, pNetActual ); + } + else + { + sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + } + else + { + flag=1; + } + } + else + { + flag=1; } + if (flag) + { + Limit = (nMsb > nLsb) ? nMsb - nLsb + 1: nLsb - nMsb + 1; + for ( Bit = nMsb, k = Limit - 1; k >= 0; Bit = (nMsb > nLsb ? Bit - 1: Bit + 1), k--) + { + // get the actual net + sprintf( Buffer, "%s[%d]", pWord, Bit ); + pNetActual = Ver_ParseFindNet( pNtk, Buffer ); + if ( pNetActual == NULL ) + { + if ( !strncmp(pWord, "Open_", 5) || + !strncmp(pWord, "dct_unconnected", 15)) + pNetActual = Abc_NtkCreateNet( pNtk ); + else + { + sprintf( pMan->sError, "Actual net \"%s\" is missing in box \"%s\".", pWord, Abc_ObjName(pNode) ); + Ver_ParsePrintErrorMessage( pMan ); + return 0; + } + } + Vec_PtrPush( pBundle->vNetsActual, pNetActual ); + } + } + } + else + { + Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) ); } } - Vec_PtrPush( pBundle->vNetsActual, Abc_ObjNotCond( pNetActual, fCompl ) ); } if ( fFormalIsGiven ) @@ -2000,8 +2073,8 @@ int Ver_ParseConnectBox( Ver_Man_t * pMan, Abc_Obj_t * pBox ) } if ( pBundle == NULL ) { - printf( "Warning: The formal output %s is not driven when instantiating network %s in box %s.", - pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) ); +// printf( "Warning: The formal output %s is not driven when instantiating network %s in box %s.", +// pNameFormal, pNtkBox->pName, Abc_ObjName(pBox) ); continue; } } diff --git a/src/base/ver/verCore.zip b/src/base/ver/verCore.zip index 45574008d7ff10e1920265551f2622903f2d8d5d..cdfcf5a45dce59a01e5cb27e99dce5faeacbfe7e 100644 GIT binary patch literal 14624 zcmV+*Ip4-mO9KQH00ICA0N81;HmQWc!>l*}0Jeq!00{s90Cr_^LvM0rE@SO|Yf~Fp zvf$_25&a*^>~$mA0s}F3cE&V43mAKd!NA&hrXy^JqmW8ajZ~#uRpPO3=C^NVp7*0( zLdek9o{4Bwb?Q9wsqSstXrATP3MznJ1v-jC>D zds>{QSwR0jZjZtwcpK;E{qrcfNIzo(YBU_iqnJ(cc~C(16OQFO!mcoh~=!2jVq zSA+G{wbkH#5oSd+2v%T_vuR!g>woP98*6KS7GuAQF5?{g#P9xdfABJpAnaXYA8XY7 z#oAw9tp7DwTYE|W4?>vbI1cu%C&7PGPtWG_?*;btzv84nnhv613FfkTzN9}H$Ep1! zj1zkF;}0+9^pAQ9O8&jt+dbHRw|%mIbof4~{3m*v)10ucptzYtgiecjZ&GyOOm+iw>*3{|o(L4LeukNFr z53lVq8SDi8^Du+Q6G5+f z!S-qY%RzifttZ$a{0O?6vbW1L9_Zbqla4XMq`dL#EQ)|6gpEJgPl_mm4XgMdPKrQ% z@HQPxM^WSE3>~cI3s?;0OLy-u3qAD!j>SyDslwKZ%RD!Q?8YkmE7D zLkGC~fG5cy%m!9B@JAV(6cPsF&*~u>!2fNWQojl-%e&l3ubWNQegYqs_qv-VNz^YY zIzKx7jXkOCXS*oE{y8*>asVaJawprvkh@Fij#=85gWpQ z`}wPA2+sx`KMn=JF2WpyF(9z~;mR)pn8bv$2xP8Ae0>}rPRAYIvK##VyL^%AFW}SL zvRT3E_j8V;VqOv=@CQyxn-zb(pCdlw`!3E*n-x5I9VT%? za3*J?^vm#VI043q%yBb7_IeINDE$9496Z5xf~_*ilP142O$H-4+h2&UX%7e|+-5)i z@RjjEj;Hb;!T5EWjl|#x+aM7e zJzN4*K^BHSLVAVY=RxP~`<mJlF%Lw(*ZYV2)e_(Qg}rCb zUQd%g3jA}>k_;tTP@wS+RQvi`2Z;wW4zoXjA4&!0a(LdYT3JyOU9N==qhHwgkkJT_o z(_%6$0vaYS20%O1yGtA)5BL=5Eb{T!L7~%@atR>rU%XBlHawb$h9E6o#*^@RwL$l}9L`ZH#q%=`ZYeAFeG?V?%UaHk>X-m_Yhb|xT)ALnr z?%&f1uAGjJLEPXW;+~kQL;U#rU`uB_w-P`E7AF0{`W2Kd6T?KO`FVKBK7pe<9dTh% z5b-T-c!wC9v!ML}QfP0FMRe5If=0{U@0(ITj?>r3E@U1gTQ%D>bcV@EdJ#$Fgu@tb zvQ;pY$s&a{<8%;>&>~114TI=ZealDt>9jFXr>D{TH&KDmeh(sBhxfw>zY^N6&T%_B zDDFAu1Lk!Wv6G%e*YF3fKsyq&BK_FIczD`7N~slX88hP_xMCdsJB1lv*q?wl)*nyA zr@dflOa`|lP%pL5znVSelMDbn>~PrSds&ud@a=AxBxwN{9}a>~yr)k~!6426t>VjQ zb;+2sacqvUOX}z?06jeOEm9pP?cuEfPh*p(f;hiuNRp&_40on;3{(fn6V{&x{BJ6zZ0S>LaZ;Wsfx5 zgP!-2BD;|b6D0YP!7J}^15NBl=V5%!#Og3P8^y^P>D8(QKf$kKIO=d_@T_!{$x`cw zX2%akag}BlsOQ5Bx^FB_}$w71(jbO{xH=E)8 zi8fC*^Ybtdh9R8%0Zm-Ie44K=F$gO2(LJ4q+wY9V$7o7D7Oq;rxxb6&TzFH$K5N`C}vMXqCghNWI8^5L_6v^C}mrVGA*^# z&bHWYb?&>uNT@*r?VZTl&VY+)9C|1Tf-s5zHF%o8goFMm!IQ38Z0Hvw84^dL5il#_ z1t_q%dvz5T=k`=;M-MvG`stu6=V1{#V^)SVa{yl+(l8yR#ddvDM`8~LfK&S-w4`8l z&ZN$H&$K8RcYGjem!DCibGkEbrAoCI} zjmr*#YqHa1a7<;#!(HWV`8hXc2tT+PaC>L>%i+mCz8vnI9PGb8>Cpo;zkk^|*xvoe z&e5+uAq8lP{HD>VVBA7Y_)x?nI6k0WcB~1i58h9rzN1Bkg8`RO(dD3Qk%oa_d%z&; zfhk*}tz}Apem`(C9yrHQi7P#fih8%IamaLEoxy6*cekZU!qhkGj{5PQ6RVRaQf*^2 zd};mD^645XZNLBSe|f#+J%HLYG@8=k%ah&Kj=er}_v=eG4)bGj-w3>$CYMoGm^eJl z(lJw%1k$2+6U_-JVDlgbT+AY1)oBtvU^Es!WD)0p>#SfEE?$!@Q=cF2>FzO%T8PH5RrzYLJI(M^jBbK_+CP_lg;_*Ga|qn`DjKW? zMjUj`0Tt0PKg-;8UWrze5f1|;dF{eFISkw{c-oCPX}vW zjaux(cigYReVBV&+~;p*M}8RdJM!N%^797k3*gT@#2q-T2xRBt@?&AV-q2Okqv1wD zIxb~y#E|EOspOk}ZLY`vdlHQ&mUrY|X*TEqgvY1pNOO|Bi;91SqiLiYjFnGMFw8d6k$Xp`Nl(QTQK!iF|R7>5@T96C5?R}neoP%a7CsOcn1P=}m^ zS;%uRG$BTT_c)#G0)#q~F4B_a&ay|asd0A8%En{34zReKLZ1r9%Y*;ZPW)`syS=d>dNkOY#s3hFV78kpixmsdR^l)&TR~vRs^C zKib>wvZa0~M=LCKHyslhF874UIX0OejldfsI&8Kh z(q@3J&oW+5NleLywQr1#ma59A-x2}EQdRMvpn^t-1y3d5j^E!B$a^T49d1( z4x_S^nWn?Sj?ZDtcYAM|4v2^~hY>Nmr|FP{#dF!uBOhQJ_|MfyTftflUiuGe7GY`` z(hDV3F8*BBog5H;8^YPlF|na7Q>~gFo@{=@9=&Ti>h(N_{k8eHAn4C;+?@}vn~s~z zb$bt6>~AtpNFTP?;kgd{Ym1RVWSr-UPpsoxF*4IA8xAgV&D5|>7Z_5aT+?BAR$cpH zVwO(Va2%O@*M1-nqrE{qdIgl(MaXpsnnG66^OWXSVCTW8KvpPbkZqlwDL=#0)`kIJE)01d)EC)D5!iH zXk1az^=6JtlVxC6?pC6MEzhUpNTw_C@TXv!gNPop`2I2wesyhEG)!AnwQenxd}!>5 zZ$Yhn4kD5K z*A0Gwol|LnfCuKQayzEAUAA|}KqltO77iO5nAHY9)70&mi0$O;@l09z?@5%6E&OL8 zxppWDrdLXDC_7C%eB&56Hr-LtqsU?vF>98um1YpzYy9dindat<8GA?5*10_xQ2u0x zbLBtzE`{T0Wn6#Z*rQFNL6JuH1x#P;N$pZ^7*kCwAsoSn5#mL z7{A9);Yac|KUF^tay?mcnjlDkHVG3nK72->0LDIJ&9{OTGggnN8u5?~HkXRL#dRxk zL5MA$Ubuu3JnQNLOMns!Y?-uA*`QxJJ zeuBp1ybXRTFc9*)wA&W{znz z>g@5O_5jXB{}G>y846@b)Q25Bi;^e{u|UEzkm?i5llYJ5hGe`MkA{)30D}QQBam&r z#6>jrBh48mCMjynCZPT1IHLtdv&ejCCou^Jf~Vr_d8TS+?pQ~6K{08sq5{MujNax* z2ReyHp&9P&L}xGelEI^)%gpe8Oe-lT%kZnY;Gk1-k`(AK&8^Ko*65N9Y{7;f*FKYP z@#C@{O)MPNr_ouQph2F!;fx)QLoBq@=UVXwN_t8Lj8aTSaZ!j6ePO%_0!RKXzf8g`y&-K&wOlrn!Gy157U-C2q1q&8SMi9U}Oc$81KhiU4Yk^!ALf~#z z#8ruH)B1V2Yz)pjD%&1=i#)zr)v$8M%=x>URJBp&Pd0NhrI z98#{(&J7!0NXOzZ>ql9N)f%2iIa)j23zQQa5^W06k56o7!Q*V1X>%_5o&&(E94Qf}SFRviApaul^Gy0n;Z1y6Mwo@bv?N)}*XK8gDA zFpdVkAvBW}mbc-qeVo}rm=_gx216a+LKsPXoc$`bBA9kNh8RC_HSj04F+VZYZ_|@# zChGU}Lm&uO=MkNaj4u@Pn@*$RDuTyCfDLuFZf;7QX{E&Vt?jfX8hc#i&G)?d-dEUI zT+g?O9V~fX-nd|lS-y?c5hLQbLSr+C9h6(|I|_()m*gp1&La}MK~H64^HBCX4xY|7 zI7OKIho*3Me~d$U9=khw(-@kDwlWPluxbPkXCjXw`7=rmu;mcdg422$VJ#a)@HfWD zpdB)@{M2kqS_O=7k)Re7#vm__@; zRe!)rrcp*in`C;~*i&rvkFaO$CTlDyUH#D(#h{YwhF=g;5iM)xt z{ErR&rIFlgUUk^LB;8vLrGqo7)#DkSV~aB znt^=tFo{zXJLI)!yM9l?J$RgTH_v}h!%XtUcITo(C|kY9JDr zl2!k_g}i!eaUitClb;>&q@JuUDp`aS^9W?Dfu)!;*4CDEZ?s4ccZwY%83VM36;DRA zmwq$MhTv`guEHN;=XFPY8$r1@d*rJiH*?cB`szx^o4W~35B7pzOV-@6+!rLREF>3^LO$2af#0cVtkjMzst`L zQ+^ht-q>iM83;jUYuQ}#oE7z18$nvdR^#;?`2^;JVGNcWB~zh|i%8*gcIOc(Ed@8^ z8rlVZ;=EGO*8PV}6MyE(wkieIN{GcZ`$Rl>g)5UWsjsdr>g9aj4MJ2>yhrXQ0Bdc@ zs12>ZVnv=EyrT-_IFt8LfdbB2hcBYmNGlHPsxDMq!VD2&G2Fdi_%0eu`&zF~ewZK?R%uY{Iuznl8~^*i z{;X)rSDnaUx7S=TVNVxXp5)FIL7Z5nrZH6Y8q9sydX&aI6d&2m-Ycy9WvSq0mNGCR zBh1jIX2bJnSc>3+ZKIecJwTjEBq-+j!g)M_A62@eyvb5%Nls7`^2EuFif`~s&h^?t zeZAbRsacUA|Cc~&R|Gx5=8(OMSd#1?;3eO;Qek@e<4Q3erKLN1vcI|>~m9$yb| zUK8>7-Mj3q8#2zfmmg3b+VE-VY5r*mrS{WEn=x)}Mexa-_tv|+0LAz+9st6z#0^g4 zs$lBLoG>ba&9bY-d1zu9-7QF}A5vbtEq?wXS+pG1(Gz()yLQVdi{QQsew^ql!bJp~ zr-LqHuexMK@=As)993lFRp(+eE9Tsta8Hs%wz$R94Pk05&a-rSc5Wpye6x@^)Aq)y zmY2kQao`%)go=oMn%c_xO6)vY9>6*V&b>l@u$nL3#>-Q6}OBp=T z#F`C27Tm&TfO@*)sC`ep+s_wKb=@wSS}0 zdAtvCeCBhw7?J$DGSe1v6%LCTofg%SZKd;~!TFxe$5AdqH0Z16>8zR4&ejQmyGd6au%G{*RF+a}h z3?_}w;Po3|7~L{KwPs4|^O(|lyD2r6)L@5sv3S6|6lU`2G|Ym{C4Xz4nWvuv#uEL_ zOU5+Lp_frRtt8VH54x!Cl(Fs-fz4nG2IJ*?S9M;K=~uC^CI?zyRu8tJzJpbe6~-MuT9+)F!CNLTi;UXP?iVQYHiP=9ND z-V`M>FHoEt>fi*>&F+;m64W+8*g#X!FpNj&GKl)&l*e|RvAYO((S2%_q#QoYnanrB zuiHv##-($0+@htIyyErsQY}eG^a7A@hGO1{*^HCi&A(nXpY>Mrsg}<4F%Umqr`dQq z3gtHjLo|o&*=JnCdqAZiXk{33=Rl~MwVuG``y%XLyiUyDN0UYqY(@#belyF3SH@GO zE+QxV{zjl4@nw_*wu7zG^wn`MT#@bZ_K>g$(U)x9|JvG~!X(oK12OQHRbj|1H?A^+ zYN@&S#fDKJrkVXzIYhD4fhU-gjP#-aUI(_cTV+z+covr!@o=1AE2#U}u7+uJz{~5E z$xP+ZU0$PPoe9HxN$oc`D{3hSPxDfPM%DDct$mRKESwyK$CDuaJ-(++e2;l4Skuxy z_!TeQBmSIM<}#pP^;N@*9x;#j1UPHZ8n>M zG9P+wIPT8B{92u-L2a%nE{OY`>jeTU_hb^r89Cdrl5RM95%ytPfCjp}Q4^Y^l32K< z+LK*)zu`#Q-Pac1Bs>RnVl(^3*$wzL%w-(sRCo@gCBm_?+M)Loof;2~E82#z{p20# zQ570IWO;xgBo@G|cyf5n0?H|9+E*Z|u_Wng6OEa!8;hg4^3IG%?WQigS$TDLx$dq) zVfaU*e^{RS(Yr&Yho6QSUJy?~_O5M%u&>&pO}_WY=_Wg**G%q6&dO`v$Xi%JNB6!v zJUZ#3Kh#Z&AS?#xueabEJYEWz}{iRLIhi~CY=(xBqSLcFcF z6hrAMUn{{yY3yh|VoZHI8FU;wN(o+fwHqHQ=5_S0;^4e%G^?X*-jn*ZVphL4oz~uU zI`@gy(3yMN#PS&(Rw7m%9A{t4VOn&|=iP5xF&yJ@eJ=u<5k&M4k4}~W=yF0nNsoL<6 zy-oWo_zOQejIN80c-8IM<~%)noTs7aACm(_eB7|H*`7p`PBQy6-G_LIU4tUA{3TCOveWoaKkM06hqw8q0b2ty2b zKpeIBW+^(X-q~c}qQz=sB$%Tqpv0`m;IkmJVv|}6C{8*A1OE{h5&myeh~siwiDi+0 zSW{ZOY%gCk05Q)RzmEtL!El355q{G|UYB5-9IFJTh3qpDAV!*fcLX*igfkSfU_g_{ z4PnNOAI&JF2Ylb|jBw(yaMOE>vVPuR{(rMr{uj@*%2B)cIXdf&T!w!yJM-l&%Ta(e z01;^5$!hTDC~!kRDdmh`l)K1{X8f|{x8v8N==wc!tB#c$f^xLSYazDIuD-h729%B+)K~B7WeL|FtKZta{QiwICK|59LntJ4}dt(-321U(93Urmda2$pt!_i zgoC2M)8l<~H=8?eI8t>tiMN{5x^3wZQhK0pDe+EIbXz?#AJIa+M2{4=Tl$GCKZnfg zre*3W-3b*OK?soiq${PJ5@RfErZ_l;JIV2iu6J7~YRCLSGHowZK=Fc9vd7{bYU~tR zkQ(d4?J6QG2bI+XayjLe5RWnm()(W6KQ|)^H4@tkV#kKcXfJ>;uD$(Kgj~W%ddMXX z(Dm!62IIi%wL`ppK8YNu2$?XQOHkG6TYX{sz5eW{s~4v&@%%L*VfLPVv!j6rSnUv@>b-)oN9prq}mlSG6PJ zLL5p&&tr74)QG*-!X0kSudx_1G%)vqm44%M=Rz(6v{lrCc@ZdZ*SvL9z~sKHy$Fd$ zrVKL!$ti@n06TBcz!+=UV#NtjLHXOGQQGeW>wk9kaW|dZphZDDC|&D>)fjF=>{}Hh zp#o$b%`zE0XFL$+tTg&u_noux5Cabmj&?f+E$CTk1H3Uz9XEv=__*)Y)9MmPLarGM zba4F1+Dk3HPk^8&C)c&Lk=YE^CPlH*9V~Qz-wzXk?^|`|Y^P&yt%`=G^4apmOU~A6 zlasWljPV-d`67y@l^4?U%*BuG%%b+8h)1xQ@OeiwJvrT1+mYMal4nDW64kmf9p?PQ zMWO{4sc2E~rpy|wLX7ElfP`zdUvC3|0!ZSy43#S}sc2-uxzN{F5230OrDlZrx?EH4 zkrn4aD>e+?s1~`?2dSuE~t~bjybILcZl|jrk8#>@Zz13ek(H#ma zQm*?dQnmoj>=hXsrlxbdge+qCmfiJ!@P4NR_@uaBFvb0%D(w_rV{Jc=KHs2TK#d=# zrj8uX9Dh0h+E1ye9V5Ne$S%F;ir~BI`T&hwM-|0BTlkV%z^S3Hi5H#pWXZ5Mt6IIi zhN9NoY9};6(ux`#ZfOmV>~6V9W-Zb%O9dKPB#MeO3$-1&Nbqs|GWlFpbEBNVer{ZV z&Sg!M%iW-6bP1Tss}vZ+G%ii;rMD7z39B>e+#>G)tI3V>_d|PT^eNvzU62Jg5(?wx zml_>`jQjIU^)8Gtfl%LJfm2}L#bH2}(8 z2qx+qie8o~6}5|)3(0IqHfu=dy;D^}#L_}ow{2-m&9O~cJaL^6qle9u)vm8tkEl)E z(JB^qg9hcPgNjqa1S?euxko}48)^l=y`YJ0@+KX(TJnmhmJCC6;q#T1O6jY?VQEPT z{gRk0=*tgGSv}wT5VmF{tPSbNTnOx(iR`=xZ8Kuq5Ks?==+2GswjjPWRJOtE`4QsV zHj;0Nddsx$Su|*00M4wIlcupkW#+2e<+>$Q_3*@7MP~NuKFqw-Jb(yc*q!Y-ET#-s zZS+~iU82!-5nREtzU^HkK2vBko)kA8)1Qp2t*sos)}+RFL+bq>|Iva#2n0$s0dd;vj*5TfF@G6K7&*ilq<*WX-DNODhf*DcQcTxN24Nt zSC0P}%JFyI_`7brDBZZEc5@pM^L_;OT4l^m^fRNrDg!uba>m*!@ojR}& zhnvAcx0fivwy59e-qL*UY!TZvE^{wjAnB=;`+@Ym#)sS5c9B zBhyyQG#g(k45~`n^DchEWBawt3_W!RQ#V*6_)*dZ$Cb@6-@})2b3!>-{Ex%vs;AO$ znk4q<)!G;iI!QLa^@5mv)8p3_NcV*B08@A!Old#g6*@%+=dEayXo(GBY5VyrR#(5n z7wWcr!ol(PFqf$?vhnY~3uwVlmf6bRU~a2XxPb((C}a`X$NMjikF={Gcqcs3@i^`X z!1n}XjWkBPcqcaLsw56A2g2$&ZQOC3l=dsCH0aDMPh}?4I2fc<#PuA**|jL!+@vW+ zQm2z=fffNfr_&z<@7HskEKfVaQH0e=naoI0}6Ut1*z{-Bag%MG*3w~Y2 zqY>7Tk(w-}SK+OiQ{tUE5LQ1WOFgj*d?^+?HSkai?F?ZQEptW`tYNt}dPKL(qgiwF zT593`n+;0Q-E-^aZ4Wze1JQYIxt>LCEJ4dN=Q-!9p#WRtgsY1wJ&~IKacmsF=kj@K zJZ~?Tp7`dzf0S3<5AG~Mw!b>3t7<4hHx3JabBVwsZU|t-hkQDT2Yq|(AkY@|?m=SK zZpGoKD=;|;SwS%n<@Jlv{P^6GW`6Z1)HwImr~|=A#jqRKtElC;0Sd7CQ7bYpoG*{c z8?JB~Kx@K4CX`d&+VM=D!}%_{i~!~}#t@56mU$vMS9X#+;|fEWTT?^<7yD}Vjg$xY zg#FGwC$7xWnd6m}a%5t8twUCC!cM21feU^|6(6dktx!d6JBh8E4R0o=X;xxbdsHzC z)`6a)wgjNvoNH>yD6F^Km(h@oyhZh*`p21guUpIo89q&`wm9Xpvt`>y(tN)e~ z{l+pS1n9-T^dv}~f%!#aTbP2Kr3=|a@j?y{l@sqBRFVN}TV}=^^BzTyaNE;Y>dg(Z zEp)PkoDz^^uDu2To-3xv63fkmpFIMO5MQMYHL@kJ3o3$MB~MpUQVWFSXcSk_i988y z>HZRQ@;$#bPRprilnW^LUu2t>B*`&vB_CsDQ_PfkD8=J4M_b8U*-Sq!SNZ440@z4^ z8pGbOqmqN_0aJ`BbNs}d{W){h-i`JuLxuaW4$Xyf->vgpmO)33`CB6tb@*Quj#j&6 zY(;f`H?R|?f}pKbCqha+jg{3Qypw)mk=9vMg?n_Jm_pw?rK)*JR5rD1D|ELNxMvWy zP3cJksgjxuXN9=E^gLBw8LS3Q)#3&zv+wPn;zc79RJHl3)bwPBVJyb0PdC&s=PY7!lzYo)ifhd_ zxQGLM5g8>KzhHUMP<{G99sjSQ;SNsG_5N$Ve%mAObHJ8R2{%S&|v@Z&Qqx$>5MAub*&6YJffXhWok&jv2D)bEJ0lRd5q z)lzp3lKuQ3Ec)kyG&N>oBEXHVKuUlbYqM1sTSd873Xt&;Rk7FQ0}C0Q({KO|VK5$m z9tMlKPUaENyUfSp+~@{1xh4!t!<&tnBmhT!v>Y<#RGmN=o(Dx_xm~uO3&apqoT=Ko z9&K<5=Gb8#6;P|*OK~R}U$_WOx;l@G$N>b$SuyNM`Y+zB<8r23UtwdhT?+}i8jU1* z)+j7pAvO*tIg0?%%1Vo$xaLB-nSP*O*rEvmCB)pKhE@p=vE zqB@87f4eSTSDpvw=@n2x5I&0-Ej8q9r7Imlf{@&tI6~U*PqT+i6V1S4w!nt8a8_|O zp{_TrcuDq?z0*Q~=0!&s#T))Tj*dezNIHd>pLmb3bAH(jr3!ef8PTVr#N?gnb8D*S zl~1waTq_w7|8+XrzIOH23Vd?)R2Lg}mZJNLP&f$ucCP^~ov2@kF+5KP+G$Boef#adY+`o3b$#Z@942ykgYNzvT=ZCF zF(2De=ye8kOT{b;M5X3z*xeS+8{@kBEys#mS=q$B#0x&)MQ#u#>bTbUeM$`Gx?LSu zPfaVbspGI1Sj}Rpx%sIj)Xdgwr13l!lP(_+vWiMpQMA_7?5le#a%hDW8oN$0 z2VUAXZ@OksB^3Pl@e68wvq7T>1Yt7Oc)FXA;&srLt;QMFqZRA9M`(pZTiy! z%Pe9g>uN9O&53qA@e>cBlb7;Nq2jw#yIU`&acX0tvPp@!vG=}-5v?XSqCyglJ4!+4 zv4}ae9<~q7Zcp@6m$i}`6gSibin^pUvm#lMr!D?;@~@Q?C5am08NWYJg;2`Pt0HN9 zy=4JBW4}nnlf2A`XXnN=Cp*;~Mx}M17SJ{FS4s%7Xd2qvd+SIfa?e zUkOZ6Iz4kp?wksV!S9bUt0c0B&4ra3!ihMPhU{b?u@2yNcE z=FN*t)uzw?G0MxMQCmROzbCcDB&4;P3x@dll$SQ4j3Qtr!Uz0PHkc*9I9kva!v_}S ztHD009vJ^Px=~lqhoiGJ1H>B#{b`1&_3(0tlHj z!Rd{U_1!Uwbv#R2Nh)I$Svi+Qhd`QO%A#?48F@1++UCpZ*M*l;k>7eIQ@k|_6EVv0 zEg~BKkOJ>MT_Widc&i;EC8BMu9NWO1+~fb8af8UO1fEl99h z(c&lpDKjRMDm_xO)6U>_u|!@R*s3R@RZEqA5=>a}OA)+gp6b=VmYMxG7G)AJ^VHAx zc0a3|Mvn7*E9h96Pu}Dqec5GKi5Z{~BW${L^PL`_sOEQIpeMevG3=_=s!B8J!rUa9 zLxmX~x;o|y*YyL*1ND~wAduybW?`D542)j$7H7Bt!>88Q5T3H+hWRqpl7Vbpb*@bIYfW%NO>OxSYSvbNnztTR6G2g(u3x2B z-KAjG9g1e%dcj+vceU2P=AwsrkB>J6t_+_^gDV@*8K<&@k~dCxF?yixg&l|2K@Oah zN($<^YL7(;d>dW^m`NCzEd;JU7#N1Y{xxOdaYwoNN?|q&b>kO2ad`YZn>CU`lod=H z^ngv&JGkTirfZ2=UsI+SE$c|0I;@yMn;`(MxhHt9(o2DZYtLnnvUo1( zwNG$gg#ng&X2({Aao;QI9A+@YiE15QEorxs8y1yPfmE68~F)5W18h2SSW7BwUq2#ckUT+&PtxHZ2Tz)?aY^q;D*sO%yn=^AwCSi zU2=Tm<%zY8Iu;ooOEpe+=R+VOao_pSX{K4p-~>MX^MD`srJm=2QYrTrrG0%$;A!1> zlNe6L(?1QCJT;rUb>F75f14nEdHNUpRw6<=h?;&r3h@p$fRFY)(T1iSoDw-;9e8XC zD>L+|XUg2(GgX$vL<%2*SCDgj5GH3>y@OY7$&Kq-8jyisl-2C3BWW7fJ6QLtlsZfV z8wX7+0p$@jeL?+GxuZ+c3tO zNmkJF8JAsx6F3S&XlTz+_a@w6*kG%l&j_#&rZSGP_ed@tihybq-YI#o`teC zpl)+3sCZW@cV|j>f7H%P5cU&M+(cZIDz4q(zxh3Y{1--qDZe<|zg%tL3qAd=^K|gy z>7YwD@Kom#dUCfNpSP=2v8PJpY6+yaSAgn4PIRXy2cnx-{&!Mm`{y^L_{Mn=_d%Nt z6Wn=LkTFiAZAaWgOLSIqRNlXZe7h*%oQPN{l1;o2TWr&1s(_hIG-6!?EKX&l zsO>gmm+0iv{yEJo46Z^IP|3iOP#orP6!#070K0%v^%o}Utf^a6=%m1>DfUCb{(@%k zFN>=fKH&4Ai=4FD%Bi>-jJ}rLW1oBo`U1x3t_J&wNH|lwkwxP$PIwdxuRGmmMbXt1 zusaVx%$?z=WHiWmh|NPR5Xer$%+*#ZHN^62Rowh5N{UHIi#cSt&qr5^RhbXdIP9@` z%b*{pzPJ$;%-(7>=*nv*x;LWA&wdUzbiU)3O0(5^OG>OLedAjP)e5tHQp92z?cnl+ z6l~pkS>81>{sca3E?_=-z}Txu>npTu!-yiCwSV5I)z}j<77(VLiE(Es{ z77W9cns73Spl2>x@pOR^$nE0tP~DFz=2IPUXnw;l6cvjDNtgHK3otyk0}Q?Kdv*Yw z$T;R8ynN+=)zjK4)b~qgYmJqP1mrD|wsb2CRO_qz5K4?#?5B`)elc?vQ*eBv(-}CIK z>ykR-(bdY-C`yeuQ{Fr+?H_i7|Tb@Ktd1nnm~3{1ZLRX-@dR{|``00Rj{N z6aWGM2msh=ur{fL!NaUL006dz0RRaA0000000031AOHXW00000c4cxyZ*pZWV^B*4 W1^@s60096205<>t0Mj@C0000K{#s-J literal 14163 zcmV-ZH>}7|O9KQH00ICA0O?F-HjtR2YTq^h07ZBK00{s90Cr_^LvM0rE@SO|Yg61v zvgr4TnExPikB4r%!9eWUyK9Eo3mAKe#lW%g?nKxQhv-&=hHj~kqy}?6>~BArSr64q zQmN@~<2m+j#L!Zy9$8uW&a7uop6tJjN70je{`>KVAAbk}?CCfhM*;kMe;sA}X%?;b zKeCr^Z}TD=v)Au;_x7I$N9je}5AxfjxQy~R55i;+z*q4w?uSL3Ch!VBS?3*`hW)GX zf(`KgpU`fUUIddc%cE>vj*+Aj>Oe%Zf_lB@J1HlRksVLXc26yLww5B8$$DjG$%ypI=Q5e57o z&T~E3T;Es^-WFk2M1x=r2DzB#MX>qTUa+;X@nn^#34)S&rl2;PWK-59;a3eEvPdzWz^~^heV{6s*8p)-PAoC*wFZ zpM-HjkAD2&*_{4SPeH}M7YF-CyKi>S4o{BX2DSf0Pji|R_7xPjlZepin&V;~UnJou z|M3TWGl+&kluXCL7s8n!_~*f!Pj3%jeL6llJ_vS#jh_Da@c8uInepu8-I@LH@c6`f z_U7P~@#J5JZw`L^;STZp(_5O?8BFR^v0XL!3&7gCslVDiJNUGF{KA+zJwAD3KKa#t zwD<0%`REw>vz|FRb38jfITOo!1v6I`mltp{`}F2@n0zXNC-gT_13H79pnn-=@OUEV zRWH~*?|(Xq&#CnUJA@xWcU$&$oyG&Tn{?9AMwnDLewjrPkc80tgTthVGT5-158|W< z$`4+rgXt*pZqCrbXwE=zTwJlA@JG+WodAB|U)5djj&8!+ys_)*4i1yJh&?7(Gld+F z;XOLQ-3L5L24OZZx`98c;8Y@EApWc$!UO)Vv9h|$z4Wu+WX&h=VRf(jX_7?! zqNekc^WWH$+J1J6BJ5v6lPI@4qR-@qYNzEqvItgx8h0EE5{H@O0%Znu9i?;X=qN1u zmz@eIOVAug#nGYT*@@>Uhsm|i7&;tvn(`(Zr`OTjDM&7#&%$$yT3FiNdqnBY4Cp132=d)rj(rF>zY~!qc z`~hcjF-kuTUxyQ5oX8xv17xq4AcVsI&%?nZY$w<%lRRnid(&hvg0uaJ_?q&7aKdi( z;}2gL59D|%{}GH|rr9_gZIh@2qenr4fCv7Le-G(pkVFONqEY|TX^|0}@ZU9HPreHh zvDU*iKow+R=p&?8_E|d{{5>&0pAi z^5o?->7&3u2Q5icQb-~(w3ruB-p}F*(=R@P$r`~OGjup?V`WxEN` z9I1xxl#^0kzlp*@ggV|1lW+$OF}&!AemT$)f9@83M$^f|KcXHgiadc5sZX=?B8&1|MdyRh zMHYS%Z}!5B^`$r8E{`%hK&a+u2c>L6cq`va+PO1wTJ}-6JV$xPKY-ulV2ZK-G-KBr4X@a;-ads!IZt6T?Fa!(dpF zf0M5$6Vz04PA`PWMPx{k!ITy>`GB=xKa`i{YIc;RsZ?JT?D+ZkQf}_w(+RGe4u?j* z;349kn5sqI`1@c-yqciAvS;@S1%BhjTjOQl22wJIe4Dxz%Su z`vb(z+#Z9hlw%7jEPG!xE&eu6pO-;LKS-udwXF&Jle6?HlE?{%G2UjYU?`JCCDx47 zK{P^B9&I!XqSEah7j>u8#$=S9LeXDE1w#8R$XXrV4yT?Xmi$%%_(+C z9lZvihZn9zmd8nXc&EWr+vKSr4syAVOp73n(KR8Zjluh`V)+L4Na|~06{jHzMy7py zGhikI5-vfJ<-g9+5Tp>=M{YwA1CcFhs{{3!_D?{eZfU4K(t2IGNV5az`5-B>Te&bn zlCK%O@*cOW#BOvR#-Ews93~f|IJqE&xNN~s@XHvEI-D6iE1lBTsPsd#;|HU-NwX_d z&|xJRVp0NNGcliL%emQ4KLwBYNc2D*rUt8dA7|<0D7ubDuw|Ruet3VT%#+RhGR%Wv z2q%9)6BjQZ=j$sBf~DPOLFeJ_JEL(ino3uLE%lA7%QD)Jb zL->=^5sDCtf-ys*fVm>^YzhI28N!e#km)d)j?cfL9d#U(s;xztmRc%jTWoiE?z_Ue zr$7S@mB`vIfQu;{dMF8kux0=?c$`0ngZ?4GldhOr=ocdy5=WvDFe~B(D6rUjbrTnt z=2RL-4?5KP@t`Z`VGufPR+=<(1YaK0Fr89Q?YgFp#2yX+r}jl?NWtYflRD>uX;CuB zHHLA1%MHAlu;_&F?j|@Nfo2SRP&9nt8mbU@6%92RoMg zzpZsD7`IRp-WBl(jt{7p9b9(Ut!qhkGj{0$)6Qh$yQf*^2d}Z^)>iNcs z^NcAYDP*I=S0KM^?0$3R?l)IVH038@(Kx!FCf89`=x933(lOJ81YV-&5iJHOAnYIp zbju>(#%U5gU`!SMT@izT>#X4hHtLeOvb5Z(!f&-fk7<)QmII6gK^4*@y#V3G$U?ru zIbgs96k-5yh>?CkGj1{I04D?CcMR-nJoa0;v`GY zN6|PK#}}7Ha8CRV&;alz;zQ+#28_Fdi8#SFo395;cFbjEpgd)V0;5|(z`v9TN zq>Hp~ zK==#>sk%A|5Z8uQxr-cxf}xfc6jTCN%v5^3L~DR~Z&fZ%upi}ZchyioN?$50bw3>w z8LoDA$T|AVk4E4P5goSMpu@rE3B^$c{ZX15xMyL8;q98&_Lm;6IGId~{8>t-zx-Ji zUBo#|A%AuggP8Fw#%RpE*$ZiTw%$z!EK*7LVHu`EV2Y;z1f#Tt}t!5l_q=`6m(!j8{j%r^(G zdC+LP6!rK;udoBCqGK_$&jvvbPd_ zXn8&zM>3U&M>qx397Ob(1?g9T@QZD`qG8&qs!eO5#6WFFTnoCphs>d=g}7p_Fja=W zHEC7VW1zy1E13b`QRogL* z?J~VP8Zt3&wQ$&&z^pg;>85VSL`*+sk7u#cf6t<9Y~VkOx;3LsF!fP7JlSd5;~U4o zv2Blv9z_<8h#9SXtu%w!T;mse$uu`>%-A`avd-PXfN~oX^D6x5% zAKcY0H=WmV)7HzC3CfKhsF|P~E*`7BvyXH}Nw+MU3Uh7|_me0ZL<1w9$dR3^5f{^H zy->UL5iv%_Z*rQFNF!zSE!3pa;Qjb{^6^_SXtR|uFxN#DF@BGq!jI&2eqR1K%GE^1 zX@VdD+9XWS`0xpR0vP**HQx!=^l&_)YQ#gf*j#FI3O9|&1tGRLdf^gE@T98>ECEU^ zjN5i=`j?aLu(rSa68xnb{1j|_9uCVUY&ooj_HK!8l|L?e9wul!&fDN;iJU%|*#iAs ztx#%4rR7t>NEFjEdiWUrybSY8-O`QC^H1Z50xq2h%LUCEyc7m?!p>h%TmaO=zqiKVus=s z67^vRFQO#MLM&eJ1f=@J@Fe~tx+NKJ#-pL-B*0(*&G1Hn^q_8e2ylXHxtyQG-37f}IX5(a2+|R$PS7CF z-f+ea#~~Kl=~Jb!0_8O&14bz(qqrzU6uvOuKVcsMLFIp;XYu)}@!;dC#y{}+)2Hg` zdLlLBjTwE^!Y_HAfr15#B_jx69%cm0*B|Maw6Q=g3n6f~YvQWJwkiEQU)2WZ9aU|Q zxkV1&Y}v4O$MpHzn^d<^?b9UNZrGf|eJWu8an*L>N&wu|i5ya{P|gh-UP#B{Fsnyd ziq#69NI6H5fdsqG`2t`AP0Q7wP0(Ty?P|jjDD`IsppiRVd{aA zo8Ny|e!pL>^8qk9h_~h9`AoE0#4jmFpW_>)QSe|Q%g{VOx^1slS%Iyi6aB@Ho^Gl` z@P0HBW2h(w+0Y>G;Lbd#iG{epQM?XE23>GWMdbhnd!IYP{NWMA-l+yTs&ckB=MI$0@D67Jo;;iMAU=C43#&i2brp3 zWhO{b6|Z6#LMxjcl$d8?UFMCQE#S5w$;C+S;a{+)ZJ zJA4hAkB-Ckbedo4pzQ@6GBZ8tZYaZ9adRHucf<_V0MMlm?W?97lx1nE=sK@fP6Rz1 z49cJaqUX#HeZ;6d5c~B9EBX7^Xm;1K)=HUq9*rSY=_nR9V8y`hhLQn7$ryZvk zz=7=rNAVc{BbbX&4-H3Ao4QKN30H6wu;Hon8KqTrn+u#&o?jD-L-Q6(`)p_jp z=)N&Dp0+XtIj}GU4`(8eA^9^Z4zS@6Rf5xc3Sq4pMesMq$e#Jz4T7dYh8()cXJV~K&rfcjnAcu;eCYZthL$YVZ-0SN5_V8-c9FbkayuE}7Dj+|&YT&4aZwx4)iAzH)iFv^eQ3dLg}QN$Hb?a299aYsy>86S5} z&2mUl!R3u1EQ=s2%nX8BDU!#X<5xBiW~jQ06JyCaC6*GDuq+_oJWS#g^$dBr*{<7@ zumF#<>gM_HX*i0D+dxmun1!{YY3^rIo0SJUtMdS+Q4K@_Q?lxxcaT@_EDwaHc=EF) zo-~uyWhIM{Vjh8vH82!&#@gDF?yVN-;Z{9EBx8W~u;R&x_R?*J*%G|%-*xyy?7Zoy zZ#}hbFV=_31y&+K2wQmRn*K9!Q=P44kR8g%ucta&OCUSSwJsyPlg#15&~7YKHltTw z9;S4t1xLl!s`0e~^*qu3Hxu zqA#R_NGJ?#^@RgqsR+V{qcVIKpTCRG-a~pqnt>2xwwCP` z$5|;qYa>XPvDJ73M?Qi1U>JiTN6A!Z?UGP9o!xmvN=v~FxrTBJpE$1+w6*w-GmuwPs3=k{DR7E3c>h2(7&1+NH{9Vx|u zZPkT}OXwj&EQY%m4Bte9X|WP~2t_)(`j%F8N+mShDrAy1s#mhla4$+=luXs(yLv)U%!;@;|jHqRQR zU?x857p-MLPHgd4)z_sd8(D7-6lD-$CFF|9v7^w@;_=l0=M52$-@VV?+9Bh7d-(z7 zp$#8a9_JrcP-;Jqlo{jJ)&!r-d2gM&3s8)&;{hNXOWfczt`4S-%n7X`*ettRT!uQP z(e;6(`XS}To80Fgl10m59X*marz;nkvIy?`;K!M|B3wk!c|7PM_Li5dNM6Zsg`x8)G|Z~ zYb{MjVFM*-=>@HM{duMFxFV=vH#o7-?>zLQ68H0;*3DvrI&0gupqV;(cxlQ= zP&wuI^F_f$d>ti$=|HJ9ZFKAlHDr6d9U?43^c5QSd$!h>ndFh6qaAP26o#s5;~6uU zRhk2zZD|ES{On_;!wXZ{9l?59fwK;5X}8W~w)G^gFw)>S!A{Whv03d<>wuR}t5RpH zqj#J}rzREEc?s!PHybG-=8yAAg|%+_U)O#_4s_QI!!q zWO%i@1u!FC7+$l0VG4?M6#(*i z>d^k)JtFztG)%K{I|^=hO+%)6l@e|8!XsmSc1W#>+mW1=*EEs0Y=VyNe0O|u)0O=YBdrV zN{t=OM~tcOCWDS;N2$Q;u2RvzW?m<6Y7WjDuUVaB^PbeNHM9EFcUlLZ)45NqfzB*! z6RT%*T#HyuaGZTD$7#{gpMQnxg1&VX(@(WTYd^MTkJxRoQme$5r*TrggCE=XQaE=( z7YIjRUG2OmlYR;NH>v!)%X#U+V$PJ|@mtsc9_`8;R_nn#IQJh`vS4k@0%3_8ac>rP zfX!F$laQOzo$(rk3OtX-J&P@r@6Bd~+m&LDwLe8>+ax9NCKrKFr-%8o(-RqgTgnOx z%1Hmp1_4|8a2o>3!-+?V#RK54#mH_T9A(7}%D>ACfU}&-Scp?44it-sd^0M-`?P2A?IFTC_Qg!z;X! zFN?}pcx5s|m7r*N9vP32Ts3!21>+$hl>p?$(!nm(9(Px6dFgDJ?>n+XDRfp97D-9(m+^W9gRY7FEog zvCIEvq07&nD1~zN@pJTDYoXi!UbW`STUMh0YXAc7z!Ajl4$0&#*^OdFZaXfM8<*>t}vC&eibH{vhca<608DCPJ) z199jsgE&-~mmdIepi=E3p=ut&h=;#JXwbszK@lEglbqH6!4Xk*g-iLy93o3~iF~7& z>$^+U_oz%%BsVlQA@o4IQs}945lAtgfTm`kr)3;_YEs0?fYKjlJ#0d+BFCv$6REKCCM?)6Qs& z&Gx2PZ-X^se{X9y!O@#*_9m}2Hg5+NHEZgP&$93)3Anvr$n?g;{1pbzs@AOwX<=3L z#Pjs?Vr-aZxK4;eiO^mQeU$o%(|WhZE$0muJhr7eTv^>AK6frYFrXP3)y!f~QHA=I zcLFAhvaBK`ycA14$I7b0wuGpwz{5Cd*hU4mml4Ceqfy%L1e<@h_HjR*+@gM`Abr<3 zEe#gb5c@7O;i>vfN43g54ZH-@R>rf?e# zI|!~;*KoXZMSWAj@h4+1l{^{&f}Wh5CGpH=Io7Fz5sPi0``dn)2z=jZvMXC1I}@cn zZPv3TD^{GXb)S>8taQZ&EA}!f_EcAKa?Hhz?aaRMu82plnecf>F$7rM*IV`4TJ~l` zjS5xBn+|jSVI$F!Go)KoTd1n#P3_yIDp#+9F}nUIlcmK1fwi?5ZaII&xZQK91)WH*1q( zSb1-xFJ8<@WBln%Ev<1Gim41JiMFsqq13+cD$b~G5{@z%fJAqzEz)^fmD^DFbki?^ z#;Q58Q3WyEJmf4W=q~tW4`p6!F3YI30M6`X#5{A8xmi+H-YT!5uK+&f(p|A!x~sZe zI(Ur*sT}Ea9=YHR*7%0vM?4+&@c?)R<=b_%oH;FJ?y4(_JaubxyuBO%H5KYwcm!I& z$$rAU;gh&H$6c@HG5NusxN-yJf)VYv3r(!aZB$pp2s2~`#q>OOLj z;Qjb{^0DUF*AUo`-c^%q)V4_y5#`S-e)K2X=|oHJL!pv$qm(VEWdm9Ccs)PLdDlk1tWYAEjysE<>I!F=)jr`H zc~NCda@zr1si}T}7xya+!i+fn;TQQxIt zqSgdAqrh+zg`fCaRORk}K*WjaRfc;f^og92|7qF&$k!Y7x72GcVb4 zs5YUe-?z*sbd|57CW2K4f9k=iu7FY$)|Ka7{Deo87 z!)K=_N`+Y739S4e>|dV79Rc{BfNZR?RI{cJHtCk(lS=fV(Q)eCFEF-4Sgnq<@5mA@|e%-{Q5f;wq3#_BSX1q*gO1x7A!up3~r6+cQFU4S| z8XhXa5h0AC#H@McNGR*GeF)D@VVgsij%i1KRfe>Xn2q?uowp{!OJ>+(SG zQPBrxTMU)xazKG$3V#M`GO>~`kBa!LaT-8tLa!pqDX&fEqT_JBiLN7nd4m(cpp#Wb zH_nxxx$PvjZhKxxN7Jmuu=c2;Aq(m$<(2@n+cQWDica-QRfWtENLP|VyPi)XC3ZWF z#4cYh1u;QL!z{zHRX|U}7E90!vKdznT_TgRFVN>TV}=^ z{dyILaNAQ?>Wr>6Ep)P!Mkyf4EH?!J+zC{YC6*NdKYIimA-+l*YGg`aS5zCZPM)r% zqy`8nFh<-=AtDWxrMpXU$oKp*2_-7gE1F*JzsU2b2s3BVHGGVlY#n@Cq zM~?ZM7m8Z^uMS6>-94(JI=_qe2vb4OE>$N&N;MIL)nmDreqoT-SyY7ux=wVVZ=O=s zyd)}<+O-wB+X~z>2-~{!q=2-Pn(p*`Xm+X5WmO7F+|PY+wN z{L*Mu&+#=5ubWZ+(EMHmeSGKk-?{yFZvXYTz1zM#)aq#}H-cpp)A0~kyW`fa`Ecol zGh>bRns*h$*IoBbn>8&Rmt3|G><)`yl%`jCFp96-TaVk0n;e!&k;tt&kMr&vaKU*n z-K%|2Qs7J`slKKLR4>P zZh5f9#T(#>$RyG51Hi`c?%@<|&%fg5H@)#L=X+W6sC1VDbp9ERrje4M z&XSz4Wc>8vlDvs@J#{*mj%uB=yx0{0Kfb_(<=5;BQCh!Bq_>Bn4UytK8@S3!zbA@4 z^|%_;NZmO|4)de1=wAxb32+%p;(8nTy5QkqzbKd>EF3H(N7F0G8@#IAipwT0t;8MVH8OyC{Aeh#{yq z({k^6w80gaV}^LtK&^f+#jPKF;UX;Q<}xlK3lJP<#jt1Tzj(8b&6)08r2)luEhXS; zG?L_5p|EsG#yFhhEc!#-Z4zfPVj_RQg#^_&Dg_~Fsqb)+%_Le2#iDQWicqRv8B*m( z$G5fMp-dszs5npYDvG&~Zabes5dtcRxj_;6%InI!&5OGjoIIa8?ln?Cwr%a|ICYyFp4+)dmNpHWQ?@RA3ky(Ve9;|8A=uKPBEZQMS-S!)92Py z&ncf`y_QxoBL3@ilzr{0txNF9)l)S}+*yk3D?)imlGExnprsS_3o(A@@jy8(>G^Mj z^dyr{;Aq3MFjrX5bBdHfBJ>S&T^CV5yxJ48FM&C+_>3s}jJx&ugbu>SATykGCC9DmDH_4=kqIU(u zkDbz)l*@_t)P`KE%-%p4y-z8|OVu6wZg7Yx(qtuZ(uYxEndLyW@`2MvT$KRPr4QLDejtnw!79>bBKXVpPlq3)hp8ROAR1C4gN7mqoz^qkRbB8Lw1);jD!@%Zb&t@iG}gtm9q435c32lnaC0)g9mN8(

iEJjFb z!XIW6AEXicsGeaNuz6CQ<&qr2NwJP!=6cFRP!>lP14+sohwG9gs>zn$MAtxnSS$Bw z+no|vWf7}bS9>{cPPF5Zn|KJFypnec72l@X-DWY3QyU$XbxOpIy^AJBw3=Lt3P}|1 zC^V>=vnbf|nlcY~530Wv1%Gh?MM#tWTxlBv|L9h zr!e!m>s6MNZd<<;REv$}-=AbgjVEW_OT}3m7s6esISUA3yrON4MJQSET`W4kX(cs*vsf0?X%Ogw8%-Q)qY;K7C@B#{b`12_3(0v_cUY9VO-z`NnW2XY z>ti_&!TGI=_1!aybv#Q-Nh)I$St*xghd}CJ%A#?49XYcq+UCms3veN7)FpoF=}hrX zD@w#D!`Fyt{6h-7{H9umz+3MSsSs@&?H1O^Krfq|BI1TI!LCopuJdiy`vjz(y?*z)>0gC;TLstm2j;c)h%`SNB?G_TLzk zNx;le7uVVStZo`P&QmN*t7knq6Nl7gS6#%Rfkuq5ZCBZ~dVEwizXt<7bCrx?7o^oy znJKTSOQJbcmrl+A9RdU08nQFyArmi|yCi|r!xS^padj&OXt3StA!x!<@&*nF3dZ&!oXs4QP#1TRzDdC%hazQ1!x& z!_PquoRrE5s<~?4iW2xb{0v|wVPLipxaMGB7y|oOl!oCAdPw&{MF7A3oox==lLN`nj{5x2x# z#!(h#mvJAEgeNCF&b9mmo-xgG4-6FVIWD5M_O3hkj5up0kJq;Tl!JEWN=C55XgqTr ztWk&$18`R?-*|Omtyjk)!(*kv>27@pL?rH8A6m^6D;b=?$A2F18KZoyPp5)&zW2wp+X@j;keVD%1Oxh2=GX7L~czm!(9FP5aKUF~4p zty1YQ5o{bZu>_Py)Qo#Fd=Azmf0#LSHI4_bMbBj$zSvGkUv^e!yYOXe4F(MVYc|?4 z#WswwVUjiUe8y#0V1*Jk>CiSf?m65+b15|@`}e$*z_BJ#p8=gKJTL)81gq3W1&HMg z?sEr$<$H;;y7Ja{6=A=wyC$8o4L`B8eYi|qekuKC%Bt5@Dr@uJFAam4U;E7H@xU=5 zEPy5_#Uw6QFfiZK2+-4Z%sR@p+?!HWkejv?tHvhTnsPN9BuUA&q4M1hX989^;+XT74vFMU%`ijCCG zy3Y!tms7y*901XGhNF_!Am<@A53xWXI}I~eTdCC$tE*LU^RFl=CM7NAkl{WbRVgmZ zeCWnuhs|3C{aCfdwWwhBR;fW(T{F?X4OM>jbFiiI9lKPTsn#1(Vom8A*E*plm$w+8w=y!cBdNPnR0r~6x#qFMcHh1a;n=;j>$h^ zG2flqavA&^%61cj{;UnwR7TP{{~1cP*SG}jaEJP|Qr3mkNPMynnxZLOft3!m&>`Bo zW7TC!0V9+6Q;oDRN-=6FZM+tvntW)lvFi3-aej8=+r`D9svlL%r#|9P|At>CDi#NlF7L|~V0dZ< z7&_zk%m6x(am+z_w=85n`J*6nx*%jenGZ4p2d}Fe)PU+IUj@}q8c{uMMD;Sp^y{KJ zhQFXa(9F;zh2|MEsX8%#?-s@Fa5@4kAz)K4*CaGkz2rfftQKp1(4N*G{3&53QO7|s zPsGuo@RagodH`n%GQTW9=P! zEz0|du(@_^5_EK;UleKalA{xon_#*we9gdtNyz%wIofyFO;BQ;W_hur6D%-xw4%+M z+P;m7!z3@P}Xl@TZBA z7|cKe2>P$kX8K{a7rdfTqQSvTWMH*^gm^xuf7DZjG5X;6MR4+xMfWxQ6FtpoPWZq7 z0Z>Z;0u%rg00ICA0O?F-HjtR2YTq^h07ZBK00{s9000000096X000000001XWpYDr da%C=KP)h{{000000RRC2Hvj+t1~&iz00845Z$kh8 diff --git a/src/map/if/ifUtil.c b/src/map/if/ifUtil.c index f4ffa4c10..f3fa049e1 100644 --- a/src/map/if/ifUtil.c +++ b/src/map/if/ifUtil.c @@ -427,6 +427,26 @@ int If_ManCrossCut( If_Man_t * p ) return nCutSizeMax; } +/**Function************************************************************* + + Synopsis [Computes cross-cut of the circuit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_ManCountTrueArea( If_Man_t * p ) +{ + If_Obj_t * pObj; + int i, Area = 0; + Vec_PtrForEachEntry( p->vMapped, pObj, i ) + Area += 1 + (If_ObjCutBest(pObj)->nLeaves > (unsigned)p->pPars->nLutSize / 2); + return Area; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// ////////////////////////////////////////////////////////////////////////