diff --git a/Makefile b/Makefile index 50cff2d17..2dfc1c691 100644 --- a/Makefile +++ b/Makefile @@ -66,7 +66,7 @@ endif ifdef ABC_USE_NAMESPACE CFLAGS += -DABC_NAMESPACE=$(ABC_USE_NAMESPACE) -fpermissive -x c++ CC := $(CXX) - $(info $(MSG_PREFIX)Compiling in namespace $(ABC_NAMESPACE)) + $(info $(MSG_PREFIX)Compiling in namespace $(ABC_USE_NAMESPACE)) endif # compile CUDD with ABC diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 273c530ec..ee79ccd7a 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -270,6 +270,7 @@ struct Gps_Par_t_ int fSkipMap; int fSlacks; int fNoColor; + int fMapOutStats; char * pDumpFile; }; @@ -387,6 +388,7 @@ struct Jf_Par_t_ float Epsilon; float * pTimesArr; float * pTimesReq; + char * ZFile; }; static inline unsigned Gia_ObjCutSign( unsigned ObjId ) { return (1 << (ObjId & 31)); } @@ -1411,6 +1413,10 @@ extern Gia_Man_t * Gia_ManDemiterToDual( Gia_Man_t * p ); extern int Gia_ManDemiterDual( Gia_Man_t * p, Gia_Man_t ** pp0, Gia_Man_t ** pp1 ); extern int Gia_ManDemiterTwoWords( Gia_Man_t * p, Gia_Man_t ** pp0, Gia_Man_t ** pp1 ); extern void Gia_ManProdAdderGen( int nArgA, int nArgB, int Seed, int fSigned, int fCla ); +typedef struct Gia_ChMan_t_ Gia_ChMan_t; +extern Gia_ChMan_t * Gia_ManDupChoicesStart( Gia_Man_t * pGia ); +extern void Gia_ManDupChoicesAdd( Gia_ChMan_t * pMan, Gia_Man_t * pGia ); +extern Gia_Man_t * Gia_ManDupChoicesFinish( Gia_ChMan_t * pMan ); /*=== giaEdge.c ==========================================================*/ extern void Gia_ManEdgeFromArray( Gia_Man_t * p, Vec_Int_t * vArray ); extern Vec_Int_t * Gia_ManEdgeToArray( Gia_Man_t * p ); @@ -1507,6 +1513,7 @@ extern int Gia_ManHashAndMulti( Gia_Man_t * p, Vec_Int_t * vLits extern int Gia_ManHashAndMulti2( Gia_Man_t * p, Vec_Int_t * vLits ); extern int Gia_ManHashDualMiter( Gia_Man_t * p, Vec_Int_t * vOuts ); /*=== giaIf.c ===========================================================*/ +extern void Gia_ManPrintOutputLutStats( Gia_Man_t * p ); extern void Gia_ManPrintMappingStats( Gia_Man_t * p, char * pDumpFile ); extern void Gia_ManPrintPackingStats( Gia_Man_t * p ); extern void Gia_ManPrintLutStats( Gia_Man_t * p ); @@ -1719,6 +1726,7 @@ extern Gia_Man_t * Gia_ManUpdateExtraAig( void * pTime, Gia_Man_t * pAig extern Gia_Man_t * Gia_ManUpdateExtraAig2( void * pTime, Gia_Man_t * pAig, Vec_Int_t * vBoxesLeft ); extern Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * vBoxPres, int fSeq ); extern int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fSeq, int fDumpFiles, int fVerbose, char * pFileSpec ); +extern Vec_Int_t * Gia_ManDeriveBoxMapping( Gia_Man_t * pGia ); /*=== giaTruth.c ===========================================================*/ extern word Gia_LutComputeTruth6( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTruths ); extern word Gia_ObjComputeTruthTable6Lut( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTemp ); diff --git a/src/aig/gia/giaCut.c b/src/aig/gia/giaCut.c index 19d98c3be..61ce665a7 100644 --- a/src/aig/gia/giaCut.c +++ b/src/aig/gia/giaCut.c @@ -1168,6 +1168,46 @@ Vec_Ptr_t * Gia_ManMatchCutsMany( Vec_Mem_t * vTtMem, Vec_Int_t * vMap, int nFun return vRes; } +/**Function************************************************************* + + Synopsis [Function enumeration.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDumpCuts( Gia_Man_t * p, int nCutSize, int nCutNum, int fVerbose ) +{ + FILE * pFile = fopen( "input.txt", "wb" ); if ( !pFile ) return; + Gia_Sto_t * pSto = Gia_ManMatchCutsInt( p, nCutSize, nCutNum, 0 ); + Vec_Int_t * vLevel; int i, k, c, * pCut, nCuts = 0, nNodes = 0; + Vec_WecForEachLevel( pSto->vCuts, vLevel, i ) if ( Vec_IntSize(vLevel) ) { + if ( !Gia_ObjIsAnd(Gia_ManObj(p, i)) ) + continue; + Sdb_ForEachCut( Vec_IntArray(vLevel), pCut, k ) { + if ( pCut[0] == 1 ) + continue; + fprintf( pFile, "%d ", i ); + for ( c = 1; c <= pCut[0]; c++ ) + fprintf( pFile, "%d ", pCut[c] ); + fprintf( pFile, "1\n" ); + nCuts += pCut[0]; + nNodes++; + } + } + Gia_Obj_t * pObj; + Gia_ManForEachCo( p, pObj, i ) { + fprintf( pFile, "%d %d 0\n", Gia_ObjId(p, pObj), Gia_ObjFaninId0p(p, pObj) ); + } + fclose( pFile ); + Gia_StoFree( pSto ); + if ( fVerbose ) + printf( "Dumped %d cuts for %d nodes into file \"input.txt\".\n", nCuts, nNodes ); +} + /**Function************************************************************* Synopsis [Function enumeration.] diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 87f2bb74c..cca6f3d4c 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -22,6 +22,7 @@ #include "misc/tim/tim.h" #include "misc/vec/vecWec.h" #include "proof/cec/cec.h" +#include "misc/util/utilTruth.h" ABC_NAMESPACE_IMPL_START @@ -3250,6 +3251,50 @@ Gia_Man_t * Gia_ManDupAndOr( Gia_Man_t * p, int nOuts, int fUseOr, int fCompl ) return pNew; } +/**Function************************************************************* + + Synopsis [Computes the AND of all POs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupAndCare( Gia_Man_t * p, Gia_Man_t * pCare ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; int i; + assert( Gia_ManRegNum(p) == 0 ); + assert( Gia_ManRegNum(pCare) == 0 ); + assert( Gia_ManPiNum(p) == Gia_ManPiNum(pCare) ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + Gia_ManConst0(p)->Value = 0; + Gia_ManConst0(pCare)->Value = 0; + Gia_ManHashAlloc( pNew ); + Gia_ManForEachPi( p, pObj, i ) + pObj->Value = Gia_ManPi(pCare, i)->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachAnd( pCare, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( Gia_ManPoNum(pCare) == 1 ) { + Gia_ManForEachPo( p, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(Gia_ManPo(pCare, 0)) ) ); + } + else if ( Gia_ManPoNum(p) == Gia_ManPoNum(pCare) ) { + Gia_ManForEachPo( p, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(Gia_ManPo(pCare, i)) ) ); + } + else assert( 0 ); + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + /**Function************************************************************* Synopsis [Transforms output names.] @@ -5995,11 +6040,11 @@ Vec_Wec_t * Gia_ManCollectIntTfos( Gia_Man_t * p, Vec_Int_t * vVarNums ) } Gia_Man_t * Gia_ManDupCofs( Gia_Man_t * p, Vec_Int_t * vVarNums ) { - Vec_Int_t * vOutLits = Vec_IntStartFull( 1 << Vec_IntSize(vVarNums) ); + int i, iLit, nMints = 1 << Vec_IntSize(vVarNums); + Vec_Int_t * vOutLits = Vec_IntAlloc( nMints * Gia_ManCoNum(p) ); Vec_Wec_t * vTfos = Gia_ManCollectIntTfos( p, vVarNums ); - Gia_Man_t * pNew, * pTemp; - Gia_Obj_t * pObj, * pRoot = Gia_ManCo(p, 0); int i, iLit; - assert( Gia_ManPoNum(p) == 1 && Gia_ManRegNum(p) == 0 ); + Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; + assert( Gia_ManRegNum(p) == 0 ); pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); Gia_ManFillValue( p ); @@ -6011,16 +6056,18 @@ Gia_Man_t * Gia_ManDupCofs( Gia_Man_t * p, Vec_Int_t * vVarNums ) Gia_ManHashAlloc( pNew ); Gia_ManForEachAnd( p, pObj, i ) pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Vec_IntWriteEntry( vOutLits, 0, Gia_ObjFanin0Copy(pRoot) ); + Gia_ManForEachCo( p, pObj, i ) + Vec_IntPush( vOutLits, Gia_ObjFanin0Copy(pObj) ); int m, g, x, b = 0; - for ( m = 1; m < Vec_IntSize(vOutLits); m++ ) + for ( m = 1; m < nMints; m++ ) { g = m ^ (m >> 1); x = (b ^ g) == 1 ? 0 : Abc_Base2Log(b ^ g); b = g; Vec_Int_t * vNode = Vec_WecEntry( vTfos, x ); Gia_ManPi(p, Vec_IntEntry(vVarNums, x))->Value ^= 1; Gia_ManForEachObjVec( vNode, p, pObj, i ) pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Vec_IntWriteEntry( vOutLits, g, Gia_ObjFanin0Copy(pRoot) ); + Gia_ManForEachCo( p, pObj, i ) + Vec_IntPush( vOutLits, Gia_ObjFanin0Copy(pObj) ); } assert( Vec_IntFindMin(vOutLits) >= 0 ); Vec_IntForEachEntry( vOutLits, iLit, i ) @@ -6166,6 +6213,273 @@ void Gia_ManCofClassEnum( Gia_Man_t * p, int nVars ) Vec_IntFree( vIns ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ObjWhichFanout( Gia_Man_t * p, int iFanin, int iFanout ) +{ + int i, FanId; + Gia_ObjForEachFanoutStaticId( p, iFanin, FanId, i ) + if ( FanId == iFanout ) + return i; + assert( 0 ); + return -1; +} +Gia_Man_t * Gia_ManDupFanouts( Gia_Man_t * p ) +{ + assert( Gia_ManRegNum(p) == 0 ); + Gia_Man_t * pNew; Gia_Obj_t * pObj; int i, f, iLit[2]; + pNew = Gia_ManStart( Gia_ManObjNum(p)+100 ); + pNew->pName = Abc_UtilStrsav( p->pName ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + Gia_ManStaticFanoutStart( p ); + pNew->vNamesIn = Vec_PtrAlloc( 100 ); + pNew->vNamesOut = Vec_PtrAlloc( 100 ); + Gia_ManForEachPi( p, pObj, i ) { + pObj->Value = Gia_ManAppendCi(pNew); + Vec_PtrPush( pNew->vNamesIn, Gia_ObjCiName(p, i) ); + for ( f = 1; f < Gia_ObjFanoutNum(p, pObj); f++ ) { + Gia_ManAppendCi(pNew); + Vec_PtrPush( pNew->vNamesIn, Abc_UtilStrsavNum(Gia_ObjCiName(p, i), f) ); + } + } + Gia_ManForEachAnd( p, pObj, i ) { + iLit[0] = Gia_ObjFanin0Copy(pObj); + if ( Gia_ObjIsPi(p, Gia_ObjFanin0(pObj)) ) + iLit[0] += 2 * Gia_ObjWhichFanout(p, Gia_ObjFaninId0(pObj, i), i); + iLit[1] = Gia_ObjFanin1Copy(pObj); + if ( Gia_ObjIsPi(p, Gia_ObjFanin1(pObj)) ) + iLit[1] += 2 * Gia_ObjWhichFanout(p, Gia_ObjFaninId1(pObj, i), i); + pObj->Value = Gia_ManAppendAnd( pNew, iLit[0], iLit[1] ); + } + Gia_ManForEachPo( p, pObj, i ) { + iLit[0] = Gia_ObjFanin0Copy(pObj); + if ( Gia_ObjIsPi(p, Gia_ObjFanin0(pObj)) ) + iLit[0] += 2 * Gia_ObjWhichFanout(p, Gia_ObjFaninId0p(p, pObj), Gia_ObjId(p, pObj)); + Gia_ManAppendCo( pNew, iLit[0] ); + Vec_PtrPush( pNew->vNamesOut, Gia_ObjCoName(p, i) ); + } + Gia_ManStaticFanoutStop( p ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Reorders choice nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManPrintChoices( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; int i; + Gia_ManForEachAnd( p, pObj, i ) + if ( p->pSibls[i] ) + printf( "%d -> %d\n", i, p->pSibls[i] ); +} +void Gia_ManReorderChoices_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj ) +{ + if ( ~pObj->Value ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Gia_Obj_t * pSibl = Gia_ObjSiblObj(p, Gia_ObjId(p, pObj)); + Gia_ManReorderChoices_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManReorderChoices_rec( pNew, p, Gia_ObjFanin1(pObj) ); + if ( pSibl ) Gia_ManReorderChoices_rec( pNew, p, pSibl ); + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( pSibl ) { + int iObjNew = Abc_Lit2Var(pObj->Value); + int iNextNew = Abc_Lit2Var(pSibl->Value); + assert( iObjNew > iNextNew ); + assert( Gia_ObjIsAnd(Gia_ManObj(pNew, iNextNew)) ); + pNew->pSibls[iObjNew] = iNextNew; + } +} +Gia_Man_t * Gia_ManReorderChoices( Gia_Man_t * p ) +{ + assert( p->pSibls ); + Gia_Obj_t * pObj; int i; + Gia_Man_t * pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + pNew->pSibls = ABC_CALLOC( int, Gia_ManObjNum(p) ); + Gia_ManFillValue(p); + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi(pNew); + Gia_ManForEachCo( p, pObj, i ) + Gia_ManReorderChoices_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + extern int Gia_ManTestChoices( Gia_Man_t * p ); + Gia_ManTestChoices( pNew ); + //Gia_ManPrintChoices( pNew ); + return pNew; +} + + +/**Function************************************************************* + + Synopsis [Duplicates AIGs while creating choices.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +struct Gia_ChMan_t_ +{ + Gia_Man_t * pNew; + Vec_Mem_t * vTtMem; + Vec_Int_t * vSibls; + Vec_Int_t * vObj2Tt; + Vec_Int_t * vTt2Obj; + Vec_Int_t * vCoLits; + word * pTruth; + int nWords; +}; + +int Gia_ManDupChoicesMark_rec( Gia_Man_t * pGia, int iObj, Vec_Int_t * vObj2Tt, int iFunc ) +{ + if ( Abc_Lit2Var(Vec_IntEntry(vObj2Tt, iObj)) == iFunc ) + return 1; + if ( Gia_ObjIsTravIdCurrentId(pGia, iObj) ) + return 0; + Gia_ObjSetTravIdCurrentId(pGia, iObj); + Gia_Obj_t * pObj = Gia_ManObj(pGia, iObj); + if ( !Gia_ObjIsAnd(pObj) ) + return 0; + if ( Gia_ManDupChoicesMark_rec( pGia, Gia_ObjFaninId0(pObj, iObj), vObj2Tt, iFunc ) ) + return 1; + if ( Gia_ManDupChoicesMark_rec( pGia, Gia_ObjFaninId1(pObj, iObj), vObj2Tt, iFunc ) ) + return 1; + return 0; +} +int Gia_ManDupChoicesMark( Gia_Man_t * pGia, int iLit0, int iLit1, Vec_Int_t * vObj2Tt, int iFunc ) +{ + Gia_ManIncrementTravId( pGia ); + if ( Gia_ManDupChoicesMark_rec( pGia, Abc_Lit2Var(iLit0), vObj2Tt, iFunc ) ) + return 1; + if ( Gia_ManDupChoicesMark_rec( pGia, Abc_Lit2Var(iLit1), vObj2Tt, iFunc ) ) + return 1; + return 0; +} +void Gia_ManDupChoicesNode( Gia_ChMan_t * p, Gia_Man_t * pGia, int iObj ) +{ + Gia_Obj_t * pObj = Gia_ManObj( pGia, iObj ); + assert( ~Gia_ObjFanin0(pObj)->Value && ~Gia_ObjFanin1(pObj)->Value ); + int obLits[2] = { Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) }; + int ttLits[2] = { Vec_IntEntry(p->vObj2Tt, Abc_Lit2Var(obLits[0])), Vec_IntEntry(p->vObj2Tt, Abc_Lit2Var(obLits[1])) }; + int fCompl[2] = { Abc_LitIsCompl(ttLits[0]) ^ Abc_LitIsCompl(obLits[0]), Abc_LitIsCompl(ttLits[1]) ^ Abc_LitIsCompl(obLits[1]) }; + word * pTruth[2] = { Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(ttLits[0])), Vec_MemReadEntry(p->vTtMem, Abc_Lit2Var(ttLits[1])) }; + Abc_TtAndCompl( p->pTruth, pTruth[0], fCompl[0], pTruth[1], fCompl[1], p->nWords ); + int fComp = (int)p->pTruth[0] & 1; if ( fComp ) Abc_TtNot( p->pTruth, p->nWords ); + int nFuncs = Vec_MemEntryNum( p->vTtMem ); + int iFunc = Vec_MemHashInsert( p->vTtMem, p->pTruth ); + assert( iFunc <= nFuncs ); + if ( iFunc == nFuncs ) { // new function + pObj->Value = Gia_ManHashAnd( p->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Vec_IntPush( p->vObj2Tt, Abc_Var2Lit(iFunc, fComp ^ Abc_LitIsCompl(pObj->Value)) ); + Vec_IntPush( p->vTt2Obj, Abc_Lit2Var(pObj->Value) ); + return; + } + int iRepr = Vec_IntEntry( p->vTt2Obj, iFunc ); + pObj->Value = Abc_Var2Lit( iRepr, fComp ^ Abc_LitIsCompl(Vec_IntEntry(p->vObj2Tt, iRepr)) ); + if ( iRepr <= Gia_ManCiNum(pGia) || Gia_ManDupChoicesMark(p->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj), p->vObj2Tt, iFunc) ) + return; + int nObjNew = Gia_ManObjNum(p->pNew); + int iLitNew = Gia_ManHashAnd( p->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( Abc_Lit2Var(iLitNew) == nObjNew ) + Vec_IntPush( p->vObj2Tt, Abc_Var2Lit(iFunc, fComp ^ Abc_LitIsCompl(iLitNew)) ); +} +void Gia_ManDupChoicesAdd( Gia_ChMan_t * p, Gia_Man_t * pGia ) +{ + Gia_Obj_t * pObj; int i; + assert( Gia_ManCiNum(p->pNew) == Gia_ManCiNum(pGia) ); + assert( !p->vCoLits || Vec_IntSize(p->vCoLits) == Gia_ManCoNum(pGia) ); + assert( Gia_ManRegNum(p->pNew) == Gia_ManRegNum(pGia) ); + Gia_ManFillValue( pGia ); + Gia_ManForEachCi( pGia, pObj, i ) + pObj->Value = Gia_ManCiLit( p->pNew, i ); + Gia_ManForEachAnd( pGia, pObj, i ) + Gia_ManDupChoicesNode( p, pGia, i ); + assert( Vec_IntSize(p->vObj2Tt) == Gia_ManObjNum(p->pNew) ); + assert( Vec_IntSize(p->vTt2Obj) == Vec_MemEntryNum(p->vTtMem) ); +} +Gia_ChMan_t * Gia_ManDupChoicesStart( Gia_Man_t * pGia ) +{ + Gia_ChMan_t * p = ABC_CALLOC( Gia_ChMan_t, 1 ); + p->pNew = Gia_ManStart( 10*Gia_ManObjNum(pGia) ); + p->pNew->pName = Abc_UtilStrsav( pGia->pName ); + p->pNew->pSpec = Abc_UtilStrsav( pGia->pSpec ); + p->vTtMem = Vec_MemAllocWithTTs( Gia_ManCiNum(pGia) ); + p->vTt2Obj = Vec_IntStartNatural( 1 + Gia_ManCiNum(pGia) ); + p->vObj2Tt = Vec_IntAlloc( 10*Gia_ManObjNum(pGia) ); + p->nWords = Abc_TtWordNum( Gia_ManCiNum(pGia) ); + p->pTruth = ABC_CALLOC( word, p->nWords ); + Gia_Obj_t * pObj; int i; + for ( i = 0; i <= Gia_ManCiNum(pGia); i++ ) + Vec_IntPush( p->vObj2Tt, Abc_Var2Lit(i, 0) ); + Gia_ManForEachCi( pGia, pObj, i ) + Gia_ManAppendCi(p->pNew); + Gia_ManSetRegNum( p->pNew, Gia_ManRegNum(pGia) ); + Gia_ManHashStart( p->pNew ); + Gia_ManDupChoicesAdd( p, pGia ); + p->vCoLits = Vec_IntAlloc( Gia_ManCoNum(pGia) ); + Gia_ManForEachCo( pGia, pObj, i ) + Vec_IntPush( p->vCoLits, Gia_ObjFanin0Copy(pObj) ); + return p; +} +Vec_Int_t * Gia_ManDupChoicesCreateSibls( Gia_ChMan_t * p ) +{ + int iObj, ttLit; + Vec_Int_t * vSibls = Vec_IntStart( Gia_ManObjNum(p->pNew) ); + assert( Vec_IntSize(p->vTt2Obj) == Vec_MemEntryNum(p->vTtMem) ); + Vec_IntForEachEntry( p->vObj2Tt, ttLit, iObj ) { + int iPrev = Vec_IntEntry(p->vTt2Obj, Abc_Lit2Var(ttLit)); + assert( iPrev <= iObj ); + if ( iPrev == iObj ) + continue; + Vec_IntWriteEntry( vSibls, iPrev, iObj ); + Vec_IntWriteEntry( p->vTt2Obj, Abc_Lit2Var(ttLit), iObj ); + } + return vSibls; +} +Gia_Man_t * Gia_ManDupChoicesFinish( Gia_ChMan_t * p ) +{ + Gia_Man_t * pTemp, * pNew = p->pNew; int i, iLit; + p->vSibls = Gia_ManDupChoicesCreateSibls( p ); + p->pNew->pSibls = Vec_IntReleaseArray( p->vSibls ); + Vec_IntForEachEntry( p->vCoLits, iLit, i ) + Gia_ManAppendCo( p->pNew, iLit ); + Vec_MemFree( p->vTtMem ); + Vec_IntFree( p->vSibls ); + Vec_IntFree( p->vTt2Obj ); + Vec_IntFree( p->vObj2Tt ); + Vec_IntFree( p->vCoLits ); + ABC_FREE( p->pTruth ); + ABC_FREE( p ); + pTemp = Gia_ManReorderChoices( pNew ); + Gia_ManStop( pNew ); + return pTemp; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaGen.c b/src/aig/gia/giaGen.c index a807fe60f..088b64191 100644 --- a/src/aig/gia/giaGen.c +++ b/src/aig/gia/giaGen.c @@ -1360,6 +1360,130 @@ Gia_Man_t * Gia_ManGenSorter( int LogN ) return p; } +/**Function************************************************************* + + Synopsis [Generates brand-name adders.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManGenPrep( int nVars, int ** p ) +{ + int i, k; + for ( i = 0; i < nVars; i++ ) + for ( k = 0; k < nVars; k++ ) + p[i][k] = -1; +} +void Gia_ManGenSK( int nVars, int ** p ) +{ + int i, k, nBits = Abc_Base2Log(nVars); + for ( i = 0; i < nBits; i++ ) + for ( k = 0; k < nVars; k++ ) + if ( (k >> i) & 1 ) + p[i+1][k] = ((1 << i) - 1) | ((k >> (i+1)) << (i+1)); +} +void Gia_ManGenBK( int nVars, int ** p ) +{ + int i, k, nBits = Abc_Base2Log(nVars); + nVars = 1 << nBits; + for ( i = 1; i < nBits; i++ ) + for ( k = (1 << i) - 1; k < nVars; k += (1 << i) ) + p[i][k] = k - (1 << (i-1)); + p[nBits][nVars-1] = (1<<(nBits-1))-1; + for ( i = 1; i < nBits; i++ ) + for ( k = (1 << i) - 1; k < nVars-(1 << i); k += (1 << i) ) + p[2*nBits-1-i][nVars-1-k+((1<<(i-1))-1)] = nVars-1-k+((1<<(i-1))-1) - (1 << (i-1)); +} +void Gia_ManGenHC( int nVars, int ** p ) +{ + int i, k, nBits = Abc_Base2Log(nVars); + nVars = 1 << nBits; + for ( k = 1; k < nVars; k += 2 ) + p[1][k] = k - 1; + for ( i = 2; i <= nBits; i++ ) + for ( k = 1 + (1 << (i-1)); k < nVars; k += 2 ) + p[i][k] = k - (1 << (i-1)); + for ( k = 2; k < nVars; k += 2 ) + p[nBits+1][k] = k - 1; +} +void Gia_ManGenRca( int nVars, int ** p ) +{ + int i; + for ( i = 1; i < nVars; i++ ) + p[i][i] = i-1; +} +void Gia_ManGenPrint( int nVars, int ** p ) +{ + int i, k; + for ( i = nVars-1; i >= 0; i-- ) + printf( "%2d ", i ); + printf( "\n" ); + for ( i = 0; i < nVars; i++ ) { + for ( k = nVars-1; k >= 0; k-- ) + if ( p[i][k] >= 0 ) + break; + for ( k = nVars-1; k >= 0; k-- ) + if ( p[i][k] == -1 ) + printf( " - " ); + else + printf( "%2d ", p[i][k] ); + printf("\n"); + } +} +void Gia_ManGenPrefix( Gia_Man_t * pNew, int * p, int * g, int p2, int g2 ) +{ + *g = Gia_ManHashOr(pNew, *g, Gia_ManHashAnd(pNew, *p, g2)); + *p = Gia_ManHashAnd(pNew, *p, p2); +} +Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fCarries, int fVerbose ) +{ + extern void Wlc_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int * ps ); + int i, k, nBits = Abc_Base2Log(nVars), nVarsAlloc = (1 << nBits) + 2; + int ** pStore = (int **)Extra_ArrayAlloc( nVarsAlloc, nVarsAlloc, 4 ); + printf( "Generating %d-bit ", nVars ); + Gia_ManGenPrep( nVars+2, pStore ); + if ( fSK ) + Gia_ManGenSK( nVars, pStore ), printf("Sklansky "); + else if ( fBK ) + Gia_ManGenBK( nVars, pStore ), printf("Brent-Kung "); + else if ( fHC ) + Gia_ManGenHC( nVars, pStore ), printf("Huan-Carlsson "); + else + Gia_ManGenRca( nVars, pStore ), printf("ripple-carry "); + printf( "adder with%s carry-in and carry-out\n", fCarries ? "":"out" ); + if ( fVerbose ) Gia_ManGenPrint( nVars, pStore ); + Gia_Man_t * p = Gia_ManStart( 1000 ), * pTemp; + p->pName = Abc_UtilStrsav( "adder" ); + int * pLitsI = ABC_CALLOC( int, 2*nVars+10 ); + for ( k = 0; k < nVars; k++ ) + pLitsI[2*k] = Gia_ManAppendCi(p); + for ( k = 0; k < nVars; k++ ) + pLitsI[2*k+1] = Gia_ManAppendCi(p); + int Carry = fCarries ? Gia_ManAppendCi(p) : 0; + Gia_ManHashStart( p ); + for ( k = 0; k < nVars; k++ ) + Wlc_BlastFullAdder( p, pLitsI[2*k], pLitsI[2*k+1], k ? 0 : Carry, &pLitsI[2*k+1], &pLitsI[2*k] ); + int * pLits = ABC_CALLOC( int, 2*nVars+10 ); + memcpy( pLits, pLitsI, sizeof(int)*2*nVars ); + for ( i = 1; i < nVars; i++ ) + for ( k = 1; k < nVars; k++ ) + if ( pStore[i][k] >= 0 ) + Gia_ManGenPrefix( p, &pLits[2*k], &pLits[2*k+1], pLits[2*pStore[i][k]], pLits[2*pStore[i][k]+1] ); + for ( k = 0; k < nVars; k++ ) + Gia_ManAppendCo( p, k ? Gia_ManHashXor(p, pLitsI[2*k], pLits[2*(k-1)+1]) : pLitsI[2*k] ); + if ( fCarries ) + Gia_ManAppendCo( p, pLits[2*(k-1)+1] ); + ABC_FREE( pStore ); + ABC_FREE( pLitsI ); + ABC_FREE( pLits ); + p = Gia_ManCleanup( pTemp = p ); + Gia_ManStop( pTemp ); + return p; +} //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index c08a91ecd..d44a47102 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -470,6 +470,65 @@ int Gia_ManCountDupLut( Gia_Man_t * p ) return nCountDup + nCountPis; } +void Gia_ManCollectLuts_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vLuts ) +{ + if ( Gia_ObjIsTravIdCurrentId( p, iObj ) || !Gia_ObjIsAnd(Gia_ManObj(p, iObj)) ) + return; + Gia_ObjSetTravIdCurrentId( p, iObj ); + int k, iFan; + Gia_LutForEachFanin( p, iObj, iFan, k ) + Gia_ManCollectLuts_rec( p, iFan, vLuts ); + Vec_IntPush( vLuts, iObj ); +} +int Gia_ManCountLutLevels( Gia_Man_t * p, Vec_Int_t * vLuts, Vec_Int_t * vLevel ) +{ + int i, iObj, k, iFan, LevelMax = 0; + Vec_IntForEachEntry( vLuts, iObj, i ) { + int Level = 0; + Gia_LutForEachFanin( p, iObj, iFan, k ) + Level = Abc_MaxInt( Level, Vec_IntEntry(vLevel, iFan) ); + Vec_IntWriteEntry( vLevel, iObj, Level+1 ); + LevelMax = Abc_MaxInt( LevelMax, Level+1 ); + } + Vec_IntForEachEntry( vLuts, iObj, i ) + Vec_IntWriteEntry( vLevel, iObj, 0 ); + return LevelMax; +} +void Gia_ManPrintOutputLutStats( Gia_Man_t * p ) +{ + int Limit = 100000; + int nLutSize = Gia_ManLutSizeMax(p); + Vec_Int_t * vLuts = Vec_IntAlloc( 1000 ); + Vec_Int_t * vNodes = Vec_IntStart( Limit ); + Vec_Int_t * vLevels = Vec_IntStart( Limit ); + Vec_Int_t * vLevel = Vec_IntStart( Gia_ManObjNum(p) ); + int i, DriverId, Value, nTotalLuts = 0; + Gia_ManForEachCoDriverId( p, DriverId, i ) { + Vec_IntClear( vLuts ); + Gia_ManIncrementTravId(p); + Gia_ManCollectLuts_rec( p, DriverId, vLuts ); + if ( Vec_IntSize(vLuts) < Limit ) + Vec_IntAddToEntry( vNodes, Vec_IntSize(vLuts), 1 ); + int Level = Gia_ManCountLutLevels( p, vLuts, vLevel ); + if ( Level < Limit ) + Vec_IntAddToEntry( vLevels, Level, 1 ); + nTotalLuts += Vec_IntSize(vLuts); + } + printf( "Level count statistics for %d AIG outputs:\n", Gia_ManCoNum(p) ); + Vec_IntForEachEntry( vLevels, Value, i ) + if ( Value ) + printf( " %2d level : Function count = %8d (%6.2f %%)\n", i, Value, 100.0*Value/Gia_ManCoNum(p) ); + printf( "LUT count statistics for %d AIG outputs:\n", Gia_ManCoNum(p) ); + Vec_IntForEachEntry( vNodes, Value, i ) + if ( Value ) + printf( " %2d LUT%d : Function count = %8d (%6.2f %%)\n", i, nLutSize, Value, 100.0*Value/Gia_ManCoNum(p) ); + printf( "Sum total of LUT counts for all outputs = %d. Shared LUT count = %d.\n", nTotalLuts, Gia_ManLutNum(p) ); + Vec_IntFree( vLuts ); + Vec_IntFree( vNodes ); + Vec_IntFree( vLevels ); + Vec_IntFree( vLevel ); +} + void Gia_ManPrintMappingStats( Gia_Man_t * p, char * pDumpFile ) { int fDisable2Lut = 1; diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index d0af551b0..2f271e35c 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -474,6 +474,7 @@ void Gia_ManLogAigStats( Gia_Man_t * p, char * pDumpFile ) fprintf( pTable, " \"name\" : \"%s\",\n", p->pName ); fprintf( pTable, " \"input\" : %d,\n", Gia_ManCiNum(p) ); fprintf( pTable, " \"output\" : %d,\n", Gia_ManCoNum(p) ); + fprintf( pTable, " \"flop\" : %d,\n", Gia_ManRegNum(p) ); fprintf( pTable, " \"and\" : %d,\n", Gia_ManAndNum(p) ); fprintf( pTable, " \"level\" : %d\n", Gia_ManLevelNum(p) ); fprintf( pTable, "}\n" ); @@ -639,6 +640,8 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars ) } if ( pPars && pPars->fSlacks ) Gia_ManDfsSlacksPrint( p ); + if ( Gia_ManHasMapping(p) && pPars->fMapOutStats ) + Gia_ManPrintOutputLutStats( p ); } /**Function************************************************************* diff --git a/src/aig/gia/giaMini.c b/src/aig/gia/giaMini.c index 5ebedfb78..e20f700e8 100644 --- a/src/aig/gia/giaMini.c +++ b/src/aig/gia/giaMini.c @@ -560,6 +560,7 @@ int * Abc_FrameGiaOutputMiniLutObj( Abc_Frame_t * pAbc ) int * pRes = NULL; if ( pAbc == NULL ) printf( "ABC framework is not initialized by calling Abc_Start()\n" ); + pAbc->vMiniLutObjs = Gia_ManDeriveBoxMapping( Abc_FrameReadGia( pAbc ) ); if ( pAbc->vMiniLutObjs == NULL ) printf( "MiniLut objects are not defined.\n" ); pRes = Vec_IntReleaseArray( pAbc->vMiniLutObjs ); diff --git a/src/aig/gia/giaNf.c b/src/aig/gia/giaNf.c index 8bcf76b33..b38093f23 100644 --- a/src/aig/gia/giaNf.c +++ b/src/aig/gia/giaNf.c @@ -2161,6 +2161,90 @@ void Nf_ManFixPoDrivers( Nf_Man_t * p ) //printf( "Fixed %d PO drivers.\n", Count ); } +/**Function************************************************************* + + Synopsis [Dump matches.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Nf_ManDumpMatches( Nf_Man_t * p ) +{ + FILE * pFile = fopen( p->pPars->ZFile, "wb" ); + Gia_Obj_t * pObj; int n, iObj; + // output matches + Gia_ManForEachCi( p->pGia, pObj, n ) + fprintf( pFile, "%d input %.2f\n", Abc_Var2Lit(Gia_ObjId(p->pGia, pObj), 0), 0.0 ); + Gia_ManForEachAnd( p->pGia, pObj, iObj ) { + assert( !Gia_ObjIsBuf(pObj) ); + for ( n = 0; n < 2; n++ ) { + int c, * pCut, * pCutSet = Nf_ObjCutSet( p, iObj ); + Nf_SetForEachCut( pCutSet, pCut, c ) { + if ( Abc_Lit2Var(Nf_CutFunc(pCut)) >= Vec_WecSize(p->vTt2Match) ) + continue; + assert( !Nf_CutIsTriv(pCut, iObj) ); + assert( Nf_CutSize(pCut) <= p->pPars->nLutSize ); + assert( Abc_Lit2Var(Nf_CutFunc(pCut)) < Vec_WecSize(p->vTt2Match) ); + int iFuncLit = Nf_CutFunc(pCut); + int fComplExt = Abc_LitIsCompl(iFuncLit); + Vec_Int_t * v = Vec_WecEntry( p->vTt2Match, Abc_Lit2Var(iFuncLit) ); + int j, k, Info, Offset, iFanin, fComplF; + Vec_IntForEachEntryDouble( v, Info, Offset, j ) { + Nf_Cfg_t Cfg = Nf_Int2Cfg(Offset); + int fCompl = Cfg.fCompl ^ fComplExt; + if ( fCompl != n ) + continue; + Mio_Cell2_t*pC = Nf_ManCell( p, Info ); + assert( Nf_CutSize(pCut) == (int)pC->nFanins ); + fprintf( pFile, "%d ", Abc_Var2Lit(iObj, n) ); + fprintf( pFile, "%s ", pC->pName ); + fprintf( pFile, "%.2f", pC->AreaF ); + Nf_CutForEachVarCompl( pCut, Cfg, iFanin, fComplF, k ) + fprintf( pFile, " %d", Abc_Var2Lit(iFanin, fComplF) ); + fprintf( pFile, "\n" ); + } + } + } + } + Gia_ManForEachCo( p->pGia, pObj, n ) + fprintf( pFile, "%d output %.2f %d\n", Abc_Var2Lit(Gia_ObjId(p->pGia, pObj), 0), 0.0, Gia_ObjFaninLit0p(p->pGia, pObj) ); + // output levels + extern int Gia_ManChoiceLevel( Gia_Man_t * p ); + int LevelMax = Gia_ManChoiceLevel( p->pGia ); + Gia_ManForEachCiId( p->pGia, iObj, n ) + fprintf( pFile, "L%d %d\n", Abc_Var2Lit(iObj, 0), 0 ); + Gia_ManForEachAnd( p->pGia, pObj, iObj ) + fprintf( pFile, "L%d %d\n", Abc_Var2Lit(iObj, 0), Gia_ObjLevelId(p->pGia, iObj) ); + Gia_ManForEachCoId( p->pGia, iObj, n ) + fprintf( pFile, "L%d %d\n", Abc_Var2Lit(iObj, 0), LevelMax+1 ); + // output mapping + Gia_ManForEachCiId( p->pGia, iObj, n ) + if ( Nf_ObjMapRefNum(p, iObj, 1) ) + fprintf( pFile, "M%d %s %.2f %d\n", Abc_Var2Lit(iObj, 1), p->pCells[3].pName, p->pCells[3].AreaF, Abc_Var2Lit(iObj, 0) ); + Gia_ManForEachAnd( p->pGia, pObj, iObj ) + for ( n = 0; n < 2; n++ ) + if ( Nf_ObjMapRefNum(p, iObj, n) ) { + Nf_Mat_t * pM = Nf_ObjMatchBest(p, iObj, n); + if ( pM->fCompl ) { + fprintf( pFile, "M%d %s %.2f %d\n", Abc_Var2Lit(iObj, n), p->pCells[3].pName, p->pCells[3].AreaF, Abc_Var2Lit(iObj, !n) ); + continue; + } + int k, iVar, fCompl, * pCut = Nf_CutFromHandle( Nf_ObjCutSet(p, iObj), pM->CutH ); + Mio_Cell2_t*pC = Nf_ManCell( p, pM->Gate ); + fprintf( pFile, "M%d ", Abc_Var2Lit(iObj, n) ); + fprintf( pFile, "%s ", pC->pName ); + fprintf( pFile, "%.2f", pC->AreaF ); + Nf_CutForEachVarCompl( pCut, pM->Cfg, iVar, fCompl, k ) + fprintf( pFile, " %d", Abc_Var2Lit(iVar, fCompl) ); + fprintf( pFile, "\n" ); + } + fclose( pFile ); +} + /**Function************************************************************* Synopsis [Deriving mapping.] @@ -2216,6 +2300,8 @@ Gia_Man_t * Nf_ManDeriveMapping( Nf_Man_t * p ) } // assert( Vec_IntCap(vMapping) == 16 || Vec_IntSize(vMapping) == Vec_IntCap(vMapping) ); p->pGia->vCellMapping = vMapping; + if ( p->pPars->ZFile ) + Nf_ManDumpMatches( p ); return p->pGia; } void Nf_ManUpdateStats( Nf_Man_t * p ) diff --git a/src/aig/gia/giaRrr.cpp b/src/aig/gia/giaRrr.cpp index 1eccd4dc2..8483641b2 100644 --- a/src/aig/gia/giaRrr.cpp +++ b/src/aig/gia/giaRrr.cpp @@ -35,7 +35,7 @@ Gia_Man_t *Gia_ManRrr(Gia_Man_t *pGia, int iSeed, int nWords, int nTimeout, int Par.fOptOnInsert = fOptOnInsert; Par.fGreedy = fGreedy; rrr::Perform(&ntk, &Par); - Gia_Man_t *pNew = rrr::CreateGia(&ntk); + Gia_Man_t *pNew = rrr::CreateGia(&ntk, false); return pNew; } diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c index b5c3c0802..734d9359b 100644 --- a/src/aig/gia/giaSimBase.c +++ b/src/aig/gia/giaSimBase.c @@ -288,6 +288,21 @@ void Gia_ManSimPatWrite( char * pFileName, Vec_Wrd_t * vSimsIn, int nWords ) SeeAlso [] ***********************************************************************/ +Vec_Wrd_t * Gia_ManDeriveNodeFuncs( Gia_Man_t * p ) +{ + int nWords = Abc_Truth6WordNum( Gia_ManCiNum(p) ); + Vec_Wrd_t * vSims = Vec_WrdStart( nWords * Gia_ManObjNum(p) ); + Gia_Obj_t * pObj; int i; + Gia_ManForEachCi( p, pObj, i ) + assert( Gia_ObjId(p, pObj) == i+1 ); + Vec_Ptr_t * vTruths = Vec_PtrAllocTruthTables( Gia_ManCiNum(p) ); + Gia_ManForEachCi( p, pObj, i ) + Abc_TtCopy( Vec_WrdEntryP(vSims, nWords*(i+1)), (word *)Vec_PtrEntry(vTruths, i), nWords, 0 ); + Vec_PtrFree( vTruths ); + Gia_ManForEachAnd( p, pObj, i ) + Gia_ManSimPatSimAnd( p, i, pObj, nWords, vSims ); + return vSims; +} word * Gia_ManDeriveFuncs( Gia_Man_t * p ) { int nVars2 = (Gia_ManCiNum(p) + 6)/2; diff --git a/src/aig/gia/giaStoch.c b/src/aig/gia/giaStoch.c index 68e23019e..c88bdae6b 100644 --- a/src/aig/gia/giaStoch.c +++ b/src/aig/gia/giaStoch.c @@ -80,8 +80,9 @@ Gia_Man_t * Gia_StochProcessSingle( Gia_Man_t * p, char * pScript, int Rand, int } return pNew; } -void Gia_StochProcessArray( Vec_Ptr_t * vGias, char * pScript, int TimeSecs, int fVerbose ) +Vec_Int_t * Gia_StochProcessArray( Vec_Ptr_t * vGias, char * pScript, int TimeSecs, int fVerbose ) { + Vec_Int_t * vGains = Vec_IntStartFull( Vec_PtrSize(vGias) ); Gia_Man_t * pGia, * pNew; int i; Vec_Int_t * vRands = Vec_IntAlloc( Vec_PtrSize(vGias) ); Abc_Random(1); @@ -90,10 +91,12 @@ void Gia_StochProcessArray( Vec_Ptr_t * vGias, char * pScript, int TimeSecs, int Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i ) { pNew = Gia_StochProcessSingle( pGia, pScript, Vec_IntEntry(vRands, i), TimeSecs ); + Vec_IntWriteEntry( vGains, i, Gia_ManAndNum(pGia) - Gia_ManAndNum(pNew) ); Gia_ManStop( pGia ); Vec_PtrWriteEntry( vGias, i, pNew ); } Vec_IntFree( vRands ); + return vGains; } /**Function************************************************************* @@ -165,14 +168,14 @@ int Gia_StochProcess1( void * p ) return 1; } -void Gia_StochProcess( Vec_Ptr_t * vGias, char * pScript, int nProcs, int TimeSecs, int fVerbose ) +Vec_Int_t * Gia_StochProcess( Vec_Ptr_t * vGias, char * pScript, int nProcs, int TimeSecs, int fVerbose ) { if ( nProcs <= 2 ) { if ( fVerbose ) printf( "Running non-concurrent synthesis.\n" ), fflush(stdout); - Gia_StochProcessArray( vGias, pScript, TimeSecs, fVerbose ); - return; + return Gia_StochProcessArray( vGias, pScript, TimeSecs, fVerbose ); } + Vec_Int_t * vGains = Vec_IntStartFull( Vec_PtrSize(vGias) ); StochSynData_t * pData = ABC_CALLOC( StochSynData_t, Vec_PtrSize(vGias) ); Vec_Ptr_t * vData = Vec_PtrAlloc( Vec_PtrSize(vGias) ); Gia_Man_t * pGia; int i; @@ -190,11 +193,13 @@ void Gia_StochProcess( Vec_Ptr_t * vGias, char * pScript, int nProcs, int TimeSe Util_ProcessThreads( Gia_StochProcess1, vData, nProcs, TimeSecs, fVerbose ); // replace old AIGs by new AIGs Vec_PtrForEachEntry( Gia_Man_t *, vGias, pGia, i ) { + Vec_IntWriteEntry( vGains, i, Gia_ManAndNum(pGia) - Gia_ManAndNum(pData[i].pOut) ); Gia_ManStop( pGia ); Vec_PtrWriteEntry( vGias, i, pData[i].pOut ); } Vec_PtrFree( vData ); ABC_FREE( pData ); + return vGains; } /**Function************************************************************* @@ -279,6 +284,428 @@ void Gia_ManStochSynthesis( Vec_Ptr_t * vAigs, char * pScript ) } } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ManFilterPartitions( Gia_Man_t * p, Vec_Ptr_t * vvIns, Vec_Ptr_t * vvNodes, Vec_Ptr_t * vvOuts, Vec_Ptr_t * vWins, Vec_Int_t * vGains ) +{ + int RetValue = Vec_PtrSize(vvIns); + Vec_Ptr_t * vvInsNew = Vec_PtrAlloc( 10 ); + Vec_Ptr_t * vvOutsNew = Vec_PtrAlloc( 10 ); + Vec_Ptr_t * vvWinsNew = Vec_PtrAlloc( 10 ); + Gia_ManIncrementTravId( p ); + while ( 1 ) { + int i, Gain, iEntry = Vec_IntArgMax(vGains); + if ( iEntry == -1 || Vec_IntEntry(vGains, iEntry) < 0 ) + break; + //printf( "Selecting partition %d with gain %d.\n", iEntry, Vec_IntEntry(vGains, iEntry) ); + Vec_IntWriteEntry( vGains, iEntry, -1 ); + Vec_PtrPush( vvInsNew, Vec_IntDup((Vec_Int_t *)Vec_PtrEntry(vvIns, iEntry)) ); + Vec_PtrPush( vvOutsNew, Vec_IntDup((Vec_Int_t *)Vec_PtrEntry(vvOuts, iEntry)) ); + Vec_PtrPush( vvWinsNew, Gia_ManDupDfs((Gia_Man_t *)Vec_PtrEntry(vWins, iEntry)) ); + extern void Gia_ManMarkTfiTfo( Vec_Int_t * vOne, Gia_Man_t * pMan ); + Gia_ManMarkTfiTfo( (Vec_Int_t *)Vec_PtrEntryLast(vvInsNew), p ); + Vec_IntForEachEntry( vGains, Gain, i ) { + if ( Gain < 0 ) + continue; + Vec_Int_t * vNodes = (Vec_Int_t *)Vec_PtrEntry(vvNodes, i); + Gia_Obj_t * pNode; int j; + Gia_ManForEachObjVec( vNodes, p, pNode, j ) + if ( Gia_ObjIsTravIdCurrent(p, pNode) ) + break; + if ( j < Vec_IntSize(vNodes) ) + Vec_IntWriteEntry( vGains, i, -1 ); + } + } + ABC_SWAP( Vec_Ptr_t, *vvInsNew, *vvIns ); + ABC_SWAP( Vec_Ptr_t, *vvOutsNew, *vvOuts ); + ABC_SWAP( Vec_Ptr_t, *vvWinsNew, *vWins ); + Vec_PtrFreeFunc( vvInsNew, (void (*)(void *)) Vec_IntFree ); + Vec_PtrFreeFunc( vvOutsNew, (void (*)(void *)) Vec_IntFree ); + Vec_PtrFreeFunc( vvWinsNew, (void (*)(void *)) Gia_ManStop ); + return RetValue; +} + +/**Function************************************************************* + + Synopsis [Partitioning.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ObjDfsMark_rec( Gia_Man_t * pGia, Gia_Obj_t * pObj ) +{ + assert( !pObj->fMark0 ); + if ( Gia_ObjIsTravIdCurrent( pGia, pObj ) ) + return; + Gia_ObjSetTravIdCurrent( pGia, pObj ); + if ( Gia_ObjIsCi(pObj) ) + return; + assert( Gia_ObjIsAnd(pObj) ); + Gia_ObjDfsMark_rec( pGia, Gia_ObjFanin0(pObj) ); + Gia_ObjDfsMark_rec( pGia, Gia_ObjFanin1(pObj) ); +} +void Gia_ObjDfsMark2_rec( Gia_Man_t * pGia, Gia_Obj_t * pObj ) +{ + Gia_Obj_t * pFanout; int i; + assert( !pObj->fMark0 ); + if ( Gia_ObjIsTravIdCurrent( pGia, pObj ) ) + return; + Gia_ObjSetTravIdCurrent( pGia, pObj ); + Gia_ObjForEachFanoutStatic( pGia, pObj, pFanout, i ) + Gia_ObjDfsMark2_rec( pGia, pFanout ); +} +Vec_Int_t * Gia_ManDeriveWinNodes( Gia_Man_t * pMan, Vec_Int_t * vIns, Vec_Wec_t * vStore ) +{ + Vec_Int_t * vLevel, * vNodes = Vec_IntAlloc( 100 ); + Gia_Obj_t * pObj, * pNext; int i, k, iLevel; + Vec_WecForEachLevel( vStore, vLevel, i ) + Vec_IntClear( vLevel ); + // mark the TFI cones of the inputs + Gia_ManIncrementTravId( pMan ); + Gia_ManForEachObjVec( vIns, pMan, pObj, i ) + Gia_ObjDfsMark_rec( pMan, pObj ); + // add unrelated fanouts of the inputs to storage + Gia_ManForEachObjVec( vIns, pMan, pObj, i ) + Gia_ObjForEachFanoutStatic( pMan, pObj, pNext, k ) + if ( Gia_ObjIsAnd(pNext) && !Gia_ObjIsTravIdCurrent(pMan, pNext) && !pNext->fMark0 ) { + pNext->fMark0 = 1; + Vec_WecPush( vStore, Gia_ObjLevel(pMan, pNext), Gia_ObjId(pMan, pNext) ); + } + // mark the inputs + Gia_ManIncrementTravId( pMan ); + Gia_ManForEachObjVec( vIns, pMan, pObj, i ) + Gia_ObjSetTravIdCurrent(pMan, pObj); + // collect those fanouts that are completely supported by the inputs + Vec_WecForEachLevel( vStore, vLevel, iLevel ) + Gia_ManForEachObjVec( vLevel, pMan, pObj, i ) { + assert( !Gia_ObjIsTravIdCurrent(pMan, pObj) ); + assert( pObj->fMark0 ); + pObj->fMark0 = 0; + if ( !Gia_ObjIsTravIdCurrent(pMan, Gia_ObjFanin0(pObj)) || + !Gia_ObjIsTravIdCurrent(pMan, Gia_ObjFanin1(pObj)) ) + continue; + Gia_ObjSetTravIdCurrent(pMan, pObj); + Vec_IntPush( vNodes, Gia_ObjId(pMan, pObj) ); + assert( Gia_ObjIsAnd(pObj) ); + // add fanouts of this node to storage + Gia_ObjForEachFanoutStatic( pMan, pObj, pNext, k ) + if ( Gia_ObjIsAnd(pNext) && !Gia_ObjIsTravIdCurrent(pMan, pNext) && !pNext->fMark0 ) { + pNext->fMark0 = 1; + assert( Gia_ObjLevel(pMan, pNext) > iLevel ); + Vec_WecPush( vStore, Gia_ObjLevel(pMan, pNext), Gia_ObjId(pMan, pNext) ); + } + } + Vec_IntSort( vNodes, 0 ); + return vNodes; +} +Vec_Ptr_t * Gia_ManDeriveWinNodesAll( Gia_Man_t * pMan, Vec_Ptr_t * vvIns, Vec_Wec_t * vStore ) +{ + Vec_Int_t * vIns; int i; + Vec_Ptr_t * vvNodes = Vec_PtrAlloc( Vec_PtrSize(vvIns) ); + Vec_PtrForEachEntry( Vec_Int_t *, vvIns, vIns, i ) + Vec_PtrPush( vvNodes, Gia_ManDeriveWinNodes(pMan, vIns, vStore) ); + return vvNodes; +} +Vec_Int_t * Gia_ManDeriveWinOuts( Gia_Man_t * pMan, Vec_Int_t * vNodes ) +{ + Vec_Int_t * vOuts = Vec_IntAlloc( 100 ); + Gia_Obj_t * pObj, * pNext; int i, k; + // mark the nodes in the window + Gia_ManIncrementTravId( pMan ); + Gia_ManForEachObjVec( vNodes, pMan, pObj, i ) + Gia_ObjSetTravIdCurrent(pMan, pObj); + // collect nodes that have unmarked fanouts + Gia_ManForEachObjVec( vNodes, pMan, pObj, i ) { + Gia_ObjForEachFanoutStatic( pMan, pObj, pNext, k ) + if ( !Gia_ObjIsTravIdCurrent(pMan, pNext) ) + break; + if ( k < Gia_ObjFanoutNum(pMan, pObj) ) + Vec_IntPush( vOuts, Gia_ObjId(pMan, pObj) ); + } + if ( Vec_IntSize(vOuts) == 0 ) + printf( "Window with %d internal nodes has no outputs (are these dangling nodes?).\n", Vec_IntSize(vNodes) ); + return vOuts; +} +Vec_Ptr_t * Gia_ManDeriveWinOutsAll( Gia_Man_t * pMan, Vec_Ptr_t * vvNodes ) +{ + Vec_Int_t * vNodes; int i; + Vec_Ptr_t * vvOuts = Vec_PtrAlloc( Vec_PtrSize(vvNodes) ); + Vec_PtrForEachEntry( Vec_Int_t *, vvNodes, vNodes, i ) + Vec_PtrPush( vvOuts, Gia_ManDeriveWinOuts(pMan, vNodes) ); + return vvOuts; +} +void Gia_ManPermuteLevel( Gia_Man_t * pMan, int Level ) +{ + Gia_Obj_t * pObj, * pNext; int i, k; + Gia_ManForEachAnd( pMan, pObj, i ) { + int LevelMin = Gia_ObjLevel(pMan, pObj), LevelMax = Level + 1; + Gia_ObjForEachFanoutStatic( pMan, pObj, pNext, k ) + if ( Gia_ObjIsAnd(pNext) ) + LevelMax = Abc_MinInt( LevelMax, Gia_ObjLevel(pMan, pNext) ); + if ( LevelMin == LevelMax ) continue; + assert( LevelMin < LevelMax ); + // randomly set level between LevelMin and LevelMax-1 + Gia_ObjSetLevel( pMan, pObj, LevelMin + (Abc_Random(0) % (LevelMax - LevelMin)) ); + assert( Gia_ObjLevel(pMan, pObj) < LevelMax ); + } +} +Vec_Int_t * Gia_ManCollectObjectsPointedTo( Gia_Man_t * pMan, int Level ) +{ + Vec_Int_t * vRes = Vec_IntAlloc( 100 ); + Gia_Obj_t * pObj, * pFanin; int i, n; + Gia_ManIncrementTravId( pMan ); + Gia_ManForEachAnd( pMan, pObj, i ) { + if ( Gia_ObjLevel(pMan, pObj) <= Level ) + continue; + for ( n = 0; n < 2; n++ ) { + Gia_Obj_t * pFanin = n ? Gia_ObjFanin1(pObj) : Gia_ObjFanin0(pObj); + if ( Gia_ObjLevel(pMan, pFanin) <= Level && !Gia_ObjIsTravIdCurrent(pMan, pFanin) ) { + Gia_ObjSetTravIdCurrent(pMan, pFanin); + Vec_IntPush( vRes, Gia_ObjId(pMan, pFanin) ); + } + } + } + Gia_ManForEachCo( pMan, pObj, i ) { + pFanin = Gia_ObjFanin0(pObj); + if ( Gia_ObjLevel(pMan, pFanin) <= Level && !Gia_ObjIsTravIdCurrent(pMan, pFanin) && Gia_ObjIsAnd(pFanin) ) { + Gia_ObjSetTravIdCurrent(pMan, pFanin); + Vec_IntPush( vRes, Gia_ObjId(pMan, pFanin) ); + } + } + Vec_IntSort( vRes, 0 ); + return vRes; +} +Vec_Wec_t * Gia_ManCollectObjectsWithSuppLimit( Gia_Man_t * pMan, int Level, int nSuppMax ) +{ + Vec_Wec_t * vResSupps = NULL; + Vec_Int_t * vBelow = Gia_ManCollectObjectsPointedTo( pMan, Level ); + Vec_Wec_t * vSupps = Vec_WecStart( Vec_IntSize(vBelow) ); + Vec_Int_t * vSuppIds = Vec_IntStartFull( Gia_ManObjNum(pMan) ); + Vec_Int_t * vTemp = Vec_IntAlloc(100); + Gia_Obj_t * pObj; int i, Count = 0; + Gia_ManForEachObjVec( vBelow, pMan, pObj, i ) { + Vec_IntWriteEntry( vSuppIds, Gia_ObjId(pMan, pObj), i ); + Vec_IntPush( Vec_WecEntry(vSupps, i), Gia_ObjId(pMan, pObj) ); + } + Gia_ManForEachAnd( pMan, pObj, i ) { + if ( Gia_ObjLevel(pMan, pObj) <= Level ) + continue; + int iSuppId0 = Vec_IntEntry( vSuppIds, Gia_ObjFaninId0(pObj, i) ); + int iSuppId1 = Vec_IntEntry( vSuppIds, Gia_ObjFaninId1(pObj, i) ); + if ( iSuppId0 == -1 || iSuppId1 == -1 ) { + Count++; + continue; + } + Vec_IntClear( vTemp ); + Vec_IntTwoMerge2( Vec_WecEntry(vSupps, iSuppId0), Vec_WecEntry(vSupps, iSuppId1), vTemp ); + if ( Vec_IntSize(vTemp) > nSuppMax ) { + Count++; + continue; + } + Vec_IntWriteEntry( vSuppIds, i, Vec_WecSize(vSupps) ); + Vec_IntAppend( Vec_WecPushLevel(vSupps), vTemp ); + } + // remove those supported nodes that are in the TFI cones of others + Gia_ManIncrementTravId( pMan ); + Gia_ManForEachAnd( pMan, pObj, i ) + if ( Gia_ObjLevel(pMan, pObj) > Level && Vec_IntEntry(vSuppIds, i) >= 0 && !Gia_ObjIsTravIdCurrent(pMan, pObj) ) { + Gia_ObjDfsMark_rec(pMan, pObj); + Gia_ObjSetTravIdPrevious(pMan, pObj); + } + // create the result + vResSupps = Vec_WecAlloc( 100 ); + Gia_ManForEachAnd( pMan, pObj, i ) + if ( Gia_ObjLevel(pMan, pObj) > Level && Vec_IntEntry(vSuppIds, i) >= 0 && !Gia_ObjIsTravIdCurrent(pMan, pObj) ) { + Vec_Int_t * vSupp = Vec_WecEntry( vSupps, Vec_IntEntry(vSuppIds, i) ); + if ( Vec_IntSize(vSupp) < 4 ) + continue; + Vec_Int_t * vThis = Vec_WecPushLevel( vResSupps ); + Vec_IntGrow( vThis, Vec_IntSize(vSupp) + 1 ); + Vec_IntAppend( vThis, vSupp ); + //Vec_IntPush( vThis, Gia_ObjId(pObj) ); + } + //printf( "Inputs = %d. Nodes with %d-support = %d. Nodes with larger support = %d. Selected outputs = %d.\n", + // Vec_IntSize(vBelow), nSuppMax, Vec_WecSize(vSupps), Count, Vec_WecSize(vResSupps) ); + Vec_WecFree( vSupps ); + Vec_IntFree( vSuppIds ); + Vec_IntFree( vBelow ); + Vec_IntFree( vTemp ); + return vResSupps; +} +// removes all supports that overlap with this one +void Gia_ManSelectRemove( Vec_Wec_t * vSupps, Vec_Int_t * vOne ) +{ + Vec_Int_t * vLevel; int i; + Vec_WecForEachLevel( vSupps, vLevel, i ) + if ( Vec_IntTwoCountCommon(vLevel, vOne) > 0 ) + Vec_IntClear( vLevel ); + Vec_WecRemoveEmpty( vSupps ); +} +// marks TFI/TFO of this one +void Gia_ManMarkTfiTfo( Vec_Int_t * vOne, Gia_Man_t * pMan ) +{ + int i; Gia_Obj_t * pObj; + Gia_ManForEachObjVec( vOne, pMan, pObj, i ) { + //Gia_ObjSetTravIdPrevious(pMan, pObj); + //Gia_ObjDfsMark_rec( pMan, pObj ); + Gia_ObjSetTravIdPrevious(pMan, pObj); + Gia_ObjDfsMark2_rec( pMan, pObj ); + } +} +// removes all supports that overlap with the TFI/TFO cones of this one +void Gia_ManSelectRemove2( Vec_Wec_t * vSupps, Vec_Int_t * vOne, Gia_Man_t * pMan ) +{ + Vec_Int_t * vLevel; int i, k; Gia_Obj_t * pObj; + Gia_ManForEachObjVec( vOne, pMan, pObj, i ) { + Gia_ObjSetTravIdPrevious(pMan, pObj); + Gia_ObjDfsMark_rec( pMan, pObj ); + Gia_ObjSetTravIdPrevious(pMan, pObj); + Gia_ObjDfsMark2_rec( pMan, pObj ); + } + Vec_WecForEachLevel( vSupps, vLevel, i ) { + Gia_ManForEachObjVec( vLevel, pMan, pObj, k ) + if ( Gia_ObjIsTravIdCurrent(pMan, pObj) ) + break; + if ( k < Vec_IntSize(vLevel) ) + Vec_IntClear( vLevel ); + } + Vec_WecRemoveEmpty( vSupps ); +} +// removes all supports that are contained in this one +void Gia_ManSelectRemove3( Vec_Wec_t * vSupps, Vec_Int_t * vOne ) +{ + Vec_Int_t * vLevel; int i; + Vec_WecForEachLevel( vSupps, vLevel, i ) + if ( Vec_IntTwoCountCommon(vLevel, vOne) == Vec_IntSize(vLevel) ) + Vec_IntClear( vLevel ); + Vec_WecRemoveEmpty( vSupps ); +} +Vec_Ptr_t * Gia_ManDeriveWinInsAll( Vec_Wec_t * vSupps, int nSuppMax, Gia_Man_t * pMan, int fOverlap ) +{ + Vec_Ptr_t * vRes = Vec_PtrAlloc( 100 ); + Gia_ManIncrementTravId( pMan ); + while ( Vec_WecSize(vSupps) > 0 ) { + int i, Item, iRand = Abc_Random(0) % Vec_WecSize(vSupps); + Vec_Int_t * vLevel, * vLevel2 = Vec_WecEntry( vSupps, iRand ); + Vec_Int_t * vCopy = Vec_IntDup( vLevel2 ); + if ( Vec_IntSize(vLevel2) == nSuppMax ) { + Vec_PtrPush( vRes, vCopy ); + if ( fOverlap ) + Gia_ManSelectRemove3( vSupps, vCopy ); + else + Gia_ManSelectRemove2( vSupps, vCopy, pMan ); + continue; + } + // find another support, which maximizes the union but does not exceed nSuppMax + int iBest = iRand, nUnion = Vec_IntSize(vCopy); + Vec_WecForEachLevel( vSupps, vLevel, i ) { + if ( i == iRand ) continue; + int nCommon = Vec_IntTwoCountCommon(vLevel, vCopy); + int nUnionCur = Vec_IntSize(vLevel) + Vec_IntSize(vCopy) - nCommon; + if ( nUnionCur <= nSuppMax && nUnion < nUnionCur ) { + nUnion = nUnionCur; + iBest = i; + } + } + vLevel = Vec_WecEntry( vSupps, iBest ); + Vec_IntForEachEntry( vLevel, Item, i ) + Vec_IntPushUniqueOrder( vCopy, Item ); + Vec_PtrPush( vRes, vCopy ); + if ( fOverlap ) + Gia_ManSelectRemove3( vSupps, vCopy ); + else + Gia_ManSelectRemove2( vSupps, vCopy, pMan ); + } + return vRes; +} +Gia_Man_t * Gia_ManDupFromArrays( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + pNew = Gia_ManStart( 5000 ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachObjVec( vCis, p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachObjVec( vAnds, p, pObj, i ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachObjVec( vCos, p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, pObj->Value ); + return pNew; +} +Vec_Ptr_t * Gia_ManDupWindows( Gia_Man_t * pMan, Vec_Ptr_t * vvIns, Vec_Ptr_t * vvNodes, Vec_Ptr_t * vvOuts ) +{ + Vec_Int_t * vNodes; int i; + Vec_Ptr_t * vWins = Vec_PtrAlloc( Vec_PtrSize(vvIns) ); + assert( Vec_PtrSize(vvIns) == Vec_PtrSize(vvNodes) ); + assert( Vec_PtrSize(vvOuts) == Vec_PtrSize(vvNodes) ); + Gia_ManFillValue( pMan ); + Gia_ManCleanMark01( pMan ); + Vec_PtrForEachEntry( Vec_Int_t *, vvNodes, vNodes, i ) { + Vec_Int_t * vIns = (Vec_Int_t *)Vec_PtrEntry(vvIns, i); + Vec_Int_t * vOuts = (Vec_Int_t *)Vec_PtrEntry(vvOuts, i); + Gia_Man_t * pNew = Gia_ManDupFromArrays( pMan, vIns, vNodes, vOuts ); + Vec_PtrPush( vWins, pNew ); + } + return vWins; +} +int Gia_ManLevelR( Gia_Man_t * pMan ) +{ + int i, LevelMax = Gia_ManLevelRNum( pMan ); + Gia_Obj_t * pNode; + Gia_ManForEachObj( pMan, pNode, i ) + Gia_ObjSetLevel( pMan, pNode, (int)(LevelMax - Gia_ObjLevel(pMan, pNode) + 1) ); + Gia_ManForEachCi( pMan, pNode, i ) + Gia_ObjSetLevel( pMan, pNode, 0 ); + return LevelMax; +} +Vec_Ptr_t * Gia_ManExtractPartitions( Gia_Man_t * pMan, int Iter, int nSuppMax, Vec_Ptr_t ** pvIns, Vec_Ptr_t ** pvOuts, Vec_Ptr_t ** pvNodes, int fOverlap ) +{ + // if ( Gia_ManCiNum(pMan) <= nSuppMax ) { + // Vec_Ptr_t * vWins = Vec_PtrAlloc( 1 ); + // Vec_PtrPush( vWins, Gia_ManDupDfs(pMan) ); + // *pvIns = *pvOuts = *pvNodes = NULL; + // return vWins; + // } + // int iUseRevL = Iter % 3 == 0 ? 0 : Abc_Random(0) & 1; + int iUseRevL = Abc_Random(0) & 1; + int LevelMax = iUseRevL ? Gia_ManLevelR(pMan) : Gia_ManLevelNum(pMan); + // int LevelCut = Iter % 3 == 0 ? 0 : LevelMax > 8 ? 2 + (Abc_Random(0) % (LevelMax - 4)) : 0; + int LevelCut = LevelMax > 8 ? (Abc_Random(0) % (LevelMax - 4)) : 0; + //printf( "Using %s cut level %d (out of %d)\n", iUseRevL ? "reverse": "direct", LevelCut, LevelMax ); + // Gia_ManPermuteLevel( pMan, LevelMax ); + Vec_Wec_t * vStore = Vec_WecStart( LevelMax+1 ); + Vec_Wec_t * vSupps = Gia_ManCollectObjectsWithSuppLimit( pMan, LevelCut, nSuppMax ); + Vec_Ptr_t * vIns = Gia_ManDeriveWinInsAll( vSupps, nSuppMax, pMan, fOverlap ); + Vec_Ptr_t * vNodes = Gia_ManDeriveWinNodesAll( pMan, vIns, vStore ); + Vec_Ptr_t * vOuts = Gia_ManDeriveWinOutsAll( pMan, vNodes ); + Vec_Ptr_t * vWins = Gia_ManDupWindows( pMan, vIns, vNodes, vOuts ); + Vec_WecFree( vSupps ); + Vec_WecFree( vStore ); + *pvIns = vIns; + *pvOuts = vOuts; + *pvNodes = vNodes; + return vWins; +} + + + /**Function************************************************************* Synopsis [] @@ -358,7 +785,8 @@ Vec_Ptr_t * Gia_ManDupDivide( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds Vec_PtrPush( vAigs, Gia_ManDupDivideOne(p, Vec_WecEntry(vCis, i), Vec_WecEntry(vAnds, i), Vec_WecEntry(vCos, i)) ); } //Gia_ManStochSynthesis( vAigs, pScript ); - Gia_StochProcess( vAigs, pScript, nProcs, TimeOut, 0 ); + Vec_Int_t * vGains = Gia_StochProcess( vAigs, pScript, nProcs, TimeOut, 0 ); + Vec_IntFree( vGains ); return vAigs; } Gia_Man_t * Gia_ManDupStitch( Gia_Man_t * p, Vec_Wec_t * vCis, Vec_Wec_t * vAnds, Vec_Wec_t * vCos, Vec_Ptr_t * vAigs, int fHash ) @@ -554,7 +982,7 @@ Vec_Wec_t * Gia_ManStochOutputs( Gia_Man_t * p, Vec_Wec_t * vAnds ) SeeAlso [] ***********************************************************************/ -void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript, int nProcs ) +void Gia_ManStochSyn( int nSuppMax, int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript, int nProcs ) { abctime nTimeToStop = TimeOut ? Abc_Clock() + TimeOut * CLOCKS_PER_SEC : 0; abctime clkStart = Abc_Clock(); @@ -564,43 +992,83 @@ void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerb Abc_Random(1); for ( i = 0; i < 10+Seed; i++ ) Abc_Random(0); - if ( fVerbose ) - printf( "Running %d iterations of script \"%s\".\n", nIters, pScript ); - for ( i = 0; i < nIters; i++ ) - { - abctime clk = Abc_Clock(); - Gia_Man_t * pGia = Gia_ManDupWithMapping( Abc_FrameReadGia(Abc_FrameGetGlobalFrame()) ); - Vec_Wec_t * vAnds = Gia_ManStochNodes( pGia, nMaxSize, Abc_Random(0) & 0x7FFFFFFF ); - Vec_Wec_t * vIns = Gia_ManStochInputs( pGia, vAnds ); - Vec_Wec_t * vOuts = Gia_ManStochOutputs( pGia, vAnds ); - Vec_Ptr_t * vAigs = Gia_ManDupDivide( pGia, vIns, vAnds, vOuts, pScript, nProcs, TimeOut ); - Gia_Man_t * pNew = Gia_ManDupStitchMap( pGia, vIns, vAnds, vOuts, vAigs ); - int fMapped = Gia_ManHasMapping(pGia) && Gia_ManHasMapping(pNew); - Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew ); - if ( fVerbose ) - printf( "Iteration %3d : Using %3d partitions. Reducing %6d to %6d %s. ", - i, Vec_PtrSize(vAigs), fMapped ? Gia_ManLutNum(pGia) : Gia_ManAndNum(pGia), - fMapped ? Gia_ManLutNum(pNew) : Gia_ManAndNum(pNew), - fMapped ? "LUTs" : "ANDs" ); - if ( fVerbose ) - Abc_PrintTime( 0, "Time", Abc_Clock() - clk ); - Gia_ManStop( pGia ); - Vec_PtrFreeFunc( vAigs, (void (*)(void *)) Gia_ManStop ); - Vec_WecFree( vAnds ); - Vec_WecFree( vIns ); - Vec_WecFree( vOuts ); - if ( nTimeToStop && Abc_Clock() > nTimeToStop ) + if ( fVerbose ) { + printf( "Running %d iterations of the script \"%s\"", nIters, pScript ); + if ( nProcs > 2 ) + printf( " using %d concurrent threads.\n", nProcs-1 ); + else + printf( " without concurrency.\n" ); + fflush(stdout); + } + if ( !nSuppMax ) { + for ( i = 0; i < nIters; i++ ) { - printf( "Runtime limit (%d sec) is reached after %d iterations.\n", TimeOut, i ); - break; + abctime clk = Abc_Clock(); + Gia_Man_t * pGia = Gia_ManDupWithMapping( Abc_FrameReadGia(Abc_FrameGetGlobalFrame()) ); + Vec_Wec_t * vAnds = Gia_ManStochNodes( pGia, nMaxSize, Abc_Random(0) & 0x7FFFFFFF ); + Vec_Wec_t * vIns = Gia_ManStochInputs( pGia, vAnds ); + Vec_Wec_t * vOuts = Gia_ManStochOutputs( pGia, vAnds ); + Vec_Ptr_t * vAigs = Gia_ManDupDivide( pGia, vIns, vAnds, vOuts, pScript, nProcs, TimeOut ); + Gia_Man_t * pNew = Gia_ManDupStitchMap( pGia, vIns, vAnds, vOuts, vAigs ); + int fMapped = Gia_ManHasMapping(pGia) && Gia_ManHasMapping(pNew); + Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew ); + if ( fVerbose ) + printf( "Iteration %3d : Using %3d partitions. Reducing %6d to %6d %s. ", + i, Vec_PtrSize(vAigs), fMapped ? Gia_ManLutNum(pGia) : Gia_ManAndNum(pGia), + fMapped ? Gia_ManLutNum(pNew) : Gia_ManAndNum(pNew), + fMapped ? "LUTs" : "ANDs" ); + if ( fVerbose ) + Abc_PrintTime( 0, "Time", Abc_Clock() - clk ); + Gia_ManStop( pGia ); + Vec_PtrFreeFunc( vAigs, (void (*)(void *)) Gia_ManStop ); + Vec_WecFree( vAnds ); + Vec_WecFree( vIns ); + Vec_WecFree( vOuts ); + if ( nTimeToStop && Abc_Clock() > nTimeToStop ) + { + printf( "Runtime limit (%d sec) is reached after %d iterations.\n", TimeOut, i ); + break; + } + } + } + else { + int fOverlap = 1; + Vec_Ptr_t * vIns = NULL, * vOuts = NULL, * vNodes = NULL; + for ( i = 0; i < nIters; i++ ) + { + extern Gia_Man_t * Gia_ManDupInsertWindows( Gia_Man_t * p, Vec_Ptr_t * vvIns, Vec_Ptr_t * vvOuts, Vec_Ptr_t * vAigs ); + abctime clk = Abc_Clock(); + Gia_Man_t * pGia = Gia_ManDup( Abc_FrameReadGia(Abc_FrameGetGlobalFrame()) ); Gia_ManStaticFanoutStart(pGia); + Vec_Ptr_t * vAigs = Gia_ManExtractPartitions( pGia, i, nSuppMax, &vIns, &vOuts, &vNodes, fOverlap ); + Vec_Int_t * vGains = Gia_StochProcess( vAigs, pScript, nProcs, TimeOut, 0 ); + int nPartsInit = fOverlap ? Gia_ManFilterPartitions( pGia, vIns, vNodes, vOuts, vAigs, vGains ) : Vec_PtrSize(vIns); + Gia_Man_t * pNew = Gia_ManDupInsertWindows( pGia, vIns, vOuts, vAigs ); Gia_ManStaticFanoutStop(pGia); + Abc_FrameUpdateGia( Abc_FrameGetGlobalFrame(), pNew ); + if ( fVerbose ) + printf( "Iteration %3d : Using %3d -> %3d partitions. Reducing node count from %6d to %6d. ", + i, nPartsInit, Vec_PtrSize(vAigs), Gia_ManAndNum(pGia), Gia_ManAndNum(pNew) ); + if ( fVerbose ) + Abc_PrintTime( 0, "Time", Abc_Clock() - clk ); + // cleanup + Gia_ManStop( pGia ); + Vec_PtrFreeFunc( vAigs, (void (*)(void *)) Gia_ManStop ); + Vec_IntFreeP( &vGains ); + if ( vIns ) Vec_PtrFreeFunc( vIns, (void (*)(void *)) Vec_IntFree ); + if ( vOuts ) Vec_PtrFreeFunc( vOuts, (void (*)(void *)) Vec_IntFree ); + if ( vNodes ) Vec_PtrFreeFunc( vNodes, (void (*)(void *)) Vec_IntFree ); + if ( nTimeToStop && Abc_Clock() > nTimeToStop ) + { + printf( "Runtime limit (%d sec) is reached after %d iterations.\n", TimeOut, i ); + break; + } } } fMapped &= Gia_ManHasMapping(Abc_FrameReadGia(Abc_FrameGetGlobalFrame())); nLutEnd = fMapped ? Gia_ManLutNum(Abc_FrameReadGia(Abc_FrameGetGlobalFrame())) : 0; nEnd = Gia_ManAndNum(Abc_FrameReadGia(Abc_FrameGetGlobalFrame())); if ( fVerbose ) - printf( "Cumulatively reduced %d %s after %d iterations. ", - fMapped ? nLutBeg - nLutEnd : nBeg - nEnd, fMapped ? "LUTs" : "ANDs", nIters ); + printf( "Cumulatively reduced %d %s (%.2f %%) after %d iterations. ", + fMapped ? nLutBeg - nLutEnd : nBeg - nEnd, fMapped ? "LUTs" : "nodes", 100.0*(nBeg - nEnd)/Abc_MaxInt(nBeg, 1), nIters ); if ( fVerbose ) Abc_PrintTime( 0, "Total time", Abc_Clock() - clkStart ); } diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c index fc40835cb..17f03aa4a 100644 --- a/src/aig/gia/giaTim.c +++ b/src/aig/gia/giaTim.c @@ -1067,6 +1067,27 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fS return Status; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManDeriveBoxMapping( Gia_Man_t * pGia ) +{ + Tim_Man_t * pTim = (Tim_Man_t *)pGia->pManTime; + Vec_Int_t * vRes = Vec_IntAlloc( 100 ); + int i, nBoxes = Tim_ManBoxNum( pTim ); + for ( i = 0; i < nBoxes; i++ ) + Vec_IntPush( vRes, Tim_ManBoxCopy(pTim, i) ); + return vRes; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h index 1d4bde4d7..b23905dd3 100644 --- a/src/base/abc/abc.h +++ b/src/base/abc/abc.h @@ -755,6 +755,7 @@ extern ABC_DLL void Abc_NtkAddDummyPiNames( Abc_Ntk_t * pNtk ); extern ABC_DLL void Abc_NtkAddDummyPoNames( Abc_Ntk_t * pNtk ); extern ABC_DLL void Abc_NtkAddDummyBoxNames( Abc_Ntk_t * pNtk ); extern ABC_DLL void Abc_NtkShortNames( Abc_Ntk_t * pNtk ); +extern ABC_DLL void Abc_NtkCharNames( Abc_Ntk_t * pNtk ); extern ABC_DLL void Abc_NtkCleanNames( Abc_Ntk_t * pNtk ); extern ABC_DLL void Abc_NtkStartNameIds( Abc_Ntk_t * p ); extern ABC_DLL void Abc_NtkTransferNameIds( Abc_Ntk_t * p, Abc_Ntk_t * pNew ); diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c index dec5f01e0..b3910236e 100644 --- a/src/base/abc/abcNames.c +++ b/src/base/abc/abcNames.c @@ -125,6 +125,12 @@ char * Abc_ObjNameDummy( char * pPrefix, int Num, int nDigits ) sprintf( Buffer, "%s%0*d", pPrefix, nDigits, Num ); return Buffer; } +char * Abc_ObjNameChar( int Num, int fCap ) +{ + static char Buffer[2000]; + sprintf( Buffer, "%c", (fCap ? 'A':'a') + Num ); + return Buffer; +} /**Function************************************************************* @@ -494,6 +500,12 @@ void Abc_NtkAddDummyPiNames( Abc_Ntk_t * pNtk ) Abc_NtkForEachPi( pNtk, pObj, i ) Abc_ObjAssignName( pObj, Abc_ObjNameDummy("pi", i, nDigits), NULL ); } +void Abc_NtkAddCharPiNames( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; int i; + Abc_NtkForEachPi( pNtk, pObj, i ) + Abc_ObjAssignName( pObj, Abc_ObjNameChar(i, 0), NULL ); +} /**Function************************************************************* @@ -514,6 +526,12 @@ void Abc_NtkAddDummyPoNames( Abc_Ntk_t * pNtk ) Abc_NtkForEachPo( pNtk, pObj, i ) Abc_ObjAssignName( pObj, Abc_ObjNameDummy("po", i, nDigits), NULL ); } +void Abc_NtkAddCharPoNames( Abc_Ntk_t * pNtk ) +{ + Abc_Obj_t * pObj; int i; + Abc_NtkForEachPo( pNtk, pObj, i ) + Abc_ObjAssignName( pObj, Abc_ObjNameChar(i, 1), NULL ); +} /**Function************************************************************* @@ -606,6 +624,14 @@ void Abc_NtkShortNames( Abc_Ntk_t * pNtk ) Abc_NtkAddDummyPoNames( pNtk ); Abc_NtkAddDummyBoxNames( pNtk ); } +void Abc_NtkCharNames( Abc_Ntk_t * pNtk ) +{ + Nm_ManFree( pNtk->pManName ); + pNtk->pManName = Nm_ManCreate( Abc_NtkCiNum(pNtk) + Abc_NtkCoNum(pNtk) + Abc_NtkBoxNum(pNtk) ); + Abc_NtkAddCharPiNames( pNtk ); + Abc_NtkAddCharPoNames( pNtk ); + Abc_NtkAddDummyBoxNames( pNtk ); +} void Abc_NtkCleanNames( Abc_Ntk_t * pNtk ) { Abc_Obj_t * pObj; int i; diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c index c4dbb36ee..9d6c4f0ea 100644 --- a/src/base/abc/abcNtk.c +++ b/src/base/abc/abcNtk.c @@ -96,6 +96,52 @@ Abc_Ntk_t * Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan pNtk->AndGateDelay = 0.0; return pNtk; } +Abc_Ntk_t * Abc_NtkAllocBdd( Abc_NtkType_t Type, Abc_NtkFunc_t Func, int fUseMemMan, int nVars ) +{ + Abc_Ntk_t * pNtk; + pNtk = ABC_ALLOC( Abc_Ntk_t, 1 ); + memset( pNtk, 0, sizeof(Abc_Ntk_t) ); + pNtk->ntkType = Type; + pNtk->ntkFunc = Func; + // start the object storage + pNtk->vObjs = Vec_PtrAlloc( 100 ); + pNtk->vPios = Vec_PtrAlloc( 100 ); + pNtk->vPis = Vec_PtrAlloc( 100 ); + pNtk->vPos = Vec_PtrAlloc( 100 ); + pNtk->vCis = Vec_PtrAlloc( 100 ); + pNtk->vCos = Vec_PtrAlloc( 100 ); + pNtk->vBoxes = Vec_PtrAlloc( 100 ); + pNtk->vLtlProperties = Vec_PtrAlloc( 100 ); + // start the memory managers + pNtk->pMmObj = fUseMemMan? Mem_FixedStart( sizeof(Abc_Obj_t) ) : NULL; + pNtk->pMmStep = fUseMemMan? Mem_StepStart( ABC_NUM_STEPS ) : NULL; + // get ready to assign the first Obj ID + pNtk->nTravIds = 1; + // start the functionality manager + if ( !Abc_NtkIsStrash(pNtk) ) + Vec_PtrPush( pNtk->vObjs, NULL ); + if ( Abc_NtkIsStrash(pNtk) ) + pNtk->pManFunc = Abc_AigAlloc( pNtk ); + else if ( Abc_NtkHasSop(pNtk) || Abc_NtkHasBlifMv(pNtk) ) + pNtk->pManFunc = Mem_FlexStart(); +#ifdef ABC_USE_CUDD + else if ( Abc_NtkHasBdd(pNtk) ) + pNtk->pManFunc = Cudd_Init( nVars, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 ); +#endif + else if ( Abc_NtkHasAig(pNtk) ) + pNtk->pManFunc = Hop_ManStart(); + else if ( Abc_NtkHasMapping(pNtk) ) + pNtk->pManFunc = Abc_FrameReadLibGen(); + else if ( !Abc_NtkHasBlackbox(pNtk) ) + assert( 0 ); + // name manager + pNtk->pManName = Nm_ManCreate( 200 ); + // attribute manager + pNtk->vAttrs = Vec_PtrStart( VEC_ATTR_TOTAL_NUM ); + // estimated AndGateDelay + pNtk->AndGateDelay = 0.0; + return pNtk; +} /**Function************************************************************* @@ -118,7 +164,7 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_ // decide whether to copy the names fCopyNames = ( Type != ABC_NTK_NETLIST ); // start the network - pNtkNew = Abc_NtkAlloc( Type, Func, 1 ); + pNtkNew = Func == ABC_FUNC_BDD ? Abc_NtkAllocBdd( Type, Func, 1, Abc_NtkCiNum(pNtk) ) : Abc_NtkAlloc( Type, Func, 1 ); pNtkNew->nConstrs = pNtk->nConstrs; pNtkNew->nBarBufs = pNtk->nBarBufs; // duplicate the name and the spec @@ -1518,6 +1564,24 @@ void Abc_NtkFixNonDrivenNets( Abc_Ntk_t * pNtk ) return; // special case + pNet = Abc_NtkFindNet( pNtk, "$false" ); + if ( pNet != NULL && !Abc_ObjFaninNum(pNet) ) + { + pNode = Abc_NtkCreateNodeConst0( pNtk ); + Abc_ObjAddFanin( pNet, pNode ); + } + pNet = Abc_NtkFindNet( pNtk, "$undef" ); + if ( pNet != NULL && !Abc_ObjFaninNum(pNet) ) + { + pNode = Abc_NtkCreateNodeConst0( pNtk ); + Abc_ObjAddFanin( pNet, pNode ); + } + pNet = Abc_NtkFindNet( pNtk, "$true" ); + if ( pNet != NULL && !Abc_ObjFaninNum(pNet) ) + { + pNode = Abc_NtkCreateNodeConst1( pNtk ); + Abc_ObjAddFanin( pNet, pNode ); + } pNet = Abc_NtkFindNet( pNtk, "[_c1_]" ); if ( pNet != NULL ) { diff --git a/src/base/abc/abcSop.c b/src/base/abc/abcSop.c index adc1639a6..3275e4772 100644 --- a/src/base/abc/abcSop.c +++ b/src/base/abc/abcSop.c @@ -1131,6 +1131,8 @@ Vec_Ptr_t * Abc_SopFromTruthsHex( char * pTruth ) char * pToken = strtok( pCopy, " \r\n\t|" ); while ( pToken ) { + if ( pToken[0] == '0' && pToken[1] == 'x' ) + pToken += 2; if ( !Abc_SopCheckReadTruth( vRes, pToken, 1 ) ) break; Vec_PtrPush( vRes, Abc_SopFromTruthHex(pToken) ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 6db456e5c..c9150ea8c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -146,6 +146,7 @@ static int Abc_CommandTestRand ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandRunSat ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRunEco ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRunGen ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandRunScript ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRunTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandRewrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -634,11 +635,13 @@ static int Abc_CommandAbc9GenMux ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9GenComp ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GenSorter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GenNeuron ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9GenAdder ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Window ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9FunAbs ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9DsdInfo ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9FunTrace ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9MulFind ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9AndCare ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -962,6 +965,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Synthesis", "runsat", Abc_CommandRunSat, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "runeco", Abc_CommandRunEco, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "rungen", Abc_CommandRunGen, 0 ); + Cmd_CommandAdd( pAbc, "Synthesis", "runscript", Abc_CommandRunScript, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "xec", Abc_CommandRunTest, 0 ); Cmd_CommandAdd( pAbc, "Synthesis", "rewrite", Abc_CommandRewrite, 1 ); @@ -1455,11 +1459,13 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&gencomp", Abc_CommandAbc9GenComp, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gensorter", Abc_CommandAbc9GenSorter, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&genneuron", Abc_CommandAbc9GenNeuron, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&genadder", Abc_CommandAbc9GenAdder, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&window", Abc_CommandAbc9Window, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&funabs", Abc_CommandAbc9FunAbs, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&dsdinfo", Abc_CommandAbc9DsdInfo, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&funtrace", Abc_CommandAbc9FunTrace, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&mulfind", Abc_CommandAbc9MulFind, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&andcare", Abc_CommandAbc9AndCare, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); @@ -2654,14 +2660,17 @@ int Abc_CommandPrintGates( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; int fUseLibrary; int fUpdateProfile; + int fVerbose; extern void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary, int fUpdateProfile ); + extern void Abc_NtkPrintGates2( Abc_Ntk_t * pNtk ); // set defaults fUseLibrary = 1; fUpdateProfile = 0; + fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "luh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "luvh" ) ) != EOF ) { switch ( c ) { @@ -2671,6 +2680,9 @@ int Abc_CommandPrintGates( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'u': fUpdateProfile ^= 1; break; + case 'v': + fVerbose ^= 1; + break; case 'h': goto usage; default: @@ -2688,15 +2700,18 @@ int Abc_CommandPrintGates( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Printing gates does not work for AIGs and sequential AIGs.\n" ); return 1; } - - Abc_NtkPrintGates( pNtk, fUseLibrary, fUpdateProfile ); + if ( fVerbose ) + Abc_NtkPrintGates2( pNtk ); + else + Abc_NtkPrintGates( pNtk, fUseLibrary, fUpdateProfile ); return 0; usage: - Abc_Print( -2, "usage: print_gates [-luh]\n" ); + Abc_Print( -2, "usage: print_gates [-luvh]\n" ); Abc_Print( -2, "\t prints statistics about gates used in the network\n" ); Abc_Print( -2, "\t-l : used library gate names (if mapped) [default = %s]\n", fUseLibrary? "yes": "no" ); Abc_Print( -2, "\t-u : update profile before printing it[default = %s]\n", fUpdateProfile? "yes": "no" ); + Abc_Print( -2, "\t-v : enable verbose output [default = %s].\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -5475,7 +5490,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) // set defaults Abc_NtkMfsParsDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCdraestpgvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "WFDMLCdraestpgcvwh" ) ) != EOF ) { switch ( c ) { @@ -5569,6 +5584,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'g': pPars->fGiaSat ^= 1; break; + case 'c': + pPars->fPrintCares ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -5602,7 +5620,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: mfs [-WFDMLC ] [-draestpgvh]\n" ); + Abc_Print( -2, "usage: mfs [-WFDMLC ] [-draestpgcvh]\n" ); Abc_Print( -2, "\t performs don't-care-based optimization of logic networks\n" ); Abc_Print( -2, "\t-W : the number of levels in the TFO cone (0 <= num) [default = %d]\n", pPars->nWinTfoLevs ); Abc_Print( -2, "\t-F : the max number of fanouts to skip (1 <= num) [default = %d]\n", pPars->nFanoutsMax ); @@ -5618,6 +5636,7 @@ usage: Abc_Print( -2, "\t-t : toggle using artificial one-hotness conditions [default = %s]\n", pPars->fOneHotness? "yes": "no" ); Abc_Print( -2, "\t-p : toggle power-aware optimization [default = %s]\n", pPars->fPower? "yes": "no" ); Abc_Print( -2, "\t-g : toggle using new SAT solver [default = %s]\n", pPars->fGiaSat? "yes": "no" ); + Abc_Print( -2, "\t-c : toggle printing careset at each node [default = %s]\n", pPars->fPrintCares? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing detailed stats for each node [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); @@ -7681,6 +7700,126 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandRunScript( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + int c, nIters = 10, nBeg = 1, nAdd = 1, fReverse = 0, fVerbose = 0; char * pScript = NULL, * pSpot = NULL; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "IBASrvh" ) ) != EOF ) + { + switch ( c ) + { + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nIters = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'B': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" ); + goto usage; + } + nBeg = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'A': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" ); + goto usage; + } + nAdd = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by a script.\n" ); + goto usage; + } + pScript = argv[globalUtilOptind]; + globalUtilOptind++; + break; + case 'r': + fReverse ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pScript == NULL ) + { + Abc_Print( -1, "Command line switch \"-S\" should be specified and followed by a string.\n" ); + goto usage; + } + pSpot = strstr( pScript, "*" ); + if ( pSpot == NULL ) + { + for ( c = 0; c < nIters; c++ ) + { + if ( fVerbose ) + printf( "ITERATION %3d : %s\n", c, pScript ); + if ( Cmd_CommandExecute(Abc_FrameGetGlobalFrame(), pScript) ) { + Abc_Print( 1, "Something did not work out with the command \"%s\".\n", pScript ); + goto usage; + } + } + printf( "Finished iterating script %d times.\n", nIters ); + return 0; + } + assert( *pSpot == '*' ); + for ( c = 0; c < nIters; c++ ) + { + char pCommLine[1000] = {0}; + char pNumber[10] = {0}; + sprintf( pNumber, "%d", fReverse ? nBeg - c*nAdd : nBeg + c*nAdd ); + strcpy( pCommLine, pScript ); + pCommLine[(int)(pSpot - pScript)] = 0; + strcat( pCommLine, pNumber ); + strcat( pCommLine, pSpot+1 ); + if ( fVerbose ) + printf( "ITERATION %3d : %s\n", c, pCommLine ); + if ( Cmd_CommandExecute(Abc_FrameGetGlobalFrame(), pCommLine) ) { + Abc_Print( 1, "Something did not work out with the command \"%s\".\n", pCommLine ); + goto usage; + } + } + printf( "Finished iterating script %d times.\n", nIters ); + return 0; + +usage: + Abc_Print( -2, "usage: runscript [-IBA num] [-S str] [-rvh]\n" ); + Abc_Print( -2, "\t running the script with different values\n" ); + Abc_Print( -2, "\t-I : the number of iterations [default = %d]\n", nIters ); + Abc_Print( -2, "\t-B : the starting number [default = %d]\n", nBeg ); + Abc_Print( -2, "\t-A : the increment added in each iteration [default = %d]\n", nAdd ); + Abc_Print( -2, "\t-S : the script to iterate [default = none]\n" ); + Abc_Print( -2, "\t-r : toggle reversing the order of counting [default = %s]\n", fReverse? "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; +} + /**Function************************************************************* Synopsis [] @@ -9056,12 +9195,12 @@ usage: int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Abc_Ntk_t * Abc_NtkLutCascadeGen( int nLutSize, int nStages, int nRails, int nShared, int fVerbose ); - extern Abc_Ntk_t * Abc_NtkLutCascade2( Abc_Ntk_t * pNtk, int nLutSize, int nLuts, int nRails, int nIters, int fVerbose, char * pGuide ); - extern void Abc_NtkLutCascadeFile( char * pFileName, int nVarNum, int nLutSize, int nLuts, int nRails, int nIters, int fVerbose, int fVeryVerbose ); + extern Abc_Ntk_t * Abc_NtkLutCascadeOne( Abc_Ntk_t * pNtk, int nLutSize, int nLuts, int nRails, int nIters, int nJRatio, int nZParam, int fXRail, int Seed, int fVerbose, int fVeryVerbose, char * pGuide, int nSubsets, int nBest ); + extern void Abc_NtkLutCascadeFile( char * pFileName, int nVarNum, int nLutSize, int nLuts, int nRails, int nIters, int nJRatio, int nZParam, int Seed, int fVerbose, int fVeryVerbose, int fPrintMyu, int fPrintLev, int fXRail, int nSubsets, int nBest ); Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes; char * pGuide = NULL, * pFileName = NULL; - int c, nVarNum = -1, nLutSize = 6, nStages = 8, nRails = 1, nShared = 2, nIters = 10, fGen = 0, fVerbose = 0, fVeryVerbose = 0; + int c, nVarNum = -1, nLutSize = 6, nStages = 8, nRails = 1, nShared = 2, Seed = 0, nIters = 10, nJRatio = -1, nZParam = 5, fGen = 0, fPrintMyu = 0, fPrintLev = 0, fXRail = 0, nSubsets = 0, nBest = 0, fVerbose = 0, fVeryVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KMRSINFgvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KMRSCIZNGBFgmlxvwh" ) ) != EOF ) { switch ( c ) { @@ -9098,15 +9237,26 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nRails < 0 ) goto usage; break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + nShared = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nShared < 0 ) + goto usage; + break; case 'S': if ( globalUtilOptind >= argc ) { Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); goto usage; } - nShared = atoi(argv[globalUtilOptind]); + Seed = atoi(argv[globalUtilOptind]); globalUtilOptind++; - if ( nShared < 0 ) + if ( Seed < 0 ) goto usage; break; case 'I': @@ -9120,6 +9270,26 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nIters < 0 ) goto usage; break; + case 'J': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-J\" should be followed by an integer.\n" ); + goto usage; + } + nJRatio = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nJRatio < 0 ) + goto usage; + break; + case 'Z': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-Z\" should be followed by a file name.\n" ); + goto usage; + } + nZParam = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + break; case 'N': if ( globalUtilOptind >= argc ) { @@ -9131,6 +9301,28 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( nVarNum < 0 ) goto usage; break; + case 'G': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-G\" should be followed by an integer.\n" ); + goto usage; + } + nSubsets = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nSubsets < 0 ) + goto usage; + break; + case 'B': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" ); + goto usage; + } + nBest = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nBest < 0 ) + goto usage; + break; case 'F': if ( globalUtilOptind >= argc ) { @@ -9143,6 +9335,15 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'g': fGen ^= 1; break; + case 'm': + fPrintMyu ^= 1; + break; + case 'l': + fPrintLev ^= 1; + break; + case 'x': + fXRail ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -9162,8 +9363,8 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "The number of variables should be given on the command line using switch \"-N \".\n" ); return 1; } - Abc_NtkLutCascadeFile( pFileName, nVarNum, nLutSize, nStages, nRails, nIters, fVerbose, fVeryVerbose ); - return 1; + Abc_NtkLutCascadeFile( pFileName, nVarNum, nLutSize, nStages, nRails, nIters, nJRatio, nZParam, Seed, fVerbose, fVeryVerbose, fPrintMyu, fPrintLev, fXRail, nSubsets, nBest ); + return 0; } if ( fGen ) { @@ -9199,7 +9400,7 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( argc == globalUtilOptind + 1 ) pGuide = argv[globalUtilOptind]; - pNtkRes = Abc_NtkLutCascade2( pNtk, nLutSize, nStages, nRails, nIters, fVerbose, pGuide ); + pNtkRes = Abc_NtkLutCascadeOne( pNtk, nLutSize, nStages, nRails, nIters, nJRatio, nZParam, fXRail, Seed, fVerbose, fVeryVerbose, pGuide, nSubsets, nBest ); if ( pNtkRes == NULL ) { Abc_Print( -1, "LUT cascade mapping failed.\n" ); @@ -9209,18 +9410,26 @@ int Abc_CommandLutCasDec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: lutcasdec [-KMRSIN ] [-F ] [-vwh]\n" ); + Abc_Print( -2, "usage: lutcasdec [-KMRCSIZNGB ] [-F ] [-gmlxvwh]\n" ); Abc_Print( -2, "\t decomposes the primary output functions into LUT cascades\n" ); Abc_Print( -2, "\t-K : the number of LUT inputs [default = %d]\n", nLutSize ); Abc_Print( -2, "\t-M : the maximum delay (the number of stages) [default = %d]\n", nStages ); Abc_Print( -2, "\t-R : the number of direct connections (rails) [default = %d]\n", nRails ); - Abc_Print( -2, "\t-S : the number of shared variables in each stage [default = %d]\n", nShared ); + Abc_Print( -2, "\t-C : the number of shared variables in each stage [default = %d]\n", nShared ); + Abc_Print( -2, "\t-S : the random seed for randomized bound-set selection [default = %d]\n", Seed ); Abc_Print( -2, "\t-I : the number of iterations when looking for a solution [default = %d]\n", nIters ); + //Abc_Print( -2, "\t-J : toggle using random bound-set every this many iterations [default = %d]\n", nJRatio ); + Abc_Print( -2, "\t-Z : the number determining how many decompositions are tried [default = %d]\n", nZParam ); Abc_Print( -2, "\t-N : the number of support variables (for truth table files only) [default = unused]\n" ); + Abc_Print( -2, "\t-G : the number of variable groups to consider [default = %d]\n", nSubsets ); + Abc_Print( -2, "\t-B : the number of best groups to use as bound-sets [default = %d]\n", nBest ); Abc_Print( -2, "\t-F : a text file with truth tables in hexadecimal listed one per line\n"); Abc_Print( -2, "\t-g : toggle generating random cascade with these parameters [default = %s]\n", fGen? "yes": "no" ); + Abc_Print( -2, "\t-m : toggle printing column multiplicity statistics [default = %s]\n", fPrintMyu? "yes": "no" ); + Abc_Print( -2, "\t-l : toggle printing level counting statistics [default = %s]\n", fPrintLev? "yes": "no" ); + Abc_Print( -2, "\t-x : toggle using extended cascade decomposition [default = %s]\n", fXRail? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-w : toggle additional verbose printout [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-w : toggle additional verbose printout [default = %s]\n", fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; } @@ -10421,11 +10630,12 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) extern int Exa3_ManExactSynthesis( Bmc_EsPar_t * pPars ); extern void Exa3_ManExactSynthesis2( Bmc_EsPar_t * pPars ); extern void Exa3_ManExactSynthesisRand( Bmc_EsPar_t * pPars ); + extern char * Abc_NtkReadTruth( Abc_Ntk_t * pNtk ); int c; Bmc_EsPar_t Pars, * pPars = &Pars; Bmc_EsParSetDefault( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "INKTSFMiaocgvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "INKTFUSYiaorfgvh" ) ) != EOF ) { switch ( c ) { @@ -10473,15 +10683,6 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->RuntimeLim < 0 ) goto usage; break; - case 'S': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); - goto usage; - } - pPars->pSymStr = argv[globalUtilOptind]; - globalUtilOptind++; - break; case 'F': if ( globalUtilOptind >= argc ) { @@ -10491,15 +10692,35 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) pPars->nRandFuncs = atoi(argv[globalUtilOptind]); globalUtilOptind++; break; - case 'M': + case 'U': if ( globalUtilOptind >= argc ) { - Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + Abc_Print( -1, "Command line switch \"-U\" should be followed by an integer.\n" ); goto usage; } pPars->nMintNum = atoi(argv[globalUtilOptind]); globalUtilOptind++; break; + case 'S': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-S\" should be followed by an integer.\n" ); + goto usage; + } + pPars->Seed = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->Seed < 0 ) + goto usage; + break; + case 'Y': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-Y\" should be followed by a string.\n" ); + goto usage; + } + pPars->pSymStr = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'i': pPars->fUseIncr ^= 1; break; @@ -10509,9 +10730,12 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'o': pPars->fFewerVars ^= 1; break; - case 'c': + case 'r': pPars->fLutCascade ^= 1; break; + case 'f': + pPars->fLutInFixed ^= 1; + break; case 'g': pPars->fGlucose ^= 1; break; @@ -10526,6 +10750,12 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) } if ( argc == globalUtilOptind + 1 ) pPars->pTtStr = argv[globalUtilOptind]; + else if ( argc == globalUtilOptind && Abc_FrameReadNtk(pAbc) ) + { + pPars->pTtStr = Abc_NtkReadTruth( Abc_FrameReadNtk(pAbc) ); + if ( pPars->pTtStr ) + pPars->nVars = Abc_NtkCiNum(Abc_FrameReadNtk(pAbc)); + } if ( pPars->pTtStr == NULL && pPars->pSymStr == NULL && pPars->nRandFuncs == 0 ) { Abc_Print( -1, "Truth table should be given on the command line.\n" ); @@ -10564,22 +10794,26 @@ int Abc_CommandLutExact( Abc_Frame_t * pAbc, int argc, char ** argv ) Exa3_ManExactSynthesis( pPars ); else Exa3_ManExactSynthesis2( pPars ); + if ( argc == globalUtilOptind && Abc_FrameReadNtk(pAbc) ) + ABC_FREE( pPars->pTtStr ); return 0; usage: - Abc_Print( -2, "usage: lutexact [-INKTFM ] [-S string] [-iaocgvh] \n" ); + Abc_Print( -2, "usage: lutexact [-INKTFUS ] [-Y string] [-iaorfgvh] \n" ); Abc_Print( -2, "\t exact synthesis of I-input function using N K-input gates\n" ); Abc_Print( -2, "\t-I : the number of input variables [default = %d]\n", pPars->nVars ); Abc_Print( -2, "\t-N : the number of K-input nodes [default = %d]\n", pPars->nNodes ); Abc_Print( -2, "\t-K : the number of node fanins [default = %d]\n", pPars->nLutSize ); Abc_Print( -2, "\t-T : the runtime limit in seconds [default = %d]\n", pPars->RuntimeLim ); Abc_Print( -2, "\t-F : the number of random functions to try [default = unused]\n" ); - Abc_Print( -2, "\t-M : the number of positive minterms in the random function [default = unused]\n" ); - Abc_Print( -2, "\t-S : charasteristic string of a symmetric function [default = %d]\n", pPars->pSymStr ); + Abc_Print( -2, "\t-U : the number of positive minterms in the random function [default = unused]\n" ); + Abc_Print( -2, "\t-S : the random seed for random function generation with -F [default = %d]\n", pPars->Seed ); + Abc_Print( -2, "\t-Y : charasteristic string of a symmetric function [default = %d]\n", pPars->pSymStr ); Abc_Print( -2, "\t-i : toggle using incremental solving [default = %s]\n", pPars->fUseIncr ? "yes" : "no" ); Abc_Print( -2, "\t-a : toggle using only AND-gates when K = 2 [default = %s]\n", pPars->fOnlyAnd ? "yes" : "no" ); Abc_Print( -2, "\t-o : toggle using additional optimizations [default = %s]\n", pPars->fFewerVars ? "yes" : "no" ); - Abc_Print( -2, "\t-c : toggle synthesizing a single-rail cascade [default = %s]\n", pPars->fLutCascade ? "yes" : "no" ); + Abc_Print( -2, "\t-r : toggle synthesizing a single-rail cascade [default = %s]\n", pPars->fLutCascade ? "yes" : "no" ); + Abc_Print( -2, "\t-f : toggle fixing LUT inputs in cascade mapping [default = %s]\n", pPars->fLutInFixed ? "yes" : "no" ); Abc_Print( -2, "\t-g : toggle using Glucose 3.0 by Gilles Audemard and Laurent Simon [default = %s]\n", pPars->fGlucose ? "yes" : "no" ); Abc_Print( -2, "\t-v : toggle verbose printout [default = %s]\n", pPars->fVerbose ? "yes" : "no" ); Abc_Print( -2, "\t-h : print the command usage\n" ); @@ -13992,13 +14226,16 @@ usage: int Abc_CommandShortNames( Abc_Frame_t * pAbc, int argc, char ** argv ) { Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); - int c, fKeepIo = 0; + int c, fKeepIo = 0, fAlpha = 0; // set defaults Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "kh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "akh" ) ) != EOF ) { switch ( c ) { + case 'a': + fAlpha ^= 1; + break; case 'k': fKeepIo ^= 1; break; @@ -14014,15 +14251,18 @@ int Abc_CommandShortNames( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Empty network.\n" ); return 1; } - if ( fKeepIo ) + if ( fAlpha ) + Abc_NtkCharNames( pNtk ); + else if ( fKeepIo ) Abc_NtkCleanNames( pNtk ); else Abc_NtkShortNames( pNtk ); return 0; usage: - Abc_Print( -2, "usage: short_names [-kh]\n" ); + Abc_Print( -2, "usage: short_names [-akh]\n" ); Abc_Print( -2, "\t replaces PI/PO/latch names by short char strings\n" ); + Abc_Print( -2, "\t-a : toggle using simple character names for PIs/POs [default = %s]\n", fAlpha? "yes": "no" ); Abc_Print( -2, "\t-k : toggle keeping PI/PO names unchanged [default = %s]\n", fKeepIo? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -20198,7 +20438,8 @@ usage: ***********************************************************************/ int Abc_CommandStochMap( Abc_Frame_t * pAbc, int argc, char ** argv ) { - Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc); + Abc_Ntk_t * pNtkRes = NULL, * pNtk = Abc_FrameReadNtk(pAbc); + extern void Mio_IntallAndLibrary(); extern void Abc_NtkStochMap( int nSuppMax, int nIters, int TimeOut, int Seed, int fOverlap, int fVerbose, char * pScript, int nProcs ); int c, nMaxSize = 14, nIters = 1, TimeOut = 0, Seed = 0, nProcs = 1, fOverlap = 0, fVerbose = 0; char * pScript; Extra_UtilGetoptReset(); @@ -20278,6 +20519,21 @@ int Abc_CommandStochMap( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandStochMap(): There is no AIG.\n" ); return 0; } + if ( Abc_NtkIsStrash(pNtk) ) + { + extern Abc_Ntk_t * Abc_NtkDarAmap( Abc_Ntk_t * pNtk, Amap_Par_t * pPars ); + Amap_Par_t Pars, * pPars = &Pars; + Amap_ManSetDefaultParams( pPars ); + Mio_IntallAndLibrary(); + pNtkRes = Abc_NtkDarAmap( pNtk, pPars ); + if ( pNtkRes == NULL ) + { + Abc_Print( -1, "Mapping has failed.\n" ); + return 1; + } + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + pNtk = Abc_FrameReadNtk(pAbc); + } if ( !Abc_NtkIsMappedLogic(pNtk) ) { Abc_Print( -1, "Abc_CommandStochMap(): Expecting a mapped current newtork as input.\n" ); @@ -20291,6 +20547,17 @@ int Abc_CommandStochMap( Abc_Frame_t * pAbc, int argc, char ** argv ) pScript = Abc_UtilStrsav( argv[globalUtilOptind] ); Abc_NtkStochMap( nMaxSize, nIters, TimeOut, Seed, fOverlap, fVerbose, pScript, nProcs ); ABC_FREE( pScript ); + if ( pNtkRes ) + { + pNtk = Abc_FrameReadNtk(pAbc); + pNtkRes = Abc_NtkStrash( pNtk, 1, 1, 0 ); + if ( pNtkRes == NULL ) + { + Abc_Print( -1, "Strashing has failed.\n" ); + return 1; + } + Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); + } return 0; usage: @@ -20664,15 +20931,17 @@ usage: ***********************************************************************/ int Abc_CommandRewire( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Abc_Ntk_t *Abc_ManRewire(Abc_Ntk_t *pNtk, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fVerbose); + extern Abc_Ntk_t *Abc_ManRewire(Abc_Ntk_t *pNtk, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fVerbose); Abc_Ntk_t *pNtk, *pTemp; - int c, nIters = 100000, nExpands = 128, nGrowth = 4, nDivs = -1, nFaninMax = 8, nSeed = 1, nTimeOut = 0, nVerbose = 1, nMode = 0, nMappedMode = 0, nDist = 0; + Gia_Man_t *pExc = NULL; + FILE *pFile = NULL; + int c, nIters = 100000, nExpands = 128, nGrowth = 4, nDivs = -1, nFaninMax = 8, nSeed = 1, nTimeOut = 0, nVerbose = 1, nMode = 0, nMappedMode = 0, nDist = 0, fCheck = 0; float nLevelGrowRatio = 0; Extra_UtilGetoptReset(); pNtk = Abc_FrameReadNtk(pAbc); - while ( ( c = Extra_UtilGetopt( argc, argv, "IEGDFSTMALRVh" ) ) != EOF ) { + while ( ( c = Extra_UtilGetopt( argc, argv, "IEGDFSTMALRCVch" ) ) != EOF ) { switch ( c ) { case 'I': if ( globalUtilOptind >= argc ) @@ -20773,6 +21042,22 @@ int Abc_CommandRewire( Abc_Frame_t * pAbc, int argc, char ** argv ) nLevelGrowRatio = atof(argv[globalUtilOptind]); globalUtilOptind++; break; + case 'C': + pFile = fopen( argv[globalUtilOptind], "rb" ); + if ( pFile == NULL ) + { + Abc_Print( -1, "Cannot open input file \"%s\".\n", argv[globalUtilOptind] ); + return 1; + } + fclose( pFile ); + pExc = Gia_AigerRead( argv[globalUtilOptind], 0, 0, 0 ); + if ( pExc == NULL ) + { + Abc_Print( -1, "Reading AIGER has failed.\n" ); + return 1; + } + globalUtilOptind++; + break; case 'V': if ( globalUtilOptind >= argc ) { @@ -20782,6 +21067,9 @@ int Abc_CommandRewire( Abc_Frame_t * pAbc, int argc, char ** argv ) nVerbose = atoi(argv[globalUtilOptind]); globalUtilOptind++; break; + case 'c': + fCheck ^= 1; + break; case 'h': default: goto usage; @@ -20797,13 +21085,20 @@ int Abc_CommandRewire( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Empty network.\n" ); return 1; } + if ( nMode == 0 && !Abc_NtkIsStrash(pNtk) ) + { + Abc_Print( -1, "Rewiring works only for the AIG representation (run \"strash\").\n" ); + return 1; + } if ( nMode >= 1 && Abc_FrameReadLibGen2() == NULL ) { Abc_Print( -1, "Library is not available.\n" ); return 1; } - pTemp = Abc_ManRewire( pNtk, nIters, nLevelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, nVerbose ); + pTemp = Abc_ManRewire( pNtk, pExc, nIters, nLevelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, fCheck, nVerbose ); + if ( pExc ) + Gia_ManStop( pExc ); Abc_FrameReplaceCurrentNetwork( pAbc, pTemp ); return 0; @@ -20818,9 +21113,11 @@ usage: Abc_Print( -2, "\t-R : level constraint (0: unlimited, 1: preserve level) [default = %g]\n", nLevelGrowRatio); Abc_Print( -2, "\t-M : optimization target [default = %s]\n", nMode ? "area" : "AIG node" ); Abc_Print( -2, "\t-A : mapper (0: amap, 1: &nf, 2: &simap) (experimental) [default = %d]\n", nMappedMode ); + Abc_Print( -2, "\t-C : AIGER specifying external cares\n"); Abc_Print( -2, "\t-S : the random seed (0: random, >= 1: user defined) [default = %d]\n", nSeed ); Abc_Print( -2, "\t-T : the timeout in seconds (0: unlimited) [default = %d]\n", nTimeOut ); Abc_Print( -2, "\t-V : the verbosity level [default = %d]\n", nVerbose ); + Abc_Print( -2, "\t-c : check the equivalence [default = %s]\n", fCheck ? "yes" : "no" ); Abc_Print( -2, "\t-h : prints the command usage\n" ); Abc_Print( -2, "\n\tThis command was contributed by Jiun-Hao Chen from National Taiwan University.\n" ); return 1; @@ -31525,7 +31822,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) int c; Pdr_ManSetDefaultParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIXalxrmuyfqipdegjonctkvwzh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIXalxrmuyfqipdegjonctkvwzhb" ) ) != EOF ) { switch ( c ) { @@ -31724,6 +32021,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'z': pPars->fNotVerbose ^= 1; break; + case 'b': + pPars->fBlocking ^= 1; + break; case 'h': default: goto usage; @@ -31804,6 +32104,7 @@ usage: Abc_Print( -2, "\t-v : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing detailed stats default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-z : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" ); + Abc_Print( -2, "\t-b : toggle clause pushing with blocking [default = %s]\n", pPars->fBlocking? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n\n"); Abc_Print( -2, "\t* Implementation of switches -S, -n, and -c is contributed by Zyad Hassan.\n"); Abc_Print( -2, "\t The theory and experiments supporting this work can be found in the following paper:\n"); @@ -34246,7 +34547,7 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv ) int c, fBest = 0; memset( pPars, 0, sizeof(Gps_Par_t) ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Dtpcnlmaszxbh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Dtpcnlmasozxbh" ) ) != EOF ) { switch ( c ) { @@ -34274,6 +34575,9 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv ) case 's': pPars->fSlacks ^= 1; break; + case 'o': + pPars->fMapOutStats ^= 1; + break; case 'z': pPars->fSkipMap ^= 1; break; @@ -34319,7 +34623,7 @@ int Abc_CommandAbc9Ps( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &ps [-tpcnlmaszxbh] [-D file]\n" ); + Abc_Print( -2, "usage: &ps [-tpcnlmasozxbh] [-D file]\n" ); Abc_Print( -2, "\t prints stats of the current AIG\n" ); Abc_Print( -2, "\t-t : toggle printing BMC tents [default = %s]\n", pPars->fTents? "yes": "no" ); Abc_Print( -2, "\t-p : toggle printing switching activity [default = %s]\n", pPars->fSwitch? "yes": "no" ); @@ -34329,6 +34633,7 @@ usage: Abc_Print( -2, "\t-m : toggle printing MUX/XOR statistics [default = %s]\n", pPars->fMuxXor? "yes": "no" ); Abc_Print( -2, "\t-a : toggle printing miter statistics [default = %s]\n", pPars->fMiter? "yes": "no" ); Abc_Print( -2, "\t-s : toggle printing slack distribution [default = %s]\n", pPars->fSlacks? "yes": "no" ); + Abc_Print( -2, "\t-o : toggle printing mapping output stats [default = %s]\n", pPars->fMapOutStats? "yes": "no" ); Abc_Print( -2, "\t-z : skip mapping statistics even if mapped [default = %s]\n", pPars->fSkipMap? "yes": "no" ); Abc_Print( -2, "\t-x : toggle using no color in the printout [default = %s]\n", pPars->fNoColor? "yes": "no" ); Abc_Print( -2, "\t-b : toggle printing saved AIG statistics [default = %s]\n", fBest? "yes": "no" ); @@ -44392,7 +44697,7 @@ int Abc_CommandAbc9Nf( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_Man_t * pNew; int c; Nf_ManSetDefaultPars( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "KCFARLEDQWakpqfvwh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "KCFARLEDQWZakpqfvwh" ) ) != EOF ) { switch ( c ) { @@ -44512,6 +44817,15 @@ int Abc_CommandAbc9Nf( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nVerbLimit < 0 ) goto usage; break; + case 'Z': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-Z\" should be followed by an output file name.\n" ); + goto usage; + } + pPars->ZFile = argv[globalUtilOptind]; + globalUtilOptind++; + break; case 'a': pPars->fAreaOnly ^= 1; break; @@ -44565,7 +44879,7 @@ usage: sprintf(Buffer, "best possible" ); else sprintf(Buffer, "%d", pPars->DelayTarget ); - Abc_Print( -2, "usage: &nf [-KCFARLEDQ num] [-akpqfvwh]\n" ); + Abc_Print( -2, "usage: &nf [-KCFARLEDQ num] [-Z file] [-akpqfvwh]\n" ); Abc_Print( -2, "\t performs technology mapping of the network\n" ); Abc_Print( -2, "\t-K num : LUT size for the mapping (2 <= K <= %d) [default = %d]\n", pPars->nLutSizeMax, pPars->nLutSize ); Abc_Print( -2, "\t-C num : the max number of priority cuts (1 <= C <= %d) [default = %d]\n", pPars->nCutNumMax, pPars->nCutNum ); @@ -44576,6 +44890,7 @@ usage: Abc_Print( -2, "\t-E num : the area/edge tradeoff parameter (0 <= num <= 100) [default = %d]\n", pPars->nAreaTuner ); Abc_Print( -2, "\t-D num : sets the delay constraint for the mapping [default = %s]\n", Buffer ); Abc_Print( -2, "\t-Q num : internal parameter impacting area of the mapping [default = %d]\n", pPars->nReqTimeFlex ); + Abc_Print( -2, "\t-Z file : the output file name to dump internal match info [default = unused]\n" ); Abc_Print( -2, "\t-a : toggles SAT-based area-oriented mapping (experimental) [default = %s]\n", pPars->fAreaOnly? "yes": "no" ); Abc_Print( -2, "\t-k : toggles coarsening the subject graph [default = %s]\n", pPars->fCoarsen? "yes": "no" ); Abc_Print( -2, "\t-p : toggles pin permutation (more matches - better quality) [default = %s]\n", pPars->fPinPerm? "yes": "no" ); @@ -46161,7 +46476,7 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv ) { Gia_Man_t *pNew; int c; - int iSeed = 0, nWords = 10, nTimeout = 0, nSchedulerVerbose = 1, nPartitionerVerbose = 0, nOptimizerVerbose = 0, nAnalyzerVerbose = 0, nSimulatorVerbose = 0, nSatSolverVerbose = 0, fUseBddCspf = 0, fUseBddMspf = 0, nConflictLimit = 0, nSortType = -1, nOptimizerFlow = 0, nSchedulerFlow = 0, nPartitionType = 0, nDistance = 0, nJobs = 1, nThreads = 1, nPartitionSize = 0, nPartitionSizeMin = 0, fDeterministic = 1, nParallelPartitions = 1, fOptOnInsert = 0, fGreedy = 1; + int iSeed = 0, nWords = 10, nTimeout = 0, nSchedulerVerbose = 0, nPartitionerVerbose = 0, nOptimizerVerbose = 0, nAnalyzerVerbose = 0, nSimulatorVerbose = 0, nSatSolverVerbose = 0, fUseBddCspf = 0, fUseBddMspf = 0, nConflictLimit = 0, nSortType = -1, nOptimizerFlow = 0, nSchedulerFlow = 0, nPartitionType = 0, nDistance = 0, nJobs = 1, nThreads = 1, nPartitionSize = 0, nPartitionSizeMin = 0, fDeterministic = 1, nParallelPartitions = 1, fOptOnInsert = 0, fGreedy = 1; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "XYZNJKLBDRWTCGVPOAQSabdegh" ) ) != EOF ) { @@ -46280,6 +46595,51 @@ int Abc_CommandAbc9Rrr( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } + if ( nSchedulerVerbose ) + { + Abc_Print( 2, "Using the following parameters :\n" ); + Abc_Print( 2, "\t-X %3d : method ", nOptimizerFlow ); + switch( nOptimizerFlow ) + { + case 0: + Abc_Print( 2, "(0 = single-add resub)" ); + break; + case 1: + Abc_Print( 2, "(1 = multi-add resub)" ); + break; + case 2: + Abc_Print( 2, "(2 = repeat single-add and multi-add resubs)" ); + break; + case 3: + Abc_Print( 2, "(3 = random one meaningful resub)" ); + break; + } + Abc_Print( 2, "\n" ); + Abc_Print( 2, "\t-Y %3d : flow ", nSchedulerFlow ); + switch ( nSchedulerFlow ) + { + case 0: + Abc_Print( 2, "(0 = apply method once)" ); + break; + case 1: + Abc_Print( 2, "(1 = iterate like transtoch)" ); + break; + case 2: + Abc_Print( 2, "(2 = iterate like deepsyn)" ); + break; + } + Abc_Print( 2, "\n" ); + Abc_Print( 2, "\t-N %3d : number of jobs to create by restarting or partitioning\n", nJobs ); + Abc_Print( 2, "\t-J %3d : number of threads\n", nThreads ); + Abc_Print( 2, "\t-K %3d : maximum partition size (0 = no partitioning)\n", nPartitionSize ); + Abc_Print( 2, "\t-L %3d : minimum partition size\n", nPartitionSizeMin ); + Abc_Print( 2, "\t-B %3d : maximum number of partitions to optimize in parallel\n", nParallelPartitions ); + Abc_Print( 2, "\t-R %3d : random number generator seed\n", iSeed ); + Abc_Print( 2, "\t-T %3d : timeout in seconds (0 = no timeout)\n", nTimeout ); + Abc_Print( 2, "\t-C %3d : conflict limit (0 = no limit)\n", nConflictLimit ); + Abc_Print( 2, "Use command line switch \"-h\" to see more options\n\n" ); + } + pNew = Gia_ManRrr( pAbc->pGia, iSeed, nWords, nTimeout, nSchedulerVerbose, nPartitionerVerbose, nOptimizerVerbose, nAnalyzerVerbose, nSimulatorVerbose, nSatSolverVerbose, fUseBddCspf, fUseBddMspf, nConflictLimit, nSortType, nOptimizerFlow, nSchedulerFlow, nPartitionType, nDistance, nJobs, nThreads, nPartitionSize, nPartitionSizeMin, fDeterministic, nParallelPartitions, fOptOnInsert, fGreedy ); Abc_FrameUpdateGia( pAbc, pNew ); @@ -46303,10 +46663,10 @@ usage: Abc_Print( -2, "\t 1: level base\n" ); Abc_Print( -2, "\t-N num : number of jobs to create by restarting or partitioning [default = %d]\n", nJobs ); Abc_Print( -2, "\t-J num : number of threads [default = %d]\n", nThreads ); - Abc_Print( -2, "\t-K num : partition size (0 = no partitioning) [default = %d]\n", nPartitionSize ); - Abc_Print( -2, "\t-K num : minimum partition size [default = %d]\n", nPartitionSizeMin ); - Abc_Print( -2, "\t-B num : max number of partitions in parallel [default = %d]\n", nParallelPartitions ); - Abc_Print( -2, "\t-D num : distance between nodes (0 = no limit) [default = %d]\n", nDistance ); + Abc_Print( -2, "\t-K num : maximum partition size (0 = no partitioning) [default = %d]\n", nPartitionSize ); + Abc_Print( -2, "\t-L num : minimum partition size [default = %d]\n", nPartitionSizeMin ); + Abc_Print( -2, "\t-B num : maximum number of partitions in parallel [default = %d]\n", nParallelPartitions ); + Abc_Print( -2, "\t-D num : maximum distance between node and new fanin (0 = no limit) [default = %d]\n", nDistance ); Abc_Print( -2, "\t-R num : random number generator seed [default = %d]\n", iSeed ); Abc_Print( -2, "\t-W num : number of simulation words [default = %d]\n", nWords ); Abc_Print( -2, "\t-T num : timeout in seconds (0 = no timeout) [default = %d]\n", nTimeout ); @@ -46321,7 +46681,7 @@ usage: Abc_Print( -2, "\t-a : use BDD-based analyzer (CSPF) [default = %s]\n", fUseBddCspf? "yes": "no" ); Abc_Print( -2, "\t-b : use BDD-based analyzer (MSPF) [default = %s]\n", fUseBddMspf? "yes": "no" ); Abc_Print( -2, "\t-d : ensure deterministic execution [default = %s]\n", fDeterministic? "yes": "no" ); - Abc_Print( -2, "\t-e : apply c2rs; dc2 after importing changes of partitions [default = %s]\n", fOptOnInsert? "yes": "no" ); + Abc_Print( -2, "\t-e : apply \"c2rs; dc2\" after importing changes of partitions [default = %s]\n", fOptOnInsert? "yes": "no" ); Abc_Print( -2, "\t-g : discard changes that increased the cost [default = %s]\n", fGreedy? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -46340,13 +46700,14 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Rewire( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t *Gia_ManRewire(Gia_Man_t *pGia, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fVerbose); - Gia_Man_t *pTemp; - int c, nIters = 100000, nExpands = 128, nGrowth = 4, nDivs = -1, nFaninMax = 8, nSeed = 1, nTimeOut = 0, nVerbose = 1, nMode = 0, nMappedMode = 0, nDist = 0; + extern Gia_Man_t *Gia_ManRewire(Gia_Man_t *pGia, Gia_Man_t *pExc, int nIters, float levelGrowRatio, int nExpands, int nGrowth, int nDivs, int nFaninMax, int nTimeOut, int nMode, int nMappedMode, int nDist, int nSeed, int fCheck, int fChoices, int fVerbose); + FILE *pFile = NULL; + Gia_Man_t *pTemp, *pExc = NULL; + int c, nIters = 100000, nExpands = 128, nGrowth = 4, nDivs = -1, nFaninMax = 8, nSeed = 1, nTimeOut = 0, nVerbose = 1, nMode = 0, nMappedMode = 0, nDist = 0, fCheck = 0, fChoices = 0; float nLevelGrowRatio = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "IEGDFSTMALRVh" ) ) != EOF ) { + while ( ( c = Extra_UtilGetopt( argc, argv, "IEGDFSTMALRCVcsh" ) ) != EOF ) { switch ( c ) { case 'I': if ( globalUtilOptind >= argc ) @@ -46447,6 +46808,22 @@ int Abc_CommandAbc9Rewire( Abc_Frame_t * pAbc, int argc, char ** argv ) nLevelGrowRatio = atof(argv[globalUtilOptind]); globalUtilOptind++; break; + case 'C': + pFile = fopen( argv[globalUtilOptind], "rb" ); + if ( pFile == NULL ) + { + Abc_Print( -1, "Cannot open input file \"%s\".\n", argv[globalUtilOptind] ); + return 1; + } + fclose( pFile ); + pExc = Gia_AigerRead( argv[globalUtilOptind], 0, 0, 0 ); + if ( pExc == NULL ) + { + Abc_Print( -1, "Reading AIGER has failed.\n" ); + return 1; + } + globalUtilOptind++; + break; case 'V': if ( globalUtilOptind >= argc ) { @@ -46456,6 +46833,12 @@ int Abc_CommandAbc9Rewire( Abc_Frame_t * pAbc, int argc, char ** argv ) nVerbose = atoi(argv[globalUtilOptind]); globalUtilOptind++; break; + case 'c': + fCheck ^= 1; + break; + case 's': + fChoices ^= 1; + break; case 'h': default: goto usage; @@ -46477,14 +46860,14 @@ int Abc_CommandAbc9Rewire( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } - pTemp = Gia_ManRewire( pAbc->pGia, nIters, nLevelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, nVerbose ); - if ( pTemp->pName == NULL ) - pTemp->pName = Abc_UtilStrsav(Extra_FileNameWithoutPath(pAbc->pGia->pName)); + pTemp = Gia_ManRewire( pAbc->pGia, pExc, nIters, nLevelGrowRatio, nExpands, nGrowth, nDivs, nFaninMax, nTimeOut, nMode, nMappedMode, nDist, nSeed, fCheck, fChoices, nVerbose ); + if ( pExc ) + Gia_ManStop( pExc ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: - Abc_Print( -2, "usage: &rewire [-IEGDFLRMASTV ]\n" ); + Abc_Print( -2, "usage: &rewire [-IEGDFLRMASTV ] [-csh]\n" ); Abc_Print( -2, "\t performs AIG re-wiring\n" ); Abc_Print( -2, "\t-I : the number of iterations [default = %d]\n", nIters ); Abc_Print( -2, "\t-E : the number of fanins to add to all nodes [default = %d]\n", nExpands ); @@ -46495,9 +46878,12 @@ usage: Abc_Print( -2, "\t-R : level constraint (0: unlimited, 1: preserve level) [default = %g]\n", nLevelGrowRatio); Abc_Print( -2, "\t-M : optimization target [default = %s]\n", nMode ? "area" : "AIG node" ); Abc_Print( -2, "\t-A : mapper (0: amap, 1: &nf, 2: &simap) (experimental) [default = %d]\n", nMappedMode ); + Abc_Print( -2, "\t-C : AIGER specifying external cares\n"); Abc_Print( -2, "\t-S : the random seed (0: random, >= 1: user defined) [default = %d]\n", nSeed ); Abc_Print( -2, "\t-T : the timeout in seconds (0: unlimited) [default = %d]\n", nTimeOut ); Abc_Print( -2, "\t-V : the verbosity level [default = %d]\n", nVerbose ); + Abc_Print( -2, "\t-c : check the equivalence [default = %s]\n", fCheck ? "yes" : "no" ); + Abc_Print( -2, "\t-s : toggle accumulating structural choices [default = %s]\n", fChoices ? "yes" : "no" ); Abc_Print( -2, "\t-h : prints the command usage\n" ); Abc_Print( -2, "\n\tThis command was contributed by Jiun-Hao Chen from National Taiwan University.\n" ); return 1; @@ -53233,10 +53619,10 @@ usage: ***********************************************************************/ int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Gia_ManStochSyn( int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript, int nProcs ); - int c, nMaxSize = 1000, nIters = 10, TimeOut = 0, Seed = 0, nProcs = 1, fVerbose = 0; char * pScript; + extern void Gia_ManStochSyn( int nSuppMax, int nMaxSize, int nIters, int TimeOut, int Seed, int fVerbose, char * pScript, int nProcs ); + int c, nSuppMax = 0, nMaxSize = 1000, nIters = 10, TimeOut = 0, Seed = 0, nProcs = 1, fVerbose = 0; char * pScript; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "NITSPvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "NMITSPvh" ) ) != EOF ) { switch ( c ) { @@ -53246,6 +53632,17 @@ int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Command line switch \"-N\" should be followed by an integer.\n" ); goto usage; } + nSuppMax = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nSuppMax < 0 ) + goto usage; + break; + case 'M': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" ); + goto usage; + } nMaxSize = atoi(argv[globalUtilOptind]); globalUtilOptind++; if ( nMaxSize < 0 ) @@ -53315,14 +53712,15 @@ int Abc_CommandAbc9StochSyn( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } pScript = Abc_UtilStrsav( argv[globalUtilOptind] ); - Gia_ManStochSyn( nMaxSize, nIters, TimeOut, Seed, fVerbose, pScript, nProcs ); + Gia_ManStochSyn( nSuppMax, nMaxSize, nIters, TimeOut, Seed, fVerbose, pScript, nProcs ); ABC_FREE( pScript ); return 0; usage: - Abc_Print( -2, "usage: &stochsyn [-NITSP ] [-tvh]