Version abc70407

This commit is contained in:
Alan Mishchenko
2007-04-07 08:01:00 -07:00
parent 00dc0f3daa
commit 94112fd22f
13 changed files with 1013 additions and 208 deletions
+70
View File
@@ -87,6 +87,69 @@ struct Kit_Graph_t_
Kit_Edge_t eRoot; // the pointer to the topmost node
};
// DSD node types
typedef enum {
KIT_DSD_NONE = 0, // 0: unknown
KIT_DSD_CONST1, // 1: constant 1
KIT_DSD_VAR, // 2: elementary variable
KIT_DSD_AND, // 3: multi-input AND
KIT_DSD_XOR, // 4: multi-input XOR
KIT_DSD_PRIME // 5: arbitrary function of 3+ variables
} Kit_Dsd_t;
// DSD node
typedef struct Kit_DsdObj_t_ Kit_DsdObj_t;
struct Kit_DsdObj_t_
{
unsigned Id : 6; // the number of this node
unsigned Type : 3; // none, const, var, AND, XOR, MUX, PRIME
unsigned fMark : 1; // finished checking output
unsigned Offset : 8; // offset to the truth table
unsigned nRefs : 8; // offset to the truth table
unsigned nFans : 6; // the number of fanins of this node
unsigned char pFans[0]; // the fanin literals
};
// DSD network
typedef struct Kit_DsdNtk_t_ Kit_DsdNtk_t;
struct Kit_DsdNtk_t_
{
unsigned char nVars; // at most 16 (perhaps 18?)
unsigned char nNodesAlloc; // the number of allocated nodes (at most nVars)
unsigned char nNodes; // the number of nodes
unsigned char Root; // the root of the tree
unsigned * pMem; // memory for the truth tables (memory manager?)
Kit_DsdObj_t * pNodes[0]; // the nodes
};
// DSD manager
typedef struct Kit_DsdMan_t_ Kit_DsdMan_t;
struct Kit_DsdMan_t_
{
int nVars; // the maximum number of variables
int nWords; // the number of words in TTs
Vec_Ptr_t * vTtElems; // elementary truth tables
Vec_Ptr_t * vTtNodes; // the node truth tables
};
static inline int Kit_DsdVar2Lit( int Var, int fCompl ) { return Var + Var + fCompl; }
static inline int Kit_DsdLit2Var( int Lit ) { return Lit >> 1; }
static inline int Kit_DsdLitIsCompl( int Lit ) { return Lit & 1; }
static inline int Kit_DsdLitNot( int Lit ) { return Lit ^ 1; }
static inline int Kit_DsdLitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); }
static inline int Kit_DsdLitRegular( int Lit ) { return Lit & 0xfe; }
static inline unsigned Kit_DsdObjOffset( int nFans ) { return (nFans >> 2) + ((nFans & 3) > 0); }
static inline unsigned * Kit_DsdObjTruth( Kit_DsdObj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; }
static inline Kit_DsdObj_t * Kit_DsdNtkObj( Kit_DsdNtk_t * pNtk, int Id ) { assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; }
static inline Kit_DsdObj_t * Kit_DsdNtkRoot( Kit_DsdNtk_t * pNtk ) { return Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(pNtk->Root) ); }
#define Kit_DsdNtkForEachObj( pNtk, pObj, i ) \
for ( i = 0; (i < (pNtk)->nNodes) && ((pObj) = (pNtk)->pNodes[i]); i++ )
#define Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) \
for ( i = 0; (i < (pObj)->nFans) && ((iLit) = (pObj)->pFans[i], 1); i++ )
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -358,6 +421,13 @@ static inline void Kit_TruthAndPhase( unsigned * pOut, unsigned * pIn0, unsigned
extern DdNode * Kit_SopToBdd( DdManager * dd, Kit_Sop_t * cSop, int nVars );
extern DdNode * Kit_GraphToBdd( DdManager * dd, Kit_Graph_t * pGraph );
extern DdNode * Kit_TruthToBdd( DdManager * dd, unsigned * pTruth, int nVars, int fMSBonTop );
/*=== kitDsd.c ==========================================================*/
extern Kit_DsdNtk_t * Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize );
extern unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk );
extern void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk );
extern Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars );
extern void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
extern int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk );
/*=== kitFactor.c ==========================================================*/
extern Kit_Graph_t * Kit_SopFactor( Vec_Int_t * vCover, int fCompl, int nVars, Vec_Int_t * vMemory );
/*=== kitGraph.c ==========================================================*/
+72 -69
View File
@@ -24,74 +24,6 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
typedef struct Kit_DsdMan_t_ Kit_DsdMan_t;
typedef struct Kit_DsdNtk_t_ Kit_DsdNtk_t;
typedef struct Kit_DsdObj_t_ Kit_DsdObj_t;
// DSD node types
typedef enum {
KIT_DSD_NONE = 0, // 0: unknown
KIT_DSD_CONST1, // 1: constant 1
KIT_DSD_VAR, // 2: elementary variable
KIT_DSD_AND, // 3: multi-input AND
KIT_DSD_XOR, // 4: multi-input XOR
KIT_DSD_PRIME // 5: arbitrary function of 3+ variables
} Kit_Dsd_t;
// DSD manager
struct Kit_DsdMan_t_
{
int nVars; // the maximum number of variables
int nWords; // the number of words in TTs
Vec_Ptr_t * vTtElems; // elementary truth tables
Vec_Ptr_t * vTtNodes; // the node truth tables
};
// DSD network
struct Kit_DsdNtk_t_
{
unsigned char nVars; // at most 16 (perhaps 18?)
unsigned char nNodesAlloc; // the number of allocated nodes (at most nVars)
unsigned char nNodes; // the number of nodes
unsigned char Root; // the root of the tree
unsigned * pMem; // memory for the truth tables (memory manager?)
Kit_DsdObj_t * pNodes[0]; // the nodes
};
// DSD node
struct Kit_DsdObj_t_
{
unsigned Id : 6; // the number of this node
unsigned Type : 3; // none, const, var, AND, XOR, MUX, PRIME
unsigned fMark : 1; // finished checking output
unsigned Offset : 8; // offset to the truth table
unsigned nRefs : 8; // offset to the truth table
unsigned nFans : 6; // the number of fanins of this node
unsigned char pFans[0]; // the fanin literals
};
static inline int Kit_DsdVar2Lit( int Var, int fCompl ) { return Var + Var + fCompl; }
static inline int Kit_DsdLit2Var( int Lit ) { return Lit >> 1; }
static inline int Kit_DsdLitIsCompl( int Lit ) { return Lit & 1; }
static inline int Kit_DsdLitNot( int Lit ) { return Lit ^ 1; }
static inline int Kit_DsdLitNotCond( int Lit, int c ) { return Lit ^ (int)(c > 0); }
static inline int Kit_DsdLitRegular( int Lit ) { return Lit & 0xfe; }
static inline unsigned Kit_DsdObjOffset( int nFans ) { return (nFans >> 2) + ((nFans & 3) > 0); }
static inline unsigned * Kit_DsdObjTruth( Kit_DsdObj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; }
static inline Kit_DsdObj_t * Kit_DsdNtkObj( Kit_DsdNtk_t * pNtk, int Id ) { assert( Id >= 0 && Id < pNtk->nVars + pNtk->nNodes ); return Id < pNtk->nVars ? NULL : pNtk->pNodes[Id - pNtk->nVars]; }
static inline Kit_DsdObj_t * Kit_DsdNtkRoot( Kit_DsdNtk_t * pNtk ) { return Kit_DsdNtkObj( pNtk, Kit_DsdLit2Var(pNtk->Root) ); }
#define Kit_DsdNtkForEachObj( pNtk, pObj, i ) \
for ( i = 0; (i < (pNtk)->nNodes) && ((pObj) = (pNtk)->pNodes[i]); i++ )
#define Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i ) \
for ( i = 0; (i < (pObj)->nFans) && ((iLit) = (pObj)->pFans[i], 1); i++ )
extern unsigned * Kit_DsdTruthCompute( Kit_DsdMan_t * p, Kit_DsdNtk_t * pNtk );
extern void Kit_DsdPrint( FILE * pFile, Kit_DsdNtk_t * pNtk );
extern Kit_DsdNtk_t * Kit_DsdDecompose( unsigned * pTruth, int nVars );
extern void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
@@ -483,7 +415,7 @@ int Kit_DsdCountLuts_rec( Kit_DsdNtk_t * pNtk, int nLutSize, int Id, int * pCoun
return nLutSize - 2;
}
assert( pObj->Type == KIT_DSD_PRIME );
if ( (int)pObj->nFans > nLutSize )
if ( (int)pObj->nFans > nLutSize ) //+ 1 )
{
*pCounter = 1000;
return 0;
@@ -491,6 +423,8 @@ int Kit_DsdCountLuts_rec( Kit_DsdNtk_t * pNtk, int nLutSize, int Id, int * pCoun
Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
Kit_DsdCountLuts_rec( pNtk, nLutSize, Kit_DsdLit2Var(iLit), pCounter );
(*pCounter)++;
// if ( (int)pObj->nFans == nLutSize + 1 )
// (*pCounter)++;
return nLutSize - pObj->nFans;
}
@@ -518,6 +452,31 @@ int Kit_DsdCountLuts( Kit_DsdNtk_t * pNtk, int nLutSize )
return Counter;
}
/**Function*************************************************************
Synopsis [Counts the number of blocks of the given number of inputs.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk )
{
Kit_DsdObj_t * pObj;
unsigned i, nSizeMax = 0;
Kit_DsdNtkForEachObj( pNtk, pObj, i )
{
if ( pObj->Type != KIT_DSD_PRIME )
continue;
if ( nSizeMax < pObj->nFans )
nSizeMax = pObj->nFans;
}
return nSizeMax;
}
/**Function*************************************************************
@@ -1197,6 +1156,50 @@ int Kit_DsdEval( unsigned * pTruth, int nVars, int nLutSize )
return Result;
}
/**Function*************************************************************
Synopsis [Performs decomposition of the truth table.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
Kit_DsdNtk_t * Kit_DsdDeriveNtk( unsigned * pTruth, int nVars, int nLutSize )
{
// Kit_DsdMan_t * p;
Kit_DsdNtk_t * pNtk;//, * pTemp;
// unsigned * pTruthC;
// int Result;
// decompose the function
pNtk = Kit_DsdDecompose( pTruth, nVars );
// pNtk = Kit_DsdExpand( pTemp = pNtk );
// Kit_DsdNtkFree( pTemp );
// Result = Kit_DsdCountLuts( pNtk, nLutSize );
// printf( "\n" );
// Kit_DsdPrint( stdout, pNtk );
// printf( "Eval = %d.\n", Result );
/*
// recompute the truth table
p = Kit_DsdManAlloc( nVars );
pTruthC = Kit_DsdTruthCompute( p, pNtk );
if ( !Extra_TruthIsEqual( pTruth, pTruthC, nVars ) )
printf( "Verification failed.\n" );
Kit_DsdManFree( p );
*/
// Kit_DsdNtkFree( pNtk );
// return Result;
return pNtk;
}
/**Function*************************************************************
Synopsis [Performs decomposition of the truth table.]
+1 -1
View File
@@ -1216,7 +1216,7 @@ unsigned Kit_TruthSemiCanonicize( unsigned * pInOut, unsigned * pAux, int nVars,
// short pStore2[32];
unsigned * pIn = pInOut, * pOut = pAux, * pTemp;
int nWords = Kit_TruthWordNum( nVars );
int i, Temp, fChange, Counter, nOnes;//, k, j, w, Limit;
int i, Temp, fChange, Counter;//, nOnes;//, k, j, w, Limit;
unsigned uCanonPhase;
// canonicize output
+36 -19
View File
@@ -25,12 +25,30 @@
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
static int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
Synopsis [Computes the level of the node using its fanin levels.]
Description []
SideEffects []
SeeAlso []
***********************************************************************/
int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj )
{
Abc_Obj_t * pFanin;
int i, Level = 0;
Abc_ObjForEachFanin( pObj, pFanin, i )
Level = ABC_MAX( Level, (int)pFanin->Level );
return Level + 1;
}
/**Function*************************************************************
Synopsis [Incrementally updates level of the nodes.]
@@ -42,18 +60,10 @@ static int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj );
SeeAlso []
***********************************************************************/
void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels )
void Res_UpdateNetworkLevel( Abc_Obj_t * pObjNew, Vec_Vec_t * vLevels )
{
Abc_Obj_t * pObjNew, * pFanin, * pFanout, * pTemp;
Abc_Obj_t * pFanout, * pTemp;
int Lev, k, m;
// create the new node
pObjNew = Abc_NtkCreateNode( pObj->pNtk );
pObjNew->pData = pFunc;
Vec_PtrForEachEntry( vFanins, pFanin, k )
Abc_ObjAddFanin( pObjNew, pFanin );
// replace the old node by the new node
pObjNew->Level = pObj->Level;
Abc_ObjReplace( pObj, pObjNew );
// check if level has changed
if ( (int)pObjNew->Level == Res_UpdateNetworkLevelNew(pObjNew) )
return;
@@ -81,7 +91,7 @@ void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc
/**Function*************************************************************
Synopsis [Computes the level of the node using its fanin levels.]
Synopsis [Incrementally updates level of the nodes.]
Description []
@@ -90,13 +100,20 @@ void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc
SeeAlso []
***********************************************************************/
int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj )
void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels )
{
Abc_Obj_t * pFanin;
int i, Level = 0;
Abc_ObjForEachFanin( pObj, pFanin, i )
Level = ABC_MAX( Level, (int)pFanin->Level );
return Level + 1;
Abc_Obj_t * pObjNew, * pFanin;
int k;
// create the new node
pObjNew = Abc_NtkCreateNode( pObj->pNtk );
pObjNew->pData = pFunc;
Vec_PtrForEachEntry( vFanins, pFanin, k )
Abc_ObjAddFanin( pObjNew, pFanin );
// replace the old node by the new node
pObjNew->Level = pObj->Level;
Abc_ObjReplace( pObj, pObjNew );
// update the level of the node
Res_UpdateNetworkLevel( pObjNew, vLevels );
}
////////////////////////////////////////////////////////////////////////