diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 3e90ba0e6..a850935eb 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1806,6 +1806,8 @@ 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 ); +extern int Bnd_ManCheckCoMerged( Gia_Man_t *p ); + // for eco extern int Bnd_ManCheckBound( Gia_Man_t *p, int fVerbose ); extern void Bnd_ManFindBound( Gia_Man_t *p, Gia_Man_t *pImpl ); diff --git a/src/aig/gia/giaBound.c b/src/aig/gia/giaBound.c index 9ae21b459..f7811967d 100644 --- a/src/aig/gia/giaBound.c +++ b/src/aig/gia/giaBound.c @@ -38,12 +38,14 @@ struct Bnd_Man_t_ int nChoice_impl; int feedthrough; + int maxNumClass; + Vec_Ptr_t* vBmiter2Spec; Vec_Ptr_t* vBmiter2Impl; - Vec_Int_t* vSpec2Impl; - Vec_Bit_t* vSpec2Impl_phase; + Vec_Bit_t* vSpec2Impl_phase; // TODO: record all phases Vec_Int_t* vImpl2Bmiter; + Vec_Int_t* vSpec2Bmiter; Vec_Int_t* vBI; Vec_Int_t* vBO; @@ -54,9 +56,6 @@ struct Bnd_Man_t_ Vec_Bit_t* vEI_phase; Vec_Bit_t* vEO_phase; - Vec_Int_t* vSpec2Impl_diff; - Vec_Int_t* vImpl2Spec_diff; // note that this include bufs, which should merge into their fanins - }; Bnd_Man_t* pBnd = 0; @@ -68,6 +67,12 @@ Bnd_Man_t* pBnd = 0; void Bnd_ManSetEqOut( int eq ) { pBnd -> eq_out = eq;} void Bnd_ManSetEqRes( int eq ) { pBnd -> eq_res = eq;} +Vec_Int_t* Bnd_ManSpec2Impl( int id ) { return (Vec_Int_t*)Vec_PtrEntry( pBnd -> vBmiter2Impl, Vec_IntEntry( pBnd->vSpec2Bmiter, id ) ); } +int Bnd_ManSpec2ImplNum( int id ) { return Vec_IntSize( (Vec_Int_t*)Vec_PtrEntry( pBnd -> vBmiter2Impl, Vec_IntEntry( pBnd->vSpec2Bmiter, id ) ) ); } + +Vec_Int_t* Bnd_ManImpl2Spec( int id ) { return (Vec_Int_t*)Vec_PtrEntry( pBnd -> vBmiter2Spec, Vec_IntEntry( pBnd->vImpl2Bmiter, id ) ); } +int Bnd_ManImpl2SpecNum( int id ) { return Vec_IntSize( (Vec_Int_t*)Vec_PtrEntry( pBnd -> vBmiter2Spec, Vec_IntEntry( pBnd->vImpl2Bmiter, id ) ) ); } + /**Function************************************************************* Synopsis [] @@ -85,23 +90,26 @@ Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl, int fVerbose ) int i; Bnd_Man_t* p = ABC_CALLOC( Bnd_Man_t, 1 ); - p -> vBmiter2Spec = Vec_PtrAlloc( Gia_ManObjNum(pSpec) + Gia_ManObjNum(pImpl) ); - p -> vBmiter2Impl = Vec_PtrAlloc( Gia_ManObjNum(pSpec) + Gia_ManObjNum(pImpl) ); - Vec_PtrFill( p -> vBmiter2Spec, (Gia_ManObjNum(pSpec) + Gia_ManObjNum(pImpl)), 0 ); - Vec_PtrFill( p -> vBmiter2Impl, (Gia_ManObjNum(pSpec) + Gia_ManObjNum(pImpl)), 0 ); + p -> maxNumClass = Gia_ManCiNum( pSpec ) + Gia_ManAndNotBufNum(pSpec) + Gia_ManAndNum(pImpl) + 2 + Gia_ManCoNum(pSpec) * 2; + // one for constant node and one for dummy + + p -> vBmiter2Spec = Vec_PtrAlloc( p -> maxNumClass ); + p -> vBmiter2Impl = Vec_PtrAlloc( p -> maxNumClass ); + Vec_PtrFill( p -> vBmiter2Spec, p -> maxNumClass, 0 ); + Vec_PtrFill( p -> vBmiter2Impl, p -> maxNumClass, 0 ); for( i = 0; i < Vec_PtrSize( p -> vBmiter2Impl ); i ++ ) { Vec_PtrSetEntry( p -> vBmiter2Spec, i, Vec_IntAlloc(1) ); Vec_PtrSetEntry( p -> vBmiter2Impl, i, Vec_IntAlloc(1) ); } - p -> vSpec2Impl = Vec_IntAlloc( Gia_ManObjNum(pSpec) ); 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 ); + Vec_IntFill( p -> vImpl2Bmiter, Gia_ManObjNum(pImpl), p -> maxNumClass - 1 ); + p -> vSpec2Bmiter = Vec_IntAlloc( Gia_ManObjNum(pSpec) ); + Vec_IntFill( p -> vSpec2Bmiter, Gia_ManObjNum(pSpec), p -> maxNumClass - 1); p -> vBI = Vec_IntAlloc(16); p -> vBO = Vec_IntAlloc(16); @@ -128,12 +136,6 @@ Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl, int fVerbose ) p -> nChoice_impl = 0; p -> feedthrough = 0; - p -> vSpec2Impl_diff = Vec_IntAlloc( Gia_ManObjNum(pSpec) ); - Vec_IntFill( p -> vSpec2Impl_diff, Gia_ManObjNum(pSpec), 0 ); - - p -> vImpl2Spec_diff = Vec_IntAlloc( Gia_ManObjNum(pImpl) ); - Vec_IntFill( p -> vImpl2Spec_diff, Gia_ManObjNum(pImpl), 0 ); - return p; } @@ -154,9 +156,9 @@ void Bnd_ManStop() Vec_PtrFree( pBnd-> vBmiter2Spec ); Vec_PtrFree( pBnd-> vBmiter2Impl ); - Vec_IntFree( pBnd-> vSpec2Impl ); Vec_BitFree( pBnd-> vSpec2Impl_phase ); Vec_IntFree( pBnd-> vImpl2Bmiter ); + Vec_IntFree( pBnd-> vSpec2Bmiter ); Vec_IntFree( pBnd->vBI ); Vec_IntFree( pBnd->vBO ); @@ -167,9 +169,6 @@ void Bnd_ManStop() Vec_BitFree( pBnd->vEI_phase ); Vec_BitFree( pBnd->vEO_phase ); - Vec_IntFree( pBnd-> vSpec2Impl_diff ); - Vec_IntFree( pBnd-> vImpl2Spec_diff ); - ABC_FREE( pBnd ); } @@ -235,7 +234,6 @@ void Bnd_ManFinalizeMappings() Vec_Ptr_t* vBmiter2Spec = pBnd -> vBmiter2Spec; Vec_Ptr_t* vBmiter2Impl = pBnd -> vBmiter2Impl; - Vec_Int_t* vSpec2Impl = pBnd -> vSpec2Impl; Vec_Int_t *vSpec, *vImpl; int i, j, id; @@ -249,27 +247,16 @@ void Bnd_ManFinalizeMappings() vSpec = (Vec_Int_t *)Vec_PtrEntry( vBmiter2Spec, i ); vImpl = (Vec_Int_t *)Vec_PtrEntry( vBmiter2Impl, i ); - // create spec2impl - if ( Vec_IntSize(vSpec) != 0 && Vec_IntSize(vImpl) != 0 ) + Vec_IntForEachEntry( vSpec, id, j ) { - Vec_IntForEachEntry( vSpec, id, j ) - { - Vec_IntSetEntry( vSpec2Impl, id, Vec_IntEntry(vImpl, 0) ); - - // record the number of different choice of vEI_impl, vEO_impl - Vec_IntSetEntry( pBnd->vSpec2Impl_diff, id, Vec_IntSize(vImpl)-1 ); - } - - Vec_IntForEachEntry( vImpl, id, j ) - { - // 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 ); - } - + // vSpec2Bmiter + Vec_IntSetEntry( pBnd->vSpec2Bmiter, id, i ); + } + Vec_IntForEachEntry( vImpl, id, j ) + { + // vImpl2Bmiter + Vec_IntSetEntry( pBnd->vImpl2Bmiter, id, i ); } // count number of nodes merged into the same circuit @@ -283,7 +270,6 @@ void Bnd_ManFinalizeMappings() } } - } void Bnd_ManPrintMappings() { @@ -512,7 +498,7 @@ int Bnd_CheckFlagRec( Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t* vFlag ) Synopsis [] - Description [] + Description [check if combnational loop exist in the extended boundary] SideEffects [] @@ -552,14 +538,14 @@ int Bnd_ManCheckExtBound( Gia_Man_t * p, Vec_Int_t *vEI, Vec_Int_t *vEO ) Synopsis [] - Description [] + Description [find the extended boundary in spec + and compute the corresponding boundary in impl] SideEffects [] SeeAlso [] ***********************************************************************/ - void Bnd_ManFindBound( Gia_Man_t * p, Gia_Man_t * pImpl ) { Vec_Int_t *vFlag; @@ -570,7 +556,6 @@ void Bnd_ManFindBound( Gia_Man_t * p, Gia_Man_t * pImpl ) Vec_Int_t *vAI = Vec_IntAlloc(16); Vec_Int_t *vAO = Vec_IntAlloc(16); - Vec_Int_t *vSpec2Impl = pBnd -> vSpec2Impl; Vec_Bit_t *vSpec2Impl_phase = pBnd -> vSpec2Impl_phase; Vec_Int_t *vBI = pBnd -> vBI; Vec_Int_t *vBO = pBnd -> vBO; @@ -607,7 +592,7 @@ void Bnd_ManFindBound( Gia_Man_t * p, Gia_Man_t * pImpl ) // compute EO, travse with flag 1 Vec_IntForEachEntry( vBO, id, i ) { - if ( Vec_IntEntry( vSpec2Impl, id ) == -1 ) // BO not matched + if ( Bnd_ManSpec2ImplNum(id) == 0 ) // BO not matched { Vec_PtrPush( vQ, Gia_ManObj(p, id) ); } @@ -630,7 +615,7 @@ void Bnd_ManFindBound( Gia_Man_t * p, Gia_Man_t * pImpl ) // printf("%d\n", id); - if ( Vec_IntEntry( vSpec2Impl, id ) != -1 ) // matched + if ( Bnd_ManSpec2ImplNum(id) != 0 ) // matched { Vec_IntPush( vEO_spec, id ); Vec_IntPush( vAO, id ); @@ -679,7 +664,7 @@ void Bnd_ManFindBound( Gia_Man_t * p, Gia_Man_t * pImpl ) // add unmatched BI to queue Vec_IntForEachEntry( vBI, id, i ) { - if ( Vec_IntEntry( vSpec2Impl, id ) == -1 ) // BO not matched + if ( Bnd_ManSpec2ImplNum(id) == 0 ) // BO not matched { Vec_PtrPush( vQ, Gia_ManObj(p, id) ); } @@ -715,7 +700,7 @@ void Bnd_ManFindBound( Gia_Man_t * p, Gia_Man_t * pImpl ) // printf("%d\n", id); - if ( Vec_IntEntry(vFlag, id) != 1 && Vec_IntEntry( vSpec2Impl, id ) != -1 ) // matched + if ( Vec_IntEntry(vFlag, id) != 1 && Bnd_ManSpec2ImplNum(id) != 0 ) // matched { Vec_IntPush( vEI_spec, id ); Vec_IntPush( vAI, id ); @@ -738,12 +723,12 @@ void Bnd_ManFindBound( Gia_Man_t * p, Gia_Man_t * pImpl ) // gen vEI_impl, vEO_impl, vEI_phase, vEO_phase Vec_IntForEachEntry( vEI_spec, id, i ) { - Vec_IntPush( vEI_impl, Vec_IntEntry( vSpec2Impl, id ) ); + Vec_IntPush( vEI_impl, Vec_IntEntry( Bnd_ManSpec2Impl(id) , 0 ) ); Vec_BitPush( vEI_phase, Vec_BitEntry( vSpec2Impl_phase, id ) ); } Vec_IntForEachEntry( vEO_spec, id, i ) { - Vec_IntPush( vEO_impl, Vec_IntEntry( vSpec2Impl, id ) ); + Vec_IntPush( vEO_impl, Vec_IntEntry( Bnd_ManSpec2Impl(id), 0 ) ); Vec_BitPush( vEO_phase, Vec_BitEntry( vSpec2Impl_phase, id ) ); } @@ -751,11 +736,11 @@ void Bnd_ManFindBound( Gia_Man_t * p, Gia_Man_t * pImpl ) // count number of choice of boundary Vec_IntForEachEntry( vEO_spec, id, i ) { - pBnd -> nChoice_impl += Vec_IntEntry( pBnd -> vSpec2Impl_diff, id ); + pBnd -> nChoice_impl += Bnd_ManSpec2ImplNum( id ) - 1; } Vec_IntForEachEntry( vEO_impl, id, i ) { - pBnd -> nChoice_spec += Vec_IntEntry( pBnd -> vImpl2Spec_diff, id ); + pBnd -> nChoice_spec += Bnd_ManImpl2SpecNum( id ) - 1; } // print @@ -781,7 +766,6 @@ void Bnd_ManFindBound( Gia_Man_t * p, Gia_Man_t * pImpl ) } - /**Function************************************************************* Synopsis [] @@ -793,7 +777,6 @@ void Bnd_ManFindBound( Gia_Man_t * p, Gia_Man_t * pImpl ) SeeAlso [] ***********************************************************************/ - Gia_Man_t* Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec_Bit_t* vEI_phase, Vec_Bit_t* vEO_phase ) { Gia_Man_t * pNew, * pTemp; @@ -925,6 +908,17 @@ void Bnd_AddNodeRec( Gia_Man_t *p, Gia_Man_t *pNew, Gia_Obj_t *pObj, int fSkipSt } } +/**Function************************************************************* + + Synopsis [] + + Description [perform ECO directly (not used)] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPatch ) { @@ -1051,6 +1045,17 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat return pNew; } +/**Function************************************************************* + + Synopsis [] + + Description [recover bounadry] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Gia_Man_t* Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec ) { @@ -1136,6 +1141,18 @@ Gia_Man_t* Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec ) return pNew; } +/**Function************************************************************* + + Synopsis [] + + Description [perform eco with recovered boundary. + bnd_man is not used] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Gia_Man_t* Bnd_ManGenPatched2( Gia_Man_t *pImpl, Gia_Man_t *pPatch, int fSkipStrash, int fVerbose ) { @@ -1318,12 +1335,36 @@ Gia_Man_t* Bnd_ManStackGias( Gia_Man_t *pSpec, Gia_Man_t *pImpl ) iLit = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); } + // miter + // Gia_ManForEachCo( pImpl, pObj, i ) + // { + // iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManCo(pSpec,i)) ); + // Gia_ManAppendCo( pNew, iLit ); + // } + + Gia_ManHashStop( pNew ); pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); return pNew; } +int Bnd_ManCheckCoMerged( Gia_Man_t* p ) +{ + int nCO = Gia_ManCoNum(p)/2; + + Gia_Obj_t* pObj1; + Gia_Obj_t* pObj2; + + for ( int i = 0; i < nCO; i++ ) + { + pObj1 = Gia_ManCo(p, i); + pObj2 = Gia_ManCo(p, i + nCO); + if ( Gia_ObjFaninLit0p(p, pObj1) != Gia_ObjFaninLit0p(p, pObj2) ) return 0; + } + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 7084b5897..70b392b3c 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -52081,6 +52081,7 @@ usage: Abc_Print( -2, "\t (the PO count of should not be less than the PI count of )\n"); return 1;} +extern Bnd_Man_t* pBnd; /**Function************************************************************* Synopsis [] @@ -52092,8 +52093,6 @@ usage: SeeAlso [] ***********************************************************************/ - -extern Bnd_Man_t* pBnd; int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv ) { extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ); @@ -52102,7 +52101,7 @@ int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_Man_t *pSpec, *pImpl_out = 0, *pSpec_out = 0, *pMiter, *pPatched = 0, *pTemp, *pBmiter; char * FileName = NULL; FILE * pFile = NULL; - int c, fVerbose = 0, success = 1; + int c, fVerbose = 0, success = 1, fEq = 1, fEqOut = 1; // params Gps_Par_t Pars, * pPars = &Pars; @@ -52115,7 +52114,7 @@ int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv ) // parse options Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vhCk" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "vhCkeo" ) ) != EOF ) { switch ( c ) { @@ -52137,6 +52136,12 @@ int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'k': pParsFra ->fUseCones ^= 1; break; + case 'e': + fEq ^= 1; + break; + case 'o': + fEqOut ^= 1; + break; case 'h': goto usage; default: @@ -52182,34 +52187,33 @@ int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv ) // start boundary manager pBnd = Bnd_ManStart( pSpec, pAbc->pGia, fVerbose ); - // verify if spec eq impl - pMiter = Gia_ManMiter( pAbc->pGia, pSpec, 0, 1, 0, 0, 0 ); - if ( !Cec_ManVerify( pMiter, pParsCec ) ) - { - Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec is not equivalent to current impl.\n" ); - success = 0; - } - Gia_ManStop(pMiter); - // check boundary - if ( success ) + if ( 0 == Bnd_ManCheckBound( pSpec, fVerbose ) ) { - if ( 0 == Bnd_ManCheckBound( pSpec, fVerbose ) ) - { - Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec has invalid boundary.\n" ); - success = 0; - } + Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec has invalid boundary.\n" ); + success = 0; } if ( success ) { // create bmiter, run fraig, record mapping - // pBmiter = Gia_ManBoundaryMiter( pSpec, pAbc->pGia, 0 ); pBmiter = Bnd_ManStackGias( pSpec, pAbc->pGia ); pTemp = Cec4_ManSimulateTest( pBmiter, pParsFra ); + + // every output should be equivalent + // else, terminate the command (TODO?) + if ( !Bnd_ManCheckCoMerged( pTemp ) ) + { + Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec and impl cannot be proved equivalent.\n" ); + success = 0; + } + Gia_ManStop(pBmiter); Gia_ManStop(pTemp); + } + if ( success ) + { // find Bnd_ManFindBound( pSpec, pAbc->pGia ); @@ -52223,22 +52227,30 @@ int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv ) // Gia_AigerWrite( pImpl_out, "impl_out.aig", 0, 0, 0 ); // Gia_ManPrintStats( pSpec_out, pPars ); // Gia_ManPrintStats( pImpl_out, pPars ); + + if ( !success ) + { + printf("Abc_CommandAbc9BRecover(): The generated boundary is invalid. The circuit is not changed.\n"); + } } - if ( !success ) - { - printf("Abc_CommandAbc9BRecover(): The generated boundary is invalid. The circuit is not changed.\n"); - } - else + if ( success ) { // check if spec_out and imnpl_out are equivalent if ( fVerbose ) { - printf("Checking the equivalence of spec_out and impl_out\n"); - pMiter = Gia_ManMiter( pSpec_out, pImpl_out, 0, 1, 0, 0, 0 ); - Bnd_ManSetEqOut( Cec_ManVerify( pMiter, pParsCec ) ); - Gia_ManStop( pMiter ); + if ( fEqOut ) + { + printf("Checking the equivalence of spec_out and impl_out\n"); + pMiter = Gia_ManMiter( pSpec_out, pImpl_out, 0, 1, 0, 0, 0 ); + Bnd_ManSetEqOut( Cec_ManVerify( pMiter, pParsCec ) ); + Gia_ManStop( pMiter ); + } + else + { + printf("Skip checking the equivalence of spec_out and impl_out\n"); + } } // generate patched impl @@ -52260,15 +52272,22 @@ int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv ) // Gia_ManStop( pTemp ); // check if patched is equiv to spec - if ( fVerbose ) printf("Checking the equivalence of patched impl and spec\n"); - pMiter = Gia_ManMiter( pSpec, pPatched, 0, 1, 0, 0, 0 ); - success = Cec_ManVerify( pMiter, pParsCec ); - Bnd_ManSetEqRes( success ); - if ( !success ) + if ( fVerbose ) { - printf("Failed. The generated AIG is not equivalent.\n"); + if ( fEq ) printf("Checking the equivalence of patched impl and spec\n"); + else printf("Skip checking the equivalence of patched impl and spec\n"); + } + if ( fEq ) + { + pMiter = Gia_ManMiter( pSpec, pPatched, 0, 1, 0, 0, 0 ); + success = Cec_ManVerify( pMiter, pParsCec ); + Bnd_ManSetEqRes( success ); + if ( !success ) + { + printf("Failed. The generated AIG is not equivalent.\n"); + } + Gia_ManStop( pMiter ); } - Gia_ManStop( pMiter ); } @@ -52279,7 +52298,8 @@ int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pImpl_out ) Gia_ManStop( pImpl_out ); if ( success ) { - printf("Success. The generated hierarchical impl is equivalent. (box size: %d -> %d)\n", Bnd_ManGetNInternal(), Bnd_ManGetNInternal() + Bnd_ManGetNExtra() ); + if ( fEq ) printf("Success. The generated hierarchical impl is equivalent. (box size: %d -> %d)\n", Bnd_ManGetNInternal(), Bnd_ManGetNInternal() + Bnd_ManGetNExtra() ); + else printf("Success. But the equivalence in unknown (box size: %d -> %d)\n", Bnd_ManGetNInternal(), Bnd_ManGetNInternal() + Bnd_ManGetNExtra() ); } if (pPatched) Abc_FrameUpdateGia( pAbc, pPatched ); Bnd_ManStop(); @@ -52291,6 +52311,10 @@ usage: Abc_Print( -2, "\t recover boundary using SAT-Sweeping\n" ); Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t-k : toggle using logic cones in the SAT solver [default = %s]\n", pParsFra->fUseCones? "yes": "no" ); + Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pParsFra->nBTLimit ); + Abc_Print( -2, "\t-e : toggle checking the equivalence of the result [default = %s]\n", fEq? "yes": "no" ); + Abc_Print( -2, "\t-o : toggle checking the equivalence of the outsides in verbose [default = %s]\n", fEqOut? "yes": "no" ); Abc_Print( -2, "\t : the implementation aig. (should be equivalent to spec)\n"); Abc_Print( -2, "\t : the modified spec. (should be a hierarchical AIG)\n"); return 1;