Skip to content

A
abc
Commit 9d219eee by Alan Mishchenko
Options

New MFS package.

parent 7bcd75d8
Showing with 937 additions and 221 deletions
abclib.dsp
...@@ -323,6 +323,10 @@ SOURCE=.\src\base\abci\abcMffc.c ...@@ -323,6 +323,10 @@ SOURCE=.\src\base\abci\abcMffc.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\base\abci\abcMfs.c
# End Source File
# Begin Source File
SOURCE=.\src\base\abci\abcMini.c SOURCE=.\src\base\abci\abcMini.c
# End Source File # End Source File
# Begin Source File # Begin Source File
...@@ -2075,15 +2079,15 @@ SOURCE=.\src\opt\sfm\sfmInt.h ...@@ -2075,15 +2079,15 @@ SOURCE=.\src\opt\sfm\sfmInt.h
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\opt\sfm\sfmMan.c SOURCE=.\src\opt\sfm\sfmNtk.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\opt\sfm\sfmNtk.c SOURCE=.\src\opt\sfm\sfmSat.c
# End Source File # End Source File
# Begin Source File # Begin Source File
SOURCE=.\src\opt\sfm\sfmSat.c SOURCE=.\src\opt\sfm\sfmWin.c
# End Source File # End Source File
# End Group # End Group
# End Group # End Group
......
src/base/abci/abc.c
...@@ -52,6 +52,7 @@ ...@@ -52,6 +52,7 @@
#include "proof/abs/abs.h" #include "proof/abs/abs.h"
#include "sat/bmc/bmc.h" #include "sat/bmc/bmc.h"
#include "proof/ssc/ssc.h" #include "proof/ssc/ssc.h"
#include "opt/sfm/sfm.h"
#ifndef _WIN32 #ifndef _WIN32
#include <unistd.h> #include <unistd.h>
...@@ -104,6 +105,7 @@ static int Abc_CommandLutpack ( Abc_Frame_t * pAbc, int argc, cha ...@@ -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_CommandLutmin ( Abc_Frame_t * pAbc, int argc, char ** argv );
//static int Abc_CommandImfs ( 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_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_CommandTrace ( Abc_Frame_t * pAbc, int argc, char ** argv );
static int Abc_CommandSpeedup ( 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 ); static int Abc_CommandPowerdown ( Abc_Frame_t * pAbc, int argc, char ** argv );
...@@ -607,6 +609,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) ...@@ -607,6 +609,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
Cmd_CommandAdd( pAbc, "Synthesis", "lutmin", Abc_CommandLutmin, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "lutmin", Abc_CommandLutmin, 1 );
// Cmd_CommandAdd( pAbc, "Synthesis", "imfs", Abc_CommandImfs, 1 ); // Cmd_CommandAdd( pAbc, "Synthesis", "imfs", Abc_CommandImfs, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "mfs", Abc_CommandMfs, 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", "trace", Abc_CommandTrace, 0 );
Cmd_CommandAdd( pAbc, "Synthesis", "speedup", Abc_CommandSpeedup, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "speedup", Abc_CommandSpeedup, 1 );
Cmd_CommandAdd( pAbc, "Synthesis", "powerdown", Abc_CommandPowerdown, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "powerdown", Abc_CommandPowerdown, 1 );
...@@ -4400,6 +4403,146 @@ usage: ...@@ -4400,6 +4403,146 @@ usage:
return 1; 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************************************************************* /**Function*************************************************************
src/base/abci/abcMfs.c 0 → 100644
/**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
src/base/abci/module.make
...@@ -30,6 +30,7 @@ SRC += src/base/abci/abc.c \ ...@@ -30,6 +30,7 @@ SRC += src/base/abci/abc.c \
src/base/abci/abcLutmin.c \ src/base/abci/abcLutmin.c \
src/base/abci/abcMap.c \ src/base/abci/abcMap.c \
src/base/abci/abcMerge.c \ src/base/abci/abcMerge.c \
src/base/abci/abcMfs.c \
src/base/abci/abcMini.c \ src/base/abci/abcMini.c \
src/base/abci/abcMiter.c \ src/base/abci/abcMiter.c \
src/base/abci/abcMulti.c \ src/base/abci/abcMulti.c \
......
src/misc/vec/vecInt.h
...@@ -255,6 +255,12 @@ static inline Vec_Int_t * Vec_IntDupArray( Vec_Int_t * pVec ) ...@@ -255,6 +255,12 @@ static inline Vec_Int_t * Vec_IntDupArray( Vec_Int_t * pVec )
SeeAlso [] 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 ) static inline void Vec_IntErase( Vec_Int_t * p )
{ {
ABC_FREE( p->pArray ); ABC_FREE( p->pArray );
......
src/misc/vec/vecWec.h
...@@ -245,6 +245,7 @@ static inline void Vec_WecClear( Vec_Wec_t * p ) ...@@ -245,6 +245,7 @@ static inline void Vec_WecClear( Vec_Wec_t * p )
int i; int i;
Vec_WecForEachLevel( p, vVec, i ) Vec_WecForEachLevel( p, vVec, i )
Vec_IntClear( vVec ); Vec_IntClear( vVec );
p->nSize = 0;
} }
/**Function************************************************************* /**Function*************************************************************
...@@ -315,10 +316,9 @@ static inline double Vec_WecMemory( Vec_Wec_t * p ) ...@@ -315,10 +316,9 @@ static inline double Vec_WecMemory( Vec_Wec_t * p )
***********************************************************************/ ***********************************************************************/
static inline void Vec_WecFree( Vec_Wec_t * p ) static inline void Vec_WecFree( Vec_Wec_t * p )
{ {
Vec_Int_t * vVec;
int i; int i;
Vec_WecForEachLevel( p, vVec, i ) for ( i = 0; i < p->nCap; i++ )
ABC_FREE( vVec->pArray ); ABC_FREE( p->pArray[i].pArray );
ABC_FREE( p->pArray ); ABC_FREE( p->pArray );
ABC_FREE( p ); ABC_FREE( p );
} }
...@@ -643,6 +643,8 @@ static inline void Vec_WecRemoveEmpty( Vec_Wec_t * vCubes ) ...@@ -643,6 +643,8 @@ static inline void Vec_WecRemoveEmpty( Vec_Wec_t * vCubes )
vCubes->pArray[k++] = *vCube; vCubes->pArray[k++] = *vCube;
else else
ABC_FREE( vCube->pArray ); ABC_FREE( vCube->pArray );
for ( i = k; i < Vec_WecSize(vCubes); i++ )
Vec_IntZero( Vec_WecEntry(vCubes, i) );
Vec_WecShrink( vCubes, k ); Vec_WecShrink( vCubes, k );
// Vec_WecSortByFirstInt( vCubes, 0 ); // Vec_WecSortByFirstInt( vCubes, 0 );
} }
......
src/opt/sfm/module.make
SRC += src/opt/sfm/sfmCnf.c \ SRC += src/opt/sfm/sfmCnf.c \
src/opt/sfm/sfmCore.c \ src/opt/sfm/sfmCore.c \
src/opt/sfm/sfmMan.c \
src/opt/sfm/sfmNtk.c \ src/opt/sfm/sfmNtk.c \
src/opt/sfm/sfmSat.c src/opt/sfm/sfmSat.c \
src/opt/sfm/sfmWin.c
src/opt/sfm/sfm.h
...@@ -26,6 +26,8 @@ ...@@ -26,6 +26,8 @@
/// INCLUDES /// /// INCLUDES ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
#include "misc/vec/vecWec.h"
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/// PARAMETERS /// /// PARAMETERS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -36,26 +38,18 @@ ABC_NAMESPACE_HEADER_START ...@@ -36,26 +38,18 @@ ABC_NAMESPACE_HEADER_START
/// BASIC TYPES /// /// BASIC TYPES ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
typedef struct Sfm_Man_t_ Sfm_Man_t;
typedef struct Sfm_Ntk_t_ Sfm_Ntk_t; typedef struct Sfm_Ntk_t_ Sfm_Ntk_t;
typedef struct Sfm_Par_t_ Sfm_Par_t; typedef struct Sfm_Par_t_ Sfm_Par_t;
struct Sfm_Par_t_ struct Sfm_Par_t_
{ {
int nWinTfoLevs; // the maximum fanout levels int nTfoLevMax; // the maximum fanout levels
int nFanoutsMax; // the maximum number of fanouts int nFanoutMax; // the maximum number of fanouts
int nDepthMax; // the maximum number of logic levels int nDepthMax; // the maximum depth to try
int nDivMax; // the maximum number of divisors int nWinSizeMax; // 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 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 fArea; // performs optimization for area
int fMoreEffort; // performs high-affort minimization 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 fVerbose; // enable basic stats
int fVeryVerbose; // enable detailed stats int fVeryVerbose; // enable detailed stats
}; };
...@@ -70,13 +64,14 @@ struct Sfm_Par_t_ ...@@ -70,13 +64,14 @@ struct Sfm_Par_t_
/*=== sfmCnf.c ==========================================================*/ /*=== sfmCnf.c ==========================================================*/
/*=== sfmCore.c ==========================================================*/ /*=== sfmCore.c ==========================================================*/
extern int Sfm_ManPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars ); extern void Sfm_ParSetDefault( Sfm_Par_t * pPars );
/*=== sfmMan.c ==========================================================*/ extern int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars );
extern Sfm_Man_t * Sfm_ManAlloc( Sfm_Ntk_t * p );
extern void Sfm_ManFree( Sfm_Man_t * p );
/*=== sfmNtk.c ==========================================================*/ /*=== 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 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 ==========================================================*/ /*=== sfmSat.c ==========================================================*/
......
src/opt/sfm/sfmCnf.c
...@@ -43,13 +43,38 @@ ABC_NAMESPACE_IMPL_START ...@@ -43,13 +43,38 @@ ABC_NAMESPACE_IMPL_START
SeeAlso [] 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 ) int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf )
{ {
Vec_StrClear( vCnf ); Vec_StrClear( vCnf );
if ( Truth == 0 || ~Truth == 0 ) if ( Truth == 0 || ~Truth == 0 )
{ {
Vec_StrPush( vCnf, (char)(Truth == 0) ); Vec_StrPush( vCnf, (char)(Truth == 0) );
Vec_StrPush( vCnf, -1 ); Vec_StrPush( vCnf, (char)-1 );
return 1; return 1;
} }
else else
...@@ -74,7 +99,7 @@ int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf ...@@ -74,7 +99,7 @@ int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf
assert( 0 ); assert( 0 );
} }
Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) ); Vec_StrPush( vCnf, (char)Abc_Var2Lit(nVars, c) );
Vec_StrPush( vCnf, -1 ); Vec_StrPush( vCnf, (char)-1 );
} }
} }
return nCubes; return nCubes;
...@@ -92,30 +117,25 @@ int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf ...@@ -92,30 +117,25 @@ int Sfm_TruthToCnf( word Truth, int nVars, Vec_Int_t * vCover, Vec_Str_t * vCnf
SeeAlso [] 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 * vClause;
Vec_Int_t * vOffsets, * vCover; int i, Lit;
int i, k, nFanins, nClauses = 0; char Entry;
vCnf = Vec_StrAlloc( 1000 ); Vec_WecClear( vRes );
vCnfs = Vec_StrAlloc( 1000 ); vClause = Vec_WecPushLevel( vRes );
vOffsets = Vec_IntAlloc( Vec_IntSize(vFanins) ); Vec_StrForEachEntry( vCnf, Entry, i )
vCover = Vec_IntAlloc( 1 << 16 );
assert( Vec_WrdSize(vTruths) == Vec_IntSize(vFanins) );
Vec_IntForEachEntry( vFanins, nFanins, i )
{ {
nClauses += Sfm_TruthToCnf( Vec_WrdEntry(vTruths, i), nFanins, vCover, vCnf ); Lit = (int)Entry;
Vec_IntPush( vOffsets, Vec_StrSize(vCnfs) ); if ( Lit == -1 )
for ( k = 0; k < Vec_StrSize(vCnf); k++ ) {
Vec_StrPush( vCnfs, Vec_StrEntry(vCnf, k) ); 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 /// /// END OF FILE ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
......
src/opt/sfm/sfmCore.c
...@@ -36,14 +36,73 @@ ABC_NAMESPACE_IMPL_START ...@@ -36,14 +36,73 @@ ABC_NAMESPACE_IMPL_START
Synopsis [] Synopsis []
Description [] 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 [] SideEffects []
SeeAlso [] 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; return 0;
} }
......
src/opt/sfm/sfmInt.h
...@@ -32,6 +32,7 @@ ...@@ -32,6 +32,7 @@
#include <assert.h> #include <assert.h>
#include "misc/vec/vec.h" #include "misc/vec/vec.h"
#include "sat/bsat/satSolver.h"
#include "sfm.h" #include "sfm.h"
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
...@@ -46,72 +47,88 @@ ABC_NAMESPACE_HEADER_START ...@@ -46,72 +47,88 @@ ABC_NAMESPACE_HEADER_START
struct Sfm_Ntk_t_ struct Sfm_Ntk_t_
{ {
// parameters
Sfm_Par_t * pPars; // parameters
// objects // objects
int * pMem; // memory for objects int nPis; // PI count (PIs should be first objects)
Vec_Int_t vObjs; // ObjId -> Offset int nPos; // PO count (POs should be last objects)
Vec_Int_t vPis; // PiId -> ObjId int nNodes; // internal nodes
Vec_Int_t vPos; // PoId -> ObjId int nObjs; // total objects
// fanins/fanouts // user data
Vec_Int_t vMem; // memory for overflow fanin/fanouts Vec_Wec_t * vFanins; // fanins
Vec_Str_t * vFixed; // persistent objects
Vec_Wrd_t * vTruths; // truth tables
// attributes // attributes
Vec_Int_t vLevels; Vec_Wec_t * vFanouts; // fanouts
Vec_Int_t vTravIds; Vec_Int_t * vLevels; // logic level
Vec_Int_t vSatVars; Vec_Int_t vTravIds; // traversal IDs
Vec_Wrd_t vTruths; Vec_Int_t vId2Var; // ObjId -> SatVar
}; Vec_Int_t vVar2Id; // SatVar -> ObjId
Vec_Wec_t * vCnfs; // CNFs
typedef struct Sfm_Obj_t_ Sfm_Obj_t; Vec_Int_t * vCover; // temporary
struct Sfm_Obj_t_ int nTravIds; // traversal IDs
{
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;
// window // window
Sfm_Obj_t * pNode; int iNode;
Vec_Int_t * vLeaves; // leaves Vec_Int_t * vLeaves; // leaves
Vec_Int_t * vRoots; // roots Vec_Int_t * vRoots; // roots
Vec_Int_t * vNodes; // internal Vec_Int_t * vNodes; // internal
Vec_Int_t * vTfo; // TFO (including pNode) Vec_Int_t * vTfo; // TFO (excluding iNode)
// SAT solving // 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 /// /// 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 /// /// FUNCTION DECLARATIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/*=== sfmCnf.c ==========================================================*/ /*=== 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 ==========================================================*/ /*=== sfmCore.c ==========================================================*/
/*=== sfmMan.c ==========================================================*/
/*=== sfmNtk.c ==========================================================*/ /*=== sfmNtk.c ==========================================================*/
extern Sfm_Ntk_t * Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPos );
/*=== sfmSat.c ==========================================================*/ /*=== sfmSat.c ==========================================================*/
extern int Sfm_CreateSatWindow( Sfm_Ntk_t * p ); 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 ==========================================================*/
ABC_NAMESPACE_HEADER_END extern int Sfm_NtkWindow( Sfm_Ntk_t * p, int iNode );
extern void Sfm_NtkWin2Sat( Sfm_Ntk_t * p );
ABC_NAMESPACE_HEADER_END
#endif #endif
......
src/opt/sfm/sfmMan.c deleted 100644 → 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
src/opt/sfm/sfmNtk.c
...@@ -42,87 +42,202 @@ ABC_NAMESPACE_IMPL_START ...@@ -42,87 +42,202 @@ ABC_NAMESPACE_IMPL_START
SeeAlso [] 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; Vec_Int_t * vArray;
Sfm_Obj_t * pObj, * pFan; int i, k, Fanin;
int i, k, nObjSize, AddOn = 2; // check entries
int nStructSize = sizeof(Sfm_Obj_t) / sizeof(int); Vec_WecForEachLevel( vFanins, vArray, i )
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_IntPush( &p->vObjs, iOffset ); // PIs have no fanins
pObj = Sfm_ManObj( p, i );
pObj->Id = i;
if ( i < nPis ) if ( i < nPis )
{ assert( Vec_IntSize(vArray) == 0 && Vec_StrEntry(vFixed, i) == (char)0 );
pObj->Type = 1; // nodes are in a topo order; POs cannot be fanins
assert( Vec_IntEntry(vFanins, i) == 0 ); Vec_IntForEachEntry( vArray, Fanin, k )
assert( Vec_IntEntry(vOpts, i) == 0 ); assert( Fanin < i && Fanin + nPos < Vec_WecSize(vFanins) );
Vec_IntPush( &p->vPis, iOffset ); // POs have one fanout
} if ( i + nPos >= Vec_WecSize(vFanins) )
else assert( Vec_IntSize(vArray) == 1 && Vec_StrEntry(vFixed, i) == (char)0 );
{ }
pObj->Type = 2; }
pObj->fOpt = Vec_IntEntry(vOpts, i);
if ( i >= nPis + nNodes ) // PO /**Function*************************************************************
{
pObj->Type = 3; Synopsis []
assert( Vec_IntEntry(vFanins, i) == 1 );
assert( Vec_IntEntry(vFanouts, i) == 0 ); Description []
assert( Vec_IntEntry(vOpts, i) == 0 );
Vec_IntPush( &p->vPos, iOffset ); SideEffects []
}
for ( k = 0; k < Vec_IntEntry(vFanins, i); k++ ) SeeAlso []
{
iFanin = Vec_IntEntry( vEdges, iFanOffset++ ); ***********************************************************************/
pFan = Sfm_ManObj( p, iFanin ); Vec_Wec_t * Sfm_CreateFanout( Vec_Wec_t * vFanins )
assert( iFanin < i ); {
pObj->Fanio[ pObj->nFanis++ ] = iFanin; Vec_Wec_t * vFanouts;
pFan->Fanio[ pFan->nFanis + pFan->nFanos++ ] = i; Vec_Int_t * vArray;
} int i, k, Fanin;
} // count fanouts
// add node size vFanouts = Vec_WecStart( Vec_WecSize(vFanins) );
nObjSize = nStructSize + Vec_IntEntry(vFanins, i) + Vec_IntEntry(vFanouts, i) + AddOn * (pObj->Type==1 || pObj->fOpt); Vec_WecForEachLevel( vFanins, vArray, i )
nObjSize += (int)( nObjSize & 1 ); Vec_IntForEachEntry( vArray, Fanin, k )
assert( (nObjSize & 1) == 0 ); Vec_WecEntry( vFanouts, Fanin )->nSize++;
iOffset += nObjSize; // allocate fanins
Vec_WecForEachLevel( vFanouts, vArray, i )
{
k = vArray->nSize; vArray->nSize = 0;
Vec_IntGrow( vArray, k );
} }
assert( iOffset <= nSize ); // add fanouts
assert( iFanOffset == Vec_IntSize(vEdges) ); Vec_WecForEachLevel( vFanins, vArray, i )
iFanOffset = 0; Vec_IntForEachEntry( vArray, Fanin, k )
Sfm_ManForEachObj( p, pObj, i ) 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 ); Sfm_TruthToCnf( uTruth, Vec_IntSize(Vec_WecEntry(p->vFanins, i)), p->vCover, vCnf );
assert( Vec_IntEntry(vFanouts, i) == (int)pObj->nFanos ); vCnfBase = (Vec_Str_t *)Vec_WecEntry( vCnfs, i );
for ( k = 0; k < (int)pObj->nFanis; k++ ) Vec_StrGrow( vCnfBase, Vec_StrSize(vCnf) );
assert( pObj->Fanio[k] == Vec_IntEntry(vEdges, iFanOffset++) ); 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; return p;
} }
void Sfm_NtkFree( Sfm_Ntk_t * p ) void Sfm_NtkFree( Sfm_Ntk_t * p )
{ {
ABC_FREE( p->pMem ); // user data
ABC_FREE( p->vObjs.pArray ); Vec_WecFree( p->vFanins );
ABC_FREE( p->vPis.pArray ); Vec_StrFree( p->vFixed );
ABC_FREE( p->vPos.pArray ); Vec_WrdFree( p->vTruths );
ABC_FREE( p->vMem.pArray ); // attributes
ABC_FREE( p->vLevels.pArray ); Vec_WecFree( p->vFanouts );
Vec_IntFree( p->vLevels );
ABC_FREE( p->vTravIds.pArray ); ABC_FREE( p->vTravIds.pArray );
ABC_FREE( p->vSatVars.pArray ); ABC_FREE( p->vId2Var.pArray );
ABC_FREE( p->vTruths.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 ); 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 /// /// END OF FILE ///
......
src/opt/sfm/sfmSat.c
...@@ -27,23 +27,76 @@ ABC_NAMESPACE_IMPL_START ...@@ -27,23 +27,76 @@ ABC_NAMESPACE_IMPL_START
/// DECLARATIONS /// /// 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 DEFINITIONS ///
//////////////////////////////////////////////////////////////////////// ////////////////////////////////////////////////////////////////////////
/**Function************************************************************* /**Function*************************************************************
Synopsis [] Synopsis [Takes SAT solver and returns interpolant.]
Description [] Description [If interpolant does not exist, returns diff SAT variables.]
SideEffects [] SideEffects []
SeeAlso [] 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; return 0;
} }
......
src/opt/sfm/sfmWin.c 0 → 100644
/**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
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment