From 7e85276780c83538813329325ba1b28e95333be5 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 2 Apr 2013 22:22:49 -0700 Subject: New MFS package. --- Makefile | 2 +- abclib.dsp | 32 ++++++++++++++ src/opt/sfm/module.make | 5 +++ src/opt/sfm/sfm.h | 90 ++++++++++++++++++++++++++++++++++++++ src/opt/sfm/sfmCnf.c | 56 ++++++++++++++++++++++++ src/opt/sfm/sfmCore.c | 56 ++++++++++++++++++++++++ src/opt/sfm/sfmInt.h | 112 ++++++++++++++++++++++++++++++++++++++++++++++++ src/opt/sfm/sfmMan.c | 59 +++++++++++++++++++++++++ src/opt/sfm/sfmNtk.c | 75 ++++++++++++++++++++++++++++++++ src/opt/sfm/sfmSat.c | 56 ++++++++++++++++++++++++ 10 files changed, 542 insertions(+), 1 deletion(-) create mode 100644 src/opt/sfm/module.make create mode 100644 src/opt/sfm/sfm.h create mode 100644 src/opt/sfm/sfmCnf.c create mode 100644 src/opt/sfm/sfmCore.c create mode 100644 src/opt/sfm/sfmInt.h create mode 100644 src/opt/sfm/sfmMan.c create mode 100644 src/opt/sfm/sfmNtk.c create mode 100644 src/opt/sfm/sfmSat.c 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 +#include +#include +#include + +#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 + -- cgit v1.2.3