/**CFile**************************************************************** FileName [ifTune.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [FPGA mapping based on priority cuts.] Synopsis [Library tuning.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - November 21, 2006.] Revision [$Id: ifTune.c,v 1.00 2006/11/21 00:00:00 alanmi Exp $] ***********************************************************************/ #include "if.h" #include "aig/gia/giaAig.h" #include "sat/bsat/satStore.h" #include "sat/cnf/cnf.h" #include "misc/extra/extra.h" #include "bool/kit/kit.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// #define IFN_INS 11 #define IFN_WRD (IFN_INS > 6 ? 1 << (IFN_INS-6) : 1) #define IFN_PAR 1024 // network types typedef enum { IF_DSD_NONE = 0, // 0: unknown IF_DSD_CONST0, // 1: constant IF_DSD_VAR, // 2: variable IF_DSD_AND, // 3: AND IF_DSD_XOR, // 4: XOR IF_DSD_MUX, // 5: MUX IF_DSD_PRIME // 6: PRIME } If_DsdType_t; // object types static char * Ifn_Symbs[16] = { NULL, // 0: unknown "const", // 1: constant "var", // 2: variable "()", // 3: AND "[]", // 4: XOR "<>", // 5: MUX "{}" // 6: PRIME }; typedef struct Ift_Obj_t_ Ift_Obj_t; typedef struct Ift_Ntk_t_ Ift_Ntk_t; struct Ift_Obj_t_ { unsigned Type : 3; // node type unsigned nFanins : 5; // fanin counter unsigned iFirst : 8; // first parameter unsigned Var : 16; // current variable int Fanins[IFN_INS]; // fanin IDs }; struct Ift_Ntk_t_ { // cell structure int nInps; // inputs int nObjs; // objects Ift_Obj_t Nodes[2*IFN_INS]; // nodes // constraints int pConstr[IFN_INS]; // constraint pairs int nConstr; // number of pairs // user data int nVars; // variables int nWords; // truth table words int nParsVNum; // selection parameters per variable int nParsVIni; // first selection parameter int nPars; // total parameters word * pTruth; // user truth table // matching procedures int Values[IFN_PAR]; // variable values word pTtElems[IFN_INS*IFN_WRD]; // elementary truth tables word pTtObjs[2*IFN_INS*IFN_WRD]; // object truth tables }; static inline word * Ift_ElemTruth( Ift_Ntk_t * p, int i ) { return p->pTtElems + i * Abc_TtWordNum(p->nInps); } static inline word * Ift_ObjTruth( Ift_Ntk_t * p, int i ) { return p->pTtObjs + i * p->nWords; } // variable ordering // - primary inputs [0; p->nInps) // - internal nodes [p->nInps; p->nObjs) // - configuration params [p->nObjs; p->nParsVIni) // - variable selection params [p->nParsVIni; p->pPars) //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Prepare network to check the given function.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Ifn_Prepare( Ift_Ntk_t * p, word * pTruth, int nVars ) { int i, fVerbose = 0; assert( nVars <= p->nInps ); p->pTruth = pTruth; p->nVars = nVars; p->nWords = Abc_TtWordNum(nVars); p->nPars = p->nObjs; for ( i = p->nInps; i < p->nObjs; i++ ) { if ( p->Nodes[i].Type != IF_DSD_PRIME ) continue; p->Nodes[i].iFirst = p->nPars; p->nPars += (1 << p->Nodes[i].nFanins); if ( fVerbose ) printf( "Node %d Start %d Vars %d\n", i, p->Nodes[i].iFirst, (1 << p->Nodes[i].nFanins) ); } if ( fVerbose ) printf( "Groups start %d\n", p->nPars ); p->nParsVIni = p->nPars; p->nParsVNum = Abc_Base2Log(nVars); p->nPars += p->nParsVNum * p->nInps; assert( p->nPars <= IFN_PAR ); memset( p->Values, 0xFF, sizeof(int) * p->nPars ); return p->nPars; } void Ifn_NtkPrint( Ift_Ntk_t * p ) { int i, k; if ( p == NULL ) printf( "String is empty.\n" ); if ( p == NULL ) return; for ( i = p->nInps; i < p->nObjs; i++ ) { printf( "%c=", 'a'+i ); printf( "%c", Ifn_Symbs[p->Nodes[i].Type][0] ); for ( k = 0; k < (int)p->Nodes[i].nFanins; k++ ) printf( "%c", 'a'+p->Nodes[i].Fanins[k] ); printf( "%c", Ifn_Symbs[p->Nodes[i].Type][1] ); printf( ";" ); } printf( "\n" ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Ifn_ManStrCheck( char * pStr, int * pnInps, int * pnObjs ) { int i, Marks[32] = {0}, MaxVar = 0, MaxDef = 0, RetValue = 1; for ( i = 0; pStr[i]; i++ ) { if ( pStr[i] == '=' || pStr[i] == ';' || pStr[i] == '(' || pStr[i] == ')' || pStr[i] == '[' || pStr[i] == ']' || pStr[i] == '<' || pStr[i] == '>' || pStr[i] == '{' || pStr[i] == '}' ) continue; if ( pStr[i] >= 'a' && pStr[i] <= 'z' ) { if ( pStr[i+1] == '=' ) Marks[pStr[i] - 'a'] = 2, MaxDef = Abc_MaxInt(MaxDef, pStr[i] - 'a'); continue; } printf( "String \"%s\" contains unrecognized symbol (%c).\n", pStr, pStr[i] ); RetValue = 0; } if ( !RetValue ) return 0; for ( i = 0; pStr[i]; i++ ) { if ( pStr[i] == '=' || pStr[i] == ';' || pStr[i] == '(' || pStr[i] == ')' || pStr[i] == '[' || pStr[i] == ']' || pStr[i] == '<' || pStr[i] == '>' || pStr[i] == '{' || pStr[i] == '}' ) continue; if ( pStr[i] >= 'a' && pStr[i] <= 'z' ) { if ( pStr[i+1] != '=' && Marks[pStr[i] - 'a'] != 2 ) Marks[pStr[i] - 'a'] = 1, MaxVar = Abc_MaxInt(MaxVar, pStr[i] - 'a'); continue; } printf( "String \"%s\" contains unrecognized symbol (%c).\n", pStr, pStr[i] ); RetValue = 0; } if ( !RetValue ) return 0; MaxVar++; MaxDef++; for ( i = 0; i < MaxDef; i++ ) if ( Marks[i] == 0 ) printf( "String \"%s\" has no symbol (%c).\n", pStr, 'a' + i ), RetValue = 0; for ( i = 0; i < MaxVar; i++ ) if ( Marks[i] == 2 ) printf( "String \"%s\" has definition of input variable (%c).\n", pStr, 'a' + i ), RetValue = 0; for ( i = MaxVar; i < MaxDef; i++ ) if ( Marks[i] == 1 ) printf( "String \"%s\" has no definition for internal variable (%c).\n", pStr, 'a' + i ), RetValue = 0; if ( !RetValue ) return 0; *pnInps = MaxVar; *pnObjs = MaxDef; return 1; } Ift_Ntk_t * Ifn_ManStrParse( char * pStr ) { int i, k, n, f, nFans, iFan; static Ift_Ntk_t P, * p = &P; memset( p, 0, sizeof(Ift_Ntk_t) ); if ( !Ifn_ManStrCheck(pStr, &p->nInps, &p->nObjs) ) return NULL; if ( p->nInps > IFN_INS ) { printf( "The number of variables (%d) exceeds predefined limit (%d). Recompile with different value of IFN_INS.\n", p->nInps, IFN_INS ); return NULL; } assert( p->nInps > 1 && p->nInps < p->nObjs && p->nInps <= IFN_INS && p->nObjs < 2*IFN_INS ); for ( i = p->nInps; i < p->nObjs; i++ ) { char Next = 0; for ( k = 0; pStr[k]; k++ ) if ( pStr[k] == 'a' + i && pStr[k+1] == '=' ) break; if ( pStr[k] == 0 ) { printf( "Cannot find definition of signal %c.\n", 'a' + i ); return NULL; } if ( pStr[k+2] == '(' ) p->Nodes[i].Type = IF_DSD_AND, Next = ')'; else if ( pStr[k+2] == '[' ) p->Nodes[i].Type = IF_DSD_XOR, Next = ']'; else if ( pStr[k+2] == '<' ) p->Nodes[i].Type = IF_DSD_MUX, Next = '>'; else if ( pStr[k+2] == '{' ) p->Nodes[i].Type = IF_DSD_PRIME, Next = '}'; else { printf( "Cannot find openning operation symbol in the defition of of signal %c.\n", 'a' + i ); return NULL; } for ( n = k + 3; pStr[n]; n++ ) if ( pStr[n] == Next ) break; if ( pStr[n] == 0 ) { printf( "Cannot find closing operation symbol in the defition of of signal %c.\n", 'a' + i ); return NULL; } nFans = n - k - 3; if ( nFans < 1 || nFans > 8 ) { printf( "Cannot find matching operation symbol in the defition of of signal %c.\n", 'a' + i ); return NULL; } for ( f = 0; f < nFans; f++ ) { iFan = pStr[k + 3 + f] - 'a'; if ( iFan < 0 || iFan >= i ) { printf( "Fanin number %d is signal %d is out of range.\n", f, 'a' + i ); return NULL; } p->Nodes[i].Fanins[f] = iFan; } p->Nodes[i].nFanins = nFans; } // truth tables Abc_TtElemInit2( p->pTtElems, p->nInps ); /* // constraints p->nConstr = 5; p->pConstr[0] = (0 << 16) | 1; p->pConstr[1] = (2 << 16) | 3; p->pConstr[2] = (3 << 16) | 4; p->pConstr[3] = (6 << 16) | 7; p->pConstr[4] = (7 << 16) | 8; */ return p; } /**Function************************************************************* Synopsis [Derive truth table given the configulation values.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ word * Ift_NtkDeriveTruth( Ift_Ntk_t * p, int * pValues ) { int i, v, f, iVar, iStart; // elementary variables for ( i = 0; i < p->nInps; i++ ) { // find variable iStart = p->nParsVIni + i * p->nParsVNum; for ( v = iVar = 0; v < p->nParsVNum; v++ ) if ( p->Values[iStart+v] ) iVar += (1 << v); // assign variable Abc_TtCopy( Ift_ObjTruth(p, i), Ift_ElemTruth(p, iVar), p->nWords, 0 ); } // internal variables for ( i = p->nInps; i < p->nObjs; i++ ) { int nFans = p->Nodes[i].nFanins; int * pFans = p->Nodes[i].Fanins; word * pTruth = Ift_ObjTruth( p, i ); if ( p->Nodes[i].Type == IF_DSD_AND ) { Abc_TtFill( pTruth, p->nWords ); for ( f = 0; f < nFans; f++ ) Abc_TtAnd( pTruth, pTruth, Ift_ObjTruth(p, pFans[f]), p->nWords, 0 ); } else if ( p->Nodes[i].Type == IF_DSD_XOR ) { Abc_TtClear( pTruth, p->nWords ); for ( f = 0; f < nFans; f++ ) Abc_TtXor( pTruth, pTruth, Ift_ObjTruth(p, pFans[f]), p->nWords, 0 ); } else if ( p->Nodes[i].Type == IF_DSD_MUX ) { assert( nFans == 3 ); Abc_TtMux( pTruth, Ift_ObjTruth(p, pFans[0]), Ift_ObjTruth(p, pFans[1]), Ift_ObjTruth(p, pFans[2]), p->nWords ); } else if ( p->Nodes[i].Type == IF_DSD_PRIME ) { int nValues = (1 << nFans); word * pTemp = Ift_ObjTruth(p, p->nObjs); Abc_TtClear( pTruth, p->nWords ); for ( v = 0; v < nValues; v++ ) { if ( pValues[p->Nodes[i].iFirst + v] == 0 ) continue; Abc_TtFill( pTemp, p->nWords ); for ( f = 0; f < nFans; f++ ) if ( (v >> f) & 1 ) Abc_TtAnd( pTemp, pTemp, Ift_ObjTruth(p, pFans[f]), p->nWords, 0 ); else Abc_TtSharp( pTemp, pTemp, Ift_ObjTruth(p, pFans[f]), p->nWords ); Abc_TtOr( pTruth, pTruth, pTemp, p->nWords ); } } else assert( 0 ); //Dau_DsdPrintFromTruth( pTruth, p->nVars ); } return Ift_ObjTruth(p, p->nObjs-1); } /**Function************************************************************* Synopsis [Compute more or equal] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ift_TtComparisonConstr( word * pTruth, int nVars, int fMore, int fEqual ) { word Cond[4], Equa[4], Temp[4]; word s_TtElems[8][4] = { ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA), ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC), ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0), ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00), ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000), ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000), ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF), ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF) }; int i, nWords = Abc_TtWordNum(2*nVars); assert( nVars > 0 && nVars <= 4 ); Abc_TtClear( pTruth, nWords ); Abc_TtFill( Equa, nWords ); for ( i = nVars - 1; i >= 0; i-- ) { if ( fMore ) Abc_TtSharp( Cond, s_TtElems[2*i+1], s_TtElems[2*i+0], nWords ); else Abc_TtSharp( Cond, s_TtElems[2*i+0], s_TtElems[2*i+1], nWords ); Abc_TtAnd( Temp, Equa, Cond, nWords, 0 ); Abc_TtOr( pTruth, pTruth, Temp, nWords ); Abc_TtXor( Temp, s_TtElems[2*i+0], s_TtElems[2*i+1], nWords, 1 ); Abc_TtAnd( Equa, Equa, Temp, nWords, 0 ); } if ( fEqual ) Abc_TtNot( pTruth, nWords ); } /**Function************************************************************* Synopsis [Adds parameter constraints.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ift_AddClause( sat_solver * pSat, int * pBeg, int * pEnd ) { int fVerbose = 0; int RetValue = sat_solver_addclause( pSat, pBeg, pEnd ); if ( fVerbose ) { for ( ; pBeg < pEnd; pBeg++ ) printf( "%c%d ", Abc_LitIsCompl(*pBeg) ? '-':'+', Abc_Lit2Var(*pBeg) ); printf( "\n" ); } assert( RetValue ); } void Ift_NtkAddConstrOne( sat_solver * pSat, Vec_Int_t * vCover, int * pVars, int nVars ) { int k, c, Cube, Literal, nLits, pLits[IFN_INS]; Vec_IntForEachEntry( vCover, Cube, c ) { nLits = 0; for ( k = 0; k < nVars; k++ ) { Literal = 3 & (Cube >> (k << 1)); if ( Literal == 1 ) // '0' -> pos lit pLits[nLits++] = Abc_Var2Lit(pVars[k], 0); else if ( Literal == 2 ) // '1' -> neg lit pLits[nLits++] = Abc_Var2Lit(pVars[k], 1); else if ( Literal != 0 ) assert( 0 ); } Ift_AddClause( pSat, pLits, pLits + nLits ); } } void Ift_NtkAddConstraints( Ift_Ntk_t * p, sat_solver * pSat ) { int fAddConstr = 0; Vec_Int_t * vCover = Vec_IntAlloc( 0 ); word uTruth = Abc_Tt6Stretch( ~Abc_Tt6Mask(p->nVars), p->nParsVNum ); assert( p->nParsVNum <= 4 ); if ( uTruth ) { int i, k, pVars[IFN_INS]; int RetValue = Kit_TruthIsop( (unsigned *)&uTruth, p->nParsVNum, vCover, 0 ); assert( RetValue == 0 ); // Dau_DsdPrintFromTruth( &uTruth, p->nParsVNum ); // add capacity constraints for ( i = 0; i < p->nInps; i++ ) { for ( k = 0; k < p->nParsVNum; k++ ) pVars[k] = p->nParsVIni + i * p->nParsVNum + k; Ift_NtkAddConstrOne( pSat, vCover, pVars, p->nParsVNum ); } } // ordering constraints if ( fAddConstr && p->nConstr ) { word pTruth[4]; int i, k, RetValue, pVars[2*IFN_INS]; int fForceDiff = (p->nVars == p->nInps); Ift_TtComparisonConstr( pTruth, p->nParsVNum, fForceDiff, fForceDiff ); RetValue = Kit_TruthIsop( (unsigned *)pTruth, 2*p->nParsVNum, vCover, 0 ); assert( RetValue == 0 ); // Kit_TruthIsopPrintCover( vCover, 2*p->nParsVNum, 0 ); for ( i = 0; i < p->nConstr; i++ ) { int iVar1 = p->pConstr[i] >> 16; int iVar2 = p->pConstr[i] & 0xFFFF; for ( k = 0; k < p->nParsVNum; k++ ) { pVars[2*k+0] = p->nParsVIni + iVar1 * p->nParsVNum + k; pVars[2*k+1] = p->nParsVIni + iVar2 * p->nParsVNum + k; } Ift_NtkAddConstrOne( pSat, vCover, pVars, 2*p->nParsVNum ); // printf( "added constraint with %d clauses for %d and %d\n", Vec_IntSize(vCover), iVar1, iVar2 ); } } Vec_IntFree( vCover ); } /**Function************************************************************* Synopsis [Derive clauses given variable assignment.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Ift_NtkAddClauses( Ift_Ntk_t * p, int * pValues, sat_solver * pSat ) { int i, f, v, nLits, pLits[IFN_INS+2], pLits2[IFN_INS+2]; // assign new variables int nSatVars = sat_solver_nvars(pSat); for ( i = 0; i < p->nObjs-1; i++ ) p->Nodes[i].Var = nSatVars++; p->Nodes[p->nObjs-1].Var = -ABC_INFINITY; sat_solver_setnvars( pSat, nSatVars ); // verify variable values for ( i = 0; i < p->nVars; i++ ) assert( pValues[i] != -1 ); for ( i = p->nVars; i < p->nObjs-1; i++ ) assert( pValues[i] == -1 ); assert( pValues[p->nObjs-1] != -1 ); // internal variables //printf( "\n" ); for ( i = 0; i < p->nInps; i++ ) { int iParStart = p->nParsVIni + i * p->nParsVNum; for ( v = 0; v < p->nVars; v++ ) { // add output literal pLits[0] = Abc_Var2Lit( p->Nodes[i].Var, pValues[v]==0 ); // add clause literals for ( f = 0; f < p->nParsVNum; f++ ) pLits[f+1] = Abc_Var2Lit( iParStart + f, (v >> f) & 1 ); Ift_AddClause( pSat, pLits, pLits+p->nParsVNum+1 ); } } //printf( "\n" ); for ( i = p->nInps; i < p->nObjs; i++ ) { int nFans = p->Nodes[i].nFanins; int * pFans = p->Nodes[i].Fanins; if ( p->Nodes[i].Type == IF_DSD_AND ) { nLits = 0; pLits[nLits++] = Abc_Var2Lit( p->Nodes[i].Var, 0 ); for ( f = 0; f < nFans; f++ ) { pLits[nLits++] = Abc_Var2Lit( p->Nodes[pFans[f]].Var, 1 ); // add small clause pLits2[0] = Abc_Var2Lit( p->Nodes[i].Var, 1 ); pLits2[1] = Abc_Var2Lit( p->Nodes[pFans[f]].Var, 0 ); Ift_AddClause( pSat, pLits2, pLits2 + 2 ); } // add big clause Ift_AddClause( pSat, pLits, pLits + nLits ); } else if ( p->Nodes[i].Type == IF_DSD_XOR ) { assert( 0 ); } else if ( p->Nodes[i].Type == IF_DSD_MUX ) { assert( 0 ); } else if ( p->Nodes[i].Type == IF_DSD_PRIME ) { int nValues = (1 << nFans); int iParStart = p->Nodes[i].iFirst; for ( v = 0; v < nValues; v++ ) { nLits = 0; if ( pValues[i] == -1 ) { pLits[nLits] = Abc_Var2Lit( p->Nodes[i].Var, 0 ); pLits2[nLits] = Abc_Var2Lit( p->Nodes[i].Var, 1 ); nLits++; } for ( f = 0; f < nFans; f++, nLits++ ) pLits[nLits] = pLits2[nLits] = Abc_Var2Lit( p->Nodes[pFans[f]].Var, (v >> f) & 1 ); pLits[nLits] = Abc_Var2Lit( iParStart + v, 1 ); pLits2[nLits] = Abc_Var2Lit( iParStart + v, 0 ); nLits++; if ( pValues[i] != 0 ) Ift_AddClause( pSat, pLits2, pLits2 + nLits ); if ( pValues[i] != 1 ) Ift_AddClause( pSat, pLits, pLits + nLits ); } } else assert( 0 ); //printf( "\n" ); } return 1; } /**Function************************************************************* Synopsis [Returns the minterm number for which there is a mismatch.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ift_SatPrintStatus( sat_solver * p, int Iter, int status, int iMint, int Value, abctime clk ) { printf( "Iter = %5d ", Iter ); printf( "Mint = %5d ", iMint ); printf( "Value = %2d ", Value ); printf( "Var = %6d ", sat_solver_nvars(p) ); printf( "Cla = %6d ", sat_solver_nclauses(p) ); printf( "Conf = %6d ", sat_solver_nconflicts(p) ); if ( status == l_False ) printf( "status = unsat" ); else if ( status == l_True ) printf( "status = sat " ); else printf( "status = undec" ); Abc_PrintTime( 1, "", clk ); } void Ift_SatPrintConfig( Ift_Ntk_t * p, sat_solver * pSat ) { int v; for ( v = p->nObjs; v < p->nPars; v++ ) { if ( v >= p->nParsVIni && (v - p->nParsVIni) % p->nParsVNum == 0 ) printf( " %d=", (v - p->nParsVIni) / p->nParsVNum ); printf( "%d", sat_solver_var_value(pSat, v) ); } printf( "\n" ); } int Ift_NtkMatch( Ift_Ntk_t * p, word * pTruth, int nVars, int fVerbose ) { word * pTruth1; int RetValue = 0; int nIterMax = (1<nPars ); Ift_NtkAddConstraints( p, pSat ); if ( fVerbose ) Ift_SatPrintStatus( pSat, 0, l_True, -1, -1, Abc_Clock() - clk ); for ( i = 0; i < nIterMax; i++ ) { // get variable assignment for ( v = 0; v < p->nObjs; v++ ) p->Values[v] = v < p->nVars ? (iMint >> v) & 1 : -1; p->Values[p->nObjs-1] = Abc_TtGetBit( pTruth, iMint ); // derive clauses if ( !Ift_NtkAddClauses( p, p->Values, pSat ) ) break; // find assignment of parameters // clk2 = Abc_Clock(); status = sat_solver_solve( pSat, NULL, NULL, 0, 0, 0, 0 ); // clkSat += Abc_Clock() - clk2; if ( fVerbose ) Ift_SatPrintStatus( pSat, i+1, status, iMint, p->Values[p->nObjs-1], Abc_Clock() - clk ); if ( status == l_False ) break; assert( status == l_True ); // collect assignment for ( v = p->nObjs; v < p->nPars; v++ ) p->Values[v] = sat_solver_var_value(pSat, v); // find truth table // clk2 = Abc_Clock(); pTruth1 = Ift_NtkDeriveTruth( p, p->Values ); // clkTru += Abc_Clock() - clk2; Abc_TtXor( pTruth1, pTruth1, p->pTruth, p->nWords, 0 ); // find mismatch if present iMint = Abc_TtFindFirstBit( pTruth1, p->nVars ); if ( iMint == -1 ) { Ift_SatPrintConfig( p, pSat ); RetValue = 1; break; } } assert( i < nIterMax ); sat_solver_delete( pSat ); printf( "Matching = %d Iters = %d. ", RetValue, i ); // Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); // Abc_PrintTime( 1, "Sat", clkSat ); // Abc_PrintTime( 1, "Tru", clkTru ); return RetValue; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Ifn_NtkRead() { int RetValue; int nVars = 9; // int nVars = 8; // int nVars = 3; // word * pTruth = Dau_DsdToTruth( "(abcdefghi)", nVars ); word * pTruth = Dau_DsdToTruth( "1008{(1008{(ab)cde}f)ghi}", nVars ); // word * pTruth = Dau_DsdToTruth( "18{(1008{(ab)cde}f)gh}", nVars ); // word * pTruth = Dau_DsdToTruth( "1008{(1008{[ab]cde}f)ghi}", nVars ); // word * pTruth = Dau_DsdToTruth( "(abcd)", nVars ); // word * pTruth = Dau_DsdToTruth( "(abc)", nVars ); // char * pStr = "e={abc};f={ed};"; // char * pStr = "d={ab};e={cd};"; char * pStr = "j=(ab);k={jcde};l=(kf);m={lghi};"; // char * pStr = "i={abc};j={ide};k={ifg};l={jkh};"; // char * pStr = "h={abcde};i={abcdf};j=;"; // char * pStr = "g=;h=;i={fgh};"; Ift_Ntk_t * p = Ifn_ManStrParse( pStr ); Ifn_NtkPrint( p ); Dau_DsdPrintFromTruth( pTruth, nVars ); // get the given function RetValue = Ift_NtkMatch( p, pTruth, nVars, 1 ); } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END