diff options
Diffstat (limited to 'src/opt/lpk')
| -rw-r--r-- | src/opt/lpk/lpk.h | 82 | ||||
| -rw-r--r-- | src/opt/lpk/lpkCore.c | 280 | ||||
| -rw-r--r-- | src/opt/lpk/lpkCut.c | 584 | ||||
| -rw-r--r-- | src/opt/lpk/lpkInt.h | 161 | ||||
| -rw-r--r-- | src/opt/lpk/lpkMan.c | 96 | ||||
| -rw-r--r-- | src/opt/lpk/lpkMap.c | 349 | ||||
| -rw-r--r-- | src/opt/lpk/lpkMulti.c | 495 | ||||
| -rw-r--r-- | src/opt/lpk/lpkMux.c | 257 | ||||
| -rw-r--r-- | src/opt/lpk/lpkSets.c | 399 | ||||
| -rw-r--r-- | src/opt/lpk/lpk_.c | 48 | ||||
| -rw-r--r-- | src/opt/lpk/module.make | 7 |
11 files changed, 2758 insertions, 0 deletions
diff --git a/src/opt/lpk/lpk.h b/src/opt/lpk/lpk.h new file mode 100644 index 00000000..092b43e1 --- /dev/null +++ b/src/opt/lpk/lpk.h @@ -0,0 +1,82 @@ +/**CFile**************************************************************** + + FileName [lpk.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Fast Boolean matching for LUT structures.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: lpk.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __LPK_H__ +#define __LPK_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Lpk_Par_t_ Lpk_Par_t; +struct Lpk_Par_t_ +{ + // user-controlled parameters + int nLutsMax; // (N) the maximum number of LUTs in the structure + int nLutsOver; // (Q) the maximum number of LUTs not in the MFFC + int nVarsShared; // (S) the maximum number of shared variables (crossbars) + int nGrowthLevel; // (L) the maximum increase in the node level after resynthesis + int fSatur; // iterate till saturation + int fZeroCost; // accept zero-cost replacements + int fVerbose; // the verbosiness flag + int fVeryVerbose; // additional verbose info printout + // internal parameters + int nLutSize; // (K) the LUT size (determined by the input network) + int nVarsMax; // (V) the largest number of variables: V = N * (K-1) + 1 +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// ITERATORS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== lpkCore.c ========================================================*/ +extern int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars ); + + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c new file mode 100644 index 00000000..cbd971e3 --- /dev/null +++ b/src/opt/lpk/lpkCore.c @@ -0,0 +1,280 @@ +/**CFile**************************************************************** + + FileName [lpkCore.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: lpkCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "lpkInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns 1 if at least one entry has changed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_NodeHasChanged( Lpk_Man_t * p, int iNode ) +{ + Vec_Ptr_t * vNodes; + Abc_Obj_t * pTemp; + int i; + vNodes = Vec_VecEntry( p->vVisited, iNode ); + if ( Vec_PtrSize(vNodes) == 0 ) + return 1; + Vec_PtrForEachEntry( vNodes, pTemp, i ) + { + // check if the node has changed + pTemp = Abc_NtkObj( p->pNtk, (int)pTemp ); + if ( pTemp == NULL ) + return 1; + // check if the number of fanouts has changed +// if ( Abc_ObjFanoutNum(pTemp) != (int)Vec_PtrEntry(vNodes, i+1) ) +// return 1; + i++; + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Performs resynthesis for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_ResynthesizeNode( Lpk_Man_t * p ) +{ + Kit_DsdNtk_t * pDsdNtk; + Lpk_Cut_t * pCut; + unsigned * pTruth; + void * pDsd = NULL; + int i, RetValue, clk; + + Lpk_Cut_t * pCutMax; + + // compute the cuts +clk = clock(); + if ( !Lpk_NodeCuts( p ) ) + { +p->timeCuts += clock() - clk; + return 0; + } +p->timeCuts += clock() - clk; + + // find the max volume cut + pCutMax = NULL; + for ( i = 0; i < p->nEvals; i++ ) + { + pCut = p->pCuts + p->pEvals[i]; + if ( pCutMax == NULL || pCutMax->nNodes < pCut->nNodes ) + pCutMax = pCut; + } + assert( pCutMax != NULL ); + + + if ( p->pPars->fVeryVerbose ) + printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals ); + // try the good cuts + p->nCutsTotal += p->nCuts; + p->nCutsUseful += p->nEvals; + for ( i = 0; i < p->nEvals; i++ ) + { + // get the cut + pCut = p->pCuts + p->pEvals[i]; + + if ( pCut != pCutMax ) + continue; + + // compute the truth table +clk = clock(); + pTruth = Lpk_CutTruth( p, pCut ); +p->timeTruth += clock() - clk; + +clk = clock(); + pDsdNtk = Kit_DsdDeriveNtk( pTruth, pCut->nLeaves, p->pPars->nLutSize ); +p->timeEval += clock() - clk; + + if ( Kit_DsdNtkRoot(pDsdNtk)->nFans == 16 ) // skip 16-input non-DSD because ISOP will not work + { + Kit_DsdNtkFree( pDsdNtk ); + continue; + } + + if ( p->pPars->fVeryVerbose ) + { + printf( " C%02d: L= %2d/%2d V= %2d/%d N= %d W= %4.2f ", + i, pCut->nLeaves, Extra_TruthSupportSize(pTruth, pCut->nLeaves), pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight ); + Kit_DsdPrint( stdout, pDsdNtk ); + } + + // update the network +clk = clock(); + RetValue = Lpk_CutExplore( p, pCut, pDsdNtk ); + Kit_DsdNtkFree( pDsdNtk ); +p->timeMap += clock() - clk; + if ( RetValue ) + break; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Performs resynthesis for one network.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars ) +{ + ProgressBar * pProgress; + Lpk_Man_t * p; + Abc_Obj_t * pObj; + double Delta; + int i, Iter, nNodes, nNodesPrev, clk = clock(); + assert( Abc_NtkIsLogic(pNtk) ); + + // get the number of inputs + pPars->nLutSize = Abc_NtkGetFaninMax( pNtk ); + // adjust the number of crossbars based on LUT size + if ( pPars->nVarsShared > pPars->nLutSize - 2 ) + pPars->nVarsShared = pPars->nLutSize - 2; + // get the max number of LUTs tried + pPars->nVarsMax = pPars->nLutsMax * (pPars->nLutSize - 1) + 1; // V = N * (K-1) + 1 + while ( pPars->nVarsMax > 16 ) + { + pPars->nLutsMax--; + pPars->nVarsMax = pPars->nLutsMax * (pPars->nLutSize - 1) + 1; + + } + if ( pPars->fVerbose ) + { + printf( "Resynthesis for %d %d-LUTs with %d non-MFFC LUTs, %d crossbars, and %d-input cuts.\n", + pPars->nLutsMax, pPars->nLutSize, pPars->nLutsOver, pPars->nVarsShared, pPars->nVarsMax ); + } + + // convert logic to AIGs + Abc_NtkToAig( pNtk ); + + // start the manager + p = Lpk_ManStart( pPars ); + p->pNtk = pNtk; + p->nNodesTotal = Abc_NtkNodeNum(pNtk); + p->vLevels = Vec_VecStart( 3 * Abc_NtkLevel(pNtk) ); // computes levels of all nodes + if ( p->pPars->fSatur ) + p->vVisited = Vec_VecStart( 0 ); + + // iterate over the network + nNodesPrev = p->nNodesTotal; + for ( Iter = 1; ; Iter++ ) + { + // expand storage for changed nodes + if ( p->pPars->fSatur ) + Vec_VecExpand( p->vVisited, Abc_NtkObjNumMax(pNtk) + 1 ); + + // consider all nodes + nNodes = Abc_NtkObjNumMax(pNtk); + if ( !pPars->fVeryVerbose ) + pProgress = Extra_ProgressBarStart( stdout, nNodes ); + Abc_NtkForEachNode( pNtk, pObj, i ) + { + // skip all except the final node +// if ( !Abc_ObjIsCo(Abc_ObjFanout0(pObj)) ) +// continue; + + if ( i >= nNodes ) + break; + if ( !pPars->fVeryVerbose ) + Extra_ProgressBarUpdate( pProgress, i, NULL ); + // skip the nodes that did not change + if ( p->pPars->fSatur && !Lpk_NodeHasChanged(p, pObj->Id) ) + continue; + // resynthesize + p->pObj = pObj; + Lpk_ResynthesizeNode( p ); + + if ( p->nChanges == 3 ) + break; + } + if ( !pPars->fVeryVerbose ) + Extra_ProgressBarStop( pProgress ); + + // check the increase + Delta = 100.00 * (nNodesPrev - Abc_NtkNodeNum(pNtk)) / p->nNodesTotal; + if ( Delta < 0.05 ) + break; + nNodesPrev = Abc_NtkNodeNum(pNtk); + if ( !p->pPars->fSatur ) + break; + + break; + } + + if ( pPars->fVerbose ) + { + printf( "N = %5d (%3d) Cut = %5d (%4d) Change = %5d Gain = %5d (%5.2f %%) Iter = %2d\n", + p->nNodesTotal, p->nNodesOver, p->nCutsTotal, p->nCutsUseful, p->nChanges, p->nGainTotal, 100.0 * p->nGainTotal / p->nNodesTotal, Iter ); + printf( "Non_DSD blocks: " ); + for ( i = 3; i <= pPars->nVarsMax; i++ ) + if ( p->nBlocks[i] ) + printf( "%d=%d ", i, p->nBlocks[i] ); + printf( "\n" ); + p->timeTotal = clock() - clk; + p->timeOther = p->timeTotal - p->timeCuts - p->timeTruth - p->timeEval - p->timeMap; + PRTP( "Cuts ", p->timeCuts, p->timeTotal ); + PRTP( "Truth ", p->timeTruth, p->timeTotal ); + PRTP( "Eval ", p->timeEval, p->timeTotal ); + PRTP( "Map ", p->timeMap, p->timeTotal ); + PRTP( "Other ", p->timeOther, p->timeTotal ); + PRTP( "TOTAL ", p->timeTotal, p->timeTotal ); + } + + Lpk_ManStop( p ); + // check the resulting network + if ( !Abc_NtkCheck( pNtk ) ) + { + printf( "Lpk_Resynthesize: The network check has failed.\n" ); + return 0; + } + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c new file mode 100644 index 00000000..251ec829 --- /dev/null +++ b/src/opt/lpk/lpkCut.c @@ -0,0 +1,584 @@ +/**CFile**************************************************************** + + FileName [lpkCut.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: lpkCut.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "lpkInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes the truth able of one cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Lpk_CutTruth_rec( Hop_Man_t * pMan, Hop_Obj_t * pObj, int nVars, Vec_Ptr_t * vTtNodes, int * iCount ) +{ + unsigned * pTruth, * pTruth0, * pTruth1; + assert( !Hop_IsComplement(pObj) ); + if ( pObj->pData ) + { + assert( ((unsigned)pObj->pData) & 0xffff0000 ); + return pObj->pData; + } + // get the plan for a new truth table + pTruth = Vec_PtrEntry( vTtNodes, (*iCount)++ ); + if ( Hop_ObjIsConst1(pObj) ) + Extra_TruthFill( pTruth, nVars ); + else + { + assert( Hop_ObjIsAnd(pObj) ); + // compute the truth tables of the fanins + pTruth0 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin0(pObj), nVars, vTtNodes, iCount ); + pTruth1 = Lpk_CutTruth_rec( pMan, Hop_ObjFanin1(pObj), nVars, vTtNodes, iCount ); + // creat the truth table of the node + Extra_TruthAndPhase( pTruth, pTruth0, pTruth1, nVars, Hop_ObjFaninC0(pObj), Hop_ObjFaninC1(pObj) ); + } + pObj->pData = pTruth; + return pTruth; +} + +/**Function************************************************************* + + Synopsis [Computes the truth able of one cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut ) +{ + Hop_Man_t * pManHop = p->pNtk->pManFunc; + Hop_Obj_t * pObjHop; + Abc_Obj_t * pObj, * pFanin; + unsigned * pTruth; + int i, k, iCount = 0; +// Lpk_NodePrintCut( p, pCut ); + + // initialize the leaves + Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i ) + pObj->pCopy = Vec_PtrEntry( p->vTtElems, i ); + + // construct truth table in the topological order + Lpk_CutForEachNodeReverse( p->pNtk, pCut, pObj, i ) + { + // get the local AIG + pObjHop = Hop_Regular(pObj->pData); + // clean the data field of the nodes in the AIG subgraph + Hop_ObjCleanData_rec( pObjHop ); + // set the initial truth tables at the fanins + Abc_ObjForEachFanin( pObj, pFanin, k ) + { + assert( ((unsigned)pFanin->pCopy) & 0xffff0000 ); + Hop_ManPi( pManHop, k )->pData = pFanin->pCopy; + } + // compute the truth table of internal nodes + pTruth = Lpk_CutTruth_rec( pManHop, pObjHop, pCut->nLeaves, p->vTtNodes, &iCount ); + if ( Hop_IsComplement(pObj->pData) ) + Extra_TruthNot( pTruth, pTruth, pCut->nLeaves ); + // set the truth table at the node + pObj->pCopy = (Abc_Obj_t *)pTruth; + } + + return pTruth; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if at least one entry has changed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_NodeRecordImpact( Lpk_Man_t * p ) +{ + Lpk_Cut_t * pCut; + Vec_Ptr_t * vNodes = Vec_VecEntry( p->vVisited, p->pObj->Id ); + Abc_Obj_t * pNode; + int i, k; + // collect the nodes that impact the given node + Vec_PtrClear( vNodes ); + for ( i = 0; i < p->nCuts; i++ ) + { + pCut = p->pCuts + i; + for ( k = 0; k < (int)pCut->nLeaves; k++ ) + { + pNode = Abc_NtkObj( p->pNtk, pCut->pLeaves[k] ); + if ( pNode->fMarkC ) + continue; + pNode->fMarkC = 1; + Vec_PtrPush( vNodes, (void *)pNode->Id ); + Vec_PtrPush( vNodes, (void *)Abc_ObjFanoutNum(pNode) ); + } + } + // clear the marks + Vec_PtrForEachEntry( vNodes, pNode, i ) + { + pNode = Abc_NtkObj( p->pNtk, (int)pNode ); + pNode->fMarkC = 0; + i++; + } +//printf( "%d ", Vec_PtrSize(vNodes) ); +} + +/**Function************************************************************* + + Synopsis [Returns 1 if the cut has structural DSD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_NodeCutsCheckDsd( Lpk_Man_t * p, Lpk_Cut_t * pCut ) +{ + Abc_Obj_t * pObj, * pFanin; + int i, k, nCands, fLeavesOnly, RetValue; + assert( pCut->nLeaves > 0 ); + // clear ref counters + memset( p->pRefs, 0, sizeof(int) * pCut->nLeaves ); + // mark cut leaves + Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i ) + { + assert( pObj->fMarkA == 0 ); + pObj->fMarkA = 1; + pObj->pCopy = (void *)i; + } + // ref leaves pointed from the internal nodes + nCands = 0; + Lpk_CutForEachNode( p->pNtk, pCut, pObj, i ) + { + fLeavesOnly = 1; + Abc_ObjForEachFanin( pObj, pFanin, k ) + if ( pFanin->fMarkA ) + p->pRefs[(int)pFanin->pCopy]++; + else + fLeavesOnly = 0; + if ( fLeavesOnly ) + p->pCands[nCands++] = pObj->Id; + } + // look at the nodes that only point to the leaves + RetValue = 0; + for ( i = 0; i < nCands; i++ ) + { + pObj = Abc_NtkObj( p->pNtk, p->pCands[i] ); + Abc_ObjForEachFanin( pObj, pFanin, k ) + { + assert( pFanin->fMarkA == 1 ); + if ( p->pRefs[(int)pFanin->pCopy] > 1 ) + break; + } + if ( k == Abc_ObjFaninNum(pObj) ) + { + RetValue = 1; + break; + } + } + // unmark cut leaves + Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i ) + pObj->fMarkA = 0; + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Returns 1 if pDom is contained in pCut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Lpk_NodeCutsOneDominance( Lpk_Cut_t * pDom, Lpk_Cut_t * pCut ) +{ + int i, k; + for ( i = 0; i < (int)pDom->nLeaves; i++ ) + { + for ( k = 0; k < (int)pCut->nLeaves; k++ ) + if ( pDom->pLeaves[i] == pCut->pLeaves[k] ) + break; + if ( k == (int)pCut->nLeaves ) // node i in pDom is not contained in pCut + return 0; + } + // every node in pDom is contained in pCut + return 1; +} + +/**Function************************************************************* + + Synopsis [Check if the cut exists.] + + Description [Returns 1 if the cut exists.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_NodeCutsOneFilter( Lpk_Cut_t * pCuts, int nCuts, Lpk_Cut_t * pCutNew ) +{ + Lpk_Cut_t * pCut; + int i, k; + assert( pCutNew->uSign[0] || pCutNew->uSign[1] ); + // try to find the cut + for ( i = 0; i < nCuts; i++ ) + { + pCut = pCuts + i; + if ( pCut->nLeaves == 0 ) + continue; + if ( pCut->nLeaves == pCutNew->nLeaves ) + { + if ( pCut->uSign[0] == pCutNew->uSign[0] && pCut->uSign[1] == pCutNew->uSign[1] ) + { + for ( k = 0; k < (int)pCutNew->nLeaves; k++ ) + if ( pCut->pLeaves[k] != pCutNew->pLeaves[k] ) + break; + if ( k == (int)pCutNew->nLeaves ) + return 1; + } + continue; + } + if ( pCut->nLeaves < pCutNew->nLeaves ) + { + // skip the non-contained cuts + if ( (pCut->uSign[0] & pCutNew->uSign[0]) != pCut->uSign[0] ) + continue; + if ( (pCut->uSign[1] & pCutNew->uSign[1]) != pCut->uSign[1] ) + continue; + // check containment seriously + if ( Lpk_NodeCutsOneDominance( pCut, pCutNew ) ) + return 1; + continue; + } + // check potential containment of other cut + + // skip the non-contained cuts + if ( (pCut->uSign[0] & pCutNew->uSign[0]) != pCutNew->uSign[0] ) + continue; + if ( (pCut->uSign[1] & pCutNew->uSign[1]) != pCutNew->uSign[1] ) + continue; + // check containment seriously + if ( Lpk_NodeCutsOneDominance( pCutNew, pCut ) ) + pCut->nLeaves = 0; // removed + } + return 0; +} + +/**Function************************************************************* + + Synopsis [Prints the given cut.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_NodePrintCut( Lpk_Man_t * p, Lpk_Cut_t * pCut, int fLeavesOnly ) +{ + Abc_Obj_t * pObj; + int i; + if ( !fLeavesOnly ) + printf( "LEAVES:\n" ); + Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i ) + printf( "%d,", pObj->Id ); + if ( !fLeavesOnly ) + { + printf( "\nNODES:\n" ); + Lpk_CutForEachNode( p->pNtk, pCut, pObj, i ) + { + printf( "%d,", pObj->Id ); + assert( Abc_ObjIsNode(pObj) ); + } + printf( "\n" ); + } +} + +/**Function************************************************************* + + Synopsis [Set the cut signature.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_NodeCutSignature( Lpk_Cut_t * pCut ) +{ + unsigned i; + pCut->uSign[0] = pCut->uSign[1] = 0; + for ( i = 0; i < pCut->nLeaves; i++ ) + { + pCut->uSign[(pCut->pLeaves[i] & 32) > 0] |= (1 << (pCut->pLeaves[i] & 31)); + if ( i != pCut->nLeaves - 1 ) + assert( pCut->pLeaves[i] < pCut->pLeaves[i+1] ); + } +} + + +/**Function************************************************************* + + Synopsis [Computes the set of all cuts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_NodeCutsOne( Lpk_Man_t * p, Lpk_Cut_t * pCut, int Node ) +{ + Lpk_Cut_t * pCutNew; + Abc_Obj_t * pObj, * pFanin; + int i, k, j, nLeavesNew; +/* + printf( "Exploring cut " ); + Lpk_NodePrintCut( p, pCut, 1 ); + printf( "with node %d\n", Node ); +*/ + // check if the cut can stand adding one more internal node + if ( pCut->nNodes == LPK_SIZE_MAX ) + return; + + // if the node is a PI, quit + pObj = Abc_NtkObj( p->pNtk, Node ); + if ( Abc_ObjIsCi(pObj) ) + return; + assert( Abc_ObjIsNode(pObj) ); + assert( Abc_ObjFaninNum(pObj) <= p->pPars->nLutSize ); + + // if the node is not in the MFFC, check the limit + if ( !Abc_NodeIsTravIdCurrent(pObj) ) + { + if ( (int)pCut->nNodesDup == p->pPars->nLutsOver ) + return; + assert( (int)pCut->nNodesDup < p->pPars->nLutsOver ); + } + + // check the possibility of adding this node using the signature + nLeavesNew = pCut->nLeaves - 1; + Abc_ObjForEachFanin( pObj, pFanin, i ) + { + if ( (pCut->uSign[(pFanin->Id & 32) > 0] & (1 << (pFanin->Id & 31))) ) + continue; + if ( ++nLeavesNew > p->pPars->nVarsMax ) + return; + } + + // initialize the set of leaves to the nodes in the cut + assert( p->nCuts < LPK_CUTS_MAX ); + pCutNew = p->pCuts + p->nCuts; +/* +if ( p->pObj->Id == 31 && Node == 38 && pCut->pNodes[0] == 31 && pCut->pNodes[1] == 34 && pCut->pNodes[2] == 35 )//p->nCuts == 48 ) +{ + int x = 0; + printf( "Start:\n" ); + Lpk_NodePrintCut( p, pCut ); +} +*/ + pCutNew->nLeaves = 0; + for ( i = 0; i < (int)pCut->nLeaves; i++ ) + if ( pCut->pLeaves[i] != Node ) + pCutNew->pLeaves[pCutNew->nLeaves++] = pCut->pLeaves[i]; + + // add new nodes + Abc_ObjForEachFanin( pObj, pFanin, i ) + { + // find the place where this node belongs + for ( k = 0; k < (int)pCutNew->nLeaves; k++ ) + if ( pCutNew->pLeaves[k] >= pFanin->Id ) + break; + if ( k < (int)pCutNew->nLeaves && pCutNew->pLeaves[k] == pFanin->Id ) + continue; + // check if there is room + if ( (int)pCutNew->nLeaves == p->pPars->nVarsMax ) + return; + // move all the nodes + for ( j = pCutNew->nLeaves; j > k; j-- ) + pCutNew->pLeaves[j] = pCutNew->pLeaves[j-1]; + pCutNew->pLeaves[k] = pFanin->Id; + pCutNew->nLeaves++; + assert( pCutNew->nLeaves <= LPK_SIZE_MAX ); + + } +/* + printf( " Trying cut: " ); + Lpk_NodePrintCut( p, pCutNew, 1 ); + printf( "\n" ); +*/ + // skip the contained cuts + Lpk_NodeCutSignature( pCutNew ); + if ( Lpk_NodeCutsOneFilter( p->pCuts, p->nCuts, pCutNew ) ) + return; + + + // update the set of internal nodes + assert( pCut->nNodes < LPK_SIZE_MAX ); + memcpy( pCutNew->pNodes, pCut->pNodes, pCut->nNodes * sizeof(int) ); + pCutNew->nNodes = pCut->nNodes; + pCutNew->pNodes[ pCutNew->nNodes++ ] = Node; + + // add the marked node + pCutNew->nNodesDup = pCut->nNodesDup + !Abc_NodeIsTravIdCurrent(pObj); +/* +if ( p->pObj->Id == 31 && Node == 38 )//p->nCuts == 48 ) +{ + int x = 0; + printf( "Finish:\n" ); + Lpk_NodePrintCut( p, pCutNew ); +} +*/ + // add the cut to storage + assert( p->nCuts < LPK_CUTS_MAX ); + p->nCuts++; + + assert( pCut->nNodes <= p->nMffc + pCutNew->nNodesDup ); +/* + printf( " Creating cut: " ); + Lpk_NodePrintCut( p, pCutNew, 1 ); + printf( "\n" ); +*/ +} + +/**Function************************************************************* + + Synopsis [Computes the set of all cuts.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_NodeCuts( Lpk_Man_t * p ) +{ + Lpk_Cut_t * pCut, * pCut2; + int i, k, Temp, nMffc, fChanges; + + // mark the MFFC of the node with the current trav ID + nMffc = p->nMffc = Abc_NodeMffcLabel( p->pObj ); + assert( nMffc > 0 ); + if ( nMffc == 1 ) + return 0; + + // initialize the first cut + pCut = p->pCuts; p->nCuts = 1; + pCut->nNodes = 0; + pCut->nNodesDup = 0; + pCut->nLeaves = 1; + pCut->pLeaves[0] = p->pObj->Id; + // assign the signature + Lpk_NodeCutSignature( pCut ); + + // perform the cut computation + for ( i = 0; i < p->nCuts; i++ ) + { + pCut = p->pCuts + i; + if ( pCut->nLeaves == 0 ) + continue; + // try to expand the fanins of this cut + for ( k = 0; k < (int)pCut->nLeaves; k++ ) + { + // create a new cut + Lpk_NodeCutsOne( p, pCut, pCut->pLeaves[k] ); + // quit if the number of cuts has exceeded the limit + if ( p->nCuts == LPK_CUTS_MAX ) + break; + } + if ( p->nCuts == LPK_CUTS_MAX ) + break; + } + if ( p->nCuts == LPK_CUTS_MAX ) + p->nNodesOver++; + + // record the impact of this node + if ( p->pPars->fSatur ) + Lpk_NodeRecordImpact( p ); + + // compress the cuts by removing empty ones, those with negative Weight, and decomposable ones + p->nEvals = 0; + for ( i = 0; i < p->nCuts; i++ ) + { + pCut = p->pCuts + i; + if ( pCut->nLeaves < 2 ) + continue; + // compute the number of LUTs neede to implement this cut + // V = N * (K-1) + 1 ~~~~~ N = Ceiling[(V-1)/(K-1)] = (V-1)/(K-1) + [(V-1)%(K-1) > 0] + pCut->nLuts = (pCut->nLeaves-1)/(p->pPars->nLutSize-1) + ( (pCut->nLeaves-1)%(p->pPars->nLutSize-1) > 0 ); + pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax; + if ( pCut->Weight <= 1.0 ) + continue; + pCut->fHasDsd = Lpk_NodeCutsCheckDsd( p, pCut ); + if ( pCut->fHasDsd ) + continue; + p->pEvals[p->nEvals++] = i; + } + if ( p->nEvals == 0 ) + return 0; + + // sort the cuts by Weight + do { + fChanges = 0; + for ( i = 0; i < p->nEvals - 1; i++ ) + { + pCut = p->pCuts + p->pEvals[i]; + pCut2 = p->pCuts + p->pEvals[i+1]; + if ( pCut->Weight >= pCut2->Weight ) + continue; + Temp = p->pEvals[i]; + p->pEvals[i] = p->pEvals[i+1]; + p->pEvals[i+1] = Temp; + fChanges = 1; + } + } while ( fChanges ); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/lpk/lpkInt.h b/src/opt/lpk/lpkInt.h new file mode 100644 index 00000000..fe442302 --- /dev/null +++ b/src/opt/lpk/lpkInt.h @@ -0,0 +1,161 @@ +/**CFile**************************************************************** + + FileName [lpkInt.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Fast Boolean matching for LUT structures.] + + Synopsis [Internal declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: lpkInt.h,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef __LPK_INT_H__ +#define __LPK_INT_H__ + +#ifdef __cplusplus +extern "C" { +#endif + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "abc.h" +#include "kit.h" +#include "if.h" +#include "lpk.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +#define LPK_SIZE_MAX 24 // the largest size of the function +#define LPK_CUTS_MAX 512 // the largest number of cuts considered + +typedef struct Lpk_Man_t_ Lpk_Man_t; +typedef struct Lpk_Cut_t_ Lpk_Cut_t; + +struct Lpk_Cut_t_ +{ + unsigned nLeaves : 6; // (L) the number of leaves + unsigned nNodes : 6; // (M) the number of nodes + unsigned nNodesDup : 6; // (Q) nodes outside of MFFC + unsigned nLuts : 6; // (N) the number of LUTs to try + unsigned unused : 6; // unused + unsigned fHasDsd : 1; // set to 1 if the cut has structural DSD (and so cannot be used) + unsigned fMark : 1; // multipurpose mark + unsigned uSign[2]; // the signature + float Weight; // the weight of the cut: (M - Q)/N(V) (the larger the better) + int Gain; // the gain achieved using this cut + int pLeaves[LPK_SIZE_MAX]; // the leaves of the cut + int pNodes[LPK_SIZE_MAX]; // the nodes of the cut +}; + +struct Lpk_Man_t_ +{ + // parameters + Lpk_Par_t * pPars; // the set of parameters + // current representation + Abc_Ntk_t * pNtk; // the network + Abc_Obj_t * pObj; // the node to resynthesize + // cut representation + int nMffc; // the size of MFFC of the node + int nCuts; // the total number of cuts + int nCutsMax; // the largest possible number of cuts + int nEvals; // the number of good cuts + Lpk_Cut_t pCuts[LPK_CUTS_MAX]; // the storage for cuts + int pEvals[LPK_CUTS_MAX]; // the good cuts + // visited nodes + Vec_Vec_t * vVisited; + // mapping manager + If_Man_t * pIfMan; + Vec_Int_t * vCover; + Vec_Vec_t * vLevels; + // temporary variables + int fCofactoring; // working in the cofactoring mode + int fCalledOnce; // limits the depth of MUX cofactoring + int pRefs[LPK_SIZE_MAX]; // fanin reference counters + int pCands[LPK_SIZE_MAX]; // internal nodes pointing only to the leaves + // truth table representation + Vec_Ptr_t * vTtElems; // elementary truth tables + Vec_Ptr_t * vTtNodes; // storage for temporary truth tables of the nodes + // variable sets + Vec_Int_t * vSets[8]; + // statistics + int nNodesTotal; // total number of nodes + int nNodesOver; // nodes with cuts over the limit + int nCutsTotal; // total number of cuts + int nCutsUseful; // useful cuts + int nGainTotal; // the gain in LUTs + int nChanges; // the number of changed nodes + // counter of non-DSD blocks + int nBlocks[17]; + // rutime + int timeCuts; + int timeTruth; + int timeEval; + int timeMap; + int timeOther; + int timeTotal; +}; + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// ITERATORS /// +//////////////////////////////////////////////////////////////////////// + +#define Lpk_CutForEachLeaf( pNtk, pCut, pObj, i ) \ + for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pLeaves[i])), 1); i++ ) +#define Lpk_CutForEachNode( pNtk, pCut, pObj, i ) \ + for ( i = 0; (i < (int)(pCut)->nNodes) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i++ ) +#define Lpk_CutForEachNodeReverse( pNtk, pCut, pObj, i ) \ + for ( i = (int)(pCut)->nNodes - 1; (i >= 0) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i-- ) + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== lpkCut.c =========================================================*/ +extern unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut ); +extern int Lpk_NodeCuts( Lpk_Man_t * p ); +/*=== lpkMap.c =========================================================*/ +extern Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars ); +extern void Lpk_ManStop( Lpk_Man_t * p ); +/*=== lpkMap.c =========================================================*/ +extern int Lpk_CutExplore( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk ); +extern If_Obj_t * Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves ); +extern If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult ); +/*=== lpkMulti.c =======================================================*/ +extern If_Obj_t * Lpk_MapTreeMulti( Lpk_Man_t * p, unsigned * pTruth, int nLeaves, If_Obj_t ** ppLeaves ); +/*=== lpkMux.c =========================================================*/ +extern If_Obj_t * Lpk_MapTreeMux_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves ); +extern If_Obj_t * Lpk_MapSuppRedDec_rec( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves ); +/*=== lpkSets.c =========================================================*/ +extern unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, int * piVar, int * piVarReused ); + +#ifdef __cplusplus +} +#endif + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/opt/lpk/lpkMan.c b/src/opt/lpk/lpkMan.c new file mode 100644 index 00000000..da8b0e3a --- /dev/null +++ b/src/opt/lpk/lpkMan.c @@ -0,0 +1,96 @@ +/**CFile**************************************************************** + + FileName [lpkMan.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: lpkMan.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "lpkInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars ) +{ + Lpk_Man_t * p; + int i; + assert( pPars->nLutsMax <= 16 ); + assert( pPars->nVarsMax > 0 ); + p = ALLOC( Lpk_Man_t, 1 ); + memset( p, 0, sizeof(Lpk_Man_t) ); + p->pPars = pPars; + p->nCutsMax = LPK_CUTS_MAX; + p->vTtElems = Vec_PtrAllocTruthTables( pPars->nVarsMax ); + p->vTtNodes = Vec_PtrAllocSimInfo( 256, Abc_TruthWordNum(pPars->nVarsMax) ); + p->vCover = Vec_IntAlloc( 1 << 12 ); + for ( i = 0; i < 8; i++ ) + p->vSets[i] = Vec_IntAlloc(100); + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_ManStop( Lpk_Man_t * p ) +{ + int i; + for ( i = 0; i < 8; i++ ) + Vec_IntFree(p->vSets[i]); + if ( p->pIfMan ) + { + void * pPars = p->pIfMan->pPars; + If_ManStop( p->pIfMan ); + free( pPars ); + } + if ( p->vLevels ) + Vec_VecFree( p->vLevels ); + if ( p->vVisited ) + Vec_VecFree( p->vVisited ); + Vec_IntFree( p->vCover ); + Vec_PtrFree( p->vTtElems ); + Vec_PtrFree( p->vTtNodes ); + free( p ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/lpk/lpkMap.c b/src/opt/lpk/lpkMap.c new file mode 100644 index 00000000..c647fdf7 --- /dev/null +++ b/src/opt/lpk/lpkMap.c @@ -0,0 +1,349 @@ +/**CFile**************************************************************** + + FileName [lpkMap.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: lpkMap.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "lpkInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +extern void Res_UpdateNetworkLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels ); + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Prepares the mapping manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_IfManStart( Lpk_Man_t * p ) +{ + If_Par_t * pPars; + assert( p->pIfMan == NULL ); + // set defaults + pPars = ALLOC( If_Par_t, 1 ); + memset( pPars, 0, sizeof(If_Par_t) ); + // user-controlable paramters + pPars->nLutSize = p->pPars->nLutSize; + pPars->nCutsMax = 16; + pPars->nFlowIters = 0; // 1 + pPars->nAreaIters = 0; // 1 + pPars->DelayTarget = -1; + pPars->fPreprocess = 0; + pPars->fArea = 1; + pPars->fFancy = 0; + pPars->fExpRed = 0; // + pPars->fLatchPaths = 0; + pPars->fSeqMap = 0; + pPars->fVerbose = 0; + // internal parameters + pPars->fTruth = 0; + pPars->fUsePerm = 0; + pPars->nLatches = 0; + pPars->pLutLib = NULL; // Abc_FrameReadLibLut(); + pPars->pTimesArr = NULL; + pPars->pTimesArr = NULL; + pPars->fUseBdds = 0; + pPars->fUseSops = 0; + pPars->fUseCnfs = 0; + pPars->fUseMv = 0; + // start the mapping manager and set its parameters + p->pIfMan = If_ManStart( pPars ); + If_ManSetupSetAll( p->pIfMan, 1000 ); + p->pIfMan->pPars->pTimesArr = ALLOC( float, 32 ); +} + +/**Function************************************************************* + + Synopsis [Transforms the decomposition graph into the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_Obj_t * Lpk_MapPrimeInternal( If_Man_t * pIfMan, Kit_Graph_t * pGraph ) +{ + Kit_Node_t * pNode; + If_Obj_t * pAnd0, * pAnd1; + int i; + // check for constant function + if ( Kit_GraphIsConst(pGraph) ) + return If_ManConst1(pIfMan); + // check for a literal + if ( Kit_GraphIsVar(pGraph) ) + return Kit_GraphVar(pGraph)->pFunc; + // build the AIG nodes corresponding to the AND gates of the graph + Kit_GraphForEachNode( pGraph, pNode, i ) + { + pAnd0 = Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc; + pAnd1 = Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc; + pNode->pFunc = If_ManCreateAnd( pIfMan, + If_NotCond( If_Regular(pAnd0), If_IsComplement(pAnd0) ^ pNode->eEdge0.fCompl ), + If_NotCond( If_Regular(pAnd1), If_IsComplement(pAnd1) ^ pNode->eEdge1.fCompl ) ); + } + return pNode->pFunc; +} + +/**Function************************************************************* + + Synopsis [Strashes one logic node using its SOP.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_Obj_t * Lpk_MapPrime( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves ) +{ + Kit_Graph_t * pGraph; + Kit_Node_t * pNode; + If_Obj_t * pRes; + int i; + // derive the factored form + pGraph = Kit_TruthToGraph( pTruth, nVars, p->vCover ); + if ( pGraph == NULL ) + return NULL; + // collect the fanins + Kit_GraphForEachLeaf( pGraph, pNode, i ) + pNode->pFunc = ppLeaves[i]; + // perform strashing + pRes = Lpk_MapPrimeInternal( p->pIfMan, pGraph ); + pRes = If_NotCond( pRes, Kit_GraphIsComplement(pGraph) ); + Kit_GraphFree( pGraph ); + return pRes; +} + +/**Function************************************************************* + + Synopsis [Prepares the mapping manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_CutExplore( Lpk_Man_t * p, Lpk_Cut_t * pCut, Kit_DsdNtk_t * pNtk ) +{ + extern Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover ); + Kit_DsdObj_t * pRoot; + If_Obj_t * pDriver, * ppLeaves[16]; + Abc_Obj_t * pLeaf, * pObjNew; + int nGain, i; +// int nOldShared; + + // check special cases + pRoot = Kit_DsdNtkRoot( pNtk ); + if ( pRoot->Type == KIT_DSD_CONST1 ) + { + if ( Kit_DsdLitIsCompl(pNtk->Root) ) + pObjNew = Abc_NtkCreateNodeConst0( p->pNtk ); + else + pObjNew = Abc_NtkCreateNodeConst1( p->pNtk ); + + // perform replacement + pObjNew->Level = p->pObj->Level; + Abc_ObjReplace( p->pObj, pObjNew ); + Res_UpdateNetworkLevel( pObjNew, p->vLevels ); + p->nGainTotal += pCut->nNodes - pCut->nNodesDup; + return 1; + } + if ( pRoot->Type == KIT_DSD_VAR ) + { + pObjNew = Abc_NtkObj( p->pNtk, pCut->pLeaves[ Kit_DsdLit2Var(pRoot->pFans[0]) ] ); + if ( Kit_DsdLitIsCompl(pNtk->Root) ^ Kit_DsdLitIsCompl(pRoot->pFans[0]) ) + pObjNew = Abc_NtkCreateNodeInv( p->pNtk, pObjNew ); + + // perform replacement + pObjNew->Level = p->pObj->Level; + Abc_ObjReplace( p->pObj, pObjNew ); + Res_UpdateNetworkLevel( pObjNew, p->vLevels ); + p->nGainTotal += pCut->nNodes - pCut->nNodesDup; + return 1; + } + assert( pRoot->Type == KIT_DSD_AND || pRoot->Type == KIT_DSD_XOR || pRoot->Type == KIT_DSD_PRIME ); + + // start the mapping manager + if ( p->pIfMan == NULL ) + Lpk_IfManStart( p ); + + // prepare the mapping manager + If_ManRestart( p->pIfMan ); + // create the PI variables + for ( i = 0; i < p->pPars->nVarsMax; i++ ) + ppLeaves[i] = If_ManCreateCi( p->pIfMan ); + // set the arrival times + Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i ) + p->pIfMan->pPars->pTimesArr[i] = (float)pLeaf->Level; + // prepare the PI cuts + If_ManSetupCiCutSets( p->pIfMan ); + // create the internal nodes + p->fCalledOnce = 0; + pDriver = Lpk_MapTree_rec( p, pNtk, ppLeaves, pNtk->Root, NULL ); + if ( pDriver == NULL ) + return 0; + // create the PO node + If_ManCreateCo( p->pIfMan, If_Regular(pDriver) ); + + // perform mapping + p->pIfMan->pPars->fAreaOnly = 1; + If_ManPerformMappingComb( p->pIfMan ); + + // compute the gain in area + nGain = pCut->nNodes - pCut->nNodesDup - (int)p->pIfMan->AreaGlo; + if ( p->pPars->fVeryVerbose ) + printf( " Mffc = %2d. Mapped = %2d. Gain = %3d. Depth increase = %d.\n", + pCut->nNodes - pCut->nNodesDup, (int)p->pIfMan->AreaGlo, nGain, (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level ); + + // quit if there is no gain + if ( !(nGain > 0 || (p->pPars->fZeroCost && nGain == 0)) ) + return 0; + + // quit if depth increases too much + if ( (int)p->pIfMan->RequiredGlo - (int)p->pObj->Level > p->pPars->nGrowthLevel ) + return 0; + + // perform replacement + p->nGainTotal += nGain; + p->nChanges++; + + // prepare the mapping manager + If_ManCleanNodeCopy( p->pIfMan ); + If_ManCleanCutData( p->pIfMan ); + // set the PIs of the cut + Lpk_CutForEachLeaf( p->pNtk, pCut, pLeaf, i ) + If_ObjSetCopy( If_ManCi(p->pIfMan, i), pLeaf ); + // get the area of mapping + pObjNew = Abc_NodeFromIf_rec( p->pNtk, p->pIfMan, If_Regular(pDriver), p->vCover ); + pObjNew->pData = Hop_NotCond( pObjNew->pData, If_IsComplement(pDriver) ); + + // perform replacement + pObjNew->Level = p->pObj->Level; + Abc_ObjReplace( p->pObj, pObjNew ); + Res_UpdateNetworkLevel( pObjNew, p->vLevels ); + return 1; +} + +/**Function************************************************************* + + Synopsis [Prepares the mapping manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_Obj_t * Lpk_MapTree_rec( Lpk_Man_t * p, Kit_DsdNtk_t * pNtk, If_Obj_t ** ppLeaves, int iLit, If_Obj_t * pResult ) +{ + Kit_DsdObj_t * pObj; + If_Obj_t * pObjNew, * pFansNew[16]; + unsigned i, iLitFanin; + + assert( iLit >= 0 ); + + // consider the case of a gate + pObj = Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(iLit) ); + if ( pObj == NULL ) + { + pObjNew = ppLeaves[Kit_DsdLit2Var(iLit)]; + return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) ); + } + if ( pObj->Type == KIT_DSD_CONST1 ) + { + return If_NotCond( If_ManConst1(p->pIfMan), Kit_DsdLitIsCompl(iLit) ); + } + if ( pObj->Type == KIT_DSD_VAR ) + { + pObjNew = ppLeaves[Kit_DsdLit2Var(pObj->pFans[0])]; + return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) ^ Kit_DsdLitIsCompl(pObj->pFans[0]) ); + } + if ( pObj->Type == KIT_DSD_AND ) + { + assert( pObj->nFans == 2 ); + pFansNew[0] = Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[0], NULL ); + pFansNew[1] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[1], NULL ); + if ( pFansNew[0] == NULL || pFansNew[1] == NULL ) + return NULL; + pObjNew = If_ManCreateAnd( p->pIfMan, pFansNew[0], pFansNew[1] ); + return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) ); + } + if ( pObj->Type == KIT_DSD_XOR ) + { + int fCompl = Kit_DsdLitIsCompl(iLit); + assert( pObj->nFans == 2 ); + pFansNew[0] = Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[0], NULL ); + pFansNew[1] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, pObj->pFans[1], NULL ); + if ( pFansNew[0] == NULL || pFansNew[1] == NULL ) + return NULL; + fCompl ^= If_IsComplement(pFansNew[0]) ^ If_IsComplement(pFansNew[1]); + pObjNew = If_ManCreateXor( p->pIfMan, If_Regular(pFansNew[0]), If_Regular(pFansNew[1]) ); + return If_NotCond( pObjNew, fCompl ); + } + assert( pObj->Type == KIT_DSD_PRIME ); + p->nBlocks[pObj->nFans]++; + + // solve for the inputs + Kit_DsdObjForEachFanin( pNtk, pObj, iLitFanin, i ) + { + if ( i == 0 ) + pFansNew[i] = pResult? pResult : Lpk_MapTree_rec( p, pNtk, ppLeaves, iLitFanin, NULL ); + else + pFansNew[i] = Lpk_MapTree_rec( p, pNtk, ppLeaves, iLitFanin, NULL ); + if ( pFansNew[i] == NULL ) + return NULL; + } +/* + if ( !p->fCofactoring && p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize ) + { + pObjNew = Lpk_MapTreeMulti( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew ); + return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) ); + } +*/ + + // find best cofactoring variable + if ( pObj->nFans > 3 && !p->fCalledOnce ) +// pObjNew = Lpk_MapTreeMux_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew ); + pObjNew = Lpk_MapSuppRedDec_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew ); + else + pObjNew = Lpk_MapPrime( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew ); + return If_NotCond( pObjNew, Kit_DsdLitIsCompl(iLit) ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/lpk/lpkMulti.c b/src/opt/lpk/lpkMulti.c new file mode 100644 index 00000000..82cf3578 --- /dev/null +++ b/src/opt/lpk/lpkMulti.c @@ -0,0 +1,495 @@ +/**CFile**************************************************************** + + FileName [lpkMulti.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: lpkMulti.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "lpkInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Records variable order.] + + Description [Increaments Order[x][y] by 1 if x should be above y in the DSD.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_CreateVarOrder( 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 Lpk_CreateCommonOrder( char pTable[][16], int piCofVar[], int nCBars, int pPrios[], int nVars, int fVerbose ) +{ + int Score[16] = {0}, pPres[16]; + int i, y, x, iVarBest, ScoreMax, PrioCount; + + // mark the present variables + for ( i = 0; i < nVars; i++ ) + pPres[i] = 1; + // remove cofactored variables + for ( i = 0; i < nCBars; i++ ) + pPres[piCofVar[i]] = 0; + + // compute scores for each leaf + for ( i = 0; i < nVars; i++ ) + { + if ( pPres[i] == 0 ) + continue; + for ( y = 0; y < nVars; y++ ) + Score[i] += pTable[i][y]; + for ( x = 0; x < nVars; x++ ) + Score[i] -= pTable[x][i]; + } + + // print the scores + if ( fVerbose ) + { + printf( "Scores: " ); + for ( i = 0; i < nVars; i++ ) + printf( "%c=%d ", 'a'+i, Score[i] ); + printf( " " ); + printf( "Prios: " ); + } + + // derive variable priority + // variables with equal score receive the same priority + for ( i = 0; i < nVars; i++ ) + pPrios[i] = 16; + + // iterate until variables remain + for ( PrioCount = 1; ; PrioCount++ ) + { + // find the present variable with the highest score + iVarBest = -1; + ScoreMax = -100000; + for ( i = 0; i < nVars; i++ ) + { + if ( pPres[i] == 0 ) + continue; + if ( ScoreMax < Score[i] ) + { + ScoreMax = Score[i]; + iVarBest = i; + } + } + if ( iVarBest == -1 ) + break; + // give the next priority to all vars having this score + if ( fVerbose ) + printf( "%d=", PrioCount ); + for ( i = 0; i < nVars; i++ ) + { + if ( pPres[i] == 0 ) + continue; + if ( Score[i] == ScoreMax ) + { + pPrios[i] = PrioCount; + pPres[i] = 0; + if ( fVerbose ) + printf( "%c", 'a'+i ); + } + } + if ( fVerbose ) + printf( " " ); + } + if ( fVerbose ) + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Finds components with the highest priority.] + + Description [Returns the number of components selected.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_FindHighest( Kit_DsdNtk_t ** ppNtks, int * piLits, int nSize, int * pPrio, int * pDecision ) +{ + Kit_DsdObj_t * pObj; + unsigned uSupps[8], uSuppFanin, uSuppTotal, uSuppLarge; + int i, pTriv[8], PrioMin, iVarMax, nComps, fOneNonTriv; + + // find individual support and total support + uSuppTotal = 0; + for ( i = 0; i < nSize; i++ ) + { + pTriv[i] = 1; + if ( piLits[i] < 0 ) + uSupps[i] = 0; + else if ( Kit_DsdLitIsLeaf(ppNtks[i], piLits[i]) ) + uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] ); + else + { + pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) ); + if ( pObj->Type == KIT_DSD_PRIME ) + { + pTriv[i] = 0; + uSuppFanin = Kit_DsdLitSupport( ppNtks[i], pObj->pFans[0] ); + } + else + { + assert( pObj->nFans == 2 ); + if ( !Kit_DsdLitIsLeaf(ppNtks[i], pObj->pFans[0]) ) + pTriv[i] = 0; + uSuppFanin = Kit_DsdLitSupport( ppNtks[i], pObj->pFans[1] ); + } + uSupps[i] = Kit_DsdLitSupport( ppNtks[i], piLits[i] ) & ~uSuppFanin; + } + assert( uSupps[i] <= 0xFFFF ); + uSuppTotal |= uSupps[i]; + } + if ( uSuppTotal == 0 ) + return 0; + + // find one support variable with the highest priority + PrioMin = ABC_INFINITY; + iVarMax = -1; + for ( i = 0; i < 16; i++ ) + if ( uSuppTotal & (1 << i) ) + if ( PrioMin > pPrio[i] ) + { + PrioMin = pPrio[i]; + iVarMax = i; + } + assert( iVarMax != -1 ); + + // select components, which have this variable + nComps = 0; + fOneNonTriv = 0; + uSuppLarge = 0; + for ( i = 0; i < nSize; i++ ) + if ( uSupps[i] & (1<<iVarMax) ) + { + if ( pTriv[i] || !fOneNonTriv ) + { + if ( !pTriv[i] ) + { + uSuppLarge = uSupps[i]; + fOneNonTriv = 1; + } + pDecision[i] = 1; + nComps++; + } + else + pDecision[i] = 0; + } + else + pDecision[i] = 0; + + // add other non-trivial not-taken components whose support is contained in the current large component support + if ( fOneNonTriv ) + for ( i = 0; i < nSize; i++ ) + if ( !pTriv[i] && pDecision[i] == 0 && (uSupps[i] & ~uSuppLarge) == 0 ) + { + pDecision[i] = 1; + nComps++; + } + + return nComps; +} + +/**Function************************************************************* + + Synopsis [Prepares the mapping manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_Obj_t * Lpk_MapTreeMulti_rec( Lpk_Man_t * p, Kit_DsdNtk_t ** ppNtks, int * piLits, int * piCofVar, int nCBars, If_Obj_t ** ppLeaves, int nLeaves, int * pPrio ) +{ + Kit_DsdObj_t * pObj; + If_Obj_t * pObjsNew[4][8], * pResPrev; + int piLitsNew[8], pDecision[8]; + int i, k, nComps, nSize; + + // find which of the variables is highest in the order + nSize = (1 << nCBars); + nComps = Lpk_FindHighest( ppNtks, piLits, nSize, pPrio, pDecision ); + if ( nComps == 0 ) + return If_Not( If_ManConst1(p->pIfMan) ); + + // iterate over the nodes + if ( p->pPars->fVeryVerbose ) + printf( "Decision: " ); + for ( i = 0; i < nSize; i++ ) + { + if ( pDecision[i] ) + { + if ( p->pPars->fVeryVerbose ) + printf( "%d ", i ); + assert( piLits[i] >= 0 ); + pObj = Kit_DsdNtkObj( ppNtks[i], Kit_DsdLit2Var(piLits[i]) ); + if ( pObj == NULL ) + piLitsNew[i] = -2; + else if ( pObj->Type == KIT_DSD_PRIME ) + piLitsNew[i] = pObj->pFans[0]; + else + piLitsNew[i] = pObj->pFans[1]; + } + else + piLitsNew[i] = piLits[i]; + } + if ( p->pPars->fVeryVerbose ) + printf( "\n" ); + + // call again + pResPrev = Lpk_MapTreeMulti_rec( p, ppNtks, piLitsNew, piCofVar, nCBars, ppLeaves, nLeaves, pPrio ); + + // create new set of nodes + for ( i = 0; i < nSize; i++ ) + { + if ( pDecision[i] ) + pObjsNew[nCBars][i] = Lpk_MapTree_rec( p, ppNtks[i], ppLeaves, piLits[i], pResPrev ); + else if ( piLits[i] == -1 ) + pObjsNew[nCBars][i] = If_ManConst1(p->pIfMan); + else if ( piLits[i] == -2 ) + pObjsNew[nCBars][i] = If_Not( If_ManConst1(p->pIfMan) ); + 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_ManCreateMux( p->pIfMan, pObjsNew[k][2*i+0], pObjsNew[k][2*i+1], ppLeaves[piCofVar[k-1]] ); + } + assert( nSize == 1 ); + return pObjsNew[0][0]; +} + +/**Function************************************************************* + + Synopsis [Prepares the mapping manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +If_Obj_t * Lpk_MapTreeMulti( Lpk_Man_t * p, unsigned * pTruth, int nVars, If_Obj_t ** ppLeaves ) +{ + static Counter = 0; + If_Obj_t * pResult; + Kit_DsdNtk_t * ppNtks[8] = {0}, * pTemp; + Kit_DsdObj_t * pRoot; + int piCofVar[4], 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 = p->pPars->fVeryVerbose; + + Counter++; +// printf( "Run %d.\n", Counter ); + + // 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 ); +// nCBars = 2; +// piCofVar[0] = 0; +// piCofVar[1] = 1; + + + // 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 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] ); + } + } + + // 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]++; + } + + // find common variable order + for ( i = 0; i < nSize; i++ ) + { + Kit_DsdGetSupports( ppNtks[i] ); + Lpk_CreateVarOrder( ppNtks[i], pTable ); + } + Lpk_CreateCommonOrder( pTable, piCofVar, nCBars, pPrios, nVars, fVerbose ); + // update priorities with frequences + for ( i = 0; i < nVars; i++ ) + pPrios[i] = pPrios[i] * 256 + (16 - pFreqs[i]) * 16 + i; + + if ( fVerbose ) + printf( "After restructuring with priority:\n" ); + + if ( Counter == 1 ) + { + int x = 0; + } + // 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] ); + assert( ppNtks[i]->pSupps[0] <= 0xFFFF ); + // 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 ); + // print the resulting networks + if ( fVerbose ) + { + printf( "Cof%d%d: ", nCBars, i ); + Kit_DsdPrint( stdout, ppNtks[i] ); + } + } + + for ( i = 0; i < nSize; i++ ) + { + // collect the roots + pRoot = Kit_DsdNtkRoot(ppNtks[i]); + if ( pRoot->Type == KIT_DSD_CONST1 ) + piLits[i] = Kit_DsdLitIsCompl(ppNtks[i]->Root)? -2: -1; + else if ( pRoot->Type == KIT_DSD_VAR ) + piLits[i] = Kit_DsdLitNotCond( pRoot->pFans[0], Kit_DsdLitIsCompl(ppNtks[i]->Root) ); + else + piLits[i] = ppNtks[i]->Root; + } + + + // recursively construct AIG for mapping + p->fCofactoring = 1; + pResult = Lpk_MapTreeMulti_rec( p, ppNtks, piLits, piCofVar, nCBars, ppLeaves, nVars, pPrios ); + p->fCofactoring = 0; + + if ( fVerbose ) + printf( "\n" ); + + // verify the transformations + nSize = (1 << nCBars); + for ( i = 0; i < nSize; i++ ) + Kit_DsdTruth( ppNtks[i], ppCofs[nCBars][i] ); + // mux the truth tables + for ( k = nCBars-1; k >= 0; k-- ) + { + nSize = (1 << k); + for ( i = 0; i < nSize; i++ ) + Kit_TruthMuxVar( ppCofs[k][i], ppCofs[k+1][2*i+0], ppCofs[k+1][2*i+1], nVars, piCofVar[k] ); + } + if ( !Extra_TruthIsEqual( pTruth, ppCofs[0][0], nVars ) ) + printf( "Verification failed.\n" ); + + + // free the networks + for ( i = 0; i < 8; i++ ) + if ( ppNtks[i] ) + Kit_DsdNtkFree( ppNtks[i] ); + free( ppCofs[0][0] ); + + return pResult; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/lpk/lpkMux.c b/src/opt/lpk/lpkMux.c new file mode 100644 index 00000000..d9e013f0 --- /dev/null +++ b/src/opt/lpk/lpkMux.c @@ -0,0 +1,257 @@ +/**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" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Find the best cofactoring variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_MapTreeBestVar( Lpk_Man_t * p, unsigned * pTruth, int nVars ) +{ +// Kit_DsdNtk_t * ppNtks[2], * pTemp; + unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 ); + unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 ); + int i, iBestVar, nSuppSizeCur0, nSuppSizeCur1, nSuppSizeCur, nSuppSizeMin; +// int nPrimeSizeCur0, nPrimeSizeCur1, nPrimeSizeCur, nPrimeSizeMin; + + // iterate through variables + iBestVar = -1; + nSuppSizeMin = ABC_INFINITY; +// nPrimeSizeMin = ABC_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; +/* + // check the size of the largest prime components + ppNtks[0] = Kit_DsdDecompose( pCof0, nVars ); + ppNtks[1] = Kit_DsdDecompose( pCof1, nVars ); + // compute the largest non-decomp block + nPrimeSizeCur0 = Kit_DsdNonDsdSizeMax(ppNtks[0]); + nPrimeSizeCur1 = Kit_DsdNonDsdSizeMax(ppNtks[1]); + nPrimeSizeCur = KIT_MAX( nPrimeSizeCur0, nPrimeSizeCur1 ); + + printf( "Evaluating variable %c:\n", 'a'+i ); +// Kit_DsdPrintExpanded( ppNtks[0] ); +// Kit_DsdPrintExpanded( ppNtks[1] ); + + ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] ); + Kit_DsdNtkFree( pTemp ); + + ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] ); + Kit_DsdNtkFree( pTemp ); + + Kit_DsdPrint( stdout, ppNtks[0] ); + Kit_DsdPrint( stdout, ppNtks[1] ); + +// Lpk_DsdEvalSets( p, ppNtks[0], ppNtks[1] ); + + // free the networks + Kit_DsdNtkFree( ppNtks[0] ); + Kit_DsdNtkFree( ppNtks[1] ); +*/ + // compare this variable with other variables + if ( nSuppSizeMin > nSuppSizeCur ) //|| (nSuppSizeMin == nSuppSizeCur && nPrimeSizeMin > nPrimeSizeCur ) ) + { + nSuppSizeMin = nSuppSizeCur; +// nPrimeSizeMin = nPrimeSizeCur; + iBestVar = i; + } + } + printf( "\n" ); + assert( iBestVar != -1 ); + 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 ) +{ + If_Obj_t * pObj0, * pObj1; + Kit_DsdNtk_t * ppNtks[2]; + unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 ); + unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 ); + int iBestVar; + assert( nVars > 3 ); + p->fCalledOnce = 1; + + // cofactor w.r.t. the best variable + iBestVar = Lpk_MapTreeBestVar( p, pTruth, nVars ); + Kit_TruthCofactor0New( pCof0, pTruth, nVars, iBestVar ); + Kit_TruthCofactor1New( pCof1, pTruth, nVars, iBestVar ); + // 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; + If_Obj_t * pObjNew; + unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 ); + unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 ); + unsigned * pDec0 = Vec_PtrEntry( p->vTtNodes, 2 ); + unsigned * pDec1 = Vec_PtrEntry( p->vTtNodes, 3 ); + unsigned * pDec = Vec_PtrEntry( p->vTtNodes, 4 ); + unsigned * pCo00 = Vec_PtrEntry( p->vTtNodes, 5 ); + unsigned * pCo01 = Vec_PtrEntry( p->vTtNodes, 6 ); + unsigned * pCo10 = Vec_PtrEntry( p->vTtNodes, 7 ); + unsigned * pCo11 = Vec_PtrEntry( p->vTtNodes, 8 ); + unsigned * pCo0 = Vec_PtrEntry( p->vTtNodes, 9 ); + unsigned * pCo1 = Vec_PtrEntry( p->vTtNodes, 10 ); + unsigned * pCo = Vec_PtrEntry( p->vTtNodes, 11 ); + int TrueMint0, TrueMint1; + 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; + + // get the bound sets + uSubset0 = uSubsets & 0xFFFF; + uSubset1 = uSubsets >> 16; + // get the cofactors + Kit_TruthCofactor0New( pCof0, pTruth, nVars, iVar ); + Kit_TruthCofactor1New( pCof1, pTruth, nVars, iVar ); + // find any true assignments of the cofactors + TrueMint0 = Kit_TruthFindFirstBit( pCof0, nVars ); + TrueMint1 = Kit_TruthFindFirstBit( pCof1, nVars ); + assert( TrueMint0 >= 0 && TrueMint1 >= 0 ); + // cofactor the cofactors according to these minterms + Kit_TruthCopy( pDec0, pCof0, nVars ); + Kit_TruthCopy( pDec1, pCof1, nVars ); + for ( i = 0; i < nVars; i++ ) + if ( !(uSubset0 & (1 << i)) ) + { + if ( TrueMint0 & (1 << i) ) + Kit_TruthCofactor1( pDec0, nVars, i ); + else + Kit_TruthCofactor0( pDec0, nVars, i ); + } + for ( i = 0; i < nVars; i++ ) + if ( !(uSubset1 & (1 << i)) ) + { + if ( TrueMint1 & (1 << i) ) + Kit_TruthCofactor1( pDec1, nVars, i ); + else + Kit_TruthCofactor0( pDec1, nVars, i ); + } + // get the decomposed function + Kit_TruthMuxVar( pDec, pDec0, pDec1, nVars, iVar ); + + // derive the remainders + Kit_TruthAndPhase( pCo00, pCof0, pDec0, nVars, 0, 1 ); + Kit_TruthAndPhase( pCo01, pCof0, pDec0, nVars, 0, 0 ); + Kit_TruthAndPhase( pCo10, pCof1, pDec1, nVars, 0, 1 ); + Kit_TruthAndPhase( pCo11, pCof1, pDec1, nVars, 0, 0 ); + // quantify bound set variables + for ( i = 0; i < nVars; i++ ) + if ( uSubset0 & (1 << i) ) + { + Kit_TruthExist( pCo00, nVars, i ); + Kit_TruthExist( pCo01, nVars, i ); + } + for ( i = 0; i < nVars; i++ ) + if ( uSubset1 & (1 << i) ) + { + Kit_TruthExist( pCo10, nVars, i ); + Kit_TruthExist( 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 ); + // derive the composition function + Kit_TruthMuxVar( pCo , pCo0 , pCo1 , nVars, iVar ); + + // process the decomposed function + pNtkDec = Kit_DsdDecompose( pDec, nVars ); + Kit_DsdPrint( stdout, pNtkDec ); + ppLeaves[iVarReused] = Lpk_MapTree_rec( p, pNtkDec, ppLeaves, pNtkDec->Root, NULL ); + Kit_DsdNtkFree( pNtkDec ); + + // process the composition function + pNtkComp = Kit_DsdDecompose( pCo, nVars ); + Kit_DsdPrint( stdout, pNtkComp ); + pObjNew = Lpk_MapTree_rec( p, pNtkComp, ppLeaves, pNtkComp->Root, NULL ); + Kit_DsdNtkFree( pNtkComp ); + return pObjNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/lpk/lpkSets.c b/src/opt/lpk/lpkSets.c new file mode 100644 index 00000000..721705cb --- /dev/null +++ b/src/opt/lpk/lpkSets.c @@ -0,0 +1,399 @@ +/**CFile**************************************************************** + + FileName [lpkSets.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: lpkSets.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "lpkInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Lpk_Set_t_ Lpk_Set_t; +struct Lpk_Set_t_ +{ + char iVar; // the cofactoring variable + char Over; // the overlap in supports + char SRed; // the support reduction + char Size; // the size of the boundset + unsigned uSubset0; // the first subset (with removed) + unsigned uSubset1; // the second subset (with removed) +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Recursively computes decomposable subsets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Lpk_ComputeSets_rec( Kit_DsdNtk_t * p, int iLit, Vec_Int_t * vSets ) +{ + unsigned i, iLitFanin, uSupport, uSuppCur; + Kit_DsdObj_t * pObj; + // consider the case of simple gate + pObj = Kit_DsdNtkObj( p, Kit_DsdLit2Var(iLit) ); + if ( pObj == NULL ) + return (1 << Kit_DsdLit2Var(iLit)); + if ( pObj->Type == KIT_DSD_AND || pObj->Type == KIT_DSD_XOR ) + { + unsigned uSupps[16], Limit, s; + uSupport = 0; + Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i ) + { + uSupps[i] = Lpk_ComputeSets_rec( p, iLitFanin, vSets ); + uSupport |= uSupps[i]; + } + // create all subsets, except empty and full + Limit = (1 << pObj->nFans) - 1; + for ( s = 1; s < Limit; s++ ) + { + uSuppCur = 0; + for ( i = 0; i < pObj->nFans; i++ ) + if ( s & (1 << i) ) + uSuppCur |= uSupps[i]; + Vec_IntPush( vSets, uSuppCur ); + } + return uSupport; + } + assert( pObj->Type == KIT_DSD_PRIME ); + // get the cumulative support of all fanins + uSupport = 0; + Kit_DsdObjForEachFanin( p, pObj, iLitFanin, i ) + { + uSuppCur = Lpk_ComputeSets_rec( p, iLitFanin, vSets ); + uSupport |= uSuppCur; + Vec_IntPush( vSets, uSuppCur ); + } + return uSupport; +} + +/**Function************************************************************* + + Synopsis [Computes the set of subsets of decomposable variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Lpk_ComputeSets( Kit_DsdNtk_t * p, Vec_Int_t * vSets ) +{ + unsigned uSupport, Entry, i; + assert( p->nVars <= 16 ); + Vec_IntClear( vSets ); + Vec_IntPush( vSets, 0 ); + if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 ) + return 0; + if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR ) + { + uSupport = ( 1 << Kit_DsdLit2Var(Kit_DsdNtkRoot(p)->pFans[0]) ); + Vec_IntPush( vSets, uSupport ); + return uSupport; + } + uSupport = Lpk_ComputeSets_rec( p, p->Root, vSets ); + assert( (uSupport & 0xFFFF0000) == 0 ); + Vec_IntPush( vSets, uSupport ); + // set the remaining variables + Vec_IntForEachEntry( vSets, Entry, i ) + Vec_IntWriteEntry( vSets, i, Entry | ((uSupport & ~Entry) << 16) ); + return uSupport; +} + +/**Function************************************************************* + + Synopsis [Prints the sets of subsets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_PrintSetOne( int uSupport ) +{ + unsigned k; + for ( k = 0; k < 16; k++ ) + if ( uSupport & (1<<k) ) + printf( "%c", 'a'+k ); + printf( " " ); +} +/**Function************************************************************* + + Synopsis [Prints the sets of subsets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_PrintSets( Vec_Int_t * vSets ) +{ + unsigned uSupport, i; + printf( "Subsets(%d): ", Vec_IntSize(vSets) ); + Vec_IntForEachEntry( vSets, uSupport, i ) + Lpk_PrintSetOne( uSupport ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Computes maximal support reducing bound-sets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_ComposeSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1, int nVars, int iCofVar, + Lpk_Set_t * pStore, int * pSize, int nSizeLimit ) +{ + static int nTravId = 0; // the number of the times this is visited + static int TravId[1<<16] = {0}; // last visited + static char SRed[1<<16]; // best support reduction + static char Over[1<<16]; // best overlaps + static unsigned Parents[1<<16]; // best set of parents + static unsigned short Used[1<<16]; // storage for used subsets + int nSuppSize, nSuppOver, nSuppRed, nUsed, nMinOver, i, k, s; + unsigned Entry, Entry0, Entry1; + unsigned uSupp, uSupp0, uSupp1, uSuppTotal; + Lpk_Set_t * pEntry; + + if ( nTravId == (1 << 30) ) + memset( TravId, 0, sizeof(int) * (1 << 16) ); + + // collect support reducing subsets + nUsed = 0; + nTravId++; + uSuppTotal = Kit_BitMask(nVars) & ~(1<<iCofVar); + Vec_IntForEachEntry( vSets0, Entry0, i ) + Vec_IntForEachEntry( vSets1, Entry1, k ) + { + uSupp0 = (Entry0 & 0xFFFF); + uSupp1 = (Entry1 & 0xFFFF); + // skip trivial + if ( uSupp0 == 0 || uSupp1 == 0 || (uSupp0 | uSupp1) == uSuppTotal ) + continue; + if ( Kit_WordHasOneBit(uSupp0) && Kit_WordHasOneBit(uSupp1) ) + continue; + // get the entry + Entry = Entry0 | Entry1; + uSupp = Entry & 0xFFFF; + // set the bound set size + nSuppSize = Kit_WordCountOnes( uSupp ); + // get the number of overlapping vars + nSuppOver = Kit_WordCountOnes( Entry & (Entry >> 16) ); + // get the support reduction + nSuppRed = nSuppSize - 1 - nSuppOver; + // only consider support-reducing subsets + if ( nSuppRed <= 0 ) + continue; + // check if this support is already used + if ( TravId[uSupp] < nTravId ) + { + Used[nUsed++] = uSupp; + + TravId[uSupp] = nTravId; + SRed[uSupp] = nSuppRed; + Over[uSupp] = nSuppOver; + Parents[uSupp] = (k << 16) | i; + } + else if ( TravId[uSupp] == nTravId && SRed[uSupp] < nSuppRed ) + { + TravId[uSupp] = nTravId; + SRed[uSupp] = nSuppRed; + Over[uSupp] = nSuppOver; + Parents[uSupp] = (k << 16) | i; + } + } + + // check if there are non-overlapping + nMinOver = 1000; + for ( s = 0; s < nUsed; s++ ) + if ( nMinOver > Over[Used[s]] ) + nMinOver = Over[Used[s]]; + + + // collect the accumulated ones + for ( s = 0; s < nUsed; s++ ) + if ( Over[Used[s]] == nMinOver ) + { + // save the entry + if ( *pSize == nSizeLimit ) + return; + pEntry = pStore + (*pSize)++; + + i = Parents[Used[s]] & 0xFFFF; + k = Parents[Used[s]] >> 16; + + pEntry->uSubset0 = Vec_IntEntry(vSets0, i); + pEntry->uSubset1 = Vec_IntEntry(vSets1, k); + Entry = pEntry->uSubset0 | pEntry->uSubset1; + + // record the cofactoring variable + pEntry->iVar = iCofVar; + // set the bound set size + pEntry->Size = Kit_WordCountOnes( Entry & 0xFFFF ); + // get the number of overlapping vars + pEntry->Over = Kit_WordCountOnes( Entry & (Entry >> 16) ); + // get the support reduction + pEntry->SRed = pEntry->Size - 1 - pEntry->Over; + assert( pEntry->SRed > 0 ); + } +} + +/**Function************************************************************* + + Synopsis [Prints one set.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_MapSuppPrintSet( Lpk_Set_t * pSet, int i ) +{ + unsigned Entry; + Entry = pSet->uSubset0 | pSet->uSubset1; + printf( "%2d : ", i ); + printf( "Var = %c ", 'a' + pSet->iVar ); + printf( "Size = %2d ", pSet->Size ); + printf( "Over = %2d ", pSet->Over ); + printf( "SRed = %2d ", pSet->SRed ); + Lpk_PrintSetOne( Entry ); + printf( " " ); + Lpk_PrintSetOne( Entry >> 16 ); + printf( "\n" ); +} + +/**Function************************************************************* + + Synopsis [Evaluates the cofactors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Lpk_MapSuppRedDecSelect( Lpk_Man_t * p, unsigned * pTruth, int nVars, int * piVar, int * piVarReused ) +{ + static int nStoreSize = 256; + static Lpk_Set_t pStore[256], * pSet, * pSetBest; + Kit_DsdNtk_t * ppNtks[2], * pTemp; + Vec_Int_t * vSets0 = p->vSets[0]; + Vec_Int_t * vSets1 = p->vSets[1]; + unsigned * pCof0 = Vec_PtrEntry( p->vTtNodes, 0 ); + unsigned * pCof1 = Vec_PtrEntry( p->vTtNodes, 1 ); + int nSets, i, SizeMax; + unsigned Entry; + + // collect decomposable subsets for each pair of cofactors + nSets = 0; + for ( i = 0; i < nVars; i++ ) + { + printf( "Evaluating variable %c:\n", 'a'+i ); + // evaluate the cofactor pair + Kit_TruthCofactor0New( pCof0, pTruth, nVars, i ); + Kit_TruthCofactor1New( pCof1, pTruth, nVars, i ); + // decompose and expand + 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_DsdPrint( stdout, ppNtks[0] ); + Kit_DsdPrint( stdout, ppNtks[1] ); + // compute subsets + Lpk_ComputeSets( ppNtks[0], vSets0 ); + Lpk_ComputeSets( ppNtks[1], vSets1 ); + // print subsets + Lpk_PrintSets( vSets0 ); + Lpk_PrintSets( vSets1 ); + // free the networks + Kit_DsdNtkFree( ppNtks[0] ); + Kit_DsdNtkFree( ppNtks[1] ); + // evaluate the pair + Lpk_ComposeSets( vSets0, vSets1, nVars, i, pStore, &nSets, nStoreSize ); + } + + // print the results + printf( "\n" ); + for ( i = 0; i < nSets; i++ ) + Lpk_MapSuppPrintSet( pStore + i, i ); + + // choose the best subset + SizeMax = 0; + pSetBest = NULL; + for ( i = 0; i < nSets; i++ ) + { + pSet = pStore + i; + if ( pSet->Size > p->pPars->nLutSize - 1 ) + continue; + if ( SizeMax < pSet->Size ) + { + pSetBest = pSet; + SizeMax = pSet->Size; + } + } + if ( pSetBest == NULL ) + { + printf( "Could not select a subset.\n" ); + return 0; + } + else + { + printf( "Selected the following subset:\n" ); + Lpk_MapSuppPrintSet( pSetBest, pSetBest - pStore ); + } + + // prepare the return result + // get the remaining variables + Entry = ((pSetBest->uSubset0 >> 16) | (pSetBest->uSubset1 >> 16)); + // get the variables to be removed + Entry = Kit_BitMask(nVars) & ~(1<<pSetBest->iVar) & ~Entry; + // make sure there are some - otherwise it is not supp-red + assert( Entry ); + // remember the first such variable + *piVarReused = Kit_WordFindFirstBit( Entry ); + *piVar = pSetBest->iVar; + return (pSetBest->uSubset1 << 16) | (pSetBest->uSubset0 & 0xFFFF); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/lpk/lpk_.c b/src/opt/lpk/lpk_.c new file mode 100644 index 00000000..d8555e08 --- /dev/null +++ b/src/opt/lpk/lpk_.c @@ -0,0 +1,48 @@ +/**CFile**************************************************************** + + FileName [lpk_.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: lpk_.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "lpkInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/lpk/module.make b/src/opt/lpk/module.make new file mode 100644 index 00000000..9e7bbc7c --- /dev/null +++ b/src/opt/lpk/module.make @@ -0,0 +1,7 @@ +SRC += src/aig/lpk/lpkCore.c \ + src/aig/lpk/lpkCut.c \ + src/aig/lpk/lpkMan.c \ + src/aig/lpk/lpkMap.c \ + src/aig/lpk/lpkMulti.c \ + src/aig/lpk/lpkMux.c \ + src/aig/lpk/lpkSets.c |