From 12578e622f62bde4cfc1d3b055aa8747e5c9590b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 27 Jan 2007 08:01:00 -0800 Subject: Version abc70127 --- src/base/abc/abc.h | 3 +- src/base/abc/abcUtil.c | 94 ++++ src/base/abci/abc.c | 39 +- src/base/abci/abcOdc.c | 1134 +++++++++++++++++++++++++++++++++++++++++++++ src/base/abci/abcPrint.c | 1 + src/base/abci/abcResub.c | 220 +++++---- src/base/abci/module.make | 1 + src/opt/res/resCore.c | 10 +- src/opt/res/resDivs.c | 2 + src/opt/res/resInt.h | 1 + src/opt/res/resSim.c | 13 +- src/opt/res/resWin.c | 2 + 12 files changed, 1426 insertions(+), 94 deletions(-) create mode 100644 src/base/abci/abcOdc.c (limited to 'src') diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 39360034..ce1947a9 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -237,7 +237,8 @@ static inline int Abc_TruthWordNum( int nVars ) { return nV static inline int Abc_InfoHasBit( unsigned * p, int i ) { return (p[(i)>>5] & (1<<((i) & 31))) > 0; } static inline void Abc_InfoSetBit( unsigned * p, int i ) { p[(i)>>5] |= (1<<((i) & 31)); } static inline void Abc_InfoXorBit( unsigned * p, int i ) { p[(i)>>5] ^= (1<<((i) & 31)); } -static inline unsigned Abc_InfoRandom() { return ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand())); } // #define RAND_MAX 0x7fff +static inline unsigned Abc_InfoRandomWord() { return ((((unsigned)rand()) << 24) ^ (((unsigned)rand()) << 12) ^ ((unsigned)rand())); } // #define RAND_MAX 0x7fff +static inline void Abc_InfoRandom( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = Abc_InfoRandomWord(); } static inline void Abc_InfoClear( unsigned * p, int nWords ) { memset( p, 0, sizeof(unsigned) * nWords ); } static inline void Abc_InfoFill( unsigned * p, int nWords ) { memset( p, 0xff, sizeof(unsigned) * nWords );} static inline void Abc_InfoNot( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = ~p[i]; } diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index 8883869c..b86dc88f 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -1450,6 +1450,100 @@ void Abc_NtkTransferCopy( Abc_Ntk_t * pNtk ) pObj->pCopy = pObj->pCopy? Abc_ObjEquiv(pObj->pCopy) : NULL; } + +/**Function************************************************************* + + Synopsis [Increaments the cut counter.] + + Description [Returns 1 if it becomes equal to the ref counter.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_ObjCrossCutInc( Abc_Obj_t * pObj ) +{ + pObj->pCopy = (void *)(((int)pObj->pCopy)++); + return (int)pObj->pCopy == Abc_ObjFanoutNum(pObj); +} + +/**Function************************************************************* + + Synopsis [Computes cross-cut of the circuit.] + + Description [Returns 1 if it is the last visit to the node.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkCrossCut_rec( Abc_Obj_t * pObj, int * pnCutSize, int * pnCutSizeMax ) +{ + Abc_Obj_t * pFanin; + int i, nDecrem = 0; + int fReverse = 0; + if ( Abc_ObjIsCi(pObj) ) + return 0; + // if visited, increment visit counter + if ( Abc_NodeIsTravIdCurrent( pObj ) ) + return Abc_ObjCrossCutInc( pObj ); + Abc_NodeSetTravIdCurrent( pObj ); + // visit the fanins + if ( !Abc_ObjIsCi(pObj) ) + { + if ( fReverse ) + { + Abc_ObjForEachFanin( pObj, pFanin, i ) + { + pFanin = Abc_ObjFanin( pObj, Abc_ObjFaninNum(pObj) - 1 - i ); + nDecrem += Abc_NtkCrossCut_rec( pFanin, pnCutSize, pnCutSizeMax ); + } + } + else + { + Abc_ObjForEachFanin( pObj, pFanin, i ) + nDecrem += Abc_NtkCrossCut_rec( pFanin, pnCutSize, pnCutSizeMax ); + } + } + // count the node + (*pnCutSize)++; + if ( *pnCutSizeMax < *pnCutSize ) + *pnCutSizeMax = *pnCutSize; + (*pnCutSize) -= nDecrem; + return Abc_ObjCrossCutInc( pObj ); +} + +/**Function************************************************************* + + Synopsis [Computes cross-cut of the circuit.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkCrossCut( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; + int nCutSize = 0, nCutSizeMax = 0; + int i; + Abc_NtkCleanCopy( pNtk ); + Abc_NtkIncrementTravId( pNtk ); + Abc_NtkForEachCo( pNtk, pObj, i ) + { + Abc_NtkCrossCut_rec( pObj, &nCutSize, &nCutSizeMax ); + nCutSize--; + } + assert( nCutSize == 0 ); + printf( "Max cross cut size = %6d. Ratio = %6.2f %%\n", nCutSizeMax, 100.0 * nCutSizeMax/Abc_NtkObjNum(pNtk) ); + return nCutSizeMax; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b20d2c8c..c2a6214d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -2999,23 +2999,27 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; int nCutsMax; int nNodesMax; + int nLevelsOdc; bool fUpdateLevel; bool fUseZeros; bool fVerbose; - extern int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutsMax, int nNodesMax, bool fUpdateLevel, bool fVerbose ); + bool fVeryVerbose; + extern int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutsMax, int nNodesMax, int nLevelsOdc, bool fUpdateLevel, bool fVerbose, bool fVeryVerbose ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); pErr = Abc_FrameReadErr(pAbc); // set defaults - nCutsMax = 8; + nCutsMax = 8; nNodesMax = 1; + nLevelsOdc = 0; fUpdateLevel = 1; fUseZeros = 0; fVerbose = 0; + fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KNlzvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KNFlzvwh" ) ) != EOF ) { switch ( c ) { @@ -3041,6 +3045,17 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nNodesMax < 0 ) goto usage; break; + case 'F': + if ( globalUtilOptind >= argc ) + { + fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" ); + goto usage; + } + nLevelsOdc = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLevelsOdc < 0 ) + goto usage; + break; case 'l': fUpdateLevel ^= 1; break; @@ -3050,6 +3065,9 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'v': fVerbose ^= 1; break; + case 'w': + fVeryVerbose ^= 1; + break; case 'h': goto usage; default: @@ -3064,7 +3082,12 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( nCutsMax < RS_CUT_MIN || nCutsMax > RS_CUT_MAX ) { - fprintf( pErr, "Can only compute the cuts for %d <= K <= %d.\n", RS_CUT_MIN, RS_CUT_MAX ); + fprintf( pErr, "Can only compute cuts for %d <= K <= %d.\n", RS_CUT_MIN, RS_CUT_MAX ); + return 1; + } + if ( nNodesMax < 0 || nNodesMax > 3 ) + { + fprintf( pErr, "Can only resubstitute at most 3 nodes.\n" ); return 1; } if ( !Abc_NtkIsStrash(pNtk) ) @@ -3079,7 +3102,7 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv ) } // modify the current network - if ( !Abc_NtkResubstitute( pNtk, nCutsMax, nNodesMax, fUpdateLevel, fVerbose ) ) + if ( !Abc_NtkResubstitute( pNtk, nCutsMax, nNodesMax, nLevelsOdc, fUpdateLevel, fVerbose, fVeryVerbose ) ) { fprintf( pErr, "Refactoring has failed.\n" ); return 1; @@ -3087,13 +3110,15 @@ int Abc_CommandResubstitute( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - fprintf( pErr, "usage: resub [-K num] [-N num] [-lzvh]\n" ); + fprintf( pErr, "usage: resub [-K num] [-N num] [-F num] [-lzvwh]\n" ); fprintf( pErr, "\t performs technology-independent restructuring of the AIG\n" ); fprintf( pErr, "\t-K num : the max cut size (%d <= num <= %d) [default = %d]\n", RS_CUT_MIN, RS_CUT_MAX, nCutsMax ); - fprintf( pErr, "\t-N num : the max number of nodes to add [default = %d]\n", nNodesMax ); + fprintf( pErr, "\t-N num : the max number of nodes to add (0 <= num <= 3) [default = %d]\n", nNodesMax ); + fprintf( pErr, "\t-F num : the number of fanout levels for ODC computation [default = %d]\n", nLevelsOdc ); fprintf( pErr, "\t-l : toggle preserving the number of levels [default = %s]\n", fUpdateLevel? "yes": "no" ); fprintf( pErr, "\t-z : toggle using zero-cost replacements [default = %s]\n", fUseZeros? "yes": "no" ); fprintf( pErr, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + fprintf( pErr, "\t-w : toggle verbose printout of ODC computation [default = %s]\n", fVeryVerbose? "yes": "no" ); fprintf( pErr, "\t-h : print the command usage\n"); return 1; } diff --git a/src/base/abci/abcOdc.c b/src/base/abci/abcOdc.c new file mode 100644 index 00000000..42b8826c --- /dev/null +++ b/src/base/abci/abcOdc.c @@ -0,0 +1,1134 @@ +/**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<<14) + +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<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 /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c index e162ada4..e66ce018 100644 --- a/src/base/abci/abcPrint.c +++ b/src/base/abci/abcPrint.c @@ -111,6 +111,7 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored ) fprintf( pFile, "\n" ); +// Abc_NtkCrossCut( pNtk ); // print the statistic into a file /* diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c index 19e6c50a..1938db7c 100644 --- a/src/base/abci/abcResub.c +++ b/src/base/abci/abcResub.c @@ -46,6 +46,8 @@ struct Abc_ManRes_t_ int nWords; // the number of unsigneds for siminfo Vec_Ptr_t * vSims; // simulation info unsigned * pInfo; // pointer to simulation info + // observability don't-cares + unsigned * pCareSet; // internal divisor storage Vec_Ptr_t * vDivs1UP; // the single-node unate divisors Vec_Ptr_t * vDivs1UN; // the single-node unate divisors @@ -58,6 +60,7 @@ struct Abc_ManRes_t_ Vec_Ptr_t * vTemp; // temporary array of nodes // runtime statistics int timeCut; + int timeTruth; int timeRes; int timeDiv; int timeMffc; @@ -109,6 +112,13 @@ static Dec_Graph_t * Abc_ManResubDivs3( Abc_ManRes_t * p, int Required ); static Vec_Ptr_t * Abc_CutFactorLarge( Abc_Obj_t * pNode, int nLeavesMax ); static int Abc_CutVolumeCheck( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves ); +// don't-care manager +extern void * Abc_NtkDontCareAlloc( int nVarsMax, int nLevels, int fVerbose, int fVeryVerbose ); +extern void Abc_NtkDontCareClear( void * p ); +extern void Abc_NtkDontCareFree( void * p ); +extern int Abc_NtkDontCareCompute( void * p, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, unsigned * puTruth ); + + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -124,11 +134,12 @@ static int Abc_CutVolumeCheck( Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves SeeAlso [] ***********************************************************************/ -int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, bool fUpdateLevel, bool fVerbose ) +int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, int nLevelsOdc, bool fUpdateLevel, bool fVerbose, bool fVeryVerbose ) { ProgressBar * pProgress; Abc_ManRes_t * pManRes; Abc_ManCut_t * pManCut; + void * pManOdc = NULL; Dec_Graph_t * pFForm; Vec_Ptr_t * vLeaves; Abc_Obj_t * pNode; @@ -142,6 +153,8 @@ int Abc_NtkResubstitute( Abc_Ntk_t * pNtk, int nCutMax, int nStepsMax, bool fUpd // start the managers pManCut = Abc_NtkManCutStart( nCutMax, 100000, 100000, 100000 ); pManRes = Abc_ManResubStart( nCutMax, ABC_RS_DIV1_MAX ); + if ( nLevelsOdc > 0 ) + pManOdc = Abc_NtkDontCareAlloc( nCutMax, nLevelsOdc, fVerbose, fVeryVerbose ); // compute the reverse levels if level update is requested if ( fUpdateLevel ) @@ -181,6 +194,14 @@ pManRes->timeCut += clock() - clk; if ( vLeaves == NULL ) continue; */ + // get the don't-cares + if ( pManOdc ) + { +clk = clock(); + Abc_NtkDontCareClear( pManOdc ); + Abc_NtkDontCareCompute( pManOdc, pNode, vLeaves, pManRes->pCareSet ); +pManRes->timeTruth += clock() - clk; + } // evaluate this cut clk = clock(); @@ -216,6 +237,7 @@ pManRes->timeTotal = clock() - clkStart; // delete the managers Abc_ManResubStop( pManRes ); Abc_NtkManCutStop( pManCut ); + if ( pManOdc ) Abc_NtkDontCareFree( pManOdc ); // clean the data field Abc_NtkForEachObj( pNtk, pNode, i ) @@ -270,11 +292,14 @@ Abc_ManRes_t * Abc_ManResubStart( int nLeavesMax, int nDivsMax ) // allocate simulation info p->nBits = (1 << p->nLeavesMax); p->nWords = (p->nBits <= 32)? 1 : (p->nBits / 32); - p->pInfo = ALLOC( unsigned, p->nWords * p->nDivsMax ); + p->pInfo = ALLOC( unsigned, p->nWords * (p->nDivsMax + 1) ); memset( p->pInfo, 0, sizeof(unsigned) * p->nWords * p->nLeavesMax ); p->vSims = Vec_PtrAlloc( p->nDivsMax ); for ( i = 0; i < p->nDivsMax; i++ ) Vec_PtrPush( p->vSims, p->pInfo + i * p->nWords ); + // assign the care set + p->pCareSet = p->pInfo + p->nDivsMax * p->nWords; + Abc_InfoFill( p->pCareSet, p->nWords ); // set elementary truth tables for ( k = 0; k < p->nLeavesMax; k++ ) { @@ -343,7 +368,7 @@ void Abc_ManResubPrint( Abc_ManRes_t * p ) printf( "Used double ANDs = %6d. ", p->nUsedNode2And ); PRT( " 1 ", p->timeRes1 ); printf( "Used OR-AND = %6d. ", p->nUsedNode2OrAnd ); PRT( " D ", p->timeResD ); printf( "Used AND-OR = %6d. ", p->nUsedNode2AndOr ); PRT( " 2 ", p->timeRes2 ); - printf( "Used OR-2ANDs = %6d. ", p->nUsedNode3OrAnd ); PRT( " 3 ", p->timeRes3 ); + printf( "Used OR-2ANDs = %6d. ", p->nUsedNode3OrAnd ); PRT( "Truth ", p->timeTruth ); //PRT( " 3 ", p->timeRes3 ); printf( "Used AND-2ORs = %6d. ", p->nUsedNode3AndOr ); PRT( "AIG ", p->timeNtk ); printf( "TOTAL = %6d. ", p->nUsedNodeC + p->nUsedNode0 + @@ -359,7 +384,6 @@ void Abc_ManResubPrint( Abc_ManRes_t * p ) printf( "Total leaves = %8d.\n", p->nTotalLeaves ); printf( "Total divisors = %8d.\n", p->nTotalDivs ); printf( "Total gain = %8d.\n", p->nTotalGain ); - } @@ -580,36 +604,6 @@ void Abc_ManResubSimulate( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, in } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Dec_Graph_t * Abc_ManResubQuit( Abc_ManRes_t * p ) -{ - Dec_Graph_t * pGraph; - unsigned * upData; - int w; - upData = p->pRoot->pData; - for ( w = 0; w < p->nWords; w++ ) - if ( upData[w] ) - break; - if ( w != p->nWords ) - return NULL; - // get constant node graph - if ( p->pRoot->fPhase ) - pGraph = Dec_GraphCreateConst1(); - else - pGraph = Dec_GraphCreateConst0(); - return pGraph; -} - /**Function************************************************************* Synopsis [] @@ -854,7 +848,8 @@ void Abc_ManResubDivsS( Abc_ManRes_t * p, int Required ) puData = pObj->pData; // check positive containment for ( w = 0; w < p->nWords; w++ ) - if ( puData[w] & ~puDataR[w] ) +// if ( puData[w] & ~puDataR[w] ) + if ( puData[w] & ~puDataR[w] & p->pCareSet[w] ) // care set break; if ( w == p->nWords ) { @@ -863,7 +858,8 @@ void Abc_ManResubDivsS( Abc_ManRes_t * p, int Required ) } // check negative containment for ( w = 0; w < p->nWords; w++ ) - if ( ~puData[w] & puDataR[w] ) +// if ( ~puData[w] & puDataR[w] ) + if ( ~puData[w] & puDataR[w] & p->pCareSet[w] ) // care set break; if ( w == p->nWords ) { @@ -913,7 +909,8 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required ) { // get positive unate divisors for ( w = 0; w < p->nWords; w++ ) - if ( (puData0[w] & puData1[w]) & ~puDataR[w] ) +// if ( (puData0[w] & puData1[w]) & ~puDataR[w] ) + if ( (puData0[w] & puData1[w]) & ~puDataR[w] & p->pCareSet[w] ) // care set break; if ( w == p->nWords ) { @@ -921,7 +918,8 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required ) Vec_PtrPush( p->vDivs2UP1, pObj1 ); } for ( w = 0; w < p->nWords; w++ ) - if ( (~puData0[w] & puData1[w]) & ~puDataR[w] ) +// if ( (~puData0[w] & puData1[w]) & ~puDataR[w] ) + if ( (~puData0[w] & puData1[w]) & ~puDataR[w] & p->pCareSet[w] ) // care set break; if ( w == p->nWords ) { @@ -929,7 +927,8 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required ) Vec_PtrPush( p->vDivs2UP1, pObj1 ); } for ( w = 0; w < p->nWords; w++ ) - if ( (puData0[w] & ~puData1[w]) & ~puDataR[w] ) +// if ( (puData0[w] & ~puData1[w]) & ~puDataR[w] ) + if ( (puData0[w] & ~puData1[w]) & ~puDataR[w] & p->pCareSet[w] ) // care set break; if ( w == p->nWords ) { @@ -937,7 +936,8 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required ) Vec_PtrPush( p->vDivs2UP1, Abc_ObjNot(pObj1) ); } for ( w = 0; w < p->nWords; w++ ) - if ( (puData0[w] | puData1[w]) & ~puDataR[w] ) +// if ( (puData0[w] | puData1[w]) & ~puDataR[w] ) + if ( (puData0[w] | puData1[w]) & ~puDataR[w] & p->pCareSet[w] ) // care set break; if ( w == p->nWords ) { @@ -950,7 +950,8 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required ) { // get negative unate divisors for ( w = 0; w < p->nWords; w++ ) - if ( ~(puData0[w] & puData1[w]) & puDataR[w] ) +// if ( ~(puData0[w] & puData1[w]) & puDataR[w] ) + if ( ~(puData0[w] & puData1[w]) & puDataR[w] & p->pCareSet[w] ) // care set break; if ( w == p->nWords ) { @@ -958,7 +959,8 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required ) Vec_PtrPush( p->vDivs2UN1, pObj1 ); } for ( w = 0; w < p->nWords; w++ ) - if ( ~(~puData0[w] & puData1[w]) & puDataR[w] ) +// if ( ~(~puData0[w] & puData1[w]) & puDataR[w] ) + if ( ~(~puData0[w] & puData1[w]) & puDataR[w] & p->pCareSet[w] ) // care set break; if ( w == p->nWords ) { @@ -966,7 +968,8 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required ) Vec_PtrPush( p->vDivs2UN1, pObj1 ); } for ( w = 0; w < p->nWords; w++ ) - if ( ~(puData0[w] & ~puData1[w]) & puDataR[w] ) +// if ( ~(puData0[w] & ~puData1[w]) & puDataR[w] ) + if ( ~(puData0[w] & ~puData1[w]) & puDataR[w] & p->pCareSet[w] ) // care set break; if ( w == p->nWords ) { @@ -974,7 +977,8 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required ) Vec_PtrPush( p->vDivs2UN1, Abc_ObjNot(pObj1) ); } for ( w = 0; w < p->nWords; w++ ) - if ( ~(puData0[w] | puData1[w]) & puDataR[w] ) +// if ( ~(puData0[w] | puData1[w]) & puDataR[w] ) + if ( ~(puData0[w] | puData1[w]) & puDataR[w] & p->pCareSet[w] ) // care set break; if ( w == p->nWords ) { @@ -991,7 +995,38 @@ void Abc_ManResubDivsD( Abc_ManRes_t * p, int Required ) /**Function************************************************************* - Synopsis [Derives unate/binate divisors.] + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Dec_Graph_t * Abc_ManResubQuit( Abc_ManRes_t * p ) +{ + Dec_Graph_t * pGraph; + unsigned * upData; + int w; + upData = p->pRoot->pData; + for ( w = 0; w < p->nWords; w++ ) +// if ( upData[w] ) + if ( upData[w] & p->pCareSet[w] ) // care set + break; + if ( w != p->nWords ) + return NULL; + // get constant node graph + if ( p->pRoot->fPhase ) + pGraph = Dec_GraphCreateConst1(); + else + pGraph = Dec_GraphCreateConst0(); + return pGraph; +} + +/**Function************************************************************* + + Synopsis [] Description [] @@ -1010,7 +1045,8 @@ Dec_Graph_t * Abc_ManResubDivs0( Abc_ManRes_t * p ) { puData = pObj->pData; for ( w = 0; w < p->nWords; w++ ) - if ( puData[w] != puDataR[w] ) +// if ( puData[w] != puDataR[w] ) + if ( (puData[w] ^ puDataR[w]) & p->pCareSet[w] ) // care set break; if ( w == p->nWords ) return Abc_ManResubQuit0( p->pRoot, pObj ); @@ -1020,7 +1056,7 @@ Dec_Graph_t * Abc_ManResubDivs0( Abc_ManRes_t * p ) /**Function************************************************************* - Synopsis [Derives unate/binate divisors.] + Synopsis [] Description [] @@ -1043,7 +1079,8 @@ Dec_Graph_t * Abc_ManResubDivs1( Abc_ManRes_t * p, int Required ) { puData1 = pObj1->pData; for ( w = 0; w < p->nWords; w++ ) - if ( (puData0[w] | puData1[w]) != puDataR[w] ) +// if ( (puData0[w] | puData1[w]) != puDataR[w] ) + if ( ((puData0[w] | puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; if ( w == p->nWords ) { @@ -1060,7 +1097,8 @@ Dec_Graph_t * Abc_ManResubDivs1( Abc_ManRes_t * p, int Required ) { puData1 = pObj1->pData; for ( w = 0; w < p->nWords; w++ ) - if ( (puData0[w] & puData1[w]) != puDataR[w] ) +// if ( (puData0[w] & puData1[w]) != puDataR[w] ) + if ( ((puData0[w] & puData1[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; if ( w == p->nWords ) { @@ -1074,7 +1112,7 @@ Dec_Graph_t * Abc_ManResubDivs1( Abc_ManRes_t * p, int Required ) /**Function************************************************************* - Synopsis [Derives unate/binate divisors.] + Synopsis [] Description [] @@ -1100,7 +1138,8 @@ Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required ) { puData2 = pObj2->pData; for ( w = 0; w < p->nWords; w++ ) - if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) +// if ( (puData0[w] | puData1[w] | puData2[w]) != puDataR[w] ) + if ( ((puData0[w] | puData1[w] | puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; if ( w == p->nWords ) { @@ -1138,7 +1177,8 @@ Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required ) { puData2 = pObj2->pData; for ( w = 0; w < p->nWords; w++ ) - if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) +// if ( (puData0[w] & puData1[w] & puData2[w]) != puDataR[w] ) + if ( ((puData0[w] & puData1[w] & puData2[w]) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; if ( w == p->nWords ) { @@ -1170,7 +1210,7 @@ Dec_Graph_t * Abc_ManResubDivs12( Abc_ManRes_t * p, int Required ) /**Function************************************************************* - Synopsis [Derives unate/binate divisors.] + Synopsis [] Description [] @@ -1198,25 +1238,29 @@ Dec_Graph_t * Abc_ManResubDivs2( Abc_ManRes_t * p, int Required ) if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) { for ( w = 0; w < p->nWords; w++ ) - if ( (puData0[w] | (puData1[w] | puData2[w])) != puDataR[w] ) +// if ( (puData0[w] | (puData1[w] | puData2[w])) != puDataR[w] ) + if ( ((puData0[w] | (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; } else if ( Abc_ObjIsComplement(pObj1) ) { for ( w = 0; w < p->nWords; w++ ) - if ( (puData0[w] | (~puData1[w] & puData2[w])) != puDataR[w] ) +// if ( (puData0[w] | (~puData1[w] & puData2[w])) != puDataR[w] ) + if ( ((puData0[w] | (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; } else if ( Abc_ObjIsComplement(pObj2) ) { for ( w = 0; w < p->nWords; w++ ) - if ( (puData0[w] | (puData1[w] & ~puData2[w])) != puDataR[w] ) +// if ( (puData0[w] | (puData1[w] & ~puData2[w])) != puDataR[w] ) + if ( ((puData0[w] | (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; } else { for ( w = 0; w < p->nWords; w++ ) - if ( (puData0[w] | (puData1[w] & puData2[w])) != puDataR[w] ) +// if ( (puData0[w] | (puData1[w] & puData2[w])) != puDataR[w] ) + if ( ((puData0[w] | (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; } if ( w == p->nWords ) @@ -1239,25 +1283,29 @@ Dec_Graph_t * Abc_ManResubDivs2( Abc_ManRes_t * p, int Required ) if ( Abc_ObjIsComplement(pObj1) && Abc_ObjIsComplement(pObj2) ) { for ( w = 0; w < p->nWords; w++ ) - if ( (puData0[w] & (puData1[w] | puData2[w])) != puDataR[w] ) +// if ( (puData0[w] & (puData1[w] | puData2[w])) != puDataR[w] ) + if ( ((puData0[w] & (puData1[w] | puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; } else if ( Abc_ObjIsComplement(pObj1) ) { for ( w = 0; w < p->nWords; w++ ) - if ( (puData0[w] & (~puData1[w] & puData2[w])) != puDataR[w] ) +// if ( (puData0[w] & (~puData1[w] & puData2[w])) != puDataR[w] ) + if ( ((puData0[w] & (~puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; } else if ( Abc_ObjIsComplement(pObj2) ) { for ( w = 0; w < p->nWords; w++ ) - if ( (puData0[w] & (puData1[w] & ~puData2[w])) != puDataR[w] ) +// if ( (puData0[w] & (puData1[w] & ~puData2[w])) != puDataR[w] ) + if ( ((puData0[w] & (puData1[w] & ~puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; } else { for ( w = 0; w < p->nWords; w++ ) - if ( (puData0[w] & (puData1[w] & puData2[w])) != puDataR[w] ) +// if ( (puData0[w] & (puData1[w] & puData2[w])) != puDataR[w] ) + if ( ((puData0[w] & (puData1[w] & puData2[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; } if ( w == p->nWords ) @@ -1272,7 +1320,7 @@ Dec_Graph_t * Abc_ManResubDivs2( Abc_ManRes_t * p, int Required ) /**Function************************************************************* - Synopsis [Derives unate/binate divisors.] + Synopsis [] Description [] @@ -1307,85 +1355,101 @@ Dec_Graph_t * Abc_ManResubDivs3( Abc_ManRes_t * p, int Required ) { case 0: // 0000 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] ) +// if ( ((puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; break; case 1: // 0001 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] ) +// if ( ((puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; break; case 2: // 0010 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] ) +// if ( ((puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; break; case 3: // 0011 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] ) +// if ( ((puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; break; case 4: // 0100 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & ~puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] ) +// if ( ((puData0[w] & ~puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & ~puData1[w]) | (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; break; case 5: // 0101 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & ~puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] ) +// if ( ((puData0[w] & ~puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & ~puData1[w]) | (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; break; case 6: // 0110 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & ~puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] ) +// if ( ((puData0[w] & ~puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & ~puData1[w]) | (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; break; case 7: // 0111 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] & ~puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] ) +// if ( ((puData0[w] & ~puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] ) + if ( (((puData0[w] & ~puData1[w]) | (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; break; case 8: // 1000 for ( w = 0; w < p->nWords; w++ ) - if ( ((~puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] ) +// if ( ((~puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((~puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; break; case 9: // 1001 for ( w = 0; w < p->nWords; w++ ) - if ( ((~puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] ) +// if ( ((~puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] ) + if ( (((~puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; break; case 10: // 1010 for ( w = 0; w < p->nWords; w++ ) - if ( ((~puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] ) +// if ( ((~puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((~puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; break; case 11: // 1011 for ( w = 0; w < p->nWords; w++ ) - if ( ((~puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] ) +// if ( ((~puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] ) + if ( (((~puData0[w] & puData1[w]) | (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; break; case 12: // 1100 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] | puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] ) +// if ( ((puData0[w] | puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((puData0[w] | puData1[w]) | (puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) // care set break; break; case 13: // 1101 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] | puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] ) +// if ( ((puData0[w] | puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] ) + if ( (((puData0[w] | puData1[w]) | (puData2[w] & ~puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 14: // 1110 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] | puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] ) +// if ( ((puData0[w] | puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] ) + if ( (((puData0[w] | puData1[w]) | (~puData2[w] & puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; case 15: // 1111 for ( w = 0; w < p->nWords; w++ ) - if ( ((puData0[w] | puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] ) +// if ( ((puData0[w] | puData1[w]) | (puData2[w] | puData3[w])) != puDataR[w] ) + if ( (((puData0[w] | puData1[w]) | (puData2[w] | puData3[w])) ^ puDataR[w]) & p->pCareSet[w] ) break; break; diff --git a/src/base/abci/module.make b/src/base/abci/module.make index 169ab577..97f42f0e 100644 --- a/src/base/abci/module.make +++ b/src/base/abci/module.make @@ -24,6 +24,7 @@ SRC += src/base/abci/abc.c \ src/base/abci/abcMiter.c \ src/base/abci/abcMulti.c \ src/base/abci/abcNtbdd.c \ + src/base/abci/abcOdc.c \ src/base/abci/abcOrder.c \ src/base/abci/abcPrint.c \ src/base/abci/abcProve.c \ diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c index 6340b175..5f814c3a 100644 --- a/src/opt/res/resCore.c +++ b/src/opt/res/resCore.c @@ -200,8 +200,11 @@ p->timeAig += clock() - clk; if ( p->pPars->fVeryVerbose ) { - printf( "%5d : ", pObj->Id ); - printf( "Win = %3d/%4d/%3d ", Vec_PtrSize(p->pWin->vLeaves), Vec_VecSizeSize(p->pWin->vLevels), Vec_PtrSize(p->pWin->vRoots) ); + printf( "%5d (lev=%2d) : ", pObj->Id, pObj->Level ); + printf( "Win = %3d/%3d/%4d/%3d ", + Vec_PtrSize(p->pWin->vLeaves) - p->pWin->nLeavesPlus, + p->pWin->nLeavesPlus, Vec_VecSizeSize(p->pWin->vLevels), + Vec_PtrSize(p->pWin->vRoots) ); printf( "D = %3d ", Vec_PtrSize(p->pWin->vDivs) ); printf( "D+ = %3d ", p->pWin->nDivsPlus ); printf( "AIG = %4d ", Abc_NtkNodeNum(p->pAig) ); @@ -242,12 +245,13 @@ p->timeSat += clock() - clk; // printf( " Sat\n" ); continue; } + p->nProvedSets++; // printf( " Unsat\n" ); + continue; // write it into a file // Sto_ManDumpClauses( p->pCnf, "trace.cnf" ); - p->nProvedSets++; // interplate the problem if it was UNSAT clk = clock(); diff --git a/src/opt/res/resDivs.c b/src/opt/res/resDivs.c index a18764ed..bff91983 100644 --- a/src/opt/res/resDivs.c +++ b/src/opt/res/resDivs.c @@ -60,6 +60,8 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax ) // mark the MFFC of the node (does not increment trav ID) Res_WinVisitMffc( p ); + // what about the fanouts of the leaves!!! + // go through all the legal levels and check if their fanouts can be divisors p->nDivsPlus = 0; Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevDivMax - 1 ) diff --git a/src/opt/res/resInt.h b/src/opt/res/resInt.h index f5c64f8e..54251722 100644 --- a/src/opt/res/resInt.h +++ b/src/opt/res/resInt.h @@ -48,6 +48,7 @@ struct Res_Win_t_ int nLevLeaves; // the level where leaves begin int nLevDivMax; // the maximum divisor level int nDivsPlus; // the number of additional divisors + int nLeavesPlus;// the number of additional leaves Abc_Obj_t * pNode; // the node in the center // the window data Vec_Vec_t * vLevels; // nodes by level diff --git a/src/opt/res/resSim.c b/src/opt/res/resSim.c index 27a6c1f0..81267540 100644 --- a/src/opt/res/resSim.c +++ b/src/opt/res/resSim.c @@ -141,12 +141,11 @@ void Res_SimSetRandom( Res_Sim_t * p ) { Abc_Obj_t * pObj; unsigned * pInfo; - int i, w; + int i; Abc_NtkForEachPi( p->pAig, pObj, i ) { pInfo = Vec_PtrEntry( p->vPats, pObj->Id ); - for ( w = 0; w < p->nWords; w++ ) - pInfo[w] = Abc_InfoRandom(); + Abc_InfoRandom( pInfo, p->nWords ); } } @@ -478,7 +477,7 @@ int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig ) // prepare the manager Res_SimAdjust( p, pAig ); // collect 0/1 simulation info - for ( Limit = 0; Limit < 100; Limit++ ) + for ( Limit = 0; Limit < 10; Limit++ ) { Res_SimSetRandom( p ); Res_SimPerformRound( p ); @@ -489,10 +488,14 @@ int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig ) } // printf( "%d ", Limit ); // report the last set of patterns -// Res_SimReportOne( p ); + Res_SimReportOne( p ); + printf( "\n" ); // quit if there is not enough if ( p->nPats0 < 4 || p->nPats1 < 4 ) + { +// Res_SimReportOne( p ); return 0; + } // create bit-matrix info if ( p->nPats0 < p->nPats ) Res_SimPadSimInfo( p->vPats0, p->nPats0, p->nWords ); diff --git a/src/opt/res/resWin.c b/src/opt/res/resWin.c index b5fe0641..fa74b219 100644 --- a/src/opt/res/resWin.c +++ b/src/opt/res/resWin.c @@ -243,6 +243,7 @@ void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj ) return; if ( !Abc_NodeIsTravIdCurrent(pObj) || (int)pObj->Level <= p->nLevLeaves ) { + p->nLeavesPlus++; Vec_PtrPush( p->vLeaves, pObj ); pObj->fMarkA = 1; return; @@ -349,6 +350,7 @@ int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t p->pNode = pNode; p->nWinTfiMax = nWinTfiMax; p->nWinTfoMax = nWinTfoMax; + p->nLeavesPlus = 0; p->nLevLeaves = ABC_MAX( 0, ((int)p->pNode->Level) - p->nWinTfiMax - 1 ); // collect the nodes in TFI cone of pNode above the level of leaves (p->nLevLeaves) Res_WinCollectNodeTfi( p ); -- cgit v1.2.3