diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-10-04 19:18:34 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-10-04 19:18:34 -0700 |
commit | 24083998ab2e6abdb0cacd90a8f45a01201aa7ce (patch) | |
tree | 5afd80e046fbb2391ebe5502863378a15e66f202 /src/map/if/ifDsd.c | |
parent | 4c7165a4f75a647dd61c5f09f51131d8ed99924d (diff) | |
download | abc-24083998ab2e6abdb0cacd90a8f45a01201aa7ce.tar.gz abc-24083998ab2e6abdb0cacd90a8f45a01201aa7ce.tar.bz2 abc-24083998ab2e6abdb0cacd90a8f45a01201aa7ce.zip |
Deriving cell mapping with &if -kz.
Diffstat (limited to 'src/map/if/ifDsd.c')
-rw-r--r-- | src/map/if/ifDsd.c | 44 |
1 files changed, 37 insertions, 7 deletions
diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c index c4cd2a3c..c71df9e7 100644 --- a/src/map/if/ifDsd.c +++ b/src/map/if/ifDsd.c @@ -90,6 +90,7 @@ struct If_DsdMan_t_ Gia_Man_t * pTtGia; // GIA to represent truth tables Vec_Int_t * vCover; // temporary memory void * pSat; // SAT solver + char * pCellStr; // symbolic cell description int nObjsPrev; // previous number of objects int fNewAsUseless; // set new as useless int nUniqueHits; // statistics @@ -195,6 +196,14 @@ void If_DsdManSetNewAsUseless( If_DsdMan_t * p ) p->nObjsPrev = If_DsdManObjNum(p); p->fNewAsUseless = 1; } +word If_DsdManGetFuncPerm( If_DsdMan_t * p, int iDsd ) +{ + return p->vPerms ? Vec_WrdEntry(p->vPerms, Abc_Lit2Var(iDsd)) : 0; +} +char * If_DsdManGetCellStr( If_DsdMan_t * p ) +{ + return p->pCellStr; +} /**Function************************************************************* @@ -339,6 +348,7 @@ void If_DsdManFree( If_DsdMan_t * p, int fVerbose ) Gia_ManStopP( &p->pTtGia ); Vec_IntFreeP( &p->vCover ); If_ManSatUnbuild( p->pSat ); + ABC_FREE( p->pCellStr ); ABC_FREE( p->pStore ); ABC_FREE( p->pBins ); ABC_FREE( p ); @@ -720,6 +730,8 @@ void If_DsdManPrint( If_DsdMan_t * p, char * pFileName, int Number, int Support, If_DsdManPrintDistrib( p ); printf( "Number of inputs = %d. LUT size = %d. Marks = %s. NewAsUseless = %s. Bookmark = %d.\n", p->nVars, p->LutSize, If_DsdManHasMarks(p)? "yes" : "no", p->fNewAsUseless? "yes" : "no", p->nObjsPrev ); + if ( p->pCellStr ) + printf( "Symbolic cell description: %s\n", p->pCellStr ); if ( p->pTtGia ) fprintf( pFile, "Non-DSD AIG nodes = %8d\n", Gia_ManAndNum(p->pTtGia) ); fprintf( pFile, "Unique table misses = %8d\n", p->nUniqueMisses ); @@ -1061,6 +1073,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; + fwrite( &Num, 4, 1, pFile ); + if ( Num ) + fwrite( Vec_WrdArray(p->vPerms), sizeof(word)*Num, 1, pFile ); + Num = p->pCellStr ? strlen(p->pCellStr) : 0; + fwrite( &Num, 4, 1, pFile ); + if ( Num ) + fwrite( p->pCellStr, sizeof(char)*Num, 1, pFile ); fclose( pFile ); } If_DsdMan_t * If_DsdManLoad( char * pFileName ) @@ -1139,6 +1159,18 @@ If_DsdMan_t * If_DsdManLoad( char * pFileName ) assert( Num2 == Vec_PtrSize(p->vTtDecs[v]) ); } ABC_FREE( pTruth ); + RetValue = fread( &Num, 4, 1, pFile ); + if ( Num ) + { + p->vPerms = Vec_WrdStart( Num ); + RetValue = fread( Vec_WrdArray(p->vPerms), sizeof(word)*Num, 1, pFile ); + } + RetValue = fread( &Num, 4, 1, pFile ); + if ( Num ) + { + p->pCellStr = ABC_CALLOC( char, Num + 1 ); + RetValue = fread( p->pCellStr, sizeof(char)*Num, 1, pFile ); + } fclose( pFile ); return p; } @@ -1187,6 +1219,7 @@ void If_DsdManCleanMarks( If_DsdMan_t * p, int fVerbose ) { If_DsdObj_t * pObj; int i; + ABC_FREE( p->pCellStr ); If_DsdVecForEachObj( &p->vObjs, pObj, i ) pObj->fMark = 0; } @@ -2371,13 +2404,6 @@ void If_DsdManTune( If_DsdMan_t * p, int LutSize, int fFast, int fAdd, int fSpec } -typedef struct Ifn_Ntk_t_ Ifn_Ntk_t; - -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 void Ifn_NtkPrint( Ifn_Ntk_t * p ); -extern int Ifn_NtkLutSizeMax( Ifn_Ntk_t * p ); -extern int Ifn_NtkInputNum( Ifn_Ntk_t * p ); /**Function************************************************************* @@ -2408,6 +2434,8 @@ void Id_DsdManTuneStr1( If_DsdMan_t * p, char * pStruct, int nConfls, int fVerbo ABC_FREE( pNtk ); return; } + ABC_FREE( p->pCellStr ); + p->pCellStr = Abc_UtilStrsav( pStruct ); 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); @@ -2544,6 +2572,8 @@ void Id_DsdManTuneStr( If_DsdMan_t * p, char * pStruct, int nConfls, int nProcs, ABC_FREE( pNtk ); return; } + ABC_FREE( p->pCellStr ); + p->pCellStr = Abc_UtilStrsav( pStruct ); 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) ); // check the largest LUT |