Version abc80202

9 files changed, 959 insertions, 0 deletions

diff --git a/src/opt/mfs/mfs.h b/src/opt/mfs/mfs.h
new file mode 100644
index 00000000..a7ca3819
--- /dev/null
+++ b/src/opt/mfs/mfs.h
@@ -0,0 +1,73 @@
+/**CFile****************************************************************
+
+  FileName    [mfs.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfs.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __MFS_H__
+#define __MFS_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Mfs_Par_t_ Mfs_Par_t;
+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           fArea;         // performs optimization for area
+    int           fDelay;        // performs optimization for delay
+    int           fVerbose;      // enable basic stats
+    int           fVeryVerbose;  // enable detailed stats
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== mfsCore.c ==========================================================*/
+extern int         Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars );
+ 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/mfs/mfsCore.c b/src/opt/mfs/mfsCore.c
new file mode 100644
index 00000000..fe0d84c3
--- /dev/null
+++ b/src/opt/mfs/mfsCore.c
@@ -0,0 +1,143 @@
+/**CFile****************************************************************
+
+  FileName    [mfsCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfsCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfsInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMfsNode( Mfs_Man_t * p, Abc_Obj_t * pNode )
+{
+    int clk;
+    // 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;
+    // 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, Abc_ObjFaninNum(pNode) );
+p->timeCnf += clock() - clk;
+    // create the SAT problem
+clk = clock();
+    p->pSat = Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
+    // solve the SAT problem
+    Abc_NtkMfsSolveSat( p, pNode );
+p->timeSat += clock() - clk;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkMfs( Abc_Ntk_t * pNtk, Mfs_Par_t * pPars )
+{
+    Mfs_Man_t * p;
+    Abc_Obj_t * pObj;
+    int i, Counter;
+
+    assert( Abc_NtkIsLogic(pNtk) );
+    if ( Abc_NtkGetFaninMax(pNtk) > MFS_FANIN_MAX )
+    {
+        printf( "Some nodes have more than %d fanins. Quitting.\n", MFS_FANIN_MAX );
+        return 1;
+    }
+    // perform the network sweep
+    Abc_NtkSweep( pNtk, 0 );
+    // convert into the AIG
+    if ( !Abc_NtkToAig(pNtk) )
+    {
+        fprintf( stdout, "Converting to BDD has failed.\n" );
+        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->pNtk  = pNtk;
+    p->pCare = pNtk->pManExdc;
+
+    // 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 );
+    }
+
+    // compute don't-cares for each node
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        Abc_NtkMfsNode( p, pObj );
+
+    // undo labesl
+    if ( p->pCare )
+    {
+        Abc_NtkForEachCi( pNtk, pObj, i )
+            pObj->pData = NULL;
+    }
+
+    // free the manager
+    Mfs_ManStop( p );
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/mfs/mfsInt.h b/src/opt/mfs/mfsInt.h
new file mode 100644
index 00000000..6ba5903e
--- /dev/null
+++ b/src/opt/mfs/mfsInt.h
@@ -0,0 +1,110 @@
+/**CFile****************************************************************
+
+  FileName    [mfsInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfsInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __MFS_INT_H__
+#define __MFS_INT_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "abc.h"
+#include "mfs.h"
+#include "aig.h"
+#include "cnf.h"
+#include "satSolver.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+#define MFS_FANIN_MAX   10
+
+typedef struct Mfs_Man_t_ Mfs_Man_t;
+struct Mfs_Man_t_
+{
+    // input data
+    Mfs_Par_t *         pPars;
+    Abc_Ntk_t *         pNtk;
+    Aig_Man_t *         pCare;
+    // intermeditate data for the node
+    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_Int_t *         vProjVars; // the projection variables
+    // 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 
+    // the result of solving
+    int                 nFanins;   // the number of fanins
+    int                 nWords;    // the number of words
+    int                 nCares;    // the number of care minterms
+    unsigned            uCare[(MFS_FANIN_MAX<=5)?1:1<<(MFS_FANIN_MAX-5)];  // the computed care-set
+    // performance statistics
+    int                 nNodesTried;
+    int                 nNodesBad;
+    int                 nMintsCare;
+    int                 nMintsTotal;
+    // statistics
+    int                 timeWin;
+    int                 timeAig;
+    int                 timeCnf;
+    int                 timeSat;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== mfsMan.c ==========================================================*/
+extern Mfs_Man_t *      Mfs_ManAlloc();
+extern void             Mfs_ManStop( Mfs_Man_t * p );
+extern void             Mfs_ManClean( Mfs_Man_t * p );
+/*=== mfsSat.c ==========================================================*/
+extern void             Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode );
+/*=== mfsStrash.c ==========================================================*/
+extern Aig_Man_t *      Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode );
+/*=== mfsWin.c ==========================================================*/
+extern Vec_Ptr_t *      Abc_MfsComputeRoots( Abc_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit );
+
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/mfs/mfsMan.c b/src/opt/mfs/mfsMan.c
new file mode 100644
index 00000000..1341e373
--- /dev/null
+++ b/src/opt/mfs/mfsMan.c
@@ -0,0 +1,132 @@
+/**CFile****************************************************************
+
+  FileName    [mfsMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    [Procedure to manipulation the manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfsMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfsInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Mfs_Man_t * Mfs_ManAlloc()
+{
+    Mfs_Man_t * p;
+    // start the manager
+    p = ALLOC( Mfs_Man_t, 1 );
+    memset( p, 0, sizeof(Mfs_Man_t) );
+    p->vProjVars = Vec_IntAlloc( 100 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mfs_ManClean( Mfs_Man_t * p )
+{
+    if ( p->pAigWin )
+        Aig_ManStop( p->pAigWin );
+    if ( p->pCnf )
+        Cnf_DataFree( p->pCnf );
+    if ( p->pSat )
+        sat_solver_delete( p->pSat );
+    if ( p->vRoots )
+        Vec_PtrFree( p->vRoots );
+    if ( p->vSupp )
+        Vec_PtrFree( p->vSupp );
+    if ( p->vNodes )
+        Vec_PtrFree( p->vNodes );
+    p->pAigWin = NULL;
+    p->pCnf = NULL;
+    p->pSat = NULL;
+    p->vRoots = NULL;
+    p->vSupp = NULL;
+    p->vNodes = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Mfs_ManStop( Mfs_Man_t * p )
+{
+    Mfs_ManPrint( p );
+    Mfs_ManClean( p );
+    Vec_IntFree( p->vProjVars );
+    free( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/mfs/mfsSat.c b/src/opt/mfs/mfsSat.c
new file mode 100644
index 00000000..d995000f
--- /dev/null
+++ b/src/opt/mfs/mfsSat.c
@@ -0,0 +1,113 @@
+/**CFile****************************************************************
+
+  FileName    [mfsSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfsSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfsInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Enumerates through the SAT assignments.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+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 )
+        return 0;
+    // add SAT assignment to the solver
+    Mint = 0;
+    Vec_IntForEachEntry( p->vProjVars, iVar, b )
+    {
+        Lits[b] = toLit( iVar );
+        if ( sat_solver_var_value( p->pSat, iVar ) )
+        {
+            Mint |= (1 << b);
+            Lits[b] = lit_neg( Lits[b] );
+        }
+    }
+    assert( !Aig_InfoHasBit(p->uCare, Mint) );
+    Aig_InfoSetBit( p->uCare, Mint );
+    // add the blocking clause
+    RetValue = sat_solver_addclause( p->pSat, Lits, Lits + Vec_IntSize(p->vProjVars) );
+    if ( RetValue == 0 )
+        return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Enumerates through the SAT assignments.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkMfsSolveSat( Mfs_Man_t * p, Abc_Obj_t * pNode )
+{
+    Aig_Obj_t * pObjPo;
+    int i;
+    // collect projection variables
+    Vec_IntClear( p->vProjVars );
+    Vec_PtrForEachEntryStart( p->pAigWin->vPos, pObjPo, i, Aig_ManPoNum(p->pAigWin) - Abc_ObjFaninNum(pNode) )
+    {
+        assert( p->pCnf->pVarNums[pObjPo->Id] >= 0 );
+        Vec_IntPush( p->vProjVars, p->pCnf->pVarNums[pObjPo->Id] );
+    }
+
+    // prepare the truth table of care set
+    p->nFanins = Vec_IntSize( p->vProjVars );
+    p->nWords = Aig_TruthWordNum( p->nFanins );
+    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] );
+
+    p->nMintsCare  += p->nCares;
+    p->nMintsTotal += 32 * p->nWords;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/mfs/mfsStrash.c b/src/opt/mfs/mfsStrash.c
new file mode 100644
index 00000000..7b467936
--- /dev/null
+++ b/src/opt/mfs/mfsStrash.c
@@ -0,0 +1,224 @@
+/**CFile****************************************************************
+
+  FileName    [mfsStrash.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    [Structural hashing of the window with ODCs.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfsStrash.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfsInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Construct BDDs and mark AIG nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_MfsConvertHopToAig_rec( Hop_Obj_t * pObj, Aig_Man_t * pMan )
+{
+    assert( !Hop_IsComplement(pObj) );
+    if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
+        return;
+    Abc_MfsConvertHopToAig_rec( Hop_ObjFanin0(pObj), pMan ); 
+    Abc_MfsConvertHopToAig_rec( Hop_ObjFanin1(pObj), pMan );
+    pObj->pData = Aig_And( pMan, (Aig_Obj_t *)Hop_ObjChild0Copy(pObj), (Aig_Obj_t *)Hop_ObjChild1Copy(pObj) ); 
+    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
+    Hop_ObjSetMarkA( pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Converts the network from AIG to BDD representation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_MfsConvertHopToAig( Abc_Obj_t * pObjOld, Aig_Man_t * pMan )
+{
+    Hop_Man_t * pHopMan;
+    Hop_Obj_t * pRoot;
+    Abc_Obj_t * pFanin;
+    int i;
+    // get the local AIG
+    pHopMan = pObjOld->pNtk->pManFunc;
+    pRoot = pObjOld->pData;
+    // check the case of a constant
+    if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
+    {
+        pObjOld->pCopy = (Abc_Obj_t *)Aig_NotCond( Aig_ManConst1(pMan), Hop_IsComplement(pRoot) );
+        pObjOld->pNext = pObjOld->pCopy;
+        return;
+    }
+
+    // assign the fanin nodes
+    Abc_ObjForEachFanin( pObjOld, pFanin, i )
+        Hop_ManPi(pHopMan, i)->pData = pFanin->pCopy;
+    // construct the AIG
+    Abc_MfsConvertHopToAig_rec( Hop_Regular(pRoot), pMan );
+    pObjOld->pCopy = (Abc_Obj_t *)Aig_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );  
+    Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
+
+    // assign the fanin nodes
+    Abc_ObjForEachFanin( pObjOld, pFanin, i )
+        Hop_ManPi(pHopMan, i)->pData = pFanin->pNext;
+    // construct the AIG
+    Abc_MfsConvertHopToAig_rec( Hop_Regular(pRoot), pMan );
+    pObjOld->pNext = (Abc_Obj_t *)Aig_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );  
+    Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the care set of the node under ODCs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Abc_NtkConstructAig_rec( Mfs_Man_t * p, Abc_Obj_t * pNode, Aig_Man_t * pMan )
+{
+    Aig_Obj_t * pRoot, * pExor;
+    Abc_Obj_t * pObj;
+    int i;
+    // assign AIG nodes to the leaves
+    Vec_PtrForEachEntry( p->vSupp, pObj, i )
+        pObj->pCopy = pObj->pNext = (Abc_Obj_t *)Aig_ObjCreatePi( pMan );
+    // strash intermediate nodes
+    Abc_NtkIncrementTravId( pNode->pNtk );
+    Vec_PtrForEachEntry( p->vNodes, pObj, i )
+    {
+        Abc_MfsConvertHopToAig( pObj, pMan );
+        if ( pObj == pNode )
+            pObj->pNext = Abc_ObjNot(pObj->pNext);
+    }
+    // create the observability condition
+    pRoot = Aig_ManConst0(pMan);
+    Vec_PtrForEachEntry( p->vRoots, pObj, i )
+    {
+        pExor = Aig_Exor( pMan, (Aig_Obj_t *)pObj->pCopy, (Aig_Obj_t *)pObj->pNext );
+        pRoot = Aig_Or( pMan, pRoot, pExor );
+    }
+    return pRoot;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Adds relevant constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Abc_NtkConstructCare_rec( Mfs_Man_t * p, Aig_Obj_t * pObj, Aig_Man_t * pMan )
+{
+    Aig_Obj_t * pObj0, * pObj1;
+    if ( Aig_ObjIsTravIdCurrent( pMan, pObj ) )
+        return pObj->pData;
+    Aig_ObjSetTravIdCurrent( pMan, pObj );
+    if ( Aig_ObjIsPi(pObj) )
+        return pObj->pData = NULL;
+    pObj0 = Abc_NtkConstructCare_rec( p, Aig_ObjFanin0(pObj), pMan );
+    if ( pObj0 == NULL )
+        return pObj->pData = NULL;
+    pObj1 = Abc_NtkConstructCare_rec( p, Aig_ObjFanin1(pObj), pMan );
+    if ( pObj1 == NULL )
+        return pObj->pData = NULL;
+    pObj0 = Aig_NotCond( pObj0, Aig_ObjFaninC0(pObj) );
+    pObj1 = Aig_NotCond( pObj1, Aig_ObjFaninC1(pObj) );
+    return pObj->pData = Aig_And( pMan, pObj0, pObj1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates AIG for the window with constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Abc_NtkConstructAig( Mfs_Man_t * p, Abc_Obj_t * pNode )
+{
+    Aig_Man_t * pMan;
+    Abc_Obj_t * pFanin;
+    Aig_Obj_t * pObjAig, * pPi, * pPo;
+    int i;
+    // start the new manager
+    pMan = Aig_ManStart( 1000 );
+    // construct the root node's AIG cone
+    pObjAig = Abc_NtkConstructAig_rec( p, pNode, pMan );
+    Aig_ObjCreatePo( pMan, pObjAig );
+    if ( p->pCare )
+    {
+        // mark the care set
+        Aig_ManIncrementTravId( p->pCare );
+        Vec_PtrForEachEntry( p->vSupp, pFanin, i )
+        {
+            if ( pFanin->pData == NULL )
+                continue;
+            pPi = Aig_ManPi( p->pCare, ((int)pFanin->pData) - 1 );
+            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 );
+            if ( pObjAig == NULL )
+                continue;
+            pObjAig = Aig_NotCond( pObjAig, Aig_ObjFaninC0(pPo) );
+            Aig_ObjCreatePo( pMan, pObjAig );
+        }
+    }
+    // construct the fanins
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+    {
+        pObjAig = (Aig_Obj_t *)pFanin->pCopy;
+        Aig_ObjCreatePo( pMan, pObjAig );
+    }
+    Aig_ManCleanup( pMan );
+    return pMan;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/mfs/mfsWin.c b/src/opt/mfs/mfsWin.c
new file mode 100644
index 00000000..b812d44d
--- /dev/null
+++ b/src/opt/mfs/mfsWin.c
@@ -0,0 +1,112 @@
+/**CFile****************************************************************
+
+  FileName    [mfsWin.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfsWin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfsInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the node should be a root.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_MfsComputeRootsCheck( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    // the node is the root if one of the following is true:
+    // (1) the node has more than fanouts than the limit
+    if ( Abc_ObjFanoutNum(pNode) > nFanoutLimit )
+        return 1;
+    // (2) the node has CO fanouts
+    // (3) the node has fanouts above the cutoff level
+    Abc_ObjForEachFanout( pNode, pFanout, i )
+        if ( Abc_ObjIsCo(pFanout) || (int)pFanout->Level > nLevelMax )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively collects the root candidates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_MfsComputeRoots_rec( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit, Vec_Ptr_t * vRoots )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    assert( Abc_ObjIsNode(pNode) );
+    if ( Abc_NodeIsTravIdCurrent(pNode) )
+        return;
+    Abc_NodeSetTravIdCurrent( pNode );
+    // check if the node should be the root
+    if ( Abc_MfsComputeRootsCheck( pNode, nLevelMax, nFanoutLimit ) )
+        Vec_PtrPush( vRoots, pNode );
+    else // if not, explore its fanouts
+        Abc_ObjForEachFanout( pNode, pFanout, i )
+            Abc_MfsComputeRoots_rec( pFanout, nLevelMax, nFanoutLimit, vRoots );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively collects the root candidates.]
+
+  Description [Returns 1 if the only root is this node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_MfsComputeRoots( Abc_Obj_t * pNode, int nWinTfoMax, int nFanoutLimit )
+{
+    Vec_Ptr_t * vRoots;
+    vRoots = Vec_PtrAlloc( 10 );
+    Abc_NtkIncrementTravId( pNode->pNtk );
+    Abc_MfsComputeRoots_rec( pNode, pNode->Level + nWinTfoMax, nFanoutLimit, vRoots );
+    assert( Vec_PtrSize(vRoots) > 0 );
+//    if ( Vec_PtrSize(vRoots) == 1 && Vec_PtrEntry(vRoots, 0) == pNode )
+//        return 0;
+    return vRoots;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/mfs/mfs_.c b/src/opt/mfs/mfs_.c
new file mode 100644
index 00000000..32caf7ff
--- /dev/null
+++ b/src/opt/mfs/mfs_.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+  FileName    [mfs_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [The good old minimization with complete don't-cares.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: mfs_.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "mfsInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/mfs/module.make b/src/opt/mfs/module.make
new file mode 100644
index 00000000..7b9f1260
--- /dev/null
+++ b/src/opt/mfs/module.make
@@ -0,0 +1,5 @@
+SRC +=  src/opt/mfs/mfsCore.c \
+    src/opt/mfs/mfsMan.c \
+    src/opt/mfs/mfsSat.c \
+    src/opt/mfs/mfsStrash.c \
+    src/opt/mfs/mfsWin.c