From 4b0c12eb1e03ac863d09efc643d3253c4bfe3af4 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 8 Mar 2014 17:09:20 -0800 Subject: Changes to LUT mappers. --- src/map/if/if.h | 4 +- src/map/if/ifDsd.c | 91 +++++------------------------- src/map/if/ifSat.c | 159 ----------------------------------------------------- 3 files changed, 14 insertions(+), 240 deletions(-) (limited to 'src/map/if') diff --git a/src/map/if/if.h b/src/map/if/if.h index 60bdfa3c..30a8d0d8 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -520,7 +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 Number, int fVerbose ); -extern void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fSpec, int fVerbose ); +extern void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fAdd, 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 ); @@ -575,12 +575,10 @@ 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 6269b5b6..7afec99e 100644 --- a/src/map/if/ifDsd.c +++ b/src/map/if/ifDsd.c @@ -875,48 +875,6 @@ int If_DsdManCheckInv_rec( If_DsdMan_t * p, int iLit ) assert( 0 ); return 0; } -/* -int If_DsdManPushInv_rec( If_DsdMan_t * p, int iLit, unsigned char * pPerm ) -{ - If_DsdObj_t * pObj; - int i, iFanin, RetValue; - pObj = If_DsdVecObj( p->vObjs, Abc_Lit2Var(iLit) ); - if ( If_DsdObjType(pObj) == IF_DSD_VAR ) - { - pPerm[0] = (unsigned char)Abc_LitNot((int)pPerm[0]); - return 1; - } - if ( If_DsdObjType(pObj) == IF_DSD_AND || If_DsdObjType(pObj) == IF_DSD_PRIME ) - return 0; - if ( If_DsdObjType(pObj) == IF_DSD_XOR ) - { - If_DsdObjForEachFaninLit( p->vObjs, pObj, iFanin, i ) - { - if ( If_DsdManCheckInv_rec(p, iFanin) ) - { - RetValue = If_DsdManPushInv_rec(p, iFanin, pPerm); assert( RetValue ); - return 1; - } - pPerm += If_DsdVecLitSuppSize(p->vObjs, iFanin); - } - return 0; - } - if ( If_DsdObjType(pObj) == IF_DSD_MUX ) - { - if ( If_DsdManCheckInv_rec(p, pObj->pFans[1]) && If_DsdManCheckInv_rec(p, pObj->pFans[2]) ) - { - pPerm += If_DsdVecLitSuppSize(p->vObjs, pObj->pFans[0]); - RetValue = If_DsdManPushInv_rec(p, pObj->pFans[1], pPerm); assert( RetValue ); - pPerm += If_DsdVecLitSuppSize(p->vObjs, pObj->pFans[1]); - RetValue = If_DsdManPushInv_rec(p, pObj->pFans[2], pPerm); assert( RetValue ); - return 1; - } - return 0; - } - assert( 0 ); - return 0; -} -*/ int If_DsdManPushInv_rec( If_DsdMan_t * p, int iLit, unsigned char * pPerm ) { If_DsdObj_t * pObj; @@ -1577,20 +1535,18 @@ void If_DsdManTest() SeeAlso [] ***********************************************************************/ -void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fSpec, int fVerbose ) +void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fAdd, 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; + if ( !fAdd ) + If_DsdVecForEachObj( p->vObjs, pObj, i ) + pObj->fMark = 0; pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(p->vObjs) ); If_DsdVecForEachObj( p->vObjs, pObj, i ) { @@ -1598,37 +1554,17 @@ void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fSpec, int fVer 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 ); - } - } - } + if ( fAdd && !pObj->fMark ) + continue; + pObj->fMark = 0; + if ( If_DsdManCheckXY(p, Abc_Var2Lit(i, 0), LutSize, 0, 0) ) + continue; + if ( fFast ) + Value = 0; 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 ); - } + pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL ); + Value = If_ManSatCheckXYall( pSat, LutSize, pTruth, nVars, vLits ); } if ( Value ) continue; @@ -1636,7 +1572,6 @@ void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fSpec, int fVer } if ( pProgress ) Extra_ProgressBarStop( pProgress ); - If_ManSatUnbuild( pSat5 ); If_ManSatUnbuild( pSat ); Vec_IntFree( vLits ); if ( fVerbose ) diff --git a/src/map/if/ifSat.c b/src/map/if/ifSat.c index 9f4ea631..4af55203 100644 --- a/src/map/if/ifSat.c +++ b/src/map/if/ifSat.c @@ -82,27 +82,6 @@ void * If_ManSatBuildXYZ( int nLutSize ) iVarM + m ); return p; } -void * If_ManSatBuild55() -{ - int nMintsL = 16; - int nMintsF = 512; - 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++ ) - { - int iVar0 = (((m >> 2) & 7) << 1) | ((m & 3) == 3); - int iVar1 = ((m >> 6) & 7); - if ( (m >> 5) & 1 ) - sat_solver_add_mux( p, iVarP0 + iVar0, iVarP1 + 2 * iVar1 + 1, iVarP1 + 2 * iVar1, iVarM + m ); - else - sat_solver_add_buffer( p, iVarP1 + 2 * iVar1, iVarM + m, 0 ); - } - return p; -} void If_ManSatUnbuild( void * p ) { if ( p ) @@ -268,128 +247,6 @@ 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************************************************************* @@ -680,22 +537,6 @@ void If_ManSatTest3() 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