| /**CFile**************************************************************** |
| |
| FileName [sbd.c] |
| |
| SystemName [ABC: Logic synthesis and verification system.] |
| |
| PackageName [SAT-based optimization using internal don't-cares.] |
| |
| Synopsis [] |
| |
| Author [Alan Mishchenko] |
| |
| Affiliation [UC Berkeley] |
| |
| Date [Ver. 1.0. Started - June 20, 2005.] |
| |
| Revision [$Id: sbd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] |
| |
| ***********************************************************************/ |
| |
| #include "sbdInt.h" |
| #include "misc/util/utilTruth.h" |
| |
| ABC_NAMESPACE_IMPL_START |
| |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// DECLARATIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| #define MAX_M 8 // max inputs |
| #define MAX_N 30 // max nodes |
| #define MAX_K 6 // max lutsize |
| #define MAX_D 8 // max delays |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// FUNCTION DEFINITIONS /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| // new AIG manager |
| typedef struct Sbd_Pro_t_ Sbd_Pro_t; |
| struct Sbd_Pro_t_ |
| { |
| int nLuts; // LUT count |
| int nSize; // LUT size |
| int nDivs; // divisor count |
| int nVars; // intermediate variables (nLuts * nSize) |
| int nPars; // total parameter count (nLuts * (1 << nSize) + nLuts * nSize * nDivs) |
| int pPars1[SBD_LUTS_MAX][1<<SBD_SIZE_MAX]; // lut parameters |
| int pPars2[SBD_LUTS_MAX][SBD_SIZE_MAX][SBD_DIV_MAX]; // topo parameters |
| int pVars[SBD_LUTS_MAX][SBD_SIZE_MAX+1]; // internal variables |
| int pDivs[SBD_DIV_MAX]; // divisor variables (external) |
| }; |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| Vec_Int_t * Sbd_ProblemSetup( Sbd_Pro_t * p, int nLuts, int nSize, int nDivs ) |
| { |
| Vec_Int_t * vCnf = Vec_IntAlloc( 1000 ); |
| int i, k, d, v, n, iVar = 0; |
| assert( nLuts >= 1 && nLuts <= 2 ); |
| memset( p, 0, sizeof(Sbd_Pro_t) ); |
| p->nLuts = nLuts; |
| p->nSize = nSize; |
| p->nDivs = nDivs; |
| p->nVars = nLuts * nSize; |
| p->nPars = nLuts * (1 << nSize) + nLuts * nSize * nDivs; |
| // set parameters |
| for ( i = 0; i < nLuts; i++ ) |
| for ( k = 0; k < (1 << nSize); k++ ) |
| p->pPars1[i][k] = iVar++; |
| for ( i = 0; i < nLuts; i++ ) |
| for ( k = 0; k < nSize; k++ ) |
| for ( d = 0; d < nDivs; d++ ) |
| p->pPars2[i][k][d] = iVar++; |
| // set intermediate variables |
| for ( i = 0; i < nLuts; i++ ) |
| for ( k = 0; k < nSize; k++ ) |
| p->pVars[i][k] = iVar++; |
| // set top variables |
| for ( i = 1; i < nLuts; i++ ) |
| p->pVars[i][nSize] = p->pVars[i-1][0]; |
| // set divisor variables |
| for ( d = 0; d < nDivs; d++ ) |
| p->pDivs[d] = iVar++; |
| assert( iVar == p->nPars + p->nVars + p->nDivs ); |
| |
| // input compatiblity clauses |
| for ( i = 0; i < nLuts; i++ ) |
| for ( k = (i > 0); k < nSize; k++ ) |
| for ( d = 0; d < nDivs; d++ ) |
| for ( n = 0; n < nDivs; n++ ) |
| { |
| if ( n < d ) |
| { |
| Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) ); |
| Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][n], 0) ); |
| Vec_IntPush( vCnf, -1 ); |
| } |
| else if ( k < nSize-1 ) |
| { |
| Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) ); |
| Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k+1][n], 0) ); |
| Vec_IntPush( vCnf, -1 ); |
| } |
| } |
| |
| // create LUT clauses |
| for ( i = 0; i < nLuts; i++ ) |
| for ( k = 0; k < (1 << nSize); k++ ) |
| for ( n = 0; n < 2; n++ ) |
| { |
| for ( v = 0; v < nSize; v++ ) |
| Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][v], (k >> v) & 1) ); |
| Vec_IntPush( vCnf, Abc_Var2Lit(p->pVars[i][nSize], n) ); |
| Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][k], !n) ); |
| Vec_IntPush( vCnf, -1 ); |
| } |
| |
| // create input clauses |
| for ( i = 0; i < nLuts; i++ ) |
| for ( k = (i > 0); k < nSize; k++ ) |
| for ( d = 0; d < nDivs; d++ ) |
| for ( n = 0; n < 2; n++ ) |
| { |
| Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars2[i][k][d], 0) ); |
| Vec_IntPush( vCnf, Abc_Var2Lit(p->pPars1[i][k], n) ); |
| Vec_IntPush( vCnf, Abc_Var2Lit(p->pDivs[d], !n) ); |
| Vec_IntPush( vCnf, -1 ); |
| } |
| |
| return vCnf; |
| } |
| // add clauses to the don't-care computation solver |
| void Sbd_ProblemLoad1( Sbd_Pro_t * p, Vec_Int_t * vCnf, int iStartVar, int * pDivVars, int iTopVar, sat_solver * pSat ) |
| { |
| int pLits[8], nLits, i, k, iLit, RetValue; |
| int ThisTopVar = p->pVars[0][p->nSize]; |
| int FirstDivVar = p->nPars + p->nVars; |
| // add clauses |
| for ( i = 0; i < Vec_IntSize(vCnf); i++ ) |
| { |
| assert( Vec_IntEntry(vCnf, i) != -1 ); |
| for ( k = i+1; k < Vec_IntSize(vCnf); k++ ) |
| if ( Vec_IntEntry(vCnf, i) == -1 ) |
| break; |
| nLits = 0; |
| Vec_IntForEachEntryStartStop( vCnf, iLit, i, i, k ) { |
| if ( Abc_Lit2Var(iLit) == ThisTopVar ) |
| pLits[nLits++] = Abc_Var2Lit( ThisTopVar, Abc_LitIsCompl(iLit) ); |
| else if ( Abc_Lit2Var(iLit) >= FirstDivVar ) |
| pLits[nLits++] = Abc_Var2Lit( pDivVars[Abc_Lit2Var(iLit)-FirstDivVar], Abc_LitIsCompl(iLit) ); |
| else |
| pLits[nLits++] = iLit + 2 * iStartVar; |
| } |
| assert( nLits <= 8 ); |
| RetValue = sat_solver_addclause( pSat, pLits, pLits + nLits ); |
| assert( RetValue ); |
| } |
| } |
| // add clauses to the functionality evaluation solver |
| void Sbd_ProblemLoad2( Sbd_Pro_t * p, Vec_Wec_t * vCnf, int iStartVar, int * pDivVarValues, int iTopVarValue, sat_solver * pSat ) |
| { |
| Vec_Int_t * vLevel; |
| int pLits[8], nLits, i, k, iLit, RetValue; |
| int ThisTopVar = p->pVars[0][p->nSize]; |
| int FirstDivVar = p->nPars + p->nVars; |
| int FirstIntVar = p->nPars; |
| // add clauses |
| Vec_WecForEachLevel( vCnf, vLevel, i ) |
| { |
| nLits = 0; |
| Vec_IntForEachEntry( vLevel, iLit, k ) { |
| if ( Abc_Lit2Var(iLit) == ThisTopVar ) |
| { |
| if ( Abc_LitIsCompl(iLit) == iTopVarValue ) |
| break; |
| continue; |
| } |
| else if ( Abc_Lit2Var(iLit) >= FirstDivVar ) |
| { |
| if ( Abc_LitIsCompl(iLit) == pDivVarValues[Abc_Lit2Var(iLit)-FirstDivVar] ) |
| break; |
| continue; |
| } |
| else if ( Abc_Lit2Var(iLit) >= FirstIntVar ) |
| pLits[nLits++] = iLit + 2 * iStartVar; |
| else |
| pLits[nLits++] = iLit; |
| } |
| if ( k < Vec_IntSize(vLevel) ) |
| continue; |
| assert( nLits <= 8 ); |
| RetValue = sat_solver_addclause( pSat, pLits, pLits + nLits ); |
| assert( RetValue ); |
| } |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| sat_solver * Sbd_SolverTopo( int M, int N, int K, int pVars[MAX_N][MAX_M+MAX_N][MAX_K], int pVars2[MAX_M+MAX_N][MAX_D], int pDelays[], int Req, int * pnVars ) // inputs, nodes, lutsize |
| { |
| sat_solver * pSat = NULL; |
| Vec_Int_t * vTemp = Vec_IntAlloc(100); |
| // assign vars |
| int RetValue, n, i, j, j2, k, k2, d, Count, nVars = 0; |
| for ( n = 0; n < N; n++ ) |
| for ( i = 0; i < M+N; i++ ) |
| for ( k = 0; k < K; k++ ) |
| pVars[n][i][k] = -1; |
| for ( n = 0; n < N; n++ ) |
| for ( i = 0; i < M+n; i++ ) |
| for ( k = 0; k < K; k++ ) |
| pVars[n][i][k] = nVars++; |
| printf( "Number of topo vars = %d.\n", nVars ); |
| *pnVars = nVars; |
| // add constraints |
| pSat = sat_solver_new(); |
| sat_solver_setnvars( pSat, nVars ); |
| // each node is used |
| for ( i = 0; i < M+N-1; i++ ) |
| { |
| Vec_IntClear( vTemp ); |
| for ( n = 0; n < N; n++ ) |
| for ( k = 0; k < K; k++ ) |
| if ( pVars[n][i][k] >= 0 ) |
| Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][k], 0) ); |
| RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) ); |
| assert( RetValue ); |
| } |
| printf( "Added %d node connectivity constraints.\n", i ); |
| // each fanin of each node is connected exactly once |
| Count = 0; |
| for ( n = 0; n < N; n++ ) |
| for ( k = 0; k < K; k++ ) |
| { |
| // connected |
| Vec_IntClear( vTemp ); |
| for ( i = 0; i < M+n; i++ ) |
| Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][k], 0) ); |
| RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) ); |
| assert( RetValue ); |
| // exactly once |
| for ( i = 0; i < M+n; i++ ) |
| for ( j = i+1; j < M+n; j++ ) |
| { |
| Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][k], 1), Abc_Var2Lit(pVars[n][j][k], 1) ); |
| RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) ); |
| assert( RetValue ); |
| Count++; |
| } |
| } |
| printf( "Added %d fanin connectivity constraints.\n", Count ); |
| // node fanins are unique |
| Count = 0; |
| for ( n = 0; n < N; n++ ) |
| for ( i = 0; i < M+n; i++ ) |
| for ( k = 0; k < K; k++ ) |
| for ( j = i; j < M+n; j++ ) |
| for ( k2 = k+1; k2 < K; k2++ ) |
| { |
| Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][k], 1), Abc_Var2Lit(pVars[n][j][k2], 1) ); |
| RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) ); |
| assert( RetValue ); |
| Count++; |
| } |
| printf( "Added %d fanin exclusivity constraints.\n", Count ); |
| // nodes are ordered |
| Count = 0; |
| for ( n = 1; n < N; n++ ) |
| for ( i = 0; i < M+n-1; i++ ) |
| { |
| // first of n cannot be smaller than first of n-1 (but can be equal) |
| for ( j = i+1; j < M+n-1; j++ ) |
| { |
| Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][0], 1), Abc_Var2Lit(pVars[n-1][j][0], 1) ); |
| RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) ); |
| assert( RetValue ); |
| Count++; |
| } |
| // if first nodes of n and n-1 are equal, second nodes are ordered |
| Vec_IntFillTwo( vTemp, 2, Abc_Var2Lit(pVars[n][i][0], 1), Abc_Var2Lit(pVars[n-1][i][0], 1) ); |
| for ( j = 0; j < i; j++ ) |
| for ( j2 = j+1; j2 < i; j2++ ) |
| { |
| Vec_IntPushTwo( vTemp, Abc_Var2Lit(pVars[n][j][1], 1), Abc_Var2Lit(pVars[n-1][j2][1], 1) ); |
| RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) ); |
| assert( RetValue ); |
| Vec_IntShrink( vTemp, 2 ); |
| Count++; |
| } |
| } |
| printf( "Added %d node ordering constraints.\n", Count ); |
| // exclude fanins of two-input nodes |
| Count = 0; |
| if ( K == 2 ) |
| for ( n = 1; n < N; n++ ) |
| for ( i = M; i < M+n; i++ ) |
| for ( j = 0; j < i; j++ ) |
| for ( k = 0; k < K; k++ ) |
| { |
| Vec_IntClear( vTemp ); |
| Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][i][0], 1) ); |
| Vec_IntPush( vTemp, Abc_Var2Lit(pVars[n][j][1], 1) ); |
| Vec_IntPush( vTemp, Abc_Var2Lit(pVars[i-M][j][k], 1) ); |
| RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) ); |
| assert( RetValue ); |
| Count++; |
| } |
| printf( "Added %d two-node non-triviality constraints.\n", Count ); |
| |
| |
| // assign delay vars |
| assert( Req < MAX_D-1 ); |
| for ( i = 0; i < M+N; i++ ) |
| for ( d = 0; d < MAX_D; d++ ) |
| pVars2[i][d] = nVars++; |
| printf( "Number of total vars = %d.\n", nVars ); |
| // set input delays |
| for ( i = 0; i < M; i++ ) |
| { |
| assert( pDelays[i] < MAX_D-2 ); |
| Vec_IntFill( vTemp, 1, Abc_Var2Lit(pVars2[i][pDelays[i]], 0) ); |
| RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) ); |
| assert( RetValue ); |
| } |
| // set output delay |
| for ( k = Req; k < MAX_D; k++ ) |
| { |
| Vec_IntFill( vTemp, 1, Abc_Var2Lit(pVars2[M+N-1][Req+1], 1) ); |
| RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) ); |
| assert( RetValue ); |
| } |
| // set internal nodes |
| for ( n = 0; n < N; n++ ) |
| for ( i = 0; i < M+n; i++ ) |
| for ( k = 0; k < K; k++ ) |
| for ( d = 0; d < MAX_D-1; d++ ) |
| { |
| Vec_IntFill( vTemp, 1, Abc_Var2Lit(pVars[n][i][k], 1) ); |
| Vec_IntPush( vTemp, Abc_Var2Lit(pVars2[i][d], 1) ); |
| Vec_IntPush( vTemp, Abc_Var2Lit(pVars2[M+n][d+1], 0) ); |
| RetValue = sat_solver_addclause( pSat, Vec_IntArray(vTemp), Vec_IntLimit(vTemp) ); |
| assert( RetValue ); |
| } |
| |
| |
| Vec_IntFree( vTemp ); |
| return pSat; |
| } |
| void Sbd_SolverTopoPrint( sat_solver * pSat, int M, int N, int K, int pVars[MAX_N][MAX_M+MAX_N][MAX_K] ) |
| { |
| int n, i, k; |
| printf( "Solution:\n" ); |
| printf( " | " ); |
| for ( n = 0; n < N; n++ ) |
| printf( "%2d ", M+n ); |
| printf( "\n" ); |
| for ( i = M+N-2; i >= 0; i-- ) |
| { |
| printf( "%2d %c | ", i, i < M ? 'i' : ' ' ); |
| for ( n = 0; n < N; n++ ) |
| { |
| for ( k = K-1; k >= 0; k-- ) |
| if ( pVars[n][i][k] == -1 ) |
| printf( " " ); |
| else |
| printf( "%c", sat_solver_var_value(pSat, pVars[n][i][k]) ? '*' : '.' ); |
| printf( " " ); |
| } |
| printf( "\n" ); |
| } |
| } |
| void Sbd_SolverTopoTest() |
| { |
| int M = 8; // 6; // inputs |
| int N = 3; // 16; // nodes |
| int K = 4; // 2; // lutsize |
| int status, v, nVars, nIter, nSols = 0; |
| int pVars[MAX_N][MAX_M+MAX_N][MAX_K]; // 20 x 32 x 6 = 3840 |
| int pVars2[MAX_M+MAX_N][MAX_D]; // 20 x 32 x 6 = 3840 |
| int pDelays[MAX_M] = {1,0,0,0,1}; |
| abctime clk = Abc_Clock(); |
| Vec_Int_t * vLits = Vec_IntAlloc(100); |
| sat_solver * pSat = Sbd_SolverTopo( M, N, K, pVars, pVars2, pDelays, 2, &nVars ); |
| for ( nIter = 0; nIter < 1000000; nIter++ ) |
| { |
| // find onset minterm |
| status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 ); |
| if ( status == l_Undef ) |
| break; |
| if ( status == l_False ) |
| break; |
| assert( status == l_True ); |
| nSols++; |
| // print solution |
| if ( nIter < 5 ) |
| Sbd_SolverTopoPrint( pSat, M, N, K, pVars ); |
| // remember variable values |
| Vec_IntClear( vLits ); |
| for ( v = 0; v < nVars; v++ ) |
| if ( sat_solver_var_value(pSat, v) ) |
| Vec_IntPush( vLits, Abc_Var2Lit(v, 1) ); |
| // add breaking clause |
| status = sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits) ); |
| if ( status == 0 ) |
| break; |
| //if ( nIter == 5 ) |
| // break; |
| } |
| sat_solver_delete( pSat ); |
| Vec_IntFree( vLits ); |
| printf( "Found %d solutions. ", nSols ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| } |
| |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Synthesize random topology.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| void Sbd_SolverSynth( int M, int N, int K, int pLuts[MAX_N][MAX_K] ) |
| { |
| int Used[MAX_M+MAX_N] = {0}; |
| int nUnused = M; |
| int n, iFan0, iFan1; |
| srand( time(NULL) ); |
| for ( n = 0; nUnused < N - n; n++ ) |
| { |
| iFan0 = iFan1 = 0; |
| while ( (iFan0 = rand() % (M + n)) == (iFan1 = rand() % (M + n)) ) |
| ; |
| pLuts[n][0] = iFan0; |
| pLuts[n][1] = iFan1; |
| if ( Used[iFan0] == 0 ) |
| { |
| Used[iFan0] = 1; |
| nUnused--; |
| } |
| if ( Used[iFan1] == 0 ) |
| { |
| Used[iFan1] = 1; |
| nUnused--; |
| } |
| nUnused++; |
| } |
| if ( nUnused == N - n ) |
| { |
| // undo the first one |
| for ( iFan0 = 0; iFan0 < M+n; iFan0++ ) |
| if ( Used[iFan0] ) |
| { |
| Used[iFan0] = 0; |
| nUnused++; |
| break; |
| } |
| |
| } |
| assert( nUnused == N - n + 1 ); |
| for ( ; n < N; n++ ) |
| { |
| for ( iFan0 = 0; iFan0 < M+n; iFan0++ ) |
| if ( Used[iFan0] == 0 ) |
| { |
| Used[iFan0] = 1; |
| break; |
| } |
| assert( iFan0 < M+n ); |
| for ( iFan1 = 0; iFan1 < M+n; iFan1++ ) |
| if ( Used[iFan1] == 0 ) |
| { |
| Used[iFan1] = 1; |
| break; |
| } |
| assert( iFan1 < M+n ); |
| pLuts[n][0] = iFan0; |
| pLuts[n][1] = iFan1; |
| } |
| |
| printf( "{\n" ); |
| for ( n = 0; n < N; n++ ) |
| printf( " {%d, %d}%s // %d\n", pLuts[n][0], pLuts[n][1], n==N-1 ? "" :",", M+n ); |
| printf( "};\n" ); |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [Compute truth table for the given parameter settings.] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| word Sbd_SolverTruth( int M, int N, int K, int pLuts[MAX_N][MAX_K], int pValues[MAX_N*((1<<MAX_K)-1)] ) |
| { |
| int i, k, v, nLutPars = (1 << K) - 1; |
| word Truths[MAX_M+MAX_N]; |
| assert( M <= 6 && N <= MAX_N ); |
| for ( i = 0; i < M; i++ ) |
| Truths[i] = s_Truths6[i]; |
| for ( i = 0; i < N; i++ ) |
| { |
| word Truth = 0, Mint; |
| for ( k = 1; k <= nLutPars; k++ ) |
| { |
| if ( !pValues[i*nLutPars+k-1] ) |
| continue; |
| Mint = ~(word)0; |
| for ( v = 0; v < K; v++ ) |
| Mint &= ((k >> v) & 1) ? Truths[pLuts[i][v]] : ~Truths[pLuts[i][v]]; |
| Truth |= Mint; |
| } |
| Truths[M+i] = Truth; |
| } |
| return Truths[M+N-1]; |
| } |
| word * Sbd_SolverTruthWord( int M, int N, int K, int pLuts[MAX_N][MAX_K], int pValues[MAX_N*((1<<MAX_K)-1)], word * pTruthsElem, int fCompl ) |
| { |
| int i, k, v, nLutPars = (1 << K) - 1; |
| int nWords = Abc_TtWordNum( M ); |
| word * pRes = pTruthsElem + (M+N-1)*nWords; |
| assert( M <= MAX_M && N <= MAX_N ); |
| for ( i = 0; i < N; i++ ) |
| { |
| word * pMint, * pTruth = pTruthsElem + (M+i)*nWords; |
| Abc_TtClear( pTruth, nWords ); |
| for ( k = 1; k <= nLutPars; k++ ) |
| { |
| if ( !pValues[i*nLutPars+k-1] ) |
| continue; |
| pMint = pTruthsElem + (M+N)*nWords; |
| Abc_TtFill( pMint, nWords ); |
| for ( v = 0; v < K; v++ ) |
| { |
| word * pFanin = pTruthsElem + pLuts[i][v]*nWords; |
| Abc_TtAndSharp( pMint, pMint, pFanin, nWords, ((k >> v) & 1) == 0 ); |
| } |
| Abc_TtOr( pTruth, pTruth, pMint, nWords ); |
| } |
| } |
| if ( fCompl ) |
| Abc_TtNot( pRes, nWords ); |
| return pRes; |
| } |
| |
| |
| /**Function************************************************************* |
| |
| Synopsis [] |
| |
| Description [] |
| |
| SideEffects [] |
| |
| SeeAlso [] |
| |
| ***********************************************************************/ |
| int Sbd_SolverFunc( int M, int N, int K, int pLuts[MAX_N][MAX_K], word * pTruthInit, int * pValues ) |
| { |
| int fVerbose = 0; |
| abctime clk = Abc_Clock(); |
| abctime clk2, clkOther = 0; |
| sat_solver * pSat = NULL; |
| int nWords = Abc_TtWordNum(M); |
| int pLits[MAX_K+2], pLits2[MAX_K+2], nLits; |
| int nLutPars = (1 << K) - 1, nVars = N * nLutPars; |
| int i, k, m, status, iMint, Iter, fCompl = (int)(pTruthInit[0] & 1); |
| // create truth tables |
| word * pTruthNew, * pTruths = ABC_ALLOC( word, Abc_TtWordNum(MAX_N) * (MAX_M + MAX_N + 1) ); |
| Abc_TtElemInit2( pTruths, M ); |
| // create solver |
| pSat = sat_solver_new(); |
| sat_solver_setnvars( pSat, nVars ); |
| printf( "Number of parameters %d x %d = %d.\n", N, nLutPars, nVars ); |
| // start with the last minterm |
| // iMint = (1 << M) - 1; |
| iMint = 1; |
| for ( Iter = 0; Iter < (1 << M); Iter++ ) |
| { |
| // assign the first intermediate variable |
| int nVarStart = sat_solver_nvars(pSat); |
| sat_solver_setnvars( pSat, nVarStart + N - 1 ); |
| // add clauses for nodes |
| //if ( fVerbose ) |
| printf( "Iter %3d : Mint = %3d. Conflicts =%8d.\n", Iter, iMint, sat_solver_nconflicts(pSat) ); |
| for ( i = 0; i < N; i++ ) |
| for ( m = 0; m <= nLutPars; m++ ) |
| { |
| if ( fVerbose ) |
| printf( "i = %d. m = %d.\n", i, m ); |
| // selector variables |
| nLits = 0; |
| for ( k = 0; k < K; k++ ) |
| { |
| if ( pLuts[i][k] >= M ) |
| { |
| assert( pLuts[i][k] - M < N - 1 ); |
| pLits[nLits] = pLits2[nLits] = Abc_Var2Lit( nVarStart + pLuts[i][k] - M, (m >> k) & 1 ); |
| nLits++; |
| } |
| else if ( ((iMint >> pLuts[i][k]) & 1) != ((m >> k) & 1) ) |
| break; |
| } |
| if ( k < K ) |
| continue; |
| // add parameter |
| if ( m ) |
| { |
| pLits[nLits] = Abc_Var2Lit( i*nLutPars + m-1, 1 ); |
| pLits2[nLits] = Abc_Var2Lit( i*nLutPars + m-1, 0 ); |
| nLits++; |
| } |
| // node variable |
| if ( i != N - 1 ) |
| { |
| pLits[nLits] = Abc_Var2Lit( nVarStart + i, 0 ); |
| pLits2[nLits] = Abc_Var2Lit( nVarStart + i, 1 ); |
| nLits++; |
| } |
| // add clauses |
| if ( i != N - 1 || Abc_TtGetBit(pTruthInit, iMint) != fCompl ) |
| { |
| status = sat_solver_addclause( pSat, pLits2, pLits2 + nLits ); |
| if ( status == 0 ) |
| { |
| fCompl = -1; |
| goto finish; |
| } |
| } |
| if ( (i != N - 1 || Abc_TtGetBit(pTruthInit, iMint) == fCompl) && m > 0 ) |
| { |
| status = sat_solver_addclause( pSat, pLits, pLits + nLits ); |
| if ( status == 0 ) |
| { |
| fCompl = -1; |
| goto finish; |
| } |
| } |
| } |
| |
| // run SAT solver |
| status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 ); |
| if ( status == l_Undef ) |
| break; |
| if ( status == l_False ) |
| { |
| fCompl = -1; |
| goto finish; |
| } |
| assert( status == l_True ); |
| |
| // collect values |
| for ( i = 0; i < nVars; i++ ) |
| pValues[i] = sat_solver_var_value(pSat, i); |
| |
| clk2 = Abc_Clock(); |
| pTruthNew = Sbd_SolverTruthWord( M, N, K, pLuts, pValues, pTruths, fCompl ); |
| clkOther += Abc_Clock() - clk2; |
| |
| if ( fVerbose ) |
| { |
| for ( i = 0; i < nVars; i++ ) |
| printf( "%d=%d ", i, pValues[i] ); |
| printf( " " ); |
| for ( i = nVars; i < sat_solver_nvars(pSat); i++ ) |
| printf( "%d=%d ", i, sat_solver_var_value(pSat, i) ); |
| printf( "\n" ); |
| Extra_PrintBinary( stdout, (unsigned *)pTruthInit, (1 << M) ); printf( "\n" ); |
| Extra_PrintBinary( stdout, (unsigned *)pTruthNew, (1 << M) ); printf( "\n" ); |
| } |
| if ( Abc_TtEqual(pTruthInit, pTruthNew, nWords) ) |
| break; |
| |
| // get new minterm |
| iMint = Abc_TtFindFirstDiffBit( pTruthInit, pTruthNew, M ); |
| } |
| finish: |
| printf( "Finished after %d iterations and %d conflicts. ", Iter, sat_solver_nconflicts(pSat) ); |
| sat_solver_delete( pSat ); |
| ABC_FREE( pTruths ); |
| Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); |
| Abc_PrintTime( 1, "Time", clkOther ); |
| return fCompl; |
| } |
| void Sbd_SolverFuncTest() |
| { |
| // int M = 4; // 6; // inputs |
| // int N = 3; // 16; // nodes |
| // int K = 2; // 2; // lutsize |
| // word Truth = ~((word)3 << 8); |
| // int pLuts[MAX_N][MAX_K] = { {0,1}, {2,3}, {4,5}, {6,7}, {8,9} }; |
| |
| /* |
| int M = 6; // 6; // inputs |
| int N = 19; // 16; // nodes |
| int K = 2; // 2; // lutsize |
| word pTruth[4] = { ABC_CONST(0x9ef7a8d9c7193a0f), 0, 0, 0 }; |
| int pLuts[MAX_N][MAX_K] = { |
| {3, 5}, {1, 6}, {0, 5}, {8, 2}, {7, 9}, |
| {0, 1}, {2, 11}, {5, 12}, {3, 13}, {1, 14}, |
| {10, 15}, {11, 2}, {3, 17}, {9, 18}, {0, 13}, |
| {20, 7}, {19, 21}, {4, 16}, {23, 22} |
| }; |
| */ |
| |
| /* |
| int M = 6; // 6; // inputs |
| int N = 5; // 16; // nodes |
| int K = 4; // 2; // lutsize |
| word Truth = ABC_CONST(0x9ef7a8d9c7193a0f); |
| int pLuts[MAX_N][MAX_K] = { |
| {0, 1, 2, 3}, // 6 |
| {1, 2, 3, 4}, // 7 |
| {2, 3, 4, 5}, // 8 |
| {0, 1, 4, 5}, // 9 |
| {6, 7, 8, 9} // 10 |
| }; |
| */ |
| |
| /* |
| int M = 8; // 6; // inputs |
| int N = 7; // 16; // nodes |
| int K = 2; // 2; // lutsize |
| // word pTruth[4] = { 0, 0, 0, ABC_CONST(0x8000000000000000) }; |
| // word pTruth[4] = { ABC_CONST(0x0000000000000001), 0, 0, 0 }; |
| word pTruth[4] = { 0, 0, 0, ABC_CONST(0x0000000000020000) }; |
| int pLuts[MAX_N][MAX_K] = { {0,1}, {2,3}, {4,5}, {6,7}, {8,9}, {10,11}, {12,13} }; |
| */ |
| |
| int M = 8; // 6; // inputs |
| int N = 7; // 16; // nodes |
| int K = 2; // 2; // lutsize |
| word pTruth[4] = { ABC_CONST(0x0000080000020000), ABC_CONST(0x0000000000020000), ABC_CONST(0x0000000000000000), ABC_CONST(0x0000000000020000) }; |
| int pLuts[MAX_N][MAX_K] = { {0,1}, {2,3}, {4,5}, {6,7}, {8,9}, {10,11}, {12,13} }; |
| |
| int pValues[MAX_N*((1<<MAX_K)-1)]; |
| int Res, i, k, nLutPars = (1 << K) - 1; |
| |
| //Sbd_SolverSynth( M, N, K, pLuts ); |
| |
| Res = Sbd_SolverFunc( M, N, K, pLuts, pTruth, pValues ); |
| if ( Res == -1 ) |
| { |
| printf( "Solution does not exist.\n" ); |
| return; |
| } |
| printf( "Result (compl = %d):\n", Res ); |
| for ( i = 0; i < N; i++ ) |
| { |
| for ( k = nLutPars-1; k >= 0; k-- ) |
| printf( "%d", pValues[i*nLutPars+k] ); |
| printf( "0\n" ); |
| } |
| } |
| |
| //////////////////////////////////////////////////////////////////////// |
| /// END OF FILE /// |
| //////////////////////////////////////////////////////////////////////// |
| |
| |
| ABC_NAMESPACE_IMPL_END |
| |
