summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2008-03-14 08:01:00 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2008-03-14 08:01:00 -0700
commitff6f0943362c30176fd1f961bcbd19e188cee520 (patch)
treefc2b888c8403ee04fb7d473433c1eb3bcc5ef8c5
parent6205eaaee3a840dd076f9baaac67720d85d6a680 (diff)
downloadabc-ff6f0943362c30176fd1f961bcbd19e188cee520.tar.gz
abc-ff6f0943362c30176fd1f961bcbd19e188cee520.tar.bz2
abc-ff6f0943362c30176fd1f961bcbd19e188cee520.zip
Version abc80314
-rw-r--r--abc.dsp4
-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
-rw-r--r--src/aig/dar/darRefact.c29
-rw-r--r--src/aig/kit/kit.h1
-rw-r--r--src/aig/kit/kitTruth.c58
-rw-r--r--src/base/abci/abc.c65
-rw-r--r--src/base/abci/abcBidec.c126
-rw-r--r--src/base/abci/abcIf.c86
-rw-r--r--src/base/abci/module.make1
-rw-r--r--src/map/if/ifTime.c2
-rw-r--r--src/map/if/ifTruth.c4
-rw-r--r--src/opt/lpk/lpkCore.c21
-rw-r--r--src/opt/mfs/mfsCore.c44
-rw-r--r--src/opt/mfs/mfsInt.h8
-rw-r--r--src/opt/mfs/mfsMan.c6
-rw-r--r--src/opt/mfs/mfsSat.c12
19 files changed, 523 insertions, 137 deletions
diff --git a/abc.dsp b/abc.dsp
index 9c043b24..89c0ebc7 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -194,6 +194,10 @@ SOURCE=.\src\base\abci\abcBalance.c
# End Source File
# Begin Source File
+SOURCE=.\src\base\abci\abcBidec.c
+# End Source File
+# Begin Source File
+
SOURCE=.\src\base\abci\abcBmc.c
# End Source File
# Begin Source File
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 []
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
index a765ec30..e814840f 100644
--- a/src/aig/dar/darRefact.c
+++ b/src/aig/dar/darRefact.c
@@ -21,6 +21,9 @@
#include "darInt.h"
#include "kit.h"
+#include "bdc.h"
+#include "bdcInt.h"
+
////////////////////////////////////////////////////////////////////////
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
@@ -44,6 +47,9 @@ struct Ref_Man_t_
Kit_Graph_t * pGraphBest; // the best factored form
int GainBest; // the best gain
int LevelBest; // the level of node with the best gain
+ // bi-decomposition
+ Bdc_Par_t DecPars; // decomposition parameters
+ Bdc_Man_t * pManDec; // decomposition manager
// node statistics
int nNodesInit; // the initial number of nodes
int nNodesTried; // the number of nodes tried
@@ -111,6 +117,11 @@ Ref_Man_t * Dar_ManRefStart( Aig_Man_t * pAig, Dar_RefPar_t * pPars )
p->vMemory = Vec_IntAlloc( 1 << 16 );
p->vCutNodes = Vec_PtrAlloc( 256 );
p->vLeavesBest = Vec_PtrAlloc( pPars->nLeafMax );
+ // alloc bi-decomposition manager
+ p->DecPars.nVarsMax = pPars->nLeafMax;
+ p->DecPars.fVerbose = pPars->fVerbose;
+ p->DecPars.fVeryVerbose = 0;
+// p->pManDec = Bdc_ManAlloc( &p->DecPars );
return p;
}
@@ -151,6 +162,8 @@ void Dar_ManRefPrintStats( Ref_Man_t * p )
***********************************************************************/
void Dar_ManRefStop( Ref_Man_t * p )
{
+ if ( p->pManDec )
+ Bdc_ManFree( p->pManDec );
if ( p->pPars->fVerbose )
Dar_ManRefPrintStats( p );
Vec_VecFree( p->vCuts );
@@ -381,6 +394,13 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
if ( RetValue > -1 )
{
pGraphCur = Kit_SopFactor( p->vMemory, 0, Vec_PtrSize(vCut), p->vMemory );
+/*
+{
+ int RetValue;
+ RetValue = Bdc_ManDecompose( p->pManDec, pTruth, NULL, Vec_PtrSize(vCut), NULL, 1000 );
+ printf( "Graph = %d. Bidec = %d.\n", Kit_GraphNodeNum(pGraphCur), RetValue );
+}
+*/
nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required );
if ( nNodesAdded > -1 )
{
@@ -403,9 +423,17 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
// try negative phase
Kit_TruthNot( pTruth, pTruth, Vec_PtrSize(vCut) );
RetValue = Kit_TruthIsop( pTruth, Vec_PtrSize(vCut), p->vMemory, 0 );
+// Kit_TruthNot( pTruth, pTruth, Vec_PtrSize(vCut) );
if ( RetValue > -1 )
{
pGraphCur = Kit_SopFactor( p->vMemory, 1, Vec_PtrSize(vCut), p->vMemory );
+/*
+{
+ int RetValue;
+ RetValue = Bdc_ManDecompose( p->pManDec, pTruth, NULL, Vec_PtrSize(vCut), NULL, 1000 );
+ printf( "Graph = %d. Bidec = %d.\n", Kit_GraphNodeNum(pGraphCur), RetValue );
+}
+*/
nNodesAdded = Dar_RefactTryGraph( p->pAig, pObj, vCut, pGraphCur, nNodesSaved - !p->pPars->fUseZeros, Required );
if ( nNodesAdded > -1 )
{
@@ -426,6 +454,7 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
Kit_GraphFree( pGraphCur );
}
}
+
return p->GainBest;
}
diff --git a/src/aig/kit/kit.h b/src/aig/kit/kit.h
index 06a93cf0..23e3ce8d 100644
--- a/src/aig/kit/kit.h
+++ b/src/aig/kit/kit.h
@@ -564,6 +564,7 @@ extern void Kit_TruthCofactor0( unsigned * pTruth, int nVars, int iVa
extern void Kit_TruthCofactor1( unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthCofactor0New( unsigned * pOut, unsigned * pIn, int nVars, int iVar );
extern void Kit_TruthCofactor1New( unsigned * pOut, unsigned * pIn, int nVars, int iVar );
+extern int Kit_TruthVarIsVacuous( unsigned * pOnset, unsigned * pOffset, int nVars, int iVar );
extern void Kit_TruthExist( unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthExistNew( unsigned * pRes, unsigned * pTruth, int nVars, int iVar );
extern void Kit_TruthExistSet( unsigned * pRes, unsigned * pTruth, int nVars, unsigned uMask );
diff --git a/src/aig/kit/kitTruth.c b/src/aig/kit/kitTruth.c
index dab60132..9ddc7562 100644
--- a/src/aig/kit/kitTruth.c
+++ b/src/aig/kit/kitTruth.c
@@ -520,6 +520,64 @@ void Kit_TruthCofactor1New( unsigned * pOut, unsigned * pIn, int nVars, int iVar
}
}
+/**Function*************************************************************
+
+ Synopsis [Computes negative cofactor of the function.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Kit_TruthVarIsVacuous( unsigned * pOnset, unsigned * pOffset, int nVars, int iVar )
+{
+ int nWords = Kit_TruthWordNum( nVars );
+ int i, k, Step;
+
+ assert( iVar < nVars );
+ switch ( iVar )
+ {
+ case 0:
+ for ( i = 0; i < nWords; i++ )
+ if ( ((pOnset[i] & (pOffset[i] >> 1)) | (pOffset[i] & (pOnset[i] >> 1))) & 0x55555555 )
+ return 0;
+ return 1;
+ case 1:
+ for ( i = 0; i < nWords; i++ )
+ if ( ((pOnset[i] & (pOffset[i] >> 2)) | (pOffset[i] & (pOnset[i] >> 2))) & 0x33333333 )
+ return 0;
+ return 1;
+ case 2:
+ for ( i = 0; i < nWords; i++ )
+ if ( ((pOnset[i] & (pOffset[i] >> 4)) | (pOffset[i] & (pOnset[i] >> 4))) & 0x0F0F0F0F )
+ return 0;
+ return 1;
+ case 3:
+ for ( i = 0; i < nWords; i++ )
+ if ( ((pOnset[i] & (pOffset[i] >> 8)) | (pOffset[i] & (pOnset[i] >> 8))) & 0x00FF00FF )
+ return 0;
+ return 1;
+ case 4:
+ for ( i = 0; i < nWords; i++ )
+ if ( ((pOnset[i] & (pOffset[i] >> 16)) || (pOffset[i] & (pOnset[i] >> 16))) & 0x0000FFFF )
+ return 0;
+ return 1;
+ default:
+ Step = (1 << (iVar - 5));
+ for ( k = 0; k < nWords; k += 2*Step )
+ {
+ for ( i = 0; i < Step; i++ )
+ if ( (pOnset[i] & pOffset[Step+i]) | (pOffset[i] & pOnset[Step+i]) )
+ return 0;
+ pOnset += 2*Step;
+ pOffset += 2*Step;
+ }
+ return 1;
+ }
+}
+
/**Function*************************************************************
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f366a612..4262cd0d 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -93,6 +93,7 @@ static int Abc_CommandSop ( Abc_Frame_t * pAbc, int argc, char ** arg
static int Abc_CommandBdd ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandAig ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandReorder ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandBidec ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandOrder ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMuxes ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandExtSeqDcs ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -275,6 +276,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Various", "bdd", Abc_CommandBdd, 0 );
Cmd_CommandAdd( pAbc, "Various", "aig", Abc_CommandAig, 0 );
Cmd_CommandAdd( pAbc, "Various", "reorder", Abc_CommandReorder, 0 );
+ Cmd_CommandAdd( pAbc, "Various", "bidec", Abc_CommandBidec, 1 );
Cmd_CommandAdd( pAbc, "Various", "order", Abc_CommandOrder, 0 );
Cmd_CommandAdd( pAbc, "Various", "muxes", Abc_CommandMuxes, 1 );
Cmd_CommandAdd( pAbc, "Various", "ext_seq_dcs", Abc_CommandExtSeqDcs, 0 );
@@ -5202,6 +5204,69 @@ usage:
SeeAlso []
***********************************************************************/
+int Abc_CommandBidec( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ FILE * pOut, * pErr;
+ Abc_Ntk_t * pNtk;
+ int c;
+ int fVerbose;
+ extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose );
+
+ pNtk = Abc_FrameReadNtk(pAbc);
+ pOut = Abc_FrameReadOut(pAbc);
+ pErr = Abc_FrameReadErr(pAbc);
+
+ // set defaults
+ fVerbose = 0;
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'v':
+ fVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+
+ if ( pNtk == NULL )
+ {
+ fprintf( pErr, "Empty network.\n" );
+ return 1;
+ }
+
+ // get the new network
+ if ( !Abc_NtkIsAigLogic(pNtk) )
+ {
+ fprintf( pErr, "Bi-decomposition only works when node functions are AIGs (run \"aig\").\n" );
+ return 1;
+ }
+ Abc_NtkBidecResyn( pNtk, fVerbose );
+ return 0;
+
+usage:
+ fprintf( pErr, "usage: bidec [-vh]\n" );
+ fprintf( pErr, "\t applies bi-decomposition to local functions of the nodes\n" );
+ fprintf( pErr, "\t-v : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );
+ fprintf( pErr, "\t-h : print the command usage\n");
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_CommandOrder( Abc_Frame_t * pAbc, int argc, char ** argv )
{
FILE * pOut, * pErr, * pFile;
diff --git a/src/base/abci/abcBidec.c b/src/base/abci/abcBidec.c
new file mode 100644
index 00000000..ad332314
--- /dev/null
+++ b/src/base/abci/abcBidec.c
@@ -0,0 +1,126 @@
+/**CFile****************************************************************
+
+ FileName [abcBidec.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Interface to bi-decomposition.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcBidec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+
+#include "bdc.h"
+#include "bdcInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj ) { return Hop_NotCond( Bdc_Regular(pObj)->pCopy, Bdc_IsComplement(pObj) ); }
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Resynthesizes nodes using bi-decomposition.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare )
+{
+ unsigned * pTruth;
+ Bdc_Fun_t * pFunc;
+ int i;
+ assert( nVars <= 16 );
+ // derive truth table
+ pTruth = Abc_ConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 );
+ if ( Hop_IsComplement(pRoot) )
+ Extra_TruthNot( pTruth, pTruth, nVars );
+ // decompose truth table
+ Bdc_ManDecompose( p, pTruth, puCare, nVars, NULL, 1000 );
+ // convert back into HOP
+ Bdc_FunWithId( p, 0 )->pCopy = Hop_ManConst1( pHop );
+ for ( i = 0; i < nVars; i++ )
+ Bdc_FunWithId( p, i+1 )->pCopy = Hop_ManPi( pHop, i );
+ for ( i = nVars + 1; i < p->nNodes; i++ )
+ {
+ pFunc = Bdc_FunWithId( p, i );
+ pFunc->pCopy = Hop_And( pHop, Bdc_FunCopyHop(pFunc->pFan0), Bdc_FunCopyHop(pFunc->pFan1) );
+ }
+ return Bdc_FunCopyHop(p->pRoot);
+}
+
+/**Function*************************************************************
+
+ Synopsis [Resynthesizes nodes using bi-decomposition.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose )
+{
+ Bdc_Par_t Pars = {0}, * pPars = &Pars;
+ Bdc_Man_t * p;
+ Abc_Obj_t * pObj;
+ Vec_Int_t * vTruth;
+ int i, nGainTotal = 0, nNodes1, nNodes2;
+ int clk = clock();
+ assert( Abc_NtkIsLogic(pNtk) );
+ if ( !Abc_NtkToAig(pNtk) )
+ return;
+ pPars->nVarsMax = Abc_NtkGetFaninMax( pNtk );
+ pPars->fVerbose = fVerbose;
+ if ( pPars->nVarsMax > 15 )
+ {
+ if ( fVerbose )
+ printf( "Resynthesis is not performed for nodes with more than 15 inputs.\n" );
+ pPars->nVarsMax = 15;
+ }
+ vTruth = Vec_IntAlloc( 0 );
+ p = Bdc_ManAlloc( pPars );
+ Abc_NtkForEachNode( pNtk, pObj, i )
+ {
+ if ( Abc_ObjFaninNum(pObj) > 15 )
+ continue;
+ nNodes1 = Hop_DagSize(pObj->pData);
+ pObj->pData = Abc_NodeIfNodeResyn( p, pNtk->pManFunc, pObj->pData, Abc_ObjFaninNum(pObj), vTruth, NULL );
+ nNodes2 = Hop_DagSize(pObj->pData);
+ nGainTotal += nNodes1 - nNodes2;
+ }
+ Bdc_ManFree( p );
+ Vec_IntFree( vTruth );
+ if ( fVerbose )
+ {
+ printf( "Total gain in AIG nodes = %d. ", nGainTotal );
+ PRT( "Total runtime", clock() - clk );
+ }
+}
+
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcIf.c b/src/base/abci/abcIf.c
index a20925b2..35ec473f 100644
--- a/src/base/abci/abcIf.c
+++ b/src/base/abci/abcIf.c
@@ -34,7 +34,7 @@ static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_O
static Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk );
extern void Abc_NtkBddReorder( Abc_Ntk_t * pNtk, int fVerbose );
-extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk );
+extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose );
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@@ -86,7 +86,7 @@ Abc_Ntk_t * Abc_NtkIf( Abc_Ntk_t * pNtk, If_Par_t * pPars )
return NULL;
If_ManStop( pIfMan );
if ( pPars->fBidec && pPars->nLutSize <= 8 )
- Abc_NtkBidecResyn( pNtkNew );
+ Abc_NtkBidecResyn( pNtkNew, 0 );
// duplicate EXDC
if ( pNtk->pExdc )
@@ -256,7 +256,7 @@ Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t
pNodeNew = Abc_NtkCreateNode( pNtkNew );
pCutBest = If_ObjCutBest( pIfObj );
// if ( pIfMan->pPars->pLutLib && pIfMan->pPars->pLutLib->fVarPinDelays )
-// If_CutRotatePins( pIfMan, pCutBest );
+ If_CutRotatePins( pIfMan, pCutBest );
if ( pIfMan->pPars->fUseCnfs || pIfMan->pPars->fUseMv )
{
If_CutForEachLeafReverse( pIfMan, pCutBest, pIfLeaf, i )
@@ -551,86 +551,6 @@ Vec_Ptr_t * Abc_NtkFindGoodOrder( Abc_Ntk_t * pNtk )
}
-#include "bdc.h"
-#include "bdcInt.h"
-
-static inline Hop_Obj_t * Bdc_FunCopyHop( Bdc_Fun_t * pObj ) { return Hop_NotCond( Bdc_Regular(pObj)->pCopy, Bdc_IsComplement(pObj) ); }
-
-/**Function*************************************************************
-
- Synopsis [Resynthesizes nodes using bi-decomposition.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth )
-{
- unsigned * pTruth;
- Bdc_Fun_t * pFunc;
- int i;
- // derive truth table
- pTruth = Abc_ConvertAigToTruth( pHop, Hop_Regular(pRoot), nVars, vTruth, 0 );
- if ( Hop_IsComplement(pRoot) )
- Extra_TruthNot( pTruth, pTruth, nVars );
- // decompose truth table
- Bdc_ManDecompose( p, pTruth, NULL, nVars, NULL, 1000 );
- // convert back into HOP
- Bdc_FunWithId( p, 0 )->pCopy = Hop_ManConst1( pHop );
- for ( i = 0; i < nVars; i++ )
- Bdc_FunWithId( p, i+1 )->pCopy = Hop_ManPi( pHop, i );
- for ( i = nVars + 1; i < p->nNodes; i++ )
- {
- pFunc = Bdc_FunWithId( p, i );
- pFunc->pCopy = Hop_And( pHop, Bdc_FunCopyHop(pFunc->pFan0), Bdc_FunCopyHop(pFunc->pFan1) );
- }
- return Bdc_FunCopyHop(p->pRoot);
-}
-
-/**Function*************************************************************
-
- Synopsis [Resynthesizes nodes using bi-decomposition.]
-
- Description []
-
- SideEffects []
-
- SeeAlso []
-
-***********************************************************************/
-void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk )
-{
- Bdc_Par_t Pars = {0}, * pPars = &Pars;
- Bdc_Man_t * p;
- Abc_Obj_t * pObj;
- Vec_Int_t * vTruth;
- int i, nGainTotal = 0, nNodes1, nNodes2;
- int clk = clock();
- pPars->nVarsMax = Abc_NtkGetFaninMax( pNtk );
- if ( pPars->nVarsMax > 8 )
- {
- printf( "Resynthesis is not performed.\n" );
- return;
- }
- vTruth = Vec_IntAlloc( 0 );
- p = Bdc_ManAlloc( pPars );
- Abc_NtkForEachNode( pNtk, pObj, i )
- {
- nNodes1 = Hop_DagSize(pObj->pData);
- pObj->pData = Abc_NodeIfNodeResyn( p, pNtk->pManFunc, pObj->pData, Abc_ObjFaninNum(pObj), vTruth );
- nNodes2 = Hop_DagSize(pObj->pData);
- nGainTotal += nNodes1 - nNodes2;
- }
-// printf( "LUTs = %d. Total gain in AIG nodes = %d. ", Abc_NtkNodeNum(pNtk), nGainTotal );
-// PRT( "Time", clock() - clk );
- Bdc_ManFree( p );
- Vec_IntFree( vTruth );
-}
-
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 55b724b8..a2f879e3 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -2,6 +2,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcAttach.c \
src/base/abci/abcAuto.c \
src/base/abci/abcBalance.c \
+ src/base/abci/abcBidec.c \
src/base/abci/abcBmc.c \
src/base/abci/abcCas.c \
src/base/abci/abcClpBdd.c \
diff --git a/src/map/if/ifTime.c b/src/map/if/ifTime.c
index 33bbdf74..59322cad 100644
--- a/src/map/if/ifTime.c
+++ b/src/map/if/ifTime.c
@@ -238,7 +238,7 @@ void If_CutRotatePins( If_Man_t * p, If_Cut_t * pCut )
float PinDelays[32];
// int PinPerm[32];
int i;
- assert( p->pPars->pLutLib && p->pPars->pLutLib->fVarPinDelays && p->pPars->fTruth );
+// assert( p->pPars->pLutLib && p->pPars->pLutLib->fVarPinDelays && p->pPars->fTruth );
If_CutForEachLeaf( p, pCut, pLeaf, i )
PinDelays[i] = If_ObjCutBest(pLeaf)->Delay;
If_CutTruthPermute( p->puTemp[0], If_CutTruth(pCut), If_CutLeaveNum(pCut), PinDelays, If_CutLeaves(pCut) );
diff --git a/src/map/if/ifTruth.c b/src/map/if/ifTruth.c
index a3a7e1ee..637a42b4 100644
--- a/src/map/if/ifTruth.c
+++ b/src/map/if/ifTruth.c
@@ -146,16 +146,18 @@ void If_CutTruthPermute( unsigned * pOut, unsigned * pIn, int nVars, float * pDe
for ( i = 0; i < nVars - 1; i++ )
{
if ( pDelays[i] >= pDelays[i+1] )
+// if ( pDelays[i] <= pDelays[i+1] )
continue;
tTemp = pDelays[i]; pDelays[i] = pDelays[i+1]; pDelays[i+1] = tTemp;
Temp = pVars[i]; pVars[i] = pVars[i+1]; pVars[i+1] = Temp;
+ if ( pOut && pIn )
If_TruthSwapAdjacentVars( pOut, pIn, nVars, i );
pTemp = pOut; pOut = pIn; pIn = pTemp;
fChange = 1;
Counter++;
}
}
- if ( Counter & 1 )
+ if ( pOut && pIn && (Counter & 1) )
If_TruthCopy( pOut, pIn, nVars );
}
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index 34911c20..80080d50 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -500,6 +500,7 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
Lpk_Man_t * p;
Abc_Obj_t * pObj;
double Delta;
+// int * pnFanouts, nObjMax;
int i, Iter, nNodes, nNodesPrev, clk = clock();
assert( Abc_NtkIsLogic(pNtk) );
@@ -554,6 +555,14 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
p->nTotalNodes = Abc_NtkNodeNum(pNtk);
}
+/*
+ // save the number of fanouts of all objects
+ nObjMax = Abc_NtkObjNumMax( pNtk );
+ pnFanouts = ALLOC( int, nObjMax );
+ memset( pnFanouts, 0, sizeof(int) * nObjMax );
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ pnFanouts[pObj->Id] = Abc_ObjFanoutNum(pObj);
+*/
// iterate over the network
nNodesPrev = p->nNodesTotal;
@@ -604,6 +613,18 @@ int Lpk_Resynthesize( Abc_Ntk_t * pNtk, Lpk_Par_t * pPars )
break;
}
Abc_NtkStopReverseLevels( pNtk );
+/*
+ // report the fanout changes
+ Abc_NtkForEachObj( pNtk, pObj, i )
+ {
+ if ( i >= nObjMax )
+ continue;
+ if ( Abc_ObjFanoutNum(pObj) - pnFanouts[pObj->Id] == 0 )
+ continue;
+ printf( "%d ", Abc_ObjFanoutNum(pObj) - pnFanouts[pObj->Id] );
+ }
+ printf( "\n" );
+*/
if ( pPars->fVerbose )
{
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index 4e4f7490..bde2ad42 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -100,7 +100,10 @@ p->timeSat += clock() - clk;
***********************************************************************/
int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
- int clk;
+ Hop_Obj_t * pObj;
+ extern Hop_Obj_t * Abc_NodeIfNodeResyn( Bdc_Man_t * p, Hop_Man_t * pHop, Hop_Obj_t * pRoot, int nVars, Vec_Int_t * vTruth, unsigned * puCare );
+
+ int nGain, clk;
p->nNodesTried++;
// prepare data structure for this node
Mfs_ManClean( p );
@@ -128,6 +131,16 @@ clk = clock();
// solve the SAT problem
Abc_NtkMfsSolveSat( p, pNode );
p->timeSat += clock() - clk;
+ // minimize the local function of the node using bi-decomposition
+ assert( p->nFanins == Abc_ObjFaninNum(pNode) );
+ pObj = Abc_NodeIfNodeResyn( p->pManDec, pNode->pNtk->pManFunc, pNode->pData, p->nFanins, p->vTruth, p->uCare );
+ nGain = Hop_DagSize(pNode->pData) - Hop_DagSize(pObj);
+ if ( nGain >= 0 )
+ {
+ p->nNodesDec++;
+ p->nNodesGained += nGain;
+ pNode->pData = pObj;
+ }
return 1;
}
@@ -146,6 +159,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
{
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters );
+ Bdc_Par_t Pars = {0}, * pDecPars = &Pars;
ProgressBar * pProgress;
Mfs_Man_t * p;
Abc_Obj_t * pObj;
@@ -157,8 +171,8 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
nFaninMax = Abc_NtkGetFaninMax(pNtk);
if ( nFaninMax > MFS_FANIN_MAX )
{
- printf( "Some nodes have more than %d fanins. Quitting.\n", MFS_FANIN_MAX );
- return 1;
+ printf( "Nodes with more than %d fanins will node be processed.\n", MFS_FANIN_MAX );
+ nFaninMax = MFS_FANIN_MAX;
}
// perform the network sweep
Abc_NtkSweep( pNtk, 0 );
@@ -186,11 +200,16 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
{
if ( p->pCare != NULL )
printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) );
- else
- printf( "Performing optimization without constraints.\n" );
+// else
+// printf( "Performing optimization without constraints.\n" );
}
if ( !pPars->fResub )
- printf( "Currently don't-cares are not used but the stats are printed.\n" );
+ {
+ pDecPars->nVarsMax = nFaninMax;
+ pDecPars->fVerbose = pPars->fVerbose;
+ p->vTruth = Vec_IntAlloc( 0 );
+ p->pManDec = Bdc_ManAlloc( pDecPars );
+ }
// label the register outputs
if ( p->pCare )
@@ -211,15 +230,26 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
{
if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
continue;
+ if ( Abc_ObjFaninNum(pObj) > MFS_FANIN_MAX )
+ continue;
if ( !p->pPars->fVeryVerbose )
Extra_ProgressBarUpdate( pProgress, i, NULL );
if ( pPars->fResub )
Abc_NtkMfsResub( p, pObj );
- else
+ else if ( Abc_ObjFaninNum(pObj) > 1 && Abc_ObjFaninNum(pObj) <= 12 )
Abc_NtkMfsNode( p, pObj );
}
Extra_ProgressBarStop( pProgress );
Abc_NtkStopReverseLevels( pNtk );
+
+ // perform the sweeping
+ if ( !pPars->fResub )
+ {
+ extern void Abc_NtkBidecResyn( Abc_Ntk_t * pNtk, int fVerbose );
+ Abc_NtkSweep( pNtk, 0 );
+ Abc_NtkBidecResyn( pNtk, 0 );
+ }
+
p->nTotalNodesEnd = Abc_NtkNodeNum(pNtk);
p->nTotalEdgesEnd = Abc_NtkGetTotalFanins(pNtk);
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index 91395d03..f4da45ef 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -35,12 +35,13 @@ extern "C" {
#include "cnf.h"
#include "satSolver.h"
#include "satStore.h"
+#include "bdc.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
-#define MFS_FANIN_MAX 10
+#define MFS_FANIN_MAX 12
typedef struct Mfs_Man_t_ Mfs_Man_t;
struct Mfs_Man_t_
@@ -64,6 +65,11 @@ struct Mfs_Man_t_
int nCexes; // the numbe rof current counter-examples
int nSatCalls;
int nSatCexes;
+ // used for bidecomposition
+ Vec_Int_t * vTruth;
+ Bdc_Man_t * pManDec;
+ int nNodesDec;
+ int nNodesGained;
// solving data
Aig_Man_t * pAigWin; // window AIG with constraints
Cnf_Dat_t * pCnf; // the CNF for the window
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index 17ca40fc..f1b3f44c 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -131,6 +131,8 @@ void Mfs_ManPrint( Mfs_Man_t * p )
1.0 * (p->nMintsTotal-p->nMintsCare) / p->nMintsTotal );
// printf( "Average ratio of sequential DCs in the global space = %5.2f.\n",
// 1.0-(p->dTotalRatios/p->nNodesTried) );
+ printf( "Nodes resyn = %d. Ratio = %5.2f. Total AIG node gain = %d.\n",
+ p->nNodesDec, 1.0 * p->nNodesDec / p->nNodesTried, p->nNodesGained );
}
/*
PRTP( "Win", p->timeWin , p->timeTotal );
@@ -158,6 +160,10 @@ void Mfs_ManStop( Mfs_Man_t * p )
{
if ( p->pPars->fVerbose )
Mfs_ManPrint( p );
+ if ( p->vTruth )
+ Vec_IntFree( p->vTruth );
+ if ( p->pManDec )
+ Bdc_ManFree( p->pManDec );
if ( p->pCare )
Aig_ManStop( p->pCare );
if ( p->vSuppsInv )
diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c
index efb09b39..2529e207 100644
--- a/src/opt/mfs/mfsSat.c
+++ b/src/opt/mfs/mfsSat.c
@@ -110,6 +110,18 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
Extra_PrintBinary( stdout, p->uCare, (1<<p->nFanins) );
printf( "\n" );
}
+
+ // map the care
+ if ( p->nFanins > 4 )
+ return;
+ if ( p->nFanins == 4 )
+ p->uCare[0] = p->uCare[0] | (p->uCare[0] << 16);
+ if ( p->nFanins == 3 )
+ p->uCare[0] = p->uCare[0] | (p->uCare[0] << 8) | (p->uCare[0] << 16) | (p->uCare[0] << 24);
+ if ( p->nFanins == 2 )
+ p->uCare[0] = p->uCare[0] | (p->uCare[0] << 4) | (p->uCare[0] << 8) | (p->uCare[0] << 12) |
+ (p->uCare[0] << 16) | (p->uCare[0] << 20) | (p->uCare[0] << 24) | (p->uCare[0] << 28);
+ assert( p->nFanins != 1 );
}
////////////////////////////////////////////////////////////////////////