summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/base/abci/abc.c18
-rw-r--r--src/base/abci/abcDec.c2
-rw-r--r--src/map/if/if.h1
-rw-r--r--src/map/if/ifCut.c2
-rw-r--r--src/map/if/ifMan.c3
-rw-r--r--src/map/if/ifMap.c52
-rw-r--r--src/map/if/ifTruth.c2
-rw-r--r--src/misc/util/utilTruth.h10
-rw-r--r--src/opt/dau/dau.h11
-rw-r--r--src/opt/dau/dauDsd.c37
-rw-r--r--src/opt/dau/dauMerge.c2
-rw-r--r--src/opt/dau/dauTree.c494
12 files changed, 474 insertions, 160 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 5fa4d7fd..de37c441 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -14561,7 +14561,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
fLutMux = 0;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGDEWSqaflepmrsdbugyojikcnvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGNDEWSqaflepmrsdbugyojikcnvh" ) ) != EOF )
{
switch ( c )
{
@@ -14622,6 +14622,17 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pPars->nGateSize < 2 )
goto usage;
break;
+ case 'N':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-N\" should be followed by a positive integer no less than 3.\n" );
+ goto usage;
+ }
+ pPars->nNonDecLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nNonDecLimit < 2 )
+ goto usage;
+ break;
case 'D':
if ( globalUtilOptind >= argc )
{
@@ -14894,6 +14905,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
{
pPars->fTruth = 1;
pPars->fCutMin = 1;
+ pPars->fExpRed = 0;
pPars->fUsePerm = 1;
}
@@ -14988,12 +15000,13 @@ usage:
sprintf(LutSize, "library" );
else
sprintf(LutSize, "%d", pPars->nLutSize );
- Abc_Print( -2, "usage: if [-KCFAG num] [-DEW float] [-S str] [-qarlepmsdbugyojikcnvh]\n" );
+ Abc_Print( -2, "usage: if [-KCFANG num] [-DEW float] [-S str] [-qarlepmsdbugyojikcnvh]\n" );
Abc_Print( -2, "\t performs FPGA technology mapping of the network\n" );
Abc_Print( -2, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
Abc_Print( -2, "\t-C num : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
Abc_Print( -2, "\t-F num : the number of area flow recovery iterations (num >= 0) [default = %d]\n", pPars->nFlowIters );
Abc_Print( -2, "\t-A num : the number of exact area recovery iterations (num >= 0) [default = %d]\n", pPars->nAreaIters );
+ Abc_Print( -2, "\t-N num : the max size of non-decomposable nodes [default = unused]\n", pPars->nNonDecLimit );
Abc_Print( -2, "\t-G num : the max AND/OR gate size for mapping (0 = unused) [default = %d]\n", pPars->nGateSize );
Abc_Print( -2, "\t-D float : sets the delay constraint for the mapping [default = %s]\n", Buffer );
Abc_Print( -2, "\t-E float : sets epsilon used for tie-breaking [default = %f]\n", pPars->Epsilon );
@@ -27472,6 +27485,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
{
pPars->fTruth = 1;
pPars->fCutMin = 1;
+ pPars->fExpRed = 0;
pPars->fUsePerm = 1;
}
diff --git a/src/base/abci/abcDec.c b/src/base/abci/abcDec.c
index 61d71dfb..d232d5aa 100644
--- a/src/base/abci/abcDec.c
+++ b/src/base/abci/abcDec.c
@@ -547,7 +547,7 @@ void Abc_TruthDecPerform( Abc_TtStore_t * p, int DecType, int fVerbose )
{
if ( fVerbose )
printf( "%7d : ", i );
- Dau_DsdDecompose( p->pFuncs[i], p->nVars, 0, pDsd );
+ Dau_DsdDecompose( p->pFuncs[i], p->nVars, 0, 1, pDsd );
if ( fVerbose )
printf( "%s\n", pDsd );
nNodes += Dau_DsdCountAnds( pDsd );
diff --git a/src/map/if/if.h b/src/map/if/if.h
index f1d78ff4..4505f6d4 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -98,6 +98,7 @@ struct If_Par_t_
int nFlowIters; // the number of iterations of area recovery
int nAreaIters; // the number of iterations of area recovery
int nGateSize; // the max size of the AND/OR gate to map into
+ int nNonDecLimit; // the max size of non-dec nodes
float DelayTarget; // delay target
float Epsilon; // value used in comparison floating point numbers
int fPreprocess; // preprossing
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index ca985910..ace197fb 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -856,7 +856,7 @@ void If_CutSort( If_Man_t * p, If_Set_t * pCutSet, If_Cut_t * pCut )
return;
}
- if ( (p->pPars->fUseBat || p->pPars->fEnableCheck07 || p->pPars->fEnableCheck08 || p->pPars->fEnableCheck10 || p->pPars->pLutStruct || p->pPars->fUserRecLib) && !pCut->fUseless )
+ if ( (p->pPars->fUseDsd || p->pPars->fUseBat || p->pPars->fEnableCheck07 || p->pPars->fEnableCheck08 || p->pPars->fEnableCheck10 || p->pPars->pLutStruct || p->pPars->fUserRecLib) && !pCut->fUseless )
{
If_Cut_t * pFirst = pCutSet->ppCuts[0];
if ( pFirst->fUseless || If_ManSortCompare(p, pFirst, pCut) == 1 )
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 076f74d6..1cc92def 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -85,7 +85,7 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
{
// p->pNamDsd = Abc_NamStart( 1000, 20 );
// p->iNamVar = Abc_NamStrFindOrAdd( p->pNamDsd, "a", NULL );
- p->pDsdMan = Dss_ManAlloc( pPars->nLutSize );
+ p->pDsdMan = Dss_ManAlloc( pPars->nLutSize, pPars->nNonDecLimit );
p->iNamVar = 2;
}
@@ -165,6 +165,7 @@ void If_ManStop( If_Man_t * p )
// Abc_NamPrint( p->pNamDsd );
Abc_NamStop( p->pNamDsd );
*/
+ Dss_ManPrint( p->pDsdMan );
Dss_ManFree( p->pDsdMan );
}
// Abc_PrintTime( 1, "Truth", p->timeTruth );
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index ad50e1cc..ac606416 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -277,32 +277,36 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
}
if ( p->pPars->fUseDsd )
{
- int j, iDsd[2] = { Abc_LitNotCond(pCut0->iDsd, pObj->fCompl0), Abc_LitNotCond(pCut1->iDsd, pObj->fCompl1) };
- int nFans[2] = { pCut0->nLeaves, pCut1->nLeaves };
- int Fans[2][DAU_MAX_VAR], * pFans[2] = { Fans[0], Fans[1] };
-/*
- char * pName = Dau_DsdMerge(
- Abc_NamStr(p->pNamDsd, pCut0->iDsd),
- If_CutPerm0(pCut, pCut0),
- Abc_NamStr(p->pNamDsd, pCut1->iDsd),
- If_CutPerm1(pCut, pCut1),
- pObj->fCompl0, pObj->fCompl1, pCut->nLimit );
- pCut->iDsd = Abc_NamStrFindOrAdd( p->pNamDsd, pName, NULL );
-*/
- // create fanins
- for ( j = 0; j < (int)pCut0->nLeaves; j++ )
- pFans[0][j] = Abc_Lit2Lit( p->pPerm[0], (int)pCut0->pPerm[j] );
- for ( j = 0; j < (int)pCut1->nLeaves; j++ )
- pFans[1][j] = Abc_Lit2Lit( p->pPerm[1], (int)pCut1->pPerm[j] );
- // canonicize
- if ( iDsd[0] > iDsd[1] )
+ if ( pCut0->iDsd < 0 || pCut1->iDsd < 0 )
+ pCut->iDsd = -1;
+ else
+ {
+ int j, iDsd[2] = { Abc_LitNotCond(pCut0->iDsd, pObj->fCompl0), Abc_LitNotCond(pCut1->iDsd, pObj->fCompl1) };
+ int nFans[2] = { pCut0->nLeaves, pCut1->nLeaves };
+ int Fans[2][DAU_MAX_VAR], * pFans[2] = { Fans[0], Fans[1] };
+ // create fanins
+ for ( j = 0; j < (int)pCut0->nLeaves; j++ )
+ pFans[0][j] = Abc_Lit2Lit( p->pPerm[0], (int)pCut0->pPerm[j] );
+ for ( j = 0; j < (int)pCut1->nLeaves; j++ )
+ pFans[1][j] = Abc_Lit2Lit( p->pPerm[1], (int)pCut1->pPerm[j] );
+ // canonicize
+ if ( iDsd[0] > iDsd[1] )
+ {
+ ABC_SWAP( int, iDsd[0], iDsd[1] );
+ ABC_SWAP( int, nFans[0], nFans[1] );
+ ABC_SWAP( int *, pFans[0], pFans[1] );
+ }
+ // derive new DSD
+ pCut->iDsd = Dss_ManMerge( p->pDsdMan, iDsd, nFans, pFans, p->uSharedMask, pCut->nLimit, pCut->pPerm, If_CutTruthW(pCut) );
+ }
+ if ( pCut->iDsd < 0 )
{
- ABC_SWAP( int, iDsd[0], iDsd[1] );
- ABC_SWAP( int, nFans[0], nFans[1] );
- ABC_SWAP( int *, pFans[0], pFans[1] );
+ pCut->fUseless = 1;
+ p->nCutsUselessAll++;
+ p->nCutsUseless[pCut->nLeaves]++;
}
- // derive new DSD
- pCut->iDsd = Dss_ManMerge( p->pDsdMan, iDsd, nFans, pFans, p->uSharedMask, pCut->nLimit, pCut->pPerm );
+ p->nCutsCountAll++;
+ p->nCutsCount[pCut->nLeaves]++;
}
// compute the application-specific cost and depth
diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c
index 4c7a1d96..c86e4381 100644
--- a/src/map/if/ifTruth.c
+++ b/src/map/if/ifTruth.c
@@ -475,6 +475,7 @@ static inline int If_CutTruthMinimize6( If_Man_t * p, If_Cut_t * pCut )
// TEMPORARY
if ( nSuppSize < 2 )
{
+//printf( "Small supp\n" );
p->nSmallSupp++;
return 2;
}
@@ -602,6 +603,7 @@ static inline int If_CutTruthMinimize2( If_Man_t * p, If_Cut_t * pCut )
// TEMPORARY
if ( nSuppSize < 2 )
{
+//printf( "Small supp\n" );
p->nSmallSupp++;
return 2;
}
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index eaaa7d2f..f4cb309a 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -657,15 +657,15 @@ static inline void Abc_TtPrintHex( word * pTruth, int nVars )
printf( "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
printf( "\n" );
}
-static inline void Abc_TtPrintHexRev( word * pTruth, int nVars )
+static inline void Abc_TtPrintHexRev( FILE * pFile, word * pTruth, int nVars )
{
word * pThis;
- int k;
+ int k, StartK = nVars >= 6 ? 16 : (1 << (nVars - 2));
assert( nVars >= 2 );
for ( pThis = pTruth + Abc_TtWordNum(nVars) - 1; pThis >= pTruth; pThis-- )
- for ( k = 15; k >= 0; k-- )
- printf( "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
- printf( "\n" );
+ for ( k = StartK - 1; k >= 0; k-- )
+ fprintf( pFile, "%c", Abc_TtPrintDigit((int)(pThis[0] >> (k << 2)) & 15) );
+// printf( "\n" );
}
static inline void Abc_TtPrintHexSpecial( word * pTruth, int nVars )
{
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h
index 7eb0b975..f80b599e 100644
--- a/src/opt/dau/dau.h
+++ b/src/opt/dau/dau.h
@@ -77,20 +77,23 @@ static inline int Dau_DsdReadVar( char * p ) { if ( *p == '!' ) p++; return *p
/*=== dauCanon.c ==========================================================*/
extern unsigned Abc_TtCanonicize( word * pTruth, int nVars, char * pCanonPerm );
/*=== dauDsd.c ==========================================================*/
-extern int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, char * pRes );
+extern int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char * pRes );
+extern void Dau_DsdPrintFromTruth( FILE * pFile, word * pTruth, int nVarsInit );
extern word * Dau_DsdToTruth( char * p, int nVars );
extern word Dau_Dsd6ToTruth( char * p );
extern void Dau_DsdNormalize( char * p );
extern int Dau_DsdCountAnds( char * pDsd );
+extern void Dau_DsdTruthCompose_rec( word * pFunc, word pFanins[DAU_MAX_VAR][DAU_MAX_WORD], word * pRes, int nVars, int nWordsR );
/*=== dauMerge.c ==========================================================*/
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 );
-/*=== dauMerge.c ==========================================================*/
-extern Dss_Man_t * Dss_ManAlloc( int nVars );
+/*=== dauTree.c ==========================================================*/
+extern Dss_Man_t * Dss_ManAlloc( int nVars, int nNonDecLimit );
extern void Dss_ManFree( Dss_Man_t * p );
-extern int Dss_ManMerge( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned uSharedMask, int nKLutSize, unsigned char * pPerm );
+extern int Dss_ManMerge( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned uSharedMask, int nKLutSize, unsigned char * pPerm, word * pTruth );
+extern void Dss_ManPrint( Dss_Man_t * p );
ABC_NAMESPACE_HEADER_END
diff --git a/src/opt/dau/dauDsd.c b/src/opt/dau/dauDsd.c
index df3dac3c..d9401895 100644
--- a/src/opt/dau/dauDsd.c
+++ b/src/opt/dau/dauDsd.c
@@ -896,7 +896,7 @@ int Dau_DsdCheck1Step( word * pTruth, int nVarsInit )
int nWords = Abc_TtWordNum(nVarsInit);
int nSizeNonDec, nSizeNonDec0, nSizeNonDec1;
int v, vBest = -2, nSumCofsBest = ABC_INFINITY, nSumCofs;
- nSizeNonDec = Dau_DsdDecompose( pTruth, nVarsInit, 0, NULL );
+ nSizeNonDec = Dau_DsdDecompose( pTruth, nVarsInit, 0, 0, NULL );
if ( nSizeNonDec == 0 )
return -1;
assert( nSizeNonDec > 0 );
@@ -905,11 +905,11 @@ int Dau_DsdCheck1Step( word * pTruth, int nVarsInit )
// try first cofactor
Abc_TtCofactor0p( pCofTemp, pTruth, nWords, v );
nSumCofs = Abc_TtSupportSize( pCofTemp, nVarsInit );
- nSizeNonDec0 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, NULL );
+ nSizeNonDec0 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, 0, NULL );
// try second cofactor
Abc_TtCofactor1p( pCofTemp, pTruth, nWords, v );
nSumCofs += Abc_TtSupportSize( pCofTemp, nVarsInit );
- nSizeNonDec1 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, NULL );
+ nSizeNonDec1 = Dau_DsdDecompose( pCofTemp, nVarsInit, 0, 0, NULL );
// compare cofactors
if ( nSizeNonDec0 || nSizeNonDec1 )
continue;
@@ -943,6 +943,7 @@ struct Dau_Dsd_t_
int nConsts; // the number of constant decompositions
int uConstMask; // constant decomposition mask
int fSplitPrime; // represent prime function as 1-step DSD
+ int fWriteTruth; // writing truth table as a hex string
char pVarDefs[32][8]; // variable definitions
char Cache[32][32]; // variable cache
char pOutput[DAU_MAX_STR]; // output stream
@@ -1023,19 +1024,19 @@ static inline int Dau_DsdWritePrime( Dau_Dsd_t * p, word * pTruth, int * pVars,
Dau_DsdWriteVar( p, pVars[vBest], 0 );
// split decomposition
Abc_TtCofactor1p( pCofTemp, pTruth, nWords, vBest );
- nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, pRes );
+ nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, p->fWriteTruth, pRes );
assert( nNonDecSize == 0 );
Dau_DsdWriteString( p, pRes );
// split decomposition
Abc_TtCofactor0p( pCofTemp, pTruth, nWords, vBest );
- nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, pRes );
+ nNonDecSize = Dau_DsdDecompose( pCofTemp, nVars, 0, p->fWriteTruth, pRes );
assert( nNonDecSize == 0 );
Dau_DsdWriteString( p, pRes );
Dau_DsdWriteString( p, ">" );
RetValue = 1;
}
}
- else
+ else if ( p->fWriteTruth )
p->nPos += Abc_TtWriteHexRev( p->pOutput + p->nPos, pTruth, nVars );
Dau_DsdWriteString( p, "{" );
for ( v = 0; v < nVars; v++ )
@@ -1333,11 +1334,15 @@ static inline int Dau_Dsd6DecomposeTripleVarsOuter( Dau_Dsd_t * p, word * pTrut
Dau_DsdDecomposeInt( p1, &tCof1, nVars - 1 );
Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput );
p->nSizeNonDec = p1->nSizeNonDec;
+ if ( p1->nSizeNonDec )
+ *pTruth = tCof1;
// split decomposition
Dau_DsdDecomposeInt( p1, &tCof0, nVars - 1 );
Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput );
Dau_DsdWriteString( p, ">" );
p->nSizeNonDec = Abc_MaxInt( p->nSizeNonDec, p1->nSizeNonDec );
+ if ( p1->nSizeNonDec )
+ *pTruth = tCof0;
return 0;
}
static inline int Dau_Dsd6DecomposeTripleVarsInner( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v, unsigned uSupports )
@@ -1693,6 +1698,7 @@ static inline int Dau_DsdDecomposeTripleVarsOuter( Dau_Dsd_t * p, word * pTruth
word pTtCof[2][DAU_MAX_WORD];
int nWords = Abc_TtWordNum(nVars);
p1->fSplitPrime = 0;
+ p1->fWriteTruth = p->fWriteTruth;
// move this variable to the top
ABC_SWAP( int, pVars[v], pVars[nVars-1] );
Abc_TtSwapVars( pTruth, nVars, v, nVars-1 );
@@ -1708,11 +1714,15 @@ static inline int Dau_DsdDecomposeTripleVarsOuter( Dau_Dsd_t * p, word * pTruth
Dau_DsdDecomposeInt( p1, pTtCof[1], nVars - 1 );
Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput );
p->nSizeNonDec = p1->nSizeNonDec;
+ if ( p1->nSizeNonDec )
+ Abc_TtCopy( pTruth, pTtCof[1], Abc_TtWordNum(p1->nSizeNonDec), 0 );
// split decomposition
Dau_DsdDecomposeInt( p1, pTtCof[0], nVars - 1 );
Dau_DsdTranslate( p, pVars, nVars - 1, p1->pOutput );
Dau_DsdWriteString( p, ">" );
p->nSizeNonDec = Abc_MaxInt( p->nSizeNonDec, p1->nSizeNonDec );
+ if ( p1->nSizeNonDec )
+ Abc_TtCopy( pTruth, pTtCof[0], Abc_TtWordNum(p1->nSizeNonDec), 0 );
return 0;
}
static inline int Dau_DsdDecomposeTripleVarsInner( Dau_Dsd_t * p, word * pTruth, int * pVars, int nVars, int v, unsigned uSupports )
@@ -1863,10 +1873,11 @@ int Dau_DsdDecomposeInt( Dau_Dsd_t * p, word * pTruth, int nVarsInit )
Dau_DsdFinalize( p );
return Status;
}
-int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, char * pRes )
+int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char * pRes )
{
Dau_Dsd_t P, * p = &P;
p->fSplitPrime = fSplitPrime;
+ p->fWriteTruth = fWriteTruth;
p->nSizeNonDec = 0;
if ( (pTruth[0] & 1) == 0 && Abc_TtIsConst0(pTruth, Abc_TtWordNum(nVarsInit)) )
{ if ( pRes ) pRes[0] = '0', pRes[1] = 0; }
@@ -1885,6 +1896,12 @@ int Dau_DsdDecompose( word * pTruth, int nVarsInit, int fSplitPrime, char * pRes
// assert( p->nSizeNonDec == 0 );
return p->nSizeNonDec;
}
+void Dau_DsdPrintFromTruth( FILE * pFile, word * pTruth, int nVarsInit )
+{
+ char pRes[DAU_MAX_STR];
+ Dau_DsdDecompose( pTruth, nVarsInit, 0, 1, pRes );
+ fprintf( pFile, "%s\n", pRes );
+}
void Dau_DsdTest44()
{
@@ -1899,7 +1916,7 @@ void Dau_DsdTest44()
// char * pStr3;
word t = Dau_Dsd6ToTruth( pStr );
// return;
- int nNonDec = Dau_DsdDecompose( &t, 6, 1, pRes );
+ int nNonDec = Dau_DsdDecompose( &t, 6, 1, 1, pRes );
// Dau_DsdNormalize( pStr2 );
// Dau_DsdExtract( pStr, 2, 0 );
t = 0;
@@ -1937,7 +1954,7 @@ void Dau_DsdTest888()
Dau_DsdPrintSupports( uSupp, nVars );
}
*/
- Status = Dau_DsdDecompose( pTruth, nVars, 0, pDsd );
+ Status = Dau_DsdDecompose( pTruth, nVars, 0, 0, pDsd );
i = 0;
}
@@ -1973,7 +1990,7 @@ void Dau_DsdTest555()
Abc_TtCopy( Tru[0], pTruth, nWords, 0 );
Abc_TtCopy( Tru[1], pTruth, nWords, 0 );
clk2 = clock();
- nSizeNonDec = Dau_DsdDecompose( Tru[1], nVars, 0, pRes );
+ nSizeNonDec = Dau_DsdDecompose( Tru[1], nVars, 0, 1, pRes );
clkDec += clock() - clk2;
Dau_DsdNormalize( pRes );
// pStr2 = Dau_DsdPerform( t ); nSizeNonDec = 0;
diff --git a/src/opt/dau/dauMerge.c b/src/opt/dau/dauMerge.c
index 2ce113be..08eaff73 100644
--- a/src/opt/dau/dauMerge.c
+++ b/src/opt/dau/dauMerge.c
@@ -717,7 +717,7 @@ Dau_DsdMergeStorePrintDefs( pS );
// assert( nVarsTotal <= 6 );
sprintf( pS->pOutput, "(%s%s)", pDsd0, pDsd1 );
pTruth = Dau_DsdToTruth( pS->pOutput, nVarsTotal );
- Status = Dau_DsdDecompose( pTruth, nVarsTotal, 0, pS->pOutput );
+ Status = Dau_DsdDecompose( pTruth, nVarsTotal, 0, 1, pS->pOutput );
//printf( "%d ", Status );
if ( Status == -1 ) // did not find 1-step DSD
return NULL;
diff --git a/src/opt/dau/dauTree.c b/src/opt/dau/dauTree.c
index d8bc8473..9e94ba29 100644
--- a/src/opt/dau/dauTree.c
+++ b/src/opt/dau/dauTree.c
@@ -58,7 +58,7 @@ struct Dss_Obj_t_
unsigned fMark1 : 1; // user mark
unsigned iVar : 8; // variable
unsigned nSupp : 8; // variable
- unsigned Data : 8; // variable
+ unsigned nWords : 8; // variable
unsigned Type : 3; // node type
unsigned nFans : 5; // fanin count
unsigned pFans[0]; // fanins
@@ -70,7 +70,7 @@ struct Dss_Ntk_t_
int nVars; // the number of variables
int nMem; // memory used
int nMemAlloc; // memory allocated
- Dss_Obj_t * pMem; // memory array
+ word * pMem; // memory array
Dss_Obj_t * pRoot; // root node
Vec_Ptr_t * vObjs; // internal nodes
};
@@ -78,6 +78,7 @@ struct Dss_Ntk_t_
struct Dss_Man_t_
{
int nVars; // variable number
+ int nNonDecLimit; // limit on non-dec size
int nBins; // table size
unsigned * pBins; // hash table
Mem_Flex_t * pMem; // memory for nodes
@@ -98,7 +99,9 @@ static inline int Dss_ObjType( Dss_Obj_t * pObj )
static inline int Dss_ObjSuppSize( Dss_Obj_t * pObj ) { return pObj->nSupp; }
static inline int Dss_ObjFaninNum( Dss_Obj_t * pObj ) { return pObj->nFans; }
static inline int Dss_ObjFaninC( Dss_Obj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return Abc_LitIsCompl(pObj->pFans[i]); }
-static inline word * Dss_ObjTruth( Dss_Obj_t * pObj ) { return (word *)(pObj->pFans + pObj->nFans + (pObj->nFans & 1)); }
+
+static inline int Dss_ObjWordNum( int nFans ) { return sizeof(Dss_Obj_t) / 8 + nFans / 2 + ((nFans & 1) > 0); }
+static inline word * Dss_ObjTruth( Dss_Obj_t * pObj ) { return (word *)pObj + pObj->nWords; }
static inline Dss_Obj_t * Dss_NtkObj( Dss_Ntk_t * p, int Id ) { return (Dss_Obj_t *)Vec_PtrEntry(p->vObjs, Id); }
static inline Dss_Obj_t * Dss_NtkConst0( Dss_Ntk_t * p ) { return Dss_NtkObj( p, 0 ); }
@@ -192,24 +195,25 @@ static inline word ** Dss_ManTtElems()
***********************************************************************/
Dss_Obj_t * Dss_ObjAllocNtk( Dss_Ntk_t * p, int Type, int nFans, int nTruthVars )
{
- int nStructs = 1 + (nFans / sizeof(Dss_Obj_t)) + (nFans % sizeof(Dss_Obj_t) > 0);
- Dss_Obj_t * pObj = p->pMem + p->nMem;
- p->nMem += nStructs;
- assert( p->nMem < p->nMemAlloc );
+ Dss_Obj_t * pObj;
+ pObj = (Dss_Obj_t *)(p->pMem + p->nMem);
Dss_ObjClean( pObj );
- pObj->Type = Type;
pObj->nFans = nFans;
+ pObj->nWords = Dss_ObjWordNum( nFans );
+ pObj->Type = Type;
pObj->Id = Vec_PtrSize( p->vObjs );
pObj->iVar = 31;
pObj->Mirror = ~0;
Vec_PtrPush( p->vObjs, pObj );
+ p->nMem += pObj->nWords + (nTruthVars ? Abc_TtWordNum(nTruthVars) : 0);
+ assert( p->nMem < p->nMemAlloc );
return pObj;
}
Dss_Obj_t * Dss_ObjCreateNtk( Dss_Ntk_t * p, int Type, Vec_Int_t * vFaninLits )
{
Dss_Obj_t * pObj;
int i, Entry;
- pObj = Dss_ObjAllocNtk( p, Type, Vec_IntSize(vFaninLits), 0 );
+ pObj = Dss_ObjAllocNtk( p, Type, Vec_IntSize(vFaninLits), Type == DAU_DSD_PRIME ? Vec_IntSize(vFaninLits) : 0 );
Vec_IntForEachEntry( vFaninLits, Entry, i )
{
pObj->pFans[i] = Entry;
@@ -226,7 +230,7 @@ Dss_Ntk_t * Dss_NtkAlloc( int nVars )
p = ABC_CALLOC( Dss_Ntk_t, 1 );
p->nVars = nVars;
p->nMemAlloc = DAU_MAX_STR;
- p->pMem = ABC_ALLOC( Dss_Obj_t, p->nMemAlloc );
+ p->pMem = ABC_ALLOC( word, p->nMemAlloc );
p->vObjs = Vec_PtrAlloc( 100 );
Dss_ObjAllocNtk( p, DAU_DSD_CONST0, 0, 0 );
for ( i = 0; i < nVars; i++ )
@@ -252,6 +256,8 @@ void Dss_NtkPrint_rec( Dss_Ntk_t * p, Dss_Obj_t * pObj )
assert( !Dss_IsComplement(pObj) );
if ( pObj->Type == DAU_DSD_VAR )
{ printf( "%c", 'a' + pObj->iVar ); return; }
+ if ( pObj->Type == DAU_DSD_PRIME )
+ Abc_TtPrintHexRev( stdout, Dss_ObjTruth(pObj), pObj->nFans );
printf( "%c", OpenType[pObj->Type] );
Dss_ObjForEachFaninNtk( p, pObj, pFanin, i )
{
@@ -311,12 +317,14 @@ int Dss_NtkCreate_rec( char * pStr, char ** p, int * pMatches, Dss_Ntk_t * pNtk
}
while ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
(*p)++;
+/*
if ( **p == '<' )
{
char * q = pStr + pMatches[ *p - pStr ];
if ( *(q+1) == '{' )
*p = q+1;
}
+*/
if ( **p >= 'a' && **p <= 'z' ) // var
return Abc_Var2Lit( Dss_ObjId(Dss_NtkVar(pNtk, **p - 'a')), fCompl );
if ( **p == '(' || **p == '[' || **p == '<' || **p == '{' ) // and/or/xor
@@ -345,7 +353,7 @@ int Dss_NtkCreate_rec( char * pStr, char ** p, int * pMatches, Dss_Ntk_t * pNtk
assert( 0 );
return -1;
}
-Dss_Ntk_t * Dss_NtkCreate( char * pDsd, int nVars )
+Dss_Ntk_t * Dss_NtkCreate( char * pDsd, int nVars, word * pTruth )
{
int fCompl = 0;
Dss_Ntk_t * pNtk = Dss_NtkAlloc( nVars );
@@ -361,6 +369,21 @@ Dss_Ntk_t * Dss_NtkCreate( char * pDsd, int nVars )
Dau_DsdMergeMatches( pDsd, pMatches );
iLit = Dss_NtkCreate_rec( pDsd, &pDsd, pMatches, pNtk );
pNtk->pRoot = Dss_Lit2ObjNtk( pNtk, iLit );
+ // assign the truth table
+ if ( pTruth )
+ {
+ Dss_Obj_t * pObj;
+ int k, Counter = 0;
+ Dss_NtkForEachNode( pNtk, pObj, k )
+ if ( pObj->Type == DAU_DSD_PRIME )
+ {
+// Kit_DsdPrintFromTruth( (unsigned *)pTruth, nVars ); printf( "\n" );
+
+ Abc_TtCopy( Dss_ObjTruth(pObj), pTruth, Abc_TtWordNum(pObj->nFans), 0 );
+ Counter++;
+ }
+ assert( Counter < 2 );
+ }
}
if ( fCompl )
pNtk->pRoot = Dss_Not(pNtk->pRoot);
@@ -477,6 +500,8 @@ void Dss_NtkTransform( Dss_Ntk_t * p, int * pPermDsd )
return;
Dss_NtkForEachNode( p, pObj, i )
{
+ if ( pObj->Type == DAU_DSD_MUX || pObj->Type == DAU_DSD_PRIME )
+ continue;
Dss_ObjForEachChildNtk( p, pObj, pChild, k )
pChildren[k] = pChild;
Dss_ObjSortNtk( p, pChildren, Dss_ObjFaninNum(pObj) );
@@ -512,8 +537,8 @@ int Dss_ObjCompare( Dss_Man_t * p, Dss_Obj_t * p0i, Dss_Obj_t * p1i )
return 1;
if ( Dss_ObjType(p0) < DAU_DSD_AND )
{
- assert( !Dss_IsComplement(p0i) );
- assert( !Dss_IsComplement(p1i) );
+// assert( !Dss_IsComplement(p0i) );
+// assert( !Dss_IsComplement(p1i) );
return 0;
}
if ( Dss_ObjFaninNum(p0) < Dss_ObjFaninNum(p1) )
@@ -565,19 +590,19 @@ void Dss_ObjSort( Dss_Man_t * p, Dss_Obj_t ** pNodes, int nNodes, int * pPerm )
***********************************************************************/
Dss_Obj_t * Dss_ObjAlloc( Dss_Man_t * p, int Type, int nFans, int nTruthVars )
{
- int nInts = sizeof(Dss_Obj_t) / sizeof(int) + nFans;
- int nWords = (nInts >> 1) + (nInts & 1) + (nTruthVars ? Abc_Truth6WordNum(nTruthVars) : 0);
+ int nWords = Dss_ObjWordNum(nFans) + (nTruthVars ? Abc_TtWordNum(nTruthVars) : 0);
Dss_Obj_t * pObj = (Dss_Obj_t *)Mem_FlexEntryFetch( p->pMem, sizeof(word) * nWords );
Dss_ObjClean( pObj );
pObj->Type = Type;
pObj->nFans = nFans;
+ pObj->nWords = Dss_ObjWordNum(nFans);
pObj->Id = Vec_PtrSize( p->vObjs );
pObj->iVar = 31;
pObj->Mirror = ~0;
Vec_PtrPush( p->vObjs, pObj );
return pObj;
}
-Dss_Obj_t * Dss_ObjCreate( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits )
+Dss_Obj_t * Dss_ObjCreate( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth )
{
Dss_Obj_t * pObj, * pFanin, * pPrev = NULL;
int i, Entry;
@@ -595,13 +620,21 @@ Dss_Obj_t * Dss_ObjCreate( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits )
pPrev = pFanin;
}
// create new node
- pObj = Dss_ObjAlloc( p, Type, Vec_IntSize(vFaninLits), 0 );
+ pObj = Dss_ObjAlloc( p, Type, Vec_IntSize(vFaninLits), Type == DAU_DSD_PRIME ? Vec_IntSize(vFaninLits) : 0 );
+ if ( Type == DAU_DSD_PRIME )
+ Abc_TtCopy( Dss_ObjTruth(pObj), pTruth, Abc_TtWordNum(Vec_IntSize(vFaninLits)), 0 );
assert( pObj->nSupp == 0 );
Vec_IntForEachEntry( vFaninLits, Entry, i )
{
pObj->pFans[i] = Entry;
pObj->nSupp += Dss_ObjFanin(p, pObj, i)->nSupp;
}
+/*
+ {
+ extern void Dss_ManPrintOne( Dss_Man_t * p, int iDsdLit, int * pPermLits );
+ Dss_ManPrintOne( p, Dss_Obj2Lit(pObj), NULL );
+ }
+*/
return pObj;
}
@@ -616,34 +649,60 @@ Dss_Obj_t * Dss_ObjCreate( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits )
SeeAlso []
***********************************************************************/
-static inline unsigned Dss_ObjHashKey( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits )
+void Dss_ManHashProfile( Dss_Man_t * p )
+{
+ Dss_Obj_t * pObj;
+ unsigned * pSpot;
+ int i, Counter;
+ for ( i = 0; i < p->nBins; i++ )
+ {
+ Counter = 0;
+ for ( pSpot = p->pBins + i; *pSpot; pSpot = &pObj->Next, Counter++ )
+ pObj = Dss_ManObj( p, *pSpot );
+ if ( Counter )
+ printf( "%d ", Counter );
+ }
+ printf( "\n" );
+}
+static inline unsigned Dss_ObjHashKey( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth )
{
static int s_Primes[8] = { 1699, 4177, 5147, 5647, 6343, 7103, 7873, 8147 };
int i, Entry;
unsigned uHash = Type * 7873 + Vec_IntSize(vFaninLits) * 8147;
Vec_IntForEachEntry( vFaninLits, Entry, i )
uHash += Entry * s_Primes[i & 0x7];
+ assert( (Type == DAU_DSD_PRIME) == (pTruth != NULL) );
+ if ( pTruth )
+ {
+ unsigned char * pTruthC = (unsigned char *)pTruth;
+ int nBytes = Abc_TtByteNum(Vec_IntSize(vFaninLits));
+ for ( i = 0; i < nBytes; i++ )
+ uHash += pTruthC[i] * s_Primes[i & 0x7];
+ }
return uHash % p->nBins;
}
-unsigned * Dss_ObjHashLookup( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits )
+unsigned * Dss_ObjHashLookup( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth )
{
Dss_Obj_t * pObj;
- unsigned * pSpot = p->pBins + Dss_ObjHashKey(p, Type, vFaninLits);
+ unsigned * pSpot = p->pBins + Dss_ObjHashKey(p, Type, vFaninLits, pTruth);
for ( ; *pSpot; pSpot = &pObj->Next )
{
pObj = Dss_ManObj( p, *pSpot );
- if ( (int)pObj->Type == Type && (int)pObj->nFans == Vec_IntSize(vFaninLits) && !memcmp(pObj->pFans, Vec_IntArray(vFaninLits), sizeof(int)*pObj->nFans) ) // equal
+ if ( (int)pObj->Type == Type &&
+ (int)pObj->nFans == Vec_IntSize(vFaninLits) &&
+ !memcmp(pObj->pFans, Vec_IntArray(vFaninLits), sizeof(int)*pObj->nFans) &&
+ (pTruth == NULL || !memcmp(Dss_ObjTruth(pObj), pTruth, Abc_TtByteNum(pObj->nFans))) ) // equal
return pSpot;
}
return pSpot;
}
-Dss_Obj_t * Dss_ObjFindOrAdd( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits )
+Dss_Obj_t * Dss_ObjFindOrAdd( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits, word * pTruth )
{
Dss_Obj_t * pObj;
- unsigned * pSpot = Dss_ObjHashLookup( p, Type, vFaninLits );
+ unsigned * pSpot = Dss_ObjHashLookup( p, Type, vFaninLits, pTruth );
if ( *pSpot )
return Dss_ManObj( p, *pSpot );
- pObj = Dss_ObjCreate( p, Type, vFaninLits );
+ pObj = Dss_ObjCreate( p, Type, vFaninLits, pTruth );
*pSpot = pObj->Id;
return pObj;
}
@@ -659,17 +718,18 @@ Dss_Obj_t * Dss_ObjFindOrAdd( Dss_Man_t * p, int Type, Vec_Int_t * vFaninLits )
SeeAlso []
***********************************************************************/
-Dss_Man_t * Dss_ManAlloc( int nVars )
+Dss_Man_t * Dss_ManAlloc( int nVars, int nNonDecLimit )
{
Dss_Man_t * p;
Dss_Obj_t * pObj;
int i;
p = ABC_CALLOC( Dss_Man_t, 1 );
p->nVars = nVars;
- p->nBins = Abc_PrimeCudd( 1000 );
+ p->nNonDecLimit = nNonDecLimit;
+ p->nBins = Abc_PrimeCudd( 100000 );
p->pBins = ABC_CALLOC( unsigned, p->nBins );
p->pMem = Mem_FlexStart();
- p->vObjs = Vec_PtrAlloc( 1000 );
+ p->vObjs = Vec_PtrAlloc( 10000 );
Dss_ObjAlloc( p, DAU_DSD_CONST0, 0, 0 );
for ( i = 0; i < nVars; i++ )
{
@@ -708,6 +768,8 @@ void Dss_ManPrint_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int * pPermLits )
printf( "%s%c", Abc_LitIsCompl(iPermLit)? "!":"", 'a' + Abc_Lit2Var(iPermLit) );
return;
}
+ if ( pObj->Type == DAU_DSD_PRIME )
+ Abc_TtPrintHexRev( stdout, Dss_ObjTruth(pObj), pObj->nFans );
printf( "%c", OpenType[pObj->Type] );
Dss_ObjForEachFanin( p, pObj, pFanin, i )
{
@@ -724,54 +786,95 @@ void Dss_ManPrintOne( Dss_Man_t * p, int iDsdLit, int * pPermLits )
Dss_ManPrint_rec( p, Dss_ManObj(p, Abc_Lit2Var(iDsdLit)), pPermLits );
printf( "\n" );
}
-void Dss_ManPrintAll( Dss_Man_t * p )
+int Dss_ManPrintIndex_rec( Dss_Man_t * p, Dss_Obj_t * pObj )
{
+ Dss_Obj_t * pFanin;
+ int i, nVarsMax = 0;
+ assert( !Dss_IsComplement(pObj) );
+ if ( pObj->Type == DAU_DSD_CONST0 )
+ return 0;
+ if ( pObj->Type == DAU_DSD_VAR )
+ return pObj->iVar + 1;
+ Dss_ObjForEachFanin( p, pObj, pFanin, i )
+ nVarsMax = Abc_MaxInt( nVarsMax, Dss_ManPrintIndex_rec(p, pFanin) );
+ return nVarsMax;
+}
+int Dss_ManCheckNonDec_rec( Dss_Man_t * p, Dss_Obj_t * pObj )
+{
+ Dss_Obj_t * pFanin;
+ int i;
+ assert( !Dss_IsComplement(pObj) );
+ if ( pObj->Type == DAU_DSD_CONST0 )
+ return 0;
+ if ( pObj->Type == DAU_DSD_VAR )
+ return 0;
+ if ( pObj->Type == DAU_DSD_PRIME )
+ return 1;
+ Dss_ObjForEachFanin( p, pObj, pFanin, i )
+ if ( Dss_ManCheckNonDec_rec( p, pFanin ) )
+ return 1;
+ return 0;
+}
+void Dss_ManDump( Dss_Man_t * p )
+{
+ char * pFileName = "dss_tts.txt";
+ FILE * pFile;
+ word Temp[DAU_MAX_WORD];
Dss_Obj_t * pObj;
- int i, nSuppMax = 0;
- printf( "DSD manager contains %d objects:\n", Vec_PtrSize(p->vObjs) );
+ int i;
+ pFile = fopen( pFileName, "wb" );
+ if ( pFile == NULL )
+ {
+ printf( "Cannot open file \"%s\".\n", pFileName );
+ return;
+ }
Dss_ManForEachObj( p, pObj, i )
{
- if ( (int)pObj->nSupp < nSuppMax )
+ if ( pObj->Type != DAU_DSD_PRIME )
continue;
- Dss_ManPrintOne( p, Dss_Obj2Lit(pObj), NULL );
- nSuppMax = Abc_MaxInt( nSuppMax, pObj->nSupp );
+ Abc_TtCopy( Temp, Dss_ObjTruth(pObj), Abc_TtWordNum(pObj->nFans), 0 );
+ Abc_TtStretch6( Temp, pObj->nFans, p->nVars );
+ fprintf( pFile, "0x" );
+ Abc_TtPrintHexRev( pFile, Temp, p->nVars );
+ fprintf( pFile, "\n" );
+
+// printf( "%6d : ", i );
+// Abc_TtPrintHexRev( stdout, Temp, p->nVars );
+// printf( " " );
+// Dau_DsdPrintFromTruth( stdout, Temp, p->nVars );
}
- printf( "\n" );
+ fclose( pFile );
}
-
-/**Function*************************************************************
-
- Synopsis []
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int Dss_NtkRebuild( Dss_Man_t * p, Dss_Ntk_t * pNtk )
+void Dss_ManPrint( Dss_Man_t * p )
{
- Dss_Obj_t * pObj, * pFanin, * pObjNew;
- int i, k;
- assert( p->nVars == pNtk->nVars );
- if ( Dss_Regular(pNtk->pRoot)->Type == DAU_DSD_CONST0 )
- return Dss_IsComplement(pNtk->pRoot);
- if ( Dss_Regular(pNtk->pRoot)->Type == DAU_DSD_VAR )
- return Abc_Var2Lit( Dss_Regular(pNtk->pRoot)->iVar, Dss_IsComplement(pNtk->pRoot) );
- Vec_IntFill( p->vCopies, Vec_PtrSize(pNtk->vObjs), -1 );
- Dss_NtkForEachNode( pNtk, pObj, i )
+ Dss_Obj_t * pObj;
+ int i, c, CountStr = 0, CountNonDsd = 0, CountNonDsdStr = 0;
+ int clk = clock();
+ Dss_ManForEachObj( p, pObj, i )
{
- Vec_IntClear( p->vLeaves );
- Dss_ObjForEachFaninNtk( pNtk, pObj, pFanin, k )
- if ( pFanin->Type == DAU_DSD_VAR )
- Vec_IntPush( p->vLeaves, Abc_Var2Lit(pFanin->iVar+1, 0) );
- else
- Vec_IntPush( p->vLeaves, Abc_Lit2Lit(Vec_IntArray(p->vCopies), pObj->pFans[k]) );
- pObjNew = Dss_ObjCreate( p, pObj->Type, p->vLeaves );
- Vec_IntWriteEntry( p->vCopies, Dss_ObjId(pObj), Dss_ObjId(pObjNew) );
+ CountStr += ((int)pObj->nSupp == Dss_ManPrintIndex_rec(p, pObj));
+ CountNonDsd += (pObj->Type == DAU_DSD_PRIME);
+ CountNonDsdStr += Dss_ManCheckNonDec_rec( p, pObj );
}
- return Abc_Lit2Lit( Vec_IntArray(p->vCopies), Dss_Obj2Lit(pNtk->pRoot) );
+ printf( "Total number of objects = %8d\n", Vec_PtrSize(p->vObjs) );
+ printf( "Total number of structures = %8d\n", CountStr );
+ printf( "Non-DSD objects (max =%2d) = %8d\n", p->nNonDecLimit, CountNonDsd );
+ printf( "Non-DSD structures = %8d\n", CountNonDsdStr );
+ printf( "Memory used for objects = %6.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) );
+ printf( "Memory used for array = %6.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) );
+ printf( "Memory used for hash table = %6.2f MB.\n", 1.0*sizeof(int)*p->nBins/(1<<20) );
+ Abc_PrintTime( 1, "Time", clock() - clk );
+// Dss_ManHashProfile( p );
+// Dss_ManDump( p );
+// return;
+ c = 0;
+ Dss_ManForEachObj( p, pObj, i )
+ if ( (int)pObj->nSupp == Dss_ManPrintIndex_rec(p, pObj) )
+ {
+ printf( "%6d : ", c++ );
+ Dss_ManPrintOne( p, Dss_Obj2Lit(pObj), NULL );
+ }
+ printf( "\n" );
}
/**Function*************************************************************
@@ -828,26 +931,33 @@ void Dss_ManComputeTruth_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int nVars, word *
}
if ( pObj->Type == DAU_DSD_PRIME ) // function
{
+ word pFanins[DAU_MAX_VAR][DAU_MAX_WORD];
+ Dss_ObjForEachChild( p, pObj, pChild, i )
+ Dss_ManComputeTruth_rec( p, pChild, nVars, pFanins[i], pPermLits );
+ Dau_DsdTruthCompose_rec( Dss_ObjTruth(pObj), pFanins, pRes, pObj->nFans, nWords );
+ if ( fCompl ) Abc_TtNot( pRes, nWords );
+ return;
}
assert( 0 );
}
word * Dss_ManComputeTruth( Dss_Man_t * p, int iDsd, int nVars, int * pPermLits )
{
- int nWords = Abc_TtWordNum( nVars );
+ Dss_Obj_t * pObj = Dss_Lit2Obj(p, iDsd);
word * pRes = p->pTtElems[DAU_MAX_VAR];
+ int nWords = Abc_TtWordNum( nVars );
assert( nVars <= DAU_MAX_VAR );
if ( iDsd == 0 )
Abc_TtConst0( pRes, nWords );
else if ( iDsd == 1 )
Abc_TtConst1( pRes, nWords );
- else if ( Abc_Lit2Var(iDsd) < p->nVars )
+ else if ( Dss_Regular(pObj)->Type == DAU_DSD_VAR )
{
- int iPermLit = pPermLits[Abc_Lit2Var(iDsd)];
+ int iPermLit = pPermLits[Dss_Regular(pObj)->iVar];
Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], nWords, Abc_LitIsCompl(iDsd) ^ Abc_LitIsCompl(iPermLit) );
}
else
- Dss_ManComputeTruth_rec( p, Dss_Lit2Obj(p, iDsd), nVars, pRes, pPermLits );
+ Dss_ManComputeTruth_rec( p, pObj, nVars, pRes, pPermLits );
return pRes;
}
@@ -888,7 +998,7 @@ Dss_Obj_t * Dss_ManShiftTree_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int Shift )
nSupp += pFanin->nSupp;
}
// create new graph
- pObjNew = Dss_ObjFindOrAdd( p, pObj->Type, vFaninLits );
+ pObjNew = Dss_ObjFindOrAdd( p, pObj->Type, vFaninLits, pObj->Type == DAU_DSD_PRIME ? Dss_ObjTruth(pObj) : NULL );
pObjNew->Mirror = pObj->Id;
Vec_IntFree( vFaninLits );
return pObjNew;
@@ -910,6 +1020,90 @@ void Dss_ManShiftTree( Dss_Man_t * p, Dss_Obj_t ** pChildren, int nChildren, Vec
/**Function*************************************************************
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+/*
+int Dss_NtkRebuild( Dss_Man_t * p, Dss_Ntk_t * pNtk )
+{
+ Dss_Obj_t * pObj, * pFanin, * pObjNew;
+ int i, k;
+ assert( p->nVars == pNtk->nVars );
+ if ( Dss_Regular(pNtk->pRoot)->Type == DAU_DSD_CONST0 )
+ return Dss_IsComplement(pNtk->pRoot);
+ if ( Dss_Regular(pNtk->pRoot)->Type == DAU_DSD_VAR )
+ return Abc_Var2Lit( Dss_Regular(pNtk->pRoot)->iVar, Dss_IsComplement(pNtk->pRoot) );
+ Vec_IntFill( p->vCopies, Vec_PtrSize(pNtk->vObjs), -1 );
+ Dss_NtkForEachNode( pNtk, pObj, i )
+ {
+ Vec_IntClear( p->vLeaves );
+ Dss_ObjForEachFaninNtk( pNtk, pObj, pFanin, k )
+ if ( pFanin->Type == DAU_DSD_VAR )
+ Vec_IntPush( p->vLeaves, Abc_Var2Lit(pFanin->iVar+1, 0) );
+ else
+ Vec_IntPush( p->vLeaves, Abc_Lit2Lit(Vec_IntArray(p->vCopies), pObj->pFans[k]) );
+ pObjNew = Dss_ObjCreate( p, pObj->Type, p->vLeaves );
+ Vec_IntWriteEntry( p->vCopies, Dss_ObjId(pObj), Dss_ObjId(pObjNew) );
+ }
+ return Abc_Lit2Lit( Vec_IntArray(p->vCopies), Dss_Obj2Lit(pNtk->pRoot) );
+}
+*/
+
+// returns literal of non-shifted tree in p, corresponding to pObj in pNtk, which may be compl
+int Dss_NtkRebuild_rec( Dss_Man_t * p, Dss_Ntk_t * pNtk, Dss_Obj_t * pObj )
+{
+ Dss_Obj_t * pChildren[DAU_MAX_VAR];
+ Dss_Obj_t * pChild, * pObjNew;
+ int k, fCompl = Dss_IsComplement(pObj);
+ pObj = Dss_Regular(pObj);
+ if ( pObj->Type == DAU_DSD_VAR )
+ return Abc_Var2Lit( 1, fCompl );
+ Dss_ObjForEachChildNtk( pNtk, pObj, pChild, k )
+ {
+ pChildren[k] = Dss_Lit2Obj( p, Dss_NtkRebuild_rec( p, pNtk, pChild ) );
+ if ( pObj->Type == DAU_DSD_XOR && Dss_IsComplement(pChildren[k]) )
+ pChildren[k] = Dss_Not(pChildren[k]), fCompl ^= 1;
+ }
+ // normalize MUX
+ if ( pObj->Type == DAU_DSD_MUX )
+ {
+ if ( Dss_IsComplement(pChildren[0]) )
+ {
+ pChildren[0] = Dss_Not(pChildren[0]);
+ ABC_SWAP( Dss_Obj_t *, pChildren[1], pChildren[2] );
+ }
+ if ( Dss_IsComplement(pChildren[1]) )
+ {
+ pChildren[1] = Dss_Not(pChildren[1]);
+ pChildren[2] = Dss_Not(pChildren[2]);
+ fCompl ^= 1;
+ }
+ }
+ // shift subgraphs
+ Dss_ManShiftTree( p, pChildren, k, p->vLeaves );
+ // create new graph
+ pObjNew = Dss_ObjFindOrAdd( p, pObj->Type, p->vLeaves, pObj->Type == DAU_DSD_PRIME ? Dss_ObjTruth(pObj) : NULL );
+ pObjNew->Mirror = pObjNew->Id;
+ return Abc_Var2Lit( pObjNew->Id, fCompl );
+}
+int Dss_NtkRebuild( Dss_Man_t * p, Dss_Ntk_t * pNtk )
+{
+ assert( p->nVars == pNtk->nVars );
+ if ( Dss_Regular(pNtk->pRoot)->Type == DAU_DSD_CONST0 )
+ return Dss_IsComplement(pNtk->pRoot);
+ if ( Dss_Regular(pNtk->pRoot)->Type == DAU_DSD_VAR )
+ return Abc_Var2Lit( Dss_Regular(pNtk->pRoot)->iVar + 1, Dss_IsComplement(pNtk->pRoot) );
+ return Dss_NtkRebuild_rec( p, pNtk, pNtk->pRoot );
+}
+
+/**Function*************************************************************
+
Synopsis [Performs DSD operation on the two literals.]
Description [Returns the perm of the resulting literals. The perm size
@@ -921,11 +1115,11 @@ void Dss_ManShiftTree( Dss_Man_t * p, Dss_Obj_t ** pChildren, int nChildren, Vec
SeeAlso []
***********************************************************************/
-int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, unsigned char * pPerm )
+int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, unsigned char * pPerm, word * pTruth )
{
Dss_Obj_t * pChildren[DAU_MAX_VAR];
Dss_Obj_t * pObj, * pChild;
- int i, k, nChildren = 0, fCompl = 0;
+ int i, k, nChildren = 0, fCompl = 0, fComplFan;
assert( Type == DAU_DSD_AND || pPerm == NULL );
if ( Type == DAU_DSD_AND && pPerm != NULL )
@@ -937,14 +1131,20 @@ int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, unsigned
pObj = Dss_Lit2Obj(p, pLits[k]);
if ( Dss_IsComplement(pObj) || pObj->Type != DAU_DSD_AND )
{
- pBegEnd[nChildren] = (nSSize << 16) | (nSSize + Dss_Regular(pObj)->nSupp);
+ fComplFan = (Dss_Regular(pObj)->Type == DAU_DSD_VAR && Dss_IsComplement(pObj));
+ if ( fComplFan )
+ pObj = Dss_Regular(pObj);
+ pBegEnd[nChildren] = (nSSize << 16) | (fComplFan << 8) | (nSSize + Dss_Regular(pObj)->nSupp);
nSSize += Dss_Regular(pObj)->nSupp;
pChildren[nChildren++] = pObj;
}
else
Dss_ObjForEachChild( p, pObj, pChild, i )
{
- pBegEnd[nChildren] = (nSSize << 16) | (nSSize + Dss_Regular(pChild)->nSupp);
+ fComplFan = (Dss_Regular(pChild)->Type == DAU_DSD_VAR && Dss_IsComplement(pChild));
+ if ( fComplFan )
+ pChild = Dss_Regular(pChild);
+ pBegEnd[nChildren] = (nSSize << 16) | (fComplFan << 8) | (nSSize + Dss_Regular(pChild)->nSupp);
nSSize += Dss_Regular(pChild)->nSupp;
pChildren[nChildren++] = pChild;
}
@@ -953,7 +1153,7 @@ int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, unsigned
// create permutation
for ( j = i = 0; i < nChildren; i++ )
for ( k = (pBegEnd[i] >> 16); k < (pBegEnd[i] & 0xFF); k++ )
- pPerm[j++] = (unsigned char)Abc_Var2Lit( k, 0 );
+ pPerm[j++] = (unsigned char)Abc_Var2Lit( k, (pBegEnd[i] >> 8) & 1 );
assert( j == nSSize );
}
else if ( Type == DAU_DSD_AND )
@@ -988,31 +1188,31 @@ int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, unsigned
}
else if ( Type == DAU_DSD_MUX )
{
- fCompl = Abc_LitIsCompl(pLits[1]) && Abc_LitIsCompl(pLits[2]);
if ( Abc_LitIsCompl(pLits[0]) )
{
- pChildren[nChildren++] = Dss_Lit2Obj(p, Abc_LitNotCond(pLits[0], 1));
- pChildren[nChildren++] = Dss_Lit2Obj(p, Abc_LitNotCond(pLits[2], fCompl));
- pChildren[nChildren++] = Dss_Lit2Obj(p, Abc_LitNotCond(pLits[1], fCompl));
+ pLits[0] = Abc_LitNot(pLits[0]);
+ ABC_SWAP( int, pLits[1], pLits[2] );
}
- else
+ if ( Abc_LitIsCompl(pLits[1]) )
{
- pChildren[nChildren++] = Dss_Lit2Obj(p, Abc_LitNotCond(pLits[0], 0));
- pChildren[nChildren++] = Dss_Lit2Obj(p, Abc_LitNotCond(pLits[1], fCompl));
- pChildren[nChildren++] = Dss_Lit2Obj(p, Abc_LitNotCond(pLits[2], fCompl));
+ pLits[1] = Abc_LitNot(pLits[1]);
+ pLits[2] = Abc_LitNot(pLits[2]);
+ fCompl ^= 1;
}
+ for ( k = 0; k < nLits; k++ )
+ pChildren[nChildren++] = Dss_Lit2Obj(p, pLits[k]);
}
else if ( Type == DAU_DSD_PRIME )
{
for ( k = 0; k < nLits; k++ )
- pChildren[nChildren++] = Dss_Lit2Obj(p, pLits[k]);
+ pChildren[nChildren++] = Dss_Lit2Obj(p, pLits[k]);
}
else assert( 0 );
// shift subgraphs
Dss_ManShiftTree( p, pChildren, nChildren, p->vLeaves );
// create new graph
- pObj = Dss_ObjFindOrAdd( p, Type, p->vLeaves );
+ pObj = Dss_ObjFindOrAdd( p, Type, p->vLeaves, pTruth );
pObj->Mirror = pObj->Id;
return Abc_Var2Lit( pObj->Id, fCompl );
}
@@ -1020,7 +1220,7 @@ Dss_Fun_t * Dss_ManOperationFun( Dss_Man_t * p, int * iDsd, int * nFans )
{
static char Buffer[100];
Dss_Fun_t * pFun = (Dss_Fun_t *)Buffer;
- pFun->iDsd = Dss_ManOperation( p, DAU_DSD_AND, iDsd, 2, pFun->pFans );
+ pFun->iDsd = Dss_ManOperation( p, DAU_DSD_AND, iDsd, 2, pFun->pFans, NULL );
pFun->nFans = nFans[0] + nFans[1];
assert( (int)pFun->nFans == Dss_ManLitSuppSize(p, pFun->iDsd) );
return pFun;
@@ -1039,7 +1239,7 @@ Dss_Fun_t * Dss_ManOperationFun( Dss_Man_t * p, int * iDsd, int * nFans )
SeeAlso []
***********************************************************************/
-Dss_Fun_t * Dss_ManBooleanAnd( Dss_Man_t * p, Dss_Ent_t * pEnt, int * nFans )
+Dss_Fun_t * Dss_ManBooleanAnd( Dss_Man_t * p, Dss_Ent_t * pEnt, int * nFans, int Counter )
{
static char Buffer[100];
Dss_Fun_t * pFun = (Dss_Fun_t *)Buffer;
@@ -1058,7 +1258,10 @@ Dss_Fun_t * Dss_ManBooleanAnd( Dss_Man_t * p, Dss_Ent_t * pEnt, int * nFans )
}
pTruthOne = Dss_ManComputeTruth( p, pEnt->iDsd0, p->nVars, pPermLits );
Abc_TtCopy( pTruth, pTruthOne, Abc_TtWordNum(p->nVars), 0 );
+if ( Counter )
+{
//Kit_DsdPrintFromTruth( pTruthOne, p->nVars ); printf( "\n" );
+}
// create second truth table
for ( i = 0; i < nFans[1]; i++ )
pPermLits[i] = -1;
@@ -1071,16 +1274,21 @@ Dss_Fun_t * Dss_ManBooleanAnd( Dss_Man_t * p, Dss_Ent_t * pEnt, int * nFans )
pPermLits[i] = Abc_Var2Lit( nSuppSize++, 0 );
}
pTruthOne = Dss_ManComputeTruth( p, pEnt->iDsd1, p->nVars, pPermLits );
+if ( Counter )
+{
//Kit_DsdPrintFromTruth( pTruthOne, p->nVars ); printf( "\n" );
+}
Abc_TtAnd( pTruth, pTruth, pTruthOne, Abc_TtWordNum(p->nVars), 0 );
// perform decomposition
- nNonDec = Dau_DsdDecompose( pTruth, nSuppSize, 0, pDsd );
+ nNonDec = Dau_DsdDecompose( pTruth, nSuppSize, 0, 0, pDsd );
+ if ( p->nNonDecLimit && nNonDec > p->nNonDecLimit )
+ return NULL;
// derive network and convert it into the manager
- pNtk = Dss_NtkCreate( pDsd, p->nVars );
-Dss_NtkPrint( pNtk );
+ pNtk = Dss_NtkCreate( pDsd, p->nVars, nNonDec ? pTruth : NULL );
+//Dss_NtkPrint( pNtk );
Dss_NtkCheck( pNtk );
Dss_NtkTransform( pNtk, pPermDsd );
-Dss_NtkPrint( pNtk );
+//Dss_NtkPrint( pNtk );
pFun->iDsd = Dss_NtkRebuild( p, pNtk );
Dss_NtkFree( pNtk );
// pPermDsd maps vars of iDsdRes into literals of pTruth
@@ -1131,12 +1339,32 @@ Dss_Ent_t * Dss_ManSharedMap( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFa
return pEnt;
}
// merge two DSD functions
-int Dss_ManMerge( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned uSharedMask, int nKLutSize, unsigned char * pPermRes )
+int Dss_ManMerge( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned uSharedMask, int nKLutSize, unsigned char * pPermRes, word * pTruth )
{
+ int fVerbose = 0;
+ static int Counter = 0;
+// word pTtTemp[DAU_MAX_WORD];
+ word * pTruthOne;
+ int pPermResInt[DAU_MAX_VAR];
Dss_Ent_t * pEnt;
Dss_Fun_t * pFun;
int i;
+ Counter++;
+
+ if ( Counter == 122053 )
+ {
+ int s = 0;
+// fVerbose = 1;
+ }
+
assert( iDsd[0] <= iDsd[1] );
+
+if ( fVerbose )
+{
+Dss_ManPrintOne( p, iDsd[0], pFans[0] );
+Dss_ManPrintOne( p, iDsd[1], pFans[1] );
+}
+
// constant argument
if ( iDsd[0] == 0 ) return 0;
if ( iDsd[0] == 1 ) return iDsd[1];
@@ -1152,24 +1380,68 @@ int Dss_ManMerge( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned
if ( uSharedMask == 0 )
pFun = Dss_ManOperationFun( p, iDsd, nFans );
else
- pFun = Dss_ManBooleanAnd( p, pEnt, nFans );
+ pFun = Dss_ManBooleanAnd( p, pEnt, nFans, 0 );
+ if ( pFun == NULL )
+ return -1;
assert( (int)pFun->nFans == Dss_ManLitSuppSize(p, pFun->iDsd) );
assert( (int)pFun->nFans <= nKLutSize );
+/*
// create permutation
for ( i = 0; i < (int)pFun->nFans; i++ )
printf( "%d ", pFun->pFans[i] );
printf( "\n" );
-
+*/
for ( i = 0; i < (int)pFun->nFans; i++ )
if ( pFun->pFans[i] < 2 * nFans[0] ) // first dec
pPermRes[i] = (unsigned char)Dss_Lit2Lit( pFans[0], pFun->pFans[i] );
else
pPermRes[i] = (unsigned char)Dss_Lit2Lit( pFans[1], pFun->pFans[i] - 2 * nFans[0] );
-
+/*
// create permutation
for ( i = 0; i < (int)pFun->nFans; i++ )
printf( "%d ", pPermRes[i] );
printf( "\n" );
+*/
+
+
+ // perform support minimization
+ if ( uSharedMask && pFun->nFans > 1 )
+ {
+ int pVarPres[DAU_MAX_VAR];
+ int nSupp = 0;
+ for ( i = 0; i < p->nVars; i++ )
+ pVarPres[i] = -1;
+ for ( i = 0; i < (int)pFun->nFans; i++ )
+ pVarPres[ Abc_Lit2Var(pPermRes[i]) ] = i;
+ for ( i = 0; i < p->nVars; i++ )
+ if ( pVarPres[i] >= 0 )
+ pPermRes[pVarPres[i]] = Abc_Var2Lit( nSupp++, Abc_LitIsCompl(pPermRes[pVarPres[i]]) );
+ assert( nSupp == (int)pFun->nFans );
+ }
+
+ for ( i = 0; i < (int)pFun->nFans; i++ )
+ pPermResInt[i] = pPermRes[i];
+
+if ( fVerbose )
+{
+Dss_ManPrintOne( p, pFun->iDsd, pPermResInt );
+printf( "\n" );
+}
+
+if ( Counter == 134 )
+{
+ int s = 0;
+// Dss_ManPrint( p );
+}
+ pTruthOne = Dss_ManComputeTruth( p, pFun->iDsd, p->nVars, pPermResInt );
+ if ( !Abc_TtEqual( pTruthOne, pTruth, Abc_TtWordNum(p->nVars) ) )
+ {
+ int s;
+// Kit_DsdPrintFromTruth( pTruthOne, p->nVars ); printf( "\n" );
+// Kit_DsdPrintFromTruth( pTruth, p->nVars ); printf( "\n" );
+ printf( "Verification failed.\n" );
+ s = 0;
+ }
return pFun->iDsd;
}
@@ -1231,7 +1503,7 @@ void Dau_DsdTest()
int nVars = 8;
// char * pDsd = "[(ab)(cd)]";
char * pDsd = "(!(a!(bh))[cde]!(fg))";
- Dss_Ntk_t * pNtk = Dss_NtkCreate( pDsd, nVars );
+ Dss_Ntk_t * pNtk = Dss_NtkCreate( pDsd, nVars, NULL );
// Dss_NtkPrint( pNtk );
// Dss_NtkCheck( pNtk );
// Dss_NtkTransform( pNtk );
@@ -1263,7 +1535,7 @@ void Dau_DsdTest_()
assert( nVars < DAU_MAX_VAR );
- p = Dss_ManAlloc( nVars );
+ p = Dss_ManAlloc( nVars, 0 );
// init
Vec_VecPushInt( vFuncs, 1, Dss_Obj2Lit(Dss_ManVar(p, 0)) );
@@ -1284,14 +1556,14 @@ void Dau_DsdTest_()
int fAddInv0 = !Dss_ObjCheckTransparent( p, Dss_ManObj(p, Abc_Lit2Var(pEntries[0])) );
int fAddInv1 = !Dss_ObjCheckTransparent( p, Dss_ManObj(p, Abc_Lit2Var(pEntries[1])) );
- iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL );
+ iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL );
assert( !Abc_LitIsCompl(iLit) );
Vec_IntPush( vRes, iLit );
if ( fAddInv0 )
{
pEntries[0] = Abc_LitNot( pEntries[0] );
- iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL );
+ iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL );
pEntries[0] = Abc_LitNot( pEntries[0] );
assert( !Abc_LitIsCompl(iLit) );
Vec_IntPush( vRes, iLit );
@@ -1300,7 +1572,7 @@ void Dau_DsdTest_()
if ( fAddInv1 )
{
pEntries[1] = Abc_LitNot( pEntries[1] );
- iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL );
+ iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL );
pEntries[1] = Abc_LitNot( pEntries[1] );
assert( !Abc_LitIsCompl(iLit) );
Vec_IntPush( vRes, iLit );
@@ -1310,14 +1582,14 @@ void Dau_DsdTest_()
{
pEntries[0] = Abc_LitNot( pEntries[0] );
pEntries[1] = Abc_LitNot( pEntries[1] );
- iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL );
+ iLit = Dss_ManOperation( p, DAU_DSD_AND, pEntries, 2, NULL, NULL );
pEntries[0] = Abc_LitNot( pEntries[0] );
pEntries[1] = Abc_LitNot( pEntries[1] );
assert( !Abc_LitIsCompl(iLit) );
Vec_IntPush( vRes, iLit );
}
- iLit = Dss_ManOperation( p, DAU_DSD_XOR, pEntries, 2, NULL );
+ iLit = Dss_ManOperation( p, DAU_DSD_XOR, pEntries, 2, NULL, NULL );
assert( !Abc_LitIsCompl(iLit) );
Vec_IntPush( vRes, iLit );
}
@@ -1342,14 +1614,14 @@ void Dau_DsdTest_()
if ( !fAddInv0 && k > j )
continue;
- iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL );
+ iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL, NULL );
assert( !Abc_LitIsCompl(iLit) );
Vec_IntPush( vRes, iLit );
if ( fAddInv1 )
{
pEntries[1] = Abc_LitNot( pEntries[1] );
- iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL );
+ iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL, NULL );
pEntries[1] = Abc_LitNot( pEntries[1] );
assert( !Abc_LitIsCompl(iLit) );
Vec_IntPush( vRes, iLit );
@@ -1358,7 +1630,7 @@ void Dau_DsdTest_()
if ( fAddInv2 )
{
pEntries[2] = Abc_LitNot( pEntries[2] );
- iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL );
+ iLit = Dss_ManOperation( p, DAU_DSD_MUX, pEntries, 3, NULL, NULL );
pEntries[2] = Abc_LitNot( pEntries[2] );
assert( !Abc_LitIsCompl(iLit) );
Vec_IntPush( vRes, iLit );
@@ -1367,7 +1639,7 @@ void Dau_DsdTest_()
}
Vec_IntUniqify( vRes );
}
- Dss_ManPrintAll( p );
+ Dss_ManPrint( p );
Dss_ManFree( p );
Vec_VecFree( vFuncs );
@@ -1387,7 +1659,7 @@ void Dau_DsdTest_()
***********************************************************************/
void Dau_DsdTest444()
{
- Dss_Man_t * p = Dss_ManAlloc( 6 );
+ Dss_Man_t * p = Dss_ManAlloc( 6, 0 );
int iLit1[3] = { 2, 4 };
int iLit2[3] = { 2, 4, 6 };
int iRes[5];
@@ -1400,10 +1672,10 @@ void Dau_DsdTest444()
unsigned uMaskShared = 2;
int i;
- iRes[0] = 1 ^ Dss_ManOperation( p, DAU_DSD_AND, iLit1, 2, NULL );
+ iRes[0] = 1 ^ Dss_ManOperation( p, DAU_DSD_AND, iLit1, 2, NULL, NULL );
iRes[1] = iRes[0];
- iRes[2] = 1 ^ Dss_ManOperation( p, DAU_DSD_AND, iRes, 2, NULL );
- iRes[3] = Dss_ManOperation( p, DAU_DSD_AND, iLit2, 3, NULL );
+ iRes[2] = 1 ^ Dss_ManOperation( p, DAU_DSD_AND, iRes, 2, NULL, NULL );
+ iRes[3] = Dss_ManOperation( p, DAU_DSD_AND, iLit2, 3, NULL, NULL );
Dss_ManPrintOne( p, iRes[0], NULL );
Dss_ManPrintOne( p, iRes[2], NULL );
@@ -1412,7 +1684,7 @@ void Dau_DsdTest444()
Dss_ManPrintOne( p, iRes[2], pPermLits1 );
Dss_ManPrintOne( p, iRes[3], pPermLits2 );
- iRes[4] = Dss_ManMerge( p, iRes+2, nFans, pPermLits, uMaskShared, 6, pPermRes );
+ iRes[4] = Dss_ManMerge( p, iRes+2, nFans, pPermLits, uMaskShared, 6, pPermRes, NULL );
for ( i = 0; i < 6; i++ )
pPermResInt[i] = pPermRes[i];
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-03 00:27:46 +0000