summaryrefslogtreecommitdiffstats
path: root/src/aig/kit/kitBdd.c
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/kit/kitBdd.c')
-rw-r--r--src/aig/kit/kitBdd.c231
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 ///
+////////////////////////////////////////////////////////////////////////
+
+