From 24083998ab2e6abdb0cacd90a8f45a01201aa7ce Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 4 Oct 2014 19:18:34 -0700 Subject: Deriving cell mapping with &if -kz. --- src/map/if/ifTune.c | 85 ++++++++++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 78 insertions(+), 7 deletions(-) (limited to 'src/map/if/ifTune.c') diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c index 6e48448b..defafcb4 100644 --- a/src/map/if/ifTune.c +++ b/src/map/if/ifTune.c @@ -58,8 +58,6 @@ static char * Ifn_Symbs[16] = { }; typedef struct Ifn_Obj_t_ Ifn_Obj_t; -typedef struct Ifn_Ntk_t_ Ifn_Ntk_t; - struct Ifn_Obj_t_ { unsigned Type : 3; // node type @@ -621,9 +619,10 @@ sat_solver * Ifn_ManSatBuild( Ifn_Ntk_t * p, Vec_Int_t ** pvPiVars, Vec_Int_t ** Gia_ManStop( p2 ); return pSat; } -void * If_ManSatBuildFromCell( char * pStr, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars, void ** ppNtk ) +void * If_ManSatBuildFromCell( char * pStr, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars, Ifn_Ntk_t ** ppNtk ) { Ifn_Ntk_t * p = Ifn_NtkParse( pStr ); + Ifn_Prepare( p, NULL, p->nInps ); *ppNtk = p; if ( p == NULL ) return NULL; @@ -651,7 +650,7 @@ void Ifn_ManSatPrintPerm( char * pPerms, int nVars ) } int Ifn_ManSatCheckOne( sat_solver * pSat, Vec_Int_t * vPoVars, word * pTruth, int nVars, int * pPerm, int nInps, Vec_Int_t * vLits ) { - int v, Value, m, mNew, nMints = (1 << nVars); + int v, Value, m, mNew, nMints = (1 << nVars); // (1 << nInps); assert( (1 << nInps) == Vec_IntSize(vPoVars) ); assert( nVars <= nInps ); // remap minterms @@ -685,7 +684,7 @@ void Ifn_ManSatDeriveOne( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vV Vec_IntForEachEntry( vPiVars, iVar, i ) Vec_IntPush( vValues, sat_solver_var_value(pSat, iVar) ); } -int Ifn_ManSatFindCofigBits( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, word * pTruth, int nVars, word Perm, int nInps, Vec_Int_t * vValues ) +int If_ManSatFindCofigBits( void * pSat, Vec_Int_t * vPiVars, Vec_Int_t * vPoVars, word * pTruth, int nVars, word Perm, int nInps, Vec_Int_t * vValues ) { // extract permutation int RetValue, i, pPerm[IF_MAX_FUNC_LUTSIZE]; @@ -696,7 +695,7 @@ int Ifn_ManSatFindCofigBits( sat_solver * pSat, Vec_Int_t * vPiVars, Vec_Int_t * assert( pPerm[i] < nVars ); } // perform SAT check - RetValue = Ifn_ManSatCheckOne( pSat, vPoVars, pTruth, nVars, pPerm, nInps, vValues ); + RetValue = Ifn_ManSatCheckOne( (sat_solver *)pSat, vPoVars, pTruth, nVars, pPerm, nInps, vValues ); Vec_IntClear( vValues ); if ( RetValue == 0 ) return 0; @@ -708,7 +707,7 @@ int Ifn_ManSatFindCofigBitsTest( Ifn_Ntk_t * p, word * pTruth, int nVars, word P Vec_Int_t * vValues = Vec_IntAlloc( 100 ); Vec_Int_t * vPiVars, * vPoVars; sat_solver * pSat = Ifn_ManSatBuild( p, &vPiVars, &vPoVars ); - int RetValue = Ifn_ManSatFindCofigBits( pSat, vPiVars, vPoVars, pTruth, nVars, Perm, p->nInps, vValues ); + int RetValue = If_ManSatFindCofigBits( pSat, vPiVars, vPoVars, pTruth, nVars, Perm, p->nInps, vValues ); Vec_IntPrint( vValues ); // cleanup sat_solver_delete( pSat ); @@ -718,6 +717,78 @@ int Ifn_ManSatFindCofigBitsTest( Ifn_Ntk_t * p, word * pTruth, int nVars, word P return RetValue; } +/**Function************************************************************* + + Synopsis [Derive GIA using programmable bits.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int If_ManSatDeriveGiaFromBits( void * pGia, Ifn_Ntk_t * p, Vec_Int_t * vValues, Vec_Int_t * vCover ) +{ + Gia_Man_t * pNew = (Gia_Man_t *)pGia; + int i, Id, k, iLit, iVar = 0, nVarsNew, pVarMap[1000]; + assert( Gia_ManCiNum(pNew) == p->nInps && p->nParsVIni < 1000 ); + Gia_ManForEachCiId( pNew, Id, i ) + pVarMap[i] = Abc_Var2Lit( Id, 0 ); + for ( i = p->nInps; i < p->nObjs; i++ ) + { + int Type = p->Nodes[i].Type; + int nFans = p->Nodes[i].nFanins; + int * pFans = p->Nodes[i].Fanins; + int iFanin = p->Nodes[i].iFirst; + assert( nFans <= 6 ); + if ( Type == IFN_DSD_AND ) + { + iLit = 1; + for ( k = 0; k < nFans; k++ ) + iLit = Gia_ManHashAnd( pNew, iLit, pVarMap[pFans[k]] ); + pVarMap[i] = iLit; + } + else if ( Type == IFN_DSD_XOR ) + { + iLit = 0; + for ( k = 0; k < nFans; k++ ) + iLit = Gia_ManHashXor( pNew, iLit, pVarMap[pFans[k]] ); + pVarMap[i] = iLit; + } + else if ( Type == IFN_DSD_MUX ) + { + assert( nFans == 3 ); + pVarMap[i] = Gia_ManHashMux( pNew, pVarMap[pFans[0]], pVarMap[pFans[1]], pVarMap[pFans[2]] ); + } + else if ( Type == IFN_DSD_PRIME ) + { + int pFaninLits[16]; + // collect truth table + word uTruth = 0; + int nMints = (1 << nFans); + for ( k = 0; k < nMints; k++ ) + if ( Vec_IntEntry( vValues, iVar++ ) ) + uTruth |= ((word)1 << k); + // collect function + for ( k = 0; k < nFans; k++ ) + pFaninLits[k] = pVarMap[pFans[k]]; + // implement the function + nVarsNew = Abc_TtMinBase( &uTruth, pFaninLits, nFans, 6 ); + if ( nVarsNew == 0 ) + pVarMap[i] = (int)(uTruth & 1); + else + { + extern int Kit_TruthToGia( Gia_Man_t * pMan, unsigned * pTruth, int nVars, Vec_Int_t * vMemory, Vec_Int_t * vLeaves, int fHash ); + Vec_Int_t Leaves = { nVarsNew, nVarsNew, pFaninLits }; + pVarMap[i] = Kit_TruthToGia( pNew, (unsigned *)uTruth, nVarsNew, vCover, &Leaves, 1 ); // hashing enabled!!! + } + } + else assert( 0 ); + } + assert( iVar == Vec_IntSize(vValues) ); + return pVarMap[p->nObjs - 1]; +} /**Function************************************************************* -- cgit v1.2.3