summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
-rw-r--r--abc.dsp8
-rw-r--r--src/base/abc/abc.h3
-rw-r--r--src/base/abc/abcUtil.c94
-rw-r--r--src/base/abci/abc.c39
-rw-r--r--src/base/abci/abcOdc.c1134
-rw-r--r--src/base/abci/abcPrint.c1
-rw-r--r--src/base/abci/abcResub.c220
-rw-r--r--src/base/abci/module.make1
-rw-r--r--src/opt/res/resCore.c10
-rw-r--r--src/opt/res/resDivs.c2
-rw-r--r--src/opt/res/resInt.h1
-rw-r--r--src/opt/res/resSim.c13
-rw-r--r--src/opt/res/resWin.c2
13 files changed, 1434 insertions, 94 deletions
diff --git a/abc.dsp b/abc.dsp
index 54bfa7b2..47e870d7 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -278,6 +278,10 @@ SOURCE=.\src\base\abci\abcNtbdd.c
# End Source File
# Begin Source File
+SOURCE=.\src\base\abci\abcOdc.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\base\abci\abcOrder.c
# End Source File
# Begin Source File
@@ -1670,6 +1674,10 @@ SOURCE=.\src\opt\res\resFilter.c
# End Source File
# Begin Source File
+SOURCE=.\src\opt\res\resInt.h
+# End Source File
+# Begin Source File
+
SOURCE=.\src\opt\res\resSat.c
# End Source File
# Begin Source File
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<<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 ///
+////////////////////////////////////////////////////////////////////////
+
+
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 );
-
}
@@ -591,36 +615,6 @@ void Abc_ManResubSimulate( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, in
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 []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
Dec_Graph_t * Abc_ManResubQuit0( Abc_Obj_t * pRoot, Abc_Obj_t * pObj )
{
Dec_Graph_t * pGraph;
@@ -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 );