Skip to content

A
abc
Commit 5f9ca14a by Alan Mishchenko
Options

Changes to LUT mappers.

parent 14aae240
Showing with 278 additions and 66 deletions
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 )
{
......
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;
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 ============================================================*/
......
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( " " );
......
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;
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment