diff options
Diffstat (limited to 'src/base')
-rw-r--r-- | src/base/abci/abc.c | 16 | ||||
-rw-r--r-- | src/base/abci/abcDar.c | 125 | ||||
-rw-r--r-- | src/base/abci/abcDsdRes.c | 367 | ||||
-rw-r--r-- | src/base/io/io.c | 15 |
4 files changed, 486 insertions, 37 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 36311596..d5bdd444 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -331,7 +331,10 @@ void Abc_Init( Abc_Frame_t * pAbc ) // Kit_TruthCountMintermsPrecomp(); // Kit_DsdPrecompute4Vars(); - Dar_LibStart(); + { + extern void Dar_LibStart(); + Dar_LibStart(); + } } /**Function************************************************************* @@ -347,7 +350,10 @@ void Abc_Init( Abc_Frame_t * pAbc ) ***********************************************************************/ void Abc_End() { - Dar_LibStop(); + { + extern void Dar_LibStop(); + Dar_LibStop(); + } Abc_NtkFraigStoreClean(); // Rwt_Man4ExplorePrint(); @@ -2915,7 +2921,7 @@ int Abc_CommandLutpack( Abc_Frame_t * pAbc, int argc, char ** argv ) memset( pPars, 0, sizeof(Lut_Par_t) ); pPars->nLutsMax = 4; // (N) the maximum number of LUTs in the structure pPars->nLutsOver = 3; // (Q) the maximum number of LUTs not in the MFFC - pPars->nVarsShared = 0; // (S) the maximum number of shared variables (crossbars) + pPars->nVarsShared = 3; // (S) the maximum number of shared variables (crossbars) pPars->nGrowthLevel = 1; pPars->fSatur = 1; pPars->fZeroCost = 0; @@ -5942,6 +5948,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) extern void Abc_NtkCompareSupports( Abc_Ntk_t * pNtk ); extern void Abc_NtkCompareCones( Abc_Ntk_t * pNtk ); extern Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk ); + extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ); pNtk = Abc_FrameReadNtk(pAbc); pOut = Abc_FrameReadOut(pAbc); @@ -6057,7 +6064,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) fprintf( pErr, "Network should be strashed. Command has failed.\n" ); return 1; } - pNtkRes = Abc_NtkDar( pNtk ); +// pNtkRes = Abc_NtkDar( pNtk ); + pNtkRes = Abc_NtkDarToCnf( pNtk, "any.cnf" ); if ( pNtkRes == NULL ) { fprintf( pErr, "Command has failed.\n" ); diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c index a936f9bf..c2988cbb 100644 --- a/src/base/abci/abcDar.c +++ b/src/base/abci/abcDar.c @@ -20,6 +20,7 @@ #include "abc.h" #include "dar.h" +#include "cnf.h" //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// @@ -317,6 +318,130 @@ Dar_CnfFree( pCnf ); } +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkConstructFromCnf( Abc_Ntk_t * pNtk, Cnf_Man_t * p, Vec_Ptr_t * vMapped ) +{ + Abc_Ntk_t * pNtkNew; + Abc_Obj_t * pNode, * pNodeNew; + Dar_Obj_t * pObj, * pLeaf; + Cnf_Cut_t * pCut; + Vec_Int_t * vCover; + unsigned uTruth; + int i, k, nDupGates; + // create the new network + pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP ); + // make the mapper point to the new network + Dar_ManConst1(p->pManAig)->pData = Abc_NtkCreateNodeConst1(pNtkNew); + Abc_NtkForEachCi( pNtk, pNode, i ) + Dar_ManPi(p->pManAig, i)->pData = pNode->pCopy; + // process the nodes in topological order + vCover = Vec_IntAlloc( 1 << 16 ); + Vec_PtrForEachEntry( vMapped, pObj, i ) + { + // create new node + pNodeNew = Abc_NtkCreateNode( pNtkNew ); + // add fanins according to the cut + pCut = pObj->pData; + Cnf_CutForEachLeaf( p->pManAig, pCut, pLeaf, k ) + Abc_ObjAddFanin( pNodeNew, pLeaf->pData ); + // add logic function + if ( pCut->nFanins < 5 ) + { + uTruth = 0xFFFF & *Cnf_CutTruth(pCut); + Cnf_SopConvertToVector( p->pSops[uTruth], p->pSopSizes[uTruth], vCover ); + pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, vCover ); + } + else + pNodeNew->pData = Abc_SopCreateFromIsop( pNtkNew->pManFunc, pCut->nFanins, pCut->vIsop[1] ); + // save the node + pObj->pData = pNodeNew; + } + Vec_IntFree( vCover ); + // add the CO drivers + Abc_NtkForEachCo( pNtk, pNode, i ) + { + pObj = Dar_ManPo(p->pManAig, i); + pNodeNew = Abc_ObjNotCond( Dar_ObjFanin0(pObj)->pData, Dar_ObjFaninC0(pObj) ); + Abc_ObjAddFanin( pNode->pCopy, pNodeNew ); + } + + // remove the constant node if not used + pNodeNew = (Abc_Obj_t *)Dar_ManConst1(p->pManAig)->pData; + if ( Abc_ObjFanoutNum(pNodeNew) == 0 ) + Abc_NtkDeleteObj( pNodeNew ); + // minimize the node +// Abc_NtkSweep( pNtkNew, 0 ); + // decouple the PO driver nodes to reduce the number of levels + nDupGates = Abc_NtkLogicMakeSimpleCos( pNtkNew, 1 ); +// if ( nDupGates && If_ManReadVerbose(pIfMan) ) +// printf( "Duplicated %d gates to decouple the CO drivers.\n", nDupGates ); + if ( !Abc_NtkCheck( pNtkNew ) ) + fprintf( stdout, "Abc_NtkConstructFromCnf(): Network check has failed.\n" ); + return pNtkNew; +} + +/**Function************************************************************* + + Synopsis [Gives the current ABC network to AIG manager for processing.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ) +{ + Abc_Ntk_t * pNtkNew = NULL; + Cnf_Man_t * pCnf; + Dar_Man_t * pMan; + Cnf_Dat_t * pData; + assert( Abc_NtkIsStrash(pNtk) ); + // convert to the AIG manager + pMan = Abc_NtkToDar( pNtk ); + if ( pMan == NULL ) + return NULL; + if ( !Dar_ManCheck( pMan ) ) + { + printf( "Abc_NtkDarToCnf: AIG check has failed.\n" ); + Dar_ManStop( pMan ); + return NULL; + } + // perform balance + Dar_ManPrintStats( pMan ); + + // derive CNF + pCnf = Cnf_ManStart(); + pData = Cnf_Derive( pCnf, pMan ); + + { + Vec_Ptr_t * vMapped; + vMapped = Cnf_ManScanMapping( pCnf, 1 ); + pNtkNew = Abc_NtkConstructFromCnf( pNtk, pCnf, vMapped ); + Vec_PtrFree( vMapped ); + } + + Dar_ManStop( pMan ); + Cnf_ManStop( pCnf ); + + // write CNF into a file +// Cnf_DataWriteIntoFile( pData, pFileName ); + Cnf_DataFree( pData ); + + return pNtkNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abci/abcDsdRes.c b/src/base/abci/abcDsdRes.c index 83e1c241..3aa71a15 100644 --- a/src/base/abci/abcDsdRes.c +++ b/src/base/abci/abcDsdRes.c @@ -69,6 +69,7 @@ struct Lut_Man_t_ Vec_Int_t * vCover; Vec_Vec_t * vLevels; // temporary variables + int fCofactoring; // working in the cofactoring mode int pRefs[LUT_SIZE_MAX]; // fanin reference counters int pCands[LUT_SIZE_MAX]; // internal nodes pointing only to the leaves // truth table representation @@ -106,6 +107,8 @@ static inline int If_IsComplement( If_Obj_t * p ) { return (int )(((un extern void Res_UpdateNetworkLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels ); +static If_Obj_t * Abc_LutIfManMapMulti( Lut_Man_t * p, unsigned * pTruth, int nLeaves, If_Obj_t ** ppLeaves ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -1003,62 +1006,81 @@ If_Obj_t * Abc_LutIfManMap_New_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit SeeAlso [] ***********************************************************************/ -/* int Abc_LutFindBestCofactoring( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, unsigned * pTruth, int nVars ) { - Kit_DsdNtk_t * pNtk0, * pNtk1, * pTemp; -// Kit_DsdObj_t * pRoot; - unsigned * pCofs2[2] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars) }; - unsigned i, * pTruth; - int MaxBlock - Verbose = 0; - int RetValue = 0; + Kit_DsdNtk_t * pNtk0, * pNtk1;//, * pTemp; + unsigned * pCofs2[3] = { pNtk->pMem, pNtk->pMem + Kit_TruthWordNum(pNtk->nVars), pNtk->pMem + 2 * Kit_TruthWordNum(pNtk->nVars) }; + int i, MaxBlock0, MaxBlock1, MaxBlockBest = 1000, VarBest = -1; + int fVerbose = 1; if ( fVerbose ) { - printf( "Function: " ); +// printf( "Function: " ); // Extra_PrintBinary( stdout, pTruth, (1 << nVars) ); - Extra_PrintHexadecimal( stdout, pTruth, nVars ); +// Extra_PrintHexadecimal( stdout, pTruth, nVars ); + printf( "\n" ); printf( "\n" ); + printf( "V =%2d: ", pNtk->nVars ); Kit_DsdPrint( stdout, pNtk ); } for ( i = 0; i < nVars; i++ ) { Kit_TruthCofactor0New( pCofs2[0], pTruth, nVars, i ); - pNtk0 = Kit_DsdDecompose( pCofs2[0], nVars ); - pNtk0 = Kit_DsdExpand( pTemp = pNtk0 ); - Kit_DsdNtkFree( pTemp ); + Kit_TruthCofactor1New( pCofs2[1], pTruth, nVars, i ); + Kit_TruthXor( pCofs2[2], pCofs2[0], pCofs2[1], nVars ); + pNtk0 = Kit_DsdDecompose( pCofs2[0], nVars ); + MaxBlock0 = Kit_DsdNonDsdSizeMax( pNtk0 ); +// pNtk0 = Kit_DsdExpand( pTemp = pNtk0 ); +// Kit_DsdNtkFree( pTemp ); if ( fVerbose ) { + printf( "Variable %2d: Diff = %6d.\n", i, Kit_TruthCountOnes(pCofs2[2], nVars) ); + printf( "Cof%d0: ", i ); Kit_DsdPrint( stdout, pNtk0 ); } - Kit_TruthCofactor1New( pCofs2[1], pTruth, nVars, i ); pNtk1 = Kit_DsdDecompose( pCofs2[1], nVars ); - pNtk1 = Kit_DsdExpand( pTemp = pNtk1 ); - Kit_DsdNtkFree( pTemp ); - + MaxBlock1 = Kit_DsdNonDsdSizeMax( pNtk1 ); +// pNtk1 = Kit_DsdExpand( pTemp = pNtk1 ); +// Kit_DsdNtkFree( pTemp ); if ( fVerbose ) { printf( "Cof%d1: ", i ); Kit_DsdPrint( stdout, pNtk1 ); } - if ( Kit_DsdCheckVar4Dec2( pNtk0, pNtk1 ) ) - RetValue = 1; + if ( fVerbose ) + { + printf( "MaxBlock0 = %2d. MaxBlock1 = %2d. ", MaxBlock0, MaxBlock1 ); + if ( MaxBlock0 < p->pPars->nLutSize && MaxBlock1 < p->pPars->nLutSize ) + printf( " feasible\n" ); + else + printf( "infeasible\n" ); + } + + if ( MaxBlock0 < p->pPars->nLutSize && MaxBlock1 < p->pPars->nLutSize ) + { + if ( MaxBlockBest > ABC_MAX(MaxBlock0, MaxBlock1) ) + { + MaxBlockBest = ABC_MAX(MaxBlock0, MaxBlock1); + VarBest = i; + } + } Kit_DsdNtkFree( pNtk0 ); Kit_DsdNtkFree( pNtk1 ); } if ( fVerbose ) + { + printf( "Best variable = %d.\n", VarBest ); printf( "\n" ); - - return RetValue; - + } + return VarBest; + } -*/ + /**Function************************************************************* Synopsis [Prepares the mapping manager.] @@ -1070,7 +1092,7 @@ int Abc_LutFindBestCofactoring( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, unsigned * p SeeAlso [] ***********************************************************************/ -If_Obj_t * Abc_LutIfManMap_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit ) +If_Obj_t * Abc_LutIfManMap_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit, If_Obj_t * pResult ) { Kit_Graph_t * pGraph; Kit_DsdObj_t * pObj; @@ -1092,8 +1114,8 @@ If_Obj_t * Abc_LutIfManMap_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit ) if ( pObj->Type == KIT_DSD_AND ) { assert( pObj->nFans == 2 ); - pFansNew[0] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[0] ); - pFansNew[1] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[1] ); + pFansNew[0] = pResult? pResult : Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[0], NULL ); + pFansNew[1] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[1], NULL ); if ( pFansNew[0] == NULL || pFansNew[1] == NULL ) return NULL; pObjNew = If_ManCreateAnd( p->pIfMan, If_Regular(pFansNew[0]), If_IsComplement(pFansNew[0]), If_Regular(pFansNew[1]), If_IsComplement(pFansNew[1]) ); @@ -1102,8 +1124,8 @@ If_Obj_t * Abc_LutIfManMap_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit ) if ( pObj->Type == KIT_DSD_XOR ) { assert( pObj->nFans == 2 ); - pFansNew[0] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[0] ); - pFansNew[1] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[1] ); + pFansNew[0] = pResult? pResult : Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[0], NULL ); + pFansNew[1] = Abc_LutIfManMap_rec( p, pNtk, pObj->pFans[1], NULL ); if ( pFansNew[0] == NULL || pFansNew[1] == NULL ) return NULL; fCompl ^= 1 ^ If_IsComplement(pFansNew[0]) ^ If_IsComplement(pFansNew[1]); @@ -1116,11 +1138,22 @@ If_Obj_t * Abc_LutIfManMap_rec( Lut_Man_t * p, Kit_DsdNtk_t * pNtk, int iLit ) // solve for the inputs Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i ) { - pFansNew[i] = Abc_LutIfManMap_rec( p, pNtk, iLitFanin ); + if ( i == 0 ) + pFansNew[i] = pResult? pResult : Abc_LutIfManMap_rec( p, pNtk, iLitFanin, NULL ); + else + pFansNew[i] = Abc_LutIfManMap_rec( p, pNtk, iLitFanin, NULL ); if ( pFansNew[i] == NULL ) return NULL; } + // find best cofactoring variable +// if ( pObj->nFans > 3 ) +// Kit_DsdCofactoring( Kit_DsdObjTruth(pObj), pObj->nFans, NULL, 4, 1 ); + if ( !p->fCofactoring && p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize ) +// return Abc_LutIfManMapMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew ); + Abc_LutIfManMapMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew ); + + // derive the factored form pGraph = Kit_TruthToGraph( Kit_DsdObjTruth(pObj), pObj->nFans, p->vCover ); if ( pGraph == NULL ) @@ -1194,7 +1227,7 @@ int Abc_LutCutUpdate( Lut_Man_t * p, Lut_Cut_t * pCut, Kit_DsdNtk_t * pNtk ) If_ManSetupCiCutSets( p->pIfMan ); // create the internal nodes // pDriver = Abc_LutIfManMap_New_rec( p, pNtk, pNtk->Root ); - pDriver = Abc_LutIfManMap_rec( p, pNtk, pNtk->Root ); + pDriver = Abc_LutIfManMap_rec( p, pNtk, pNtk->Root, NULL ); if ( pDriver == NULL ) return 0; // create the PO node @@ -1460,6 +1493,280 @@ int Abc_LutResynthesize( Abc_Ntk_t * pNtk, Lut_Par_t * pPars ) return 1; } + + + + + +/**Function************************************************************* + + Synopsis [Records variable order.] + + Description [Increaments Order[x][y] by 1 if x should be above y in the DSD.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_LutCreateVarOrder( Kit_DsdNtk_t * pNtk, char pTable[][16] ) +{ + Kit_DsdObj_t * pObj; + unsigned uSuppFanins, k; + int Above[16], Below[16]; + int nAbove, nBelow, iFaninLit, i, x, y; + // iterate through the nodes + Kit_DsdNtkForEachObj( pNtk, pObj, i ) + { + // collect fanin support of this node + nAbove = 0; + uSuppFanins = 0; + Kit_DsdObjForEachFanin( pNtk, pObj, iFaninLit, k ) + { + if ( Kit_DsdLitIsLeaf( pNtk, iFaninLit ) ) + Above[nAbove++] = Kit_DsdLit2Var(iFaninLit); + else + uSuppFanins |= Kit_DsdLitSupport( pNtk, iFaninLit ); + } + // find the below variables + nBelow = 0; + for ( y = 0; y < 16; y++ ) + if ( uSuppFanins & (1 << y) ) + Below[nBelow++] = y; + // create all pairs + for ( x = 0; x < nAbove; x++ ) + for ( y = 0; y < nBelow; y++ ) + pTable[Above[x]][Below[y]]++; + } +} + +/**Function************************************************************* + + Synopsis [Creates commmon variable order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Abc_LutCreateCommonOrder( char pTable[][16], int pOrder[], int nLeaves ) +{ + int Score[16] = {0}; + int i, y, x; + // compute scores for each leaf + for ( i = 0; i < nLeaves; i++ ) + { + for ( y = 0; y < nLeaves; y++ ) + Score[i] += pTable[i][y]; + for ( x = 0; x < nLeaves; x++ ) + Score[i] -= pTable[x][i]; + } +/* + printf( "Scores: " ); + for ( i = 0; i < nLeaves; i++ ) + printf( "%d ", Score[i] ); + printf( "\n" ); +*/ + // sort the scores + Extra_BubbleSort( pOrder, Score, nLeaves, 0 ); +/* + printf( "Scores: " ); + for ( i = 0; i < nLeaves; i++ ) + printf( "%d ", Score[pOrder[i]] ); + printf( "\n" ); +*/ +} + +/**Function************************************************************* + + Synopsis [Prepares the mapping manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_Obj_t * Abc_LutIfManMapMulti_rec( Lut_Man_t * p, Kit_DsdNtk_t ** ppNtks, int * piLits, int * piCofVar, int nCBars, If_Obj_t ** ppLeaves, int nLeaves, int * pOrder ) +{ + Kit_DsdObj_t * pObj; + If_Obj_t * pObjsNew[4][8], * pResPrev; + unsigned uSupps[8], uSuppFanin; + int piLitsNew[8], pDecision[8] = {0}; + int i, v, k, nSize = (1 << nCBars); + + // find which of the variables is highest in the order + + // go though non-trivial components + for ( i = 0; i < nSize; i++ ) + { + if ( piLits[i] == -1 ) + continue; + pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) ); + uSuppFanin = pObj? Kit_DsdLitSupport( ppNtks[i], pObj->pFans[0] ) : 0; + uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] ) & ~uSuppFanin; + } + // find the variable that appears the highest in the order + for ( v = 0; v < nLeaves; v++ ) + { + for ( i = 0; i < nSize; i++ ) + if ( uSupps[i] & (1 << pOrder[v]) ) + break; + } + assert( v < nLeaves ); + // pull out all components that have this variable + for ( i = 0; i < nSize; i++ ) + pDecision[i] = ( uSupps[i] & (1 << pOrder[v]) ); + + + // iterate over the nodes + for ( i = 0; i < nSize; i++ ) + { + pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) ); + if ( pDecision[i] ) + piLitsNew[i] = pObj->pFans[0]; + else + piLitsNew[i] = piLits[i]; + } + + // call again + pResPrev = Abc_LutIfManMapMulti_rec( p, ppNtks, piLitsNew, piCofVar, nCBars, ppLeaves, nLeaves, pOrder ); + + // create new set of nodes + for ( i = 0; i < nSize; i++ ) + { + if ( pDecision[i] ) + pObjsNew[nCBars][i] = Abc_LutIfManMap_rec( p, ppNtks[i], piLits[i], pResPrev ); + else + pObjsNew[nCBars][i] = pResPrev; + } + + // create MUX using these outputs + for ( k = nCBars; k > 0; k-- ) + { + nSize /= 2; + for ( i = 0; i < nSize; i++ ) + pObjsNew[k-1][i] = If_ManCreateMnux( p->pIfMan, pObjsNew[k][2*i+0], pObjsNew[k][2*i+1], ppLeaves[piCofVar[k-1]] ); + } + assert( nCBars == 1 && nSize == 1 ); + return If_NotCond( pObjsNew[0][0], nCBars & 1 ); +} + +/**Function************************************************************* + + Synopsis [Prepares the mapping manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_Obj_t * Abc_LutIfManMapMulti( Lut_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves ) +{ + If_Obj_t * pResult; + Kit_DsdNtk_t * ppNtks[8] = {0}, * pTemp; + int piCofVar[4], pOrder[16] = {0}, pPrios[16], pFreqs[16] = {0}, piLits[16]; + int i, k, nCBars, nSize, nMemSize; + unsigned * ppCofs[4][8], uSupport; + char pTable[16][16] = {0}; + int fVerbose = 1; + + // allocate storage for cofactors + nMemSize = Kit_TruthWordNum(nVars); + ppCofs[0][0] = ALLOC( unsigned, 32 * nMemSize ); + nSize = 0; + for ( i = 0; i < 4; i++ ) + for ( k = 0; k < 8; k++ ) + ppCofs[i][k] = ppCofs[0][0] + nMemSize * nSize++; + assert( nSize == 32 ); + + // find the best cofactoring variables + nCBars = Kit_DsdCofactoring( pTruth, nVars, piCofVar, p->pPars->nVarsShared, 0 ); + + // copy the function + Kit_TruthCopy( ppCofs[0][0], pTruth, nVars ); + + // decompose w.r.t. these variables + for ( k = 0; k < nCBars; k++ ) + { + nSize = (1 << k); + for ( i = 0; i < nSize; i++ ) + { + Kit_TruthCofactor0New( ppCofs[k+1][2*i+0], ppCofs[k][i], nVars, piCofVar[k] ); + Kit_TruthCofactor1New( ppCofs[k+1][2*i+1], ppCofs[k][i], nVars, piCofVar[k] ); + } + } + nSize = (1 << nCBars); + // compute variable frequences + for ( i = 0; i < nSize; i++ ) + { + uSupport = Kit_TruthSupport( ppCofs[nCBars][i], nVars ); + for ( k = 0; k < nVars; k++ ) + if ( uSupport & (1<<k) ) + pFreqs[k]++; + } + // compute DSD networks + for ( i = 0; i < nSize; i++ ) + { + ppNtks[i] = Kit_DsdDecompose( ppCofs[nCBars][i], nVars ); + ppNtks[i] = Kit_DsdExpand( pTemp = ppNtks[i] ); + Kit_DsdNtkFree( pTemp ); + if ( fVerbose ) + { + printf( "Cof%d%d: ", nCBars, i ); + Kit_DsdPrint( stdout, ppNtks[i] ); + } + } + free( ppCofs[0][0] ); + + // find common variable order + for ( i = 0; i < nSize; i++ ) + { + Kit_DsdGetSupports( ppNtks[i] ); + Abc_LutCreateVarOrder( ppNtks[i], pTable ); + } + Abc_LutCreateCommonOrder( pTable, pOrder, nVars ); + + printf( "Common variable order: " ); + for ( i = 0; i < nVars; i++ ) + printf( "%c ", 'a' + pOrder[i] ); + printf( "\n" ); + + // derive variable priority + for ( i = 0; i < 16; i++ ) + pPrios[i] = 16; + for ( i = 0; i < nVars; i++ ) + pPrios[pOrder[i]] = i; + + // transform all networks according to the variable order + for ( i = 0; i < nSize; i++ ) + { + ppNtks[i] = Kit_DsdShrink( pTemp = ppNtks[i], pPrios ); + Kit_DsdNtkFree( pTemp ); + Kit_DsdGetSupports( ppNtks[i] ); + // undec nodes should be rotated in such a way that the first input has as many shared inputs as possible + Kit_DsdRotate( ppNtks[i], pFreqs ); + // collect the roots + piLits[i] = ppNtks[i]->Root; + } +/* + p->fCofactoring = 1; + pResult = Abc_LutIfManMapMulti_rec( p, ppNtks[nCBars], piLits, piCofVar, nCBars, ppLeaves, nVars, pOrder ); + p->fCofactoring = 0; +*/ + // free the networks + for ( i = 0; i < 8; i++ ) + if ( ppNtks[i] ) + Kit_DsdNtkFree( ppNtks[i] ); + + return pResult; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/io/io.c b/src/base/io/io.c index 09d1a8a5..e1d4de97 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -1414,13 +1414,19 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv ) char * pFileName; int c; int fAllPrimes; + int fNewAlgo; + extern Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName ); + fNewAlgo = 1; fAllPrimes = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "ph" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "nph" ) ) != EOF ) { switch ( c ) { + case 'n': + fNewAlgo ^= 1; + break; case 'p': fAllPrimes ^= 1; break; @@ -1441,15 +1447,18 @@ int IoCommandWriteCnf( Abc_Frame_t * pAbc, int argc, char **argv ) printf( "Warning: Selected option to write all primes has no effect when deriving CNF from AIG.\n" ); } // call the corresponding file writer - if ( fAllPrimes ) + if ( fNewAlgo ) + Abc_NtkDarToCnf( pAbc->pNtkCur, pFileName ); + else if ( fAllPrimes ) Io_WriteCnf( pAbc->pNtkCur, pFileName, 1 ); else Io_Write( pAbc->pNtkCur, pFileName, IO_FILE_CNF ); return 0; usage: - fprintf( pAbc->Err, "usage: write_cnf [-ph] <file>\n" ); + fprintf( pAbc->Err, "usage: write_cnf [-nph] <file>\n" ); fprintf( pAbc->Err, "\t write the miter cone into a CNF file\n" ); + fprintf( pAbc->Err, "\t-n : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes" : "no" ); fprintf( pAbc->Err, "\t-p : toggle using all primes to enhance implicativity [default = %s]\n", fAllPrimes? "yes" : "no" ); fprintf( pAbc->Err, "\t-h : print the help massage\n" ); fprintf( pAbc->Err, "\tfile : the name of the file to write\n" ); |