summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--src/aig/gia/giaIf.c120
-rw-r--r--src/base/abci/abc.c32
-rw-r--r--src/map/if/if.h3
-rw-r--r--src/map/if/ifDsd.c91
-rw-r--r--src/map/if/ifSat.c98
5 files changed, 278 insertions, 66 deletions
diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c
index 9ab57356..a494ca8f 100644
--- a/src/aig/gia/giaIf.c
+++ b/src/aig/gia/giaIf.c
@@ -22,6 +22,8 @@
#include "aig/aig/aig.h"
#include "map/if/if.h"
#include "bool/kit/kit.h"
+#include "base/main/main.h"
+#include "sat/bsat/satSolver.h"
ABC_NAMESPACE_IMPL_START
@@ -1169,23 +1171,77 @@ int Gia_ManNodeIfToGia( Gia_Man_t * pNew, If_Man_t * pIfMan, If_Obj_t * pIfObj,
SeeAlso []
***********************************************************************/
-static inline word Gia_ManTt6Stretch( word t, int nVars )
+int Gia_ManFromIfLogicFindLut( If_Man_t * pIfMan, Gia_Man_t * pNew, If_Cut_t * pCutBest, sat_solver * pSat, Vec_Int_t * vLeaves, Vec_Int_t * vLits, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vPacking )
{
- assert( nVars >= 0 );
- if ( nVars == 0 )
- nVars++, t = (t & 0x1) | ((t & 0x1) << 1);
- if ( nVars == 1 )
- nVars++, t = (t & 0x3) | ((t & 0x3) << 2);
- if ( nVars == 2 )
- nVars++, t = (t & 0xF) | ((t & 0xF) << 4);
- if ( nVars == 3 )
- nVars++, t = (t & 0xFF) | ((t & 0xFF) << 8);
- if ( nVars == 4 )
- nVars++, t = (t & 0xFFFF) | ((t & 0xFFFF) << 16);
- if ( nVars == 5 )
- nVars++, t = (t & 0xFFFFFFFF) | ((t & 0xFFFFFFFF) << 32);
- assert( nVars == 6 );
- return t;
+ word uBound, uFree;
+ int nLutSize = (int)(pIfMan->pPars->pLutStruct[0] - '0');
+ int nVarsF = 0, pVarsF[IF_MAX_FUNC_LUTSIZE];
+ int nVarsB = 0, pVarsB[IF_MAX_FUNC_LUTSIZE];
+ int nVarsS = 0, pVarsS[IF_MAX_FUNC_LUTSIZE];
+ unsigned uSetNew, uSetOld;
+ int RetValue, RetValue2, k;
+ if ( Vec_IntSize(vLeaves) <= nLutSize )
+ {
+ RetValue = Gia_ManFromIfLogicCreateLut( pNew, If_CutTruthW(pIfMan, pCutBest), vLeaves, vCover, vMapping, vMapping2 );
+ // write packing
+ if ( !Gia_ObjIsCi(Gia_ManObj(pNew, Abc_Lit2Var(RetValue))) )
+ {
+ Vec_IntPush( vPacking, 1 );
+ Vec_IntPush( vPacking, Abc_Lit2Var(RetValue) );
+ Vec_IntAddToEntry( vPacking, 0, 1 );
+ }
+ return RetValue;
+ }
+ // find the bound set
+ uSetOld = If_DsdManCheckXY( pIfMan->pIfDsdMan, pCutBest->iCutDsd, nLutSize, 1, 0 );
+ // remap bound set
+ uSetNew = 0;
+ for ( k = 0; k < If_CutLeaveNum(pCutBest); k++ )
+ {
+ int iVar = Abc_Lit2Var((int)pCutBest->pPerm[k]);
+ int Value = ((uSetOld >> (k << 1)) & 3);
+ if ( Value == 1 )
+ uSetNew |= (1 << (2*iVar));
+ else if ( Value == 3 )
+ uSetNew |= (3 << (2*iVar));
+ else assert( Value == 0 );
+ }
+ RetValue = If_ManSatCheckXY( pSat, nLutSize, If_CutTruthW(pIfMan, pCutBest), pCutBest->nLeaves, uSetNew, &uBound, &uFree, vLits );
+ assert( RetValue );
+ // collect variables
+ for ( k = 0; k < If_CutLeaveNum(pCutBest); k++ )
+ {
+ int Value = ((uSetNew >> (k << 1)) & 3);
+ if ( Value == 0 )
+ pVarsF[nVarsF++] = k;
+ else if ( Value == 1 )
+ pVarsB[nVarsB++] = k;
+ else if ( Value == 3 )
+ pVarsS[nVarsS++] = k;
+ else assert( Value == 0 );
+ }
+ // collect bound set variables
+ Vec_IntClear( vLits );
+ for ( k = 0; k < nVarsS; k++ )
+ Vec_IntPush( vLits, Vec_IntEntry(vLeaves, pVarsS[k]) );
+ for ( k = 0; k < nVarsB; k++ )
+ Vec_IntPush( vLits, Vec_IntEntry(vLeaves, pVarsB[k]) );
+ RetValue = Gia_ManFromIfLogicCreateLut( pNew, &uBound, vLits, vCover, vMapping, vMapping2 );
+ // collecct free set variables
+ Vec_IntClear( vLits );
+ Vec_IntPush( vLits, RetValue );
+ for ( k = 0; k < nVarsS; k++ )
+ Vec_IntPush( vLits, Vec_IntEntry(vLeaves, pVarsS[k]) );
+ for ( k = 0; k < nVarsF; k++ )
+ Vec_IntPush( vLits, Vec_IntEntry(vLeaves, pVarsF[k]) );
+ // add packing
+ RetValue2 = Gia_ManFromIfLogicCreateLut( pNew, &uFree, vLits, vCover, vMapping, vMapping2 );
+ // write packing
+ Vec_IntPush( vPacking, 2 );
+ Vec_IntPush( vPacking, Abc_Lit2Var(RetValue) );
+ Vec_IntPush( vPacking, Abc_Lit2Var(RetValue2) );
+ Vec_IntAddToEntry( vPacking, 0, 1 );
+ return RetValue2;
}
/**Function*************************************************************
@@ -1205,8 +1261,8 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
If_Cut_t * pCutBest;
If_Obj_t * pIfObj, * pIfLeaf;
Vec_Int_t * vMapping, * vMapping2, * vPacking = NULL;
- Vec_Int_t * vLeaves, * vLeaves2, * vCover;
-// word Truth = 0, * pTruthTable;
+ Vec_Int_t * vLeaves, * vLeaves2, * vCover, * vLits;
+ sat_solver * pSat = NULL;
int i, k, Entry;
assert( !pIfMan->pPars->fDeriveLuts || pIfMan->pPars->fTruth );
// if ( pIfMan->pPars->fEnableCheck07 )
@@ -1222,6 +1278,7 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
// create new manager
pNew = Gia_ManStart( If_ManObjNum(pIfMan) );
// iterate through nodes used in the mapping
+ vLits = Vec_IntAlloc( 1000 );
vCover = Vec_IntAlloc( 1 << 16 );
vLeaves = Vec_IntAlloc( 16 );
vLeaves2 = Vec_IntAlloc( 16 );
@@ -1241,7 +1298,17 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
If_CutForEachLeaf( pIfMan, pCutBest, pIfLeaf, k )
Vec_IntPush( vLeaves, pIfLeaf->iCopy );
// perform one of the two types of mapping: with and without structures
- if ( pIfMan->pPars->fDeriveLuts && pIfMan->pPars->fTruth )
+ if ( pIfMan->pPars->fUseDsd )
+ {
+ if ( pSat == NULL )
+ pSat = (sat_solver *)If_ManSatBuildXY( (int)(pIfMan->pPars->pLutStruct[0] - '0') );
+ if ( pIfMan->pPars->pLutStruct && pIfMan->pPars->fDeriveLuts )
+ pIfObj->iCopy = Gia_ManFromIfLogicFindLut( pIfMan, pNew, pCutBest, pSat, vLeaves, vLits, vCover, vMapping, vMapping2, vPacking );
+ else
+ pIfObj->iCopy = Gia_ManFromIfLogicCreateLut( pNew, If_CutTruthW(pIfMan, pCutBest), vLeaves, vCover, vMapping, vMapping2 );
+ pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl );
+ }
+ else if ( pIfMan->pPars->fDeriveLuts && pIfMan->pPars->fTruth )
{
// perform decomposition of the cut
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 );
@@ -1274,9 +1341,12 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan )
}
else assert( 0 );
}
+ Vec_IntFree( vLits );
Vec_IntFree( vCover );
Vec_IntFree( vLeaves );
Vec_IntFree( vLeaves2 );
+ if ( pSat != NULL )
+ sat_solver_delete(pSat);
// printf( "Mapping array size: IfMan = %d. Gia = %d. Increase = %.2f\n",
// If_ManObjNum(pIfMan), Gia_ManObjNum(pNew), 1.0 * Gia_ManObjNum(pNew) / If_ManObjNum(pIfMan) );
// finish mapping
@@ -1458,8 +1528,10 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp, int fNormalized )
If_Man_t * pIfMan;
If_Par_t * pPars = (If_Par_t *)pp;
// disable cut minimization when GIA strucure is needed
- if ( !pPars->fDelayOpt && !pPars->fUserRecLib && !pPars->fDeriveLuts )
+// if ( !pPars->fDelayOpt && !pPars->fUserRecLib && !pPars->fDeriveLuts )
+ if ( !pPars->fDelayOpt && !pPars->fUserRecLib && !pPars->pLutStruct )
pPars->fCutMin = 0;
+
// reconstruct GIA according to the hierarchy manager
assert( pPars->pTimesArr == NULL );
assert( pPars->pTimesReq == NULL );
@@ -1488,6 +1560,14 @@ Gia_Man_t * Gia_ManPerformMapping( Gia_Man_t * p, void * pp, int fNormalized )
Gia_ManStop( p );
return NULL;
}
+ // create DSD manager
+ if ( pPars->fUseDsd )
+ {
+ If_DsdMan_t * p = (If_DsdMan_t *)Abc_FrameReadManDsd();
+ assert( pPars->nLutSize <= If_DsdManVarNum(p) );
+ assert( (pPars->pLutStruct == NULL && If_DsdManLutSize(p) == 0) || (pPars->pLutStruct && pPars->pLutStruct[0] - '0' == If_DsdManLutSize(p)) );
+ pIfMan->pIfDsdMan = (If_DsdMan_t *)Abc_FrameReadManDsd();
+ }
// compute switching for the IF objects
if ( pPars->fPower )
{
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 5361e1b2..0c9e3098 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -29244,7 +29244,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
}
pPars->pLutLib = (If_LibLut_t *)pAbc->pLibLut;
Extra_UtilGetoptReset();
- while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRDEWSTqalepmrsdbgyojikfuztvh" ) ) != EOF )
+ while ( ( c = Extra_UtilGetopt( argc, argv, "KCFAGRDEWSTqalepmrsdbgyojikfuztnvh" ) ) != EOF )
{
switch ( c )
{
@@ -29434,6 +29434,9 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
case 't':
pPars->fRepack ^= 1;
break;
+ case 'n':
+ pPars->fUseDsd ^= 1;
+ break;
case 'v':
pPars->fVerbose ^= 1;
break;
@@ -29597,6 +29600,7 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->nLutSize = pPars->nGateSize;
}
+
if ( pPars->fUseDsd )
{
pPars->fTruth = 1;
@@ -29605,6 +29609,29 @@ int Abc_CommandAbc9If( Abc_Frame_t * pAbc, int argc, char ** argv )
pPars->fUsePerm = 1;
}
+ if ( pPars->fUseDsd )
+ {
+ int LutSize = (pPars->pLutStruct && pPars->pLutStruct[2] == 0)? pPars->pLutStruct[0] - '0' : 0;
+ If_DsdMan_t * p = (If_DsdMan_t *)Abc_FrameReadManDsd();
+ if ( pPars->pLutStruct && pPars->pLutStruct[2] != 0 )
+ {
+ printf( "DSD only works for LUT structures XY.\n" );
+ return 0;
+ }
+ if ( p && pPars->nLutSize > If_DsdManVarNum(p) )
+ {
+ printf( "DSD manager has incompatible number of variables.\n" );
+ return 0;
+ }
+ if ( p && LutSize != If_DsdManLutSize(p) )
+ {
+ printf( "DSD manager has different LUT size.\n" );
+ return 0;
+ }
+ if ( p == NULL )
+ Abc_FrameSetManDsd( If_DsdManAlloc(pPars->nLutSize, LutSize) );
+ }
+
// complain if truth tables are requested but the cut size is too large
if ( pPars->fTruth && pPars->nLutSize > IF_MAX_FUNC_LUTSIZE )
{
@@ -29636,7 +29663,7 @@ usage:
sprintf(LutSize, "library" );
else
sprintf(LutSize, "%d", pPars->nLutSize );
- Abc_Print( -2, "usage: &if [-KCFAGRT num] [-DEW float] [-S str] [-qarlepmsdbgyojikfucztvh]\n" );
+ Abc_Print( -2, "usage: &if [-KCFAGRT num] [-DEW float] [-S str] [-qarlepmsdbgyojikfucztnvh]\n" );
Abc_Print( -2, "\t performs FPGA technology mapping of the network\n" );
Abc_Print( -2, "\t-K num : the number of LUT inputs (2 < num < %d) [default = %s]\n", IF_MAX_LUTSIZE+1, LutSize );
Abc_Print( -2, "\t-C num : the max number of priority cuts (0 < num < 2^12) [default = %d]\n", pPars->nCutsMax );
@@ -29669,6 +29696,7 @@ usage:
Abc_Print( -2, "\t-u : toggles enabling additional check [default = %s]\n", pPars->fEnableCheck75u? "yes": "no" );
Abc_Print( -2, "\t-z : toggles deriving LUTs when mapping into LUT structures [default = %s]\n", pPars->fDeriveLuts? "yes": "no" );
Abc_Print( -2, "\t-t : toggles repacking LUTs into new structures [default = %s]\n", pPars->fRepack? "yes": "no" );
+ Abc_Print( -2, "\t-n : toggles computing DSDs of the cut functions [default = %s]\n", pPars->fUseDsd? "yes": "no" );
Abc_Print( -2, "\t-v : toggles verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : prints the command usage\n");
return 1;
diff --git a/src/map/if/if.h b/src/map/if/if.h
index c8b04ef1..cf26c53c 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -572,6 +572,9 @@ extern void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj
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 );
+/*=== ifSat.c ==========================================================*/
+extern void * If_ManSatBuildXY( int nLutSize );
+extern int If_ManSatCheckXY( void * pSat, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, Vec_Int_t * vLits );
/*=== ifSeq.c =============================================================*/
extern int If_ManPerformMappingSeq( If_Man_t * p );
/*=== ifTime.c ============================================================*/
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c
index af586ce2..63341ad3 100644
--- a/src/map/if/ifDsd.c
+++ b/src/map/if/ifDsd.c
@@ -62,7 +62,8 @@ struct If_DsdMan_t_
Mem_Flex_t * pMem; // memory for nodes
Vec_Ptr_t * vObjs; // objects
Vec_Int_t * vNexts; // next pointers
- Vec_Int_t * vNodes; // temp
+ Vec_Int_t * vTemp1; // temp
+ Vec_Int_t * vTemp2; // temp
word ** pTtElems; // elementary TTs
Vec_Mem_t * vTtMem; // truth table memory and hash table
Vec_Ptr_t * vTtDecs; // truth table decompositions
@@ -198,7 +199,8 @@ If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize )
p->vNexts = Vec_IntAlloc( 10000 );
If_DsdObjAlloc( p, IF_DSD_CONST0, 0 );
If_DsdObjAlloc( p, IF_DSD_VAR, 0 )->nSupp = 1;
- p->vNodes = Vec_IntAlloc( 32 );
+ p->vTemp1 = Vec_IntAlloc( 32 );
+ p->vTemp2 = Vec_IntAlloc( 32 );
p->pTtElems = If_ManDsdTtElems();
p->vTtDecs = Vec_PtrAlloc( 1000 );
p->vTtMem = Vec_MemAlloc( Abc_TtWordNum(nVars), 12 );
@@ -227,7 +229,8 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
Vec_VecFree( (Vec_Vec_t *)p->vTtDecs );
Vec_MemHashFree( p->vTtMem );
Vec_MemFreeP( &p->vTtMem );
- Vec_IntFreeP( &p->vNodes );
+ Vec_IntFreeP( &p->vTemp1 );
+ Vec_IntFreeP( &p->vTemp2 );
Vec_IntFreeP( &p->vNexts );
Vec_PtrFreeP( &p->vObjs );
Mem_FlexStop( p->pMem, 0 );
@@ -662,20 +665,29 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName )
SeeAlso []
***********************************************************************/
-void If_DsdManCollect_rec( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes )
+void If_DsdManCollect_rec( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes, Vec_Int_t * vFirsts, int * pnSupp )
{
- int i, iFanin;
+ int i, iFanin, iFirst;
If_DsdObj_t * pObj = If_DsdVecObj( p->vObjs, Id );
- if ( If_DsdObjType(pObj) == IF_DSD_CONST0 || If_DsdObjType(pObj) == IF_DSD_VAR )
+ if ( If_DsdObjType(pObj) == IF_DSD_CONST0 )
+ return;
+ if ( If_DsdObjType(pObj) == IF_DSD_VAR )
+ {
+ (*pnSupp)++;
return;
+ }
+ iFirst = *pnSupp;
If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i )
- If_DsdManCollect_rec( p, Abc_Lit2Var(iFanin), vNodes );
+ If_DsdManCollect_rec( p, Abc_Lit2Var(iFanin), vNodes, vFirsts, pnSupp );
Vec_IntPush( vNodes, Id );
+ Vec_IntPush( vFirsts, iFirst );
}
-void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes )
+void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes, Vec_Int_t * vFirsts )
{
+ int nSupp = 0;
Vec_IntClear( vNodes );
- If_DsdManCollect_rec( p, Id, vNodes );
+ Vec_IntClear( vFirsts );
+ If_DsdManCollect_rec( p, Id, vNodes, vFirsts, &nSupp );
}
/**Function*************************************************************
@@ -1129,7 +1141,7 @@ void If_DsdManGetSuppSizes( If_DsdMan_t * p, If_DsdObj_t * pObj, int * pSSizes )
pSSizes[i] = If_DsdObjSuppSize(pFanin);
}
// checks if there is a way to package some fanins
-unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
+unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
{
int i[6], LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR];
int nFans = If_DsdObjFaninNum(pObj), pFirsts[DAU_MAX_VAR];
@@ -1148,7 +1160,8 @@ unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll
if ( !fDerive )
return ~0;
If_DsdManComputeFirst( p, pObj, pFirsts );
- return If_DsdSign(p, pObj, i[0], pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], pFirsts[i[1]], 0);
+ return If_DsdSign(p, pObj, i[0], iFirst + pFirsts[i[0]], 0) |
+ If_DsdSign(p, pObj, i[1], iFirst + pFirsts[i[1]], 0);
}
if ( pObj->nFans == 3 )
return 0;
@@ -1163,7 +1176,9 @@ unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll
if ( !fDerive )
return ~0;
If_DsdManComputeFirst( p, pObj, pFirsts );
- return If_DsdSign(p, pObj, i[0], pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], pFirsts[i[1]], 0) | If_DsdSign(p, pObj, i[2], pFirsts[i[2]], 0);
+ return If_DsdSign(p, pObj, i[0], iFirst + pFirsts[i[0]], 0) |
+ If_DsdSign(p, pObj, i[1], iFirst + pFirsts[i[1]], 0) |
+ If_DsdSign(p, pObj, i[2], iFirst + pFirsts[i[2]], 0);
}
if ( pObj->nFans == 4 )
return 0;
@@ -1179,12 +1194,15 @@ unsigned If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll
if ( !fDerive )
return ~0;
If_DsdManComputeFirst( p, pObj, pFirsts );
- return If_DsdSign(p, pObj, i[0], pFirsts[i[0]], 0) | If_DsdSign(p, pObj, i[1], pFirsts[i[1]], 0) | If_DsdSign(p, pObj, i[2], pFirsts[i[2]], 0) | If_DsdSign(p, pObj, i[3], pFirsts[i[3]], 0);
+ return If_DsdSign(p, pObj, i[0], iFirst + pFirsts[i[0]], 0) |
+ If_DsdSign(p, pObj, i[1], iFirst + pFirsts[i[1]], 0) |
+ If_DsdSign(p, pObj, i[2], iFirst + pFirsts[i[2]], 0) |
+ If_DsdSign(p, pObj, i[3], iFirst + pFirsts[i[3]], 0);
}
return 0;
}
// checks if there is a way to package some fanins
-unsigned If_DsdManCheckMux( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
+unsigned If_DsdManCheckMux( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
{
int LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR];
assert( If_DsdObjFaninNum(pObj) == 3 );
@@ -1194,28 +1212,28 @@ unsigned If_DsdManCheckMux( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, i
assert( LimitOut < LutSize );
// first input
SizeIn = pSSizes[0] + pSSizes[1];
- SizeOut = pSSizes[2];
+ SizeOut = pSSizes[0] + pSSizes[2] + 1;
if ( SizeIn <= LutSize && SizeOut <= LimitOut )
{
if ( !fDerive )
return ~0;
If_DsdManComputeFirst( p, pObj, pFirsts );
- return If_DsdSign(p, pObj, 0, pFirsts[0], 1) | If_DsdSign(p, pObj, 1, pFirsts[1], 0);
+ return If_DsdSign(p, pObj, 0, iFirst + pFirsts[0], 1) | If_DsdSign(p, pObj, 1, iFirst + pFirsts[1], 0);
}
// second input
SizeIn = pSSizes[0] + pSSizes[2];
- SizeOut = pSSizes[1];
+ SizeOut = pSSizes[0] + pSSizes[1] + 1;
if ( SizeIn <= LutSize && SizeOut <= LimitOut )
{
if ( !fDerive )
return ~0;
If_DsdManComputeFirst( p, pObj, pFirsts );
- return If_DsdSign(p, pObj, 0, pFirsts[0], 1) | If_DsdSign(p, pObj, 2, pFirsts[2], 0);
+ return If_DsdSign(p, pObj, 0, iFirst + pFirsts[0], 1) | If_DsdSign(p, pObj, 2, iFirst + pFirsts[2], 0);
}
return 0;
}
// checks if there is a way to package some fanins
-unsigned If_DsdManCheckPrime( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
+unsigned If_DsdManCheckPrime( If_DsdMan_t * p, int iFirst, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fDerive, int fVerbose )
{
int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR], pFirsts[DAU_MAX_VAR];
int truthId = If_DsdObjTruthId( p, pObj );
@@ -1245,7 +1263,7 @@ Dau_DecPrintSets( vSets, nFans );
SizeIn += pSSizes[v];
SizeOut += pSSizes[v];
}
- else assert( Value == 0 );
+ else assert( 0 );
if ( SizeIn > LutSize || SizeOut > LimitOut )
break;
}
@@ -1262,10 +1280,10 @@ Dau_DecPrintSets( vSets, nFans );
if ( Value == 0 )
{}
else if ( Value == 1 )
- uSign |= If_DsdSign(p, pObj, v, pFirsts[v], 0);
+ uSign |= If_DsdSign(p, pObj, v, iFirst + pFirsts[v], 0);
else if ( Value == 3 )
- uSign |= If_DsdSign(p, pObj, v, pFirsts[v], 1);
- else assert( Value == 0 );
+ uSign |= If_DsdSign(p, pObj, v, iFirst + pFirsts[v], 1);
+ else assert( 0 );
}
return uSign;
}
@@ -1274,7 +1292,13 @@ Dau_DecPrintSets( vSets, nFans );
}
unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, int fVerbose )
{
- If_DsdObj_t * pObj, * pTemp; int i, Mask;
+ 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 );
@@ -1284,20 +1308,21 @@ unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive,
printf( " Trivial\n" );
return ~0;
}
- If_DsdManCollect( p, pObj->Id, p->vNodes );
- If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
+ If_DsdManCollect( p, pObj->Id, p->vTemp1, p->vTemp2 );
+ If_DsdVecForEachObjVec( p->vTemp1, p->vObjs, pTemp, i )
if ( If_DsdObjSuppSize(pTemp) <= LutSize && If_DsdObjSuppSize(pObj) - If_DsdObjSuppSize(pTemp) <= LutSize - 1 )
{
if ( fVerbose )
printf( " Dec using node " );
if ( fVerbose )
If_DsdManPrintOne( stdout, p, pTemp->Id, NULL, 1 );
- return ~0;
+ iFirst = Vec_IntEntry(p->vTemp2, i);
+ return If_DsdSign_rec(p, pTemp, &iFirst);
}
- If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
+ If_DsdVecForEachObjVec( p->vTemp1, p->vObjs, pTemp, i )
if ( (If_DsdObjType(pTemp) == IF_DSD_AND || If_DsdObjType(pTemp) == IF_DSD_XOR) && If_DsdObjFaninNum(pTemp) > 2 && If_DsdObjSuppSize(pTemp) > LutSize )
{
- if ( (Mask = If_DsdManCheckAndXor(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
+ if ( (Mask = If_DsdManCheckAndXor(p, Vec_IntEntry(p->vTemp2, i), pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
{
if ( fVerbose )
printf( " " );
@@ -1308,10 +1333,10 @@ unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive,
return Mask;
}
}
- If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
+ If_DsdVecForEachObjVec( p->vTemp1, p->vObjs, pTemp, i )
if ( If_DsdObjType(pTemp) == IF_DSD_MUX && If_DsdObjSuppSize(pTemp) > LutSize )
{
- if ( (Mask = If_DsdManCheckMux(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
+ if ( (Mask = If_DsdManCheckMux(p, Vec_IntEntry(p->vTemp2, i), pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
{
if ( fVerbose )
printf( " " );
@@ -1322,10 +1347,10 @@ unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive,
return Mask;
}
}
- If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
+ If_DsdVecForEachObjVec( p->vTemp1, p->vObjs, pTemp, i )
if ( If_DsdObjType(pTemp) == IF_DSD_PRIME && If_DsdObjSuppSize(pTemp) > LutSize )
{
- if ( (Mask = If_DsdManCheckPrime(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
+ if ( (Mask = If_DsdManCheckPrime(p, Vec_IntEntry(p->vTemp2, i), pTemp, If_DsdObjSuppSize(pObj), LutSize, fDerive, fVerbose)) )
{
if ( fVerbose )
printf( " " );
diff --git a/src/map/if/ifSat.c b/src/map/if/ifSat.c
index 3fec34e0..cfce7369 100644
--- a/src/map/if/ifSat.c
+++ b/src/map/if/ifSat.c
@@ -42,7 +42,7 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
-sat_solver * If_ManSatBuildXY( int nLutSize )
+void * If_ManSatBuildXY( int nLutSize )
{
int nMintsL = (1 << nLutSize);
int nMintsF = (1 << (2 * nLutSize - 1));
@@ -59,6 +59,54 @@ sat_solver * If_ManSatBuildXY( int nLutSize )
/**Function*************************************************************
+ Synopsis [Verification for 6-input function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static word If_ManSat6ComposeLut4( int t, word f[4], int k )
+{
+ int m, v, nMints = (1 << k);
+ word c, r = 0;
+ assert( k <= 4 );
+ for ( m = 0; m < nMints; m++ )
+ {
+ if ( !((t >> m) & 1) )
+ continue;
+ c = ~(word)0;
+ for ( v = 0; v < k; v++ )
+ c &= ((m >> v) & 1) ? f[v] : ~f[v];
+ r |= c;
+ }
+ return r;
+}
+word If_ManSat6Truth( word uBound, word uFree, int * pBSet, int nBSet, int * pSSet, int nSSet, int * pFSet, int nFSet )
+{
+ word r, q, f[4];
+ int i, k = 0;
+ // bound set vars
+ for ( i = 0; i < nSSet; i++ )
+ f[k++] = s_Truths6[pSSet[i]];
+ for ( i = 0; i < nBSet; i++ )
+ f[k++] = s_Truths6[pBSet[i]];
+ q = If_ManSat6ComposeLut4( (int)(uBound & 0xffff), f, k );
+ // free set vars
+ k = 0;
+ f[k++] = q;
+ for ( i = 0; i < nSSet; i++ )
+ f[k++] = s_Truths6[pSSet[i]];
+ for ( i = 0; i < nFSet; i++ )
+ f[k++] = s_Truths6[pFSet[i]];
+ r = If_ManSat6ComposeLut4( (int)(uFree & 0xffff), f, k );
+ return r;
+}
+
+/**Function*************************************************************
+
Synopsis [Returns config string for the given truth table.]
Description []
@@ -68,14 +116,16 @@ sat_solver * If_ManSatBuildXY( int nLutSize )
SeeAlso []
***********************************************************************/
-int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, Vec_Int_t * vLits )
+int If_ManSatCheckXY( void * pSat, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, Vec_Int_t * vLits )
{
- int iBSet, nBSet = 0;
- int iSSet, nSSet = 0;
- int iFSet, nFSet = 0;
+ sat_solver * p = (sat_solver *)pSat;
+ int iBSet, nBSet = 0, pBSet[IF_MAX_FUNC_LUTSIZE];
+ int iSSet, nSSet = 0, pSSet[IF_MAX_FUNC_LUTSIZE];
+ int iFSet, nFSet = 0, pFSet[IF_MAX_FUNC_LUTSIZE];
int nMintsL = (1 << nLutSize);
int nMintsF = (1 << (2 * nLutSize - 1));
int v, Value, m, mNew, nMintsFNew, nMintsLNew;
+ word Res;
// collect variable sets
Dau_DecSortSet( uSet, nVars, &nBSet, &nSSet, &nFSet );
assert( nBSet + nSSet + nFSet == nVars );
@@ -94,13 +144,13 @@ int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, un
if ( Value == 0 ) // FS
{
if ( ((m >> v) & 1) )
- mNew |= 1 << (nLutSize + nSSet + iFSet);
+ mNew |= 1 << (nLutSize + nSSet + iFSet), pFSet[iFSet] = v;
iFSet++;
}
else if ( Value == 1 ) // BS
{
if ( ((m >> v) & 1) )
- mNew |= 1 << (nSSet + iBSet);
+ mNew |= 1 << (nSSet + iBSet), pBSet[iBSet] = v;
iBSet++;
}
else if ( Value == 3 ) // SS
@@ -109,6 +159,7 @@ int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, un
{
mNew |= 1 << iSSet;
mNew |= 1 << (nLutSize + iSSet);
+ pSSet[iSSet] = v;
}
iSSet++;
}
@@ -143,11 +194,36 @@ int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, un
// collect configs
assert( nSSet + nFSet + 1 <= nLutSize );
*pTFree = 0;
- nMintsLNew = (1 << (nSSet + nFSet + 1));
+ nMintsLNew = (1 << (1 + nSSet + nFSet));
for ( m = 0; m < nMintsLNew; m++ )
if ( sat_solver_var_value(p, nMintsL+m) )
Abc_TtSetBit( pTFree, m );
- *pTFree = Abc_Tt6Stretch( *pTFree, nSSet + nFSet + 1 );
+ *pTFree = Abc_Tt6Stretch( *pTFree, 1 + nSSet + nFSet );
+ if ( nVars != 6 )
+ return 1;
+ // verify the result
+ Res = If_ManSat6Truth( *pTBound, *pTFree, pBSet, nBSet, pSSet, nSSet, pFSet, nFSet );
+ if ( pTruth[0] != Res )
+ {
+ Dau_DsdPrintFromTruth( pTruth, nVars );
+ Dau_DsdPrintFromTruth( &Res, nVars );
+ Dau_DsdPrintFromTruth( pTBound, nSSet+nBSet );
+ Dau_DsdPrintFromTruth( pTFree, nSSet+nFSet+1 );
+ printf( "Verification failed!\n" );
+ }
+/*
+ else
+ {
+// Kit_DsdPrintFromTruth( (unsigned*)pTBound, nSSet+nBSet ); printf( "\n" );
+// Kit_DsdPrintFromTruth( (unsigned*)pTFree, nSSet+nFSet+1 ); printf( "\n" );
+
+ Dau_DsdPrintFromTruth( pTruth, nVars );
+ Dau_DsdPrintFromTruth( &Res, nVars );
+ Dau_DsdPrintFromTruth( pTBound, nSSet+nBSet );
+ Dau_DsdPrintFromTruth( pTFree, nSSet+nFSet+1 );
+ printf( "Verification OK!\n" );
+ }
+*/
return 1;
}
@@ -166,7 +242,7 @@ void If_ManSatTest2()
{
int nVars = 6;
int nLutSize = 4;
- sat_solver * p = If_ManSatBuildXY( nLutSize );
+ sat_solver * p = (sat_solver *)If_ManSatBuildXY( nLutSize );
// char * pDsd = "(abcdefg)";
// char * pDsd = "([a!bc]d!e)";
char * pDsd = "0123456789ABCDEF{abcdef}";
@@ -194,7 +270,7 @@ void If_ManSatTest()
{
int nVars = 4;
int nLutSize = 3;
- sat_solver * p = If_ManSatBuildXY( nLutSize );
+ sat_solver * p = (sat_solver *)If_ManSatBuildXY( nLutSize );
word t = 0x183C, * pTruth = &t;
word uBound, uFree;
unsigned uSet;
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 23:14:07 +0000