From 9f5ef0d6184ef9c73591250ef00b18edfd99885b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 31 Aug 2007 08:01:00 -0700 Subject: Version abc70831 --- src/opt/lpk/lpkAbcCore.c | 158 +++++++++++++++++++ src/opt/lpk/lpkAbcDsd.c | 395 +++++++++++++++++++++++++++++++++++++++++++++++ src/opt/lpk/lpkAbcFun.c | 204 ++++++++++++++++++++++++ src/opt/lpk/lpkAbcMux.c | 254 ++++++++++++++++++++++++++++++ src/opt/lpk/lpkCore.c | 90 ++++++++++- src/opt/lpk/lpkCut.c | 58 ++----- src/opt/lpk/lpkInt.h | 59 +++++++ src/opt/lpk/lpkMan.c | 2 +- 8 files changed, 1169 insertions(+), 51 deletions(-) create mode 100644 src/opt/lpk/lpkAbcCore.c create mode 100644 src/opt/lpk/lpkAbcDsd.c create mode 100644 src/opt/lpk/lpkAbcFun.c create mode 100644 src/opt/lpk/lpkAbcMux.c (limited to 'src/opt') diff --git a/src/opt/lpk/lpkAbcCore.c b/src/opt/lpk/lpkAbcCore.c new file mode 100644 index 00000000..53b2668d --- /dev/null +++ b/src/opt/lpk/lpkAbcCore.c @@ -0,0 +1,158 @@ +/**CFile**************************************************************** + + FileName [lpkAbcCore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Fast Boolean matching for LUT structures.] + + Synopsis [The new core procedure.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: lpkAbcCore.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "lpkInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Implements the function.] + + Description [Returns the node implementing this function.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Lpk_FunImplement( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, Lpk_Fun_t * p ) +{ + Abc_Obj_t * pObjNew; + int i; + pObjNew = Abc_NtkCreateNode( pNtk ); + for ( i = 0; i < (int)p->nVars; i++ ) + Abc_ObjAddFanin( pObjNew, Vec_PtrEntry(vLeaves, p->pFanins[i]) ); + Abc_ObjLevelNew( pObjNew ); + // create the logic function + { + extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph ); + // allocate memory for the ISOP + Vec_Int_t * vCover = Vec_IntAlloc( 0 ); + // transform truth table into the decomposition tree + Kit_Graph_t * pGraph = Kit_TruthToGraph( Lpk_FunTruth(p, 0), p->nVars, vCover ); + // derive the AIG for the decomposition tree + pObjNew->pData = Kit_GraphToHop( pNtk->pManFunc, pGraph ); + Kit_GraphFree( pGraph ); + Vec_IntFree( vCover ); + } + return pObjNew; +} + +/**Function************************************************************* + + Synopsis [Implements the function.] + + Description [Returns the node implementing this function.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Lpk_LptImplement( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, int nLeavesOld ) +{ + Lpk_Fun_t * pFun; + Abc_Obj_t * pRes; + int i; + for ( i = Vec_PtrSize(vLeaves) - 1; i >= nLeavesOld; i-- ) + { + pFun = Vec_PtrEntry( vLeaves, i ); + pRes = Lpk_FunImplement( pNtk, vLeaves, pFun ); + Vec_PtrWriteEntry( vLeaves, i, pRes ); + Lpk_FunFree( pFun ); + } + return pRes; +} + +/**Function************************************************************* + + Synopsis [Decomposes the function using recursive MUX decomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_LpkDecompose_rec( Lpk_Fun_t * p ) +{ + Lpk_Fun_t * p2; + int VarPol; + assert( p->nAreaLim > 0 ); + if ( p->nVars <= p->nLutK ) + return 1; + // check if decomposition exists + VarPol = Lpk_FunAnalizeMux( p ); + if ( VarPol == -1 ) + return 0; + // split and call recursively + p2 = Lpk_FunSplitMux( p, VarPol ); + if ( !Lpk_LpkDecompose_rec( p2 ) ) + return 0; + return Lpk_LpkDecompose_rec( p ); +} + + +/**Function************************************************************* + + Synopsis [Decomposes the function using recursive MUX decomposition.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Obj_t * Lpk_LpkDecompose( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim ) +{ + Lpk_Fun_t * p; + Abc_Obj_t * pObjNew = NULL; + int i, nLeaves; + // create the starting function + nLeaves = Vec_PtrSize( vLeaves ); + p = Lpk_FunCreate( pNtk, vLeaves, pTruth, nLutK, AreaLim, DelayLim ); + Lpk_FunSuppMinimize( p ); + // decompose the function + if ( Lpk_LpkDecompose_rec(p) ) + pObjNew = Lpk_LptImplement( pNtk, vLeaves, nLeaves ); + else + { + for ( i = Vec_PtrSize(vLeaves) - 1; i >= nLeaves; i-- ) + Lpk_FunFree( Vec_PtrEntry(vLeaves, i) ); + } + Vec_PtrShrink( vLeaves, nLeaves ); + return pObjNew; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/lpk/lpkAbcDsd.c b/src/opt/lpk/lpkAbcDsd.c new file mode 100644 index 00000000..893844e0 --- /dev/null +++ b/src/opt/lpk/lpkAbcDsd.c @@ -0,0 +1,395 @@ +/**CFile**************************************************************** + + FileName [lpkAbcDsd.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: lpkAbcDsd.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "lpkInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Returns the variable whose cofs have min sum of supp sizes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_FunComputeMinSuppSizeVar( Lpk_Fun_t * p, unsigned ** ppTruths, int nTruths, unsigned ** ppCofs ) +{ + int i, Var, VarBest, nSuppSize0, nSuppSize1, nSuppTotalMin, nSuppTotalCur, nSuppMaxMin, nSuppMaxCur; + VarBest = -1; + Lpk_SuppForEachVar( p->uSupp, Var ) + { + nSuppMaxCur = 0; + nSuppTotalCur = 0; + for ( i = 0; i < nTruths; i++ ) + { + Kit_TruthCofactor0New( ppCofs[2*i+0], ppTruths[i], p->nVars, Var ); + Kit_TruthCofactor1New( ppCofs[2*i+1], ppTruths[i], p->nVars, Var ); + nSuppSize0 = Kit_TruthSupportSize( ppCofs[2*i+0], p->nVars ); + nSuppSize1 = Kit_TruthSupportSize( ppCofs[2*i+1], p->nVars ); + nSuppMaxCur = ABC_MAX( nSuppMaxCur, nSuppSize0 ); + nSuppMaxCur = ABC_MAX( nSuppMaxCur, nSuppSize1 ); + nSuppTotalCur += nSuppSize0 + nSuppSize1; + } + if ( VarBest == -1 || nSuppTotalMin > nSuppTotalCur || + (nSuppTotalMin == nSuppTotalCur && nSuppMaxMin > nSuppMaxCur) ) + { + VarBest = Var; + nSuppMaxMin = nSuppMaxCur; + nSuppTotalMin = nSuppTotalCur; + } + } + // recompute cofactors for the best var + for ( i = 0; i < nTruths; i++ ) + { + Kit_TruthCofactor0New( ppCofs[2*i+0], ppTruths[i], p->nVars, VarBest ); + Kit_TruthCofactor1New( ppCofs[2*i+1], ppTruths[i], p->nVars, VarBest ); + } + return VarBest; +} + +/**Function************************************************************* + + Synopsis [Recursively computes decomposable subsets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +unsigned Lpk_ComputeBoundSets_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_ComputeBoundSets_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_ComputeBoundSets_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 [] + +***********************************************************************/ +Vec_Int_t * Lpk_ComputeBoundSets( Kit_DsdNtk_t * p, int nSizeMax ) +{ + Vec_Int_t * vSets; + unsigned uSupport, Entry; + int Number, i; + assert( p->nVars <= 16 ); + vSets = Vec_IntAlloc( 100 ); + Vec_IntPush( vSets, 0 ); + if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_CONST1 ) + return vSets; + if ( Kit_DsdNtkRoot(p)->Type == KIT_DSD_VAR ) + { + uSupport = ( 1 << Kit_DsdLit2Var(Kit_DsdNtkRoot(p)->pFans[0]) ); + Vec_IntPush( vSets, uSupport ); + return vSets; + } + uSupport = Lpk_ComputeBoundSets_rec( p, p->Root, vSets ); + assert( (uSupport & 0xFFFF0000) == 0 ); + Vec_IntPush( vSets, uSupport ); + // set the remaining variables + Vec_IntForEachEntry( vSets, Number, i ) + { + Entry = Number; + Vec_IntWriteEntry( vSets, i, Entry | ((uSupport & ~Entry) << 16) ); + } + return vSets; +} + +/**Function************************************************************* + + Synopsis [Merges two bound sets.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Lpk_MergeBoundSets( Vec_Int_t * vSets0, Vec_Int_t * vSets1 ) +{ + Vec_Int_t * vSets; + int Entry0, Entry1, Entry; + int i, k; + vSets = Vec_IntAlloc( 100 ); + Vec_IntForEachEntry( vSets0, Entry0, i ) + Vec_IntForEachEntry( vSets1, Entry1, k ) + { + Entry = Entry0 | Entry1; + if ( (Entry & (Entry >> 16)) ) + continue; + Vec_IntPush( vSets, Entry ); + } + return vSets; +} + +/**Function************************************************************* + + Synopsis [Allocates truth tables for cofactors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_FunAllocTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5][16] ) +{ + int i; + assert( nCofDepth <= 4 ); + ppTruths[0][0] = Lpk_FunTruth( p, 0 ); + if ( nCofDepth >= 1 ) + { + ppTruths[1][0] = Lpk_FunTruth( p, 1 ); + ppTruths[1][1] = Lpk_FunTruth( p, 2 ); + } + if ( nCofDepth >= 2 ) + { + ppTruths[2][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 4 ); + for ( i = 1; i < 4; i++ ) + ppTruths[2][i] = ppTruths[2][0] + Kit_TruthWordNum(p->nVars) * i; + } + if ( nCofDepth >= 3 ) + { + ppTruths[3][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 8 ); + for ( i = 1; i < 8; i++ ) + ppTruths[3][i] = ppTruths[3][0] + Kit_TruthWordNum(p->nVars) * i; + } + if ( nCofDepth >= 4 ) + { + ppTruths[4][0] = ALLOC( unsigned, Kit_TruthWordNum(p->nVars) * 16 ); + for ( i = 1; i < 16; i++ ) + ppTruths[4][i] = ppTruths[4][0] + Kit_TruthWordNum(p->nVars) * i; + } +} + +/**Function************************************************************* + + Synopsis [Allocates truth tables for cofactors.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_FunFreeTruthTables( Lpk_Fun_t * p, int nCofDepth, unsigned * ppTruths[5][16] ) +{ + if ( nCofDepth >= 2 ) + free( ppTruths[2][0] ); + if ( nCofDepth >= 3 ) + free( ppTruths[3][0] ); + if ( nCofDepth >= 4 ) + free( ppTruths[4][0] ); +} + +/**Function************************************************************* + + Synopsis [Performs DSD-based decomposition of the function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Lpk_Res_t * Lpk_FunAnalizeDsd( Lpk_Fun_t * p, int nCofDepth ) +{ + static Lpk_Res_t Res, * pRes = &Res; + unsigned * ppTruths[5][16]; + Vec_Int_t * pvBSets[4][8]; + Kit_DsdNtk_t * pNtkDec, * pTemp; + unsigned uBoundSet; + int i, k, nVarsBS, nVarsRem, Delay, Area; + Lpk_FunAllocTruthTables( p, nCofDepth, ppTruths ); + // find the best cofactors + memset( pRes, 0, sizeof(Lpk_Res_t) ); + pRes->nCofVars = nCofDepth; + for ( i = 0; i < nCofDepth; i++ ) + pRes->pCofVars[i] = Lpk_FunComputeMinSuppSizeVar( p, ppTruths[i], 1<nVars ); + pNtkDec = Kit_DsdExpand( pTemp = pNtkDec ); Kit_DsdNtkFree( pTemp ); + pvBSets[nCofDepth][i] = Lpk_ComputeBoundSets( pNtkDec, p->nLutK - nCofDepth ); + Kit_DsdNtkFree( pNtkDec ); + } + // derive the set of feasible boundsets + for ( i = nCofDepth - 1; i >= 0; i-- ) + for ( k = 0; k < (1<> 16)) == 0 ); + nVarsBS = Kit_WordCountOnes( uBoundSet & 0xFFFF ); + nVarsRem = p->nVars - nVarsBS + nCofDepth + 1; + Delay = 1 + Lpk_SuppDelay( uBoundSet & 0xFFFF, p->pDelays ); + Area = 1 + Lpk_LutNumLuts( nVarsRem, p->nLutK ); + if ( Delay > (int)p->nDelayLim || Area > (int)p->nAreaLim ) + continue; + if ( uBoundSet == 0 || pRes->DelayEst > Delay || pRes->DelayEst == Delay && pRes->nSuppSizeL > nVarsRem ) + { + pRes->nBSVars = nVarsBS; + pRes->BSVars = uBoundSet; + pRes->nSuppSizeS = nVarsBS; + pRes->nSuppSizeL = nVarsRem; + pRes->DelayEst = Delay; + pRes->AreaEst = Area; + } + } + // free cofactor storage + Lpk_FunFreeTruthTables( p, nCofDepth, ppTruths ); + return pRes; +} + +/**Function************************************************************* + + Synopsis [Splits the function into two subfunctions using DSD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Lpk_Fun_t * Lpk_FunSplitDsd( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet ) +{ + Kit_DsdMan_t * pDsdMan; + Kit_DsdNtk_t * pNtkDec, * pTemp; + unsigned * pTruth = Lpk_FunTruth( p, 0 ); + unsigned * pTruth0 = Lpk_FunTruth( p, 1 ); + unsigned * pTruth1 = Lpk_FunTruth( p, 2 ); + Lpk_Fun_t * pNew; + unsigned * ppTruths[5][16]; + char pBSVars[5]; + int i, k, nVars, nCofs; + // get the bound set variables + nVars = Lpk_SuppToVars( uBoundSet, pBSVars ); + // compute the cofactors + Lpk_FunAllocTruthTables( p, nCofVars, ppTruths ); + for ( i = 0; i < nCofVars; i++ ) + for ( k = 0; k < (1<nVars, pCofVars[i] ); + Kit_TruthCofactor1New( ppTruths[i+1][2*k+1], ppTruths[i][k], p->nVars, pCofVars[i] ); + } + // decompose each cofactor w.r.t. the bound set + nCofs = (1<nVars, p->nVars * 4 ); + for ( k = 0; k < nCofs; k++ ) + { + pNtkDec = Kit_DsdDecompose( ppTruths[nCofVars][k], p->nVars ); + pNtkDec = Kit_DsdExpand( pTemp = pNtkDec ); Kit_DsdNtkFree( pTemp ); + Kit_DsdTruthPartialTwo( pDsdMan, pNtkDec, uBoundSet, pBSVars[0], ppTruths[nCofVars+1][k], ppTruths[nCofVars+1][nCofs+k] ); + Kit_DsdNtkFree( pNtkDec ); + } + Kit_DsdManFree( pDsdMan ); + // compute the composition function + for ( i = nCofVars - 1; i >= 1; i-- ) + for ( k = 0; k < (1<nVars ); + p->uSupp = Kit_TruthSupport( pTruth0, p->nVars ); + p->pFanins[pBSVars[0]] = pNew->Id; + p->pDelays[pBSVars[0]] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays ); + // support minimize both + Lpk_FunSuppMinimize( p ); + Lpk_FunSuppMinimize( pNew ); + // update delay and area requirements + pNew->nDelayLim = p->nDelayLim - 1; + pNew->nAreaLim = 1; + p->nAreaLim = p->nAreaLim - 1; + + // free cofactor storage + Lpk_FunFreeTruthTables( p, nCofVars, ppTruths ); + return pNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/lpk/lpkAbcFun.c b/src/opt/lpk/lpkAbcFun.c new file mode 100644 index 00000000..f7d2f402 --- /dev/null +++ b/src/opt/lpk/lpkAbcFun.c @@ -0,0 +1,204 @@ +/**CFile**************************************************************** + + FileName [lpkAbcFun.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Fast Boolean matching for LUT structures.] + + Synopsis [Procedures working on decomposed functions.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: lpkAbcFun.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "lpkInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Allocates the function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Lpk_Fun_t * Lpk_FunAlloc( int nVars ) +{ + Lpk_Fun_t * p; + p = (Lpk_Fun_t *)malloc( sizeof(Lpk_Fun_t) + sizeof(unsigned) * Kit_TruthWordNum(nVars) * 3 ); + memset( p, 0, sizeof(Lpk_Fun_t) ); + return p; +} + +/**Function************************************************************* + + Synopsis [Deletes the function] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_FunFree( Lpk_Fun_t * p ) +{ + free( p ); +} + +/**Function************************************************************* + + Synopsis [Creates the starting function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Lpk_Fun_t * Lpk_FunCreate( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim ) +{ + Lpk_Fun_t * p; + Abc_Obj_t * pNode; + int i; + p = Lpk_FunAlloc( Vec_PtrSize(vLeaves) ); + p->Id = Vec_PtrSize(vLeaves); + p->vNodes = vLeaves; + p->nVars = Vec_PtrSize(vLeaves); + p->nLutK = nLutK; + p->nAreaLim = AreaLim; + p->nDelayLim = DelayLim; + p->uSupp = Kit_TruthSupport( pTruth, p->nVars ); + Kit_TruthCopy( Lpk_FunTruth(p,0), pTruth, p->nVars ); + Vec_PtrForEachEntry( vLeaves, pNode, i ) + { + p->pFanins[i] = i; + p->pDelays[i] = pNode->Level; + } + Vec_PtrPush( p->vNodes, p ); + return p; +} + +/**Function************************************************************* + + Synopsis [Creates the new function with the given truth table.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Lpk_Fun_t * Lpk_FunDup( Lpk_Fun_t * p, unsigned * pTruth ) +{ + Lpk_Fun_t * pNew; + pNew = Lpk_FunAlloc( p->nVars ); + pNew->Id = Vec_PtrSize(p->vNodes); + pNew->vNodes = p->vNodes; + pNew->nVars = p->nVars; + pNew->nLutK = p->nLutK; + pNew->nAreaLim = p->nAreaLim; + pNew->nDelayLim = p->nDelayLim; + pNew->uSupp = Kit_TruthSupport( pTruth, p->nVars ); + Kit_TruthCopy( Lpk_FunTruth(pNew,0), pTruth, p->nVars ); + memcpy( pNew->pFanins, p->pFanins, 16 ); + memcpy( pNew->pDelays, p->pDelays, 16 ); + Vec_PtrPush( p->vNodes, pNew ); + return p; +} + +/**Function************************************************************* + + Synopsis [Minimizes support of the function.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_FunSuppMinimize( Lpk_Fun_t * p ) +{ + int j, k, nVarsNew; + // compress the truth table + if ( p->uSupp == Kit_BitMask(p->nVars) ) + return; + // minimize support + nVarsNew = Kit_WordCountOnes(p->uSupp); + Kit_TruthShrink( Lpk_FunTruth(p, 1), Lpk_FunTruth(p, 0), nVarsNew, p->nVars, p->uSupp, 1 ); + for ( j = k = 0; j < (int)p->nVars; j++ ) + if ( p->uSupp & (1 << j) ) + { + p->pFanins[k] = p->pFanins[j]; + p->pDelays[k] = p->pDelays[j]; + k++; + } + assert( k == nVarsNew ); + p->nVars = k; + p->uSupp = Kit_BitMask(p->nVars); +} + +/**Function************************************************************* + + Synopsis [Get the delay of the bound set.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_SuppDelay( unsigned uSupp, char * pDelays ) +{ + int Delay, Var; + Delay = 0; + Lpk_SuppForEachVar( uSupp, Var ) + Delay = ABC_MAX( Delay, pDelays[Var] ); + return Delay + 1; +} + +/**Function************************************************************* + + Synopsis [Converts support into variables.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_SuppToVars( unsigned uBoundSet, char * pVars ) +{ + int i, nVars = 0; + Lpk_SuppForEachVar( uBoundSet, i ) + pVars[nVars++] = i; + return nVars; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/lpk/lpkAbcMux.c b/src/opt/lpk/lpkAbcMux.c new file mode 100644 index 00000000..1525a7e0 --- /dev/null +++ b/src/opt/lpk/lpkAbcMux.c @@ -0,0 +1,254 @@ +/**CFile**************************************************************** + + FileName [lpkAbcMux.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Fast Boolean matching for LUT structures.] + + Synopsis [Iterative MUX decomposition.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - April 28, 2007.] + + Revision [$Id: lpkAbcMux.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "lpkInt.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Computes cofactors w.r.t. the given var.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_FunComputeCofs( Lpk_Fun_t * p, int iVar ) +{ + unsigned * pTruth = Lpk_FunTruth( p, 0 ); + unsigned * pTruth0 = Lpk_FunTruth( p, 1 ); + unsigned * pTruth1 = Lpk_FunTruth( p, 2 ); + Kit_TruthCofactor0New( pTruth0, pTruth, p->nVars, iVar ); + Kit_TruthCofactor1New( pTruth1, pTruth, p->nVars, iVar ); +} + + +/**Function************************************************************* + + Synopsis [Computes cofactors w.r.t. each variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Lpk_FunComputeCofSupps( Lpk_Fun_t * p, unsigned * puSupps ) +{ + unsigned * pTruth = Lpk_FunTruth( p, 0 ); + unsigned * pTruth0 = Lpk_FunTruth( p, 1 ); + unsigned * pTruth1 = Lpk_FunTruth( p, 2 ); + int Var; + Lpk_SuppForEachVar( p->uSupp, Var ) + { + Lpk_FunComputeCofs( p, Var ); + puSupps[2*Var+0] = Kit_TruthSupport( pTruth0, p->nVars ); + puSupps[2*Var+1] = Kit_TruthSupport( pTruth1, p->nVars ); + } +} + +/**Function************************************************************* + + Synopsis [Checks the possibility of MUX decomposition.] + + Description [Returns the best variable to use for MUX decomposition.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_FunAnalizeMux( Lpk_Fun_t * p ) +{ + unsigned puSupps[32] = {0}; + int nSuppSize0, nSuppSize1, Delay, Delay0, Delay1, DelayA, DelayB; + int Var, Area, Polarity, VarBest, AreaBest, PolarityBest, nSuppSizeBest; + + if ( p->nVars > p->nAreaLim * (p->nLutK - 1) + 1 ) + return -1; + // get cofactor supports for each variable + Lpk_FunComputeCofSupps( p, puSupps ); + // derive the delay and area of each MUX-decomposition + VarBest = -1; + Lpk_SuppForEachVar( p->uSupp, Var ) + { + nSuppSize0 = Kit_WordCountOnes(puSupps[2*Var+0]); + nSuppSize1 = Kit_WordCountOnes(puSupps[2*Var+1]); + if ( nSuppSize0 <= (int)p->nLutK - 2 && nSuppSize1 <= (int)p->nLutK - 2 ) + { + // include cof var into 0-block + DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<pDelays ); + DelayB = Lpk_SuppDelay( puSupps[2*Var+1] , p->pDelays ); + Delay0 = ABC_MAX( DelayA, DelayB + 1 ); + // include cof var into 1-block + DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<pDelays ); + DelayB = Lpk_SuppDelay( puSupps[2*Var+0] , p->pDelays ); + Delay1 = ABC_MAX( DelayA, DelayB + 1 ); + // get the best delay + Delay = ABC_MIN( Delay0, Delay1 ); + Area = 2; + Polarity = (int)(Delay1 == Delay); + } + else if ( nSuppSize0 <= (int)p->nLutK - 2 ) + { + DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<pDelays ); + DelayB = Lpk_SuppDelay( puSupps[2*Var+1] , p->pDelays ); + Delay = ABC_MAX( DelayA, DelayB + 1 ); + Area = 1 + Lpk_LutNumLuts( nSuppSize1, p->nLutK ); + Polarity = 0; + } + else if ( nSuppSize0 <= (int)p->nLutK ) + { + DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<pDelays ); + DelayB = Lpk_SuppDelay( puSupps[2*Var+0] , p->pDelays ); + Delay = ABC_MAX( DelayA, DelayB + 1 ); + Area = 1 + Lpk_LutNumLuts( nSuppSize1+2, p->nLutK ); + Polarity = 1; + } + else if ( nSuppSize1 <= (int)p->nLutK - 2 ) + { + DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<pDelays ); + DelayB = Lpk_SuppDelay( puSupps[2*Var+0] , p->pDelays ); + Delay = ABC_MAX( DelayA, DelayB + 1 ); + Area = 1 + Lpk_LutNumLuts( nSuppSize0, p->nLutK ); + Polarity = 1; + } + else if ( nSuppSize1 <= (int)p->nLutK ) + { + DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<pDelays ); + DelayB = Lpk_SuppDelay( puSupps[2*Var+1] , p->pDelays ); + Delay = ABC_MAX( DelayA, DelayB + 1 ); + Area = 1 + Lpk_LutNumLuts( nSuppSize0+2, p->nLutK ); + Polarity = 0; + } + else + { + // include cof var into 0-block + DelayA = Lpk_SuppDelay( puSupps[2*Var+0] | (1<pDelays ); + DelayB = Lpk_SuppDelay( puSupps[2*Var+1] , p->pDelays ); + Delay0 = ABC_MAX( DelayA, DelayB + 1 ); + // include cof var into 1-block + DelayA = Lpk_SuppDelay( puSupps[2*Var+1] | (1<pDelays ); + DelayB = Lpk_SuppDelay( puSupps[2*Var+0] , p->pDelays ); + Delay1 = ABC_MAX( DelayA, DelayB + 1 ); + // get the best delay + Delay = ABC_MIN( Delay0, Delay1 ); + if ( Delay == Delay0 ) + Area = Lpk_LutNumLuts( nSuppSize0+2, p->nLutK ) + Lpk_LutNumLuts( nSuppSize1, p->nLutK ); + else + Area = Lpk_LutNumLuts( nSuppSize1+2, p->nLutK ) + Lpk_LutNumLuts( nSuppSize0, p->nLutK ); + Polarity = (int)(Delay1 == Delay); + } + // find the best variable + if ( Delay > (int)p->nDelayLim ) + continue; + if ( Area > (int)p->nAreaLim ) + continue; + if ( VarBest == -1 || AreaBest > Area || (AreaBest == Area && nSuppSizeBest > nSuppSize0+nSuppSize1) ) + { + VarBest = Var; + AreaBest = Area; + PolarityBest = Polarity; + nSuppSizeBest = nSuppSize0+nSuppSize1; + } + } + return (VarBest == -1)? -1 : (2*VarBest + Polarity); +} + +/**Function************************************************************* + + Synopsis [Transforms the function decomposed by the MUX decomposition.] + + Description [Returns the best variable to use for MUX decomposition.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Lpk_Fun_t * Lpk_FunSplitMux( Lpk_Fun_t * p, int VarPol ) +{ + Lpk_Fun_t * pNew; + unsigned * pTruth = Lpk_FunTruth( p, 0 ); + unsigned * pTruth0 = Lpk_FunTruth( p, 1 ); + unsigned * pTruth1 = Lpk_FunTruth( p, 2 ); + int Var = VarPol / 2; + int Pol = VarPol % 2; + int iVarVac; + assert( VarPol >= 0 && VarPol < 2 * (int)p->nVars ); + assert( p->nAreaLim >= 2 ); + Lpk_FunComputeCofs( p, Var ); + if ( Pol == 0 ) + { + // derive the new component + pNew = Lpk_FunDup( p, pTruth1 ); + // update the old component + p->uSupp = Kit_TruthSupport( pTruth0, p->nVars ); + iVarVac = Kit_WordFindFirstBit( ~(p->uSupp | (1 << Var)) ); + assert( iVarVac < (int)p->nVars ); + Kit_TruthIthVar( pTruth, p->nVars, iVarVac ); + // update the truth table + Kit_TruthMux( pTruth, pTruth0, pTruth1, pTruth, p->nVars ); + p->pFanins[iVarVac] = pNew->Id; + p->pDelays[iVarVac] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays ); + // support minimize both + Lpk_FunSuppMinimize( p ); + Lpk_FunSuppMinimize( pNew ); + // update delay and area requirements + pNew->nDelayLim = p->nDelayLim - 1; + if ( p->nVars <= p->nLutK ) + { + pNew->nAreaLim = p->nAreaLim - 1; + p->nAreaLim = 1; + } + else if ( pNew->nVars <= pNew->nLutK ) + { + pNew->nAreaLim = 1; + p->nAreaLim = p->nAreaLim - 1; + } + else if ( p->nVars < pNew->nVars ) + { + pNew->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2; + p->nAreaLim = p->nAreaLim / 2 - p->nAreaLim % 2; + } + else // if ( pNew->nVars < p->nVars ) + { + pNew->nAreaLim = p->nAreaLim / 2 - p->nAreaLim % 2; + p->nAreaLim = p->nAreaLim / 2 + p->nAreaLim % 2; + } + } + return p; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c index a1da45b5..2158f8f7 100644 --- a/src/opt/lpk/lpkCore.c +++ b/src/opt/lpk/lpkCore.c @@ -258,11 +258,6 @@ p->timeCuts += clock() - clk; if ( p->pPars->fFirst && i == 1 ) break; - if ( p->pObj->Id == 8835 ) - { - int x = 0; - } - // compute the truth table clk = clock(); pTruth = Lpk_CutTruth( p, pCut ); @@ -310,6 +305,91 @@ p->timeEval += clock() - clk; return 1; } +/**Function************************************************************* + + Synopsis [Performs resynthesis for one node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Lpk_ResynthesizeNodeNew( Lpk_Man_t * p ) +{ + static int Count = 0; + Vec_Ptr_t * vLeaves; + Abc_Obj_t * pObjNew; + Lpk_Cut_t * pCut; + unsigned * pTruth; + void * pDsd = NULL; + int i, k, clk; + + // compute the cuts +clk = clock(); + if ( !Lpk_NodeCuts( p ) ) + { +p->timeCuts += clock() - clk; + return 0; + } +p->timeCuts += clock() - clk; + + if ( p->pPars->fVeryVerbose ) + printf( "Node %5d : Mffc size = %5d. Cuts = %5d.\n", p->pObj->Id, p->nMffc, p->nEvals ); + vLeaves = Vec_PtrAlloc( 32 ); + // 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 ( p->pPars->fFirst && i == 1 ) + break; + + // collect nodes into the array + Vec_PtrClear( vLeaves ); + for ( k = 0; k < (int)pCut->nLeaves; k++ ) + Vec_PtrPush( vLeaves, Abc_NtkObj(p->pNtk, pCut->pLeaves[i]) ); + + // compute the truth table +clk = clock(); + pTruth = Lpk_CutTruth( p, pCut ); +p->timeTruth += clock() - clk; + + if ( p->pPars->fVeryVerbose ) + { +// char * pFileName; + int nSuppSize; + Kit_DsdNtk_t * pDsdNtk; + nSuppSize = Extra_TruthSupportSize(pTruth, pCut->nLeaves); + printf( " C%02d: L= %2d/%2d V= %2d/%d N= %d W= %4.2f ", + i, pCut->nLeaves, nSuppSize, pCut->nNodes, pCut->nNodesDup, pCut->nLuts, pCut->Weight ); + + pDsdNtk = Kit_DsdDecompose( pTruth, pCut->nLeaves ); +// Kit_DsdVerify( pDsdNtk, pTruth, pCut->nLeaves ); + Kit_DsdPrint( stdout, pDsdNtk ); + Kit_DsdNtkFree( pDsdNtk ); +// Kit_DsdPrintFromTruth( pTruth, pCut->nLeaves ); +// pFileName = Kit_TruthDumpToFile( pTruth, pCut->nLeaves, Count++ ); +// printf( "Saved truth table in file \"%s\".\n", pFileName ); + } + + // update the network +clk = clock(); + pObjNew = Lpk_LpkDecompose( p->pNtk, vLeaves, pTruth, p->pPars->nLutSize, + (int)pCut->nNodes - (int)pCut->nNodesDup - 1, Abc_ObjRequiredLevel(p->pObj) ); +p->timeEval += clock() - clk; + + // perform replacement + if ( pObjNew ) + Abc_NtkUpdate( p->pObj, pObjNew, p->vLevels ); + } + Vec_PtrFree( vLeaves ); + return 1; +} + /**Function************************************************************* Synopsis [Performs resynthesis for one network.] diff --git a/src/opt/lpk/lpkCut.c b/src/opt/lpk/lpkCut.c index 27a0317c..d0908a6a 100644 --- a/src/opt/lpk/lpkCut.c +++ b/src/opt/lpk/lpkCut.c @@ -410,14 +410,6 @@ void Lpk_NodeCutsOne( Lpk_Man_t * p, Lpk_Cut_t * pCut, int Node ) // 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 ) @@ -443,47 +435,30 @@ if ( p->pObj->Id == 31 && Node == 38 && pCut->pNodes[0] == 31 && pCut->pNodes[1] 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 ); -} -*/ + pCutNew->nNodesDup = pCut->nNodesDup; + // check if the node is already there + for ( i = 0; i < (int)pCutNew->nNodes; i++ ) + if ( pCutNew->pNodes[i] == Node ) + break; + if ( i == (int)pCutNew->nNodes ) // new node + { + pCutNew->pNodes[ pCutNew->nNodes++ ] = Node; + pCutNew->nNodesDup += !Abc_NodeIsTravIdCurrent(pObj); + } + // the number of nodes does not exceed MFFC plus duplications + assert( pCutNew->nNodes <= p->nMffc + pCutNew->nNodesDup ); // 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" ); -*/ - -// if ( !(pCut->nNodes <= p->nMffc + pCutNew->nNodesDup) ) -// printf( "Assertion in line 477 failed.\n" ); } /**Function************************************************************* @@ -527,13 +502,6 @@ int Lpk_NodeCuts( Lpk_Man_t * p ) // try to expand the fanins of this cut for ( k = 0; k < (int)pCut->nLeaves; k++ ) { - - if ( p->pObj->Id == 28 && i == 273 && k == 13 ) - { - Abc_Obj_t * pFanin = Abc_NtkObj(p->pNtk, pCut->pLeaves[k]); - int s = 0; - } - // create a new cut Lpk_NodeCutsOne( p, pCut, pCut->pLeaves[k] ); // quit if the number of cuts has exceeded the limit @@ -559,7 +527,7 @@ int Lpk_NodeCuts( Lpk_Man_t * p ) continue; // compute the minimum number of LUTs needed 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->nLuts = Lpk_LutNumLuts( pCut->nLeaves, p->pPars->nLutSize ); pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax; if ( pCut->Weight <= 1.001 ) continue; diff --git a/src/opt/lpk/lpkInt.h b/src/opt/lpk/lpkInt.h index 683e7b92..d04032ef 100644 --- a/src/opt/lpk/lpkInt.h +++ b/src/opt/lpk/lpkInt.h @@ -117,6 +117,47 @@ struct Lpk_Man_t_ int timeTotal; }; + +// preliminary decomposition result +typedef struct Lpk_Res_t_ Lpk_Res_t; +struct Lpk_Res_t_ +{ + int nBSVars; + unsigned BSVars; + int nCofVars; + char pCofVars[4]; + int nSuppSizeS; + int nSuppSizeL; + int DelayEst; + int AreaEst; +}; + +// function to be decomposed +typedef struct Lpk_Fun_t_ Lpk_Fun_t; +struct Lpk_Fun_t_ +{ + Vec_Ptr_t * vNodes; // the array of all functions + unsigned int Id : 5; // the ID of this node + unsigned int nVars : 5; // the number of variables + unsigned int nLutK : 4; // the number of LUT inputs + unsigned int nAreaLim : 8; // the area limit (the largest allowed) + unsigned int nDelayLim : 10; // the delay limit (the largest allowed) + char pFanins[16]; // the fanins of this function + char pDelays[16]; // the delays of the inputs + unsigned uSupp; // the support of this component + unsigned pTruth[0]; // the truth table (contains room for three truth tables) +}; + +#define Lpk_SuppForEachVar( Supp, Var )\ + for ( Var = 0; Var < 16; Var++ )\ + if ( !(Supp & (1< 0); } + +static inline unsigned * Lpk_FunTruth( Lpk_Fun_t * p, int Num ) { assert( Num < 3 ); return p->pTruth + Kit_TruthWordNum(p->nVars) * Num; } + + //////////////////////////////////////////////////////////////////////// /// MACRO DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -136,6 +177,24 @@ struct Lpk_Man_t_ /// FUNCTION DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +/*=== lpkAbcCore.c ============================================================*/ +extern Abc_Obj_t * Lpk_LpkDecompose( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim ); +/*=== lpkAbcFun.c ============================================================*/ +extern Lpk_Fun_t * Lpk_FunAlloc( int nVars ); +extern void Lpk_FunFree( Lpk_Fun_t * p ); +extern Lpk_Fun_t * Lpk_FunCreate( Abc_Ntk_t * pNtk, Vec_Ptr_t * vLeaves, unsigned * pTruth, int nLutK, int AreaLim, int DelayLim ); +extern Lpk_Fun_t * Lpk_FunDup( Lpk_Fun_t * p, unsigned * pTruth ); +extern void Lpk_FunSuppMinimize( Lpk_Fun_t * p ); +extern int Lpk_SuppDelay( unsigned uSupp, char * pDelays ); +extern int Lpk_SuppToVars( unsigned uBoundSet, char * pVars ); +/*=== lpkAbcDsd.c ============================================================*/ +extern Lpk_Res_t * Lpk_FunAnalizeDsd( Lpk_Fun_t * p, int nCofDepth ); +extern Lpk_Fun_t * Lpk_FunSplitDsd( Lpk_Fun_t * p, char * pCofVars, int nCofVars, unsigned uBoundSet ); +/*=== lpkAbcMux.c ============================================================*/ +extern int Lpk_FunAnalizeMux( Lpk_Fun_t * p ); +extern Lpk_Fun_t * Lpk_FunSplitMux( Lpk_Fun_t * p, int VarPol ); + + /*=== lpkCut.c =========================================================*/ extern unsigned * Lpk_CutTruth( Lpk_Man_t * p, Lpk_Cut_t * pCut ); extern int Lpk_NodeCuts( Lpk_Man_t * p ); diff --git a/src/opt/lpk/lpkMan.c b/src/opt/lpk/lpkMan.c index c11a0a33..5be198d7 100644 --- a/src/opt/lpk/lpkMan.c +++ b/src/opt/lpk/lpkMan.c @@ -54,7 +54,7 @@ Lpk_Man_t * Lpk_ManStart( Lpk_Par_t * pPars ) p->vCover = Vec_IntAlloc( 1 << 12 ); for ( i = 0; i < 8; i++ ) p->vSets[i] = Vec_IntAlloc(100); - p->pDsdMan = Kit_DsdManAlloc( pPars->nVarsMax ); + p->pDsdMan = Kit_DsdManAlloc( pPars->nVarsMax, 64 ); return p; } -- cgit v1.2.3