summaryrefslogtreecommitdiffstats
path: root/src/bool
diff options
context:
space:
mode:
Diffstat (limited to 'src/bool')
-rw-r--r--src/bool/bdc/bdc.h2
-rw-r--r--src/bool/bdc/bdcCore.c66
-rw-r--r--src/bool/kit/kit.h13
-rw-r--r--src/bool/kit/kitDsd.c88
4 files changed, 158 insertions, 11 deletions
diff --git a/src/bool/bdc/bdc.h b/src/bool/bdc/bdc.h
index a7572fe8..bd0f7d7d 100644
--- a/src/bool/bdc/bdc.h
+++ b/src/bool/bdc/bdc.h
@@ -67,10 +67,12 @@ static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c ) { return (Bdc_F
/*=== bdcCore.c ==========================================================*/
extern Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars );
extern void Bdc_ManFree( Bdc_Man_t * p );
+extern void Bdc_ManDecPrint( Bdc_Man_t * p );
extern int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax );
extern Bdc_Fun_t * Bdc_ManFunc( Bdc_Man_t * p, int i );
extern Bdc_Fun_t * Bdc_ManRoot( Bdc_Man_t * p );
extern int Bdc_ManNodeNum( Bdc_Man_t * p );
+extern int Bdc_ManAndNum( Bdc_Man_t * p );
extern Bdc_Fun_t * Bdc_FuncFanin0( Bdc_Fun_t * p );
extern Bdc_Fun_t * Bdc_FuncFanin1( Bdc_Fun_t * p );
extern void * Bdc_FuncCopy( Bdc_Fun_t * p );
diff --git a/src/bool/bdc/bdcCore.c b/src/bool/bdc/bdcCore.c
index fb318e0d..a810146d 100644
--- a/src/bool/bdc/bdcCore.c
+++ b/src/bool/bdc/bdcCore.c
@@ -46,6 +46,7 @@ ABC_NAMESPACE_IMPL_START
Bdc_Fun_t * Bdc_ManFunc( Bdc_Man_t * p, int i ) { return Bdc_FunWithId(p, i); }
Bdc_Fun_t * Bdc_ManRoot( Bdc_Man_t * p ) { return p->pRoot; }
int Bdc_ManNodeNum( Bdc_Man_t * p ) { return p->nNodes; }
+int Bdc_ManAndNum( Bdc_Man_t * p ) { return p->nNodes-p->nVars-1;}
Bdc_Fun_t * Bdc_FuncFanin0( Bdc_Fun_t * p ) { return p->pFan0; }
Bdc_Fun_t * Bdc_FuncFanin1( Bdc_Fun_t * p ) { return p->pFan1; }
void * Bdc_FuncCopy( Bdc_Fun_t * p ) { return p->pCopy; }
@@ -186,7 +187,7 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
/**Function*************************************************************
- Synopsis [Clears the manager.]
+ Synopsis [Prints bi-decomposition in a simple format.]
Description []
@@ -195,7 +196,7 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
SeeAlso []
***********************************************************************/
-void Bdc_ManDecPrint( Bdc_Man_t * p )
+void Bdc_ManDecPrintSimple( Bdc_Man_t * p )
{
Bdc_Fun_t * pNode;
int i;
@@ -211,7 +212,7 @@ void Bdc_ManDecPrint( Bdc_Man_t * p )
printf( "%s%d &", Bdc_IsComplement(pNode->pFan0)? "-":"", Bdc_FunId(p,Bdc_Regular(pNode->pFan0)) );
printf( " %s%d ", Bdc_IsComplement(pNode->pFan1)? "-":"", Bdc_FunId(p,Bdc_Regular(pNode->pFan1)) );
}
- Extra_PrintBinary( stdout, pNode->puFunc, (1<<p->nVars) );
+// Extra_PrintBinary( stdout, pNode->puFunc, (1<<p->nVars) );
printf( "\n" );
}
printf( "Root = %s%d.\n", Bdc_IsComplement(p->pRoot)? "-":"", Bdc_FunId(p,Bdc_Regular(p->pRoot)) );
@@ -219,6 +220,65 @@ void Bdc_ManDecPrint( Bdc_Man_t * p )
/**Function*************************************************************
+ Synopsis [Prints bi-decomposition recursively.]
+
+ Description [This procedure prints bi-decomposition as a factored form.
+ In doing so, logic sharing, if present, will be replicated several times.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Bdc_ManDecPrint_rec( Bdc_Man_t * p, Bdc_Fun_t * pNode )
+{
+ if ( pNode->Type == BDC_TYPE_PI )
+ printf( "%c", 'a' + Bdc_FunId(p,pNode) - 1 );
+ else if ( pNode->Type == BDC_TYPE_AND )
+ {
+ Bdc_Fun_t * pNode0 = Bdc_FuncFanin0( pNode );
+ Bdc_Fun_t * pNode1 = Bdc_FuncFanin1( pNode );
+
+ if ( Bdc_IsComplement(pNode0) )
+ printf( "!" );
+ if ( Bdc_IsComplement(pNode0) && Bdc_Regular(pNode0)->Type != BDC_TYPE_PI )
+ printf( "(" );
+ Bdc_ManDecPrint_rec( p, Bdc_Regular(pNode0) );
+ if ( Bdc_IsComplement(pNode0) && Bdc_Regular(pNode0)->Type != BDC_TYPE_PI )
+ printf( ")" );
+
+ if ( Bdc_IsComplement(pNode1) )
+ printf( "!" );
+ if ( Bdc_IsComplement(pNode1) && Bdc_Regular(pNode1)->Type != BDC_TYPE_PI )
+ printf( "(" );
+ Bdc_ManDecPrint_rec( p, Bdc_Regular(pNode1) );
+ if ( Bdc_IsComplement(pNode1) && Bdc_Regular(pNode1)->Type != BDC_TYPE_PI )
+ printf( ")" );
+ }
+ else assert( 0 );
+}
+void Bdc_ManDecPrint( Bdc_Man_t * p )
+{
+ Bdc_Fun_t * pRoot = Bdc_Regular(p->pRoot);
+
+ printf( "F = " );
+ if ( pRoot->Type == BDC_TYPE_CONST1 ) // constant 0
+ printf( "Constant %d", !Bdc_IsComplement(p->pRoot) );
+ else if ( pRoot->Type == BDC_TYPE_PI ) // literal
+ printf( "%s%d", Bdc_IsComplement(p->pRoot) ? "!" : "", Bdc_FunId(p,pRoot)-1 );
+ else
+ {
+ if ( Bdc_IsComplement(p->pRoot) )
+ printf( "!(" );
+ Bdc_ManDecPrint_rec( p, pRoot );
+ if ( Bdc_IsComplement(p->pRoot) )
+ printf( ")" );
+ }
+ printf( "\n" );
+}
+
+/**Function*************************************************************
+
Synopsis [Performs decomposition of one function.]
Description []
diff --git a/src/bool/kit/kit.h b/src/bool/kit/kit.h
index dfee532e..8151f1d2 100644
--- a/src/bool/kit/kit.h
+++ b/src/bool/kit/kit.h
@@ -112,17 +112,17 @@ struct Kit_DsdObj_t_
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
+ unsigned short 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 short nVars; // at most 16 (perhaps 18?)
+ unsigned short nNodesAlloc; // the number of allocated nodes (at most nVars)
+ unsigned short nNodes; // the number of nodes
+ unsigned short Root; // the root of the tree
unsigned * pMem; // memory for the truth tables (memory manager?)
unsigned * pSupps; // supports of the nodes
Kit_DsdObj_t** pNodes; // the nodes
@@ -142,7 +142,7 @@ struct Kit_DsdMan_t_
Vec_Int_t * vNodes; // temporary array for BDD nodes
};
-static inline unsigned Kit_DsdObjOffset( int nFans ) { return (nFans >> 2) + ((nFans & 3) > 0); }
+static inline unsigned Kit_DsdObjOffset( int nFans ) { return (nFans >> 1) + ((nFans & 1) > 0); }
static inline unsigned * Kit_DsdObjTruth( Kit_DsdObj_t * pObj ) { return pObj->Type == KIT_DSD_PRIME ? (unsigned *)pObj->pFans + pObj->Offset: NULL; }
static inline int Kit_DsdNtkObjNum( Kit_DsdNtk_t * pNtk ){ return pNtk->nVars + pNtk->nNodes; }
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]; }
@@ -538,6 +538,7 @@ extern void Kit_DsdNtkFree( Kit_DsdNtk_t * pNtk );
extern int Kit_DsdNonDsdSizeMax( Kit_DsdNtk_t * pNtk );
extern Kit_DsdObj_t * Kit_DsdNonDsdPrimeMax( Kit_DsdNtk_t * pNtk );
extern unsigned Kit_DsdNonDsdSupports( Kit_DsdNtk_t * pNtk );
+extern int Kit_DsdCountAigNodes( Kit_DsdNtk_t * pNtk );
extern unsigned Kit_DsdGetSupports( Kit_DsdNtk_t * p );
extern Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p );
extern Kit_DsdNtk_t * Kit_DsdShrink( Kit_DsdNtk_t * p, int pPrios[] );
diff --git a/src/bool/kit/kitDsd.c b/src/bool/kit/kitDsd.c
index 3df16d8c..d026afbc 100644
--- a/src/bool/kit/kitDsd.c
+++ b/src/bool/kit/kitDsd.c
@@ -1485,7 +1485,7 @@ Kit_DsdNtk_t * Kit_DsdExpand( Kit_DsdNtk_t * p )
SeeAlso []
***********************************************************************/
-void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], unsigned char * piLits, int nVars, unsigned piLitsRes[] )
+void Kit_DsdCompSort( int pPrios[], unsigned uSupps[], unsigned short * piLits, int nVars, unsigned piLitsRes[] )
{
int nSuppSizes[16], Priority[16], pOrder[16];
int i, k, iVarBest, SuppMax, PrioMax;
@@ -1827,6 +1827,90 @@ int Kit_DsdFindLargeBox( Kit_DsdNtk_t * pNtk, int Size )
/**Function*************************************************************
+ Synopsis [Returns 1 if there is a component with more than 3 inputs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_DsdCountAigNodes_rec( Kit_DsdNtk_t * pNtk, int Id )
+{
+ Kit_DsdObj_t * pObj;
+ unsigned iLit, i, RetValue;
+ pObj = Kit_DsdNtkObj( pNtk, Id );
+ if ( pObj == NULL )
+ return 0;
+ if ( pObj->Type == KIT_DSD_CONST1 || pObj->Type == KIT_DSD_VAR )
+ return 0;
+ if ( pObj->nFans < 2 ) // why this happens? - need to figure out
+ return 0;
+ assert( pObj->nFans > 1 );
+ if ( pObj->Type == KIT_DSD_AND )
+ RetValue = ((int)pObj->nFans - 1);
+ else if ( pObj->Type == KIT_DSD_XOR )
+ RetValue = ((int)pObj->nFans - 1) * 3;
+ else if ( pObj->Type == KIT_DSD_PRIME )
+ {
+ // assuming MUX decomposition
+ assert( (int)pObj->nFans == 3 );
+ RetValue = 3;
+ }
+ else assert( 0 );
+ Kit_DsdObjForEachFanin( pNtk, pObj, iLit, i )
+ RetValue += Kit_DsdCountAigNodes_rec( pNtk, Abc_Lit2Var(iLit) );
+ return RetValue;
+}
+
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if there is a component with more than 3 inputs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_DsdCountAigNodes2( Kit_DsdNtk_t * pNtk )
+{
+ return Kit_DsdCountAigNodes_rec( pNtk, Abc_Lit2Var(pNtk->Root) );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Returns 1 if there is a component with more than 3 inputs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_DsdCountAigNodes( Kit_DsdNtk_t * pNtk )
+{
+ Kit_DsdObj_t * pObj;
+ int i, Counter = 0;
+ for ( i = 0; i < pNtk->nNodes; i++ )
+ {
+ pObj = pNtk->pNodes[i];
+ if ( pObj->Type == KIT_DSD_AND )
+ Counter += ((int)pObj->nFans - 1);
+ else if ( pObj->Type == KIT_DSD_XOR )
+ Counter += ((int)pObj->nFans - 1) * 3;
+ else if ( pObj->Type == KIT_DSD_PRIME ) // assuming MUX decomposition
+ Counter += 3;
+ }
+ return Counter;
+}
+
+/**Function*************************************************************
+
Synopsis [Returns 1 if the non-DSD 4-var func is implementable with two 3-LUTs.]
Description []
@@ -1883,7 +1967,7 @@ int Kit_DsdCheckVar4Dec2( Kit_DsdNtk_t * pNtk0, Kit_DsdNtk_t * pNtk1 )
SeeAlso []
***********************************************************************/
-void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uSupp, unsigned char * pPar, int nDecMux )
+void Kit_DsdDecompose_rec( Kit_DsdNtk_t * pNtk, Kit_DsdObj_t * pObj, unsigned uSupp, unsigned short * pPar, int nDecMux )
{
Kit_DsdObj_t * pRes, * pRes0, * pRes1;
int nWords = Kit_TruthWordNum(pObj->nFans);
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 00:01:08 +0000