diff options
Diffstat (limited to 'src/opt/sfm')
-rw-r--r-- | src/opt/sfm/module.make | 4 | ||||
-rw-r--r-- | src/opt/sfm/sfm.h | 31 | ||||
-rw-r--r-- | src/opt/sfm/sfmCnf.c | 62 | ||||
-rw-r--r-- | src/opt/sfm/sfmCore.c | 61 | ||||
-rw-r--r-- | src/opt/sfm/sfmInt.h | 105 | ||||
-rw-r--r-- | src/opt/sfm/sfmMan.c | 59 | ||||
-rw-r--r-- | src/opt/sfm/sfmNtk.c | 249 | ||||
-rw-r--r-- | src/opt/sfm/sfmSat.c | 59 | ||||
-rw-r--r-- | src/opt/sfm/sfmWin.c | 171 |
9 files changed, 586 insertions, 215 deletions
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 + |