/**CFile**************************************************************** FileName [bmcMesh.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [SAT-based bounded model checking.] Synopsis [Synthesis for mesh of LUTs.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: bmcMesh.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #include "bmc.h" #include "sat/satoko/satoko.h" #include "sat/satoko/solver.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// #define NCPARS 16 static inline int Bmc_MeshTVar( int Me[102][102], int x, int y ) { return Me[x][y]; } static inline int Bmc_MeshGVar( int Me[102][102], int x, int y ) { return Me[x][y] + Me[101][100]; } static inline int Bmc_MeshCVar( int Me[102][102], int x, int y ) { return Me[x][y] + Me[101][100] + Me[101][101]; } static inline int Bmc_MeshUVar( int Me[102][102], int x, int y ) { return Me[x][y] + Me[101][100] + Me[101][101] + NCPARS; } //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline int Bmc_MeshVarValue( satoko_t * p, int v ) { int value = var_value(p, v) != VAR_UNASSING ? var_value(p, v) : var_polarity(p, v); return value == LIT_TRUE; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Bmc_MeshAddOneHotness( satoko_t * pSat, int iFirst, int iLast ) { int i, j, v, pVars[100], nVars = 0, nCount = 0; assert( iFirst < iLast && iFirst + 110 > iLast ); for ( v = iFirst; v < iLast; v++ ) if ( Bmc_MeshVarValue(pSat, v) ) // v = 1 { assert( nVars < 100 ); pVars[ nVars++ ] = v; } if ( nVars <= 1 ) return 0; for ( i = 0; i < nVars; i++ ) for ( j = i+1; j < nVars; j++ ) { int pLits[2], RetValue; pLits[0] = Abc_Var2Lit( pVars[i], 1 ); pLits[1] = Abc_Var2Lit( pVars[j], 1 ); RetValue = satoko_add_clause( pSat, pLits, 2 ); assert( RetValue ); nCount++; } return nCount; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Bmc_MeshTest( Gia_Man_t * p, int X, int Y, int T, int fVerbose ) { abctime clk = Abc_Clock(); satoko_t * pSat = satoko_create(); Gia_Obj_t * pObj; int Me[102][102] = {{0}}; int pN[102][2] = {{0}}; int I = Gia_ManPiNum(p); int G = I + Gia_ManAndNum(p); int i, x, y, t, g, c, status, RetValue, Lit, iVar, nClauses = 0; assert( X <= 100 && Y <= 100 && T <= 100 && G <= 100 ); // init the graph for ( i = 0; i < I; i++ ) pN[i][0] = pN[i][1] = -1; Gia_ManForEachAnd( p, pObj, i ) { pN[i-1][0] = Gia_ObjFaninId0(pObj, i)-1; pN[i-1][1] = Gia_ObjFaninId1(pObj, i)-1; } if ( fVerbose ) { printf( "The graph has %d inputs: ", Gia_ManPiNum(p) ); for ( i = 0; i < I; i++ ) printf( "%c ", 'a' + i ); printf( " and %d nodes: ", Gia_ManAndNum(p) ); for ( i = I; i < G; i++ ) printf( "%c=%c%c ", 'a' + i, 'a' + pN[i][0] , 'a' + pN[i][1] ); printf( "\n" ); } // init SAT variables (time vars + graph vars + config vars) // config variables: 16 = 4 buff vars + 12 node vars iVar = 0; for ( y = 0; y < Y; y++ ) for ( x = 0; x < X; x++ ) { //printf( "%3d %3d %3d %s", iVar, iVar+T, iVar+T+G, x == X-1 ? "\n":"" ); Me[x][y] = iVar; iVar += T + G + NCPARS + 1; } Me[101][100] = T; Me[101][101] = G; if ( fVerbose ) printf( "SAT variable count is %d (%d time vars + %d graph vars + %d config vars + %d aux vars)\n", iVar, X*Y*T, X*Y*G, X*Y*NCPARS, X*Y ); // add constraints // time 0 and primary inputs only on the boundary for ( x = 0; x < X; x++ ) for ( y = 0; y < Y; y++ ) { int iTVar = Bmc_MeshTVar( Me, x, y ); int iGVar = Bmc_MeshGVar( Me, x, y ); if ( x == 0 || x == X-1 || y == 0 || y == Y-1 ) // boundary { // time 0 is required for ( t = 0; t < T; t++ ) { Lit = Abc_Var2Lit( iTVar+t, (int)(t > 0) ); RetValue = satoko_add_clause( pSat, &Lit, 1 ); assert( RetValue ); } // internal nodes are not allowed for ( g = I; g < G; g++ ) { Lit = Abc_Var2Lit( iGVar+g, 1 ); RetValue = satoko_add_clause( pSat, &Lit, 1 ); assert( RetValue ); } } else // not a boundary { Lit = Abc_Var2Lit( iTVar, 1 ); // cannot have time 0 RetValue = satoko_add_clause( pSat, &Lit, 1 ); assert( RetValue ); } } for ( x = 1; x < X-1; x++ ) for ( y = 1; y < Y-1; y++ ) { int pLits[100], nLits; int iTVar = Bmc_MeshTVar( Me, x, y ); int iGVar = Bmc_MeshGVar( Me, x, y ); int iCVar = Bmc_MeshCVar( Me, x, y ); int iUVar = Bmc_MeshUVar( Me, x, y ); // 0=left 1=up 2=right 3=down int iTVars[4]; int iGVars[4]; iTVars[0] = Bmc_MeshTVar( Me, x-1, y ); iGVars[0] = Bmc_MeshGVar( Me, x-1, y ); iTVars[1] = Bmc_MeshTVar( Me, x, y-1 ); iGVars[1] = Bmc_MeshGVar( Me, x, y-1 ); iTVars[2] = Bmc_MeshTVar( Me, x+1, y ); iGVars[2] = Bmc_MeshGVar( Me, x+1, y ); iTVars[3] = Bmc_MeshTVar( Me, x, y+1 ); iGVars[3] = Bmc_MeshGVar( Me, x, y+1 ); // condition when cell is used for ( g = 0; g < G; g++ ) { pLits[0] = Abc_Var2Lit( iGVar+g, 1 ); pLits[1] = Abc_Var2Lit( iUVar, 0 ); RetValue = satoko_add_clause( pSat, pLits, 2 ); assert( RetValue ); nClauses++; } // at least one time is used pLits[0] = Abc_Var2Lit( iUVar, 1 ); for ( t = 1; t < T; t++ ) pLits[t] = Abc_Var2Lit( iTVar+t, 0 ); RetValue = satoko_add_clause( pSat, pLits, T ); assert( RetValue ); nClauses++; // at least one config is used pLits[0] = Abc_Var2Lit( iUVar, 1 ); for ( c = 0; c < NCPARS; c++ ) pLits[c+1] = Abc_Var2Lit( iCVar+c, 0 ); RetValue = satoko_add_clause( pSat, pLits, NCPARS+1 ); assert( RetValue ); nClauses++; // constraints for each time for ( t = 1; t < T; t++ ) { int Conf[12][2] = {{0, 1}, {0, 2}, {0, 3}, {1, 2}, {1, 3}, {2, 3}, {1, 0}, {2, 0}, {3, 0}, {2, 1}, {3, 1}, {3, 2}}; // buffer for ( g = 0; g < G; g++ ) for ( c = 0; c < 4; c++ ) { nLits = 0; pLits[ nLits++ ] = Abc_Var2Lit( iTVar+t, 1 ); pLits[ nLits++ ] = Abc_Var2Lit( iGVar+g, 1 ); pLits[ nLits++ ] = Abc_Var2Lit( iCVar+c, 1 ); pLits[ nLits++ ] = Abc_Var2Lit( iTVars[c]+t-1, 0 ); RetValue = satoko_add_clause( pSat, pLits, nLits ); assert( RetValue ); nLits = 0; pLits[ nLits++ ] = Abc_Var2Lit( iTVar+t, 1 ); pLits[ nLits++ ] = Abc_Var2Lit( iGVar+g, 1 ); pLits[ nLits++ ] = Abc_Var2Lit( iCVar+c, 1 ); pLits[ nLits++ ] = Abc_Var2Lit( iGVars[c]+g, 0 ); RetValue = satoko_add_clause( pSat, pLits, nLits ); assert( RetValue ); nClauses += 2; } for ( g = 0; g < I; g++ ) for ( c = 4; c < NCPARS; c++ ) { pLits[0] = Abc_Var2Lit( iGVar+g, 1 ); pLits[1] = Abc_Var2Lit( iCVar+c, 1 ); RetValue = satoko_add_clause( pSat, pLits, 2 ); assert( RetValue ); nClauses++; } // node for ( g = I; g < G; g++ ) for ( c = 0; c < 12; c++ ) { assert( pN[g][0] >= 0 && pN[g][1] >= 0 ); nLits = 0; pLits[ nLits++ ] = Abc_Var2Lit( iTVar+t, 1 ); pLits[ nLits++ ] = Abc_Var2Lit( iGVar+g, 1 ); pLits[ nLits++ ] = Abc_Var2Lit( iCVar+c+4, 1 ); pLits[ nLits++ ] = Abc_Var2Lit( iTVars[Conf[c][0]]+t-1, 0 ); RetValue = satoko_add_clause( pSat, pLits, nLits ); assert( RetValue ); nLits = 0; pLits[ nLits++ ] = Abc_Var2Lit( iTVar+t, 1 ); pLits[ nLits++ ] = Abc_Var2Lit( iGVar+g, 1 ); pLits[ nLits++ ] = Abc_Var2Lit( iCVar+c+4, 1 ); pLits[ nLits++ ] = Abc_Var2Lit( iTVars[Conf[c][1]]+t-1, 0 ); RetValue = satoko_add_clause( pSat, pLits, nLits ); assert( RetValue ); nLits = 0; pLits[ nLits++ ] = Abc_Var2Lit( iTVar+t, 1 ); pLits[ nLits++ ] = Abc_Var2Lit( iGVar+g, 1 ); pLits[ nLits++ ] = Abc_Var2Lit( iCVar+c+4, 1 ); pLits[ nLits++ ] = Abc_Var2Lit( iGVars[Conf[c][0]]+pN[g][0], 0 ); RetValue = satoko_add_clause( pSat, pLits, nLits ); assert( RetValue ); nLits = 0; pLits[ nLits++ ] = Abc_Var2Lit( iTVar+t, 1 ); pLits[ nLits++ ] = Abc_Var2Lit( iGVar+g, 1 ); pLits[ nLits++ ] = Abc_Var2Lit( iCVar+c+4, 1 ); pLits[ nLits++ ] = Abc_Var2Lit( iGVars[Conf[c][1]]+pN[g][1], 0 ); RetValue = satoko_add_clause( pSat, pLits, nLits ); assert( RetValue ); nClauses += 4; } } } // final condition { int iGVar = Bmc_MeshGVar( Me, 1, 1 ) + G-1; Lit = Abc_Var2Lit( iGVar, 0 ); RetValue = satoko_add_clause( pSat, &Lit, 1 ); if ( RetValue == 0 ) { printf( "Problem has no solution. " ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); satoko_destroy( pSat ); return; } } if ( fVerbose ) printf( "Finished adding %d clauses. Started solving...\n", nClauses ); while ( 1 ) { int nAddClauses = 0; status = satoko_solve( pSat ); if ( status == SATOKO_UNSAT ) { printf( "Problem has no solution. " ); break; } if ( status == SATOKO_UNDEC ) { printf( "Computation timed out. " ); break; } assert( status == SATOKO_SAT ); // check if the solution is valid and add constraints for ( x = 0; x < X; x++ ) for ( y = 0; y < Y; y++ ) { if ( x == 0 || x == X-1 || y == 0 || y == Y-1 ) // boundary { int iGVar = Bmc_MeshGVar( Me, x, y ); nAddClauses += Bmc_MeshAddOneHotness( pSat, iGVar, iGVar + G ); } else { int iTVar = Bmc_MeshTVar( Me, x, y ); int iGVar = Bmc_MeshGVar( Me, x, y ); int iCVar = Bmc_MeshCVar( Me, x, y ); nAddClauses += Bmc_MeshAddOneHotness( pSat, iTVar, iTVar + T ); nAddClauses += Bmc_MeshAddOneHotness( pSat, iGVar, iGVar + G ); nAddClauses += Bmc_MeshAddOneHotness( pSat, iCVar, iCVar + NCPARS ); } } if ( nAddClauses > 0 ) { printf( "Adding %d one-hotness clauses.\n", nAddClauses ); continue; } printf( "Satisfying solution found. " ); /* iVar = solver_varnum(pSat); for ( i = 0; i < iVar; i++ ) if ( Bmc_MeshVarValue(pSat, i) ) printf( "%d ", i ); printf( "\n" ); */ break; } Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); if ( status == SATOKO_SAT ) { // count the number of nodes and buffers int nBuffs = 0, nNodes = 0; for ( y = 1; y < Y-1; y++ ) for ( x = 1; x < X-1; x++ ) { int iCVar = Bmc_MeshCVar( Me, x, y ); for ( c = 0; c < 4; c++ ) if ( Bmc_MeshVarValue(pSat, iCVar+c) ) { //printf( "Buffer y=%d x=%d (var = %d; config = %d)\n", y, x, iCVar+c, c ); nBuffs++; } for ( c = 4; c < NCPARS; c++ ) if ( Bmc_MeshVarValue(pSat, iCVar+c) ) { //printf( "Node y=%d x=%d (var = %d; config = %d)\n", y, x, iCVar+c, c ); nNodes++; } } printf( "The %d x %d mesh with latency %d with %d active cells (%d nodes and %d buffers):\n", X, Y, T, nNodes+nBuffs, nNodes, nBuffs ); // print mesh printf( " Y\\X " ); for ( x = 0; x < X; x++ ) printf( " %-2d ", x ); printf( "\n" ); for ( y = 0; y < Y; y++ ) { printf( " %-2d ", y ); for ( x = 0; x < X; x++ ) { int iTVar = Bmc_MeshTVar( Me, x, y ); int iGVar = Bmc_MeshGVar( Me, x, y ); int fFound = 0; ; for ( t = 0; t < T; t++ ) for ( g = 0; g < G; g++ ) if ( Bmc_MeshVarValue(pSat, iTVar+t) && Bmc_MeshVarValue(pSat, iGVar+g) ) { printf( " %c%-2d ", 'a' + g, t ); fFound = 1; } if ( fFound ) continue; if ( x == 0 || x == X-1 || y == 0 || y == Y-1 ) // boundary printf( " * " ); else printf( " " ); } printf( "\n" ); } } satoko_destroy( pSat ); } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END