Skip to content

A
abc
Commit de48fd79 by Alan Mishchenko
Options

Changes to LUT mappers.

parent b556c259
Showing with 201 additions and 41 deletions
src/map/if/if.h
......@@ -236,6 +236,7 @@ struct If_Man_t_
Vec_Int_t * vTtDsds; // mapping of truth table into DSD
Vec_Str_t * vTtPerms; // mapping of truth table into permutations
int nBestCutSmall[2];
int nCountNonDec[2];
// timing manager
Tim_Man_t * pManTim;
......@@ -519,7 +520,7 @@ extern int If_CluCheckExt3( void * p, word * pTruth, int nVars, int
extern If_DsdMan_t * If_DsdManAlloc( int nLutSize );
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 void If_DsdManFree( If_DsdMan_t * p, int fVerbose );
extern int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char * pPerm, char * pLutStruct );
extern int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd );
/*=== ifLib.c =============================================================*/
......
src/map/if/ifDsd.c
......@@ -19,6 +19,7 @@
***********************************************************************/
#include "if.h"
#include "misc/extra/extra.h"
ABC_NAMESPACE_IMPL_START
......@@ -63,12 +64,13 @@ struct If_DsdMan_t_
word ** pTtElems; // elementary TTs
Vec_Mem_t * vTtMem; // truth table memory and hash table
Vec_Ptr_t * vTtDecs; // truth table decompositions
int * pSched[16]; // grey code schedules
int nUniqueHits; // statistics
int nUniqueMisses; // statistics
abctime timeBeg; // statistics
abctime timeDec; // statistics
abctime timeLook; // statistics
abctime timeEnd; // statistics
abctime timeDsd; // statistics
abctime timeCanon; // statistics
abctime timeCheck; // statistics
abctime timeVerify; // statistics
};
static inline int If_DsdObjWordNum( int nFans ) { return sizeof(If_DsdObj_t) / 8 + nFans / 2 + ((nFans & 1) > 0); }
......@@ -212,6 +214,8 @@ int If_DsdObjCreate( If_DsdMan_t * p, int Type, int * pLits, int nLits, int trut
iPrev = pLits[i];
}
}
if ( Vec_PtrSize(p->vObjs) % p->nBins == 0 )
printf( "Warning: The number of objects in If_DsdObjCreate() is more than the number of bins.\n" );
// create new node
pObj = If_DsdObjAlloc( p, Type, nLits );
if ( Type == DAU_DSD_PRIME )
......@@ -256,7 +260,7 @@ static inline word ** If_ManDsdTtElems()
}
If_DsdMan_t * If_DsdManAlloc( int nVars )
{
If_DsdMan_t * p;
If_DsdMan_t * p; int v;
p = ABC_CALLOC( If_DsdMan_t, 1 );
p->nVars = nVars;
p->nWords = Abc_TtWordNum( nVars );
......@@ -272,21 +276,25 @@ If_DsdMan_t * If_DsdManAlloc( int nVars )
p->vTtDecs = Vec_PtrAlloc( 1000 );
p->vTtMem = Vec_MemAlloc( Abc_TtWordNum(nVars), 12 );
Vec_MemHashAlloc( p->vTtMem, 10000 );
for ( v = 2; v < nVars; v++ )
p->pSched[v] = Extra_GreyCodeSchedule( v );
return p;
}
void If_DsdManFree( If_DsdMan_t * p )
void If_DsdManFree( If_DsdMan_t * p, int fVerbose )
{
int fVerbose = 0;
int v;
// If_DsdManDump( p );
If_DsdManPrint( p, NULL, 0 );
Vec_MemDumpTruthTables( p->vTtMem, "dumpdsd", p->nVars );
if ( fVerbose )
{
Abc_PrintTime( 1, "Time begin ", p->timeBeg );
Abc_PrintTime( 1, "Time decomp", p->timeDec );
Abc_PrintTime( 1, "Time lookup", p->timeLook );
Abc_PrintTime( 1, "Time end ", p->timeEnd );
Abc_PrintTime( 1, "Time DSD ", p->timeDsd );
Abc_PrintTime( 1, "Time canon ", p->timeCanon-p->timeCheck );
Abc_PrintTime( 1, "Time check ", p->timeCheck );
Abc_PrintTime( 1, "Time verify", p->timeVerify );
}
for ( v = 2; v < p->nVars; v++ )
ABC_FREE( p->pSched[v] );
Vec_VecFree( (Vec_Vec_t *)p->vTtDecs );
Vec_MemHashFree( p->vTtMem );
Vec_MemFreeP( &p->vTtMem );
......@@ -297,6 +305,23 @@ void If_DsdManFree( If_DsdMan_t * p )
ABC_FREE( p->pBins );
ABC_FREE( p );
}
void If_DsdManHashProfile( If_DsdMan_t * p )
{
If_DsdObj_t * pObj;
unsigned * pSpot;
int i, Counter;
for ( i = 0; i < p->nBins; i++ )
{
Counter = 0;
for ( pSpot = p->pBins + i; *pSpot; pSpot = (unsigned *)Vec_IntEntryP(p->vNexts, pObj->Id), Counter++ )
pObj = If_DsdVecObj( p->vObjs, *pSpot );
// if ( Counter > 5 )
// printf( "%d ", Counter );
// if ( i > 10000 )
// break;
}
// printf( "\n" );
}
int If_DsdManCheckNonDec_rec( If_DsdMan_t * p, int Id )
{
If_DsdObj_t * pObj;
......@@ -454,30 +479,18 @@ void If_DsdManCollect( If_DsdMan_t * p, int Id, Vec_Int_t * vNodes )
SeeAlso []
***********************************************************************/
void If_DsdManHashProfile( If_DsdMan_t * p )
{
If_DsdObj_t * pObj;
unsigned * pSpot;
int i, Counter;
for ( i = 0; i < p->nBins; i++ )
{
Counter = 0;
for ( pSpot = p->pBins + i; *pSpot; pSpot = (unsigned *)Vec_IntEntryP(p->vNexts, pObj->Id), Counter++ )
pObj = If_DsdVecObj( p->vObjs, *pSpot );
if ( Counter )
printf( "%d ", Counter );
}
printf( "\n" );
}
static inline unsigned If_DsdObjHashKey( If_DsdMan_t * p, int Type, int * pLits, int nLits, int truthId )
{
static int s_Primes[8] = { 1699, 4177, 5147, 5647, 6343, 7103, 7873, 8147 };
// static int s_Primes[8] = { 1699, 4177, 5147, 5647, 6343, 7103, 7873, 8147 };
static int s_Primes[24] = { 1049, 1297, 1559, 1823, 2089, 2371, 2663, 2909,
3221, 3517, 3779, 4073, 4363, 4663, 4973, 5281,
5573, 5861, 6199, 6481, 6803, 7109, 7477, 7727 };
int i;
unsigned uHash = Type * 7873 + nLits * 8147;
for ( i = 0; i < nLits; i++ )
uHash += pLits[i] * s_Primes[i & 0x7];
uHash += pLits[i] * s_Primes[i & 0xF];
if ( Type == IF_DSD_PRIME )
uHash += truthId * s_Primes[i & 0x7];
uHash += truthId * s_Primes[i & 0xF];
return uHash % p->nBins;
}
unsigned * If_DsdObjHashLookup( If_DsdMan_t * p, int Type, int * pLits, int nLits, int truthId )
......@@ -503,15 +516,19 @@ int If_DsdObjFindOrAdd( If_DsdMan_t * p, int Type, int * pLits, int nLits, word
{
int truthId = (Type == IF_DSD_PRIME) ? Vec_MemHashInsert(p->vTtMem, pTruth) : -1;
unsigned * pSpot = If_DsdObjHashLookup( p, Type, pLits, nLits, truthId );
abctime clk;
if ( *pSpot )
return *pSpot;
clk = Abc_Clock();
if ( truthId >= 0 && truthId == Vec_PtrSize(p->vTtDecs) )
{
Vec_Int_t * vSets = Dau_DecFindSets( pTruth, nLits );
Vec_Int_t * vSets = Dau_DecFindSets_int( pTruth, nLits, p->pSched );
// printf( "%d ", Vec_IntSize(vSets) );
assert( truthId == Vec_MemEntryNum(p->vTtMem)-1 );
Vec_PtrPush( p->vTtDecs, vSets );
// Dau_DecPrintSets( vSets, nLits );
}
p->timeCheck += Abc_Clock() - clk;
*pSpot = Vec_PtrSize( p->vObjs );
return If_DsdObjCreate( p, Type, pLits, nLits, truthId );
}
......@@ -686,6 +703,7 @@ int If_DsdManOperation( If_DsdMan_t * p, int Type, int * pLits, int nLits, unsig
unsigned char pPermNew[DAU_MAX_VAR];
int nChildren = 0, pChildren[DAU_MAX_VAR], pBegEnd[DAU_MAX_VAR];
int i, k, j, Id, iFanin, fComplFan, fCompl = 0, nSSize = 0;
// abctime clk;
if ( Type == IF_DSD_AND )
{
for ( k = 0; k < nLits; k++ )
......@@ -855,7 +873,7 @@ int If_DsdManAddDsd_rec( char * pStr, char ** p, int * pMatches, If_DsdMan_t * p
fCompl = 1;
(*p)++;
}
assert( !((**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9')) );
// assert( !((**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9')) );
if ( **p >= 'a' && **p <= 'z' ) // var
{
pPerm[(*pnSupp)++] = Abc_Var2Lit( **p - 'a', fCompl );
......@@ -881,6 +899,22 @@ int If_DsdManAddDsd_rec( char * pStr, char ** p, int * pMatches, If_DsdMan_t * p
iRes = If_DsdManOperation( pMan, Type, pLits, nLits, pPermStart, pTruth );
return Abc_LitNotCond( iRes, fCompl );
}
if ( (**p >= 'A' && **p <= 'F') || (**p >= '0' && **p <= '9') )
{
word pFunc[DAU_MAX_WORD];
int nLits = 0, pLits[DAU_MAX_VAR];
char * q;
int i, nVarsF = Abc_TtReadHex( pFunc, *p );
*p += Abc_TtHexDigitNum( nVarsF );
q = pStr + pMatches[ *p - pStr ];
assert( **p == '{' && *q == '}' );
for ( i = 0, (*p)++; *p < q; (*p)++, i++ )
pLits[nLits++] = If_DsdManAddDsd_rec( pStr, p, pMatches, pMan, pTruth, pPerm, pnSupp );
assert( i == nVarsF );
assert( *p == q );
iRes = If_DsdManOperation( pMan, DAU_DSD_PRIME, pLits, nLits, pPermStart, pFunc );
return Abc_LitNotCond( iRes, fCompl );
}
assert( 0 );
return -1;
}
......@@ -1143,9 +1177,23 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char
word pCopy[DAU_MAX_WORD], * pRes;
char pDsd[DAU_MAX_STR];
int iDsd, nSizeNonDec, nSupp = 0;
abctime clk;
assert( nLeaves <= DAU_MAX_VAR );
Abc_TtCopy( pCopy, pTruth, p->nWords, 0 );
nSizeNonDec = Dau_DsdDecompose( pCopy, nLeaves, 0, 0, pDsd );
clk = Abc_Clock();
nSizeNonDec = Dau_DsdDecompose( pCopy, nLeaves, 0, 1, pDsd );
p->timeDsd += Abc_Clock() - clk;
/*
if ( nLeaves <= 6 )
{
word pCopy2[DAU_MAX_WORD], t;
char pDsd2[DAU_MAX_STR];
Abc_TtCopy( pCopy2, pTruth, p->nWords, 0 );
nSizeNonDec = Dau_DsdDecompose( pCopy2, nLeaves, 0, 1, pDsd2 );
t = Dau_Dsd6ToTruth( pDsd2 );
assert( t == *pTruth );
}
*/
// if ( !strcmp(pDsd, "(![(!e!d)c]!(b!a))") )
// {
// int x = 0;
......@@ -1153,17 +1201,24 @@ int If_DsdManCompute( If_DsdMan_t * p, word * pTruth, int nLeaves, unsigned char
if ( nSizeNonDec > 0 )
Abc_TtStretch6( pCopy, nSizeNonDec, p->nVars );
memset( pPerm, 0xFF, nLeaves );
clk = Abc_Clock();
iDsd = If_DsdManAddDsd( p, pDsd, pCopy, pPerm, &nSupp );
p->timeCanon += Abc_Clock() - clk;
assert( nSupp == nLeaves );
// verify the result
clk = Abc_Clock();
pRes = If_DsdManComputeTruth( p, iDsd, pPerm );
p->timeVerify += Abc_Clock() - clk;
if ( !Abc_TtEqual(pRes, pTruth, p->nWords) )
{
// If_DsdManPrint( p, NULL );
printf( "\n" );
printf( "Verification failed!\n" );
printf( "%s\n", pDsd );
Dau_DsdPrintFromTruth( pTruth, nLeaves );
Dau_DsdPrintFromTruth( pRes, nLeaves );
// Kit_DsdPrintFromTruth( (unsigned *)pTruth, nLeaves ); printf( "\n" );
// Kit_DsdPrintFromTruth( (unsigned *)pRes, nLeaves ); printf( "\n" );
If_DsdManPrintOne( stdout, p, Abc_Lit2Var(iDsd), pPerm, 1 );
printf( "\n" );
}
......
src/map/if/ifMan.c
......@@ -161,7 +161,9 @@ void If_ManStop( If_Man_t * p )
if ( p->pPars->fVerbose && p->nCuts5 )
Abc_Print( 1, "Statistics about 5-cuts: Total = %d Non-decomposable = %d (%.2f %%)\n", p->nCuts5, p->nCuts5-p->nCuts5a, 100.0*(p->nCuts5-p->nCuts5a)/p->nCuts5 );
if ( p->pPars->fUseDsd )
If_DsdManFree( p->pIfDsdMan );
If_DsdManFree( p->pIfDsdMan, p->pPars->fVerbose );
if ( p->pPars->fUseDsd )
printf( "NonDec0 = %d. NonDec1 = %d.\n", p->nCountNonDec[0], p->nCountNonDec[1] );
// Abc_PrintTime( 1, "Truth", p->timeTruth );
// Abc_Print( 1, "Small support = %d.\n", p->nSmallSupp );
Vec_IntFreeP( &p->vCoAttrs );
......
src/map/if/ifMap.c
......@@ -279,6 +279,39 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
int Value = If_DsdManCheckDec( p->pIfDsdMan, pCut->iCutDsd );
if ( Value != (int)pCut->fUseless )
{
if ( pCut->fUseless && !Value )
p->nCountNonDec[0]++;
if ( !pCut->fUseless && Value )
p->nCountNonDec[1]++;
/*
// if ( pCut->fUseless && !Value )
// printf( "Old does not work. New works.\n" );
if ( !pCut->fUseless && Value )
printf( "Old works. New does not work. DSD = %d.\n", Abc_Lit2Var(pCut->iCutDsd) );
if ( !pCut->fUseless && Value )
{
extern word If_Dec6Perform( word t, int fDerive );
extern word * If_DsdManComputeTruth( If_DsdMan_t * p, int iDsd, unsigned char * pPermLits );
int s;
// word z, t = *If_CutTruthW(p, pCut);
word z, t = *If_DsdManComputeTruth( p->pIfDsdMan, pCut->iCutDsd, NULL );
Extra_PrintHex( stdout, (unsigned *)If_CutTruthW(p, pCut), pCut->nLeaves ); printf( "\n" );
Dau_DsdPrintFromTruth( &t, pCut->nLeaves );
// Dau_DsdPrintFromTruth( If_CutTruthW(p, pCut), pCut->nLeaves );
// If_DsdManPrintOne( stdout, p->pIfDsdMan, Abc_Lit2Var(pCut->iCutDsd), pCut->pPerm, 1 );
// printf( "Old works. New does not work. DSD = %d.\n", Abc_Lit2Var(pCut->iCutDsd) );
z = If_Dec6Perform( t, 1 );
If_DecPrintConfig( z );
s = If_DsdManCheckXY( p->pIfDsdMan, pCut->iCutDsd, 4, 1 );
printf( "Confirm %d\n", s );
s = 0;
}
*/
}
}
}
......
src/map/if/ifSat.c
......@@ -122,12 +122,12 @@ int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, un
v = 0;
Vec_IntForEachEntry( vLits, Value, m )
{
printf( "%d", (Value >= 0) ? Value : 2 );
// 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) );
// 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 )
......@@ -162,7 +162,7 @@ int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, un
SeeAlso []
***********************************************************************/
void If_ManSatTest()
void If_ManSatTest2()
{
int nVars = 6;
int nLutSize = 4;
......@@ -190,6 +190,67 @@ void If_ManSatTest()
Vec_IntFree( vLits );
}
void If_ManSatTest()
{
int nVars = 4;
int nLutSize = 3;
sat_solver * p = If_ManSatBuildXY( nLutSize );
word t = 0x183C, * pTruth = &t;
word uBound, uFree;
unsigned uSet;
int RetValue;
Vec_Int_t * vLits = Vec_IntAlloc( 100 );
uSet = (3 << 0) | (1 << 2) | (1 << 4);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue );
uSet = (1 << 0) | (3 << 2) | (1 << 4);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue );
uSet = (1 << 0) | (1 << 2) | (3 << 4);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue );
uSet = (3 << 0) | (1 << 2) | (1 << 6);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue );
uSet = (1 << 0) | (3 << 2) | (1 << 6);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue );
uSet = (1 << 0) | (1 << 2) | (3 << 6);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue );
uSet = (3 << 0) | (1 << 4) | (1 << 6);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue );
uSet = (1 << 0) | (3 << 4) | (1 << 6);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue );
uSet = (1 << 0) | (1 << 4) | (3 << 6);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue );
uSet = (3 << 2) | (1 << 4) | (1 << 6);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue );
uSet = (1 << 2) | (3 << 4) | (1 << 6);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue );
uSet = (1 << 2) | (1 << 4) | (3 << 6);
RetValue = If_ManSatCheckXY( p, nLutSize, pTruth, nVars, uSet, &uBound, &uFree, vLits );
printf( "%d", RetValue );
printf( "\n" );
sat_solver_delete(p);
Vec_IntFree( vLits );
}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
......
src/map/if/module.make
......@@ -12,6 +12,7 @@ SRC += src/map/if/ifCom.c \
src/map/if/ifMan.c \
src/map/if/ifMap.c \
src/map/if/ifReduce.c \
src/map/if/ifSat.c \
src/map/if/ifSelect.c \
src/map/if/ifSeq.c \
src/map/if/ifTime.c \
......
src/opt/dau/dau.h
......@@ -98,6 +98,7 @@ extern void Dau_DsdRemoveBraces( char * pDsd, int * pMatches );
extern char * Dau_DsdMerge( char * pDsd0i, int * pPerm0, char * pDsd1i, int * pPerm1, int fCompl0, int fCompl1, int nVars );
/*=== dauNonDsd.c ==========================================================*/
extern Vec_Int_t * Dau_DecFindSets_int( word * pInit, int nVars, int * pSched[16] );
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 );
......
src/opt/dau/dauNonDsd.c
......@@ -459,20 +459,17 @@ void Dau_DecMoveFreeToLSB( word * p, int nVars, int * V2P, int * P2V, int maskB,
Abc_TtMoveVar( p, nVars, V2P, P2V, v, c++ );
assert( c == nVars - sizeB );
}
Vec_Int_t * Dau_DecFindSets( word * pInit, int nVars )
Vec_Int_t * Dau_DecFindSets_int( word * pInit, int nVars, int * pSched[16] )
{
Vec_Int_t * vSets = Vec_IntAlloc( 32 );
int V2P[16], P2V[16], pVarsB[16];
int Limit = (1 << nVars);
int c, v, sizeB, sizeS, maskB, maskS;
int * pSched[16] = {NULL};
unsigned setMixed;
word p[1<<10];
memcpy( p, pInit, sizeof(word) * Abc_TtWordNum(nVars) );
for ( v = 0; v < nVars; v++ )
assert( Abc_TtHasVar( p, nVars, v ) );
for ( v = 2; v < nVars; v++ )
pSched[v] = Extra_GreyCodeSchedule( v );
// initialize permutation
for ( v = 0; v < nVars; v++ )
V2P[v] = P2V[v] = v;
......@@ -514,6 +511,15 @@ Vec_Int_t * Dau_DecFindSets( word * pInit, int nVars )
Vec_IntPush( vSets, setMixed );
}
}
return vSets;
}
Vec_Int_t * Dau_DecFindSets( word * pInit, int nVars )
{
Vec_Int_t * vSets;
int v, * pSched[16] = {NULL};
for ( v = 2; v < nVars; v++ )
pSched[v] = Extra_GreyCodeSchedule( v );
vSets = Dau_DecFindSets_int( pInit, nVars, pSched );
for ( v = 2; v < nVars; v++ )
ABC_FREE( pSched[v] );
return vSets;
......
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