summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2014-02-16 19:30:38 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2014-02-16 19:30:38 -0800
commit46532e6c2f3d0dabdb03daad5c55f6f732311797 (patch)
tree8ce2a3bd42c7cf9ed19ef035eecc50bfa4d65eea /src
parentea1baf6f70baec775086b0bff57a27f720ca870d (diff)
downloadabc-46532e6c2f3d0dabdb03daad5c55f6f732311797.tar.gz
abc-46532e6c2f3d0dabdb03daad5c55f6f732311797.tar.bz2
abc-46532e6c2f3d0dabdb03daad5c55f6f732311797.zip
Significant improvement to LUT mappers (if, &if).
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaIf.c12
-rw-r--r--src/base/abci/abc.c4
-rw-r--r--src/base/abci/abcIf.c8
-rw-r--r--src/base/abci/abcIfMux.c4
-rw-r--r--src/base/abci/abcRec.c8
-rw-r--r--src/base/abci/abcRec2.c6
-rw-r--r--src/base/abci/abcRec3.c32
-rw-r--r--src/base/abci/abcRenode.c44
-rw-r--r--src/map/if/if.h43
-rw-r--r--src/map/if/ifCore.c12
-rw-r--r--src/map/if/ifCut.c69
-rw-r--r--src/map/if/ifDec16.c25
-rw-r--r--src/map/if/ifMan.c41
-rw-r--r--src/map/if/ifMap.c75
-rw-r--r--src/map/if/ifSeq.c4
-rw-r--r--src/map/if/ifTime.c12
-rw-r--r--src/map/if/ifTruth.c673
-rw-r--r--src/misc/util/utilTruth.h2
-rw-r--r--src/misc/vec/vecMem.h39
-rw-r--r--src/proof/int/intCore.c2
20 files changed, 292 insertions, 823 deletions
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 51668cba..9ab57356 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -1206,7 +1206,7 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
If_Obj_t * pIfObj, * pIfLeaf;
Vec_Int_t * vMapping, * vMapping2, * vPacking = NULL;
Vec_Int_t * vLeaves, * vLeaves2, * vCover;
- word Truth = 0, * pTruthTable;
+// word Truth = 0, * pTruthTable;
int i, k, Entry;
assert( !pIfMan->pPars->fDeriveLuts || pIfMan->pPars->fTruth );
// if ( pIfMan->pPars->fEnableCheck07 )
@@ -1243,16 +1243,8 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
// perform one of the two types of mapping: with and without structures
if ( pIfMan->pPars->fDeriveLuts && pIfMan->pPars->fTruth )
{
- // adjust the truth table
- int nSize = pIfMan->pPars->nLutSize;
- pTruthTable = (word *)If_CutTruth(pCutBest);
- if ( nSize < 6 )
- {
- Truth = Gia_ManTt6Stretch( *pTruthTable, nSize );
- pTruthTable = &Truth;
- }
// perform decomposition of the cut
- pIfObj->iCopy = Gia_ManFromIfLogicNode( pIfMan, pNew, i, vLeaves, vLeaves2, pTruthTable, pIfMan->pPars->pLutStruct, vCover, vMapping, vMapping2, vPacking, (pIfMan->pPars->fEnableCheck75 || pIfMan->pPars->fEnableCheck75u), pIfMan->pPars->fEnableCheck07 );
+ pIfObj->iCopy = Gia_ManFromIfLogicNode( pIfMan, pNew, i, vLeaves, vLeaves2, If_CutTruthW(pIfMan, pCutBest), pIfMan->pPars->pLutStruct, vCover, vMapping, vMapping2, vPacking, (pIfMan->pPars->fEnableCheck75 || pIfMan->pPars->fEnableCheck75u), pIfMan->pPars->fEnableCheck07 );
pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
}
else
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1b53285a..08104383 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -15854,7 +15854,7 @@ int Abc_CommandIf( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fLutMux )
{
- extern int Abc_NtkCutCostMux( If_Cut_t * pCut );
+ extern int Abc_NtkCutCostMux( If_Man_t * p, If_Cut_t * pCut );
pPars->fCutMin = 1;
pPars->fTruth = 1;
pPars->pFuncCost = Abc_NtkCutCostMux;
@@ -30228,6 +30228,8 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
{
pPars->fTruth = 1;
pPars->fExpRed = 0;
+ if ( pPars->pLutStruct == NULL )
+ pPars->fDeriveLuts = 1;
}
// modify the subgraph recording
if ( pPars->fUserRecLib )
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index 312e0591..dd2e4d9c 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -448,17 +448,17 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
if ( pIfMan->pPars->fUseBdds )
{
// transform truth table into the BDD
- pNodeNew->pData = Kit_TruthToBdd( (DdManager *)pNtkNew->pManFunc, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), 0 ); Cudd_Ref((DdNode *)pNodeNew->pData);
+ pNodeNew->pData = Kit_TruthToBdd( (DdManager *)pNtkNew->pManFunc, If_CutTruth(pIfMan, pCutBest), If_CutLeaveNum(pCutBest), 0 ); Cudd_Ref((DdNode *)pNodeNew->pData);
}
else if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
{
// transform truth table into the BDD
- pNodeNew->pData = Kit_TruthToBdd( (DdManager *)pNtkNew->pManFunc, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), 1 ); Cudd_Ref((DdNode *)pNodeNew->pData);
+ pNodeNew->pData = Kit_TruthToBdd( (DdManager *)pNtkNew->pManFunc, If_CutTruth(pIfMan, pCutBest), If_CutLeaveNum(pCutBest), 1 ); Cudd_Ref((DdNode *)pNodeNew->pData);
}
else if ( pIfMan->pPars->fUseSops || pIfMan->pPars->nGateSize > 0 )
{
// transform truth table into the SOP
- int RetValue = Kit_TruthIsop( If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), vCover, 1 );
+ int RetValue = Kit_TruthIsop( If_CutTruth(pIfMan, pCutBest), If_CutLeaveNum(pCutBest), vCover, 1 );
assert( RetValue == 0 || RetValue == 1 );
// check the case of constant cover
if ( Vec_IntSize(vCover) == 0 || (Vec_IntSize(vCover) == 1 && Vec_IntEntry(vCover,0) == 0) )
@@ -496,7 +496,7 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
else
{
extern Hop_Obj_t * Kit_TruthToHop( Hop_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory );
- pNodeNew->pData = Kit_TruthToHop( (Hop_Man_t *)pNtkNew->pManFunc, If_CutTruth(pCutBest), If_CutLeaveNum(pCutBest), vCover );
+ pNodeNew->pData = Kit_TruthToHop( (Hop_Man_t *)pNtkNew->pManFunc, If_CutTruth(pIfMan, pCutBest), If_CutLeaveNum(pCutBest), vCover );
}
// complement the node if the cut was complemented
if ( pCutBest->fCompl )
diff --git a/src/base/abci/abcIfMux.c b/src/base/abci/abcIfMux.c
index 69098b4f..035345b6 100644
--- a/src/base/abci/abcIfMux.c
+++ b/src/base/abci/abcIfMux.c
@@ -145,7 +145,7 @@ void Abc_NtkCutCostMuxPrecompute()
SeeAlso []
***********************************************************************/
-int Abc_NtkCutCostMux( If_Cut_t * pCut )
+int Abc_NtkCutCostMux( If_Man_t * p, If_Cut_t * pCut )
{
static char uLookup[256] = {
1, // 0 0x00
@@ -407,7 +407,7 @@ int Abc_NtkCutCostMux( If_Cut_t * pCut )
};
if ( pCut->nLeaves < 3 )
return 1;
- if ( pCut->nLeaves == 3 && uLookup[0xff & *If_CutTruth(pCut)] )
+ if ( pCut->nLeaves == 3 && uLookup[0xff & *If_CutTruth(p, pCut)] )
return 1;
return (1 << pCut->nLeaves) - 1;
}
diff --git a/src/base/abci/abcRec.c b/src/base/abci/abcRec.c
index 4cc1b86e..40a05661 100644
--- a/src/base/abci/abcRec.c
+++ b/src/base/abci/abcRec.c
@@ -865,7 +865,7 @@ Hop_Obj_t * Abc_RecToHop( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut,
nLeaves = If_CutLeaveNum(pCut);
// if (nLeaves < 3)
// return Abc_NodeTruthToHop(pMan, pIfMan, pCut);
- Kit_TruthCopy(pInOut, If_CutTruth(pCut), pCut->nLimit);
+ Kit_TruthCopy(pInOut, If_CutTruth(pIfMan, pCut), pCut->nLimit);
//special cases when cut-minimization return 2, that means there is only one leaf in the cut.
if ((Kit_TruthIsConst0(pInOut, nLeaves) && pCut->fCompl == 0) || (Kit_TruthIsConst1(pInOut, nLeaves) && pCut->fCompl == 1))
return Hop_ManConst0(pMan);
@@ -2513,7 +2513,7 @@ void Abc_NtkRecBackUpCut(If_Cut_t* pCut)
s_pMan->tempNleaves = pCut->nLeaves;
for (i = 0; i < (int)pCut->nLeaves; i++)
s_pMan->pTempleaves[i] = pCut->pLeaves[i];
- Kit_TruthCopy(s_pMan->pTempTruth, pCut->pTruth, s_pMan->nVars);
+// Kit_TruthCopy(s_pMan->pTempTruth, pCut->pTruth, s_pMan->nVars);
}
/**Function*************************************************************
@@ -2534,7 +2534,7 @@ void Abc_NtkRecRestoreCut(If_Cut_t* pCut)
pCut->nLeaves = s_pMan->tempNleaves;
for (i = 0; i < (int)pCut->nLeaves; i++)
pCut->pLeaves[i] = s_pMan->pTempleaves[i];
- Kit_TruthCopy(pCut->pTruth ,s_pMan->pTempTruth, s_pMan->nVars);
+// Kit_TruthCopy(pCut->pTruth ,s_pMan->pTempTruth, s_pMan->nVars);
}
/**Function*************************************************************
@@ -2791,7 +2791,7 @@ int If_CutDelayRecCost(If_Man_t* p, If_Cut_t* pCut, If_Obj_t * pObj)
nLeaves = If_CutLeaveNum(pCut);
s_pMan->nFunsTried++;
assert( nLeaves >= 2 && nLeaves <= nVars );
- Kit_TruthCopy(pInOut, If_CutTruth(pCut), nLeaves);
+ Kit_TruthCopy(pInOut, If_CutTruth(p, pCut), nLeaves);
//if not every variables are in the support, skip this cut.
if ( Kit_TruthSupport(pInOut, nLeaves) != Kit_BitMask(nLeaves) )
{
diff --git a/src/base/abci/abcRec2.c b/src/base/abci/abcRec2.c
index cdc1fe13..c62068c2 100644
--- a/src/base/abci/abcRec2.c
+++ b/src/base/abci/abcRec2.c
@@ -1858,7 +1858,7 @@ int If_CutDelayRecCost2(If_Man_t* p, If_Cut_t* pCut, If_Obj_t * pObj)
nLeaves = If_CutLeaveNum(pCut);
s_pMan->nFunsTried++;
assert( nLeaves >= 2 && nLeaves <= nVars );
- Kit_TruthCopy(pInOut, If_CutTruth(pCut), nLeaves);
+ Kit_TruthCopy(pInOut, If_CutTruth(p, pCut), nLeaves);
//if not every variables are in the support, skip this cut.
if ( Kit_TruthSupport(pInOut, nLeaves) != Kit_BitMask(nLeaves) )
{
@@ -1980,7 +1980,7 @@ Hop_Obj_t * Abc_RecToHop2( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut,
nLeaves = If_CutLeaveNum(pCut);
// if (nLeaves < 3)
// return Abc_NodeTruthToHop(pMan, pIfMan, pCut);
- Kit_TruthCopy(pInOut, If_CutTruth(pCut), pCut->nLimit);
+ Kit_TruthCopy(pInOut, If_CutTruth(pIfMan, pCut), pCut->nLimit);
//special cases when cut-minimization return 2, that means there is only one leaf in the cut.
if ((Kit_TruthIsConst0(pInOut, nLeaves) && pCut->fCompl == 0) || (Kit_TruthIsConst1(pInOut, nLeaves) && pCut->fCompl == 1))
return Hop_ManConst0(pMan);
@@ -2093,7 +2093,7 @@ int Abc_RecToGia2( Gia_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut, If_Obj_
nLeaves = If_CutLeaveNum(pCut);
// if (nLeaves < 3)
// return Abc_NodeTruthToHop(pMan, pIfMan, pCut);
- Kit_TruthCopy(pInOut, If_CutTruth(pCut), pCut->nLimit);
+ Kit_TruthCopy(pInOut, If_CutTruth(pIfMan, pCut), pCut->nLimit);
//special cases when cut-minimization return 2, that means there is only one leaf in the cut.
if ((Kit_TruthIsConst0(pInOut, nLeaves) && pCut->fCompl == 0) || (Kit_TruthIsConst1(pInOut, nLeaves) && pCut->fCompl == 1))
return 0;
diff --git a/src/base/abci/abcRec3.c b/src/base/abci/abcRec3.c
index 8bf46feb..c0abba34 100644
--- a/src/base/abci/abcRec3.c
+++ b/src/base/abci/abcRec3.c
@@ -705,7 +705,7 @@ int Abc_NtkRecAddCut3( If_Man_t * pIfMan, If_Obj_t * pRoot, If_Cut_t * pCut )
// skip small cuts
assert( p->nVars == (int)pCut->nLimit );
- if ( nLeaves < 2 || (nLeaves == 2 && Abc_TtSupportSize(If_CutTruthW(pCut), 2) != 2) )
+ if ( nLeaves < 2 || (nLeaves == 2 && Abc_TtSupportSize(If_CutTruthW(pIfMan, pCut), 2) != 2) )
{
p->nFilterSize++;
return 1;
@@ -716,7 +716,7 @@ int Abc_NtkRecAddCut3( If_Man_t * pIfMan, If_Obj_t * pRoot, If_Cut_t * pCut )
// semi-canonicize truth table
clk = Abc_Clock();
- memcpy( p->pTemp1, If_CutTruthW(pCut), p->nWords * sizeof(word) );
+ memcpy( p->pTemp1, If_CutTruthW(pIfMan, pCut), p->nWords * sizeof(word) );
#ifdef LMS_USE_OLD_FORM
uCanonPhase = Kit_TruthSemiCanonicize( (unsigned *)p->pTemp1, (unsigned *)p->pTemp2, nLeaves, pCanonPerm );
#else
@@ -908,10 +908,9 @@ static inline int If_CutFindBestStruct( If_Man_t * pIfMan, If_Cut_t * pCut, char
int uSupport, nLeaves = If_CutLeaveNum( pCut );
word DelayProfile;
abctime clk;
- assert( nLeaves > 1 );
pCut->fUser = 1;
// compute support
- uSupport = Abc_TtSupport( If_CutTruthW(pCut), nLeaves );
+ uSupport = Abc_TtSupport( If_CutTruthW(pIfMan, pCut), nLeaves );
if ( uSupport == 0 )
{
pCut->Cost = 1;
@@ -932,7 +931,7 @@ static inline int If_CutFindBestStruct( If_Man_t * pIfMan, If_Cut_t * pCut, char
// semicanonicize the function
clk = Abc_Clock();
- memcpy( p->pTemp1, If_CutTruthW(pCut), p->nWords * sizeof(word) );
+ memcpy( p->pTemp1, If_CutTruthW(pIfMan, pCut), p->nWords * sizeof(word) );
#ifdef LMS_USE_OLD_FORM
*puCanonPhase = Kit_TruthSemiCanonicize( (unsigned *)p->pTemp1, (unsigned *)p->pTemp2, nLeaves, pCanonPerm );
#else
@@ -1018,16 +1017,15 @@ Hop_Obj_t * Abc_RecToHop3( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut,
Gia_Obj_t * pGiaPo, * pGiaTemp = NULL;
int i, uSupport, BestPo = -1, nLeaves = If_CutLeaveNum(pCut);
assert( pIfMan->pPars->fCutMin == 1 );
- assert( nLeaves > 1 );
// compute support
- uSupport = Abc_TtSupport( If_CutTruthW(pCut), nLeaves );
+ uSupport = Abc_TtSupport( If_CutTruthW(pIfMan, pCut), nLeaves );
if ( uSupport == 0 )
- return Hop_NotCond( Hop_ManConst0(pMan), (int)(*If_CutTruthW(pCut) & 1) );
+ return Hop_NotCond( Hop_ManConst0(pMan), If_CutTruthIsCompl(pCut) );
if ( !Abc_TtSuppIsMinBase(uSupport) || uSupport == 1 )
{
assert( Abc_TtSuppOnlyOne(uSupport) );
- return Hop_NotCond( Hop_IthVar(pMan, Abc_TtSuppFindFirst(uSupport)), (int)(*If_CutTruthW(pCut) & 1) );
+ return Hop_NotCond( Hop_IthVar(pMan, Abc_TtSuppFindFirst(uSupport)), If_CutTruthIsCompl(pCut) );
}
assert( Gia_WordCountOnes(uSupport) == nLeaves );
@@ -1035,15 +1033,6 @@ Hop_Obj_t * Abc_RecToHop3( Hop_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut,
If_CutFindBestStruct( pIfMan, pCut, pCanonPerm, &uCanonPhase, &BestPo );
assert( BestPo >= 0 );
pGiaPo = Gia_ManCo( pGia, BestPo );
-/*
-if ( If_CutLeaveNum(pCut) == 6 )
-{
-printf( "\n" );
-Kit_DsdPrintFromTruth( If_CutTruth(pCut), If_CutLeaveNum(pCut) ); printf( "\n" );
-//Gia_ManPrintCo( pGia, pGiaPo );
-Gia_ManPrintCone2( pGia, pGiaPo );
-}
-*/
// collect internal nodes into pGia->vTtNodes
if ( pGia->vTtNodes == NULL )
pGia->vTtNodes = Vec_IntAlloc( 256 );
@@ -1102,17 +1091,16 @@ int Abc_RecToGia3( Gia_Man_t * pMan, If_Man_t * pIfMan, If_Cut_t * pCut, Vec_Int
Gia_Obj_t * pGiaPo, * pGiaTemp = NULL;
int i, uSupport, BestPo = -1, nLeaves = If_CutLeaveNum(pCut);
assert( pIfMan->pPars->fCutMin == 1 );
- assert( nLeaves > 1 );
assert( nLeaves == Vec_IntSize(vLeaves) );
// compute support
- uSupport = Abc_TtSupport( If_CutTruthW(pCut), nLeaves );
+ uSupport = Abc_TtSupport( If_CutTruthW(pIfMan, pCut), nLeaves );
if ( uSupport == 0 )
- return Abc_LitNotCond( 0, (int)(*If_CutTruthW(pCut) & 1) );
+ return Abc_LitNotCond( 0, If_CutTruthIsCompl(pCut) );
if ( !Abc_TtSuppIsMinBase(uSupport) || uSupport == 1 )
{
assert( Abc_TtSuppOnlyOne(uSupport) );
- return Abc_LitNotCond( Vec_IntEntry(vLeaves, Abc_TtSuppFindFirst(uSupport)), (int)(*If_CutTruthW(pCut) & 1) );
+ return Abc_LitNotCond( Vec_IntEntry(vLeaves, Abc_TtSuppFindFirst(uSupport)), If_CutTruthIsCompl(pCut) );
}
assert( Gia_WordCountOnes(uSupport) == nLeaves );
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index 9fd6d0eb..3d5ebc66 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -31,11 +31,11 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
-static int Abc_NtkRenodeEvalAig( If_Cut_t * pCut );
-static int Abc_NtkRenodeEvalBdd( If_Cut_t * pCut );
-static int Abc_NtkRenodeEvalSop( If_Cut_t * pCut );
-static int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut );
-static int Abc_NtkRenodeEvalMv( If_Cut_t * pCut );
+static int Abc_NtkRenodeEvalAig( If_Man_t * p, If_Cut_t * pCut );
+static int Abc_NtkRenodeEvalBdd( If_Man_t * p, If_Cut_t * pCut );
+static int Abc_NtkRenodeEvalSop( If_Man_t * p, If_Cut_t * pCut );
+static int Abc_NtkRenodeEvalCnf( If_Man_t * p, If_Cut_t * pCut );
+static int Abc_NtkRenodeEvalMv( If_Man_t * p, If_Cut_t * pCut );
static reo_man * s_pReo = NULL;
static DdManager * s_pDd = NULL;
@@ -162,7 +162,7 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF
SeeAlso []
***********************************************************************/
-int Abc_NtkRenodeEvalAig( If_Cut_t * pCut )
+int Abc_NtkRenodeEvalAig( If_Man_t * p, If_Cut_t * pCut )
{
Kit_Graph_t * pGraph;
int i, nNodes;
@@ -171,10 +171,10 @@ extern void Kit_DsdTest( unsigned * pTruth, int nVars );
if ( If_CutLeaveNum(pCut) == 8 )
{
nDsdCounter++;
- Kit_DsdTest( If_CutTruth(pCut), If_CutLeaveNum(pCut) );
+ Kit_DsdTest( If_CutTruth(p, pCut), If_CutLeaveNum(pCut) );
}
*/
- pGraph = Kit_TruthToGraph( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory );
+ pGraph = Kit_TruthToGraph( If_CutTruth(p, pCut), If_CutLeaveNum(pCut), s_vMemory );
if ( pGraph == NULL )
{
for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
@@ -199,14 +199,14 @@ if ( If_CutLeaveNum(pCut) == 8 )
SeeAlso []
***********************************************************************/
-int Abc_NtkRenodeEvalBdd( If_Cut_t * pCut )
+int Abc_NtkRenodeEvalBdd( If_Man_t * p, If_Cut_t * pCut )
{
int pOrder[IF_MAX_LUTSIZE];
DdNode * bFunc, * bFuncNew;
int i, k, nNodes;
for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
pCut->pPerm[i] = pOrder[i] = -100;
- bFunc = Kit_TruthToBdd( s_pDd, If_CutTruth(pCut), If_CutLeaveNum(pCut), 0 ); Cudd_Ref( bFunc );
+ bFunc = Kit_TruthToBdd( s_pDd, If_CutTruth(p, pCut), If_CutLeaveNum(pCut), 0 ); Cudd_Ref( bFunc );
bFuncNew = Extra_Reorder( s_pReo, s_pDd, bFunc, pOrder ); Cudd_Ref( bFuncNew );
for ( i = k = 0; i < If_CutLeaveNum(pCut); i++ )
if ( pOrder[i] >= 0 )
@@ -228,12 +228,12 @@ int Abc_NtkRenodeEvalBdd( If_Cut_t * pCut )
SeeAlso []
***********************************************************************/
-int Abc_NtkRenodeEvalSop( If_Cut_t * pCut )
+int Abc_NtkRenodeEvalSop( If_Man_t * p, If_Cut_t * pCut )
{
int i, RetValue;
for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
pCut->pPerm[i] = 1;
- RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 1 );
+ RetValue = Kit_TruthIsop( If_CutTruth(p, pCut), If_CutLeaveNum(pCut), s_vMemory, 1 );
if ( RetValue == -1 )
return IF_COST_MAX;
assert( RetValue == 0 || RetValue == 1 );
@@ -251,22 +251,22 @@ int Abc_NtkRenodeEvalSop( If_Cut_t * pCut )
SeeAlso []
***********************************************************************/
-int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut )
+int Abc_NtkRenodeEvalCnf( If_Man_t * p, If_Cut_t * pCut )
{
int i, RetValue, nClauses;
// set internal mapper parameters
for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
pCut->pPerm[i] = 1;
// compute ISOP for the positive phase
- RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 0 );
+ RetValue = Kit_TruthIsop( If_CutTruth(p, pCut), If_CutLeaveNum(pCut), s_vMemory, 0 );
if ( RetValue == -1 )
return IF_COST_MAX;
assert( RetValue == 0 || RetValue == 1 );
nClauses = Vec_IntSize( s_vMemory );
// compute ISOP for the negative phase
- Kit_TruthNot( If_CutTruth(pCut), If_CutTruth(pCut), If_CutLeaveNum(pCut) );
- RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 0 );
- Kit_TruthNot( If_CutTruth(pCut), If_CutTruth(pCut), If_CutLeaveNum(pCut) );
+ Kit_TruthNot( If_CutTruth(p, pCut), If_CutTruth(p, pCut), If_CutLeaveNum(pCut) );
+ RetValue = Kit_TruthIsop( If_CutTruth(p, pCut), If_CutLeaveNum(pCut), s_vMemory, 0 );
+ Kit_TruthNot( If_CutTruth(p, pCut), If_CutTruth(p, pCut), If_CutLeaveNum(pCut) );
if ( RetValue == -1 )
return IF_COST_MAX;
assert( RetValue == 0 || RetValue == 1 );
@@ -285,21 +285,21 @@ int Abc_NtkRenodeEvalCnf( If_Cut_t * pCut )
SeeAlso []
***********************************************************************/
-int Abc_NtkRenodeEvalMv( If_Cut_t * pCut )
+int Abc_NtkRenodeEvalMv( If_Man_t * p, If_Cut_t * pCut )
{
int i, RetValue;
// set internal mapper parameters
for ( i = 0; i < If_CutLeaveNum(pCut); i++ )
pCut->pPerm[i] = 1;
// compute ISOP for the positive phase
- RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory, 0 );
+ RetValue = Kit_TruthIsop( If_CutTruth(p, pCut), If_CutLeaveNum(pCut), s_vMemory, 0 );
if ( RetValue == -1 )
return IF_COST_MAX;
assert( RetValue == 0 || RetValue == 1 );
// compute ISOP for the negative phase
- Kit_TruthNot( If_CutTruth(pCut), If_CutTruth(pCut), If_CutLeaveNum(pCut) );
- RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), s_vMemory2, 0 );
- Kit_TruthNot( If_CutTruth(pCut), If_CutTruth(pCut), If_CutLeaveNum(pCut) );
+ Kit_TruthNot( If_CutTruth(p, pCut), If_CutTruth(p, pCut), If_CutLeaveNum(pCut) );
+ RetValue = Kit_TruthIsop( If_CutTruth(p, pCut), If_CutLeaveNum(pCut), s_vMemory2, 0 );
+ Kit_TruthNot( If_CutTruth(p, pCut), If_CutTruth(p, pCut), If_CutLeaveNum(pCut) );
if ( RetValue == -1 )
return IF_COST_MAX;
assert( RetValue == 0 || RetValue == 1 );
diff --git a/src/map/if/if.h b/src/map/if/if.h
index 62992138..a3e921cc 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -36,6 +36,8 @@
#include "misc/tim/tim.h"
#include "misc/util/utilNam.h"
#include "opt/dau/dau.h"
+#include "misc/vec/vecMem.h"
+#include "misc/util/utilTruth.h"
ABC_NAMESPACE_HEADER_START
@@ -149,7 +151,7 @@ struct If_Par_t_
If_LibLut_t * pLutLib; // the LUT library
float * pTimesArr; // arrival times
float * pTimesReq; // required times
- int (* pFuncCost) (If_Cut_t *); // procedure to compute the user's cost of a cut
+ int (* pFuncCost) (If_Man_t *, If_Cut_t *); // procedure to compute the user's cost of a cut
int (* pFuncUser) (If_Man_t *, If_Obj_t *, If_Cut_t *); // procedure called for each cut when cut computation is finished
int (* pFuncCell) (If_Man_t *, unsigned *, int, int, char *); // procedure called for cut functions
void * pReoMan; // reordering manager
@@ -177,7 +179,6 @@ struct If_Man_t_
Vec_Ptr_t * vCos; // the primary outputs
Vec_Ptr_t * vObjs; // all objects
Vec_Ptr_t * vObjsRev; // reverse topological order of objects
-// Vec_Ptr_t * vMapped; // objects used in the mapping
Vec_Ptr_t * vTemp; // temporary array
int nObjs[IF_VOID];// the number of objects by type
// various data
@@ -191,7 +192,7 @@ struct If_Man_t_
int nCutsUsed; // the number of cuts currently used
int nCutsMerged; // the total number of cuts merged
unsigned * puTemp[4]; // used for the truth table computation
- If_Cut_t * pCutTemp; // temporary cut
+ word * puTempW; // used for the truth table computation
int SortMode; // one of the three sorting modes
int fNextRound; // set to 1 after the first round
int nChoices; // the number of choice nodes
@@ -212,7 +213,7 @@ struct If_Man_t_
int nMaxIters; // the maximum number of iterations
int Period; // the current value of the clock period (for seq mapping)
// memory management
- int nTruthWords; // the size of the truth table if allocated
+ int nTruth6Words; // the size of the truth table if allocated
int nPermWords; // the size of the permutation array (in words)
int nObjBytes; // the size of the object
int nCutBytes; // the size of the cut
@@ -232,6 +233,8 @@ struct If_Man_t_
// Abc_Nam_t * pNamDsd;
int iNamVar;
Dss_Man_t * pDsdMan;
+ Vec_Mem_t * vTtMem; // truth table memory and hash table
+ int nBestCutSmall[2];
// timing manager
Tim_Man_t * pManTim;
@@ -253,7 +256,7 @@ struct If_Cut_t_
float Edge; // the edge flow
float Power; // the power flow
float Delay; // delay of the cut
- int iDsd; // DSD ID of the cut
+ int iCutFunc; // DSD ID of the cut
unsigned uSign; // cut signature
unsigned Cost : 13; // the user's cost of the cut (related to IF_COST_MAX)
unsigned fCompl : 1; // the complemented attribute
@@ -263,7 +266,7 @@ struct If_Cut_t_
unsigned nLeaves : 8; // the number of leaves
int * pLeaves; // array of fanins
char * pPerm; // permutation
- unsigned * pTruth; // the truth table
+// unsigned * pTruth; // the truth table
};
// set of priority cut
@@ -375,8 +378,15 @@ static inline void If_ObjSetLevel( If_Obj_t * pObj, int Level ) { p
static inline void If_ObjSetCopy( If_Obj_t * pObj, void * pCopy ) { pObj->pCopy = pCopy; }
static inline void If_ObjSetChoice( If_Obj_t * pObj, If_Obj_t * pEqu ) { pObj->pEquiv = pEqu; }
+static inline int If_CutLeaveNum( If_Cut_t * pCut ) { return pCut->nLeaves; }
+static inline int * If_CutLeaves( If_Cut_t * pCut ) { return pCut->pLeaves; }
+static inline unsigned If_CutSuppMask( If_Cut_t * pCut ) { return (~(unsigned)0) >> (32-pCut->nLeaves); }
+static inline int If_CutTruthWords( int nVarsMax ) { return nVarsMax <= 5 ? 2 : (1 << (nVarsMax - 5)); }
+static inline int If_CutPermWords( int nVarsMax ) { return nVarsMax / sizeof(int) + ((nVarsMax % sizeof(int)) > 0); }
+
static inline If_Cut_t * If_ObjCutBest( If_Obj_t * pObj ) { return &pObj->CutBest; }
static inline unsigned If_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId % 31)); }
+static inline unsigned If_ObjCutSignCompute( If_Cut_t * p ) { unsigned s = 0; int i; for ( i = 0; i < If_CutLeaveNum(p); i++ ) s |= If_ObjCutSign(p->pLeaves[i]); return s; }
static inline float If_ObjArrTime( If_Obj_t * pObj ) { return If_ObjCutBest(pObj)->Delay; }
static inline void If_ObjSetArrTime( If_Obj_t * pObj, float ArrTime ) { If_ObjCutBest(pObj)->Delay = ArrTime; }
@@ -390,13 +400,11 @@ static inline void If_CutSetData( If_Cut_t * pCut, void * pData ) { *
static inline int If_CutDataInt( If_Cut_t * pCut ) { return *(int *)pCut; }
static inline void If_CutSetDataInt( If_Cut_t * pCut, int Data ) { *(int *)pCut = Data; }
-static inline int If_CutLeaveNum( If_Cut_t * pCut ) { return pCut->nLeaves; }
-static inline int * If_CutLeaves( If_Cut_t * pCut ) { return pCut->pLeaves; }
-static inline unsigned * If_CutTruth( If_Cut_t * pCut ) { return pCut->pTruth; }
-static inline word * If_CutTruthW( If_Cut_t * pCut ) { return (word *)pCut->pTruth; }
-static inline unsigned If_CutSuppMask( If_Cut_t * pCut ) { return (~(unsigned)0) >> (32-pCut->nLeaves); }
-static inline int If_CutTruthWords( int nVarsMax ) { return nVarsMax <= 5 ? 2 : (1 << (nVarsMax - 5)); }
-static inline int If_CutPermWords( int nVarsMax ) { return nVarsMax / sizeof(int) + ((nVarsMax % sizeof(int)) > 0); }
+static inline word * If_CutTruthWR( If_Man_t * p, If_Cut_t * pCut ) { return p->vTtMem ? Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(pCut->iCutFunc)) : NULL; }
+static inline unsigned * If_CutTruthR( If_Man_t * p, If_Cut_t * pCut ) { return (unsigned *)If_CutTruthWR(p, pCut); }
+static inline int If_CutTruthIsCompl( If_Cut_t * pCut ) { assert( pCut->iCutFunc >= 0 ); return Abc_LitIsCompl(pCut->iCutFunc); }
+static inline word * If_CutTruthW( If_Man_t * p, If_Cut_t * pCut ) { if ( p->vTtMem == NULL ) return NULL; assert( pCut->iCutFunc >= 0 ); Abc_TtCopy( p->puTempW, If_CutTruthWR(p, pCut), p->nTruth6Words, If_CutTruthIsCompl(pCut) ); return p->puTempW; }
+static inline unsigned * If_CutTruth( If_Man_t * p, If_Cut_t * pCut ) { return (unsigned *)If_CutTruthW(p, pCut); }
static inline float If_CutLutArea( If_Man_t * p, If_Cut_t * pCut ) { return pCut->fUser? (float)pCut->Cost : (p->pPars->pLutLib? p->pPars->pLutLib->pLutAreas[pCut->nLeaves] : (float)1.0); }
static inline float If_CutLutDelay( If_LibLut_t * p, int Size, int iPin ) { return p ? (p->fVarPinDelays ? p->pLutDelays[Size][iPin] : p->pLutDelays[Size][0]) : 1.0; }
@@ -544,9 +552,9 @@ extern void If_ManDerefNodeCutSet( If_Man_t * p, If_Obj_t * pObj );
extern void If_ManDerefChoiceCutSet( If_Man_t * p, If_Obj_t * pObj );
extern void If_ManSetupSetAll( If_Man_t * p, int nCrossCut );
/*=== ifMap.c =============================================================*/
-extern void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPreprocess );
+extern void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPreprocess, int fFirst );
extern void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPreprocess );
-extern int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPreprocess, char * pLabel );
+extern int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPreprocess, int fFirst, char * pLabel );
/*=== ifReduce.c ==========================================================*/
extern void If_ManImproveMapping( If_Man_t * p );
/*=== ifSeq.c =============================================================*/
@@ -558,12 +566,9 @@ extern int If_CutDelaySop( If_Man_t * p, If_Cut_t * pCut );
extern Vec_Wrd_t * If_CutDelaySopArray( If_Man_t * p, If_Cut_t * pCut );
extern float If_CutDelay( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut );
extern void If_CutPropagateRequired( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut, float Required );
-extern void If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut );
/*=== ifTruth.c ===========================================================*/
-extern int If_CutTruthMinimize( If_Man_t * p, If_Cut_t * pCut );
-extern void If_CutTruthPermute( unsigned * pOut, unsigned * pIn, int nVars, float * pDelays, int * pVars );
+extern void If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut );
extern int If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
-extern int If_CutComputeTruth2( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 );
/*=== ifUtil.c ============================================================*/
extern void If_ManCleanNodeCopy( If_Man_t * p );
extern void If_ManCleanCutData( If_Man_t * p );
diff --git a/src/map/if/ifCore.c b/src/map/if/ifCore.c
index 38c9c5ba..be5b49ac 100644
--- a/src/map/if/ifCore.c
+++ b/src/map/if/ifCore.c
@@ -94,20 +94,20 @@ int If_ManPerformMappingComb( If_Man_t * p )
if ( p->pPars->fPreprocess && !p->pPars->fArea )
{
// map for delay
- If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 1, "Delay" );
+ If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 1, 1, "Delay" );
// map for delay second option
p->pPars->fFancy = 1;
If_ManResetOriginalRefs( p );
- If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 1, "Delay-2" );
+ If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 1, 0, "Delay-2" );
p->pPars->fFancy = 0;
// map for area
p->pPars->fArea = 1;
If_ManResetOriginalRefs( p );
- If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 1, "Area" );
+ If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 1, 0, "Area" );
p->pPars->fArea = 0;
}
else
- If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 0, "Delay" );
+ If_ManPerformMappingRound( p, p->pPars->nCutsMax, 0, 0, 1, "Delay" );
// try to improve area by expanding and reducing the cuts
if ( p->pPars->fExpRed )
@@ -116,7 +116,7 @@ int If_ManPerformMappingComb( If_Man_t * p )
// area flow oriented mapping
for ( i = 0; i < p->pPars->nFlowIters; i++ )
{
- If_ManPerformMappingRound( p, p->pPars->nCutsMax, 1, 0, "Flow" );
+ If_ManPerformMappingRound( p, p->pPars->nCutsMax, 1, 0, 0, "Flow" );
if ( p->pPars->fExpRed )
If_ManImproveMapping( p );
}
@@ -124,7 +124,7 @@ int If_ManPerformMappingComb( If_Man_t * p )
// area oriented mapping
for ( i = 0; i < p->pPars->nAreaIters; i++ )
{
- If_ManPerformMappingRound( p, p->pPars->nCutsMax, 2, 0, "Area" );
+ If_ManPerformMappingRound( p, p->pPars->nCutsMax, 2, 0, 0, "Area" );
if ( p->pPars->fExpRed )
If_ManImproveMapping( p );
}
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index c9edc66b..9d84a496 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -421,6 +421,35 @@ int If_CutMerge( If_Man_t * p, If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t * pC )
p->uSharedMask = Abc_InfoMask( nLimit );
return 1;
}
+ // one cut is empty
+ if ( nSizeC0 == 0 )
+ {
+ assert( pC0->uSign == 0 );
+ for ( i = 0; i < nSizeC1; i++ )
+ {
+ pC->pLeaves[i] = pC1->pLeaves[i];
+ p->pPerm[1][i] = i;
+ }
+ p->nShared = 0;
+ pC->nLeaves = nSizeC1;
+ pC->uSign = pC0->uSign | pC1->uSign;
+ p->uSharedMask = 0;
+ return 1;
+ }
+ if ( nSizeC1 == 0 )
+ {
+ assert( pC1->uSign == 0 );
+ for ( i = 0; i < nSizeC0; i++ )
+ {
+ pC->pLeaves[i] = pC0->pLeaves[i];
+ p->pPerm[0][i] = i;
+ }
+ p->nShared = 0;
+ pC->nLeaves = nSizeC0;
+ pC->uSign = pC0->uSign | pC1->uSign;
+ p->uSharedMask = 0;
+ return 1;
+ }
// compare two cuts with different numbers
i = k = c = s = 0;
@@ -928,6 +957,8 @@ int If_CutCheck( If_Cut_t * pCut )
{
int i;
assert( pCut->nLeaves <= pCut->nLimit );
+ if ( pCut->nLeaves < 2 )
+ return 1;
for ( i = 1; i < (int)pCut->nLeaves; i++ )
{
if ( pCut->pLeaves[i-1] >= pCut->pLeaves[i] )
@@ -1018,17 +1049,17 @@ void If_CutCopy( If_Man_t * p, If_Cut_t * pCutDest, If_Cut_t * pCutSrc )
{
int * pLeaves;
char * pPerm;
- unsigned * pTruth;
+// unsigned * pTruth;
// save old arrays
pLeaves = pCutDest->pLeaves;
pPerm = pCutDest->pPerm;
- pTruth = pCutDest->pTruth;
+// pTruth = pCutDest->pTruth;
// copy the cut info
memcpy( pCutDest, pCutSrc, p->nCutBytes );
// restore the arrays
pCutDest->pLeaves = pLeaves;
pCutDest->pPerm = pPerm;
- pCutDest->pTruth = pTruth;
+// pCutDest->pTruth = pTruth;
}
@@ -1048,7 +1079,7 @@ float If_CutAreaFlow( If_Man_t * p, If_Cut_t * pCut )
If_Obj_t * pLeaf;
float Flow;
int i;
- assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+// assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
Flow = If_CutLutArea(p, pCut);
If_CutForEachLeaf( p, pCut, pLeaf, i )
{
@@ -1081,7 +1112,7 @@ float If_CutEdgeFlow( If_Man_t * p, If_Cut_t * pCut )
If_Obj_t * pLeaf;
float Flow;
int i;
- assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+// assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
Flow = pCut->nLeaves;
If_CutForEachLeaf( p, pCut, pLeaf, i )
{
@@ -1115,7 +1146,7 @@ float If_CutPowerFlow( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pRoot )
float * pSwitching = (float *)p->vSwitching->pArray;
float Power = 0;
int i;
- assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+// assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
If_CutForEachLeaf( p, pCut, pLeaf, i )
{
Power += pSwitching[pLeaf->Id];
@@ -1147,7 +1178,7 @@ float If_CutAverageRefs( If_Man_t * p, If_Cut_t * pCut )
{
If_Obj_t * pLeaf;
int nRefsTotal, i;
- assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+// assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
nRefsTotal = 0;
If_CutForEachLeaf( p, pCut, pLeaf, i )
nRefsTotal += pLeaf->nRefs;
@@ -1223,7 +1254,9 @@ float If_CutAreaRef( If_Man_t * p, If_Cut_t * pCut )
float If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut )
{
float aResult, aResult2;
- assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+// assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+ if ( pCut->nLeaves < 2 )
+ return 0;
aResult2 = If_CutAreaRef( p, pCut );
aResult = If_CutAreaDeref( p, pCut );
assert( aResult > aResult2 - p->fEpsilon );
@@ -1245,7 +1278,9 @@ float If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut )
float If_CutAreaRefed( If_Man_t * p, If_Cut_t * pCut )
{
float aResult, aResult2;
- assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+// assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+ if ( pCut->nLeaves < 2 )
+ return 0;
aResult2 = If_CutAreaDeref( p, pCut );
aResult = If_CutAreaRef( p, pCut );
assert( aResult > aResult2 - p->fEpsilon );
@@ -1322,7 +1357,9 @@ float If_CutEdgeRef( If_Man_t * p, If_Cut_t * pCut )
float If_CutEdgeDerefed( If_Man_t * p, If_Cut_t * pCut )
{
float aResult, aResult2;
- assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+// assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+ if ( pCut->nLeaves < 2 )
+ return pCut->nLeaves;
aResult2 = If_CutEdgeRef( p, pCut );
aResult = If_CutEdgeDeref( p, pCut );
assert( aResult > aResult2 - p->fEpsilon );
@@ -1344,7 +1381,9 @@ float If_CutEdgeDerefed( If_Man_t * p, If_Cut_t * pCut )
float If_CutEdgeRefed( If_Man_t * p, If_Cut_t * pCut )
{
float aResult, aResult2;
- assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+// assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+ if ( pCut->nLeaves < 2 )
+ return pCut->nLeaves;
aResult2 = If_CutEdgeDeref( p, pCut );
aResult = If_CutEdgeRef( p, pCut );
assert( aResult > aResult2 - p->fEpsilon );
@@ -1423,7 +1462,9 @@ float If_CutPowerRef( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pRoot )
float If_CutPowerDerefed( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pRoot )
{
float aResult, aResult2;
- assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+// assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+ if ( pCut->nLeaves < 2 )
+ return 0;
aResult2 = If_CutPowerRef( p, pCut, pRoot );
aResult = If_CutPowerDeref( p, pCut, pRoot );
assert( aResult > aResult2 - p->fEpsilon );
@@ -1445,7 +1486,9 @@ float If_CutPowerDerefed( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pRoot )
float If_CutPowerRefed( If_Man_t * p, If_Cut_t * pCut, If_Obj_t * pRoot )
{
float aResult, aResult2;
- assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+// assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+ if ( pCut->nLeaves < 2 )
+ return 0;
aResult2 = If_CutPowerDeref( p, pCut, pRoot );
aResult = If_CutPowerRef( p, pCut, pRoot );
assert( aResult > aResult2 - p->fEpsilon );
diff --git a/src/map/if/ifDec16.c b/src/map/if/ifDec16.c
index df98a916..e1339222 100644
--- a/src/map/if/ifDec16.c
+++ b/src/map/if/ifDec16.c
@@ -1752,7 +1752,7 @@ If_Grp_t If_CluCheck( If_Man_t * p, word * pTruth0, int nVars, int iVarStart, in
return G1;
}
-
+/*
static inline word Abc_Tt6Cofactor0( word t, int iVar )
{
assert( iVar >= 0 && iVar < 6 );
@@ -1763,6 +1763,7 @@ static inline word Abc_Tt6Cofactor1( word t, int iVar )
assert( iVar >= 0 && iVar < 6 );
return (t & Truth6[iVar]) | ((t & Truth6[iVar]) >> (1<<iVar));
}
+*/
int If_CluCheckDecInAny( word t, int nVars )
{
int v, u, Cof2[2], Cof4[4];
@@ -2151,7 +2152,7 @@ float If_CutDelayLutStruct( If_Man_t * p, If_Cut_t * pCut, char * pStr, float Wi
}
// derive the first group
- G1 = If_CluCheck( p, (word *)If_CutTruth(pCut), nLeaves, 0, 0, nLutLeaf, nLutRoot, NULL, NULL, NULL, NULL, 1 );
+ G1 = If_CluCheck( p, If_CutTruthW(p, pCut), nLeaves, 0, 0, nLutLeaf, nLutRoot, NULL, NULL, NULL, NULL, 1 );
if ( G1.nVars == 0 )
return ABC_INFINITY;
@@ -2247,23 +2248,9 @@ int If_CutPerformCheck16( If_Man_t * p, unsigned * pTruth, int nVars, int nLeave
}
#endif
- // if cutmin is disabled, minimize the cut
- if ( !p->pPars->fCutMin && If_CluSupportSize((word *)pTruth, nVars) < nLeaves )
- {
- If_Cut_t * pCut = p->pCutTemp;
- pCut->nLimit = nVars;
- pCut->nLeaves = nLeaves;
- pCut->pLeaves = (int *)(pCut + 1);
- for ( i = 0; i < nLeaves; i++ )
- pCut->pLeaves[i] = i;
- pCut->pTruth = (unsigned *)pCut->pLeaves + pCut->nLimit + p->nPermWords;
- If_CluCopy( (word *)If_CutTruth(pCut), (word *)pTruth, nVars );
- if ( If_CutTruthMinimize( p, pCut ) >= 2 )
- return 0;
- nLeaves = pCut->nLeaves;
-// If_CluCopy( (word *)pTruth, (word *)If_CutTruth(pCut), nVars );
- pTruth = If_CutTruth(pCut);
- }
+ // if cutmin is disabled, minimize the function
+ if ( !p->pPars->fCutMin )
+ nLeaves = Abc_TtMinBase( (word *)pTruth, NULL, nLeaves, nVars );
// quit if parameters are wrong
Length = strlen(pStr);
diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c
index 939e5a7b..3034df67 100644
--- a/src/map/if/ifMan.c
+++ b/src/map/if/ifMan.c
@@ -64,23 +64,25 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
// p->vMapped = Vec_PtrAlloc( 100 );
p->vTemp = Vec_PtrAlloc( 100 );
// prepare the memory manager
- p->nTruthWords = p->pPars->fTruth? If_CutTruthWords( p->pPars->nLutSize ) : 0;
+ p->vTtMem = p->pPars->fTruth? Vec_MemAllocForTT( p->pPars->nLutSize ) : NULL;
+ p->nTruth6Words= p->pPars->fTruth? Abc_Truth6WordNum( p->pPars->nLutSize ) : 0;
+// p->nTruthWords = p->pPars->fTruth? If_CutTruthWords( p->pPars->nLutSize ) : 0;
p->nPermWords = p->pPars->fUsePerm? If_CutPermWords( p->pPars->nLutSize ) : 0;
- p->nObjBytes = sizeof(If_Obj_t) + sizeof(int) * (p->pPars->nLutSize + p->nPermWords + p->nTruthWords);
- p->nCutBytes = sizeof(If_Cut_t) + sizeof(int) * (p->pPars->nLutSize + p->nPermWords + p->nTruthWords);
+ p->nObjBytes = sizeof(If_Obj_t) + sizeof(int) * (p->pPars->nLutSize + p->nPermWords/* + p->nTruthWords*/);
+ p->nCutBytes = sizeof(If_Cut_t) + sizeof(int) * (p->pPars->nLutSize + p->nPermWords/* + p->nTruthWords*/);
p->nSetBytes = sizeof(If_Set_t) + (sizeof(If_Cut_t *) + p->nCutBytes) * (p->pPars->nCutsMax + 1);
p->pMemObj = Mem_FixedStart( p->nObjBytes );
// p->pMemSet = Mem_FixedStart( p->nSetBytes );
// report expected memory usage
if ( p->pPars->fVerbose )
Abc_Print( 1, "K = %d. Memory (bytes): Truth = %4d. Cut = %4d. Obj = %4d. Set = %4d. CutMin = %s\n",
- p->pPars->nLutSize, 4 * p->nTruthWords, p->nCutBytes, p->nObjBytes, p->nSetBytes, p->pPars->fCutMin? "yes":"no" );
+ p->pPars->nLutSize, 8 * p->nTruth6Words, p->nCutBytes, p->nObjBytes, p->nSetBytes, p->pPars->fCutMin? "yes":"no" );
// room for temporary truth tables
- p->puTemp[0] = p->pPars->fTruth? ABC_ALLOC( unsigned, 4 * p->nTruthWords ) : NULL;
- p->puTemp[1] = p->puTemp[0] + p->nTruthWords;
- p->puTemp[2] = p->puTemp[1] + p->nTruthWords;
- p->puTemp[3] = p->puTemp[2] + p->nTruthWords;
- p->pCutTemp = (If_Cut_t *)ABC_ALLOC( char, p->nCutBytes );
+ p->puTemp[0] = p->pPars->fTruth? ABC_ALLOC( unsigned, 8 * p->nTruth6Words ) : NULL;
+ p->puTemp[1] = p->puTemp[0] + p->nTruth6Words*2;
+ p->puTemp[2] = p->puTemp[1] + p->nTruth6Words*2;
+ p->puTemp[3] = p->puTemp[2] + p->nTruth6Words*2;
+ p->puTempW = p->pPars->fTruth? ABC_ALLOC( word, p->nTruth6Words ) : NULL;
if ( pPars->fUseDsd )
{
// p->pNamDsd = Abc_NamStart( 1000, 20 );
@@ -144,6 +146,8 @@ void If_ManStop( If_Man_t * p )
// If_CluHashFindMedian( p );
// If_CluHashTableCheck( p );
}
+ if ( p->pPars->fVerbose && p->vTtMem )
+ printf( "Unique truth tables = %d. Memory = %.2f MB\n", Vec_MemEntryNum(p->vTtMem), Vec_MemMemory(p->vTtMem) / (1<<20) );
if ( p->pPars->fVerbose && p->nCutsUselessAll )
{
int i;
@@ -176,7 +180,6 @@ void If_ManStop( If_Man_t * p )
Vec_PtrFree( p->vCis );
Vec_PtrFree( p->vCos );
Vec_PtrFree( p->vObjs );
-// Vec_PtrFree( p->vMapped );
Vec_PtrFree( p->vTemp );
Vec_IntFreeP( &p->vCover );
Vec_WrdFreeP( &p->vAnds );
@@ -185,11 +188,13 @@ void If_ManStop( If_Man_t * p )
if ( p->vObjsRev ) Vec_PtrFree( p->vObjsRev );
if ( p->vLatchOrder ) Vec_PtrFree( p->vLatchOrder );
if ( p->vLags ) Vec_IntFree( p->vLags );
+ Vec_MemHashFree( p->vTtMem );
+ Vec_MemFreeP( &p->vTtMem );
Mem_FixedStop( p->pMemObj, 0 );
ABC_FREE( p->pMemCi );
ABC_FREE( p->pMemAnd );
ABC_FREE( p->puTemp[0] );
- ABC_FREE( p->pCutTemp );
+ ABC_FREE( p->puTempW );
// free pars memory
ABC_FREE( p->pPars->pTimesArr );
ABC_FREE( p->pPars->pTimesReq );
@@ -383,8 +388,6 @@ void If_ManSetupCut( If_Man_t * p, If_Cut_t * pCut )
pCut->pLeaves = (int *)(pCut + 1);
if ( p->pPars->fUsePerm )
pCut->pPerm = (char *)(pCut->pLeaves + p->pPars->nLutSize);
- if ( p->pPars->fTruth )
- pCut->pTruth = (unsigned *)pCut->pLeaves + p->pPars->nLutSize + p->nPermWords;
}
/**Function*************************************************************
@@ -435,17 +438,11 @@ void If_ManSetupCutTriv( If_Man_t * p, If_Cut_t * pCut, int ObjId )
pCut->uSign = If_ObjCutSign( pCut->pLeaves[0] );
if ( p->pPars->fUseDsd )
{
- pCut->iDsd = p->iNamVar;
+ pCut->iCutFunc = p->iNamVar;
pCut->pPerm[0] = 0;
}
// set up elementary truth table of the unit cut
- if ( p->pPars->fTruth )
- {
- int i, nTruthWords = If_CutTruthWords(pCut->nLimit);
- for ( i = 0; i < nTruthWords; i++ )
- If_CutTruth(pCut)[i] = 0xAAAAAAAA;
- }
-
+ pCut->iCutFunc = p->pPars->fTruth ? 2 : -1;
assert( pCut->pLeaves[0] < p->vObjs->nSize );
}
@@ -523,11 +520,9 @@ If_Set_t * If_ManSetupNodeCutSet( If_Man_t * p, If_Obj_t * pObj )
assert( pObj->pCutSet == NULL );
// pObj->pCutSet = (If_Set_t *)Mem_FixedEntryFetch( p->pMemSet );
// If_ManSetupSet( p, pObj->pCutSet );
-
pObj->pCutSet = If_ManCutSetFetch( p );
pObj->pCutSet->nCuts = 0;
pObj->pCutSet->nCutsMax = p->pPars->nCutsMax;
-
return pObj->pCutSet;
}
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index e6a5d821..58f0ad7b 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -135,7 +135,7 @@ static inline int * If_CutPerm1( If_Cut_t * pCut, If_Cut_t * pCut1 )
SeeAlso []
***********************************************************************/
-void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPreprocess )
+void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPreprocess, int fFirst )
{
If_Set_t * pCutSet;
If_Cut_t * pCut0, * pCut1, * pCut;
@@ -160,7 +160,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
// get the current assigned best cut
pCut = If_ObjCutBest(pObj);
- if ( pCut->nLeaves > 0 )
+ if ( !fFirst )
{
// recompute the parameters of the best cut
if ( p->pPars->fUserRecLib )
@@ -209,7 +209,6 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
assert( If_CutCheck( pCut ) );
if ( pObj->fSpec && pCut->nLeaves == (unsigned)p->pPars->nLutSize )
continue;
- assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
p->nCutsMerged++;
p->nCutsTotal++;
// check if this cut is contained in any of the available cuts
@@ -218,18 +217,18 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
continue;
// compute the truth table
pCut->fCompl = 0;
+ pCut->iCutFunc = -1;
if ( p->pPars->fTruth )
{
// abctime clk = Abc_Clock();
-// int RetValue = If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
- int RetValue = If_CutComputeTruth2( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
+ int RetValue = If_CutComputeTruth( p, pCut, pCut0, pCut1, pObj->fCompl0, pObj->fCompl1 );
// p->timeTruth += Abc_Clock() - clk;
pCut->fUseless = 0;
if ( p->pPars->pFuncCell && RetValue < 2 )
{
assert( pCut->nLimit >= 4 && pCut->nLimit <= 16 );
- pCut->fUseless = !p->pPars->pFuncCell( p, If_CutTruth(pCut), pCut->nLimit, pCut->nLeaves, p->pPars->pLutStruct );
+ pCut->fUseless = !p->pPars->pFuncCell( p, If_CutTruth(p, pCut), pCut->nLimit, pCut->nLeaves, p->pPars->pLutStruct );
p->nCutsUselessAll += pCut->fUseless;
p->nCutsUseless[pCut->nLeaves] += pCut->fUseless;
p->nCutsCountAll++;
@@ -239,7 +238,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
{
extern int If_CluCheckDecInAny( word t, int nVars );
extern int If_CluCheckDecOut( word t, int nVars );
- unsigned TruthU = *If_CutTruth(pCut);
+ unsigned TruthU = *If_CutTruth(p, pCut);
word Truth = (((word)TruthU << 32) | (word)TruthU);
p->nCuts5++;
if ( If_CluCheckDecInAny( Truth, 5 ) )
@@ -251,7 +250,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
{
extern int If_CluCheckDecInAny( word t, int nVars );
extern int If_CluCheckDecOut( word t, int nVars );
- unsigned TruthU = *If_CutTruth(pCut);
+ unsigned TruthU = *If_CutTruth(p, pCut);
word Truth = (((word)TruthU << 32) | (word)TruthU);
p->nCuts5++;
if ( If_CluCheckDecInAny( Truth, 5 ) || If_CluCheckDecOut( Truth, 5 ) )
@@ -261,11 +260,11 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
}
if ( p->pPars->fUseDsd )
{
- if ( pCut0->iDsd < 0 || pCut1->iDsd < 0 )
- pCut->iDsd = -1;
+ if ( pCut0->iCutFunc < 0 || pCut1->iCutFunc < 0 )
+ pCut->iCutFunc = -1;
else
{
- int j, iDsd[2] = { Abc_LitNotCond(pCut0->iDsd, pObj->fCompl0), Abc_LitNotCond(pCut1->iDsd, pObj->fCompl1) };
+ int j, iDsd[2] = { Abc_LitNotCond(pCut0->iCutFunc, pObj->fCompl0), Abc_LitNotCond(pCut1->iCutFunc, pObj->fCompl1) };
int nFans[2] = { pCut0->nLeaves, pCut1->nLeaves };
int Fans[2][DAU_MAX_VAR], * pFans[2] = { Fans[0], Fans[1] };
// create fanins
@@ -281,9 +280,9 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
ABC_SWAP( int *, pFans[0], pFans[1] );
}
// derive new DSD
- pCut->iDsd = Dss_ManMerge( p->pDsdMan, iDsd, nFans, pFans, p->uSharedMask, pCut->nLimit, (unsigned char *)pCut->pPerm, If_CutTruthW(pCut) );
+ pCut->iCutFunc = Dss_ManMerge( p->pDsdMan, iDsd, nFans, pFans, p->uSharedMask, pCut->nLimit, (unsigned char *)pCut->pPerm, If_CutTruthW(p, pCut) );
}
- if ( pCut->iDsd < 0 )
+ if ( pCut->iCutFunc < 0 )
{
pCut->fUseless = 1;
p->nCutsUselessAll++;
@@ -295,7 +294,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
// compute the application-specific cost and depth
pCut->fUser = (p->pPars->pFuncCost != NULL);
- pCut->Cost = p->pPars->pFuncCost? p->pPars->pFuncCost(pCut) : 0;
+ pCut->Cost = p->pPars->pFuncCost? p->pPars->pFuncCost(p, pCut) : 0;
if ( pCut->Cost == IF_COST_MAX )
continue;
// check if the cut satisfies the required times
@@ -333,21 +332,8 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
If_CutSort( p, pCutSet, pCut );
// If_CutTraverse( p, pObj, pCut );
}
-/*
- printf( "Node %d\n", pObj->Id );
- for ( i = 0; i < pCutSet->nCuts; i++ )
- If_CutPrint( pCutSet->ppCuts[i] );
- printf( "\n" );
-*/
assert( pCutSet->nCuts > 0 );
- // add the trivial cut to the set
- if ( !pObj->fSkipCut )
- {
- If_ManSetupCutTriv( p, pCutSet->ppCuts[pCutSet->nCuts++], pObj->Id );
- assert( pCutSet->nCuts <= pCutSet->nCutsMax+1 );
- }
-
// update the best cut
if ( !fPreprocess || pCutSet->ppCuts[0]->Delay <= pObj->Required + p->fEpsilon )
{
@@ -355,19 +341,26 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
if(p->pPars->fUserRecLib)
assert(If_ObjCutBest(pObj)->Cost < IF_COST_MAX && If_ObjCutBest(pObj)->Delay < ABC_INFINITY);
}
- assert( p->pPars->fSeqMap || If_ObjCutBest(pObj)->nLeaves > 1 );
+ // add the trivial cut to the set
+ if ( !pObj->fSkipCut && If_ObjCutBest(pObj)->nLeaves > 1 )
+ {
+ If_ManSetupCutTriv( p, pCutSet->ppCuts[pCutSet->nCuts++], pObj->Id );
+ assert( pCutSet->nCuts <= pCutSet->nCutsMax+1 );
+ }
+// if ( If_ObjCutBest(pObj)->nLeaves == 0 )
+// p->nBestCutSmall[0]++;
+// else if ( If_ObjCutBest(pObj)->nLeaves == 1 )
+// p->nBestCutSmall[1]++;
+
// ref the selected cut
if ( Mode && pObj->nRefs > 0 )
If_CutAreaRef( p, If_ObjCutBest(pObj) );
if ( If_ObjCutBest(pObj)->fUseless )
Abc_Print( 1, "The best cut is useless.\n" );
-
// call the user specified function for each cut
if ( p->pPars->pFuncUser )
If_ObjForEachCut( pObj, pCut, i )
p->pPars->pFuncUser( p, pObj, pCut );
-
-
// free the cuts
If_ManDerefNodeCutSet( p, pObj );
}
@@ -445,22 +438,20 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP
}
assert( pCutSet->nCuts > 0 );
+ // update the best cut
+ if ( !fPreprocess || pCutSet->ppCuts[0]->Delay <= pObj->Required + p->fEpsilon )
+ If_CutCopy( p, If_ObjCutBest(pObj), pCutSet->ppCuts[0] );
+ assert( p->pPars->fSeqMap || If_ObjCutBest(pObj)->nLeaves > 1 );
// add the trivial cut to the set
- if ( !pObj->fSkipCut )
+ if ( !pObj->fSkipCut && If_ObjCutBest(pObj)->nLeaves > 1 )
{
If_ManSetupCutTriv( p, pCutSet->ppCuts[pCutSet->nCuts++], pObj->Id );
assert( pCutSet->nCuts <= pCutSet->nCutsMax+1 );
}
- // update the best cut
- if ( !fPreprocess || pCutSet->ppCuts[0]->Delay <= pObj->Required + p->fEpsilon )
- If_CutCopy( p, If_ObjCutBest(pObj), pCutSet->ppCuts[0] );
- assert( p->pPars->fSeqMap || If_ObjCutBest(pObj)->nLeaves > 1 );
-
// ref the selected cut
if ( Mode && pObj->nRefs > 0 )
If_CutAreaRef( p, If_ObjCutBest(pObj) );
-
// free the cuts
If_ManDerefChoiceCutSet( p, pObj );
}
@@ -476,7 +467,7 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP
SeeAlso []
***********************************************************************/
-int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPreprocess, char * pLabel )
+int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPreprocess, int fFirst, char * pLabel )
{
// ProgressBar * pProgress;
If_Obj_t * pObj;
@@ -484,6 +475,7 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPrepr
abctime clk = Abc_Clock();
float arrTime;
assert( Mode >= 0 && Mode <= 2 );
+ p->nBestCutSmall[0] = p->nBestCutSmall[1] = 0;
// set the sorting function
if ( Mode || p->pPars->fArea ) // area
p->SortMode = 1;
@@ -505,7 +497,7 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPrepr
{
if ( If_ObjIsAnd(pObj) )
{
- If_ObjPerformMappingAnd( p, pObj, Mode, fPreprocess );
+ If_ObjPerformMappingAnd( p, pObj, Mode, fPreprocess, fFirst );
if ( pObj->fRepr )
If_ObjPerformMappingChoice( p, pObj, Mode, fPreprocess );
}
@@ -534,7 +526,7 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPrepr
If_ManForEachNode( p, pObj, i )
{
// Extra_ProgressBarUpdate( pProgress, i, pLabel );
- If_ObjPerformMappingAnd( p, pObj, Mode, fPreprocess );
+ If_ObjPerformMappingAnd( p, pObj, Mode, fPreprocess, fFirst );
if ( pObj->fRepr )
If_ObjPerformMappingChoice( p, pObj, Mode, fPreprocess );
}
@@ -551,6 +543,7 @@ int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, int Mode, int fPrepr
char Symb = fPreprocess? 'P' : ((Mode == 0)? 'D' : ((Mode == 1)? 'F' : 'A'));
Abc_Print( 1, "%c: Del = %7.2f. Ar = %9.1f. Edge = %8d. Switch = %7.2f. Cut = %8d. ",
Symb, p->RequiredGlo, p->AreaGlo, p->nNets, p->dPower, p->nCutsMerged );
+// printf( "Cut0 =%4d. Cut1 =%4d. ", p->nBestCutSmall[0], p->nBestCutSmall[1] );
Abc_PrintTime( 1, "T", Abc_Clock() - clk );
// Abc_Print( 1, "Max number of cuts = %d. Average number of cuts = %5.2f.\n",
// p->nCutsMax, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
diff --git a/src/map/if/ifSeq.c b/src/map/if/ifSeq.c
index adb97b22..32cef52a 100644
--- a/src/map/if/ifSeq.c
+++ b/src/map/if/ifSeq.c
@@ -142,7 +142,7 @@ int If_ManPerformMappingRoundSeq( If_Man_t * p, int nIter )
p->nCutsMerged = 0;
If_ManForEachNode( p, pObj, i )
{
- If_ObjPerformMappingAnd( p, pObj, 0, 0 );
+ If_ObjPerformMappingAnd( p, pObj, 0, 0, 0 );
if ( pObj->fRepr )
If_ObjPerformMappingChoice( p, pObj, 0, 0 );
}
@@ -345,7 +345,7 @@ int If_ManPerformMappingSeq( If_Man_t * p )
p->SortMode = 0;
// perform combinational mapping to get the upper bound on the clock period
- If_ManPerformMappingRound( p, 1, 0, 0, NULL );
+ If_ManPerformMappingRound( p, 1, 0, 0, 1, NULL );
p->RequiredGlo = If_ManDelayMax( p, 0 );
p->RequiredGlo2 = p->RequiredGlo;
diff --git a/src/map/if/ifTime.c b/src/map/if/ifTime.c
index f0fd3046..f07b502e 100644
--- a/src/map/if/ifTime.c
+++ b/src/map/if/ifTime.c
@@ -261,7 +261,7 @@ Vec_Wrd_t * If_CutDelaySopArray( If_Man_t * p, If_Cut_t * pCut )
p->vAndGate = Vec_WrdAlloc(100);
if ( p->vOrGate == NULL )
p->vOrGate = Vec_WrdAlloc(100);
- RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), p->vCover, 1 );
+ RetValue = Kit_TruthIsop( If_CutTruth(p, pCut), If_CutLeaveNum(pCut), p->vCover, 1 );
if ( RetValue == -1 )
return NULL;
assert( RetValue == 0 || RetValue == 1 );
@@ -499,7 +499,7 @@ int If_CutDelaySopArray2( If_Man_t * p, If_Cut_t * pCut, int * pArea )
p->vAndGate = Vec_WrdAlloc(100);
if ( p->vOrGate == NULL )
p->vOrGate = Vec_WrdAlloc(100);
- RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), p->vCover, 1 );
+ RetValue = Kit_TruthIsop( If_CutTruth(p, pCut), If_CutLeaveNum(pCut), p->vCover, 1 );
if ( RetValue == -1 )
return -1;
assert( RetValue == 0 || RetValue == 1 );
@@ -581,7 +581,7 @@ int If_CutDelaySop( If_Man_t * p, If_Cut_t * pCut )
pCut->fUser = 1;
if ( p->vCover == NULL )
p->vCover = Vec_IntAlloc(0);
- RetValue = Kit_TruthIsop( If_CutTruth(pCut), If_CutLeaveNum(pCut), p->vCover, 1 );
+ RetValue = Kit_TruthIsop( If_CutTruth(p, pCut), If_CutLeaveNum(pCut), p->vCover, 1 );
if ( RetValue == -1 )
return ABC_INFINITY;
assert( RetValue == 0 || RetValue == 1 );
@@ -631,7 +631,7 @@ float If_CutDelay( If_Man_t * p, If_Obj_t * pObj, If_Cut_t * pCut )
float Delay, DelayCur;
float * pLutDelays;
int i, Shift, Pin2PinDelay;//, iLeaf;
- assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
+// assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
Delay = -IF_FLOAT_LARGE;
if ( p->pPars->pLutLib )
{
@@ -810,6 +810,7 @@ void If_CutSortInputPins( If_Man_t * p, If_Cut_t * pCut, int * pPinPerm, float *
SeeAlso []
***********************************************************************/
+/*
void If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut )
{
If_Obj_t * pLeaf;
@@ -819,9 +820,10 @@ void If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut )
// assert( p->pPars->pLutLib && p->pPars->pLutLib->fVarPinDelays && p->pPars->fTruth );
If_CutForEachLeaf( p, pCut, pLeaf, i )
PinDelays[i] = If_ObjCutBest(pLeaf)->Delay;
- If_CutTruthPermute( p->puTemp[0], If_CutTruth(pCut), If_CutLeaveNum(pCut), PinDelays, If_CutLeaves(pCut) );
+ If_CutTruthPermute( p->puTemp[0], If_CutTruth(p, pCut), If_CutLeaveNum(pCut), PinDelays, If_CutLeaves(pCut) );
// If_CutSortInputPins( p, pCut, PinPerm, PinDelays );
}
+*/
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c
index 95831f66..ad8a4773 100644
--- a/src/map/if/ifTruth.c
+++ b/src/map/if/ifTruth.c
@@ -36,7 +36,7 @@ ABC_NAMESPACE_IMPL_START
/**Function*************************************************************
- Synopsis [Several simple procedures working with truth tables.]
+ Synopsis [Sorts the pins in the decreasing order of delays.]
Description []
@@ -45,634 +45,42 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
-static inline void If_TruthNot( unsigned * pOut, unsigned * pIn, int nVars )
+void If_CutTruthPermute( word * pTruth, int nLeaves, int nVars, int nWords, float * pDelays, int * pVars )
{
- int w;
- for ( w = If_CutTruthWords(nVars)-1; w >= 0; w-- )
- pOut[w] = ~pIn[w];
-}
-static inline void If_TruthCopy( unsigned * pOut, unsigned * pIn, int nVars )
-{
- int w;
- for ( w = If_CutTruthWords(nVars)-1; w >= 0; w-- )
- pOut[w] = pIn[w];
-}
-static inline void If_TruthNand( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
-{
- int w;
- for ( w = If_CutTruthWords(nVars)-1; w >= 0; w-- )
- pOut[w] = ~(pIn0[w] & pIn1[w]);
-}
-static inline void If_TruthAnd( unsigned * pOut, unsigned * pIn0, unsigned * pIn1, int nVars )
-{
- int w;
- for ( w = If_CutTruthWords(nVars)-1; w >= 0; w-- )
- pOut[w] = pIn0[w] & pIn1[w];
-}
-
-/**Function*************************************************************
-
- Synopsis [Swaps two adjacent variables in the truth table.]
-
- Description [Swaps var number Start and var number Start+1 (0-based numbers).
- The input truth table is pIn. The output truth table is pOut.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void If_TruthSwapAdjacentVars( unsigned * pOut, unsigned * pIn, int nVars, int iVar )
-{
- static unsigned PMasks[4][3] = {
- { 0x99999999, 0x22222222, 0x44444444 },
- { 0xC3C3C3C3, 0x0C0C0C0C, 0x30303030 },
- { 0xF00FF00F, 0x00F000F0, 0x0F000F00 },
- { 0xFF0000FF, 0x0000FF00, 0x00FF0000 }
- };
- int nWords = If_CutTruthWords( nVars );
- int i, k, Step, Shift;
-
- assert( iVar < nVars - 1 );
- if ( iVar < 4 )
- {
- Shift = (1 << iVar);
- for ( i = 0; i < nWords; i++ )
- pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift);
- }
- else if ( iVar > 4 )
- {
- Step = (1 << (iVar - 5));
- for ( k = 0; k < nWords; k += 4*Step )
- {
- for ( i = 0; i < Step; i++ )
- pOut[i] = pIn[i];
- for ( i = 0; i < Step; i++ )
- pOut[Step+i] = pIn[2*Step+i];
- for ( i = 0; i < Step; i++ )
- pOut[2*Step+i] = pIn[Step+i];
- for ( i = 0; i < Step; i++ )
- pOut[3*Step+i] = pIn[3*Step+i];
- pIn += 4*Step;
- pOut += 4*Step;
- }
- }
- else // if ( iVar == 4 )
+ while ( 1 )
{
- for ( i = 0; i < nWords; i += 2 )
- {
- pOut[i] = (pIn[i] & 0x0000FFFF) | ((pIn[i+1] & 0x0000FFFF) << 16);
- pOut[i+1] = (pIn[i+1] & 0xFFFF0000) | ((pIn[i] & 0xFFFF0000) >> 16);
- }
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Implements given permutation of variables.]
-
- Description [Permutes truth table in-place (returns it in pIn).]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void If_CutTruthPermute( unsigned * pOut, unsigned * pIn, int nVars, float * pDelays, int * pVars )
-{
- unsigned * pTemp;
- float tTemp;
- int i, Temp, Counter = 0, fChange = 1;
- while ( fChange )
- {
- fChange = 0;
- for ( i = 0; i < nVars - 1; i++ )
+ int i, fChange = 0;
+ for ( i = 0; i < nLeaves - 1; i++ )
{
if ( pDelays[i] >= pDelays[i+1] )
-// if ( pDelays[i] <= pDelays[i+1] )
continue;
- tTemp = pDelays[i]; pDelays[i] = pDelays[i+1]; pDelays[i+1] = tTemp;
- Temp = pVars[i]; pVars[i] = pVars[i+1]; pVars[i+1] = Temp;
- if ( pOut && pIn )
- If_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
- pTemp = pOut; pOut = pIn; pIn = pTemp;
+ ABC_SWAP( float, pDelays[i], pDelays[i+1] );
+ ABC_SWAP( int, pVars[i], pVars[i+1] );
+ if ( pTruth )
+ Abc_TtSwapAdjacent( pTruth, nWords, i );
fChange = 1;
- Counter++;
- }
- }
- if ( pOut && pIn && (Counter & 1) )
- If_TruthCopy( pOut, pIn, nVars );
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Expands the truth table according to the phase.]
-
- Description [The input and output truth tables are in pIn/pOut. The current number
- of variables is nVars. The total number of variables in nVarsAll. The last argument
- (Phase) contains shows where the variables should go.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void If_TruthStretch( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase )
-{
- unsigned * pTemp;
- int i, k, Var = nVars - 1, Counter = 0;
- for ( i = nVarsAll - 1; i >= 0; i-- )
- if ( Phase & (1 << i) )
- {
- for ( k = Var; k < i; k++ )
- {
- If_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
- pTemp = pIn; pIn = pOut; pOut = pTemp;
- Counter++;
- }
- Var--;
- }
- assert( Var == -1 );
- // swap if it was moved an even number of times
- if ( !(Counter & 1) )
- If_TruthCopy( pOut, pIn, nVarsAll );
-}
-
-/**Function*************************************************************
-
- Synopsis [Shrinks the truth table according to the phase.]
-
- Description [The input and output truth tables are in pIn/pOut. The current number
- of variables is nVars. The total number of variables in nVarsAll. The last argument
- (Phase) contains shows what variables should remain.]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void If_TruthShrink( unsigned * pOut, unsigned * pIn, int nVars, int nVarsAll, unsigned Phase, int fReturnIn )
-{
- unsigned * pTemp;
- int i, k, Var = 0, Counter = 0;
- for ( i = 0; i < nVarsAll; i++ )
- if ( Phase & (1 << i) )
- {
- for ( k = i-1; k >= Var; k-- )
- {
- If_TruthSwapAdjacentVars( pOut, pIn, nVarsAll, k );
- pTemp = pIn; pIn = pOut; pOut = pTemp;
- Counter++;
- }
- Var++;
- }
- assert( Var == nVars );
- // swap if it was moved an even number of times
- if ( fReturnIn ^ !(Counter & 1) )
- If_TruthCopy( pOut, pIn, nVarsAll );
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns 1 if TT depends on the given variable.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int If_CutTruthVarInSupport( unsigned * pTruth, int nVars, int iVar )
-{
- int nWords = If_CutTruthWords( nVars );
- int i, k, Step;
-
- assert( iVar < nVars );
- switch ( iVar )
- {
- case 0:
- for ( i = 0; i < nWords; i++ )
- if ( (pTruth[i] & 0x55555555) != ((pTruth[i] & 0xAAAAAAAA) >> 1) )
- return 1;
- return 0;
- case 1:
- for ( i = 0; i < nWords; i++ )
- if ( (pTruth[i] & 0x33333333) != ((pTruth[i] & 0xCCCCCCCC) >> 2) )
- return 1;
- return 0;
- case 2:
- for ( i = 0; i < nWords; i++ )
- if ( (pTruth[i] & 0x0F0F0F0F) != ((pTruth[i] & 0xF0F0F0F0) >> 4) )
- return 1;
- return 0;
- case 3:
- for ( i = 0; i < nWords; i++ )
- if ( (pTruth[i] & 0x00FF00FF) != ((pTruth[i] & 0xFF00FF00) >> 8) )
- return 1;
- return 0;
- case 4:
- for ( i = 0; i < nWords; i++ )
- if ( (pTruth[i] & 0x0000FFFF) != ((pTruth[i] & 0xFFFF0000) >> 16) )
- return 1;
- return 0;
- default:
- Step = (1 << (iVar - 5));
- for ( k = 0; k < nWords; k += 2*Step )
- {
- for ( i = 0; i < Step; i++ )
- if ( pTruth[i] != pTruth[Step+i] )
- return 1;
- pTruth += 2*Step;
- }
- return 0;
- }
-}
-
-/**Function*************************************************************
-
- Synopsis [Returns support of the function.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-unsigned If_CutTruthSupport( unsigned * pTruth, int nVars, int * pnSuppSize )
-{
- int i, Support = 0;
- int nSuppSize = 0;
- for ( i = 0; i < nVars; i++ )
- if ( If_CutTruthVarInSupport( pTruth, nVars, i ) )
- {
- Support |= (1 << i);
- nSuppSize++;
- }
- *pnSuppSize = nSuppSize;
- return Support;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Computes the stretching phase of the cut w.r.t. the merged cut.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline unsigned If_CutTruthPhase( If_Cut_t * pCut, If_Cut_t * pCut1 )
-{
- unsigned uPhase = 0;
- int i, k;
- for ( i = k = 0; i < (int)pCut->nLeaves; i++ )
- {
- if ( k == (int)pCut1->nLeaves )
- break;
- if ( pCut->pLeaves[i] < pCut1->pLeaves[k] )
- continue;
- assert( pCut->pLeaves[i] == pCut1->pLeaves[k] );
- uPhase |= (1 << i);
- k++;
- }
- return uPhase;
-}
-
-//static FILE * pTruths;
-
-/**Function*************************************************************
-
- Synopsis [Performs truth table computation.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 )
-{
- extern void If_CutFactorTest( unsigned * pTruth, int nVars );
-
- // permute the first table
- if ( fCompl0 ^ pCut0->fCompl )
- If_TruthNot( p->puTemp[0], If_CutTruth(pCut0), pCut->nLimit );
- else
- If_TruthCopy( p->puTemp[0], If_CutTruth(pCut0), pCut->nLimit );
- If_TruthStretch( p->puTemp[2], p->puTemp[0], pCut0->nLeaves, pCut->nLimit, If_CutTruthPhase(pCut, pCut0) );
- // permute the second table
- if ( fCompl1 ^ pCut1->fCompl )
- If_TruthNot( p->puTemp[1], If_CutTruth(pCut1), pCut->nLimit );
- else
- If_TruthCopy( p->puTemp[1], If_CutTruth(pCut1), pCut->nLimit );
- If_TruthStretch( p->puTemp[3], p->puTemp[1], pCut1->nLeaves, pCut->nLimit, If_CutTruthPhase(pCut, pCut1) );
- // produce the resulting table
- assert( pCut->fCompl == 0 );
- if ( pCut->fCompl )
- If_TruthNand( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit );
- else
- If_TruthAnd( If_CutTruth(pCut), p->puTemp[2], p->puTemp[3], pCut->nLimit );
-/*
- if ( pCut->nLeaves == 5 )
- {
- if ( pTruths == NULL )
- pTruths = fopen( "fun5var.txt", "w" );
- Extra_PrintHex( pTruths, If_CutTruth(pCut), pCut->nLeaves );
- fprintf( pTruths, "\n" );
- }
-*/
- // minimize the support of the cut
- if ( p->pPars->fCutMin )
- return If_CutTruthMinimize( p, pCut );
-
- // perform
-// If_CutFactorTest( If_CutTruth(pCut), pCut->nLimit );
-// printf( "%d ", If_CutLeaveNum(pCut) - If_CutTruthSupportSize(If_CutTruth(pCut), If_CutLeaveNum(pCut)) );
- return 0;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Minimize support of the cut.]
-
- Description [Returns 1 if the node's support has changed]
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-int If_CutTruthMinimize( If_Man_t * p, If_Cut_t * pCut )
-{
- unsigned uSupport;
- int nSuppSize, i, k;
- // compute the support of the cut's function
- uSupport = If_CutTruthSupport( If_CutTruth(pCut), If_CutLeaveNum(pCut), &nSuppSize );
- if ( nSuppSize == If_CutLeaveNum(pCut) )
- return 0;
-
-// TEMPORARY
- if ( nSuppSize < 2 )
- {
- p->nSmallSupp++;
- return 2;
- }
-// if ( If_CutLeaveNum(pCut) - nSuppSize > 1 )
-// return 0;
-//printf( "%d %d ", If_CutLeaveNum(pCut), nSuppSize );
-// pCut->fUseless = 1;
-
- // shrink the truth table
- If_TruthShrink( p->puTemp[0], If_CutTruth(pCut), nSuppSize, pCut->nLimit, uSupport, 1 );
- // update leaves and signature
- pCut->uSign = 0;
- for ( i = k = 0; i < If_CutLeaveNum(pCut); i++ )
- {
- if ( !(uSupport & (1 << i)) )
- continue;
- pCut->pLeaves[k++] = pCut->pLeaves[i];
- pCut->uSign |= If_ObjCutSign( pCut->pLeaves[i] );
- }
- assert( k == nSuppSize );
- pCut->nLeaves = nSuppSize;
- // verify the result
-// uSupport = If_CutTruthSupport( If_CutTruth(pCut), If_CutLeaveNum(pCut), &nSuppSize );
-// assert( nSuppSize == If_CutLeaveNum(pCut) );
- return 1;
-}
-
-
-
-
-/**Function*************************************************************
-
- Synopsis [Performs truth table computation.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-static inline int If_CutTruthMinimize6( If_Man_t * p, If_Cut_t * pCut )
-{
- unsigned uSupport;
- int i, k, nSuppSize;
- int nVars = If_CutLeaveNum(pCut);
- // compute the support of the cut's function
- uSupport = Abc_Tt6SupportAndSize( *If_CutTruthW(pCut), nVars, &nSuppSize );
- if ( nSuppSize == If_CutLeaveNum(pCut) )
- return 0;
-// TEMPORARY
- if ( nSuppSize < 2 )
- {
-//printf( "Small supp\n" );
- p->nSmallSupp++;
- return 2;
- }
- // update leaves and signature
- pCut->uSign = 0;
- for ( i = k = 0; i < nVars; i++ )
- {
- if ( !(uSupport & (1 << i)) )
- continue;
- pCut->uSign |= If_ObjCutSign( pCut->pLeaves[i] );
- if ( k < i )
- {
- pCut->pLeaves[k] = pCut->pLeaves[i];
- Abc_TtSwapVars( If_CutTruthW(pCut), pCut->nLimit, k, i );
- }
- k++;
- }
- assert( k == nSuppSize );
- pCut->nLeaves = nSuppSize;
- // verify the result
-// assert( nSuppSize == Abc_TtSupportSize(If_CutTruthW(pCut), nVars) );
- return 1;
-}
-static inline word If_TruthStretch6_( word Truth, If_Cut_t * pCut, If_Cut_t * pCut0 )
-{
- int i, k;
- for ( i = (int)pCut->nLeaves - 1, k = (int)pCut0->nLeaves - 1; i >= 0 && k >= 0; i-- )
- {
- if ( pCut0->pLeaves[k] < pCut->pLeaves[i] )
- continue;
- assert( pCut0->pLeaves[k] == pCut->pLeaves[i] );
- if ( k < i )
- Abc_TtSwapVars( &Truth, pCut->nLimit, k, i );
- k--;
- }
- return Truth;
-}
-static inline word If_TruthStretch6( word Truth, int nVars, int * pPerm, int nVarsCut )
-{
- int i;
- for ( i = nVarsCut - 1; i >= 0; i-- )
- if ( i < pPerm[i] )
- Abc_TtSwapVars( &Truth, nVars, i, pPerm[i] );
- return Truth;
-}
-static inline int If_CutComputeTruth6( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 )
-{
- word t0 = (fCompl0 ^ pCut0->fCompl) ? ~*If_CutTruthW(pCut0) : *If_CutTruthW(pCut0);
- word t1 = (fCompl1 ^ pCut1->fCompl) ? ~*If_CutTruthW(pCut1) : *If_CutTruthW(pCut1);
- assert( pCut->nLimit <= 6 );
-// t0 = If_TruthStretch6( t0, pCut, pCut0 );
-// t1 = If_TruthStretch6( t1, pCut, pCut1 );
- t0 = If_TruthStretch6( t0, pCut->nLimit, p->pPerm[0], pCut0->nLeaves );
- t1 = If_TruthStretch6( t1, pCut->nLimit, p->pPerm[1], pCut1->nLeaves );
- *If_CutTruthW(pCut) = t0 & t1;
-
-#ifdef IF_TRY_NEW
- {
- word pCopy[1024];
- char pCanonPerm[16];
- memcpy( pCopy, If_CutTruthW(pCut), sizeof(word) * 1 );
- Abc_TtCanonicize( pCopy, pCut->nLimit, pCanonPerm );
- }
-#endif
-
- if ( p->pPars->fCutMin )
- return If_CutTruthMinimize6( p, pCut );
- return 0;
-}
-
-
-/**Function*************************************************************
-
- Synopsis [Performs truth table computation.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-// this procedure handles special case reductions
-static inline int If_CutTruthMinimize21( If_Man_t * p, If_Cut_t * pCut )
-{
- word * pTruth = If_CutTruthW(pCut);
- int i, k, nVars = If_CutLeaveNum(pCut);
- unsigned uSign = 0;
- for ( i = k = 0; i < nVars; i++ )
- {
- if ( !Abc_TtHasVar( pTruth, nVars, i ) )
- continue;
- uSign |= If_ObjCutSign( pCut->pLeaves[i] );
- if ( k < i )
- {
- pCut->pLeaves[k] = pCut->pLeaves[i];
- Abc_TtSwapVars( pTruth, nVars, k, i );
}
- k++;
- }
- if ( k == nVars )
- return 0;
- assert( k < nVars );
- pCut->nLeaves = k;
- pCut->uSign = uSign;
-// TEMPORARY
- if ( pCut->nLeaves < 2 )
- {
- p->nSmallSupp++;
- return 2;
+ if ( !fChange )
+ return;
}
- // verify the result
- assert( If_CutLeaveNum(pCut) == Abc_TtSupportSize(pTruth, nVars) );
- return 1;
}
-static inline int If_CutTruthMinimize2( If_Man_t * p, If_Cut_t * pCut )
+void If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut )
{
- unsigned uSupport;
- int i, k, nSuppSize;
- int nVars = If_CutLeaveNum(pCut);
- // compute the support of the cut's function
- uSupport = Abc_TtSupportAndSize( If_CutTruthW(pCut), nVars, &nSuppSize );
- if ( nSuppSize == If_CutLeaveNum(pCut) )
- return 0;
-// TEMPORARY
- if ( nSuppSize < 2 )
- {
-//printf( "Small supp\n" );
- p->nSmallSupp++;
- return 2;
- }
- // update leaves and signature
- pCut->uSign = 0;
- for ( i = k = 0; i < nVars; i++ )
+ If_Obj_t * pLeaf;
+ float PinDelays[IF_MAX_LUTSIZE];
+ int i, truthId;
+ If_CutForEachLeaf( p, pCut, pLeaf, i )
+ PinDelays[i] = If_ObjCutBest(pLeaf)->Delay;
+ if ( p->vTtMem == NULL )
{
- if ( !(uSupport & (1 << i)) )
- continue;
- pCut->uSign |= If_ObjCutSign( pCut->pLeaves[i] );
- if ( k < i )
- {
- pCut->pLeaves[k] = pCut->pLeaves[i];
- Abc_TtSwapVars( If_CutTruthW(pCut), pCut->nLimit, k, i );
- }
- k++;
+ If_CutTruthPermute( NULL, If_CutLeaveNum(pCut), pCut->nLimit, p->nTruth6Words, PinDelays, If_CutLeaves(pCut) );
+ return;
}
- assert( k == nSuppSize );
- pCut->nLeaves = nSuppSize;
- // verify the result
-// assert( nSuppSize == Abc_TtSupportSize(If_CutTruthW(pCut), nVars) );
- return 1;
-}
-static inline void If_TruthStretch2_( word * pTruth, If_Cut_t * pCut, If_Cut_t * pCut0 )
-{
- int i, k;
- for ( i = (int)pCut->nLeaves - 1, k = (int)pCut0->nLeaves - 1; i >= 0 && k >= 0; i-- )
- {
- if ( pCut0->pLeaves[k] < pCut->pLeaves[i] )
- continue;
- assert( pCut0->pLeaves[k] == pCut->pLeaves[i] );
- if ( k < i )
- Abc_TtSwapVars( pTruth, pCut->nLimit, k, i );
- k--;
- }
-}
-static inline void If_TruthStretch2( word * pTruth, int nVars, int * pPerm, int nVarsCut )
-{
- int i;
- for ( i = nVarsCut - 1; i >= 0; i-- )
- if ( i < pPerm[i] )
- Abc_TtSwapVars( pTruth, nVars, i, pPerm[i] );
-}
-int If_CutComputeTruth2( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 )
-{
- int nWords;
- if ( pCut->nLimit < 7 )
- return If_CutComputeTruth6( p, pCut, pCut0, pCut1, fCompl0, fCompl1 );
- nWords = Abc_TtWordNum( pCut->nLimit );
- Abc_TtCopy( (word *)p->puTemp[0], If_CutTruthW(pCut0), nWords, fCompl0 ^ pCut0->fCompl );
- Abc_TtCopy( (word *)p->puTemp[1], If_CutTruthW(pCut1), nWords, fCompl1 ^ pCut1->fCompl );
-// If_TruthStretch2( (word *)p->puTemp[0], pCut, pCut0 );
-// If_TruthStretch2( (word *)p->puTemp[1], pCut, pCut1 );
- If_TruthStretch2( (word *)p->puTemp[0], pCut->nLimit, p->pPerm[0], pCut0->nLeaves );
- If_TruthStretch2( (word *)p->puTemp[1], pCut->nLimit, p->pPerm[1], pCut1->nLeaves );
- Abc_TtAnd( If_CutTruthW(pCut), (word *)p->puTemp[0], (word *)p->puTemp[1], nWords, 0 );
-
-#ifdef IF_TRY_NEW
- {
- word pCopy[1024];
- char pCanonPerm[16];
- memcpy( pCopy, If_CutTruthW(pCut), sizeof(word) * nWords );
- Abc_TtCanonicize( pCopy, pCut->nLimit, pCanonPerm );
- }
-#endif
-
- if ( p->pPars->fCutMin )
- return If_CutTruthMinimize2( p, pCut );
- return 0;
+ Abc_TtCopy( p->puTempW, If_CutTruthWR(p, pCut), p->nTruth6Words, 0 );
+ If_CutTruthPermute( p->puTempW, If_CutLeaveNum(pCut), pCut->nLimit, p->nTruth6Words, PinDelays, If_CutLeaves(pCut) );
+ truthId = Vec_MemHashInsert( p->vTtMem, p->puTempW );
+ pCut->iCutFunc = Abc_Var2Lit( truthId, If_CutTruthIsCompl(pCut) );
+ assert( (p->puTempW[0] & 1) == 0 );
}
/**Function*************************************************************
@@ -686,12 +94,11 @@ int If_CutComputeTruth2( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut
SeeAlso []
***********************************************************************/
-/*
-int If_CutComputeTruth3( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 )
+int If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 )
{
- int fCompl, truthId;
- int iFuncLit0 = pCut0->iDsd;
- int iFuncLit1 = pCut1->iDsd;
+ int fCompl, truthId, nLeavesNew;
+ int iFuncLit0 = pCut0->iCutFunc;
+ int iFuncLit1 = pCut1->iCutFunc;
int nWords = Abc_TtWordNum( pCut->nLimit );
word * pTruth0s = Vec_MemReadEntry( p->vTtMem, Abc_Lit2Var(iFuncLit0) );
word * pTruth1s = Vec_MemReadEntry( p->vTtMem, Abc_Lit2Var(iFuncLit1) );
@@ -704,13 +111,29 @@ int If_CutComputeTruth3( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut
Abc_TtStretch( pTruth1, pCut->nLimit, pCut1->pLeaves, pCut1->nLeaves, pCut->pLeaves, pCut->nLeaves );
fCompl = (pTruth0[0] & pTruth1[0] & 1);
Abc_TtAnd( pTruth, pTruth0, pTruth1, nWords, fCompl );
- pCut->nLeaves = Abc_TtMinBase( pTruth, pCut->pLeaves, pCut->nLeaves, pCut->nLimit );
+ if ( p->pPars->fCutMin )
+ {
+ nLeavesNew = Abc_TtMinBase( pTruth, pCut->pLeaves, pCut->nLeaves, pCut->nLimit );
+ if ( nLeavesNew < If_CutLeaveNum(pCut) )
+ {
+ pCut->nLeaves = nLeavesNew;
+ pCut->uSign = If_ObjCutSignCompute( pCut );
+ }
+ }
truthId = Vec_MemHashInsert( p->vTtMem, pTruth );
- pCut->iDsd = Abc_Var2Lit( truthId, fCompl );
+ pCut->iCutFunc = Abc_Var2Lit( truthId, fCompl );
assert( (pTruth[0] & 1) == 0 );
+#ifdef IF_TRY_NEW
+ {
+ word pCopy[1024];
+ char pCanonPerm[16];
+ memcpy( pCopy, If_CutTruthW(pCut), sizeof(word) * nWords );
+ Abc_TtCanonicize( pCopy, pCut->nLimit, pCanonPerm );
+ }
+#endif
return 1;
}
-*/
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h
index c6937b40..0faf8330 100644
--- a/src/misc/util/utilTruth.h
+++ b/src/misc/util/utilTruth.h
@@ -1156,7 +1156,7 @@ static inline int Abc_TtMinBase( word * pTruth, int * pVars, int nVars, int nVar
continue;
if ( k < i )
{
- pVars[k] = pVars[i];
+ if ( pVars ) pVars[k] = pVars[i];
Abc_TtSwapVars( pTruth, nVarsAll, k, i );
}
k++;
diff --git a/src/misc/vec/vecMem.h b/src/misc/vec/vecMem.h
index cba76a59..3f1b4517 100644
--- a/src/misc/vec/vecMem.h
+++ b/src/misc/vec/vecMem.h
@@ -310,6 +310,8 @@ static inline void Vec_MemHashAlloc( Vec_Mem_t * p, int nTableSize )
}
static inline void Vec_MemHashFree( Vec_Mem_t * p )
{
+ if ( p == NULL )
+ return;
Vec_IntFreeP( &p->vTable );
Vec_IntFreeP( &p->vNexts );
}
@@ -362,6 +364,43 @@ static int Vec_MemHashInsert( Vec_Mem_t * p, word * pEntry )
}
+/**Function*************************************************************
+
+ Synopsis [Allocates memory vector for storing truth tables.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline Vec_Mem_t * Vec_MemAllocForTT( int nVars )
+{
+ int Value, nWords = (nVars <= 6 ? 1 : (1 << (nVars - 6)));
+ word * uTruth = ABC_ALLOC( word, nWords );
+ Vec_Mem_t * vTtMem = Vec_MemAlloc( nWords, 12 );
+ Vec_MemHashAlloc( vTtMem, 10000 );
+ memset( uTruth, 0x00, sizeof(word) * nWords );
+ Value = Vec_MemHashInsert( vTtMem, uTruth ); assert( Value == 0 );
+ memset( uTruth, 0xAA, sizeof(word) * nWords );
+ Value = Vec_MemHashInsert( vTtMem, uTruth ); assert( Value == 1 );
+ ABC_FREE( uTruth );
+ return vTtMem;
+}
+static inline void Vec_MemDumpTruthTables( Vec_Mem_t * p, char * pName, int nLutSize )
+{
+ FILE * pFile;
+ char pFileName[1000];
+ sprintf( pFileName, "tt_%s_%02d.txt", pName, nLutSize );
+ pFile = fopen( pFileName, "wb" );
+ Vec_MemDump( pFile, p );
+ fclose( pFile );
+ printf( "Dumped %d %d-var truth tables into file \"%s\" (%.2f MB).\n",
+ Vec_MemEntryNum(p), nLutSize, pFileName,
+ 8.0 * Vec_MemEntryNum(p) * Vec_MemEntrySize(p) / (1 << 20) );
+}
+
ABC_NAMESPACE_HEADER_END
#endif
diff --git a/src/proof/int/intCore.c b/src/proof/int/intCore.c
index f4251215..8e0fb441 100644
--- a/src/proof/int/intCore.c
+++ b/src/proof/int/intCore.c
@@ -24,7 +24,7 @@
ABC_NAMESPACE_IMPL_START
-////////////////////////////////////////////////////////////////////////
+////////////////////////////////////////////////////////////////////////`
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
generated by cgit v1.2.3 (git 2.25.1) at 2025-10-31 04:07:07 +0000