kitBdd.c File Reference

#include "kit.h"
#include "misc/extra/extraBdd.h"

Go to the source code of this file.

Functions
ABC_NAMESPACE_IMPL_START DdNode *	Kit_SopToBdd (DdManager *dd, Kit_Sop_t *cSop, int nVars)
	DECLARATIONS ///. More...
DdNode *	Kit_GraphToBdd (DdManager *dd, Kit_Graph_t *pGraph)
DdNode *	Kit_TruthToBdd_rec (DdManager *dd, unsigned *pTruth, int iBit, int nVars, int nVarsTotal, int fMSBonTop)
DdNode *	Kit_TruthToBdd (DdManager *dd, unsigned *pTruth, int nVars, int fMSBonTop)
int	Kit_SopFactorVerify (Vec_Int_t *vCover, Kit_Graph_t *pFForm, int nVars)

Function Documentation

DdNode* Kit_GraphToBdd	(	DdManager *	dd,
		Kit_Graph_t *	pGraph
	)

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

Synopsis [Converts graph to BDD.]

Description []

SideEffects []

SeeAlso []

Definition at line 91 of file kitBdd.c.

{
    DdNode * bFunc, * bFunc0, * bFunc1;
    Kit_Node_t * pNode = NULL; // Suppress "might be used uninitialized"
    int i;

    // sanity checks
    assert( Kit_GraphLeaveNum(pGraph) >= 0 );
    assert( Kit_GraphLeaveNum(pGraph) <= pGraph->nSize );

    // check for constant function
    if ( Kit_GraphIsConst(pGraph) )
        return Cudd_NotCond( b1, Kit_GraphIsComplement(pGraph) );
    // check for a literal
    if ( Kit_GraphIsVar(pGraph) )
        return Cudd_NotCond( Cudd_bddIthVar(dd, Kit_GraphVarInt(pGraph)), Kit_GraphIsComplement(pGraph) );

    // assign the elementary variables
    Kit_GraphForEachLeaf( pGraph, pNode, i )
        pNode->pFunc = Cudd_bddIthVar( dd, i );

    // compute the function for each internal node
    Kit_GraphForEachNode( pGraph, pNode, i )
    {
        bFunc0 = Cudd_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
        bFunc1 = Cudd_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
        pNode->pFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( (DdNode *)pNode->pFunc );
    }

    // deref the intermediate results
    bFunc = (DdNode *)pNode->pFunc;   Cudd_Ref( bFunc );
    Kit_GraphForEachNode( pGraph, pNode, i )
        Cudd_RecursiveDeref( dd, (DdNode *)pNode->pFunc );
    Cudd_Deref( bFunc );

    // complement the result if necessary
    return Cudd_NotCond( bFunc, Kit_GraphIsComplement(pGraph) );
}

int Kit_SopFactorVerify	(	Vec_Int_t *	vCover,
		Kit_Graph_t *	pFForm,
		int	nVars
	)

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

Synopsis [Verifies that the factoring is correct.]

Description []

SideEffects []

SeeAlso []

Definition at line 198 of file kitBdd.c.

{
    static DdManager * dd = NULL;
    Kit_Sop_t Sop, * cSop = &Sop;
    DdNode * bFunc1, * bFunc2;
    Vec_Int_t * vMemory;
    int RetValue;
    // get the manager
    if ( dd == NULL )
        dd = Cudd_Init( 16, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
    // derive SOP
    vMemory = Vec_IntAlloc( Vec_IntSize(vCover) );
    Kit_SopCreate( cSop, vCover, nVars, vMemory );
    // get the functions
    bFunc1 = Kit_SopToBdd( dd, cSop, nVars );      Cudd_Ref( bFunc1 );
    bFunc2 = Kit_GraphToBdd( dd, pFForm );         Cudd_Ref( bFunc2 );
//Extra_bddPrint( dd, bFunc1 ); printf("\n");
//Extra_bddPrint( dd, bFunc2 ); printf("\n");
    RetValue = (bFunc1 == bFunc2);
    if ( bFunc1 != bFunc2 )
    {
        int s;
        Extra_bddPrint( dd, bFunc1 ); printf("\n");
        Extra_bddPrint( dd, bFunc2 ); printf("\n");
        s  = 0;
    }
    Cudd_RecursiveDeref( dd, bFunc1 );
    Cudd_RecursiveDeref( dd, bFunc2 );
    Vec_IntFree( vMemory );
    return RetValue;
}

ABC_NAMESPACE_IMPL_START DdNode* Kit_SopToBdd	(	DdManager *	dd,
		Kit_Sop_t *	cSop,
		int	nVars
	)

DECLARATIONS ///.

FUNCTION DECLARATIONS ///.

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

FileName [kitBdd.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Computation kit.]

Synopsis [Procedures involving BDDs.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Dec 6, 2006.]

Revision [

Id:

kitBdd.c,v 1.00 2006/12/06 00:00:00 alanmi Exp

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

Synopsis [Derives the BDD for the given SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file kitBdd.c.

{
    DdNode * bSum, * bCube, * bTemp, * bVar;
    unsigned uCube;
    int Value, i, v;
    assert( nVars < 16 );
    // start the cover
    bSum = Cudd_ReadLogicZero(dd);   Cudd_Ref( bSum );
   // check the logic function of the node
    Kit_SopForEachCube( cSop, uCube, i )
    {
        bCube = Cudd_ReadOne(dd);   Cudd_Ref( bCube );
        for ( v = 0; v < nVars; v++ )
        {
            Value = ((uCube >> 2*v) & 3);
            if ( Value == 1 )
                bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) );
            else if ( Value == 2 )
                bVar = 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
    Cudd_Deref( bSum );
    return bSum;
}

DdNode* Kit_TruthToBdd	(	DdManager *	dd,
		unsigned *	pTruth,
		int	nVars,
		int	fMSBonTop
	)

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

Synopsis [Compute BDD corresponding to the truth table.]

Description [If truth table has N vars, the BDD depends on N topmost variables of the BDD manager. The most significant variable of the table is encoded by the topmost variable of the manager. BDD construction is efficient in this case because BDD is constructed one node at a time, by simply adding BDD nodes on top of existent BDD nodes.]

SideEffects []

SeeAlso []

Definition at line 182 of file kitBdd.c.

{
    return Kit_TruthToBdd_rec( dd, pTruth, 0, nVars, nVars, fMSBonTop );
}

DdNode* Kit_TruthToBdd_rec	(	DdManager *	dd,
		unsigned *	pTruth,
		int	iBit,
		int	nVars,
		int	nVarsTotal,
		int	fMSBonTop
	)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 141 of file kitBdd.c.

{
    DdNode * bF0, * bF1, * bF;
    int Var;
    if ( nVars <= 5 )
    {
        unsigned uTruth, uMask;
        uMask = ((~(unsigned)0) >> (32 - (1<<nVars)));
        uTruth = (pTruth[iBit>>5] >> (iBit&31)) & uMask;
        if ( uTruth == 0 )
            return b0;
        if ( uTruth == uMask )
            return b1;        
    }
    // find the variable to use
    Var = fMSBonTop? nVarsTotal-nVars : nVars-1;
    // other special cases can be added
    bF0 = Kit_TruthToBdd_rec( dd, pTruth, iBit,                nVars-1, nVarsTotal, fMSBonTop );  Cudd_Ref( bF0 );
    bF1 = Kit_TruthToBdd_rec( dd, pTruth, iBit+(1<<(nVars-1)), nVars-1, nVarsTotal, fMSBonTop );  Cudd_Ref( bF1 );
    bF  = Cudd_bddIte( dd, dd->vars[Var], bF1, bF0 );                     Cudd_Ref( bF );
    Cudd_RecursiveDeref( dd, bF0 );
    Cudd_RecursiveDeref( dd, bF1 );
    Cudd_Deref( bF );
    return bF;
}