/**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<= 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<> 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<> 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<= 0; k-- ) printf( "%d", pValues[i*nLutPars+k] ); printf( "0\n" ); } } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END