summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abci/abc.c4
-rw-r--r--src/base/abci/abcDec.c9
-rw-r--r--src/map/if/if.h10
-rw-r--r--src/map/if/ifDsd.c255
-rw-r--r--src/map/if/ifMan.c12
-rw-r--r--src/map/if/ifMap.c22
-rw-r--r--src/opt/dau/dau.h5
-rw-r--r--src/opt/dau/dauNonDsd.c29
8 files changed, 295 insertions, 51 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b170bfc4..6db36aa0 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2201,7 +2201,7 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
extern void Kit_DsdTest( unsigned * pTruth, int nVars );
extern void Kit_DsdPrintCofactors( unsigned * pTruth, int nVars, int nCofLevel, int fVerbose );
- extern void Dau_DecTrySets( word * p, int nVars );
+ extern void Dau_DecTrySets( word * p, int nVars, int fVerbose );
// set defaults
nCofLevel = 1;
@@ -2274,7 +2274,7 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
// Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) );
// Abc_Print( -1, "\n" );
if ( fPrintDec )//&&Abc_ObjFaninNum(pObj) <= 6 )
- Dau_DecTrySets( (word *)pTruth, Abc_ObjFaninNum(pObj) );
+ Dau_DecTrySets( (word *)pTruth, Abc_ObjFaninNum(pObj), 1 );
if ( fProfile )
Kit_TruthPrintProfile( pTruth, Abc_ObjFaninNum(pObj) );
else if ( fCofactor )
diff --git a/src/base/abci/abcDec.c b/src/base/abci/abcDec.c
index 873ef876..3ed73c26 100644
--- a/src/base/abci/abcDec.c
+++ b/src/base/abci/abcDec.c
@@ -25,6 +25,7 @@
#include "bool/dec/dec.h"
#include "bool/kit/kit.h"
#include "opt/dau/dau.h"
+#include "misc/util/utilTruth.h"
ABC_NAMESPACE_IMPL_START
@@ -564,11 +565,13 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose )
{
for ( i = 0; i < p->nFuncs; i++ )
{
- extern void Dau_DecTrySets( word * pInit, int nVars );
+ extern void Dau_DecTrySets( word * pInit, int nVars, int fVerbose );
+ int nSuppSize = Abc_TtSupportSize( p->pFuncs[i], p->nVars );
if ( fVerbose )
printf( "%7d : ", i );
- Dau_DecTrySets( p->pFuncs[i], p->nVars );
- printf( "\n" );
+ Dau_DecTrySets( p->pFuncs[i], nSuppSize, fVerbose );
+ if ( fVerbose )
+ printf( "\n" );
}
}
else assert( 0 );
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 8821d06f..41d30da4 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -35,9 +35,9 @@
#include "misc/mem/mem.h"
#include "misc/tim/tim.h"
#include "misc/util/utilNam.h"
-#include "opt/dau/dau.h"
#include "misc/vec/vecMem.h"
#include "misc/util/utilTruth.h"
+#include "opt/dau/dau.h"
ABC_NAMESPACE_HEADER_START
@@ -153,8 +153,8 @@ struct If_Par_t_
float * pTimesArr; // arrival times
float * pTimesReq; // required times
int (* pFuncCost) (If_Man_t *, If_Cut_t *); // procedure to compute the user's cost of a cut
- int (* pFuncUser) (If_Man_t *, If_Obj_t *, If_Cut_t *); // procedure called for each cut when cut computation is finished
- int (* pFuncCell) (If_Man_t *, unsigned *, int, int, char *); // procedure called for cut functions
+ int (* pFuncUser) (If_Man_t *, If_Obj_t *, If_Cut_t *); // procedure called for each cut when cut computation is finished
+ int (* pFuncCell) (If_Man_t *, unsigned *, int, int, char *); // procedure called for cut functions
void * pReoMan; // reordering manager
};
@@ -233,6 +233,7 @@ struct If_Man_t_
int nCuts5, nCuts5a;
If_DsdMan_t * pIfDsdMan;
Vec_Mem_t * vTtMem; // truth table memory and hash table
+ Vec_Int_t * vDsds; // mapping of truth table into DSD
int nBestCutSmall[2];
// timing manager
@@ -518,7 +519,8 @@ extern If_DsdMan_t * If_DsdManAlloc( int nLutSize );
extern void If_DsdManDump( If_DsdMan_t * p );
extern void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose );
extern void If_DsdManFree( If_DsdMan_t * p );
-extern int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm );
+extern int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm, char * pLutStruct );
+extern int If_DsdManCheckDec( If_DsdMan_t * pIfMan, int iDsd );
/*=== ifLib.c =============================================================*/
extern If_LibLut_t * If_LibLutRead( char * FileName );
extern If_LibLut_t * If_LibLutDup( If_LibLut_t * p );
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index f387e645..5c3fecc9 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -44,7 +44,8 @@ struct If_DsdObj_t_
unsigned Id; // node ID
unsigned Type : 3; // node type
unsigned nSupp : 5; // variable
- unsigned Count : 19; // variable
+ unsigned fMark : 1; // user mark
+ unsigned Count : 18; // variable
unsigned nFans : 5; // fanin count
unsigned pFans[0]; // fanins
};
@@ -58,10 +59,10 @@ struct If_DsdMan_t_
Mem_Flex_t * pMem; // memory for nodes
Vec_Ptr_t * vObjs; // objects
Vec_Int_t * vNexts; // next pointers
- Vec_Int_t * vLeaves; // temp
- Vec_Int_t * vCopies; // temp
+ Vec_Int_t * vNodes; // temp
word ** pTtElems; // elementary TTs
Vec_Mem_t * vTtMem; // truth table memory and hash table
+ Vec_Ptr_t * vTtDecs; // truth table decompositions
int nUniqueHits; // statistics
int nUniqueMisses; // statistics
abctime timeBeg; // statistics
@@ -90,13 +91,15 @@ static inline If_DsdObj_t * If_DsdVecVar( Vec_Ptr_t * p, int v )
static inline int If_DsdVecObjSuppSize( Vec_Ptr_t * p, int iObj ) { return If_DsdVecObj( p, iObj )->nSupp; }
static inline int If_DsdVecLitSuppSize( Vec_Ptr_t * p, int iLit ) { return If_DsdVecObjSuppSize( p, Abc_Lit2Var(iLit) ); }
static inline int If_DsdVecObjRef( Vec_Ptr_t * p, int iObj ) { return If_DsdVecObj( p, iObj )->Count; }
-static inline void If_DsdVecObjIncRef( Vec_Ptr_t * p, int iObj ) { if ( If_DsdVecObjRef(p, iObj) < 0x7FFFF ) If_DsdVecObj( p, iObj )->Count++; }
+static inline void If_DsdVecObjIncRef( Vec_Ptr_t * p, int iObj ) { if ( If_DsdVecObjRef(p, iObj) < 0x3FFFF ) If_DsdVecObj( p, iObj )->Count++; }
static inline If_DsdObj_t * If_DsdObjFanin( Vec_Ptr_t * p, If_DsdObj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return If_DsdVecObj(p, Abc_Lit2Var(pObj->pFans[i])); }
+static inline int If_DsdVecObjMark( Vec_Ptr_t * p, int iObj ) { return If_DsdVecObj( p, iObj )->fMark; }
+static inline void If_DsdVecObjSetMark( Vec_Ptr_t * p, int iObj ) { If_DsdVecObj( p, iObj )->fMark = 1; }
#define If_DsdVecForEachObj( vVec, pObj, i ) \
Vec_PtrForEachEntry( If_DsdObj_t *, vVec, pObj, i )
-#define If_DsdVecForEachObjVec( vLits, vVec, pObj, i ) \
- for ( i = 0; (i < Vec_IntSize(vLits)) && ((pObj) = Dss_Lit2Obj(vVec, Vec_IntEntry(vLits,i))); i++ )
+#define If_DsdVecForEachObjVec( vNodes, vVec, pObj, i ) \
+ for ( i = 0; (i < Vec_IntSize(vNodes)) && ((pObj) = If_DsdVecObj(vVec, Vec_IntEntry(vNodes,i))); i++ )
#define If_DsdVecForEachNode( vVec, pObj, i ) \
Vec_PtrForEachEntry( If_DsdObj_t *, vVec, pObj, i ) \
if ( If_DsdObjType(pObj) == IF_DSD_CONST0 || If_DsdObjType(pObj) == IF_DSD_VAR ) {} else
@@ -183,6 +186,7 @@ If_DsdObj_t * If_DsdObjAlloc( If_DsdMan_t * p, int Type, int nFans )
pObj->Type = Type;
pObj->nFans = nFans;
pObj->Id = Vec_PtrSize( p->vObjs );
+ pObj->fMark = 0;
pObj->Count = 0;
Vec_PtrPush( p->vObjs, pObj );
Vec_IntPush( p->vNexts, 0 );
@@ -263,10 +267,11 @@ If_DsdMan_t * If_DsdManAlloc( int nVars )
p->vNexts = Vec_IntAlloc( 10000 );
If_DsdObjAlloc( p, IF_DSD_CONST0, 0 );
If_DsdObjAlloc( p, IF_DSD_VAR, 0 )->nSupp = 1;
- p->vLeaves = Vec_IntAlloc( 32 );
- p->vCopies = Vec_IntAlloc( 32 );
+ p->vNodes = Vec_IntAlloc( 32 );
p->pTtElems = If_ManDsdTtElems();
- p->vTtMem = Vec_MemAllocForTT( nVars );
+ p->vTtDecs = Vec_PtrAlloc( 1000 );
+ p->vTtMem = Vec_MemAlloc( Abc_TtWordNum(nVars), 12 );
+ Vec_MemHashAlloc( p->vTtMem, 10000 );
return p;
}
void If_DsdManFree( If_DsdMan_t * p )
@@ -282,10 +287,10 @@ void If_DsdManFree( If_DsdMan_t * p )
Abc_PrintTime( 1, "Time lookup", p->timeLook );
Abc_PrintTime( 1, "Time end ", p->timeEnd );
}
+ Vec_VecFree( (Vec_Vec_t *)p->vTtDecs );
Vec_MemHashFree( p->vTtMem );
Vec_MemFreeP( &p->vTtMem );
- Vec_IntFreeP( &p->vCopies );
- Vec_IntFreeP( &p->vLeaves );
+ Vec_IntFreeP( &p->vNodes );
Vec_IntFreeP( &p->vNexts );
Vec_PtrFreeP( &p->vObjs );
Mem_FlexStop( p->pMem, 0 );
@@ -331,20 +336,21 @@ void If_DsdManPrint_rec( FILE * pFile, If_DsdMan_t * p, int iDsdLit, unsigned ch
If_DsdManPrint_rec( pFile, p, iFanin, pPermLits, pnSupp );
fprintf( pFile, "%c", CloseType[If_DsdObjType(pObj)] );
}
-void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char * pPermLits )
+void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char * pPermLits, int fNewLine )
{
int nSupp = 0;
fprintf( pFile, "%6d : ", iObjId );
fprintf( pFile, "%2d ", If_DsdVecObjSuppSize(p->vObjs, iObjId) );
fprintf( pFile, "%8d ", If_DsdVecObjRef(p->vObjs, iObjId) );
If_DsdManPrint_rec( pFile, p, Abc_Var2Lit(iObjId, 0), pPermLits, &nSupp );
- fprintf( pFile, "\n" );
+ if ( fNewLine )
+ fprintf( pFile, "\n" );
assert( nSupp == If_DsdVecObjSuppSize(p->vObjs, iObjId) );
}
void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose )
{
If_DsdObj_t * pObj;
- int CountNonDsd = 0, CountNonDsdStr = 0;
+ int DsdMax = 0, CountUsed = 0, CountNonDsdStr = 0;
int i, clk = Abc_Clock();
FILE * pFile;
pFile = pFileName ? fopen( pFileName, "wb" ) : stdout;
@@ -355,17 +361,20 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose )
}
If_DsdVecForEachObj( p->vObjs, pObj, i )
{
- CountNonDsd += (If_DsdObjType(pObj) == IF_DSD_PRIME);
+ if ( If_DsdObjType(pObj) == IF_DSD_PRIME )
+ DsdMax = Abc_MaxInt( DsdMax, pObj->nFans );
CountNonDsdStr += If_DsdManCheckNonDec_rec( p, pObj->Id );
+ CountUsed += ( If_DsdVecObjRef(p->vObjs, pObj->Id) > 0 );
}
fprintf( pFile, "Total number of objects = %8d\n", Vec_PtrSize(p->vObjs) );
- fprintf( pFile, "Non-DSD objects (max =%2d) = %8d\n", Vec_MemEntryNum(p->vTtMem), CountNonDsd );
+ fprintf( pFile, "Externally used objects = %8d\n", CountUsed );
+ fprintf( pFile, "Non-DSD objects (max =%2d) = %8d\n", DsdMax, Vec_MemEntryNum(p->vTtMem) );
fprintf( pFile, "Non-DSD structures = %8d\n", CountNonDsdStr );
- fprintf( pFile, "Memory used for objects = %6.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) );
- fprintf( pFile, "Memory used for array = %6.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) );
- fprintf( pFile, "Memory used for hash table = %6.2f MB.\n", 1.0*sizeof(int)*p->nBins/(1<<20) );
fprintf( pFile, "Unique table hits = %8d\n", p->nUniqueHits );
fprintf( pFile, "Unique table misses = %8d\n", p->nUniqueMisses );
+ fprintf( pFile, "Memory used for objects = %8.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) );
+ fprintf( pFile, "Memory used for hash table = %8.2f MB.\n", 1.0*sizeof(int)*p->nBins/(1<<20) );
+ fprintf( pFile, "Memory used for array = %8.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
// If_DsdManHashProfile( p );
// If_DsdManDump( p );
@@ -376,7 +385,7 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose )
{
// if ( i == 50 )
// break;
- If_DsdManPrintOne( pFile, p, pObj->Id, NULL );
+ If_DsdManPrintOne( pFile, p, pObj->Id, NULL, 1 );
}
fprintf( pFile, "\n" );
if ( pFileName )
@@ -403,13 +412,39 @@ void If_DsdManDump( If_DsdMan_t * p )
fprintf( pFile, "\n" );
printf( " " );
Dau_DsdPrintFromTruth( If_DsdObjTruth(p, pObj), p->nVars );
- printf( "\n" );
}
fclose( pFile );
}
/**Function*************************************************************
+ Synopsis [Collect nodes of the tree.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void If_DsdManCollect_rec( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes )
+{
+ int i, iFanin;
+ If_DsdObj_t * pObj = If_DsdVecObj( p->vObjs, Id );
+ if ( If_DsdObjType(pObj) == IF_DSD_CONST0 || If_DsdObjType(pObj) == IF_DSD_VAR )
+ return;
+ If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i )
+ If_DsdManCollect_rec( p, Abc_Lit2Var(iFanin), vNodes );
+ Vec_IntPush( vNodes, Id );
+}
+void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes )
+{
+ Vec_IntClear( vNodes );
+ If_DsdManCollect_rec( p, Id, vNodes );
+}
+
+/**Function*************************************************************
+
Synopsis []
Description []
@@ -470,6 +505,12 @@ int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word
unsigned * pSpot = If_DsdObjHashLookup( p, Type, pLits, nLits, truthId );
if ( *pSpot )
return *pSpot;
+ if ( truthId >= 0 && truthId == Vec_MemEntryNum(p->vTtMem)-1 )
+ {
+ Vec_Int_t * vSets = Dau_DecFindSets( pTruth, nLits );
+ Vec_PtrPush( p->vTtDecs, vSets );
+// Dau_DecPrintSets( vSets, nLits );
+ }
*pSpot = Vec_PtrSize( p->vObjs );
return If_DsdObjCreate( p, Type, pLits, nLits, truthId );
}
@@ -768,6 +809,7 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig
assert( j == nSSize );
for ( j = 0; j < nSSize; j++ )
pPerm[j] = pPermNew[j];
+ Abc_TtStretch6( pTruth, nLits, p->nVars );
}
else assert( 0 );
// create new graph
@@ -864,6 +906,158 @@ int If_DsdManAddDsd( If_DsdMan_t * p, char * pDsd, word * pTruth, unsigned char
/**Function*************************************************************
+ Synopsis [Returns 1 if XY-decomposability holds to this LUT size.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+// collect supports of the node
+void If_DsdManGetSuppSizes( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pSSizes )
+{
+ If_DsdObj_t * pFanin; int i;
+ If_DsdObjForEachFanin( p->vObjs, pObj, pFanin, i )
+ pSSizes[i] = If_DsdObjSuppSize(pFanin);
+}
+// checks if there is a way to package some fanins
+int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize )
+{
+ int i[6], LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR];
+ int nFans = If_DsdObjFaninNum(pObj);
+ assert( pObj->nFans > 2 );
+ assert( If_DsdObjSuppSize(pObj) > LutSize );
+ If_DsdManGetSuppSizes( p, pObj, pSSizes );
+ LimitOut = LutSize - (nSuppAll - pObj->nSupp + 1);
+ assert( LimitOut < LutSize );
+ for ( i[0] = 0; i[0] < nFans; i[0]++ )
+ for ( i[1] = i[0]+1; i[1] < nFans; i[1]++ )
+ {
+ SizeIn = pSSizes[i[0]] + pSSizes[i[1]];
+ SizeOut = pObj->nSupp - SizeIn;
+ if ( SizeIn > LutSize || SizeOut > LimitOut )
+ continue;
+ return (1 << i[0]) | (1 << i[1]);
+ }
+ if ( pObj->nFans == 3 )
+ return 0;
+ for ( i[0] = 0; i[0] < nFans; i[0]++ )
+ for ( i[1] = i[0]+1; i[1] < nFans; i[1]++ )
+ for ( i[2] = i[1]+1; i[2] < nFans; i[2]++ )
+ {
+ SizeIn = pSSizes[i[0]] + pSSizes[i[1]] + pSSizes[i[2]];
+ SizeOut = pObj->nSupp - SizeIn;
+ if ( SizeIn > LutSize || SizeOut > LimitOut )
+ continue;
+ return (1 << i[0]) | (1 << i[1]) | (1 << i[2]);
+ }
+ return 0;
+}
+// checks if there is a way to package some fanins
+int If_DsdManCheckPrime( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize )
+{
+ int fVerbose = 0;
+ int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR];
+ int truthId = If_DsdObjTruthId( p, pObj );
+ int nFans = If_DsdObjFaninNum(pObj);
+ Vec_Int_t * vSets = (Vec_Int_t *)Vec_PtrEntry(p->vTtDecs, truthId);
+if ( fVerbose )
+printf( "\n" );
+if ( fVerbose )
+Dau_DecPrintSets( vSets, nFans );
+ assert( pObj->nFans > 2 );
+ assert( If_DsdObjSuppSize(pObj) > LutSize );
+ If_DsdManGetSuppSizes( p, pObj, pSSizes );
+ LimitOut = LutSize - (nSuppAll - pObj->nSupp + 1);
+ assert( LimitOut < LutSize );
+ Vec_IntForEachEntry( vSets, set, i )
+ {
+ SizeIn = SizeOut = 0;
+ for ( v = 0; v < nFans; v++ )
+ {
+ int Value = ((set >> (v << 1)) & 3);
+ if ( Value == 0 )
+ SizeOut += pSSizes[v];
+ else if ( Value == 1 )
+ SizeIn += pSSizes[v];
+ else if ( Value == 3 )
+ {
+ SizeIn += pSSizes[v];
+ SizeOut += pSSizes[v];
+ }
+ else assert( Value == 0 );
+ if ( SizeIn > LutSize || SizeOut > LimitOut )
+ break;
+ }
+ if ( v == nFans )
+ return set;
+ }
+ return 0;
+}
+int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize )
+{
+ int fVerbose = 0;
+ If_DsdObj_t * pObj, * pTemp; int i, Mask;
+ pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iDsd) );
+ if ( fVerbose )
+ If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 0 );
+ if ( If_DsdObjSuppSize(pObj) <= LutSize )
+ {
+ if ( fVerbose )
+ printf( " Trivial\n" );
+ return 1;
+ }
+ If_DsdManCollect( p, pObj->Id, p->vNodes );
+ If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
+ if ( If_DsdObjSuppSize(pTemp) <= LutSize && If_DsdObjSuppSize(pObj) - If_DsdObjSuppSize(pTemp) <= LutSize - 1 )
+ {
+ if ( fVerbose )
+ printf( " Dec using node " );
+ if ( fVerbose )
+ If_DsdManPrintOne( stdout, p, pTemp->Id, NULL, 1 );
+ return 1;
+ }
+ If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
+ if ( (If_DsdObjType(pTemp) == IF_DSD_AND || If_DsdObjType(pTemp) == IF_DSD_XOR) && If_DsdObjFaninNum(pTemp) > 2 && If_DsdObjSuppSize(pTemp) > LutSize )
+ {
+ if ( (Mask = If_DsdManCheckAndXor(p, pTemp, If_DsdObjSuppSize(pObj), LutSize)) )
+ {
+ if ( fVerbose )
+ printf( " " );
+ if ( fVerbose )
+ Abc_TtPrintBinary( (word *)&Mask, 4 );
+ if ( fVerbose )
+ printf( " Using multi-input AND/XOR node\n" );
+ return 1;
+ }
+ }
+ If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
+ if ( If_DsdObjType(pTemp) == IF_DSD_PRIME )
+ {
+ if ( (Mask = If_DsdManCheckPrime(p, pTemp, If_DsdObjSuppSize(pObj), LutSize)) )
+ {
+ if ( fVerbose )
+ printf( " " );
+ if ( fVerbose )
+ Dau_DecPrintSet( Mask, If_DsdObjFaninNum(pTemp), 0 );
+ if ( fVerbose )
+ printf( " Using prime node\n" );
+ return 1;
+ }
+ }
+ if ( fVerbose )
+ printf( " UNDEC\n" );
+ return 0;
+}
+int If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize )
+{
+ return 1;
+}
+
+/**Function*************************************************************
+
Synopsis [Add the function to the DSD manager.]
Description []
@@ -873,7 +1067,7 @@ int If_DsdManAddDsd( If_DsdMan_t * p, char * pDsd, word * pTruth, unsigned char
SeeAlso []
***********************************************************************/
-int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm )
+int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm, char * pLutStruct )
{
word pCopy[DAU_MAX_WORD], * pRes;
char pDsd[DAU_MAX_STR];
@@ -897,14 +1091,25 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char
// If_DsdManPrint( p, NULL );
printf( "\n" );
printf( "Verification failed!\n" );
- Dau_DsdPrintFromTruth( pTruth, nLeaves ); printf( "\n" );
- Dau_DsdPrintFromTruth( pRes, nLeaves ); printf( "\n" );
- If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), pPerm );
+ Dau_DsdPrintFromTruth( pTruth, nLeaves );
+ Dau_DsdPrintFromTruth( pRes, nLeaves );
+ If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), pPerm, 1 );
printf( "\n" );
}
If_DsdVecObjIncRef( p->vObjs, Abc_Lit2Var(iDsd) );
+ if ( pLutStruct )
+ {
+ int LutSize = (int)(pLutStruct[0] - '0');
+ assert( pLutStruct[2] == 0 );
+ if ( If_DsdManCheckXY( p, iDsd, LutSize ) )
+ If_DsdVecObjSetMark( p->vObjs, Abc_Lit2Var(iDsd) );
+ }
return iDsd;
}
+int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd )
+{
+ return If_DsdVecObjMark( p->vObjs, Abc_Lit2Var(iDsd) );
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 529b8cb9..ae7552b3 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -84,7 +84,12 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
p->puTemp[3] = p->puTemp[2] + p->nTruth6Words*2;
p->puTempW = p->pPars->fTruth? ABC_ALLOC( word, p->nTruth6Words ) : NULL;
if ( pPars->fUseDsd )
+ {
p->pIfDsdMan = If_DsdManAlloc( pPars->nLutSize );
+ p->vDsds = Vec_IntAlloc( 1000 );
+ Vec_IntPush( p->vDsds, 0 );
+ Vec_IntPush( p->vDsds, 2 );
+ }
// create the constant node
p->pConst1 = If_ManSetupObj( p );
p->pConst1->Type = IF_CONST1;
@@ -165,9 +170,10 @@ void If_ManStop( If_Man_t * p )
Vec_WrdFreeP( &p->vAnds );
Vec_WrdFreeP( &p->vAndGate );
Vec_WrdFreeP( &p->vOrGate );
- if ( p->vObjsRev ) Vec_PtrFree( p->vObjsRev );
- if ( p->vLatchOrder ) Vec_PtrFree( p->vLatchOrder );
- if ( p->vLags ) Vec_IntFree( p->vLags );
+ Vec_PtrFreeP( &p->vObjsRev );
+ Vec_PtrFreeP( &p->vLatchOrder );
+ Vec_IntFreeP( &p->vLags );
+ Vec_IntFreeP( &p->vDsds );
Vec_MemHashFree( p->vTtMem );
Vec_MemFreeP( &p->vTtMem );
Mem_FixedStop( p->pMemObj, 0 );
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index c22d8604..34e83139 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -217,6 +217,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
// abctime clk = Abc_Clock();
If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
// p->timeTruth += Abc_Clock() - clk;
+ // run user functions
pCut->fUseless = 0;
if ( p->pPars->pFuncCell )
{
@@ -250,9 +251,26 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
p->nCuts5a++;
}
}
+ if ( p->pPars->fUseDsd )
+ {
+ int truthId = Abc_Lit2Var(pCut->iCutFunc);
+ if ( Vec_IntSize(p->vDsds) <= truthId || Vec_IntEntry(p->vDsds, truthId) == -1 )
+ {
+ pCut->iCutDsd = If_DsdManCompute( p->pIfDsdMan, If_CutTruthW(p, pCut), pCut->nLeaves, (unsigned char *)pCut->pPerm, p->pPars->pLutStruct );
+ while ( Vec_IntSize(p->vDsds) <= truthId )
+ Vec_IntPush( p->vDsds, -1 );
+ Vec_IntWriteEntry( p->vDsds, truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) );
+ }
+ else
+ pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vDsds, truthId), Abc_LitIsCompl(pCut->iCutFunc) );
+ if ( p->pPars->pLutStruct )
+ {
+ int Value = If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd );
+ if ( Value != (int)pCut->fUseless )
+ printf( "Difference\n" );
+ }
+ }
}
- if ( p->pPars->fUseDsd && Abc_Lit2Var(pCut->iCutFunc) == Vec_MemEntryNum(p->vTtMem)-1 )
- pCut->iCutDsd = If_DsdManCompute( p->pIfDsdMan, If_CutTruthW(p, pCut), pCut->nLeaves, (unsigned char *)pCut->pPerm );
// compute the application-specific cost and depth
pCut->fUser = (p->pPars->pFuncCost != NULL);
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h
index dab49bc3..2e56899b 100644
--- a/src/opt/dau/dau.h
+++ b/src/opt/dau/dau.h
@@ -97,6 +97,11 @@ extern void * Dsm_ManDeriveGia( void * p, int fUseMuxes );
extern void Dau_DsdRemoveBraces( char * pDsd, int * pMatches );
extern char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1, int nVars );
+/*=== dauNonDsd.c ==========================================================*/
+extern Vec_Int_t * Dau_DecFindSets( word * pInit, int nVars );
+extern void Dau_DecPrintSets( Vec_Int_t * vSets, int nVars );
+extern void Dau_DecPrintSet( unsigned set, int nVars, int fNewLine );
+
/*=== dauTree.c ==========================================================*/
extern Dss_Man_t * Dss_ManAlloc( int nVars, int nNonDecLimit );
extern void Dss_ManFree( Dss_Man_t * p );
diff --git a/src/opt/dau/dauNonDsd.c b/src/opt/dau/dauNonDsd.c
index e5cc58e1..53eafe92 100644
--- a/src/opt/dau/dauNonDsd.c
+++ b/src/opt/dau/dauNonDsd.c
@@ -459,7 +459,7 @@ void Dau_DecMoveFreeToLSB( word * p, int nVars, int * V2P, int * P2V, int maskB,
Abc_TtMoveVar( p, nVars, V2P, P2V, v, c++ );
assert( c == nVars - sizeB );
}
-Vec_Int_t * Dau_DecFindSets( word * p, int nVars )
+Vec_Int_t * Dau_DecFindSets( word * pInit, int nVars )
{
Vec_Int_t * vSets = Vec_IntAlloc( 32 );
int V2P[16], P2V[16], pVarsB[16];
@@ -467,6 +467,8 @@ Vec_Int_t * Dau_DecFindSets( word * p, int nVars )
int c, v, sizeB, sizeS, maskB, maskS;
int * pSched[16] = {NULL};
unsigned setMixed;
+ word p[1<<10];
+ memcpy( p, pInit, sizeof(word) * Abc_TtWordNum(nVars) );
for ( v = 0; v < nVars; v++ )
assert( Abc_TtHasVar( p, nVars, v ) );
for ( v = 2; v < nVars; v++ )
@@ -703,7 +705,7 @@ int Dau_DecVerify( word * pInit, int nVars, char * pDsdC, char * pDsdD )
printf( "\n" );
return 1;
}
-int Dau_DecPerform( word * p, int nVars, unsigned uSet )
+int Dau_DecPerform6( word * p, int nVars, unsigned uSet )
{
word tComp = 0, tDec = 0, tDec0, tComp0, tComp1, FuncC, FuncD;
char pDsdC[1000], pDsdD[1000];
@@ -760,7 +762,7 @@ int Dau_DecPerform( word * p, int nVars, unsigned uSet )
return 1;
}
-int Dau_DecPerform2( word * pInit, int nVars, unsigned uSet )
+int Dau_DecPerform( word * pInit, int nVars, unsigned uSet )
{
word p[1<<10], pDec[1<<10], pComp[1<<10]; // at most 2^10 words
char pDsdC[5000], pDsdD[5000]; // at most 2^12 hex digits
@@ -820,15 +822,18 @@ int Dau_DecPerform2( word * pInit, int nVars, unsigned uSet )
Dau_DecVerify( pInit, nVars, pDsdC, pDsdD );
return 1;
}
-void Dau_DecTrySets( word * pInit, int nVars )
+void Dau_DecTrySets( word * pInit, int nVars, int fVerbose )
{
- word p[1<<10];
Vec_Int_t * vSets;
int i, Entry;
assert( nVars <= 16 );
- memcpy( p, pInit, sizeof(word) * Abc_TtWordNum(nVars) );
- vSets = Dau_DecFindSets( p, nVars );
- Dau_DsdPrintFromTruth( p, nVars );
+ vSets = Dau_DecFindSets( pInit, nVars );
+ if ( !fVerbose )
+ {
+ Vec_IntFree( vSets );
+ return;
+ }
+ Dau_DsdPrintFromTruth( pInit, nVars );
printf( "This %d-variable function has %d decomposable variable sets:\n", nVars, Vec_IntSize(vSets) );
Vec_IntForEachEntry( vSets, Entry, i )
{
@@ -837,12 +842,12 @@ void Dau_DecTrySets( word * pInit, int nVars )
if ( nVars > 6 )
{
Dau_DecPrintSet( uSet, nVars, 0 );
- Dau_DecPerform2( pInit, nVars, uSet );
+ Dau_DecPerform( pInit, nVars, uSet );
}
else
{
Dau_DecPrintSet( uSet, nVars, 1 );
- Dau_DecPerform( pInit, nVars, uSet );
+ Dau_DecPerform6( pInit, nVars, uSet );
}
}
Vec_IntFree( vSets );
@@ -860,7 +865,7 @@ void Dau_DecFindSetsTest3()
// char * pStr = "Abcd";
// char * pStr = "ab";
unsigned uSet = Dau_DecReadSet( pStr );
- Dau_DecPerform( &t, nVars, uSet );
+ Dau_DecPerform6( &t, nVars, uSet );
}
void Dau_DecFindSetsTest()
@@ -879,7 +884,7 @@ void Dau_DecFindSetsTest()
// word t = ABC_CONST(0x2B0228022B022802); // 5-var non-dec0x0F7700000F770000
// word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e)
// word t = ABC_CONST(0x7F00000000000000); // (!(abc)def)
- Dau_DecTrySets( &t, nVars );
+ Dau_DecTrySets( &t, nVars, 1 );
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 19:16:50 +0000