From bcf04fadb6f50755b7844cc36fe19e57eca47fd7 Mon Sep 17 00:00:00 2001 From: Allen Ho Date: Mon, 4 Mar 2024 00:54:23 +0800 Subject: [PATCH] &brecover done --- src/aig/gia/gia.h | 2 + src/aig/gia/giaBound.c | 111 +++++++++++++++++++++--- src/base/abci/abc.c | 189 ++++++++++++++++++++++++++++++++++++++++- 3 files changed, 287 insertions(+), 15 deletions(-) diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index e0654afda..5e8f5f36d 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1806,6 +1806,8 @@ 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 void Bnd_ManSetEqOut( int eq ); extern void Bnd_ManSetEqRes( int eq ); extern void Bnd_ManPrintStats(); diff --git a/src/aig/gia/giaBound.c b/src/aig/gia/giaBound.c index 916ed8e1f..a3a298e35 100644 --- a/src/aig/gia/giaBound.c +++ b/src/aig/gia/giaBound.c @@ -572,7 +572,7 @@ void Bnd_ManFindBound( Gia_Man_t * p ) { if ( cnt < pBnd -> nBI ) { - Vec_IntPush( vBI, Gia_ObjId(p, pObj) ); + Vec_IntPush( vBI, Gia_ObjId(p, Gia_ObjFanin0(pObj) ) ); } else { @@ -884,27 +884,32 @@ Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t* p ) return pNew; } -void Bnd_AddNodeRec( Gia_Man_t *p, Gia_Man_t *pNew, Gia_Obj_t *pObj ) +void Bnd_AddNodeRec( Gia_Man_t *p, Gia_Man_t *pNew, Gia_Obj_t *pObj, int fSkipStrash ) { // TODO does this mean constant zero node? if ( pObj -> Value != ~0 ) return; for( int i = 0; i < Gia_ObjFaninNum(p, pObj); i++ ) { - Bnd_AddNodeRec( p, pNew, Gia_ObjFanin(pObj, i) ); + Bnd_AddNodeRec( p, pNew, Gia_ObjFanin(pObj, i), fSkipStrash ); } if ( Gia_ObjIsAnd(pObj) ) { - pObj -> Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( fSkipStrash ) + { + if ( Gia_ObjIsBuf(pObj) ) pObj -> Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) ); + else pObj -> Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } + else + { + pObj -> Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } } else { - if ( Gia_ObjIsCi(pObj) ) - { - printf("Ci with value 0 encountered (id = %d)\n", Gia_ObjId(p, pObj) ); - } assert( Gia_ObjIsCo(pObj) ); + // if ( Gia_ObjIsCi(pObj) ) printf("Ci with value ~0 encountered (id = %d)\n", Gia_ObjId(p, pObj) ); pObj -> Value = Gia_ObjFanin0Copy(pObj); } } @@ -963,7 +968,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat for ( i = 0; i < Vec_IntSize( pBnd -> vEI_spec ); i++ ) { pObj = Gia_ManCo(pOut, i + Gia_ManCoNum(pSpec) ); - Bnd_AddNodeRec( pOut, pNew, pObj ); + Bnd_AddNodeRec( pOut, pNew, pObj, 0 ); // set Spec EI Gia_ManObj( pSpec, Vec_IntEntry(pBnd -> vEI_spec, i) ) -> Value = pObj -> Value; @@ -976,7 +981,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat Vec_IntForEachEntry( pBnd -> vBI, id, i ) { pObj = Gia_ManObj( pSpec, id ); - Bnd_AddNodeRec( pSpec, pNew, pObj ); + Bnd_AddNodeRec( pSpec, pNew, pObj, 0 ); // set patch bi Gia_ManObj( pPatch, Vec_IntEntry( vBI_patch, i) ) -> Value = pObj -> Value; @@ -989,7 +994,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat Vec_IntForEachEntry( vBO_patch, id, i ) { pObj = Gia_ManObj( pPatch, id ); - Bnd_AddNodeRec( pPatch, pNew, pObj ); + Bnd_AddNodeRec( pPatch, pNew, pObj, 0 ); // set spec bo Gia_ManObj( pSpec, Vec_IntEntry( pBnd -> vBO, i) ) -> Value = pObj -> Value; @@ -1002,7 +1007,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat Vec_IntForEachEntry( pBnd -> vEO_spec, id, i ) { pObj = Gia_ManObj( pSpec, id ); - Bnd_AddNodeRec( pSpec, pNew, pObj ); + Bnd_AddNodeRec( pSpec, pNew, pObj, 0 ); // set impl EO (PI) Gia_ManCi( pOut, i + Gia_ManCiNum(pSpec) ) -> Value = pObj -> Value; @@ -1015,7 +1020,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat for ( i = 0; i < Gia_ManCoNum(pSpec); i++ ) { pObj = Gia_ManCo( pOut, i ); - Bnd_AddNodeRec( pOut, pNew, pObj ); + Bnd_AddNodeRec( pOut, pNew, pObj, 0 ); Gia_ManAppendCo( pNew, pObj->Value ); // printf(" %d",pObj -> Value); } @@ -1036,7 +1041,87 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat return pNew; } +Gia_Man_t* Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, id; + + pNew = Gia_ManStart( Gia_ManObjNum(pOut) + Gia_ManObjNum( pSpec ) ); + pNew -> pName = ABC_ALLOC( char, strlen(pOut->pName)+3); + sprintf( pNew -> pName, "%s_p", pOut -> pName ); + + Gia_ManFillValue(pOut); + Gia_ManFillValue(pSpec); + Gia_ManConst0(pOut)->Value = 0; + Gia_ManConst0(pSpec)->Value = 0; + + + // add Impl (real) PI + for ( i = 0; i < Gia_ManCiNum(pSpec); i++ ) + { + pObj = Gia_ManCi(pOut, i); + pObj -> Value = Gia_ManAppendCi( pNew ); + } + + // add Impl EI to CI + 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) ); + Bnd_AddNodeRec( pOut, pNew, pObj, 1 ); + + // set Spec EI + Gia_ManObj( pSpec, Vec_IntEntry(pBnd -> vEI_spec, i) ) -> Value = pObj -> Value; + printf(" %d",pObj -> Value); + } + printf("\n"); + + // add Spec EO to EI + // add BI -> BO -> EO to maintain the order of bufs + 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 ); + } + Vec_IntForEachEntry( pBnd -> vEO_spec, id, i ) + { + pObj = Gia_ManObj( pSpec, id ); + Bnd_AddNodeRec( pSpec, pNew, pObj, 1 ); + + // set impl EO (PI) + Gia_ManCi( pOut, i + Gia_ManCiNum(pSpec) ) -> Value = pObj -> Value; + // printf(" %d",pObj -> Value); + } + // printf("\n"); + + // add Impl (real) PO to EO + // printf("adding CO to EO in Impl\n"); + for ( i = 0; i < Gia_ManCoNum(pSpec); i++ ) + { + pObj = Gia_ManCo( pOut, i ); + Bnd_AddNodeRec( pOut, pNew, pObj, 1 ); + Gia_ManAppendCo( pNew, pObj->Value ); + // printf(" %d",pObj -> Value); + } + // printf("\n"); + + + // clean up + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + + pBnd -> nNode_patched = Gia_ManAndNum( pNew ); + pBnd -> status = 3; + + return pNew; +} diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 9a558c2da..60aa58c08 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -599,6 +599,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_CommandAbc9BRecover ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9StrEco ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1381,6 +1382,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", "&brecover", Abc_CommandAbc9BRecover, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&str_eco", Abc_CommandAbc9StrEco, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); @@ -52092,6 +52094,191 @@ usage: ***********************************************************************/ 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 ); + 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; + char * FileName = NULL; + FILE * pFile = NULL; + int c, fVerbose = 0, success = 1; + + // params + Gps_Par_t Pars, * pPars = &Pars; + memset( pPars, 0, sizeof(Gps_Par_t) ); + Cec_ParCec_t ParsCec, *pParsCec = &ParsCec; + Cec_ManCecSetDefaultParams( pParsCec ); + Cec_ParFra_t ParsFra, *pParsFra = &ParsFra; + Cec4_ManSetParams( pParsFra ); + pParsFra -> fBMiterInfo = 1; + + // parse options + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9BRecover(): There is no AIG.\n" ); + return 0; + } + if ( argc != globalUtilOptind + 1 ) + { + printf("%d\n", argc-globalUtilOptind); + Abc_Print( -1, "Abc_CommandAbc9BRecover(): AIG should be given on the command line.\n" ); + return 0; + } + + // read spec + 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 ); + pSpec = Gia_AigerRead( FileName, 0, 1, 0 ); + if ( pSpec == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9BRecover(): Cannot read the file name on the command line.\n" ); + return 0; + } + if ( Gia_ManBufNum(pSpec) == 0 ) + { + Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec should be hierarchical.\n" ); + Gia_ManStop(pSpec); + return 0; + } + + // start boundary manager + pBnd = Bnd_ManStart( pSpec, pAbc->pGia ); + + // 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 ) ) + { + 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 ); + pTemp = Cec4_ManSimulateTest( pBmiter, pParsFra ); + Gia_ManStop(pBmiter); + Gia_ManStop(pTemp); + + // find + Bnd_ManFindBound( pSpec ); + + // create spec_out and + pSpec_out = Bnd_ManGenSpecOut( pSpec ); + if ( !pSpec_out ) success = 0; + pImpl_out = Bnd_ManGenImplOut( pAbc->pGia ); + 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_ManGenPatched1( pImpl_out, pSpec ); + + // // 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 spec + printf("Checking the equivalence of patched impl and patch\n"); + pMiter = Gia_ManMiter( pSpec, pPatched, 0, 1, 0, 0, 0 ); + Bnd_ManSetEqRes( Cec_ManVerify( pMiter, pParsCec ) ); + Gia_ManStop( pMiter ); + + } + + 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 ); + } + Bnd_ManStop(); + + return 0; + +usage: + Abc_Print( -2, "usage: &str_eco -I [-vh] \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-h : print the command usage\n"); + 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; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + 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 ); @@ -52111,8 +52298,6 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) Cec4_ManSetParams( pParsFra ); pParsFra -> fBMiterInfo = 1; - // TODO: save return value and return at the end of the function - // parse options Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )