giaClp.c File Reference

#include "gia.h"
#include "misc/extra/extraBdd.h"
#include "bdd/dsd/dsd.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START int	Abc_ConvertZddToSop (DdManager *dd, DdNode *zCover, char *pSop, int nFanins, Vec_Str_t *vCube, int fPhase)
	DECLARATIONS ///. More...
int	Abc_CountZddCubes (DdManager *dd, DdNode *zCover)
int	Abc_NtkDeriveFlatGiaSop (Gia_Man_t *pGia, int *gFanins, char *pSop)
int	Gia_ManFactorNode (Gia_Man_t *p, char *pSop, Vec_Int_t *vLeaves)
Vec_Ptr_t *	Gia_GetFakeNames (int nNames)
	FUNCTION DEFINITIONS ///. More...
int	Gia_ManRebuildIsop (DdManager *dd, DdNode *bLocal, Gia_Man_t *pNew, Vec_Int_t *vFanins, Vec_Str_t *vSop, Vec_Str_t *vCube)
int	Gia_ManRebuildNode (Dsd_Manager_t *pManDsd, Dsd_Node_t *pNodeDsd, Gia_Man_t *pNew, DdManager *ddNew, Vec_Int_t *vFanins, Vec_Str_t *vSop, Vec_Str_t *vCube)
Gia_Man_t *	Gia_ManRebuild (Gia_Man_t *p, Dsd_Manager_t *pManDsd, DdManager *ddNew)
void	Gia_ManCollapseDeref (DdManager *dd, Vec_Ptr_t *vFuncs)
void	Gia_ObjCollapseDeref (Gia_Man_t *p, DdManager *dd, Vec_Ptr_t *vFuncs, int Id)
Vec_Ptr_t *	Gia_ManCollapse (Gia_Man_t *p, DdManager *dd, int nBddLimit, int fVerbose)
Gia_Man_t *	Gia_ManCollapseTest (Gia_Man_t *p, int fVerbose)
void	Gia_ManCollapseTestTest (Gia_Man_t *p)

Function Documentation

int Abc_ConvertZddToSop	(	DdManager *	dd,
		DdNode *	zCover,
		char *	pSop,
		int	nFanins,
		Vec_Str_t *	vCube,
		int	fPhase
	)

DECLARATIONS ///.

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

FileName [giaClp.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [Collapsing AIG.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

Id:

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

]

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

Synopsis [Derive the BDD for the function in the cut.]

Description []

SideEffects []

SeeAlso []

Definition at line 471 of file abcFunc.c.

{
    int nCubes = 0;
    Abc_ConvertZddToSop_rec( dd, zCover, pSop, nFanins, vCube, fPhase, &nCubes );
    return nCubes;
}

int Abc_CountZddCubes	(	DdManager *	dd,
		DdNode *	zCover
	)

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

Synopsis [Count the number of paths in the ZDD.]

Description []

SideEffects []

SeeAlso []

Definition at line 593 of file abcFunc.c.

{
    int nCubes = 0;
    Abc_CountZddCubes_rec( dd, zCover, &nCubes );
    return nCubes;
}

int Abc_NtkDeriveFlatGiaSop	(	Gia_Man_t *	pGia,
		int *	gFanins,
		char *	pSop
	)

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

Synopsis [Strashes one logic node using its SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 131 of file abcHieCec.c.

{
    char * pCube;
    int gAnd, gSum;
    int i, Value, nFanins;
    // get the number of variables
    nFanins = Abc_SopGetVarNum(pSop);
    if ( Abc_SopIsExorType(pSop) )
    {
        gSum = 0; 
        for ( i = 0; i < nFanins; i++ )
            gSum = Gia_ManHashXor( pGia, gSum, gFanins[i] );
    }
    else
    {
        // go through the cubes of the node's SOP
        gSum = 0; 
        Abc_SopForEachCube( pSop, nFanins, pCube )
        {
            // create the AND of literals
            gAnd = 1;
            Abc_CubeForEachVar( pCube, Value, i )
            {
                if ( Value == '1' )
                    gAnd = Gia_ManHashAnd( pGia, gAnd, gFanins[i] );
                else if ( Value == '0' )
                    gAnd = Gia_ManHashAnd( pGia, gAnd, Abc_LitNot(gFanins[i]) );
            }
            // add to the sum of cubes
            gSum = Gia_ManHashAnd( pGia, Abc_LitNot(gSum), Abc_LitNot(gAnd) );
            gSum = Abc_LitNot( gSum );
        }
    }
    // decide whether to complement the result
    if ( Abc_SopIsComplement(pSop) )
        gSum = Abc_LitNot(gSum);
    return gSum;
}

Vec_Ptr_t* Gia_GetFakeNames

(

int

nNames

)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 51 of file giaClp.c.

{
    Vec_Ptr_t * vNames;
    char Buffer[5];
    int i;

    vNames = Vec_PtrAlloc( nNames );
    for ( i = 0; i < nNames; i++ )
    {
        if ( nNames < 26 )
        {
            Buffer[0] = 'a' + i;
            Buffer[1] = 0;
        }
        else
        {
            Buffer[0] = 'a' + i%26;
            Buffer[1] = '0' + i/26;
            Buffer[2] = 0;
        }
        Vec_PtrPush( vNames, Extra_UtilStrsav(Buffer) );
    }
    return vNames;
}

Vec_Ptr_t* Gia_ManCollapse	(	Gia_Man_t *	p,
		DdManager *	dd,
		int	nBddLimit,
		int	fVerbose
	)

Definition at line 288 of file giaClp.c.

{
    Vec_Ptr_t * vFuncs;
    DdNode * bFunc0, * bFunc1, * bFunc;
    Gia_Obj_t * pObj;
    int i, Id;
    Gia_ManCreateRefs( p );
    // assign constant node
    vFuncs = Vec_PtrStart( Gia_ManObjNum(p) );
    if ( Gia_ObjRefNumId(p, 0) > 0 )
        Vec_PtrWriteEntry( vFuncs, 0, Cudd_ReadLogicZero(dd) ), Cudd_Ref(Cudd_ReadLogicZero(dd));
    // assign elementary variables
    Gia_ManForEachCiId( p, Id, i )
        if ( Gia_ObjRefNumId(p, Id) > 0 )
            Vec_PtrWriteEntry( vFuncs, Id, Cudd_bddIthVar(dd,i) ), Cudd_Ref(Cudd_bddIthVar(dd,i));
    // create BDD for AND nodes
    Gia_ManForEachAnd( p, pObj, i )
    {
        bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Gia_ObjFaninId0(pObj, i)), Gia_ObjFaninC0(pObj) );
        bFunc1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Gia_ObjFaninId1(pObj, i)), Gia_ObjFaninC1(pObj) );
        bFunc  = Cudd_bddAndLimit( dd, bFunc0, bFunc1, nBddLimit );  
        if ( bFunc == NULL )
        {
            Gia_ManCollapseDeref( dd, vFuncs );
            return NULL;
        }        
        Cudd_Ref( bFunc );
        Vec_PtrWriteEntry( vFuncs, i, bFunc );
        Gia_ObjCollapseDeref( p, dd, vFuncs, Gia_ObjFaninId0(pObj, i) );
        Gia_ObjCollapseDeref( p, dd, vFuncs, Gia_ObjFaninId1(pObj, i) );
    }
    // create BDD for outputs
    Gia_ManForEachCoId( p, Id, i )
    {
        pObj = Gia_ManCo( p, i );
        bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(vFuncs, Gia_ObjFaninId0(pObj, Id)), Gia_ObjFaninC0(pObj) );
        Vec_PtrWriteEntry( vFuncs, Id, bFunc0 ); Cudd_Ref( bFunc0 );
        Gia_ObjCollapseDeref( p, dd, vFuncs, Gia_ObjFaninId0(pObj, Id) );
    }
    assert( Vec_PtrSize(vFuncs) == Vec_PtrCountZero(vFuncs) + Gia_ManCoNum(p) );
    // compact
    Gia_ManForEachCoId( p, Id, i )
        Vec_PtrWriteEntry( vFuncs, i, Vec_PtrEntry(vFuncs, Id) );
    Vec_PtrShrink( vFuncs, Gia_ManCoNum(p) );
    return vFuncs;
}

void Gia_ManCollapseDeref	(	DdManager *	dd,
		Vec_Ptr_t *	vFuncs
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 273 of file giaClp.c.

{
    DdNode * bFunc; int i;
    Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i )
        if ( bFunc )
            Cudd_RecursiveDeref( dd, bFunc );
    Vec_PtrFree( vFuncs );
}

Gia_Man_t* Gia_ManCollapseTest	(	Gia_Man_t *	p,
		int	fVerbose
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 346 of file giaClp.c.

{
    Gia_Man_t * pNew;
    DdManager * dd, * ddNew;
    Dsd_Manager_t * pManDsd;
    Vec_Ptr_t * vFuncs;
    // derive global BDDs
    dd = Cudd_Init( Gia_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
    Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
    vFuncs = Gia_ManCollapse( p, dd, 10000, 0 );
    Cudd_AutodynDisable( dd );
    if ( vFuncs == NULL ) 
    {
        Extra_StopManager( dd );
        return Gia_ManDup(p);
    }
    // start ISOP manager
    ddNew = Cudd_Init( Gia_ManCiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
    Cudd_zddVarsFromBddVars( ddNew, 2 );
//    Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
    if ( fVerbose )
    printf( "Ins = %d. Outs = %d.  Shared BDD nodes = %d.  Peak live nodes = %d. Peak nodes = %d.\n", 
        Gia_ManCiNum(p), Gia_ManCoNum(p), 
        Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) ),
        Cudd_ReadPeakLiveNodeCount(dd), (int)Cudd_ReadNodeCount(dd) );
    // perform decomposition
    pManDsd = Dsd_ManagerStart( dd, Gia_ManCiNum(p), 0 );
    Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) );
    if ( fVerbose )
    {
        Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p) );
        Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p) );
        char ** ppNamesCi = (char **)Vec_PtrArray( vNamesCi );
        char ** ppNamesCo = (char **)Vec_PtrArray( vNamesCo );
        Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1 );
        Vec_PtrFreeFree( vNamesCi );
        Vec_PtrFreeFree( vNamesCo );
    }

    pNew = Gia_ManRebuild( p, pManDsd, ddNew );
    Dsd_ManagerStop( pManDsd );
    // return manager
    Gia_ManCollapseDeref( dd, vFuncs );
    Extra_StopManager( dd );
    Extra_StopManager( ddNew );
    return pNew;
}

void Gia_ManCollapseTestTest

(

Gia_Man_t *

p

)

Definition at line 393 of file giaClp.c.

{
    Gia_Man_t * pNew;
    pNew = Gia_ManCollapseTest( p, 0 );
    Gia_ManPrintStats( p, NULL );
    Gia_ManPrintStats( pNew, NULL );
    Gia_ManStop( pNew );
}

int Gia_ManFactorNode	(	Gia_Man_t *	p,
		char *	pSop,
		Vec_Int_t *	vLeaves
	)

Definition at line 99 of file giaFx.c.

{
    if ( Kit_PlaGetVarNum(pSop) == 0 )
        return Abc_LitNotCond( 1, Kit_PlaIsConst0(pSop) );
    assert( Kit_PlaGetVarNum(pSop) == Vec_IntSize(vLeaves) );
    if ( Kit_PlaGetVarNum(pSop) > 2 && Kit_PlaGetCubeNum(pSop) > 1 )
    {
        Dec_Graph_t * pFForm;
        Dec_Node_t * pFFNode;
        int i, Lit;
        pFForm = Dec_Factor( pSop );
        // assign fanins
        Dec_GraphForEachLeaf( pFForm, pFFNode, i )
        {
            assert( Vec_IntEntry(vLeaves, i) >= 0 );
            pFFNode->iFunc = Vec_IntEntry(vLeaves, i);
        }
        // perform strashing
        Lit = Gia_ManGraphToAig( p, pFForm );
        Dec_GraphFree( pFForm );
        return Lit;
    }
    return Gia_ManSopToAig( p, pSop, vLeaves );
}

Gia_Man_t* Gia_ManRebuild	(	Gia_Man_t *	p,
		Dsd_Manager_t *	pManDsd,
		DdManager *	ddNew
	)

Definition at line 206 of file giaClp.c.

{
    Gia_Man_t * pNew;
    Dsd_Node_t ** ppNodesDsd;
    Dsd_Node_t * pNodeDsd;
    int i, nNodesDsd, iLit = -1;
    Vec_Str_t * vSop, * vCube;
    Vec_Int_t * vFanins;

    vFanins = Vec_IntAlloc( 1000 );
    vSop    = Vec_StrAlloc( 10000 );
    vCube   = Vec_StrAlloc( 1000 );

    pNew = Gia_ManStart( 2*Gia_ManObjNum(p) );
    pNew->pName = Abc_UtilStrsav( p->pName );
    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
    Gia_ManHashAlloc( pNew );

    // save the CI nodes in the DSD nodes
    Dsd_NodeSetMark( Dsd_ManagerReadConst1(pManDsd), 1 );
    for ( i = 0; i < Gia_ManCiNum(p); i++ )
    {
        pNodeDsd = Dsd_ManagerReadInput( pManDsd, i );
        Dsd_NodeSetMark( pNodeDsd, Gia_ManAppendCi( pNew ) );
    }

    // collect DSD nodes in DFS order (leaves and const1 are not collected)
    ppNodesDsd = Dsd_TreeCollectNodesDfs( pManDsd, &nNodesDsd );
    for ( i = 0; i < nNodesDsd; i++ )
    {
        iLit = Gia_ManRebuildNode( pManDsd, ppNodesDsd[i], pNew, ddNew, vFanins, vSop, vCube );
        if ( iLit == -1 )
            break;
    }
    ABC_FREE( ppNodesDsd );
    Vec_IntFree( vFanins );
    Vec_StrFree( vSop );
    Vec_StrFree( vCube );
    if ( iLit == -1 )
    {
        Gia_ManStop( pNew );
        return Gia_ManDup(p);
    }

    // set the pointers to the CO drivers
    for ( i = 0; i < Gia_ManCoNum(p); i++ )
    {
        pNodeDsd = Dsd_ManagerReadRoot( pManDsd, i );
        iLit = Dsd_NodeReadMark( Dsd_Regular(pNodeDsd) );
        iLit = Abc_LitNotCond( iLit, Dsd_IsComplement(pNodeDsd) );
        Gia_ManAppendCo( pNew, iLit );
    }
    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
    return pNew;
}

int Gia_ManRebuildIsop	(	DdManager *	dd,
		DdNode *	bLocal,
		Gia_Man_t *	pNew,
		Vec_Int_t *	vFanins,
		Vec_Str_t *	vSop,
		Vec_Str_t *	vCube
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 87 of file giaClp.c.

{
    char * pSop;
    DdNode * bCover, * zCover, * zCover0, * zCover1;
    int nFanins = Vec_IntSize(vFanins);
    int fPhase, nCubes, nCubes0, nCubes1;

    // get the ZDD of the negative polarity
    bCover = Cudd_zddIsop( dd, Cudd_Not(bLocal), Cudd_Not(bLocal), &zCover0 );
    Cudd_Ref( zCover0 );
    Cudd_Ref( bCover );
    Cudd_RecursiveDeref( dd, bCover );
    nCubes0 = Abc_CountZddCubes( dd, zCover0 );

    // get the ZDD of the positive polarity
    bCover = Cudd_zddIsop( dd, bLocal, bLocal, &zCover1 );
    Cudd_Ref( zCover1 );
    Cudd_Ref( bCover );
    Cudd_RecursiveDeref( dd, bCover );
    nCubes1 = Abc_CountZddCubes( dd, zCover1 );

    // compare the number of cubes
    if ( nCubes1 <= nCubes0 )
    { // use positive polarity
        nCubes = nCubes1;
        zCover = zCover1;
        Cudd_RecursiveDerefZdd( dd, zCover0 );
        fPhase = 1;
    }
    else
    { // use negative polarity
        nCubes = nCubes0;
        zCover = zCover0;
        Cudd_RecursiveDerefZdd( dd, zCover1 );
        fPhase = 0;
    }
    if ( nCubes > 1000 )
    {
        Cudd_RecursiveDerefZdd( dd, zCover );
        return -1;
    }

    // allocate memory for the cover
    Vec_StrGrow( vSop, (nFanins + 3) * nCubes + 1 );
    pSop = Vec_StrArray( vSop );
    pSop[(nFanins + 3) * nCubes] = 0;
    // create the SOP
    Vec_StrFill( vCube, nFanins, '-' );
    Vec_StrPush( vCube, '\0' );
    Abc_ConvertZddToSop( dd, zCover, pSop, nFanins, vCube, fPhase );
    Cudd_RecursiveDerefZdd( dd, zCover );

    // perform factoring
//    return Abc_NtkDeriveFlatGiaSop( pNew, Vec_IntArray(vFanins), pSop );
    return Gia_ManFactorNode( pNew, pSop, vFanins );
}

int Gia_ManRebuildNode	(	Dsd_Manager_t *	pManDsd,
		Dsd_Node_t *	pNodeDsd,
		Gia_Man_t *	pNew,
		DdManager *	ddNew,
		Vec_Int_t *	vFanins,
		Vec_Str_t *	vSop,
		Vec_Str_t *	vCube
	)

Definition at line 143 of file giaClp.c.

{
    DdManager * ddDsd = Dsd_ManagerReadDd( pManDsd );
    DdNode * bLocal, * bTemp;
    Dsd_Node_t * pFaninDsd;
    Dsd_Type_t Type;
    int i, nDecs, iLit = -1;

    // add the fanins
    Type  = Dsd_NodeReadType( pNodeDsd );
    nDecs = Dsd_NodeReadDecsNum( pNodeDsd );
    assert( nDecs > 1 );
    Vec_IntClear( vFanins );
    for ( i = 0; i < nDecs; i++ )
    {
        pFaninDsd = Dsd_NodeReadDec( pNodeDsd, i );
        iLit      = Dsd_NodeReadMark( Dsd_Regular(pFaninDsd) );
        iLit      = Abc_LitNotCond( iLit, Dsd_IsComplement(pFaninDsd) );
        assert( Type == DSD_NODE_OR || !Dsd_IsComplement(pFaninDsd) );
        Vec_IntPush( vFanins, iLit );
    }

    // create the local function depending on the type of the node
    switch ( Type )
    {
        case DSD_NODE_CONST1:
        {
            iLit = 1;
            break;
        }
        case DSD_NODE_OR:
        {
            iLit = 0;
            for ( i = 0; i < nDecs; i++ )
                iLit = Gia_ManHashOr( pNew, iLit, Vec_IntEntry(vFanins, i) );
            break;
        }
        case DSD_NODE_EXOR:
        {
            iLit = 0;
            for ( i = 0; i < nDecs; i++ )
                iLit = Gia_ManHashXor( pNew, iLit, Vec_IntEntry(vFanins, i) );
            break;
        }
        case DSD_NODE_PRIME:
        {
            bLocal = Dsd_TreeGetPrimeFunction( ddDsd, pNodeDsd );                Cudd_Ref( bLocal );
            bLocal = Extra_TransferLevelByLevel( ddDsd, ddNew, bTemp = bLocal ); Cudd_Ref( bLocal );
            Cudd_RecursiveDeref( ddDsd, bTemp );
            // bLocal is now in the new BDD manager
            iLit = Gia_ManRebuildIsop( ddNew, bLocal, pNew, vFanins, vSop, vCube );
            Cudd_RecursiveDeref( ddNew, bLocal );
            break;
        }
        default:
        {
            assert( 0 );
            break;
        }
    }
    Dsd_NodeSetMark( pNodeDsd, iLit );
    return iLit;
}

void Gia_ObjCollapseDeref	(	Gia_Man_t *	p,
		DdManager *	dd,
		Vec_Ptr_t *	vFuncs,
		int	Id
	)

Definition at line 281 of file giaClp.c.

{
    if ( Gia_ObjRefDecId(p, Id) )
        return;
    Cudd_RecursiveDeref( dd, (DdNode *)Vec_PtrEntry(vFuncs, Id) );
    Vec_PtrWriteEntry( vFuncs, Id, NULL );
}