From 56f783157abf00a7d3d9744a75fa1503ea698262 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sun, 8 Mar 2015 20:17:59 -0700 Subject: Support for representing programmable cell configuration data. --- src/map/if/if.h | 10 ++-- src/map/if/ifDsd.c | 134 ++++++++++++++++++++++++++++++++----------------- src/map/if/ifTune.c | 142 ++++++++++++++++++++++++++++++++++++++++++++++------ 3 files changed, 222 insertions(+), 64 deletions(-) (limited to 'src/map') diff --git a/src/map/if/if.h b/src/map/if/if.h index 6a47a52b..067ce0ad 100644 --- a/src/map/if/if.h +++ b/src/map/if/if.h @@ -559,12 +559,14 @@ extern char * If_DsdManFileName( If_DsdMan_t * p ); extern int If_DsdManVarNum( If_DsdMan_t * p ); extern int If_DsdManObjNum( If_DsdMan_t * p ); extern int If_DsdManLutSize( If_DsdMan_t * p ); +extern int If_DsdManTtBitNum( If_DsdMan_t * p ); +extern int If_DsdManPermBitNum( If_DsdMan_t * p ); extern void If_DsdManSetLutSize( If_DsdMan_t * p, int nLutSize ); extern int If_DsdManSuppSize( If_DsdMan_t * p, int iDsd ); extern int If_DsdManCheckDec( If_DsdMan_t * p, int iDsd ); extern int If_DsdManReadMark( If_DsdMan_t * p, int iDsd ); extern void If_DsdManSetNewAsUseless( If_DsdMan_t * p ); -extern word If_DsdManGetFuncPerm( If_DsdMan_t * p, int iDsd ); +extern word * If_DsdManGetFuncConfig( If_DsdMan_t * p, int iDsd ); extern char * If_DsdManGetCellStr( If_DsdMan_t * p ); extern unsigned If_DsdManCheckXY( If_DsdMan_t * p, int iDsd, int LutSize, int fDerive, unsigned uMaskNot, int fHighEffort, int fVerbose ); extern int If_CutDsdBalanceEval( If_Man_t * p, If_Cut_t * pCut, Vec_Int_t * vAig ); @@ -631,13 +633,15 @@ extern int If_CutComputeTruth( If_Man_t * p, If_Cut_t * pCut, If_Cut extern int If_CutComputeTruthPerm( If_Man_t * p, If_Cut_t * pCut, If_Cut_t * pCut0, If_Cut_t * pCut1, int fCompl0, int fCompl1 ); /*=== ifTune.c ===========================================================*/ extern Ifn_Ntk_t * Ifn_NtkParse( char * pStr ); -extern int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word * pPerm ); +extern int Ifn_NtkTtBits( char * pStr ); +extern int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word * pConfig ); extern void Ifn_NtkPrint( Ifn_Ntk_t * p ); extern int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p ); extern int Ifn_NtkInputNum( Ifn_Ntk_t * p ); extern void * If_ManSatBuildFromCell( char * pStr, Vec_Int_t ** pvPiVars, Vec_Int_t ** pvPoVars, Ifn_Ntk_t ** ppNtk ); extern 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 ); -extern int If_ManSatDeriveGiaFromBits( void * pNew, Ifn_Ntk_t * p, Vec_Int_t * vLeaves, Vec_Int_t * vValues ); +extern int If_ManSatDeriveGiaFromBits( void * pNew, Ifn_Ntk_t * p, word * pTtData, Vec_Int_t * vLeaves, Vec_Int_t * vValues ); +extern void * If_ManDeriveGiaFromCells( void * p ); /*=== ifUtil.c ============================================================*/ extern void If_ManCleanNodeCopy( If_Man_t * p ); extern void If_ManCleanCutData( If_Man_t * p ); diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c index 9b09ce95..cdc34b2a 100644 --- a/src/map/if/ifDsd.c +++ b/src/map/if/ifDsd.c @@ -44,6 +44,8 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#define DSD_VERSION "dsd1" + // network types typedef enum { IF_DSD_NONE = 0, // 0: unknown @@ -86,7 +88,9 @@ struct If_DsdMan_t_ Vec_Ptr_t * vTtDecs[IF_MAX_FUNC_LUTSIZE+1]; // truth table decompositions Vec_Wec_t * vIsops[IF_MAX_FUNC_LUTSIZE+1]; // ISOP for each function int * pSched[IF_MAX_FUNC_LUTSIZE]; // grey code schedules - Vec_Wrd_t * vPerms; // permutations + int nTtBits; // the number of truth table bits + int nConfigWords; // the number of words for config data per node + Vec_Wrd_t * vConfigs; // permutations Gia_Man_t * pTtGia; // GIA to represent truth tables Vec_Int_t * vCover; // temporary memory void * pSat; // SAT solver @@ -174,6 +178,14 @@ int If_DsdManLutSize( If_DsdMan_t * p ) { return p->LutSize; } +int If_DsdManTtBitNum( If_DsdMan_t * p ) +{ + return p->nTtBits; +} +int If_DsdManPermBitNum( If_DsdMan_t * p ) +{ + return (Abc_Base2Log(p->nVars + 1) + 1) * p->nVars; +} void If_DsdManSetLutSize( If_DsdMan_t * p, int nLutSize ) { p->LutSize = nLutSize; @@ -196,9 +208,9 @@ void If_DsdManSetNewAsUseless( If_DsdMan_t * p ) p->nObjsPrev = If_DsdManObjNum(p); p->fNewAsUseless = 1; } -word If_DsdManGetFuncPerm( If_DsdMan_t * p, int iDsd ) +word * If_DsdManGetFuncConfig( If_DsdMan_t * p, int iDsd ) { - return p->vPerms ? Vec_WrdEntry(p->vPerms, Abc_Lit2Var(iDsd)) : 0; + return p->vConfigs ? Vec_WrdEntryP(p->vConfigs, p->nConfigWords * Abc_Lit2Var(iDsd)) : NULL; } char * If_DsdManGetCellStr( If_DsdMan_t * p ) { @@ -259,6 +271,7 @@ If_DsdMan_t * If_DsdManAlloc( int nVars, int LutSize ) p->nBins = Abc_PrimeCudd( 100000 ); p->pBins = ABC_CALLOC( unsigned, p->nBins ); p->pMem = Mem_FlexStart(); + p->nConfigWords = 1; Vec_PtrGrow( &p->vObjs, 10000 ); Vec_IntGrow( &p->vNexts, 10000 ); Vec_IntGrow( &p->vTruths, 10000 ); @@ -338,7 +351,7 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose ) if ( p->vIsops[v] ) Vec_WecFree( p->vIsops[v] ); } - Vec_WrdFreeP( &p->vPerms ); + Vec_WrdFreeP( &p->vConfigs ); Vec_IntFreeP( &p->vTemp1 ); Vec_IntFreeP( &p->vTemp2 ); ABC_FREE( p->vObjs.pArray ); @@ -1033,7 +1046,6 @@ void If_DsdManSave( If_DsdMan_t * p, char * pFileName ) { If_DsdObj_t * pObj; Vec_Int_t * vSets; - char * pBuffer = "dsd0"; word * pTruth; int i, v, Num; FILE * pFile = fopen( pFileName ? pFileName : p->pStore, "wb" ); @@ -1042,7 +1054,7 @@ void If_DsdManSave( If_DsdMan_t * p, char * pFileName ) printf( "Writing DSD manager file \"%s\" has failed.\n", pFileName ? pFileName : p->pStore ); return; } - fwrite( pBuffer, 4, 1, pFile ); + fwrite( DSD_VERSION, 4, 1, pFile ); Num = p->nVars; fwrite( &Num, 4, 1, pFile ); Num = p->LutSize; @@ -1073,10 +1085,14 @@ void If_DsdManSave( If_DsdMan_t * p, char * pFileName ) fwrite( Vec_IntArray(vSets), sizeof(int)*Num, 1, pFile ); } } - Num = p->vPerms ? Vec_WrdSize(p->vPerms) : 0; + Num = p->nConfigWords; + fwrite( &Num, 4, 1, pFile ); + Num = p->nTtBits; + fwrite( &Num, 4, 1, pFile ); + Num = p->vConfigs ? Vec_WrdSize(p->vConfigs) : 0; fwrite( &Num, 4, 1, pFile ); if ( Num ) - fwrite( Vec_WrdArray(p->vPerms), sizeof(word)*Num, 1, pFile ); + fwrite( Vec_WrdArray(p->vConfigs), sizeof(word)*Num, 1, pFile ); Num = p->pCellStr ? strlen(p->pCellStr) : 0; fwrite( &Num, 4, 1, pFile ); if ( Num ) @@ -1099,7 +1115,7 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName ) return NULL; } RetValue = fread( pBuffer, 4, 1, pFile ); - if ( pBuffer[0] != 'd' && pBuffer[1] != 's' && pBuffer[2] != 'd' && pBuffer[3] != '0' ) + if ( strncmp(pBuffer, DSD_VERSION, strlen(DSD_VERSION)) ) { printf( "Unrecognized format of file \"%s\".\n", pFileName ); return NULL; @@ -1160,10 +1176,14 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName ) } ABC_FREE( pTruth ); RetValue = fread( &Num, 4, 1, pFile ); + p->nConfigWords = Num; + RetValue = fread( &Num, 4, 1, pFile ); + p->nTtBits = Num; + RetValue = fread( &Num, 4, 1, pFile ); if ( RetValue && Num ) { - p->vPerms = Vec_WrdStart( Num ); - RetValue = fread( Vec_WrdArray(p->vPerms), sizeof(word)*Num, 1, pFile ); + p->vConfigs = Vec_WrdStart( Num ); + RetValue = fread( Vec_WrdArray(p->vConfigs), sizeof(word)*Num, 1, pFile ); } RetValue = fread( &Num, 4, 1, pFile ); if ( RetValue && Num ) @@ -1190,14 +1210,16 @@ void If_DsdManMerge( If_DsdMan_t * p, If_DsdMan_t * pNew ) printf( "LUT size should be the same.\n" ); return; } + assert( p->nTtBits == pNew->nTtBits ); + assert( p->nConfigWords == pNew->nConfigWords ); if ( If_DsdManHasMarks(p) != If_DsdManHasMarks(pNew) ) printf( "Warning! Old manager has %smarks while new manager has %smarks.\n", If_DsdManHasMarks(p) ? "" : "no ", If_DsdManHasMarks(pNew) ? "" : "no " ); vMap = Vec_IntAlloc( Vec_PtrSize(&pNew->vObjs) ); Vec_IntPush( vMap, 0 ); Vec_IntPush( vMap, 1 ); - if ( p->vPerms && pNew->vPerms ) - Vec_WrdFillExtra( p->vPerms, Vec_PtrSize(&p->vObjs) + Vec_PtrSize(&pNew->vObjs), 0 ); + if ( p->vConfigs && pNew->vConfigs ) + Vec_WrdFillExtra( p->vConfigs, p->nConfigWords * (Vec_PtrSize(&p->vObjs) + Vec_PtrSize(&pNew->vObjs)), 0 ); If_DsdVecForEachNode( &pNew->vObjs, pObj, i ) { If_DsdObjForEachFaninLit( &pNew->vObjs, pObj, iFanin, k ) @@ -1205,14 +1227,19 @@ void If_DsdManMerge( If_DsdMan_t * p, If_DsdMan_t * pNew ) Id = If_DsdObjFindOrAdd( p, pObj->Type, pFanins, pObj->nFans, pObj->Type == IF_DSD_PRIME ? If_DsdObjTruth(pNew, pObj) : NULL ); if ( pObj->fMark ) If_DsdVecObjSetMark( &p->vObjs, Id ); - if ( p->vPerms && pNew->vPerms && i < Vec_WrdSize(pNew->vPerms) ) - Vec_WrdFillExtra( p->vPerms, Id, Vec_WrdEntry(pNew->vPerms, i) ); + if ( p->vConfigs && pNew->vConfigs && p->nConfigWords * i < Vec_WrdSize(pNew->vConfigs) ) + { + //Vec_WrdFillExtra( p->vConfigs, Id, Vec_WrdEntry(pNew->vConfigs, i) ); + word * pConfigNew = Vec_WrdEntryP(pNew->vConfigs, p->nConfigWords * i); + word * pConfigOld = Vec_WrdEntryP(p->vConfigs, p->nConfigWords * Id); + memcpy( pConfigOld, pConfigNew, sizeof(word) * p->nConfigWords ); + } Vec_IntPush( vMap, Id ); } assert( Vec_IntSize(vMap) == Vec_PtrSize(&pNew->vObjs) ); Vec_IntFree( vMap ); - if ( p->vPerms && pNew->vPerms ) - Vec_WrdShrink( p->vPerms, Vec_PtrSize(&p->vObjs) ); + if ( p->vConfigs && pNew->vConfigs ) + Vec_WrdShrink( p->vConfigs, p->nConfigWords * Vec_PtrSize(&p->vObjs) ); } void If_DsdManCleanOccur( If_DsdMan_t * p, int fVerbose ) { @@ -1226,7 +1253,7 @@ void If_DsdManCleanMarks( If_DsdMan_t * p, int fVerbose ) If_DsdObj_t * pObj; int i; ABC_FREE( p->pCellStr ); - Vec_WrdFreeP( &p->vPerms ); + Vec_WrdFreeP( &p->vConfigs ); If_DsdVecForEachObj( &p->vObjs, pObj, i ) pObj->fMark = 0; } @@ -1235,7 +1262,7 @@ void If_DsdManInvertMarks( If_DsdMan_t * p, int fVerbose ) If_DsdObj_t * pObj; int i; ABC_FREE( p->pCellStr ); - Vec_WrdFreeP( &p->vPerms ); + Vec_WrdFreeP( &p->vConfigs ); If_DsdVecForEachObj( &p->vObjs, pObj, i ) pObj->fMark = !pObj->fMark; } @@ -2440,7 +2467,7 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo int fVeryVerbose = 0; ProgressBar * pProgress = NULL; If_DsdObj_t * pObj; - word * pTruth, Perm; + word * pTruth, * pConfig; int i, nVars, Value, LutSize; abctime clk = Abc_Clock(); // parse the structure @@ -2458,6 +2485,8 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo if ( If_DsdManVarNum(p) < Ifn_NtkInputNum(pNtk) ) printf( "Warning: The support of DSD manager (%d) is less than the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) ); LutSize = Ifn_NtkLutSizeMax(pNtk); + p->nTtBits = Ifn_NtkTtBits( pStruct ); + p->nConfigWords = 1 + Abc_Bit6WordNum( p->nTtBits ); // print if ( fVerbose ) { @@ -2471,30 +2500,32 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo If_DsdVecForEachObj( &p->vObjs, pObj, i ) if ( i >= p->nObjsPrev ) pObj->fMark = 0; - if ( p->vPerms == NULL ) - p->vPerms = Vec_WrdStart( Vec_PtrSize(&p->vObjs) ); + if ( p->vConfigs == NULL ) + p->vConfigs = Vec_WrdStart( p->nConfigWords * Vec_PtrSize(&p->vObjs) ); else - Vec_WrdFillExtra( p->vPerms, Vec_PtrSize(&p->vObjs), 0 ); + Vec_WrdFillExtra( p->vConfigs, p->nConfigWords * Vec_PtrSize(&p->vObjs), 0 ); pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) ); If_DsdVecForEachObjStart( &p->vObjs, pObj, i, p->nObjsPrev ) { if ( (i & 0xFF) == 0 ) Extra_ProgressBarUpdate( pProgress, i, NULL ); nVars = If_DsdObjSuppSize(pObj); - if ( nVars <= LutSize ) - continue; + //if ( nVars <= LutSize ) + // continue; pTruth = If_DsdManComputeTruth( p, Abc_Var2Lit(i, 0), NULL ); if ( fVeryVerbose ) Dau_DsdPrintFromTruth( pTruth, nVars ); if ( fVerbose ) printf( "%6d : %2d ", i, nVars ); - Value = Ifn_NtkMatch( pNtk, pTruth, nVars, nConfls, fVerbose, fVeryVerbose, &Perm ); + pConfig = Vec_WrdEntryP( p->vConfigs, p->nConfigWords * i ); + Value = Ifn_NtkMatch( pNtk, pTruth, nVars, nConfls, fVerbose, fVeryVerbose, pConfig ); if ( fVeryVerbose ) printf( "\n" ); if ( Value == 0 ) + { If_DsdVecObjSetMark( &p->vObjs, i ); - else - Vec_WrdWriteEntry( p->vPerms, i, Perm ); + memset( pConfig, 0, sizeof(word) * p->nConfigWords ); + } } p->nObjsPrev = 0; p->LutSize = 0; @@ -2531,12 +2562,13 @@ typedef struct Ifn_ThData_t_ { Ifn_Ntk_t * pNtk; // network word pTruth[DAU_MAX_WORD]; + word pConfig[10]; // configuration data + int nConfigWords;// configuration data word count int nVars; // support int Id; // object int nConfls; // conflicts int Result; // result int Status; // state - word Perm; // permutation abctime clkUsed; // total runtime } Ifn_ThData_t; void * Ifn_WorkerThread( void * pArg ) @@ -2555,7 +2587,8 @@ void * Ifn_WorkerThread( void * pArg ) return NULL; } clk = Abc_Clock(); - pThData->Result = Ifn_NtkMatch( pThData->pNtk, pThData->pTruth, pThData->nVars, pThData->nConfls, 0, 0, &pThData->Perm ); + memset( pThData->pConfig, 0, sizeof(word) * pThData->nConfigWords ); + pThData->Result = Ifn_NtkMatch( pThData->pNtk, pThData->pTruth, pThData->nVars, pThData->nConfls, 0, 0, pThData->pConfig ); pThData->clkUsed += Abc_Clock() - clk; pThData->Status = 0; // printf( "Finished object %d\n", pThData->Id ); @@ -2597,6 +2630,9 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs, printf( "Warning: The support of DSD manager (%d) is less than the support of the structure (%d).\n", If_DsdManVarNum(p), Ifn_NtkInputNum(pNtk) ); // check the largest LUT LutSize = Ifn_NtkLutSizeMax(pNtk); + p->nTtBits = Ifn_NtkTtBits( pStruct ); + p->nConfigWords = 1 + Abc_Bit6WordNum( p->nTtBits ); + assert( p->nConfigWords <= 10 ); if ( fVerbose ) { printf( "Considering programmable cell: " ); @@ -2610,10 +2646,10 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs, If_DsdVecForEachObj( &p->vObjs, pObj, i ) if ( i >= p->nObjsPrev ) pObj->fMark = 0; - if ( p->vPerms == NULL ) - p->vPerms = Vec_WrdStart( Vec_PtrSize(&p->vObjs) ); + if ( p->vConfigs == NULL ) + p->vConfigs = Vec_WrdStart( p->nConfigWords * Vec_PtrSize(&p->vObjs) ); else - Vec_WrdFillExtra( p->vPerms, Vec_PtrSize(&p->vObjs), 0 ); + Vec_WrdFillExtra( p->vConfigs, p->nConfigWords * Vec_PtrSize(&p->vObjs), 0 ); pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) ); // perform concurrent solving @@ -2625,13 +2661,14 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs, // start the threads for ( i = 0; i < nProcs; i++ ) { - ThData[i].pNtk = Ifn_NtkParse( pStruct ); - ThData[i].nVars = -1; // support - ThData[i].Id = -1; // object - ThData[i].nConfls = nConfls; // conflicts - ThData[i].Result = -1; // result - ThData[i].Status = 0; // state - ThData[i].clkUsed = 0; // total runtime + ThData[i].pNtk = Ifn_NtkParse( pStruct ); + ThData[i].nVars = -1; // support + ThData[i].Id = -1; // object + ThData[i].nConfls = nConfls; // conflicts + ThData[i].Result = -1; // result + ThData[i].Status = 0; // state + ThData[i].clkUsed = 0; // total runtime + ThData[i].nConfigWords = p->nConfigWords; status = pthread_create( WorkerThread + i, NULL, Ifn_WorkerThread, (void *)(ThData + i) ); assert( status == 0 ); } // run the threads @@ -2649,7 +2686,10 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs, if ( ThData[i].Result == 0 ) If_DsdVecObjSetMark( &p->vObjs, ThData[i].Id ); else - Vec_WrdWriteEntry( p->vPerms, ThData[i].Id, ThData[i].Perm ); + { + word * pTtWords = Vec_WrdEntryP( p->vConfigs, p->nConfigWords * ThData[i].Id ); + memcpy( pTtWords, ThData[i].pConfig, sizeof(word) * p->nConfigWords ); + } ThData[i].Id = -1; ThData[i].Result = -1; } @@ -2659,8 +2699,8 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs, Extra_ProgressBarUpdate( pProgress, k, NULL ); pObj = If_DsdVecObj( &p->vObjs, k ); nVars = If_DsdObjSuppSize(pObj); - if ( nVars <= LutSize ) - continue; + //if ( nVars <= LutSize ) + // continue; clk = Abc_Clock(); If_DsdManComputeTruthPtr( p, Abc_Var2Lit(k, 0), NULL, ThData[i].pTruth ); clkUsed += Abc_Clock() - clk; @@ -2738,10 +2778,10 @@ void Id_DsdManTuneThresh( If_DsdMan_t * p, int fUnate, int fThresh, int fVerbose If_DsdVecForEachObj( &p->vObjs, pObj, i ) if ( i >= p->nObjsPrev ) pObj->fMark = 0; - if ( p->vPerms == NULL ) - p->vPerms = Vec_WrdStart( Vec_PtrSize(&p->vObjs) ); + if ( p->vConfigs == NULL ) + p->vConfigs = Vec_WrdStart( Vec_PtrSize(&p->vObjs) ); else - Vec_WrdFillExtra( p->vPerms, Vec_PtrSize(&p->vObjs), 0 ); + Vec_WrdFillExtra( p->vConfigs, Vec_PtrSize(&p->vObjs), 0 ); pProgress = Extra_ProgressBarStart( stdout, Vec_PtrSize(&p->vObjs) ); If_DsdVecForEachObjStart( &p->vObjs, pObj, i, p->nObjsPrev ) { @@ -2767,7 +2807,7 @@ void Id_DsdManTuneThresh( If_DsdMan_t * p, int fUnate, int fThresh, int fVerbose if ( Value ) If_DsdVecObjSetMark( &p->vObjs, i ); else - Vec_WrdWriteEntry( p->vPerms, i, Perm ); + Vec_WrdWriteEntry( p->vConfigs, i, Perm ); } p->nObjsPrev = 0; p->LutSize = 0; diff --git a/src/map/if/ifTune.c b/src/map/if/ifTune.c index 8b7e9d1c..a0e95eaa 100644 --- a/src/map/if/ifTune.c +++ b/src/map/if/ifTune.c @@ -95,7 +95,7 @@ static inline word * Ifn_ObjTruth( Ifn_Ntk_t * p, int i ) { return p->pTt // - primary inputs [0; p->nInps) // - internal nodes [p->nInps; p->nObjs) // - configuration params [p->nObjs; p->nParsVIni) -// - variable selection params [p->nParsVIni; p->pPars) +// - variable selection params [p->nParsVIni; p->nPars) //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -460,6 +460,16 @@ Ifn_Ntk_t * Ifn_NtkParse( char * pStr ) // printf( "Finished parsing: " ); Ifn_NtkPrint(p); return p; } +int Ifn_NtkTtBits( char * pStr ) +{ + int i, Counter = 0; + Ifn_Ntk_t * pNtk = Ifn_NtkParse( pStr ); + for ( i = pNtk->nInps; i < pNtk->nObjs; i++ ) + if ( pNtk->Nodes[i].Type == IFN_DSD_PRIME ) + Counter += (1 << pNtk->Nodes[i].nFanins); + ABC_FREE( pNtk ); + return Counter; +} @@ -728,13 +738,21 @@ int Ifn_ManSatFindCofigBitsTest( Ifn_Ntk_t * p, word * pTruth, int nVars, word P SeeAlso [] ***********************************************************************/ -int If_ManSatDeriveGiaFromBits( void * pGia, Ifn_Ntk_t * p, Vec_Int_t * vValues, Vec_Int_t * vCover ) +int If_ManSatDeriveGiaFromBits( Gia_Man_t * pNew, Ifn_Ntk_t * p, word * pConfigData, Vec_Int_t * vLeaves, 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 ); + int i, k, iLit, iVar = 0, nVarsNew, pVarMap[1000]; + int nTtBits = p->nParsVIni - p->nObjs; + int nPermBits = Abc_Base2Log(p->nInps + 1) + 1; + int fCompl = Abc_TtGetBit( pConfigData, nTtBits + nPermBits * p->nInps ); + assert( Vec_IntSize(vLeaves) <= p->nInps && p->nParsVIni < 1000 ); + for ( i = 0; i < p->nInps; i++ ) + { + for ( iLit = k = 0; k < nPermBits; k++ ) + if ( Abc_TtGetBit(pConfigData, nTtBits + i * nPermBits + k) ) + iLit |= (1 << k); + assert( Abc_Lit2Var(iLit) < Vec_IntSize(vLeaves) ); + pVarMap[i] = Abc_Lit2LitL( Vec_IntArray(vLeaves), iLit ); + } for ( i = p->nInps; i < p->nObjs; i++ ) { int Type = p->Nodes[i].Type; @@ -768,7 +786,7 @@ int If_ManSatDeriveGiaFromBits( void * pGia, Ifn_Ntk_t * p, Vec_Int_t * vValues, word uTruth = 0; int nMints = (1 << nFans); for ( k = 0; k < nMints; k++ ) - if ( Vec_IntEntry( vValues, iVar++ ) ) + if ( Abc_TtGetBit(pConfigData, iVar++) ) uTruth |= ((word)1 << k); uTruth = Abc_Tt6Stretch( uTruth, nFans ); // collect function @@ -787,8 +805,89 @@ int If_ManSatDeriveGiaFromBits( void * pGia, Ifn_Ntk_t * p, Vec_Int_t * vValues, } else assert( 0 ); } - assert( iVar == Vec_IntSize(vValues) ); - return pVarMap[p->nObjs - 1]; + assert( iVar == nTtBits ); + return Abc_LitNotCond( pVarMap[p->nObjs - 1], fCompl ); +} + +/**Function************************************************************* + + Synopsis [Derive GIA using programmable bits.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void * If_ManDeriveGiaFromCells( void * pGia ) +{ + Gia_Man_t * p = (Gia_Man_t *)pGia; + Gia_Man_t * pNew, * pTemp; + Vec_Int_t * vCover, * vLeaves; + Ifn_Ntk_t * pNtkCell; + Gia_Obj_t * pObj; + word * pConfigData; + //word * pTruth; + int k, i, iLut, iVar; + int nConfigInts, Count = 0; + assert( p->vConfigs != NULL ); + assert( p->pCellStr != NULL ); + assert( Gia_ManHasMapping(p) ); + // derive cell network + pNtkCell = Ifn_NtkParse( p->pCellStr ); + Ifn_Prepare( pNtkCell, NULL, pNtkCell->nInps ); + nConfigInts = Vec_IntEntry( p->vConfigs, 1 ); + // create new manager + pNew = Gia_ManStart( 6*Gia_ManObjNum(p)/5 + 100 ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + // map primary inputs + Gia_ManFillValue(p); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + // iterate through nodes used in the mapping + vLeaves = Vec_IntAlloc( 16 ); + vCover = Vec_IntAlloc( 1 << 16 ); + Gia_ManHashStart( pNew ); + //Gia_ObjComputeTruthTableStart( p, Gia_ManLutSizeMax(p) ); + Gia_ManForEachAnd( p, pObj, iLut ) + { + if ( Gia_ObjIsBuf(pObj) ) + { + pObj->Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) ); + continue; + } + if ( !Gia_ObjIsLut(p, iLut) ) + continue; + // collect leaves + //Vec_IntClear( vLeaves ); + //Gia_LutForEachFanin( p, iLut, iVar, k ) + // Vec_IntPush( vLeaves, iVar ); + //pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, iLut), vLeaves ); + // collect incoming literals + Vec_IntClear( vLeaves ); + Gia_LutForEachFanin( p, iLut, iVar, k ) + Vec_IntPush( vLeaves, Gia_ManObj(p, iVar)->Value ); + pConfigData = (word *)Vec_IntEntryP( p->vConfigs, 2 + nConfigInts * Count++ ); + Gia_ManObj(p, iLut)->Value = If_ManSatDeriveGiaFromBits( pNew, pNtkCell, pConfigData, vLeaves, vCover ); + } + assert( Vec_IntEntry(p->vConfigs, 0) == Count ); + assert( Vec_IntSize(p->vConfigs) == 2 + nConfigInts * Count ); + //Gia_ObjComputeTruthTableStop( p ); + Gia_ManForEachCo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManHashStop( pNew ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + Vec_IntFree( vLeaves ); + Vec_IntFree( vCover ); + ABC_FREE( pNtkCell ); + // perform cleanup + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; + } /**Function************************************************************* @@ -1196,6 +1295,21 @@ word Ifn_NtkMatchCollectPerm( Ifn_Ntk_t * p, sat_solver * pSat ) } return Perm; } +void Ifn_NtkMatchCollectConfig( Ifn_Ntk_t * p, sat_solver * pSat, word * pConfig ) +{ + int i, v, Mint; + assert( p->nParsVNum <= 4 ); + for ( i = 0; i < p->nInps; i++ ) + { + for ( Mint = v = 0; v < p->nParsVNum; v++ ) + if ( sat_solver_var_value(pSat, p->nParsVIni + i * p->nParsVNum + v) ) + Mint |= (1 << v); + Abc_TtSetHex( pConfig, i, Mint ); + } + for ( v = p->nObjs; v < p->nParsVIni; v++ ) + if ( sat_solver_var_value(pSat, v) ) + Abc_TtSetBit( pConfig + 1, v - p->nObjs ); +} void Ifn_NtkMatchPrintPerm( word Perm, int nInps ) { int i; @@ -1204,7 +1318,7 @@ void Ifn_NtkMatchPrintPerm( word Perm, int nInps ) printf( "%c", 'a' + Abc_TtGetHex(&Perm, i) ); printf( "\n" ); } -int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word * pPerm ) +int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVerbose, int fVeryVerbose, word * pConfig ) { word * pTruth1; int RetValue = 0; @@ -1218,7 +1332,7 @@ int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVer Ifn_NtkAddConstraints( p, pSat ); if ( fVeryVerbose ) Ifn_NtkMatchPrintStatus( pSat, 0, l_True, -1, -1, Abc_Clock() - clk ); - if ( pPerm ) *pPerm = 0; + if ( pConfig ) assert( *pConfig == 0 ); for ( i = 0; i < nIterMax; i++ ) { // get variable assignment @@ -1248,8 +1362,8 @@ int Ifn_NtkMatch( Ifn_Ntk_t * p, word * pTruth, int nVars, int nConfls, int fVer iMint = Abc_TtFindFirstBit( pTruth1, p->nVars ); if ( iMint == -1 ) { - if ( pPerm ) - *pPerm = Ifn_NtkMatchCollectPerm( p, pSat ); + if ( pConfig ) + Ifn_NtkMatchCollectConfig( p, pSat, pConfig ); /* if ( pPerm ) { -- cgit v1.2.3