summaryrefslogtreecommitdiffstats
path: root/src/aig/bdc
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig/bdc')
-rw-r--r--src/aig/bdc/bdcCore.c28
-rw-r--r--src/aig/bdc/bdcDec.c115
-rw-r--r--src/aig/bdc/bdcInt.h17
-rw-r--r--src/aig/bdc/bdcTable.c33
4 files changed, 149 insertions, 44 deletions
diff --git a/src/aig/bdc/bdcCore.c b/src/aig/bdc/bdcCore.c
index f0b0f3bc..13275377 100644
--- a/src/aig/bdc/bdcCore.c
+++ b/src/aig/bdc/bdcCore.c
@@ -48,11 +48,11 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
p->pPars = pPars;
p->nWords = Kit_TruthWordNum( pPars->nVarsMax );
p->nDivsLimit = 200;
- // memory
- p->vMemory = Vec_IntStart( 1 << 16 );
// internal nodes
p->nNodesAlloc = 512;
p->pNodes = ALLOC( Bdc_Fun_t, p->nNodesAlloc );
+ // memory
+ p->vMemory = Vec_IntStart( 4 * p->nWords * p->nNodesAlloc );
// set up hash table
p->nTableSize = (1 << p->pPars->nVarsMax);
p->pTable = ALLOC( Bdc_Fun_t *, p->nTableSize );
@@ -69,7 +69,7 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
p->pIsfOR = &p->IsfOR; Bdc_IsfStart( p, p->pIsfOR );
p->pIsfAL = &p->IsfAL; Bdc_IsfStart( p, p->pIsfAL );
p->pIsfAR = &p->IsfAR; Bdc_IsfStart( p, p->pIsfAR );
- return p;
+ return p;
}
/**Function*************************************************************
@@ -85,6 +85,18 @@ Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
***********************************************************************/
void Bdc_ManFree( Bdc_Man_t * p )
{
+ if ( p->pPars->fVerbose )
+ {
+ printf( "Bi-decomposition stats: Calls = %d. Nodes = %d. Reuse = %d.\n",
+ p->numCalls, p->numNodes, p->numReuse );
+ printf( "ANDs = %d. ORs = %d. Weak = %d. Muxes = %d. Memory = %.2f K\n",
+ p->numAnds, p->numOrs, p->numWeaks, p->numMuxes, 4.0 * Vec_IntSize(p->vMemory) / (1<<10) );
+ PRT( "Cache", p->timeCache );
+ PRT( "Check", p->timeCheck );
+ PRT( "Muxes", p->timeMuxes );
+ PRT( "Supps", p->timeSupps );
+ PRT( "TOTAL", p->timeTotal );
+ }
Vec_IntFree( p->vMemory );
Vec_IntFree( p->vSpots );
Vec_PtrFree( p->vTruths );
@@ -118,7 +130,8 @@ void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
// add constant 1
pNode = Bdc_FunNew( p );
pNode->Type = BDC_TYPE_CONST1;
- pNode->puFunc = NULL;
+ pNode->puFunc = (unsigned *)Vec_IntFetch(p->vMemory, p->nWords);
+ Kit_TruthFill( pNode->puFunc, p->nVars );
pNode->uSupp = 0;
Bdc_TableAdd( p, pNode );
// add variables
@@ -192,6 +205,7 @@ void Bdc_ManDecPrint( Bdc_Man_t * p )
int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodesMax )
{
Bdc_Isf_t Isf, * pIsf = &Isf;
+ int clk = clock();
assert( nVars <= p->pPars->nVarsMax );
// set current manager parameters
p->nVars = nVars;
@@ -213,8 +227,14 @@ int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int n
Bdc_SuppMinimize( p, pIsf );
// call decomposition
p->pRoot = Bdc_ManDecompose_rec( p, pIsf );
+ p->timeTotal += clock() - clk;
+ p->numCalls++;
+ p->numNodes += p->nNodesNew;
if ( p->pRoot == NULL )
return -1;
+ if ( !Bdc_ManNodeVerify( p, pIsf, p->pRoot ) )
+ printf( "Bdc_ManDecompose(): Internal verification failed.\n" );
+// assert( Bdc_ManNodeVerify( p, pIsf, p->pRoot ) );
return p->nNodesNew;
}
diff --git a/src/aig/bdc/bdcDec.c b/src/aig/bdc/bdcDec.c
index 13a33196..55ce97a0 100644
--- a/src/aig/bdc/bdcDec.c
+++ b/src/aig/bdc/bdcDec.c
@@ -30,6 +30,82 @@
/**Function*************************************************************
+ Synopsis [Minimizes the support of the ISF.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Bdc_SuppMinimize2( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
+{
+ int v, clk;
+ if ( p->pPars->fVerbose )
+ clk = clock();
+ // compute support
+ pIsf->uSupp = Kit_TruthSupport( pIsf->puOn, p->nVars ) |
+ Kit_TruthSupport( pIsf->puOff, p->nVars );
+ // go through the support variables
+ for ( v = 0; v < p->nVars; v++ )
+ {
+ if ( (pIsf->uSupp & (1 << v)) == 0 )
+ continue;
+ Kit_TruthExistNew( p->puTemp1, pIsf->puOn, p->nVars, v );
+ Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, v );
+ if ( !Kit_TruthIsDisjoint( p->puTemp1, p->puTemp2, p->nVars ) )
+ continue;
+// if ( !Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) )
+// continue;
+ // remove the variable
+ Kit_TruthCopy( pIsf->puOn, p->puTemp1, p->nVars );
+ Kit_TruthCopy( pIsf->puOff, p->puTemp2, p->nVars );
+// Kit_TruthExist( pIsf->puOn, p->nVars, v );
+// Kit_TruthExist( pIsf->puOff, p->nVars, v );
+ pIsf->uSupp &= ~(1 << v);
+ }
+ if ( p->pPars->fVerbose )
+ p->timeSupps += clock() - clk;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Minimizes the support of the ISF.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
+{
+ int v, clk;
+ if ( p->pPars->fVerbose )
+ clk = clock();
+ // go through the support variables
+ pIsf->uSupp = 0;
+ for ( v = 0; v < p->nVars; v++ )
+ {
+ if ( !Kit_TruthVarInSupport( pIsf->puOn, p->nVars, v ) &&
+ !Kit_TruthVarInSupport( pIsf->puOff, p->nVars, v ) )
+ continue;
+ if ( Kit_TruthVarIsVacuous( pIsf->puOn, pIsf->puOff, p->nVars, v ) )
+ {
+ Kit_TruthExist( pIsf->puOn, p->nVars, v );
+ Kit_TruthExist( pIsf->puOff, p->nVars, v );
+ continue;
+ }
+ pIsf->uSupp |= (1 << v);
+ }
+ if ( p->pPars->fVerbose )
+ p->timeSupps += clock() - clk;
+}
+
+/**Function*************************************************************
+
Synopsis [Updates the ISF of the right after the left was decompoosed.]
Description []
@@ -418,12 +494,16 @@ Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL
// check if there is any reuse for the components
if ( WeightOrL + WeightOrR > WeightAndL + WeightAndR )
{
+ p->numReuse++;
+ p->numOrs++;
Bdc_IsfCopy( pIsfL, p->pIsfOL );
Bdc_IsfCopy( pIsfR, p->pIsfOR );
return BDC_TYPE_OR;
}
if ( WeightOrL + WeightOrR < WeightAndL + WeightAndR )
{
+ p->numReuse++;
+ p->numAnds++;
Bdc_IsfCopy( pIsfL, p->pIsfAL );
Bdc_IsfCopy( pIsfR, p->pIsfAR );
return BDC_TYPE_AND;
@@ -432,10 +512,16 @@ Bdc_Type_t Bdc_DecomposeStep( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL
// compare the two-component costs
if ( WeightOr > WeightAnd )
{
+ if ( WeightOr < BDC_SCALE )
+ p->numWeaks++;
+ p->numOrs++;
Bdc_IsfCopy( pIsfL, p->pIsfOL );
Bdc_IsfCopy( pIsfR, p->pIsfOR );
return BDC_TYPE_OR;
}
+ if ( WeightAnd < BDC_SCALE )
+ p->numWeaks++;
+ p->numAnds++;
Bdc_IsfCopy( pIsfL, p->pIsfAL );
Bdc_IsfCopy( pIsfR, p->pIsfAR );
return BDC_TYPE_AND;
@@ -456,6 +542,9 @@ int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bd
{
int Var, VarMin, nSuppMin, nSuppCur;
unsigned uSupp0, uSupp1;
+ int clk;
+ if ( p->pPars->fVerbose )
+ clk = clock();
VarMin = -1;
nSuppMin = 1000;
for ( Var = 0; Var < p->nVars; Var++ )
@@ -473,7 +562,7 @@ int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bd
{
nSuppMin = nSuppCur;
VarMin = Var;
-// break;
+ break;
}
}
if ( VarMin >= 0 )
@@ -485,6 +574,8 @@ int Bdc_DecomposeStepMux( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Isf_t * pIsfL, Bd
Bdc_SuppMinimize( p, pIsfL );
Bdc_SuppMinimize( p, pIsfR );
}
+ if ( p->pPars->fVerbose )
+ p->timeMuxes += clock() - clk;
return VarMin;
}
@@ -582,6 +673,7 @@ Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
Bdc_Fun_t * pFunc, * pFunc0, * pFunc1;
Bdc_Isf_t IsfL, * pIsfL = &IsfL;
Bdc_Isf_t IsfB, * pIsfR = &IsfB;
+ int iVar, clk;
/*
printf( "Init function (%d):\n", LocalCounter );
Extra_PrintBinary( stdout, pIsf->puOn, 1<<4 );printf("\n");
@@ -589,13 +681,27 @@ Extra_PrintBinary( stdout, pIsf->puOff, 1<<4 );printf("\n");
*/
// check computed results
assert( Kit_TruthIsDisjoint(pIsf->puOn, pIsf->puOff, p->nVars) );
- if ( pFunc = Bdc_TableLookup( p, pIsf ) )
+ if ( p->pPars->fVerbose )
+ clk = clock();
+ pFunc = Bdc_TableLookup( p, pIsf );
+ if ( p->pPars->fVerbose )
+ p->timeCache += clock() - clk;
+ if ( pFunc )
return pFunc;
// decide on the decomposition type
+ if ( p->pPars->fVerbose )
+ clk = clock();
Type = Bdc_DecomposeStep( p, pIsf, pIsfL, pIsfR );
+ if ( p->pPars->fVerbose )
+ p->timeCheck += clock() - clk;
if ( Type == BDC_TYPE_MUX )
{
- int iVar = Bdc_DecomposeStepMux( p, pIsf, pIsfL, pIsfR );
+ if ( p->pPars->fVerbose )
+ clk = clock();
+ iVar = Bdc_DecomposeStepMux( p, pIsf, pIsfL, pIsfR );
+ if ( p->pPars->fVerbose )
+ p->timeMuxes += clock() - clk;
+ p->numMuxes++;
pFunc0 = Bdc_ManDecompose_rec( p, pIsfL );
pFunc1 = Bdc_ManDecompose_rec( p, pIsfR );
if ( pFunc0 == NULL || pFunc1 == NULL )
@@ -625,9 +731,6 @@ Extra_PrintBinary( stdout, pIsf->puOff, 1<<4 );printf("\n");
// create new gate
pFunc = Bdc_ManCreateGate( p, pFunc0, pFunc1, Type );
}
- if ( pFunc == NULL )
- return NULL;
- assert( Bdc_ManNodeVerify( p, pIsf, pFunc ) );
return pFunc;
}
diff --git a/src/aig/bdc/bdcInt.h b/src/aig/bdc/bdcInt.h
index 5fda4301..afba0e67 100644
--- a/src/aig/bdc/bdcInt.h
+++ b/src/aig/bdc/bdcInt.h
@@ -106,6 +106,20 @@ struct Bdc_Man_t_
Bdc_Isf_t * pIsfAR, IsfAR;
// internal memory manager
Vec_Int_t * vMemory; // memory for internal truth tables
+ // statistics
+ int numCalls;
+ int numNodes;
+ int numMuxes;
+ int numAnds;
+ int numOrs;
+ int numWeaks;
+ int numReuse;
+ // runtime
+ int timeCache;
+ int timeCheck;
+ int timeMuxes;
+ int timeSupps;
+ int timeTotal;
};
// working with complemented attributes of objects
@@ -132,11 +146,12 @@ static inline void Bdc_IsfNot( Bdc_Isf_t * p ) { unsign
/*=== bdcDec.c ==========================================================*/
extern Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
+extern void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
+extern int Bdc_ManNodeVerify( Bdc_Man_t * p, Bdc_Isf_t * pIsf, Bdc_Fun_t * pFunc );
/*=== bdcTable.c ==========================================================*/
extern Bdc_Fun_t * Bdc_TableLookup( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
extern void Bdc_TableAdd( Bdc_Man_t * p, Bdc_Fun_t * pFunc );
extern void Bdc_TableClear( Bdc_Man_t * p );
-extern void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
extern int Bdc_TableCheckContainment( Bdc_Man_t * p, Bdc_Isf_t * pIsf, unsigned * puTruth );
#ifdef __cplusplus
diff --git a/src/aig/bdc/bdcTable.c b/src/aig/bdc/bdcTable.c
index b7f10344..3a6ed126 100644
--- a/src/aig/bdc/bdcTable.c
+++ b/src/aig/bdc/bdcTable.c
@@ -30,39 +30,6 @@
/**Function*************************************************************
- Synopsis [Minimizes the support of the ISF.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
-{
- int v;
- // compute support
- pIsf->uSupp = Kit_TruthSupport( pIsf->puOn, p->nVars ) |
- Kit_TruthSupport( pIsf->puOff, p->nVars );
- // go through the support variables
- for ( v = 0; v < p->nVars; v++ )
- {
- if ( (pIsf->uSupp & (1 << v)) == 0 )
- continue;
- Kit_TruthExistNew( p->puTemp1, pIsf->puOn, p->nVars, v );
- Kit_TruthExistNew( p->puTemp2, pIsf->puOff, p->nVars, v );
- if ( !Kit_TruthIsDisjoint( p->puTemp1, p->puTemp2, p->nVars ) )
- continue;
- // remove the variable
- Kit_TruthCopy( pIsf->puOn, p->puTemp1, p->nVars );
- Kit_TruthCopy( pIsf->puOff, p->puTemp2, p->nVars );
- pIsf->uSupp &= ~(1 << v);
- }
-}
-
-/**Function*************************************************************
-
Synopsis [Checks containment of the function in the ISF.]
Description []
generated by cgit v1.2.3 (git 2.25.1) at 2025-01-13 22:31:48 +0000