luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Changes to LUT mappers.

This commit is contained in:
Alan Mishchenko 2014-02-27 21:11:05 -08:00
parent caa2227b11
commit b556c2591e
9 changed files with 398 additions and 36 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
abclib.dsp
View File

@ -2343,6 +2343,10 @@ SOURCE=.\src\map\if\ifReduce.c
# End Source File
# Begin Source File
SOURCE=.\src\map\if\ifSat.c
# End Source File
# Begin Source File
SOURCE=.\src\map\if\ifSelect.c
# End Source File
# Begin Source File

7
src/base/abci/abc.c
View File

@ -974,6 +974,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
{
// extern void Dau_DsdTest();
// Dau_DsdTest();
// extern void If_ManSatTest();
// If_ManSatTest();
}
if ( Sdm_ManCanRead() )
@ -2274,7 +2276,12 @@ int Abc_CommandPrintDsd( Abc_Frame_t * pAbc, int argc, char ** argv )
// Extra_PrintBinary( stdout, pTruth, 1 << Abc_ObjFaninNum(pObj) );
// Abc_Print( -1, "\n" );
if ( fPrintDec )//&&Abc_ObjFaninNum(pObj) <= 6 )
{
word * pTruthW = (word *)pTruth;
if ( Abc_ObjFaninNum(pObj) < 6 )
pTruthW[0] = Abc_Tt6Stretch( pTruthW[0], Abc_ObjFaninNum(pObj) );
Dau_DecTrySets( (word *)pTruth, Abc_ObjFaninNum(pObj), 1 );
}
if ( fProfile )
Kit_TruthPrintProfile( pTruth, Abc_ObjFaninNum(pObj) );
else if ( fCofactor )

7
src/map/if/if.h
View File

@ -55,7 +55,7 @@ ABC_NAMESPACE_HEADER_START
// the largest possible user cut cost
#define IF_COST_MAX 8191 // ((1<<13)-1)
#define IF_BIG_CHAR 120
#define IF_BIG_CHAR ((char)120)
// object types
typedef enum {
@ -233,7 +233,8 @@ struct If_Man_t_
int nCuts5, nCuts5a;
If_DsdMan_t * pIfDsdMan;
Vec_Mem_t * vTtMem; // truth table memory and hash table
Vec_Int_t * vDsds; // mapping of truth table into DSD
Vec_Int_t * vTtDsds; // mapping of truth table into DSD
Vec_Str_t * vTtPerms; // mapping of truth table into permutations
int nBestCutSmall[2];
// timing manager
@ -520,7 +521,7 @@ extern void If_DsdManDump( If_DsdMan_t * p );
extern void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose );
extern void If_DsdManFree( If_DsdMan_t * p );
extern int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm, char * pLutStruct );
extern int If_DsdManCheckDec( If_DsdMan_t * pIfMan, int iDsd );
extern int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd );
/*=== ifLib.c =============================================================*/
extern If_LibLut_t * If_LibLutRead( char * FileName );
extern If_LibLut_t * If_LibLutDup( If_LibLut_t * p );

132
src/map/if/ifDsd.c
View File

@ -505,9 +505,10 @@ int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word
unsigned * pSpot = If_DsdObjHashLookup( p, Type, pLits, nLits, truthId );
if ( *pSpot )
return *pSpot;
if ( truthId >= 0 && truthId == Vec_MemEntryNum(p->vTtMem)-1 )
if ( truthId >= 0 && truthId == Vec_PtrSize(p->vTtDecs) )
{
Vec_Int_t * vSets = Dau_DecFindSets( pTruth, nLits );
assert( truthId == Vec_MemEntryNum(p->vTtMem)-1 );
Vec_PtrPush( p->vTtDecs, vSets );
// Dau_DecPrintSets( vSets, nLits );
}
@ -533,7 +534,8 @@ void If_DsdManComputeTruth_rec( If_DsdMan_t * p, int iDsd, word * pRes, unsigned
If_DsdObj_t * pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iDsd) );
if ( If_DsdObjType(pObj) == IF_DSD_VAR )
{
int iPermLit = (int)pPermLits[(*pnSupp)++];
int iPermLit = pPermLits ? (int)pPermLits[*pnSupp] : Abc_Var2Lit(*pnSupp, 0);
(*pnSupp)++;
assert( (*pnSupp) <= p->nVars );
Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], p->nWords, fCompl ^ Abc_LitIsCompl(iPermLit) );
return;
@ -589,7 +591,8 @@ word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLi
Abc_TtConst1( pRes, p->nWords );
else if ( pObj->Type == IF_DSD_VAR )
{
int iPermLit = (int)pPermLits[nSupp++];
int iPermLit = pPermLits ? (int)pPermLits[nSupp] : Abc_Var2Lit(nSupp, 0);
nSupp++;
Abc_TtCopy( pRes, p->pTtElems[Abc_Lit2Var(iPermLit)], p->nWords, Abc_LitIsCompl(iDsd) ^ Abc_LitIsCompl(iPermLit) );
}
else
@ -923,7 +926,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
int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize )
int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fVerbose )
{
int i[6], LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR];
int nFans = If_DsdObjFaninNum(pObj);
@ -953,12 +956,49 @@ int If_DsdManCheckAndXor( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int
continue;
return (1 << i[0]) | (1 << i[1]) | (1 << i[2]);
}
if ( pObj->nFans == 4 )
return 0;
for ( i[0] = 0; i[0] < nFans; i[0]++ )
for ( i[1] = i[0]+1; i[1] < nFans; i[1]++ )
for ( i[2] = i[1]+1; i[2] < nFans; i[2]++ )
for ( i[3] = i[2]+1; i[3] < nFans; i[3]++ )
{
SizeIn = pSSizes[i[0]] + pSSizes[i[1]] + pSSizes[i[2]] + pSSizes[i[3]];
SizeOut = pObj->nSupp - SizeIn;
if ( SizeIn > LutSize || SizeOut > LimitOut )
continue;
return (1 << i[0]) | (1 << i[1]) | (1 << i[2]) | (1 << i[3]);
}
return 0;
}
// checks if there is a way to package some fanins
int If_DsdManCheckPrime( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize )
int If_DsdManCheckMux( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fVerbose )
{
int LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR];
assert( If_DsdObjFaninNum(pObj) == 3 );
assert( If_DsdObjSuppSize(pObj) > LutSize );
If_DsdManGetSuppSizes( p, pObj, pSSizes );
LimitOut = LutSize - (nSuppAll - If_DsdObjSuppSize(pObj) + 1);
assert( LimitOut < LutSize );
// first input
SizeIn = pSSizes[0] + pSSizes[1];
SizeOut = pSSizes[2];
if ( SizeIn <= LutSize && SizeOut <= LimitOut )
{
return 1;
}
// second input
SizeIn = pSSizes[0] + pSSizes[2];
SizeOut = pSSizes[1];
if ( SizeIn <= LutSize && SizeOut <= LimitOut )
{
return 1;
}
return 0;
}
// checks if there is a way to package some fanins
int If_DsdManCheckPrime( If_DsdMan_t * p, If_DsdObj_t * pObj, int nSuppAll, int LutSize, int fVerbose )
{
int fVerbose = 0;
int i, v, set, LimitOut, SizeIn, SizeOut, pSSizes[DAU_MAX_VAR];
int truthId = If_DsdObjTruthId( p, pObj );
int nFans = If_DsdObjFaninNum(pObj);
@ -967,10 +1007,10 @@ if ( fVerbose )
printf( "\n" );
if ( fVerbose )
Dau_DecPrintSets( vSets, nFans );
assert( pObj->nFans > 2 );
assert( If_DsdObjFaninNum(pObj) > 2 );
assert( If_DsdObjSuppSize(pObj) > LutSize );
If_DsdManGetSuppSizes( p, pObj, pSSizes );
LimitOut = LutSize - (nSuppAll - pObj->nSupp + 1);
LimitOut = LutSize - (nSuppAll - If_DsdObjSuppSize(pObj) + 1);
assert( LimitOut < LutSize );
Vec_IntForEachEntry( vSets, set, i )
{
@ -996,9 +1036,8 @@ Dau_DecPrintSets( vSets, nFans );
}
return 0;
}
int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize )
int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fVerbose )
{
int fVerbose = 0;
If_DsdObj_t * pObj, * pTemp; int i, Mask;
pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iDsd) );
if ( fVerbose )
@ -1022,7 +1061,7 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize )
If_DsdVecForEachObjVec( p->vNodes, 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)) )
if ( (Mask = If_DsdManCheckAndXor(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fVerbose)) )
{
if ( fVerbose )
printf( " " );
@ -1034,9 +1073,23 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize )
}
}
If_DsdVecForEachObjVec( p->vNodes, p->vObjs, pTemp, i )
if ( If_DsdObjType(pTemp) == IF_DSD_PRIME )
if ( If_DsdObjType(pTemp) == IF_DSD_MUX && If_DsdObjSuppSize(pTemp) > LutSize )
{
if ( (Mask = If_DsdManCheckPrime(p, pTemp, If_DsdObjSuppSize(pObj), LutSize)) )
if ( (Mask = If_DsdManCheckMux(p, pTemp, If_DsdObjSuppSize(pObj), LutSize, fVerbose)) )
{
if ( fVerbose )
printf( " " );
if ( fVerbose )
Abc_TtPrintBinary( (word *)&Mask, 4 );
if ( fVerbose )
printf( " Using multi-input MUX node\n" );
return 1;
}
}
If_DsdVecForEachObjVec( p->vNodes, 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, fVerbose)) )
{
if ( fVerbose )
printf( " " );
@ -1049,6 +1102,8 @@ int If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize )
}
if ( fVerbose )
printf( " UNDEC\n" );
// If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), NULL, 1 );
return 0;
}
int If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize )
@ -1056,6 +1111,22 @@ int If_DsdManCheckXYZ( If_DsdMan_t * p, int iDsd, int LutSize )
return 1;
}
/**Function*************************************************************
Synopsis [Checks existence of decomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd )
{
return If_DsdVecObjMark( p->vObjs, Abc_Lit2Var(iDsd) );
}
/**Function*************************************************************
Synopsis [Add the function to the DSD manager.]
@ -1075,10 +1146,10 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char
assert( nLeaves <= DAU_MAX_VAR );
Abc_TtCopy( pCopy, pTruth, p->nWords, 0 );
nSizeNonDec = Dau_DsdDecompose( pCopy, nLeaves, 0, 0, pDsd );
if ( !strcmp(pDsd, "(![(!e!d)c]!(b!a))") )
{
// if ( !strcmp(pDsd, "(![(!e!d)c]!(b!a))") )
// {
// int x = 0;
}
// }
if ( nSizeNonDec > 0 )
Abc_TtStretch6( pCopy, nSizeNonDec, p->nVars );
memset( pPerm, 0xFF, nLeaves );
@ -1096,19 +1167,36 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char
If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), pPerm, 1 );
printf( "\n" );
}
If_DsdVecObjIncRef( p->vObjs, Abc_Lit2Var(iDsd) );
if ( pLutStruct )
if ( pLutStruct && If_DsdVecObjRef(p->vObjs, Abc_Lit2Var(iDsd)) )
{
int LutSize = (int)(pLutStruct[0] - '0');
assert( pLutStruct[2] == 0 );
if ( If_DsdManCheckXY( p, iDsd, LutSize ) )
assert( pLutStruct[2] == 0 ); // XY
if ( !If_DsdManCheckXY( p, iDsd, LutSize, 0 ) )
If_DsdVecObjSetMark( p->vObjs, Abc_Lit2Var(iDsd) );
}
If_DsdVecObjIncRef( p->vObjs, Abc_Lit2Var(iDsd) );
return iDsd;
}
int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd )
/**Function*************************************************************
Synopsis [Checks existence of decomposition.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void If_DsdManTest()
{
return If_DsdVecObjMark( p->vObjs, Abc_Lit2Var(iDsd) );
Vec_Int_t * vSets;
word t = 0x5277;
t = Abc_Tt6Stretch( t, 4 );
// word t = 0xD9D900D900D900001010001000100000;
vSets = Dau_DecFindSets( &t, 6 );
Vec_IntFree( vSets );
}
////////////////////////////////////////////////////////////////////////

12
src/map/if/ifMan.c
View File

@ -86,9 +86,12 @@ If_Man_t * If_ManStart( If_Par_t * pPars )
if ( pPars->fUseDsd )
{
p->pIfDsdMan = If_DsdManAlloc( pPars->nLutSize );
p->vDsds = Vec_IntAlloc( 1000 );
Vec_IntPush( p->vDsds, 0 );
Vec_IntPush( p->vDsds, 2 );
p->vTtDsds = Vec_IntAlloc( 1000 );
Vec_IntPush( p->vTtDsds, 0 );
Vec_IntPush( p->vTtDsds, 2 );
p->vTtPerms = Vec_StrAlloc( 10000 );
Vec_StrFill( p->vTtPerms, 2 * p->pPars->nLutSize, IF_BIG_CHAR );
Vec_StrWriteEntry( p->vTtPerms, p->pPars->nLutSize, 0 );
}
// create the constant node
p->pConst1 = If_ManSetupObj( p );
@ -173,7 +176,8 @@ void If_ManStop( If_Man_t * p )
Vec_PtrFreeP( &p->vObjsRev );
Vec_PtrFreeP( &p->vLatchOrder );
Vec_IntFreeP( &p->vLags );
Vec_IntFreeP( &p->vDsds );
Vec_IntFreeP( &p->vTtDsds );
Vec_StrFreeP( &p->vTtPerms );
Vec_MemHashFree( p->vTtMem );
Vec_MemFreeP( &p->vTtMem );
Mem_FixedStop( p->pMemObj, 0 );

26
src/map/if/ifMap.c
View File

@ -140,7 +140,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
{
If_Set_t * pCutSet;
If_Cut_t * pCut0, * pCut1, * pCut;
int i, k;
int i, k, v;
assert( p->pPars->fSeqMap || !If_ObjIsAnd(pObj->pFanin0) || pObj->pFanin0->pCutSet->nCuts > 0 );
assert( p->pPars->fSeqMap || !If_ObjIsAnd(pObj->pFanin1) || pObj->pFanin1->pCutSet->nCuts > 0 );
@ -254,20 +254,32 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
if ( p->pPars->fUseDsd )
{
int truthId = Abc_Lit2Var(pCut->iCutFunc);
if ( Vec_IntSize(p->vDsds) <= truthId || Vec_IntEntry(p->vDsds, truthId) == -1 )
if ( Vec_IntSize(p->vTtDsds) <= truthId || Vec_IntEntry(p->vTtDsds, truthId) == -1 )
{
pCut->iCutDsd = If_DsdManCompute( p->pIfDsdMan, If_CutTruthW(p, pCut), pCut->nLeaves, (unsigned char *)pCut->pPerm, p->pPars->pLutStruct );
while ( Vec_IntSize(p->vDsds) <= truthId )
Vec_IntPush( p->vDsds, -1 );
Vec_IntWriteEntry( p->vDsds, truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) );
// printf( "%d(%d) ", pCut->iCutDsd, If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd ) );
while ( Vec_IntSize(p->vTtDsds) <= truthId )
{
Vec_IntPush( p->vTtDsds, -1 );
for ( v = 0; v < p->pPars->nLutSize; v++ )
Vec_StrPush( p->vTtPerms, IF_BIG_CHAR );
}
Vec_IntWriteEntry( p->vTtDsds, truthId, Abc_LitNotCond(pCut->iCutDsd, Abc_LitIsCompl(pCut->iCutFunc)) );
for ( v = 0; v < (int)pCut->nLeaves; v++ )
Vec_StrWriteEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v, (char)pCut->pPerm[v] );
}
else
pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vDsds, truthId), Abc_LitIsCompl(pCut->iCutFunc) );
{
pCut->iCutDsd = Abc_LitNotCond( Vec_IntEntry(p->vTtDsds, truthId), Abc_LitIsCompl(pCut->iCutFunc) );
for ( v = 0; v < (int)pCut->nLeaves; v++ )
pCut->pPerm[v] = (unsigned char)Vec_StrEntry( p->vTtPerms, truthId * p->pPars->nLutSize + v );
}
if ( p->pPars->pLutStruct )
{
int Value = If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd );
if ( Value != (int)pCut->fUseless )
printf( "Difference\n" );
{
}
}
}
}

199
src/map/if/ifSat.c Normal file
View File

@ -0,0 +1,199 @@
/**CFile****************************************************************
FileName [ifSat.c]
SystemName [ABC: Logic synthesis and verification system.]
PackageName [FPGA mapping based on priority cuts.]
Synopsis [SAT-based evaluation.]
Author [Alan Mishchenko]
Affiliation [UC Berkeley]
Date [Ver. 1.0. Started - November 21, 2006.]
Revision [$Id: ifSat.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $]
***********************************************************************/
#include "if.h"
#include "sat/bsat/satSolver.h"
ABC_NAMESPACE_IMPL_START
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Builds SAT instance for the given structure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
sat_solver * If_ManSatBuildXY( int nLutSize )
{
int nMintsL = (1 << nLutSize);
int nMintsF = (1 << (2 * nLutSize - 1));
int nVars = 2 * nMintsL + nMintsF;
int iVarP0 = 0; // LUT0 parameters (total nMintsL)
int iVarP1 = nMintsL; // LUT1 parameters (total nMintsL)
int m,iVarM = 2 * nMintsL; // MUX vars (total nMintsF)
sat_solver * p = sat_solver_new();
sat_solver_setnvars( p, nVars );
for ( m = 0; m < nMintsF; m++ )
sat_solver_add_mux( p, iVarP0 + m % nMintsL, iVarP1 + 2 * (m / nMintsL) + 1, iVarP1 + 2 * (m / nMintsL), iVarM + m );
return p;
}
/**Function*************************************************************
Synopsis [Returns config string for the given truth table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int If_ManSatCheckXY( sat_solver * p, 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;
int nMintsL = (1 << nLutSize);
int nMintsF = (1 << (2 * nLutSize - 1));
int v, Value, m, mNew, nMintsFNew, nMintsLNew;
// collect variable sets
Dau_DecSortSet( uSet, nVars, &nBSet, &nSSet, &nFSet );
assert( nBSet + nSSet + nFSet == nVars );
// check variable bounds
assert( nSSet + nBSet <= nLutSize );
assert( nLutSize + nSSet + nFSet <= 2*nLutSize - 1 );
nMintsFNew = (1 << (nLutSize + nSSet + nFSet));
// remap minterms
Vec_IntFill( vLits, nMintsF, -1 );
for ( m = 0; m < (1 << nVars); m++ )
{
mNew = iBSet = iSSet = iFSet = 0;
for ( v = 0; v < nVars; v++ )
{
Value = ((uSet >> (v << 1)) & 3);
if ( Value == 0 ) // FS
{
if ( ((m >> v) & 1) )
mNew |= 1 << (nLutSize + nSSet + iFSet);
iFSet++;
}
else if ( Value == 1 ) // BS
{
if ( ((m >> v) & 1) )
mNew |= 1 << (nSSet + iBSet);
iBSet++;
}
else if ( Value == 3 ) // SS
{
if ( ((m >> v) & 1) )
{
mNew |= 1 << iSSet;
mNew |= 1 << (nLutSize + iSSet);
}
iSSet++;
}
else assert( Value == 0 );
}
assert( iBSet == nBSet && iFSet == nFSet );
assert( Vec_IntEntry(vLits, mNew) == -1 );
Vec_IntWriteEntry( vLits, mNew, Abc_TtGetBit(pTruth, m) );
}
// find assumptions
v = 0;
Vec_IntForEachEntry( vLits, Value, m )
{
printf( "%d", (Value >= 0) ? Value : 2 );
if ( Value >= 0 )
Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(2 * nMintsL + m, !Value) );
}
Vec_IntShrink( vLits, v );
printf( " %d\n", Vec_IntSize(vLits) );
// run SAT solver
Value = sat_solver_solve( p, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 );
if ( Value != l_True )
return 0;
// collect config
assert( nSSet + nBSet <= nLutSize );
*pTBound = 0;
nMintsLNew = (1 << (nSSet + nBSet));
for ( m = 0; m < nMintsLNew; m++ )
if ( sat_solver_var_value(p, m) )
Abc_TtSetBit( pTBound, m );
*pTBound = Abc_Tt6Stretch( *pTBound, nSSet + nBSet );
// collect configs
assert( nSSet + nFSet + 1 <= nLutSize );
*pTFree = 0;
nMintsLNew = (1 << (nSSet + nFSet + 1));
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 );
return 1;
}
/**Function*************************************************************
Synopsis [Test procedure.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
void If_ManSatTest()
{
int nVars = 6;
int nLutSize = 4;
sat_solver * p = If_ManSatBuildXY( nLutSize );
// char * pDsd = "(abcdefg)";
// char * pDsd = "([a!bc]d!e)";
char * pDsd = "0123456789ABCDEF{abcdef}";
word * pTruth = Dau_DsdToTruth( pDsd, nVars );
word uBound, uFree;
Vec_Int_t * vLits = Vec_IntAlloc( 100 );
// unsigned uSet = (1 << 0) | (1 << 2) | (1 << 4) | (1 << 6);
// unsigned uSet = (3 << 0) | (1 << 2) | (1 << 8) | (1 << 4);
unsigned uSet = (1 << 0) | (3 << 2) | (1 << 4) | (1 << 6);
int RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
assert( RetValue );
// Abc_TtPrintBinary( pTruth, nVars );
// Abc_TtPrintBinary( &uBound, nLutSize );
// Abc_TtPrintBinary( &uFree, nLutSize );
Dau_DsdPrintFromTruth( pTruth, nVars );
Dau_DsdPrintFromTruth( &uBound, nLutSize );
Dau_DsdPrintFromTruth( &uFree, nLutSize );
sat_solver_delete(p);
Vec_IntFree( vLits );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
ABC_NAMESPACE_IMPL_END

1
src/opt/dau/dau.h
View File

@ -99,6 +99,7 @@ extern char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, i
/*=== dauNonDsd.c ==========================================================*/
extern Vec_Int_t * Dau_DecFindSets( word * pInit, int nVars );
extern void Dau_DecSortSet( unsigned set, int nVars, int * pnUnique, int * pnShared, int * pnFree );
extern void Dau_DecPrintSets( Vec_Int_t * vSets, int nVars );
extern void Dau_DecPrintSet( unsigned set, int nVars, int fNewLine );

46
src/sat/bsat/satSolver.h
View File

@ -368,6 +368,52 @@ static inline int sat_solver_add_xor( sat_solver * pSat, int iVarA, int iVarB, i
assert( Cid );
return 4;
}
static inline int sat_solver_add_mux( sat_solver * pSat, int iVarC, int iVarT, int iVarE, int iVarZ )
{
lit Lits[3];
int Cid;
assert( iVarC >= 0 && iVarT >= 0 && iVarE >= 0 && iVarZ >= 0 );
Lits[0] = toLitCond( iVarC, 1 );
Lits[1] = toLitCond( iVarT, 1 );
Lits[2] = toLitCond( iVarZ, 0 );
Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
assert( Cid );
Lits[0] = toLitCond( iVarC, 1 );
Lits[1] = toLitCond( iVarT, 0 );
Lits[2] = toLitCond( iVarZ, 1 );
Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
assert( Cid );
Lits[0] = toLitCond( iVarC, 0 );
Lits[1] = toLitCond( iVarE, 1 );
Lits[2] = toLitCond( iVarZ, 0 );
Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
assert( Cid );
Lits[0] = toLitCond( iVarC, 0 );
Lits[1] = toLitCond( iVarE, 0 );
Lits[2] = toLitCond( iVarZ, 1 );
Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
assert( Cid );
if ( iVarT == iVarE )
return 4;
Lits[0] = toLitCond( iVarT, 0 );
Lits[1] = toLitCond( iVarE, 0 );
Lits[2] = toLitCond( iVarZ, 1 );
Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
assert( Cid );
Lits[0] = toLitCond( iVarT, 1 );
Lits[1] = toLitCond( iVarE, 1 );
Lits[2] = toLitCond( iVarZ, 0 );
Cid = sat_solver_addclause( pSat, Lits, Lits + 3 );
assert( Cid );
return 6;
}
static inline int sat_solver_add_xor_and( sat_solver * pSat, int iVarF, int iVarA, int iVarB, int iVarC )
{
// F = (a (+) b) * c