diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-02 22:22:49 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2013-04-02 22:22:49 -0700 |
commit | 7e85276780c83538813329325ba1b28e95333be5 (patch) | |
tree | 5e7e21a0a46230c4c9d3cc99abb19990bafb8d73 /src/opt | |
parent | f1c9f1829a1960865bd7b964169f714abc3db597 (diff) | |
download | abc-7e85276780c83538813329325ba1b28e95333be5.tar.gz abc-7e85276780c83538813329325ba1b28e95333be5.tar.bz2 abc-7e85276780c83538813329325ba1b28e95333be5.zip |
New MFS package.
Diffstat (limited to 'src/opt')
-rw-r--r-- | src/opt/sfm/module.make | 5 | ||||
-rw-r--r-- | src/opt/sfm/sfm.h | 90 | ||||
-rw-r--r-- | src/opt/sfm/sfmCnf.c | 56 | ||||
-rw-r--r-- | src/opt/sfm/sfmCore.c | 56 | ||||
-rw-r--r-- | src/opt/sfm/sfmInt.h | 112 | ||||
-rw-r--r-- | src/opt/sfm/sfmMan.c | 59 | ||||
-rw-r--r-- | src/opt/sfm/sfmNtk.c | 75 | ||||
-rw-r--r-- | src/opt/sfm/sfmSat.c | 56 |
8 files changed, 509 insertions, 0 deletions
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 + |