| /**CFile**************************************************************** |
| |
| FileName [extraUtilSupp.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [extra] |
| |
| Synopsis [Support minimization.] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: extraUtilSupp.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include <stdio.h> |
| #include <stdlib.h> |
| #include <string.h> |
| #include <assert.h> |
| #include "misc/vec/vec.h" |
| #include "misc/vec/vecWec.h" |
| #include "extra.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits ); |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| /**Function************************************************************* |
| |
| Synopsis [Generate m-out-of-n vectors.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline int Abc_SuppCountOnes( unsigned i ) |
| { |
| i = i - ((i >> 1) & 0x55555555); |
| i = (i & 0x33333333) + ((i >> 2) & 0x33333333); |
| i = ((i + (i >> 4)) & 0x0F0F0F0F); |
| return (i*(0x01010101))>>24; |
| } |
| Vec_Wrd_t * Abc_SuppGen( int m, int n ) |
| { |
| Vec_Wrd_t * vRes = Vec_WrdAlloc( 1000 ); |
| int i, Size = (1 << n); |
| for ( i = 0; i < Size; i++ ) |
| if ( Abc_SuppCountOnes(i) == m ) |
| Vec_WrdPush( vRes, i ); |
| return vRes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Perform verification.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Abc_SuppVerify( Vec_Wrd_t * p, word * pMatrix, int nVars, int nVarsMin ) |
| { |
| Vec_Wrd_t * pNew; |
| word * pLimit, * pEntry1, * pEntry2; |
| word Entry, EntryNew; |
| int i, k, v, Value, Counter = 0; |
| pNew = Vec_WrdAlloc( Vec_WrdSize(p) ); |
| Vec_WrdForEachEntry( p, Entry, i ) |
| { |
| EntryNew = 0; |
| for ( v = 0; v < nVarsMin; v++ ) |
| { |
| Value = 0; |
| for ( k = 0; k < nVars; k++ ) |
| if ( ((pMatrix[v] >> k) & 1) && ((Entry >> k) & 1) ) |
| Value ^= 1; |
| if ( Value ) |
| EntryNew |= (((word)1) << v); |
| } |
| Vec_WrdPush( pNew, EntryNew ); |
| } |
| // check that they are disjoint |
| pLimit = Vec_WrdLimit(pNew); |
| pEntry1 = Vec_WrdArray(pNew); |
| for ( ; pEntry1 < pLimit; pEntry1++ ) |
| for ( pEntry2 = pEntry1 + 1; pEntry2 < pLimit; pEntry2++ ) |
| if ( *pEntry1 == *pEntry2 ) |
| Counter++; |
| if ( Counter ) |
| printf( "The total of %d pairs fail verification.\n", Counter ); |
| else |
| printf( "Verification successful.\n" ); |
| Vec_WrdFree( pNew ); |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Generate pairs.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Wrd_t * Abc_SuppGenPairs( Vec_Wrd_t * p, int nBits ) |
| { |
| Vec_Wrd_t * vRes = Vec_WrdAlloc( 1000 ); |
| unsigned * pMap = ABC_CALLOC( unsigned, 1 << Abc_MaxInt(0,nBits-5) ); |
| word * pLimit = Vec_WrdLimit(p); |
| word * pEntry1 = Vec_WrdArray(p); |
| word * pEntry2, Value; |
| for ( ; pEntry1 < pLimit; pEntry1++ ) |
| for ( pEntry2 = pEntry1 + 1; pEntry2 < pLimit; pEntry2++ ) |
| { |
| Value = *pEntry1 ^ *pEntry2; |
| if ( Abc_InfoHasBit(pMap, (int)Value) ) |
| continue; |
| Abc_InfoXorBit( pMap, (int)Value ); |
| Vec_WrdPush( vRes, Value ); |
| } |
| ABC_FREE( pMap ); |
| return vRes; |
| } |
| Vec_Wrd_t * Abc_SuppGenPairs2( int nOnes, int nBits ) |
| { |
| Vec_Wrd_t * vRes = Vec_WrdAlloc( 1000 ); |
| int i, k, Size = (1 << nBits), Value; |
| for ( i = 0; i < Size; i++ ) |
| { |
| Value = Abc_SuppCountOnes(i); |
| for ( k = 1; k <= nOnes; k++ ) |
| if ( Value == 2*k ) |
| break; |
| if ( k <= nOnes ) |
| Vec_WrdPush( vRes, i ); |
| } |
| return vRes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Select variable.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Abc_SuppPrintMask( word uMask, int nBits ) |
| { |
| int i; |
| for ( i = 0; i < nBits; i++ ) |
| printf( "%d", (int)((uMask >> i) & 1) ); |
| printf( "\n" ); |
| } |
| void Abc_SuppGenProfile( Vec_Wrd_t * p, int nBits, int * pCounts ) |
| { |
| word Ent; |
| int i, k, b; |
| Vec_WrdForEachEntry( p, Ent, i ) |
| for ( b = ((Ent >> nBits) & 1), k = 0; k < nBits; k++ ) |
| pCounts[k] += ((Ent >> k) & 1) ^ b; |
| } |
| void Abc_SuppPrintProfile( Vec_Wrd_t * p, int nBits ) |
| { |
| int k, Counts[64] = {0}; |
| Abc_SuppGenProfile( p, nBits, Counts ); |
| for ( k = 0; k < nBits; k++ ) |
| printf( "%2d : %6d %6.2f %%\n", k, Counts[k], 100.0 * Counts[k] / Vec_WrdSize(p) ); |
| } |
| int Abc_SuppGenFindBest( Vec_Wrd_t * p, int nBits, int * pMerit ) |
| { |
| int k, kBest = 0, Counts[64] = {0}; |
| Abc_SuppGenProfile( p, nBits, Counts ); |
| for ( k = 1; k < nBits; k++ ) |
| if ( Counts[kBest] < Counts[k] ) |
| kBest = k; |
| *pMerit = Counts[kBest]; |
| return kBest; |
| } |
| void Abc_SuppGenSelectVar( Vec_Wrd_t * p, int nBits, int iVar ) |
| { |
| word * pEntry = Vec_WrdArray(p); |
| word * pLimit = Vec_WrdLimit(p); |
| for ( ; pEntry < pLimit; pEntry++ ) |
| if ( (*pEntry >> iVar) & 1 ) |
| *pEntry ^= (((word)1) << nBits); |
| } |
| void Abc_SuppGenFilter( Vec_Wrd_t * p, int nBits ) |
| { |
| word Ent; |
| int i, k = 0; |
| Vec_WrdForEachEntry( p, Ent, i ) |
| if ( ((Ent >> nBits) & 1) == 0 ) |
| Vec_WrdWriteEntry( p, k++, Ent ); |
| Vec_WrdShrink( p, k ); |
| } |
| word Abc_SuppFindOne( Vec_Wrd_t * p, int nBits ) |
| { |
| word uMask = 0; |
| int Prev = -1, This, Var; |
| while ( 1 ) |
| { |
| Var = Abc_SuppGenFindBest( p, nBits, &This ); |
| if ( Prev >= This ) |
| break; |
| Prev = This; |
| Abc_SuppGenSelectVar( p, nBits, Var ); |
| uMask |= (((word)1) << Var); |
| } |
| return uMask; |
| } |
| int Abc_SuppMinimize( word * pMatrix, Vec_Wrd_t * p, int nBits, int fVerbose ) |
| { |
| int i; |
| for ( i = 0; Vec_WrdSize(p) > 0; i++ ) |
| { |
| // Abc_SuppPrintProfile( p, nBits ); |
| pMatrix[i] = Abc_SuppFindOne( p, nBits ); |
| Abc_SuppGenFilter( p, nBits ); |
| if ( !fVerbose ) |
| continue; |
| // print stats |
| printf( "%2d : ", i ); |
| printf( "%6d ", Vec_WrdSize(p) ); |
| Abc_SuppPrintMask( pMatrix[i], nBits ); |
| // printf( "\n" ); |
| } |
| return i; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Create representation.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Abc_SuppTest( int nOnes, int nVars, int fUseSimple, int fCheck, int fVerbose ) |
| { |
| int nVarsMin; |
| word Matrix[64]; |
| abctime clk = Abc_Clock(); |
| // create the problem |
| Vec_Wrd_t * vRes = Abc_SuppGen( nOnes, nVars ); |
| Vec_Wrd_t * vPairs = fUseSimple ? Abc_SuppGenPairs2( nOnes, nVars ) : Abc_SuppGenPairs( vRes, nVars ); |
| assert( nVars < 100 ); |
| printf( "M = %2d N = %2d : ", nOnes, nVars ); |
| printf( "K = %6d ", Vec_WrdSize(vRes) ); |
| printf( "Total = %12.0f ", 0.5 * Vec_WrdSize(vRes) * (Vec_WrdSize(vRes) - 1) ); |
| printf( "Distinct = %8d ", Vec_WrdSize(vPairs) ); |
| Abc_PrintTime( 1, "Reduction time", Abc_Clock() - clk ); |
| // solve the problem |
| clk = Abc_Clock(); |
| nVarsMin = Abc_SuppMinimize( Matrix, vPairs, nVars, fVerbose ); |
| printf( "Solution with %d variables found. ", nVarsMin ); |
| Abc_PrintTime( 1, "Covering time", Abc_Clock() - clk ); |
| if ( fCheck ) |
| Abc_SuppVerify( vRes, Matrix, nVars, nVarsMin ); |
| Vec_WrdFree( vPairs ); |
| Vec_WrdFree( vRes ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Reads the input part of the cubes specified in MIN format.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Wrd_t * Abc_SuppReadMin( char * pFileName, int * pnVars ) |
| { |
| Vec_Wrd_t * vRes; word uCube; |
| int nCubes = 0, nVars = -1, iVar; |
| char * pCur, * pToken, * pStart = "INPUT F-COVER"; |
| char * pStr = Extra_FileReadContents( pFileName ); |
| if ( pStr == NULL ) |
| { printf( "Cannot open input file (%s).\n", pFileName ); return NULL; } |
| pCur = strstr( pStr, pStart ); |
| if ( pCur == NULL ) |
| { printf( "Cannot find beginning of cube cover (%s).\n", pStart ); return NULL; } |
| pToken = strtok( pCur + strlen(pStart), " \t\r\n," ); |
| nCubes = atoi( pToken ); |
| if ( nCubes < 1 || nCubes > 1000000 ) |
| { printf( "The number of cubes in not in the range [1; 1000000].\n" ); return NULL; } |
| vRes = Vec_WrdAlloc( 1000 ); |
| uCube = 0; iVar = 0; |
| while ( (pToken = strtok(NULL, " \t\r\n,")) != NULL ) |
| { |
| if ( strlen(pToken) > 2 ) |
| { |
| if ( !strncmp(pToken, "INPUT", strlen("INPUT")) ) |
| break; |
| if ( iVar > 64 ) |
| { printf( "The number of inputs (%d) is too high.\n", iVar ); Vec_WrdFree(vRes); return NULL; } |
| if ( nVars == -1 ) |
| nVars = iVar; |
| else if ( nVars != iVar ) |
| { printf( "The number of inputs (%d) does not match declaration (%d).\n", nVars, iVar ); Vec_WrdFree(vRes); return NULL; } |
| Vec_WrdPush( vRes, uCube ); |
| uCube = 0; iVar = 0; |
| continue; |
| } |
| if ( pToken[1] == '0' && pToken[0] == '1' ) // value 1 |
| uCube |= (((word)1) << iVar); |
| else if ( pToken[1] != '1' || pToken[0] != '0' ) // value 0 |
| { printf( "Strange literal representation (%s) of cube %d.\n", pToken, nCubes ); Vec_WrdFree(vRes); return NULL; } |
| iVar++; |
| } |
| ABC_FREE( pStr ); |
| if ( Vec_WrdSize(vRes) != nCubes ) |
| { printf( "The number of cubes (%d) does not match declaration (%d).\n", Vec_WrdSize(vRes), nCubes ); Vec_WrdFree(vRes); return NULL; } |
| else |
| printf( "Successfully parsed function with %d inputs and %d cubes.\n", nVars, nCubes ); |
| *pnVars = nVars; |
| return vRes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Wrd_t * Abc_SuppDiffMatrix( Vec_Wrd_t * vCubes ) |
| { |
| abctime clk = Abc_Clock(); |
| word * pEnt2, * pEnt = Vec_WrdArray( vCubes ); |
| word * pLimit = Vec_WrdLimit( vCubes ); |
| Vec_Wrd_t * vRes, * vPairs = Vec_WrdAlloc( Vec_WrdSize(vCubes) * (Vec_WrdSize(vCubes) - 1) / 2 ); |
| word * pStore = Vec_WrdArray( vPairs ); |
| for ( ; pEnt < pLimit; pEnt++ ) |
| for ( pEnt2 = pEnt+1; pEnt2 < pLimit; pEnt2++ ) |
| *pStore++ = *pEnt ^ *pEnt2; |
| vPairs->nSize = Vec_WrdCap(vPairs); |
| assert( pStore == Vec_WrdLimit(vPairs) ); |
| // Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| // vRes = Vec_WrdUniqifyHash( vPairs, 1 ); |
| vRes = Vec_WrdDup( vPairs ); |
| printf( "Successfully generated diff matrix with %10d rows (%6.2f %%). ", |
| Vec_WrdSize(vRes), 100.0 * Vec_WrdSize(vRes) / Vec_WrdSize(vPairs) ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| Vec_WrdFree( vPairs ); |
| return vRes; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [Solve difference matrix.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| static inline int Abc_SuppCountOnes64( word i ) |
| { |
| i = i - ((i >> 1) & 0x5555555555555555); |
| i = (i & 0x3333333333333333) + ((i >> 2) & 0x3333333333333333); |
| i = ((i + (i >> 4)) & 0x0F0F0F0F0F0F0F0F); |
| return (i*(0x0101010101010101))>>56; |
| } |
| int Abc_SuppFindVar( Vec_Wec_t * pS, Vec_Wec_t * pD, int nVars ) |
| { |
| int v, vBest = -1, dBest = -1; |
| for ( v = 0; v < nVars; v++ ) |
| { |
| if ( Vec_WecLevelSize(pS, v) ) |
| continue; |
| if ( vBest == -1 || dBest > Vec_WecLevelSize(pD, v) ) |
| vBest = v, dBest = Vec_WecLevelSize(pD, v); |
| } |
| return vBest; |
| } |
| void Abc_SuppRemove( Vec_Wrd_t * p, int * pCounts, Vec_Wec_t * pS, Vec_Wec_t * pD, int iVar, int nVars ) |
| { |
| word Entry; int i, v; |
| assert( Vec_WecLevelSize(pS, iVar) == 0 ); |
| Vec_IntClear( Vec_WecEntry(pD, iVar) ); |
| Vec_WrdForEachEntry( p, Entry, i ) |
| { |
| if ( ((Entry >> iVar) & 1) == 0 ) |
| continue; |
| pCounts[i]--; |
| if ( pCounts[i] == 1 ) |
| { |
| for ( v = 0; v < nVars; v++ ) |
| if ( (Entry >> v) & 1 ) |
| { |
| Vec_IntRemove( Vec_WecEntry(pD, v), i ); |
| Vec_WecPush( pS, v, i ); |
| } |
| } |
| else if ( pCounts[i] == 2 ) |
| { |
| for ( v = 0; v < nVars; v++ ) |
| if ( (Entry >> v) & 1 ) |
| Vec_WecPush( pD, v, i ); |
| } |
| } |
| } |
| void Abc_SuppProfile( Vec_Wec_t * pS, Vec_Wec_t * pD, int nVars ) |
| { |
| int v; |
| for ( v = 0; v < nVars; v++ ) |
| printf( "%2d : S = %3d D = %3d\n", v, Vec_WecLevelSize(pS, v), Vec_WecLevelSize(pD, v) ); |
| } |
| int Abc_SuppSolve( Vec_Wrd_t * p, int nVars ) |
| { |
| abctime clk = Abc_Clock(); |
| Vec_Wrd_t * pNew = Vec_WrdDup( p ); |
| Vec_Wec_t * vSingles = Vec_WecStart( 64 ); |
| Vec_Wec_t * vDoubles = Vec_WecStart( 64 ); |
| word Entry; int i, v, iVar, nVarsNew = nVars; |
| int * pCounts = ABC_ALLOC( int, Vec_WrdSize(p) ); |
| Vec_WrdForEachEntry( p, Entry, i ) |
| { |
| pCounts[i] = Abc_SuppCountOnes64( Entry ); |
| if ( pCounts[i] == 1 ) |
| { |
| for ( v = 0; v < nVars; v++ ) |
| if ( (Entry >> v) & 1 ) |
| Vec_WecPush( vSingles, v, i ); |
| } |
| else if ( pCounts[i] == 2 ) |
| { |
| for ( v = 0; v < nVars; v++ ) |
| if ( (Entry >> v) & 1 ) |
| Vec_WecPush( vDoubles, v, i ); |
| } |
| } |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| // Abc_SuppProfile( vSingles, vDoubles, nVars ); |
| // find variable in 0 singles and the smallest doubles |
| while ( 1 ) |
| { |
| iVar = Abc_SuppFindVar( vSingles, vDoubles, nVars ); |
| if ( iVar == -1 ) |
| break; |
| // printf( "Selected variable %d.\n", iVar ); |
| Abc_SuppRemove( pNew, pCounts, vSingles, vDoubles, iVar, nVars ); |
| // Abc_SuppProfile( vSingles, vDoubles, nVars ); |
| nVarsNew--; |
| } |
| // printf( "Result = %d (out of %d)\n", nVarsNew, nVars ); |
| Vec_WecFree( vSingles ); |
| Vec_WecFree( vDoubles ); |
| Vec_WrdFree( pNew ); |
| ABC_FREE( pCounts ); |
| return nVarsNew; |
| } |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Abc_SuppReadMinTest( char * pFileName ) |
| { |
| // int fVerbose = 0; |
| abctime clk = Abc_Clock(); |
| // word Matrix[64]; |
| int nVars, nVarsMin; |
| Vec_Wrd_t * vPairs, * vCubes; |
| vCubes = Abc_SuppReadMin( pFileName, &nVars ); |
| if ( vCubes == NULL ) |
| return; |
| vPairs = Abc_SuppDiffMatrix( vCubes ); |
| Vec_WrdFreeP( &vCubes ); |
| // solve the problem |
| clk = Abc_Clock(); |
| // nVarsMin = Abc_SuppMinimize( Matrix, vPairs, nVars, fVerbose ); |
| nVarsMin = Abc_SuppSolve( vPairs, nVars ); |
| printf( "Solution with %d variables found. ", nVarsMin ); |
| Abc_PrintTime( 1, "Covering time", Abc_Clock() - clk ); |
| |
| Vec_WrdFreeP( &vPairs ); |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
