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

&stc_eco and &brecover done

This commit is contained in:
Allen Ho 2024-03-04 09:36:35 +08:00
parent bcf04fadb6
commit bfbec71211
3 changed files with 216 additions and 163 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -1793,21 +1793,26 @@ extern int Tas_ManSolveArray( Tas_Man_t * p, Vec_Ptr_t * vObjs )
/*=== giaBound.c ===========================================================*/
typedef struct Bnd_Man_t_ Bnd_Man_t;
extern Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl );
extern Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl, int fVerbose );
extern void Bnd_ManStop();
// getter
extern int Bnd_ManGetNInternal();
extern int Bnd_ManGetNExtra();
//for fraig
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();
// for eco
extern int Bnd_ManCheckBound( Gia_Man_t *p );
extern int Bnd_ManCheckBound( Gia_Man_t *p, int fVerbose );
extern void Bnd_ManFindBound( Gia_Man_t *p );
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 );
extern Gia_Man_t* Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec );
extern Gia_Man_t* Bnd_ManGenPatched2( Gia_Man_t *p, Gia_Man_t *pPatch );
extern Gia_Man_t* Bnd_ManGenPatched2( Gia_Man_t *pImpl, Gia_Man_t *pPatch, int fSkiptStrash, int fVerbose );
extern void Bnd_ManSetEqOut( int eq );
extern void Bnd_ManSetEqRes( int eq );
extern void Bnd_ManPrintStats();

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

@ -29,6 +29,7 @@ struct Bnd_Man_t_
int nNode_patched;
int status; // 0: init 1: boundary found 2: out generated 3: patched generated
int fVerbose;
int combLoop_spec;
int combLoop_impl;
@ -57,7 +58,7 @@ struct Bnd_Man_t_
};
Bnd_Man_t* pBnd;
Bnd_Man_t* pBnd = 0;
////////////////////////////////////////////////////////////////////////
/// FUNCTION DEFINITIONS ///
@ -78,7 +79,7 @@ void Bnd_ManSetEqRes( int eq ) { pBnd -> eq_res = eq;}
***********************************************************************/
Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl )
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 );
@ -113,6 +114,8 @@ Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl )
p -> nNode_patched = 0;
p -> status = 0;
p -> fVerbose = fVerbose;
p -> combLoop_spec = 0;
p -> combLoop_impl = 0;
p -> eq_out = 0;
@ -166,6 +169,8 @@ void Bnd_ManStop()
ABC_FREE( pBnd );
}
int Bnd_ManGetNInternal() { assert(pBnd); return pBnd -> nInternal; }
int Bnd_ManGetNExtra() { assert(pBnd); return pBnd -> nExtra; }
void Bnd_ManMap( int iLit, int id, int spec )
{
@ -370,23 +375,22 @@ void Bnd_ManPrintStats()
Description [check if the given boundary is valid. Return 0 if
the boundary is invalid. Return k if the boundary is valid and
there're k boundary inputs. ]
there're k boundary inputs.
Can be called even if Bnd_Man_t is not created]
SideEffects []
SeeAlso []
***********************************************************************/
int Bnd_ManCheckBound( Gia_Man_t * p )
int Bnd_ManCheckBound( Gia_Man_t * p, int fVerbose )
{
int i;
Gia_Obj_t *pObj;
int valid = 1;
pBnd -> nBI = 0;
pBnd -> nBO = 0;
pBnd -> nInternal = 0;
int nBI = 0, nBO = 0, nInternal = 0;
printf( "Checking boundary... \n");
if ( fVerbose ) printf( "Checking boundary... \n");
Vec_Int_t *vPath;
vPath = Vec_IntAlloc( Gia_ManObjNum(p) );
@ -417,7 +421,7 @@ int Bnd_ManCheckBound( Gia_Man_t * p )
if ( path == 1 ) // boundary input
{
// TODO: record BIs here since they may not be in the first n buffers
pBnd -> nBO ++;
nBO ++;
}
}
else if ( Gia_ObjFaninNum( p, pObj ) >= 1 )
@ -431,7 +435,7 @@ int Bnd_ManCheckBound( Gia_Man_t * p )
if ( path == 2 ) // inside boundary
{
// TODO: record BIs here since they may not be in the first n buffers
pBnd -> nInternal ++;
nInternal ++;
}
}
else // PI or const, check validity
@ -445,20 +449,33 @@ int Bnd_ManCheckBound( Gia_Man_t * p )
}
}
pBnd -> nBI = Gia_ManBufNum(p) - pBnd -> nBO;
nBI = Gia_ManBufNum(p) - nBO;
if ( !valid )
{
printf("invalid boundary\n");
return 0;
}
else if ( nBI == 0 )
{
printf("no boundary\n");
return 0;
}
else
{
printf("valid boundary (");
printf("#BI = %d\t#BO = %d\t", pBnd -> nBI, Gia_ManBufNum(p)- pBnd -> nBI);
printf("#Internal = %d)\n", pBnd -> nInternal );
assert( pBnd -> nBI > 0 );
return pBnd -> nBI;
if ( fVerbose )
{
printf("valid boundary (");
printf("#BI = %d\t#BO = %d\t", nBI, Gia_ManBufNum(p)- nBI);
printf("#Internal = %d)\n", nInternal );
}
if ( pBnd )
{
pBnd -> nBI = nBI;
pBnd -> nBO = nBO;
pBnd -> nInternal = nInternal;
}
return nBI;
}
}
@ -593,7 +610,7 @@ void Bnd_ManFindBound( Gia_Man_t * p )
Vec_IntPush(vEO_spec, id);
}
}
printf("%d BO doesn't match. ", Vec_PtrSize(vQ) );
if ( pBnd -> fVerbose ) printf("%d BO doesn't match. ", Vec_PtrSize(vQ) );
pBnd -> nBO_miss = Vec_PtrSize(vQ);
int cnt_extra = - Vec_PtrSize(vQ);
@ -622,7 +639,7 @@ void Bnd_ManFindBound( Gia_Man_t * p )
}
}
// printf("%d AO found with %d extra nodes\n", Vec_IntSize(vAO) , cnt_extra );
printf("%d AO found\n", Vec_IntSize(vAO) );
if ( pBnd -> fVerbose ) printf("%d AO found\n", Vec_IntSize(vAO) );
// mark TFOC of BO with flag 1 to prevent them from being selected into EI
@ -665,7 +682,7 @@ void Bnd_ManFindBound( Gia_Man_t * p )
Vec_IntPush(vEI_spec, id);
}
}
printf("%d BI doesn't match. ", Vec_PtrSize(vQ) );
if ( pBnd -> fVerbose ) printf("%d BI doesn't match. ", Vec_PtrSize(vQ) );
pBnd -> nBI_miss = Vec_PtrSize(vQ);
cnt_extra -= Vec_PtrSize(vQ);
@ -708,7 +725,7 @@ void Bnd_ManFindBound( Gia_Man_t * p )
Vec_IntSetEntry( vFlag, id, 2 );
}
printf("%d AI found with %d extra nodes in total\n", Vec_IntSize(vAI) , cnt_extra );
if ( pBnd -> fVerbose ) printf("%d AI found with %d extra nodes in total\n", Vec_IntSize(vAI) , cnt_extra );
pBnd -> nExtra = cnt_extra;
@ -738,8 +755,11 @@ void Bnd_ManFindBound( Gia_Man_t * p )
// print
pBnd -> status = 1;
printf("#EI = %d\t#EO = %d\t#Extra Node = %d\n", Vec_IntSize(vEI_spec) , Vec_IntSize(vEO_spec), cnt_extra );
Bnd_ManPrintBound();
if ( pBnd -> fVerbose )
{
printf("#EI = %d\t#EO = %d\t#Extra Node = %d\n", Vec_IntSize(vEI_spec) , Vec_IntSize(vEO_spec), cnt_extra );
Bnd_ManPrintBound();
}
// check boundary has comb loop
if ( !Bnd_ManCheckExtBound( p, vEI_spec, vEO_spec ) )
@ -869,15 +889,15 @@ Gia_Man_t* Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec
}
Gia_Man_t* Bnd_ManGenSpecOut( Gia_Man_t* p )
Gia_Man_t* Bnd_ManGenSpecOut( Gia_Man_t* p )
{
printf("Generating spec_out with given boundary.\n");
if ( pBnd -> fVerbose ) printf("Generating spec_out with given boundary.\n");
Gia_Man_t *pNew = Bnd_ManCutBoundary( p, pBnd->vEI_spec, pBnd->vEO_spec, 0, 0 );
return pNew;
}
Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t* p )
Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t* p)
{
printf("Generating impl_out with given boundary.\n");
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;
@ -1066,7 +1086,7 @@ Gia_Man_t* Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec )
}
// add Impl EI to CI
printf("adding EI to CI in Impl\n");
// printf("adding EI to CI in Impl\n");
for ( i = 0; i < Vec_IntSize( pBnd -> vEI_spec ); i++ )
{
pObj = Gia_ManCo(pOut, i + Gia_ManCoNum(pSpec) );
@ -1074,20 +1094,24 @@ Gia_Man_t* Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec )
// set Spec EI
Gia_ManObj( pSpec, Vec_IntEntry(pBnd -> vEI_spec, i) ) -> Value = pObj -> Value;
printf(" %d",pObj -> Value);
// printf(" %d",pObj -> Value);
}
printf("\n");
// printf("\n");
// add Spec EO to EI
// add BI -> BO -> EO to maintain the order of bufs
Vec_IntForEachEntry( pBnd -> vBI, id, i )
// Vec_IntForEachEntry( pBnd -> vBI, id, i )
// {
// pObj = Gia_ManObj( pSpec, id );
// Bnd_AddNodeRec( pSpec, pNew, pObj, 1 );
// }
// Vec_IntForEachEntry( pBnd -> vBO, id, i )
// {
// pObj = Gia_ManObj( pSpec, id );
// Bnd_AddNodeRec( pSpec, pNew, pObj, 1 );
// }
Gia_ManForEachBuf( pSpec, pObj, i )
{
pObj = Gia_ManObj( pSpec, id );
Bnd_AddNodeRec( pSpec, pNew, pObj, 1 );
}
Vec_IntForEachEntry( pBnd -> vBO, id, i )
{
pObj = Gia_ManObj( pSpec, id );
Bnd_AddNodeRec( pSpec, pNew, pObj, 1 );
}
Vec_IntForEachEntry( pBnd -> vEO_spec, id, i )
@ -1123,6 +1147,100 @@ Gia_Man_t* Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec )
return pNew;
}
Gia_Man_t* Bnd_ManGenPatched2( Gia_Man_t *pImpl, Gia_Man_t *pPatch, int fSkipStrash, int fVerbose )
{
Gia_Man_t * pNew, * pTemp;
Gia_Obj_t * pObj;
int i, nBI, nBI_patch, cnt;
Vec_Int_t* vLit;
// check boundary first
nBI = Bnd_ManCheckBound( pImpl, fVerbose );
nBI_patch = Bnd_ManCheckBound( pPatch, fVerbose );
if ( 0 == nBI_patch || Gia_ManBufNum(pImpl) != Gia_ManBufNum(pPatch) || nBI != nBI_patch )
{
Abc_Print( -1, "Abc_CommandAbc9StrEco(): The given boundary is invalid.\n" );
return 0;
}
// prepare new network
pNew = Gia_ManStart( Gia_ManObjNum(pImpl) + Gia_ManObjNum( pPatch ) );
pNew -> pName = ABC_ALLOC( char, strlen(pImpl->pName)+3);
sprintf( pNew -> pName, "%s_p", pImpl -> pName );
if ( !fSkipStrash )
{
Gia_ManHashAlloc( pNew );
}
Gia_ManFillValue(pImpl);
Gia_ManFillValue(pPatch);
Gia_ManConst0(pImpl)->Value = 0;
Gia_ManConst0(pPatch)->Value = 0;
vLit = Vec_IntAlloc( Gia_ManBufNum(pImpl) );
// add Impl (real) CI
Gia_ManForEachCi( pImpl, pObj, i )
{
pObj -> Value = Gia_ManAppendCi( pNew );
}
// add Impl BI to CI
cnt = 0;
Gia_ManForEachBuf( pImpl, pObj, i )
{
Bnd_AddNodeRec( pImpl, pNew, pObj, fSkipStrash );
Vec_IntPush( vLit, pObj -> Value );
cnt ++;
if ( cnt >= nBI ) break;
}
// set BI in patch
// add patch BO to BI
cnt = 0;
Gia_ManForEachBuf( pPatch, pObj, i )
{
if ( cnt < nBI )
{
pObj -> Value = Vec_IntEntry( vLit, cnt );
}
else
{
Bnd_AddNodeRec( pPatch, pNew, pObj, fSkipStrash );
Vec_IntPush( vLit, pObj -> Value );
}
cnt ++;
if ( cnt == nBI ) Vec_IntClear( vLit );
}
// set BO in impl
cnt = 0;
Gia_ManForEachBuf( pImpl, pObj, i )
{
cnt ++;
if ( cnt <= nBI) continue;
pObj -> Value = Vec_IntEntry( vLit, cnt-nBI-1 );
}
// add impl CO to BO
Gia_ManForEachCo( pImpl, pObj, i )
{
Bnd_AddNodeRec( pImpl, pNew, pObj, fSkipStrash );
Gia_ManAppendCo( pNew, pObj -> Value );
}
// clean up
if ( !fSkipStrash )
{
Gia_ManHashStop( pNew );
}
Vec_IntFree( vLit );
pNew = Gia_ManCleanup( pTemp = pNew );
Gia_ManStop( pTemp );
return pNew;
}
////////////////////////////////////////////////////////////////////////

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

@ -52099,7 +52099,7 @@ 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 );
extern void Cec4_ManSetParams( Cec_ParFra_t * pPars );
extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose );
Gia_Man_t *pSpec, *pImpl_out = 0, *pSpec_out = 0, *pMiter, *pPatched, *pTemp, *pBmiter;
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;
@ -52165,7 +52165,7 @@ int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv )
}
// start boundary manager
pBnd = Bnd_ManStart( pSpec, pAbc->pGia );
pBnd = Bnd_ManStart( pSpec, pAbc->pGia, fVerbose );
// verify if spec eq impl
pMiter = Gia_ManMiter( pAbc->pGia, pSpec, 0, 1, 0, 0, 0 );
@ -52179,7 +52179,7 @@ int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv )
// check boundary
if ( success )
{
if ( 0 == Bnd_ManCheckBound( pSpec ) )
if ( 0 == Bnd_ManCheckBound( pSpec, fVerbose ) )
{
Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec has invalid boundary.\n" );
success = 0;
@ -52209,17 +52209,24 @@ int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv )
// Gia_ManPrintStats( pImpl_out, pPars );
}
if ( success )
if ( !success )
{
printf("Abc_CommandAbc9BRecover(): The generated boundary is invalid. The circuit is not changed.\n");
}
else
{
// check if spec_out and imnpl_out are equivalent
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 ( 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 );
}
// generate patched impl
printf("Generating patched impl\n");
if ( fVerbose ) printf("Generating patched impl\n");
pPatched = Bnd_ManGenPatched1( pImpl_out, pSpec );
// // generate patched spec just for debugging
@ -52237,29 +52244,35 @@ int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv )
// Gia_ManStop( pTemp );
// check if patched is equiv to spec
printf("Checking the equivalence of patched impl and patch\n");
if ( fVerbose ) printf("Checking the equivalence of patched impl and spec\n");
pMiter = Gia_ManMiter( pSpec, pPatched, 0, 1, 0, 0, 0 );
Bnd_ManSetEqRes( Cec_ManVerify( pMiter, pParsCec ) );
success = Cec_ManVerify( pMiter, pParsCec );
Bnd_ManSetEqRes( success );
if ( !success )
{
printf("Failed. The generated AIG is not equivalent.\n");
}
Gia_ManStop( pMiter );
}
Bnd_ManPrintStats();
if ( fVerbose ) Bnd_ManPrintStats();
Gia_ManStop( pSpec );
if ( pSpec_out ) Gia_ManStop( pSpec_out );
if ( pImpl_out ) Gia_ManStop( pImpl_out );
if ( success )
{
Abc_FrameUpdateGia( pAbc, pPatched );
printf("Success. The generated hierarchical impl is equivalent. (box size: %d -> %d)\n", Bnd_ManGetNInternal(), Bnd_ManGetNInternal() + Bnd_ManGetNExtra() );
}
if (pPatched) Abc_FrameUpdateGia( pAbc, pPatched );
Bnd_ManStop();
return 0;
usage:
Abc_Print( -2, "usage: &str_eco -I <biNum> [-vh] <impl> <patch>\n" );
Abc_Print( -2, "\t SAT-sweeping-based ECO\n" );
Abc_Print( -2, "usage: &brecover -I <biNum> [-vh] <impl> <patch>\n" );
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<impl> : the implementation aig. (should be equivalent to spec)\n");
@ -52283,11 +52296,11 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars );
extern void Cec4_ManSetParams( Cec_ParFra_t * pPars );
extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose );
Gia_Man_t *pImpl, *pImpl_out = 0, *pSpec_out = 0, *pMiter, *pPatch, *pPatched, *pTemp, *pBmiter;;
Gia_Man_t *pMiter, *pPatch, *pPatched;
char * FileName = NULL;
FILE * pFile = NULL;
int c, fVerbose = 0, success = 1;
int c, success = 1;
int fVerbose = 0, fSkipStrash = 0;
// params
Gps_Par_t Pars, * pPars = &Pars;
@ -52300,13 +52313,16 @@ int Abc_CommandAbc9StrEco( 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, "vsh" ) ) != EOF )
{
switch ( c )
{
case 'v':
fVerbose ^= 1;
break;
case 's':
fSkipStrash ^= 1;
break;
case 'h':
goto usage;
default:
@ -52318,33 +52334,15 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Abc_CommandAbc9StrEco(): There is no AIG.\n" );
return 0;
}
if ( argc != globalUtilOptind + 2 )
if ( argc != globalUtilOptind + 1 )
{
printf("%d\n", argc-globalUtilOptind);
Abc_Print( -1, "Abc_CommandAbc9StrEco(): AIG should be given on the command line.\n" );
return 0;
}
// read impl
FileName = argv[globalUtilOptind];
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", ".blif", ".pla", ".eqn", ".bench" )) )
Abc_Print( 1, "Did you mean \"%s\"?", FileName );
Abc_Print( 1, "\n" );
return 1;
}
fclose( pFile );
pImpl = Gia_AigerRead( FileName, 0, 0, 0 );
if ( pImpl == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9StrEco(): Cannot read the file name on the command line.\n" );
return 0;
}
// read patch
FileName = argv[globalUtilOptind+1];
FileName = argv[globalUtilOptind];
if ( (pFile = fopen( FileName, "r" )) == NULL )
{
Abc_Print( -1, "Cannot open input file \"%s\". ", FileName );
@ -52361,98 +52359,29 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
}
// start boundary manager
pBnd = Bnd_ManStart( pAbc->pGia, pImpl );
// generate patched impl
if ( fVerbose ) printf("Generating patched impl\n");
pPatched = Bnd_ManGenPatched2( pAbc->pGia, pPatch, fSkipStrash, fVerbose );
// verify if spec eq impl
pMiter = Gia_ManMiter( pAbc->pGia, pImpl, 0, 1, 0, 0, 0 );
if ( !Cec_ManVerify( pMiter, pParsCec ) )
if ( pPatched )
{
Abc_Print( -1, "Abc_CommandAbc9StrEco(): The given impl is not equivalent to spec.\n" );
success = 0;
}
Gia_ManStop(pMiter);
// check boundary
if ( success )
{
if ( 0 == Bnd_ManCheckBound( pPatch ) || 0 == Bnd_ManCheckBound( pAbc -> pGia ) )
{
Abc_Print( -1, "Abc_CommandAbc9StrEco(): The given boundary is invalid.\n" );
success = 0;
}
}
if ( success )
{
// create bmiter, run fraig
pBmiter = Gia_ManBoundaryMiter( pAbc -> pGia, pImpl, 0 );
pTemp = Cec4_ManSimulateTest( pBmiter, pParsFra );
Gia_ManStop(pBmiter);
Gia_ManStop(pTemp);
// find
Bnd_ManFindBound( pAbc -> pGia );
// create spec_out and
pSpec_out = Bnd_ManGenSpecOut( pAbc -> pGia );
if ( !pSpec_out ) success = 0;
pImpl_out = Bnd_ManGenImplOut( pImpl );
if ( !pImpl_out ) success = 0;
// Gia_AigerWrite( pSpec_out, "spec_out.aig", 0, 0, 0 );
// Gia_AigerWrite( pImpl_out, "impl_out.aig", 0, 0, 0 );
// Gia_ManPrintStats( pSpec_out, pPars );
// Gia_ManPrintStats( pImpl_out, pPars );
}
if ( success )
{
// check if spec_out and imnpl_out are equivalent
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 );
// generate patched impl
printf("Generating patched impl\n");
pPatched = Bnd_ManGenPatched( pImpl_out, pAbc->pGia, pPatch );
// generate patched spec just for debugging
printf("Generating patched spec\n");
pTemp = Bnd_ManGenPatched( pSpec_out, pAbc->pGia, pPatch );
printf("Checking the equivalence of patched spec and patched impl\n");
pMiter = Gia_ManMiter( pTemp, pPatched, 0, 1, 0, 0, 0 );
Cec_ManVerify( pMiter, pParsCec );
Gia_ManStop( pMiter );
printf("Checking the equivalence of patched spec and patch\n");
pMiter = Gia_ManMiter( pTemp, pPatch, 0, 1, 0, 0, 0 );
Cec_ManVerify( pMiter, pParsCec );
Gia_ManStop( pMiter );
Gia_ManStop( pTemp );
// check if patched is equiv to patch
printf("Checking the equivalence of patched impl and patch\n");
if ( fVerbose ) printf("Checking the equivalence of patched impl and patch\n");
pMiter = Gia_ManMiter( pPatch, pPatched, 0, 1, 0, 0, 0 );
Bnd_ManSetEqRes( Cec_ManVerify( pMiter, pParsCec ) );
success = Cec_ManVerify( pMiter, pParsCec );
if( !success )
{
printf("Failed. The patched circuit is not equivalent.\n");
}
Gia_ManStop( pMiter );
}
Bnd_ManPrintStats();
Gia_ManStop( pImpl );
Gia_ManStop( pPatch );
if ( pSpec_out ) Gia_ManStop( pSpec_out );
if ( pImpl_out ) Gia_ManStop( pImpl_out );
if ( success )
{
Abc_FrameUpdateGia( pAbc, pPatched );
}
Bnd_ManStop();
Gia_ManStop( pPatch );
if ( success )
{
printf("Success. The patched circuit is equivalent.\n");
}
return 0;
@ -52460,6 +52389,7 @@ usage:
Abc_Print( -2, "usage: &str_eco -I <biNum> [-vh] <impl> <patch>\n" );
Abc_Print( -2, "\t SAT-sweeping-based ECO\n" );
Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-s : toggles skipping structural hash [default = %s]\n", fSkipStrash? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
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");