diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index db4072d71..665164eb2 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -5719,6 +5719,139 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ) return pNew; } +/**Function************************************************************* + Synopsis [Duplicates AIG while putting objects in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManImplFromBMiter( Gia_Man_t * p, int nPo, int nBInput ) +{ + Gia_Man_t * pNew, *pTemp; + Gia_Obj_t * pObj, *pObj2; + int i; + int nBoundI = 0, nBoundO = 0; + int nExtra; + Gia_ManFillValue( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + // pNew->pName = Abc_UtilStrsav( p->pName ); + // pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + + // add po of impl + Gia_ManForEachCo( p, pObj, i ) + { + if ( i < nPo ) + { + Gia_ManDupOrderDfs_rec( pNew, p, pObj ); + } + } + nExtra = Gia_ManAndNum( pNew ); + + // add boundary as buf + Gia_ManForEachCo( p, pObj, i ) + { + if ( i >= 2 * nPo ) + { + pObj2 = Gia_ObjFanin0(pObj); + if (~pObj2->Value) // visited boundary + { + if ( i >= 2 * nPo + nBInput ) + { + nBoundO ++; + } + else nBoundI ++; + } + + Gia_ManDupOrderDfs_rec( pNew, p, pObj2 ); + Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) ); + } + } + nExtra = Gia_ManAndNum( pNew ) - nExtra - Gia_ManBufNum( pNew ); + + Gia_ManForEachCi( p, pObj, i ) + if ( !~pObj->Value ) + pObj->Value = Gia_ManAppendCi(pNew); + assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) ); + + Gia_ManDupRemapCis( pNew, p ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + + + printf( "synthesized implementation:\n" ); + printf( "\t%d / %d input boundary recovered.\n", nBoundI, nBInput ); + printf( "\t%d / %d output boundary recovered.\n", nBoundO, Gia_ManCoNum(p)-2*nPo-nBInput ); + printf( "\t%d / %d unused nodes in the box.\n", nExtra, Gia_ManAndNum(pNew) - Gia_ManBufNum( pNew ) ); + + return pNew; +} + +/**Function************************************************************* + + Synopsis [Duplicates AIG while putting objects in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManMiterFromBMiter( Gia_Man_t * p, int nPo ) +{ + Gia_Man_t * pNew, *pTemp; + Gia_Obj_t * pObj, *pObj2; + int i, iXor, iPo, i1, i2; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( "miter" ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + + // create primary inputs + Gia_ManForEachCi( p, pObj, i ) + if ( !~pObj->Value ) + pObj->Value = Gia_ManAppendCi(pNew); + + Gia_ManForEachCo( p, pObj, i ) + { + if ( i == nPo ) + { + break; + } + else + { + pObj2 = Gia_ManCo( p, i + nPo ); + + i1 = Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(pObj) ); + i2 = Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(pObj2) ); + + iXor = Gia_ManAppendXor2( pNew, Gia_ObjFaninC0(pObj) ? i1+1 : i1 , Gia_ObjFaninC0(pObj2 ) ? i2+1 : i2 ); + if ( i > 0 ) + { + iPo = Gia_ManAppendOr2( pNew, iPo, iXor ); + } + else + { + iPo = iXor; + } + } + } + Gia_ManAppendCo( pNew, iPo ); + + + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + pNew = Gia_ManDupNormalize( pTemp = pNew, 0 ); + Gia_ManStop( pTemp ); + + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 5bc50032c..906b456ad 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -597,6 +597,7 @@ static int Abc_CommandAbc9ProdAdd ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9AddFlop ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9BMiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GenHie ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9RecoverBoundary ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1376,6 +1377,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&addflop", Abc_CommandAbc9AddFlop, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bmiter", Abc_CommandAbc9BMiter, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gen_hie", Abc_CommandAbc9GenHie, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&rb", Abc_CommandAbc9RecoverBoundary, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); { @@ -51809,6 +51811,133 @@ usage: Abc_Print( -2, "\t (the PO count of should not be less than the PI count of )\n"); return 1;} +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9RecoverBoundary( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_ManDeepSyn( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fVerbose ); + extern Gia_Man_t * Gia_ManImplFromBMiter( Gia_Man_t * p, int nPo, int nBInput ); + extern Gia_Man_t * Gia_ManMiterFromBMiter( Gia_Man_t * p, int nPo ); + int c, nIters = 1, nNoImpr = ABC_INFINITY, TimeOut = 20, nAnds = 0, Seed = 0, fUseTwo = 0, fVerbose = 0; + + int fKeepBMiter = 0; + Gia_Man_t * pMiter; + Gia_Man_t * pImpl; + Gia_Man_t * pDup; + Gia_Obj_t* pObj; + Gia_Man_t * pSpec = NULL; + char ** pArgvNew; + int i, nArgcNew, nPo; + int nBInput = -1; + char *FileName; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vkhI," ) ) != EOF ) + { + switch ( c ) + { + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nBInput = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nBInput < 0 ) + goto usage; + break; + case 'k': + fKeepBMiter ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + pArgvNew = argv + globalUtilOptind; + nArgcNew = argc - globalUtilOptind; + if ( nArgcNew != 1 ) + { + Abc_Print( -1, "There is no file name.\n" ); + return 1; + } + + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9RecoverBoundary(): There is no AIG.\n" ); + return 0; + } + FileName = pArgvNew[0]; + + + // printing + + // Gia_ManForEachCo( pAbc->pGia, pObj, i ){ + // printf("Original node: %s id: %i\n", Gia_ObjCoName(pAbc->pGia, i), i); + // } + + + /* + // perform heavy synthesis + pTemp = Gia_ManDeepSyn( pAbc->pGia, nIters, nNoImpr, TimeOut, nAnds, Seed, fUseTwo, fVerbose ); + Abc_FrameUpdateGia( pAbc, pTemp ); + // print spec/impl and boundary information + Gia_ManForEachCo( pAbc->pGia, pObj, i ){ + printf("Output node: %s id: %i\n", Gia_ObjCoName(pAbc->pGia, i), i); + } + */ + + + + // check boundary recovery status + pSpec = Gia_AigerRead( FileName, false, true, 0 ); + if ( !pSpec ) + { + Abc_Print( -1, "Abc_CommandAbc9RecoverBoundary(): fail to read spec.\n" ); + return 1; + } + nPo = Gia_ManCoNum( pSpec ); + + // duplicate + pDup = Gia_ManDup( pAbc->pGia ); + + // option 1: remove po and keep the buffers + // default nbinput: + if ( nBInput == -1 ) nBInput = (Gia_ManCoNum(pDup)-2*nPo)/2; + pImpl = Gia_ManImplFromBMiter( pDup, nPo, nBInput ); + + // option 2: build miter (with uif?) + if (!fKeepBMiter ) + { + pMiter = Gia_ManMiterFromBMiter( pAbc->pGia, nPo ); + Abc_FrameUpdateGia( pAbc, pMiter ); + } + + return 0; + +usage: + Abc_Print( -2, "usage: &rb [-vkh] \n" ); + Abc_Print( -2, "\t generate an implementation aig with specification boundary\n" ); + Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-k : keep the bmiter and print the boundary status only.\n"); + Abc_Print( -2, "\t-I num : the number of inputs in the boundary\n"); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t : the specification file\n"); + return 1; +} /**Function*************************************************************