summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/base/abci/abc.c143
-rw-r--r--src/base/abci/abcMfs.c189
-rw-r--r--src/base/abci/module.make1
-rw-r--r--src/misc/vec/vecInt.h6
-rw-r--r--src/misc/vec/vecWec.h8
-rw-r--r--src/opt/sfm/module.make4
-rw-r--r--src/opt/sfm/sfm.h31
-rw-r--r--src/opt/sfm/sfmCnf.c62
-rw-r--r--src/opt/sfm/sfmCore.c61
-rw-r--r--src/opt/sfm/sfmInt.h105
-rw-r--r--src/opt/sfm/sfmMan.c59
-rw-r--r--src/opt/sfm/sfmNtk.c249
-rw-r--r--src/opt/sfm/sfmSat.c59
-rw-r--r--src/opt/sfm/sfmWin.c171
14 files changed, 930 insertions, 218 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index bd18200c..70646874 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -52,6 +52,7 @@
#include "proof/abs/abs.h"
#include "sat/bmc/bmc.h"
#include "proof/ssc/ssc.h"
+#include "opt/sfm/sfm.h"
#ifndef _WIN32
#include <unistd.h>
@@ -104,6 +105,7 @@ static int Abc_CommandLutpack ( Abc_Frame_t * pAbc, int argc, cha
static int Abc_CommandLutmin ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandImfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandMfs ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandMfs2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandTrace ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSpeedup ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandPowerdown ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -607,6 +609,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "lutmin", Abc_CommandLutmin, 1 );
// Cmd_CommandAdd( pAbc, "Synthesis", "imfs", Abc_CommandImfs, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "mfs", Abc_CommandMfs, 1 );
+ Cmd_CommandAdd( pAbc, "Synthesis", "mfs2", Abc_CommandMfs2, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "trace", Abc_CommandTrace, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "speedup", Abc_CommandSpeedup, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "powerdown", Abc_CommandPowerdown, 1 );
@@ -4400,6 +4403,146 @@ usage:
return 1;
}
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_CommandMfs2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+ extern int Abc_NtkPerformMfs( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars );
+ Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+ Sfm_Par_t Pars, * pPars = &Pars;
+ int c;
+ // set defaults
+ Sfm_ParSetDefault( pPars );
+ Extra_UtilGetoptReset();
+ while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMClaevwh" ) ) != EOF )
+ {
+ switch ( c )
+ {
+ case 'W':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nTfoLevMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nTfoLevMax < 0 )
+ goto usage;
+ break;
+ case 'F':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nFanoutMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nFanoutMax < 1 )
+ goto usage;
+ break;
+ case 'D':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-D\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nDepthMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nDepthMax < 0 )
+ goto usage;
+ break;
+ case 'M':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nWinSizeMax = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nWinSizeMax < 0 )
+ goto usage;
+ break;
+ case 'C':
+ if ( globalUtilOptind >= argc )
+ {
+ Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+ goto usage;
+ }
+ pPars->nBTLimit = atoi(argv[globalUtilOptind]);
+ globalUtilOptind++;
+ if ( pPars->nBTLimit < 0 )
+ goto usage;
+ break;
+ case 'l':
+ pPars->fFixLevel ^= 1;
+ break;
+ case 'a':
+ pPars->fArea ^= 1;
+ break;
+ case 'e':
+ pPars->fMoreEffort ^= 1;
+ break;
+ case 'v':
+ pPars->fVerbose ^= 1;
+ break;
+ case 'w':
+ pPars->fVeryVerbose ^= 1;
+ break;
+ case 'h':
+ goto usage;
+ default:
+ goto usage;
+ }
+ }
+ if ( pNtk == NULL )
+ {
+ Abc_Print( -1, "Empty network.\n" );
+ return 1;
+ }
+ if ( !Abc_NtkIsLogic(pNtk) )
+ {
+ Abc_Print( -1, "This command can only be applied to a logic network.\n" );
+ return 1;
+ }
+ if ( !Abc_NtkIsSopLogic(pNtk) )
+ {
+ Abc_Print( -1, "Currently this command works only for SOP logic networks (run \"sop\").\n" );
+ return 1;
+ }
+ // modify the current network
+ if ( !Abc_NtkPerformMfs( pNtk, pPars ) )
+ {
+ Abc_Print( -1, "Resynthesis has failed.\n" );
+ return 1;
+ }
+ return 0;
+
+usage:
+ Abc_Print( -2, "usage: mfs2 [-WFDMC <num>] [-laevwh]\n" );
+ Abc_Print( -2, "\t performs don't-care-based optimization of logic networks\n" );
+ Abc_Print( -2, "\t-W <num> : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nTfoLevMax );
+ Abc_Print( -2, "\t-F <num> : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutMax );
+ Abc_Print( -2, "\t-D <num> : the max depth nodes to try (0 = no limit) [default = %d]\n", pPars->nDepthMax );
+ Abc_Print( -2, "\t-M <num> : the max node count of windows to consider (0 = no limit) [default = %d]\n", pPars->nWinSizeMax );
+ Abc_Print( -2, "\t-C <num> : the max number of conflicts in one SAT run (0 = no limit) [default = %d]\n", pPars->nBTLimit );
+ Abc_Print( -2, "\t-l : allow logic level to increase [default = %s]\n", !pPars->fFixLevel? "yes": "no" );
+ Abc_Print( -2, "\t-a : toggle minimizing area or area+edges [default = %s]\n", pPars->fArea? "area": "area+edges" );
+ Abc_Print( -2, "\t-e : toggle high-effort resubstitution [default = %s]\n", pPars->fMoreEffort? "yes": "no" );
+ Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
+ Abc_Print( -2, "\t-h : print the command usage\n");
+ return 1;
+}
+
/**Function*************************************************************
diff --git a/src/base/abci/abcMfs.c b/src/base/abci/abcMfs.c
new file mode 100644
index 00000000..ddc91467
--- /dev/null
+++ b/src/base/abci/abcMfs.c
@@ -0,0 +1,189 @@
+/**CFile****************************************************************
+
+ FileName [abcMfs.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [Network and node package.]
+
+ Synopsis [Optimization with don't-cares.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: abcMfs.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "base/abc/abc.h"
+#include "opt/sfm/sfm.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Ptr_t * Abc_NtkAssignIDs( Abc_Ntk_t * pNtk )
+{
+ Vec_Ptr_t * vNodes;
+ Abc_Obj_t * pObj;
+ int i;
+ vNodes = Abc_NtkDfs( pNtk, 0 );
+ Abc_NtkCleanCopy( pNtk );
+ Abc_NtkForEachPi( pNtk, pObj, i )
+ pObj->iTemp = i;
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+ pObj->iTemp = Abc_NtkPiNum(pNtk) + i;
+ Abc_NtkForEachPo( pNtk, pObj, i )
+ pObj->iTemp = Abc_NtkPiNum(pNtk) + Vec_PtrSize(vNodes) + i;
+ return vNodes;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Extracts information about the network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk )
+{
+ Vec_Ptr_t * vNodes;
+ Vec_Wec_t * vFanins;
+ Vec_Str_t * vFixed;
+ Vec_Wrd_t * vTruths;
+ Vec_Int_t * vArray;
+ Abc_Obj_t * pObj, * pFanin;
+ int i, k, nObjs;
+ vNodes = Abc_NtkAssignIDs( pNtk );
+ nObjs = Abc_NtkPiNum(pNtk) + Vec_PtrSize(vNodes) + Abc_NtkPoNum(pNtk);
+ vFanins = Vec_WecStart( nObjs );
+ vFixed = Vec_StrStart( nObjs );
+ vTruths = Vec_WrdStart( nObjs );
+ Vec_PtrForEachEntry( Abc_Obj_t *, vNodes, pObj, i )
+ {
+ vArray = Vec_WecEntry( vFanins, pObj->iTemp );
+ Vec_IntGrow( vArray, Abc_ObjFaninNum(pObj) );
+ Abc_ObjForEachFanin( pObj, pFanin, k )
+ Vec_IntPush( vArray, pFanin->iTemp );
+ Vec_WrdWriteEntry( vTruths, pObj->iTemp, Abc_SopToTruth((char *)pObj->pData, Abc_ObjFaninNum(pObj)) );
+ }
+ Abc_NtkForEachPo( pNtk, pObj, i )
+ {
+ vArray = Vec_WecEntry( vFanins, pObj->iTemp );
+ Vec_IntGrow( vArray, Abc_ObjFaninNum(pObj) );
+ Abc_ObjForEachFanin( pObj, pFanin, k )
+ Vec_IntPush( vArray, pFanin->iTemp );
+ }
+ Vec_PtrFree( vNodes );
+ return Sfm_NtkConstruct( vFanins, Abc_NtkPiNum(pNtk), Abc_NtkPoNum(pNtk), vFixed, vTruths );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p )
+{
+ Vec_Int_t * vMap, * vArray;
+ Abc_Obj_t * pNode;
+ int i, k, Fanin;
+ // map new IDs into old nodes
+ vMap = Vec_IntStart( Abc_NtkObjNumMax(pNtk) );
+ Abc_NtkForEachPi( pNtk, pNode, i )
+ Vec_IntWriteEntry( vMap, pNode->iTemp, Abc_ObjId(pNode) );
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ if ( pNode->iTemp > 0 )
+ Vec_IntWriteEntry( vMap, pNode->iTemp, Abc_ObjId(pNode) );
+ // remove old fanins
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ Abc_ObjRemoveFanins( pNode );
+ // create new fanins
+ Abc_NtkForEachNode( pNtk, pNode, i )
+ if ( pNode->iTemp > 0 && !Sfm_NodeReadFixed(p, pNode->iTemp) )
+ {
+ vArray = Sfm_NodeReadFanins( p, pNode->iTemp );
+ Vec_IntForEachEntry( vArray, Fanin, k )
+ Abc_ObjAddFanin( pNode, Abc_NtkObj(pNtk, Vec_IntEntry(vMap, Fanin)) );
+ pNode->pData = Abc_SopCreateFromTruth( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), (unsigned *)Sfm_NodeReadTruth(p, pNode->iTemp) );
+ }
+ Vec_IntFree( vMap );
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+int Abc_NtkPerformMfs( Abc_Ntk_t * pNtk, Sfm_Par_t * pPars )
+{
+ Sfm_Ntk_t * p;
+ int nFaninMax, nNodes;
+ assert( Abc_NtkIsSopLogic(pNtk) );
+ // count fanouts
+ nFaninMax = Abc_NtkGetFaninMax( pNtk );
+ if ( nFaninMax > 6 )
+ {
+ Abc_Print( 1, "Currently \"mfs\" cannot process the network containing nodes with more than 6 fanins.\n" );
+ return 0;
+ }
+ // collect information
+ p = Abc_NtkExtractMfs( pNtk );
+ // perform optimization
+ nNodes = Sfm_NtkPerform( p, pPars );
+ // call the fast extract procedure
+ if ( nNodes == 0 )
+ Abc_Print( 1, "The networks is not changed by \"mfs\".\n" );
+ else
+ {
+ Abc_NtkInsertMfs( pNtk, p );
+ Abc_Print( 1, "The networks has %d nodes changed by \"mfs\".\n", nNodes );
+ }
+ Sfm_NtkFree( p );
+ return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 89e1849b..c7645775 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -30,6 +30,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcLutmin.c \
src/base/abci/abcMap.c \
src/base/abci/abcMerge.c \
+ src/base/abci/abcMfs.c \
src/base/abci/abcMini.c \
src/base/abci/abcMiter.c \
src/base/abci/abcMulti.c \
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index a99e6f29..c821d121 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -255,6 +255,12 @@ static inline Vec_Int_t * Vec_IntDupArray( Vec_Int_t * pVec )
SeeAlso []
***********************************************************************/
+static inline void Vec_IntZero( Vec_Int_t * p )
+{
+ p->pArray = NULL;
+ p->nSize = 0;
+ p->nCap = 0;
+}
static inline void Vec_IntErase( Vec_Int_t * p )
{
ABC_FREE( p->pArray );
diff --git a/src/misc/vec/vecWec.h b/src/misc/vec/vecWec.h
index 8a924f90..ece7b0a1 100644
--- a/src/misc/vec/vecWec.h
+++ b/src/misc/vec/vecWec.h
@@ -245,6 +245,7 @@ static inline void Vec_WecClear( Vec_Wec_t * p )
int i;
Vec_WecForEachLevel( p, vVec, i )
Vec_IntClear( vVec );
+ p->nSize = 0;
}
/**Function*************************************************************
@@ -315,10 +316,9 @@ static inline double Vec_WecMemory( Vec_Wec_t * p )
***********************************************************************/
static inline void Vec_WecFree( Vec_Wec_t * p )
{
- Vec_Int_t * vVec;
int i;
- Vec_WecForEachLevel( p, vVec, i )
- ABC_FREE( vVec->pArray );
+ for ( i = 0; i < p->nCap; i++ )
+ ABC_FREE( p->pArray[i].pArray );
ABC_FREE( p->pArray );
ABC_FREE( p );
}
@@ -643,6 +643,8 @@ static inline void Vec_WecRemoveEmpty( Vec_Wec_t * vCubes )
vCubes->pArray[k++] = *vCube;
else
ABC_FREE( vCube->pArray );
+ for ( i = k; i < Vec_WecSize(vCubes); i++ )
+ Vec_IntZero( Vec_WecEntry(vCubes, i) );
Vec_WecShrink( vCubes, k );
// Vec_WecSortByFirstInt( vCubes, 0 );
}
diff --git a/src/opt/sfm/module.make b/src/opt/sfm/module.make
index 9d952aaf..b78355e1 100644
--- a/src/opt/sfm/module.make
+++ b/src/opt/sfm/module.make
@@ -1,5 +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/sfmSat.c \
+ src/opt/sfm/sfmWin.c
diff --git a/src/opt/sfm/sfm.h b/src/opt/sfm/sfm.h
index 42f8156a..deb055c5 100644
--- a/src/opt/sfm/sfm.h
+++ b/src/opt/sfm/sfm.h
@@ -26,6 +26,8 @@
/// INCLUDES ///
////////////////////////////////////////////////////////////////////////
+#include "misc/vec/vecWec.h"
+
////////////////////////////////////////////////////////////////////////
/// PARAMETERS ///
////////////////////////////////////////////////////////////////////////
@@ -36,26 +38,18 @@ 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 nTfoLevMax; // the maximum fanout levels
+ int nFanoutMax; // the maximum number of fanouts
+ int nDepthMax; // the maximum depth to try
+ int nWinSizeMax; // the maximum number of divisors
int nBTLimit; // the maximum number of conflicts in one SAT run
- int fResub; // performs resubstitution
+ int fFixLevel; // does not allow level to increase
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
};
@@ -70,13 +64,14 @@ struct Sfm_Par_t_
/*=== 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 );
+extern void Sfm_ParSetDefault( Sfm_Par_t * pPars );
+extern int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars );
/*=== sfmNtk.c ==========================================================*/
-extern Sfm_Ntk_t * Sfm_NtkAlloc( int nPis, int nPos, int nNodes, Vec_Int_t * vFanins, Vec_Int_t * vFanouts, Vec_Int_t * vEdges, Vec_Int_t * vOpts );
+extern Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Wrd_t * vTruths );
extern void Sfm_NtkFree( Sfm_Ntk_t * p );
+extern Vec_Int_t * Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i );
+extern word Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i );
+extern int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i );
/*=== sfmSat.c ==========================================================*/
diff --git a/src/opt/sfm/sfmCnf.c b/src/opt/sfm/sfmCnf.c
index 6b152524..825c336b 100644
--- a/src/opt/sfm/sfmCnf.c
+++ b/src/opt/sfm/sfmCnf.c
@@ -43,13 +43,38 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
+void Sfm_PrintCnf( Vec_Str_t * vCnf )
+{
+ char Entry;
+ int i, Lit;
+ Vec_StrForEachEntry( vCnf, Entry, i )
+ {
+ Lit = (int)Entry;
+ if ( Lit == -1 )
+ printf( "\n" );
+ else
+ printf( "%s%d ", Abc_LitIsCompl(Lit) ? "-":"", Abc_Lit2Var(Lit) );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
{
Vec_StrClear( vCnf );
if ( Truth == 0 || ~Truth == 0 )
{
Vec_StrPush( vCnf, (char)(Truth == 0) );
- Vec_StrPush( vCnf, -1 );
+ Vec_StrPush( vCnf, (char)-1 );
return 1;
}
else
@@ -74,7 +99,7 @@ int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf
assert( 0 );
}
Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) );
- Vec_StrPush( vCnf, -1 );
+ Vec_StrPush( vCnf, (char)-1 );
}
}
return nCubes;
@@ -92,30 +117,25 @@ int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf
SeeAlso []
***********************************************************************/
-int Sfm_DeriveCnfs( Vec_Wrd_t * vTruths, Vec_Int_t * vFanins, Vec_Str_t ** pvCnfs, Vec_Int_t ** pvOffsets )
+void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap )
{
- Vec_Str_t * vCnfs, * vCnf;
- Vec_Int_t * vOffsets, * vCover;
- int i, k, nFanins, nClauses = 0;
- vCnf = Vec_StrAlloc( 1000 );
- vCnfs = Vec_StrAlloc( 1000 );
- vOffsets = Vec_IntAlloc( Vec_IntSize(vFanins) );
- vCover = Vec_IntAlloc( 1 << 16 );
- assert( Vec_WrdSize(vTruths) == Vec_IntSize(vFanins) );
- Vec_IntForEachEntry( vFanins, nFanins, i )
+ Vec_Int_t * vClause;
+ int i, Lit;
+ char Entry;
+ Vec_WecClear( vRes );
+ vClause = Vec_WecPushLevel( vRes );
+ Vec_StrForEachEntry( vCnf, Entry, i )
{
- nClauses += Sfm_TruthToCnf( Vec_WrdEntry(vTruths, i), nFanins, vCover, vCnf );
- Vec_IntPush( vOffsets, Vec_StrSize(vCnfs) );
- for ( k = 0; k < Vec_StrSize(vCnf); k++ )
- Vec_StrPush( vCnfs, Vec_StrEntry(vCnf, k) );
+ Lit = (int)Entry;
+ if ( Lit == -1 )
+ {
+ vClause = Vec_WecPushLevel( vRes );
+ continue;
+ }
+ Vec_IntPush( vClause, Abc_Lit2LitV( Vec_IntArray(vFaninMap), Lit ) );
}
- Vec_IntPush( vOffsets, Vec_StrSize(vCnfs) );
- Vec_StrFree( vCnf );
- Vec_IntFree( vCover );
- return nClauses;
}
-
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
index 351b4ef9..a8ff1e21 100644
--- a/src/opt/sfm/sfmCore.c
+++ b/src/opt/sfm/sfmCore.c
@@ -36,14 +36,73 @@ ABC_NAMESPACE_IMPL_START
Synopsis []
Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sfm_ParSetDefault( Sfm_Par_t * pPars )
+{
+ memset( pPars, 0, sizeof(Sfm_Par_t) );
+ pPars->nTfoLevMax = 2; // the maximum fanout levels
+ pPars->nFanoutMax = 10; // the maximum number of fanouts
+ pPars->nDepthMax = 0; // the maximum depth to try
+ pPars->nWinSizeMax = 500; // the maximum number of divisors
+ pPars->nBTLimit = 0; // the maximum number of conflicts in one SAT run
+ pPars->fFixLevel = 0; // does not allow level to increase
+ pPars->fArea = 0; // performs optimization for area
+ pPars->fMoreEffort = 0; // performs high-affort minimization
+ pPars->fVerbose = 0; // enable basic stats
+ pPars->fVeryVerbose = 0; // enable detailed stats
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sfm_NtkPrepare( Sfm_Ntk_t * p )
+{
+ p->vLeaves = Vec_IntAlloc( 1000 );
+ p->vRoots = Vec_IntAlloc( 1000 );
+ p->vNodes = Vec_IntAlloc( 1000 );
+ p->vTfo = Vec_IntAlloc( 1000 );
+ p->vDivs = Vec_IntAlloc( 100 );
+ p->vLits = Vec_IntAlloc( 100 );
+ p->vClauses = Vec_WecAlloc( 100 );
+ p->vFaninMap = Vec_IntAlloc( 10 );
+}
+
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
SideEffects []
SeeAlso []
***********************************************************************/
-int Sfm_ManPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
+int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
{
+ int i;
+ p->pPars = pPars;
+ Sfm_NtkPrepare( p );
+ Sfm_NtkForEachNode( p, i )
+ {
+ printf( "Node %d:\n", i );
+ Sfm_PrintCnf( (Vec_Str_t *)Vec_WecEntry(p->vCnfs, i) );
+ printf( "\n" );
+ }
return 0;
}
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index 9dad053f..d52b46e4 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -32,6 +32,7 @@
#include <assert.h>
#include "misc/vec/vec.h"
+#include "sat/bsat/satSolver.h"
#include "sfm.h"
////////////////////////////////////////////////////////////////////////
@@ -46,72 +47,88 @@ ABC_NAMESPACE_HEADER_START
struct Sfm_Ntk_t_
{
+ // parameters
+ Sfm_Par_t * pPars; // parameters
// 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
+ int nPis; // PI count (PIs should be first objects)
+ int nPos; // PO count (POs should be last objects)
+ int nNodes; // internal nodes
+ int nObjs; // total objects
+ // user data
+ Vec_Wec_t * vFanins; // fanins
+ Vec_Str_t * vFixed; // persistent objects
+ Vec_Wrd_t * vTruths; // truth tables
// 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 fOpt : 1;
- unsigned fTfo : 1;
- unsigned nFanis : 4;
- unsigned nFanos : 26;
- int Fanio[0];
-};
-
-struct Sfm_Man_t_
-{
- Sfm_Ntk_t * pNtk;
+ Vec_Wec_t * vFanouts; // fanouts
+ Vec_Int_t * vLevels; // logic level
+ Vec_Int_t vTravIds; // traversal IDs
+ Vec_Int_t vId2Var; // ObjId -> SatVar
+ Vec_Int_t vVar2Id; // SatVar -> ObjId
+ Vec_Wec_t * vCnfs; // CNFs
+ Vec_Int_t * vCover; // temporary
+ int nTravIds; // traversal IDs
// 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)
+ int iNode;
+ Vec_Int_t * vLeaves; // leaves
+ Vec_Int_t * vRoots; // roots
+ Vec_Int_t * vNodes; // internal
+ Vec_Int_t * vTfo; // TFO (excluding iNode)
// SAT solving
+ int nSatVars; // the number of variables
+ sat_solver * pSat1; // SAT solver for the on-set
+ sat_solver * pSat0; // SAT solver for the off-set
+ // intermediate data
+ Vec_Int_t * vDivs; // divisors
+ Vec_Int_t * vLits; // literals
+ Vec_Int_t * vFani; // iterator fanins
+ Vec_Int_t * vFano; // iterator fanouts
+ Vec_Wec_t * vClauses; // CNF clauses for the node
+ Vec_Int_t * vFaninMap;// mapping fanins into their SAT vars
};
+#define SFM_SAT_UNDEC 0x1234567812345678
+#define SFM_SAT_SAT 0x8765432187654321
+
////////////////////////////////////////////////////////////////////////
/// MACRO DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
-static inline Sfm_Obj_t * Sfm_ManObj( Sfm_Ntk_t * p, int Id ) { return (Sfm_Obj_t *)Vec_IntEntryP( &p->vObjs, Id ); }
+#define Sfm_NtkForEachNode( p, i ) for ( i = p->nPis; i + p->nPos < p->nObjs; i++ )
+#define Sfm_NodeForEachFanin( p, Node, Fan, i ) for ( p->vFani = Vec_WecEntry(p->vFanins, Node), i = 0; i < Vec_IntSize(p->vFani) && ((Fan = Vec_IntEntry(p->vFani, i)), 1); i++ )
+#define Sfm_NodeForEachFanout( p, Node, Fan, i ) for ( p->vFano = Vec_WecEntry(p->vFanouts, Node), i = 0; i < Vec_IntSize(p->vFani) && ((Fan = Vec_IntEntry(p->vFano, i)), 1); i++ )
+
+static inline int Sfm_ObjIsPi( Sfm_Ntk_t * p, int i ) { return i < p->nPis; }
+static inline int Sfm_ObjIsPo( Sfm_Ntk_t * p, int i ) { return i + p->nPos < p->nObjs; }
+static inline int Sfm_ObjIsNode( Sfm_Ntk_t * p, int i ) { return i >= p->nPis && i + p->nPos < p->nObjs; }
+
+static inline int Sfm_ObjFaninNum( Sfm_Ntk_t * p, int i ) { return Vec_IntSize(Vec_WecEntry(p->vFanins, i)); }
+static inline int Sfm_ObjFanoutNum( Sfm_Ntk_t * p, int i ) { return Vec_IntSize(Vec_WecEntry(p->vFanouts, i)); }
+
+static inline int Sfm_ObjSatVar( Sfm_Ntk_t * p, int iObj ) { return Vec_IntEntry(&p->vId2Var, iObj); }
+static inline void Sfm_ObjSetSatVar( Sfm_Ntk_t * p, int iObj, int Num ) { assert(Sfm_ObjSatVar(p, iObj) == -1); Vec_IntWriteEntry(&p->vId2Var, iObj, Num); Vec_IntWriteEntry(&p->vVar2Id, Num, iObj); }
+static inline void Sfm_ObjCleanSatVar( Sfm_Ntk_t * p, int Num ) { assert(Sfm_ObjSatVar(p, Vec_IntEntry(&p->vVar2Id, Num)) != -1); Vec_IntWriteEntry(&p->vId2Var, Vec_IntEntry(&p->vVar2Id, Num), Num); Vec_IntWriteEntry(&p->vVar2Id, Num, -1); }
+static inline void Sfm_NtkCleanVars( Sfm_Ntk_t * p, int nSize ) { int i; for ( i = 1; i < nSize; i++ ) Sfm_ObjCleanSatVar( p, i ); }
-#define Sfm_ManForEachObj( p, pObj, i ) \
- for ( i = 0; (i < Vec_IntSize(&p->vObjs) && ((pObj) = Sfm_ManObj(p, i))); i++ )
-#define Sfm_ManForEachPi( p, pObj, i ) \
- for ( i = 0; (i < Vec_IntSize(&p->vPis) && ((pObj) = Sfm_ManObj(p, Vec_IntEntry(&p->vPis, i)))); i++ )
-#define Sfm_ManForEachPo( p, pObj, i ) \
- for ( i = 0; (i < Vec_IntSize(&p->vPos) && ((pObj) = Sfm_ManObj(p, Vec_IntEntry(&p->vPos, i)))); i++ )
////////////////////////////////////////////////////////////////////////
/// FUNCTION DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
/*=== sfmCnf.c ==========================================================*/
-extern int Sfm_DeriveCnfs( Vec_Wrd_t * vTruths, Vec_Int_t * vFanins, Vec_Str_t ** pvCnfs, Vec_Int_t ** pvOffsets );
+extern void Sfm_PrintCnf( Vec_Str_t * vCnf );
+extern int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf );
+extern void Sfm_TranslateCnf( Vec_Wec_t * vRes, Vec_Str_t * vCnf, Vec_Int_t * vFaninMap );
/*=== sfmCore.c ==========================================================*/
-/*=== sfmMan.c ==========================================================*/
/*=== sfmNtk.c ==========================================================*/
+extern Sfm_Ntk_t * Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPos );
/*=== sfmSat.c ==========================================================*/
-extern int Sfm_CreateSatWindow( Sfm_Ntk_t * p );
-
-ABC_NAMESPACE_HEADER_END
+extern word Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_t * vDivs, Vec_Int_t * vLits, Vec_Int_t * vDiffs, int nBTLimit );
+/*=== sfmWin.c ==========================================================*/
+extern int Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode );
+extern void Sfm_NtkWin2Sat( Sfm_Ntk_t * p );
+ABC_NAMESPACE_HEADER_END
#endif
diff --git a/src/opt/sfm/sfmMan.c b/src/opt/sfm/sfmMan.c
deleted file mode 100644
index 90cfe42e..00000000
--- a/src/opt/sfm/sfmMan.c
+++ /dev/null
@@ -1,59 +0,0 @@
-/**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
index 21252e60..602f6d75 100644
--- a/src/opt/sfm/sfmNtk.c
+++ b/src/opt/sfm/sfmNtk.c
@@ -42,87 +42,202 @@ ABC_NAMESPACE_IMPL_START
SeeAlso []
***********************************************************************/
-Sfm_Ntk_t * Sfm_NtkAlloc( int nPis, int nPos, int nNodes, Vec_Int_t * vFanins, Vec_Int_t * vFanouts, Vec_Int_t * vEdges, Vec_Int_t * vOpts )
+void Sfm_CheckConsistency( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed )
{
- Sfm_Ntk_t * p;
- Sfm_Obj_t * pObj, * pFan;
- int i, k, nObjSize, AddOn = 2;
- int nStructSize = sizeof(Sfm_Obj_t) / sizeof(int);
- int iFanin, iOffset = 2, iFanOffset = 0;
- int nEdges = Vec_IntSize(vEdges);
- int nObjs = nPis + nPos + nNodes;
- int nSize = 2 + nObjs * (nStructSize + 1) + 2 * nEdges + AddOn * (nPis + Vec_IntSum(vOpts));
- assert( sizeof(Sfm_Obj_t) % sizeof(int) == 0 );
- assert( nEdges == Vec_IntSum(vFanins) );
- assert( nEdges == Vec_IntSum(vFanouts) );
- p = ABC_CALLOC( Sfm_Ntk_t, 1 );
- p->pMem = ABC_CALLOC( int, nSize );
- for ( i = 0; i < nObjs; i++ )
+ Vec_Int_t * vArray;
+ int i, k, Fanin;
+ // check entries
+ Vec_WecForEachLevel( vFanins, vArray, i )
{
- Vec_IntPush( &p->vObjs, iOffset );
- pObj = Sfm_ManObj( p, i );
- pObj->Id = i;
+ // PIs have no fanins
if ( i < nPis )
- {
- pObj->Type = 1;
- assert( Vec_IntEntry(vFanins, i) == 0 );
- assert( Vec_IntEntry(vOpts, i) == 0 );
- Vec_IntPush( &p->vPis, iOffset );
- }
- else
- {
- pObj->Type = 2;
- pObj->fOpt = Vec_IntEntry(vOpts, i);
- if ( i >= nPis + nNodes ) // PO
- {
- pObj->Type = 3;
- assert( Vec_IntEntry(vFanins, i) == 1 );
- assert( Vec_IntEntry(vFanouts, i) == 0 );
- assert( Vec_IntEntry(vOpts, i) == 0 );
- Vec_IntPush( &p->vPos, iOffset );
- }
- for ( k = 0; k < Vec_IntEntry(vFanins, i); k++ )
- {
- iFanin = Vec_IntEntry( vEdges, iFanOffset++ );
- pFan = Sfm_ManObj( p, iFanin );
- assert( iFanin < i );
- pObj->Fanio[ pObj->nFanis++ ] = iFanin;
- pFan->Fanio[ pFan->nFanis + pFan->nFanos++ ] = i;
- }
- }
- // add node size
- nObjSize = nStructSize + Vec_IntEntry(vFanins, i) + Vec_IntEntry(vFanouts, i) + AddOn * (pObj->Type==1 || pObj->fOpt);
- nObjSize += (int)( nObjSize & 1 );
- assert( (nObjSize & 1) == 0 );
- iOffset += nObjSize;
+ assert( Vec_IntSize(vArray) == 0 && Vec_StrEntry(vFixed, i) == (char)0 );
+ // nodes are in a topo order; POs cannot be fanins
+ Vec_IntForEachEntry( vArray, Fanin, k )
+ assert( Fanin < i && Fanin + nPos < Vec_WecSize(vFanins) );
+ // POs have one fanout
+ if ( i + nPos >= Vec_WecSize(vFanins) )
+ assert( Vec_IntSize(vArray) == 1 && Vec_StrEntry(vFixed, i) == (char)0 );
+ }
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Wec_t * Sfm_CreateFanout( Vec_Wec_t * vFanins )
+{
+ Vec_Wec_t * vFanouts;
+ Vec_Int_t * vArray;
+ int i, k, Fanin;
+ // count fanouts
+ vFanouts = Vec_WecStart( Vec_WecSize(vFanins) );
+ Vec_WecForEachLevel( vFanins, vArray, i )
+ Vec_IntForEachEntry( vArray, Fanin, k )
+ Vec_WecEntry( vFanouts, Fanin )->nSize++;
+ // allocate fanins
+ Vec_WecForEachLevel( vFanouts, vArray, i )
+ {
+ k = vArray->nSize; vArray->nSize = 0;
+ Vec_IntGrow( vArray, k );
}
- assert( iOffset <= nSize );
- assert( iFanOffset == Vec_IntSize(vEdges) );
- iFanOffset = 0;
- Sfm_ManForEachObj( p, pObj, i )
+ // add fanouts
+ Vec_WecForEachLevel( vFanins, vArray, i )
+ Vec_IntForEachEntry( vArray, Fanin, k )
+ Vec_IntPush( Vec_WecEntry( vFanouts, Fanin ), i );
+ // verify
+ Vec_WecForEachLevel( vFanins, vArray, i )
+ assert( Vec_IntSize(vArray) == Vec_IntCap(vArray) );
+ return vFanouts;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Sfm_CreateLevel( Vec_Wec_t * vFanins )
+{
+ Vec_Int_t * vLevels;
+ Vec_Int_t * vArray;
+ int i, k, Fanin, * pLevels;
+ vLevels = Vec_IntStart( Vec_WecSize(vFanins) );
+ pLevels = Vec_IntArray( vLevels );
+ Vec_WecForEachLevel( vFanins, vArray, i )
+ Vec_IntForEachEntry( vArray, Fanin, k )
+ pLevels[i] = Abc_MaxInt( pLevels[i], pLevels[Fanin] + 1 );
+ return vLevels;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Wec_t * Sfm_CreateCnf( Sfm_Ntk_t * p )
+{
+ Vec_Wec_t * vCnfs;
+ Vec_Str_t * vCnf, * vCnfBase;
+ word uTruth;
+ int i;
+ vCnf = Vec_StrAlloc( 100 );
+ vCnfs = Vec_WecStart( p->nObjs );
+ Vec_WrdForEachEntryStartStop( p->vTruths, uTruth, i, p->nPis, Vec_WrdSize(p->vTruths)-p->nPos )
{
- assert( Vec_IntEntry(vFanins, i) == (int)pObj->nFanis );
- assert( Vec_IntEntry(vFanouts, i) == (int)pObj->nFanos );
- for ( k = 0; k < (int)pObj->nFanis; k++ )
- assert( pObj->Fanio[k] == Vec_IntEntry(vEdges, iFanOffset++) );
+ Sfm_TruthToCnf( uTruth, Vec_IntSize(Vec_WecEntry(p->vFanins, i)), p->vCover, vCnf );
+ vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, i );
+ Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) );
+ memcpy( Vec_StrArray(vCnfBase), Vec_StrArray(vCnf), Vec_StrSize(vCnf) );
+ vCnfBase->nSize = Vec_StrSize(vCnf);
}
- assert( iFanOffset == Vec_IntSize(vEdges) );
+ Vec_StrFree( vCnf );
+ return vCnfs;
+}
+
+/**Function*************************************************************
+
+ Synopsis []
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Wrd_t * vTruths )
+{
+ Sfm_Ntk_t * p;
+ Sfm_CheckConsistency( vFanins, nPis, nPos, vFixed );
+ p = ABC_CALLOC( Sfm_Ntk_t, 1 );
+ p->nObjs = Vec_WecSize( vFanins );
+ p->nPis = nPis;
+ p->nPos = nPos;
+ p->nNodes = p->nObjs - p->nPis - p->nPos;
+ p->vFanins = vFanins;
+ // user data
+ p->vFixed = vFixed;
+ p->vTruths = vTruths;
+ // attributes
+ p->vFanouts = Sfm_CreateFanout( vFanins );
+ p->vLevels = Sfm_CreateLevel( vFanins );
+ Vec_IntFill( &p->vTravIds, p->nObjs, 0 );
+ Vec_IntFill( &p->vId2Var, p->nObjs, -1 );
+ Vec_IntFill( &p->vVar2Id, p->nObjs, -1 );
+ p->vCover = Vec_IntAlloc( 1 << 16 );
+ p->vCnfs = Sfm_CreateCnf( p );
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 );
+ // user data
+ Vec_WecFree( p->vFanins );
+ Vec_StrFree( p->vFixed );
+ Vec_WrdFree( p->vTruths );
+ // attributes
+ Vec_WecFree( p->vFanouts );
+ Vec_IntFree( p->vLevels );
ABC_FREE( p->vTravIds.pArray );
- ABC_FREE( p->vSatVars.pArray );
- ABC_FREE( p->vTruths.pArray );
+ ABC_FREE( p->vId2Var.pArray );
+ ABC_FREE( p->vVar2Id.pArray );
+ Vec_WecFree( p->vCnfs );
+ Vec_IntFree( p->vCover );
+ // other data
+ Vec_IntFreeP( &p->vLeaves );
+ Vec_IntFreeP( &p->vRoots );
+ Vec_IntFreeP( &p->vNodes );
+ Vec_IntFreeP( &p->vTfo );
+ Vec_IntFreeP( &p->vDivs );
+ Vec_IntFreeP( &p->vLits );
+ Vec_WecFreeP( &p->vClauses );
+ Vec_IntFreeP( &p->vFaninMap );
+ if ( p->pSat0 ) sat_solver_delete( p->pSat0 );
+ if ( p->pSat1 ) sat_solver_delete( p->pSat1 );
ABC_FREE( p );
}
+/**Function*************************************************************
+
+ Synopsis [Public APIs of this network.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Sfm_NodeReadFanins( Sfm_Ntk_t * p, int i )
+{
+ return Vec_WecEntry( p->vFanins, i );
+}
+word Sfm_NodeReadTruth( Sfm_Ntk_t * p, int i )
+{
+ return Vec_WrdEntry( p->vTruths, i );
+}
+int Sfm_NodeReadFixed( Sfm_Ntk_t * p, int i )
+{
+ return (int)Vec_StrEntry( p->vFixed, i );
+}
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c
index ed2a53c4..6431cd50 100644
--- a/src/opt/sfm/sfmSat.c
+++ b/src/opt/sfm/sfmSat.c
@@ -27,23 +27,76 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS ///
////////////////////////////////////////////////////////////////////////
+static word s_Truths6[6] = {
+ ABC_CONST(0xAAAAAAAAAAAAAAAA),
+ ABC_CONST(0xCCCCCCCCCCCCCCCC),
+ ABC_CONST(0xF0F0F0F0F0F0F0F0),
+ ABC_CONST(0xFF00FF00FF00FF00),
+ ABC_CONST(0xFFFF0000FFFF0000),
+ ABC_CONST(0xFFFFFFFF00000000)
+};
+
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
////////////////////////////////////////////////////////////////////////
/**Function*************************************************************
- Synopsis []
+ Synopsis [Takes SAT solver and returns interpolant.]
- Description []
+ Description [If interpolant does not exist, returns diff SAT variables.]
SideEffects []
SeeAlso []
***********************************************************************/
-int Sfm_CreateSatWindow( Sfm_Ntk_t * p )
+word Sfm_ComputeInterpolant( sat_solver * pSatOn, sat_solver * pSatOff, Vec_Int_t * vDivs, Vec_Int_t * vLits, Vec_Int_t * vDiffs, int nBTLimit )
{
+ word uTruth = 0, uCube;
+ int status, i, Div, iVar, nFinal, * pFinal;
+ int nVars = sat_solver_nvars(pSatOn);
+ int iNewLit = Abc_Var2Lit( nVars, 0 );
+ while ( 1 )
+ {
+ // find onset minterm
+ status = sat_solver_solve( pSatOn, &iNewLit, &iNewLit + 1, nBTLimit, 0, 0, 0 );
+ if ( status == l_Undef )
+ return SFM_SAT_UNDEC;
+ if ( status == l_False )
+ return uTruth;
+ assert( status == l_True );
+ // collect literals
+ Vec_IntClear( vLits );
+ Vec_IntForEachEntry( vDivs, Div, i )
+ Vec_IntPush( vLits, Abc_LitNot(sat_solver_var_literal(pSatOn, Div)) );
+ // check against offset
+ status = sat_solver_solve( pSatOff, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), nBTLimit, 0, 0, 0 );
+ if ( status == l_Undef )
+ return SFM_SAT_UNDEC;
+ if ( status == l_True )
+ {
+ Vec_IntClear( vDiffs );
+ for ( i = 0; i < nVars; i++ )
+ Vec_IntPush( vDiffs, sat_solver_var_value(pSatOn, i) ^ sat_solver_var_value(pSatOff, i) );
+ return SFM_SAT_SAT;
+ }
+ assert( status == l_False );
+ // compute cube and add clause
+ nFinal = sat_solver_final( pSatOff, &pFinal );
+ uCube = ~(word)0;
+ Vec_IntClear( vLits );
+ Vec_IntPush( vLits, Abc_LitNot(iNewLit) );
+ for ( i = 0; i < nFinal; i++ )
+ {
+ Vec_IntPush( vLits, pFinal[i] );
+ iVar = Vec_IntFind( vDivs, Abc_Lit2Var(pFinal[i]) ); assert( iVar >= 0 );
+ uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
+ }
+ uTruth |= uCube;
+ sat_solver_addclause( pSatOn, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) );
+ }
+ assert( 0 );
return 0;
}
diff --git a/src/opt/sfm/sfmWin.c b/src/opt/sfm/sfmWin.c
new file mode 100644
index 00000000..2dd98806
--- /dev/null
+++ b/src/opt/sfm/sfmWin.c
@@ -0,0 +1,171 @@
+/**CFile****************************************************************
+
+ FileName [sfmWin.c]
+
+ SystemName [ABC: Logic synthesis and verification system.]
+
+ PackageName [SAT-based optimization using internal don't-cares.]
+
+ Synopsis [Structural window computation.]
+
+ Author [Alan Mishchenko]
+
+ Affiliation [UC Berkeley]
+
+ Date [Ver. 1.0. Started - June 20, 2005.]
+
+ Revision [$Id: sfmWin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "sfmInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+/// DECLARATIONS ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+/// FUNCTION DEFINITIONS ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+ Synopsis [Working with traversal IDs.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+static inline void Sfm_NtkIncrementTravId( Sfm_Ntk_t * p ) { p->nTravIds++; }
+static inline void Sfm_ObjSetTravIdCurrent( Sfm_Ntk_t * p, int Id ) { Vec_IntWriteEntry( &p->vTravIds, Id, p->nTravIds ); }
+static inline int Sfm_ObjIsTravIdCurrent( Sfm_Ntk_t * p, int Id ) { return (Vec_IntEntry(&p->vTravIds, Id) == p->nTravIds); }
+
+/**Function*************************************************************
+
+ Synopsis [Computes structural window.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sfm_NtkCollectTfi_rec( Sfm_Ntk_t * p, int iNode )
+{
+ int i, iFanin;
+ if ( Sfm_ObjIsTravIdCurrent( p, iNode ) )
+ return;
+ Sfm_ObjSetTravIdCurrent( p, iNode );
+ if ( Sfm_ObjIsPi( p, iNode ) )
+ {
+ Vec_IntPush( p->vLeaves, iNode );
+ return;
+ }
+ Sfm_NodeForEachFanin( p, iNode, iFanin, i )
+ Sfm_NtkCollectTfi_rec( p, iFanin );
+ Vec_IntPush( p->vNodes, iNode );
+}
+int Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode )
+{
+// int i, iRoot;
+ assert( Sfm_ObjIsNode( p, iNode ) );
+ Sfm_NtkIncrementTravId( p );
+ Vec_IntClear( p->vLeaves ); // leaves
+ Vec_IntClear( p->vNodes ); // internal
+ // collect transitive fanin
+ Sfm_NtkCollectTfi_rec( p, iNode );
+ // collect TFO
+ Vec_IntClear( p->vRoots ); // roots
+ Vec_IntClear( p->vTfo ); // roots
+ Vec_IntPush( p->vRoots, iNode );
+/*
+ Vec_IntForEachEntry( p->vRoots, iRoot, i )
+ {
+ assert( Sfm_ObjIsNode(p, iRoot) );
+ if ( Sfm_ObjIsTravIdCurrent(p, iRoot) )
+ continue;
+ if ( Sfm_ObjFanoutNum(p, iRoot) >= p->pPars->nFanoutMax )
+ continue;
+ }
+*/
+ return 1;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Converts a window into a SAT solver.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+void Sfm_NtkWin2Sat( Sfm_Ntk_t * p )
+{
+ Vec_Int_t * vClause;
+ int RetValue, Lit, iNode, iFanin, i, k;
+ sat_solver * pSat0 = sat_solver_new();
+ sat_solver * pSat1 = sat_solver_new();
+ sat_solver_setnvars( pSat0, 1 + Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) );
+ sat_solver_setnvars( pSat1, 1 + Vec_IntSize(p->vLeaves) + Vec_IntSize(p->vNodes) + 2 * Vec_IntSize(p->vTfo) + Vec_IntSize(p->vRoots) );
+ // create SAT variables
+ p->nSatVars = 1;
+ Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
+ Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
+ Vec_IntForEachEntryReverse( p->vLeaves, iNode, i )
+ Sfm_ObjSetSatVar( p, iNode, p->nSatVars++ );
+ // add CNF clauses
+ Vec_IntForEachEntryReverse( p->vNodes, iNode, i )
+ {
+ // collect fanin variables
+ Vec_IntClear( p->vFaninMap );
+ Sfm_NodeForEachFanin( p, iNode, iFanin, k )
+ Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iFanin) );
+ Vec_IntPush( p->vFaninMap, Sfm_ObjSatVar(p, iNode) );
+ // generate CNF
+ Sfm_TranslateCnf( p->vClauses, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode), p->vFaninMap );
+ // add clauses
+ Vec_WecForEachLevel( p->vClauses, vClause, k )
+ {
+ if ( Vec_IntSize(vClause) == 0 )
+ break;
+ RetValue = sat_solver_addclause( pSat0, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
+ assert( RetValue );
+ RetValue = sat_solver_addclause( pSat1, Vec_IntArray(vClause), Vec_IntArray(vClause) + Vec_IntSize(vClause) );
+ assert( RetValue );
+ }
+ }
+ // add unit clause
+ Lit = Abc_Var2Lit( Sfm_ObjSatVar(p, iNode), 1 );
+ RetValue = sat_solver_addclause( pSat0, &Lit, &Lit + 1 );
+ assert( RetValue );
+ // add unit clause
+ Lit = Abc_Var2Lit( Sfm_ObjSatVar(p, iNode), 0 );
+ RetValue = sat_solver_addclause( pSat1, &Lit, &Lit + 1 );
+ assert( RetValue );
+ // finalize
+ sat_solver_compress( p->pSat0 );
+ sat_solver_compress( p->pSat1 );
+ // return the result
+ assert( p->pSat0 == NULL );
+ assert( p->pSat1 == NULL );
+ p->pSat0 = pSat0;
+ p->pSat1 = pSat1;
+}
+
+////////////////////////////////////////////////////////////////////////
+/// END OF FILE ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
generated by cgit v1.2.3 (git 2.25.1) at 2024-12-25 06:51:34 +0000