/**CFile**************************************************************** FileName [lpkMux.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [Fast Boolean matching for LUT structures.] Synopsis [] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - April 28, 2007.] Revision [$Id: lpkMux.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] ***********************************************************************/ #include "lpkInt.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Find the best cofactoring variable.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Lpk_MapTreeBestCofVar( Lpk_Man_t * p, unsigned * pTruth, int nVars, unsigned * pCof0, unsigned * pCof1 ) { int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin; // iterate through variables iBestVar = -1; nSuppSizeMin = KIT_INFINITY; for ( i = 0; i < nVars; i++ ) { // cofactor the functiona and get support sizes Kit_TruthCofactor0New( pCof0, pTruth, nVars, i ); Kit_TruthCofactor1New( pCof1, pTruth, nVars, i ); nSuppSizeCur0 = Kit_TruthSupportSize( pCof0, nVars ); nSuppSizeCur1 = Kit_TruthSupportSize( pCof1, nVars ); nSuppSizeCur = nSuppSizeCur0 + nSuppSizeCur1; // skip cofactoring that goes above the limit if ( nSuppSizeCur0 > p->pPars->nLutSize || nSuppSizeCur1 > p->pPars->nLutSize ) continue; // compare this variable with other variables if ( nSuppSizeMin > nSuppSizeCur ) { nSuppSizeMin = nSuppSizeCur; iBestVar = i; } } // cofactor w.r.t. this variable if ( iBestVar != -1 ) { Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar ); Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar ); } return iBestVar; } /**Function************************************************************* Synopsis [Maps the function by the best cofactoring.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ If_Obj_t * Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves ) { unsigned * pCof0 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 0 ); unsigned * pCof1 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 1 ); If_Obj_t * pObj0, * pObj1; Kit_DsdNtk_t * ppNtks[2]; int iBestVar; assert( nVars > 3 ); p->fCalledOnce = 1; // cofactor w.r.t. the best variable iBestVar = Lpk_MapTreeBestCofVar( p, pTruth, nVars, pCof0, pCof1 ); if ( iBestVar == -1 ) return NULL; // decompose the functions ppNtks[0] = Kit_DsdDecompose( pCof0, nVars ); ppNtks[1] = Kit_DsdDecompose( pCof1, nVars ); if ( p->pPars->fVeryVerbose ) { printf( "Cofactoring w.r.t. var %c (%d -> %d+%d supp vars):\n", 'a'+iBestVar, nVars, Kit_TruthSupportSize(pCof0, nVars), Kit_TruthSupportSize(pCof1, nVars) ); Kit_DsdPrintExpanded( ppNtks[0] ); Kit_DsdPrintExpanded( ppNtks[1] ); } // map the DSD structures pObj0 = Lpk_MapTree_rec( p, ppNtks[0], ppLeaves, ppNtks[0]->Root, NULL ); pObj1 = Lpk_MapTree_rec( p, ppNtks[1], ppLeaves, ppNtks[1]->Root, NULL ); Kit_DsdNtkFree( ppNtks[0] ); Kit_DsdNtkFree( ppNtks[1] ); return If_ManCreateMux( p->pIfMan, pObj0, pObj1, ppLeaves[iBestVar] ); } /**Function************************************************************* Synopsis [Implements support-reducing decomposition.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves ) { Kit_DsdNtk_t * pNtkDec, * pNtkComp, * ppNtks[2], * pTemp; If_Obj_t * pObjNew; unsigned * pCof0 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 0 ); unsigned * pCof1 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 1 ); unsigned * pDec0 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 2 ); unsigned * pDec1 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 3 ); unsigned * pDec = (unsigned *)Vec_PtrEntry( p->vTtNodes, 4 ); unsigned * pCo00 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 5 ); unsigned * pCo01 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 6 ); unsigned * pCo10 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 7 ); unsigned * pCo11 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 8 ); unsigned * pCo0 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 9 ); unsigned * pCo1 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 10 ); unsigned * pCo = (unsigned *)Vec_PtrEntry( p->vTtNodes, 11 ); int TrueMint0, TrueMint1, FalseMint0, FalseMint1; int uSubsets, uSubset0, uSubset1, iVar, iVarReused, i; // determine if supp-red decomposition exists uSubsets = Lpk_MapSuppRedDecSelect( p, pTruth, nVars, &iVar, &iVarReused ); if ( uSubsets == 0 ) return NULL; p->nCalledSRed++; // get the cofactors Kit_TruthCofactor0New( pCof0, pTruth, nVars, iVar ); Kit_TruthCofactor1New( pCof1, pTruth, nVars, iVar ); // get the bound sets uSubset0 = uSubsets & 0xFFFF; uSubset1 = uSubsets >> 16; // compute the decomposed functions ppNtks[0] = Kit_DsdDecompose( pCof0, nVars ); ppNtks[1] = Kit_DsdDecompose( pCof1, nVars ); ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] ); Kit_DsdNtkFree( pTemp ); ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] ); Kit_DsdNtkFree( pTemp ); Kit_DsdTruthPartial( p->pDsdMan, ppNtks[0], pDec0, uSubset0 ); Kit_DsdTruthPartial( p->pDsdMan, ppNtks[1], pDec1, uSubset1 ); // Kit_DsdTruthPartialTwo( p->pDsdMan, ppNtks[0], uSubset0, iVarReused, pCo0, pDec0 ); // Kit_DsdTruthPartialTwo( p->pDsdMan, ppNtks[1], uSubset1, iVarReused, pCo1, pDec1 ); Kit_DsdNtkFree( ppNtks[0] ); Kit_DsdNtkFree( ppNtks[1] ); //Kit_DsdPrintFromTruth( pDec0, nVars ); //Kit_DsdPrintFromTruth( pDec1, nVars ); // get the decomposed function Kit_TruthMuxVar( pDec, pDec0, pDec1, nVars, iVar ); // find any true assignments of the decomposed functions TrueMint0 = Kit_TruthFindFirstBit( pDec0, nVars ); TrueMint1 = Kit_TruthFindFirstBit( pDec1, nVars ); assert( TrueMint0 >= 0 && TrueMint1 >= 0 ); // find any false assignments of the decomposed functions FalseMint0 = Kit_TruthFindFirstZero( pDec0, nVars ); FalseMint1 = Kit_TruthFindFirstZero( pDec1, nVars ); assert( FalseMint0 >= 0 && FalseMint1 >= 0 ); // cofactor the cofactors according to these minterms Kit_TruthCopy( pCo00, pCof0, nVars ); Kit_TruthCopy( pCo01, pCof0, nVars ); for ( i = 0; i < nVars; i++ ) if ( uSubset0 & (1 << i) ) { if ( FalseMint0 & (1 << i) ) Kit_TruthCofactor1( pCo00, nVars, i ); else Kit_TruthCofactor0( pCo00, nVars, i ); if ( TrueMint0 & (1 << i) ) Kit_TruthCofactor1( pCo01, nVars, i ); else Kit_TruthCofactor0( pCo01, nVars, i ); } Kit_TruthCopy( pCo10, pCof1, nVars ); Kit_TruthCopy( pCo11, pCof1, nVars ); for ( i = 0; i < nVars; i++ ) if ( uSubset1 & (1 << i) ) { if ( FalseMint1 & (1 << i) ) Kit_TruthCofactor1( pCo10, nVars, i ); else Kit_TruthCofactor0( pCo10, nVars, i ); if ( TrueMint1 & (1 << i) ) Kit_TruthCofactor1( pCo11, nVars, i ); else Kit_TruthCofactor0( pCo11, nVars, i ); } // derive the functions by composing them with the new variable (iVarReused) Kit_TruthMuxVar( pCo0, pCo00, pCo01, nVars, iVarReused ); Kit_TruthMuxVar( pCo1, pCo10, pCo11, nVars, iVarReused ); //Kit_DsdPrintFromTruth( pCo0, nVars ); //Kit_DsdPrintFromTruth( pCo1, nVars ); // derive the composition function Kit_TruthMuxVar( pCo , pCo0 , pCo1 , nVars, iVar ); // process the decomposed function pNtkDec = Kit_DsdDecompose( pDec, nVars ); pNtkComp = Kit_DsdDecompose( pCo, nVars ); //Kit_DsdPrint( stdout, pNtkDec ); //Kit_DsdPrint( stdout, pNtkComp ); //printf( "cofactored variable %c\n", 'a' + iVar ); //printf( "reused variable %c\n", 'a' + iVarReused ); ppLeaves[iVarReused] = Lpk_MapTree_rec( p, pNtkDec, ppLeaves, pNtkDec->Root, NULL ); pObjNew = Lpk_MapTree_rec( p, pNtkComp, ppLeaves, pNtkComp->Root, NULL ); Kit_DsdNtkFree( pNtkDec ); Kit_DsdNtkFree( pNtkComp ); return pObjNew; } /**Function************************************************************* Synopsis [Evaluates 4-LUT decompositions of larger functions.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Lpk_TryDec( word * pTruth, int nVars ) { extern word If_Dec6Perform( word t, int fDerive ); extern void If_Dec6Verify( word t, word z ); int nWords = Abc_Truth6WordNum( nVars ); assert( nVars == 8 ); printf( "%d", If_Dec6Perform(pTruth[0], 1) > 0 ); printf( "%d", If_Dec6Perform(pTruth[1], 1) > 0 ); printf( "%d", If_Dec6Perform(pTruth[2], 1) > 0 ); printf( "%d", If_Dec6Perform(pTruth[3], 1) > 0 ); printf( "\n" ); } void Lpk_TryDecTest() { word t0 = ABC_CONST(0x4f1ead396f247a04); word t1 = ABC_CONST(0x10bdb210c006eab5); word t2 = ABC_CONST(0x68ab4bfa8acb7a13); word t3 = ABC_CONST(0xb14ede67096c6eed); word Truth[4] = {t0, t1, t2, t3}; Lpk_TryDec( Truth, 8 ); } //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END