From de48fd79992a5218c18da8dca62869b865a62f0e Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 28 Feb 2014 10:35:36 -0800 Subject: Changes to LUT mappers. --- src/map/if/if.h | 3 +- src/map/if/ifDsd.c | 119 ++++++++++++++++++++++++++++++++++++------------- src/map/if/ifMan.c | 4 +- src/map/if/ifMap.c | 33 ++++++++++++++ src/map/if/ifSat.c | 67 ++++++++++++++++++++++++++-- src/map/if/module.make | 1 + 6 files changed, 190 insertions(+), 37 deletions(-) (limited to 'src/map/if') diff --git a/src/map/if/if.h b/src/map/if/if.h index 13828701..47bd7390 100644 --- a/src/map/if/if.h +++ b/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 =============================================================*/ diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c index e6c2dfac..23160e62 100644 --- a/src/map/if/ifDsd.c +++ b/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" ); } diff --git a/src/map/if/ifMan.c b/src/map/if/ifMan.c index 5025429e..d03fc200 100644 --- a/src/map/if/ifMan.c +++ b/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 ); diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c index c719215f..d7b7f4cc 100644 --- a/src/map/if/ifMap.c +++ b/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; + } +*/ } } } diff --git a/src/map/if/ifSat.c b/src/map/if/ifSat.c index 0afe7ea5..5ddb8241 100644 --- a/src/map/if/ifSat.c +++ b/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 /// //////////////////////////////////////////////////////////////////////// diff --git a/src/map/if/module.make b/src/map/if/module.make index c8c18e88..f0c1860f 100644 --- a/src/map/if/module.make +++ b/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 \ -- cgit v1.2.3