src/aig/kit/kitBdd.c File Reference

#include "kit.h"
#include "extra.h"
Include dependency graph for kitBdd.c:

Go to the source code of this file.

Functions

DdNode * Kit_SopToBdd (DdManager *dd, Kit_Sop_t *cSop, int nVars)
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 88 of file kitBdd.c.

00089 {
00090     DdNode * bFunc, * bFunc0, * bFunc1;
00091     Kit_Node_t * pNode;
00092     int i;
00093 
00094     // sanity checks
00095     assert( Kit_GraphLeaveNum(pGraph) >= 0 );
00096     assert( Kit_GraphLeaveNum(pGraph) <= pGraph->nSize );
00097 
00098     // check for constant function
00099     if ( Kit_GraphIsConst(pGraph) )
00100         return Cudd_NotCond( b1, Kit_GraphIsComplement(pGraph) );
00101     // check for a literal
00102     if ( Kit_GraphIsVar(pGraph) )
00103         return Cudd_NotCond( Cudd_bddIthVar(dd, Kit_GraphVarInt(pGraph)), Kit_GraphIsComplement(pGraph) );
00104 
00105     // assign the elementary variables
00106     Kit_GraphForEachLeaf( pGraph, pNode, i )
00107         pNode->pFunc = Cudd_bddIthVar( dd, i );
00108 
00109     // compute the function for each internal node
00110     Kit_GraphForEachNode( pGraph, pNode, i )
00111     {
00112         bFunc0 = Cudd_NotCond( Kit_GraphNode(pGraph, pNode->eEdge0.Node)->pFunc, pNode->eEdge0.fCompl ); 
00113         bFunc1 = Cudd_NotCond( Kit_GraphNode(pGraph, pNode->eEdge1.Node)->pFunc, pNode->eEdge1.fCompl ); 
00114         pNode->pFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( pNode->pFunc );
00115     }
00116 
00117     // deref the intermediate results
00118     bFunc = pNode->pFunc;   Cudd_Ref( bFunc );
00119     Kit_GraphForEachNode( pGraph, pNode, i )
00120         Cudd_RecursiveDeref( dd, pNode->pFunc );
00121     Cudd_Deref( bFunc );
00122 
00123     // complement the result if necessary
00124     return Cudd_NotCond( bFunc, Kit_GraphIsComplement(pGraph) );
00125 }

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 195 of file kitBdd.c.

00196 {
00197     static DdManager * dd = NULL;
00198     Kit_Sop_t Sop, * cSop = &Sop;
00199     DdNode * bFunc1, * bFunc2;
00200     Vec_Int_t * vMemory;
00201     int RetValue;
00202     // get the manager
00203     if ( dd == NULL )
00204         dd = Cudd_Init( 16, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
00205     // derive SOP
00206     vMemory = Vec_IntAlloc( Vec_IntSize(vCover) );
00207     Kit_SopCreate( cSop, vCover, nVars, vMemory );
00208     // get the functions
00209     bFunc1 = Kit_SopToBdd( dd, cSop, nVars );      Cudd_Ref( bFunc1 );
00210     bFunc2 = Kit_GraphToBdd( dd, pFForm );         Cudd_Ref( bFunc2 );
00211 //Extra_bddPrint( dd, bFunc1 ); printf("\n");
00212 //Extra_bddPrint( dd, bFunc2 ); printf("\n");
00213     RetValue = (bFunc1 == bFunc2);
00214     if ( bFunc1 != bFunc2 )
00215     {
00216         int s;
00217         Extra_bddPrint( dd, bFunc1 ); printf("\n");
00218         Extra_bddPrint( dd, bFunc2 ); printf("\n");
00219         s  = 0;
00220     }
00221     Cudd_RecursiveDeref( dd, bFunc1 );
00222     Cudd_RecursiveDeref( dd, bFunc2 );
00223     Vec_IntFree( vMemory );
00224     return RetValue;
00225 }

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

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

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

Synopsis [Derives the BDD for the given SOP.]

Description []

SideEffects []

SeeAlso []

Definition at line 43 of file kitBdd.c.

00044 {
00045     DdNode * bSum, * bCube, * bTemp, * bVar;
00046     unsigned uCube;
00047     int Value, i, v;
00048     assert( nVars < 16 );
00049     // start the cover
00050     bSum = Cudd_ReadLogicZero(dd);   Cudd_Ref( bSum );
00051    // check the logic function of the node
00052     Kit_SopForEachCube( cSop, uCube, i )
00053     {
00054         bCube = Cudd_ReadOne(dd);   Cudd_Ref( bCube );
00055         for ( v = 0; v < nVars; v++ )
00056         {
00057             Value = ((uCube >> 2*v) & 3);
00058             if ( Value == 1 )
00059                 bVar = Cudd_Not( Cudd_bddIthVar( dd, v ) );
00060             else if ( Value == 2 )
00061                 bVar = Cudd_bddIthVar( dd, v );
00062             else
00063                 continue;
00064             bCube  = Cudd_bddAnd( dd, bTemp = bCube, bVar );   Cudd_Ref( bCube );
00065             Cudd_RecursiveDeref( dd, bTemp );
00066         }
00067         bSum = Cudd_bddOr( dd, bTemp = bSum, bCube );   
00068         Cudd_Ref( bSum );
00069         Cudd_RecursiveDeref( dd, bTemp );
00070         Cudd_RecursiveDeref( dd, bCube );
00071     }
00072     // complement the result if necessary
00073     Cudd_Deref( bSum );
00074     return bSum;
00075 }

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 179 of file kitBdd.c.

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

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

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 138 of file kitBdd.c.

00139 {
00140     DdNode * bF0, * bF1, * bF;
00141     int Var;
00142     if ( nVars <= 5 )
00143     {
00144         unsigned uTruth, uMask;
00145         uMask = ((~(unsigned)0) >> (32 - (1<<nVars)));
00146         uTruth = (pTruth[iBit>>5] >> (iBit&31)) & uMask;
00147         if ( uTruth == 0 )
00148             return b0;
00149         if ( uTruth == uMask )
00150             return b1;        
00151     }
00152     // find the variable to use
00153     Var = fMSBonTop? nVarsTotal-nVars : nVars-1;
00154     // other special cases can be added
00155     bF0 = Kit_TruthToBdd_rec( dd, pTruth, iBit,                nVars-1, nVarsTotal, fMSBonTop );  Cudd_Ref( bF0 );
00156     bF1 = Kit_TruthToBdd_rec( dd, pTruth, iBit+(1<<(nVars-1)), nVars-1, nVarsTotal, fMSBonTop );  Cudd_Ref( bF1 );
00157     bF  = Cudd_bddIte( dd, dd->vars[Var], bF1, bF0 );                     Cudd_Ref( bF );
00158     Cudd_RecursiveDeref( dd, bF0 );
00159     Cudd_RecursiveDeref( dd, bF1 );
00160     Cudd_Deref( bF );
00161     return bF;
00162 }

Generated on Tue Jan 5 12:18:27 2010 for abc70930 by  doxygen 1.6.1