From 6f5656c18837f86f2a9e18fe35046fb7ee306c9f Mon Sep 17 00:00:00 2001 From: Allen Ho Date: Fri, 1 Mar 2024 16:05:41 +0800 Subject: [PATCH] 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 )