diff options
Diffstat (limited to 'src/base/abci/abcOdc.c')
| -rw-r--r-- | src/base/abci/abcOdc.c | 1134 |
1 files changed, 0 insertions, 1134 deletions
diff --git a/src/base/abci/abcOdc.c b/src/base/abci/abcOdc.c deleted file mode 100644 index d6e59328..00000000 --- a/src/base/abci/abcOdc.c +++ /dev/null @@ -1,1134 +0,0 @@ -/**CFile**************************************************************** - - FileName [abcOdc.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Network and node package.] - - Synopsis [Scalable computation of observability don't-cares.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: abcOdc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "abc.h" - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -#define ABC_DC_MAX_NODES (1<<15) - -typedef unsigned short Odc_Lit_t; - -typedef struct Odc_Obj_t_ Odc_Obj_t; // 16 bytes -struct Odc_Obj_t_ -{ - Odc_Lit_t iFan0; // first fanin - Odc_Lit_t iFan1; // second fanin - Odc_Lit_t iNext; // next node in the hash table - unsigned short TravId; // the traversal ID - unsigned uData; // the computed data - unsigned uMask; // the variable mask -}; - -typedef struct Odc_Man_t_ Odc_Man_t; -struct Odc_Man_t_ -{ - // dont'-care parameters - int nVarsMax; // the max number of cut variables - int nLevels; // the number of ODC levels - int fVerbose; // the verbosiness flag - int fVeryVerbose;// the verbosiness flag to print per-node stats - int nPercCutoff; // cutoff percentage - - // windowing - Abc_Obj_t * pNode; // the node for windowing - Vec_Ptr_t * vLeaves; // the number of the cut - Vec_Ptr_t * vRoots; // the roots of the cut - Vec_Ptr_t * vBranches; // additional inputs - - // internal AIG package - // objects - int nPis; // number of PIs (nVarsMax + 32) - int nObjs; // number of objects (Const1, PIs, ANDs) - int nObjsAlloc; // number of objects allocated - Odc_Obj_t * pObjs; // objects - Odc_Lit_t iRoot; // the root object - unsigned short nTravIds; // the number of travIDs - // structural hashing - Odc_Lit_t * pTable; // hash table - int nTableSize; // hash table size - Vec_Int_t * vUsedSpots; // the used spots - - // truth tables - int nBits; // the number of bits - int nWords; // the number of words - Vec_Ptr_t * vTruths; // truth tables for each node - Vec_Ptr_t * vTruthsElem; // elementary truth tables for the PIs - unsigned * puTruth; // the place where the resulting truth table does - - // statistics - int nWins; // the number of windows processed - int nWinsEmpty; // the number of empty windows - int nSimsEmpty; // the number of empty simulation infos - int nQuantsOver; // the number of quantification overflows - int nWinsFinish; // the number of windows that finished - int nTotalDcs; // total percentage of DCs - - // runtime - int timeClean; // windowing - int timeWin; // windowing - int timeMiter; // computing the miter - int timeSim; // simulation - int timeQuant; // quantification - int timeTruth; // truth table - int timeTotal; // useful runtime - int timeAbort; // aborted runtime -}; - - -// quantity of different objects -static inline int Odc_PiNum( Odc_Man_t * p ) { return p->nPis; } -static inline int Odc_NodeNum( Odc_Man_t * p ) { return p->nObjs - p->nPis - 1; } -static inline int Odc_ObjNum( Odc_Man_t * p ) { return p->nObjs; } - -// complemented attributes of objects -static inline int Odc_IsComplement( Odc_Lit_t Lit ) { return Lit & (Odc_Lit_t)1; } -static inline Odc_Lit_t Odc_Regular( Odc_Lit_t Lit ) { return Lit & ~(Odc_Lit_t)1; } -static inline Odc_Lit_t Odc_Not( Odc_Lit_t Lit ) { return Lit ^ (Odc_Lit_t)1; } -static inline Odc_Lit_t Odc_NotCond( Odc_Lit_t Lit, int c ) { return Lit ^ (Odc_Lit_t)(c!=0); } - -// specialized Literals -static inline Odc_Lit_t Odc_Const0() { return 1; } -static inline Odc_Lit_t Odc_Const1() { return 0; } -static inline Odc_Lit_t Odc_Var( Odc_Man_t * p, int i ) { assert( i >= 0 && i < p->nPis ); return (i+1) << 1; } -static inline int Odc_IsConst( Odc_Lit_t Lit ) { return Lit < (Odc_Lit_t)2; } -static inline int Odc_IsTerm( Odc_Man_t * p, Odc_Lit_t Lit ) { return (int)(Lit>>1) <= p->nPis; } - -// accessing internal storage -static inline Odc_Obj_t * Odc_ObjNew( Odc_Man_t * p ) { assert( p->nObjs < p->nObjsAlloc ); return p->pObjs + p->nObjs++; } -static inline Odc_Lit_t Odc_Obj2Lit( Odc_Man_t * p, Odc_Obj_t * pObj ) { assert( pObj ); return (pObj - p->pObjs) << 1; } -static inline Odc_Obj_t * Odc_Lit2Obj( Odc_Man_t * p, Odc_Lit_t Lit ) { assert( !(Lit & 1) && (int)(Lit>>1) < p->nObjs ); return p->pObjs + (Lit>>1); } - -// fanins and their complements -static inline Odc_Lit_t Odc_ObjChild0( Odc_Obj_t * pObj ) { return pObj->iFan0; } -static inline Odc_Lit_t Odc_ObjChild1( Odc_Obj_t * pObj ) { return pObj->iFan1; } -static inline Odc_Lit_t Odc_ObjFanin0( Odc_Obj_t * pObj ) { return Odc_Regular(pObj->iFan0); } -static inline Odc_Lit_t Odc_ObjFanin1( Odc_Obj_t * pObj ) { return Odc_Regular(pObj->iFan1); } -static inline int Odc_ObjFaninC0( Odc_Obj_t * pObj ) { return Odc_IsComplement(pObj->iFan0); } -static inline int Odc_ObjFaninC1( Odc_Obj_t * pObj ) { return Odc_IsComplement(pObj->iFan1); } - -// traversal IDs -static inline void Odc_ManIncrementTravId( Odc_Man_t * p ) { p->nTravIds++; } -static inline void Odc_ObjSetTravIdCurrent( Odc_Man_t * p, Odc_Obj_t * pObj ) { pObj->TravId = p->nTravIds; } -static inline int Odc_ObjIsTravIdCurrent( Odc_Man_t * p, Odc_Obj_t * pObj ) { return (int )((int)pObj->TravId == p->nTravIds); } - -// truth tables -static inline unsigned * Odc_ObjTruth( Odc_Man_t * p, Odc_Lit_t Lit ) { assert( !(Lit & 1) ); return Vec_PtrEntry(p->vTruths, Lit >> 1); } - -// iterators -#define Odc_ForEachPi( p, Lit, i ) \ - for ( i = 0; (i < Odc_PiNum(p)) && (((Lit) = Odc_Var(p, i)), 1); i++ ) -#define Odc_ForEachAnd( p, pObj, i ) \ - for ( i = 1 + Odc_CiNum(p); (i < Odc_ObjNum(p)) && ((pObj) = (p)->pObjs + i); i++ ) - - -// exported functions -extern Odc_Man_t * Abc_NtkDontCareAlloc( int nVarsMax, int nLevels, int fVerbose, int fVeryVerbose ); -extern void Abc_NtkDontCareClear( Odc_Man_t * p ); -extern void Abc_NtkDontCareFree( Odc_Man_t * p ); -extern int Abc_NtkDontCareCompute( Odc_Man_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, unsigned * puTruth ); - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Allocates the don't-care manager.] - - Description [The parameters are the max number of cut variables, - the number of fanout levels used for the ODC computation, and verbosiness.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Odc_Man_t * Abc_NtkDontCareAlloc( int nVarsMax, int nLevels, int fVerbose, int fVeryVerbose ) -{ - Odc_Man_t * p; - unsigned * pData; - int i, k; - p = ALLOC( Odc_Man_t, 1 ); - memset( p, 0, sizeof(Odc_Man_t) ); - assert( nVarsMax > 4 && nVarsMax < 16 ); - assert( nLevels > 0 && nLevels < 10 ); - - srand( 0xABC ); - - // dont'-care parameters - p->nVarsMax = nVarsMax; - p->nLevels = nLevels; - p->fVerbose = fVerbose; - p->fVeryVerbose = fVeryVerbose; - p->nPercCutoff = 10; - - // windowing - p->vRoots = Vec_PtrAlloc( 128 ); - p->vBranches = Vec_PtrAlloc( 128 ); - - // internal AIG package - // allocate room for objects - p->nObjsAlloc = ABC_DC_MAX_NODES; - p->pObjs = ALLOC( Odc_Obj_t, p->nObjsAlloc * sizeof(Odc_Obj_t) ); - p->nPis = nVarsMax + 32; - p->nObjs = 1 + p->nPis; - memset( p->pObjs, 0, p->nObjs * sizeof(Odc_Obj_t) ); - // set the PI masks - for ( i = 0; i < 32; i++ ) - p->pObjs[1 + p->nVarsMax + i].uMask = (1 << i); - // allocate hash table - p->nTableSize = p->nObjsAlloc/3 + 1; - p->pTable = ALLOC( Odc_Lit_t, p->nTableSize * sizeof(Odc_Lit_t) ); - memset( p->pTable, 0, p->nTableSize * sizeof(Odc_Lit_t) ); - p->vUsedSpots = Vec_IntAlloc( 1000 ); - - // truth tables - p->nWords = Abc_TruthWordNum( p->nVarsMax ); - p->nBits = p->nWords * 8 * sizeof(unsigned); - p->vTruths = Vec_PtrAllocSimInfo( p->nObjsAlloc, p->nWords ); - p->vTruthsElem = Vec_PtrAllocSimInfo( p->nVarsMax, p->nWords ); - - // set elementary truth tables - Abc_InfoFill( Vec_PtrEntry(p->vTruths, 0), p->nWords ); - for ( k = 0; k < p->nVarsMax; k++ ) - { -// pData = Odc_ObjTruth( p, Odc_Var(p, k) ); - pData = Vec_PtrEntry( p->vTruthsElem, k ); - Abc_InfoClear( pData, p->nWords ); - for ( i = 0; i < p->nBits; i++ ) - if ( i & (1 << k) ) - pData[i>>5] |= (1 << (i&31)); - } - - // set random truth table for the additional inputs - for ( k = p->nVarsMax; k < p->nPis; k++ ) - { - pData = Odc_ObjTruth( p, Odc_Var(p, k) ); - Abc_InfoRandom( pData, p->nWords ); - } - - // set the miter to the unused value - p->iRoot = 0xffff; - return p; -} - -/**Function************************************************************* - - Synopsis [Clears the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkDontCareClear( Odc_Man_t * p ) -{ - int clk = clock(); - // clean the structural hashing table - if ( Vec_IntSize(p->vUsedSpots) > p->nTableSize/3 ) // more than one third - memset( p->pTable, 0, sizeof(Odc_Lit_t) * p->nTableSize ); - else - { - int iSpot, i; - Vec_IntForEachEntry( p->vUsedSpots, iSpot, i ) - p->pTable[iSpot] = 0; - } - Vec_IntClear( p->vUsedSpots ); - // reset the number of nodes - p->nObjs = 1 + p->nPis; - // reset the root node - p->iRoot = 0xffff; - -p->timeClean += clock() - clk; -} - -/**Function************************************************************* - - Synopsis [Frees the don't-care manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkDontCareFree( Odc_Man_t * p ) -{ - if ( p->fVerbose ) - { - printf( "Wins = %5d. Empty = %5d. SimsEmpty = %5d. QuantOver = %5d. WinsFinish = %5d.\n", - p->nWins, p->nWinsEmpty, p->nSimsEmpty, p->nQuantsOver, p->nWinsFinish ); - printf( "Ave DCs per window = %6.2f %%. Ave DCs per finished window = %6.2f %%.\n", - 1.0*p->nTotalDcs/p->nWins, 1.0*p->nTotalDcs/p->nWinsFinish ); - printf( "Runtime stats of the ODC manager:\n" ); - PRT( "Cleaning ", p->timeClean ); - PRT( "Windowing ", p->timeWin ); - PRT( "Miter ", p->timeMiter ); - PRT( "Simulation ", p->timeSim ); - PRT( "Quantifying ", p->timeQuant ); - PRT( "Truth table ", p->timeTruth ); - PRT( "TOTAL ", p->timeTotal ); - PRT( "Aborted ", p->timeAbort ); - } - Vec_PtrFree( p->vRoots ); - Vec_PtrFree( p->vBranches ); - Vec_PtrFree( p->vTruths ); - Vec_PtrFree( p->vTruthsElem ); - Vec_IntFree( p->vUsedSpots ); - free( p->pObjs ); - free( p->pTable ); - free( p ); -} - - - -/**Function************************************************************* - - Synopsis [Marks the TFO of the collected nodes up to the given level.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkDontCareWinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNode ) -{ - Abc_Obj_t * pFanout; - int i; - if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit || pObj == pNode ) - return; - if ( Abc_NodeIsTravIdCurrent(pObj) ) - return; - Abc_NodeSetTravIdCurrent( pObj ); - //////////////////////////////////////// - // try to reduce the runtime - if ( Abc_ObjFanoutNum(pObj) > 100 ) - return; - //////////////////////////////////////// - Abc_ObjForEachFanout( pObj, pFanout, i ) - Abc_NtkDontCareWinSweepLeafTfo_rec( pFanout, nLevelLimit, pNode ); -} - -/**Function************************************************************* - - Synopsis [Marks the TFO of the collected nodes up to the given level.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkDontCareWinSweepLeafTfo( Odc_Man_t * p ) -{ - Abc_Obj_t * pObj; - int i; - Abc_NtkIncrementTravId( p->pNode->pNtk ); - Vec_PtrForEachEntry( p->vLeaves, pObj, i ) - Abc_NtkDontCareWinSweepLeafTfo_rec( pObj, p->pNode->Level + p->nLevels, p->pNode ); -} - -/**Function************************************************************* - - Synopsis [Recursively collects the roots.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkDontCareWinCollectRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots ) -{ - Abc_Obj_t * pFanout; - int i; - assert( Abc_ObjIsNode(pObj) ); - assert( Abc_NodeIsTravIdCurrent(pObj) ); - // check if the node has all fanouts marked - Abc_ObjForEachFanout( pObj, pFanout, i ) - if ( !Abc_NodeIsTravIdCurrent(pFanout) ) - break; - // if some of the fanouts are unmarked, add the node to the root - if ( i < Abc_ObjFanoutNum(pObj) ) - { - Vec_PtrPushUnique( vRoots, pObj ); - return; - } - // otherwise, call recursively - Abc_ObjForEachFanout( pObj, pFanout, i ) - Abc_NtkDontCareWinCollectRoots_rec( pFanout, vRoots ); -} - -/**Function************************************************************* - - Synopsis [Collects the roots of the window.] - - Description [Roots of the window are the nodes that have at least - one fanout that it not in the TFO of the leaves.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkDontCareWinCollectRoots( Odc_Man_t * p ) -{ - assert( !Abc_NodeIsTravIdCurrent(p->pNode) ); - // mark the node with the old traversal ID - Abc_NodeSetTravIdCurrent( p->pNode ); - // collect the roots - Vec_PtrClear( p->vRoots ); - Abc_NtkDontCareWinCollectRoots_rec( p->pNode, p->vRoots ); -} - -/**Function************************************************************* - - Synopsis [Recursively adds missing nodes and leaves.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkDontCareWinAddMissing_rec( Odc_Man_t * p, Abc_Obj_t * pObj ) -{ - Abc_Obj_t * pFanin; - int i; - // skip the already collected leaves and branches - if ( Abc_NodeIsTravIdCurrent(pObj) ) - return 1; - // if this is not an internal node - make it a new branch - if ( !Abc_NodeIsTravIdPrevious(pObj) || Abc_ObjIsCi(pObj) ) //|| (int)pObj->Level <= p->nLevLeaves ) - { - Abc_NodeSetTravIdCurrent( pObj ); - Vec_PtrPush( p->vBranches, pObj ); - return Vec_PtrSize(p->vBranches) <= 32; - } - // visit the fanins of the node - Abc_ObjForEachFanin( pObj, pFanin, i ) - if ( !Abc_NtkDontCareWinAddMissing_rec( p, pFanin ) ) - return 0; - return 1; -} - -/**Function************************************************************* - - Synopsis [Adds to the window nodes and leaves in the TFI of the roots.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkDontCareWinAddMissing( Odc_Man_t * p ) -{ - Abc_Obj_t * pObj; - int i; - // set the leaves - Abc_NtkIncrementTravId( p->pNode->pNtk ); - Vec_PtrForEachEntry( p->vLeaves, pObj, i ) - Abc_NodeSetTravIdCurrent( pObj ); - // explore from the roots - Vec_PtrClear( p->vBranches ); - Vec_PtrForEachEntry( p->vRoots, pObj, i ) - if ( !Abc_NtkDontCareWinAddMissing_rec( p, pObj ) ) - return 0; - return 1; -} - -/**Function************************************************************* - - Synopsis [Computes window for the node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkDontCareWindow( Odc_Man_t * p ) -{ - // mark the TFO of the collected nodes up to the given level (p->pNode->Level + p->nWinTfoMax) - Abc_NtkDontCareWinSweepLeafTfo( p ); - // find the roots of the window - Abc_NtkDontCareWinCollectRoots( p ); - if ( Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode ) - { -// printf( "Empty window\n" ); - return 0; - } - // add the nodes in the TFI of the roots that are not yet in the window - if ( !Abc_NtkDontCareWinAddMissing( p ) ) - { -// printf( "Too many branches (%d)\n", Vec_PtrSize(p->vBranches) ); - return 0; - } - return 1; -} - - - - - -/**Function************************************************************* - - Synopsis [Performing hashing of two AIG Literals.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline unsigned Odc_HashKey( Odc_Lit_t iFan0, Odc_Lit_t iFan1, int TableSize ) -{ - unsigned Key = 0; - Key ^= Odc_Regular(iFan0) * 7937; - Key ^= Odc_Regular(iFan1) * 2971; - Key ^= Odc_IsComplement(iFan0) * 911; - Key ^= Odc_IsComplement(iFan1) * 353; - return Key % TableSize; -} - -/**Function************************************************************* - - Synopsis [Checks if the given name node already exists in the table.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Odc_Lit_t * Odc_HashLookup( Odc_Man_t * p, Odc_Lit_t iFan0, Odc_Lit_t iFan1 ) -{ - Odc_Obj_t * pObj; - Odc_Lit_t * pEntry; - unsigned uHashKey; - assert( iFan0 < iFan1 ); - // get the hash key for this node - uHashKey = Odc_HashKey( iFan0, iFan1, p->nTableSize ); - // remember the spot in the hash table that will be used - if ( p->pTable[uHashKey] == 0 ) - Vec_IntPush( p->vUsedSpots, uHashKey ); - // find the entry - for ( pEntry = p->pTable + uHashKey; *pEntry; pEntry = &pObj->iNext ) - { - pObj = Odc_Lit2Obj( p, *pEntry ); - if ( pObj->iFan0 == iFan0 && pObj->iFan1 == iFan1 ) - return pEntry; - } - return pEntry; -} - -/**Function************************************************************* - - Synopsis [Finds node by structural hashing or creates a new node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Odc_Lit_t Odc_And( Odc_Man_t * p, Odc_Lit_t iFan0, Odc_Lit_t iFan1 ) -{ - Odc_Obj_t * pObj; - Odc_Lit_t * pEntry; - unsigned uMask0, uMask1; - int Temp; - // consider trivial cases - if ( iFan0 == iFan1 ) - return iFan0; - if ( iFan0 == Odc_Not(iFan1) ) - return Odc_Const0(); - if ( Odc_Regular(iFan0) == Odc_Const1() ) - return iFan0 == Odc_Const1() ? iFan1 : Odc_Const0(); - if ( Odc_Regular(iFan1) == Odc_Const1() ) - return iFan1 == Odc_Const1() ? iFan0 : Odc_Const0(); - // canonicize the fanin order - if ( iFan0 > iFan1 ) - Temp = iFan0, iFan0 = iFan1, iFan1 = Temp; - // check if a node with these fanins exists - pEntry = Odc_HashLookup( p, iFan0, iFan1 ); - if ( *pEntry ) - return *pEntry; - // create a new node - pObj = Odc_ObjNew( p ); - pObj->iFan0 = iFan0; - pObj->iFan1 = iFan1; - pObj->iNext = 0; - pObj->TravId = 0; - // set the mask - uMask0 = Odc_Lit2Obj(p, Odc_Regular(iFan0))->uMask; - uMask1 = Odc_Lit2Obj(p, Odc_Regular(iFan1))->uMask; - pObj->uMask = uMask0 | uMask1; - // add to the table - *pEntry = Odc_Obj2Lit( p, pObj ); - return *pEntry; -} - -/**Function************************************************************* - - Synopsis [Boolean OR.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Odc_Lit_t Odc_Or( Odc_Man_t * p, Odc_Lit_t iFan0, Odc_Lit_t iFan1 ) -{ - return Odc_Not( Odc_And(p, Odc_Not(iFan0), Odc_Not(iFan1)) ); -} - -/**Function************************************************************* - - Synopsis [Boolean XOR.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline Odc_Lit_t Odc_Xor( Odc_Man_t * p, Odc_Lit_t iFan0, Odc_Lit_t iFan1 ) -{ - return Odc_Or( p, Odc_And(p, iFan0, Odc_Not(iFan1)), Odc_And(p, Odc_Not(iFan0), iFan1) ); -} - - - - - -/**Function************************************************************* - - Synopsis [Transfers the window into the AIG package.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void * Abc_NtkDontCareTransfer_rec( Odc_Man_t * p, Abc_Obj_t * pNode, Abc_Obj_t * pPivot ) -{ - unsigned uData0, uData1; - Odc_Lit_t uLit0, uLit1, uRes0, uRes1; - assert( !Abc_ObjIsComplement(pNode) ); - // skip visited objects - if ( Abc_NodeIsTravIdCurrent(pNode) ) - return pNode->pCopy; - Abc_NodeSetTravIdCurrent(pNode); - assert( Abc_ObjIsNode(pNode) ); - // consider the case when the node is the pivot - if ( pNode == pPivot ) - return pNode->pCopy = (void *)((Odc_Const1() << 16) | Odc_Const0()); - // compute the cofactors - uData0 = (unsigned)Abc_NtkDontCareTransfer_rec( p, Abc_ObjFanin0(pNode), pPivot ); - uData1 = (unsigned)Abc_NtkDontCareTransfer_rec( p, Abc_ObjFanin1(pNode), pPivot ); - // find the 0-cofactor - uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 & 0xffff), Abc_ObjFaninC0(pNode) ); - uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 & 0xffff), Abc_ObjFaninC1(pNode) ); - uRes0 = Odc_And( p, uLit0, uLit1 ); - // find the 1-cofactor - uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 >> 16), Abc_ObjFaninC0(pNode) ); - uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 >> 16), Abc_ObjFaninC1(pNode) ); - uRes1 = Odc_And( p, uLit0, uLit1 ); - // find the result - return pNode->pCopy = (void *)((uRes1 << 16) | uRes0); -} - -/**Function************************************************************* - - Synopsis [Transfers the window into the AIG package.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkDontCareTransfer( Odc_Man_t * p ) -{ - Abc_Obj_t * pObj; - Odc_Lit_t uRes0, uRes1; - Odc_Lit_t uLit; - unsigned uData; - int i; - Abc_NtkIncrementTravId( p->pNode->pNtk ); - // set elementary variables at the leaves - Vec_PtrForEachEntry( p->vLeaves, pObj, i ) - { - uLit = Odc_Var( p, i ); - pObj->pCopy = (void *)((uLit << 16) | uLit); - Abc_NodeSetTravIdCurrent(pObj); - } - // set elementary variables at the branched - Vec_PtrForEachEntry( p->vBranches, pObj, i ) - { - uLit = Odc_Var( p, i+p->nVarsMax ); - pObj->pCopy = (void *)((uLit << 16) | uLit); - Abc_NodeSetTravIdCurrent(pObj); - } - // compute the AIG for the window - p->iRoot = Odc_Const0(); - Vec_PtrForEachEntry( p->vRoots, pObj, i ) - { - uData = (unsigned)Abc_NtkDontCareTransfer_rec( p, pObj, p->pNode ); - // get the cofactors - uRes0 = uData & 0xffff; - uRes1 = uData >> 16; - // compute the miter -// assert( uRes0 != uRes1 ); // may be false if the node is redundant w.r.t. this root - uLit = Odc_Xor( p, uRes0, uRes1 ); - p->iRoot = Odc_Or( p, p->iRoot, uLit ); - } - return 1; -} - - -/**Function************************************************************* - - Synopsis [Recursively computes the pair of cofactors.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -unsigned Abc_NtkDontCareCofactors_rec( Odc_Man_t * p, Odc_Lit_t Lit, unsigned uMask ) -{ - Odc_Obj_t * pObj; - unsigned uData0, uData1; - Odc_Lit_t uLit0, uLit1, uRes0, uRes1; - assert( !Odc_IsComplement(Lit) ); - // skip visited objects - pObj = Odc_Lit2Obj( p, Lit ); - if ( Odc_ObjIsTravIdCurrent(p, pObj) ) - return pObj->uData; - Odc_ObjSetTravIdCurrent(p, pObj); - // skip objects out of the cone - if ( (pObj->uMask & uMask) == 0 ) - return pObj->uData = ((Lit << 16) | Lit); - // consider the case when the node is the var - if ( pObj->uMask == uMask && Odc_IsTerm(p, Lit) ) - return pObj->uData = ((Odc_Const1() << 16) | Odc_Const0()); - // compute the cofactors - uData0 = Abc_NtkDontCareCofactors_rec( p, Odc_ObjFanin0(pObj), uMask ); - uData1 = Abc_NtkDontCareCofactors_rec( p, Odc_ObjFanin1(pObj), uMask ); - // find the 0-cofactor - uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 & 0xffff), Odc_ObjFaninC0(pObj) ); - uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 & 0xffff), Odc_ObjFaninC1(pObj) ); - uRes0 = Odc_And( p, uLit0, uLit1 ); - // find the 1-cofactor - uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 >> 16), Odc_ObjFaninC0(pObj) ); - uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 >> 16), Odc_ObjFaninC1(pObj) ); - uRes1 = Odc_And( p, uLit0, uLit1 ); - // find the result - return pObj->uData = ((uRes1 << 16) | uRes0); -} - -/**Function************************************************************* - - Synopsis [Quantifies the branch variables.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkDontCareQuantify( Odc_Man_t * p ) -{ - Odc_Lit_t uRes0, uRes1; - unsigned uData; - int i; - assert( p->iRoot < 0xffff ); - assert( Vec_PtrSize(p->vBranches) <= 32 ); // the mask size - for ( i = 0; i < Vec_PtrSize(p->vBranches); i++ ) - { - // compute the cofactors w.r.t. this variable - Odc_ManIncrementTravId( p ); - uData = Abc_NtkDontCareCofactors_rec( p, Odc_Regular(p->iRoot), (1 << i) ); - uRes0 = Odc_NotCond( (Odc_Lit_t)(uData & 0xffff), Odc_IsComplement(p->iRoot) ); - uRes1 = Odc_NotCond( (Odc_Lit_t)(uData >> 16), Odc_IsComplement(p->iRoot) ); - // quantify this variable existentially - p->iRoot = Odc_Or( p, uRes0, uRes1 ); - // check the limit - if ( Odc_ObjNum(p) > ABC_DC_MAX_NODES/2 ) - return 0; - } - assert( p->nObjs <= p->nObjsAlloc ); - return 1; -} - - - -/**Function************************************************************* - - Synopsis [Set elementary truth tables for PIs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkDontCareSimulateSetElem2( Odc_Man_t * p ) -{ - unsigned * pData; - int i, k; - for ( k = 0; k < p->nVarsMax; k++ ) - { - pData = Odc_ObjTruth( p, Odc_Var(p, k) ); - Abc_InfoClear( pData, p->nWords ); - for ( i = 0; i < p->nBits; i++ ) - if ( i & (1 << k) ) - pData[i>>5] |= (1 << (i&31)); - } -} - -/**Function************************************************************* - - Synopsis [Set elementary truth tables for PIs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkDontCareSimulateSetElem( Odc_Man_t * p ) -{ - unsigned * pData, * pData2; - int k; - for ( k = 0; k < p->nVarsMax; k++ ) - { - pData = Odc_ObjTruth( p, Odc_Var(p, k) ); - pData2 = Vec_PtrEntry( p->vTruthsElem, k ); - Abc_InfoCopy( pData, pData2, p->nWords ); - } -} - -/**Function************************************************************* - - Synopsis [Set random simulation words for PIs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkDontCareSimulateSetRand( Odc_Man_t * p ) -{ - unsigned * pData; - int w, k, Number; - for ( w = 0; w < p->nWords; w++ ) - { - Number = rand(); - for ( k = 0; k < p->nVarsMax; k++ ) - { - pData = Odc_ObjTruth( p, Odc_Var(p, k) ); - pData[w] = (Number & (1<<k)) ? ~0 : 0; - } - } -} - -/**Function************************************************************* - - Synopsis [Set random simulation words for PIs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkDontCareCountMintsWord( Odc_Man_t * p, unsigned * puTruth ) -{ - int w, Counter = 0; - for ( w = 0; w < p->nWords; w++ ) - if ( puTruth[w] ) - Counter++; - return Counter; -} - -/**Function************************************************************* - - Synopsis [Simulates one node.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkDontCareTruthOne( Odc_Man_t * p, Odc_Lit_t Lit ) -{ - Odc_Obj_t * pObj; - unsigned * pInfo, * pInfo1, * pInfo2; - int k, fComp1, fComp2; - assert( !Odc_IsComplement( Lit ) ); - assert( !Odc_IsTerm( p, Lit ) ); - // get the truth tables - pObj = Odc_Lit2Obj( p, Lit ); - pInfo = Odc_ObjTruth( p, Lit ); - pInfo1 = Odc_ObjTruth( p, Odc_ObjFanin0(pObj) ); - pInfo2 = Odc_ObjTruth( p, Odc_ObjFanin1(pObj) ); - fComp1 = Odc_ObjFaninC0( pObj ); - fComp2 = Odc_ObjFaninC1( pObj ); - // simulate - if ( fComp1 && fComp2 ) - for ( k = 0; k < p->nWords; k++ ) - pInfo[k] = ~pInfo1[k] & ~pInfo2[k]; - else if ( fComp1 && !fComp2 ) - for ( k = 0; k < p->nWords; k++ ) - pInfo[k] = ~pInfo1[k] & pInfo2[k]; - else if ( !fComp1 && fComp2 ) - for ( k = 0; k < p->nWords; k++ ) - pInfo[k] = pInfo1[k] & ~pInfo2[k]; - else // if ( fComp1 && fComp2 ) - for ( k = 0; k < p->nWords; k++ ) - pInfo[k] = pInfo1[k] & pInfo2[k]; -} - -/**Function************************************************************* - - Synopsis [Computes the truth table.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Abc_NtkDontCareSimulate_rec( Odc_Man_t * p, Odc_Lit_t Lit ) -{ - Odc_Obj_t * pObj; - assert( !Odc_IsComplement(Lit) ); - // skip terminals - if ( Odc_IsTerm(p, Lit) ) - return; - // skip visited objects - pObj = Odc_Lit2Obj( p, Lit ); - if ( Odc_ObjIsTravIdCurrent(p, pObj) ) - return; - Odc_ObjSetTravIdCurrent(p, pObj); - // call recursively - Abc_NtkDontCareSimulate_rec( p, Odc_ObjFanin0(pObj) ); - Abc_NtkDontCareSimulate_rec( p, Odc_ObjFanin1(pObj) ); - // construct the truth table - Abc_NtkDontCareTruthOne( p, Lit ); -} - -/**Function************************************************************* - - Synopsis [Computes the truth table of the care set.] - - Description [Returns the number of ones in the simulation info.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkDontCareSimulate( Odc_Man_t * p, unsigned * puTruth ) -{ - Odc_ManIncrementTravId( p ); - Abc_NtkDontCareSimulate_rec( p, Odc_Regular(p->iRoot) ); - Abc_InfoCopy( puTruth, Odc_ObjTruth(p, Odc_Regular(p->iRoot)), p->nWords ); - if ( Odc_IsComplement(p->iRoot) ) - Abc_InfoNot( puTruth, p->nWords ); - return Extra_TruthCountOnes( puTruth, p->nVarsMax ); -} - -/**Function************************************************************* - - Synopsis [Computes the truth table of the care set.] - - Description [Returns the number of ones in the simulation info.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkDontCareSimulateBefore( Odc_Man_t * p, unsigned * puTruth ) -{ - int nIters = 2; - int nRounds, Counter, r; - // decide how many rounds to simulate - nRounds = p->nBits / p->nWords; - Counter = 0; - for ( r = 0; r < nIters; r++ ) - { - Abc_NtkDontCareSimulateSetRand( p ); - Abc_NtkDontCareSimulate( p, puTruth ); - Counter += Abc_NtkDontCareCountMintsWord( p, puTruth ); - } - // normalize - Counter = Counter * nRounds / nIters; - return Counter; -} - -/**Function************************************************************* - - Synopsis [Computes ODCs for the node in terms of the cut variables.] - - Description [Returns the number of don't care minterms in the truth table. - In particular, this procedure returns 0 if there is no don't-cares.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Abc_NtkDontCareCompute( Odc_Man_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, unsigned * puTruth ) -{ - int nMints, RetValue; - int clk, clkTotal = clock(); - - p->nWins++; - - // set the parameters - assert( !Abc_ObjIsComplement(pNode) ); - assert( Abc_ObjIsNode(pNode) ); - assert( Vec_PtrSize(vLeaves) <= p->nVarsMax ); - p->vLeaves = vLeaves; - p->pNode = pNode; - - // compute the window -clk = clock(); - RetValue = Abc_NtkDontCareWindow( p ); -p->timeWin += clock() - clk; - if ( !RetValue ) - { -p->timeAbort += clock() - clkTotal; - Abc_InfoFill( puTruth, p->nWords ); - p->nWinsEmpty++; - return 0; - } - - if ( p->fVeryVerbose ) - { - printf( " %5d : ", pNode->Id ); - printf( "Leaf = %2d ", Vec_PtrSize(p->vLeaves) ); - printf( "Root = %2d ", Vec_PtrSize(p->vRoots) ); - printf( "Bran = %2d ", Vec_PtrSize(p->vBranches) ); - printf( " | " ); - } - - // transfer the window into the AIG package -clk = clock(); - Abc_NtkDontCareTransfer( p ); -p->timeMiter += clock() - clk; - - // simulate to estimate the amount of don't-cares -clk = clock(); - nMints = Abc_NtkDontCareSimulateBefore( p, puTruth ); -p->timeSim += clock() - clk; - if ( p->fVeryVerbose ) - { - printf( "AIG = %5d ", Odc_NodeNum(p) ); - printf( "%6.2f %% ", 100.0 * (p->nBits - nMints) / p->nBits ); - } - - // if there is less then the given percentage of don't-cares, skip - if ( 100.0 * (p->nBits - nMints) / p->nBits < 1.0 * p->nPercCutoff ) - { -p->timeAbort += clock() - clkTotal; - if ( p->fVeryVerbose ) - printf( "Simulation cutoff.\n" ); - Abc_InfoFill( puTruth, p->nWords ); - p->nSimsEmpty++; - return 0; - } - - // quantify external variables -clk = clock(); - RetValue = Abc_NtkDontCareQuantify( p ); -p->timeQuant += clock() - clk; - if ( !RetValue ) - { -p->timeAbort += clock() - clkTotal; - if ( p->fVeryVerbose ) - printf( "=== Overflow! ===\n" ); - Abc_InfoFill( puTruth, p->nWords ); - p->nQuantsOver++; - return 0; - } - - // get the truth table -clk = clock(); - Abc_NtkDontCareSimulateSetElem( p ); - nMints = Abc_NtkDontCareSimulate( p, puTruth ); -p->timeTruth += clock() - clk; - if ( p->fVeryVerbose ) - { - printf( "AIG = %5d ", Odc_NodeNum(p) ); - printf( "%6.2f %% ", 100.0 * (p->nBits - nMints) / p->nBits ); - printf( "\n" ); - } -p->timeTotal += clock() - clkTotal; - p->nWinsFinish++; - p->nTotalDcs += (int)(100.0 * (p->nBits - nMints) / p->nBits); - return nMints; -} - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - |