mirror of https://github.com/YosysHQ/abc.git
Simple BDD package.
This commit is contained in:
Alan Mishchenko
parent
3697bdbe43
commit
8cb55037cb
|
|
@ -0,0 +1,395 @@
|
|||
/**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 <stdio.h>
|
||||
#include <stdlib.h>
|
||||
#include <string.h>
|
||||
#include <assert.h>
|
||||
#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 <arg0, arg1, AND(arg0, arg1)>
|
||||
int * pObjs; // array of pairs <cof0, cof1> 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
|
||||
|
||||
Loading…
Reference in New Issue