lpkInt.h File Reference

#include "base/abc/abc.h"
#include "bool/kit/kit.h"
#include "map/if/if.h"
#include "lpk.h"

Go to the source code of this file.

Data Structures
struct	Lpk_Cut_t_
struct	Lpk_Man_t_
struct	Lpk_Fun_t_
struct	Lpk_Res_t_

Macros
#define	LPK_SIZE_MAX   24
	INCLUDES ///. More...
#define	LPK_CUTS_MAX   512
#define	Lpk_CutForEachLeaf(pNtk, pCut, pObj, i)   for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pLeaves[i])), 1); i++ )
	MACRO DEFINITIONS ///. More...
#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-- )
#define	Lpk_SuppForEachVar(Supp, Var)

Typedefs
typedef struct Lpk_Man_t_	Lpk_Man_t
typedef struct Lpk_Cut_t_	Lpk_Cut_t
typedef struct Lpk_Fun_t_	Lpk_Fun_t
typedef struct Lpk_Res_t_	Lpk_Res_t

Functions
static int	Lpk_LutNumVars (int nLutsLim, int nLutK)
static int	Lpk_LutNumLuts (int nVarsMax, int nLutK)
static unsigned *	Lpk_FunTruth (Lpk_Fun_t *p, int Num)
Abc_Obj_t *	Lpk_Decompose (Lpk_Man_t *pMan, Abc_Ntk_t *pNtk, Vec_Ptr_t *vLeaves, unsigned *pTruth, unsigned *puSupps, int nLutK, int AreaLim, int DelayLim)
	FUNCTION DECLARATIONS ///. More...
Lpk_Res_t *	Lpk_DsdAnalize (Lpk_Man_t *pMan, Lpk_Fun_t *p, int nShared)
Lpk_Fun_t *	Lpk_DsdSplit (Lpk_Man_t *pMan, Lpk_Fun_t *p, char *pCofVars, int nCofVars, unsigned uBoundSet)
Lpk_Res_t *	Lpk_MuxAnalize (Lpk_Man_t *pMan, Lpk_Fun_t *p)
	DECLARATIONS ///. More...
Lpk_Fun_t *	Lpk_MuxSplit (Lpk_Man_t *pMan, Lpk_Fun_t *p, int Var, int Pol)
Lpk_Fun_t *	Lpk_FunAlloc (int nVars)
	DECLARATIONS ///. More...
void	Lpk_FunFree (Lpk_Fun_t *p)
Lpk_Fun_t *	Lpk_FunCreate (Abc_Ntk_t *pNtk, Vec_Ptr_t *vLeaves, unsigned *pTruth, int nLutK, int AreaLim, int DelayLim)
Lpk_Fun_t *	Lpk_FunDup (Lpk_Fun_t *p, unsigned *pTruth)
int	Lpk_FunSuppMinimize (Lpk_Fun_t *p)
void	Lpk_FunComputeCofSupps (Lpk_Fun_t *p)
int	Lpk_SuppDelay (unsigned uSupp, char *pDelays)
int	Lpk_SuppToVars (unsigned uBoundSet, char *pVars)
unsigned *	Lpk_CutTruth (Lpk_Man_t *p, Lpk_Cut_t *pCut, int fInv)
int	Lpk_NodeCuts (Lpk_Man_t *p)
Lpk_Man_t *	Lpk_ManStart (Lpk_Par_t *pPars)
	DECLARATIONS ///. More...
void	Lpk_ManStop (Lpk_Man_t *p)
If_Obj_t *	Lpk_MapPrime (Lpk_Man_t *p, unsigned *pTruth, int nVars, If_Obj_t **ppLeaves)
If_Obj_t *	Lpk_MapTree_rec (Lpk_Man_t *p, Kit_DsdNtk_t *pNtk, If_Obj_t **ppLeaves, int iLit, If_Obj_t *pResult)
If_Obj_t *	Lpk_MapTreeMulti (Lpk_Man_t *p, unsigned *pTruth, int nLeaves, If_Obj_t **ppLeaves)
If_Obj_t *	Lpk_MapTreeMux_rec (Lpk_Man_t *p, unsigned *pTruth, int nVars, If_Obj_t **ppLeaves)
If_Obj_t *	Lpk_MapSuppRedDec_rec (Lpk_Man_t *p, unsigned *pTruth, int nVars, If_Obj_t **ppLeaves)
unsigned	Lpk_MapSuppRedDecSelect (Lpk_Man_t *p, unsigned *pTruth, int nVars, int *piVar, int *piVarReused)

Macro Definition Documentation

#define Lpk_CutForEachLeaf	(		pNtk,
			pCut,
			pObj,
			i
	)		for ( i = 0; (i < (int)(pCut)->nLeaves) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pLeaves[i])), 1); i++ )

MACRO DEFINITIONS ///.

ITERATORS ///

Definition at line 189 of file lpkInt.h.

#define Lpk_CutForEachNode	(		pNtk,
			pCut,
			pObj,
			i
	)		for ( i = 0; (i < (int)(pCut)->nNodes) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i++ )

Definition at line 191 of file lpkInt.h.

#define Lpk_CutForEachNodeReverse	(		pNtk,
			pCut,
			pObj,
			i
	)		for ( i = (int)(pCut)->nNodes - 1; (i >= 0) && (((pObj) = Abc_NtkObj(pNtk, (pCut)->pNodes[i])), 1); i-- )

Definition at line 193 of file lpkInt.h.

#define LPK_CUTS_MAX   512

Definition at line 48 of file lpkInt.h.

#define LPK_SIZE_MAX   24

INCLUDES ///.

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

]PARAMETERS ///BASIC TYPES ///

Definition at line 47 of file lpkInt.h.

#define Lpk_SuppForEachVar	(		Supp,
			Var
	)

Value:

for ( Var = 0; Var < 16; Var++ )\
        if ( !(Supp & (1<<Var)) ) {} else

Definition at line 195 of file lpkInt.h.

Typedef Documentation

typedef struct Lpk_Cut_t_ Lpk_Cut_t

Definition at line 51 of file lpkInt.h.

typedef struct Lpk_Fun_t_ Lpk_Fun_t

Definition at line 143 of file lpkInt.h.

typedef struct Lpk_Man_t_ Lpk_Man_t

Definition at line 50 of file lpkInt.h.

typedef struct Lpk_Res_t_ Lpk_Res_t

Definition at line 162 of file lpkInt.h.

Function Documentation

unsigned* Lpk_CutTruth	(	Lpk_Man_t *	p,
		Lpk_Cut_t *	pCut,
		int	fInv
	)

Function*************************************************************

Synopsis [Computes the truth able of one cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 175 of file lpkCut.c.

{
    Hop_Man_t * pManHop = (Hop_Man_t *)p->pNtk->pManFunc;
    Hop_Obj_t * pObjHop;
    Abc_Obj_t * pObj = NULL; // Suppress "might be used uninitialized"
    Abc_Obj_t * pFanin;
    unsigned * pTruth = NULL; // Suppress "might be used uninitialized"
    int i, k, iCount = 0;
//    Lpk_NodePrintCut( p, pCut );
    assert( pCut->nNodes > 0 );

    // initialize the leaves
    Lpk_CutForEachLeaf( p->pNtk, pCut, pObj, i )
        pObj->pCopy = (Abc_Obj_t *)Vec_PtrEntry( p->vTtElems, fInv? pCut->nLeaves-1-i : i );

    // construct truth table in the topological order
    Lpk_CutForEachNodeReverse( p->pNtk, pCut, pObj, i )
    {
        // get the local AIG
        pObjHop = Hop_Regular((Hop_Obj_t *)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)(ABC_PTRUINT_T)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((Hop_Obj_t *)pObj->pData) )
            Kit_TruthNot( pTruth, pTruth, pCut->nLeaves );
        // set the truth table at the node
        pObj->pCopy = (Abc_Obj_t *)pTruth;
    }

    // make sure direct truth table is stored elsewhere (assuming the first call for direct truth!!!)
    if ( fInv == 0 )
    {
        pTruth = (unsigned *)Vec_PtrEntry( p->vTtNodes, iCount++ );
        Kit_TruthCopy( pTruth, (unsigned *)(ABC_PTRUINT_T)pObj->pCopy, pCut->nLeaves );
    }
    assert( iCount <= Vec_PtrSize(p->vTtNodes) );
    return pTruth;
}

Abc_Obj_t* Lpk_Decompose	(	Lpk_Man_t *	p,
		Abc_Ntk_t *	pNtk,
		Vec_Ptr_t *	vLeaves,
		unsigned *	pTruth,
		unsigned *	puSupps,
		int	nLutK,
		int	AreaLim,
		int	DelayLim
	)

FUNCTION DECLARATIONS ///.

Function*************************************************************

Synopsis [Decomposes the function using recursive MUX decomposition.]

Description []

SideEffects []

SeeAlso []

Definition at line 258 of file lpkAbcDec.c.

{
    Lpk_Fun_t * pFun;
    Abc_Obj_t * pObjNew = NULL;
    int nLeaves = Vec_PtrSize( vLeaves );
    pFun = Lpk_FunCreate( pNtk, vLeaves, pTruth, nLutK, AreaLim, DelayLim );
    if ( puSupps[0] || puSupps[1] )
    {
/*
        int i;
        Lpk_FunComputeCofSupps( pFun );
        for ( i = 0; i < nLeaves; i++ )
        {
            assert( pFun->puSupps[2*i+0] == puSupps[2*i+0] );
            assert( pFun->puSupps[2*i+1] == puSupps[2*i+1] );
        }
*/
        memcpy( pFun->puSupps, puSupps, sizeof(unsigned) * 2 * nLeaves );
        pFun->fSupports = 1;
    }
    Lpk_FunSuppMinimize( pFun );
    if ( pFun->nVars <= pFun->nLutK )
        pObjNew = Lpk_ImplementFun( p, pNtk, vLeaves, pFun );
    else if ( Lpk_Decompose_rec(p, pFun) )
        pObjNew = Lpk_Implement( p, pNtk, vLeaves, nLeaves );
    Lpk_DecomposeClean( vLeaves, nLeaves );
    return pObjNew;
}

Lpk_Res_t* Lpk_DsdAnalize	(	Lpk_Man_t *	pMan,
		Lpk_Fun_t *	p,
		int	nShared
	)

Function*************************************************************

Synopsis [Performs DSD-based decomposition of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 452 of file lpkAbcDsd.c.

{ 
    static Lpk_Res_t Res0, * pRes0 = &Res0;
    static Lpk_Res_t Res1, * pRes1 = &Res1;
    static Lpk_Res_t Res2, * pRes2 = &Res2;
    static Lpk_Res_t Res3, * pRes3 = &Res3;
    int fUseBackLooking = 1;
    Lpk_Res_t * pRes = NULL;
    Vec_Int_t * vBSets;
    Kit_DsdNtk_t * pNtks[8] = {NULL};
    char pCofVars[5];
    int i;

    assert( p->nLutK >= 3 );
    assert( nShared >= 0 && nShared <= 3 );
    assert( p->uSupp == Kit_BitMask(p->nVars) );

    // try decomposition without cofactoring
    pNtks[0] = Kit_DsdDecomposeExpand( Lpk_FunTruth( p, 0 ), p->nVars );
    if ( pMan->pPars->fVerbose )
        pMan->nBlocks[ Kit_DsdNonDsdSizeMax(pNtks[0]) ]++;
    vBSets = Lpk_ComputeBoundSets( pNtks[0], p->nLutK );
    Lpk_FunCompareBoundSets( p, vBSets, 0, 0xFFFF, Lpk_DsdLateArriving(p), pRes0 );
    Vec_IntFree( vBSets );

    // check the result
    if ( pRes0->nBSVars == (int)p->nLutK )
        { pRes = pRes0; goto finish; }
    if ( pRes0->nBSVars == (int)p->nLutK - 1 )
        { pRes = pRes0; goto finish; }
    if ( nShared == 0 )
        goto finish;

    // prepare storage
    Kit_TruthCopy( pMan->ppTruths[0][0], Lpk_FunTruth( p, 0 ), p->nVars );

    // cofactor 1 time
    if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 1, pRes1 ) )
        goto finish;
    assert( pRes1->nBSVars <= (int)p->nLutK - 1 );
    if ( pRes1->nBSVars == (int)p->nLutK - 1 )
        { pRes = pRes1; goto finish; }
    if ( pRes0->nBSVars == (int)p->nLutK - 2 )
        { pRes = pRes0; goto finish; }
    if ( pRes1->nBSVars == (int)p->nLutK - 2 )
        { pRes = pRes1; goto finish; }
    if ( nShared == 1 )
        goto finish;

    // cofactor 2 times
    if ( p->nLutK >= 4 ) 
    {
        if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 2, pRes2 ) )
            goto finish;
        assert( pRes2->nBSVars <= (int)p->nLutK - 2 );
        if ( pRes2->nBSVars == (int)p->nLutK - 2 )
            { pRes = pRes2; goto finish; }
        if ( fUseBackLooking )
        {
            if ( pRes0->nBSVars == (int)p->nLutK - 3 )
                { pRes = pRes0; goto finish; }
            if ( pRes1->nBSVars == (int)p->nLutK - 3 )
                { pRes = pRes1; goto finish; }
        }
        if ( pRes2->nBSVars == (int)p->nLutK - 3 )
            { pRes = pRes2; goto finish; }
        if ( nShared == 2 )
            goto finish;
        assert( nShared == 3 );
    }

    // cofactor 3 times
    if ( p->nLutK >= 5 ) 
    {
        if ( !Lpk_DsdAnalizeOne( p, pMan->ppTruths, pNtks, pCofVars, 3, pRes3 ) )
            goto finish;
        assert( pRes3->nBSVars <= (int)p->nLutK - 3 );
        if ( pRes3->nBSVars == (int)p->nLutK - 3 )
            { pRes = pRes3; goto finish; }
        if ( fUseBackLooking )
        {
            if ( pRes0->nBSVars == (int)p->nLutK - 4 )
                { pRes = pRes0; goto finish; }
            if ( pRes1->nBSVars == (int)p->nLutK - 4 )
                { pRes = pRes1; goto finish; }
            if ( pRes2->nBSVars == (int)p->nLutK - 4 )
                { pRes = pRes2; goto finish; }
        }
        if ( pRes3->nBSVars == (int)p->nLutK - 4 )
            { pRes = pRes3; goto finish; }
    }

finish:
    // free the networks
    for ( i = 0; i < (1<<nShared); i++ )
        if ( pNtks[i] )
            Kit_DsdNtkFree( pNtks[i] );
    // choose the best under these conditions
    return pRes;
}

Lpk_Fun_t* Lpk_DsdSplit	(	Lpk_Man_t *	pMan,
		Lpk_Fun_t *	p,
		char *	pCofVars,
		int	nCofVars,
		unsigned	uBoundSet
	)

Function*************************************************************

Synopsis [Splits the function into two subfunctions using DSD.]

Description []

SideEffects []

SeeAlso []

Definition at line 564 of file lpkAbcDsd.c.

{
    Lpk_Fun_t * pNew;
    Kit_DsdNtk_t * pNtkDec;
    int i, k, iVacVar, nCofs;
    // prepare storage
    Kit_TruthCopy( pMan->ppTruths[0][0], Lpk_FunTruth(p, 0), p->nVars );
    // get the vacuous variable
    iVacVar = Kit_WordFindFirstBit( uBoundSet );
    // compute the cofactors
    for ( i = 0; i < nCofVars; i++ )
        for ( k = 0; k < (1<<i); k++ )
        {
            Kit_TruthCofactor0New( pMan->ppTruths[i+1][2*k+0], pMan->ppTruths[i][k], p->nVars, pCofVars[i] );
            Kit_TruthCofactor1New( pMan->ppTruths[i+1][2*k+1], pMan->ppTruths[i][k], p->nVars, pCofVars[i] );
        }
    // decompose each cofactor w.r.t. the bound set
    nCofs = (1<<nCofVars);
    for ( k = 0; k < nCofs; k++ )
    {
        pNtkDec = Kit_DsdDecomposeExpand( pMan->ppTruths[nCofVars][k], p->nVars );
        Kit_DsdTruthPartialTwo( pMan->pDsdMan, pNtkDec, uBoundSet, iVacVar, pMan->ppTruths[nCofVars+1][k], pMan->ppTruths[nCofVars+1][nCofs+k] );
        Kit_DsdNtkFree( pNtkDec );
    }
    // compute the composition/decomposition functions (they will be in pMan->ppTruths[1][0]/pMan->ppTruths[1][1])
    for ( i = nCofVars; i >= 1; i-- )
        for ( k = 0; k < (1<<i); k++ )
            Kit_TruthMuxVar( pMan->ppTruths[i][k], pMan->ppTruths[i+1][2*k+0], pMan->ppTruths[i+1][2*k+1], p->nVars, pCofVars[i-1] );

    // derive the new component (decomposition function)
    pNew = Lpk_FunDup( p, pMan->ppTruths[1][1] );
    // update the old component (composition function)
    Kit_TruthCopy( Lpk_FunTruth(p, 0), pMan->ppTruths[1][0], p->nVars );
    p->uSupp = Kit_TruthSupport( Lpk_FunTruth(p, 0), p->nVars );
    p->pFanins[iVacVar] = pNew->Id;
    p->pDelays[iVacVar] = Lpk_SuppDelay( pNew->uSupp, pNew->pDelays );
    // support minimize both
    p->fSupports = 0;
    Lpk_FunSuppMinimize( p );
    Lpk_FunSuppMinimize( pNew );
    // update delay and area requirements
    pNew->nDelayLim = p->pDelays[iVacVar];
    pNew->nAreaLim = 1;
    p->nAreaLim = p->nAreaLim - 1;
    return pNew;
}

Lpk_Fun_t* Lpk_FunAlloc

(

int

nVars

)

DECLARATIONS ///.

CFile****************************************************************

FileName [lpkAbcUtil.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:

lpkAbcUtil.c,v 1.00 2007/04/28 00:00:00 alanmi Exp

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Allocates the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file lpkAbcUtil.c.

{
    Lpk_Fun_t * p;
    p = (Lpk_Fun_t *)ABC_ALLOC( char, sizeof(Lpk_Fun_t) + sizeof(unsigned) * Kit_TruthWordNum(nVars) * 3 );
    memset( p, 0, sizeof(Lpk_Fun_t) );
    return p;
}

void Lpk_FunComputeCofSupps

(

Lpk_Fun_t *

p

)

Function*************************************************************

Synopsis [Computes cofactors w.r.t. each variable.]

Description []

SideEffects []

SeeAlso []

Definition at line 186 of file lpkAbcUtil.c.

{
    unsigned * pTruth  = Lpk_FunTruth( p, 0 );
    unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
    unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
    int Var;
    assert( p->fSupports == 0 );
//    Lpk_SuppForEachVar( p->uSupp, Var )
    for ( Var = 0; Var < (int)p->nVars; Var++ )
    {
        Kit_TruthCofactor0New( pTruth0, pTruth, p->nVars, Var );
        Kit_TruthCofactor1New( pTruth1, pTruth, p->nVars, Var );
        p->puSupps[2*Var+0] = Kit_TruthSupport( pTruth0, p->nVars );
        p->puSupps[2*Var+1] = Kit_TruthSupport( pTruth1, p->nVars );
    }
    p->fSupports = 1;
}

Lpk_Fun_t* Lpk_FunCreate	(	Abc_Ntk_t *	pNtk,
		Vec_Ptr_t *	vLeaves,
		unsigned *	pTruth,
		int	nLutK,
		int	AreaLim,
		int	DelayLim
	)

Function*************************************************************

Synopsis [Creates the starting function.]

Description []

SideEffects []

SeeAlso []

Definition at line 80 of file lpkAbcUtil.c.

{
    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( Abc_Obj_t *, vLeaves, pNode, i )
    {
        p->pFanins[i] = i;
        p->pDelays[i] = pNode->Level;
    }
    Vec_PtrPush( p->vNodes, p );
    return p;
}

Lpk_Fun_t* Lpk_FunDup	(	Lpk_Fun_t *	p,
		unsigned *	pTruth
	)

Function*************************************************************

Synopsis [Creates the new function with the given truth table.]

Description []

SideEffects []

SeeAlso []

Definition at line 114 of file lpkAbcUtil.c.

{
    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 pNew;
}

void Lpk_FunFree

(

Lpk_Fun_t *

p

)

Function*************************************************************

Synopsis [Deletes the function]

Description []

SideEffects []

SeeAlso []

Definition at line 64 of file lpkAbcUtil.c.

{
    ABC_FREE( p );
}

int Lpk_FunSuppMinimize

(

Lpk_Fun_t *

p

)

Function*************************************************************

Synopsis [Minimizes support of the function.]

Description []

SideEffects []

SeeAlso []

Definition at line 143 of file lpkAbcUtil.c.

{
    int i, k, nVarsNew;
    // compress the truth table
    if ( p->uSupp == Kit_BitMask(p->nVars) )
        return 0;
    // invalidate support info
    p->fSupports = 0;
//Extra_PrintBinary( stdout, &p->uSupp, p->nVars ); printf( "\n" );
    // minimize support
    nVarsNew = Kit_WordCountOnes(p->uSupp);
    Kit_TruthShrink( Lpk_FunTruth(p, 1), Lpk_FunTruth(p, 0), nVarsNew, p->nVars, p->uSupp, 1 );
    k = 0;
    Lpk_SuppForEachVar( p->uSupp, i )
    {
        p->pFanins[k] = p->pFanins[i];
        p->pDelays[k] = p->pDelays[i];
/*
        if ( p->fSupports )
        {
            p->puSupps[2*k+0] = p->puSupps[2*i+0];
            p->puSupps[2*k+1] = p->puSupps[2*i+1];
        }
*/
        k++;
    }
    assert( k == nVarsNew );
    p->nVars = k;
    p->uSupp = Kit_BitMask(p->nVars);
    return 1;
}

static unsigned* Lpk_FunTruth ( Lpk_Fun_t *  p, int  Num  )

inlinestatic

Definition at line 179 of file lpkInt.h.

{ assert( Num < 3 ); return p->pTruth + Kit_TruthWordNum(p->nVars) * Num;        }

static int Lpk_LutNumLuts ( int  nVarsMax, int  nLutK  )

inlinestatic

Definition at line 178 of file lpkInt.h.

{ return (nVarsMax - 1) / (nLutK - 1) + (int)((nVarsMax - 1) % (nLutK - 1) > 0); }

static int Lpk_LutNumVars ( int  nLutsLim, int  nLutK  )

inlinestatic

Definition at line 177 of file lpkInt.h.

{ return  nLutsLim * (nLutK - 1) + 1;                                            }

Lpk_Man_t* Lpk_ManStart

(

Lpk_Par_t *

pPars

)

DECLARATIONS ///.

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

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file lpkMan.c.

{
    Lpk_Man_t * p;
    int i, nWords;
    assert( pPars->nLutsMax <= 16 );
    assert( pPars->nVarsMax > 0 && pPars->nVarsMax <= 16 );
    p = ABC_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( 1024, Abc_TruthWordNum(pPars->nVarsMax) );
    p->vCover = Vec_IntAlloc( 1 << 12 );
    p->vLeaves = Vec_PtrAlloc( 32 );
    for ( i = 0; i < 8; i++ )
        p->vSets[i] = Vec_IntAlloc(100);
    p->pDsdMan = Kit_DsdManAlloc( pPars->nVarsMax, 64 );
    p->vMemory = Vec_IntAlloc( 1024 * 32 );
    p->vBddDir = Vec_IntAlloc( 256 );
    p->vBddInv = Vec_IntAlloc( 256 );
    // allocate temporary storage for truth tables
    nWords = Kit_TruthWordNum(pPars->nVarsMax);
    p->ppTruths[0][0] = ABC_ALLOC( unsigned, 32 * nWords );
    p->ppTruths[1][0] = p->ppTruths[0][0] + 1 * nWords;
    for ( i = 1; i < 2; i++ )
        p->ppTruths[1][i] = p->ppTruths[1][0] + i * nWords;
    p->ppTruths[2][0] = p->ppTruths[1][0] + 2 * nWords;
    for ( i = 1; i < 4; i++ )
        p->ppTruths[2][i] = p->ppTruths[2][0] + i * nWords;
    p->ppTruths[3][0] = p->ppTruths[2][0] + 4 * nWords; 
    for ( i = 1; i < 8; i++ )
        p->ppTruths[3][i] = p->ppTruths[3][0] + i * nWords;
    p->ppTruths[4][0] = p->ppTruths[3][0] + 8 * nWords; 
    for ( i = 1; i < 16; i++ )
        p->ppTruths[4][i] = p->ppTruths[4][0] + i * nWords;
    return p;
}

void Lpk_ManStop

(

Lpk_Man_t *

p

)

Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 94 of file lpkMan.c.

{
    int i;
    ABC_FREE( p->ppTruths[0][0] );
    Vec_IntFree( p->vBddDir );
    Vec_IntFree( p->vBddInv );
    Vec_IntFree( p->vMemory );
    Kit_DsdManFree( p->pDsdMan );
    for ( i = 0; i < 8; i++ )
        Vec_IntFree(p->vSets[i]);
    if ( p->pIfMan )
    {
        void * pPars = p->pIfMan->pPars;
        If_ManStop( p->pIfMan );
        ABC_FREE( pPars );
    }
    if ( p->vLevels )
        Vec_VecFree( p->vLevels );
    if ( p->vVisited )
        Vec_VecFree( p->vVisited );
    Vec_PtrFree( p->vLeaves );
    Vec_IntFree( p->vCover );
    Vec_PtrFree( p->vTtElems );
    Vec_PtrFree( p->vTtNodes );
    ABC_FREE( p );
}

If_Obj_t* Lpk_MapPrime	(	Lpk_Man_t *	p,
		unsigned *	pTruth,
		int	nVars,
		If_Obj_t **	ppLeaves
	)

Function*************************************************************

Synopsis [Strashes one logic node using its SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 79 of file lpkMap.c.

{
    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;
}

If_Obj_t* Lpk_MapSuppRedDec_rec	(	Lpk_Man_t *	p,
		unsigned *	pTruth,
		int	nVars,
		If_Obj_t **	ppLeaves
	)

Function*************************************************************

Synopsis [Implements support-reducing decomposition.]

Description []

SideEffects []

SeeAlso []

Definition at line 133 of file lpkMux.c.

{
    Kit_DsdNtk_t * pNtkDec, * pNtkComp, * ppNtks[2], * pTemp;
    If_Obj_t * pObjNew;
    unsigned * pCof0 = (unsigned *)Vec_PtrEntry( p->vTtNodes,  0 );
    unsigned * pCof1 = (unsigned *)Vec_PtrEntry( p->vTtNodes,  1 );
    unsigned * pDec0 = (unsigned *)Vec_PtrEntry( p->vTtNodes,  2 );
    unsigned * pDec1 = (unsigned *)Vec_PtrEntry( p->vTtNodes,  3 );
    unsigned * pDec  = (unsigned *)Vec_PtrEntry( p->vTtNodes,  4 );
    unsigned * pCo00 = (unsigned *)Vec_PtrEntry( p->vTtNodes,  5 );
    unsigned * pCo01 = (unsigned *)Vec_PtrEntry( p->vTtNodes,  6 );
    unsigned * pCo10 = (unsigned *)Vec_PtrEntry( p->vTtNodes,  7 );
    unsigned * pCo11 = (unsigned *)Vec_PtrEntry( p->vTtNodes,  8 );
    unsigned * pCo0  = (unsigned *)Vec_PtrEntry( p->vTtNodes,  9 );
    unsigned * pCo1  = (unsigned *)Vec_PtrEntry( p->vTtNodes, 10 );
    unsigned * pCo   = (unsigned *)Vec_PtrEntry( p->vTtNodes, 11 );
    int TrueMint0, TrueMint1, FalseMint0, FalseMint1;
    int uSubsets, uSubset0, uSubset1, iVar, iVarReused, i;

    // determine if supp-red decomposition exists
    uSubsets = Lpk_MapSuppRedDecSelect( p, pTruth, nVars, &iVar, &iVarReused );
    if ( uSubsets == 0 )
        return NULL;
    p->nCalledSRed++;

    // get the cofactors
    Kit_TruthCofactor0New( pCof0, pTruth, nVars, iVar );
    Kit_TruthCofactor1New( pCof1, pTruth, nVars, iVar );

    // get the bound sets
    uSubset0 = uSubsets & 0xFFFF;
    uSubset1 = uSubsets >> 16;

    // compute the decomposed functions
    ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
    ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
    ppNtks[0] = Kit_DsdExpand( pTemp = ppNtks[0] );      Kit_DsdNtkFree( pTemp );
    ppNtks[1] = Kit_DsdExpand( pTemp = ppNtks[1] );      Kit_DsdNtkFree( pTemp );
    Kit_DsdTruthPartial( p->pDsdMan, ppNtks[0], pDec0, uSubset0 );
    Kit_DsdTruthPartial( p->pDsdMan, ppNtks[1], pDec1, uSubset1 );
//    Kit_DsdTruthPartialTwo( p->pDsdMan, ppNtks[0], uSubset0, iVarReused, pCo0, pDec0 );
//    Kit_DsdTruthPartialTwo( p->pDsdMan, ppNtks[1], uSubset1, iVarReused, pCo1, pDec1 );
    Kit_DsdNtkFree( ppNtks[0] );
    Kit_DsdNtkFree( ppNtks[1] );
//Kit_DsdPrintFromTruth( pDec0, nVars );
//Kit_DsdPrintFromTruth( pDec1, nVars );
    // get the decomposed function
    Kit_TruthMuxVar( pDec, pDec0, pDec1, nVars, iVar );

    // find any true assignments of the decomposed functions
    TrueMint0 = Kit_TruthFindFirstBit( pDec0, nVars );
    TrueMint1 = Kit_TruthFindFirstBit( pDec1, nVars );
    assert( TrueMint0 >= 0 && TrueMint1 >= 0 );
    // find any false assignments of the decomposed functions
    FalseMint0 = Kit_TruthFindFirstZero( pDec0, nVars );
    FalseMint1 = Kit_TruthFindFirstZero( pDec1, nVars );
    assert( FalseMint0 >= 0 && FalseMint1 >= 0 );

    // cofactor the cofactors according to these minterms
    Kit_TruthCopy( pCo00, pCof0, nVars );
    Kit_TruthCopy( pCo01, pCof0, nVars );
    for ( i = 0; i < nVars; i++ )
        if ( uSubset0 & (1 << i) )
        {
            if ( FalseMint0 & (1 << i) )
                Kit_TruthCofactor1( pCo00, nVars, i );
            else
                Kit_TruthCofactor0( pCo00, nVars, i );
            if ( TrueMint0 & (1 << i) )
                Kit_TruthCofactor1( pCo01, nVars, i );
            else
                Kit_TruthCofactor0( pCo01, nVars, i );
        }
    Kit_TruthCopy( pCo10, pCof1, nVars );
    Kit_TruthCopy( pCo11, pCof1, nVars );
    for ( i = 0; i < nVars; i++ )
        if ( uSubset1 & (1 << i) )
        {
            if ( FalseMint1 & (1 << i) )
                Kit_TruthCofactor1( pCo10, nVars, i );
            else
                Kit_TruthCofactor0( pCo10, nVars, i );
            if ( TrueMint1 & (1 << i) )
                Kit_TruthCofactor1( pCo11, nVars, i );
            else
                Kit_TruthCofactor0( pCo11, nVars, i );
        }

    // derive the functions by composing them with the new variable (iVarReused)
    Kit_TruthMuxVar( pCo0, pCo00, pCo01, nVars, iVarReused );
    Kit_TruthMuxVar( pCo1, pCo10, pCo11, nVars, iVarReused );
//Kit_DsdPrintFromTruth( pCo0, nVars );
//Kit_DsdPrintFromTruth( pCo1, nVars );

    // derive the composition function
    Kit_TruthMuxVar( pCo , pCo0 , pCo1 , nVars, iVar );

    // process the decomposed function
    pNtkDec = Kit_DsdDecompose( pDec, nVars );
    pNtkComp = Kit_DsdDecompose( pCo, nVars );
//Kit_DsdPrint( stdout, pNtkDec );
//Kit_DsdPrint( stdout, pNtkComp );
//printf( "cofactored variable %c\n", 'a' + iVar );
//printf( "reused variable %c\n", 'a' + iVarReused );

    ppLeaves[iVarReused] = Lpk_MapTree_rec( p, pNtkDec, ppLeaves, pNtkDec->Root, NULL );
    pObjNew = Lpk_MapTree_rec( p, pNtkComp, ppLeaves, pNtkComp->Root, NULL );

    Kit_DsdNtkFree( pNtkDec );
    Kit_DsdNtkFree( pNtkComp );
    return pObjNew;
}

unsigned Lpk_MapSuppRedDecSelect	(	Lpk_Man_t *	p,
		unsigned *	pTruth,
		int	nVars,
		int *	piVar,
		int *	piVarReused
	)

Function*************************************************************

Synopsis [Evaluates the cofactors.]

Description []

SideEffects []

SeeAlso []

Definition at line 323 of file lpkSets.c.

{
    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 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 0 );
    unsigned * pCof1 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 1 );
    int nSets, i, SizeMax;//, SRedMax;
    unsigned Entry;
    int fVerbose = p->pPars->fVeryVerbose;
//    int fVerbose = 0;

    // collect decomposable subsets for each pair of cofactors
    if ( fVerbose )
    {
        printf( "\nExploring support-reducing bound-sets of function:\n" );
        Kit_DsdPrintFromTruth( pTruth, nVars );
    }
    nSets = 0;
    for ( i = 0; i < nVars; i++ )
    {
        if ( fVerbose )
        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 );
        if ( fVerbose )
        Kit_DsdPrint( stdout, ppNtks[0] );
        if ( fVerbose )
        Kit_DsdPrint( stdout, ppNtks[1] );
        // compute subsets
        Lpk_ComputeSets( ppNtks[0], vSets0 );
        Lpk_ComputeSets( ppNtks[1], vSets1 );
        // print subsets
        if ( fVerbose )
        Lpk_PrintSets( vSets0 );
        if ( fVerbose )
        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
    if ( fVerbose )
    printf( "\n" );
    if ( fVerbose )
    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 the best is not choosen, select the one with largest reduction
    SRedMax = 0;
    if ( pSetBest == NULL )
    {
        for ( i = 0; i < nSets; i++ )
        {
            pSet = pStore + i;
            if ( SRedMax < pSet->SRed )
            {
                pSetBest = pSet;
                SRedMax = pSet->SRed;
            }
        }
    }
*/
    if ( pSetBest == NULL )
    {
        if ( fVerbose )
        printf( "Could not select a subset.\n" );
        return 0;
    }
    else
    {
        if ( fVerbose )
        printf( "Selected the following subset:\n" );
        if ( fVerbose )
        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);
}

If_Obj_t* Lpk_MapTree_rec	(	Lpk_Man_t *	p,
		Kit_DsdNtk_t *	pNtk,
		If_Obj_t **	ppLeaves,
		int	iLit,
		If_Obj_t *	pResult
	)

Function*************************************************************

Synopsis [Prepares the mapping manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 110 of file lpkMap.c.

{
    Kit_DsdObj_t * pObj;
    If_Obj_t * pObjNew = NULL, * pObjNew2 = NULL, * pFansNew[16];
    unsigned i, iLitFanin;

    assert( iLit >= 0 );

    // consider the case of a gate
    pObj = Kit_DsdNtkObj( pNtk, Abc_Lit2Var(iLit) );
    if ( pObj == NULL )
    {
        pObjNew = ppLeaves[Abc_Lit2Var(iLit)];
        return If_NotCond( pObjNew, Abc_LitIsCompl(iLit) );
    }
    if ( pObj->Type == KIT_DSD_CONST1 )
    {
        return If_NotCond( If_ManConst1(p->pIfMan), Abc_LitIsCompl(iLit) );
    }
    if ( pObj->Type == KIT_DSD_VAR )
    {
        pObjNew = ppLeaves[Abc_Lit2Var(pObj->pFans[0])];
        return If_NotCond( pObjNew, Abc_LitIsCompl(iLit) ^ Abc_LitIsCompl(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, Abc_LitIsCompl(iLit) );
    }
    if ( pObj->Type == KIT_DSD_XOR )
    {
        int fCompl = Abc_LitIsCompl(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, Abc_LitIsCompl(iLit) );
    }
*/
/*
    if ( (int)pObj->nFans > p->pPars->nLutSize )
    {
        pObjNew2 = Lpk_MapTreeMux_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
//        if ( pObjNew2 )
//            return If_NotCond( pObjNew2, Abc_LitIsCompl(iLit) );
    }
*/

    // find best cofactoring variable
    if ( p->pPars->nVarsShared > 0 && (int)pObj->nFans > p->pPars->nLutSize )
    {
        pObjNew2 = Lpk_MapSuppRedDec_rec( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );
        if ( pObjNew2 )
            return If_NotCond( pObjNew2, Abc_LitIsCompl(iLit) );
    }

    pObjNew = Lpk_MapPrime( p, Kit_DsdObjTruth(pObj), pObj->nFans, pFansNew );

    // add choice
    if ( pObjNew && pObjNew2 )
    {
        If_ObjSetChoice( If_Regular(pObjNew), If_Regular(pObjNew2) );
        If_ManCreateChoice( p->pIfMan, If_Regular(pObjNew) );
    }
    return If_NotCond( pObjNew, Abc_LitIsCompl(iLit) );
}

If_Obj_t* Lpk_MapTreeMulti	(	Lpk_Man_t *	p,
		unsigned *	pTruth,
		int	nVars,
		If_Obj_t **	ppLeaves
	)

Function*************************************************************

Synopsis [Prepares the mapping manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 347 of file lpkMulti.c.

{
    static int 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,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0},
      {0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0}
    };
    int fVerbose = p->pPars->fVeryVerbose;

    Counter++;
//    printf( "Run %d.\n", Counter );

    // allocate storage for cofactors
    nMemSize = Kit_TruthWordNum(nVars);
    ppCofs[0][0] = ABC_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" );

    // 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] = Abc_LitIsCompl(ppNtks[i]->Root)? -2: -1;
        else if ( pRoot->Type == KIT_DSD_VAR )
            piLits[i] = Abc_LitNotCond( pRoot->pFans[0], Abc_LitIsCompl(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] );
    ABC_FREE( ppCofs[0][0] );

    return pResult;
}

If_Obj_t* Lpk_MapTreeMux_rec	(	Lpk_Man_t *	p,
		unsigned *	pTruth,
		int	nVars,
		If_Obj_t **	ppLeaves
	)

Function*************************************************************

Synopsis [Maps the function by the best cofactoring.]

Description []

SideEffects []

SeeAlso []

Definition at line 89 of file lpkMux.c.

{
    unsigned * pCof0 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 0 );
    unsigned * pCof1 = (unsigned *)Vec_PtrEntry( p->vTtNodes, 1 );
    If_Obj_t * pObj0, * pObj1;
    Kit_DsdNtk_t * ppNtks[2];
    int iBestVar;
    assert( nVars > 3 );
    p->fCalledOnce = 1;
    // cofactor w.r.t. the best variable
    iBestVar = Lpk_MapTreeBestCofVar( p, pTruth, nVars, pCof0, pCof1 );
    if ( iBestVar == -1 )
        return NULL;
    // decompose the functions
    ppNtks[0] = Kit_DsdDecompose( pCof0, nVars );
    ppNtks[1] = Kit_DsdDecompose( pCof1, nVars );
    if ( p->pPars->fVeryVerbose )
    {
        printf( "Cofactoring w.r.t. var %c (%d -> %d+%d supp vars):\n", 
            'a'+iBestVar, nVars, Kit_TruthSupportSize(pCof0, nVars), Kit_TruthSupportSize(pCof1, nVars) );
        Kit_DsdPrintExpanded( ppNtks[0] );
        Kit_DsdPrintExpanded( ppNtks[1] );
    }
    // map the DSD structures
    pObj0 = Lpk_MapTree_rec( p, ppNtks[0], ppLeaves, ppNtks[0]->Root, NULL );
    pObj1 = Lpk_MapTree_rec( p, ppNtks[1], ppLeaves, ppNtks[1]->Root, NULL );
    Kit_DsdNtkFree( ppNtks[0] );
    Kit_DsdNtkFree( ppNtks[1] );
    return If_ManCreateMux( p->pIfMan, pObj0, pObj1, ppLeaves[iBestVar] );
}

Lpk_Res_t* Lpk_MuxAnalize	(	Lpk_Man_t *	pMan,
		Lpk_Fun_t *	p
	)

DECLARATIONS ///.

CFile****************************************************************

FileName [lpkAbcMux.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Fast Boolean matching for LUT structures.]

Synopsis [LUT-decomposition based on recursive 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

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis [Checks the possibility of MUX decomposition.]

Description [Returns the best variable to use for MUX decomposition.]

SideEffects []

SeeAlso []

Definition at line 45 of file lpkAbcMux.c.

{
    static Lpk_Res_t Res, * pRes = &Res;
    int nSuppSize0, nSuppSize1, nSuppSizeS, nSuppSizeL;
    int Var, Area, Polarity, Delay, Delay0, Delay1, DelayA, DelayB;
    memset( pRes, 0, sizeof(Lpk_Res_t) );
    assert( p->uSupp == Kit_BitMask(p->nVars) );
    assert( p->fSupports );
    // derive the delay and area after MUX-decomp with each var - and find the best var
    pRes->Variable = -1;
    Lpk_SuppForEachVar( p->uSupp, Var )
    {
        nSuppSize0 = Kit_WordCountOnes(p->puSupps[2*Var+0]);
        nSuppSize1 = Kit_WordCountOnes(p->puSupps[2*Var+1]);
        assert( nSuppSize0 < (int)p->nVars );
        assert( nSuppSize1 < (int)p->nVars );
        if ( nSuppSize0 < 1 || nSuppSize1 < 1 )
            continue;
//printf( "%d %d    ", nSuppSize0, nSuppSize1 );
        if ( nSuppSize0 <= (int)p->nLutK - 2 && nSuppSize1 <= (int)p->nLutK - 2 )
        {
            // include cof var into 0-block
            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<<Var), p->pDelays );
            DelayB = Lpk_SuppDelay( p->puSupps[2*Var+1]           , p->pDelays );
            Delay0 = Abc_MaxInt( DelayA, DelayB + 1 );
            // include cof var into 1-block
            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<<Var), p->pDelays );
            DelayB = Lpk_SuppDelay( p->puSupps[2*Var+0]           , p->pDelays );
            Delay1 = Abc_MaxInt( DelayA, DelayB + 1 );
            // get the best delay
            Delay = Abc_MinInt( Delay0, Delay1 );
            Area = 2;
            Polarity = (int)(Delay == Delay1);
        }
        else if ( nSuppSize0 <= (int)p->nLutK - 2 )
        {
            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<<Var), p->pDelays );
            DelayB = Lpk_SuppDelay( p->puSupps[2*Var+1]           , p->pDelays );
            Delay = Abc_MaxInt( DelayA, DelayB + 1 );
            Area = 1 + Lpk_LutNumLuts( nSuppSize1, p->nLutK );
            Polarity = 0;
        }
        else if ( nSuppSize1 <= (int)p->nLutK - 2 )
        {
            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<<Var), p->pDelays );
            DelayB = Lpk_SuppDelay( p->puSupps[2*Var+0]           , p->pDelays );
            Delay = Abc_MaxInt( DelayA, DelayB + 1 );
            Area = 1 + Lpk_LutNumLuts( nSuppSize0, p->nLutK );
            Polarity = 1;
        }
        else if ( nSuppSize0 <= (int)p->nLutK )
        {
            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<<Var), p->pDelays );
            DelayB = Lpk_SuppDelay( p->puSupps[2*Var+0]           , p->pDelays );
            Delay = Abc_MaxInt( DelayA, DelayB + 1 );
            Area = 1 + Lpk_LutNumLuts( nSuppSize1+2, p->nLutK );
            Polarity = 1;
        }
        else if ( nSuppSize1 <= (int)p->nLutK )
        {
            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<<Var), p->pDelays );
            DelayB = Lpk_SuppDelay( p->puSupps[2*Var+1]           , p->pDelays );
            Delay = Abc_MaxInt( DelayA, DelayB + 1 );
            Area = 1 + Lpk_LutNumLuts( nSuppSize0+2, p->nLutK );
            Polarity = 0;
        }
        else
        {
            // include cof var into 0-block
            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+0] | (1<<Var), p->pDelays );
            DelayB = Lpk_SuppDelay( p->puSupps[2*Var+1]           , p->pDelays );
            Delay0 = Abc_MaxInt( DelayA, DelayB + 1 );
            // include cof var into 1-block
            DelayA = Lpk_SuppDelay( p->puSupps[2*Var+1] | (1<<Var), p->pDelays );
            DelayB = Lpk_SuppDelay( p->puSupps[2*Var+0]           , p->pDelays );
            Delay1 = Abc_MaxInt( DelayA, DelayB + 1 );
            // get the best delay
            Delay = Abc_MinInt( 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)(Delay == Delay1);
        }
        // find the best variable
        if ( Delay > (int)p->nDelayLim )
            continue;
        if ( Area > (int)p->nAreaLim )
            continue;
        nSuppSizeS = Abc_MinInt( nSuppSize0 + 2 *!Polarity, nSuppSize1 + 2 * Polarity );
        nSuppSizeL = Abc_MaxInt( nSuppSize0 + 2 *!Polarity, nSuppSize1 + 2 * Polarity );
        if ( nSuppSizeL > (int)p->nVars )
            continue;
        if ( pRes->Variable == -1 || pRes->AreaEst > Area || 
            (pRes->AreaEst == Area && pRes->nSuppSizeS + pRes->nSuppSizeL > nSuppSizeS + nSuppSizeL) || 
            (pRes->AreaEst == Area && pRes->nSuppSizeS + pRes->nSuppSizeL == nSuppSizeS + nSuppSizeL && pRes->DelayEst > Delay) )
        {
            pRes->Variable = Var;
            pRes->Polarity = Polarity;
            pRes->AreaEst  = Area;
            pRes->DelayEst = Delay;
            pRes->nSuppSizeS = nSuppSizeS;
            pRes->nSuppSizeL = nSuppSizeL;
        }
    }
    return pRes->Variable == -1 ? NULL : pRes;
}

Lpk_Fun_t* Lpk_MuxSplit	(	Lpk_Man_t *	pMan,
		Lpk_Fun_t *	p,
		int	Var,
		int	Pol
	)

Function*************************************************************

Synopsis [Transforms the function decomposed by the MUX decomposition.]

Description [Returns the best variable to use for MUX decomposition.]

SideEffects []

SeeAlso []

Definition at line 164 of file lpkAbcMux.c.

{
    Lpk_Fun_t * pNew;
    unsigned * pTruth  = Lpk_FunTruth( p, 0 );
    unsigned * pTruth0 = Lpk_FunTruth( p, 1 );
    unsigned * pTruth1 = Lpk_FunTruth( p, 2 );
//    unsigned uSupp;
    int iVarVac; 
    assert( Var >= 0 && Var < (int)p->nVars );
    assert( p->nAreaLim >= 2 );
    assert( p->uSupp == Kit_BitMask(p->nVars) );
    Kit_TruthCofactor0New( pTruth0, pTruth, p->nVars, Var );
    Kit_TruthCofactor1New( pTruth1, pTruth, p->nVars, Var );
/*
uSupp = Kit_TruthSupport( pTruth, p->nVars );
Extra_PrintBinary( stdout, &uSupp, 16 ); printf( "\n" );
uSupp = Kit_TruthSupport( pTruth0, p->nVars );
Extra_PrintBinary( stdout, &uSupp, 16 ); printf( "\n" );
uSupp = Kit_TruthSupport( pTruth1, p->nVars );
Extra_PrintBinary( stdout, &uSupp, 16 ); printf( "\n\n" );
*/
    // derive the new component
    pNew = Lpk_FunDup( p, Pol ? pTruth0 : pTruth1 );
    // update the support of the old component
    p->uSupp  = Kit_TruthSupport( Pol ? pTruth1 : pTruth0, p->nVars );
    p->uSupp |= (1 << Var);
    // update the truth table of the old component
    iVarVac = Kit_WordFindFirstBit( ~p->uSupp );
    assert( iVarVac < (int)p->nVars );
    p->uSupp |= (1 << iVarVac);
    Kit_TruthIthVar( pTruth, p->nVars, iVarVac );
    if ( Pol )
        Kit_TruthMuxVar( pTruth, pTruth, pTruth1, p->nVars, Var );
    else
        Kit_TruthMuxVar( pTruth, pTruth0, pTruth, p->nVars, Var );
    assert( p->uSupp == Kit_TruthSupport(pTruth, p->nVars) );
    // set the decomposed variable
    p->pFanins[iVarVac] = pNew->Id;
    p->pDelays[iVarVac] = p->nDelayLim - 1;
    // support minimize both
    p->fSupports = 0;
    Lpk_FunSuppMinimize( p );
    Lpk_FunSuppMinimize( pNew );
    // update delay and area requirements
    pNew->nDelayLim = p->nDelayLim - 1;
    if ( pNew->nVars <= pNew->nLutK )
    {
        pNew->nAreaLim = 1;
        p->nAreaLim = p->nAreaLim - 1;
    }
    else if ( p->nVars <= p->nLutK )
    {
        pNew->nAreaLim = p->nAreaLim - 1;
        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;
    }
    pNew->fMark = 1;
    return pNew;
}

int Lpk_NodeCuts

(

Lpk_Man_t *

p

)

Function*************************************************************

Synopsis [Computes the set of all cuts.]

Description []

SideEffects []

SeeAlso []

Definition at line 588 of file lpkCut.c.

{
    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 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 = Lpk_LutNumLuts( pCut->nLeaves, p->pPars->nLutSize ); 
//        pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup - 1) / pCut->nLuts; //p->pPars->nLutsMax;
        pCut->Weight = (float)1.0 * (pCut->nNodes - pCut->nNodesDup) / pCut->nLuts; //p->pPars->nLutsMax;
        if ( pCut->Weight <= 1.001 )
//        if ( pCut->Weight <= 0.999 )
            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 - 0.001 )
                continue;
            Temp = p->pEvals[i];
            p->pEvals[i] = p->pEvals[i+1];
            p->pEvals[i+1] = Temp;
            fChanges = 1;
        }
    } while ( fChanges );
/*
    for ( i = 0; i < p->nEvals; i++ )
    {
        pCut = p->pCuts + p->pEvals[i];
        printf( "Cut %3d : W = %5.2f.\n", i, pCut->Weight );
    }
    printf( "\n" );
*/
    return 1;
}

int Lpk_SuppDelay	(	unsigned	uSupp,
		char *	pDelays
	)

Function*************************************************************

Synopsis [Get the delay of the bound set.]

Description []

SideEffects []

SeeAlso []

Definition at line 215 of file lpkAbcUtil.c.

{
    int Delay, Var;
    Delay = 0;
    Lpk_SuppForEachVar( uSupp, Var )
        Delay = Abc_MaxInt( Delay, pDelays[Var] );
    return Delay + 1;
}

int Lpk_SuppToVars	(	unsigned	uBoundSet,
		char *	pVars
	)

Function*************************************************************

Synopsis [Converts support into variables.]

Description []

SideEffects []

SeeAlso []

Definition at line 235 of file lpkAbcUtil.c.

{
    int i, nVars = 0;
    Lpk_SuppForEachVar( uBoundSet, i )
        pVars[nVars++] = i;
    return nVars;
}