From 024715ed09e59c2a6308955ae996a7678193d928 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 9 Mar 2014 19:49:03 -0700 Subject: Changes to LUT mappers. --- src/map/if/ifTune.c | 261 ++++++++++++++++++++++++++++++++++++++++++++++++---- 1 file changed, 243 insertions(+), 18 deletions(-) (limited to 'src/map/if/ifTune.c') diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c index 1893814e..223882b8 100644 --- a/src/map/if/ifTune.c +++ b/src/map/if/ifTune.c @@ -19,7 +19,10 @@ ***********************************************************************/ #include "if.h" -#include "sat/bsat/satSolver.h" +#include "aig/gia/giaAig.h" +#include "sat/bsat/satStore.h" +#include "sat/cnf/cnf.h" +#include "misc/extra/extra.h" ABC_NAMESPACE_IMPL_START @@ -67,30 +70,53 @@ int If_ManStrCheck( char * pStr, int * pnVars, int * pnObjs ) if ( pStr[i] >= 'a' && pStr[i] <= 'z' ) { if ( pStr[i+1] == '=' ) - Marks[pStr[i] - 'a'] = 2, MaxDef = 1 + Abc_MaxInt(MaxDef, pStr[i] - 'a'); - else - Marks[pStr[i] - 'a'] = 1, MaxVar = 1 + Abc_MaxInt(MaxVar, pStr[i] - 'a'); + 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' + Marks[i] ), RetValue = 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' + Marks[i] ), RetValue = 0; + 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' + Marks[i] ), RetValue = 0; - *pnVars = RetValue ? MaxVar : 0; - *pnObjs = RetValue ? MaxDef : 0; - return RetValue; + printf( "String \"%s\" has no definition for internal variable (%c).\n", pStr, 'a' + i ), RetValue = 0; + if ( !RetValue ) + return 0; + *pnVars = MaxVar; + *pnObjs = MaxDef; + return 1; } -int If_ManStrParse( char * pStr, int nVars, int nObjs, int * pTypes, int * pnFans, int ppFans[][6] ) +int If_ManStrParse( char * pStr, int nVars, int nObjs, int * pTypes, int * pnFans, int ppFans[][6], int * pFirsts, int * pnSatVars ) { - int i, k, n, f; + int i, k, n, f, nPars = nVars; char Next = 0; assert( nVars < nObjs ); for ( i = nVars; i < nObjs; i++ ) @@ -117,12 +143,104 @@ int If_ManStrParse( char * pStr, int nVars, int nObjs, int * pTypes, int * pnFan for ( f = 0; f < pnFans[i]; f++ ) { ppFans[i][f] = pStr[k + 3 + f] - 'a'; + assert( ppFans[i][k] < i ); if ( ppFans[i][f] < 0 || ppFans[i][f] >= nObjs ) printf( "Error!\n" ); } + if ( pTypes[i] != IF_DSD_PRIME ) + continue; + pFirsts[i] = nPars; + nPars += (1 << pnFans[i]); } + *pnSatVars = nPars; return 1; } +Gia_Man_t * If_ManStrFindModel( int nVars, int nObjs, int nSatVars, int * pTypes, int * pnFans, int ppFans[][6], int * pFirsts ) +{ + Gia_Man_t * pNew, * pTemp; + int * pVarsPar, * pVarsObj; + int i, k, n, Step, iLit, nMints, nPars = 0; + pNew = Gia_ManStart( 1000 ); + pNew->pName = Abc_UtilStrsav( "model" ); + Gia_ManHashStart( pNew ); + pVarsPar = ABC_ALLOC( int, nSatVars ); + pVarsObj = ABC_ALLOC( int, nObjs ); + for ( i = 0; i < nSatVars; i++ ) + pVarsPar[i] = Gia_ManAppendCi(pNew); + for ( i = 0; i < nVars; i++ ) + pVarsObj[i] = pVarsPar[nSatVars - nVars + i]; + for ( i = nVars; i < nObjs; i++ ) + { + if ( pTypes[i] == IF_DSD_AND ) + { + iLit = 1; + for ( k = 0; k < pnFans[i]; k++ ) + iLit = Gia_ManHashAnd( pNew, iLit, pVarsObj[ppFans[i][k]] ); + pVarsObj[i] = iLit; + } + else if ( pTypes[i] == IF_DSD_XOR ) + { + iLit = 0; + for ( k = 0; k < pnFans[i]; k++ ) + iLit = Gia_ManHashXor( pNew, iLit, pVarsObj[ppFans[i][k]] ); + pVarsObj[i] = iLit; + } + else if ( pTypes[i] == IF_DSD_MUX ) + { + assert( pnFans[i] == 3 ); + pVarsObj[i] = Gia_ManHashMux( pNew, pVarsObj[ppFans[i][0]], pVarsObj[ppFans[i][1]], pVarsObj[ppFans[i][2]] ); + } + else if ( pTypes[i] == IF_DSD_PRIME ) + { + int pVarsData[64]; + assert( pnFans[i] >= 1 && pnFans[i] <= 6 ); + nMints = (1 << pnFans[i]); + for ( k = 0; k < nMints; k++ ) + pVarsData[k] = pVarsPar[nPars++]; + for ( Step = 1, k = 0; k < pnFans[i]; k++, Step <<= 1 ) + for ( n = 0; n < nMints; n += Step << 1 ) + pVarsData[n] = Gia_ManHashMux( pNew, pVarsObj[ppFans[i][k]], pVarsData[n+Step], pVarsData[n] ); + assert( Step == nMints ); + pVarsObj[i] = pVarsData[0]; + } + else assert( 0 ); + } + assert( nPars + nVars == nSatVars ); + Gia_ManAppendCo( pNew, pVarsObj[nObjs-1] ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + ABC_FREE( pVarsPar ); + ABC_FREE( pVarsObj ); + assert( Gia_ManPiNum(pNew) == nSatVars ); + assert( Gia_ManPoNum(pNew) == 1 ); + return pNew; +} +Gia_Man_t * If_ManStrFindCofactors( int nPars, Gia_Man_t * p ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, m, nMints = 1 << (Gia_ManCiNum(p) - nPars); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + Gia_ManHashAlloc( pNew ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + if ( i < nPars ) + pObj->Value = Gia_ManAppendCi( pNew ); + for ( m = 0; m < nMints; m++ ) + { + Gia_ManForEachCi( p, pObj, i ) + if ( i >= nPars ) + pObj->Value = ((m >> (i - nPars)) & 1); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachPo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} /**Function************************************************************* @@ -135,23 +253,70 @@ int If_ManStrParse( char * pStr, int nVars, int nObjs, int * pTypes, int * pnFan SeeAlso [] ***********************************************************************/ -sat_solver * If_ManSatBuild( char * pStr ) +static inline Cnf_Dat_t * Cnf_DeriveGiaRemapped( Gia_Man_t * p ) +{ + Cnf_Dat_t * pCnf; + Aig_Man_t * pAig = Gia_ManToAigSimple( p ); + pAig->nRegs = 0; + pCnf = Cnf_Derive( pAig, Aig_ManCoNum(pAig) ); + Aig_ManStop( pAig ); + return pCnf; +} +sat_solver * If_ManStrFindSolver( Gia_Man_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars ) { - int nVars, nObjs; + sat_solver * pSat; + Gia_Obj_t * pObj; + Cnf_Dat_t * pCnf; + int i; + pCnf = Cnf_DeriveGiaRemapped( p ); + // start the SAT solver + pSat = sat_solver_new(); + sat_solver_setnvars( pSat, pCnf->nVars ); + // add timeframe clauses + for ( i = 0; i < pCnf->nClauses; i++ ) + if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) ) + assert( 0 ); + // inputs/outputs + *pvPiVars = Vec_IntAlloc( Gia_ManPiNum(p) ); + Gia_ManForEachCi( p, pObj, i ) + Vec_IntPush( *pvPiVars, pCnf->pVarNums[Gia_ObjId(p, pObj)] ); + *pvPoVars = Vec_IntAlloc( Gia_ManPoNum(p) ); + Gia_ManForEachCo( p, pObj, i ) + Vec_IntPush( *pvPoVars, pCnf->pVarNums[Gia_ObjId(p, pObj)] ); + Cnf_DataFree( pCnf ); + return pSat; +} + +sat_solver * If_ManSatBuild( char * pStr, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars ) +{ + int nVars, nObjs, nSatVars; int pTypes[32] = {0}; int pnFans[32] = {0}; int ppFans[32][6] = {{0}}; + int pFirsts[32] = {0}; + Gia_Man_t * p1, * p2; sat_solver * pSat = NULL; + *pvPiVars = *pvPoVars = NULL; if ( !If_ManStrCheck(pStr, &nVars, &nObjs) ) return NULL; - if ( !If_ManStrParse(pStr, nVars, nObjs, pTypes, pnFans, ppFans) ) + if ( !If_ManStrParse(pStr, nVars, nObjs, pTypes, pnFans, ppFans, pFirsts, &nSatVars) ) + return NULL; + p1 = If_ManStrFindModel(nVars, nObjs, nSatVars, pTypes, pnFans, ppFans, pFirsts); + if ( p1 == NULL ) return NULL; +// Gia_AigerWrite( p1, "satbuild.aig", 0, 0 ); + p2 = If_ManStrFindCofactors( nSatVars - nVars, p1 ); + Gia_ManStop( p1 ); + if ( p2 == NULL ) + return NULL; +// Gia_AigerWrite( p2, "satbuild2.aig", 0, 0 ); + pSat = If_ManStrFindSolver( p2, pvPiVars, pvPoVars ); + Gia_ManStop( p2 ); return pSat; } - /**Function************************************************************* - Synopsis [Test procedure.] + Synopsis [] Description [] @@ -160,8 +325,68 @@ sat_solver * If_ManSatBuild( char * pStr ) SeeAlso [] ***********************************************************************/ -void If_ManSatTest() +void If_ManSatPrintPerm( char * pPerms, int nVars ) { + int i; + for ( i = 0; i < nVars; i++ ) + printf( "%c", 'a' + pPerms[i] ); + printf( "\n" ); +} +int If_ManSatCheckOne( sat_solver * pSat, Vec_Int_t * vPoVars, word * pTruth, int nVars, int * pPerm, int nVarsAll, Vec_Int_t * vLits ) +{ + int v, Value, m, mNew, nMints = (1 << nVars); + assert( (1 << nVarsAll) == Vec_IntSize(vPoVars) ); + assert( nMints <= Vec_IntSize(vPoVars) ); + // remap minterms + Vec_IntFill( vLits, Vec_IntSize(vPoVars), -1 ); + for ( m = 0; m < nMints; m++ ) + { + mNew = 0; + for ( v = 0; v < nVarsAll; v++ ) + { + assert( pPerm[v] < nVars ); + if ( ((m >> pPerm[v]) & 1) ) + mNew |= (1 << v); + } + assert( Vec_IntEntry(vLits, mNew) == -1 ); + Vec_IntWriteEntry( vLits, mNew, Abc_TtGetBit(pTruth, m) ); + } + // find assumptions + v = 0; + Vec_IntForEachEntry( vLits, Value, m ) + if ( Value >= 0 ) + Vec_IntWriteEntry( vLits, v++, Abc_Var2Lit(Vec_IntEntry(vPoVars, m), !Value) ); + Vec_IntShrink( vLits, v ); + // run SAT solver + Value = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ); + return (int)(Value == l_True); +} +void If_ManSatDeriveOne( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vValues ) +{ + int i, iVar; + Vec_IntClear( vValues ); + Vec_IntForEachEntry( vPiVars, iVar, i ) + Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) ); +} +int If_ManSatCheckAll_int( sat_solver * pSat, Vec_Int_t * vPoVars, word * pTruth, int nVars, Vec_Int_t * vLits, char ** pPerms, int nPerms ) +{ + int pPerm[IF_MAX_FUNC_LUTSIZE]; + int p, i; + for ( p = 0; p < nPerms; p++ ) + { + for ( i = 0; i < nVars; i++ ) + pPerm[i] = (int)pPerms[p][i]; + if ( If_ManSatCheckOne(pSat, vPoVars, pTruth, nVars, pPerm, nVars, vLits) ) + return p; + } + return -1; +} +int If_ManSatCheckAll( sat_solver * pSat, Vec_Int_t * vPoVars, word * pTruth, int nVars, Vec_Int_t * vLits, char ** pPerms, int nPerms ) +{ + abctime clk = Abc_Clock(); + int RetValue = If_ManSatCheckAll_int( pSat, vPoVars, pTruth, nVars, vLits, pPerms, nPerms ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + return RetValue; } //////////////////////////////////////////////////////////////////////// -- cgit v1.2.3