New MFS package.

Makefile

@@ -18,7 +18,7 @@ MODULES := \
 	src/misc/mem src/misc/bar src/misc/bbl \
 	src/opt/cut src/opt/fxu src/opt/rwr src/opt/mfs src/opt/sim \
 	src/opt/ret src/opt/res src/opt/lpk src/opt/nwk src/opt/rwt \
-	src/opt/cgt src/opt/csw src/opt/dar src/opt/dau \
+	src/opt/cgt src/opt/csw src/opt/dar src/opt/dau src/opt/sfm \
 	src/sat/bsat src/sat/csat src/sat/msat src/sat/psat src/sat/cnf src/sat/bmc \
 	src/bool/bdc src/bool/deco src/bool/dec src/bool/kit src/bool/lucky src/bool/rsb \
 	src/proof/pdr src/proof/int src/proof/bbr src/proof/llb src/proof/live \

abclib.dsp

@@ -2046,6 +2046,38 @@ SOURCE=.\src\opt\dau\dauMerge.c
 SOURCE=.\src\opt\dau\dauTree.c
 # End Source File
 # End Group
+# Begin Group "sfm"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\sfm\sfm.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sfm\sfmCnf.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sfm\sfmCore.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sfm\sfmInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sfm\sfmMan.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sfm\sfmNtk.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\sfm\sfmSat.c
+# End Source File
+# End Group
 # End Group
 # Begin Group "map"
 

src/opt/sfm/module.make

@@ -0,0 +1,5 @@
+SRC +=    src/opt/sfm/sfmCnf.c \
+    src/opt/sfm/sfmCore.c \
+    src/opt/sfm/sfmMan.c \
+    src/opt/sfm/sfmNtk.c \
+    src/opt/sfm/sfmSat.c

src/opt/sfm/sfm.h

@@ -0,0 +1,90 @@
+/**CFile****************************************************************
+
+  FileName    [sfm.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based optimization using internal don't-cares.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: sfm.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__opt_sfm__h
+#define ABC__opt_sfm__h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Sfm_Man_t_ Sfm_Man_t;
+typedef struct Sfm_Ntk_t_ Sfm_Ntk_t;
+typedef struct Sfm_Par_t_ Sfm_Par_t;
+struct Sfm_Par_t_
+{
+    int           nWinTfoLevs;   // the maximum fanout levels
+    int           nFanoutsMax;   // the maximum number of fanouts
+    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           nBTLimit;      // the maximum number of conflicts in one SAT run
+    int           fResub;        // performs resubstitution
+    int           fArea;         // performs optimization for area
+    int           fMoreEffort;   // performs high-affort minimization
+    int           fSwapEdge;     // performs edge swapping
+    int           fOneHotness;   // adds one-hotness conditions
+    int           fDelay;        // performs optimization for delay
+    int           fPower;        // performs power-aware optimization
+    int           fGiaSat;       // use new SAT solver
+    int           fVerbose;      // enable basic stats
+    int           fVeryVerbose;  // enable detailed stats
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== sfmCnf.c ==========================================================*/
+/*=== sfmCore.c ==========================================================*/
+extern int          Sfm_ManPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars );
+/*=== sfmMan.c ==========================================================*/
+extern Sfm_Man_t *  Sfm_ManAlloc( Sfm_Ntk_t * p );
+extern void         Sfm_ManFree( Sfm_Man_t * p );
+/*=== sfmNtk.c ==========================================================*/
+extern Sfm_Ntk_t *  Sfm_NtkAlloc( int nPis, int nPos, int nNodes, int nEdges );
+extern void         Sfm_NtkFree( Sfm_Ntk_t * p );
+/*=== sfmSat.c ==========================================================*/
+
+
+ABC_NAMESPACE_HEADER_END
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+

src/opt/sfm/sfmCnf.c

@@ -0,0 +1,56 @@
+/**CFile****************************************************************
+
+  FileName    [sfmCnf.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based optimization using internal don't-cares.]
+
+  Synopsis    [CNF computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: sfmCnf.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sfmInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Sfm_TruthToCnf( word Truth )
+{
+    return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+

src/opt/sfm/sfmCore.c

@@ -0,0 +1,56 @@
+/**CFile****************************************************************
+
+  FileName    [sfmCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based optimization using internal don't-cares.]
+
+  Synopsis    [Core procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: sfmCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sfmInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sfm_ManPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
+{
+    return 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+

src/opt/sfm/sfmInt.h

@@ -0,0 +1,112 @@
+/**CFile****************************************************************
+
+  FileName    [rsbInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based optimization using internal don't-cares.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: rsbInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__opt_sfmInt__h
+#define ABC__opt_sfmInt__h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <assert.h>
+
+#include "misc/vec/vec.h"
+#include "sfm.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+struct Sfm_Ntk_t_
+{
+    // objects
+    int *             pMem;   // memory for objects
+    Vec_Int_t         vObjs;  // ObjId -> Offset
+    Vec_Int_t         vPis;   // PiId -> ObjId
+    Vec_Int_t         vPos;   // PoId -> ObjId
+    // fanins/fanouts
+    Vec_Int_t         vMem;   // memory for overflow fanin/fanouts
+    // attributes
+    Vec_Int_t         vLevels;
+    Vec_Int_t         vTravIds;
+    Vec_Int_t         vSatVars;
+    Vec_Wrd_t         vTruths;
+};
+
+typedef struct Sfm_Obj_t_ Sfm_Obj_t;
+struct Sfm_Obj_t_
+{
+    unsigned          Type   :  2;
+    unsigned          Id     : 30;
+    unsigned          fFixed :  1;
+    unsigned          fTfo   :  1;
+    unsigned          nFanis :  4;
+    unsigned          nFanos : 26;
+    int               Fanio[0];
+};
+
+struct Sfm_Man_t_
+{
+    Sfm_Ntk_t *       pNtk;
+    // window
+    Sfm_Obj_t *       pNode;
+    Vec_Int_t *       vLeaves;      // leaves 
+    Vec_Int_t *       vRoots;       // roots
+    Vec_Int_t *       vNodes;       // internal
+    Vec_Int_t *       vTfo;         // TFO (including pNode)
+    // SAT solving
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== sfmCnf.c ==========================================================*/
+extern Vec_Int_t *  Sfm_TruthToCnf( word Truth );
+/*=== sfmCore.c ==========================================================*/
+/*=== sfmMan.c ==========================================================*/
+/*=== sfmNtk.c ==========================================================*/
+/*=== sfmSat.c ==========================================================*/
+extern int          Sfm_CreateSatWindow( Sfm_Ntk_t * p );
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+

src/opt/sfm/sfmMan.c

@@ -0,0 +1,59 @@
+/**CFile****************************************************************
+
+  FileName    [sfmMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based optimization using internal don't-cares.]
+
+  Synopsis    [Manager maintenance.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: sfmMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sfmInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Sfm_Man_t *  Sfm_ManAlloc( Sfm_Ntk_t * p )
+{
+    return NULL;
+}
+void Sfm_ManFree( Sfm_Man_t * p )
+{
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+

src/opt/sfm/sfmNtk.c

@@ -0,0 +1,75 @@
+/**CFile****************************************************************
+
+  FileName    [sfmNtk.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based optimization using internal don't-cares.]
+
+  Synopsis    [Logic network.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: sfmNtk.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sfmInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Sfm_Ntk_t * Sfm_NtkAlloc( int nPis, int nPos, int nNodes, int nEdges )
+{
+    Sfm_Ntk_t * p;
+    int AddOn = 2;
+    int nSize = (nPis + nPos + nNodes) * (sizeof(Sfm_Obj_t) / sizeof(int) + AddOn) + 2 * nEdges;
+    p = ABC_CALLOC( Sfm_Ntk_t, 1 );
+    p->pMem = ABC_CALLOC( int, nSize );
+    return p;
+}
+void Sfm_NtkFree( Sfm_Ntk_t * p )
+{
+    ABC_FREE( p->pMem );
+    ABC_FREE( p->vObjs.pArray );
+    ABC_FREE( p->vPis.pArray );
+    ABC_FREE( p->vPos.pArray );
+    ABC_FREE( p->vMem.pArray );
+    ABC_FREE( p->vLevels.pArray );
+    ABC_FREE( p->vTravIds.pArray );
+    ABC_FREE( p->vSatVars.pArray );
+    ABC_FREE( p->vTruths.pArray );
+    ABC_FREE( p );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+

src/opt/sfm/sfmSat.c

@@ -0,0 +1,56 @@
+/**CFile****************************************************************
+
+  FileName    [sfmSat.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based optimization using internal don't-cares.]
+
+  Synopsis    [SAT-based procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: sfmSat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sfmInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Sfm_CreateSatWindow( Sfm_Ntk_t * p )
+{
+    return 0;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+