diff options
35 files changed, 1843 insertions, 113 deletions
@@ -1083,6 +1083,10 @@ SOURCE=.\src\base\acb\acbPar.h # End Source File # Begin Source File +SOURCE=.\src\base\acb\acbPush.c +# End Source File +# Begin Source File + SOURCE=.\src\base\acb\acbSets.c # End Source File # Begin Source File @@ -4803,6 +4807,10 @@ SOURCE=.\src\aig\gia\giaSupMin.c # End Source File # Begin Source File +SOURCE=.\src\aig\gia\giaSupp.c +# End Source File +# Begin Source File + SOURCE=.\src\aig\gia\giaSweep.c # End Source File # Begin Source File diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 5ad87008..f8e36a4f 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -577,6 +577,7 @@ static inline int Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pO static inline int Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert( Gia_ObjId(p, pObj) < p->nTravIdsAlloc ); return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds - 1); } static inline void Gia_ObjSetTravIdCurrentId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); p->pTravIds[Id] = p->nTravIds; } static inline int Gia_ObjIsTravIdCurrentId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); return (p->pTravIds[Id] == p->nTravIds); } +static inline int Gia_ObjIsTravIdPreviousId( Gia_Man_t * p, int Id ) { assert( Id < p->nTravIdsAlloc ); return (p->pTravIds[Id] == p->nTravIds - 1); } static inline void Gia_ManTimeClean( Gia_Man_t * p ) { int i; assert( p->vTiming != NULL ); Vec_FltFill(p->vTiming, 3*Gia_ManObjNum(p), 0); for ( i = 0; i < Gia_ManObjNum(p); i++ ) Vec_FltWriteEntry( p->vTiming, 3*i+1, (float)(ABC_INFINITY) ); } static inline void Gia_ManTimeStart( Gia_Man_t * p ) { assert( p->vTiming == NULL ); p->vTiming = Vec_FltAlloc(0); Gia_ManTimeClean( p ); } @@ -1464,6 +1465,15 @@ extern int Gia_ManComputeOneWin( Gia_Man_t * p, int iPivot, Vec_ /*=== giaStg.c ============================================================*/ extern void Gia_ManStgPrint( FILE * pFile, Vec_Int_t * vLines, int nIns, int nOuts, int nStates ); extern Gia_Man_t * Gia_ManStgRead( char * pFileName, int kHot, int fVerbose ); +/*=== giaSupp.c ============================================================*/ +typedef struct Gia_ManMin_t_ Gia_ManMin_t; +extern Gia_ManMin_t * Gia_ManSuppStart( Gia_Man_t * pGia ); +extern void Gia_ManSuppStop( Gia_ManMin_t * p ); +extern int Gia_ManSupportAnd( Gia_ManMin_t * p, int iLit0, int iLit1 ); +typedef struct Gia_Man2Min_t_ Gia_Man2Min_t; +extern Gia_Man2Min_t * Gia_Man2SuppStart( Gia_Man_t * pGia ); +extern void Gia_Man2SuppStop( Gia_Man2Min_t * p ); +extern int Gia_Man2SupportAnd( Gia_Man2Min_t * p, int iLit0, int iLit1 ); /*=== giaSweep.c ============================================================*/ extern Gia_Man_t * Gia_ManFraigSweepSimple( Gia_Man_t * p, void * pPars ); extern Gia_Man_t * Gia_ManSweepWithBoxes( Gia_Man_t * p, void * pParsC, void * pParsS, int fConst, int fEquiv, int fVerbose, int fVerbEquivs ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index ee709df4..5e7dc639 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -1638,6 +1638,57 @@ Gia_Man_t * Gia_ManDupExist( Gia_Man_t * p, int iVar ) /**Function************************************************************* + Synopsis [Existentially quantified given variable.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupUniv( Gia_Man_t * p, int iVar ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i; + assert( iVar >= 0 && iVar < Gia_ManPiNum(p) ); + assert( Gia_ManRegNum(p) == 0 ); + Gia_ManFillValue( p ); + // find the cofactoring variable + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManHashAlloc( pNew ); + // compute negative cofactor + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 0 ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachPo( p, pObj, i ) + pObj->Value = Gia_ObjFanin0Copy(pObj); + // compute the positive cofactor + Gia_ManPi( p, iVar )->Value = Abc_Var2Lit( 0, 1 ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + // create OR gate + Gia_ManForEachPo( p, pObj, i ) + { + if ( i == 0 ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ManHashAnd(pNew, Gia_ObjFanin0Copy(pObj), pObj->Value) ); + else + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + +/**Function************************************************************* + Synopsis [Existentially quantifies the given variable.] Description [] diff --git a/src/aig/gia/giaEsop.c b/src/aig/gia/giaEsop.c index 13627c0c..a819bc20 100644 --- a/src/aig/gia/giaEsop.c +++ b/src/aig/gia/giaEsop.c @@ -167,7 +167,7 @@ Vec_Wec_t * Eso_ManCoverDerive( Eso_Man_t * p, Vec_Ptr_t * vCover ) } } } - assert( Abc_MaxInt(Vec_WecSize(vRes), 8) == Vec_WecCap(vRes) ); + //assert( Abc_MaxInt(Vec_WecSize(vRes), 8) == Vec_WecCap(vRes) ); return vRes; } Gia_Man_t * Eso_ManCoverConvert( Eso_Man_t * p, Vec_Ptr_t * vCover ) diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index ab80a762..0f656b03 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -1498,7 +1498,7 @@ int Gia_ManFromIfLogicFindLut( If_Man_t * pIfMan, Gia_Man_t * pNew, If_Cut_t * p SeeAlso [] ***********************************************************************/ -void Gia_ManFromIfGetConfig( Vec_Int_t * vConfigs, If_Man_t * pIfMan, If_Cut_t * pCutBest, int fCompl ) +void Gia_ManFromIfGetConfig( Vec_Int_t * vConfigs, If_Man_t * pIfMan, If_Cut_t * pCutBest, int iLit, Vec_Str_t * vConfigsStr ) { If_Obj_t * pIfObj; word * pPerm = If_DsdManGetFuncConfig( pIfMan->pIfDsdMan, If_CutDsdLit(pIfMan, pCutBest) ); // cell input -> DSD input @@ -1537,10 +1537,33 @@ void Gia_ManFromIfGetConfig( Vec_Int_t * vConfigs, If_Man_t * pIfMan, If_Cut_t * } // remember complementation assert( nTtBitNum + nPermBitNum < 32 * nIntNum ); - if ( Abc_LitIsCompl(If_CutDsdLit(pIfMan, pCutBest)) ^ pCutBest->fCompl ^ fCompl ) + if ( Abc_LitIsCompl(If_CutDsdLit(pIfMan, pCutBest)) ^ pCutBest->fCompl ^ Abc_LitIsCompl(iLit) ) Abc_TtSetBit( pArray, nTtBitNum + nPermBitNum ); // update count Vec_IntAddToEntry( vConfigs, 0, 1 ); + // write configs + if ( vConfigsStr ) + { + Vec_StrPrintF( vConfigsStr, "%d", Abc_Lit2Var(iLit) ); + Vec_StrPush( vConfigsStr, ' ' ); + for ( i = 0; i < nTtBitNum; i++ ) + Vec_StrPush( vConfigsStr, (char)(Abc_TtGetBit(pArray, i) ? '1' : '0') ); + Vec_StrPush( vConfigsStr, ' ' ); + Vec_StrPush( vConfigsStr, ' ' ); + for ( v = 0; v < nVarNum; v++ ) + { + for ( i = 0; i < nPermBitOne; i++ ) + { + Vec_StrPush( vConfigsStr, (char)(Abc_TtGetBit(pArray, nTtBitNum + v * nPermBitOne + i) ? '1' : '0') ); + if ( i == 0 ) + Vec_StrPush( vConfigsStr, ' ' ); + } + Vec_StrPush( vConfigsStr, ' ' ); + Vec_StrPush( vConfigsStr, ' ' ); + } + Vec_StrPush( vConfigsStr, (char)(Abc_TtGetBit(pArray, nTtBitNum + nPermBitNum) ? '1' : '0') ); + Vec_StrPush( vConfigsStr, '\n' ); + } } int Gia_ManFromIfLogicFindCell( If_Man_t * pIfMan, Gia_Man_t * pNew, Gia_Man_t * pTemp, If_Cut_t * pCutBest, Ifn_Ntk_t * pNtkCell, int nLutMax, Vec_Int_t * vLeaves, Vec_Int_t * vLits, Vec_Int_t * vCover, Vec_Int_t * vMapping, Vec_Int_t * vMapping2, Vec_Int_t * vConfigs ) { @@ -1730,11 +1753,13 @@ int Gia_ManFromIfLogicAndVars( Gia_Man_t * pNew, If_Man_t * pIfMan, If_Cut_t * p ***********************************************************************/ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) { + int fWriteConfigs = 1; Gia_Man_t * pNew, * pHashed = NULL; If_Cut_t * pCutBest; If_Obj_t * pIfObj, * pIfLeaf; Vec_Int_t * vMapping, * vMapping2, * vPacking = NULL, * vConfigs = NULL; Vec_Int_t * vLeaves, * vLeaves2, * vCover, * vLits; + Vec_Str_t * vConfigsStr = NULL; Ifn_Ntk_t * pNtkCell = NULL; sat_solver * pSat = NULL; int i, k, Entry; @@ -1757,6 +1782,8 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) vConfigs = Vec_IntAlloc( 1000 ); Vec_IntPush( vConfigs, 0 ); Vec_IntPush( vConfigs, nConfigInts ); + if ( fWriteConfigs ) + vConfigsStr = Vec_StrAlloc( 1000 ); } // create new manager pNew = Gia_ManStart( If_ManObjNum(pIfMan) ); @@ -1840,7 +1867,7 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) pIfObj->iCopy = Gia_ManFromIfLogicNode( pIfMan, pNew, i, vLeaves, vLeaves2, pTruth, pIfMan->pPars->pLutStruct, vCover, vMapping, vMapping2, vPacking, (pIfMan->pPars->fEnableCheck75 || pIfMan->pPars->fEnableCheck75u), pIfMan->pPars->fEnableCheck07 ); pIfObj->iCopy = Abc_LitNotCond( pIfObj->iCopy, pCutBest->fCompl ); if ( vConfigs && Vec_IntSize(vLeaves) > 1 && !Gia_ObjIsCi(Gia_ManObj(pNew, Abc_Lit2Var(pIfObj->iCopy))) && pIfObj->iCopy > 1 ) - Gia_ManFromIfGetConfig( vConfigs, pIfMan, pCutBest, Abc_LitIsCompl(pIfObj->iCopy) ); + Gia_ManFromIfGetConfig( vConfigs, pIfMan, pCutBest, pIfObj->iCopy, vConfigsStr ); } else { @@ -1921,6 +1948,27 @@ Gia_Man_t * Gia_ManFromIfLogic( If_Man_t * pIfMan ) Gia_ManForEachCi( pNew, pObj, i ) assert( !Gia_ObjIsLut(pNew, Gia_ObjId(pNew, pObj)) ); } + // dump configuration strings + if ( vConfigsStr ) + { + FILE * pFile; int status; + char * pStr, Buffer[1000] = {0}; + char * pNameGen = pIfMan->pName? Extra_FileNameGeneric( pIfMan->pName ) : "nameless_"; + sprintf( Buffer, "%s_configs.txt", pNameGen ); + ABC_FREE( pNameGen ); + pFile = fopen( Buffer, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\".\n", Buffer ); + return pNew; + } + Vec_StrPush( vConfigsStr, '\0' ); + pStr = Vec_StrArray(vConfigsStr); + status = fwrite( pStr, strlen(pStr), 1, pFile ); + Vec_StrFree( vConfigsStr ); + fclose( pFile ); + printf( "Finished dumping configs into file \"%s\".\n", Buffer ); + } return pNew; } diff --git a/src/aig/gia/giaSupp.c b/src/aig/gia/giaSupp.c new file mode 100644 index 00000000..d9ba4e70 --- /dev/null +++ b/src/aig/gia/giaSupp.c @@ -0,0 +1,887 @@ +/**CFile**************************************************************** + + FileName [giaSupp.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Support minimization for AIGs.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaSupp.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "sat/satoko/satoko.h" +#include "sat/satoko/solver.h" + +#ifdef ABC_USE_CUDD +#include "bdd/extrab/extraBdd.h" +#endif + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#ifdef ABC_USE_CUDD + +struct Gia_ManMin_t_ +{ + // problem formulation + Gia_Man_t * pGia; + int iLits[2]; + // structural information + Vec_Int_t * vCis[2]; + Vec_Int_t * vObjs[2]; + Vec_Int_t * vCleared; + // intermediate functions + DdManager * dd; + Vec_Ptr_t * vFuncs; + Vec_Int_t * vSupp; +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Create/delete the data representation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_ManMin_t * Gia_ManSuppStart( Gia_Man_t * pGia ) +{ + Gia_ManMin_t * p; + p = ABC_CALLOC( Gia_ManMin_t, 1 ); + p->pGia = pGia; + p->vCis[0] = Vec_IntAlloc( 512 ); + p->vCis[1] = Vec_IntAlloc( 512 ); + p->vObjs[0] = Vec_IntAlloc( 512 ); + p->vObjs[1] = Vec_IntAlloc( 512 ); + p->vCleared = Vec_IntAlloc( 512 ); + p->dd = Cudd_Init( 0, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); +// Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT ); + Cudd_AutodynDisable( p->dd ); + p->vFuncs = Vec_PtrAlloc( 10000 ); + p->vSupp = Vec_IntAlloc( 10000 ); + return p; +} +void Gia_ManSuppStop( Gia_ManMin_t * p ) +{ + Vec_IntFreeP( &p->vCis[0] ); + Vec_IntFreeP( &p->vCis[1] ); + Vec_IntFreeP( &p->vObjs[0] ); + Vec_IntFreeP( &p->vObjs[1] ); + Vec_IntFreeP( &p->vCleared ); + Vec_PtrFreeP( &p->vFuncs ); + Vec_IntFreeP( &p->vSupp ); + printf( "Refs = %d. \n", Cudd_CheckZeroRef( p->dd ) ); + Cudd_Quit( p->dd ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Compute variables, which are not in the support.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManFindRemoved( Gia_ManMin_t * p ) +{ + extern void ddSupportStep2( DdNode * f, int * support ); + extern void ddClearFlag2( DdNode * f ); + + //int fVerbose = 1; + int nBddLimit = 100000; + int nPart0 = Vec_IntSize(p->vCis[0]); + int n, i, iObj, nVars = 0; + DdNode * bFunc0, * bFunc1, * bFunc; + Vec_PtrFillExtra( p->vFuncs, Gia_ManObjNum(p->pGia), NULL ); + // assign variables + for ( n = 0; n < 2; n++ ) + Vec_IntForEachEntry( p->vCis[n], iObj, i ) + Vec_PtrWriteEntry( p->vFuncs, iObj, Cudd_bddIthVar(p->dd, nVars++) ); + // create nodes + for ( n = 0; n < 2; n++ ) + Vec_IntForEachEntry( p->vObjs[n], iObj, i ) + { + Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj ); + bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(p->vFuncs, Gia_ObjFaninId0(pObj, iObj)), Gia_ObjFaninC0(pObj) ); + bFunc1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(p->vFuncs, Gia_ObjFaninId1(pObj, iObj)), Gia_ObjFaninC1(pObj) ); + bFunc = Cudd_bddAndLimit( p->dd, bFunc0, bFunc1, nBddLimit ); + assert( bFunc != NULL ); + Cudd_Ref( bFunc ); + Vec_PtrWriteEntry( p->vFuncs, iObj, bFunc ); + } + // create new node + bFunc0 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(p->vFuncs, Abc_Lit2Var(p->iLits[0])), Abc_LitIsCompl(p->iLits[0]) ); + bFunc1 = Cudd_NotCond( (DdNode *)Vec_PtrEntry(p->vFuncs, Abc_Lit2Var(p->iLits[1])), Abc_LitIsCompl(p->iLits[1]) ); + bFunc = Cudd_bddAndLimit( p->dd, bFunc0, bFunc1, nBddLimit ); + assert( bFunc != NULL ); + Cudd_Ref( bFunc ); + //if ( fVerbose ) Extra_bddPrint( p->dd, bFunc ), printf( "\n" ); + // collect support + Vec_IntFill( p->vSupp, nVars, 0 ); + ddSupportStep2( Cudd_Regular(bFunc), Vec_IntArray(p->vSupp) ); + ddClearFlag2( Cudd_Regular(bFunc) ); + // find variables not present in the support + Vec_IntClear( p->vCleared ); + for ( i = 0; i < nVars; i++ ) + if ( Vec_IntEntry(p->vSupp, i) == 0 ) + Vec_IntPush( p->vCleared, i < nPart0 ? Vec_IntEntry(p->vCis[0], i) : Vec_IntEntry(p->vCis[1], i-nPart0) ); + //printf( "%d(%d)%d ", Cudd_SupportSize(p->dd, bFunc), Vec_IntSize(p->vCleared), Cudd_DagSize(bFunc) ); + // deref results + Cudd_RecursiveDeref( p->dd, bFunc ); + for ( n = 0; n < 2; n++ ) + Vec_IntForEachEntry( p->vObjs[n], iObj, i ) + Cudd_RecursiveDeref( p->dd, (DdNode *)Vec_PtrEntry(p->vFuncs, iObj) ); + //Vec_IntPrint( p->vCleared ); + return Vec_IntSize(p->vCleared); +} + +/**Function************************************************************* + + Synopsis [Compute variables, which are not in the support.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManRebuildOne( Gia_ManMin_t * p, int n ) +{ + int i, iObj, iGiaLitNew = -1; + Vec_Int_t * vTempIns = p->vCis[n]; + Vec_Int_t * vTempNds = p->vObjs[n]; + Vec_Int_t * vCopies = &p->pGia->vCopies; + Vec_IntFillExtra( vCopies, Gia_ManObjNum(p->pGia), -1 ); + assert( p->iLits[n] >= 2 ); + // process inputs + Vec_IntForEachEntry( vTempIns, iObj, i ) + Vec_IntWriteEntry( vCopies, iObj, Abc_Var2Lit(iObj, 0) ); + // process constants + assert( Vec_IntSize(p->vCleared) > 0 ); + Vec_IntForEachEntry( p->vCleared, iObj, i ) + Vec_IntWriteEntry( vCopies, iObj, 0 ); + if ( Vec_IntSize(vTempNds) == 0 ) + iGiaLitNew = Vec_IntEntry( vCopies, Abc_Lit2Var(p->iLits[n]) ); + else + { + Vec_IntForEachEntry( vTempNds, iObj, i ) + { + Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj ); + int iGiaLit0 = Vec_IntEntry( vCopies, Gia_ObjFaninId0p(p->pGia, pObj) ); + int iGiaLit1 = Vec_IntEntry( vCopies, Gia_ObjFaninId1p(p->pGia, pObj) ); + iGiaLit0 = Abc_LitNotCond( iGiaLit0, Gia_ObjFaninC0(pObj) ); + iGiaLit1 = Abc_LitNotCond( iGiaLit1, Gia_ObjFaninC1(pObj) ); + iGiaLitNew = Gia_ManHashAnd( p->pGia, iGiaLit0, iGiaLit1 ); + Vec_IntWriteEntry( vCopies, iObj, iGiaLitNew ); + } + assert( Abc_Lit2Var(p->iLits[n]) == iObj ); + } + return Abc_LitNotCond( iGiaLitNew, Abc_LitIsCompl(p->iLits[n]) ); +} + +/**Function************************************************************* + + Synopsis [Collect nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_ManGatherSupp_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vCis, Vec_Int_t * vObjs ) +{ + int Val0, Val1; + Gia_Obj_t * pObj; + if ( Gia_ObjIsTravIdPreviousId(p, iObj) ) + return 1; + if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) + return 0; + Gia_ObjSetTravIdCurrentId(p, iObj); + pObj = Gia_ManObj( p, iObj ); + if ( Gia_ObjIsCi(pObj) ) + { + Vec_IntPush( vCis, iObj ); + return 0; + } + assert( Gia_ObjIsAnd(pObj) ); + Val0 = Gia_ManGatherSupp_rec( p, Gia_ObjFaninId0(pObj, iObj), vCis, vObjs ); + Val1 = Gia_ManGatherSupp_rec( p, Gia_ObjFaninId1(pObj, iObj), vCis, vObjs ); + Vec_IntPush( vObjs, iObj ); + return Val0 || Val1; +} +int Gia_ManGatherSupp( Gia_ManMin_t * p ) +{ + int n, Overlap = 0; + Gia_ManIncrementTravId( p->pGia ); + for ( n = 0; n < 2; n++ ) + { + Vec_IntClear( p->vCis[n] ); + Vec_IntClear( p->vObjs[n] ); + Gia_ManIncrementTravId( p->pGia ); + Overlap = Gia_ManGatherSupp_rec( p->pGia, Abc_Lit2Var(p->iLits[n]), p->vCis[n], p->vObjs[n] ); + assert( n || !Overlap ); + } + return Overlap; +} + +/**Function************************************************************* + + Synopsis [Takes a literal and returns a support-minized literal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManSupportAnd( Gia_ManMin_t * p, int iLit0, int iLit1 ) +{ + int iLitNew0, iLitNew1; + p->iLits[0] = iLit0; + p->iLits[1] = iLit1; + if ( iLit0 < 2 || iLit1 < 2 || !Gia_ManGatherSupp(p) || !Gia_ManFindRemoved(p) ) + return Gia_ManHashAnd( p->pGia, iLit0, iLit1 ); + iLitNew0 = Gia_ManRebuildOne( p, 0 ); + iLitNew1 = Gia_ManRebuildOne( p, 1 ); + return Gia_ManHashAnd( p->pGia, iLitNew0, iLitNew1 ); +} + + +#else + +Gia_ManMin_t * Gia_ManSuppStart( Gia_Man_t * pGia ) { return NULL; } +int Gia_ManSupportAnd( Gia_ManMin_t * p, int iLit0, int iLit1 ) { return 0; } +void Gia_ManSuppStop( Gia_ManMin_t * p ) {} + +#endif + + +/**Function************************************************************* + + Synopsis [Testbench.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManSupportAndTest( Gia_Man_t * pGia ) +{ + Gia_ManMin_t * pMan; + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i; + Gia_ManFillValue( pGia ); + pNew = Gia_ManStart( Gia_ManObjNum(pGia) ); + pNew->pName = Abc_UtilStrsav( pGia->pName ); + pNew->pSpec = Abc_UtilStrsav( pGia->pSpec ); + Gia_ManHashAlloc( pNew ); + Gia_ManConst0(pGia)->Value = 0; + pMan = Gia_ManSuppStart( pNew ); + Gia_ManForEachObj1( pGia, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + { +// pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + pObj->Value = Gia_ManSupportAnd( pMan, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } + else if ( Gia_ObjIsCi(pObj) ) + pObj->Value = Gia_ManAppendCi( pNew ); + else if ( Gia_ObjIsCo(pObj) ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + else assert( 0 ); + + if ( i % 10000 == 0 ) + printf( "%d\n", i ); + } + Gia_ManSuppStop( pMan ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia) ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + + + + +struct Gia_Man2Min_t_ +{ + // problem formulation + Gia_Man_t * pGia; + int iLits[2]; + // structural information + Vec_Int_t * vCis[2]; + Vec_Int_t * vObjs[2]; + // SAT solving + satoko_t * pSat; // SAT solver + Vec_Wrd_t * vSims; // simulation + Vec_Ptr_t * vFrontier; // CNF construction + Vec_Ptr_t * vFanins; // CNF construction + Vec_Int_t * vSatVars; // nodes + int nCisOld; // previous number of CIs + int iPattern; // the next pattern to write + int nSatSat; + int nSatUnsat; + int nCalls; + int nSims; + int nSupps; +}; + +static inline int Gia_Min2ObjSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { return Gia_ObjCopyArray(p, Gia_ObjId(p, pObj)); } +static inline int Gia_Min2ObjSetSatId( Gia_Man_t * p, Gia_Obj_t * pObj, int Num ) { assert(Gia_Min2ObjSatId(p, pObj) == -1); Gia_ObjSetCopyArray(p, Gia_ObjId(p, pObj), Num); return Num; } +static inline void Gia_Min2ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(Gia_Min2ObjSatId(p, pObj) != -1); Gia_ObjSetCopyArray(p, Gia_ObjId(p, pObj), -1); } + + +/**Function************************************************************* + + Synopsis [Create/delete the data representation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man2Min_t * Gia_Man2SuppStart( Gia_Man_t * pGia ) +{ + Gia_Man2Min_t * p; + p = ABC_CALLOC( Gia_Man2Min_t, 1 ); + p->pGia = pGia; + p->vCis[0] = Vec_IntAlloc( 512 ); + p->vCis[1] = Vec_IntAlloc( 512 ); + p->vObjs[0] = Vec_IntAlloc( 512 ); + p->vObjs[1] = Vec_IntAlloc( 512 ); + // SAT solving + p->pSat = satoko_create(); + p->vSims = Vec_WrdAlloc( 1000 ); + p->vFrontier = Vec_PtrAlloc( 1000 ); + p->vFanins = Vec_PtrAlloc( 100 ); + p->vSatVars = Vec_IntAlloc( 100 ); + p->iPattern = 1; + p->pSat->opts.learnt_ratio = 0; // prevent garbage collection + return p; +} +void Gia_Man2SuppStop( Gia_Man2Min_t * p ) +{ + printf( "Total calls = %8d. Supps = %6d. Sims = %6d. SAT = %6d. UNSAT = %6d.\n", + p->nCalls, p->nSupps, p->nSims, p->nSatSat, p->nSatUnsat ); + Vec_IntFreeP( &p->vCis[0] ); + Vec_IntFreeP( &p->vCis[1] ); + Vec_IntFreeP( &p->vObjs[0] ); + Vec_IntFreeP( &p->vObjs[1] ); + Gia_ManCleanMark01( p->pGia ); + satoko_destroy( p->pSat ); + Vec_WrdFreeP( &p->vSims ); + Vec_PtrFreeP( &p->vFrontier ); + Vec_PtrFreeP( &p->vFanins ); + Vec_IntFreeP( &p->vSatVars ); + ABC_FREE( p ); +} + +/**Function************************************************************* + + Synopsis [Adds clauses to the solver.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_Min2AddClausesMux( Gia_Man_t * p, Gia_Obj_t * pNode, satoko_t * pSat ) +{ + int fPolarFlip = 0; + Gia_Obj_t * pNodeI, * pNodeT, * pNodeE; + int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE; + + assert( !Gia_IsComplement( pNode ) ); + assert( pNode->fMark0 ); + // get nodes (I = if, T = then, E = else) + pNodeI = Gia_ObjRecognizeMux( pNode, &pNodeT, &pNodeE ); + // get the variable numbers + VarF = Gia_Min2ObjSatId(p, pNode); + VarI = Gia_Min2ObjSatId(p, pNodeI); + VarT = Gia_Min2ObjSatId(p, Gia_Regular(pNodeT)); + VarE = Gia_Min2ObjSatId(p, Gia_Regular(pNodeE)); + // get the complementation flags + fCompT = Gia_IsComplement(pNodeT); + fCompE = Gia_IsComplement(pNodeE); + + // f = ITE(i, t, e) + + // i' + t' + f + // i' + t + f' + // i + e' + f + // i + e + f' + + // create four clauses + pLits[0] = Abc_Var2Lit(VarI, 1); + pLits[1] = Abc_Var2Lit(VarT, 1^fCompT); + pLits[2] = Abc_Var2Lit(VarF, 0); + if ( fPolarFlip ) + { + if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); + if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] ); + } + RetValue = satoko_add_clause( pSat, pLits, 3 ); + assert( RetValue ); + pLits[0] = Abc_Var2Lit(VarI, 1); + pLits[1] = Abc_Var2Lit(VarT, 0^fCompT); + pLits[2] = Abc_Var2Lit(VarF, 1); + if ( fPolarFlip ) + { + if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); + if ( Gia_Regular(pNodeT)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] ); + } + RetValue = satoko_add_clause( pSat, pLits, 3 ); + assert( RetValue ); + pLits[0] = Abc_Var2Lit(VarI, 0); + pLits[1] = Abc_Var2Lit(VarE, 1^fCompE); + pLits[2] = Abc_Var2Lit(VarF, 0); + if ( fPolarFlip ) + { + if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); + if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] ); + } + RetValue = satoko_add_clause( pSat, pLits, 3 ); + assert( RetValue ); + pLits[0] = Abc_Var2Lit(VarI, 0); + pLits[1] = Abc_Var2Lit(VarE, 0^fCompE); + pLits[2] = Abc_Var2Lit(VarF, 1); + if ( fPolarFlip ) + { + if ( pNodeI->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); + if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] ); + } + RetValue = satoko_add_clause( pSat, pLits, 3 ); + assert( RetValue ); + + // two additional clauses + // t' & e' -> f' + // t & e -> f + + // t + e + f' + // t' + e' + f + + if ( VarT == VarE ) + { +// assert( fCompT == !fCompE ); + return; + } + + pLits[0] = Abc_Var2Lit(VarT, 0^fCompT); + pLits[1] = Abc_Var2Lit(VarE, 0^fCompE); + pLits[2] = Abc_Var2Lit(VarF, 1); + if ( fPolarFlip ) + { + if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); + if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] ); + } + RetValue = satoko_add_clause( pSat, pLits, 3 ); + assert( RetValue ); + pLits[0] = Abc_Var2Lit(VarT, 1^fCompT); + pLits[1] = Abc_Var2Lit(VarE, 1^fCompE); + pLits[2] = Abc_Var2Lit(VarF, 0); + if ( fPolarFlip ) + { + if ( Gia_Regular(pNodeT)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); + if ( Gia_Regular(pNodeE)->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); + if ( pNode->fPhase ) pLits[2] = Abc_LitNot( pLits[2] ); + } + RetValue = satoko_add_clause( pSat, pLits, 3 ); + assert( RetValue ); +} +void Gia_Min2AddClausesSuper( Gia_Man_t * p, Gia_Obj_t * pNode, Vec_Ptr_t * vSuper, satoko_t * pSat ) +{ + int fPolarFlip = 0; + Gia_Obj_t * pFanin; + int * pLits, nLits, RetValue, i; + assert( !Gia_IsComplement(pNode) ); + assert( Gia_ObjIsAnd( pNode ) ); + // create storage for literals + nLits = Vec_PtrSize(vSuper) + 1; + pLits = ABC_ALLOC( int, nLits ); + // suppose AND-gate is A & B = C + // add !A => !C or A + !C + Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i ) + { + pLits[0] = Abc_Var2Lit(Gia_Min2ObjSatId(p, Gia_Regular(pFanin)), Gia_IsComplement(pFanin)); + pLits[1] = Abc_Var2Lit(Gia_Min2ObjSatId(p, pNode), 1); + if ( fPolarFlip ) + { + if ( Gia_Regular(pFanin)->fPhase ) pLits[0] = Abc_LitNot( pLits[0] ); + if ( pNode->fPhase ) pLits[1] = Abc_LitNot( pLits[1] ); + } + RetValue = satoko_add_clause( pSat, pLits, 2 ); + assert( RetValue ); + } + // add A & B => C or !A + !B + C + Vec_PtrForEachEntry( Gia_Obj_t *, vSuper, pFanin, i ) + { + pLits[i] = Abc_Var2Lit(Gia_Min2ObjSatId(p, Gia_Regular(pFanin)), !Gia_IsComplement(pFanin)); + if ( fPolarFlip ) + { + if ( Gia_Regular(pFanin)->fPhase ) pLits[i] = Abc_LitNot( pLits[i] ); + } + } + pLits[nLits-1] = Abc_Var2Lit(Gia_Min2ObjSatId(p, pNode), 0); + if ( fPolarFlip ) + { + if ( pNode->fPhase ) pLits[nLits-1] = Abc_LitNot( pLits[nLits-1] ); + } + RetValue = satoko_add_clause( pSat, pLits, nLits ); + assert( RetValue ); + ABC_FREE( pLits ); +} + +/**Function************************************************************* + + Synopsis [Adds clauses and returns CNF variable of the node.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_Min2CollectSuper_rec( Gia_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes ) +{ + // if the new node is complemented or a PI, another gate begins + if ( Gia_IsComplement(pObj) || Gia_ObjIsCi(pObj) || + (!fFirst && Gia_ObjValue(pObj) > 1) || + (fUseMuxes && pObj->fMark0) ) + { + Vec_PtrPushUnique( vSuper, pObj ); + return; + } + // go through the branches + Gia_Min2CollectSuper_rec( Gia_ObjChild0(pObj), vSuper, 0, fUseMuxes ); + Gia_Min2CollectSuper_rec( Gia_ObjChild1(pObj), vSuper, 0, fUseMuxes ); +} +void Gia_Min2CollectSuper( Gia_Obj_t * pObj, int fUseMuxes, Vec_Ptr_t * vSuper ) +{ + assert( !Gia_IsComplement(pObj) ); + assert( !Gia_ObjIsCi(pObj) ); + Vec_PtrClear( vSuper ); + Gia_Min2CollectSuper_rec( pObj, vSuper, 1, fUseMuxes ); +} +void Gia_Min2ObjAddToFrontier( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vFrontier, satoko_t * pSat, Vec_Int_t * vSatVars ) +{ + assert( !Gia_IsComplement(pObj) ); + assert( !Gia_ObjIsConst0(pObj) ); + if ( Gia_Min2ObjSatId(p, pObj) >= 0 ) + return; + assert( Gia_Min2ObjSatId(p, pObj) == -1 ); + Vec_IntPush( vSatVars, Gia_ObjId(p, pObj) ); + Gia_Min2ObjSetSatId( p, pObj, satoko_add_variable(pSat, 0) ); + if ( Gia_ObjIsAnd(pObj) ) + Vec_PtrPush( vFrontier, pObj ); +} +int Gia_Min2ObjGetCnfVar( Gia_Man2Min_t * p, int iObj ) +{ + Gia_Obj_t * pObj = Gia_ManObj(p->pGia, iObj); + Gia_Obj_t * pNode, * pFanin; + int i, k, fUseMuxes = 1; + if ( Gia_Min2ObjSatId(p->pGia, pObj) >= 0 ) + return Gia_Min2ObjSatId(p->pGia, pObj); + if ( Gia_ObjIsCi(pObj) ) + { + Vec_IntPush( p->vSatVars, iObj ); + return Gia_Min2ObjSetSatId( p->pGia, pObj, satoko_add_variable(p->pSat, 0) ); + } + assert( Gia_ObjIsAnd(pObj) ); + // start the frontier + Vec_PtrClear( p->vFrontier ); + Gia_Min2ObjAddToFrontier( p->pGia, pObj, p->vFrontier, p->pSat, p->vSatVars ); + // explore nodes in the frontier + Vec_PtrForEachEntry( Gia_Obj_t *, p->vFrontier, pNode, i ) + { + assert( Gia_Min2ObjSatId(p->pGia,pNode) >= 0 ); + if ( fUseMuxes && pNode->fMark0 ) + { + Vec_PtrClear( p->vFanins ); + Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin0(pNode) ) ); + Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin0( Gia_ObjFanin1(pNode) ) ); + Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin0(pNode) ) ); + Vec_PtrPushUnique( p->vFanins, Gia_ObjFanin1( Gia_ObjFanin1(pNode) ) ); + Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k ) + Gia_Min2ObjAddToFrontier( p->pGia, Gia_Regular(pFanin), p->vFrontier, p->pSat, p->vSatVars ); + Gia_Min2AddClausesMux( p->pGia, pNode, p->pSat ); + } + else + { + Gia_Min2CollectSuper( pNode, fUseMuxes, p->vFanins ); + Vec_PtrForEachEntry( Gia_Obj_t *, p->vFanins, pFanin, k ) + Gia_Min2ObjAddToFrontier( p->pGia, Gia_Regular(pFanin), p->vFrontier, p->pSat, p->vSatVars ); + Gia_Min2AddClausesSuper( p->pGia, pNode, p->vFanins, p->pSat ); + } + assert( Vec_PtrSize(p->vFanins) > 1 ); + } + return Gia_Min2ObjSatId(p->pGia,pObj); +} + +/**Function************************************************************* + + Synopsis [Returns 0 if the node is not a constant.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_Min2ManSimulate( Gia_Man2Min_t * p ) +{ + word Sim0, Sim1; int n, i, iObj; + p->nSims++; + // add random values to new CIs + Vec_WrdFillExtra( p->vSims, Gia_ManObjNum(p->pGia), 0 ); + for ( i = p->nCisOld; i < Gia_ManCiNum(p->pGia); i++ ) + Vec_WrdWriteEntry( p->vSims, Gia_ManCiIdToId(p->pGia, i), Gia_ManRandomW( 0 ) << 1 ); + p->nCisOld = Gia_ManCiNum(p->pGia); + // simulate internal nodes + for ( n = 0; n < 2; n++ ) + Vec_IntForEachEntry( p->vObjs[n], iObj, i ) + { + Gia_Obj_t * pObj = Gia_ManObj( p->pGia, iObj ); + Sim0 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId0p(p->pGia, pObj) ); + Sim1 = Vec_WrdEntry( p->vSims, Gia_ObjFaninId1p(p->pGia, pObj) ); + Sim0 = Gia_ObjFaninC0(pObj) ? ~Sim0 : Sim0; + Sim1 = Gia_ObjFaninC1(pObj) ? ~Sim1 : Sim1; + Vec_WrdWriteEntry( p->vSims, iObj, Sim0 & Sim1 ); + } + Sim0 = Vec_WrdEntry( p->vSims, Abc_Lit2Var(p->iLits[0]) ); + Sim1 = Vec_WrdEntry( p->vSims, Abc_Lit2Var(p->iLits[1]) ); + Sim0 = Abc_LitIsCompl(p->iLits[0]) ? ~Sim0 : Sim0; + Sim1 = Abc_LitIsCompl(p->iLits[1]) ? ~Sim1 : Sim1; +// assert( (Sim0 & Sim1) != ~0 ); + return (Sim0 & Sim1) == 0; +} + +/**Function************************************************************* + + Synopsis [Internal simulation APIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Gia_Min2SimSetInputBit( Gia_Man2Min_t * p, int iObj, int Bit, int iPattern ) +{ + word * pSim = Vec_WrdEntryP( p->vSims, iObj ); + assert( iPattern > 0 && iPattern < 64 ); + if ( Abc_InfoHasBit( (unsigned*)pSim, iPattern ) != Bit ) + Abc_InfoXorBit( (unsigned*)pSim, iPattern ); +} +int Gia_Min2ManSolve( Gia_Man2Min_t * p ) +{ + int iObj0 = Abc_Lit2Var(p->iLits[0]); + int iObj1 = Abc_Lit2Var(p->iLits[1]); + int n, i, status, iVar0, iVar1, iTemp; + assert( iObj0 > 0 && iObj1 > 0 ); +// Vec_IntForEachEntry( &p->pGia->vCopies, iTemp, i ) +// assert( iTemp == -1 ); + Vec_IntFillExtra( &p->pGia->vCopies, Gia_ManObjNum(p->pGia), -1 ); + Vec_IntClear( p->vSatVars ); + assert( solver_varnum(p->pSat) == 0 ); + iVar0 = Gia_Min2ObjGetCnfVar( p, iObj0 ); + iVar1 = Gia_Min2ObjGetCnfVar( p, iObj1 ); + satoko_assump_push( p->pSat, Abc_Var2Lit(iVar0, Abc_LitIsCompl(p->iLits[0])) ); + satoko_assump_push( p->pSat, Abc_Var2Lit(iVar1, Abc_LitIsCompl(p->iLits[1])) ); + status = satoko_solve( p->pSat ); + satoko_assump_pop( p->pSat ); + satoko_assump_pop( p->pSat ); + if ( status == SATOKO_SAT ) + { + //printf( "Disproved %d %d\n", p->iLits[0], p->iLits[1] ); + assert( Gia_Min2ManSimulate(p) == 1 ); + for ( n = 0; n < 2; n++ ) + Vec_IntForEachEntry( p->vCis[n], iTemp, i ) + Gia_Min2SimSetInputBit( p, iTemp, var_polarity(p->pSat, Gia_Min2ObjSatId(p->pGia, Gia_ManObj(p->pGia, iTemp))) == LIT_TRUE, p->iPattern ); + assert( Gia_Min2ManSimulate(p) == 0 ); + p->iPattern = p->iPattern == 63 ? 1 : p->iPattern + 1; + p->nSatSat++; + } + //printf( "supp %d node %d vars %d\n", + // Vec_IntSize(p->vCis[0]) + Vec_IntSize(p->vCis[1]), + // Vec_IntSize(p->vObjs[0]) + Vec_IntSize(p->vObjs[1]), + // Vec_IntSize(p->vSatVars) ); + satoko_rollback( p->pSat ); + Vec_IntForEachEntry( p->vSatVars, iTemp, i ) + Gia_Min2ObjCleanSatId( p->pGia, Gia_ManObj(p->pGia, iTemp) ); + return status == SATOKO_UNSAT; +} + +/**Function************************************************************* + + Synopsis [Collect nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Gia_Min2ManGatherSupp_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vCis, Vec_Int_t * vObjs ) +{ + int Val0, Val1; + Gia_Obj_t * pObj; + if ( Gia_ObjIsTravIdPreviousId(p, iObj) ) + return 1; + if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) + return 0; + Gia_ObjSetTravIdCurrentId(p, iObj); + pObj = Gia_ManObj( p, iObj ); + if ( Gia_ObjIsCi(pObj) ) + { + Vec_IntPush( vCis, iObj ); + return 0; + } + assert( Gia_ObjIsAnd(pObj) ); + Val0 = Gia_Min2ManGatherSupp_rec( p, Gia_ObjFaninId0(pObj, iObj), vCis, vObjs ); + Val1 = Gia_Min2ManGatherSupp_rec( p, Gia_ObjFaninId1(pObj, iObj), vCis, vObjs ); + Vec_IntPush( vObjs, iObj ); + return Val0 || Val1; +} +int Gia_Min2ManGatherSupp( Gia_Man2Min_t * p ) +{ + int n, Overlap = 0; + p->nSupps++; + Gia_ManIncrementTravId( p->pGia ); + for ( n = 0; n < 2; n++ ) + { + Vec_IntClear( p->vCis[n] ); + Vec_IntClear( p->vObjs[n] ); + Gia_ManIncrementTravId( p->pGia ); + Overlap = Gia_Min2ManGatherSupp_rec( p->pGia, Abc_Lit2Var(p->iLits[n]), p->vCis[n], p->vObjs[n] ); + assert( n || !Overlap ); + } + return Overlap; +} + +/**Function************************************************************* + + Synopsis [Takes a literal and returns a support-minized literal.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_Man2SupportAnd( Gia_Man2Min_t * p, int iLit0, int iLit1 ) +{ + p->nCalls++; + //return Gia_ManHashAnd( p->pGia, iLit0, iLit1 ); + p->iLits[0] = iLit0; + p->iLits[1] = iLit1; + if ( iLit0 < 2 || iLit1 < 2 || Abc_Lit2Var(iLit0) == Abc_Lit2Var(iLit1) || Gia_ManHashLookupInt(p->pGia, iLit0, iLit1) || + !Gia_Min2ManGatherSupp(p) || !Gia_Min2ManSimulate(p) || !Gia_Min2ManSolve(p) ) + return Gia_ManHashAnd( p->pGia, iLit0, iLit1 ); + //printf( "%d %d\n", iLit0, iLit1 ); + p->nSatUnsat++; + return 0; +} + +/**Function************************************************************* + + Synopsis [Testbench.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_Man2SupportAndTest( Gia_Man_t * pGia ) +{ + Gia_Man2Min_t * pMan; + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i; + Gia_ManRandomW( 1 ); + Gia_ManFillValue( pGia ); + pNew = Gia_ManStart( Gia_ManObjNum(pGia) ); + pNew->pName = Abc_UtilStrsav( pGia->pName ); + pNew->pSpec = Abc_UtilStrsav( pGia->pSpec ); + Gia_ManHashAlloc( pNew ); + Gia_ManConst0(pGia)->Value = 0; + pMan = Gia_Man2SuppStart( pNew ); + Gia_ManForEachObj1( pGia, pObj, i ) + { + if ( Gia_ObjIsAnd(pObj) ) + { +// pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + pObj->Value = Gia_Man2SupportAnd( pMan, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } + else if ( Gia_ObjIsCi(pObj) ) + pObj->Value = Gia_ManAppendCi( pNew ); + else if ( Gia_ObjIsCo(pObj) ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + else assert( 0 ); + + //if ( i % 10000 == 0 ) + // printf( "%d\n", i ); + } + Gia_Man2SuppStop( pMan ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia) ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 1f4c4c07..7ffd6bc5 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -76,6 +76,7 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaStg.c \ src/aig/gia/giaStr.c \ src/aig/gia/giaSupMin.c \ + src/aig/gia/giaSupp.c \ src/aig/gia/giaSweep.c \ src/aig/gia/giaSweeper.c \ src/aig/gia/giaSwitch.c \ diff --git a/src/aig/miniaig/miniaig.h b/src/aig/miniaig/miniaig.h index 6843648e..217fea51 100644 --- a/src/aig/miniaig/miniaig.h +++ b/src/aig/miniaig/miniaig.h @@ -171,9 +171,9 @@ static void Mini_AigDump( Mini_Aig_t * p, char * pFileName ) printf( "Cannot open file for writing \"%s\".\n", pFileName ); return; } - RetValue = fwrite( &p->nSize, sizeof(int), 1, pFile ); - RetValue = fwrite( &p->nRegs, sizeof(int), 1, pFile ); - RetValue = fwrite( p->pArray, sizeof(int), p->nSize, pFile ); + RetValue = (int)fwrite( &p->nSize, sizeof(int), 1, pFile ); + RetValue = (int)fwrite( &p->nRegs, sizeof(int), 1, pFile ); + RetValue = (int)fwrite( p->pArray, sizeof(int), p->nSize, pFile ); fclose( pFile ); } static Mini_Aig_t * Mini_AigLoad( char * pFileName ) @@ -187,12 +187,12 @@ static Mini_Aig_t * Mini_AigLoad( char * pFileName ) printf( "Cannot open file for reading \"%s\".\n", pFileName ); return NULL; } - RetValue = fread( &nSize, sizeof(int), 1, pFile ); + RetValue = (int)fread( &nSize, sizeof(int), 1, pFile ); p = MINI_AIG_CALLOC( Mini_Aig_t, 1 ); p->nSize = p->nCap = nSize; p->pArray = MINI_AIG_ALLOC( int, p->nCap ); - RetValue = fread( &p->nRegs, sizeof(int), 1, pFile ); - RetValue = fread( p->pArray, sizeof(int), p->nSize, pFile ); + RetValue = (int)fread( &p->nRegs, sizeof(int), 1, pFile ); + RetValue = (int)fread( p->pArray, sizeof(int), p->nSize, pFile ); fclose( pFile ); return p; } diff --git a/src/aig/miniaig/minilut.h b/src/aig/miniaig/minilut.h index 5040f4b7..e84428d4 100644 --- a/src/aig/miniaig/minilut.h +++ b/src/aig/miniaig/minilut.h @@ -191,11 +191,11 @@ static void Mini_LutDump( Mini_Lut_t * p, char * pFileName ) printf( "Cannot open file for writing \"%s\".\n", pFileName ); return; } - RetValue = fwrite( &p->nSize, sizeof(int), 1, pFile ); - RetValue = fwrite( &p->nRegs, sizeof(int), 1, pFile ); - RetValue = fwrite( &p->LutSize, sizeof(int), 1, pFile ); - RetValue = fwrite( p->pArray, sizeof(int), p->nSize * p->LutSize, pFile ); - RetValue = fwrite( p->pTruths, sizeof(int), p->nSize * Mini_LutWordNum(p->LutSize), pFile ); + RetValue = (int)fwrite( &p->nSize, sizeof(int), 1, pFile ); + RetValue = (int)fwrite( &p->nRegs, sizeof(int), 1, pFile ); + RetValue = (int)fwrite( &p->LutSize, sizeof(int), 1, pFile ); + RetValue = (int)fwrite( p->pArray, sizeof(int), p->nSize * p->LutSize, pFile ); + RetValue = (int)fwrite( p->pTruths, sizeof(int), p->nSize * Mini_LutWordNum(p->LutSize), pFile ); fclose( pFile ); } static Mini_Lut_t * Mini_LutLoad( char * pFileName ) @@ -209,15 +209,15 @@ static Mini_Lut_t * Mini_LutLoad( char * pFileName ) printf( "Cannot open file for reading \"%s\".\n", pFileName ); return NULL; } - RetValue = fread( &nSize, sizeof(int), 1, pFile ); + RetValue = (int)fread( &nSize, sizeof(int), 1, pFile ); p = MINI_LUT_CALLOC( Mini_Lut_t, 1 ); p->nSize = p->nCap = nSize; - RetValue = fread( &p->nRegs, sizeof(int), 1, pFile ); - RetValue = fread( &p->LutSize, sizeof(int), 1, pFile ); + RetValue = (int)fread( &p->nRegs, sizeof(int), 1, pFile ); + RetValue = (int)fread( &p->LutSize, sizeof(int), 1, pFile ); p->pArray = MINI_LUT_ALLOC( int, p->nCap * p->LutSize ); p->pTruths = MINI_LUT_ALLOC( unsigned, p->nCap * Mini_LutWordNum(p->LutSize) ); - RetValue = fread( p->pArray, sizeof(int), p->nCap * p->LutSize, pFile ); - RetValue = fread( p->pTruths, sizeof(int), p->nCap * Mini_LutWordNum(p->LutSize), pFile ); + RetValue = (int)fread( p->pArray, sizeof(int), p->nCap * p->LutSize, pFile ); + RetValue = (int)fread( p->pTruths, sizeof(int), p->nCap * Mini_LutWordNum(p->LutSize), pFile ); fclose( pFile ); return p; } diff --git a/src/aig/miniaig/ndr.h b/src/aig/miniaig/ndr.h index 4450d22c..9e85c870 100644 --- a/src/aig/miniaig/ndr.h +++ b/src/aig/miniaig/ndr.h @@ -220,7 +220,7 @@ static inline void Ndr_DataPushString( Ndr_Data_t * p, int Type, char * pFunc ) { if ( !pFunc ) return; - Ndr_DataPushArray( p, Type, (strlen(pFunc) + 4) / 4, (int *)pFunc ); + Ndr_DataPushArray( p, Type, ((int)strlen(pFunc) + 4) / 4, (int *)pFunc ); } //////////////////////////////////////////////////////////////////////// @@ -457,8 +457,8 @@ static inline void * Ndr_ModuleRead( char * pFileName ) p->nSize = p->nCap = nFileSize / 5; p->pHead = malloc( p->nCap ); p->pBody = malloc( p->nCap * 4 ); - RetValue = fread( p->pBody, 4, p->nCap, pFile ); - RetValue = fread( p->pHead, 1, p->nCap, pFile ); + RetValue = (int)fread( p->pBody, 4, p->nCap, pFile ); + RetValue = (int)fread( p->pHead, 1, p->nCap, pFile ); assert( p->nSize == (int)p->pBody[0] ); fclose( pFile ); return p; @@ -468,8 +468,8 @@ static inline void Ndr_ModuleWrite( char * pFileName, void * pModule ) Ndr_Data_t * p = (Ndr_Data_t *)pModule; int RetValue; FILE * pFile = fopen( pFileName, "wb" ); if ( pFile == NULL ) { printf( "Cannot open file \"%s\" for writing.\n", pFileName ); return; } - RetValue = fwrite( p->pBody, 4, p->pBody[0], pFile ); - RetValue = fwrite( p->pHead, 1, p->pBody[0], pFile ); + RetValue = (int)fwrite( p->pBody, 4, p->pBody[0], pFile ); + RetValue = (int)fwrite( p->pHead, 1, p->pBody[0], pFile ); fclose( pFile ); } diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c index dc6cd3b3..6b67d82a 100644 --- a/src/base/abc/abcUtil.c +++ b/src/base/abc/abcUtil.c @@ -3109,7 +3109,9 @@ int Abc_GateToType( Abc_Obj_t * pObj ) if ( !strncmp(pGateName, "or", 2) ) return ABC_OPER_BIT_OR; if ( !strncmp(pGateName, "nor", 3) ) return ABC_OPER_BIT_NOR; if ( !strncmp(pGateName, "xor", 3) ) return ABC_OPER_BIT_XOR; - if ( !strncmp(pGateName, "nxor", 4) ) return ABC_OPER_BIT_NXOR; + if ( !strncmp(pGateName, "xnor", 4) ) return ABC_OPER_BIT_NXOR; + if ( !strncmp(pGateName, "zero", 4) ) return ABC_OPER_CONST_F; + if ( !strncmp(pGateName, "one", 3) ) return ABC_OPER_CONST_T; assert( 0 ); return -1; } @@ -3141,6 +3143,81 @@ Vec_Wec_t * Abc_SopSynthesize( Vec_Ptr_t * vSops ) return vRes; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_NtkClpOneGia_rec( Gia_Man_t * pNew, Abc_Obj_t * pNode ) +{ + int iLit0, iLit1; + if ( Abc_NodeIsTravIdCurrent(pNode) || Abc_ObjFaninNum(pNode) == 0 || Abc_ObjIsCi(pNode) ) + return pNode->iTemp; + assert( Abc_ObjIsNode( pNode ) ); + Abc_NodeSetTravIdCurrent( pNode ); + iLit0 = Abc_NtkClpOneGia_rec( pNew, Abc_ObjFanin0(pNode) ); + iLit1 = Abc_NtkClpOneGia_rec( pNew, Abc_ObjFanin1(pNode) ); + iLit0 = Abc_LitNotCond( iLit0, Abc_ObjFaninC0(pNode) ); + iLit1 = Abc_LitNotCond( iLit1, Abc_ObjFaninC1(pNode) ); + return (pNode->iTemp = Gia_ManHashAnd(pNew, iLit0, iLit1)); +} +Gia_Man_t * Abc_NtkStrashToGia( Abc_Ntk_t * pNtk ) +{ + int i, iLit; + Abc_Obj_t * pNode; + Gia_Man_t * pNew, * pTemp; + assert( Abc_NtkIsStrash(pNtk) ); + Abc_NtkForEachObj( pNtk, pNode, i ) + pNode->iTemp = -1; + // start new manager + pNew = Gia_ManStart( Abc_NtkObjNum(pNtk) ); + pNew->pName = Abc_UtilStrsav( pNtk->pName ); + pNew->pSpec = Abc_UtilStrsav( pNtk->pSpec ); + Gia_ManHashStart( pNew ); + // primary inputs + Abc_AigConst1(pNtk)->iTemp = 1; + Abc_NtkForEachCi( pNtk, pNode, i ) + pNode->iTemp = Gia_ManAppendCi(pNew); + // create the first cone + Abc_NtkIncrementTravId( pNtk ); + Abc_NtkForEachCo( pNtk, pNode, i ) + { + iLit = Abc_NtkClpOneGia_rec( pNew, Abc_ObjFanin0(pNode) ); + iLit = Abc_LitNotCond( iLit, Abc_ObjFaninC0(pNode) ); + Gia_ManAppendCo( pNew, iLit ); + } + // perform cleanup + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} +Gia_Man_t * Abc_SopSynthesizeOne( Vec_Ptr_t * vSops ) +{ + Abc_Ntk_t * pNtkNew, * pNtk; + char * pSop = (char *)Vec_PtrEntry(vSops, 0); + assert( Vec_PtrSize(vSops) == 1 ); + if ( strlen(pSop) == 3 ) + { + Gia_Man_t * pNew = Gia_ManStart( 1 ); + pNew->pName = Abc_UtilStrsav( "top" ); + //Gia_ManAppendCi( pNew ); + assert( pSop[1] == '0' || pSop[1] == '1' ); + Gia_ManAppendCo( pNew, pSop[1] == '1' ); + return pNew; + } + pNtk = Abc_NtkCreateFromSops( "top", vSops ); + Abc_FrameReplaceCurrentNetwork( Abc_FrameReadGlobalFrame(), pNtk ); + Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), "fx; strash; dc2" ); + pNtkNew = Abc_FrameReadNtk( Abc_FrameReadGlobalFrame() ); + return Abc_NtkStrashToGia( pNtkNew ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index f9f2f2e0..7055bf59 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -124,6 +124,7 @@ static int Abc_CommandMfs ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandMfs2 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMfs3 ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandMfse ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandLogicPush ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTrace ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandGlitch ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandSpeedup ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -781,6 +782,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "mfs2", Abc_CommandMfs2, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "mfs3", Abc_CommandMfs3, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "mfse", Abc_CommandMfse, 1 ); + Cmd_CommandAdd( pAbc, "Synthesis", "logicpush", Abc_CommandLogicPush, 1 ); Cmd_CommandAdd( pAbc, "Synthesis", "trace", Abc_CommandTrace, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "glitch", Abc_CommandGlitch, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "speedup", Abc_CommandSpeedup, 1 ); @@ -4151,7 +4153,7 @@ int Abc_CommandFastExtract( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Empty network.\n" ); return 1; } - if ( Abc_NtkNodeNum(pNtk) == 0 ) + if ( Abc_NtkNodeNum(pNtk) == 0 || Abc_NtkPiNum(pNtk) == 0 ) { Abc_Print( -1, "The network does not have internal nodes.\n" ); return 1; @@ -5807,6 +5809,74 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandLogicPush( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Abc_Ntk_t * Abc_NtkOptPush( Abc_Ntk_t * pNtk, int nLutSize, int fVerbose ); + Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); + Abc_Ntk_t * pNtkRes; + int nLutSize = 4; + int fVerbose = 0; + int c; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Kvh" ) ) != EOF ) + { + switch ( c ) + { + case 'K': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-K\" should be followed by a positive integer.\n" ); + goto usage; + } + nLutSize = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nLutSize < 0 ) + goto usage; + break; + case 'v': + fVerbose ^= 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; + } + nLutSize = Abc_MaxInt( nLutSize, Abc_NtkGetFaninMax(pNtk) ); + Abc_NtkToSop( pNtk, -1, ABC_INFINITY ); + pNtkRes = Abc_NtkOptPush( pNtk, nLutSize, fVerbose ); + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + return 0; +usage: + Abc_Print( -2, "usage: logicpush [-K num] [-vh]\n" ); + Abc_Print( -2, "\t performs logic pushing to reduce structural bias\n" ); + Abc_Print( -2, "\t-K <num> : the LUT size used in the mapping [default = %d]\n", nLutSize ); + Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* @@ -18315,7 +18385,7 @@ int Abc_CommandDsdFilter( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( fInvMarks ) If_DsdManInvertMarks( pDsd, fVerbose ); #ifdef ABC_USE_CUDD - else + else if ( nLimit == 0 ) Id_DsdManTuneThresh( pDsd, fUnate, fThresh, fThreshHeuristic, fVerbose ); #endif return 0; diff --git a/src/base/acb/acb.h b/src/base/acb/acb.h index 7c228acb..baecd161 100644 --- a/src/base/acb/acb.h +++ b/src/base/acb/acb.h @@ -256,7 +256,8 @@ static inline int * Acb_ObjFanins( Acb_Ntk_t * p, int i ) static inline int Acb_ObjFanin( Acb_Ntk_t * p, int i, int k ) { return Acb_ObjFanins(p, i)[k+1]; } static inline int Acb_ObjFaninNum( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[0]; } static inline int Acb_ObjFanoutNum( Acb_Ntk_t * p, int i ) { return Vec_IntSize( Vec_WecEntry(&p->vFanouts, i) ); } -static inline Vec_Int_t * Acb_ObjFanoutVec( Acb_Ntk_t * p, int i ) { return Vec_WecEntry( &p->vFanouts, i ); } +static inline Vec_Int_t * Acb_ObjFanoutVec( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_WecEntry( &p->vFanouts, i ); } +static inline int Acb_ObjFanout( Acb_Ntk_t * p, int i, int k ) { return Vec_IntEntry( Acb_ObjFanoutVec(p, i), k ); } static inline int Acb_ObjFanin0( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[1]; } static inline int Acb_ObjCioId( Acb_Ntk_t * p, int i ) { return Acb_ObjFanins(p, i)[2]; } @@ -276,7 +277,6 @@ static inline int Acb_ObjLevelR( Acb_Ntk_t * p, int i ) static inline int Acb_ObjPathD( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vPathD, i); } static inline int Acb_ObjPathR( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_IntEntry(&p->vPathR, i); } static inline float Acb_ObjCounts( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_FltEntry(&p->vCounts, i); } -static inline Vec_Int_t * Acb_ObjFanout( Acb_Ntk_t * p, int i ) { assert(i>0); return Vec_WecEntry(&p->vFanouts, i); } static inline Vec_Str_t * Acb_ObjCnfs( Acb_Ntk_t * p, int i ) { assert(i>0); return (Vec_Str_t *)Vec_WecEntry(&p->vCnfs, i); } static inline void Acb_ObjSetCopy( Acb_Ntk_t * p, int i, int x ) { assert(Acb_ObjCopy(p, i) == -1); Vec_IntWriteEntry( &p->vObjCopy, i, x ); } @@ -361,6 +361,8 @@ static inline void Acb_NtkIncTravId( Acb_Ntk_t * p ) for ( i = Vec_StrSize(&p->vObjType)-1; i > 0; i-- ) if ( !Acb_ObjType(p, i) ) {} else #define Acb_NtkForEachNode( p, i ) \ for ( i = 1; i < Vec_StrSize(&p->vObjType); i++ ) if ( !Acb_ObjType(p, i) || Acb_ObjIsCio(p, i) ) {} else +#define Acb_NtkForEachNodeSupp( p, i, nSuppSize ) \ + for ( i = 1; i < Vec_StrSize(&p->vObjType); i++ ) if ( !Acb_ObjType(p, i) || Acb_ObjIsCio(p, i) || Acb_ObjFaninNum(p, i) != nSuppSize ) {} else #define Acb_NtkForEachNodeReverse( p, i ) \ for ( i = Vec_StrSize(&p->vObjType)-1; i > 0; i-- ) if ( !Acb_ObjType(p, i) || Acb_ObjIsCio(p, i) ) {} else #define Acb_NtkForEachObjType( p, Type, i ) \ @@ -403,12 +405,35 @@ static inline int Acb_ObjFonNum( Acb_Ntk_t * p, int iObj ) Count++; return Count; } +static inline int Acb_ObjWhatFanin( Acb_Ntk_t * p, int iObj, int iFaninGiven ) +{ + int k, iFanin, * pFanins; + Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k ) + if ( iFanin == iFaninGiven ) + return k; + return -1; +} static inline void Acb_ObjAddFanin( Acb_Ntk_t * p, int iObj, int iFanin ) { int * pFanins = Acb_ObjFanins( p, iObj ); assert( pFanins[ 1 + pFanins[0] ] == -1 ); pFanins[ 1 + pFanins[0]++ ] = iFanin; } +static inline void Acb_ObjDeleteFaninIndex( Acb_Ntk_t * p, int iObj, int iFaninIndex ) +{ + int i, * pFanins = Acb_ObjFanins( p, iObj ); + pFanins[0]--; + for ( i = iFaninIndex; i < pFanins[0]; i++ ) + pFanins[ 1 + i ] = pFanins[ 2 + i ]; + pFanins[ 1 + pFanins[0] ] = -1; +} +static inline void Acb_ObjDeleteFanin( Acb_Ntk_t * p, int iObj, int iFanin ) +{ + int * pFanins = Acb_ObjFanins( p, iObj ); + int iFaninIndex = Acb_ObjWhatFanin( p, iObj, iFanin ); + assert( pFanins[ 1 + iFaninIndex ] == iFanin ); + Acb_ObjDeleteFaninIndex( p, iObj, iFaninIndex ); +} static inline void Acb_ObjAddFanins( Acb_Ntk_t * p, int iObj, Vec_Int_t * vFanins ) { int i, iFanin; @@ -495,12 +520,23 @@ static inline void Acb_ObjDelete( Acb_Ntk_t * p, int iObj ) Acb_ObjForEachFon( p, iObj, i ) Acb_ObjCleanType( p, i ); } +static inline void Acb_ObjAddFaninFanoutOne( Acb_Ntk_t * p, int iObj, int iFanin ) +{ + Vec_IntPush( Vec_WecEntry(&p->vFanouts, iFanin), iObj ); + Acb_ObjAddFanin( p, iObj, iFanin ); +} static inline void Acb_ObjAddFaninFanout( Acb_Ntk_t * p, int iObj ) { int k, iFanin, * pFanins; Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k ) Vec_IntPush( Vec_WecEntry(&p->vFanouts, iFanin), iObj ); } +static inline void Acb_ObjRemoveFaninFanoutOne( Acb_Ntk_t * p, int iObj, int iFanin ) +{ + int RetValue = Vec_IntRemove( Vec_WecEntry(&p->vFanouts, iFanin), iObj ); + assert( RetValue ); + Acb_ObjDeleteFanin( p, iObj, iFanin ); +} static inline void Acb_ObjRemoveFaninFanout( Acb_Ntk_t * p, int iObj ) { int k, iFanin, * pFanins; @@ -510,6 +546,19 @@ static inline void Acb_ObjRemoveFaninFanout( Acb_Ntk_t * p, int iObj ) assert( RetValue ); } } +static inline void Acb_ObjPatchFanin( Acb_Ntk_t * p, int iObj, int iFanin, int iFaninNew ) +{ + int i, RetValue, * pFanins = Acb_ObjFanins( p, iObj ); + assert( iFanin != iFaninNew ); + for ( i = 0; i < pFanins[0]; i++ ) + if ( pFanins[ 1 + i ] == iFanin ) + pFanins[ 1 + i ] = iFaninNew; + if ( !Acb_NtkHasObjFanout(p) ) + return; + RetValue = Vec_IntRemove( Vec_WecEntry(&p->vFanouts, iFanin), iObj ); + assert( RetValue ); + Vec_IntPush( Vec_WecEntry(&p->vFanouts, iFaninNew), iObj ); +} static inline void Acb_NtkCreateFanout( Acb_Ntk_t * p ) { int iObj; diff --git a/src/base/acb/acbAbc.c b/src/base/acb/acbAbc.c index 2b07a202..7b215a56 100644 --- a/src/base/acb/acbAbc.c +++ b/src/base/acb/acbAbc.c @@ -271,6 +271,28 @@ Abc_Ntk_t * Abc_NtkOptMfse( Abc_Ntk_t * pNtk, Acb_Par_t * pPars ) return pNtkNew; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Abc_Ntk_t * Abc_NtkOptPush( Abc_Ntk_t * pNtk, int nLutSize, int fVerbose ) +{ + extern void Acb_NtkPushLogic( Acb_Ntk_t * p, int nLutSize, int fVerbose ); + Abc_Ntk_t * pNtkNew; + Acb_Ntk_t * p = Acb_NtkFromAbc( pNtk ); + Acb_NtkPushLogic( p, nLutSize, fVerbose ); + pNtkNew = Acb_NtkToAbc( pNtk, p ); + Acb_ManFree( p->pDesign ); + return pNtkNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/acb/acbMfs.c b/src/base/acb/acbMfs.c index d8c6fb16..9fce00f8 100644 --- a/src/base/acb/acbMfs.c +++ b/src/base/acb/acbMfs.c @@ -1576,7 +1576,7 @@ cleanup: void Acb_NtkOpt( Acb_Ntk_t * pNtk, Acb_Par_t * pPars ) { Acb_Mfs_t * pMan = Acb_MfsStart( pNtk, pPars ); - //if ( pPars->fVerbose ) + if ( pPars->fVerbose ) printf( "%s-optimization parameters: TfiLev(I) = %d TfoLev(O) = %d WinMax(W) = %d LutSize = %d\n", pMan->pPars->fArea ? "Area" : "Delay", pMan->pPars->nTfiLevMax, pMan->pPars->nTfoLevMax, pMan->pPars->nWinNodeMax, pMan->pPars->nLutSize ); Acb_NtkCreateFanout( pNtk ); // fanout data structure @@ -1592,8 +1592,8 @@ void Acb_NtkOpt( Acb_Ntk_t * pNtk, Acb_Par_t * pPars ) if ( iObj < nNodes && !Vec_BitEntry(vVisited, iObj) && Acb_NtkObjMffcEstimate(pNtk, iObj) >= n ) { pMan->nNodes++; - if ( iObj != 103 ) - continue; + //if ( iObj != 103 ) + // continue; //Acb_NtkOptNode( pMan, iObj ); while ( (RetValue = Acb_NtkOptNode(pMan, iObj)) && Acb_ObjFaninNum(pNtk, iObj) ); Vec_BitWriteEntry( vVisited, iObj, 1 ); @@ -1609,13 +1609,13 @@ void Acb_NtkOpt( Acb_Ntk_t * pNtk, Acb_Par_t * pPars ) int iObj = Vec_QuePop(pNtk->vQue); if ( !Acb_ObjType(pNtk, iObj) ) continue; - if ( iObj != 103 ) - continue; + //if ( iObj != 103 ) + // continue; //printf( "Trying node %4d (%4d) ", iObj, Value ); Acb_NtkOptNode( pMan, iObj ); } } - //if ( pPars->fVerbose ) + if ( pPars->fVerbose ) { pMan->timeTotal = Abc_Clock() - pMan->timeTotal; printf( "Node = %d Win = %d (Ave = %d) DivAve = %d Change = %d C = %d N1 = %d N2 = %d N3 = %d Over = %d Str = %d 2Node = %d.\n", diff --git a/src/base/acb/acbPush.c b/src/base/acb/acbPush.c new file mode 100644 index 00000000..01de31db --- /dev/null +++ b/src/base/acb/acbPush.c @@ -0,0 +1,372 @@ +/**CFile**************************************************************** + + FileName [acbPush.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Hierarchical word-level netlist.] + + Synopsis [Implementation of logic pushing.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - July 21, 2015.] + + Revision [$Id: acbPush.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "acb.h" +#include "misc/util/utilTruth.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Pushing logic to the fanout.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_ObjPushToFanout( Acb_Ntk_t * p, int iObj, int iFaninIndex, int iFanout ) +{ + word c0, uTruthObjNew = 0, uTruthObj = Acb_ObjTruth( p, iObj ), Gate; + word c1, uTruthFanNew = 0, uTruthFan = Acb_ObjTruth( p, iFanout ); + int DecType = Abc_TtCheckOutAnd( uTruthObj, iFaninIndex, &uTruthObjNew ); + int iFanin = Acb_ObjFanin( p, iObj, iFaninIndex ); + int iFanoutObjIndex = Acb_ObjWhatFanin( p, iFanout, iObj ); + int iFanoutFaninIndex = Acb_ObjWhatFanin( p, iFanout, iFanin ); + if ( iFanoutFaninIndex == -1 ) + iFanoutFaninIndex = Acb_ObjFaninNum(p, iFanout); + assert( !Acb_ObjIsCio(p, iObj) ); + assert( !Acb_ObjIsCio(p, iFanout) ); + assert( iFanoutFaninIndex >= 0 ); + assert( iFaninIndex < Acb_ObjFaninNum(p, iObj) ); + assert( Acb_ObjFanoutNum(p, iObj) == 1 ); + // compute new function of the fanout + c0 = Abc_Tt6Cofactor0( uTruthFan, iFanoutObjIndex ); + c1 = Abc_Tt6Cofactor1( uTruthFan, iFanoutObjIndex ); + if ( DecType == 0 ) // F = i * G + Gate = s_Truths6[iFanoutFaninIndex] & s_Truths6[iFanoutObjIndex]; + else if ( DecType == 1 ) // F = ~i * G + Gate = ~s_Truths6[iFanoutFaninIndex] & s_Truths6[iFanoutObjIndex]; + else if ( DecType == 2 ) // F = ~i + G + Gate = ~s_Truths6[iFanoutFaninIndex] | s_Truths6[iFanoutObjIndex]; + else if ( DecType == 3 ) // F = i + G + Gate = s_Truths6[iFanoutFaninIndex] | s_Truths6[iFanoutObjIndex]; + else if ( DecType == 4 ) // F = i # G + Gate = s_Truths6[iFanoutFaninIndex] ^ s_Truths6[iFanoutObjIndex]; + else assert( 0 ); + uTruthFanNew = (~Gate & c0) | (Gate & c1); + // update functions + Vec_WrdWriteEntry( &p->vObjTruth, iObj, Abc_Tt6RemoveVar(uTruthObjNew, iFaninIndex) ); + Vec_WrdWriteEntry( &p->vObjTruth, iFanout, uTruthFanNew ); + // update fanins + Acb_ObjRemoveFaninFanoutOne( p, iObj, iFanin ); + if ( iFanoutFaninIndex == Acb_ObjFaninNum(p, iFanout) ) // adding new + Acb_ObjAddFaninFanoutOne( p, iFanout, iFanin ); +} + +/**Function************************************************************* + + Synopsis [Pushing logic to the fanin.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_ObjPushToFanin( Acb_Ntk_t * p, int iObj, int iFaninIndex2, int iFanin ) +{ + word uTruthObjNew = 0, uTruthObj = Acb_ObjTruth( p, iObj ); + word uTruthFanNew = 0, uTruthFan = Acb_ObjTruth( p, iFanin ); + int iFaninIndex = Acb_ObjWhatFanin( p, iObj, iFanin ); + int DecType = Abc_TtCheckDsdAnd( uTruthObj, iFaninIndex, iFaninIndex2, &uTruthObjNew ); + int iFanin2 = Acb_ObjFanin( p, iObj, iFaninIndex2 ); + int iFaninFaninIndex = Acb_ObjWhatFanin( p, iFanin, iFanin2 ); + if ( iFaninFaninIndex == -1 ) + iFaninFaninIndex = Acb_ObjFaninNum(p, iFanin); + assert( !Acb_ObjIsCio(p, iObj) ); + assert( !Acb_ObjIsCio(p, iFanin) ); + assert( iFaninIndex < Acb_ObjFaninNum(p, iObj) ); + assert( iFaninIndex2 < Acb_ObjFaninNum(p, iObj) ); + assert( iFaninIndex != iFaninIndex2 ); + assert( Acb_ObjFanoutNum(p, iFanin) == 1 ); + // compute new function of the fanout + if ( DecType == 0 ) // i * j + uTruthFanNew = uTruthFan & s_Truths6[iFaninFaninIndex]; + else if ( DecType == 1 ) // i * !j + uTruthFanNew = ~uTruthFan & s_Truths6[iFaninFaninIndex]; + else if ( DecType == 2 ) // !i * j + uTruthFanNew = uTruthFan & ~s_Truths6[iFaninFaninIndex]; + else if ( DecType == 3 ) // !i * !j + uTruthFanNew = ~uTruthFan & ~s_Truths6[iFaninFaninIndex]; + else if ( DecType == 4 ) // i # j + uTruthFanNew = uTruthFan ^ s_Truths6[iFaninFaninIndex]; + else assert( 0 ); + // update functions + Vec_WrdWriteEntry( &p->vObjTruth, iObj, Abc_Tt6RemoveVar(uTruthObjNew, iFaninIndex2) ); + Vec_WrdWriteEntry( &p->vObjTruth, iFanin, uTruthFanNew ); + // update fanins + Acb_ObjRemoveFaninFanoutOne( p, iObj, iFanin2 ); + if ( iFaninFaninIndex == Acb_ObjFaninNum(p, iFanin) ) // adding new + Acb_ObjAddFaninFanoutOne( p, iFanin, iFanin2 ); +} + +/**Function************************************************************* + + Synopsis [Removing constants, buffers, duplicated fanins.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Acb_ObjFindNodeFanout( Acb_Ntk_t * p, int iObj ) +{ + int i, iFanout; + Acb_ObjForEachFanout( p, iObj, iFanout, i ) + if ( !Acb_ObjIsCio(p, iFanout) ) + return iFanout; + return -1; +} +int Acb_ObjSuppMin_int( Acb_Ntk_t * p, int iObj ) +{ + int k, iFanin, * pFanins; + word uTruth = Acb_ObjTruth( p, iObj ); + Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k ) + { + if ( Abc_Tt6HasVar(uTruth, k) ) + continue; + Acb_ObjDeleteFaninIndex( p, iObj, k ); + Vec_IntRemove( Vec_WecEntry(&p->vFanouts, iFanin), iObj ); + Vec_WrdWriteEntry( &p->vObjTruth, iObj, Abc_Tt6RemoveVar(uTruth, k) ); + return 1; + } + return 0; +} +void Acb_ObjSuppMin( Acb_Ntk_t * p, int iObj ) +{ + while ( Acb_ObjSuppMin_int(p, iObj) ); +} +void Acb_ObjRemoveDup( Acb_Ntk_t * p, int iObj, int i, int j ) +{ + word c00, c11, uTruthNew, uTruth = Acb_ObjTruth( p, iObj ); + assert( !Acb_ObjIsCio(p, iObj) ); + assert( Acb_ObjFanin(p, iObj, i) == Acb_ObjFanin(p, iObj, j) ); + c00 = Abc_Tt6Cofactor0( Abc_Tt6Cofactor0(uTruth, i), j ); + c11 = Abc_Tt6Cofactor1( Abc_Tt6Cofactor1(uTruth, i), j ); + uTruthNew = (~s_Truths6[i] & c00) | (s_Truths6[i] & c11); + Vec_WrdWriteEntry( &p->vObjTruth, iObj, Abc_Tt6RemoveVar(uTruthNew, j) ); + Acb_ObjDeleteFaninIndex( p, iObj, j ); + Vec_IntRemove( Vec_WecEntry(&p->vFanouts, iObj), Acb_ObjFanin(p, iObj, j) ); + Acb_ObjSuppMin( p, iObj ); +} +int Acb_ObjRemoveDupFanins_int( Acb_Ntk_t * p, int iObj ) +{ + int i, k, * pFanins = Acb_ObjFanins( p, iObj ); + for ( i = 0; i < pFanins[0]; i++ ) + for ( k = i+1; k < pFanins[0]; k++ ) + { + if ( pFanins[1+i] != pFanins[1+k] ) + continue; + Acb_ObjRemoveDup( p, iObj, i, k ); + return 1; + } + return 0; +} +void Acb_ObjRemoveDupFanins( Acb_Ntk_t * p, int iObj ) +{ + assert( !Acb_ObjIsCio(p, iObj) ); + while ( Acb_ObjRemoveDupFanins_int(p, iObj) ); +} +void Acb_ObjRemoveConst( Acb_Ntk_t * p, int iObj ) +{ + int iFanout; + word uTruth = Acb_ObjTruth( p, iObj ); + assert( !Acb_ObjIsCio(p, iObj) ); + assert( Acb_ObjFaninNum(p, iObj) == 0 ); + assert( uTruth == 0 || ~uTruth == 0 ); + while ( (iFanout = Acb_ObjFindNodeFanout(p, iObj)) >= 0 ) + { + int iObjIndex = Acb_ObjWhatFanin( p, iFanout, iObj ); + word uTruthF = Acb_ObjTruth( p, iFanout ); + Acb_ObjRemoveFaninFanoutOne( p, iFanout, iObj ); + uTruthF = (uTruth & 1) ? Abc_Tt6Cofactor1(uTruthF, iObjIndex) : Abc_Tt6Cofactor0(uTruthF, iObjIndex); + Vec_WrdWriteEntry( &p->vObjTruth, iFanout, Abc_Tt6RemoveVar(uTruthF, iObjIndex) ); + Acb_ObjSuppMin( p, iFanout ); + } + if ( Acb_ObjFanoutNum(p, iObj) == 0 ) + Acb_ObjCleanType( p, iObj ); +} +void Acb_ObjRemoveBufInv( Acb_Ntk_t * p, int iObj ) +{ + int iFanout; + word uTruth = Acb_ObjTruth( p, iObj ); + assert( !Acb_ObjIsCio(p, iObj) ); + assert( Acb_ObjFaninNum(p, iObj) == 1 ); + assert( uTruth == s_Truths6[0] || ~uTruth == s_Truths6[0] ); + while ( (iFanout = Acb_ObjFindNodeFanout(p, iObj)) >= 0 ) + { + int iFanin = Acb_ObjFanin( p, iObj, 0 ); + int iObjIndex = Acb_ObjWhatFanin( p, iFanout, iObj ); + Acb_ObjPatchFanin( p, iFanout, iObj, iFanin ); + if ( uTruth & 1 ) // inv + { + word uTruthF = Acb_ObjTruth( p, iFanout ); + Vec_WrdWriteEntry( &p->vObjTruth, iFanout, Abc_Tt6Flip(uTruthF, iObjIndex) ); + } + Acb_ObjRemoveDupFanins( p, iFanout ); + } + while ( (uTruth & 1) == 0 && Acb_ObjFanoutNum(p, iObj) > 0 ) + { + int iFanin = Acb_ObjFanin( p, iObj, 0 ); + int iFanout = Acb_ObjFanout( p, iObj, 0 ); + assert( Acb_ObjIsCo(p, iFanout) ); + Acb_ObjPatchFanin( p, iFanout, iObj, iFanin ); + } + if ( Acb_ObjFanoutNum(p, iObj) == 0 ) + { + Acb_ObjRemoveFaninFanout( p, iObj ); + Acb_ObjRemoveFanins( p, iObj ); + Acb_ObjCleanType( p, iObj ); + } +} + +/**Function************************************************************* + + Synopsis [Check if the node can have its logic pushed.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Acb_ObjFindFaninPushableIndex( Acb_Ntk_t * p, int iObj, int iFanIndex ) +{ + int k, iFanin, * pFanins; + Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k ) + if ( k != iFanIndex && Abc_TtCheckDsdAnd(Acb_ObjTruth(p, iObj), k, iFanIndex, NULL) >= 0 ) + return k; + return -1; +} +static inline int Acb_ObjFindFanoutPushableIndex( Acb_Ntk_t * p, int iObj ) +{ + int k, iFanin, * pFanins; + Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k ) + if ( Abc_TtCheckOutAnd(Acb_ObjTruth(p, iObj), k, NULL) >= 0 ) + return k; + return -1; +} +int Acb_ObjPushToFanins( Acb_Ntk_t * p, int iObj, int nLutSize ) +{ + int k, k2, iFanin, * pFanins; + if ( Acb_ObjFaninNum(p, iObj) < 2 ) + return 0; + Acb_ObjForEachFaninFast( p, iObj, pFanins, iFanin, k ) + { + if ( Acb_ObjIsCi(p, iFanin) ) + continue; + if ( Acb_ObjFanoutNum(p, iFanin) > 1 ) + continue; + if ( Acb_ObjFaninNum(p, iFanin) == nLutSize ) + continue; + if ( (k2 = Acb_ObjFindFaninPushableIndex(p, iObj, k)) == -1 ) + continue; + //printf( "Object %4d : Pushing fanin %d (%d) into fanin %d.\n", iObj, Acb_ObjFanin(p, iObj, k2), k2, iFanin ); + Acb_ObjPushToFanin( p, iObj, k2, iFanin ); + return 1; + } + if ( Acb_ObjFaninNum(p, iObj) == 2 && Acb_ObjFanoutNum(p, iObj) == 1 ) + { + int iFanout = Acb_ObjFanout( p, iObj, 0 ); + if ( !Acb_ObjIsCo(p, iFanout) && Acb_ObjFaninNum(p, iFanout) < nLutSize ) + { + k2 = Acb_ObjFindFanoutPushableIndex( p, iObj ); + //printf( "Object %4d : Pushing fanin %d (%d) into fanout %d.\n", iObj, Acb_ObjFanin(p, iObj, k2), k2, iFanout ); + Acb_ObjPushToFanout( p, iObj, k2, iFanout ); + return 1; + } + } + return 0; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_NtkPushLogic( Acb_Ntk_t * p, int nLutSize, int fVerbose ) +{ + int n = 0, iObj, nNodes = Acb_NtkNodeNum(p), nPushes = 0; + Acb_NtkCreateFanout( p ); // fanout data structure + Acb_NtkForEachNodeSupp( p, iObj, 0 ) + Acb_ObjRemoveConst( p, iObj ); + Acb_NtkForEachNodeSupp( p, iObj, 1 ) + Acb_ObjRemoveBufInv( p, iObj ); + for ( n = 2; n <= nLutSize; n++ ) + Acb_NtkForEachNodeSupp( p, iObj, n ) + { + while ( Acb_ObjPushToFanins(p, iObj, nLutSize) ) + nPushes++; + if ( Acb_ObjFaninNum(p, iObj) == 1 ) + Acb_ObjRemoveBufInv( p, iObj ); + } + printf( "Saved %d nodes after %d pushes.\n", nNodes - Acb_NtkNodeNum(p), nPushes ); +} + +/**Function************************************************************* + + Synopsis [Pushing logic to the fanin.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Acb_NtkPushLogic2( Acb_Ntk_t * p, int nLutSize, int fVerbose ) +{ + int iObj; + Acb_NtkCreateFanout( p ); // fanout data structure + Acb_NtkForEachObj( p, iObj ) + if ( !Acb_ObjIsCio(p, iObj) ) + break; + Acb_ObjPushToFanout( p, iObj, Acb_ObjFaninNum(p, iObj)-1, Acb_ObjFanout(p, iObj, 0) ); +// Acb_ObjPushToFanin( p, Acb_ObjFanout(p, iObj, 0), Acb_ObjFaninNum(p, iObj)-1, iObj ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/base/acb/module.make b/src/base/acb/module.make index 06affeff..46294f9f 100644 --- a/src/base/acb/module.make +++ b/src/base/acb/module.make @@ -3,5 +3,6 @@ SRC += src/base/acb/acbAbc.c \ src/base/acb/acbCom.c \ src/base/acb/acbFunc.c \ src/base/acb/acbMfs.c \ + src/base/acb/acbPush.c \ src/base/acb/acbSets.c \ src/base/acb/acbUtil.c diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 7086cc9f..eff3acba 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -325,7 +325,7 @@ extern int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars ); /*=== wlcAbs2.c ========================================================*/ extern int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars ); /*=== wlcBlast.c ========================================================*/ -extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, int nRange, int fGiaSimple, int fAddOutputs, int fBooth, int fNoCleanup ); +extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, int nRange, int fGiaSimple, int fAddOutputs, int fBooth, int fNoCleanup, int fCreateMiter ); /*=== wlcCom.c ========================================================*/ extern void Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk ); /*=== wlcNtk.c ========================================================*/ diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c index d0ef1f07..a183fb5f 100644 --- a/src/base/wlc/wlcAbs.c +++ b/src/base/wlc/wlcAbs.c @@ -320,7 +320,7 @@ static Vec_Int_t * Wlc_NtkGetCoreSels( Gia_Man_t * pFrames, int nFrames, int fir static Gia_Man_t * Wlc_NtkUnrollWoCex(Wlc_Ntk_t * pChoice, int nFrames, int first_sel_pi, int num_sel_pis) { - Gia_Man_t * pGiaChoice = Wlc_NtkBitBlast( pChoice, NULL, -1, 0, 0, 0, 0, 0 ); + Gia_Man_t * pGiaChoice = Wlc_NtkBitBlast( pChoice, NULL, -1, 0, 0, 0, 0, 0, 0 ); Gia_Man_t * pFrames = NULL, * pGia; Gia_Obj_t * pObj, * pObjRi; int f, i; @@ -366,7 +366,7 @@ static Gia_Man_t * Wlc_NtkUnrollWoCex(Wlc_Ntk_t * pChoice, int nFrames, int firs static Gia_Man_t * Wlc_NtkUnrollWithCex(Wlc_Ntk_t * pChoice, Abc_Cex_t * pCex, int nbits_old_pis, int num_sel_pis, int * p_num_ppis, int sel_pi_first, int fUsePPI) { - Gia_Man_t * pGiaChoice = Wlc_NtkBitBlast( pChoice, NULL, -1, 0, 0, 0, 0, 0 ); + Gia_Man_t * pGiaChoice = Wlc_NtkBitBlast( pChoice, NULL, -1, 0, 0, 0, 0, 0, 0 ); int nbits_new_pis = Wlc_NtkNumPiBits( pChoice ); int num_ppis = nbits_new_pis - nbits_old_pis - num_sel_pis; int num_undc_pis = Gia_ManPiNum(pGiaChoice) - nbits_new_pis; @@ -560,7 +560,7 @@ Wlc_Ntk_t * Wlc_NtkIntroduceChoices( Wlc_Ntk_t * pNtk, Vec_Int_t * vBlacks, Vec_ static Abc_Cex_t * Wlc_NtkCexIsReal( Wlc_Ntk_t * pOrig, Abc_Cex_t * pCex ) { - Gia_Man_t * pGiaOrig = Wlc_NtkBitBlast( pOrig, NULL, -1, 0, 0, 0, 0, 0 ); + Gia_Man_t * pGiaOrig = Wlc_NtkBitBlast( pOrig, NULL, -1, 0, 0, 0, 0, 0, 0 ); int f, i; Gia_Obj_t * pObj, * pObjRi; Abc_Cex_t * pCexReal = Abc_CexAlloc( Gia_ManRegNum(pGiaOrig), Gia_ManPiNum(pGiaOrig), pCex->iFrame + 1 ); @@ -1401,7 +1401,7 @@ Aig_Man_t * Wla_ManBitBlast( Wla_Man_t * pWla, Wlc_Ntk_t * pAbs ) Gia_Man_t * pTemp; Aig_Man_t * pAig; - pWla->pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0, 0 ); + pWla->pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0, 0, 0 ); // if the abstraction has flops with DC-init state, // new PIs were introduced by bit-blasting at the end of the PI list @@ -1829,7 +1829,7 @@ int Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, NULL, pPars->fVerbose ); } - pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0, 0 ); + pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0, 0, 0 ); // if the abstraction has flops with DC-init state, // new PIs were introduced by bit-blasting at the end of the PI list diff --git a/src/base/wlc/wlcAbs2.c b/src/base/wlc/wlcAbs2.c index ff0092e6..4b2e6740 100644 --- a/src/base/wlc/wlcAbs2.c +++ b/src/base/wlc/wlcAbs2.c @@ -328,7 +328,7 @@ int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars ) // get abstracted GIA and the set of pseudo-PIs (vPisNew) pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, pPars->fVerbose ); - pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0, 0 ); + pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0, 0, 0 ); // if the abstraction has flops with DC-init state, // new PIs were introduced by bit-blasting at the end of the PI list diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index 02cb2b1c..b2d0e287 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -868,14 +868,14 @@ void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int SeeAlso [] ***********************************************************************/ -Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, int nOutputRange, int fGiaSimple, int fAddOutputs, int fBooth, int fNoCleanup ) +Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, int nOutputRange, int fGiaSimple, int fAddOutputs, int fBooth, int fNoCleanup, int fCreateMiter ) { int fVerbose = 0; int fUseOldMultiplierBlasting = 0; int fSkipBitRange = 0; Tim_Man_t * pManTime = NULL; Gia_Man_t * pTemp, * pNew, * pExtra = NULL; - Wlc_Obj_t * pObj; + Wlc_Obj_t * pObj, * pObj2; Vec_Int_t * vBits = &p->vBits, * vTemp0, * vTemp1, * vTemp2, * vRes, * vAddOutputs = NULL, * vAddObjs = NULL; int nBits = Wlc_NtkPrepareBits( p ); int nRange, nRange0, nRange1, nRange2; @@ -1211,6 +1211,31 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in for ( k = 1; k < nRange; k++ ) Vec_IntPush( vRes, 0 ); } + else if ( pObj->Type == WLC_OBJ_COMP_NOTEQU && Wlc_ObjFaninNum(pObj) > 2 ) + { + // find the max range + int a, b, iRes = 1, nRangeMax = Abc_MaxInt( nRange0, nRange1 ); + for ( k = 2; k < Wlc_ObjFaninNum(pObj); k++ ) + nRangeMax = Abc_MaxInt( nRangeMax, Wlc_ObjRange( Wlc_NtkObj(p, Wlc_ObjFaninId(pObj, k)) ) ); + // create pairwise distinct + for ( a = 0; a < Wlc_ObjFaninNum(pObj); a++ ) + for ( b = a+1; b < Wlc_ObjFaninNum(pObj); b++ ) + { + int nRange0 = Wlc_ObjRange( Wlc_NtkObj(p, Wlc_ObjFaninId(pObj, a)) ); + int nRange1 = Wlc_ObjRange( Wlc_NtkObj(p, Wlc_ObjFaninId(pObj, b)) ); + int * pFans0 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId(pObj, a)) ); + int * pFans1 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId(pObj, b)) ); + int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, 0 ); + int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, 0 ); + int iLit = 0; + for ( k = 0; k < nRangeMax; k++ ) + iLit = Gia_ManHashOr( pNew, iLit, Gia_ManHashXor(pNew, pArg0[k], pArg1[k]) ); + iRes = Gia_ManHashAnd( pNew, iRes, iLit ); + } + Vec_IntFill( vRes, 1, iRes ); + for ( k = 1; k < nRange; k++ ) + Vec_IntPush( vRes, 0 ); + } else if ( pObj->Type == WLC_OBJ_COMP_EQU || pObj->Type == WLC_OBJ_COMP_NOTEQU ) { int iLit = 0, nRangeMax = Abc_MaxInt( nRange0, nRange1 ); @@ -1363,38 +1388,91 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in Vec_IntFree( vTemp2 ); Vec_IntFree( vRes ); // create COs - Wlc_NtkForEachCo( p, pObj, i ) + if ( fCreateMiter ) { - // skip all outputs except the given ones - if ( iOutput >= 0 && (i < iOutput || i >= iOutput + nOutputRange) ) - continue; - // create additional PO literals - if ( vAddOutputs && pObj->fIsFi ) - { - Vec_IntForEachEntry( vAddOutputs, iLit, k ) - Gia_ManAppendCo( pNew, iLit ); - printf( "Created %d additional POs for %d interesting internal word-level variables.\n", Vec_IntSize(vAddOutputs), Vec_IntSize(vAddObjs) ); - Vec_IntFreeP( &vAddOutputs ); - } - nRange = Wlc_ObjRange( pObj ); - pFans0 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)) ); - if ( fVerbose ) - printf( "%s(%d) ", Wlc_ObjName(p, Wlc_ObjId(p, pObj)), Gia_ManCoNum(pNew) ); - if ( Wlc_ObjRangeIsReversed(pObj) ) + int nPairs = 0, nBits = 0; + assert( Wlc_NtkPoNum(p) % 2 == 0 ); + Wlc_NtkForEachCo( p, pObj, i ) { - for ( k = 0; k < nRange; k++ ) - Gia_ManAppendCo( pNew, pFans0[nRange-1-k] ); + if ( pObj->fIsFi ) + { + nRange = Wlc_ObjRange( pObj ); + pFans0 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)) ); + if ( Wlc_ObjRangeIsReversed(pObj) ) + { + for ( k = 0; k < nRange; k++ ) + Gia_ManAppendCo( pNew, pFans0[nRange-1-k] ); + } + else + { + for ( k = 0; k < nRange; k++ ) + Gia_ManAppendCo( pNew, pFans0[k] ); + } + nFFins += nRange; + continue; + } + pObj2 = Wlc_NtkCo( p, ++i ); + nRange1 = Wlc_ObjRange( pObj ); + nRange2 = Wlc_ObjRange( pObj2 ); + assert( nRange1 == nRange2 ); + pFans1 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)) ); + pFans2 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj2)) ); + if ( Wlc_ObjRangeIsReversed(pObj) ) + { + for ( k = 0; k < nRange1; k++ ) + { + Gia_ManAppendCo( pNew, pFans1[nRange1-1-k] ); + Gia_ManAppendCo( pNew, pFans2[nRange2-1-k] ); + } + } + else + { + for ( k = 0; k < nRange1; k++ ) + { + Gia_ManAppendCo( pNew, pFans1[k] ); + Gia_ManAppendCo( pNew, pFans2[k] ); + } + } + nPairs++; + nBits += nRange1; } - else + printf( "Derived a dual-output miter with %d pairs of bits belonging to %d pairs of word-level outputs.\n", nBits, nPairs ); + } + else + { + Wlc_NtkForEachCo( p, pObj, i ) { - for ( k = 0; k < nRange; k++ ) - Gia_ManAppendCo( pNew, pFans0[k] ); + // skip all outputs except the given ones + if ( iOutput >= 0 && (i < iOutput || i >= iOutput + nOutputRange) ) + continue; + // create additional PO literals + if ( vAddOutputs && pObj->fIsFi ) + { + Vec_IntForEachEntry( vAddOutputs, iLit, k ) + Gia_ManAppendCo( pNew, iLit ); + printf( "Created %d additional POs for %d interesting internal word-level variables.\n", Vec_IntSize(vAddOutputs), Vec_IntSize(vAddObjs) ); + Vec_IntFreeP( &vAddOutputs ); + } + nRange = Wlc_ObjRange( pObj ); + pFans0 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjId(p, pObj)) ); + if ( fVerbose ) + printf( "%s(%d) ", Wlc_ObjName(p, Wlc_ObjId(p, pObj)), Gia_ManCoNum(pNew) ); + if ( Wlc_ObjRangeIsReversed(pObj) ) + { + for ( k = 0; k < nRange; k++ ) + Gia_ManAppendCo( pNew, pFans0[nRange-1-k] ); + } + else + { + for ( k = 0; k < nRange; k++ ) + Gia_ManAppendCo( pNew, pFans0[k] ); + } + if ( pObj->fIsFi ) + nFFins += nRange; } - if ( pObj->fIsFi ) - nFFins += nRange; + if ( fVerbose ) + printf( "\n" ); } - if ( fVerbose ) - printf( "\n" ); //Vec_IntErase( vBits ); //Vec_IntErase( &p->vCopies ); // set the number of registers diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 16ed29cc..abcb9e19 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -885,9 +885,9 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv ) Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc); Vec_Int_t * vBoxIds = NULL; Gia_Man_t * pNew = NULL; - int c, iOutput = -1, nOutputRange = 2, fGiaSimple = 0, fAddOutputs = 0, fMulti = 0, fBooth = 0, fVerbose = 0; + int c, iOutput = -1, nOutputRange = 2, fGiaSimple = 0, fAddOutputs = 0, fMulti = 0, fBooth = 0, fCreateMiter = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "ORcombvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "ORcombdvh" ) ) != EOF ) { switch ( c ) { @@ -925,6 +925,9 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'b': fBooth ^= 1; break; + case 'd': + fCreateMiter ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -951,7 +954,7 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } // transform - pNew = Wlc_NtkBitBlast( pNtk, vBoxIds, iOutput, nOutputRange, fGiaSimple, fAddOutputs, fBooth, 0 ); + pNew = Wlc_NtkBitBlast( pNtk, vBoxIds, iOutput, nOutputRange, fGiaSimple, fAddOutputs, fBooth, 0, fCreateMiter ); Vec_IntFreeP( &vBoxIds ); if ( pNew == NULL ) { @@ -961,7 +964,7 @@ int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameUpdateGia( pAbc, pNew ); return 0; usage: - Abc_Print( -2, "usage: %%blast [-OR num] [-combvh]\n" ); + Abc_Print( -2, "usage: %%blast [-OR num] [-combdvh]\n" ); Abc_Print( -2, "\t performs bit-blasting of the word-level design\n" ); Abc_Print( -2, "\t-O num : zero-based index of the first word-level PO to bit-blast [default = %d]\n", iOutput ); Abc_Print( -2, "\t-R num : the total number of word-level POs to bit-blast [default = %d]\n", nOutputRange ); @@ -969,6 +972,7 @@ usage: Abc_Print( -2, "\t-o : toggle using additional POs on the word-level boundaries [default = %s]\n", fAddOutputs? "yes": "no" ); Abc_Print( -2, "\t-m : toggle creating boxes for all multipliers in the design [default = %s]\n", fMulti? "yes": "no" ); Abc_Print( -2, "\t-b : toggle generating radix-4 Booth multipliers [default = %s]\n", fBooth? "yes": "no" ); + Abc_Print( -2, "\t-d : toggle creating dual-output miter [default = %s]\n", fCreateMiter? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; diff --git a/src/base/wlc/wlcGraft.c b/src/base/wlc/wlcGraft.c index 33de00c5..f1f55eb3 100644 --- a/src/base/wlc/wlcGraft.c +++ b/src/base/wlc/wlcGraft.c @@ -210,7 +210,7 @@ Wlc_Ntk_t * Wlc_NtkGraftMulti( Wlc_Ntk_t * p, int fVerbose ) Gia_Obj_t * pObj; Vec_Int_t * vObjsLHS = Wlc_NtkCollectObjs( p, 0, &nMultiLHS ); Vec_Int_t * vObjsRHS = Wlc_NtkCollectObjs( p, 1, &nMultiRHS ); - Gia_Man_t * pGia = Wlc_NtkBitBlast( p, NULL, -1, 0, 0, 0, 0, 1 ); + Gia_Man_t * pGia = Wlc_NtkBitBlast( p, NULL, -1, 0, 0, 0, 0, 1, 0 ); Vec_Mem_t * vTtMem = Vec_MemAlloc( nWords, 10 ); Vec_MemHashAlloc( vTtMem, 10000 ); @@ -540,7 +540,7 @@ int Sbc_ManWlcNodes( Wlc_Ntk_t * pNtk, Gia_Man_t * p, Vec_Int_t * vGia2Out, int void Sbc_ManDetectMultTest( Wlc_Ntk_t * pNtk, int fVerbose ) { extern Vec_Int_t * Sdb_StoComputeCutsDetect( Gia_Man_t * pGia ); - Gia_Man_t * p = Wlc_NtkBitBlast( pNtk, NULL, -1, 0, 0, 0, 0, 1 ); + Gia_Man_t * p = Wlc_NtkBitBlast( pNtk, NULL, -1, 0, 0, 0, 0, 1, 0 ); Vec_Int_t * vIns, * vGia2Out; int iObjFound = -1; // Gia_Obj_t * pObj; int i; diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c index 69a01ab0..230b34ad 100644 --- a/src/base/wlc/wlcReadSmt.c +++ b/src/base/wlc/wlcReadSmt.c @@ -331,7 +331,7 @@ static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, in Type == WLC_OBJ_LOGIC_OR || // 29: logic OR Type == WLC_OBJ_LOGIC_XOR || // 30: logic XOR Type == WLC_OBJ_COMP_EQU || // 31: compare equal - Type == WLC_OBJ_COMP_NOTEQU || // 32: compare not equal +// Type == WLC_OBJ_COMP_NOTEQU || // 32: compare not equal -- bug fix Type == WLC_OBJ_COMP_LESS || // 33: compare less Type == WLC_OBJ_COMP_MORE || // 34: compare more Type == WLC_OBJ_COMP_LESSEQU || // 35: compare less or equal diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c index 63a6926b..a829e0fd 100644 --- a/src/base/wlc/wlcReadVer.c +++ b/src/base/wlc/wlcReadVer.c @@ -1292,7 +1292,7 @@ void Io_ReadWordTest( char * pFileName ) return; Wlc_WriteVer( pNtk, "test.v", 0, 0 ); - pNew = Wlc_NtkBitBlast( pNtk, NULL, -1, 0, 0, 0, 0, 0 ); + pNew = Wlc_NtkBitBlast( pNtk, NULL, -1, 0, 0, 0, 0, 0, 0 ); Gia_AigerWrite( pNew, "test.aig", 0, 0 ); Gia_ManStop( pNew ); diff --git a/src/base/wlc/wlcSim.c b/src/base/wlc/wlcSim.c index 2ae3c86e..31a8a4a0 100644 --- a/src/base/wlc/wlcSim.c +++ b/src/base/wlc/wlcSim.c @@ -129,7 +129,7 @@ Vec_Ptr_t * Wlc_NtkSimulate( Wlc_Ntk_t * p, Vec_Int_t * vNodes, int nWords, int { Gia_Obj_t * pObj; Vec_Ptr_t * vOne, * vRes; - Gia_Man_t * pGia = Wlc_NtkBitBlast( p, NULL, -1, 0, 0, 0, 0, 0 ); + Gia_Man_t * pGia = Wlc_NtkBitBlast( p, NULL, -1, 0, 0, 0, 0, 0, 0 ); Wlc_Obj_t * pWlcObj; int f, i, k, w, nBits, Counter = 0; // allocate simulation info for one timeframe diff --git a/src/bdd/extrab/extraBddMisc.c b/src/bdd/extrab/extraBddMisc.c index bc4d8a7a..a5cda242 100644 --- a/src/bdd/extrab/extraBddMisc.c +++ b/src/bdd/extrab/extraBddMisc.c @@ -58,8 +58,8 @@ static DdNode * cuddBddPermuteRecur ARGS( ( DdManager * manager, DdHashTable * t static DdNode * extraBddAndPermute( DdHashTable * table, DdManager * ddF, DdNode * bF, DdManager * ddG, DdNode * bG, int * pPermute ); // file "cuddUtils.c" -static void ddSupportStep(DdNode *f, int *support); -static void ddClearFlag(DdNode *f); +void ddSupportStep2(DdNode *f, int *support); +void ddClearFlag2(DdNode *f); static DdNode* extraZddPrimes( DdManager *dd, DdNode* F ); @@ -547,8 +547,8 @@ Extra_SupportArray( support[i] = 0; /* Compute support and clean up markers. */ - ddSupportStep(Cudd_Regular(f),support); - ddClearFlag(Cudd_Regular(f)); + ddSupportStep2(Cudd_Regular(f),support); + ddClearFlag2(Cudd_Regular(f)); return(support); @@ -584,9 +584,9 @@ Extra_VectorSupportArray( /* Compute support and clean up markers. */ for ( i = 0; i < n; i++ ) - ddSupportStep( Cudd_Regular(F[i]), support ); + ddSupportStep2( Cudd_Regular(F[i]), support ); for ( i = 0; i < n; i++ ) - ddClearFlag( Cudd_Regular(F[i]) ); + ddClearFlag2( Cudd_Regular(F[i]) ); return support; } @@ -782,8 +782,8 @@ DdNode * Extra_bddSupportNegativeCube( DdManager * dd, DdNode * f ) } /* Compute support and clean up markers. */ - ddSupportStep( Cudd_Regular( f ), support ); - ddClearFlag( Cudd_Regular( f ) ); + ddSupportStep2( Cudd_Regular( f ), support ); + ddClearFlag2( Cudd_Regular( f ) ); /* Transform support from array to cube. */ do @@ -1689,8 +1689,8 @@ extraTransferPermuteRecur( SeeAlso [ddClearFlag] ******************************************************************************/ -static void -ddSupportStep( +void +ddSupportStep2( DdNode * f, int * support) { @@ -1699,8 +1699,8 @@ ddSupportStep( } support[f->index] = 1; - ddSupportStep(cuddT(f),support); - ddSupportStep(Cudd_Regular(cuddE(f)),support); + ddSupportStep2(cuddT(f),support); + ddSupportStep2(Cudd_Regular(cuddE(f)),support); /* Mark as visited. */ f->next = Cudd_Not(f->next); return; @@ -1720,8 +1720,8 @@ ddSupportStep( SeeAlso [ddSupportStep ddDagInt] ******************************************************************************/ -static void -ddClearFlag( +void +ddClearFlag2( DdNode * f) { if (!Cudd_IsComplement(f->next)) { @@ -1732,8 +1732,8 @@ ddClearFlag( if (cuddIsConstant(f)) { return; } - ddClearFlag(cuddT(f)); - ddClearFlag(Cudd_Regular(cuddE(f))); + ddClearFlag2(cuddT(f)); + ddClearFlag2(Cudd_Regular(cuddE(f))); return; } /* end of ddClearFlag */ diff --git a/src/misc/extra/extraUtilCube.c b/src/misc/extra/extraUtilCube.c index c053e23a..f518405b 100644 --- a/src/misc/extra/extraUtilCube.c +++ b/src/misc/extra/extraUtilCube.c @@ -159,8 +159,8 @@ Iter 12 -> 3674160 Time = 70.48 sec SeeAlso [] ***********************************************************************/ -static inline int Abc_DataHasBit( word * p, word i ) { return (p[(i)>>6] & (1<<((i) & 63))) > 0; } -static inline void Abc_DataXorBit( word * p, word i ) { p[(i)>>6] ^= (1<<((i) & 63)); } +static inline int Abc_DataHasBit( word * p, word i ) { return (p[(i)>>6] & (((word)1)<<((i) & 63))) > 0; } +static inline void Abc_DataXorBit( word * p, word i ) { p[(i)>>6] ^= (((word)1)<<((i) & 63)); } static inline int Abc_DataGetCube( word w, int i ) { return (w >> (5*i)) & 31; } static inline word Abc_DataXorCube( word w, int i, int c ) { return w ^ (((word)c) << (5*i)); } static inline word Abc_CubeGenerateSign( char * pState ) diff --git a/src/misc/extra/extraUtilEnum.c b/src/misc/extra/extraUtilEnum.c index 31364a16..84b0b089 100644 --- a/src/misc/extra/extraUtilEnum.c +++ b/src/misc/extra/extraUtilEnum.c @@ -298,8 +298,8 @@ void Abc_EnumPrint( Vec_Int_t * vGates, int i, int nVars ) SeeAlso [] ***********************************************************************/ -static inline int Abc_DataHasBit( word * p, word i ) { return (p[(i)>>6] & (1<<((i) & 63))) > 0; } -static inline void Abc_DataXorBit( word * p, word i ) { p[(i)>>6] ^= (1<<((i) & 63)); } +static inline int Abc_DataHasBit( word * p, word i ) { return (p[(i)>>6] & (((word)1)<<((i) & 63))) > 0; } +static inline void Abc_DataXorBit( word * p, word i ) { p[(i)>>6] ^= (((word)1)<<((i) & 63)); } /**Function************************************************************* diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h index 9e906816..b68d7b4c 100644 --- a/src/misc/util/abc_global.h +++ b/src/misc/util/abc_global.h @@ -312,16 +312,16 @@ static inline void Abc_Print( int level, const char * format, ... ) printf( "Warning: " ); }else{ if ( level == ABC_ERROR ) - Gia_ManToBridgeText( stdout, strlen("Error: "), (unsigned char*)"Error: " ); + Gia_ManToBridgeText( stdout, (int)strlen("Error: "), (unsigned char*)"Error: " ); else if ( level == ABC_WARNING ) - Gia_ManToBridgeText( stdout, strlen("Warning: "), (unsigned char*)"Warning: " ); + Gia_ManToBridgeText( stdout, (int)strlen("Warning: "), (unsigned char*)"Warning: " ); } va_start( args, format ); if ( Abc_FrameIsBridgeMode() ) { char * tmp = vnsprintf( format, args ); - Gia_ManToBridgeText( stdout, strlen(tmp), (unsigned char*)tmp ); + Gia_ManToBridgeText( stdout, (int)strlen(tmp), (unsigned char*)tmp ); free( tmp ); } else diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index e04ffbc9..4736a291 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -1378,6 +1378,13 @@ static inline void Abc_TtMoveVar( word * pF, int nVars, int * V2P, int * P2V, in P2V[jVar] ^= P2V[iVar]; P2V[iVar] ^= P2V[jVar]; } +static inline word Abc_Tt6RemoveVar( word t, int iVar ) +{ + assert( !Abc_Tt6HasVar(t, iVar) ); + while ( iVar < 5 ) + t = Abc_Tt6SwapAdjacent( t, iVar++ ); + return t; +} /**Function************************************************************* @@ -2209,7 +2216,51 @@ static inline int Abc_Tt6EsopVerify( word t, int nVars ) /**Function************************************************************* - Synopsis [Check if the function is decomposable with the given pair.] + Synopsis [Check if the function is output-decomposable with the given var.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline int Abc_TtCheckOutAnd( word t, int i, word * pOut ) +{ + word c0 = Abc_Tt6Cofactor0( t, i ); + word c1 = Abc_Tt6Cofactor1( t, i ); + assert( c0 != c1 ); + if ( c0 == 0 ) // F = i * G + { + if ( pOut ) *pOut = c1; + return 0; + } + if ( c1 == 0 ) // F = ~i * G + { + if ( pOut ) *pOut = c0; + return 1; + } + if ( ~c0 == 0 ) // F = ~i + G + { + if ( pOut ) *pOut = c1; + return 2; + } + if ( ~c1 == 0 ) // F = i + G + { + if ( pOut ) *pOut = c0; + return 3; + } + if ( c0 == ~c1 ) // F = i # G + { + if ( pOut ) *pOut = c0; + return 4; + } + return -1; +} + +/**Function************************************************************* + + Synopsis [Check if the function is input-decomposable with the given pair.] Description [] diff --git a/src/misc/vec/vecSet.h b/src/misc/vec/vecSet.h index ac3dd95c..e2ae337f 100644 --- a/src/misc/vec/vecSet.h +++ b/src/misc/vec/vecSet.h @@ -120,7 +120,7 @@ static inline void Vec_SetAlloc_( Vec_Set_t * p, int nPageSize ) p->uPageMask = (unsigned)((1 << nPageSize) - 1); p->nPagesAlloc = 256; p->pPages = ABC_CALLOC( word *, p->nPagesAlloc ); - p->pPages[0] = ABC_ALLOC( word, (1 << p->nPageSize) ); + p->pPages[0] = ABC_ALLOC( word, (int)(((word)1) << p->nPageSize) ); p->pPages[0][0] = ~0; p->pPages[0][1] = ~0; Vec_SetWriteLimit( p->pPages[0], 2 ); @@ -195,7 +195,7 @@ static inline double Vec_ReportMemory( Vec_Set_t * p ) { double Mem = sizeof(Vec_Set_t); Mem += p->nPagesAlloc * sizeof(void *); - Mem += sizeof(word) * (1 << p->nPageSize) * (1 + p->iPage); + Mem += sizeof(word) * (int)(((word)1) << p->nPageSize) * (1 + p->iPage); return Mem; } @@ -224,7 +224,7 @@ static inline int Vec_SetAppend( Vec_Set_t * p, int * pArray, int nSize ) p->nPagesAlloc *= 2; } if ( p->pPages[p->iPage] == NULL ) - p->pPages[p->iPage] = ABC_ALLOC( word, (1 << p->nPageSize) ); + p->pPages[p->iPage] = ABC_ALLOC( word, (int)(((word)1) << p->nPageSize) ); Vec_SetWriteLimit( p->pPages[p->iPage], 2 ); p->pPages[p->iPage][1] = ~0; } @@ -252,7 +252,7 @@ static inline void * Vec_SetFetch( Vec_Set_t * p, int nBytes ) } static inline char * Vec_SetStrsav( Vec_Set_t * p, char * pName ) { - char * pStr = (char *)Vec_SetFetch( p, strlen(pName) + 1 ); + char * pStr = (char *)Vec_SetFetch( p, (int)strlen(pName) + 1 ); strcpy( pStr, pName ); return pStr; } diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h index 04cd5da8..ef5e9a41 100644 --- a/src/misc/vec/vecStr.h +++ b/src/misc/vec/vecStr.h @@ -671,7 +671,7 @@ static inline void Vec_StrPrintNumStar( Vec_Str_t * p, int Num, int nDigits ) ***********************************************************************/ static inline void Vec_StrPrintStr( Vec_Str_t * p, const char * pStr ) { - int i, Length = strlen(pStr); + int i, Length = (int)strlen(pStr); for ( i = 0; i < Length; i++ ) Vec_StrPush( p, pStr[i] ); } diff --git a/src/opt/fxch/FxchSCHashTable.c b/src/opt/fxch/FxchSCHashTable.c index f854a1fa..80753677 100644 --- a/src/opt/fxch/FxchSCHashTable.c +++ b/src/opt/fxch/FxchSCHashTable.c @@ -195,7 +195,8 @@ int Fxch_SCHashTableInsert( Fxch_SCHashTable_t* pSCHashTable, } else if ( pBin->Size == pBin->Cap ) { - pBin->Cap = 2 * pBin->Size; + assert(pBin->Cap <= 0xAAAA); + pBin->Cap = ( pBin->Cap >> 1 ) * 3; pBin->vSCData = ABC_REALLOC( Fxch_SubCube_t, pBin->vSCData, pBin->Cap ); } diff --git a/src/sat/bsat/satClause.h b/src/sat/bsat/satClause.h index 0b1756ff..3a6afa20 100644 --- a/src/sat/bsat/satClause.h +++ b/src/sat/bsat/satClause.h @@ -199,8 +199,8 @@ static inline void Sat_MemAlloc_( Sat_Mem_t * p, int nPageSize ) p->uPageMask = (unsigned)((1 << nPageSize) - 1); p->nPagesAlloc = 256; p->pPages = ABC_CALLOC( int *, p->nPagesAlloc ); - p->pPages[0] = ABC_ALLOC( int, (1 << p->nPageSize) ); - p->pPages[1] = ABC_ALLOC( int, (1 << p->nPageSize) ); + p->pPages[0] = ABC_ALLOC( int, (int)(((word)1) << p->nPageSize) ); + p->pPages[1] = ABC_ALLOC( int, (int)(((word)1) << p->nPageSize) ); p->iPage[0] = 0; p->iPage[1] = 1; Sat_MemWriteLimit( p->pPages[0], 2 ); @@ -315,7 +315,7 @@ static inline int Sat_MemAppend( Sat_Mem_t * p, int * pArray, int nSize, int lrn p->nPagesAlloc *= 2; } if ( p->pPages[p->iPage[lrn]] == NULL ) - p->pPages[p->iPage[lrn]] = ABC_ALLOC( int, (1 << p->nPageSize) ); + p->pPages[p->iPage[lrn]] = ABC_ALLOC( int, (int)(((word)1) << p->nPageSize) ); pPage = p->pPages[p->iPage[lrn]]; Sat_MemWriteLimit( pPage, 2 ); } |