summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaIf.c3
-rw-r--r--src/base/abci/abcIf.c2
-rw-r--r--src/map/if/if.h7
-rw-r--r--src/map/if/ifCut.c2
-rw-r--r--src/map/if/ifDsd.c41
-rw-r--r--src/map/if/ifMan.c26
-rw-r--r--src/map/if/ifMap.c19
7 files changed, 53 insertions, 47 deletions
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 1c9ecca5..2ca98785 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -1192,6 +1192,7 @@ int Gia_ManFromIfLogicFindLut( If_Man_t * pIfMan, Gia_Man_t * pNew, If_Cut_t * p
}
return RetValue;
}
+ assert( If_DsdManSuppSize(pIfMan->pIfDsdMan, pCutBest->iCutDsd) == (int)pCutBest->nLeaves );
// find the bound set
uSetOld = If_DsdManCheckXY( pIfMan->pIfDsdMan, pCutBest->iCutDsd, nLutSize, 1, 1, 0 );
// remap bound set
@@ -1313,7 +1314,7 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
word * pTruth = If_CutTruthW(pIfMan, pCutBest);
if ( pIfMan->pPars->fUseTtPerm )
for ( k = 0; k < (int)pCutBest->nLeaves; k++ )
- if ( (pCutBest->iCutDsd >> k) & 1 )
+ if ( If_CutLeafBit(pCutBest, k) )
Abc_TtFlip( pTruth, Abc_TtWordNum(pCutBest->nLimit), k );
// perform decomposition of the cut
pIfObj->iCopy = Gia_ManFromIfLogicNode( pIfMan, pNew, i, vLeaves, vLeaves2, pTruth, pIfMan->pPars->pLutStruct, vCover, vMapping, vMapping2, vPacking, (pIfMan->pPars->fEnableCheck75 || pIfMan->pPars->fEnableCheck75u), pIfMan->pPars->fEnableCheck07 );
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 301b7ae0..e53e06a7 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -500,7 +500,7 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
word * pTruth = If_CutTruthW(pIfMan, pCutBest);
if ( pIfMan->pPars->fUseTtPerm )
for ( i = 0; i < (int)pCutBest->nLeaves; i++ )
- if ( (pCutBest->iCutDsd >> i) & 1 )
+ if ( If_CutLeafBit(pCutBest, i) )
Abc_TtFlip( pTruth, Abc_TtWordNum(pCutBest->nLimit), i );
pNodeNew->pData = Kit_TruthToHop( (Hop_Man_t *)pNtkNew->pManFunc, (unsigned *)pTruth, If_CutLeaveNum(pCutBest), vCover );
}
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 2d1351b4..273119c0 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -233,10 +233,10 @@ struct If_Man_t_
int nCutsCountAll;
int nCutsUselessAll;
int nCuts5, nCuts5a;
- Vec_Mem_t * vTtMem[IF_MAX_FUNC_LUTSIZE+1]; // truth table memory and hash table
If_DsdMan_t * pIfDsdMan; // DSD manager
- Vec_Int_t * vTtDsds; // mapping of truth table into DSD
- Vec_Str_t * vTtPerms; // mapping of truth table into permutations
+ Vec_Mem_t * vTtMem[IF_MAX_FUNC_LUTSIZE+1]; // truth table memory and hash table
+ Vec_Int_t * vTtDsds[IF_MAX_FUNC_LUTSIZE+1]; // mapping of truth table into DSD
+ Vec_Str_t * vTtPerms[IF_MAX_FUNC_LUTSIZE+1]; // mapping of truth table into permutations
Hash_IntMan_t * vPairHash; // hashing pairs of truth tables
Vec_Int_t * vPairRes; // resulting truth table
Vec_Str_t * vPairPerms; // resulting permutation
@@ -543,6 +543,7 @@ extern int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLe
extern char * If_DsdManFileName( If_DsdMan_t * p );
extern int If_DsdManVarNum( If_DsdMan_t * p );
extern int If_DsdManLutSize( If_DsdMan_t * p );
+extern int If_DsdManSuppSize( If_DsdMan_t * p, int iDsd );
extern int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd );
extern unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fHighEffort, int fVerbose );
/*=== ifLib.c =============================================================*/
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index d7166baf..6715f706 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -859,7 +859,7 @@ void If_CutPrint( If_Cut_t * pCut )
unsigned i;
Abc_Print( 1, "{" );
for ( i = 0; i < pCut->nLeaves; i++ )
- Abc_Print( 1, " %s%d", ((pCut->iCutDsd >> i) & 1) ? "!":"", pCut->pLeaves[i] );
+ Abc_Print( 1, " %s%d", If_CutLeafBit(pCut, i) ? "!":"", pCut->pLeaves[i] );
Abc_Print( 1, " }\n" );
}
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index ac324d13..cb1e3bd7 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -150,6 +150,10 @@ int If_DsdManLutSize( If_DsdMan_t * p )
{
return p->LutSize;
}
+int If_DsdManSuppSize( If_DsdMan_t * p, int iDsd )
+{
+ return If_DsdVecLitSuppSize( &p->vObjs, iDsd );
+}
int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd )
{
return If_DsdVecObjMark( &p->vObjs, Abc_Lit2Var(iDsd) );
@@ -845,10 +849,10 @@ int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word
{
int objId, truthId = (Type == IF_DSD_PRIME) ? Vec_MemHashInsert(p->vTtMem[nLits], pTruth) : -1;
unsigned * pSpot = If_DsdObjHashLookup( p, Type, pLits, nLits, truthId );
-abctime clk;
+//abctime clk;
if ( *pSpot )
return (int)*pSpot;
-clk = Abc_Clock();
+//clk = Abc_Clock();
if ( p->LutSize && truthId >= 0 && truthId == Vec_PtrSize(p->vTtDecs[nLits]) )
{
Vec_Int_t * vSets = Dau_DecFindSets_int( pTruth, nLits, p->pSched );
@@ -863,7 +867,7 @@ clk = Abc_Clock();
// printf( "%d ", Gia_ManAndNum(p->pTtGia)-nObjOld );
Gia_ManAppendCo( p->pTtGia, Lit );
}
-p->timeCheck += Abc_Clock() - clk;
+//p->timeCheck += Abc_Clock() - clk;
*pSpot = Vec_PtrSize( &p->vObjs );
objId = If_DsdObjCreate( p, Type, pLits, nLits, truthId );
if ( Vec_PtrSize(&p->vObjs) > p->nBins )
@@ -1661,13 +1665,6 @@ unsigned If_DsdManCheckXY_int( If_DsdMan_t * p, int iDsd, int LutSize, int fDeri
{
If_DsdObj_t * pObj, * pTemp;
int i, Mask, iFirst;
-/*
- if ( 193 == iDsd )
- {
- int s = 0;
- If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 );
- }
-*/
pObj = If_DsdVecObj( &p->vObjs, Abc_Lit2Var(iDsd) );
if ( fVerbose )
If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 0 );
@@ -1740,7 +1737,7 @@ unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive,
unsigned uSet = If_DsdManCheckXY_int( p, iDsd, LutSize, fDerive, fVerbose );
if ( uSet == 0 && fHighEffort )
{
- abctime clk = Abc_Clock();
+// abctime clk = Abc_Clock();
int nVars = If_DsdVecLitSuppSize( &p->vObjs, iDsd );
word * pRes = If_DsdManComputeTruth( p, iDsd, NULL );
uSet = If_ManSatCheckXYall( p->pSat, LutSize, pRes, nVars, p->vTemp1 );
@@ -1749,8 +1746,7 @@ unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive,
// If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 );
// Dau_DecPrintSet( uSet, nVars, 1 );
}
-// Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
- p->timeCheck2 += Abc_Clock() - clk;
+// p->timeCheck2 += Abc_Clock() - clk;
}
return uSet;
}
@@ -1788,27 +1784,23 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char
char pDsd[DAU_MAX_STR];
int iDsd, nSizeNonDec, nSupp = 0;
int nWords = Abc_TtWordNum(nLeaves);
- abctime clk;
+ abctime clk = 0;
assert( nLeaves <= DAU_MAX_VAR );
Abc_TtCopy( pCopy, pTruth, nWords, 0 );
-clk = Abc_Clock();
+//clk = Abc_Clock();
nSizeNonDec = Dau_DsdDecompose( pCopy, nLeaves, 0, 1, pDsd );
-p->timeDsd += Abc_Clock() - clk;
-// if ( !strcmp(pDsd, "(![(!e!d)c]!(b!a))") )
-// {
-// int x = 0;
-// }
+//p->timeDsd += Abc_Clock() - clk;
if ( nSizeNonDec > 0 )
Abc_TtStretch6( pCopy, nSizeNonDec, p->nVars );
memset( pPerm, 0xFF, nLeaves );
-clk = Abc_Clock();
+//clk = Abc_Clock();
iDsd = If_DsdManAddDsd( p, pDsd, pCopy, pPerm, &nSupp );
-p->timeCanon += Abc_Clock() - clk;
+//p->timeCanon += Abc_Clock() - clk;
assert( nSupp == nLeaves );
// verify the result
-clk = Abc_Clock();
+//clk = Abc_Clock();
pRes = If_DsdManComputeTruth( p, iDsd, pPerm );
-p->timeVerify += Abc_Clock() - clk;
+//p->timeVerify += Abc_Clock() - clk;
if ( !Abc_TtEqual(pRes, pTruth, nWords) )
{
// If_DsdManPrint( p, NULL );
@@ -1821,6 +1813,7 @@ p->timeVerify += Abc_Clock() - clk;
printf( "\n" );
}
If_DsdVecObjIncRef( &p->vObjs, Abc_Lit2Var(iDsd) );
+ assert( If_DsdVecLitSuppSize(&p->vObjs, iDsd) == nLeaves );
return iDsd;
}
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 7874d7e0..7e52650d 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -92,12 +92,20 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
p->puTempW = p->pPars->fTruth? ABC_ALLOC( word, p->nTruth6Words[p->pPars->nLutSize] ) : NULL;
if ( pPars->fUseDsd )
{
- p->vTtDsds = Vec_IntAlloc( 1000 );
- Vec_IntPush( p->vTtDsds, 0 );
- Vec_IntPush( p->vTtDsds, 2 );
- p->vTtPerms = Vec_StrAlloc( 10000 );
- Vec_StrFill( p->vTtPerms, 2 * p->pPars->nLutSize, IF_BIG_CHAR );
- Vec_StrWriteEntry( p->vTtPerms, p->pPars->nLutSize, 0 );
+ for ( v = 6; v <= p->pPars->nLutSize; v++ )
+ {
+ p->vTtDsds[v] = Vec_IntAlloc( 1000 );
+ Vec_IntPush( p->vTtDsds[v], 0 );
+ Vec_IntPush( p->vTtDsds[v], 2 );
+ p->vTtPerms[v] = Vec_StrAlloc( 10000 );
+ Vec_StrFill( p->vTtPerms[v], 2 * v, IF_BIG_CHAR );
+ Vec_StrWriteEntry( p->vTtPerms[v], v, 0 );
+ }
+ for ( v = 0; v < 6; v++ )
+ {
+ p->vTtDsds[v] = p->vTtDsds[6];
+ p->vTtPerms[v] = p->vTtPerms[6];
+ }
}
if ( pPars->fUseTtPerm )
{
@@ -204,8 +212,10 @@ void If_ManStop( If_Man_t * p )
Vec_PtrFreeP( &p->vObjsRev );
Vec_PtrFreeP( &p->vLatchOrder );
Vec_IntFreeP( &p->vLags );
- Vec_IntFreeP( &p->vTtDsds );
- Vec_StrFreeP( &p->vTtPerms );
+ for ( i = 6; i <= p->pPars->nLutSize; i++ )
+ Vec_IntFreeP( &p->vTtDsds[i] );
+ for ( i = 6; i <= p->pPars->nLutSize; i++ )
+ Vec_StrFreeP( &p->vTtPerms[i] );
Vec_IntFreeP( &p->vCutData );
Vec_IntFreeP( &p->vPairRes );
Vec_StrFreeP( &p->vPairPerms );
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index f04cb201..b3bc4b70 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -208,24 +208,25 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
{
extern void If_ManCacheRecord( If_Man_t * p, int iDsd0, int iDsd1, int nShared, int iDsd );
int truthId = Abc_Lit2Var(pCut->iCutFunc);
- if ( Vec_IntSize(p->vTtDsds) <= truthId || Vec_IntEntry(p->vTtDsds, truthId) == -1 )
+ if ( Vec_IntSize(p->vTtDsds[pCut->nLeaves]) <= truthId || Vec_IntEntry(p->vTtDsds[pCut->nLeaves], 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->vTtDsds) <= truthId )
+ while ( Vec_IntSize(p->vTtDsds[pCut->nLeaves]) <= truthId )
{
- Vec_IntPush( p->vTtDsds, -1 );
- for ( v = 0; v < p->pPars->nLutSize; v++ )
- Vec_StrPush( p->vTtPerms, IF_BIG_CHAR );
+ Vec_IntPush( p->vTtDsds[pCut->nLeaves], -1 );
+ for ( v = 0; v < Abc_MaxInt(6, pCut->nLeaves); v++ )
+ Vec_StrPush( p->vTtPerms[pCut->nLeaves], IF_BIG_CHAR );
}
- Vec_IntWriteEntry( p->vTtDsds, truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) );
+ Vec_IntWriteEntry( p->vTtDsds[pCut->nLeaves], truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) );
for ( v = 0; v < (int)pCut->nLeaves; v++ )
- Vec_StrWriteEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v, (char)pCut->pPerm[v] );
+ Vec_StrWriteEntry( p->vTtPerms[pCut->nLeaves], truthId * Abc_MaxInt(6, pCut->nLeaves) + v, (char)pCut->pPerm[v] );
}
else
{
- pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vTtDsds, truthId), Abc_LitIsCompl(pCut->iCutFunc) );
+ pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vTtDsds[pCut->nLeaves], truthId), Abc_LitIsCompl(pCut->iCutFunc) );
for ( v = 0; v < (int)pCut->nLeaves; v++ )
- pCut->pPerm[v] = (unsigned char)Vec_StrEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v );
+ pCut->pPerm[v] = (unsigned char)Vec_StrEntry( p->vTtPerms[pCut->nLeaves], truthId * Abc_MaxInt(6, pCut->nLeaves) + v );
+// assert( If_DsdManSuppSize(p->pIfDsdMan, pCut->iCutDsd) == (int)pCut->nLeaves );
}
// If_ManCacheRecord( p, pCut0->iCutDsd, pCut1->iCutDsd, nShared, pCut->iCutDsd );
}
generated by cgit v1.2.3 (git 2.25.1) at 2025-11-04 13:03:18 +0000