From 839632140e675c628e08a00dc904b6d7cb877ba0 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 6 Mar 2014 21:21:02 -0800 Subject: Changes to LUT mappers. --- src/map/if/if.h | 3 ++ src/map/if/ifDsd.c | 127 ++++++++++++++++++++++++++++++++++++++++++++--- src/map/if/ifSat.c | 142 ++++++++++++++++++++++++++++++++++++++++++++++++++++- 3 files changed, 264 insertions(+), 8 deletions(-) (limited to 'src/map/if') diff --git a/src/map/if/if.h b/src/map/if/if.h index 8af5cff3..8693e74e 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -520,6 +520,7 @@ extern int If_CluCheckExt3( void * p, word * pTruth, int nVars, int extern If_DsdMan_t * If_DsdManAlloc( int nVars, 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_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fSpec, int fVerbose ); extern void If_DsdManFree( If_DsdMan_t * p, int fVerbose ); extern void If_DsdManSave( If_DsdMan_t * p, char * pFileName ); extern If_DsdMan_t * If_DsdManLoad( char * pFileName ); @@ -574,10 +575,12 @@ extern int If_ManPerformMappingRound( If_Man_t * p, int nCutsUsed, i extern void If_ManImproveMapping( If_Man_t * p ); /*=== ifSat.c ==========================================================*/ extern void * If_ManSatBuildXY( int nLutSize ); +extern void * If_ManSatBuild55(); extern void * If_ManSatBuildXYZ( int nLutSize ); extern void If_ManSatUnbuild( void * p ); extern int If_ManSatCheckXY( void * pSat, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, Vec_Int_t * vLits ); extern unsigned If_ManSatCheckXYall( void * pSat, int nLutSize, word * pTruth, int nVars, Vec_Int_t * vLits ); +extern unsigned If_ManSatCheck55all( void * pSat, word * pTruth, int nVars, 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 5222c376..e1a4f2b5 100644 --- a/src/map/if/ifDsd.c +++ b/src/map/if/ifDsd.c @@ -20,6 +20,7 @@ #include "if.h" #include "misc/extra/extra.h" +#include "sat/bsat/satSolver.h" ABC_NAMESPACE_IMPL_START @@ -102,6 +103,7 @@ static inline void If_DsdVecObjIncRef( Vec_Ptr_t * p, int iObj ) static inline If_DsdObj_t * If_DsdObjFanin( Vec_Ptr_t * p, If_DsdObj_t * pObj, int i ) { assert(i < (int)pObj->nFans); return If_DsdVecObj(p, Abc_Lit2Var(pObj->pFans[i])); } static inline int If_DsdVecObjMark( Vec_Ptr_t * p, int iObj ) { return If_DsdVecObj( p, iObj )->fMark; } static inline void If_DsdVecObjSetMark( Vec_Ptr_t * p, int iObj ) { If_DsdVecObj( p, iObj )->fMark = 1; } +static inline void If_DsdVecObjClearMark( Vec_Ptr_t * p, int iObj ) { If_DsdVecObj( p, iObj )->fMark = 0; } #define If_DsdVecForEachObj( vVec, pObj, i ) \ Vec_PtrForEachEntry( If_DsdObj_t *, vVec, pObj, i ) @@ -365,10 +367,39 @@ void If_DsdManPrintOne( FILE * pFile, If_DsdMan_t * p, int iObjId, unsigned char fprintf( pFile, "\n" ); assert( nSupp == If_DsdVecObjSuppSize(p->vObjs, iObjId) ); } +void If_DsdManPrintDistrib( If_DsdMan_t * p ) +{ + If_DsdObj_t * pObj; + int CountAll[IF_MAX_FUNC_LUTSIZE] = {0}; + int CountNon[IF_MAX_FUNC_LUTSIZE] = {0}; + int i, nVars, CountNonTotal = 0; + If_DsdVecForEachObj( p->vObjs, pObj, i ) + { + nVars = If_DsdObjSuppSize(pObj); + CountAll[nVars]++; + if ( !If_DsdVecObjMark(p->vObjs, i) ) + continue; + CountNon[nVars]++; + CountNonTotal++; + } + for ( i = 0; i <= p->nVars; i++ ) + { + printf( "%3d : ", i ); + printf( "All = %8d ", CountAll[i] ); + printf( "Non = %8d ", CountNon[i] ); + printf( "(%6.2f %%)", 100.0 * CountNon[i] / CountAll[i] ); + printf( "\n" ); + } + printf( "All : " ); + printf( "All = %8d ", Vec_PtrSize(p->vObjs) ); + printf( "Non = %8d ", CountNonTotal ); + printf( "(%6.2f %%)", 100.0 * CountNonTotal / Vec_PtrSize(p->vObjs) ); + printf( "\n" ); +} void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose ) { If_DsdObj_t * pObj; - int i, DsdMax = 0, CountUsed = 0, CountNonDsdStr = 0; + int i, DsdMax = 0, CountUsed = 0, CountNonDsdStr = 0, CountMarked = 0; FILE * pFile; pFile = pFileName ? fopen( pFileName, "wb" ) : stdout; if ( pFileName && pFile == NULL ) @@ -382,9 +413,11 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose ) DsdMax = Abc_MaxInt( DsdMax, pObj->nFans ); CountNonDsdStr += If_DsdManCheckNonDec_rec( p, pObj->Id ); CountUsed += ( If_DsdVecObjRef(p->vObjs, pObj->Id) > 0 ); + CountMarked += If_DsdVecObjMark( p->vObjs, i ); } fprintf( pFile, "Total number of objects = %8d\n", Vec_PtrSize(p->vObjs) ); fprintf( pFile, "Externally used objects = %8d\n", CountUsed ); + fprintf( pFile, "Marked objects = %8d\n", CountMarked ); fprintf( pFile, "Non-DSD objects (max =%2d) = %8d\n", DsdMax, Vec_MemEntryNum(p->vTtMem) ); fprintf( pFile, "Non-DSD structures = %8d\n", CountNonDsdStr ); fprintf( pFile, "Unique table hits = %8d\n", p->nUniqueHits ); @@ -392,11 +425,15 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int fVerbose ) fprintf( pFile, "Memory used for objects = %8.2f MB.\n", 1.0*Mem_FlexReadMemUsage(p->pMem)/(1<<20) ); fprintf( pFile, "Memory used for hash table = %8.2f MB.\n", 1.0*sizeof(int)*p->nBins/(1<<20) ); fprintf( pFile, "Memory used for array = %8.2f MB.\n", 1.0*sizeof(void *)*Vec_PtrCap(p->vObjs)/(1<<20) ); - 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 check2", p->timeCheck2 ); - Abc_PrintTime( 1, "Time verify", p->timeVerify ); + If_DsdManPrintDistrib( p ); + if ( p->timeDsd ) + { + 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 check2", p->timeCheck2 ); + Abc_PrintTime( 1, "Time verify", p->timeVerify ); + } // If_DsdManHashProfile( p ); // If_DsdManDump( p ); // If_DsdManDumpAll( p ); @@ -1442,6 +1479,84 @@ void If_DsdManTest() Vec_IntFree( vSets ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fSpec, int fVerbose ) +{ + ProgressBar * pProgress = NULL; + If_DsdObj_t * pObj; + sat_solver * pSat = NULL; + sat_solver * pSat5 = NULL; + Vec_Int_t * vLits = Vec_IntAlloc( 1000 ); + int i, Value, nVars; + word * pTruth; + pSat = (sat_solver *)If_ManSatBuildXY( LutSize ); + if ( LutSize == 5 && fSpec ) + pSat5 = (sat_solver *)If_ManSatBuild55(); + If_DsdVecForEachObj( p->vObjs, pObj, i ) + pObj->fMark = 0; + pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(p->vObjs) ); + If_DsdVecForEachObj( p->vObjs, pObj, i ) + { + Extra_ProgressBarUpdate( pProgress, i, NULL ); + nVars = If_DsdObjSuppSize(pObj); + if ( nVars <= LutSize ) + continue; + if ( LutSize == 5 && fSpec ) + { + if ( nVars == 9 ) + { + pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL ); + Value = If_ManSatCheck55all( pSat5, pTruth, nVars, vLits ); + } + else + { + if ( If_DsdManCheckXY(p, Abc_Var2Lit(i, 0), LutSize, 0, 0) ) + continue; + if ( fFast ) + Value = 0; + else + { + pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL ); + Value = If_ManSatCheckXYall( pSat, LutSize, pTruth, nVars, vLits ); + } + } + } + else + { + if ( If_DsdManCheckXY(p, Abc_Var2Lit(i, 0), LutSize, 0, 0) ) + continue; + if ( fFast ) + Value = 0; + else + { + pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL ); + Value = If_ManSatCheckXYall( pSat, LutSize, pTruth, nVars, vLits ); + } + } + if ( Value ) + continue; + If_DsdVecObjSetMark( p->vObjs, i ); + } + if ( pProgress ) + Extra_ProgressBarStop( pProgress ); + If_ManSatUnbuild( pSat5 ); + If_ManSatUnbuild( pSat ); + Vec_IntFree( vLits ); + if ( fVerbose ) + If_DsdManPrintDistrib( p ); +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/map/if/ifSat.c b/src/map/if/ifSat.c index a0fc5737..9f4ea631 100644 --- a/src/map/if/ifSat.c +++ b/src/map/if/ifSat.c @@ -268,6 +268,128 @@ int If_ManSatCheckXY( void * pSat, int nLutSize, word * pTruth, int nVars, unsig } return 1; } +int If_ManSatCheck55( void * pSat, word * pTruth, int nVars, int * pPerm9, word * pTBound, word * pTFree, Vec_Int_t * vLits ) +{ + sat_solver * p = (sat_solver *)pSat; + int v, Value, m, mNew; + int nMintsL = 16; + // remap minterms + Vec_IntFill( vLits, 512, -1 ); + for ( m = 0; m < (1 << nVars); m++ ) + { + mNew = 0; + for ( v = 0; v < 9; v++ ) + { + assert( pPerm9[v] < nVars ); + if ( ((m >> pPerm9[v]) & 1) ) + mNew |= (1 << v); + } + assert( Vec_IntEntry(vLits, mNew) == -1 ); + Vec_IntWriteEntry( vLits, mNew, Abc_TtGetBit(pTruth, m) ); + } + // find assumptions + v = 0; + Vec_IntForEachEntry( vLits, Value, m ) + if ( Value >= 0 ) + Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(2 * nMintsL + m, !Value) ); + Vec_IntShrink( vLits, v ); + // 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; + if ( pTBound && pTFree ) + { + // collect config + *pTBound = 0; + for ( m = 0; m < nMintsL; m++ ) + if ( sat_solver_var_value(p, m) ) + Abc_TtSetBit( pTBound, m ); + *pTBound = Abc_Tt6Stretch( *pTBound, 4 ); + // collect configs + *pTFree = 0; + for ( m = 0; m < nMintsL; m++ ) + if ( sat_solver_var_value(p, nMintsL+m) ) + Abc_TtSetBit( pTFree, m ); + *pTFree = Abc_Tt6Stretch( *pTFree, 4 ); + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Returns config string for the given truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned If_ManSatCheck55all_int( void * pSat, word * pTruth, int nVars, Vec_Int_t * vLits ) +{ + int Combs[10][5] = { + {0,1,2,3,4}, + {0,2,1,3,4}, + {0,3,1,2,4}, + {0,4,1,2,3}, + {1,2,0,3,4}, + {1,3,0,2,4}, + {1,4,0,2,3}, + {2,3,0,1,4}, + {2,4,0,1,3}, + {3,4,0,1,2} + }; + int pPerm9[9], Mark[9], i[6], k, n, c; + assert( nVars == 9 || nVars == 8 || nVars == 7 ); + for ( i[0] = 0; i[0] < nVars; i[0]++ ) + for ( i[1] = i[0]+1; i[1] < nVars; i[1]++ ) + for ( i[2] = i[1]+1; i[2] < nVars; i[2]++ ) + for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ ) + for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ ) + { + // add remaining ones + n = 5; + for ( k = 0; k < nVars; k++ ) + Mark[k] = 0; + for ( k = 0; k < 5; k++ ) + Mark[i[k]] = 1; + for ( k = 0; k < nVars; k++ ) + if ( Mark[k] == 0 ) + pPerm9[n++] = k; + assert( n == nVars ); + for ( ; n < 9; n++ ) + pPerm9[n] = pPerm9[n-1]; + assert( n == 9 ); + // current ones + for ( c = 0; c < 10; c++ ) + { + for ( n = 0; n < 5; n++ ) + pPerm9[n] = i[Combs[c][n]]; + // try different combinations + for ( k = 5; k < nVars; k++ ) + { + ABC_SWAP( int, pPerm9[5], pPerm9[k] ); + if ( If_ManSatCheck55(pSat, pTruth, nVars, pPerm9, NULL, NULL, vLits) ) + { +// for ( k = 0; k < 9; k++ ) +// printf( "%c", 'a' + pPerm9[k] ); +// printf( "\n" ); + return 1; + } + ABC_SWAP( int, pPerm9[5], pPerm9[k] ); + } + } + } + return 0; +} +unsigned If_ManSatCheck55all( void * pSat, word * pTruth, int nVars, Vec_Int_t * vLits ) +{ +// abctime clk = Abc_Clock(); + unsigned Value = If_ManSatCheck55all_int( pSat, pTruth, nVars, vLits ); +// Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + return Value; +} /**Function************************************************************* @@ -408,6 +530,7 @@ unsigned If_ManSatCheckXYall_int( void * pSat, int nLutSize, word * pTruth, int for ( i[3] = i[2]+1; i[3] < nVars; i[3]++ ) for ( i[4] = i[3]+1; i[4] < nVars; i[4]++ ) { + uSet = (1 << (2*i[0])) | (1 << (2*i[1])) | (1 << (2*i[2])) | (1 << (2*i[3])) | (1 << (2*i[4])); for ( s[0] = 0; s[0] < nLutSize; s[0]++ ) for ( s[1] = s[0]+1; s[1] < nLutSize; s[1]++ ) for ( s[2] = s[1]+1; s[2] < nLutSize; s[2]++ ) @@ -538,8 +661,7 @@ void If_ManSatTest2() sat_solver_delete(p); Vec_IntFree( vLits ); } - -void If_ManSatTest() +void If_ManSatTest3() { int nVars = 6; int nLutSize = 4; @@ -558,6 +680,22 @@ void If_ManSatTest() sat_solver_delete(p); Vec_IntFree( vLits ); } +void If_ManSatTest() +{ + int nVars = 9; + sat_solver * p = (sat_solver *)If_ManSatBuild55(); +// char * pDsd = "[([(ab)cde]f)ghi]"; +// char * pDsd = "[([(hi)cde]f)gab]"; + char * pDsd = "[(0123{(hi)cde}f)gab]"; + word * pTruth = Dau_DsdToTruth( pDsd, nVars ); + Vec_Int_t * vLits = Vec_IntAlloc( 1000 ); + if ( If_ManSatCheck55all( p, pTruth, nVars, vLits ) ) + printf( "Found!\n" ); + else + printf( "Not found!\n" ); + sat_solver_delete(p); + Vec_IntFree( vLits ); +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// -- cgit v1.2.3