summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abci/abc.c14
-rw-r--r--src/map/if/if.h6
-rw-r--r--src/map/if/ifCut.c3
-rw-r--r--src/map/if/ifMan.c17
-rw-r--r--src/map/if/ifMap.c19
-rw-r--r--src/misc/util/abc_global.h1
-rw-r--r--src/opt/dau/dau.h6
-rw-r--r--src/opt/dau/dauTree.c483
8 files changed, 525 insertions, 24 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 89d1c6dd..5fa4d7fd 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -14890,6 +14890,13 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->nLutSize = pPars->nGateSize;
}
+ if ( pPars->fUseDsd )
+ {
+ pPars->fTruth = 1;
+ pPars->fCutMin = 1;
+ pPars->fUsePerm = 1;
+ }
+
if ( pPars->fUserRecLib )
{
if ( Abc_NtkRecIsRunning() + Abc_NtkRecIsRunning2() + Abc_NtkRecIsRunning3() != 1 )
@@ -27461,6 +27468,13 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->nLutSize = pPars->nGateSize;
}
+ if ( pPars->fUseDsd )
+ {
+ pPars->fTruth = 1;
+ pPars->fCutMin = 1;
+ pPars->fUsePerm = 1;
+ }
+
// complain if truth tables are requested but the cut size is too large
if ( pPars->fTruth && pPars->nLutSize > IF_MAX_FUNC_LUTSIZE )
{
diff --git a/src/map/if/if.h b/src/map/if/if.h
index e8c57998..f1d78ff4 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -35,7 +35,7 @@
#include "misc/mem/mem.h"
#include "misc/tim/tim.h"
#include "misc/util/utilNam.h"
-
+#include "opt/dau/dau.h"
ABC_NAMESPACE_HEADER_START
@@ -189,6 +189,7 @@ struct If_Man_t_
Vec_Int_t * vSwitching; // switching activity of each node
Vec_Int_t ** pDriverCuts; // temporary driver cuts
int pPerm[3][IF_MAX_LUTSIZE]; // permutations
+ unsigned uSharedMask; // mask of shared variables
int nShared; // the number of shared variables
// SOP balancing
Vec_Int_t * vCover; // used to compute ISOP
@@ -218,8 +219,9 @@ struct If_Man_t_
int nCutsCount[32];
int nCutsCountAll;
int nCutsUselessAll;
- Abc_Nam_t * pNamDsd;
+// Abc_Nam_t * pNamDsd;
int iNamVar;
+ Dss_Man_t * pDsdMan;
// timing manager
Tim_Man_t * pManTim;
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index 8e89977f..ca985910 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -418,11 +418,13 @@ int If_CutMerge( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC )
p->nShared = nLimit;
pC->nLeaves = nLimit;
pC->uSign = pC0->uSign | pC1->uSign;
+ p->uSharedMask = Abc_InfoMask( nLimit );
return 1;
}
// compare two cuts with different numbers
i = k = c = s = 0;
+ p->uSharedMask = 0;
while ( 1 )
{
if ( c == nLimit ) return 0;
@@ -440,6 +442,7 @@ int If_CutMerge( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC )
}
else
{
+ p->uSharedMask |= (1 << c);
p->pPerm[0][i] = p->pPerm[1][k] = p->pPerm[2][s++] = c;
pC->pLeaves[c++] = pC0->pLeaves[i++]; k++;
if ( i == nSizeC0 ) goto FlushCut1;
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 776c5ba6..076f74d6 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -83,8 +83,10 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
p->pCutTemp = (If_Cut_t *)ABC_ALLOC( char, p->nCutBytes );
if ( pPars->fUseDsd )
{
- p->pNamDsd = Abc_NamStart( 1000, 20 );
- p->iNamVar = Abc_NamStrFindOrAdd( p->pNamDsd, "a", NULL );
+// p->pNamDsd = Abc_NamStart( 1000, 20 );
+// p->iNamVar = Abc_NamStrFindOrAdd( p->pNamDsd, "a", NULL );
+ p->pDsdMan = Dss_ManAlloc( pPars->nLutSize );
+ p->iNamVar = 2;
}
// create the constant node
@@ -150,8 +152,9 @@ void If_ManStop( If_Man_t * p )
Abc_Print( 1, "Useless cuts %2d = %9d (out of %9d) (%6.2f %%)\n", i, p->nCutsUseless[i], p->nCutsCount[i], 100.0*p->nCutsUseless[i]/(p->nCutsCount[i]+1) );
Abc_Print( 1, "Useless cuts all = %9d (out of %9d) (%6.2f %%)\n", p->nCutsUselessAll, p->nCutsCountAll, 100.0*p->nCutsUselessAll/(p->nCutsCountAll+1) );
}
- if ( p->pNamDsd )
+ if ( p->pPars->fUseDsd )
{
+/*
if ( p->pPars->fVerbose )
Abc_Print( 1, "Number of unique entries in the DSD table = %d. Memory = %.1f MB.\n",
Abc_NamObjNumMax(p->pNamDsd), 1.0*Abc_NamMemAlloc(p->pNamDsd)/(1<<20) );
@@ -161,6 +164,8 @@ void If_ManStop( If_Man_t * p )
Abc_PrintTime( 1, "Time3", s_TimeComp[3] );
// Abc_NamPrint( p->pNamDsd );
Abc_NamStop( p->pNamDsd );
+*/
+ Dss_ManFree( p->pDsdMan );
}
// Abc_PrintTime( 1, "Truth", p->timeTruth );
// Abc_Print( 1, "Small support = %d.\n", p->nSmallSupp );
@@ -427,7 +432,11 @@ void If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId )
pCut->nLeaves = 1;
pCut->pLeaves[0] = p->pPars->fLiftLeaves? (ObjId << 8) : ObjId;
pCut->uSign = If_ObjCutSign( pCut->pLeaves[0] );
- pCut->iDsd = p->iNamVar;
+ if ( p->pPars->fUseDsd )
+ {
+ pCut->iDsd = p->iNamVar;
+ pCut->pPerm[0] = 0;
+ }
// set up elementary truth table of the unit cut
if ( p->pPars->fTruth )
{
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 11b9449d..ad50e1cc 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -277,6 +277,10 @@ 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),
@@ -284,6 +288,21 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
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] )
+ {
+ 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 );
}
// compute the application-specific cost and depth
diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h
index 2b4e17a7..7535014b 100644
--- a/src/misc/util/abc_global.h
+++ b/src/misc/util/abc_global.h
@@ -257,6 +257,7 @@ static inline int Abc_LitIsCompl( int Lit ) { return Lit & 1;
static inline int Abc_LitNot( int Lit ) { return Lit ^ 1; }
static inline int Abc_LitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); }
static inline int Abc_LitRegular( int Lit ) { return Lit & ~01; }
+static inline int Abc_Lit2Lit( int * pMap, int Lit ) { return Abc_Var2Lit( pMap[Abc_Lit2Var(Lit)], Abc_LitIsCompl(Lit) ); }
enum Abc_VerbLevel
{
diff --git a/src/opt/dau/dau.h b/src/opt/dau/dau.h
index 782d4e89..7eb0b975 100644
--- a/src/opt/dau/dau.h
+++ b/src/opt/dau/dau.h
@@ -87,6 +87,12 @@ extern int Dau_DsdCountAnds( char * pDsd );
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 );
+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 );
+
+
ABC_NAMESPACE_HEADER_END
diff --git a/src/opt/dau/dauTree.c b/src/opt/dau/dauTree.c
index 2a817f04..d8bc8473 100644
--- a/src/opt/dau/dauTree.c
+++ b/src/opt/dau/dauTree.c
@@ -20,6 +20,7 @@
#include "dauInt.h"
#include "misc/mem/mem.h"
+#include "misc/util/utilTruth.h"
ABC_NAMESPACE_IMPL_START
@@ -27,6 +28,26 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+typedef struct Dss_Fun_t_ Dss_Fun_t;
+struct Dss_Fun_t_
+{
+ unsigned iDsd : 27; // DSD literal
+ unsigned nFans : 5; // fanin count
+ unsigned char pFans[0]; // fanins
+};
+
+typedef struct Dss_Ent_t_ Dss_Ent_t;
+struct Dss_Ent_t_
+{
+ Dss_Fun_t * pFunc;
+ Dss_Ent_t * pNext;
+ unsigned iDsd0 : 27; // dsd entry
+ unsigned nWords : 5; // total word count (struct + shared)
+ unsigned iDsd1 : 27; // dsd entry
+ unsigned nShared: 5; // shared count
+ unsigned char pShared[0]; // shared literals
+};
+
typedef struct Dss_Obj_t_ Dss_Obj_t;
struct Dss_Obj_t_
{
@@ -62,6 +83,8 @@ struct Dss_Man_t_
Mem_Flex_t * pMem; // memory for nodes
Vec_Ptr_t * vObjs; // objects
Vec_Int_t * vLeaves; // temp
+ Vec_Int_t * vCopies; // temp
+ word ** pTtElems; // elementary TTs
};
static inline Dss_Obj_t * Dss_Regular( Dss_Obj_t * p ) { return (Dss_Obj_t *)((ABC_PTRUINT_T)(p) & ~01); }
@@ -72,6 +95,7 @@ static inline int Dss_IsComplement( Dss_Obj_t * p )
static inline void Dss_ObjClean( Dss_Obj_t * pObj ) { memset( pObj, 0, sizeof(Dss_Obj_t) ); }
static inline int Dss_ObjId( Dss_Obj_t * pObj ) { return pObj->Id; }
static inline int Dss_ObjType( Dss_Obj_t * pObj ) { return pObj->Type; }
+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)); }
@@ -87,12 +111,18 @@ static inline Dss_Obj_t * Dss_ObjChildNtk( Dss_Ntk_t * p, Dss_Obj_t * pObj,int
static inline Dss_Obj_t * Dss_ManObj( Dss_Man_t * p, int Id ) { return (Dss_Obj_t *)Vec_PtrEntry(p->vObjs, Id); }
static inline Dss_Obj_t * Dss_ManConst0( Dss_Man_t * p ) { return Dss_ManObj( p, 0 ); }
static inline Dss_Obj_t * Dss_ManVar( Dss_Man_t * p, int v ) { assert( v >= 0 && v < p->nVars ); return Dss_ManObj( p, v+1 ); }
+static inline int Dss_ManLitSuppSize( Dss_Man_t * p, int iLit ) { return Dss_ManObj( p, Abc_Lit2Var(iLit) )->nSupp; }
static inline int Dss_Obj2Lit( Dss_Obj_t * pObj ) { return Abc_Var2Lit(Dss_Regular(pObj)->Id, Dss_IsComplement(pObj)); }
static inline Dss_Obj_t * Dss_Lit2Obj( Dss_Man_t * p, int iLit ) { return Dss_NotCond(Dss_ManObj(p, Abc_Lit2Var(iLit)), Abc_LitIsCompl(iLit)); }
static inline Dss_Obj_t * Dss_ObjFanin( Dss_Man_t * p, Dss_Obj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return Dss_ManObj(p, Abc_Lit2Var(pObj->pFans[i])); }
static inline Dss_Obj_t * Dss_ObjChild( Dss_Man_t * p, Dss_Obj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return Dss_Lit2Obj(p, pObj->pFans[i]); }
+static inline int Dss_EntWordNum( Dss_Ent_t * p ) { return sizeof(Dss_Ent_t) / 8 + p->nShared / 4 + ((p->nShared & 3) > 0); }
+static inline int Dss_FunWordNum( Dss_Fun_t * p ) { assert(p->nFans >= 2); return (p->nFans + 4) / 8 + (((p->nFans + 4) & 7) > 0); }
+static inline word * Dss_FunTruth( Dss_Fun_t * p ) { assert(p->nFans >= 2); return (word *)p + Dss_FunWordNum(p); }
+
+
#define Dss_NtkForEachNode( p, pObj, i ) \
Vec_PtrForEachEntryStart( Dss_Obj_t *, p->vObjs, pObj, i, p->nVars + 1 )
#define Dss_ObjForEachFaninNtk( p, pObj, pFanin, i ) \
@@ -109,6 +139,17 @@ static inline Dss_Obj_t * Dss_ObjChild( Dss_Man_t * p, Dss_Obj_t * pObj, int i
#define Dss_ObjForEachChild( p, pObj, pFanin, i ) \
for ( i = 0; (i < Dss_ObjFaninNum(pObj)) && ((pFanin) = Dss_ObjChild(p, pObj, i)); i++ )
+static inline int Dss_WordCountOnes( unsigned uWord )
+{
+ uWord = (uWord & 0x55555555) + ((uWord>>1) & 0x55555555);
+ uWord = (uWord & 0x33333333) + ((uWord>>2) & 0x33333333);
+ uWord = (uWord & 0x0F0F0F0F) + ((uWord>>4) & 0x0F0F0F0F);
+ uWord = (uWord & 0x00FF00FF) + ((uWord>>8) & 0x00FF00FF);
+ return (uWord & 0x0000FFFF) + (uWord>>16);
+}
+
+static inline int Dss_Lit2Lit( int * pMapLit, int Lit ) { return Abc_Var2Lit( Abc_Lit2Var(pMapLit[Abc_Lit2Var(Lit)]), Abc_LitIsCompl(Lit) ^ Abc_LitIsCompl(pMapLit[Abc_Lit2Var(Lit)]) ); }
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -116,6 +157,30 @@ static inline Dss_Obj_t * Dss_ObjChild( Dss_Man_t * p, Dss_Obj_t * pObj, int i
/**Function*************************************************************
+ Synopsis [Elementary truth tables.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline word ** Dss_ManTtElems()
+{
+ static word TtElems[DAU_MAX_VAR+1][DAU_MAX_WORD], * pTtElems[DAU_MAX_VAR+1] = {NULL};
+ if ( pTtElems[0] == NULL )
+ {
+ int v;
+ for ( v = 0; v <= DAU_MAX_VAR; v++ )
+ pTtElems[v] = TtElems[v];
+ Abc_TtElemInit( pTtElems, DAU_MAX_VAR );
+ }
+ return pTtElems;
+}
+
+/**Function*************************************************************
+
Synopsis [Creating DSD network.]
Description []
@@ -387,11 +452,29 @@ void Dss_NtkCheck( Dss_Ntk_t * p )
}
}
}
-void Dss_NtkTransform( Dss_Ntk_t * p )
+int Dss_NtkCollectPerm_rec( Dss_Ntk_t * p, Dss_Obj_t * pObj, int * pPermDsd, int * pnPerms )
+{
+ Dss_Obj_t * pChild;
+ int k, fCompl = Dss_IsComplement(pObj);
+ pObj = Dss_Regular( pObj );
+ if ( pObj->Type == DAU_DSD_VAR )
+ {
+ pPermDsd[*pnPerms] = Abc_Var2Lit(pObj->iVar, fCompl);
+ pObj->iVar = (*pnPerms)++;
+ return fCompl;
+ }
+ Dss_ObjForEachChildNtk( p, pObj, pChild, k )
+ if ( Dss_NtkCollectPerm_rec( p, pChild, pPermDsd, pnPerms ) )
+ pObj->pFans[k] = (unsigned char)Abc_LitRegular((int)pObj->pFans[k]);
+ return 0;
+}
+void Dss_NtkTransform( Dss_Ntk_t * p, int * pPermDsd )
{
Dss_Obj_t * pChildren[DAU_MAX_VAR];
Dss_Obj_t * pObj, * pChild;
- int i, k;
+ int i, k, nPerms;
+ if ( Dss_Regular(p->pRoot)->Type == DAU_DSD_CONST0 )
+ return;
Dss_NtkForEachNode( p, pObj, i )
{
Dss_ObjForEachChildNtk( p, pObj, pChild, k )
@@ -400,6 +483,10 @@ void Dss_NtkTransform( Dss_Ntk_t * p )
for ( k = 0; k < Dss_ObjFaninNum(pObj); k++ )
pObj->pFans[k] = Dss_Obj2Lit( pChildren[k] );
}
+ nPerms = 0;
+ if ( Dss_NtkCollectPerm_rec( p, p->pRoot, pPermDsd, &nPerms ) )
+ p->pRoot = Dss_Regular(p->pRoot);
+ assert( nPerms == (int)Dss_Regular(p->pRoot)->nSupp );
}
/**Function*************************************************************
@@ -447,7 +534,7 @@ int Dss_ObjCompare( Dss_Man_t * p, Dss_Obj_t * p0i, Dss_Obj_t * p1i )
return 1;
return 0;
}
-void Dss_ObjSort( Dss_Man_t * p, Dss_Obj_t ** pNodes, int nNodes )
+void Dss_ObjSort( Dss_Man_t * p, Dss_Obj_t ** pNodes, int nNodes, int * pPerm )
{
int i, j, best_i;
for ( i = 0; i < nNodes-1; i++ )
@@ -459,6 +546,8 @@ void Dss_ObjSort( Dss_Man_t * p, Dss_Obj_t ** pNodes, int nNodes )
if ( i == best_i )
continue;
ABC_SWAP( Dss_Obj_t *, pNodes[i], pNodes[best_i] );
+ if ( pPerm )
+ ABC_SWAP( int, pPerm[i], pPerm[best_i] );
}
}
@@ -590,18 +679,21 @@ Dss_Man_t * Dss_ManAlloc( int nVars )
pObj->Mirror = 1;
}
p->vLeaves = Vec_IntAlloc( 32 );
+ p->vCopies = Vec_IntAlloc( 32 );
+ p->pTtElems = Dss_ManTtElems();
return p;
}
void Dss_ManFree( Dss_Man_t * p )
{
+ Vec_IntFreeP( &p->vCopies );
Vec_IntFreeP( &p->vLeaves );
Vec_PtrFreeP( &p->vObjs );
Mem_FlexStop( p->pMem, 0 );
ABC_FREE( p->pBins );
ABC_FREE( p );
}
-void Dss_ManPrint_rec( Dss_Man_t * p, Dss_Obj_t * pObj )
+void Dss_ManPrint_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int * pPermLits )
{
char OpenType[7] = {0, 0, 0, '(', '[', '<', '{'};
char CloseType[7] = {0, 0, 0, ')', ']', '>', '}'};
@@ -611,20 +703,25 @@ void Dss_ManPrint_rec( Dss_Man_t * p, Dss_Obj_t * pObj )
if ( pObj->Type == DAU_DSD_CONST0 )
{ printf( "0" ); return; }
if ( pObj->Type == DAU_DSD_VAR )
- { printf( "%c", 'a' + pObj->iVar ); return; }
+ {
+ int iPermLit = pPermLits ? pPermLits[pObj->iVar] : Abc_Var2Lit(pObj->iVar, 0);
+ printf( "%s%c", Abc_LitIsCompl(iPermLit)? "!":"", 'a' + Abc_Lit2Var(iPermLit) );
+ return;
+ }
printf( "%c", OpenType[pObj->Type] );
Dss_ObjForEachFanin( p, pObj, pFanin, i )
{
printf( "%s", Dss_ObjFaninC(pObj, i) ? "!":"" );
- Dss_ManPrint_rec( p, pFanin );
+ Dss_ManPrint_rec( p, pFanin, pPermLits );
}
printf( "%c", CloseType[pObj->Type] );
}
-void Dss_ManPrintOne( Dss_Man_t * p, Dss_Obj_t * pObj )
+void Dss_ManPrintOne( Dss_Man_t * p, int iDsdLit, int * pPermLits )
{
- printf( "%6d : ", Dss_ObjId(pObj) );
- printf( "%2d ", pObj->nSupp );
- Dss_ManPrint_rec( p, pObj );
+ printf( "%6d : ", Abc_Lit2Var(iDsdLit) );
+ printf( "%2d ", Dss_ManLitSuppSize(p, iDsdLit) );
+ printf( "%s", Abc_LitIsCompl(iDsdLit) ? "!" : "" );
+ Dss_ManPrint_rec( p, Dss_ManObj(p, Abc_Lit2Var(iDsdLit)), pPermLits );
printf( "\n" );
}
void Dss_ManPrintAll( Dss_Man_t * p )
@@ -636,12 +733,124 @@ void Dss_ManPrintAll( Dss_Man_t * p )
{
if ( (int)pObj->nSupp < nSuppMax )
continue;
- Dss_ManPrintOne( p, pObj );
+ Dss_ManPrintOne( p, Dss_Obj2Lit(pObj), NULL );
nSuppMax = Abc_MaxInt( nSuppMax, pObj->nSupp );
}
printf( "\n" );
}
+/**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) );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dss_ManComputeTruth_rec( Dss_Man_t * p, Dss_Obj_t * pObj, int nVars, word * pRes, int * pPermLits )
+{
+ Dss_Obj_t * pChild;
+ int nWords = Abc_TtWordNum(nVars);
+ int i, fCompl = Dss_IsComplement(pObj);
+ pObj = Dss_Regular(pObj);
+ if ( pObj->Type == DAU_DSD_VAR )
+ {
+ int iPermLit = pPermLits[(int)pObj->iVar];
+ assert( (int)pObj->iVar < nVars );
+ Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], nWords, fCompl ^ Abc_LitIsCompl(iPermLit) );
+ return;
+ }
+ if ( pObj->Type == DAU_DSD_AND || pObj->Type == DAU_DSD_XOR )
+ {
+ word pTtTemp[DAU_MAX_WORD];
+ if ( pObj->Type == DAU_DSD_AND )
+ Abc_TtConst1( pRes, nWords );
+ else
+ Abc_TtConst0( pRes, nWords );
+ Dss_ObjForEachChild( p, pObj, pChild, i )
+ {
+ Dss_ManComputeTruth_rec( p, pChild, nVars, pTtTemp, pPermLits );
+ if ( pObj->Type == DAU_DSD_AND )
+ Abc_TtAnd( pRes, pRes, pTtTemp, nWords, 0 );
+ else
+ Abc_TtXor( pRes, pRes, pTtTemp, nWords, 0 );
+ }
+ if ( fCompl ) Abc_TtNot( pRes, nWords );
+ return;
+ }
+ if ( pObj->Type == DAU_DSD_MUX ) // mux
+ {
+ word pTtTemp[3][DAU_MAX_WORD];
+ Dss_ObjForEachChild( p, pObj, pChild, i )
+ Dss_ManComputeTruth_rec( p, pChild, nVars, pTtTemp[i], pPermLits );
+ assert( i == 3 );
+ Abc_TtMux( pRes, pTtTemp[0], pTtTemp[1], pTtTemp[2], nWords );
+ if ( fCompl ) Abc_TtNot( pRes, nWords );
+ return;
+ }
+ if ( pObj->Type == DAU_DSD_PRIME ) // function
+ {
+ }
+ assert( 0 );
+
+}
+word * Dss_ManComputeTruth( Dss_Man_t * p, int iDsd, int nVars, int * pPermLits )
+{
+ int nWords = Abc_TtWordNum( nVars );
+ word * pRes = p->pTtElems[DAU_MAX_VAR];
+ 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 )
+ {
+ int iPermLit = pPermLits[Abc_Lit2Var(iDsd)];
+ 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 );
+ return pRes;
+}
+
/**Function*************************************************************
@@ -701,33 +910,64 @@ void Dss_ManShiftTree( Dss_Man_t * p, Dss_Obj_t ** pChildren, int nChildren, Vec
/**Function*************************************************************
- Synopsis []
+ Synopsis [Performs DSD operation on the two literals.]
- Description []
+ Description [Returns the perm of the resulting literals. The perm size
+ is equal to the number of support variables. The perm variables are 0-based
+ numbers of pLits[0] followed by nLits[0]-based numbers of pLits[1].]
SideEffects []
SeeAlso []
***********************************************************************/
-int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, int * pPerm )
+int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, unsigned char * pPerm )
{
Dss_Obj_t * pChildren[DAU_MAX_VAR];
Dss_Obj_t * pObj, * pChild;
- int i, k, nChildren = 0, fCompl = 0, nSupp = 0;
+ int i, k, nChildren = 0, fCompl = 0;
- if ( Type == DAU_DSD_AND )
+ assert( Type == DAU_DSD_AND || pPerm == NULL );
+ if ( Type == DAU_DSD_AND && pPerm != NULL )
{
+ int pBegEnd[DAU_MAX_VAR];
+ int j, nSSize = 0;
for ( k = 0; k < nLits; k++ )
{
pObj = Dss_Lit2Obj(p, pLits[k]);
if ( Dss_IsComplement(pObj) || pObj->Type != DAU_DSD_AND )
+ {
+ pBegEnd[nChildren] = (nSSize << 16) | (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);
+ nSSize += Dss_Regular(pChild)->nSupp;
pChildren[nChildren++] = pChild;
+ }
}
- Dss_ObjSort( p, pChildren, nChildren );
+ Dss_ObjSort( p, pChildren, nChildren, pBegEnd );
+ // 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 );
+ assert( j == nSSize );
+ }
+ else if ( Type == DAU_DSD_AND )
+ {
+ for ( k = 0; k < nLits; k++ )
+ {
+ pObj = Dss_Lit2Obj(p, pLits[k]);
+ if ( Dss_IsComplement(pObj) || pObj->Type != DAU_DSD_AND )
+ pChildren[nChildren++] = pObj;
+ else
+ Dss_ObjForEachChild( p, pObj, pChild, i )
+ pChildren[nChildren++] = pChild;
+ }
+ Dss_ObjSort( p, pChildren, nChildren, NULL );
}
else if ( Type == DAU_DSD_XOR )
{
@@ -744,7 +984,7 @@ int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, int * pPe
pChildren[nChildren++] = pChild;
}
}
- Dss_ObjSort( p, pChildren, nChildren );
+ Dss_ObjSort( p, pChildren, nChildren, NULL );
}
else if ( Type == DAU_DSD_MUX )
{
@@ -776,6 +1016,164 @@ int Dss_ManOperation( Dss_Man_t * p, int Type, int * pLits, int nLits, int * pPe
pObj->Mirror = pObj->Id;
return Abc_Var2Lit( pObj->Id, fCompl );
}
+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->nFans = nFans[0] + nFans[1];
+ assert( (int)pFun->nFans == Dss_ManLitSuppSize(p, pFun->iDsd) );
+ return pFun;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs AND on two DSD functions with support overlap.]
+
+ Description [Returns the perm of the resulting literals. The perm size
+ is equal to the number of support variables. The perm variables are 0-based
+ numbers of pLits[0] followed by nLits[0]-based numbers of pLits[1].]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Dss_Fun_t * Dss_ManBooleanAnd( Dss_Man_t * p, Dss_Ent_t * pEnt, int * nFans )
+{
+ static char Buffer[100];
+ Dss_Fun_t * pFun = (Dss_Fun_t *)Buffer;
+ Dss_Ntk_t * pNtk;
+ word * pTruthOne, pTruth[DAU_MAX_WORD];
+ char pDsd[DAU_MAX_STR];
+ int pMapDsd2Truth[DAU_MAX_VAR];
+ int pPermLits[DAU_MAX_VAR];
+ int pPermDsd[DAU_MAX_VAR];
+ int i, nNonDec, nSuppSize = 0;
+ // create first truth table
+ for ( i = 0; i < nFans[0]; i++ )
+ {
+ pMapDsd2Truth[nSuppSize] = i;
+ pPermLits[i] = Abc_Var2Lit( nSuppSize++, 0 );
+ }
+ pTruthOne = Dss_ManComputeTruth( p, pEnt->iDsd0, p->nVars, pPermLits );
+ Abc_TtCopy( pTruth, pTruthOne, Abc_TtWordNum(p->nVars), 0 );
+//Kit_DsdPrintFromTruth( pTruthOne, p->nVars ); printf( "\n" );
+ // create second truth table
+ for ( i = 0; i < nFans[1]; i++ )
+ pPermLits[i] = -1;
+ for ( i = 0; i < (int)pEnt->nShared; i++ )
+ pPermLits[pEnt->pShared[2*i+0]] = pEnt->pShared[2*i+1];
+ for ( i = 0; i < nFans[1]; i++ )
+ if ( pPermLits[i] == -1 )
+ {
+ pMapDsd2Truth[nSuppSize] = nFans[0] + i;
+ pPermLits[i] = Abc_Var2Lit( nSuppSize++, 0 );
+ }
+ pTruthOne = Dss_ManComputeTruth( p, pEnt->iDsd1, p->nVars, pPermLits );
+//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 );
+ // derive network and convert it into the manager
+ pNtk = Dss_NtkCreate( pDsd, p->nVars );
+Dss_NtkPrint( pNtk );
+ Dss_NtkCheck( pNtk );
+ Dss_NtkTransform( pNtk, pPermDsd );
+Dss_NtkPrint( pNtk );
+ pFun->iDsd = Dss_NtkRebuild( p, pNtk );
+ Dss_NtkFree( pNtk );
+ // pPermDsd maps vars of iDsdRes into literals of pTruth
+ // translate this map into the one that maps vars of iDsdRes into literals of cut
+ pFun->nFans = Dss_ManLitSuppSize( p, pFun->iDsd );
+ for ( i = 0; i < (int)pFun->nFans; i++ )
+ pFun->pFans[i] = (unsigned char)Abc_Lit2Lit( pMapDsd2Truth, pPermDsd[i] );
+ return pFun;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+// returns mapping of variables of dsd1 into literals of dsd0
+Dss_Ent_t * Dss_ManSharedMap( Dss_Man_t * p, int * iDsd, int * nFans, int ** pFans, unsigned uSharedMask )
+{
+ static char Buffer[100];
+ Dss_Ent_t * pEnt = (Dss_Ent_t *)Buffer;
+ pEnt->iDsd0 = iDsd[0];
+ pEnt->iDsd1 = iDsd[1];
+ pEnt->nShared = 0;
+ if ( uSharedMask )
+ {
+ int i, g, pMapGtoL[DAU_MAX_VAR] = {-1};
+ for ( i = 0; i < nFans[0]; i++ )
+ pMapGtoL[ Abc_Lit2Var(pFans[0][i]) ] = Abc_Var2Lit( i, Abc_LitIsCompl(pFans[0][i]) );
+ for ( i = 0; i < nFans[1]; i++ )
+ {
+ g = Abc_Lit2Var( pFans[1][i] );
+ if ( (uSharedMask >> g) & 1 )
+ {
+ assert( pMapGtoL[g] >= 0 );
+ pEnt->pShared[2*pEnt->nShared+0] = (unsigned char)i;
+ pEnt->pShared[2*pEnt->nShared+1] = (unsigned char)Abc_LitNotCond( pMapGtoL[g], Abc_LitIsCompl(pFans[1][i]) );
+ pEnt->nShared++;
+ }
+ }
+ }
+ pEnt->nWords = Dss_EntWordNum( pEnt );
+ 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 )
+{
+ Dss_Ent_t * pEnt;
+ Dss_Fun_t * pFun;
+ int i;
+ assert( iDsd[0] <= iDsd[1] );
+ // constant argument
+ if ( iDsd[0] == 0 ) return 0;
+ if ( iDsd[0] == 1 ) return iDsd[1];
+ if ( iDsd[1] == 0 ) return 0;
+ if ( iDsd[1] == 1 ) return iDsd[0];
+ // no overlap
+ assert( nFans[0] == Dss_ManLitSuppSize(p, iDsd[0]) );
+ assert( nFans[1] == Dss_ManLitSuppSize(p, iDsd[1]) );
+ assert( nFans[0] + nFans[1] <= nKLutSize + Dss_WordCountOnes(uSharedMask) );
+ // create map of shared variables
+ pEnt = Dss_ManSharedMap( p, iDsd, nFans, pFans, uSharedMask );
+ // check cache
+ if ( uSharedMask == 0 )
+ pFun = Dss_ManOperationFun( p, iDsd, nFans );
+ else
+ pFun = Dss_ManBooleanAnd( p, pEnt, nFans );
+ 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" );
+
+ return pFun->iDsd;
+}
+
/**Function*************************************************************
@@ -976,6 +1374,55 @@ void Dau_DsdTest_()
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Dau_DsdTest444()
+{
+ Dss_Man_t * p = Dss_ManAlloc( 6 );
+ int iLit1[3] = { 2, 4 };
+ int iLit2[3] = { 2, 4, 6 };
+ int iRes[5];
+ int nFans[2] = { 4, 3 };
+ int pPermLits1[4] = { 0, 2, 5, 6 };
+ int pPermLits2[5] = { 2, 9, 10 };
+ int * pPermLits[2] = { pPermLits1, pPermLits2 };
+ unsigned char pPermRes[6];
+ int pPermResInt[6];
+ unsigned uMaskShared = 2;
+ int i;
+
+ iRes[0] = 1 ^ Dss_ManOperation( p, DAU_DSD_AND, iLit1, 2, 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 );
+
+ Dss_ManPrintOne( p, iRes[0], NULL );
+ Dss_ManPrintOne( p, iRes[2], NULL );
+ Dss_ManPrintOne( p, iRes[3], NULL );
+
+ Dss_ManPrintOne( p, iRes[2], pPermLits1 );
+ Dss_ManPrintOne( p, iRes[3], pPermLits2 );
+
+ iRes[4] = Dss_ManMerge( p, iRes+2, nFans, pPermLits, uMaskShared, 6, pPermRes );
+
+ for ( i = 0; i < 6; i++ )
+ pPermResInt[i] = pPermRes[i];
+
+ Dss_ManPrintOne( p, iRes[4], NULL );
+ Dss_ManPrintOne( p, iRes[4], pPermResInt );
+
+ Dss_ManFree( p );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2025-05-15 21:59:56 +0000