diff options
Diffstat (limited to 'src/aig/kit/kitBdd.c')
| -rw-r--r-- | src/aig/kit/kitBdd.c | 231 |
1 files changed, 231 insertions, 0 deletions
diff --git a/src/aig/kit/kitBdd.c b/src/aig/kit/kitBdd.c new file mode 100644 index 00000000..9c8d4f7a --- /dev/null +++ b/src/aig/kit/kitBdd.c @@ -0,0 +1,231 @@ +/**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 $] + +***********************************************************************/ + +#include "kit.h" +#include "extra.h" + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Derives the BDD for the given SOP.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Kit_SopToBdd( DdManager * dd, Kit_Sop_t * cSop, int nVars ) +{ + 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; +} + +/**Function************************************************************* + + Synopsis [Converts graph to BDD.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph ) +{ + DdNode * bFunc, * bFunc0, * bFunc1; + Kit_Node_t * pNode; + 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( pNode->pFunc ); + } + + // deref the intermediate results + bFunc = pNode->pFunc; Cudd_Ref( bFunc ); + Kit_GraphForEachNode( pGraph, pNode, i ) + Cudd_RecursiveDeref( dd, pNode->pFunc ); + Cudd_Deref( bFunc ); + + // complement the result if necessary + return Cudd_NotCond( bFunc, Kit_GraphIsComplement(pGraph) ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +DdNode * Kit_TruthToBdd_rec( DdManager * dd, unsigned * pTruth, int iBit, int nVars, int nVarsTotal, int fMSBonTop ) +{ + 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; +} + +/**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 [] + +***********************************************************************/ +DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars, int fMSBonTop ) +{ + return Kit_TruthToBdd_rec( dd, pTruth, 0, nVars, nVars, fMSBonTop ); +} + +/**Function************************************************************* + + Synopsis [Verifies that the factoring is correct.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Kit_SopFactorVerify( Vec_Int_t * vCover, Kit_Graph_t * pFForm, int nVars ) +{ + 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; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + |