diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index f12ab35df..3e90ba0e6 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1805,9 +1805,10 @@ extern void Bnd_ManMap( int iLit, int id, int spec ); extern void Bnd_ManMerge( int id1, int id2, int phaseDiff ); extern void Bnd_ManFinalizeMappings(); extern void Bnd_ManPrintMappings(); +extern Gia_Man_t* Bnd_ManStackGias( Gia_Man_t *pSpec, Gia_Man_t *pImpl ); // for eco extern int Bnd_ManCheckBound( Gia_Man_t *p, int fVerbose ); -extern void Bnd_ManFindBound( Gia_Man_t *p ); +extern void Bnd_ManFindBound( Gia_Man_t *p, Gia_Man_t *pImpl ); extern Gia_Man_t* Bnd_ManGenSpecOut( Gia_Man_t *p ); extern Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t *p ); extern Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPatch ); diff --git a/src/aig/gia/giaBound.c b/src/aig/gia/giaBound.c index a420b818d..9ae21b459 100644 --- a/src/aig/gia/giaBound.c +++ b/src/aig/gia/giaBound.c @@ -28,7 +28,6 @@ struct Bnd_Man_t_ int nNode_patch; int nNode_patched; - int status; // 0: init 1: boundary found 2: out generated 3: patched generated int fVerbose; int combLoop_spec; @@ -43,6 +42,8 @@ struct Bnd_Man_t_ Vec_Ptr_t* vBmiter2Impl; Vec_Int_t* vSpec2Impl; Vec_Bit_t* vSpec2Impl_phase; + + Vec_Int_t* vImpl2Bmiter; Vec_Int_t* vBI; Vec_Int_t* vBO; @@ -98,6 +99,9 @@ Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl, int fVerbose ) p -> vSpec2Impl_phase = Vec_BitAlloc( Gia_ManObjNum(pSpec) ); Vec_IntFill( p -> vSpec2Impl, Gia_ManObjNum(pSpec), -1 ); Vec_BitFill( p -> vSpec2Impl_phase, Gia_ManObjNum(pSpec), 0 ); + + p -> vImpl2Bmiter = Vec_IntAlloc( Gia_ManObjNum(pImpl) ); + Vec_IntFill( p -> vImpl2Bmiter, Gia_ManObjNum(pImpl), -1 ); p -> vBI = Vec_IntAlloc(16); p -> vBO = Vec_IntAlloc(16); @@ -113,7 +117,6 @@ Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl, int fVerbose ) p -> nNode_patch = 0; p -> nNode_patched = 0; - p -> status = 0; p -> fVerbose = fVerbose; p -> combLoop_spec = 0; @@ -153,6 +156,7 @@ void Bnd_ManStop() Vec_PtrFree( pBnd-> vBmiter2Impl ); Vec_IntFree( pBnd-> vSpec2Impl ); Vec_BitFree( pBnd-> vSpec2Impl_phase ); + Vec_IntFree( pBnd-> vImpl2Bmiter ); Vec_IntFree( pBnd->vBI ); Vec_IntFree( pBnd->vBO ); @@ -260,6 +264,9 @@ void Bnd_ManFinalizeMappings() { // record the number of different choice of vEI_impl, vEO_impl Vec_IntSetEntry( pBnd->vImpl2Spec_diff, id, Vec_IntSize(vSpec)-1 ); + + // vImpl2Bmiter + Vec_IntSetEntry( pBnd->vImpl2Bmiter, id, i ); } @@ -332,41 +339,41 @@ void Bnd_ManPrintStats() warning = 1; printf("WARNING: multiple equiv nodes on the boundary of impl\n"); } - if ( p->feedthrough ) - { - warning = 1; - printf("WARNING: feedthrough inside patch\n"); - } printf("The outsides of spec and impl are %sEQ.\n", p->eq_out ? "" : "NOT " ); - printf("The patched impl and patch are %sEQ.\n", p->eq_res ? "" : "NOT " ); + printf("The patched impl is %sEQ. to spec (and impl)\n", p->eq_res ? "" : "NOT " ); // #internal // nBI, nBO // nBI_miss, nBO_miss - // nAI, nAO, nExtra + // nEI, nEO, nExtra // #spec, #impl, #patched // combLoop_spec, combLoop_impl - // status - // #different choice of impl on boundary + // #choice_impl + // #choice_spec + // #feedthrough // warning (may be neq) // eq_out, eq_res - // printf("\nRESULT\n"); - // printf("%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d\n", - // p->nInternal, - // p->nBI, p->nBO, - // p->nBI_miss, p->nBO_miss, - // Vec_IntSize(p->vEI_spec), Vec_IntSize(p->vEO_spec), p->nExtra, - // p->nNode_spec, p->nNode_impl, p->nNode_patched, - // p->combLoop_spec, p->combLoop_impl, - // p->status, - // p->nChoice_impl, - // p->nChoice_spec, - // p->feedthrough, - // warning, - // p->eq_out, p->eq_res - // ); + printf("\nRESULT\n"); + printf("%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d,%d\n", + p->nInternal, + p->nBI, p->nBO, + p->nBI_miss, p->nBO_miss, + Vec_IntSize(p->vEI_spec), Vec_IntSize(p->vEO_spec), p->nExtra, + p->nNode_spec, p->nNode_impl, p->nNode_patched, + p->combLoop_spec, p->combLoop_impl, + p->nChoice_impl, + p->nChoice_spec, + warning, + p->eq_out, p->eq_res + ); + + printf("#Choice Spec\t%d\n", p->nChoice_spec); + printf("#Choice Impl\t%d\n", p->nChoice_impl); + + + } /**Function************************************************************* @@ -541,7 +548,6 @@ int Bnd_ManCheckExtBound( Gia_Man_t * p, Vec_Int_t *vEI, Vec_Int_t *vEO ) } - /**Function************************************************************* Synopsis [] @@ -554,7 +560,7 @@ int Bnd_ManCheckExtBound( Gia_Man_t * p, Vec_Int_t *vEI, Vec_Int_t *vEO ) ***********************************************************************/ -void Bnd_ManFindBound( Gia_Man_t * p ) +void Bnd_ManFindBound( Gia_Man_t * p, Gia_Man_t * pImpl ) { Vec_Int_t *vFlag; Vec_Ptr_t *vQ; @@ -743,18 +749,16 @@ void Bnd_ManFindBound( Gia_Man_t * p ) // count number of choice of boundary - Vec_IntForEachEntry( vEI_spec, id, i ) - pBnd -> nChoice_impl += Vec_IntEntry( pBnd -> vSpec2Impl_diff, id ); Vec_IntForEachEntry( vEO_spec, id, i ) + { pBnd -> nChoice_impl += Vec_IntEntry( pBnd -> vSpec2Impl_diff, id ); - Vec_IntForEachEntry( vEI_impl, id, i ) - pBnd -> nChoice_spec += Vec_IntEntry( pBnd -> vImpl2Spec_diff, id ); + } Vec_IntForEachEntry( vEO_impl, id, i ) + { pBnd -> nChoice_spec += Vec_IntEntry( pBnd -> vImpl2Spec_diff, id ); - pBnd -> nChoice_spec -= ( pBnd->nBI + pBnd ->nBO - pBnd->nBI_miss - pBnd->nBO_miss); + } // print - pBnd -> status = 1; if ( pBnd -> fVerbose ) { printf("#EI = %d\t#EO = %d\t#Extra Node = %d\n", Vec_IntSize(vEI_spec) , Vec_IntSize(vEO_spec), cnt_extra ); @@ -764,8 +768,10 @@ void Bnd_ManFindBound( Gia_Man_t * p ) // check boundary has comb loop if ( !Bnd_ManCheckExtBound( p, vEI_spec, vEO_spec ) ) { + printf("Combinational loop exist\n"); pBnd -> combLoop_spec = 1; + } @@ -776,7 +782,6 @@ void Bnd_ManFindBound( Gia_Man_t * p ) - /**Function************************************************************* Synopsis [] @@ -804,18 +809,6 @@ Gia_Man_t* Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec return 0; } - // detect feedthrough - Gia_ManFillValue(p); - Vec_IntForEachEntry(vEO, id, i) - { - Gia_ManObj(p, id) -> Value = 1; - } - Vec_IntForEachEntry(vEI, id, i) - { - if ( Gia_ManObj(p, id) -> Value == 1 ) - pBnd -> feedthrough = 1; - } - // initialize pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew -> pName = ABC_ALLOC( char, strlen(p->pName)+10); @@ -847,7 +840,6 @@ Gia_Man_t* Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec } } - // add aig nodes Gia_ManForEachAnd(p, pObj, i) { @@ -899,8 +891,7 @@ Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t* p) { if ( pBnd -> fVerbose ) printf("Generating impl_out with given boundary.\n"); Gia_Man_t *pNew = Bnd_ManCutBoundary( p, pBnd->vEI_impl, pBnd->vEO_impl, pBnd->vEI_phase, pBnd->vEO_phase ); - if ( pNew ) pBnd -> status = 2; - else pBnd -> combLoop_impl = 1; + if (!pNew) pBnd -> combLoop_impl = 1; return pNew; } @@ -1056,7 +1047,6 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat Gia_ManStop( pTemp ); pBnd -> nNode_patched = Gia_ManAndNum( pNew ); - pBnd -> status = 3; return pNew; } @@ -1142,7 +1132,6 @@ Gia_Man_t* Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec ) Gia_ManStop( pTemp ); pBnd -> nNode_patched = Gia_ManAndNum( pNew ); - pBnd -> status = 3; return pNew; } @@ -1243,6 +1232,99 @@ Gia_Man_t* Bnd_ManGenPatched2( Gia_Man_t *pImpl, Gia_Man_t *pPatch, int fSkipStr } +Gia_Man_t* Bnd_ManStackGias( Gia_Man_t *pSpec, Gia_Man_t *pImpl ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + + int i, iLit; + if ( Gia_ManBufNum(pSpec) == 0 ) { + printf( "The spec AIG should have a boundary.\n" ); + return NULL; + } + if ( Gia_ManBufNum(pImpl) != 0 ) { + printf( "The impl AIG should have no boundary.\n" ); + return NULL; + } + + assert( Gia_ManBufNum(pSpec) > 0 ); + assert( Gia_ManBufNum(pImpl) == 0 ); + assert( Gia_ManRegNum(pSpec) == 0 ); + assert( Gia_ManRegNum(pImpl) == 0 ); + assert( Gia_ManCiNum(pSpec) == Gia_ManCiNum(pImpl) ); + assert( Gia_ManCoNum(pSpec) == Gia_ManCoNum(pImpl) ); + + pNew = Gia_ManStart( Gia_ManObjNum(pSpec) + Gia_ManObjNum(pImpl) ); + pNew->pName = ABC_ALLOC( char, strlen(pSpec->pName) + 10 ); + sprintf( pNew->pName, "%s_stack", pSpec->pName ); + + Gia_ManHashStart( pNew ); + Gia_ManConst0(pSpec)->Value = 0; + Gia_ManConst0(pImpl)->Value = 0; + + for( int i = 0; i < Gia_ManCiNum(pSpec); i++ ) + { + int iLit = Gia_ManCi(pSpec, i)->Value = Gia_ManCi(pImpl, i) -> Value = Gia_ManAppendCi(pNew); + + pObj = Gia_ManCi(pSpec, i); + Bnd_ManMap( iLit, Gia_ObjId( pSpec, pObj ), 1 ); + + pObj = Gia_ManCi(pImpl, i); + Bnd_ManMap( iLit, Gia_ObjId( pImpl, pObj) , 0 ); + } + + // record the corresponding impl node of each lit + Gia_ManForEachAnd( pImpl, pObj, i ) + { + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( pBnd ) Bnd_ManMap( pObj -> Value, Gia_ObjId(pImpl, pObj), 0 ); + } + + Vec_Int_t* vFlag = Vec_IntAlloc( Gia_ManObjNum( pSpec ) ); + Vec_IntFill( vFlag, Gia_ManObjNum(pSpec), 0 ); + int count = 0; + Gia_ManForEachBuf( pSpec, pObj, i ) + { + if ( count < pBnd -> nBI ) + { + // it's BI, don't record buf + Vec_IntSetEntry( vFlag, Gia_ObjId( pSpec, pObj ), 1 ); + } + else + { + // it's BO, don't record buf's fanin + Vec_IntSetEntry( vFlag, Gia_ObjId( pSpec, Gia_ObjFanin0( pObj ) ), 1 ); + } + count++; + } + + // record hashed equivalent nodes + Gia_ManForEachAnd( pSpec, pObj, i ) + { + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( Vec_IntEntry( vFlag, Gia_ObjId( pSpec, pObj ) ) == 0 ) + { + Bnd_ManMap( pObj -> Value, Gia_ObjId(pSpec, pObj), 1 ); + } + } + Vec_IntFree( vFlag ); + + Gia_ManForEachCo( pImpl, pObj, i ) + { + iLit = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + Gia_ManForEachCo( pSpec, pObj, i ) + { + iLit = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 46c6f4da0..92eb2ac89 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -5712,10 +5712,10 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ) int iLit = Gia_ManCi(p1, i)->Value = Gia_ManCi(p2, i) -> Value = Gia_ManAppendCi(pNew); pObj = Gia_ManCi(p1, i); - Bnd_ManMap( iLit, Gia_ObjId( p1, pObj ), 1 ); + if ( pBnd ) Bnd_ManMap( iLit, Gia_ObjId( p1, pObj ), 1 ); pObj = Gia_ManCi(p2, i); - Bnd_ManMap( iLit, Gia_ObjId( p2, pObj) , 0 ); + if ( pBnd ) Bnd_ManMap( iLit, Gia_ObjId( p2, pObj) , 0 ); } @@ -5723,14 +5723,14 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ) Gia_ManForEachAnd( p2, pObj, i ) { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Bnd_ManMap( pObj -> Value, Gia_ObjId(p2, pObj), 0 ); + if ( pBnd ) Bnd_ManMap( pObj -> Value, Gia_ObjId(p2, pObj), 0 ); } // record hashed equivalent nodes Gia_ManForEachAnd( p1, pObj, i ) { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Bnd_ManMap( pObj -> Value, Gia_ObjId(p1, pObj), 1 ); + if ( pBnd ) Bnd_ManMap( pObj -> Value, Gia_ObjId(p1, pObj), 1 ); } Gia_ManForEachCo( p2, pObj, i ) @@ -5741,6 +5741,7 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ) { iLit = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); } + // Vec_IntForEachEntry( vLits, iLit, i ) // Gia_ManAppendCo( pNew, iLit ); // Vec_IntFree( vLits ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index d6363a0cc..7084b5897 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -52115,12 +52115,27 @@ int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv ) // parse options Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "vhCk" ) ) != EOF ) { switch ( c ) { case 'v': fVerbose ^= 1; + pParsFra->fVerbose ^= 1; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pParsFra->nBTLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pParsFra->nBTLimit < 0 ) + goto usage; + break; + case 'k': + pParsFra ->fUseCones ^= 1; break; case 'h': goto usage; @@ -52189,13 +52204,14 @@ int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( success ) { // create bmiter, run fraig, record mapping - pBmiter = Gia_ManBoundaryMiter( pSpec, pAbc->pGia, 0 ); + // pBmiter = Gia_ManBoundaryMiter( pSpec, pAbc->pGia, 0 ); + pBmiter = Bnd_ManStackGias( pSpec, pAbc->pGia ); pTemp = Cec4_ManSimulateTest( pBmiter, pParsFra ); Gia_ManStop(pBmiter); Gia_ManStop(pTemp); // find - Bnd_ManFindBound( pSpec ); + Bnd_ManFindBound( pSpec, pAbc->pGia ); // create spec_out and pSpec_out = Bnd_ManGenSpecOut( pSpec );