luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

clean up & add options for &brecover

This commit is contained in:
Allen Ho 2024-03-16 01:40:11 +08:00
parent 015dd2a367
commit b7884aaf2b
3 changed files with 161 additions and 94 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

2
src/aig/gia/gia.h
View File

@ -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 );

155
src/aig/gia/giaBound.c
View File

@ -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 ///

98
src/base/abci/abc.c
View File

@ -52081,6 +52081,7 @@ usage:
Abc_Print( -2, "\t (the PO count of <file[i]> should not be less than the PI count of <file[i+1]>)\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<impl> : the implementation aig. (should be equivalent to spec)\n");
Abc_Print( -2, "\t<patch> : the modified spec. (should be a hierarchical AIG)\n");
return 1;