| /**CFile**************************************************************** | |
| FileName [fsimFront.c] | |
| SystemName [ABC: Logic synthesis and verification system.] | |
| PackageName [Fast sequential AIG simulator.] | |
| Synopsis [Simulation frontier.] | |
| Author [Alan Mishchenko] | |
| Affiliation [UC Berkeley] | |
| Date [Ver. 1.0. Started - June 20, 2005.] | |
| Revision [$Id: fsimFront.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] | |
| ***********************************************************************/ | |
| #include "fsimInt.h" | |
| ABC_NAMESPACE_IMPL_START | |
| //////////////////////////////////////////////////////////////////////// | |
| /// DECLARATIONS /// | |
| //////////////////////////////////////////////////////////////////////// | |
| //////////////////////////////////////////////////////////////////////// | |
| /// FUNCTION DEFINITIONS /// | |
| //////////////////////////////////////////////////////////////////////// | |
| /**Function************************************************************* | |
| Synopsis [] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| static inline void Fsim_ManStoreNum( Fsim_Man_t * p, int Num ) | |
| { | |
| unsigned x = (unsigned)Num; | |
| assert( Num >= 0 ); | |
| while ( x & ~0x7f ) | |
| { | |
| *p->pDataCur++ = (x & 0x7f) | 0x80; | |
| x >>= 7; | |
| } | |
| *p->pDataCur++ = x; | |
| assert( p->pDataCur - p->pDataAig < p->nDataAig ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| static inline int Fsim_ManRestoreNum( Fsim_Man_t * p ) | |
| { | |
| int ch, i, x = 0; | |
| for ( i = 0; (ch = *p->pDataCur++) & 0x80; i++ ) | |
| x |= (ch & 0x7f) << (7 * i); | |
| assert( p->pDataCur - p->pDataAig < p->nDataAig ); | |
| return x | (ch << (7 * i)); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| static inline void Fsim_ManStoreObj( Fsim_Man_t * p, Fsim_Obj_t * pObj ) | |
| { | |
| if ( p->pDataAig2 ) | |
| { | |
| *p->pDataCur2++ = pObj->iNode; | |
| *p->pDataCur2++ = pObj->iFan0; | |
| *p->pDataCur2++ = pObj->iFan1; | |
| return; | |
| } | |
| if ( pObj->iFan0 && pObj->iFan1 ) // and | |
| { | |
| assert( pObj->iNode ); | |
| assert( pObj->iNode >= p->iNodePrev ); | |
| assert( (pObj->iNode << 1) > pObj->iFan0 ); | |
| assert( pObj->iFan0 > pObj->iFan1 ); | |
| Fsim_ManStoreNum( p, ((pObj->iNode - p->iNodePrev) << 2) | 3 ); | |
| Fsim_ManStoreNum( p, (pObj->iNode << 1) - pObj->iFan0 ); | |
| Fsim_ManStoreNum( p, pObj->iFan0 - pObj->iFan1 ); | |
| p->iNodePrev = pObj->iNode; | |
| } | |
| else if ( !pObj->iFan0 && !pObj->iFan1 ) // ci | |
| { | |
| assert( pObj->iNode ); | |
| assert( pObj->iNode >= p->iNodePrev ); | |
| Fsim_ManStoreNum( p, ((pObj->iNode - p->iNodePrev) << 2) | 1 ); | |
| p->iNodePrev = pObj->iNode; | |
| } | |
| else // if ( !pObj->iFan0 && pObj->iFan1 ) // co | |
| { | |
| assert( pObj->iNode == 0 ); | |
| assert( pObj->iFan0 != 0 ); | |
| assert( pObj->iFan1 == 0 ); | |
| assert( ((p->iNodePrev << 1) | 1) >= pObj->iFan0 ); | |
| Fsim_ManStoreNum( p, (((p->iNodePrev << 1) | 1) - pObj->iFan0) << 1 ); | |
| } | |
| } | |
| /**Function************************************************************* | |
| Synopsis [] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| static inline int Fsim_ManRestoreObj( Fsim_Man_t * p, Fsim_Obj_t * pObj ) | |
| { | |
| int iValue = Fsim_ManRestoreNum( p ); | |
| if ( (iValue & 3) == 3 ) // and | |
| { | |
| pObj->iNode = (iValue >> 2) + p->iNodePrev; | |
| pObj->iFan0 = (pObj->iNode << 1) - Fsim_ManRestoreNum( p ); | |
| pObj->iFan1 = pObj->iFan0 - Fsim_ManRestoreNum( p ); | |
| p->iNodePrev = pObj->iNode; | |
| } | |
| else if ( (iValue & 3) == 1 ) // ci | |
| { | |
| pObj->iNode = (iValue >> 2) + p->iNodePrev; | |
| pObj->iFan0 = 0; | |
| pObj->iFan1 = 0; | |
| p->iNodePrev = pObj->iNode; | |
| } | |
| else // if ( (iValue & 1) == 0 ) // co | |
| { | |
| pObj->iNode = 0; | |
| pObj->iFan0 = ((p->iNodePrev << 1) | 1) - (iValue >> 1); | |
| pObj->iFan1 = 0; | |
| } | |
| return 1; | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Determine the frontier.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| static inline int Fsim_ManFrontFindNext( Fsim_Man_t * p, char * pFront ) | |
| { | |
| assert( p->iNumber < (1 << 30) - p->nFront ); | |
| while ( 1 ) | |
| { | |
| if ( p->iNumber % p->nFront == 0 ) | |
| p->iNumber++; | |
| if ( pFront[p->iNumber % p->nFront] == 0 ) | |
| { | |
| pFront[p->iNumber % p->nFront] = 1; | |
| return p->iNumber; | |
| } | |
| p->iNumber++; | |
| } | |
| return -1; | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Verifies the frontier.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Fsim_ManVerifyFront( Fsim_Man_t * p ) | |
| { | |
| Fsim_Obj_t * pObj; | |
| int * pFans0, * pFans1; // representation of fanins | |
| int * pFrontToId; // mapping of nodes into frontier variables | |
| int i, iVar0, iVar1; | |
| pFans0 = ABC_ALLOC( int, p->nObjs ); | |
| pFans1 = ABC_ALLOC( int, p->nObjs ); | |
| pFans0[0] = pFans1[0] = 0; | |
| pFans0[1] = pFans1[1] = 0; | |
| pFrontToId = ABC_CALLOC( int, p->nFront ); | |
| if ( Aig_ObjRefs(Aig_ManConst1(p->pAig)) ) | |
| pFrontToId[1] = 1; | |
| Fsim_ManForEachObj( p, pObj, i ) | |
| { | |
| if ( pObj->iNode ) | |
| pFrontToId[pObj->iNode % p->nFront] = i; | |
| iVar0 = Fsim_Lit2Var(pObj->iFan0); | |
| iVar1 = Fsim_Lit2Var(pObj->iFan1); | |
| pFans0[i] = Fsim_Var2Lit(pFrontToId[iVar0 % p->nFront], Fsim_LitIsCompl(pObj->iFan0)); | |
| pFans1[i] = Fsim_Var2Lit(pFrontToId[iVar1 % p->nFront], Fsim_LitIsCompl(pObj->iFan1)); | |
| } | |
| for ( i = 0; i < p->nObjs; i++ ) | |
| { | |
| assert( pFans0[i] == p->pFans0[i] ); | |
| assert( pFans1[i] == p->pFans1[i] ); | |
| } | |
| ABC_FREE( pFrontToId ); | |
| ABC_FREE( pFans0 ); | |
| ABC_FREE( pFans1 ); | |
| } | |
| /**Function************************************************************* | |
| Synopsis [Determine the frontier.] | |
| Description [] | |
| SideEffects [] | |
| SeeAlso [] | |
| ***********************************************************************/ | |
| void Fsim_ManFront( Fsim_Man_t * p, int fCompressAig ) | |
| { | |
| Fsim_Obj_t Obj, * pObj = &Obj; | |
| char * pFront; // places used for the frontier | |
| int * pIdToFront; // mapping of nodes into frontier places | |
| int i, iVar0, iVar1, nCrossCut = 0, nCrossCutMax = 0; | |
| // start the frontier | |
| pFront = ABC_CALLOC( char, p->nFront ); | |
| pIdToFront = ABC_ALLOC( int, p->nObjs ); | |
| pIdToFront[0] = -1; | |
| pIdToFront[1] = -1; | |
| // add constant node | |
| p->iNumber = 1; | |
| if ( p->pRefs[1] ) | |
| { | |
| pIdToFront[1] = Fsim_ManFrontFindNext( p, pFront ); | |
| nCrossCut = 1; | |
| } | |
| // allocate room for data | |
| if ( fCompressAig ) | |
| { | |
| p->nDataAig = p->nObjs * 6; | |
| p->pDataAig = ABC_ALLOC( unsigned char, p->nDataAig ); | |
| p->pDataCur = p->pDataAig; | |
| p->iNodePrev = 0; | |
| } | |
| else | |
| { | |
| p->pDataAig2 = ABC_ALLOC( int, 3 * p->nObjs ); | |
| p->pDataCur2 = p->pDataAig2 + 6; | |
| } | |
| // iterate through the objects | |
| for ( i = 2; i < p->nObjs; i++ ) | |
| { | |
| if ( p->pFans0[i] == 0 ) // ci | |
| { | |
| // store node | |
| pIdToFront[i] = Fsim_ManFrontFindNext( p, pFront ); | |
| pObj->iNode = pIdToFront[i]; | |
| pObj->iFan0 = 0; | |
| pObj->iFan1 = 0; | |
| Fsim_ManStoreObj( p, pObj ); | |
| // handle CIs without fanout | |
| if ( p->pRefs[i] == 0 ) | |
| { | |
| pFront[pIdToFront[i] % p->nFront] = 0; | |
| pIdToFront[i] = -1; | |
| } | |
| } | |
| else if ( p->pFans1[i] == 0 ) // co | |
| { | |
| assert( p->pRefs[i] == 0 ); | |
| // get the fanin | |
| iVar0 = Fsim_Lit2Var(p->pFans0[i]); | |
| assert( pIdToFront[iVar0] > 0 ); | |
| // store node | |
| pObj->iNode = 0; | |
| pObj->iFan0 = Fsim_Var2Lit(pIdToFront[iVar0], Fsim_LitIsCompl(p->pFans0[i])); | |
| pObj->iFan1 = 0; | |
| Fsim_ManStoreObj( p, pObj ); | |
| // deref the fanin | |
| if ( --p->pRefs[iVar0] == 0 ) | |
| { | |
| pFront[pIdToFront[iVar0] % p->nFront] = 0; | |
| pIdToFront[iVar0] = -1; | |
| nCrossCut--; | |
| } | |
| } | |
| else | |
| { | |
| // get the fanins | |
| iVar0 = Fsim_Lit2Var(p->pFans0[i]); | |
| assert( pIdToFront[iVar0] > 0 ); | |
| iVar1 = Fsim_Lit2Var(p->pFans1[i]); | |
| assert( pIdToFront[iVar1] > 0 ); | |
| // store node | |
| pIdToFront[i] = Fsim_ManFrontFindNext( p, pFront ); | |
| pObj->iNode = pIdToFront[i]; | |
| pObj->iFan0 = Fsim_Var2Lit(pIdToFront[iVar0], Fsim_LitIsCompl(p->pFans0[i])); | |
| pObj->iFan1 = Fsim_Var2Lit(pIdToFront[iVar1], Fsim_LitIsCompl(p->pFans1[i])); | |
| Fsim_ManStoreObj( p, pObj ); | |
| // deref the fanins | |
| if ( --p->pRefs[iVar0] == 0 ) | |
| { | |
| pFront[pIdToFront[iVar0] % p->nFront] = 0; | |
| pIdToFront[iVar0] = -1; | |
| nCrossCut--; | |
| } | |
| if ( --p->pRefs[iVar1] == 0 ) | |
| { | |
| pFront[pIdToFront[iVar1] % p->nFront] = 0; | |
| pIdToFront[iVar1] = -1; | |
| nCrossCut--; | |
| } | |
| // handle nodes without fanout (choice nodes) | |
| if ( p->pRefs[i] == 0 ) | |
| { | |
| pFront[pIdToFront[i] % p->nFront] = 0; | |
| pIdToFront[i] = -1; | |
| } | |
| } | |
| if ( p->pRefs[i] ) | |
| if ( nCrossCutMax < ++nCrossCut ) | |
| nCrossCutMax = nCrossCut; | |
| } | |
| assert( p->pDataAig2 == NULL || p->pDataCur2 - p->pDataAig2 == (3 * p->nObjs) ); | |
| assert( nCrossCut == 0 ); | |
| assert( nCrossCutMax == p->nCrossCutMax ); | |
| for ( i = 0; i < p->nFront; i++ ) | |
| assert( pFront[i] == 0 ); | |
| ABC_FREE( pFront ); | |
| ABC_FREE( pIdToFront ); | |
| // Fsim_ManVerifyFront( p ); | |
| ABC_FREE( p->pFans0 ); | |
| ABC_FREE( p->pFans1 ); | |
| ABC_FREE( p->pRefs ); | |
| } | |
| //////////////////////////////////////////////////////////////////////// | |
| /// END OF FILE /// | |
| //////////////////////////////////////////////////////////////////////// | |
| ABC_NAMESPACE_IMPL_END | |