/**CFile**************************************************************** FileName [extraUtilMult.c] SystemName [ABC: Logic synthesis and verification system.] PackageName [extra] Synopsis [Simple BDD package.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - May 23, 2018.] Revision [$Id: extraUtilMult.c,v 1.0 2018/05/23 00:00:00 alanmi Exp $] ***********************************************************************/ #include #include #include #include #include "misc/vec/vec.h" #include "aig/gia/gia.h" ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// typedef struct Abc_BddMan_ Abc_BddMan; struct Abc_BddMan_ { int nVars; // the number of variables int nObjs; // the number of nodes used int nObjsAlloc; // the number of nodes allocated int * pUnique; // unique table for nodes int * pNexts; // next pointer for nodes int * pCache; // array of triples int * pObjs; // array of pairs for each node unsigned char * pVars; // array of variables for each node unsigned char * pMark; // array of marks for each BDD node unsigned nUniqueMask; // selection mask for unique table unsigned nCacheMask; // selection mask for computed table int nCacheLookups; // the number of computed table lookups int nCacheMisses; // the number of computed table misses word nMemory; // total amount of memory used (in bytes) }; static inline int Abc_BddIthVar( int i ) { return Abc_Var2Lit(i + 1, 0); } static inline unsigned Abc_BddHash( int Arg0, int Arg1, int Arg2 ) { return 12582917 * Arg0 + 4256249 * Arg1 + 741457 * Arg2; } static inline int Abc_BddVar( Abc_BddMan * p, int i ) { return (int)p->pVars[Abc_Lit2Var(i)]; } static inline int Abc_BddThen( Abc_BddMan * p, int i ) { return Abc_LitNotCond(p->pObjs[Abc_LitRegular(i)], Abc_LitIsCompl(i)); } static inline int Abc_BddElse( Abc_BddMan * p, int i ) { return Abc_LitNotCond(p->pObjs[Abc_LitRegular(i)+1], Abc_LitIsCompl(i)); } static inline int Abc_BddMark( Abc_BddMan * p, int i ) { return (int)p->pMark[Abc_Lit2Var(i)]; } static inline void Abc_BddSetMark( Abc_BddMan * p, int i, int m ){ p->pMark[Abc_Lit2Var(i)] = m; } //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* Synopsis [Creating new node.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline int Abc_BddUniqueCreateInt( Abc_BddMan * p, int Var, int Then, int Else ) { int *q = p->pUnique + (Abc_BddHash(Var, Then, Else) & p->nUniqueMask); for ( ; *q; q = p->pNexts + *q ) if ( (int)p->pVars[*q] == Var && p->pObjs[*q+*q] == Then && p->pObjs[*q+*q+1] == Else ) return Abc_Var2Lit(*q, 0); if ( p->nObjs == p->nObjsAlloc ) printf( "Aborting because the number of nodes exceeded %d.\n", p->nObjsAlloc ), fflush(stdout); assert( p->nObjs < p->nObjsAlloc ); *q = p->nObjs++; p->pVars[*q] = Var; p->pObjs[*q+*q] = Then; p->pObjs[*q+*q+1] = Else; // printf( "Added node %3d: Var = %3d. Then = %3d. Else = %3d\n", *q, Var, Then, Else ); assert( !Abc_LitIsCompl(Else) ); return Abc_Var2Lit(*q, 0); } static inline int Abc_BddUniqueCreate( Abc_BddMan * p, int Var, int Then, int Else ) { assert( Var >= 0 && Var < p->nVars ); assert( Var < Abc_BddVar(p, Then) ); assert( Var < Abc_BddVar(p, Else) ); if ( Then == Else ) return Else; if ( !Abc_LitIsCompl(Else) ) return Abc_BddUniqueCreateInt( p, Var, Then, Else ); return Abc_LitNot( Abc_BddUniqueCreateInt(p, Var, Abc_LitNot(Then), Abc_LitNot(Else)) ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ static inline int Abc_BddCacheLookup( Abc_BddMan * p, int Arg1, int Arg2 ) { int * pEnt = p->pCache + 3*(Abc_BddHash(0, Arg1, Arg2) & p->nCacheMask); p->nCacheLookups++; return (pEnt[0] == Arg1 && pEnt[1] == Arg2) ? pEnt[2] : -1; } static inline int Abc_BddCacheInsert( Abc_BddMan * p, int Arg1, int Arg2, int Res ) { int * pEnt = p->pCache + 3*(Abc_BddHash(0, Arg1, Arg2) & p->nCacheMask); pEnt[0] = Arg1; pEnt[1] = Arg2; pEnt[2] = Res; p->nCacheMisses++; assert( Res >= 0 ); return Res; } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ Abc_BddMan * Abc_BddManAlloc( int nVars, int nObjs ) { Abc_BddMan * p; int i; p = ABC_CALLOC( Abc_BddMan, 1 ); p->nVars = nVars; p->nObjsAlloc = nObjs; p->nUniqueMask = (1 << Abc_Base2Log(nObjs)) - 1; p->nCacheMask = (1 << Abc_Base2Log(nObjs)) - 1; p->pUnique = ABC_CALLOC( int, p->nUniqueMask + 1 ); p->pNexts = ABC_CALLOC( int, p->nObjsAlloc ); p->pCache = ABC_CALLOC( int, 3*(p->nCacheMask + 1) ); p->pObjs = ABC_CALLOC( int, 2*p->nObjsAlloc ); p->pMark = ABC_CALLOC( unsigned char, p->nObjsAlloc ); p->pVars = ABC_CALLOC( unsigned char, p->nObjsAlloc ); p->pVars[0] = 0xff; p->nObjs = 1; for ( i = 0; i < nVars; i++ ) Abc_BddUniqueCreate( p, i, 1, 0 ); assert( p->nObjs == nVars + 1 ); p->nMemory = sizeof(Abc_BddMan)/4 + p->nUniqueMask + 1 + p->nObjsAlloc + (p->nCacheMask + 1) * 3 * sizeof(int)/4 + p->nObjsAlloc * 2 * sizeof(int)/4; return p; } void Abc_BddManFree( Abc_BddMan * p ) { printf( "BDD stats: Var = %d Obj = %d Alloc = %d Hit = %d Miss = %d ", p->nVars, p->nObjs, p->nObjsAlloc, p->nCacheLookups-p->nCacheMisses, p->nCacheMisses ); printf( "Mem = %.2f MB\n", 4.0*(int)(p->nMemory/(1<<20)) ); ABC_FREE( p->pUnique ); ABC_FREE( p->pNexts ); ABC_FREE( p->pCache ); ABC_FREE( p->pObjs ); ABC_FREE( p->pVars ); ABC_FREE( p ); } /**Function************************************************************* Synopsis [Boolean AND.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_BddAnd( Abc_BddMan * p, int a, int b ) { int r0, r1, r; if ( a == 0 ) return 0; if ( b == 0 ) return 0; if ( a == 1 ) return b; if ( b == 1 ) return a; if ( a == b ) return a; if ( a > b ) return Abc_BddAnd( p, b, a ); if ( (r = Abc_BddCacheLookup(p, a, b)) >= 0 ) return r; if ( Abc_BddVar(p, a) < Abc_BddVar(p, b) ) r0 = Abc_BddAnd( p, Abc_BddElse(p, a), b ), r1 = Abc_BddAnd( p, Abc_BddThen(p, a), b ); else if ( Abc_BddVar(p, a) > Abc_BddVar(p, b) ) r0 = Abc_BddAnd( p, a, Abc_BddElse(p, b) ), r1 = Abc_BddAnd( p, a, Abc_BddThen(p, b) ); else // if ( Abc_BddVar(p, a) == Abc_BddVar(p, b) ) r0 = Abc_BddAnd( p, Abc_BddElse(p, a), Abc_BddElse(p, b) ), r1 = Abc_BddAnd( p, Abc_BddThen(p, a), Abc_BddThen(p, b) ); r = Abc_BddUniqueCreate( p, Abc_MinInt(Abc_BddVar(p, a), Abc_BddVar(p, b)), r1, r0 ); return Abc_BddCacheInsert( p, a, b, r ); } int Abc_BddOr( Abc_BddMan * p, int a, int b ) { return Abc_LitNot( Abc_BddAnd(p, Abc_LitNot(a), Abc_LitNot(b)) ); } /**Function************************************************************* Synopsis [Counting nodes.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ int Abc_BddCount_rec( Abc_BddMan * p, int i ) { if ( i < 2 ) return 0; if ( Abc_BddMark(p, i) ) return 0; Abc_BddSetMark( p, i, 1 ); return 1 + Abc_BddCount_rec(p, Abc_BddElse(p, i)) + Abc_BddCount_rec(p, Abc_BddThen(p, i)); } void Abc_BddUnmark_rec( Abc_BddMan * p, int i ) { if ( i < 2 ) return; if ( !Abc_BddMark(p, i) ) return; Abc_BddSetMark( p, i, 0 ); Abc_BddUnmark_rec( p, Abc_BddElse(p, i) ); Abc_BddUnmark_rec( p, Abc_BddThen(p, i) ); } int Abc_BddCountNodes( Abc_BddMan * p, int i ) { int Count = Abc_BddCount_rec( p, i ); Abc_BddUnmark_rec( p, i ); return Count; } int Abc_BddCountNodesArray( Abc_BddMan * p, Vec_Int_t * vNodes ) { int i, a, Count = 0; Vec_IntForEachEntry( vNodes, a, i ) Count += Abc_BddCount_rec( p, a ); Vec_IntForEachEntry( vNodes, a, i ) Abc_BddUnmark_rec( p, a ); return Count; } int Abc_BddCountNodesArray2( Abc_BddMan * p, Vec_Int_t * vNodes ) { int i, a, Count = 0; Vec_IntForEachEntry( vNodes, a, i ) { Count += Abc_BddCount_rec( p, a ); Abc_BddUnmark_rec( p, a ); } return Count; } /**Function************************************************************* Synopsis [Printing BDD.] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_BddPrint_rec( Abc_BddMan * p, int a, int * pPath ) { if ( a == 0 ) return; if ( a == 1 ) { int i; for ( i = 0; i < p->nVars; i++ ) if ( pPath[i] == 0 || pPath[i] == 1 ) printf( "%c%d", pPath[i] ? '+' : '-', i ); printf( " " ); return; } pPath[Abc_BddVar(p, a)] = 0; Abc_BddPrint_rec( p, Abc_BddElse(p, a), pPath ); pPath[Abc_BddVar(p, a)] = 1; Abc_BddPrint_rec( p, Abc_BddThen(p, a), pPath ); pPath[Abc_BddVar(p, a)] = -1; } void Abc_BddPrint( Abc_BddMan * p, int a ) { int * pPath = ABC_FALLOC( int, p->nVars ); printf( "BDD %d = ", a ); Abc_BddPrint_rec( p, a, pPath ); ABC_FREE( pPath ); printf( "\n" ); } void Abc_BddPrintTest( Abc_BddMan * p ) { int bVarA = Abc_BddIthVar(0); int bVarB = Abc_BddIthVar(1); int bVarC = Abc_BddIthVar(2); int bVarD = Abc_BddIthVar(3); int bAndAB = Abc_BddAnd( p, bVarA, bVarB ); int bAndCD = Abc_BddAnd( p, bVarC, bVarD ); int bFunc = Abc_BddOr( p, bAndAB, bAndCD ); Abc_BddPrint( p, bFunc ); printf( "Nodes = %d\n", Abc_BddCountNodes(p, bFunc) ); } /**Function************************************************************* Synopsis [] Description [] SideEffects [] SeeAlso [] ***********************************************************************/ void Abc_BddGiaTest2( Gia_Man_t * pGia, int fVerbose ) { Abc_BddMan * p = Abc_BddManAlloc( 10, 100 ); Abc_BddPrintTest( p ); Abc_BddManFree( p ); } void Abc_BddGiaTest( Gia_Man_t * pGia, int fVerbose ) { Abc_BddMan * p; Vec_Int_t * vNodes; Gia_Obj_t * pObj; int i; p = Abc_BddManAlloc( Gia_ManCiNum(pGia), 1 << 20 ); // 30 B/node Gia_ManFillValue( pGia ); Gia_ManConst0(pGia)->Value = 0; Gia_ManForEachCi( pGia, pObj, i ) pObj->Value = Abc_BddIthVar( i ); vNodes = Vec_IntAlloc( Gia_ManAndNum(pGia) ); Gia_ManForEachAnd( pGia, pObj, i ) { int Cof0 = Abc_LitNotCond(Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj)); int Cof1 = Abc_LitNotCond(Gia_ObjFanin1(pObj)->Value, Gia_ObjFaninC1(pObj)); pObj->Value = Abc_BddAnd( p, Cof0, Cof1 ); } Gia_ManForEachCo( pGia, pObj, i ) pObj->Value = Abc_LitNotCond(Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj)); Gia_ManForEachCo( pGia, pObj, i ) { if ( fVerbose ) Abc_BddPrint( p, pObj->Value ); Vec_IntPush( vNodes, pObj->Value ); } printf( "Shared nodes = %d.\n", Abc_BddCountNodesArray2(p, vNodes) ); Vec_IntFree( vNodes ); Abc_BddManFree( p ); } /* abc 04> c.aig; &get; &test Shared nodes = 80. BDD stats: Var = 23 Obj = 206 Alloc = 1048576 Hit = 59 Miss = 216 Mem = 28.00 MB abc 05> c.aig; clp -r; ps c : i/o = 23/ 2 lat = 0 nd = 2 edge = 46 bdd = 80 lev = 1 */ //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_IMPL_END