From 31ad17fa1acdc90378bb633a02841f23bd5b5364 Mon Sep 17 00:00:00 2001 From: Allen Ho Date: Wed, 20 Sep 2023 14:23:47 +0800 Subject: [PATCH 01/11] add abc9RecoverBoundary --- src/aig/gia/giaDup.c | 133 +++++++++++++++++++++++++++++++++++++++++++ src/base/abci/abc.c | 129 +++++++++++++++++++++++++++++++++++++++++ 2 files changed, 262 insertions(+) diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index db4072d71..665164eb2 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -5719,6 +5719,139 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ) return pNew; } +/**Function************************************************************* + Synopsis [Duplicates AIG while putting objects in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManImplFromBMiter( Gia_Man_t * p, int nPo, int nBInput ) +{ + Gia_Man_t * pNew, *pTemp; + Gia_Obj_t * pObj, *pObj2; + int i; + int nBoundI = 0, nBoundO = 0; + int nExtra; + Gia_ManFillValue( p ); + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + // pNew->pName = Abc_UtilStrsav( p->pName ); + // pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + + // add po of impl + Gia_ManForEachCo( p, pObj, i ) + { + if ( i < nPo ) + { + Gia_ManDupOrderDfs_rec( pNew, p, pObj ); + } + } + nExtra = Gia_ManAndNum( pNew ); + + // add boundary as buf + Gia_ManForEachCo( p, pObj, i ) + { + if ( i >= 2 * nPo ) + { + pObj2 = Gia_ObjFanin0(pObj); + if (~pObj2->Value) // visited boundary + { + if ( i >= 2 * nPo + nBInput ) + { + nBoundO ++; + } + else nBoundI ++; + } + + Gia_ManDupOrderDfs_rec( pNew, p, pObj2 ); + Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) ); + } + } + nExtra = Gia_ManAndNum( pNew ) - nExtra - Gia_ManBufNum( pNew ); + + Gia_ManForEachCi( p, pObj, i ) + if ( !~pObj->Value ) + pObj->Value = Gia_ManAppendCi(pNew); + assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) ); + + Gia_ManDupRemapCis( pNew, p ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + + + printf( "synthesized implementation:\n" ); + printf( "\t%d / %d input boundary recovered.\n", nBoundI, nBInput ); + printf( "\t%d / %d output boundary recovered.\n", nBoundO, Gia_ManCoNum(p)-2*nPo-nBInput ); + printf( "\t%d / %d unused nodes in the box.\n", nExtra, Gia_ManAndNum(pNew) - Gia_ManBufNum( pNew ) ); + + return pNew; +} + +/**Function************************************************************* + + Synopsis [Duplicates AIG while putting objects in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManMiterFromBMiter( Gia_Man_t * p, int nPo ) +{ + Gia_Man_t * pNew, *pTemp; + Gia_Obj_t * pObj, *pObj2; + int i, iXor, iPo, i1, i2; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( "miter" ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + + // create primary inputs + Gia_ManForEachCi( p, pObj, i ) + if ( !~pObj->Value ) + pObj->Value = Gia_ManAppendCi(pNew); + + Gia_ManForEachCo( p, pObj, i ) + { + if ( i == nPo ) + { + break; + } + else + { + pObj2 = Gia_ManCo( p, i + nPo ); + + i1 = Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(pObj) ); + i2 = Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(pObj2) ); + + iXor = Gia_ManAppendXor2( pNew, Gia_ObjFaninC0(pObj) ? i1+1 : i1 , Gia_ObjFaninC0(pObj2 ) ? i2+1 : i2 ); + if ( i > 0 ) + { + iPo = Gia_ManAppendOr2( pNew, iPo, iXor ); + } + else + { + iPo = iXor; + } + } + } + Gia_ManAppendCo( pNew, iPo ); + + + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + pNew = Gia_ManDupNormalize( pTemp = pNew, 0 ); + Gia_ManStop( pTemp ); + + return pNew; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 5bc50032c..906b456ad 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -597,6 +597,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_CommandAbc9RecoverBoundary ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1376,6 +1377,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", "&rb", Abc_CommandAbc9RecoverBoundary, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); { @@ -51809,6 +51811,133 @@ usage: Abc_Print( -2, "\t (the PO count of should not be less than the PI count of )\n"); return 1;} +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9RecoverBoundary( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_ManDeepSyn( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fVerbose ); + extern Gia_Man_t * Gia_ManImplFromBMiter( Gia_Man_t * p, int nPo, int nBInput ); + extern Gia_Man_t * Gia_ManMiterFromBMiter( Gia_Man_t * p, int nPo ); + int c, nIters = 1, nNoImpr = ABC_INFINITY, TimeOut = 20, nAnds = 0, Seed = 0, fUseTwo = 0, fVerbose = 0; + + int fKeepBMiter = 0; + Gia_Man_t * pMiter; + Gia_Man_t * pImpl; + Gia_Man_t * pDup; + Gia_Obj_t* pObj; + Gia_Man_t * pSpec = NULL; + char ** pArgvNew; + int i, nArgcNew, nPo; + int nBInput = -1; + char *FileName; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vkhI," ) ) != EOF ) + { + switch ( c ) + { + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + nBInput = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( nBInput < 0 ) + goto usage; + break; + case 'k': + fKeepBMiter ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + pArgvNew = argv + globalUtilOptind; + nArgcNew = argc - globalUtilOptind; + if ( nArgcNew != 1 ) + { + Abc_Print( -1, "There is no file name.\n" ); + return 1; + } + + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9RecoverBoundary(): There is no AIG.\n" ); + return 0; + } + FileName = pArgvNew[0]; + + + // printing + + // Gia_ManForEachCo( pAbc->pGia, pObj, i ){ + // printf("Original node: %s id: %i\n", Gia_ObjCoName(pAbc->pGia, i), i); + // } + + + /* + // perform heavy synthesis + pTemp = Gia_ManDeepSyn( pAbc->pGia, nIters, nNoImpr, TimeOut, nAnds, Seed, fUseTwo, fVerbose ); + Abc_FrameUpdateGia( pAbc, pTemp ); + // print spec/impl and boundary information + Gia_ManForEachCo( pAbc->pGia, pObj, i ){ + printf("Output node: %s id: %i\n", Gia_ObjCoName(pAbc->pGia, i), i); + } + */ + + + + // check boundary recovery status + pSpec = Gia_AigerRead( FileName, false, true, 0 ); + if ( !pSpec ) + { + Abc_Print( -1, "Abc_CommandAbc9RecoverBoundary(): fail to read spec.\n" ); + return 1; + } + nPo = Gia_ManCoNum( pSpec ); + + // duplicate + pDup = Gia_ManDup( pAbc->pGia ); + + // option 1: remove po and keep the buffers + // default nbinput: + if ( nBInput == -1 ) nBInput = (Gia_ManCoNum(pDup)-2*nPo)/2; + pImpl = Gia_ManImplFromBMiter( pDup, nPo, nBInput ); + + // option 2: build miter (with uif?) + if (!fKeepBMiter ) + { + pMiter = Gia_ManMiterFromBMiter( pAbc->pGia, nPo ); + Abc_FrameUpdateGia( pAbc, pMiter ); + } + + return 0; + +usage: + Abc_Print( -2, "usage: &rb [-vkh] \n" ); + Abc_Print( -2, "\t generate an implementation aig with specification boundary\n" ); + Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-k : keep the bmiter and print the boundary status only.\n"); + Abc_Print( -2, "\t-I num : the number of inputs in the boundary\n"); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t : the specification file\n"); + return 1; +} /**Function************************************************************* From ba64d6118b16f4f405b65affb0b04797e5b665e1 Mon Sep 17 00:00:00 2001 From: Allen Ho Date: Mon, 30 Oct 2023 15:09:01 -0700 Subject: [PATCH 02/11] out-side box matching --- Makefile | 3 +- src/aig/gia/giaDup.c | 96 ++++++++++++++++++++++++++++++++++++++++ src/proof/cec/cecSatG2.c | 57 ++++++++++++++++++++++++ 3 files changed, 155 insertions(+), 1 deletion(-) diff --git a/Makefile b/Makefile index 3976cf7b1..e6c0f4453 100644 --- a/Makefile +++ b/Makefile @@ -33,7 +33,8 @@ MODULES := \ src/proof/pdr src/proof/abs src/proof/live src/proof/ssc src/proof/int \ src/proof/cec src/proof/acec src/proof/dch src/proof/fraig src/proof/fra src/proof/ssw \ src/aig/aig src/aig/saig src/aig/gia src/aig/ioa src/aig/ivy src/aig/hop \ - src/aig/miniaig + src/aig/miniaig \ + src/sat/bsat2 all: $(PROG) default: $(PROG) diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 665164eb2..4efbe90dc 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -30,6 +30,8 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +Vec_Int_t* vLitBmiter; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -5699,13 +5701,107 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ) Gia_ManConst0(p2)->Value = 0; Gia_ManForEachCi( p1, pObj, i ) pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew ); + + // TODO: record the corresponding impl node of each lit + vLitBmiter = Vec_IntAlloc( Gia_ManObjNum(p2) ); + Vec_IntFill( vLitBmiter, Gia_ManObjNum(p2) + Gia_ManObjNum(p1), 0 ); + Gia_ManForEachAnd( p2, pObj, i ) + { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 3 ); + } + + // TODO: find nodes in spec + + Vec_Int_t * vTypeSpec = Vec_IntAlloc( 16 ); + Vec_IntFill( vTypeSpec, Gia_ManObjNum(p1), 0 ); + int n = Gia_ManBufNum(p1) / 2; + + Gia_ManStaticFanoutStart( p1 ); + Vec_Ptr_t * vQ = Vec_PtrAlloc(16); + Gia_Obj_t * pObj2; + int c1 = 0; + int c2 = 0; + int count; + Gia_ManForEachBuf( p1, pObj, i ) + { + if ( count < n ) + { + Vec_IntSetEntry( vTypeSpec, Gia_ObjId( p1, pObj ), 1 ); + c1++; + count ++; + + Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) ); + Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) ); + while ( Vec_PtrSize(vQ) != 0 ) + { + pObj2 = Vec_PtrPop(vQ); + if ( Vec_IntEntry( vTypeSpec, Gia_ObjId(p1, pObj2) ) != 0 ) continue; + c1 ++; + Vec_IntSetEntry( vTypeSpec, Gia_ObjId(p1, pObj2), 1 ); + if ( Gia_ObjFaninNum(p1, pObj2) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj2) ); + if ( Gia_ObjFaninNum(p1, pObj2) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj2) ); + } + + } + else + { + Vec_IntSetEntry( vTypeSpec, Gia_ObjId( p1, pObj ), 2 ); + c2 ++; + + int j; + // pObj = Gia_ObjFanin0(pObj); + Gia_ObjForEachFanoutStatic(p1, pObj, pObj2, j) + { + Vec_PtrPush( vQ, pObj2 ); + } + while ( Vec_PtrSize(vQ) != 0 ) + { + pObj2 = Vec_PtrPop(vQ); + if ( Vec_IntEntry( vTypeSpec, Gia_ObjId(p1, pObj2) ) != 0 ) continue; + Vec_IntSetEntry( vTypeSpec, Gia_ObjId(p1, pObj2), 2 ); + c2 ++; + for( int j = 0; j < Gia_ObjFanoutNum(p1, pObj2); j++ ) + { + Vec_PtrPush( vQ, Gia_ObjFanout(p1, pObj2, j) ); + } + } + + } + } + + Gia_ManStaticFanoutStop( p1 ); + + printf( "category %d %d %d\n", c1, c2, Gia_ManObjNum(p1) ); + + + // TODO: record hashed equivalent nodes + Gia_ManForEachAnd( p1, pObj, i ) { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) > 0 ) + { + if ( Vec_IntGetEntry( vLitBmiter, pObj->Value ) == 3 ) // eq node in impl + { + Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 3 + Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) ); + } + else + { + Vec_IntUpdateEntry( vLitBmiter, pObj->Value, Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) ); + } + } if ( Gia_ObjIsBuf(pObj) ) Vec_IntPush( vLits, pObj->Value ); } + + // int e; + // Vec_IntForEachEntry( vLitBmiter, e, i ) + // { + // printf( "%d ", e ); + // } + // printf("\n"); + Gia_ManForEachCo( p2, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); //Gia_ManForEachCo( p1, pObj, i ) diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 281deb0e9..d641704f7 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -143,6 +143,9 @@ static inline int Cec4_ObjSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) static inline int Cec4_ObjSetSatId( Gia_Man_t * p, Gia_Obj_t * pObj, int Num ) { assert(Cec4_ObjSatId(p, pObj) == -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), Num); Vec_IntPush(&p->vSuppVars, Gia_ObjId(p, pObj)); if ( Gia_ObjIsCi(pObj) ) Vec_IntPushTwo(&p->vCopiesTwo, Gia_ObjId(p, pObj), Num); assert(Vec_IntSize(&p->vVarMap) == Num); Vec_IntPush(&p->vVarMap, Gia_ObjId(p, pObj)); return Num; } static inline void Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(Cec4_ObjSatId(p, pObj) != -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), -1); } + +extern Vec_Int_t* vLitBmiter; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -1887,7 +1890,43 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p continue; } if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) ) + { + if ( Vec_IntEntry( vLitBmiter, pRepr->Value ) == 3 ) + { + switch ( Vec_IntEntry( vLitBmiter, pObj -> Value ) ) + { + case 1: + case 4: + Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 4 ); + break; + case 2: + case 5: + Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 5 ); + break; + default: + break; + } + } + else + { + if ( Vec_IntEntry(vLitBmiter, pObj->Value ) == 3 ) + switch ( Vec_IntEntry( vLitBmiter, pRepr -> Value ) ) + { + case 1: + case 4: + Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 4 ); + break; + case 2: + case 5: + Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 5 ); + break; + default: + break; + + } + } pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase ); + } } if ( p->iPatsPi > 0 ) { @@ -1933,10 +1972,28 @@ finalize: Gia_ManRemoveWrongChoices( p ); return p->pCexSeq ? 0 : 1; } +extern Vec_Int_t * vLitBmiter; Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ) { Gia_Man_t * pNew = NULL; Cec4_ManPerformSweeping( p, pPars, &pNew, 0 ); + + int e, i, c1=0, c2=0, c3=0, c4=0, c5=0; + Vec_IntForEachEntry( vLitBmiter, e, i ) + { + if ( i%2 ) continue; + switch (e) + { + case 1: c1++; break; + case 2: c2++; break; + case 3: c3++; break; + case 4: c4++; break; + case 5: c5++; break; + default: + break; + } + } + printf("category %d %d %d %d %d\n", c1, c2, c3+c4+c5, c4, c5); return pNew; } void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose ) From 50010139ef9b41040d902bad898458c59424771f Mon Sep 17 00:00:00 2001 From: Allen Ho Date: Mon, 6 Nov 2023 18:37:40 +0800 Subject: [PATCH 03/11] why --- src/proof/cec/cecSatG2.c | 1 + 1 file changed, 1 insertion(+) diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index d641704f7..1a6309ebe 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -1978,6 +1978,7 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ) Gia_Man_t * pNew = NULL; Cec4_ManPerformSweeping( p, pPars, &pNew, 0 ); + // TODO int e, i, c1=0, c2=0, c3=0, c4=0, c5=0; Vec_IntForEachEntry( vLitBmiter, e, i ) { From 67a2b97cf0f5437198f01cea2d99b54d77a6491e Mon Sep 17 00:00:00 2001 From: WWFUG Date: Wed, 8 Nov 2023 19:00:03 +0800 Subject: [PATCH 04/11] added -I options in &bmiter --- .gitignore | 6 ++++ src/aig/gia/giaDup.c | 5 ++- src/base/abci/abc.c | 24 ++++++++++--- src/base/abci/abcMiter.c | 1 + src/proof/cec/cec.h | 1 + src/proof/cec/cecSatG2.c | 75 +++++++++++++++++++++------------------- 6 files changed, 71 insertions(+), 41 deletions(-) diff --git a/.gitignore b/.gitignore index cbb424152..f0c5201c6 100644 --- a/.gitignore +++ b/.gitignore @@ -8,6 +8,12 @@ ReleaseExt/ _/ _TEST/ +_sandwich/ +_scripts/ +*.aig +*.vcproj +*.sh +*.v lib/abc* lib/m114* lib/bip* diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 4efbe90dc..24c1d3b0e 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -5669,7 +5669,7 @@ Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ) +Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum) { Vec_Int_t * vLits; Gia_Man_t * pNew, * pTemp; @@ -5717,6 +5717,9 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ) Vec_Int_t * vTypeSpec = Vec_IntAlloc( 16 ); Vec_IntFill( vTypeSpec, Gia_ManObjNum(p1), 0 ); int n = Gia_ManBufNum(p1) / 2; + if(biNum > 0){ + n = biNum; + } Gia_ManStaticFanoutStart( p1 ); Vec_Ptr_t * vQ = Vec_PtrAlloc(16); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 906b456ad..dab809c25 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -37921,7 +37921,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500, nMaxNodes = 0; Cec4_ManSetParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMrmdckngxysopwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMrmdckngxysopwqvh" ) ) != EOF ) { switch ( c ) { @@ -38074,6 +38074,9 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'w': pPars->fVeryVerbose ^= 1; break; + case 'q': + pPars->fBMiterInfo ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -38138,6 +38141,7 @@ usage: Abc_Print( -2, "\t-o : toggle using the old SAT sweeper [default = %s]\n", fUseIvy? "yes": "no" ); Abc_Print( -2, "\t-p : toggle trying to prove when running the old SAT sweeper [default = %s]\n", fUseProve? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing even more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); + Abc_Print( -2, "\t-q : toggle printing additional information for boundary miters [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -51689,16 +51693,25 @@ usage: ***********************************************************************/ int Abc_CommandAbc9BMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ); + extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum); Gia_Man_t * pTemp, * pSecond; char * FileName = NULL; FILE * pFile = NULL; int c, fVerbose = 0; + int bi = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF ) { switch ( c ) { + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + bi = atoi(argv[globalUtilOptind++]); + break; case 'v': fVerbose ^= 1; break; @@ -51737,14 +51750,15 @@ int Abc_CommandAbc9BMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9BMiter(): Cannot read the file name on the command line.\n" ); return 0; } - pTemp = Gia_ManBoundaryMiter( pAbc->pGia, pSecond, fVerbose ); + pTemp = Gia_ManBoundaryMiter( pAbc->pGia, pSecond, fVerbose, bi); Gia_ManStop( pSecond ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; usage: - Abc_Print( -2, "usage: &bmiter [-vh] \n" ); + Abc_Print( -2, "usage: &bmiter -I [-vh] \n" ); Abc_Print( -2, "\t creates the boundary miter\n" ); + Abc_Print( -2, "\t-I : number of boundary inputs\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 file\n"); diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c index 6086fc616..6077a20c2 100644 --- a/src/base/abci/abcMiter.c +++ b/src/base/abci/abcMiter.c @@ -789,6 +789,7 @@ Abc_Ntk_t * Abc_NtkFrames( Abc_Ntk_t * pNtk, int nFrames, int fInitial, int fVer pNtkFrames->pName = Extra_UtilStrsav(Buffer); // map the constant nodes Abc_AigConst1(pNtk)->pCopy = Abc_AigConst1(pNtkFrames); + // create new latches (or their initial values) and remember them in the new latches if ( !fInitial ) { diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index d11bca3c3..ca4ac9aba 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -120,6 +120,7 @@ struct Cec_ParFra_t_ int fVeryVerbose; // verbose stats int fVerbose; // verbose stats int iOutFail; // the failed output + int fBMiterInfo; // printing BMiter information }; // combinational equivalence checking parameters diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 1a6309ebe..424369b8c 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -222,6 +222,7 @@ void Cec4_ManSetParams( Cec_ParFra_t * pPars ) pPars->nSatVarMax = 1000; // the max number of SAT variables before recycling SAT solver pPars->nCallsRecycle = 500; // calls to perform before recycling SAT solver pPars->nGenIters = 100; // pattern generation iterations + pPars->fBMiterInfo = 0; // printing BMiter information } /**Function************************************************************* @@ -1891,39 +1892,41 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p } if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) ) { - if ( Vec_IntEntry( vLitBmiter, pRepr->Value ) == 3 ) - { - switch ( Vec_IntEntry( vLitBmiter, pObj -> Value ) ) + if (pPars->fBMiterInfo){ + if ( Vec_IntEntry( vLitBmiter, pRepr->Value ) == 3 ) { - case 1: - case 4: - Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 4 ); - break; - case 2: - case 5: - Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 5 ); - break; - default: - break; - } - } - else - { - if ( Vec_IntEntry(vLitBmiter, pObj->Value ) == 3 ) - switch ( Vec_IntEntry( vLitBmiter, pRepr -> Value ) ) + switch ( Vec_IntEntry( vLitBmiter, pObj -> Value ) ) { case 1: case 4: - Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 4 ); + Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 4 ); break; case 2: case 5: - Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 5 ); + Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 5 ); break; default: break; - } + } + else + { + if ( Vec_IntEntry(vLitBmiter, pObj->Value ) == 3 ) + switch ( Vec_IntEntry( vLitBmiter, pRepr -> Value ) ) + { + case 1: + case 4: + Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 4 ); + break; + case 2: + case 5: + Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 5 ); + break; + default: + break; + + } + } } pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase ); } @@ -1979,22 +1982,24 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ) Cec4_ManPerformSweeping( p, pPars, &pNew, 0 ); // TODO - int e, i, c1=0, c2=0, c3=0, c4=0, c5=0; - Vec_IntForEachEntry( vLitBmiter, e, i ) - { - if ( i%2 ) continue; - switch (e) + if (pPars -> fBMiterInfo){ + int e, i, c1=0, c2=0, c3=0, c4=0, c5=0; + Vec_IntForEachEntry( vLitBmiter, e, i ) { - case 1: c1++; break; - case 2: c2++; break; - case 3: c3++; break; - case 4: c4++; break; - case 5: c5++; break; - default: - break; + if ( i%2 ) continue; + switch (e) + { + case 1: c1++; break; + case 2: c2++; break; + case 3: c3++; break; + case 4: c4++; break; + case 5: c5++; break; + default: + break; + } } + printf("category %d %d %d %d %d\n", c1, c2, c3+c4+c5, c4, c5); } - printf("category %d %d %d %d %d\n", c1, c2, c3+c4+c5, c4, c5); return pNew; } void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose ) From a31684734192df82d5a135e2e0d263e83dfdf54e Mon Sep 17 00:00:00 2001 From: Allen Ho Date: Thu, 23 Nov 2023 19:33:05 +0800 Subject: [PATCH 05/11] correct fanout count --- src/aig/gia/giaDup.c | 36 +++++++++++++++++-------- src/proof/cec/cecSatG2.c | 57 +++++++++++++++++++++++++++++++++------- 2 files changed, 73 insertions(+), 20 deletions(-) diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 24c1d3b0e..9d9b56a1c 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -5703,8 +5703,9 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew ); // TODO: record the corresponding impl node of each lit - vLitBmiter = Vec_IntAlloc( Gia_ManObjNum(p2) ); - Vec_IntFill( vLitBmiter, Gia_ManObjNum(p2) + Gia_ManObjNum(p1), 0 ); + vLitBmiter = Vec_IntAlloc( (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) * 2 ); + Vec_IntFill( vLitBmiter, (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) * 2, 0 ); + printf( "allocated size: %d\n", Vec_IntSize(vLitBmiter) ); Gia_ManForEachAnd( p2, pObj, i ) { @@ -5776,7 +5777,7 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, Gia_ManStaticFanoutStop( p1 ); - printf( "category %d %d %d\n", c1, c2, Gia_ManObjNum(p1) ); + printf( "spec: fanin: %d / fanout: %d / total %d\n", c1, c2, Gia_ManObjNum(p1) ); // TODO: record hashed equivalent nodes @@ -5798,17 +5799,30 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, Vec_IntPush( vLits, pObj->Value ); } - // int e; - // Vec_IntForEachEntry( vLitBmiter, e, i ) - // { - // printf( "%d ", e ); - // } - // printf("\n"); + + int e, c3=0, c4=0, c5=0; + c1 = 0; c2 = 0; + + Vec_IntForEachEntry( vLitBmiter, e, i ) + { + if ( i%2 ) continue; + switch (e) + { + case 1: c1++; break; + case 2: c2++; break; + case 3: c3++; break; + case 4: c4++; break; + case 5: c5++; break; + default: + break; + } + } + printf("(strash) impl: eq_fanin: %d / eq_fanout: %d / total: %d\n", c4, c5, c3+c4+c5); Gia_ManForEachCo( p2, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - //Gia_ManForEachCo( p1, pObj, i ) - // Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManForEachCo( p1, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Vec_IntForEachEntry( vLits, iLit, i ) Gia_ManAppendCo( pNew, iLit ); Vec_IntFree( vLits ); diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 424369b8c..4a39e95d3 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -1882,8 +1882,46 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p if ( pRepr == NULL ) continue; } + int lit_obj = Gia_ObjId( p, pObj ) << 1; + int lit_repr = Gia_ObjId( p, pRepr ) << 1; + if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) ) { + // printf( "*node %d (%d) merged into node %d (%d)\n", lit_obj >> 1, Vec_IntEntry( vLitBmiter, lit_obj ), lit_repr >> 1, Vec_IntEntry( vLitBmiter, lit_repr) ); + if ( Vec_IntEntry( vLitBmiter, lit_repr ) == 3 ) + { + switch ( Vec_IntEntry( vLitBmiter, lit_obj ) ) + { + case 1: + case 4: + Vec_IntUpdateEntry( vLitBmiter, lit_repr, 4 ); + break; + case 2: + case 5: + Vec_IntUpdateEntry( vLitBmiter, lit_repr, 5 ); + break; + default: + break; + } + } + else + { + if ( Vec_IntEntry(vLitBmiter, lit_obj ) == 3 ) + switch ( Vec_IntEntry( vLitBmiter, lit_repr ) ) + { + case 1: + case 4: + Vec_IntUpdateEntry( vLitBmiter, lit_obj, 4 ); + break; + case 2: + case 5: + Vec_IntUpdateEntry( vLitBmiter, lit_obj, 5 ); + break; + default: + break; + + } + } assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) ); Gia_ObjSetProved( p, i ); if ( Gia_ObjId(p, pRepr) == 0 ) @@ -1893,17 +1931,18 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) ) { if (pPars->fBMiterInfo){ - if ( Vec_IntEntry( vLitBmiter, pRepr->Value ) == 3 ) + // printf( "node %d (%d) merged into node %d (%d)\n", lit_obj, Vec_IntEntry( vLitBmiter, lit_obj ), lit_repr, Vec_IntEntry( vLitBmiter, lit_repr ) ); + if ( Vec_IntEntry( vLitBmiter, lit_repr ) == 3 ) { - switch ( Vec_IntEntry( vLitBmiter, pObj -> Value ) ) + switch ( Vec_IntEntry( vLitBmiter, lit_obj ) ) { case 1: case 4: - Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 4 ); + Vec_IntUpdateEntry( vLitBmiter, lit_repr, 4 ); break; case 2: case 5: - Vec_IntUpdateEntry( vLitBmiter, pRepr->Value, 5 ); + Vec_IntUpdateEntry( vLitBmiter, lit_repr, 5 ); break; default: break; @@ -1911,16 +1950,16 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p } else { - if ( Vec_IntEntry(vLitBmiter, pObj->Value ) == 3 ) - switch ( Vec_IntEntry( vLitBmiter, pRepr -> Value ) ) + if ( Vec_IntEntry(vLitBmiter, lit_obj ) == 3 ) + switch ( Vec_IntEntry( vLitBmiter, lit_repr ) ) { case 1: case 4: - Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 4 ); + Vec_IntUpdateEntry( vLitBmiter, lit_obj, 4 ); break; case 2: case 5: - Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 5 ); + Vec_IntUpdateEntry( vLitBmiter, lit_obj, 5 ); break; default: break; @@ -1998,7 +2037,7 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ) break; } } - printf("category %d %d %d %d %d\n", c1, c2, c3+c4+c5, c4, c5); + printf("(fraig) impl: eq_fanin: %d / eq_fanout: %d / total: %d\n", c4, c5, c3+c4+c5); } return pNew; } From 9bb5333f6210a49d7e0895139ef30386585b2594 Mon Sep 17 00:00:00 2001 From: Allen Ho Date: Thu, 7 Dec 2023 19:07:52 +0800 Subject: [PATCH 06/11] extend bo --- abc.rc | 148 ---------------------------------- src/aig/gia/giaDup.c | 19 +++++ src/base/abci/abc.c | 14 +++- src/proof/cec/cec.h | 1 + src/proof/cec/cecSatG2.c | 168 +++++++++++++++++++++++++++++---------- 5 files changed, 157 insertions(+), 193 deletions(-) delete mode 100644 abc.rc diff --git a/abc.rc b/abc.rc deleted file mode 100644 index a3efc0b09..000000000 --- a/abc.rc +++ /dev/null @@ -1,148 +0,0 @@ -# global parameters -set check # checks intermediate networks -#set checkfio # prints warnings when fanins/fanouts are duplicated -#unset checkread # does not check new networks after reading from file -#set backup # saves backup networks retrived by "undo" and "recall" -#set savesteps 1 # sets the maximum number of backup networks to save -#set progressbar # display the progress bar - -# program names for internal calls -set dotwin dot.exe -set dotunix dot -set gsviewwin gsview32.exe -set gsviewunix gv -set siswin sis.exe -set sisunix sis -set mvsiswin mvsis.exe -set mvsisunix mvsis -set capowin MetaPl-Capo10.1-Win32.exe -set capounix MetaPl-Capo10.1 -set gnuplotwin wgnuplot.exe -set gnuplotunix gnuplot - -# Niklas Een's commands -#load_plugin C:\_projects\abc\lib\bip_win.exe "BIP" - -# standard aliases -alias hi history -alias b balance -alias cg clockgate -alias cl cleanup -alias clp collapse -alias cs care_set -alias el eliminate -alias esd ext_seq_dcs -alias f fraig -alias fs fraig_sweep -alias fsto fraig_store -alias fres fraig_restore -alias fr fretime -alias ft fraig_trust -alias ic indcut -alias lp lutpack -alias pcon print_cone -alias pd print_dsd -alias pex print_exdc -d -alias pf print_factor -alias pfan print_fanio -alias pg print_gates -alias pl print_level -alias plat print_latch -alias pio print_io -alias pk print_kmap -alias pm print_miter -alias ps print_stats -alias psb print_stats -b -alias psu print_supp -alias psy print_symm -alias pun print_unate -alias q quit -alias r read -alias ra read_aiger -alias r3 retime -M 3 -alias r3f retime -M 3 -f -alias r3b retime -M 3 -b -alias ren renode -alias rh read_hie -alias ri read_init -alias rl read_blif -alias rb read_bench -alias ret retime -alias dret dretime -alias rp read_pla -alias rt read_truth -alias rv read_verilog -alias rvl read_verlib -alias rsup read_super mcnc5_old.super -alias rlib read_library -alias rlibc read_library cadence.genlib -alias rty read_liberty -alias rlut read_lut -alias rw rewrite -alias rwz rewrite -z -alias rf refactor -alias rfz refactor -z -alias re restructure -alias rez restructure -z -alias rs resub -alias rsz resub -z -alias sa set autoexec ps -alias scl scleanup -alias sif if -s -alias so source -x -alias st strash -alias sw sweep -alias ssw ssweep -alias tr0 trace_start -alias tr1 trace_check -alias trt "r c.blif; st; tr0; b; tr1" -alias u undo -alias w write -alias wa write_aiger -alias wb write_bench -alias wc write_cnf -alias wh write_hie -alias wl write_blif -alias wp write_pla -alias wv write_verilog - -# standard scripts -alias resyn "b; rw; rwz; b; rwz; b" -alias resyn2 "b; rw; rf; b; rw; rwz; b; rfz; rwz; b" -alias resyn2a "b; rw; b; rw; rwz; b; rwz; b" -alias resyn3 "b; rs; rs -K 6; b; rsz; rsz -K 6; b; rsz -K 5; b" -alias compress "b -l; rw -l; rwz -l; b -l; rwz -l; b -l" -alias compress2 "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l" -alias choice "fraig_store; resyn; fraig_store; resyn2; fraig_store; fraig_restore" -alias choice2 "fraig_store; balance; fraig_store; resyn; fraig_store; resyn2; fraig_store; resyn2; fraig_store; fraig_restore" -alias rwsat "st; rw -l; b -l; rw -l; rf -l" -alias drwsat2 "st; drw; b -l; drw; drf; ifraig -C 20; drw; b -l; drw; drf" -alias share "st; multi -m; sop; fx; resyn2" -alias addinit "read_init; undc; strash; zero" -alias blif2aig "undc; strash; zero" -alias v2p "&vta_gla; &ps; &gla_derive; &put; w 1.aig; pdr -v" -alias g2p "&ps; &gla_derive; &put; w 2.aig; pdr -v" -alias &sw_ "&put; sweep; st; &get" -alias &fx_ "&put; sweep; sop; fx; st; &get" -alias &dc3 "&b; &jf -K 6; &b; &jf -K 4; &b" -alias &dc4 "&b; &jf -K 7; &fx; &b; &jf -K 5; &fx; &b" - -# resubstitution scripts for the IWLS paper -alias src_rw "st; rw -l; rwz -l; rwz -l" -alias src_rs "st; rs -K 6 -N 2 -l; rs -K 9 -N 2 -l; rs -K 12 -N 2 -l" -alias src_rws "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l; rs -K 12 -N 2 -l" -alias resyn2rs "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b" -alias r2rs "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b" -alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l" -alias c2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l" - -# use this script to convert 1-valued and DC-valued flops for an AIG -alias fix_aig "logic; undc; strash; zero" - -# use this script to convert 1-valued and DC-valued flops for a logic network coming from BLIF -alias fix_blif "undc; strash; zero" - -# lazy man's synthesis -alias recadd3 "st; rec_add3; b; rec_add3; dc2; rec_add3; if -K 8; bidec; st; rec_add3; dc2; rec_add3; if -g -K 6; st; rec_add3" - - diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 9d9b56a1c..ffd776cc4 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -31,6 +31,8 @@ ABC_NAMESPACE_IMPL_START //////////////////////////////////////////////////////////////////////// Vec_Int_t* vLitBmiter; +Vec_Int_t* vIdBI; +Vec_Int_t* vIdBO; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -5728,6 +5730,11 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int c1 = 0; int c2 = 0; int count; + int val; + + vIdBI = Vec_IntAlloc(16); + vIdBO = Vec_IntAlloc(16); + Gia_ManForEachBuf( p1, pObj, i ) { if ( count < n ) @@ -5782,6 +5789,7 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, // TODO: record hashed equivalent nodes + count = 0; Gia_ManForEachAnd( p1, pObj, i ) { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); if ( Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) > 0 ) @@ -5796,7 +5804,18 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, } } if ( Gia_ObjIsBuf(pObj) ) + { Vec_IntPush( vLits, pObj->Value ); + if ( count < n ) + { + Vec_IntPush( vIdBI, (pObj->Value) >> 1 ); + } + else + { + Vec_IntPush( vIdBO, (pObj->Value) >> 1 ); + } + count ++; + } } diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index dab809c25..755aeaea0 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -37921,7 +37921,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500, nMaxNodes = 0; Cec4_ManSetParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMrmdckngxysopwqvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "OJWRILDCNPMrmdckngxysopwqvh" ) ) != EOF ) { switch ( c ) { @@ -37969,6 +37969,18 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nItersMax < 0 ) goto usage; break; + case 'O': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nPO = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nPO < 1 ) + goto usage; + break; + case 'L': if ( globalUtilOptind >= argc ) { diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index ca4ac9aba..c9aa96658 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -121,6 +121,7 @@ struct Cec_ParFra_t_ int fVerbose; // verbose stats int iOutFail; // the failed output int fBMiterInfo; // printing BMiter information + int nPO; // number of po in original design given a bmiter }; // combinational equivalence checking parameters diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 4a39e95d3..a01cc7445 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -145,6 +145,9 @@ static inline void Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) extern Vec_Int_t* vLitBmiter; +extern Vec_Int_t* vIdBI; +extern Vec_Int_t* vIdBO; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -1887,51 +1890,9 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) ) { - // printf( "*node %d (%d) merged into node %d (%d)\n", lit_obj >> 1, Vec_IntEntry( vLitBmiter, lit_obj ), lit_repr >> 1, Vec_IntEntry( vLitBmiter, lit_repr) ); - if ( Vec_IntEntry( vLitBmiter, lit_repr ) == 3 ) + printf( "*node %d (%d) merged into node %d (%d)\n", lit_obj >> 1, Vec_IntEntry( vLitBmiter, lit_obj ), lit_repr >> 1, Vec_IntEntry( vLitBmiter, lit_repr) ); + if ( pPars->fBMiterInfo ) { - switch ( Vec_IntEntry( vLitBmiter, lit_obj ) ) - { - case 1: - case 4: - Vec_IntUpdateEntry( vLitBmiter, lit_repr, 4 ); - break; - case 2: - case 5: - Vec_IntUpdateEntry( vLitBmiter, lit_repr, 5 ); - break; - default: - break; - } - } - else - { - if ( Vec_IntEntry(vLitBmiter, lit_obj ) == 3 ) - switch ( Vec_IntEntry( vLitBmiter, lit_repr ) ) - { - case 1: - case 4: - Vec_IntUpdateEntry( vLitBmiter, lit_obj, 4 ); - break; - case 2: - case 5: - Vec_IntUpdateEntry( vLitBmiter, lit_obj, 5 ); - break; - default: - break; - - } - } - assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) ); - Gia_ObjSetProved( p, i ); - if ( Gia_ObjId(p, pRepr) == 0 ) - pMan->iLastConst = i; - continue; - } - if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) ) - { - if (pPars->fBMiterInfo){ - // printf( "node %d (%d) merged into node %d (%d)\n", lit_obj, Vec_IntEntry( vLitBmiter, lit_obj ), lit_repr, Vec_IntEntry( vLitBmiter, lit_repr ) ); if ( Vec_IntEntry( vLitBmiter, lit_repr ) == 3 ) { switch ( Vec_IntEntry( vLitBmiter, lit_obj ) ) @@ -1966,10 +1927,129 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p } } + // TODO + Vec_IntSetEntry( vLitBmiter, lit_obj, Vec_IntEntry( vLitBmiter, lit_repr) ); + } + assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) ); + Gia_ObjSetProved( p, i ); + if ( Gia_ObjId(p, pRepr) == 0 ) + pMan->iLastConst = i; + continue; + } + if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) ) + { + if (pPars->fBMiterInfo){ + printf( "node %d (%d) merged into node %d (%d)\n", lit_obj >> 1, Vec_IntEntry( vLitBmiter, lit_obj ), lit_repr >> 1, Vec_IntEntry( vLitBmiter, lit_repr ) ); + if ( Vec_IntEntry( vLitBmiter, lit_repr ) == 3 ) + { + switch ( Vec_IntEntry( vLitBmiter, lit_obj ) ) + { + case 1: + case 4: + Vec_IntUpdateEntry( vLitBmiter, lit_repr, 4 ); + break; + case 2: + case 5: + Vec_IntUpdateEntry( vLitBmiter, lit_repr, 5 ); + break; + default: + break; + } + } + else + { + if ( Vec_IntEntry(vLitBmiter, lit_obj ) == 3 ) + switch ( Vec_IntEntry( vLitBmiter, lit_repr ) ) + { + case 1: + case 4: + Vec_IntUpdateEntry( vLitBmiter, lit_obj, 4 ); + break; + case 2: + case 5: + Vec_IntUpdateEntry( vLitBmiter, lit_obj, 5 ); + break; + default: + break; + + } + } + // TODO + Vec_IntSetEntry( vLitBmiter, lit_obj, Vec_IntEntry( vLitBmiter, lit_repr) ); } pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase ); } } + + + if ( pPars->fBMiterInfo ) + { + + // check bi, bo + Vec_Ptr_t* vBO = Vec_PtrAlloc( 16 ); + Vec_Ptr_t * vQ = Vec_PtrAlloc(16); + + int val; + printf("BI:"); + Vec_IntForEachEntry( vIdBI, val, i ) + { + printf( " %d (%d)", val, Vec_IntEntry( vLitBmiter, val << 1) ); + } + printf("\nBO:"); + Vec_IntForEachEntry( vIdBO, val, i ) + { + printf( " %d (%d)", val, Vec_IntEntry( vLitBmiter, val << 1) ); + if ( Vec_IntEntry( vLitBmiter, val << 1) != 5 ) + { + Vec_PtrPush(vQ, &((p->pObjs)[val]) ); + } + } + printf("\n"); + + // find bound + + Gia_ManStaticFanoutStart( p ); + + Vec_Int_t* vFlag = Vec_IntAlloc( p->nObjs ); + Vec_IntFill( vFlag, p->nObjs, 0 ); + Gia_Obj_t * pObj2; + int cnt_node = 0; + int cnt_newBo = 0; + + while ( Vec_PtrSize(vQ) != 0 ) + { + pObj2 = Vec_PtrPop(vQ); + if ( Vec_IntEntry( vFlag, Gia_ObjId(p, pObj2) ) != 0 ) continue; + cnt_node ++; + Vec_IntSetEntry( vFlag, Gia_ObjId(p, pObj2), 1 ); + + val = Vec_IntEntry(vLitBmiter, Gia_ObjId(p, pObj2) << 1); + if ( val == 5 || Gia_ObjIsCo( pObj2 ) ) // boundary found + { + cnt_newBo ++; + Vec_PtrPush( vBO, pObj2 ); + continue; + } + + for( int j = 0; j < Gia_ObjFanoutNum(p, pObj2); j++ ) + { + Vec_PtrPush( vQ, Gia_ObjFanout(p, pObj2, j) ); + printf( "add fanout\n"); + } + } + + Gia_ManStaticFanoutStop(p); + + + printf("extended BO with %d extra nodes:", cnt_node); + Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i ) + { + printf( " %d", Gia_ObjId(p, pObj) ); + } + printf("\n"); + } + + if ( p->iPatsPi > 0 ) { abctime clk2 = Abc_Clock(); From 284b9d6a9c01c7df0636a696fc35a47d10f10f0a Mon Sep 17 00:00:00 2001 From: Allen Ho Date: Sun, 10 Dec 2023 21:30:46 +0800 Subject: [PATCH 07/11] extended box report; --- src/aig/gia/giaDup.c | 68 ++++++++++++++---- src/base/abci/abc.c | 14 +--- src/proof/cec/cecSatG2.c | 150 +++++++++++++++++++++++++++------------ 3 files changed, 160 insertions(+), 72 deletions(-) diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index ffd776cc4..aa8f1c053 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -30,7 +30,7 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -Vec_Int_t* vLitBmiter; +Vec_Int_t* vMarkBmiter; Vec_Int_t* vIdBI; Vec_Int_t* vIdBO; @@ -5701,18 +5701,24 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, Gia_ManHashStart( pNew ); Gia_ManConst0(p1)->Value = 0; Gia_ManConst0(p2)->Value = 0; + + // allocate vMarkBmiter + vMarkBmiter = Vec_IntAlloc( (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) ); + Vec_IntFill( vMarkBmiter, (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)), 0 ); + printf( "allocated size: %d\n", Vec_IntSize(vMarkBmiter) ); + Gia_ManForEachCi( p1, pObj, i ) - pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew ); + { + int id = pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew ); + Vec_IntSetEntry( vMarkBmiter, id >> 1, 4 ); + } // TODO: record the corresponding impl node of each lit - vLitBmiter = Vec_IntAlloc( (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) * 2 ); - Vec_IntFill( vLitBmiter, (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) * 2, 0 ); - printf( "allocated size: %d\n", Vec_IntSize(vLitBmiter) ); Gia_ManForEachAnd( p2, pObj, i ) { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 3 ); + Vec_IntUpdateEntry( vMarkBmiter, pObj->Value >> 1, 3 ); } // TODO: find nodes in spec @@ -5726,11 +5732,11 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, Gia_ManStaticFanoutStart( p1 ); Vec_Ptr_t * vQ = Vec_PtrAlloc(16); + Vec_Ptr_t * vBO = Vec_PtrAlloc(16); Gia_Obj_t * pObj2; int c1 = 0; int c2 = 0; - int count; - int val; + int count = 0; vIdBI = Vec_IntAlloc(16); vIdBO = Vec_IntAlloc(16); @@ -5759,6 +5765,7 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, else { Vec_IntSetEntry( vTypeSpec, Gia_ObjId( p1, pObj ), 2 ); + Vec_PtrPush( vBO, pObj ); c2 ++; int j; @@ -5782,6 +5789,37 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, } } + Vec_Int_t* vFlag = Vec_IntAlloc( Gia_ManObjNum(p1) ); + Vec_IntFill( vFlag, Gia_ManObjNum(p1), 0 ); + int id; + int count_node = 0; + + // count nodes + Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i ) + { + Vec_PtrPush( vQ, pObj ); + } + while( Vec_PtrSize(vQ) > 0 ) + { + pObj = Vec_PtrPop(vQ); + id = Gia_ObjId( p1, pObj ); + if ( Vec_IntEntry( vFlag, Gia_ObjId(p1, pObj) ) != 0 ) continue; + Vec_IntSetEntry( vFlag, Gia_ObjId(p1, pObj), 1 ); + count_node ++; + + if ( Vec_IntEntry( vTypeSpec, id ) == 1 ) + { + continue; + } + else + { + if ( Gia_ObjFaninNum(p1, pObj) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) ); + if ( Gia_ObjFaninNum(p1, pObj) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) ); + } + } + printf( "BI: %d, BO: %d, Box Size: %d\n", n, Gia_ManBufNum(p1)-n, count_node ); + + Gia_ManStaticFanoutStop( p1 ); printf( "spec: fanin: %d / fanout: %d / total %d\n", c1, c2, Gia_ManObjNum(p1) ); @@ -5794,13 +5832,13 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); if ( Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) > 0 ) { - if ( Vec_IntGetEntry( vLitBmiter, pObj->Value ) == 3 ) // eq node in impl + if ( Vec_IntGetEntry( vMarkBmiter, pObj->Value >> 1 ) == 3 ) // eq node in impl { - Vec_IntUpdateEntry( vLitBmiter, pObj->Value, 3 + Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) ); + Vec_IntUpdateEntry( vMarkBmiter, pObj->Value >> 1, 3 + Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) ); } else { - Vec_IntUpdateEntry( vLitBmiter, pObj->Value, Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) ); + Vec_IntUpdateEntry( vMarkBmiter, pObj->Value >> 1, Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) ); } } if ( Gia_ObjIsBuf(pObj) ) @@ -5822,9 +5860,8 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int e, c3=0, c4=0, c5=0; c1 = 0; c2 = 0; - Vec_IntForEachEntry( vLitBmiter, e, i ) + Vec_IntForEachEntry( vMarkBmiter, e, i ) { - if ( i%2 ) continue; switch (e) { case 1: c1++; break; @@ -5839,7 +5876,10 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, printf("(strash) impl: eq_fanin: %d / eq_fanout: %d / total: %d\n", c4, c5, c3+c4+c5); Gia_ManForEachCo( p2, pObj, i ) - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + { + int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) << 1; + Vec_IntSetEntry( vMarkBmiter, id, 5 ); + } Gia_ManForEachCo( p1, pObj, i ) Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Vec_IntForEachEntry( vLits, iLit, i ) diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 755aeaea0..dab809c25 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -37921,7 +37921,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500, nMaxNodes = 0; Cec4_ManSetParams( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "OJWRILDCNPMrmdckngxysopwqvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMrmdckngxysopwqvh" ) ) != EOF ) { switch ( c ) { @@ -37969,18 +37969,6 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) if ( pPars->nItersMax < 0 ) goto usage; break; - case 'O': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" ); - goto usage; - } - pPars->nPO = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( pPars->nPO < 1 ) - goto usage; - break; - case 'L': if ( globalUtilOptind >= argc ) { diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index a01cc7445..7377367e2 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -144,7 +144,7 @@ static inline int Cec4_ObjSetSatId( Gia_Man_t * p, Gia_Obj_t * pObj, int Num static inline void Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(Cec4_ObjSatId(p, pObj) != -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), -1); } -extern Vec_Int_t* vLitBmiter; +extern Vec_Int_t* vMarkBmiter; extern Vec_Int_t* vIdBI; extern Vec_Int_t* vIdBO; @@ -1885,25 +1885,25 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p if ( pRepr == NULL ) continue; } - int lit_obj = Gia_ObjId( p, pObj ) << 1; - int lit_repr = Gia_ObjId( p, pRepr ) << 1; + int id_obj = Gia_ObjId( p, pObj ); + int id_repr = Gia_ObjId( p, pRepr ); if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) ) { - printf( "*node %d (%d) merged into node %d (%d)\n", lit_obj >> 1, Vec_IntEntry( vLitBmiter, lit_obj ), lit_repr >> 1, Vec_IntEntry( vLitBmiter, lit_repr) ); + // printf( "*node %d (%d) merged into node %d (%d)\n", id_obj, Vec_IntEntry( vMarkBmiter, id_obj ), id_repr, Vec_IntEntry( vMarkBmiter, id_repr) ); if ( pPars->fBMiterInfo ) { - if ( Vec_IntEntry( vLitBmiter, lit_repr ) == 3 ) + if ( Vec_IntEntry( vMarkBmiter, id_repr ) == 3 ) { - switch ( Vec_IntEntry( vLitBmiter, lit_obj ) ) + switch ( Vec_IntEntry( vMarkBmiter, id_obj ) ) { case 1: case 4: - Vec_IntUpdateEntry( vLitBmiter, lit_repr, 4 ); + Vec_IntUpdateEntry( vMarkBmiter, id_repr, 4 ); break; case 2: case 5: - Vec_IntUpdateEntry( vLitBmiter, lit_repr, 5 ); + Vec_IntUpdateEntry( vMarkBmiter, id_repr, 5 ); break; default: break; @@ -1911,16 +1911,16 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p } else { - if ( Vec_IntEntry(vLitBmiter, lit_obj ) == 3 ) - switch ( Vec_IntEntry( vLitBmiter, lit_repr ) ) + if ( Vec_IntEntry(vMarkBmiter, id_obj ) == 3 ) + switch ( Vec_IntEntry( vMarkBmiter, id_repr ) ) { case 1: case 4: - Vec_IntUpdateEntry( vLitBmiter, lit_obj, 4 ); + Vec_IntUpdateEntry( vMarkBmiter, id_obj, 4 ); break; case 2: case 5: - Vec_IntUpdateEntry( vLitBmiter, lit_obj, 5 ); + Vec_IntUpdateEntry( vMarkBmiter, id_obj, 5 ); break; default: break; @@ -1928,7 +1928,7 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p } } // TODO - Vec_IntSetEntry( vLitBmiter, lit_obj, Vec_IntEntry( vLitBmiter, lit_repr) ); + Vec_IntSetEntry( vMarkBmiter, id_obj, Vec_IntEntry( vMarkBmiter, id_repr) ); } assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) ); Gia_ObjSetProved( p, i ); @@ -1939,18 +1939,18 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) ) { if (pPars->fBMiterInfo){ - printf( "node %d (%d) merged into node %d (%d)\n", lit_obj >> 1, Vec_IntEntry( vLitBmiter, lit_obj ), lit_repr >> 1, Vec_IntEntry( vLitBmiter, lit_repr ) ); - if ( Vec_IntEntry( vLitBmiter, lit_repr ) == 3 ) + // printf( "node %d (%d) merged into node %d (%d)\n", id_obj, Vec_IntEntry( vMarkBmiter, id_obj ), id_repr, Vec_IntEntry( vMarkBmiter, id_repr ) ); + if ( Vec_IntEntry( vMarkBmiter, id_repr ) == 3 ) { - switch ( Vec_IntEntry( vLitBmiter, lit_obj ) ) + switch ( Vec_IntEntry( vMarkBmiter, id_obj ) ) { case 1: case 4: - Vec_IntUpdateEntry( vLitBmiter, lit_repr, 4 ); + Vec_IntUpdateEntry( vMarkBmiter, id_repr, 4 ); break; case 2: case 5: - Vec_IntUpdateEntry( vLitBmiter, lit_repr, 5 ); + Vec_IntUpdateEntry( vMarkBmiter, id_repr, 5 ); break; default: break; @@ -1958,16 +1958,16 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p } else { - if ( Vec_IntEntry(vLitBmiter, lit_obj ) == 3 ) - switch ( Vec_IntEntry( vLitBmiter, lit_repr ) ) + if ( Vec_IntEntry(vMarkBmiter, id_obj ) == 3 ) + switch ( Vec_IntEntry( vMarkBmiter, id_repr ) ) { case 1: case 4: - Vec_IntUpdateEntry( vLitBmiter, lit_obj, 4 ); + Vec_IntUpdateEntry( vMarkBmiter, id_obj, 4 ); break; case 2: case 5: - Vec_IntUpdateEntry( vLitBmiter, lit_obj, 5 ); + Vec_IntUpdateEntry( vMarkBmiter, id_obj, 5 ); break; default: break; @@ -1975,7 +1975,7 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p } } // TODO - Vec_IntSetEntry( vLitBmiter, lit_obj, Vec_IntEntry( vLitBmiter, lit_repr) ); + Vec_IntSetEntry( vMarkBmiter, id_obj, Vec_IntEntry( vMarkBmiter, id_repr) ); } pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase ); } @@ -1986,67 +1986,128 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p { // check bi, bo - Vec_Ptr_t* vBO = Vec_PtrAlloc( 16 ); - Vec_Ptr_t * vQ = Vec_PtrAlloc(16); - + Vec_Ptr_t* vAO = Vec_PtrAlloc( 16 ); // additioal output boundary + Vec_Ptr_t* vAI = Vec_PtrAlloc( 16 ); // additional input boundary + Vec_Ptr_t* vMI = Vec_PtrAlloc(16); // missing input boundary + Vec_Ptr_t* vMO = Vec_PtrAlloc(16); // missing input boundary + Vec_Ptr_t* vQ = Vec_PtrAlloc(16); // queue for fanout traversal int val; + int cnt_TO = 0; + int cnt_TI = 0; + int cnt_SIDE = 0; + int cnt_MI = 0; + int cnt_MO = 0; + Vec_Int_t* vFlag = Vec_IntAlloc( p->nObjs ); + Vec_IntFill( vFlag, p->nObjs, 0 ); + printf("BI:"); Vec_IntForEachEntry( vIdBI, val, i ) { - printf( " %d (%d)", val, Vec_IntEntry( vLitBmiter, val << 1) ); + printf( " %d (%d)", val, Vec_IntEntry( vMarkBmiter, val) ); + if ( Vec_IntEntry( vMarkBmiter, val) <= 3 ) + { + Vec_PtrPush(vMI, &((p->pObjs)[val]) ); + } + else cnt_MI ++; } printf("\nBO:"); Vec_IntForEachEntry( vIdBO, val, i ) { - printf( " %d (%d)", val, Vec_IntEntry( vLitBmiter, val << 1) ); - if ( Vec_IntEntry( vLitBmiter, val << 1) != 5 ) + printf( " %d (%d)", val, Vec_IntEntry( vMarkBmiter, val) ); + if ( Vec_IntEntry( vMarkBmiter, val) <= 3 ) { Vec_PtrPush(vQ, &((p->pObjs)[val]) ); + Vec_PtrPush(vMO, &((p->pObjs)[val]) ); + Vec_IntSetEntry( vFlag, val, 2 ); } + else cnt_MO ++; } printf("\n"); - // find bound + // find extended output boundary Gia_ManStaticFanoutStart( p ); - Vec_Int_t* vFlag = Vec_IntAlloc( p->nObjs ); - Vec_IntFill( vFlag, p->nObjs, 0 ); Gia_Obj_t * pObj2; - int cnt_node = 0; - int cnt_newBo = 0; + cnt_TO -= Vec_PtrSize(vQ); while ( Vec_PtrSize(vQ) != 0 ) { pObj2 = Vec_PtrPop(vQ); - if ( Vec_IntEntry( vFlag, Gia_ObjId(p, pObj2) ) != 0 ) continue; - cnt_node ++; + if ( Vec_IntEntry( vFlag, Gia_ObjId(p, pObj2) ) == 1 ) continue; Vec_IntSetEntry( vFlag, Gia_ObjId(p, pObj2), 1 ); + cnt_TO ++; - val = Vec_IntEntry(vLitBmiter, Gia_ObjId(p, pObj2) << 1); + val = Vec_IntEntry(vMarkBmiter, Gia_ObjId(p, pObj2)); if ( val == 5 || Gia_ObjIsCo( pObj2 ) ) // boundary found { - cnt_newBo ++; - Vec_PtrPush( vBO, pObj2 ); + Vec_PtrPush( vAO, pObj2 ); continue; } for( int j = 0; j < Gia_ObjFanoutNum(p, pObj2); j++ ) { Vec_PtrPush( vQ, Gia_ObjFanout(p, pObj2, j) ); - printf( "add fanout\n"); } } Gia_ManStaticFanoutStop(p); - printf("extended BO with %d extra nodes:", cnt_node); - Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i ) + // find extneded input boundary + + Vec_PtrForEachEntry( Gia_Obj_t*, vMO, pObj, i ) + { + Vec_IntSetEntry( vFlag, Gia_ObjId(p, pObj), 2 ); + } + + int id; + Vec_PtrForEachEntry( Gia_Obj_t*, vMI, pObj, i ) Vec_PtrPush( vQ, pObj ); + Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i ) Vec_PtrPush( vQ, pObj ); + cnt_TI -= Vec_PtrSize(vQ); + while ( Vec_PtrSize(vQ) > 0 ) + { + pObj = Vec_PtrPop(vQ); + id = Gia_ObjId( p, pObj ); + if ( Vec_IntEntry( vFlag, id ) == 2 ) continue; + printf( "backtrace to node %d\n", id ); + if ( Vec_IntEntry(vMarkBmiter, id ) != 2 ) cnt_TI ++; + Vec_IntSetEntry( vFlag, id, 2 ); + + + if ( Vec_IntEntry( vMarkBmiter, id ) >= 3 || Gia_ObjIsCi( pObj ) ) // matched + { + if ( Vec_IntEntry( vMarkBmiter, id ) < 5 || Gia_ObjIsCi( pObj ) ) + { + Vec_PtrPush( vAI, pObj ); + } + continue; + } + else + { + if ( Gia_ObjFaninNum(p, pObj) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) ); + if ( Gia_ObjFaninNum(p, pObj) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) ); + } + } + + + // print result + printf("extended BO with %d extra nodes:", cnt_TO); + Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i ) { printf( " %d", Gia_ObjId(p, pObj) ); } printf("\n"); + + printf("extended BI with %d extra nodes:", cnt_TI); + Vec_PtrForEachEntry( Gia_Obj_t*, vAI, pObj, i ) + { + printf( " %d", Gia_ObjId(p, pObj) ); + } + printf("\n"); + + printf("matched BI: %d / matched BO: %d / AI: %d / AO: %d / Extra nodes: %d\n", cnt_MI, cnt_MO, Vec_PtrSize(vAI), Vec_PtrSize(vAO), cnt_TO + cnt_TI ); + } @@ -2094,7 +2155,7 @@ finalize: Gia_ManRemoveWrongChoices( p ); return p->pCexSeq ? 0 : 1; } -extern Vec_Int_t * vLitBmiter; +extern Vec_Int_t * vMarkBmiter; Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ) { Gia_Man_t * pNew = NULL; @@ -2103,9 +2164,8 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ) // TODO if (pPars -> fBMiterInfo){ int e, i, c1=0, c2=0, c3=0, c4=0, c5=0; - Vec_IntForEachEntry( vLitBmiter, e, i ) + Vec_IntForEachEntry( vMarkBmiter, e, i ) { - if ( i%2 ) continue; switch (e) { case 1: c1++; break; From c74144c6eb75095bfd280022f1e7a3ddca28f7f3 Mon Sep 17 00:00:00 2001 From: Allen Ho Date: Thu, 1 Feb 2024 07:25:46 +0800 Subject: [PATCH 08/11] str_eco ver1 --- src/aig/gia/giaDup.c | 730 ++++++++++++++++++++++++++++++--------- src/base/abci/abc.c | 107 ++++++ src/proof/cec/cecSatG2.c | 295 +++++----------- 3 files changed, 767 insertions(+), 365 deletions(-) diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index aa8f1c053..37b3e8e3b 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -30,9 +30,12 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -Vec_Int_t* vMarkBmiter; -Vec_Int_t* vIdBI; -Vec_Int_t* vIdBO; +Vec_Ptr_t* vBmiter2Spec; +Vec_Ptr_t* vBmiter2Impl; +Vec_Int_t* vPatch2Impl; +Vec_Bit_t* vImpl2Spec_phase; +Vec_Int_t* vBI_patch; +Vec_Int_t* vBO_patch; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -5702,186 +5705,55 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, Gia_ManConst0(p1)->Value = 0; Gia_ManConst0(p2)->Value = 0; - // allocate vMarkBmiter - vMarkBmiter = Vec_IntAlloc( (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) ); - Vec_IntFill( vMarkBmiter, (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)), 0 ); - printf( "allocated size: %d\n", Vec_IntSize(vMarkBmiter) ); + // allocate vImpl2Spec_phase; + vImpl2Spec_phase = Vec_BitAlloc( Gia_ManObjNum(p2) ); + Vec_BitFill( vImpl2Spec_phase, Gia_ManObjNum(p2), 0 ); + + // allocate vBmiter2Impl and vBmiter2Spec + Vec_Int_t* pVec_Int; + vBmiter2Impl = Vec_PtrAlloc( (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) ); + Vec_PtrFill( vBmiter2Impl, (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)), 0 ); + Vec_PtrForEachEntry( Vec_Int_t*, vBmiter2Impl, pVec_Int, i) + { + Vec_PtrSetEntry(vBmiter2Impl, i, Vec_IntAlloc(2) ); + } + vBmiter2Spec = Vec_PtrAlloc( (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) ); + Vec_PtrFill( vBmiter2Spec, (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)), 0 ); + Vec_PtrForEachEntry( Vec_Int_t*, vBmiter2Spec, pVec_Int, i) + { + Vec_PtrSetEntry(vBmiter2Spec, i, Vec_IntAlloc(2) ); + } Gia_ManForEachCi( p1, pObj, i ) { - int id = pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew ); - Vec_IntSetEntry( vMarkBmiter, id >> 1, 4 ); + pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew ); + Vec_IntPush( Vec_PtrEntry(vBmiter2Spec, pObj->Value >> 1), Gia_ObjId(p1, pObj) ); + Vec_IntPush( Vec_PtrEntry(vBmiter2Impl, pObj->Value >> 1), Gia_ObjId(p1, pObj) ); // same pi id in impl and spec } // TODO: record the corresponding impl node of each lit - Gia_ManForEachAnd( p2, pObj, i ) { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Vec_IntUpdateEntry( vMarkBmiter, pObj->Value >> 1, 3 ); + Vec_IntPush( Vec_PtrEntry(vBmiter2Impl, pObj->Value >> 1), Gia_ObjId(p2, pObj) ); } - // TODO: find nodes in spec - - Vec_Int_t * vTypeSpec = Vec_IntAlloc( 16 ); - Vec_IntFill( vTypeSpec, Gia_ManObjNum(p1), 0 ); - int n = Gia_ManBufNum(p1) / 2; - if(biNum > 0){ - n = biNum; - } - - Gia_ManStaticFanoutStart( p1 ); - Vec_Ptr_t * vQ = Vec_PtrAlloc(16); - Vec_Ptr_t * vBO = Vec_PtrAlloc(16); - Gia_Obj_t * pObj2; - int c1 = 0; - int c2 = 0; - int count = 0; - - vIdBI = Vec_IntAlloc(16); - vIdBO = Vec_IntAlloc(16); - - Gia_ManForEachBuf( p1, pObj, i ) - { - if ( count < n ) - { - Vec_IntSetEntry( vTypeSpec, Gia_ObjId( p1, pObj ), 1 ); - c1++; - count ++; - - Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) ); - Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) ); - while ( Vec_PtrSize(vQ) != 0 ) - { - pObj2 = Vec_PtrPop(vQ); - if ( Vec_IntEntry( vTypeSpec, Gia_ObjId(p1, pObj2) ) != 0 ) continue; - c1 ++; - Vec_IntSetEntry( vTypeSpec, Gia_ObjId(p1, pObj2), 1 ); - if ( Gia_ObjFaninNum(p1, pObj2) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj2) ); - if ( Gia_ObjFaninNum(p1, pObj2) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj2) ); - } - - } - else - { - Vec_IntSetEntry( vTypeSpec, Gia_ObjId( p1, pObj ), 2 ); - Vec_PtrPush( vBO, pObj ); - c2 ++; - - int j; - // pObj = Gia_ObjFanin0(pObj); - Gia_ObjForEachFanoutStatic(p1, pObj, pObj2, j) - { - Vec_PtrPush( vQ, pObj2 ); - } - while ( Vec_PtrSize(vQ) != 0 ) - { - pObj2 = Vec_PtrPop(vQ); - if ( Vec_IntEntry( vTypeSpec, Gia_ObjId(p1, pObj2) ) != 0 ) continue; - Vec_IntSetEntry( vTypeSpec, Gia_ObjId(p1, pObj2), 2 ); - c2 ++; - for( int j = 0; j < Gia_ObjFanoutNum(p1, pObj2); j++ ) - { - Vec_PtrPush( vQ, Gia_ObjFanout(p1, pObj2, j) ); - } - } - - } - } - - Vec_Int_t* vFlag = Vec_IntAlloc( Gia_ManObjNum(p1) ); - Vec_IntFill( vFlag, Gia_ManObjNum(p1), 0 ); - int id; - int count_node = 0; - - // count nodes - Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i ) - { - Vec_PtrPush( vQ, pObj ); - } - while( Vec_PtrSize(vQ) > 0 ) - { - pObj = Vec_PtrPop(vQ); - id = Gia_ObjId( p1, pObj ); - if ( Vec_IntEntry( vFlag, Gia_ObjId(p1, pObj) ) != 0 ) continue; - Vec_IntSetEntry( vFlag, Gia_ObjId(p1, pObj), 1 ); - count_node ++; - - if ( Vec_IntEntry( vTypeSpec, id ) == 1 ) - { - continue; - } - else - { - if ( Gia_ObjFaninNum(p1, pObj) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) ); - if ( Gia_ObjFaninNum(p1, pObj) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) ); - } - } - printf( "BI: %d, BO: %d, Box Size: %d\n", n, Gia_ManBufNum(p1)-n, count_node ); - - - Gia_ManStaticFanoutStop( p1 ); - - printf( "spec: fanin: %d / fanout: %d / total %d\n", c1, c2, Gia_ManObjNum(p1) ); - - // TODO: record hashed equivalent nodes - - count = 0; Gia_ManForEachAnd( p1, pObj, i ) { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - if ( Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) > 0 ) - { - if ( Vec_IntGetEntry( vMarkBmiter, pObj->Value >> 1 ) == 3 ) // eq node in impl - { - Vec_IntUpdateEntry( vMarkBmiter, pObj->Value >> 1, 3 + Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) ); - } - else - { - Vec_IntUpdateEntry( vMarkBmiter, pObj->Value >> 1, Vec_IntEntry( vTypeSpec, Gia_ObjId( p1, pObj) ) ); - } - } - if ( Gia_ObjIsBuf(pObj) ) - { - Vec_IntPush( vLits, pObj->Value ); - if ( count < n ) - { - Vec_IntPush( vIdBI, (pObj->Value) >> 1 ); - } - else - { - Vec_IntPush( vIdBO, (pObj->Value) >> 1 ); - } - count ++; - } + Vec_IntPush( Vec_PtrEntry(vBmiter2Spec, pObj->Value >> 1), Gia_ObjId(p1, pObj) ); } - - int e, c3=0, c4=0, c5=0; - c1 = 0; c2 = 0; - - Vec_IntForEachEntry( vMarkBmiter, e, i ) - { - switch (e) - { - case 1: c1++; break; - case 2: c2++; break; - case 3: c3++; break; - case 4: c4++; break; - case 5: c5++; break; - default: - break; - } - } - printf("(strash) impl: eq_fanin: %d / eq_fanout: %d / total: %d\n", c4, c5, c3+c4+c5); - Gia_ManForEachCo( p2, pObj, i ) { - int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) << 1; - Vec_IntSetEntry( vMarkBmiter, id, 5 ); + int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1; + Vec_IntPush( Vec_PtrEntry(vBmiter2Impl, id), Gia_ObjId(p2, pObj) ); } Gia_ManForEachCo( p1, pObj, i ) - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + { + int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1; + Vec_IntPush( Vec_PtrEntry(vBmiter2Spec, id), Gia_ObjId(p1, pObj) ); + } Vec_IntForEachEntry( vLits, iLit, i ) Gia_ManAppendCo( pNew, iLit ); Vec_IntFree( vLits ); @@ -6024,6 +5896,538 @@ Gia_Man_t * Gia_ManMiterFromBMiter( Gia_Man_t * p, int nPo ) return pNew; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManPatch( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum) +{ + Vec_Int_t * vLits; + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, iLit; + if ( Gia_ManBufNum(p1) == 0 ) { + printf( "The first AIG should have a boundary.\n" ); + return NULL; + } + if ( Gia_ManBufNum(p2) == 0 ) { + printf( "The second AIG should have a boundary.\n" ); + return NULL; + } + assert( Gia_ManBufNum(p1) > 0 ); + assert( Gia_ManBufNum(p2) > 0 ); + assert( Gia_ManBufNum(p1) == Gia_ManBufNum(p2) ); + assert( Gia_ManRegNum(p1) == 0 ); + assert( Gia_ManRegNum(p2) == 0 ); + assert( Gia_ManCiNum(p1) == Gia_ManCiNum(p2) ); + assert( Gia_ManCoNum(p1) == Gia_ManCoNum(p2) ); + if ( fVerbose ) + printf( "Mapping spec to patch with %d inputs, %d outputs, and %d buffers.\n", + Gia_ManCiNum(p1), Gia_ManCoNum(p1), Gia_ManBufNum(p1) ); + pNew = Gia_ManStart( Gia_ManObjNum(p2) ); + pNew->pName = ABC_ALLOC( char, strlen(p1->pName) + 10 ); + sprintf( pNew->pName, "%s_patch", p1->pName ); + Gia_ManHashStart( pNew ); + Gia_ManConst0(p1)->Value = 0; + Gia_ManConst0(p2)->Value = 0; + + // add patch aig first + // record lit -> patch id + Vec_Int_t* vVar2Patch = Vec_IntAlloc( Gia_ManObjNum(p2) ); + Vec_IntFill( vVar2Patch, Gia_ManObjNum(p2), -1 ); + + Gia_ManForEachCi( p2, pObj, i ) + { + pObj->Value = Gia_ManCi(p1, i)->Value = Gia_ManAppendCi( pNew ); + Vec_IntSetEntry( vVar2Patch, pObj->Value >> 1, Gia_ObjId( p2, pObj ) ); + } + Gia_ManForEachAnd( p2, pObj, i ) + { + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + printf( "\t%d: %d %d\n", Gia_ObjId( p2, pObj), Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Vec_IntSetEntry( vVar2Patch, pObj->Value >> 1, Gia_ObjId( p2, pObj ) ); + } + + + // alloc vCompl; + Vec_Bit_t * vComplBuf = Vec_BitAlloc(Gia_ManBufNum(p1)); + Vec_Bit_t * vCompl = Vec_BitAlloc(Gia_ManObjNum(p1)); + Vec_BitFill( vCompl, Gia_ManObjNum(p1), 0 ); + Gia_ManForEachBuf( p2, pObj, i ) + { + printf("\tbuf compl %d: %d\n", Gia_ObjId(p2, pObj), Gia_ObjFaninC0(pObj)); + Vec_BitPush( vComplBuf, Gia_ObjFaninC0(pObj) ); + } + int cnt = 0; + Gia_ManForEachBuf( p1, pObj, i ) + { + printf("\tbuf compl %d: %d\n", Gia_ObjId(p1, pObj), Gia_ObjFaninC0(pObj)); + if ( Vec_BitEntry( vComplBuf, cnt ) || Gia_ObjFaninC0(pObj) ) + { + Vec_BitSetEntry( vCompl, Gia_ObjId( p1, pObj ), 1 ); + printf("\tset\n"); + } + cnt++; + } + + + + // mark the box in spec + Vec_Int_t* vFlagSpec = Vec_IntAlloc( Gia_ManObjNum(p1) ); // 1: bi, 2: inside the box, 3: bo + Vec_IntFill( vFlagSpec, Gia_ManObjNum(p1), 0 ); + int cnt_buf = 0; + Gia_ManForEachBuf( p1, pObj, i ) + { + if ( cnt_buf < biNum ) + { + Vec_IntSetEntry( vFlagSpec, Gia_ObjId(p1, Gia_ObjFanin0(pObj) ), 1 ); + } + else + { + Vec_IntSetEntry( vFlagSpec, Gia_ObjId(p1, Gia_ObjFanin0(pObj) ), 3 ); + } + cnt_buf ++; + } + + int fanin0, fanin1; + Gia_ManForEachAnd( p1, pObj, i ) + { + if ( Vec_IntEntry( vFlagSpec, Gia_ObjId(p1, pObj) ) != 0 ) continue ; + fanin0 = Vec_IntEntry( vFlagSpec, Gia_ObjId(p1, Gia_ObjFanin0(pObj) ) ); + fanin1 = Vec_IntEntry( vFlagSpec, Gia_ObjId(p1, Gia_ObjFanin1(pObj) ) ); + if ( fanin0 == 1 || fanin0 == 2 || fanin1 == 1 || fanin1 == 2 ) + Vec_IntSetEntry( vFlagSpec, Gia_ObjId(p1, pObj ), 2 ); + } + + + // compute spec2impl + Vec_Int_t* vSpec2Impl = Vec_IntAlloc( Gia_ManObjNum(p1) ); + Vec_IntFill( vSpec2Impl, Gia_ManObjNum(p1), -1 ); + Vec_Int_t* vSpec, *vImpl; + int j, id; + for ( i = 0; i < Vec_PtrSize( vBmiter2Spec ); i++ ) + { + vSpec = Vec_PtrEntry( vBmiter2Spec, i ); + vImpl = Vec_PtrEntry( vBmiter2Impl, i ); + Vec_IntForEachEntry( vSpec, id, j ) + { + if ( Vec_IntEntry( vSpec2Impl, id ) == -1 && Vec_IntSize( vImpl ) > 0 ) + { + Vec_IntSetEntry( vSpec2Impl, id, Vec_IntEntry( vImpl, 0 ) ); + } + } + } + + // print + // printf("spec 2 impl:\n"); + // Vec_IntForEachEntry( vSpec2Impl, id, i ) + // { + // printf( "\t%d:\t %d\n", i, id ); + // } + + // alloc patch2impl + vPatch2Impl = Vec_IntAlloc( Gia_ManObjNum(p2) ); + Vec_IntFill( vPatch2Impl, Gia_ManObjNum(p2), -1 ); + Vec_IntSetEntry( vPatch2Impl, 0, 0 ); + + Gia_ManForEachCi( p2, pObj, i ) + { + Vec_IntSetEntry( vVar2Patch, pObj->Value >> 1, pObj->Value >> 1); + Vec_IntSetEntry( vPatch2Impl, pObj->Value>>1, Vec_IntEntry( vSpec2Impl, pObj->Value>>1) ); + } + + // set the litral on the boundary of spec as in patch and record patch2impl + Vec_Int_t* vBufLit = Vec_IntAlloc( Gia_ManBufNum( p2 ) ); + vBI_patch = Vec_IntAlloc( Gia_ManBufNum(p2) ); + vBO_patch = Vec_IntAlloc( Gia_ManBufNum(p2) ); + cnt_buf = 0; + Gia_ManForEachBuf( p2, pObj, i ) + { + // TODO: check compl + Vec_IntPush( vBufLit, Gia_ObjFanin0( pObj ) -> Value ); + if ( cnt_buf < biNum ) + { + Vec_IntPush( vBI_patch, Gia_ObjFanin0( pObj) -> Value >> 1 ); + } + else + { + Vec_IntPush( vBO_patch, Gia_ObjFanin0( pObj) -> Value >> 1 ); + } + cnt_buf++; + } + Vec_Int_t* vSpec2Patch = Vec_IntAlloc( Gia_ManObjNum(p1) ); + Vec_IntFill( vSpec2Patch, Gia_ManObjNum(p1), -1 ); + + cnt_buf = 0; + Gia_Obj_t * pObj2; + + Gia_ManForEachBuf( p1, pObj, i ) + { + // TODO: compl? + pObj2 = Gia_ObjFanin0(pObj); + pObj2 -> Value = Vec_IntEntry( vBufLit, cnt_buf ); + Vec_IntSetEntry( vSpec2Patch, Gia_ObjId( p1, pObj2 ), Vec_IntEntry( vVar2Patch, pObj2->Value>>1 ) ); + // printf( "spec node %d -> patch node %d\n", Gia_ObjId( p1, pObj2 ), Vec_IntEntry( vVar2Patch, pObj2->Value>>1 ) ); + + Vec_IntSetEntry( vPatch2Impl, pObj2 -> Value>>1, Vec_IntEntry( vSpec2Impl, Gia_ObjId(p1, pObj2) ) ); + pObj->Value = pObj2->Value; + cnt_buf++; + } + + + // hash the area outside the box in spec and record patch2impl + int lit0, lit1; + Gia_ManForEachAnd( p1, pObj, i ) { + printf( "spec node %d(%d) = %d %d\n", Gia_ObjId( p1, pObj ), Vec_IntEntry( vFlagSpec, Gia_ObjId(p1, pObj)), Gia_ObjId( p1, Gia_ObjFanin0(pObj) ), Gia_ObjId( p1, Gia_ObjFanin1(pObj) ) ); + if ( Vec_IntEntry( vFlagSpec, Gia_ObjId(p1, pObj) ) > 1 ) continue; + if ( Gia_ObjIsBuf(pObj) ) continue; + + lit0 = Gia_ObjFanin0Copy(pObj); + lit1 = Gia_ObjFanin1Copy(pObj); + if ( Vec_BitEntry( vCompl, Gia_ObjId(p1, Gia_ObjFanin0(pObj) ) ) ) lit0 ^= 1; + if ( Vec_BitEntry( vCompl, Gia_ObjId(p1, Gia_ObjFanin1(pObj) ) ) ) lit1 ^= 1; + pObj->Value = Gia_ManHashAnd( pNew, lit0, lit1 ); + + + assert( (pObj->Value>>1) < Vec_IntSize( vVar2Patch) ); + assert( Vec_IntEntry( vVar2Patch, pObj->Value>>1 ) != -1 ); + + Vec_IntSetEntry( vSpec2Patch, Gia_ObjId( p1, pObj ), Vec_IntEntry( vVar2Patch, pObj->Value>>1 ) ); + printf( "spec node %d -> patch node %d\n", Gia_ObjId( p1, pObj ), Vec_IntEntry( vVar2Patch, pObj->Value>>1 ) ); + + Vec_IntSetEntry( vPatch2Impl, pObj->Value >> 1, Vec_IntEntry( vSpec2Impl, Gia_ObjId(p1, pObj) ) ); + } + + + // print + printf("patch 2 impl:\n"); + Vec_IntForEachEntry( vPatch2Impl, id, i ) + { + printf( "\t%d:\t %d\n", i, id ); + } + + // handle co + Gia_ManForEachCo( p2, pObj, i ) + { + int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1; + } + // TODO: also check spec CO + // Gia_ManForEachCo( p1, pObj, i ) + // { + // int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1; + // Vec_IntPush( Vec_PtrEntry(vBmiter2Spec, id), Gia_ObjId(p1, pObj) ); + // } + + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +Gia_Man_t * Gia_ManPatchImpl( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum) +{ + Vec_Int_t * vLits; + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, *pObj2; + int i, j, iLit, id, id2; + assert( Gia_ManRegNum(p1) == 0 ); + assert( Gia_ManRegNum(p2) == 0 ); + assert( Gia_ManCiNum(p1) == Gia_ManCiNum(p2) ); + assert( Gia_ManCoNum(p1) == Gia_ManCoNum(p2) ); + if ( fVerbose ) + printf( "Mapping spec to patch with %d inputs, %d outputs, and %d buffers.\n", + Gia_ManCiNum(p1), Gia_ManCoNum(p1), Gia_ManBufNum(p1) ); + pNew = Gia_ManStart( Gia_ManObjNum(p2) ); + pNew->pName = ABC_ALLOC( char, strlen(p1->pName) + 10 ); + sprintf( pNew->pName, "%s_patch", p1->pName ); + Gia_ManHashStart( pNew ); + Gia_ManConst0(p1)->Value = 0; + Gia_ManConst0(p2)->Value = 0; + + + // p1: patch + // p2: impl + + // compute extended box + + Gia_ManStaticFanoutStart( p1 ); + Vec_Ptr_t* vBO = Vec_PtrAlloc(16); + Vec_Ptr_t* vBI = Vec_PtrAlloc(16); + Vec_Ptr_t* vAO = Vec_PtrAlloc(16); + Vec_Ptr_t* vAI = Vec_PtrAlloc(16); + + + + Vec_Ptr_t* vQ = Vec_PtrAlloc(16); + Vec_Int_t* vFlag = Vec_IntAlloc( Gia_ManObjNum(p1) ); + Vec_IntFill( vFlag, Gia_ManObjNum(p1), 0 ); + Vec_IntForEachEntry( vBO_patch, id, i ) + { + if ( Vec_IntEntry( vPatch2Impl, id ) == -1 ) // if no match on the boundary + Vec_PtrPush( vQ, p1->pObjs+id ); + else + Vec_PtrPush( vBO, p1->pObjs+id ); + } + + while( Vec_PtrSize(vQ) > 0 ) + { + pObj = Vec_PtrPop(vQ); + id = Gia_ObjId( p1, pObj ); + + if ( Vec_IntEntry( vFlag, id ) == 1 ) continue; + Vec_IntSetEntry( vFlag, id, 1 ); + + printf("%d\n", id); + + if ( Vec_IntEntry( vPatch2Impl, id ) != -1 ) // matched + { + Vec_PtrPush( vAO, pObj ); + } + else + { + for( j = 0; j < Gia_ObjFanoutNum(p1, pObj); j++ ) + { + Vec_PtrPush( vQ, Gia_ObjFanout(p1, pObj, j) ); + printf("\t%d\n", Gia_ObjId( p1, Gia_ObjFanout(p1, pObj, j) ) ); + } + + } + } + + // set flag 2 for FOC + Vec_IntForEachEntry( vBO_patch, id, i ) + { + Vec_PtrPush( vQ, p1->pObjs+id ); + } + while( Vec_PtrSize(vQ) > 0 ) + { + pObj = Vec_PtrPop(vQ); + id = Gia_ObjId( p1, pObj ); + + if ( Vec_IntEntry( vFlag, Gia_ObjId(p1, pObj) ) == 2 ) continue; + Vec_IntSetEntry( vFlag, Gia_ObjId(p1, pObj), 2 ); + + for( j = 0; j < Gia_ObjFanoutNum(p1, pObj); j++ ) + { + Vec_PtrPush( vQ, Gia_ObjFanout(p1, pObj, j) ); + } + } + + // set flag 3 for BO + Vec_IntForEachEntry( vBO_patch, id, i ) + { + Vec_IntSetEntry( vFlag, id, 3 ); + } + + // traverse down from unmated BI and AO + Vec_IntForEachEntry( vBI_patch, id, i ) + { + if ( Vec_IntEntry( vPatch2Impl, id ) == -1 ) // if no match on the boundary + Vec_PtrPush( vQ, p1->pObjs+id ); + else + Vec_PtrPush( vBI, p1->pObjs+id ); + } + Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i ) + { + Vec_PtrPush( vQ, pObj ); + } + + // traverse down + printf("traverse down\n"); + while ( Vec_PtrSize(vQ) != 0 ) + { + pObj = Vec_PtrPop(vQ); + id = Gia_ObjId( p1, pObj ); + if ( Vec_IntEntry( vFlag, id ) == 4 ) continue; + + printf("%d\n", id); + + if ( Vec_IntEntry( vPatch2Impl, id ) != -1 && Vec_IntEntry( vFlag, id ) < 2 ) // matched + { + Vec_PtrPush( vAI, pObj ); + printf("matched\n"); + } + else if ( Vec_IntEntry( vFlag, id ) < 3 ) + { + if ( Gia_ObjFaninNum(p1, pObj) > 0 ) + { + Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) ); + printf("\t%d\n", Gia_ObjId( p1, Gia_ObjFanin0(pObj) ) ); + } + + if ( Gia_ObjFaninNum(p1, pObj) > 1 ) + { + Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) ); + printf("\t%d\n", Gia_ObjId( p1, Gia_ObjFanin1(pObj) ) ); + } + } + printf("2impl / flag: %d / %d\n", Vec_IntEntry( vPatch2Impl, id ), Vec_IntEntry( vFlag, id ) ); + + Vec_IntSetEntry( vFlag, id, 4 ); + } + + + // print + printf( "matched BI:"); + Vec_PtrForEachEntry( Gia_Obj_t*, vBI, pObj, i ) printf( " %d(%d)", Gia_ObjId( p1, pObj ), Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj)) ); + printf("\nAI:"); + Vec_PtrForEachEntry( Gia_Obj_t*, vAI, pObj, i ) printf( " %d(%d)", Gia_ObjId( p1, pObj ), Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj)) ); + printf("\nmateched BO:"); + Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i ) printf( " %d(%d)", Gia_ObjId( p1, pObj ), Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj)) ); + printf("\nAO:"); + Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i ) printf( " %d(%d)", Gia_ObjId( p1, pObj ), Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj)) ); + printf("\n"); + + // create patched impl + + // mark fanin cone of Extended Input in impl + Vec_Int_t* vFlag_impl = Vec_IntAlloc( Gia_ManObjNum(p2) ); + Vec_IntFill( vFlag_impl, Gia_ManObjNum(p2), 0 ); + + Vec_PtrForEachEntry( Gia_Obj_t*, vBI, pObj, i ) + { + Vec_PtrPush( vQ, p2->pObjs + Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj) ) ); + } + Vec_PtrForEachEntry( Gia_Obj_t*, vAI, pObj, i ) + { + Vec_PtrPush( vQ, p2->pObjs + Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj) ) ); + } + + while ( Vec_PtrSize(vQ) != 0 ) + { + pObj = Vec_PtrPop(vQ); + id = Gia_ObjId( p2, pObj ); + if ( Vec_IntEntry( vFlag_impl, id ) == 1 ) continue; + Vec_IntSetEntry( vFlag_impl, id, 1 ); + + if ( Gia_ObjFaninNum(p2, pObj) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) ); + if ( Gia_ObjFaninNum(p2, pObj) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) ); + } + + // add pi + Gia_ManForEachCi( p2, pObj, i ) + { + pObj->Value = Gia_ManCi(p1, i)->Value = Gia_ManAppendCi( pNew ); + } + // add fanin cone of EI in impl + int cnt = 0; + Gia_ManForEachAnd( p2, pObj, i ) + { + if ( Vec_IntEntry( vFlag_impl, Gia_ObjId(p2, pObj) ) == 0 ) continue; + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + printf( "%d\n", pObj->Value>>1 ); + cnt ++; + } + printf( "%d node added in the fanin cone of EI\n", cnt ); + // set literal and flag of EI in patch + // TODO: input phase + Vec_PtrForEachEntry( Gia_Obj_t*, vBI, pObj, i ) + { + id = Gia_ObjId( p1, pObj ); + pObj -> Value = ( p2 -> pObjs + Vec_IntEntry( vPatch2Impl, id ) ) -> Value; + Vec_IntSetEntry( vFlag, id, 5 ); + } + Vec_PtrForEachEntry( Gia_Obj_t*, vAI, pObj, i ) + { + id = Gia_ObjId( p1, pObj ); + pObj -> Value = ( p2 -> pObjs + Vec_IntEntry( vPatch2Impl, id ) ) -> Value; + Vec_IntSetEntry( vFlag, id, 5 ); + } + // mark fanin cone of EO in patch (to flag 5) + Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i ) + Vec_PtrPush( vQ, pObj ); + Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i ) + Vec_PtrPush( vQ, pObj ); + while ( Vec_PtrSize(vQ) != 0 ) + { + pObj = Vec_PtrPop(vQ); + id = Gia_ObjId( p1, pObj ); + if ( Vec_IntEntry( vFlag, id ) >= 5 ) continue; + Vec_IntSetEntry( vFlag, id, 6 ); + + if ( Gia_ObjFaninNum(p1, pObj) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) ); + if ( Gia_ObjFaninNum(p1, pObj) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) ); + } + // add fanin cone of EO to EI in patch + cnt = 0; + Gia_ManForEachAnd( p1, pObj, i ) + { + if ( Vec_IntEntry( vFlag, Gia_ObjId(p1, pObj) ) != 6 ) continue; + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + printf( "%d\n", pObj->Value>>1 ); + cnt ++; + } + printf( "%d node added in the extended boundary\n", cnt ); + + // set literal and flag(1) of EO in impl + Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i ) + { + id = Gia_ObjId( p1, pObj ); + id2 = Vec_IntEntry( vPatch2Impl, id ); + pObj2 = p2 -> pObjs + id2; + pObj2 -> Value = pObj -> Value; + if ( Vec_BitEntry( vImpl2Spec_phase, id2 ) ) pObj2 -> Value ^= 1; + Vec_IntSetEntry( vFlag_impl, id2, 1 ); + } + Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i ) + { + id = Gia_ObjId( p1, pObj ); + id2 = Vec_IntEntry( vPatch2Impl, id ); + pObj2 = p2 -> pObjs + id2; + pObj2 -> Value = pObj -> Value; + printf( "id %d matched to id %d in impl, phase %d\n", id, id2, Vec_BitEntry( vImpl2Spec_phase, id2 ) ); + if ( Vec_BitEntry( vImpl2Spec_phase, id2 ) ) pObj2 -> Value ^= 1; + Vec_IntSetEntry( vFlag_impl, id2, 1 ); + } + + // add flag 0 in impl + cnt = 0; + Gia_ManForEachAnd( p2, pObj, i ) + { + if ( Vec_IntEntry( vFlag_impl, Gia_ObjId(p2, pObj) ) != 0 ) continue; + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + printf( "%d\n", pObj->Value>>1 ); + cnt++; + } + printf( "%d node added in the fanout cone\n", cnt ); + + // handle co + cnt = 0; + Gia_ManForEachCo( p2, pObj, i ) + { + id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1; + printf( "%d\n", id ); + cnt ++; + } + + Gia_ManStaticFanoutStop( p1 ); + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index dab809c25..1a837d030 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -598,6 +598,7 @@ static int Abc_CommandAbc9AddFlop ( Abc_Frame_t * pAbc, int argc, cha 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_CommandAbc9RecoverBoundary ( 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 ); @@ -1378,6 +1379,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&bmiter", Abc_CommandAbc9BMiter, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gen_hie", Abc_CommandAbc9GenHie, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&rb", Abc_CommandAbc9RecoverBoundary, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&str_eco", Abc_CommandAbc9StrEco, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); { @@ -51953,6 +51955,111 @@ usage: return 1; } +int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Gia_ManPatch( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum); + extern Gia_Man_t * Gia_ManPatchImpl( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum); + Gia_Man_t * pTemp, * pSecond, *pImpl, *pPatched; + char * FileName = NULL; + char * FileName2 = NULL; + FILE * pFile = NULL; + int c, fVerbose = 0; + int bi = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF ) + { + switch ( c ) + { + case 'I': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); + goto usage; + } + bi = atoi(argv[globalUtilOptind++]); + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9StrEco(): There is no AIG.\n" ); + return 0; + } + if ( argc != globalUtilOptind + 2 ) + { + printf("%d\n", argc-globalUtilOptind); + Abc_Print( -1, "Abc_CommandAbc9StrEco(): AIG should be given on the command line.\n" ); + return 0; + } + + // get the input file name + 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 ); + + // get the input file name 2 + FileName2 = argv[globalUtilOptind+1]; + if ( (pFile = fopen( FileName2, "r" )) == NULL ) + { + Abc_Print( -1, "Cannot open input file \"%s\". ", FileName2 ); + if ( (FileName2 = Extra_FileGetSimilarName( FileName2, ".aig", ".blif", ".pla", ".eqn", ".bench" )) ) + Abc_Print( 1, "Did you mean \"%s\"?", FileName2 ); + Abc_Print( 1, "\n" ); + return 1; + } + fclose( pFile ); + + // map spec to patch + pSecond = Gia_AigerRead( FileName, 0, 1, 0 ); + if ( pSecond == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9StrEco(): Cannot read the file name on the command line.\n" ); + return 0; + } + pTemp = Gia_ManPatch( pAbc->pGia, pSecond, fVerbose, bi); + // Gia_ManStop( pSecond ); + // Abc_FrameUpdateGia( pAbc, pTemp ); + // return 0; + + // generated patched impl + pImpl = Gia_AigerRead( FileName2, 0, 0, 0 ); + if ( pImpl == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9StrEco(): Cannot read the file name on the command line.\n" ); + return 0; + } + pPatched = Gia_ManPatchImpl( pTemp, pImpl, fVerbose, bi); + + Gia_ManStop( pSecond ); + Gia_ManStop( pImpl ); + Gia_ManStop( pTemp ); + Abc_FrameUpdateGia( pAbc, pPatched ); + return 0; + +usage: + Abc_Print( -2, "usage: &str_eco -I [-vh] \n" ); + Abc_Print( -2, "\t creates the boundary miter\n" ); + Abc_Print( -2, "\t-I : number of boundary inputs\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 file\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 7377367e2..0659b3f60 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -147,6 +147,8 @@ static inline void Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) extern Vec_Int_t* vMarkBmiter; extern Vec_Int_t* vIdBI; extern Vec_Int_t* vIdBO; +extern Vec_Ptr_t* vBmiter2Spec; +extern Vec_Ptr_t* vBmiter2Impl; //////////////////////////////////////////////////////////////////////// @@ -1788,6 +1790,8 @@ void Gia_ManRemoveWrongChoices( Gia_Man_t * p ) } //Abc_Print( 1, "Removed %d wrong choices.\n", Counter ); } + +extern Vec_Bit_t* vImpl2Spec_phase; int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** ppNew, int fSimOnly ) { Cec4_Man_t * pMan = Cec4_ManCreate( p, pPars ); @@ -1890,45 +1894,24 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) ) { - // printf( "*node %d (%d) merged into node %d (%d)\n", id_obj, Vec_IntEntry( vMarkBmiter, id_obj ), id_repr, Vec_IntEntry( vMarkBmiter, id_repr) ); if ( pPars->fBMiterInfo ) { - if ( Vec_IntEntry( vMarkBmiter, id_repr ) == 3 ) + int eId, j; + Vec_Int_t *vIds_spec_repr, *vIds_impl_repr, *vIds_spec_obj, *vIds_impl_obj; + vIds_spec_repr = Vec_PtrEntry( vBmiter2Spec, id_repr ); + vIds_impl_repr = Vec_PtrEntry( vBmiter2Impl, id_repr ); + vIds_spec_obj = Vec_PtrEntry( vBmiter2Spec, id_obj ); + vIds_impl_obj = Vec_PtrEntry( vBmiter2Impl, id_obj ); + Vec_IntForEachEntry( vIds_spec_obj, eId, j) { - switch ( Vec_IntEntry( vMarkBmiter, id_obj ) ) - { - case 1: - case 4: - Vec_IntUpdateEntry( vMarkBmiter, id_repr, 4 ); - break; - case 2: - case 5: - Vec_IntUpdateEntry( vMarkBmiter, id_repr, 5 ); - break; - default: - break; - } + Vec_IntPush(vIds_spec_repr, eId); } - else + Vec_IntForEachEntry( vIds_impl_obj, eId, j) { - if ( Vec_IntEntry(vMarkBmiter, id_obj ) == 3 ) - switch ( Vec_IntEntry( vMarkBmiter, id_repr ) ) - { - case 1: - case 4: - Vec_IntUpdateEntry( vMarkBmiter, id_obj, 4 ); - break; - case 2: - case 5: - Vec_IntUpdateEntry( vMarkBmiter, id_obj, 5 ); - break; - default: - break; - - } + Vec_IntPush(vIds_impl_repr, eId); } - // TODO - Vec_IntSetEntry( vMarkBmiter, id_obj, Vec_IntEntry( vMarkBmiter, id_repr) ); + Vec_IntClear(vIds_spec_obj); + Vec_IntClear(vIds_impl_obj); } assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) ); Gia_ObjSetProved( p, i ); @@ -1939,178 +1922,101 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p if ( Cec4_ManSweepNode(pMan, i, Gia_ObjId(p, pRepr)) && Gia_ObjProved(p, i) ) { if (pPars->fBMiterInfo){ - // printf( "node %d (%d) merged into node %d (%d)\n", id_obj, Vec_IntEntry( vMarkBmiter, id_obj ), id_repr, Vec_IntEntry( vMarkBmiter, id_repr ) ); - if ( Vec_IntEntry( vMarkBmiter, id_repr ) == 3 ) + + int eId, j; + Vec_Int_t *vIds_spec_repr, *vIds_impl_repr, *vIds_spec_obj, *vIds_impl_obj; + vIds_spec_repr = Vec_PtrEntry( vBmiter2Spec, id_repr ); + vIds_impl_repr = Vec_PtrEntry( vBmiter2Impl, id_repr ); + vIds_spec_obj = Vec_PtrEntry( vBmiter2Spec, id_obj ); + vIds_impl_obj = Vec_PtrEntry( vBmiter2Impl, id_obj ); + + Vec_IntForEachEntry( vIds_spec_obj, eId, j) { - switch ( Vec_IntEntry( vMarkBmiter, id_obj ) ) + Vec_IntPush(vIds_spec_repr, eId); + } + Vec_IntForEachEntry( vIds_impl_obj, eId, j) + { + Vec_IntPush(vIds_impl_repr, eId); + } + + // handle phase before cleaning + printf( "proven %d merged into %d (phase : %d)\n", Gia_ObjId(p, pObj), Gia_ObjId(p,pRepr), pObj->fPhase ^ pRepr -> fPhase ); + if ( Vec_IntSize(vIds_spec_repr) == 0 ) // no match + { + if ( pObj->fPhase ^ pRepr -> fPhase ) { - case 1: - case 4: - Vec_IntUpdateEntry( vMarkBmiter, id_repr, 4 ); - break; - case 2: - case 5: - Vec_IntUpdateEntry( vMarkBmiter, id_repr, 5 ); - break; - default: - break; + Vec_IntForEachEntry( vIds_impl_obj, eId, j ) + { + Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) ); + printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) ); + } } } - else + else if ( Vec_IntSize( vIds_spec_repr ) == Vec_IntSize( vIds_spec_obj) && Vec_IntSize( vIds_impl_obj ) == 0 ) // new match { - if ( Vec_IntEntry(vMarkBmiter, id_obj ) == 3 ) - switch ( Vec_IntEntry( vMarkBmiter, id_repr ) ) + if ( pObj->fPhase ^ pRepr -> fPhase ) + { + Vec_IntForEachEntry( vIds_impl_repr, eId, j ) { - case 1: - case 4: - Vec_IntUpdateEntry( vMarkBmiter, id_obj, 4 ); - break; - case 2: - case 5: - Vec_IntUpdateEntry( vMarkBmiter, id_obj, 5 ); - break; - default: - break; - + Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) ); + printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) ); } + printf("new match flip\n"); + } } - // TODO - Vec_IntSetEntry( vMarkBmiter, id_obj, Vec_IntEntry( vMarkBmiter, id_repr) ); + else if ( Vec_IntSize( vIds_spec_repr ) > 0 && Vec_IntSize( vIds_impl_obj ) > 0 ) // matched, merge impl + { + if ( ( pObj->fPhase ^ pRepr -> fPhase) ^ ( Vec_BitEntry( vImpl2Spec_phase, Vec_IntEntry(vIds_impl_repr, 0)) ^ Vec_BitEntry( vImpl2Spec_phase, Vec_IntEntry(vIds_impl_obj, 0)) ) ) + { + if ( Vec_IntSize( vIds_spec_repr ) == Vec_IntSize( vIds_spec_obj) ) // unmatched repr, matched obj, set repr bits + { + Vec_IntForEachEntry( vIds_impl_repr, eId, j ) + { + if ( j >= Vec_IntSize( vIds_impl_repr)-Vec_IntSize(vIds_impl_obj) ) break; + Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) ); + printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) ); + } + } + else // set obj bits + { + Vec_IntForEachEntry( vIds_impl_obj, eId, j ) + { + Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) ); + printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) ); + } + } + } + } + + Vec_IntClear(vIds_spec_obj); + Vec_IntClear(vIds_impl_obj); + } pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase ); + + } } - if ( pPars->fBMiterInfo ) { - - // check bi, bo - Vec_Ptr_t* vAO = Vec_PtrAlloc( 16 ); // additioal output boundary - Vec_Ptr_t* vAI = Vec_PtrAlloc( 16 ); // additional input boundary - Vec_Ptr_t* vMI = Vec_PtrAlloc(16); // missing input boundary - Vec_Ptr_t* vMO = Vec_PtrAlloc(16); // missing input boundary - Vec_Ptr_t* vQ = Vec_PtrAlloc(16); // queue for fanout traversal - int val; - int cnt_TO = 0; - int cnt_TI = 0; - int cnt_SIDE = 0; - int cnt_MI = 0; - int cnt_MO = 0; - Vec_Int_t* vFlag = Vec_IntAlloc( p->nObjs ); - Vec_IntFill( vFlag, p->nObjs, 0 ); - - printf("BI:"); - Vec_IntForEachEntry( vIdBI, val, i ) + // print + Vec_Int_t* vIds_spec, *vIds_impl; + int k, id; + for( int j=0; j < Vec_PtrSize(vBmiter2Spec); j++ ) { - printf( " %d (%d)", val, Vec_IntEntry( vMarkBmiter, val) ); - if ( Vec_IntEntry( vMarkBmiter, val) <= 3 ) - { - Vec_PtrPush(vMI, &((p->pObjs)[val]) ); - } - else cnt_MI ++; + printf("node %d: ", j); + vIds_spec = Vec_PtrEntry( vBmiter2Spec, j); + vIds_impl = Vec_PtrEntry( vBmiter2Impl, j); + Vec_IntForEachEntry(vIds_spec, id, k) + printf("%d ", id); + printf("| "); + Vec_IntForEachEntry(vIds_impl, id, k) + printf("%d ", id); + printf("\n"); } - printf("\nBO:"); - Vec_IntForEachEntry( vIdBO, val, i ) - { - printf( " %d (%d)", val, Vec_IntEntry( vMarkBmiter, val) ); - if ( Vec_IntEntry( vMarkBmiter, val) <= 3 ) - { - Vec_PtrPush(vQ, &((p->pObjs)[val]) ); - Vec_PtrPush(vMO, &((p->pObjs)[val]) ); - Vec_IntSetEntry( vFlag, val, 2 ); - } - else cnt_MO ++; - } - printf("\n"); - - // find extended output boundary - - Gia_ManStaticFanoutStart( p ); - - Gia_Obj_t * pObj2; - cnt_TO -= Vec_PtrSize(vQ); - - while ( Vec_PtrSize(vQ) != 0 ) - { - pObj2 = Vec_PtrPop(vQ); - if ( Vec_IntEntry( vFlag, Gia_ObjId(p, pObj2) ) == 1 ) continue; - Vec_IntSetEntry( vFlag, Gia_ObjId(p, pObj2), 1 ); - cnt_TO ++; - - val = Vec_IntEntry(vMarkBmiter, Gia_ObjId(p, pObj2)); - if ( val == 5 || Gia_ObjIsCo( pObj2 ) ) // boundary found - { - Vec_PtrPush( vAO, pObj2 ); - continue; - } - - for( int j = 0; j < Gia_ObjFanoutNum(p, pObj2); j++ ) - { - Vec_PtrPush( vQ, Gia_ObjFanout(p, pObj2, j) ); - } - } - - Gia_ManStaticFanoutStop(p); - - - // find extneded input boundary - - Vec_PtrForEachEntry( Gia_Obj_t*, vMO, pObj, i ) - { - Vec_IntSetEntry( vFlag, Gia_ObjId(p, pObj), 2 ); - } - - int id; - Vec_PtrForEachEntry( Gia_Obj_t*, vMI, pObj, i ) Vec_PtrPush( vQ, pObj ); - Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i ) Vec_PtrPush( vQ, pObj ); - cnt_TI -= Vec_PtrSize(vQ); - while ( Vec_PtrSize(vQ) > 0 ) - { - pObj = Vec_PtrPop(vQ); - id = Gia_ObjId( p, pObj ); - if ( Vec_IntEntry( vFlag, id ) == 2 ) continue; - printf( "backtrace to node %d\n", id ); - if ( Vec_IntEntry(vMarkBmiter, id ) != 2 ) cnt_TI ++; - Vec_IntSetEntry( vFlag, id, 2 ); - - - if ( Vec_IntEntry( vMarkBmiter, id ) >= 3 || Gia_ObjIsCi( pObj ) ) // matched - { - if ( Vec_IntEntry( vMarkBmiter, id ) < 5 || Gia_ObjIsCi( pObj ) ) - { - Vec_PtrPush( vAI, pObj ); - } - continue; - } - else - { - if ( Gia_ObjFaninNum(p, pObj) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) ); - if ( Gia_ObjFaninNum(p, pObj) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) ); - } - } - - - // print result - printf("extended BO with %d extra nodes:", cnt_TO); - Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i ) - { - printf( " %d", Gia_ObjId(p, pObj) ); - } - printf("\n"); - - printf("extended BI with %d extra nodes:", cnt_TI); - Vec_PtrForEachEntry( Gia_Obj_t*, vAI, pObj, i ) - { - printf( " %d", Gia_ObjId(p, pObj) ); - } - printf("\n"); - - printf("matched BI: %d / matched BO: %d / AI: %d / AO: %d / Extra nodes: %d\n", cnt_MI, cnt_MO, Vec_PtrSize(vAI), Vec_PtrSize(vAO), cnt_TO + cnt_TI ); - } - if ( p->iPatsPi > 0 ) { abctime clk2 = Abc_Clock(); @@ -2155,7 +2061,6 @@ finalize: Gia_ManRemoveWrongChoices( p ); return p->pCexSeq ? 0 : 1; } -extern Vec_Int_t * vMarkBmiter; Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ) { Gia_Man_t * pNew = NULL; @@ -2163,22 +2068,8 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ) // TODO if (pPars -> fBMiterInfo){ - int e, i, c1=0, c2=0, c3=0, c4=0, c5=0; - Vec_IntForEachEntry( vMarkBmiter, e, i ) - { - switch (e) - { - case 1: c1++; break; - case 2: c2++; break; - case 3: c3++; break; - case 4: c4++; break; - case 5: c5++; break; - default: - break; - } - } - printf("(fraig) impl: eq_fanin: %d / eq_fanout: %d / total: %d\n", c4, c5, c3+c4+c5); } + return pNew; } void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose ) From 6f5656c18837f86f2a9e18fe35046fb7ee306c9f Mon Sep 17 00:00:00 2001 From: Allen Ho Date: Fri, 1 Mar 2024 16:05:41 +0800 Subject: [PATCH 09/11] shared EI/EO not handled yet --- src/aig/gia/gia.h | 23 + src/aig/gia/giaBound.c | 1043 ++++++++++++++++++++++++++++++++++++++ src/aig/gia/giaDup.c | 600 +--------------------- src/aig/gia/module.make | 3 +- src/base/abci/abc.c | 168 ++++-- src/misc/vec/vecBit.h | 21 + src/proof/cec/cecSatG2.c | 119 +---- 7 files changed, 1240 insertions(+), 737 deletions(-) create mode 100644 src/aig/gia/giaBound.c diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index dab6770bb..cbd2b9484 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1789,6 +1789,29 @@ extern void Tas_ManSatPrintStats( Tas_Man_t * p ); extern int Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 ); 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 void Bnd_ManStop(); +//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 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 void Bnd_ManSetEqOut( int eq ); +extern void Bnd_ManSetEqRes( int eq ); +extern void Bnd_ManPrintStats(); + +// util +extern 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 ); + ABC_NAMESPACE_HEADER_END diff --git a/src/aig/gia/giaBound.c b/src/aig/gia/giaBound.c new file mode 100644 index 000000000..63b2c389b --- /dev/null +++ b/src/aig/gia/giaBound.c @@ -0,0 +1,1043 @@ +#include "gia.h" +#include "misc/tim/tim.h" +#include "misc/vec/vecWec.h" +#include "proof/cec/cec.h" + + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +typedef struct Bnd_Man_t_ Bnd_Man_t; + +struct Bnd_Man_t_ +{ + int nBI; + int nBO; + int nBI_miss; + int nBO_miss; + int nInternal; + int nExtra; + int nMerged_spec; + int nMerged_impl; + + int nNode_spec; + int nNode_impl; + int nNode_patch; + int nNode_patched; + + int status; // 0: init 1: boundary found 2: out generated 3: patched generated + + int combLoop_spec; + int combLoop_impl; + int eq_out; + int eq_res; + int nChoice; + + Vec_Ptr_t* vBmiter2Spec; + Vec_Ptr_t* vBmiter2Impl; + Vec_Int_t* vSpec2Impl; + Vec_Bit_t* vSpec2Impl_phase; + + Vec_Int_t* vBI; + Vec_Int_t* vBO; + Vec_Int_t* vEI_spec; + Vec_Int_t* vEO_spec; + Vec_Int_t* vEI_impl; + Vec_Int_t* vEO_impl; + Vec_Bit_t* vEI_phase; + Vec_Bit_t* vEO_phase; + + Vec_Int_t* vSpec2Impl_diff; + +}; + +Bnd_Man_t* pBnd; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +void Bnd_ManSetEqOut( int eq ) { pBnd -> eq_out = eq;} +void Bnd_ManSetEqRes( int eq ) { pBnd -> eq_res = eq;} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl ) +{ + 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 ); + 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 -> vBI = Vec_IntAlloc(16); + p -> vBO = Vec_IntAlloc(16); + p -> vEI_spec = Vec_IntAlloc(16); + p -> vEO_spec = Vec_IntAlloc(16); + p -> vEI_impl = Vec_IntAlloc(16); + p -> vEO_impl = Vec_IntAlloc(16); + p -> vEI_phase = Vec_BitAlloc(16); + p -> vEO_phase = Vec_BitAlloc(16); + + p -> nNode_spec = Gia_ManAndNum(pSpec) - Gia_ManBufNum(pSpec); + p -> nNode_impl = Gia_ManAndNum(pImpl); + p -> nNode_patch = 0; + p -> nNode_patched = 0; + + p -> status = 0; + p -> combLoop_spec = 0; + p -> combLoop_impl = 0; + p -> eq_out = 0; + p -> eq_res = 0; + + p -> nChoice = 0; + + p -> vSpec2Impl_diff = Vec_IntAlloc( Gia_ManObjNum(pSpec) ); + Vec_IntFill( p -> vSpec2Impl_diff, Gia_ManObjNum(pSpec), 0 ); + + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bnd_ManStop() +{ + assert(pBnd); + + Vec_PtrFree( pBnd-> vBmiter2Spec ); + Vec_PtrFree( pBnd-> vBmiter2Impl ); + Vec_IntFree( pBnd-> vSpec2Impl ); + Vec_BitFree( pBnd-> vSpec2Impl_phase ); + + Vec_IntFree( pBnd->vBI ); + Vec_IntFree( pBnd->vBO ); + Vec_IntFree( pBnd->vEI_spec ); + Vec_IntFree( pBnd->vEO_spec ); + Vec_IntFree( pBnd->vEI_impl ); + Vec_IntFree( pBnd->vEO_impl ); + Vec_BitFree( pBnd->vEI_phase ); + Vec_BitFree( pBnd->vEO_phase ); + + Vec_IntFree( pBnd-> vSpec2Impl_diff ); + + ABC_FREE( pBnd ); +} + + +void Bnd_ManMap( int iLit, int id, int spec ) +{ + + if ( spec ) + { + Vec_IntPush( Vec_PtrEntry( pBnd -> vBmiter2Spec, iLit >> 1), id ); + Vec_BitSetEntry( pBnd -> vSpec2Impl_phase, id, iLit & 1 ); + } + else + { + assert( (iLit & 1) == 0 ); + Vec_IntPush( Vec_PtrEntry( pBnd -> vBmiter2Impl, iLit >> 1), id ); + } +} + +void Bnd_ManMerge( int id_repr, int id_obj, int phaseDiff ) +{ + + + Vec_Ptr_t* vBmiter2Spec = pBnd -> vBmiter2Spec; + Vec_Ptr_t* vBmiter2Impl = pBnd -> vBmiter2Impl; + Vec_Bit_t* vSpec2Impl_phase = pBnd -> vSpec2Impl_phase; + int id, i; + + Vec_Int_t *vIds_spec_repr, *vIds_impl_repr, *vIds_spec_obj, *vIds_impl_obj; + + vIds_spec_repr = Vec_PtrEntry( vBmiter2Spec, id_repr ); + vIds_impl_repr = Vec_PtrEntry( vBmiter2Impl, id_repr ); + vIds_spec_obj = Vec_PtrEntry( vBmiter2Spec, id_obj ); + vIds_impl_obj = Vec_PtrEntry( vBmiter2Impl, id_obj ); + + Vec_IntForEachEntry( vIds_spec_obj, id, i ) + { + Vec_IntPush(vIds_spec_repr, id); + } + Vec_IntForEachEntry( vIds_impl_obj, id, i ) + { + Vec_IntPush(vIds_impl_repr, id); + } + + // handle spec2impl phase + if ( phaseDiff ) + { + Vec_IntForEachEntry( vIds_spec_obj, id, i ) + { + Vec_BitSetEntry( vSpec2Impl_phase, id, !Vec_BitEntry(vSpec2Impl_phase, id) ); + // printf( "spec id %d's phase set to %d\n", id, Vec_BitEntry(vSpec2Impl_phase, id) ); + } + } + + // handle impl2spec phase + /* + if ( Vec_IntSize(vIds_spec_repr) == 0 ) // no match + { + if ( pObj->fPhase ^ pRepr -> fPhase ) + { + Vec_IntForEachEntry( vIds_impl_obj, eId, j ) + { + Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) ); + printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) ); + } + } + } + else if ( Vec_IntSize( vIds_spec_repr ) == Vec_IntSize( vIds_spec_obj) && Vec_IntSize( vIds_impl_obj ) == 0 ) // new match + { + if ( pObj->fPhase ^ pRepr -> fPhase ) + { + Vec_IntForEachEntry( vIds_impl_repr, eId, j ) + { + Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) ); + printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) ); + } + printf("new match flip\n"); + } + } + else if ( Vec_IntSize( vIds_spec_repr ) > 0 && Vec_IntSize( vIds_impl_obj ) > 0 ) // matched, merge impl + { + if ( ( pObj->fPhase ^ pRepr -> fPhase) ^ ( Vec_BitEntry( vImpl2Spec_phase, Vec_IntEntry(vIds_impl_repr, 0)) ^ Vec_BitEntry( vImpl2Spec_phase, Vec_IntEntry(vIds_impl_obj, 0)) ) ) + { + if ( Vec_IntSize( vIds_spec_repr ) == Vec_IntSize( vIds_spec_obj) ) // unmatched repr, matched obj, set repr bits + { + Vec_IntForEachEntry( vIds_impl_repr, eId, j ) + { + if ( j >= Vec_IntSize( vIds_impl_repr)-Vec_IntSize(vIds_impl_obj) ) break; + Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) ); + printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) ); + } + } + else // set obj bits + { + Vec_IntForEachEntry( vIds_impl_obj, eId, j ) + { + Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) ); + printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) ); + } + } + } + } + */ + + Vec_IntClear(vIds_spec_obj); + Vec_IntClear(vIds_impl_obj); + +} +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; + + pBnd -> nMerged_impl = 0; + pBnd -> nMerged_spec = 0; + + + for( i = 0; i < Vec_PtrSize(vBmiter2Spec); i++ ) + { + vSpec = Vec_PtrEntry( vBmiter2Spec, i ); + vImpl = Vec_PtrEntry( vBmiter2Impl, i ); + + // create spec2impl + if ( Vec_IntSize(vSpec) != 0 && Vec_IntSize(vImpl) != 0 ) + { + 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 ); + } + + + } + + // count number of nodes merged into the same circuit + if ( Vec_IntSize(vSpec) != 0 ) + { + pBnd->nMerged_spec += Vec_IntSize(vSpec) - 1; + } + if ( Vec_IntSize(vImpl) != 0 ) + { + pBnd->nMerged_impl += Vec_IntSize(vImpl) - 1; + } + + + + + } + + +} +void Bnd_ManPrintMappings() +{ + Vec_Ptr_t* vBmiter2Spec = pBnd -> vBmiter2Spec; + Vec_Ptr_t* vBmiter2Impl = pBnd -> vBmiter2Impl; + Vec_Int_t* vIds_spec, *vIds_impl; + int k, id; + for( int j=0; j < Vec_PtrSize(vBmiter2Spec); j++ ) + { + printf("node %d: ", j); + vIds_spec = Vec_PtrEntry( vBmiter2Spec, j); + vIds_impl = Vec_PtrEntry( vBmiter2Impl, j); + Vec_IntForEachEntry(vIds_spec, id, k) + printf("%d ", id); + printf("| "); + Vec_IntForEachEntry(vIds_impl, id, k) + printf("%d ", id); + printf("\n"); + } + +} + +void Bnd_ManPrintBound() +{ + + printf("%d nodes merged in spec\n", pBnd ->nMerged_spec - Vec_IntSize(pBnd->vBI) - Vec_IntSize(pBnd->vBO) ); + printf("%d nodes merged in impl\n", pBnd ->nMerged_impl ); + + printf("BI spec:"); Vec_IntPrint(pBnd -> vBI); + printf("BO spec:"); Vec_IntPrint(pBnd -> vBO); + printf("\nEI spec:"); Vec_IntPrint(pBnd -> vEI_spec); + printf("EI impl:"); Vec_IntPrint(pBnd -> vEI_impl); + printf("EI phase:"); Vec_BitPrint(pBnd -> vEI_phase); + printf("\nEO spec:"); Vec_IntPrint(pBnd -> vEO_spec); + printf("EO impl:"); Vec_IntPrint(pBnd -> vEO_impl); + printf("EO phase:"); Vec_BitPrint(pBnd -> vEO_phase); +} + +void Bnd_ManPrintStats() +{ + Bnd_Man_t* p = pBnd; + + // #internal + // nBI, nBO + // nBI_miss, nBO_miss + // nAI, nAO, nExtra + // #spec, #impl, #patched + + // combLoop_spec, combLoop_impl + + // eq_out, eq_res + // status + + // #different choice of impl on boundary + + printf("\nRESULT\n"); + printf("%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->eq_out, p->eq_res, + p->status, + p->nChoice + ); +} + +/**Function************************************************************* + + Synopsis [] + + 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. ] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bnd_ManCheckBound( Gia_Man_t * p ) +{ + int i; + Gia_Obj_t *pObj; + int valid = 1; + pBnd -> nBI = 0; + pBnd -> nBO = 0; + pBnd -> nInternal = 0; + + printf( "Checking boundary... \n"); + + Vec_Int_t *vPath; + vPath = Vec_IntAlloc( Gia_ManObjNum(p) ); + Vec_IntFill( vPath, Gia_ManObjNum(p), 0 ); + int path; + + Gia_ManForEachObjReverse1( p , pObj, i ) + { + if ( Gia_ObjIsCo( pObj ) ) + { + Vec_IntSetEntry( vPath, Gia_ObjId( p, pObj ), 1 ); + } + + path = Vec_IntEntry( vPath, Gia_ObjId(p, pObj) ); + // printf("path = %d\n", path); + + if ( path >= 8 ) + { + valid = 0; + printf("there're more than 2 bufs in a path\n"); + break; + } + + + if( Gia_ObjIsBuf( pObj ) ) + { + Vec_IntSetEntry( vPath, Gia_ObjId( p, Gia_ObjFanin0( pObj ) ), Vec_IntEntry( vPath, Gia_ObjId(p, Gia_ObjFanin0( pObj ) ) ) | path << 1 ); + if ( path == 1 ) // boundary input + { + // TODO: record BIs here since they may not be in the first n buffers + pBnd -> nBO ++; + } + } + else if ( Gia_ObjFaninNum( p, pObj ) >= 1 ) + { + Vec_IntSetEntry( vPath, Gia_ObjId( p, Gia_ObjFanin0( pObj ) ), Vec_IntEntry( vPath, Gia_ObjId(p, Gia_ObjFanin0( pObj ) ) ) | path ); + if ( Gia_ObjFaninNum( p, pObj ) >= 2 ) + { + assert( Gia_ObjFaninNum( p, pObj ) <= 2 ); + Vec_IntSetEntry( vPath, Gia_ObjId( p, Gia_ObjFanin1( pObj ) ), Vec_IntEntry( vPath, Gia_ObjId(p, Gia_ObjFanin1( pObj ) ) ) | path ); + } + if ( path == 2 ) // inside boundary + { + // TODO: record BIs here since they may not be in the first n buffers + pBnd -> nInternal ++; + } + } + else // PI or const, check validity + { + if ( (Vec_IntEntry( vPath, Gia_ObjId(p, pObj) ) | 5) != 5 ) + { + valid = 0; + printf("incorrect buf number at pi %d\n", Vec_IntEntry(vPath, Gia_ObjId(p, pObj)) ); + break; + } + } + } + + pBnd -> nBI = Gia_ManBufNum(p) - pBnd -> nBO; + + if ( !valid ) + { + printf("invalid 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; + } +} + + +int Bnd_CheckFlagRec( Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t* vFlag ) +{ + int id = Gia_ObjId(p, pObj); + if ( Vec_IntEntry(vFlag, id) == 1 ) return 1; + if ( Vec_IntEntry(vFlag, id) == 2 ) return 0; + + Vec_IntSetEntry(vFlag, id, 1); + + int ret = 1; + for( int i = 0; i < Gia_ObjFaninNum(p, pObj); i++ ) + { + if ( !Bnd_CheckFlagRec( p, Gia_ObjFanin(pObj, i), vFlag ) ) + { + ret = 0; + break; + } + } + return ret; + +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bnd_ManCheckExtBound( Gia_Man_t * p, Vec_Int_t *vEI, Vec_Int_t *vEO ) +{ + Vec_Int_t *vFlag = Vec_IntAlloc( Gia_ManObjNum(p) ); + Vec_IntFill( vFlag, Gia_ManObjNum(p), 0 ); + int success = 1; + int i, id; + + Vec_IntForEachEntry( vEO, id, i ) + { + Vec_IntSetEntry( vFlag, id, 2 ); + } + + Vec_IntForEachEntry( vEI, id, i ) + { + if ( Vec_IntEntry(vFlag, id) == 2 ) continue; // BI connected to BO directly + + if ( !Bnd_CheckFlagRec( p, Gia_ManObj(p, id), vFlag ) ) + { + success = 0; + break; + } + } + + + Vec_IntFree(vFlag); + return success; +} + + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +void Bnd_ManFindBound( Gia_Man_t * p ) +{ + Vec_Int_t *vFlag; + Vec_Ptr_t *vQ; + Gia_Obj_t *pObj; + int i, j, id, cnt; + + 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; + Vec_Int_t *vEI_spec = pBnd -> vEI_spec; + Vec_Int_t *vEO_spec = pBnd -> vEO_spec; + Vec_Int_t *vEI_impl = pBnd -> vEI_impl; + Vec_Int_t *vEO_impl = pBnd -> vEO_impl; + Vec_Bit_t *vEI_phase = pBnd -> vEI_phase; + Vec_Bit_t *vEO_phase = pBnd -> vEO_phase; + + + // prepare to compute extended boundary + vQ = Vec_PtrAlloc(16); + vFlag = Vec_IntAlloc( Gia_ManObjNum(p) ); + Vec_IntFill( vFlag, Gia_ManObjNum(p), 0 ); + + Gia_ManStaticFanoutStart(p); + + // save bo, bi + cnt = 0; + Gia_ManForEachBuf(p, pObj, i) + { + if ( cnt < pBnd -> nBI ) + { + Vec_IntPush( vBI, Gia_ObjId(p, pObj) ); + } + else + { + Vec_IntPush( vBO, Gia_ObjId(p, pObj) ); + } + cnt++; + } + printf("#BI = %d #BO = %d\n", Vec_IntSize(vBI), Vec_IntSize(vBO) ); + + // compute EO, travse with flag 1 + Vec_IntForEachEntry( vBO, id, i ) + { + if ( Vec_IntEntry( vSpec2Impl, id ) == -1 ) // BO not matched + { + Vec_PtrPush( vQ, Gia_ManObj(p, id) ); + } + else + { + Vec_IntPush(vEO_spec, id); + } + } + printf("%d BO doesn't match\n", Vec_PtrSize(vQ) ); + pBnd -> nBO_miss = Vec_PtrSize(vQ); + + int cnt_extra = - Vec_PtrSize(vQ); + while( Vec_PtrSize(vQ) > 0 ) + { + pObj = Vec_PtrPop(vQ); + id = Gia_ObjId( p, pObj ); + + if ( Vec_IntEntry( vFlag, id ) == 1 ) continue; + Vec_IntSetEntry( vFlag, id, 1 ); + + // printf("%d\n", id); + + if ( Vec_IntEntry( vSpec2Impl, id ) != -1 ) // matched + { + Vec_IntPush( vEO_spec, id ); + Vec_IntPush( vAO, id ); + } + else + { + for( j = 0; j < Gia_ObjFanoutNum(p, pObj); j++ ) + { + Vec_PtrPush( vQ, Gia_ObjFanout(p, pObj, j) ); + // printf("\t%d\n", Gia_ObjId( p1, Gia_ObjFanout(p1, pObj, j) ) ); + } + } + } + // printf("%d AO found with %d extra nodes\n", Vec_IntSize(vAO) , cnt_extra ); + printf("%d AO found\n", Vec_IntSize(vAO) ); + + + // mark TFOC of BO with flag 1 to prevent them from being selected into EI + // stop at CO + Vec_IntForEachEntry( pBnd -> vBO, id, i ) + { + Vec_PtrPush( vQ, Gia_ManObj(p, id) ); + } + Vec_IntForEachEntry( vFlag, id, i ) + { + Vec_IntSetEntry( vFlag, id, 0 ); + } + while( Vec_PtrSize(vQ) > 0 ) + { + pObj = Vec_PtrPop(vQ); + id = Gia_ObjId( p, pObj ); + + if ( Vec_IntEntry( vFlag, id ) == 1 ) continue; + Vec_IntSetEntry( vFlag, id, 1 ); + + for( j = 0; j < Gia_ObjFanoutNum(p, pObj); j++ ) + { + Vec_PtrPush( vQ, Gia_ObjFanout(p, pObj, j) ); + } + } + + + + // compute EI, traverse with flag 2 + + // add unmatched BI to queue + Vec_IntForEachEntry( vBI, id, i ) + { + if ( Vec_IntEntry( vSpec2Impl, id ) == -1 ) // BO not matched + { + Vec_PtrPush( vQ, Gia_ManObj(p, id) ); + } + else + { + Vec_IntPush(vEI_spec, id); + } + } + printf("%d BI doesn't match\n", Vec_PtrSize(vQ) ); + pBnd -> nBI_miss = Vec_PtrSize(vQ); + cnt_extra -= Vec_PtrSize(vQ); + + // add AO to queue + Vec_IntForEachEntry( vAO, id, i ) + { + Vec_PtrPush( vQ, Gia_ManObj(p, id) ); + } + + // set flag 2 for BO + Vec_IntForEachEntry( vBO, id, i ) + { + Vec_IntSetEntry( vFlag, id, 2 ); + } + + // traverse down from AI and unmatched BI + while( Vec_PtrSize(vQ) > 0 ) + { + pObj = Vec_PtrPop(vQ); + id = Gia_ObjId( p, pObj ); + + if ( Vec_IntEntry( vFlag, id ) == 2 ) continue; + cnt_extra ++; + + // printf("%d\n", id); + + if ( Vec_IntEntry(vFlag, id) != 1 && Vec_IntEntry( vSpec2Impl, id ) != -1 ) // matched + { + Vec_IntPush( vEI_spec, id ); + Vec_IntPush( vAI, id ); + } + else + { + for( j = 0; j < Gia_ObjFaninNum(p, pObj); j++ ) + { + Vec_PtrPush( vQ, Gia_ObjFanin(pObj, j) ); + // printf("\t%d\n", Gia_ObjId( p1, Gia_ObjFanout(p1, pObj, j) ) ); + } + } + + Vec_IntSetEntry( vFlag, id, 2 ); + } + printf("%d AI found with %d extra nodes in total\n", Vec_IntSize(vAI) , cnt_extra ); + pBnd -> nExtra = cnt_extra; + + + // gen vEI_impl, vEO_impl, vEI_phase, vEO_phase + Vec_IntForEachEntry( vEI_spec, id, i ) + { + Vec_IntPush( vEI_impl, Vec_IntEntry( vSpec2Impl, id ) ); + Vec_BitPush( vEI_phase, Vec_BitEntry( vSpec2Impl_phase, id ) ); + } + Vec_IntForEachEntry( vEO_spec, id, i ) + { + Vec_IntPush( vEO_impl, Vec_IntEntry( vSpec2Impl, id ) ); + Vec_BitPush( vEO_phase, Vec_BitEntry( vSpec2Impl_phase, id ) ); + } + + + // count number of choice of boundary in impl + Vec_IntForEachEntry( vEI_spec, id, i ) + { + pBnd -> nChoice += Vec_IntEntry( pBnd -> vSpec2Impl_diff, id ); + } + Vec_IntForEachEntry( vEO_spec, id, i ) + { + pBnd -> nChoice += Vec_IntEntry( pBnd -> vSpec2Impl_diff, id ); + } + + + // 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(); + + // check boundary has comb loop + if ( !Bnd_ManCheckExtBound( p, vEI_spec, vEO_spec ) ) + { + printf("Combinational loop exist\n"); + pBnd -> combLoop_spec = 1; + } + + + // clean up + Vec_IntFree(vAI); + Vec_IntFree(vAO); +} + + + + +/**Function************************************************************* + + Synopsis [] + + Description [create circuit with the boundary changed to CI/CO] + + SideEffects [] + + 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; + Gia_Obj_t * pObj; + int i, id, lit; + + // check if the boundary has loop (EO cannot be in the TFC of EI ) + if ( !Bnd_ManCheckExtBound( p, vEI, vEO ) ) + { + printf("Combinational loop exist\n"); + pBnd -> combLoop_impl = 1; + return 0; + } + + + // initialize + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew -> pName = ABC_ALLOC( char, strlen(p->pName)+10); + sprintf( pNew -> pName, "%s_out", p -> pName ); + Gia_ManHashStart( pNew ); + Gia_ManConst0(p) -> Value = 0; + Gia_ManCleanValue(p); + + + // create ci for ci and eo + Gia_ManForEachCi( p, pObj, i ) + { + pObj -> Value = Gia_ManAppendCi( pNew ); + } + Vec_IntForEachEntry( vEO, id, i ) + { + Gia_ManObj( p, id ) -> Value = Gia_ManAppendCi(pNew); + if ( vEO_phase && Vec_BitEntry( vEO_phase, i ) ) + { + Gia_ManObj( p, id ) -> Value ^= 1; + } + } + + // TODO: consider where EI and EO share the same node + + // add aig nodes + Gia_ManForEachAnd(p, pObj, i) + { + if ( pObj -> Value ) continue; + pObj -> Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } + + // create co for co and ei + Gia_ManForEachCo(p, pObj, i) + { + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + Vec_IntForEachEntry( vEI, id, i ) + { + lit = Gia_ManObj(p, id)->Value; + // lit = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( vEI_phase && Vec_BitEntry( vEI_phase, i ) ) lit ^= 1; + Gia_ManAppendCo( pNew, lit ); + } + + // clean up + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; + +} + +Gia_Man_t* Bnd_ManGenSpecOut( Gia_Man_t* p ) +{ + 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 ) +{ + 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; + return pNew; +} + +void Bnd_AddNodeRec( Gia_Man_t *p, Gia_Man_t *pNew, Gia_Obj_t *pObj ) +{ + // TODO does this mean constant zero node? + if ( pObj -> Value != 0 || Gia_ObjIsConst0(pObj) ) return; + + for( int i = 0; i < Gia_ObjFaninNum(p, pObj); i++ ) + { + Bnd_AddNodeRec( p, pNew, Gia_ObjFanin(pObj, i) ); + } + + if ( Gia_ObjIsAnd(pObj) ) + { + 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) ); + pObj -> Value = Gia_ObjFanin0Copy(pObj); + } +} + +Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPatch ) +{ + + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, id, cnt; + Vec_Int_t *vBI_patch, *vBO_patch; + + printf("Generating patched implementation\n"); + pBnd -> nNode_patch = Gia_ManAndNotBufNum( pPatch ); + + pNew = Gia_ManStart( Gia_ManObjNum(pOut) + Gia_ManObjNum( pSpec ) + Gia_ManObjNum(pPatch) ); + pNew -> pName = ABC_ALLOC( char, strlen(pOut->pName)+3); + sprintf( pNew -> pName, "%s_p", pOut -> pName ); + Gia_ManHashStart( pNew ); + Gia_ManCleanValue(pOut); + Gia_ManCleanValue(pSpec); + Gia_ManCleanValue(pPatch); + + // get bi and bo in patch + cnt = 0; + vBI_patch = Vec_IntAlloc(16); + vBO_patch = Vec_IntAlloc(16); + Gia_ManForEachBuf( pPatch, pObj, i ) + { + if ( cnt < pBnd -> nBI ) + { + Vec_IntPush( vBI_patch, Gia_ObjId( pPatch, pObj ) ); + } + else + { + + Vec_IntPush( vBO_patch, Gia_ObjId( pPatch, pObj ) ); + } + cnt ++; + } + assert( Vec_IntSize( vBI_patch ) == Vec_IntSize(pBnd->vBI) ); + assert( Vec_IntSize( vBO_patch ) == Vec_IntSize(pBnd->vBO) ); + assert( Bnd_ManCheckBound(pPatch) != 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 ); + + // set Spec EI + Gia_ManObj( pSpec, Vec_IntEntry(pBnd -> vEI_spec, i) ) -> Value = pObj -> Value; + printf("%d ", pObj->Value); + } + printf("\n"); + + // add Spec BI to EI + printf("adding BI to EI in Spec\n"); + Vec_IntForEachEntry( pBnd -> vBI, id, i ) + { + pObj = Gia_ManObj( pSpec, id ); + Bnd_AddNodeRec( pSpec, pNew, pObj ); + + // set patch bi + Gia_ManObj( pPatch, Vec_IntEntry( vBI_patch, i) ) -> Value = pObj -> Value; + printf("%d ", pObj->Value); + } + printf("\n"); + + // check + // cnt = 0; + // Gia_ManForEachBuf( pPatch, pObj, i ) + // { + // if ( cnt < pBnd -> nBI ) + // { + // assert(pObj -> Value != 0); + // } + // cnt++; + // } + + // add Patch BO to BI + printf("adding BO to BI in Patch\n"); + Vec_IntForEachEntry( vBO_patch, id, i ) + { + pObj = Gia_ManObj( pPatch, id ); + Bnd_AddNodeRec( pPatch, pNew, pObj ); + + // set spec bo + Gia_ManObj( pSpec, Vec_IntEntry( pBnd -> vBO, i) ) -> Value = pObj -> Value; + printf("%d ", pObj->Value); + } + printf("\n"); + + // add Spec EO to BO + printf("adding EO to BO in Spec\n"); + Vec_IntForEachEntry( pBnd -> vEO_spec, id, i ) + { + pObj = Gia_ManObj( pSpec, id ); + Bnd_AddNodeRec( pSpec, pNew, pObj ); + + // 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 ); + Gia_ManAppendCo( pNew, pObj->Value ); + printf("%d ", pObj->Value); + } + printf("\n"); + + + // clean up + Vec_IntFree( vBI_patch ); + Vec_IntFree( vBO_patch ); + Gia_ManHashStop( pNew ); + + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + + pBnd -> nNode_patched = Gia_ManAndNum( pNew ); + pBnd -> status = 3; + + return pNew; +} + + + + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END \ No newline at end of file diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 37b3e8e3b..bdcbb970e 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -30,12 +30,8 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// -Vec_Ptr_t* vBmiter2Spec; -Vec_Ptr_t* vBmiter2Impl; -Vec_Int_t* vPatch2Impl; -Vec_Bit_t* vImpl2Spec_phase; -Vec_Int_t* vBI_patch; -Vec_Int_t* vBO_patch; + +extern Bnd_Man_t* pBnd; //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// @@ -5674,9 +5670,9 @@ Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum) +Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ) { - Vec_Int_t * vLits; + // Vec_Int_t * vLits; Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; int i, iLit; @@ -5694,7 +5690,7 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, assert( Gia_ManRegNum(p2) == 0 ); assert( Gia_ManCiNum(p1) == Gia_ManCiNum(p2) ); assert( Gia_ManCoNum(p1) == Gia_ManCoNum(p2) ); - vLits = Vec_IntAlloc( Gia_ManBufNum(p1) ); + // vLits = Vec_IntAlloc( Gia_ManBufNum(p1) ); if ( fVerbose ) printf( "Creating a boundary miter with %d inputs, %d outputs, and %d buffers.\n", Gia_ManCiNum(p1), Gia_ManCoNum(p1), Gia_ManBufNum(p1) ); @@ -5705,58 +5701,44 @@ Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, Gia_ManConst0(p1)->Value = 0; Gia_ManConst0(p2)->Value = 0; - // allocate vImpl2Spec_phase; - vImpl2Spec_phase = Vec_BitAlloc( Gia_ManObjNum(p2) ); - Vec_BitFill( vImpl2Spec_phase, Gia_ManObjNum(p2), 0 ); - // allocate vBmiter2Impl and vBmiter2Spec - Vec_Int_t* pVec_Int; - vBmiter2Impl = Vec_PtrAlloc( (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) ); - Vec_PtrFill( vBmiter2Impl, (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)), 0 ); - Vec_PtrForEachEntry( Vec_Int_t*, vBmiter2Impl, pVec_Int, i) + for( int i = 0; i < Gia_ManCiNum(p1); i++ ) { - Vec_PtrSetEntry(vBmiter2Impl, i, Vec_IntAlloc(2) ); - } - vBmiter2Spec = Vec_PtrAlloc( (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)) ); - Vec_PtrFill( vBmiter2Spec, (Gia_ManObjNum(p2) + Gia_ManObjNum(p1)), 0 ); - Vec_PtrForEachEntry( Vec_Int_t*, vBmiter2Spec, pVec_Int, i) - { - Vec_PtrSetEntry(vBmiter2Spec, i, Vec_IntAlloc(2) ); + 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 ); + + pObj = Gia_ManCi(p2, i); + Bnd_ManMap( iLit, Gia_ObjId( p2, pObj) , 0 ); + } - Gia_ManForEachCi( p1, pObj, i ) - { - pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew ); - Vec_IntPush( Vec_PtrEntry(vBmiter2Spec, pObj->Value >> 1), Gia_ObjId(p1, pObj) ); - Vec_IntPush( Vec_PtrEntry(vBmiter2Impl, pObj->Value >> 1), Gia_ObjId(p1, pObj) ); // same pi id in impl and spec - } - - // TODO: record the corresponding impl node of each lit + // record the corresponding impl node of each lit Gia_ManForEachAnd( p2, pObj, i ) { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Vec_IntPush( Vec_PtrEntry(vBmiter2Impl, pObj->Value >> 1), Gia_ObjId(p2, pObj) ); + Bnd_ManMap( pObj -> Value, Gia_ObjId(p2, pObj), 0 ); } - // TODO: record hashed equivalent nodes - Gia_ManForEachAnd( p1, pObj, i ) { + // record hashed equivalent nodes + Gia_ManForEachAnd( p1, pObj, i ) + { pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Vec_IntPush( Vec_PtrEntry(vBmiter2Spec, pObj->Value >> 1), Gia_ObjId(p1, pObj) ); + Bnd_ManMap( pObj -> Value, Gia_ObjId(p1, pObj), 1 ); } Gia_ManForEachCo( p2, pObj, i ) { - int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1; - Vec_IntPush( Vec_PtrEntry(vBmiter2Impl, id), Gia_ObjId(p2, pObj) ); + iLit = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); } Gia_ManForEachCo( p1, pObj, i ) { - int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1; - Vec_IntPush( Vec_PtrEntry(vBmiter2Spec, id), Gia_ObjId(p1, pObj) ); + iLit = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); } - Vec_IntForEachEntry( vLits, iLit, i ) - Gia_ManAppendCo( pNew, iLit ); - Vec_IntFree( vLits ); + // Vec_IntForEachEntry( vLits, iLit, i ) + // Gia_ManAppendCo( pNew, iLit ); + // Vec_IntFree( vLits ); Gia_ManHashStop( pNew ); pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); @@ -5896,538 +5878,6 @@ Gia_Man_t * Gia_ManMiterFromBMiter( Gia_Man_t * p, int nPo ) return pNew; } -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ManPatch( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum) -{ - Vec_Int_t * vLits; - Gia_Man_t * pNew, * pTemp; - Gia_Obj_t * pObj; - int i, iLit; - if ( Gia_ManBufNum(p1) == 0 ) { - printf( "The first AIG should have a boundary.\n" ); - return NULL; - } - if ( Gia_ManBufNum(p2) == 0 ) { - printf( "The second AIG should have a boundary.\n" ); - return NULL; - } - assert( Gia_ManBufNum(p1) > 0 ); - assert( Gia_ManBufNum(p2) > 0 ); - assert( Gia_ManBufNum(p1) == Gia_ManBufNum(p2) ); - assert( Gia_ManRegNum(p1) == 0 ); - assert( Gia_ManRegNum(p2) == 0 ); - assert( Gia_ManCiNum(p1) == Gia_ManCiNum(p2) ); - assert( Gia_ManCoNum(p1) == Gia_ManCoNum(p2) ); - if ( fVerbose ) - printf( "Mapping spec to patch with %d inputs, %d outputs, and %d buffers.\n", - Gia_ManCiNum(p1), Gia_ManCoNum(p1), Gia_ManBufNum(p1) ); - pNew = Gia_ManStart( Gia_ManObjNum(p2) ); - pNew->pName = ABC_ALLOC( char, strlen(p1->pName) + 10 ); - sprintf( pNew->pName, "%s_patch", p1->pName ); - Gia_ManHashStart( pNew ); - Gia_ManConst0(p1)->Value = 0; - Gia_ManConst0(p2)->Value = 0; - - // add patch aig first - // record lit -> patch id - Vec_Int_t* vVar2Patch = Vec_IntAlloc( Gia_ManObjNum(p2) ); - Vec_IntFill( vVar2Patch, Gia_ManObjNum(p2), -1 ); - - Gia_ManForEachCi( p2, pObj, i ) - { - pObj->Value = Gia_ManCi(p1, i)->Value = Gia_ManAppendCi( pNew ); - Vec_IntSetEntry( vVar2Patch, pObj->Value >> 1, Gia_ObjId( p2, pObj ) ); - } - Gia_ManForEachAnd( p2, pObj, i ) - { - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - printf( "\t%d: %d %d\n", Gia_ObjId( p2, pObj), Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Vec_IntSetEntry( vVar2Patch, pObj->Value >> 1, Gia_ObjId( p2, pObj ) ); - } - - - // alloc vCompl; - Vec_Bit_t * vComplBuf = Vec_BitAlloc(Gia_ManBufNum(p1)); - Vec_Bit_t * vCompl = Vec_BitAlloc(Gia_ManObjNum(p1)); - Vec_BitFill( vCompl, Gia_ManObjNum(p1), 0 ); - Gia_ManForEachBuf( p2, pObj, i ) - { - printf("\tbuf compl %d: %d\n", Gia_ObjId(p2, pObj), Gia_ObjFaninC0(pObj)); - Vec_BitPush( vComplBuf, Gia_ObjFaninC0(pObj) ); - } - int cnt = 0; - Gia_ManForEachBuf( p1, pObj, i ) - { - printf("\tbuf compl %d: %d\n", Gia_ObjId(p1, pObj), Gia_ObjFaninC0(pObj)); - if ( Vec_BitEntry( vComplBuf, cnt ) || Gia_ObjFaninC0(pObj) ) - { - Vec_BitSetEntry( vCompl, Gia_ObjId( p1, pObj ), 1 ); - printf("\tset\n"); - } - cnt++; - } - - - - // mark the box in spec - Vec_Int_t* vFlagSpec = Vec_IntAlloc( Gia_ManObjNum(p1) ); // 1: bi, 2: inside the box, 3: bo - Vec_IntFill( vFlagSpec, Gia_ManObjNum(p1), 0 ); - int cnt_buf = 0; - Gia_ManForEachBuf( p1, pObj, i ) - { - if ( cnt_buf < biNum ) - { - Vec_IntSetEntry( vFlagSpec, Gia_ObjId(p1, Gia_ObjFanin0(pObj) ), 1 ); - } - else - { - Vec_IntSetEntry( vFlagSpec, Gia_ObjId(p1, Gia_ObjFanin0(pObj) ), 3 ); - } - cnt_buf ++; - } - - int fanin0, fanin1; - Gia_ManForEachAnd( p1, pObj, i ) - { - if ( Vec_IntEntry( vFlagSpec, Gia_ObjId(p1, pObj) ) != 0 ) continue ; - fanin0 = Vec_IntEntry( vFlagSpec, Gia_ObjId(p1, Gia_ObjFanin0(pObj) ) ); - fanin1 = Vec_IntEntry( vFlagSpec, Gia_ObjId(p1, Gia_ObjFanin1(pObj) ) ); - if ( fanin0 == 1 || fanin0 == 2 || fanin1 == 1 || fanin1 == 2 ) - Vec_IntSetEntry( vFlagSpec, Gia_ObjId(p1, pObj ), 2 ); - } - - - // compute spec2impl - Vec_Int_t* vSpec2Impl = Vec_IntAlloc( Gia_ManObjNum(p1) ); - Vec_IntFill( vSpec2Impl, Gia_ManObjNum(p1), -1 ); - Vec_Int_t* vSpec, *vImpl; - int j, id; - for ( i = 0; i < Vec_PtrSize( vBmiter2Spec ); i++ ) - { - vSpec = Vec_PtrEntry( vBmiter2Spec, i ); - vImpl = Vec_PtrEntry( vBmiter2Impl, i ); - Vec_IntForEachEntry( vSpec, id, j ) - { - if ( Vec_IntEntry( vSpec2Impl, id ) == -1 && Vec_IntSize( vImpl ) > 0 ) - { - Vec_IntSetEntry( vSpec2Impl, id, Vec_IntEntry( vImpl, 0 ) ); - } - } - } - - // print - // printf("spec 2 impl:\n"); - // Vec_IntForEachEntry( vSpec2Impl, id, i ) - // { - // printf( "\t%d:\t %d\n", i, id ); - // } - - // alloc patch2impl - vPatch2Impl = Vec_IntAlloc( Gia_ManObjNum(p2) ); - Vec_IntFill( vPatch2Impl, Gia_ManObjNum(p2), -1 ); - Vec_IntSetEntry( vPatch2Impl, 0, 0 ); - - Gia_ManForEachCi( p2, pObj, i ) - { - Vec_IntSetEntry( vVar2Patch, pObj->Value >> 1, pObj->Value >> 1); - Vec_IntSetEntry( vPatch2Impl, pObj->Value>>1, Vec_IntEntry( vSpec2Impl, pObj->Value>>1) ); - } - - // set the litral on the boundary of spec as in patch and record patch2impl - Vec_Int_t* vBufLit = Vec_IntAlloc( Gia_ManBufNum( p2 ) ); - vBI_patch = Vec_IntAlloc( Gia_ManBufNum(p2) ); - vBO_patch = Vec_IntAlloc( Gia_ManBufNum(p2) ); - cnt_buf = 0; - Gia_ManForEachBuf( p2, pObj, i ) - { - // TODO: check compl - Vec_IntPush( vBufLit, Gia_ObjFanin0( pObj ) -> Value ); - if ( cnt_buf < biNum ) - { - Vec_IntPush( vBI_patch, Gia_ObjFanin0( pObj) -> Value >> 1 ); - } - else - { - Vec_IntPush( vBO_patch, Gia_ObjFanin0( pObj) -> Value >> 1 ); - } - cnt_buf++; - } - Vec_Int_t* vSpec2Patch = Vec_IntAlloc( Gia_ManObjNum(p1) ); - Vec_IntFill( vSpec2Patch, Gia_ManObjNum(p1), -1 ); - - cnt_buf = 0; - Gia_Obj_t * pObj2; - - Gia_ManForEachBuf( p1, pObj, i ) - { - // TODO: compl? - pObj2 = Gia_ObjFanin0(pObj); - pObj2 -> Value = Vec_IntEntry( vBufLit, cnt_buf ); - Vec_IntSetEntry( vSpec2Patch, Gia_ObjId( p1, pObj2 ), Vec_IntEntry( vVar2Patch, pObj2->Value>>1 ) ); - // printf( "spec node %d -> patch node %d\n", Gia_ObjId( p1, pObj2 ), Vec_IntEntry( vVar2Patch, pObj2->Value>>1 ) ); - - Vec_IntSetEntry( vPatch2Impl, pObj2 -> Value>>1, Vec_IntEntry( vSpec2Impl, Gia_ObjId(p1, pObj2) ) ); - pObj->Value = pObj2->Value; - cnt_buf++; - } - - - // hash the area outside the box in spec and record patch2impl - int lit0, lit1; - Gia_ManForEachAnd( p1, pObj, i ) { - printf( "spec node %d(%d) = %d %d\n", Gia_ObjId( p1, pObj ), Vec_IntEntry( vFlagSpec, Gia_ObjId(p1, pObj)), Gia_ObjId( p1, Gia_ObjFanin0(pObj) ), Gia_ObjId( p1, Gia_ObjFanin1(pObj) ) ); - if ( Vec_IntEntry( vFlagSpec, Gia_ObjId(p1, pObj) ) > 1 ) continue; - if ( Gia_ObjIsBuf(pObj) ) continue; - - lit0 = Gia_ObjFanin0Copy(pObj); - lit1 = Gia_ObjFanin1Copy(pObj); - if ( Vec_BitEntry( vCompl, Gia_ObjId(p1, Gia_ObjFanin0(pObj) ) ) ) lit0 ^= 1; - if ( Vec_BitEntry( vCompl, Gia_ObjId(p1, Gia_ObjFanin1(pObj) ) ) ) lit1 ^= 1; - pObj->Value = Gia_ManHashAnd( pNew, lit0, lit1 ); - - - assert( (pObj->Value>>1) < Vec_IntSize( vVar2Patch) ); - assert( Vec_IntEntry( vVar2Patch, pObj->Value>>1 ) != -1 ); - - Vec_IntSetEntry( vSpec2Patch, Gia_ObjId( p1, pObj ), Vec_IntEntry( vVar2Patch, pObj->Value>>1 ) ); - printf( "spec node %d -> patch node %d\n", Gia_ObjId( p1, pObj ), Vec_IntEntry( vVar2Patch, pObj->Value>>1 ) ); - - Vec_IntSetEntry( vPatch2Impl, pObj->Value >> 1, Vec_IntEntry( vSpec2Impl, Gia_ObjId(p1, pObj) ) ); - } - - - // print - printf("patch 2 impl:\n"); - Vec_IntForEachEntry( vPatch2Impl, id, i ) - { - printf( "\t%d:\t %d\n", i, id ); - } - - // handle co - Gia_ManForEachCo( p2, pObj, i ) - { - int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1; - } - // TODO: also check spec CO - // Gia_ManForEachCo( p1, pObj, i ) - // { - // int id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1; - // Vec_IntPush( Vec_PtrEntry(vBmiter2Spec, id), Gia_ObjId(p1, pObj) ); - // } - - Gia_ManHashStop( pNew ); - pNew = Gia_ManCleanup( pTemp = pNew ); - Gia_ManStop( pTemp ); - return pNew; -} - - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ - -Gia_Man_t * Gia_ManPatchImpl( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum) -{ - Vec_Int_t * vLits; - Gia_Man_t * pNew, * pTemp; - Gia_Obj_t * pObj, *pObj2; - int i, j, iLit, id, id2; - assert( Gia_ManRegNum(p1) == 0 ); - assert( Gia_ManRegNum(p2) == 0 ); - assert( Gia_ManCiNum(p1) == Gia_ManCiNum(p2) ); - assert( Gia_ManCoNum(p1) == Gia_ManCoNum(p2) ); - if ( fVerbose ) - printf( "Mapping spec to patch with %d inputs, %d outputs, and %d buffers.\n", - Gia_ManCiNum(p1), Gia_ManCoNum(p1), Gia_ManBufNum(p1) ); - pNew = Gia_ManStart( Gia_ManObjNum(p2) ); - pNew->pName = ABC_ALLOC( char, strlen(p1->pName) + 10 ); - sprintf( pNew->pName, "%s_patch", p1->pName ); - Gia_ManHashStart( pNew ); - Gia_ManConst0(p1)->Value = 0; - Gia_ManConst0(p2)->Value = 0; - - - // p1: patch - // p2: impl - - // compute extended box - - Gia_ManStaticFanoutStart( p1 ); - Vec_Ptr_t* vBO = Vec_PtrAlloc(16); - Vec_Ptr_t* vBI = Vec_PtrAlloc(16); - Vec_Ptr_t* vAO = Vec_PtrAlloc(16); - Vec_Ptr_t* vAI = Vec_PtrAlloc(16); - - - - Vec_Ptr_t* vQ = Vec_PtrAlloc(16); - Vec_Int_t* vFlag = Vec_IntAlloc( Gia_ManObjNum(p1) ); - Vec_IntFill( vFlag, Gia_ManObjNum(p1), 0 ); - Vec_IntForEachEntry( vBO_patch, id, i ) - { - if ( Vec_IntEntry( vPatch2Impl, id ) == -1 ) // if no match on the boundary - Vec_PtrPush( vQ, p1->pObjs+id ); - else - Vec_PtrPush( vBO, p1->pObjs+id ); - } - - while( Vec_PtrSize(vQ) > 0 ) - { - pObj = Vec_PtrPop(vQ); - id = Gia_ObjId( p1, pObj ); - - if ( Vec_IntEntry( vFlag, id ) == 1 ) continue; - Vec_IntSetEntry( vFlag, id, 1 ); - - printf("%d\n", id); - - if ( Vec_IntEntry( vPatch2Impl, id ) != -1 ) // matched - { - Vec_PtrPush( vAO, pObj ); - } - else - { - for( j = 0; j < Gia_ObjFanoutNum(p1, pObj); j++ ) - { - Vec_PtrPush( vQ, Gia_ObjFanout(p1, pObj, j) ); - printf("\t%d\n", Gia_ObjId( p1, Gia_ObjFanout(p1, pObj, j) ) ); - } - - } - } - - // set flag 2 for FOC - Vec_IntForEachEntry( vBO_patch, id, i ) - { - Vec_PtrPush( vQ, p1->pObjs+id ); - } - while( Vec_PtrSize(vQ) > 0 ) - { - pObj = Vec_PtrPop(vQ); - id = Gia_ObjId( p1, pObj ); - - if ( Vec_IntEntry( vFlag, Gia_ObjId(p1, pObj) ) == 2 ) continue; - Vec_IntSetEntry( vFlag, Gia_ObjId(p1, pObj), 2 ); - - for( j = 0; j < Gia_ObjFanoutNum(p1, pObj); j++ ) - { - Vec_PtrPush( vQ, Gia_ObjFanout(p1, pObj, j) ); - } - } - - // set flag 3 for BO - Vec_IntForEachEntry( vBO_patch, id, i ) - { - Vec_IntSetEntry( vFlag, id, 3 ); - } - - // traverse down from unmated BI and AO - Vec_IntForEachEntry( vBI_patch, id, i ) - { - if ( Vec_IntEntry( vPatch2Impl, id ) == -1 ) // if no match on the boundary - Vec_PtrPush( vQ, p1->pObjs+id ); - else - Vec_PtrPush( vBI, p1->pObjs+id ); - } - Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i ) - { - Vec_PtrPush( vQ, pObj ); - } - - // traverse down - printf("traverse down\n"); - while ( Vec_PtrSize(vQ) != 0 ) - { - pObj = Vec_PtrPop(vQ); - id = Gia_ObjId( p1, pObj ); - if ( Vec_IntEntry( vFlag, id ) == 4 ) continue; - - printf("%d\n", id); - - if ( Vec_IntEntry( vPatch2Impl, id ) != -1 && Vec_IntEntry( vFlag, id ) < 2 ) // matched - { - Vec_PtrPush( vAI, pObj ); - printf("matched\n"); - } - else if ( Vec_IntEntry( vFlag, id ) < 3 ) - { - if ( Gia_ObjFaninNum(p1, pObj) > 0 ) - { - Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) ); - printf("\t%d\n", Gia_ObjId( p1, Gia_ObjFanin0(pObj) ) ); - } - - if ( Gia_ObjFaninNum(p1, pObj) > 1 ) - { - Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) ); - printf("\t%d\n", Gia_ObjId( p1, Gia_ObjFanin1(pObj) ) ); - } - } - printf("2impl / flag: %d / %d\n", Vec_IntEntry( vPatch2Impl, id ), Vec_IntEntry( vFlag, id ) ); - - Vec_IntSetEntry( vFlag, id, 4 ); - } - - - // print - printf( "matched BI:"); - Vec_PtrForEachEntry( Gia_Obj_t*, vBI, pObj, i ) printf( " %d(%d)", Gia_ObjId( p1, pObj ), Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj)) ); - printf("\nAI:"); - Vec_PtrForEachEntry( Gia_Obj_t*, vAI, pObj, i ) printf( " %d(%d)", Gia_ObjId( p1, pObj ), Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj)) ); - printf("\nmateched BO:"); - Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i ) printf( " %d(%d)", Gia_ObjId( p1, pObj ), Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj)) ); - printf("\nAO:"); - Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i ) printf( " %d(%d)", Gia_ObjId( p1, pObj ), Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj)) ); - printf("\n"); - - // create patched impl - - // mark fanin cone of Extended Input in impl - Vec_Int_t* vFlag_impl = Vec_IntAlloc( Gia_ManObjNum(p2) ); - Vec_IntFill( vFlag_impl, Gia_ManObjNum(p2), 0 ); - - Vec_PtrForEachEntry( Gia_Obj_t*, vBI, pObj, i ) - { - Vec_PtrPush( vQ, p2->pObjs + Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj) ) ); - } - Vec_PtrForEachEntry( Gia_Obj_t*, vAI, pObj, i ) - { - Vec_PtrPush( vQ, p2->pObjs + Vec_IntEntry( vPatch2Impl, Gia_ObjId(p1, pObj) ) ); - } - - while ( Vec_PtrSize(vQ) != 0 ) - { - pObj = Vec_PtrPop(vQ); - id = Gia_ObjId( p2, pObj ); - if ( Vec_IntEntry( vFlag_impl, id ) == 1 ) continue; - Vec_IntSetEntry( vFlag_impl, id, 1 ); - - if ( Gia_ObjFaninNum(p2, pObj) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) ); - if ( Gia_ObjFaninNum(p2, pObj) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) ); - } - - // add pi - Gia_ManForEachCi( p2, pObj, i ) - { - pObj->Value = Gia_ManCi(p1, i)->Value = Gia_ManAppendCi( pNew ); - } - // add fanin cone of EI in impl - int cnt = 0; - Gia_ManForEachAnd( p2, pObj, i ) - { - if ( Vec_IntEntry( vFlag_impl, Gia_ObjId(p2, pObj) ) == 0 ) continue; - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - printf( "%d\n", pObj->Value>>1 ); - cnt ++; - } - printf( "%d node added in the fanin cone of EI\n", cnt ); - // set literal and flag of EI in patch - // TODO: input phase - Vec_PtrForEachEntry( Gia_Obj_t*, vBI, pObj, i ) - { - id = Gia_ObjId( p1, pObj ); - pObj -> Value = ( p2 -> pObjs + Vec_IntEntry( vPatch2Impl, id ) ) -> Value; - Vec_IntSetEntry( vFlag, id, 5 ); - } - Vec_PtrForEachEntry( Gia_Obj_t*, vAI, pObj, i ) - { - id = Gia_ObjId( p1, pObj ); - pObj -> Value = ( p2 -> pObjs + Vec_IntEntry( vPatch2Impl, id ) ) -> Value; - Vec_IntSetEntry( vFlag, id, 5 ); - } - // mark fanin cone of EO in patch (to flag 5) - Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i ) - Vec_PtrPush( vQ, pObj ); - Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i ) - Vec_PtrPush( vQ, pObj ); - while ( Vec_PtrSize(vQ) != 0 ) - { - pObj = Vec_PtrPop(vQ); - id = Gia_ObjId( p1, pObj ); - if ( Vec_IntEntry( vFlag, id ) >= 5 ) continue; - Vec_IntSetEntry( vFlag, id, 6 ); - - if ( Gia_ObjFaninNum(p1, pObj) > 0 ) Vec_PtrPush( vQ, Gia_ObjFanin0(pObj) ); - if ( Gia_ObjFaninNum(p1, pObj) > 1 ) Vec_PtrPush( vQ, Gia_ObjFanin1(pObj) ); - } - // add fanin cone of EO to EI in patch - cnt = 0; - Gia_ManForEachAnd( p1, pObj, i ) - { - if ( Vec_IntEntry( vFlag, Gia_ObjId(p1, pObj) ) != 6 ) continue; - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - printf( "%d\n", pObj->Value>>1 ); - cnt ++; - } - printf( "%d node added in the extended boundary\n", cnt ); - - // set literal and flag(1) of EO in impl - Vec_PtrForEachEntry( Gia_Obj_t*, vBO, pObj, i ) - { - id = Gia_ObjId( p1, pObj ); - id2 = Vec_IntEntry( vPatch2Impl, id ); - pObj2 = p2 -> pObjs + id2; - pObj2 -> Value = pObj -> Value; - if ( Vec_BitEntry( vImpl2Spec_phase, id2 ) ) pObj2 -> Value ^= 1; - Vec_IntSetEntry( vFlag_impl, id2, 1 ); - } - Vec_PtrForEachEntry( Gia_Obj_t*, vAO, pObj, i ) - { - id = Gia_ObjId( p1, pObj ); - id2 = Vec_IntEntry( vPatch2Impl, id ); - pObj2 = p2 -> pObjs + id2; - pObj2 -> Value = pObj -> Value; - printf( "id %d matched to id %d in impl, phase %d\n", id, id2, Vec_BitEntry( vImpl2Spec_phase, id2 ) ); - if ( Vec_BitEntry( vImpl2Spec_phase, id2 ) ) pObj2 -> Value ^= 1; - Vec_IntSetEntry( vFlag_impl, id2, 1 ); - } - - // add flag 0 in impl - cnt = 0; - Gia_ManForEachAnd( p2, pObj, i ) - { - if ( Vec_IntEntry( vFlag_impl, Gia_ObjId(p2, pObj) ) != 0 ) continue; - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - printf( "%d\n", pObj->Value>>1 ); - cnt++; - } - printf( "%d node added in the fanout cone\n", cnt ); - - // handle co - cnt = 0; - Gia_ManForEachCo( p2, pObj, i ) - { - id = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ) >> 1; - printf( "%d\n", id ); - cnt ++; - } - - Gia_ManStaticFanoutStop( p1 ); - Gia_ManHashStop( pNew ); - pNew = Gia_ManCleanup( pTemp = pNew ); - Gia_ManStop( pTemp ); - return pNew; -} - - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 236d43b32..9e5ae3a57 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -109,4 +109,5 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaTsim.c \ src/aig/gia/giaTtopt.cpp \ src/aig/gia/giaUnate.c \ - src/aig/gia/giaUtil.c + src/aig/gia/giaUtil.c \ + src/aig/gia/giaBound.c \ No newline at end of file diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 1a837d030..537e78c24 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -51695,13 +51695,14 @@ usage: ***********************************************************************/ int Abc_CommandAbc9BMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum); + extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ); Gia_Man_t * pTemp, * pSecond; char * FileName = NULL; FILE * pFile = NULL; int c, fVerbose = 0; int bi = 0; Extra_UtilGetoptReset(); + // TODO: use a flag to block Bnd_Man while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF ) { switch ( c ) @@ -51752,7 +51753,7 @@ int Abc_CommandAbc9BMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9BMiter(): Cannot read the file name on the command line.\n" ); return 0; } - pTemp = Gia_ManBoundaryMiter( pAbc->pGia, pSecond, fVerbose, bi); + pTemp = Gia_ManBoundaryMiter( pAbc->pGia, pSecond, fVerbose ); Gia_ManStop( pSecond ); Abc_FrameUpdateGia( pAbc, pTemp ); return 0; @@ -51852,7 +51853,7 @@ int Abc_CommandAbc9RecoverBoundary( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_Obj_t* pObj; Gia_Man_t * pSpec = NULL; char ** pArgvNew; - int i, nArgcNew, nPo; + int nArgcNew, nPo; int nBInput = -1; char *FileName; Extra_UtilGetoptReset(); @@ -51955,29 +51956,34 @@ usage: return 1; } +extern Bnd_Man_t* pBnd; int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_ManPatch( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum); - extern Gia_Man_t * Gia_ManPatchImpl( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose, int biNum); - Gia_Man_t * pTemp, * pSecond, *pImpl, *pPatched; + 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;; char * FileName = NULL; - char * FileName2 = NULL; FILE * pFile = NULL; - int c, fVerbose = 0; - int bi = 0; + 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; + + // TODO: save return value and return at the end of the function + + // parse options Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Ivh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) { switch ( c ) { - case 'I': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); - goto usage; - } - bi = atoi(argv[globalUtilOptind++]); - break; case 'v': fVerbose ^= 1; break; @@ -51999,7 +52005,10 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } - // get the input file name + // params + + + // read impl FileName = argv[globalUtilOptind]; if ( (pFile = fopen( FileName, "r" )) == NULL ) { @@ -52010,44 +52019,103 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } fclose( pFile ); - - // get the input file name 2 - FileName2 = argv[globalUtilOptind+1]; - if ( (pFile = fopen( FileName2, "r" )) == NULL ) - { - Abc_Print( -1, "Cannot open input file \"%s\". ", FileName2 ); - if ( (FileName2 = Extra_FileGetSimilarName( FileName2, ".aig", ".blif", ".pla", ".eqn", ".bench" )) ) - Abc_Print( 1, "Did you mean \"%s\"?", FileName2 ); - Abc_Print( 1, "\n" ); - return 1; - } - fclose( pFile ); - - // map spec to patch - pSecond = Gia_AigerRead( FileName, 0, 1, 0 ); - if ( pSecond == NULL ) - { - Abc_Print( -1, "Abc_CommandAbc9StrEco(): Cannot read the file name on the command line.\n" ); - return 0; - } - pTemp = Gia_ManPatch( pAbc->pGia, pSecond, fVerbose, bi); - // Gia_ManStop( pSecond ); - // Abc_FrameUpdateGia( pAbc, pTemp ); - // return 0; - - // generated patched impl - pImpl = Gia_AigerRead( FileName2, 0, 0, 0 ); + 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; } - pPatched = Gia_ManPatchImpl( pTemp, pImpl, fVerbose, bi); - Gia_ManStop( pSecond ); + // read patch + FileName = argv[globalUtilOptind+1]; + 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 ); + pPatch = Gia_AigerRead( FileName, 0, 1, 0 ); + if ( pPatch == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9StrEco(): Cannot read the file name on the command line.\n" ); + return 0; + } + + + // verify if spec eq impl + pMiter = Gia_ManMiter( pAbc->pGia, pImpl, 0, 1, 0, 0, 0 ); + assert( Cec_ManVerify( pMiter, pParsCec ) ); + Gia_ManStop(pMiter); + + // start boundary manager + pBnd = Bnd_ManStart( pAbc->pGia, pImpl ); + + // check boundary + if ( 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 + pPatched = Bnd_ManGenPatched( pImpl_out, pAbc->pGia, pPatch ); + + // check if patched is equiv to patch + printf("Checking the equivalence of patch and patched\n"); + pMiter = Gia_ManMiter( pPatch, pPatched, 0, 1, 0, 0, 0 ); + Bnd_ManSetEqRes( Cec_ManVerify( pMiter, pParsCec ) ); + Gia_ManStop( pMiter ); + + } + + Bnd_ManPrintStats(); + Gia_ManStop( pImpl ); - Gia_ManStop( pTemp ); - Abc_FrameUpdateGia( pAbc, pPatched ); + 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(); + return 0; usage: diff --git a/src/misc/vec/vecBit.h b/src/misc/vec/vecBit.h index e41d95aa9..9b0af9d94 100644 --- a/src/misc/vec/vecBit.h +++ b/src/misc/vec/vecBit.h @@ -626,6 +626,27 @@ static inline void Vec_BitReset( Vec_Bit_t * p ) p->pArray[i] = 0; } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Vec_BitPrint( Vec_Bit_t * p ) +{ + int i, Entry; + printf( "Vector has %d entries: {", Vec_BitSize(p) ); + Vec_BitForEachEntry( p, Entry, i ) + printf( " %d", Entry ); + printf( " }\n" ); +} + ABC_NAMESPACE_HEADER_END #endif diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index 0659b3f60..b198c7ffe 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -143,14 +143,6 @@ static inline int Cec4_ObjSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) static inline int Cec4_ObjSetSatId( Gia_Man_t * p, Gia_Obj_t * pObj, int Num ) { assert(Cec4_ObjSatId(p, pObj) == -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), Num); Vec_IntPush(&p->vSuppVars, Gia_ObjId(p, pObj)); if ( Gia_ObjIsCi(pObj) ) Vec_IntPushTwo(&p->vCopiesTwo, Gia_ObjId(p, pObj), Num); assert(Vec_IntSize(&p->vVarMap) == Num); Vec_IntPush(&p->vVarMap, Gia_ObjId(p, pObj)); return Num; } static inline void Cec4_ObjCleanSatId( Gia_Man_t * p, Gia_Obj_t * pObj ) { assert(Cec4_ObjSatId(p, pObj) != -1); Gia_ObjSetCopy2Array(p, Gia_ObjId(p, pObj), -1); } - -extern Vec_Int_t* vMarkBmiter; -extern Vec_Int_t* vIdBI; -extern Vec_Int_t* vIdBO; -extern Vec_Ptr_t* vBmiter2Spec; -extern Vec_Ptr_t* vBmiter2Impl; - - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -1791,9 +1783,9 @@ void Gia_ManRemoveWrongChoices( Gia_Man_t * p ) //Abc_Print( 1, "Removed %d wrong choices.\n", Counter ); } -extern Vec_Bit_t* vImpl2Spec_phase; int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** ppNew, int fSimOnly ) { + Cec4_Man_t * pMan = Cec4_ManCreate( p, pPars ); Gia_Obj_t * pObj, * pRepr; int i, fSimulate = 1; @@ -1894,25 +1886,11 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) ) { - if ( pPars->fBMiterInfo ) + if ( pPars->fBMiterInfo ) { - int eId, j; - Vec_Int_t *vIds_spec_repr, *vIds_impl_repr, *vIds_spec_obj, *vIds_impl_obj; - vIds_spec_repr = Vec_PtrEntry( vBmiter2Spec, id_repr ); - vIds_impl_repr = Vec_PtrEntry( vBmiter2Impl, id_repr ); - vIds_spec_obj = Vec_PtrEntry( vBmiter2Spec, id_obj ); - vIds_impl_obj = Vec_PtrEntry( vBmiter2Impl, id_obj ); - Vec_IntForEachEntry( vIds_spec_obj, eId, j) - { - Vec_IntPush(vIds_spec_repr, eId); - } - Vec_IntForEachEntry( vIds_impl_obj, eId, j) - { - Vec_IntPush(vIds_impl_repr, eId); - } - Vec_IntClear(vIds_spec_obj); - Vec_IntClear(vIds_impl_obj); + Bnd_ManMerge( id_repr, id_obj, pObj->fPhase ^ pRepr->fPhase ); } + assert( (pObj->Value ^ pRepr->Value) == (pObj->fPhase ^ pRepr->fPhase) ); Gia_ObjSetProved( p, i ); if ( Gia_ObjId(p, pRepr) == 0 ) @@ -1923,73 +1901,8 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p { if (pPars->fBMiterInfo){ - int eId, j; - Vec_Int_t *vIds_spec_repr, *vIds_impl_repr, *vIds_spec_obj, *vIds_impl_obj; - vIds_spec_repr = Vec_PtrEntry( vBmiter2Spec, id_repr ); - vIds_impl_repr = Vec_PtrEntry( vBmiter2Impl, id_repr ); - vIds_spec_obj = Vec_PtrEntry( vBmiter2Spec, id_obj ); - vIds_impl_obj = Vec_PtrEntry( vBmiter2Impl, id_obj ); - - Vec_IntForEachEntry( vIds_spec_obj, eId, j) - { - Vec_IntPush(vIds_spec_repr, eId); - } - Vec_IntForEachEntry( vIds_impl_obj, eId, j) - { - Vec_IntPush(vIds_impl_repr, eId); - } - - // handle phase before cleaning - printf( "proven %d merged into %d (phase : %d)\n", Gia_ObjId(p, pObj), Gia_ObjId(p,pRepr), pObj->fPhase ^ pRepr -> fPhase ); - if ( Vec_IntSize(vIds_spec_repr) == 0 ) // no match - { - if ( pObj->fPhase ^ pRepr -> fPhase ) - { - Vec_IntForEachEntry( vIds_impl_obj, eId, j ) - { - Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) ); - printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) ); - } - } - } - else if ( Vec_IntSize( vIds_spec_repr ) == Vec_IntSize( vIds_spec_obj) && Vec_IntSize( vIds_impl_obj ) == 0 ) // new match - { - if ( pObj->fPhase ^ pRepr -> fPhase ) - { - Vec_IntForEachEntry( vIds_impl_repr, eId, j ) - { - Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) ); - printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) ); - } - printf("new match flip\n"); - } - } - else if ( Vec_IntSize( vIds_spec_repr ) > 0 && Vec_IntSize( vIds_impl_obj ) > 0 ) // matched, merge impl - { - if ( ( pObj->fPhase ^ pRepr -> fPhase) ^ ( Vec_BitEntry( vImpl2Spec_phase, Vec_IntEntry(vIds_impl_repr, 0)) ^ Vec_BitEntry( vImpl2Spec_phase, Vec_IntEntry(vIds_impl_obj, 0)) ) ) - { - if ( Vec_IntSize( vIds_spec_repr ) == Vec_IntSize( vIds_spec_obj) ) // unmatched repr, matched obj, set repr bits - { - Vec_IntForEachEntry( vIds_impl_repr, eId, j ) - { - if ( j >= Vec_IntSize( vIds_impl_repr)-Vec_IntSize(vIds_impl_obj) ) break; - Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) ); - printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) ); - } - } - else // set obj bits - { - Vec_IntForEachEntry( vIds_impl_obj, eId, j ) - { - Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) ); - printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) ); - } - } - } - } - - Vec_IntClear(vIds_spec_obj); - Vec_IntClear(vIds_impl_obj); + Bnd_ManMerge( id_repr, id_obj, pObj->fPhase ^ pRepr->fPhase ); + // printf( "proven %d merged into %d (phase : %d)\n", Gia_ObjId(p, pObj), Gia_ObjId(p,pRepr), pObj->fPhase ^ pRepr -> fPhase ); } pObj->Value = Abc_LitNotCond( pRepr->Value, pObj->fPhase ^ pRepr->fPhase ); @@ -2001,20 +1914,8 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p if ( pPars->fBMiterInfo ) { // print - Vec_Int_t* vIds_spec, *vIds_impl; - int k, id; - for( int j=0; j < Vec_PtrSize(vBmiter2Spec); j++ ) - { - printf("node %d: ", j); - vIds_spec = Vec_PtrEntry( vBmiter2Spec, j); - vIds_impl = Vec_PtrEntry( vBmiter2Impl, j); - Vec_IntForEachEntry(vIds_spec, id, k) - printf("%d ", id); - printf("| "); - Vec_IntForEachEntry(vIds_impl, id, k) - printf("%d ", id); - printf("\n"); - } + Bnd_ManFinalizeMappings(); + // Bnd_ManPrintMappings(); } if ( p->iPatsPi > 0 ) @@ -2066,10 +1967,6 @@ Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ) Gia_Man_t * pNew = NULL; Cec4_ManPerformSweeping( p, pPars, &pNew, 0 ); - // TODO - if (pPars -> fBMiterInfo){ - } - return pNew; } void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose ) From f5f4dca013bdcf62282d88ac9d7fa2238a9c0dcd Mon Sep 17 00:00:00 2001 From: Allen Ho Date: Sat, 2 Mar 2024 21:08:10 +0800 Subject: [PATCH 10/11] clean up --- src/aig/gia/giaBound.c | 214 ++++++++++++++++++++--------------------- src/aig/gia/giaDup.c | 61 ------------ src/base/abci/abc.c | 180 ++++++++-------------------------- 3 files changed, 144 insertions(+), 311 deletions(-) diff --git a/src/aig/gia/giaBound.c b/src/aig/gia/giaBound.c index 63b2c389b..9fad955d7 100644 --- a/src/aig/gia/giaBound.c +++ b/src/aig/gia/giaBound.c @@ -34,7 +34,9 @@ struct Bnd_Man_t_ int combLoop_impl; int eq_out; int eq_res; - int nChoice; + int nChoice_spec; + int nChoice_impl; + int feedthrough; Vec_Ptr_t* vBmiter2Spec; Vec_Ptr_t* vBmiter2Impl; @@ -51,6 +53,7 @@ struct Bnd_Man_t_ 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 }; @@ -115,11 +118,16 @@ Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl ) p -> eq_out = 0; p -> eq_res = 0; - p -> nChoice = 0; + p -> nChoice_spec = 0; + 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; } @@ -153,6 +161,7 @@ void Bnd_ManStop() Vec_BitFree( pBnd->vEO_phase ); Vec_IntFree( pBnd-> vSpec2Impl_diff ); + Vec_IntFree( pBnd-> vImpl2Spec_diff ); ABC_FREE( pBnd ); } @@ -208,56 +217,6 @@ void Bnd_ManMerge( int id_repr, int id_obj, int phaseDiff ) } } - // handle impl2spec phase - /* - if ( Vec_IntSize(vIds_spec_repr) == 0 ) // no match - { - if ( pObj->fPhase ^ pRepr -> fPhase ) - { - Vec_IntForEachEntry( vIds_impl_obj, eId, j ) - { - Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) ); - printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) ); - } - } - } - else if ( Vec_IntSize( vIds_spec_repr ) == Vec_IntSize( vIds_spec_obj) && Vec_IntSize( vIds_impl_obj ) == 0 ) // new match - { - if ( pObj->fPhase ^ pRepr -> fPhase ) - { - Vec_IntForEachEntry( vIds_impl_repr, eId, j ) - { - Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) ); - printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) ); - } - printf("new match flip\n"); - } - } - else if ( Vec_IntSize( vIds_spec_repr ) > 0 && Vec_IntSize( vIds_impl_obj ) > 0 ) // matched, merge impl - { - if ( ( pObj->fPhase ^ pRepr -> fPhase) ^ ( Vec_BitEntry( vImpl2Spec_phase, Vec_IntEntry(vIds_impl_repr, 0)) ^ Vec_BitEntry( vImpl2Spec_phase, Vec_IntEntry(vIds_impl_obj, 0)) ) ) - { - if ( Vec_IntSize( vIds_spec_repr ) == Vec_IntSize( vIds_spec_obj) ) // unmatched repr, matched obj, set repr bits - { - Vec_IntForEachEntry( vIds_impl_repr, eId, j ) - { - if ( j >= Vec_IntSize( vIds_impl_repr)-Vec_IntSize(vIds_impl_obj) ) break; - Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) ); - printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) ); - } - } - else // set obj bits - { - Vec_IntForEachEntry( vIds_impl_obj, eId, j ) - { - Vec_BitSetEntry( vImpl2Spec_phase, eId, !Vec_BitEntry(vImpl2Spec_phase, eId) ); - printf( "impl id %d's phase set to %d\n", eId, Vec_BitEntry(vImpl2Spec_phase, eId) ); - } - } - } - } - */ - Vec_IntClear(vIds_spec_obj); Vec_IntClear(vIds_impl_obj); @@ -292,6 +251,12 @@ void Bnd_ManFinalizeMappings() 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 ); + } + } @@ -304,10 +269,6 @@ void Bnd_ManFinalizeMappings() { pBnd->nMerged_impl += Vec_IntSize(vImpl) - 1; } - - - - } @@ -336,15 +297,14 @@ void Bnd_ManPrintMappings() void Bnd_ManPrintBound() { - printf("%d nodes merged in spec\n", pBnd ->nMerged_spec - Vec_IntSize(pBnd->vBI) - Vec_IntSize(pBnd->vBO) ); - printf("%d nodes merged in impl\n", pBnd ->nMerged_impl ); - + // printf("%d nodes merged in spec\n", pBnd ->nMerged_spec - Vec_IntSize(pBnd->vBI) - Vec_IntSize(pBnd->vBO) ); + // printf("%d nodes merged in impl\n", pBnd ->nMerged_impl ); printf("BI spec:"); Vec_IntPrint(pBnd -> vBI); printf("BO spec:"); Vec_IntPrint(pBnd -> vBO); - printf("\nEI spec:"); Vec_IntPrint(pBnd -> vEI_spec); + printf("EI spec:"); Vec_IntPrint(pBnd -> vEI_spec); printf("EI impl:"); Vec_IntPrint(pBnd -> vEI_impl); printf("EI phase:"); Vec_BitPrint(pBnd -> vEI_phase); - printf("\nEO spec:"); Vec_IntPrint(pBnd -> vEO_spec); + printf("EO spec:"); Vec_IntPrint(pBnd -> vEO_spec); printf("EO impl:"); Vec_IntPrint(pBnd -> vEO_impl); printf("EO phase:"); Vec_BitPrint(pBnd -> vEO_phase); } @@ -353,30 +313,54 @@ void Bnd_ManPrintStats() { Bnd_Man_t* p = pBnd; + + printf("\nSTATS\n"); + + int warning = 0; + if ( p->nChoice_spec > 0 ) + { + warning = 1; + printf("WARNING: multiple equiv nodes on the boundary of spec\n"); + } + if ( p->nChoice_impl > 0 ) + { + 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 " ); + // #internal // nBI, nBO // nBI_miss, nBO_miss // nAI, nAO, nExtra // #spec, #impl, #patched - // combLoop_spec, combLoop_impl - - // eq_out, eq_res // status - // #different choice of impl on boundary + // 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\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->eq_out, p->eq_res, p->status, - p->nChoice + p->nChoice_impl, + p->nChoice_spec, + p->feedthrough, + warning, + p->eq_out, p->eq_res ); } @@ -610,7 +594,7 @@ void Bnd_ManFindBound( Gia_Man_t * p ) Vec_IntPush(vEO_spec, id); } } - printf("%d BO doesn't match\n", Vec_PtrSize(vQ) ); + printf("%d BO doesn't match. ", Vec_PtrSize(vQ) ); pBnd -> nBO_miss = Vec_PtrSize(vQ); int cnt_extra = - Vec_PtrSize(vQ); @@ -682,7 +666,7 @@ void Bnd_ManFindBound( Gia_Man_t * p ) Vec_IntPush(vEI_spec, id); } } - printf("%d BI doesn't match\n", Vec_PtrSize(vQ) ); + printf("%d BI doesn't match. ", Vec_PtrSize(vQ) ); pBnd -> nBI_miss = Vec_PtrSize(vQ); cnt_extra -= Vec_PtrSize(vQ); @@ -742,16 +726,16 @@ void Bnd_ManFindBound( Gia_Man_t * p ) } - // count number of choice of boundary in impl + // count number of choice of boundary Vec_IntForEachEntry( vEI_spec, id, i ) - { - pBnd -> nChoice += Vec_IntEntry( pBnd -> vSpec2Impl_diff, id ); - } + pBnd -> nChoice_impl += Vec_IntEntry( pBnd -> vSpec2Impl_diff, id ); Vec_IntForEachEntry( vEO_spec, id, i ) - { - pBnd -> nChoice += Vec_IntEntry( pBnd -> vSpec2Impl_diff, id ); - } - + 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; @@ -790,6 +774,7 @@ Gia_Man_t* Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec { Gia_Man_t * pNew, * pTemp; Gia_Obj_t * pObj; + Vec_Int_t * vValue; int i, id, lit; // check if the boundary has loop (EO cannot be in the TFC of EI ) @@ -809,6 +794,9 @@ Gia_Man_t* Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec Gia_ManConst0(p) -> Value = 0; Gia_ManCleanValue(p); + // record the original value for eo + vValue = Vec_IntAlloc( Gia_ManObjNum(p) ); + Vec_IntFill( vValue, Gia_ManObjNum(p), -1 ); // create ci for ci and eo Gia_ManForEachCi( p, pObj, i ) @@ -817,6 +805,10 @@ Gia_Man_t* Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec } Vec_IntForEachEntry( vEO, id, i ) { + if( Gia_ManObj(p, id) -> Value != 0 ) + { + Vec_IntSetEntry( vValue, id, Gia_ManObj(p, id) -> Value ); + } Gia_ManObj( p, id ) -> Value = Gia_ManAppendCi(pNew); if ( vEO_phase && Vec_BitEntry( vEO_phase, i ) ) { @@ -824,7 +816,14 @@ Gia_Man_t* Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec } } - // TODO: consider where EI and EO share the same node + + // record where EI and EO share the same node + // this may cause non-equivalent + Vec_IntForEachEntry( vEI, id, i ) + { + if ( Gia_ManObj(p, id) -> Value != 0 ) + pBnd -> feedthrough = 1; + } // add aig nodes Gia_ManForEachAnd(p, pObj, i) @@ -840,13 +839,26 @@ Gia_Man_t* Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec } Vec_IntForEachEntry( vEI, id, i ) { - lit = Gia_ManObj(p, id)->Value; - // lit = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + pObj = Gia_ManObj(p, id); + // lit = Gia_ManObj(p, id)->Value; + if ( Gia_ObjIsAnd(pObj) ) lit = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else + { + assert(Gia_ObjIsCi(pObj) || Gia_ObjIsConst0(pObj)); + if ( Vec_IntEntry(vValue, id) != -1 ) + { + lit = Vec_IntEntry( vValue, id ); // EI at PI and EI merged with EO + } + else { + lit = pObj -> Value; // EI at PI + } + } if ( vEI_phase && Vec_BitEntry( vEI_phase, i ) ) lit ^= 1; Gia_ManAppendCo( pNew, lit ); } // clean up + Vec_IntFree( vValue ); Gia_ManHashStop( pNew ); pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); @@ -872,7 +884,12 @@ Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t* p ) void Bnd_AddNodeRec( Gia_Man_t *p, Gia_Man_t *pNew, Gia_Obj_t *pObj ) { // TODO does this mean constant zero node? - if ( pObj -> Value != 0 || Gia_ObjIsConst0(pObj) ) return; + if ( pObj -> Value != 0 ) return; + if ( Gia_ObjIsConst0(pObj) ) + { + printf( "contant zero encountered\n"); + return; + } for( int i = 0; i < Gia_ObjFaninNum(p, pObj); i++ ) { @@ -902,7 +919,6 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat int i, id, cnt; Vec_Int_t *vBI_patch, *vBO_patch; - printf("Generating patched implementation\n"); pBnd -> nNode_patch = Gia_ManAndNotBufNum( pPatch ); pNew = Gia_ManStart( Gia_ManObjNum(pOut) + Gia_ManObjNum( pSpec ) + Gia_ManObjNum(pPatch) ); @@ -932,7 +948,6 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat } assert( Vec_IntSize( vBI_patch ) == Vec_IntSize(pBnd->vBI) ); assert( Vec_IntSize( vBO_patch ) == Vec_IntSize(pBnd->vBO) ); - assert( Bnd_ManCheckBound(pPatch) != 0 ); // add Impl (real) PI @@ -943,7 +958,7 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat } // 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) ); @@ -951,12 +966,10 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat // set Spec EI Gia_ManObj( pSpec, Vec_IntEntry(pBnd -> vEI_spec, i) ) -> Value = pObj -> Value; - printf("%d ", pObj->Value); } - printf("\n"); // add Spec BI to EI - printf("adding BI to EI in Spec\n"); + // printf("adding BI to EI in Spec\n"); Vec_IntForEachEntry( pBnd -> vBI, id, i ) { pObj = Gia_ManObj( pSpec, id ); @@ -964,23 +977,10 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat // set patch bi Gia_ManObj( pPatch, Vec_IntEntry( vBI_patch, i) ) -> Value = pObj -> Value; - printf("%d ", pObj->Value); } - printf("\n"); - - // check - // cnt = 0; - // Gia_ManForEachBuf( pPatch, pObj, i ) - // { - // if ( cnt < pBnd -> nBI ) - // { - // assert(pObj -> Value != 0); - // } - // cnt++; - // } // add Patch BO to BI - printf("adding BO to BI in Patch\n"); + // printf("adding BO to BI in Patch\n"); Vec_IntForEachEntry( vBO_patch, id, i ) { pObj = Gia_ManObj( pPatch, id ); @@ -988,12 +988,10 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat // set spec bo Gia_ManObj( pSpec, Vec_IntEntry( pBnd -> vBO, i) ) -> Value = pObj -> Value; - printf("%d ", pObj->Value); } - printf("\n"); // add Spec EO to BO - printf("adding EO to BO in Spec\n"); + // printf("adding EO to BO in Spec\n"); Vec_IntForEachEntry( pBnd -> vEO_spec, id, i ) { pObj = Gia_ManObj( pSpec, id ); @@ -1001,20 +999,16 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat // 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"); + // 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 ); Gia_ManAppendCo( pNew, pObj->Value ); - printf("%d ", pObj->Value); } - printf("\n"); // clean up diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index bdcbb970e..61acab995 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -5817,67 +5817,6 @@ Gia_Man_t * Gia_ManImplFromBMiter( Gia_Man_t * p, int nPo, int nBInput ) return pNew; } -/**Function************************************************************* - - Synopsis [Duplicates AIG while putting objects in the DFS order.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ManMiterFromBMiter( Gia_Man_t * p, int nPo ) -{ - Gia_Man_t * pNew, *pTemp; - Gia_Obj_t * pObj, *pObj2; - int i, iXor, iPo, i1, i2; - pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Abc_UtilStrsav( "miter" ); - Gia_ManFillValue( p ); - Gia_ManConst0(p)->Value = 0; - - // create primary inputs - Gia_ManForEachCi( p, pObj, i ) - if ( !~pObj->Value ) - pObj->Value = Gia_ManAppendCi(pNew); - - Gia_ManForEachCo( p, pObj, i ) - { - if ( i == nPo ) - { - break; - } - else - { - pObj2 = Gia_ManCo( p, i + nPo ); - - i1 = Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(pObj) ); - i2 = Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(pObj2) ); - - iXor = Gia_ManAppendXor2( pNew, Gia_ObjFaninC0(pObj) ? i1+1 : i1 , Gia_ObjFaninC0(pObj2 ) ? i2+1 : i2 ); - if ( i > 0 ) - { - iPo = Gia_ManAppendOr2( pNew, iPo, iXor ); - } - else - { - iPo = iXor; - } - } - } - Gia_ManAppendCo( pNew, iPo ); - - - pNew = Gia_ManCleanup( pTemp = pNew ); - Gia_ManStop( pTemp ); - pNew = Gia_ManDupNormalize( pTemp = pNew, 0 ); - Gia_ManStop( pTemp ); - - return pNew; -} - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 537e78c24..ed930636b 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -597,7 +597,6 @@ 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_CommandAbc9RecoverBoundary ( 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 ); @@ -1378,7 +1377,6 @@ 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", "&rb", Abc_CommandAbc9RecoverBoundary, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&str_eco", Abc_CommandAbc9StrEco, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); @@ -51839,122 +51837,6 @@ usage: SeeAlso [] ***********************************************************************/ -int Abc_CommandAbc9RecoverBoundary( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - extern Gia_Man_t * Gia_ManDeepSyn( Gia_Man_t * pGia, int nIters, int nNoImpr, int TimeOut, int nAnds, int Seed, int fUseTwo, int fVerbose ); - extern Gia_Man_t * Gia_ManImplFromBMiter( Gia_Man_t * p, int nPo, int nBInput ); - extern Gia_Man_t * Gia_ManMiterFromBMiter( Gia_Man_t * p, int nPo ); - int c, nIters = 1, nNoImpr = ABC_INFINITY, TimeOut = 20, nAnds = 0, Seed = 0, fUseTwo = 0, fVerbose = 0; - - int fKeepBMiter = 0; - Gia_Man_t * pMiter; - Gia_Man_t * pImpl; - Gia_Man_t * pDup; - Gia_Obj_t* pObj; - Gia_Man_t * pSpec = NULL; - char ** pArgvNew; - int nArgcNew, nPo; - int nBInput = -1; - char *FileName; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vkhI," ) ) != EOF ) - { - switch ( c ) - { - case 'I': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" ); - goto usage; - } - nBInput = atoi(argv[globalUtilOptind]); - globalUtilOptind++; - if ( nBInput < 0 ) - goto usage; - break; - case 'k': - fKeepBMiter ^= 1; - break; - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; - } - } - pArgvNew = argv + globalUtilOptind; - nArgcNew = argc - globalUtilOptind; - if ( nArgcNew != 1 ) - { - Abc_Print( -1, "There is no file name.\n" ); - return 1; - } - - if ( pAbc->pGia == NULL ) - { - Abc_Print( -1, "Abc_CommandAbc9RecoverBoundary(): There is no AIG.\n" ); - return 0; - } - FileName = pArgvNew[0]; - - - // printing - - // Gia_ManForEachCo( pAbc->pGia, pObj, i ){ - // printf("Original node: %s id: %i\n", Gia_ObjCoName(pAbc->pGia, i), i); - // } - - - /* - // perform heavy synthesis - pTemp = Gia_ManDeepSyn( pAbc->pGia, nIters, nNoImpr, TimeOut, nAnds, Seed, fUseTwo, fVerbose ); - Abc_FrameUpdateGia( pAbc, pTemp ); - // print spec/impl and boundary information - Gia_ManForEachCo( pAbc->pGia, pObj, i ){ - printf("Output node: %s id: %i\n", Gia_ObjCoName(pAbc->pGia, i), i); - } - */ - - - - // check boundary recovery status - pSpec = Gia_AigerRead( FileName, false, true, 0 ); - if ( !pSpec ) - { - Abc_Print( -1, "Abc_CommandAbc9RecoverBoundary(): fail to read spec.\n" ); - return 1; - } - nPo = Gia_ManCoNum( pSpec ); - - // duplicate - pDup = Gia_ManDup( pAbc->pGia ); - - // option 1: remove po and keep the buffers - // default nbinput: - if ( nBInput == -1 ) nBInput = (Gia_ManCoNum(pDup)-2*nPo)/2; - pImpl = Gia_ManImplFromBMiter( pDup, nPo, nBInput ); - - // option 2: build miter (with uif?) - if (!fKeepBMiter ) - { - pMiter = Gia_ManMiterFromBMiter( pAbc->pGia, nPo ); - Abc_FrameUpdateGia( pAbc, pMiter ); - } - - return 0; - -usage: - Abc_Print( -2, "usage: &rb [-vkh] \n" ); - Abc_Print( -2, "\t generate an implementation aig with specification boundary\n" ); - Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); - Abc_Print( -2, "\t-k : keep the bmiter and print the boundary status only.\n"); - Abc_Print( -2, "\t-I num : the number of inputs in the boundary\n"); - Abc_Print( -2, "\t-h : print the command usage\n"); - Abc_Print( -2, "\t : the specification file\n"); - return 1; -} extern Bnd_Man_t* pBnd; int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) @@ -52005,9 +51887,6 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } - // params - - // read impl FileName = argv[globalUtilOptind]; if ( (pFile = fopen( FileName, "r" )) == NULL ) @@ -52044,21 +51923,27 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; } - - // verify if spec eq impl - pMiter = Gia_ManMiter( pAbc->pGia, pImpl, 0, 1, 0, 0, 0 ); - assert( Cec_ManVerify( pMiter, pParsCec ) ); - Gia_ManStop(pMiter); - // start boundary manager pBnd = Bnd_ManStart( pAbc->pGia, pImpl ); - // check boundary - if ( 0 == Bnd_ManCheckBound( pAbc -> pGia ) ) + // verify if spec eq impl + pMiter = Gia_ManMiter( pAbc->pGia, pImpl, 0, 1, 0, 0, 0 ); + if ( !Cec_ManVerify( pMiter, pParsCec ) ) { - Abc_Print( -1, "Abc_CommandAbc9StrEco(): The given boundary is invalid.\n" ); + 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 ) { @@ -52077,10 +51962,10 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) 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 ); + // 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 ); } @@ -52093,11 +51978,26 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) Bnd_ManSetEqOut( Cec_ManVerify( pMiter, pParsCec ) ); Gia_ManStop( pMiter ); - // generate patched + // 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 patch and patched\n"); + printf("Checking the equivalence of patch and patched impl\n"); pMiter = Gia_ManMiter( pPatch, pPatched, 0, 1, 0, 0, 0 ); Bnd_ManSetEqRes( Cec_ManVerify( pMiter, pParsCec ) ); Gia_ManStop( pMiter ); @@ -52119,12 +52019,12 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &str_eco -I [-vh] \n" ); - Abc_Print( -2, "\t creates the boundary miter\n" ); - Abc_Print( -2, "\t-I : number of boundary inputs\n" ); + 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 file\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; } From 23654254e1e6f8965454504892fe68698e32990c Mon Sep 17 00:00:00 2001 From: Allen Ho Date: Sun, 3 Mar 2024 03:06:13 +0800 Subject: [PATCH 11/11] clean up --- src/aig/gia/giaBound.c | 99 +++++++++++++++++++++++------------------- src/base/abci/abc.c | 2 +- 2 files changed, 56 insertions(+), 45 deletions(-) diff --git a/src/aig/gia/giaBound.c b/src/aig/gia/giaBound.c index 9fad955d7..7988d8655 100644 --- a/src/aig/gia/giaBound.c +++ b/src/aig/gia/giaBound.c @@ -299,14 +299,14 @@ void Bnd_ManPrintBound() // printf("%d nodes merged in spec\n", pBnd ->nMerged_spec - Vec_IntSize(pBnd->vBI) - Vec_IntSize(pBnd->vBO) ); // printf("%d nodes merged in impl\n", pBnd ->nMerged_impl ); - printf("BI spec:"); Vec_IntPrint(pBnd -> vBI); - printf("BO spec:"); Vec_IntPrint(pBnd -> vBO); - printf("EI spec:"); Vec_IntPrint(pBnd -> vEI_spec); - printf("EI impl:"); Vec_IntPrint(pBnd -> vEI_impl); - printf("EI phase:"); Vec_BitPrint(pBnd -> vEI_phase); - printf("EO spec:"); Vec_IntPrint(pBnd -> vEO_spec); - printf("EO impl:"); Vec_IntPrint(pBnd -> vEO_impl); - printf("EO phase:"); Vec_BitPrint(pBnd -> vEO_phase); + printf("BI spec:\t"); Vec_IntPrint(pBnd -> vBI); + printf("BO spec:\t"); Vec_IntPrint(pBnd -> vBO); + printf("EI spec:\t"); Vec_IntPrint(pBnd -> vEI_spec); + printf("EI impl:\t"); Vec_IntPrint(pBnd -> vEI_impl); + printf("EI phase:\t"); Vec_BitPrint(pBnd -> vEI_phase); + printf("EO spec:\t"); Vec_IntPrint(pBnd -> vEO_spec); + printf("EO impl:\t"); Vec_IntPrint(pBnd -> vEO_impl); + printf("EO phase:\t"); Vec_BitPrint(pBnd -> vEO_phase); } void Bnd_ManPrintStats() @@ -347,21 +347,21 @@ void Bnd_ManPrintStats() // 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,%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 + // ); } /**Function************************************************************* @@ -580,7 +580,6 @@ void Bnd_ManFindBound( Gia_Man_t * p ) } cnt++; } - printf("#BI = %d #BO = %d\n", Vec_IntSize(vBI), Vec_IntSize(vBO) ); // compute EO, travse with flag 1 Vec_IntForEachEntry( vBO, id, i ) @@ -785,14 +784,26 @@ 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); sprintf( pNew -> pName, "%s_out", p -> pName ); Gia_ManHashStart( pNew ); + Gia_ManFillValue(p); Gia_ManConst0(p) -> Value = 0; - Gia_ManCleanValue(p); + // record the original value for eo vValue = Vec_IntAlloc( Gia_ManObjNum(p) ); @@ -805,7 +816,7 @@ Gia_Man_t* Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec } Vec_IntForEachEntry( vEO, id, i ) { - if( Gia_ManObj(p, id) -> Value != 0 ) + if( Gia_ManObj(p, id) -> Value != ~0 ) { Vec_IntSetEntry( vValue, id, Gia_ManObj(p, id) -> Value ); } @@ -817,18 +828,10 @@ Gia_Man_t* Bnd_ManCutBoundary( Gia_Man_t *p, Vec_Int_t* vEI, Vec_Int_t* vEO, Vec } - // record where EI and EO share the same node - // this may cause non-equivalent - Vec_IntForEachEntry( vEI, id, i ) - { - if ( Gia_ManObj(p, id) -> Value != 0 ) - pBnd -> feedthrough = 1; - } - // add aig nodes Gia_ManForEachAnd(p, pObj, i) { - if ( pObj -> Value ) continue; + if ( pObj -> Value != ~0 ) continue; pObj -> Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); } @@ -884,12 +887,7 @@ Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t* p ) void Bnd_AddNodeRec( Gia_Man_t *p, Gia_Man_t *pNew, Gia_Obj_t *pObj ) { // TODO does this mean constant zero node? - if ( pObj -> Value != 0 ) return; - if ( Gia_ObjIsConst0(pObj) ) - { - printf( "contant zero encountered\n"); - return; - } + if ( pObj -> Value != ~0 ) return; for( int i = 0; i < Gia_ObjFaninNum(p, pObj); i++ ) { @@ -925,9 +923,12 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat pNew -> pName = ABC_ALLOC( char, strlen(pOut->pName)+3); sprintf( pNew -> pName, "%s_p", pOut -> pName ); Gia_ManHashStart( pNew ); - Gia_ManCleanValue(pOut); - Gia_ManCleanValue(pSpec); - Gia_ManCleanValue(pPatch); + Gia_ManFillValue(pOut); + Gia_ManFillValue(pSpec); + Gia_ManFillValue(pPatch); + Gia_ManConst0(pOut)->Value = 0; + Gia_ManConst0(pSpec)->Value = 0; + Gia_ManConst0(pPatch)->Value = 0; // get bi and bo in patch cnt = 0; @@ -966,7 +967,9 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat // set Spec EI Gia_ManObj( pSpec, Vec_IntEntry(pBnd -> vEI_spec, i) ) -> Value = pObj -> Value; + // printf(" %d",pObj -> Value); } + // printf("\n"); // add Spec BI to EI // printf("adding BI to EI in Spec\n"); @@ -977,7 +980,9 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat // set patch bi Gia_ManObj( pPatch, Vec_IntEntry( vBI_patch, i) ) -> Value = pObj -> Value; + // printf(" %d",pObj -> Value); } + // printf("\n"); // add Patch BO to BI // printf("adding BO to BI in Patch\n"); @@ -988,7 +993,9 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat // set spec bo Gia_ManObj( pSpec, Vec_IntEntry( pBnd -> vBO, i) ) -> Value = pObj -> Value; + // printf(" %d",pObj -> Value); } + // printf("\n"); // add Spec EO to BO // printf("adding EO to BO in Spec\n"); @@ -999,7 +1006,9 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat // 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"); @@ -1008,7 +1017,9 @@ Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPat pObj = Gia_ManCo( pOut, i ); Bnd_AddNodeRec( pOut, pNew, pObj ); Gia_ManAppendCo( pNew, pObj->Value ); + // printf(" %d",pObj -> Value); } + // printf("\n"); // clean up diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index ed930636b..4f53096f8 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -51997,7 +51997,7 @@ int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_ManStop( pTemp ); // check if patched is equiv to patch - printf("Checking the equivalence of patch and patched impl\n"); + 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 ) ); Gia_ManStop( pMiter );