summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
Diffstat
-rw-r--r--Makefile2
-rw-r--r--abclib.dsp32
-rw-r--r--src/opt/sfm/module.make5
-rw-r--r--src/opt/sfm/sfm.h90
-rw-r--r--src/opt/sfm/sfmCnf.c56
-rw-r--r--src/opt/sfm/sfmCore.c56
-rw-r--r--src/opt/sfm/sfmInt.h112
-rw-r--r--src/opt/sfm/sfmMan.c59
-rw-r--r--src/opt/sfm/sfmNtk.c75
-rw-r--r--src/opt/sfm/sfmSat.c56
10 files changed, 542 insertions, 1 deletions
diff --git a/Makefile b/Makefile
index 7ea37b2c..b025f8e9 100644
--- a/Makefile
+++ b/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 \
diff --git a/abclib.dsp b/abclib.dsp
index 6c2d3ee6..16d2d3a1 100644
--- a/abclib.dsp
+++ b/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"
diff --git a/src/opt/sfm/module.make b/src/opt/sfm/module.make
new file mode 100644
index 00000000..9d952aaf
--- /dev/null
+++ b/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
diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
new file mode 100644
index 00000000..fd25a6a1
--- /dev/null
+++ b/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 ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/sfm/sfmCnf.c b/src/opt/sfm/sfmCnf.c
new file mode 100644
index 00000000..9518c37a
--- /dev/null
+++ b/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
+
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
new file mode 100644
index 00000000..351b4ef9
--- /dev/null
+++ b/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
+
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
new file mode 100644
index 00000000..66f1c216
--- /dev/null
+++ b/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 ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/sfm/sfmMan.c b/src/opt/sfm/sfmMan.c
new file mode 100644
index 00000000..90cfe42e
--- /dev/null
+++ b/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
+
diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c
new file mode 100644
index 00000000..24ca514d
--- /dev/null
+++ b/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
+
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c
new file mode 100644
index 00000000..ed2a53c4
--- /dev/null
+++ b/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
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-05 02:02:23 +0000