From 5f9ca14a7f3635bda76dbc137811b26a00816bcf Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 4 Mar 2014 14:48:36 -0800 Subject: Changes to LUT mappers. --- src/map/if/ifSat.c | 98 ++++++++++++++++++++++++++++++++++++++++++++++++------ 1 file changed, 87 insertions(+), 11 deletions(-) (limited to 'src/map/if/ifSat.c') diff --git a/src/map/if/ifSat.c b/src/map/if/ifSat.c index 3fec34e0..cfce7369 100644 --- a/src/map/if/ifSat.c +++ b/src/map/if/ifSat.c @@ -42,7 +42,7 @@ ABC_NAMESPACE_IMPL_START SeeAlso [] ***********************************************************************/ -sat_solver * If_ManSatBuildXY( int nLutSize ) +void * If_ManSatBuildXY( int nLutSize ) { int nMintsL = (1 << nLutSize); int nMintsF = (1 << (2 * nLutSize - 1)); @@ -57,6 +57,54 @@ sat_solver * If_ManSatBuildXY( int nLutSize ) return p; } +/**Function************************************************************* + + Synopsis [Verification for 6-input function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static word If_ManSat6ComposeLut4( int t, word f[4], int k ) +{ + int m, v, nMints = (1 << k); + word c, r = 0; + assert( k <= 4 ); + for ( m = 0; m < nMints; m++ ) + { + if ( !((t >> m) & 1) ) + continue; + c = ~(word)0; + for ( v = 0; v < k; v++ ) + c &= ((m >> v) & 1) ? f[v] : ~f[v]; + r |= c; + } + return r; +} +word If_ManSat6Truth( word uBound, word uFree, int * pBSet, int nBSet, int * pSSet, int nSSet, int * pFSet, int nFSet ) +{ + word r, q, f[4]; + int i, k = 0; + // bound set vars + for ( i = 0; i < nSSet; i++ ) + f[k++] = s_Truths6[pSSet[i]]; + for ( i = 0; i < nBSet; i++ ) + f[k++] = s_Truths6[pBSet[i]]; + q = If_ManSat6ComposeLut4( (int)(uBound & 0xffff), f, k ); + // free set vars + k = 0; + f[k++] = q; + for ( i = 0; i < nSSet; i++ ) + f[k++] = s_Truths6[pSSet[i]]; + for ( i = 0; i < nFSet; i++ ) + f[k++] = s_Truths6[pFSet[i]]; + r = If_ManSat6ComposeLut4( (int)(uFree & 0xffff), f, k ); + return r; +} + /**Function************************************************************* Synopsis [Returns config string for the given truth table.] @@ -68,14 +116,16 @@ sat_solver * If_ManSatBuildXY( int nLutSize ) SeeAlso [] ***********************************************************************/ -int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, unsigned uSet, word * pTBound, word * pTFree, Vec_Int_t * vLits ) +int If_ManSatCheckXY( void * pSat, 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; + sat_solver * p = (sat_solver *)pSat; + int iBSet, nBSet = 0, pBSet[IF_MAX_FUNC_LUTSIZE]; + int iSSet, nSSet = 0, pSSet[IF_MAX_FUNC_LUTSIZE]; + int iFSet, nFSet = 0, pFSet[IF_MAX_FUNC_LUTSIZE]; int nMintsL = (1 << nLutSize); int nMintsF = (1 << (2 * nLutSize - 1)); int v, Value, m, mNew, nMintsFNew, nMintsLNew; + word Res; // collect variable sets Dau_DecSortSet( uSet, nVars, &nBSet, &nSSet, &nFSet ); assert( nBSet + nSSet + nFSet == nVars ); @@ -94,13 +144,13 @@ int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, un if ( Value == 0 ) // FS { if ( ((m >> v) & 1) ) - mNew |= 1 << (nLutSize + nSSet + iFSet); + mNew |= 1 << (nLutSize + nSSet + iFSet), pFSet[iFSet] = v; iFSet++; } else if ( Value == 1 ) // BS { if ( ((m >> v) & 1) ) - mNew |= 1 << (nSSet + iBSet); + mNew |= 1 << (nSSet + iBSet), pBSet[iBSet] = v; iBSet++; } else if ( Value == 3 ) // SS @@ -109,6 +159,7 @@ int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, un { mNew |= 1 << iSSet; mNew |= 1 << (nLutSize + iSSet); + pSSet[iSSet] = v; } iSSet++; } @@ -143,11 +194,36 @@ int If_ManSatCheckXY( sat_solver * p, int nLutSize, word * pTruth, int nVars, un // collect configs assert( nSSet + nFSet + 1 <= nLutSize ); *pTFree = 0; - nMintsLNew = (1 << (nSSet + nFSet + 1)); + nMintsLNew = (1 << (1 + nSSet + nFSet)); 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 ); + *pTFree = Abc_Tt6Stretch( *pTFree, 1 + nSSet + nFSet ); + if ( nVars != 6 ) + return 1; + // verify the result + Res = If_ManSat6Truth( *pTBound, *pTFree, pBSet, nBSet, pSSet, nSSet, pFSet, nFSet ); + if ( pTruth[0] != Res ) + { + Dau_DsdPrintFromTruth( pTruth, nVars ); + Dau_DsdPrintFromTruth( &Res, nVars ); + Dau_DsdPrintFromTruth( pTBound, nSSet+nBSet ); + Dau_DsdPrintFromTruth( pTFree, nSSet+nFSet+1 ); + printf( "Verification failed!\n" ); + } +/* + else + { +// Kit_DsdPrintFromTruth( (unsigned*)pTBound, nSSet+nBSet ); printf( "\n" ); +// Kit_DsdPrintFromTruth( (unsigned*)pTFree, nSSet+nFSet+1 ); printf( "\n" ); + + Dau_DsdPrintFromTruth( pTruth, nVars ); + Dau_DsdPrintFromTruth( &Res, nVars ); + Dau_DsdPrintFromTruth( pTBound, nSSet+nBSet ); + Dau_DsdPrintFromTruth( pTFree, nSSet+nFSet+1 ); + printf( "Verification OK!\n" ); + } +*/ return 1; } @@ -166,7 +242,7 @@ void If_ManSatTest2() { int nVars = 6; int nLutSize = 4; - sat_solver * p = If_ManSatBuildXY( nLutSize ); + sat_solver * p = (sat_solver *)If_ManSatBuildXY( nLutSize ); // char * pDsd = "(abcdefg)"; // char * pDsd = "([a!bc]d!e)"; char * pDsd = "0123456789ABCDEF{abcdef}"; @@ -194,7 +270,7 @@ void If_ManSatTest() { int nVars = 4; int nLutSize = 3; - sat_solver * p = If_ManSatBuildXY( nLutSize ); + sat_solver * p = (sat_solver *)If_ManSatBuildXY( nLutSize ); word t = 0x183C, * pTruth = &t; word uBound, uFree; unsigned uSet; -- cgit v1.2.3