abcCascade.c File Reference

#include "base/abc/abc.h"
#include "bdd/reo/reo.h"
#include "misc/extra/extraBdd.h"

Go to the source code of this file.

Macros
#define	BDD_FUNC_MAX   256
	DECLARATIONS ///. More...

Functions
DdNode *	Abc_ConvertSopToBdd (DdManager *dd, char *pSop, DdNode **pbVars)
	FUNCTION DEFINITIONS ///. More...
DdNode *	Abc_ResBuildBdd (Abc_Ntk_t *pNtk, DdManager *dd)
	FUNCTION DEFINITIONS ///. More...
void	Abc_ResStartPart (int nInputs, unsigned uParts[], int nParts)
void	Abc_ResStartPart2 (int nInputs, unsigned uParts[], int nParts)
int	Abc_ResCheckUnique (char Pats[], int nPats, int pat)
int	Abc_ResCheckNonStrict (char Pattern[], int nVars, int nBits)
int	Abc_ResCofCount (DdManager *dd, DdNode *bFunc, unsigned uMask, int *pCheck)
int	Abc_ResCost (DdManager *dd, DdNode *bFunc, unsigned uMask, int *pnCofs, int *pCheck)
int	Abc_ResMigrate (DdManager *dd, DdNode *bFunc, int nInputs, unsigned uParts[], int iPart1, int iPart2)
void	Abc_ResPrint (DdManager *dd, DdNode *bFunc, int nInputs, unsigned uParts[], int nParts)
void	Abc_ResPrintAllCofs (DdManager *dd, DdNode *bFunc, int nInputs, int nCofMax)
void	Abc_ResSwapRandom (DdManager *dd, DdNode *bFunc, int nInputs, unsigned uParts[], int nParts, int nTimes)
void	Abc_ResPartition (DdManager *dd, DdNode *bFunc, int nInputs)
void	Abc_ResPartitionTest (Abc_Ntk_t *pNtk)
int	Abc_NtkBddCofCount (DdManager *dd, DdNode *bFunc, DdNode **pbVars, int nVars)
void	Abc_NtkExploreCofs2 (DdManager *dd, DdNode *bFunc, DdNode **pbVars, int nIns, int nLutSize)
void	Abc_NtkExploreCofs (DdManager *dd, DdNode *bFunc, DdNode **pbVars, int nIns, int nLutSize)
DdNode *	Abc_NtkBddFindAddConst (DdManager *dd, DdNode *bFunc, int nOuts)
DdNode *	Abc_NtkBddToAdd_rec (DdManager *dd, DdNode *bFunc, int nOuts, stmm_table *tTable, int fCompl)
DdNode *	Abc_NtkBddToAdd (DdManager *dd, DdNode *bFunc, int nOuts)
DdNode *	Abc_NtkAddToBdd_rec (DdManager *dd, DdNode *aFunc, int nIns, int nOuts, stmm_table *tTable)
DdNode *	Abc_NtkAddToBdd (DdManager *dd, DdNode *aFunc, int nIns, int nOuts)
DdNode *	Abc_NtkBddDecCharFunc (DdManager *dd, DdNode **pFuncs, int nOuts, int Mask, int nBits)
DdNode *	Abc_NtkBddDecTry (reo_man *pReo, DdManager *dd, DdNode **pFuncs, int nIns, int nOuts, int Mask, int nBits)
DdNode *	Abc_NtkBddDecInt (reo_man *pReo, DdManager *dd, DdNode **pFuncs, int nIns, int nOuts)
Abc_Ntk_t *	Abc_NtkCreateFromCharFunc (Abc_Ntk_t *pNtk, DdManager *dd, DdNode *bFunc)
Abc_Ntk_t *	Abc_NtkBddDec (Abc_Ntk_t *pNtk, int fVerbose)

Macro Definition Documentation

#define BDD_FUNC_MAX   256

DECLARATIONS ///.

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

FileName [abcCascade.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Network and node package.]

Synopsis [Collapsing the network into two-levels.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:

abcCollapse.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 31 of file abcCascade.c.

Function Documentation

DdNode* Abc_ConvertSopToBdd	(	DdManager *	dd,
		char *	pSop,
		DdNode **	pbVars
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Converts the node from SOP to BDD representation.]

Description []

SideEffects []

SeeAlso []

Definition at line 56 of file abcFunc.c.

{
    DdNode * bSum, * bCube, * bTemp, * bVar;
    char * pCube;
    int nVars, Value, v;

    // start the cover
    nVars = Abc_SopGetVarNum(pSop);
    bSum = Cudd_ReadLogicZero(dd);   Cudd_Ref( bSum );
    if ( Abc_SopIsExorType(pSop) )
    {
        for ( v = 0; v < nVars; v++ )
        {
            bSum  = Cudd_bddXor( dd, bTemp = bSum, pbVars? pbVars[v] : Cudd_bddIthVar(dd, v) );   Cudd_Ref( bSum );
            Cudd_RecursiveDeref( dd, bTemp );
        }
    }
    else
    {
        // check the logic function of the node
        Abc_SopForEachCube( pSop, nVars, pCube )
        {
            bCube = Cudd_ReadOne(dd);   Cudd_Ref( bCube );
            Abc_CubeForEachVar( pCube, Value, v )
            {
                if ( Value == '0' )
                    bVar = Cudd_Not( pbVars? pbVars[v] : Cudd_bddIthVar( dd, v ) );
                else if ( Value == '1' )
                    bVar = pbVars? pbVars[v] : Cudd_bddIthVar( dd, v );
                else
                    continue;
                bCube  = Cudd_bddAnd( dd, bTemp = bCube, bVar );   Cudd_Ref( bCube );
                Cudd_RecursiveDeref( dd, bTemp );
            }
            bSum = Cudd_bddOr( dd, bTemp = bSum, bCube );   
            Cudd_Ref( bSum );
            Cudd_RecursiveDeref( dd, bTemp );
            Cudd_RecursiveDeref( dd, bCube );
        }
    }
    // complement the result if necessary
    bSum = Cudd_NotCond( bSum, !Abc_SopGetPhase(pSop) );
    Cudd_Deref( bSum );
    return bSum;
}

DdNode* Abc_NtkAddToBdd	(	DdManager *	dd,
		DdNode *	aFunc,
		int	nIns,
		int	nOuts
	)

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

Synopsis [R]

Description []

SideEffects []

SeeAlso []

Definition at line 818 of file abcCascade.c.

{
    DdNode * bFunc, * bTemp, * aTemp;
    stmm_table * tTable;
    stmm_generator * gen;
    tTable = stmm_init_table( st__ptrcmp, st__ptrhash );
    bFunc = Abc_NtkAddToBdd_rec( dd, aFunc, nIns, nOuts, tTable );  
    stmm_foreach_item( tTable, gen, (char **)&aTemp, (char **)&bTemp )
        Cudd_RecursiveDeref( dd, bTemp );
    stmm_free_table( tTable );
    Cudd_Deref( bFunc );
    return bFunc;
}

DdNode* Abc_NtkAddToBdd_rec	(	DdManager *	dd,
		DdNode *	aFunc,
		int	nIns,
		int	nOuts,
		stmm_table *	tTable
	)

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

Synopsis [Recursively construct ADD for BDD.]

Description []

SideEffects []

SeeAlso []

Definition at line 785 of file abcCascade.c.

{
    DdNode * bFunc0, * bFunc1, * bFunc;
    DdNode ** ppSlot;
    assert( !Cudd_IsComplement(aFunc) );
    if ( stmm_find_or_add( tTable, (char *)aFunc, (char ***)&ppSlot ) )
        return *ppSlot;
    if ( Cudd_IsConstant(aFunc) )
    {
        assert( Cudd_ReadSize(dd) >= nIns + nOuts );
        bFunc  = Extra_bddBitsToCube( dd, (int)Cudd_V(aFunc), nOuts, dd->vars + nIns, 1 );  Cudd_Ref( bFunc );
    }
    else
    {
        assert( aFunc->index < nIns );
        bFunc0 = Abc_NtkAddToBdd_rec( dd, cuddE(aFunc), nIns, nOuts, tTable );
        bFunc1 = Abc_NtkAddToBdd_rec( dd, cuddT(aFunc), nIns, nOuts, tTable );                                                
        bFunc  = Cudd_bddIte( dd, Cudd_bddIthVar(dd, aFunc->index), bFunc1, bFunc0 );  Cudd_Ref( bFunc );
    }
    return (*ppSlot = bFunc);
}

int Abc_NtkBddCofCount	(	DdManager *	dd,
		DdNode *	bFunc,
		DdNode **	pbVars,
		int	nVars
	)

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

Synopsis [Compute the number of distinct cofactors in the BDD.]

Description []

SideEffects []

SeeAlso []

Definition at line 581 of file abcCascade.c.

{
    Vec_Ptr_t * vCofs;
    DdNode * bCof, * bCube;
    int i, Result;
    vCofs = Vec_PtrAlloc( 100 );
    for ( i = 0; i < (1 << nVars); i++ )
    {
        bCube = Extra_bddBitsToCube( dd, i, nVars, pbVars, 1 );  Cudd_Ref( bCube );
        bCof  = Cudd_Cofactor( dd, bFunc, bCube );               Cudd_Ref( bCof );
        Cudd_RecursiveDeref( dd, bCube );
        if ( Vec_PtrPushUnique( vCofs, bCof ) )
            Cudd_RecursiveDeref( dd, bCof );
    }
    Result = Vec_PtrSize( vCofs );
    Vec_PtrForEachEntry( DdNode *, vCofs, bCof, i )
        Cudd_RecursiveDeref( dd, bCof );
    Vec_PtrFree( vCofs );
    return Result;
}

Abc_Ntk_t* Abc_NtkBddDec	(	Abc_Ntk_t *	pNtk,
		int	fVerbose
	)

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

Synopsis [Evaluate Sasao's decomposition.]

Description []

SideEffects []

SeeAlso []

Definition at line 994 of file abcCascade.c.

{
    int nBddSizeMax   = 1000000;
    int fDropInternal =       0;
    int fReorder      =       1;
    Abc_Ntk_t * pNtkNew;
    reo_man * pReo;
    DdManager * dd;
    DdNode * pFuncs[BDD_FUNC_MAX];
    DdNode * bFunc;
    Abc_Obj_t * pNode;
    int i;
    assert( Abc_NtkIsStrash(pNtk) );
    assert( Abc_NtkCoNum(pNtk) <= BDD_FUNC_MAX );
    dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, nBddSizeMax, fDropInternal, fReorder, fVerbose );
    if ( dd == NULL )
    {
        Abc_Print( -1, "Construction of global BDDs has failed.\n" );
        return NULL;
    }
    // collect global BDDs
    Abc_NtkForEachCo( pNtk, pNode, i )
        pFuncs[i] = (DdNode *)Abc_ObjGlobalBdd(pNode);

    // create new variables at the bottom
    assert( dd->size == Abc_NtkCiNum(pNtk) );
    for ( i = 0; i < Abc_NtkCoNum(pNtk); i++ )
        Cudd_addNewVarAtLevel( dd, dd->size );

    // prepare reordering engine
    pReo = Extra_ReorderInit( Abc_NtkCiNum(pNtk), 1000 );
    Extra_ReorderSetMinimizationType( pReo, REO_MINIMIZE_WIDTH );
    Extra_ReorderSetVerification( pReo, 1 );
    Extra_ReorderSetVerbosity( pReo, 1 );

    // derive characteristic function
    bFunc = Abc_NtkBddDecInt( pReo, dd, pFuncs, Abc_NtkCiNum(pNtk), Abc_NtkCoNum(pNtk) );  Cudd_Ref( bFunc );
    Extra_ReorderQuit( pReo );

Abc_NtkExploreCofs( dd, bFunc, dd->vars, Abc_NtkCiNum(pNtk), 6 );

    // create new network
//    pNtkNew = Abc_NtkCreateFromCharFunc( pNtk, dd, bFunc );
    pNtkNew = Abc_NtkDup( pNtk );

    // cleanup
    Cudd_RecursiveDeref( dd, bFunc );
    Abc_NtkFreeGlobalBdds( pNtk, 1 );
    return pNtkNew;
}

DdNode* Abc_NtkBddDecCharFunc	(	DdManager *	dd,
		DdNode **	pFuncs,
		int	nOuts,
		int	Mask,
		int	nBits
	)

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

Synopsis [Computes the characteristic function.]

Description []

SideEffects []

SeeAlso []

Definition at line 843 of file abcCascade.c.

{
    DdNode * bFunc, * bTemp, * bExor, * bVar;
    int i, Count = 0;
    bFunc = Cudd_ReadOne( dd );  Cudd_Ref( bFunc );
    for ( i = 0; i < nOuts; i++ )
    {
        if ( (Mask & (1 << i)) == 0 )
            continue;
        Count++;
        bVar  = Cudd_bddIthVar( dd, dd->size - nOuts + i );
        bExor = Cudd_bddXor( dd, pFuncs[i], bVar );                  Cudd_Ref( bExor );
        bFunc = Cudd_bddAnd( dd, bTemp = bFunc, Cudd_Not(bExor) );   Cudd_Ref( bFunc );
        Cudd_RecursiveDeref( dd, bTemp );
        Cudd_RecursiveDeref( dd, bExor );
    }
    Cudd_Deref( bFunc );
    assert( Count == nBits );
    return bFunc;
}

DdNode* Abc_NtkBddDecInt	(	reo_man *	pReo,
		DdManager *	dd,
		DdNode **	pFuncs,
		int	nIns,
		int	nOuts
	)

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

Synopsis [Evaluate Sasao's decomposition.]

Description []

SideEffects []

SeeAlso []

Definition at line 919 of file abcCascade.c.

{
/*
    int i, k;
    for ( i = 1; i <= nOuts; i++ )
    {
        for ( k = 0; k < (1<<nOuts); k++ )
            if ( Extra_WordCountOnes(k) == i )
            {
                Extra_PrintBinary( stdout, (unsigned *)&k, nOuts );
                Abc_NtkBddDecTry( pReo, dd, pFuncs, nOuts, k, i );
                printf( "\n" );
            }
    }
*/
    return Abc_NtkBddDecTry( pReo, dd, pFuncs, nIns, nOuts, ~(1<<(32-nOuts)), nOuts );

}

DdNode* Abc_NtkBddDecTry	(	reo_man *	pReo,
		DdManager *	dd,
		DdNode **	pFuncs,
		int	nIns,
		int	nOuts,
		int	Mask,
		int	nBits
	)

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

Synopsis [Evaluate Sasao's decomposition.]

Description []

SideEffects []

SeeAlso []

Definition at line 875 of file abcCascade.c.

{
//    int fReorder = 0;
    DdNode * bFunc;//, * aFunc, * aFuncNew;
    // derive the characteristic function
    bFunc = Abc_NtkBddDecCharFunc( dd, pFuncs, nOuts, Mask, nBits );    Cudd_Ref( bFunc );
/*
    // transfer to ADD
    aFunc = Abc_NtkBddToAdd( dd, bFunc, nOuts );                        Cudd_Ref( aFunc );
    Cudd_RecursiveDeref( dd, bFunc );
//Abc_NodeShowBddOne( dd, aFunc );

    // perform reordering for BDD width
    if ( fReorder )
    {
        aFuncNew = Extra_Reorder( pReo, dd, aFunc, NULL );              Cudd_Ref( aFuncNew );
        printf( "Before = %d.  After = %d.\n", Cudd_DagSize(aFunc), Cudd_DagSize(aFuncNew) );
        Cudd_RecursiveDeref( dd, aFunc );
    }
    else
        aFuncNew = aFunc;

    // get back to BDD
    bFunc = Abc_NtkAddToBdd( dd, aFuncNew, nIns, nOuts );  Cudd_Ref( bFunc );
    Cudd_RecursiveDeref( dd, aFuncNew );
//Abc_NodeShowBddOne( dd, bFunc );
    // print the result
//    reoProfileWidthPrint( pReo );
*/
    Cudd_Deref( bFunc );
    return bFunc;
}

DdNode* Abc_NtkBddFindAddConst	(	DdManager *	dd,
		DdNode *	bFunc,
		int	nOuts
	)

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

Synopsis [Find the constant node corresponding to the encoded output value.]

Description []

SideEffects []

SeeAlso []

Definition at line 686 of file abcCascade.c.

{
    int i, TermMask = 0;
    DdNode * bFunc0, * bFunc1, * bConst0, * bConst1;
    bConst0 = Cudd_ReadLogicZero( dd );
    bConst1 = Cudd_ReadOne( dd );
    for ( i = 0; i < nOuts; i++ )
    {
        if ( Cudd_IsComplement(bFunc) )
        {
            bFunc0 = Cudd_Not(Cudd_E(bFunc));
            bFunc1 = Cudd_Not(Cudd_T(bFunc));
        }
        else
        {
            bFunc0 = Cudd_E(bFunc);
            bFunc1 = Cudd_T(bFunc);
        }
        assert( bFunc0 == bConst0 || bFunc1 == bConst0 );
        if ( bFunc0 == bConst0 )
        {
            TermMask ^= (1 << i);
            bFunc = bFunc1;
        }
        else
            bFunc = bFunc0;
    }
    assert( bFunc == bConst1 );
    return Cudd_addConst( dd, TermMask );
}

DdNode* Abc_NtkBddToAdd	(	DdManager *	dd,
		DdNode *	bFunc,
		int	nOuts
	)

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

Synopsis [R]

Description []

SideEffects []

SeeAlso []

Definition at line 760 of file abcCascade.c.

{
    DdNode * aFunc, * aTemp, * bTemp;
    stmm_table * tTable;
    stmm_generator * gen;
    tTable = stmm_init_table( st__ptrcmp, st__ptrhash );
    aFunc = Abc_NtkBddToAdd_rec( dd, Cudd_Regular(bFunc), nOuts, tTable, Cudd_IsComplement(bFunc) );  
    stmm_foreach_item( tTable, gen, (char **)&bTemp, (char **)&aTemp )
        Cudd_RecursiveDeref( dd, aTemp );
    stmm_free_table( tTable );
    Cudd_Deref( aFunc );
    return aFunc;
}

DdNode* Abc_NtkBddToAdd_rec	(	DdManager *	dd,
		DdNode *	bFunc,
		int	nOuts,
		stmm_table *	tTable,
		int	fCompl
	)

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

Synopsis [Recursively construct ADD for BDD.]

Description []

SideEffects []

SeeAlso []

Definition at line 728 of file abcCascade.c.

{
    DdNode * aFunc0, * aFunc1, * aFunc;
    DdNode ** ppSlot;
    assert( !Cudd_IsComplement(bFunc) );
    if ( stmm_find_or_add( tTable, (char *)bFunc, (char ***)&ppSlot ) )
        return *ppSlot;
    if ( (int)bFunc->index >= Cudd_ReadSize(dd) - nOuts )
    {
        assert( Cudd_ReadPerm(dd, bFunc->index) >= Cudd_ReadSize(dd) - nOuts );
        aFunc = Abc_NtkBddFindAddConst( dd, Cudd_NotCond(bFunc, fCompl), nOuts ); Cudd_Ref( aFunc );
    }
    else
    {
        aFunc0 = Abc_NtkBddToAdd_rec( dd, Cudd_Regular(cuddE(bFunc)), nOuts, tTable, fCompl ^ Cudd_IsComplement(cuddE(bFunc)) );
        aFunc1 = Abc_NtkBddToAdd_rec( dd, cuddT(bFunc), nOuts, tTable, fCompl );                                                
        aFunc  = Cudd_addIte( dd, Cudd_addIthVar(dd, bFunc->index), aFunc1, aFunc0 );  Cudd_Ref( aFunc );
    }
    return (*ppSlot = aFunc);
}

Abc_Ntk_t* Abc_NtkCreateFromCharFunc	(	Abc_Ntk_t *	pNtk,
		DdManager *	dd,
		DdNode *	bFunc
	)

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

Synopsis [Evaluate Sasao's decomposition.]

Description []

SideEffects []

SeeAlso []

Definition at line 949 of file abcCascade.c.

{    
    Abc_Ntk_t * pNtkNew; 
    Abc_Obj_t * pNode, * pNodeNew, * pNodePo;
    int i;
    // start the network
    pNtkNew = Abc_NtkAlloc( ABC_NTK_LOGIC, ABC_FUNC_BDD, 1 );
    pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
    // create inputs for CIs
    pNodeNew = Abc_NtkCreateNode( pNtkNew );
    Abc_NtkForEachCi( pNtk, pNode, i )
    {
        pNode->pCopy = Abc_NtkCreatePi( pNtkNew );
        Abc_ObjAddFanin( pNodeNew, pNode->pCopy );
        Abc_ObjAssignName( pNode->pCopy, Abc_ObjName(pNode), NULL );
    }
    // create inputs for COs
    Abc_NtkForEachCo( pNtk, pNode, i )
    {
        pNode->pCopy = Abc_NtkCreatePi( pNtkNew );
        Abc_ObjAddFanin( pNodeNew, pNode->pCopy );
        Abc_ObjAssignName( pNode->pCopy, Abc_ObjName(pNode), NULL );
    }
    // transfer BDD
    pNodeNew->pData = Extra_TransferLevelByLevel( dd, (DdManager *)pNtkNew->pManFunc, bFunc ); Cudd_Ref( (DdNode *)pNodeNew->pData );
    // transfer BDD into to be the local function
    pNodePo = Abc_NtkCreatePo( pNtkNew );
    Abc_ObjAddFanin( pNodePo, pNodeNew );
    Abc_ObjAssignName( pNodePo, "out", NULL );
    if ( !Abc_NtkCheck( pNtkNew ) )
        fprintf( stdout, "Abc_NtkCreateFromCharFunc(): Network check has failed.\n" );
    return pNtkNew;
}

void Abc_NtkExploreCofs	(	DdManager *	dd,
		DdNode *	bFunc,
		DdNode **	pbVars,
		int	nIns,
		int	nLutSize
	)

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

Synopsis [Compute the number of distinct cofactors in the BDD.]

Description []

SideEffects []

SeeAlso []

Definition at line 632 of file abcCascade.c.

{
    DdManager * ddNew;
    DdNode * bFuncNew;
    DdNode * pbVarsNew[32];
    int i, k, c, nCofs, nBits;

    ddNew = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
    Cudd_ShuffleHeap( ddNew, dd->invperm );
    bFuncNew = Cudd_bddTransfer( dd, ddNew, bFunc );  Cudd_Ref( bFuncNew );

    for ( i = 0; i < (1 << nIns); i++ )
    {
        nBits = Extra_WordCountOnes(i);
        if ( nBits != nLutSize && nBits != nLutSize -1 && nBits != nLutSize -2  )
            continue;
        for ( c = k = 0; k < nIns; k++ )
        {
            if ( (i & (1 << k)) == 0 )
                continue;
//            pbVarsNew[c++] = pbVars[k];
            pbVarsNew[c++] = ddNew->vars[k];
        }
        nCofs = Abc_NtkBddCofCount(ddNew, bFuncNew, pbVarsNew, c);
        if ( nCofs > 8 )
            continue;

        for ( c = k = 0; k < nIns; k++ )
        {
            if ( (i & (1 << k)) == 0 )
            {
                printf( "-" );
                continue;
            }
            printf( "%c", k + 'a' );
        }
        printf( " : %2d\n", nCofs );
    }

    Cudd_RecursiveDeref( ddNew, bFuncNew );
    Extra_StopManager( ddNew );
}

void Abc_NtkExploreCofs2	(	DdManager *	dd,
		DdNode *	bFunc,
		DdNode **	pbVars,
		int	nIns,
		int	nLutSize
	)

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

Synopsis [Compute the number of distinct cofactors in the BDD.]

Description []

SideEffects []

SeeAlso []

Definition at line 613 of file abcCascade.c.

{
    int i;
    printf( "Inputs = %2d.  Nodes = %2d.  LutSize = %2d.\n", nIns, Cudd_DagSize(bFunc), nLutSize );
    for ( i = 0; i <= nIns - nLutSize; i++ )
        printf( "[%2d %2d] : %3d\n", i, i+nLutSize-1, Abc_NtkBddCofCount(dd, bFunc, dd->vars+i, nLutSize) );
}

DdNode* Abc_ResBuildBdd	(	Abc_Ntk_t *	pNtk,
		DdManager *	dd
	)

FUNCTION DEFINITIONS ///.

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

Synopsis [Derive BDD of the characteristic function.]

Description []

SideEffects []

SeeAlso []

Definition at line 51 of file abcCascade.c.

{
    Vec_Ptr_t * vNodes, * vBdds, * vLocals;
    Abc_Obj_t * pObj, * pFanin;
    DdNode * bFunc, * bPart, * bTemp, * bVar;
    int i, k;
    assert( Abc_NtkIsSopLogic(pNtk) );
    assert( Abc_NtkCoNum(pNtk) <= 3 );
    vBdds = Vec_PtrStart( Abc_NtkObjNumMax(pNtk) );
    Abc_NtkForEachCi( pNtk, pObj, i )
        Vec_PtrWriteEntry( vBdds, Abc_ObjId(pObj), Cudd_bddIthVar(dd, i) );
    // create internal node BDDs
    vNodes = Abc_NtkDfs( pNtk, 0 );
    vLocals = Vec_PtrAlloc( 6 );
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
    {
        if ( Abc_ObjFaninNum(pObj) == 0 )
        {
            bFunc = Cudd_NotCond( Cudd_ReadOne(dd), Abc_SopIsConst0((char *)pObj->pData) );  Cudd_Ref( bFunc );
            Vec_PtrWriteEntry( vBdds, Abc_ObjId(pObj), bFunc );
            continue;
        }
        Vec_PtrClear( vLocals );
        Abc_ObjForEachFanin( pObj, pFanin, k )
            Vec_PtrPush( vLocals, Vec_PtrEntry(vBdds, Abc_ObjId(pFanin)) );
        bFunc = Abc_ConvertSopToBdd( dd, (char *)pObj->pData, (DdNode **)Vec_PtrArray(vLocals) );  Cudd_Ref( bFunc );
        Vec_PtrWriteEntry( vBdds, Abc_ObjId(pObj), bFunc );
    }
    Vec_PtrFree( vLocals );
    // create char function
    bFunc = Cudd_ReadOne( dd );  Cudd_Ref( bFunc );
    Abc_NtkForEachCo( pNtk, pObj, i )
    {
        bVar  = Cudd_bddIthVar( dd, i + Abc_NtkCiNum(pNtk) );
        bTemp = (DdNode *)Vec_PtrEntry( vBdds, Abc_ObjFaninId0(pObj) );
        bPart = Cudd_bddXnor( dd, bTemp, bVar );          Cudd_Ref( bPart );
        bFunc = Cudd_bddAnd( dd, bTemp = bFunc, bPart );  Cudd_Ref( bFunc );
        Cudd_RecursiveDeref( dd, bTemp );
        Cudd_RecursiveDeref( dd, bPart );
    }
    // dereference
    Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
        Cudd_RecursiveDeref( dd, (DdNode *)Vec_PtrEntry(vBdds, Abc_ObjId(pObj)) );
    Vec_PtrFree( vBdds );
    Vec_PtrFree( vNodes );
    // reorder
    Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
    Cudd_Deref( bFunc );
    return bFunc;
}

int Abc_ResCheckNonStrict	(	char	Pattern[],
		int	nVars,
		int	nBits
	)

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

Synopsis [Check if pattern is decomposable with non-strict.]

Description []

SideEffects []

SeeAlso []

Definition at line 187 of file abcCascade.c.

{
    static char Pat0[256], Pat1[256];
    int v, m, nPats0, nPats1, nNumber = (1 << (nBits - 1));
    int Result = 0;
    for ( v = 0; v < nVars; v++ )
    {
        nPats0 = nPats1 = 0;
        for ( m = 0; m < (1<<nVars); m++ )
        {
            if ( (m & (1 << v)) == 0 )
            {
                if ( Abc_ResCheckUnique( Pat0, nPats0, Pattern[m] ) )
                {
                    Pat0[ nPats0++ ] = Pattern[m];
                    if ( nPats0 > nNumber )
                        break;
                }
            }
            else
            {
                if ( Abc_ResCheckUnique( Pat1, nPats1, Pattern[m] ) )
                {
                    Pat1[ nPats1++ ] = Pattern[m];
                    if ( nPats1 > nNumber )
                        break;
                }
            }
        }
        if ( m == (1<<nVars) )
            Result++;
    }
    return Result;
}

int Abc_ResCheckUnique	(	char	Pats[],
		int	nPats,
		int	pat
	)

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

Synopsis [Returns one if unique pattern.]

Description []

SideEffects []

SeeAlso []

Definition at line 167 of file abcCascade.c.

{
    int i;
    for ( i = 0; i < nPats; i++ )
        if ( Pats[i] == pat )
            return 0;
    return 1;
}

int Abc_ResCofCount	(	DdManager *	dd,
		DdNode *	bFunc,
		unsigned	uMask,
		int *	pCheck
	)

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

Synopsis [Compute the number of distinct cofactors in the BDD.]

Description []

SideEffects []

SeeAlso []

Definition at line 233 of file abcCascade.c.

{
    static char Pattern[256];
    DdNode * pbVars[32];
    Vec_Ptr_t * vCofs;
    DdNode * bCof, * bCube, * bTemp;
    int i, k, Result, nVars = 0;
    // collect variables
    for ( i = 0; i < 32; i++ )
        if ( uMask & (1 << i) )
            pbVars[nVars++] = dd->vars[i];
    assert( nVars <= 8 );
    // compute cofactors
    vCofs = Vec_PtrAlloc( 100 );
    for ( i = 0; i < (1 << nVars); i++ )
    {
        bCube = Extra_bddBitsToCube( dd, i, nVars, pbVars, 1 );  Cudd_Ref( bCube );
        bCof  = Cudd_Cofactor( dd, bFunc, bCube );               Cudd_Ref( bCof );
        Cudd_RecursiveDeref( dd, bCube );
        Vec_PtrForEachEntry( DdNode *, vCofs, bTemp, k )
            if ( bTemp == bCof )
                break;
        if ( k < Vec_PtrSize(vCofs) )
            Cudd_RecursiveDeref( dd, bCof );
        else
            Vec_PtrPush( vCofs, bCof );
        Pattern[i] = k;
    }
    Result = Vec_PtrSize( vCofs );
    Vec_PtrForEachEntry( DdNode *, vCofs, bCof, i )
        Cudd_RecursiveDeref( dd, bCof );
    Vec_PtrFree( vCofs );
    if ( pCheck )
    {
        *pCheck = Abc_ResCheckNonStrict( Pattern, nVars, Abc_Base2Log(Result) );
/*
        if ( *pCheck == 1 && nVars == 4 && Result == 8 )
        {
            for ( i = 0; i < (1 << nVars); i++ )
                printf( "%d ", Pattern[i] );
            i = 0;
        }
*/
    }
    return Result;
}

int Abc_ResCost	(	DdManager *	dd,
		DdNode *	bFunc,
		unsigned	uMask,
		int *	pnCofs,
		int *	pCheck
	)

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

Synopsis [Computes cost of the partition.]

Description []

SideEffects []

SeeAlso []

Definition at line 291 of file abcCascade.c.

{
    int nCofs = Abc_ResCofCount( dd, bFunc, uMask, pCheck );
    int n2Log = Abc_Base2Log( nCofs );
    if ( pnCofs ) *pnCofs = nCofs;
    return 10000 * n2Log + (nCofs - (1 << (n2Log-1))) * (nCofs - (1 << (n2Log-1)));
}

int Abc_ResMigrate	(	DdManager *	dd,
		DdNode *	bFunc,
		int	nInputs,
		unsigned	uParts[],
		int	iPart1,
		int	iPart2
	)

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

Synopsis [Migrates variables between the two groups.]

Description [Returns 1 if there is change.]

SideEffects []

SeeAlso []

Definition at line 310 of file abcCascade.c.

{
    unsigned uParts2[2] = { uParts[iPart1], uParts[iPart2] };
    int i, k, CostCur, CostBest, fChange = 0;
    assert( (uParts[iPart1] & uParts[iPart2]) == 0 );
    CostBest = Abc_ResCost( dd, bFunc, uParts[iPart1], NULL, NULL ) 
             + Abc_ResCost( dd, bFunc, uParts[iPart2], NULL, NULL );
    for ( i = 0; i < nInputs; i++ )
    if ( uParts[iPart1] & (1 << i) )
    {
        for ( k = 0; k < nInputs; k++ )
        if ( uParts[iPart2] & (1 << k) )
        {
            if ( i == k )
                continue;
            uParts[iPart1] ^= (1 << i) | (1 << k);
            uParts[iPart2] ^= (1 << i) | (1 << k);
            CostCur = Abc_ResCost( dd, bFunc, uParts[iPart1], NULL, NULL ) + Abc_ResCost( dd, bFunc, uParts[iPart2], NULL, NULL );
            if ( CostCur < CostBest )
            {
                CostCur    = CostBest;
                uParts2[0] = uParts[iPart1];
                uParts2[1] = uParts[iPart2];
                fChange = 1;
            }
            uParts[iPart1] ^= (1 << i) | (1 << k);
            uParts[iPart2] ^= (1 << i) | (1 << k);
        }
    }
    uParts[iPart1] = uParts2[0];
    uParts[iPart2] = uParts2[1];
    return fChange;
}

void Abc_ResPartition	(	DdManager *	dd,
		DdNode *	bFunc,
		int	nInputs
	)

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

Synopsis [Compute the number of distinct cofactors in the BDD.]

Description []

SideEffects []

SeeAlso []

Definition at line 450 of file abcCascade.c.

{
    int nIters = 5;
    unsigned uParts[10];
    int i, fChange = 1;
    int nSuppSize = Cudd_SupportSize( dd, bFunc );
    printf( "Ins =%3d. Outs =%2d. Nodes =%3d. Supp =%2d.\n", 
        nInputs, dd->size-nInputs, Cudd_DagSize(bFunc), nSuppSize );
//Abc_ResPrintAllCofs( dd, bFunc, nInputs, 4 );

    if ( nSuppSize <= 6 )
    {
        printf( "Support is less or equal than 6\n" );
        return;
    }
    if ( nInputs <= 12 )
    {
        Abc_ResStartPart( nInputs, uParts, 2 );
        Abc_ResPrint( dd, bFunc, nInputs, uParts, 2 );
        for ( i = 0; i < nIters; i++ )
        {
            if ( i ) 
            {
                printf( "Randomizing... \n" );
                Abc_ResSwapRandom( dd, bFunc, nInputs, uParts, 2, 20 );
                Abc_ResPrint( dd, bFunc, nInputs, uParts, 2 );
            }
            fChange = 1;
            while ( fChange )
            {
                fChange  = Abc_ResMigrate( dd, bFunc, nInputs, uParts, 0, 1 );
                Abc_ResPrint( dd, bFunc, nInputs, uParts, 2 );
            }
        }
    }
    else if ( nInputs > 12 && nInputs <= 18 )
    {
        Abc_ResStartPart( nInputs, uParts, 3 );
        Abc_ResPrint( dd, bFunc, nInputs, uParts, 3 );
        for ( i = 0; i < nIters; i++ )
        {
            if ( i ) 
            {
                printf( "Randomizing... \n" );
                Abc_ResSwapRandom( dd, bFunc, nInputs, uParts, 3, 20 );
                Abc_ResPrint( dd, bFunc, nInputs, uParts, 3 );
            }
            fChange = 1;
            while ( fChange )
            {
                fChange  = Abc_ResMigrate( dd, bFunc, nInputs, uParts, 0, 1 );
                Abc_ResPrint( dd, bFunc, nInputs, uParts, 3 );
                fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 0, 2 );
                Abc_ResPrint( dd, bFunc, nInputs, uParts, 3 );
                fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 1, 2 );
                Abc_ResPrint( dd, bFunc, nInputs, uParts, 3 );
            }
        }
    }
    else if ( nInputs > 18 && nInputs <= 24 )
    {
        Abc_ResStartPart( nInputs, uParts, 4 );
        Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
        for ( i = 0; i < nIters; i++ )
        {
            if ( i )
            {
                printf( "Randomizing... \n" );
                Abc_ResSwapRandom( dd, bFunc, nInputs, uParts, 4, 20 );
                Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
            }
            fChange = 1;
            while ( fChange )
            {
                fChange  = Abc_ResMigrate( dd, bFunc, nInputs, uParts, 0, 1 );
                Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
                fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 0, 2 );
                Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
                fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 0, 3 );
                Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
                fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 1, 2 );
                Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
                fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 1, 3 );
                Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
                fChange |= Abc_ResMigrate( dd, bFunc, nInputs, uParts, 2, 3 );
                Abc_ResPrint( dd, bFunc, nInputs, uParts, 4 );
            }
        }
    }
//    else assert( 0 );
}

void Abc_ResPartitionTest

(

Abc_Ntk_t *

pNtk

)

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

Synopsis [Compute the number of distinct cofactors in the BDD.]

Description []

SideEffects []

SeeAlso []

Definition at line 553 of file abcCascade.c.

{
    DdManager * dd;
    DdNode * bFunc;
    dd = Cudd_Init( Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
    bFunc = Abc_ResBuildBdd( pNtk, dd );   Cudd_Ref( bFunc );
    Abc_ResPartition( dd, bFunc, Abc_NtkCiNum(pNtk) );
    Cudd_RecursiveDeref( dd, bFunc );
    Extra_StopManager( dd );
}

void Abc_ResPrint	(	DdManager *	dd,
		DdNode *	bFunc,
		int	nInputs,
		unsigned	uParts[],
		int	nParts
	)

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

Synopsis [Migrates variables between the two groups.]

Description [Returns 1 if there is change.]

SideEffects []

SeeAlso []

Definition at line 355 of file abcCascade.c.

{
    int i, k, nCofs, Cost, CostAll = 0, fCheck;
    for ( i = 0; i < nParts; i++ )
    {
        Cost = Abc_ResCost( dd, bFunc, uParts[i], &nCofs, &fCheck );
        CostAll += Cost;
        for ( k = 0; k < nInputs; k++ )
            printf( "%c", (uParts[i] & (1 << k))? 'a' + k : '-' );
        printf( " %2d %d-%d %6d   ", nCofs, Abc_Base2Log(nCofs), fCheck, Cost );
    }
    printf( "%4d\n", CostAll );
}

void Abc_ResPrintAllCofs	(	DdManager *	dd,
		DdNode *	bFunc,
		int	nInputs,
		int	nCofMax
	)

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

Synopsis [PrintCompute the number of distinct cofactors in the BDD.]

Description []

SideEffects []

SeeAlso []

Definition at line 380 of file abcCascade.c.

{
    int i, k, nBits, nCofs, Cost, fCheck;
    for ( i = 0; i < (1<<nInputs); i++ )
    {
        nBits = Extra_WordCountOnes( i );
        if ( nBits < 3 || nBits > 6 )
            continue;
        Cost = Abc_ResCost( dd, bFunc, i, &nCofs, &fCheck );
        if ( nCofs > nCofMax )
            continue;
        for ( k = 0; k < nInputs; k++ )
            printf( "%c", (i & (1 << k))? 'a' + k : '-' );
        printf( "  n=%2d  c=%2d  l=%d-%d   %6d\n", 
            Extra_WordCountOnes(i), nCofs, Abc_Base2Log(nCofs), fCheck, Cost );
    }
}

void Abc_ResStartPart	(	int	nInputs,
		unsigned	uParts[],
		int	nParts
	)

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

Synopsis [Initializes variable partition.]

Description []

SideEffects []

SeeAlso []

Definition at line 113 of file abcCascade.c.

{
    int i, Group, Left, Shift = 0, Count = 0;
    Group = nInputs / nParts;
    Left  = nInputs % nParts;
    for ( i = 0; i < Left; i++ )
    {
        uParts[i] = (~((~0) << (Group+1))) << Shift;
        Shift += Group+1;
    }
    for (      ; i < nParts; i++ )
    {
        uParts[i] = (~((~0) << Group)) << Shift;
        Shift += Group;
    }
    for ( i = 0; i < nParts; i++ )
        Count += Extra_WordCountOnes( uParts[i] );
    assert( Count == nInputs );
}

void Abc_ResStartPart2	(	int	nInputs,
		unsigned	uParts[],
		int	nParts
	)

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

Synopsis [Initializes variable partition.]

Description []

SideEffects []

SeeAlso []

Definition at line 144 of file abcCascade.c.

{
    int i, Count = 0;
    for ( i = 0; i < nParts; i++ )
        uParts[i] = 0;
    for ( i = 0; i < nInputs; i++ )
        uParts[i % nParts] |= (1 << i);
    for ( i = 0; i < nParts; i++ )
        Count += Extra_WordCountOnes( uParts[i] );
    assert( Count == nInputs );
}

void Abc_ResSwapRandom	(	DdManager *	dd,
		DdNode *	bFunc,
		int	nInputs,
		unsigned	uParts[],
		int	nParts,
		int	nTimes
	)

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

Synopsis [Compute the number of distinct cofactors in the BDD.]

Description []

SideEffects []

SeeAlso []

Definition at line 409 of file abcCascade.c.

{
    int i, k, n, iPart1, iPart2;
    for ( n = 0; n < nTimes; )
    {
        // get the vars
        i = k = 0;
        while ( i == k )
        {
            i = rand() % nInputs;
            k = rand() % nInputs;
        }
        // find the groups
        for ( iPart1 = 0; iPart1 < nParts; iPart1++ )
            if ( uParts[iPart1] & (1 << i) )
                break;
        for ( iPart2 = 0; iPart2 < nParts; iPart2++ )
            if ( uParts[iPart2] & (1 << k) )
                break;
        if ( iPart1 == iPart2 )
            continue;
        // swap the vars
        uParts[iPart1] ^= (1 << i) | (1 << k);
        uParts[iPart2] ^= (1 << i) | (1 << k);
        n++;
//printf( "   " );
//Abc_ResPrint( dd, bFunc, nInputs, uParts, nParts );
    }
}