summaryrefslogtreecommitdiffstats
path: root/src/opt/mfs
diff options
context:
space:
mode:
Diffstat (limited to 'src/opt/mfs')
-rw-r--r--src/opt/mfs/mfs.h6
-rw-r--r--src/opt/mfs/mfsCore.c116
-rw-r--r--src/opt/mfs/mfsDiv.c303
-rw-r--r--src/opt/mfs/mfsInt.h35
-rw-r--r--src/opt/mfs/mfsInter.c254
-rw-r--r--src/opt/mfs/mfsMan.c66
-rw-r--r--src/opt/mfs/mfsResub.c276
-rw-r--r--src/opt/mfs/mfsSat.c24
-rw-r--r--src/opt/mfs/mfsStrash.c41
-rw-r--r--src/opt/mfs/mfsWin.c2
-rw-r--r--src/opt/mfs/module.make3
11 files changed, 1072 insertions, 54 deletions
diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h
index a7ca3819..9fc6a253 100644
--- a/src/opt/mfs/mfs.h
+++ b/src/opt/mfs/mfs.h
@@ -43,7 +43,11 @@ struct Mfs_Par_t_
// general parameters
int nWinTfoLevs; // the maximum fanout levels
int nFanoutsMax; // the maximum number of fanouts
- int nGrowthLevel; // the maximum allowed growth in level after one iteration of resynthesis
+ int nDepthMax; // the maximum number of logic levels
+ int nDivMax; // the maximum number of divisors
+ int nWinSizeMax; // the maximum size of the window
+ int nGrowthLevel; // the maximum allowed growth in level
+ int fResub; // performs resubstitution
int fArea; // performs optimization for area
int fDelay; // performs optimization for delay
int fVerbose; // enable basic stats
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
index fe0d84c3..332a6ad9 100644
--- a/src/opt/mfs/mfsCore.c
+++ b/src/opt/mfs/mfsCore.c
@@ -6,7 +6,7 @@
PackageName [The good old minimization with complete don't-cares.]
- Synopsis []
+ Synopsis [Core procedures of this package.]
Author [Alan Mishchenko]
@@ -39,9 +39,64 @@
SeeAlso []
***********************************************************************/
+int Abc_NtkMfsResub( Mfs_Man_t * p, Abc_Obj_t * pNode )
+{
+ int clk;
+ p->nNodesTried++;
+ // prepare data structure for this node
+ Mfs_ManClean( p );
+ // compute window roots, window support, and window nodes
+clk = clock();
+ p->vRoots = Abc_MfsComputeRoots( pNode, p->pPars->nWinTfoLevs, p->pPars->nFanoutsMax );
+ p->vSupp = Abc_NtkNodeSupport( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
+ p->vNodes = Abc_NtkDfsNodes( p->pNtk, (Abc_Obj_t **)Vec_PtrArray(p->vRoots), Vec_PtrSize(p->vRoots) );
+p->timeWin += clock() - clk;
+ if ( p->pPars->nWinSizeMax && Vec_PtrSize(p->vNodes) > p->pPars->nWinSizeMax )
+ return 1;
+ // compute the divisors of the window
+clk = clock();
+ p->vDivs = Abc_MfsComputeDivisors( p, pNode, Abc_ObjRequiredLevel(pNode) - 1 );
+p->timeDiv += clock() - clk;
+ // construct AIG for the window
+clk = clock();
+ p->pAigWin = Abc_NtkConstructAig( p, pNode );
+p->timeAig += clock() - clk;
+ // translate it into CNF
+clk = clock();
+ p->pCnf = Cnf_DeriveSimple( p->pAigWin, 1 + Vec_PtrSize(p->vDivs) );
+p->timeCnf += clock() - clk;
+ // create the SAT problem
+clk = clock();
+ p->pSat = Abc_MfsCreateSolverResub( p, NULL, 0 );
+ if ( p->pSat == NULL )
+ {
+ p->nNodesBad++;
+ return 1;
+ }
+ // solve the SAT problem
+ if ( p->pPars->fArea )
+ Abc_NtkMfsResubArea( p, pNode );
+ else
+ Abc_NtkMfsResubEdge( p, pNode );
+p->timeSat += clock() - clk;
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
{
int clk;
+ p->nNodesTried++;
// prepare data structure for this node
Mfs_ManClean( p );
// compute window roots, window support, and window nodes
@@ -80,9 +135,14 @@ p->timeSat += clock() - clk;
***********************************************************************/
int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
{
+ extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters );
+
+ ProgressBar * pProgress;
Mfs_Man_t * p;
Abc_Obj_t * pObj;
- int i, Counter;
+ int i, clk = clock();
+ int nTotalNodesBeg = Abc_NtkNodeNum(pNtk);
+ int nTotalEdgesBeg = Abc_NtkGetTotalFanins(pNtk);
assert( Abc_NtkIsLogic(pNtk) );
if ( Abc_NtkGetFaninMax(pNtk) > MFS_FANIN_MAX )
@@ -99,30 +159,57 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
return 0;
}
assert( Abc_NtkHasAig(pNtk) );
- if ( pNtk->pManExdc != NULL )
- printf( "Performing don't-care computation with don't-cares.\n" );
// start the manager
- p = Mfs_ManAlloc();
- p->pPars = pPars;
+ p = Mfs_ManAlloc( pPars );
p->pNtk = pNtk;
- p->pCare = pNtk->pManExdc;
+ if ( pNtk->pExcare )
+ {
+ Abc_Ntk_t * pTemp;
+ pTemp = Abc_NtkStrash( pNtk->pExcare, 0, 0, 0 );
+ p->pCare = Abc_NtkToDar( pTemp, 0 );
+ Abc_NtkDelete( pTemp );
+ }
+ if ( pPars->fVerbose )
+ {
+ if ( p->pCare != NULL )
+ printf( "Performing optimization with %d external care clauses.\n", Aig_ManPoNum(p->pCare) );
+ else
+ printf( "Performing optimization without constraints.\n" );
+ }
+ if ( !pPars->fResub )
+ printf( "Currently don't-cares are not used but the stats are printed.\n" );
// label the register outputs
if ( p->pCare )
{
- Counter = 1;
Abc_NtkForEachCi( pNtk, pObj, i )
- if ( Abc_ObjFaninNum(pObj) == 0 )
- pObj->pData = NULL;
- else
- pObj->pData = (void *)Counter++;
- assert( Counter == Abc_NtkLatchNum(pNtk) + 1 );
+ pObj->pData = (void *)i;
}
+
+ // compute levels
+ Abc_NtkLevel( pNtk );
+ Abc_NtkStartReverseLevels( pNtk, pPars->nGrowthLevel );
// compute don't-cares for each node
+ p->nTotalNodesBeg = nTotalNodesBeg;
+ p->nTotalEdgesBeg = nTotalEdgesBeg;
+ pProgress = Extra_ProgressBarStart( stdout, Abc_NtkObjNumMax(pNtk) );
Abc_NtkForEachNode( pNtk, pObj, i )
- Abc_NtkMfsNode( p, pObj );
+ {
+ if ( p->pPars->nDepthMax && (int)pObj->Level > p->pPars->nDepthMax )
+ continue;
+ if ( !p->pPars->fVeryVerbose )
+ Extra_ProgressBarUpdate( pProgress, i, NULL );
+ if ( pPars->fResub )
+ Abc_NtkMfsResub( p, pObj );
+ else
+ Abc_NtkMfsNode( p, pObj );
+ }
+ Extra_ProgressBarStop( pProgress );
+ Abc_NtkStopReverseLevels( pNtk );
+ p->nTotalNodesEnd = Abc_NtkNodeNum(pNtk);
+ p->nTotalEdgesEnd = Abc_NtkGetTotalFanins(pNtk);
// undo labesl
if ( p->pCare )
@@ -132,6 +219,7 @@ int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
}
// free the manager
+ p->timeTotal = clock() - clk;
Mfs_ManStop( p );
return 1;
}
diff --git a/src/opt/mfs/mfsDiv.c b/src/opt/mfs/mfsDiv.c
new file mode 100644
index 00000000..7b156b97
--- /dev/null
+++ b/src/opt/mfs/mfsDiv.c
@@ -0,0 +1,303 @@
+/**CFile****************************************************************
+
+ FileName [mfsDiv.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [The good old minimization with complete don't-cares.]
+
+ Synopsis [Procedures to compute candidate divisors.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: mfsDiv.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfsInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Marks and collects the TFI cone of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_MfsWinMarkTfi_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vCone )
+{
+ Abc_Obj_t * pFanin;
+ int i;
+ if ( Abc_NodeIsTravIdCurrent(pObj) )
+ return;
+ Abc_NodeSetTravIdCurrent( pObj );
+ if ( Abc_ObjIsCi(pObj) )
+ {
+ Vec_PtrPush( vCone, pObj );
+ return;
+ }
+ assert( Abc_ObjIsNode(pObj) );
+ // visit the fanins of the node
+ Abc_ObjForEachFanin( pObj, pFanin, i )
+ Abc_MfsWinMarkTfi_rec( pFanin, vCone );
+ Vec_PtrPush( vCone, pObj );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Marks and collects the TFI cone of the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_MfsWinMarkTfi( Abc_Obj_t * pNode )
+{
+ Vec_Ptr_t * vCone;
+ vCone = Vec_PtrAlloc( 100 );
+ Abc_MfsWinMarkTfi_rec( pNode, vCone );
+ return vCone;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Marks the TFO of the collected nodes up to the given level.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_MfsWinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit )
+{
+ Abc_Obj_t * pFanout;
+ int i;
+ if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit )
+ return;
+ if ( Abc_NodeIsTravIdCurrent(pObj) )
+ return;
+ Abc_NodeSetTravIdCurrent( pObj );
+ Abc_ObjForEachFanout( pObj, pFanout, i )
+ Abc_MfsWinSweepLeafTfo_rec( pFanout, nLevelLimit );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Dereferences the node's MFFC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_MfsNodeDeref_rec( Abc_Obj_t * pNode )
+{
+ Abc_Obj_t * pFanin;
+ int i, Counter = 1;
+ if ( Abc_ObjIsCi(pNode) )
+ return 0;
+ Abc_NodeSetTravIdCurrent( pNode );
+ Abc_ObjForEachFanin( pNode, pFanin, i )
+ {
+ assert( pFanin->vFanouts.nSize > 0 );
+ if ( --pFanin->vFanouts.nSize == 0 )
+ Counter += Abc_MfsNodeDeref_rec( pFanin );
+ }
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [References the node's MFFC.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_MfsNodeRef_rec( Abc_Obj_t * pNode )
+{
+ Abc_Obj_t * pFanin;
+ int i, Counter = 1;
+ if ( Abc_ObjIsCi(pNode) )
+ return 0;
+ Abc_ObjForEachFanin( pNode, pFanin, i )
+ {
+ if ( pFanin->vFanouts.nSize++ == 0 )
+ Counter += Abc_MfsNodeRef_rec( pFanin );
+ }
+ return Counter;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Labels MFFC of the node with the current trav ID.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_MfsWinVisitMffc( Abc_Obj_t * pNode )
+{
+ int Count1, Count2;
+ assert( Abc_ObjIsNode(pNode) );
+ // dereference the node (mark with the current trav ID)
+ Count1 = Abc_MfsNodeDeref_rec( pNode );
+ // reference it back
+ Count2 = Abc_MfsNodeRef_rec( pNode );
+ assert( Count1 == Count2 );
+ return Count1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Computes divisors and add them to nodes in the window.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDivMax )
+{
+ Vec_Ptr_t * vCone, * vDivs;
+ Abc_Obj_t * pObj, * pFanout, * pFanin;
+ int k, f, m;
+ int nDivsPlus = 0, nTrueSupp;
+ assert( p->vDivs == NULL );
+
+ // mark the TFI with the current trav ID
+ Abc_NtkIncrementTravId( pNode->pNtk );
+ vCone = Abc_MfsWinMarkTfi( pNode );
+
+ // count the number of PIs
+ nTrueSupp = 0;
+ Vec_PtrForEachEntry( vCone, pObj, k )
+ nTrueSupp += Abc_ObjIsCi(pObj);
+// printf( "%d(%d) ", Vec_PtrSize(p->vSupp), m );
+
+ // mark with the current trav ID those nodes that should not be divisors:
+ // (1) the node and its TFO
+ // (2) the MFFC of the node
+ // (3) the node's fanins (these are treated as a special case)
+ Abc_NtkIncrementTravId( pNode->pNtk );
+ Abc_MfsWinSweepLeafTfo_rec( pNode, nLevDivMax );
+ Abc_MfsWinVisitMffc( pNode );
+ Abc_ObjForEachFanin( pNode, pObj, k )
+ Abc_NodeSetTravIdCurrent( pObj );
+
+ // at this point the nodes are marked with two trav IDs:
+ // nodes to be collected as divisors are marked with previous trav ID
+ // nodes to be avoided as divisors are marked with current trav ID
+
+ // start collecting the divisors
+ vDivs = Vec_PtrAlloc( p->pPars->nDivMax );
+ Vec_PtrForEachEntry( vCone, pObj, k )
+ {
+ if ( !Abc_NodeIsTravIdPrevious(pObj) )
+ continue;
+ if ( (int)pObj->Level > nLevDivMax )
+ continue;
+ Vec_PtrPush( vDivs, pObj );
+ if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
+ break;
+ }
+ Vec_PtrFree( vCone );
+
+ // explore the fanouts of already collected divisors
+ if ( Vec_PtrSize(vDivs) < p->pPars->nDivMax )
+ Vec_PtrForEachEntry( vDivs, pObj, k )
+ {
+ // consider fanouts of this node
+ Abc_ObjForEachFanout( pObj, pFanout, f )
+ {
+ // stop if there are too many fanouts
+ if ( f > 20 )
+ break;
+ // skip nodes that are already added
+ if ( Abc_NodeIsTravIdPrevious(pFanout) )
+ continue;
+ // skip nodes in the TFO or in the MFFC of node
+ if ( Abc_NodeIsTravIdCurrent(pFanout) )
+ continue;
+ // skip COs
+ if ( !Abc_ObjIsNode(pFanout) )
+ continue;
+ // skip nodes with large level
+ if ( (int)pFanout->Level >= nLevDivMax )
+ continue;
+ // skip nodes whose fanins are not divisors
+ Abc_ObjForEachFanin( pFanout, pFanin, m )
+ if ( !Abc_NodeIsTravIdPrevious(pFanin) )
+ break;
+ if ( m < Abc_ObjFaninNum(pFanout) )
+ continue;
+ // make sure this divisor in not among the nodes
+// Vec_PtrForEachEntry( p->vNodes, pFanin, m )
+// assert( pFanout != pFanin );
+ // add the node to the divisors
+ Vec_PtrPush( vDivs, pFanout );
+// Vec_PtrPush( p->vNodes, pFanout );
+ Vec_PtrPushUnique( p->vNodes, pFanout );
+ Abc_NodeSetTravIdPrevious( pFanout );
+ nDivsPlus++;
+ if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
+ break;
+ }
+ if ( Vec_PtrSize(vDivs) >= p->pPars->nDivMax )
+ break;
+ }
+
+ // sort the divisors by level in the increasing order
+ Vec_PtrSort( vDivs, Abc_NodeCompareLevelsIncrease );
+
+ // add the fanins of the node
+ Abc_ObjForEachFanin( pNode, pFanin, k )
+ Vec_PtrPush( vDivs, pFanin );
+
+/*
+ printf( "Node level = %d. ", Abc_ObjLevel(p->pNode) );
+ Vec_PtrForEachEntryStart( vDivs, pObj, k, Vec_PtrSize(vDivs)-p->nDivsPlus )
+ printf( "%d ", Abc_ObjLevel(pObj) );
+ printf( "\n" );
+*/
+//printf( "%d ", p->nDivsPlus );
+// printf( "(%d+%d)(%d+%d+%d) ", Vec_PtrSize(p->vSupp), Vec_PtrSize(p->vNodes),
+// nTrueSupp, Vec_PtrSize(vDivs)-nTrueSupp-nDivsPlus, nDivsPlus );
+ return vDivs;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
index 6ba5903e..54826bc1 100644
--- a/src/opt/mfs/mfsInt.h
+++ b/src/opt/mfs/mfsInt.h
@@ -34,6 +34,7 @@ extern "C" {
#include "aig.h"
#include "cnf.h"
#include "satSolver.h"
+#include "satStore.h"
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
@@ -52,11 +53,23 @@ struct Mfs_Man_t_
Vec_Ptr_t * vRoots; // the roots of the window
Vec_Ptr_t * vSupp; // the support of the window
Vec_Ptr_t * vNodes; // the internal nodes of the window
+ Vec_Ptr_t * vDivs; // the divisors of the node
+ Vec_Int_t * vDivLits; // the SAT literals of divisor nodes
Vec_Int_t * vProjVars; // the projection variables
+ // intermediate simulation data
+ Vec_Ptr_t * vDivCexes; // the counter-example for dividors
+ int nDivWords; // the number of words
+ int nCexes; // the numbe rof current counter-examples
+ int nSatCalls;
+ int nSatCexes;
// solving data
Aig_Man_t * pAigWin; // window AIG with constraints
Cnf_Dat_t * pCnf; // the CNF for the window
sat_solver * pSat; // the SAT solver used
+ Int_Man_t * pMan; // interpolation manager;
+ Vec_Int_t * vMem; // memory for intermediate SOPs
+ Vec_Vec_t * vLevels; // levelized structure for updating
+ Vec_Ptr_t * vFanins; // the new set of fanins
// the result of solving
int nFanins; // the number of fanins
int nWords; // the number of words
@@ -64,14 +77,24 @@ struct Mfs_Man_t_
unsigned uCare[(MFS_FANIN_MAX<=5)?1:1<<(MFS_FANIN_MAX-5)]; // the computed care-set
// performance statistics
int nNodesTried;
- int nNodesBad;
+ int nNodesResub;
+ int nNodesGained;
int nMintsCare;
int nMintsTotal;
+ int nNodesBad;
+ // node/edge stats
+ int nTotalNodesBeg;
+ int nTotalNodesEnd;
+ int nTotalEdgesBeg;
+ int nTotalEdgesEnd;
// statistics
int timeWin;
+ int timeDiv;
int timeAig;
int timeCnf;
int timeSat;
+ int timeInt;
+ int timeTotal;
};
////////////////////////////////////////////////////////////////////////
@@ -86,10 +109,18 @@ struct Mfs_Man_t_
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+/*=== mfsDiv.c ==========================================================*/
+extern Vec_Ptr_t * Abc_MfsComputeDivisors( Mfs_Man_t * p, Abc_Obj_t * pNode, int nLevDivMax );
+/*=== mfsInter.c ==========================================================*/
+extern sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands );
+extern Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands );
/*=== mfsMan.c ==========================================================*/
-extern Mfs_Man_t * Mfs_ManAlloc();
+extern Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars );
extern void Mfs_ManStop( Mfs_Man_t * p );
extern void Mfs_ManClean( Mfs_Man_t * p );
+/*=== mfsResub.c ==========================================================*/
+extern int Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode );
+extern int Abc_NtkMfsResubEdge( Mfs_Man_t * p, Abc_Obj_t * pNode );
/*=== mfsSat.c ==========================================================*/
extern void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode );
/*=== mfsStrash.c ==========================================================*/
diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c
new file mode 100644
index 00000000..16db5061
--- /dev/null
+++ b/src/opt/mfs/mfsInter.c
@@ -0,0 +1,254 @@
+/**CFile****************************************************************
+
+ FileName [mfsInter.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [The good old minimization with complete don't-cares.]
+
+ Synopsis [Procedures for computing resub function by interpolation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: mfsInter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfsInt.h"
+#include "kit.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Adds constraints for the two-input AND-gate.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_MfsSatAddXor( sat_solver * pSat, int iVarA, int iVarB, int iVarC )
+{
+ lit Lits[3];
+
+ Lits[0] = toLitCond( iVarA, 1 );
+ Lits[1] = toLitCond( iVarB, 1 );
+ Lits[2] = toLitCond( iVarC, 1 );
+ if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
+ return 0;
+
+ Lits[0] = toLitCond( iVarA, 1 );
+ Lits[1] = toLitCond( iVarB, 0 );
+ Lits[2] = toLitCond( iVarC, 0 );
+ if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
+ return 0;
+
+ Lits[0] = toLitCond( iVarA, 0 );
+ Lits[1] = toLitCond( iVarB, 1 );
+ Lits[2] = toLitCond( iVarC, 0 );
+ if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
+ return 0;
+
+ Lits[0] = toLitCond( iVarA, 0 );
+ Lits[1] = toLitCond( iVarB, 0 );
+ Lits[2] = toLitCond( iVarC, 1 );
+ if ( !sat_solver_addclause( pSat, Lits, Lits + 3 ) )
+ return 0;
+
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Creates miter for checking resubsitution.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands )
+{
+ sat_solver * pSat;
+ Aig_Obj_t * pObjPo;
+ int Lits[2], status, iVar, i, c;
+
+ // get the literal for the output of F
+ pObjPo = Aig_ManPo( p->pAigWin, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) - 1 );
+ Lits[0] = toLitCond( p->pCnf->pVarNums[pObjPo->Id], 0 );
+
+ // collect the outputs of the divisors
+ Vec_IntClear( p->vProjVars );
+ Vec_PtrForEachEntryStart( p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Vec_PtrSize(p->vDivs) )
+ {
+ assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
+ Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] );
+ }
+ assert( Vec_IntSize(p->vProjVars) == Vec_PtrSize(p->vDivs) );
+
+ // start the solver
+ pSat = sat_solver_new();
+ sat_solver_setnvars( pSat, 2 * p->pCnf->nVars + Vec_PtrSize(p->vDivs) );
+ if ( pCands )
+ sat_solver_store_alloc( pSat );
+
+ // load the first copy of the clauses
+ for ( i = 0; i < p->pCnf->nClauses; i++ )
+ {
+ if ( !sat_solver_addclause( pSat, p->pCnf->pClauses[i], p->pCnf->pClauses[i+1] ) )
+ {
+ sat_solver_delete( pSat );
+ return NULL;
+ }
+ }
+ // add the clause for the first output of F
+ if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
+ {
+ sat_solver_delete( pSat );
+ return NULL;
+ }
+
+ // bookmark the clauses of A
+ if ( pCands )
+ sat_solver_store_mark_clauses_a( pSat );
+
+ // transform the literals
+ for ( i = 0; i < p->pCnf->nLiterals; i++ )
+ p->pCnf->pClauses[0][i] += 2 * p->pCnf->nVars;
+ // load the second copy of the clauses
+ for ( i = 0; i < p->pCnf->nClauses; i++ )
+ {
+ if ( !sat_solver_addclause( pSat, p->pCnf->pClauses[i], p->pCnf->pClauses[i+1] ) )
+ {
+ sat_solver_delete( pSat );
+ return NULL;
+ }
+ }
+ // transform the literals
+ for ( i = 0; i < p->pCnf->nLiterals; i++ )
+ p->pCnf->pClauses[0][i] -= 2 * p->pCnf->nVars;
+ // add the clause for the second output of F
+ Lits[0] = 2 * p->pCnf->nVars + lit_neg( Lits[0] );
+ if ( !sat_solver_addclause( pSat, Lits, Lits+1 ) )
+ {
+ sat_solver_delete( pSat );
+ return NULL;
+ }
+
+ if ( pCands )
+ {
+ // add relevant clauses for EXOR gates
+ for ( c = 0; c < nCands; c++ )
+ {
+ // get the variable number of this divisor
+ i = lit_var( pCands[c] ) - 2 * p->pCnf->nVars;
+ // get the corresponding SAT variable
+ iVar = Vec_IntEntry( p->vProjVars, i );
+ // add the corresponding EXOR gate
+ if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
+ {
+ sat_solver_delete( pSat );
+ return NULL;
+ }
+ // add the corresponding clause
+ if ( !sat_solver_addclause( pSat, pCands + c, pCands + c + 1 ) )
+ {
+ sat_solver_delete( pSat );
+ return NULL;
+ }
+ }
+ // bookmark the roots
+ sat_solver_store_mark_roots( pSat );
+ }
+ else
+ {
+ // add the clauses for the EXOR gates - and remember their outputs
+ Vec_IntForEachEntry( p->vProjVars, iVar, i )
+ {
+ if ( !Abc_MfsSatAddXor( pSat, iVar, iVar + p->pCnf->nVars, 2 * p->pCnf->nVars + i ) )
+ {
+ sat_solver_delete( pSat );
+ return NULL;
+ }
+ Vec_IntWriteEntry( p->vProjVars, i, 2 * p->pCnf->nVars + i );
+ }
+ // simplify the solver
+ status = sat_solver_simplify(pSat);
+ if ( status == 0 )
+ {
+// printf( "Abc_MfsCreateSolverResub(): SAT solver construction has failed. Skipping node.\n" );
+ sat_solver_delete( pSat );
+ return NULL;
+ }
+ }
+ return pSat;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs interpolation.]
+
+ Description [Derives the new function of the node.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Hop_Obj_t * Abc_NtkMfsInterplate( Mfs_Man_t * p, int * pCands, int nCands )
+{
+ extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
+
+ sat_solver * pSat;
+ Sto_Man_t * pCnf = NULL;
+ unsigned * puTruth;
+ Kit_Graph_t * pGraph;
+ Hop_Obj_t * pFunc;
+ int nFanins, status;
+
+ // derive the SAT solver for interpolation
+ pSat = Abc_MfsCreateSolverResub( p, pCands, nCands );
+
+ // solve the problem
+ status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+ if ( status != l_False )
+ {
+ printf( "Abc_NtkMfsInterplate(): Internal error. The problem is not UNSAT.\n" );
+ return NULL;
+ }
+ // get the learned clauses
+ pCnf = sat_solver_store_release( pSat );
+ sat_solver_delete( pSat );
+
+ // derive the interpolant
+ nFanins = Int_ManInterpolate( p->pMan, pCnf, 0, &puTruth );
+ Sto_ManFree( pCnf );
+ assert( nFanins == nCands );
+
+ // transform interpolant into AIG
+ pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem );
+ pFunc = Kit_GraphToHop( p->pNtk->pManFunc, pGraph );
+ Kit_GraphFree( pGraph );
+ return pFunc;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
index 1341e373..67981d5a 100644
--- a/src/opt/mfs/mfsMan.c
+++ b/src/opt/mfs/mfsMan.c
@@ -6,7 +6,7 @@
PackageName [The good old minimization with complete don't-cares.]
- Synopsis [Procedure to manipulation the manager.]
+ Synopsis [Procedures working with the manager.]
Author [Alan Mishchenko]
@@ -28,7 +28,6 @@
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-
/**Function*************************************************************
Synopsis []
@@ -40,13 +39,21 @@
SeeAlso []
***********************************************************************/
-Mfs_Man_t * Mfs_ManAlloc()
+Mfs_Man_t * Mfs_ManAlloc( Mfs_Par_t * pPars )
{
Mfs_Man_t * p;
// start the manager
p = ALLOC( Mfs_Man_t, 1 );
memset( p, 0, sizeof(Mfs_Man_t) );
+ p->pPars = pPars;
p->vProjVars = Vec_IntAlloc( 100 );
+ p->vDivLits = Vec_IntAlloc( 100 );
+ p->nDivWords = Aig_BitWordNum(p->pPars->nDivMax + MFS_FANIN_MAX);
+ p->vDivCexes = Vec_PtrAllocSimInfo( p->pPars->nDivMax+MFS_FANIN_MAX+1, p->nDivWords );
+ p->pMan = Int_ManAlloc();
+ p->vMem = Vec_IntAlloc( 0 );
+ p->vLevels = Vec_VecStart( 32 );
+ p->vFanins = Vec_PtrAlloc( 32 );
return p;
}
@@ -75,12 +82,15 @@ void Mfs_ManClean( Mfs_Man_t * p )
Vec_PtrFree( p->vSupp );
if ( p->vNodes )
Vec_PtrFree( p->vNodes );
+ if ( p->vDivs )
+ Vec_PtrFree( p->vDivs );
p->pAigWin = NULL;
- p->pCnf = NULL;
- p->pSat = NULL;
+ p->pCnf = NULL;
+ p->pSat = NULL;
p->vRoots = NULL;
- p->vSupp = NULL;
+ p->vSupp = NULL;
p->vNodes = NULL;
+ p->vDivs = NULL;
}
/**Function*************************************************************
@@ -96,14 +106,31 @@ void Mfs_ManClean( Mfs_Man_t * p )
***********************************************************************/
void Mfs_ManPrint( Mfs_Man_t * p )
{
- printf( "Nodes tried = %d. Bad nodes = %d.\n",
- p->nNodesTried, p->nNodesBad );
- printf( "Total mints = %d. Care mints = %d. Ratio = %5.2f.\n",
- p->nMintsTotal, p->nMintsCare, 1.0 * p->nMintsCare / p->nMintsTotal );
- PRT( "Win", p->timeWin );
- PRT( "Aig", p->timeAig );
- PRT( "Cnf", p->timeCnf );
- PRT( "Sat", p->timeSat );
+ if ( p->pPars->fResub )
+ {
+ printf( "Reduction in nodes = %5d. (%.2f %%) ",
+ p->nTotalNodesBeg-p->nTotalNodesEnd,
+ 100.0*(p->nTotalNodesBeg-p->nTotalNodesEnd)/p->nTotalNodesBeg );
+ printf( "Reduction in edges = %5d. (%.2f %%) ",
+ p->nTotalEdgesBeg-p->nTotalEdgesEnd,
+ 100.0*(p->nTotalEdgesBeg-p->nTotalEdgesEnd)/p->nTotalEdgesBeg );
+ printf( "\n" );
+ printf( "Nodes = %d. Tried = %d. Resub = %d. Skipped = %d. SAT calls = %d.\n",
+ Abc_NtkNodeNum(p->pNtk), p->nNodesTried, p->nNodesResub, p->nNodesBad, p->nSatCalls );
+ }
+ else
+ {
+ printf( "Nodes = %d. Care mints = %d. Total mints = %d. Ratio = %5.2f.\n",
+ p->nNodesTried, p->nMintsCare, p->nMintsTotal, 1.0 * p->nMintsCare / p->nMintsTotal );
+ }
+ PRTP( "Win", p->timeWin , p->timeTotal );
+ PRTP( "Div", p->timeDiv , p->timeTotal );
+ PRTP( "Aig", p->timeAig , p->timeTotal );
+ PRTP( "Cnf", p->timeCnf , p->timeTotal );
+ PRTP( "Sat", p->timeSat-p->timeInt , p->timeTotal );
+ PRTP( "Int", p->timeInt , p->timeTotal );
+ PRTP( "ALL", p->timeTotal , p->timeTotal );
+
}
/**Function*************************************************************
@@ -119,9 +146,18 @@ void Mfs_ManPrint( Mfs_Man_t * p )
***********************************************************************/
void Mfs_ManStop( Mfs_Man_t * p )
{
- Mfs_ManPrint( p );
+ if ( p->pPars->fVerbose )
+ Mfs_ManPrint( p );
+ if ( p->pCare )
+ Aig_ManStop( p->pCare );
Mfs_ManClean( p );
+ Int_ManFree( p->pMan );
+ Vec_IntFree( p->vMem );
+ Vec_VecFree( p->vLevels );
+ Vec_PtrFree( p->vFanins );
Vec_IntFree( p->vProjVars );
+ Vec_IntFree( p->vDivLits );
+ Vec_PtrFree( p->vDivCexes );
free( p );
}
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
new file mode 100644
index 00000000..ae1132f2
--- /dev/null
+++ b/src/opt/mfs/mfsResub.c
@@ -0,0 +1,276 @@
+/**CFile****************************************************************
+
+ FileName [mfsResub.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [The good old minimization with complete don't-cares.]
+
+ Synopsis [Procedures to perform resubstitution.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: mfsResub.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfsInt.h"
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Updates the network after resubstitution.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkMfsUpdateNetwork( Mfs_Man_t * p, Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc )
+{
+ 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
+//printf( "Replacing node " ); Abc_ObjPrint( stdout, pObj );
+//printf( "Inserting node " ); Abc_ObjPrint( stdout, pObjNew );
+ // update the level of the node
+ Abc_NtkUpdate( pObj, pObjNew, p->vLevels );
+}
+
+/**Function*************************************************************
+
+ Synopsis [Tries resubstitution.]
+
+ Description [Returns 1 if it is feasible, or 0 if c-ex is found.]
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkMfsTryResubOnce( Mfs_Man_t * p, int * pCands, int nCands )
+{
+ unsigned * pData, * pDataTot;
+ int RetValue, iVar, i;
+ p->nSatCalls++;
+ RetValue = sat_solver_solve( p->pSat, pCands, pCands + nCands, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+ assert( RetValue == l_False || RetValue == l_True );
+ if ( RetValue == l_False )
+ return 1;
+ p->nSatCexes++;
+ // store the counter-example
+ pData = Vec_PtrEntry( p->vDivCexes, p->nCexes++ );
+ assert( pData[0] == 0 );
+ Vec_IntForEachEntry( p->vProjVars, iVar, i )
+ {
+ if ( sat_solver_var_value( p->pSat, iVar ) )
+ Aig_InfoSetBit( pData, i );
+ }
+ // AND the result with the previous ones
+ pDataTot = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
+ for ( i = 0; i < p->nDivWords; i++ )
+ pDataTot[i] &= pData[i];
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs resubstitution for the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkMfsSolveSatResub( Mfs_Man_t * p, Abc_Obj_t * pNode, int iFanin, int fOnlyRemove )
+{
+ int fVeryVerbose = p->pPars->fVeryVerbose && Vec_PtrSize(p->vDivs) < 80;
+ unsigned * pData;
+ int pCands[MFS_FANIN_MAX];
+ int iVar, i, nCands, clk;
+ Abc_Obj_t * pFanin;
+ Hop_Obj_t * pFunc;
+ assert( iFanin >= 0 );
+
+ // clean simulation info
+ Vec_PtrCleanSimInfo( p->vDivCexes, 0, p->nDivWords );
+ pData = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
+ memset( pData, 0xFF, sizeof(unsigned) * p->nDivWords );
+ p->nCexes = 0;
+
+ if ( fVeryVerbose )
+ {
+ printf( "\n" );
+ printf( "Node %5d : Level = %2d. Divs = %3d. Fanin = %d (out of %d). MFFC = %d\n",
+ pNode->Id, pNode->Level, Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode),
+ iFanin, Abc_ObjFaninNum(pNode),
+ Abc_ObjFanoutNum(Abc_ObjFanin(pNode, iFanin)) == 1 ? Abc_NodeMffcLabel(Abc_ObjFanin(pNode, iFanin)) : 0 );
+ }
+
+ // try fanins without the critical fanin
+ nCands = 0;
+ Vec_PtrClear( p->vFanins );
+ Abc_ObjForEachFanin( pNode, pFanin, i )
+ {
+ if ( i == iFanin )
+ continue;
+ Vec_PtrPush( p->vFanins, pFanin );
+ iVar = Vec_PtrSize(p->vDivs) - Abc_ObjFaninNum(pNode) + i;
+ pCands[nCands++] = toLitCond( Vec_IntEntry( p->vProjVars, iVar ), 1 );
+ }
+ if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands ) )
+ {
+ if ( fVeryVerbose )
+ printf( "Node %d: Fanin %d can be removed.\n", pNode->Id, iFanin );
+ p->nNodesResub++;
+// p->nNodesGained += Abc_NodeMffcLabel(pNode);
+clk = clock();
+ // derive the function
+ pFunc = Abc_NtkMfsInterplate( p, pCands, nCands );
+ // update the network
+ Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
+p->timeInt += clock() - clk;
+ return 1;
+ }
+
+ if ( fOnlyRemove )
+ return 0;
+
+ // shift variables by 1
+ for ( i = Vec_PtrSize(p->vFanins); i > 0; i-- )
+ p->vFanins->pArray[i] = p->vFanins->pArray[i-1];
+ p->vFanins->nSize++;
+
+ if ( fVeryVerbose )
+ {
+ for ( i = 0; i < 8; i++ )
+ printf( " " );
+ for ( i = 0; i < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); i++ )
+ printf( "%d", i % 10 );
+ for ( i = 0; i < Abc_ObjFaninNum(pNode); i++ )
+ if ( i == iFanin )
+ printf( "*" );
+ else
+ printf( "%c", 'a' + i );
+ printf( "\n" );
+ }
+ iVar = -1;
+ while ( 1 )
+ {
+ if ( fVeryVerbose )
+ {
+ printf( "%3d: %2d ", p->nCexes, iVar );
+ pData = Vec_PtrEntry( p->vDivCexes, p->nCexes-1 );
+// Extra_PrintBinary( stdout, pData, Vec_PtrSize(p->vDivs) );
+ for ( i = 0; i < Vec_PtrSize(p->vDivs); i++ )
+ printf( "%d", Aig_InfoHasBit(pData, i) );
+ printf( "\n" );
+ }
+
+ // find the next divisor to try
+ pData = Vec_PtrEntry( p->vDivCexes, Vec_PtrSize(p->vDivs) );
+ for ( iVar = 0; iVar < Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode); iVar++ )
+ if ( Aig_InfoHasBit( pData, iVar ) )
+ break;
+ if ( iVar == Vec_PtrSize(p->vDivs)-Abc_ObjFaninNum(pNode) )
+ return 0;
+ pCands[nCands] = toLitCond( Vec_IntEntry(p->vProjVars, iVar), 1 );
+ if ( Abc_NtkMfsTryResubOnce( p, pCands, nCands+1 ) )
+ {
+ if ( fVeryVerbose )
+ printf( "Node %d: Fanin %d can be replaced by divisor %d.\n", pNode->Id, iFanin, iVar );
+ p->nNodesResub++;
+// p->nNodesGained += Abc_NodeMffcLabel(pNode);
+clk = clock();
+ // derive the function
+ pFunc = Abc_NtkMfsInterplate( p, pCands, nCands+1 );
+ // update the network
+// Vec_PtrPush( p->vFanins, Vec_PtrEntry(p->vDivs, iVar) );
+ Vec_PtrWriteEntry( p->vFanins, 0, Vec_PtrEntry(p->vDivs, iVar) );
+ Abc_NtkMfsUpdateNetwork( p, pNode, p->vFanins, pFunc );
+p->timeInt += clock() - clk;
+ return 1;
+ }
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs resubstitution for the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkMfsResubArea( Mfs_Man_t * p, Abc_Obj_t * pNode )
+{
+ Abc_Obj_t * pFanin;
+ int i;
+ Abc_ObjForEachFanin( pNode, pFanin, i )
+ if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
+ {
+ if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0 ) )
+ return 1;
+ }
+ return 0;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Performs resubstitution for the node.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkMfsResubEdge( Mfs_Man_t * p, Abc_Obj_t * pNode )
+{
+ Abc_Obj_t * pFanin;
+ int i;
+ Abc_ObjForEachFanin( pNode, pFanin, i )
+ if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) == 1 )
+ {
+ if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 0 ) )
+ return 1;
+ }
+ Abc_ObjForEachFanin( pNode, pFanin, i )
+ if ( !Abc_ObjIsCi(pFanin) && Abc_ObjFanoutNum(pFanin) != 1 )
+ {
+ if ( Abc_NtkMfsSolveSatResub( p, pNode, i, 1 ) )
+ return 1;
+ }
+ return 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c
index d995000f..efb09b39 100644
--- a/src/opt/mfs/mfsSat.c
+++ b/src/opt/mfs/mfsSat.c
@@ -6,7 +6,7 @@
PackageName [The good old minimization with complete don't-cares.]
- Synopsis []
+ Synopsis [Procedures to compute don't-cares using SAT.]
Author [Alan Mishchenko]
@@ -43,9 +43,11 @@ int Abc_NtkMfsSolveSat_iter( Mfs_Man_t * p )
{
int Lits[MFS_FANIN_MAX];
int RetValue, iVar, b, Mint;
- RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
- if ( RetValue != l_True )
+ RetValue = sat_solver_solve( p->pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+ assert( RetValue == l_False || RetValue == l_True );
+ if ( RetValue == l_False )
return 0;
+ p->nCares++;
// add SAT assignment to the solver
Mint = 0;
Vec_IntForEachEntry( p->vProjVars, iVar, b )
@@ -95,15 +97,19 @@ void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
memset( p->uCare, 0, sizeof(unsigned) * p->nWords );
// iterate through the SAT assignments
- while ( Abc_NtkMfsSolveSat_iter( p ) );
-
- // write statistics
p->nCares = 0;
- for ( i = 0; i < p->nWords; i++ )
- p->nCares += Aig_WordCountOnes( p->uCare[i] );
+ while ( Abc_NtkMfsSolveSat_iter(p) );
+ // write statistics
p->nMintsCare += p->nCares;
- p->nMintsTotal += 32 * p->nWords;
+ p->nMintsTotal += (1<<p->nFanins);
+
+ if ( p->pPars->fVeryVerbose )
+ {
+ printf( "Node %4d : Care = %2d. Total = %2d. ", pNode->Id, p->nCares, (1<<p->nFanins) );
+ Extra_PrintBinary( stdout, p->uCare, (1<<p->nFanins) );
+ printf( "\n" );
+ }
}
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/mfs/mfsStrash.c b/src/opt/mfs/mfsStrash.c
index 7b467936..8e945045 100644
--- a/src/opt/mfs/mfsStrash.c
+++ b/src/opt/mfs/mfsStrash.c
@@ -144,18 +144,18 @@ Aig_Obj_t * Abc_NtkConstructAig_rec( Mfs_Man_t * p, Abc_Obj_t * pNode, Aig_Man_t
SeeAlso []
***********************************************************************/
-Aig_Obj_t * Abc_NtkConstructCare_rec( Mfs_Man_t * p, Aig_Obj_t * pObj, Aig_Man_t * pMan )
+Aig_Obj_t * Abc_NtkConstructCare_rec( Aig_Man_t * pCare, Aig_Obj_t * pObj, Aig_Man_t * pMan )
{
Aig_Obj_t * pObj0, * pObj1;
- if ( Aig_ObjIsTravIdCurrent( pMan, pObj ) )
+ if ( Aig_ObjIsTravIdCurrent( pCare, pObj ) )
return pObj->pData;
- Aig_ObjSetTravIdCurrent( pMan, pObj );
+ Aig_ObjSetTravIdCurrent( pCare, pObj );
if ( Aig_ObjIsPi(pObj) )
return pObj->pData = NULL;
- pObj0 = Abc_NtkConstructCare_rec( p, Aig_ObjFanin0(pObj), pMan );
+ pObj0 = Abc_NtkConstructCare_rec( pCare, Aig_ObjFanin0(pObj), pMan );
if ( pObj0 == NULL )
return pObj->pData = NULL;
- pObj1 = Abc_NtkConstructCare_rec( p, Aig_ObjFanin1(pObj), pMan );
+ pObj1 = Abc_NtkConstructCare_rec( pCare, Aig_ObjFanin1(pObj), pMan );
if ( pObj1 == NULL )
return pObj->pData = NULL;
pObj0 = Aig_NotCond( pObj0, Aig_ObjFaninC0(pObj) );
@@ -184,6 +184,7 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode )
pMan = Aig_ManStart( 1000 );
// construct the root node's AIG cone
pObjAig = Abc_NtkConstructAig_rec( p, pNode, pMan );
+// assert( Aig_ManConst1(pMan) == pObjAig );
Aig_ObjCreatePo( pMan, pObjAig );
if ( p->pCare )
{
@@ -191,27 +192,43 @@ Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode )
Aig_ManIncrementTravId( p->pCare );
Vec_PtrForEachEntry( p->vSupp, pFanin, i )
{
- if ( pFanin->pData == NULL )
- continue;
- pPi = Aig_ManPi( p->pCare, ((int)pFanin->pData) - 1 );
+ pPi = Aig_ManPi( p->pCare, (int)pFanin->pData );
Aig_ObjSetTravIdCurrent( p->pCare, pPi );
pPi->pData = pFanin->pCopy;
}
// construct the constraints
Aig_ManForEachPo( p->pCare, pPo, i )
{
- pObjAig = Abc_NtkConstructCare_rec( p, Aig_ObjFanin0(pPo), pMan );
+// assert( Aig_ObjFanin0(pPo) != Aig_ManConst1(p->pCare) );
+ if ( Aig_ObjFanin0(pPo) == Aig_ManConst1(p->pCare) )
+ continue;
+ pObjAig = Abc_NtkConstructCare_rec( p->pCare, Aig_ObjFanin0(pPo), pMan );
if ( pObjAig == NULL )
continue;
pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
Aig_ObjCreatePo( pMan, pObjAig );
}
}
- // construct the fanins
- Abc_ObjForEachFanin( pNode, pFanin, i )
+ if ( p->pPars->fResub )
{
- pObjAig = (Aig_Obj_t *)pFanin->pCopy;
+ // construct the node
+ pObjAig = (Aig_Obj_t *)pNode->pCopy;
Aig_ObjCreatePo( pMan, pObjAig );
+ // construct the divisors
+ Vec_PtrForEachEntry( p->vDivs, pFanin, i )
+ {
+ pObjAig = (Aig_Obj_t *)pFanin->pCopy;
+ Aig_ObjCreatePo( pMan, pObjAig );
+ }
+ }
+ else
+ {
+ // construct the fanins
+ Abc_ObjForEachFanin( pNode, pFanin, i )
+ {
+ pObjAig = (Aig_Obj_t *)pFanin->pCopy;
+ Aig_ObjCreatePo( pMan, pObjAig );
+ }
}
Aig_ManCleanup( pMan );
return pMan;
diff --git a/src/opt/mfs/mfsWin.c b/src/opt/mfs/mfsWin.c
index b812d44d..e3e5e24e 100644
--- a/src/opt/mfs/mfsWin.c
+++ b/src/opt/mfs/mfsWin.c
@@ -6,7 +6,7 @@
PackageName [The good old minimization with complete don't-cares.]
- Synopsis []
+ Synopsis [Procedures to compute windows stretching to the PIs.]
Author [Alan Mishchenko]
diff --git a/src/opt/mfs/module.make b/src/opt/mfs/module.make
index 7b9f1260..544accec 100644
--- a/src/opt/mfs/module.make
+++ b/src/opt/mfs/module.make
@@ -1,5 +1,8 @@
SRC += src/opt/mfs/mfsCore.c \
+ src/opt/mfs/mfsDiv.c \
+ src/opt/mfs/mfsInter.c \
src/opt/mfs/mfsMan.c \
+ src/opt/mfs/mfsResub.c \
src/opt/mfs/mfsSat.c \
src/opt/mfs/mfsStrash.c \
src/opt/mfs/mfsWin.c
generated by cgit v1.2.3 (git 2.25.1) at 2024-11-03 23:11:05 +0000