diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 25a3758eb..ca413f31d 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1532,6 +1532,7 @@ extern void Gia_ManSetRegNum( Gia_Man_t * p, int nRegs ); extern void Gia_ManReportImprovement( Gia_Man_t * p, Gia_Man_t * pNew ); extern void Gia_ManPrintNpnClasses( Gia_Man_t * p ); extern void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int fVerBufs, int fInter, int fInterComb, int fAssign, int fReverse ); +extern void Gia_ManDumpVerilogNand( Gia_Man_t * p, char * pFileName ); /*=== giaMem.c ===========================================================*/ extern Gia_MmFixed_t * Gia_MmFixedStart( int nEntrySize, int nEntriesMax ); extern void Gia_MmFixedStop( Gia_MmFixed_t * p, int fVerbose ); @@ -1790,6 +1791,39 @@ 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, int fVerbose ); +extern void Bnd_ManStop(); + +// getter +extern int Bnd_ManGetNInternal(); +extern int Bnd_ManGetNExtra(); + +//for fraig +extern void Bnd_ManMap( int iLit, int id, int spec ); +extern void Bnd_ManMerge( int id1, int id2, int phaseDiff ); +extern void Bnd_ManFinalizeMappings(); +extern void Bnd_ManPrintMappings(); +extern Gia_Man_t* Bnd_ManStackGias( Gia_Man_t *pSpec, Gia_Man_t *pImpl ); +extern int Bnd_ManCheckCoMerged( Gia_Man_t *p ); + +// for eco +extern int Bnd_ManCheckBound( Gia_Man_t *p, int fVerbose ); +extern void Bnd_ManFindBound( Gia_Man_t *p, Gia_Man_t *pImpl ); +extern Gia_Man_t* Bnd_ManGenSpecOut( Gia_Man_t *p ); +extern Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t *p ); +extern Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPatch ); +extern Gia_Man_t* Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec ); +extern Gia_Man_t* Bnd_ManGenPatched2( Gia_Man_t *pImpl, Gia_Man_t *pPatch, int fSkiptStrash, int fVerbose ); +extern void Bnd_ManSetEqOut( int eq ); +extern void Bnd_ManSetEqRes( int eq ); +extern void Bnd_ManPrintStats(); + +// 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..f7811967d --- /dev/null +++ b/src/aig/gia/giaBound.c @@ -0,0 +1,1374 @@ +#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 fVerbose; + + int combLoop_spec; + int combLoop_impl; + int eq_out; + int eq_res; + int nChoice_spec; + int nChoice_impl; + int feedthrough; + + int maxNumClass; + + Vec_Ptr_t* vBmiter2Spec; + Vec_Ptr_t* vBmiter2Impl; + Vec_Bit_t* vSpec2Impl_phase; // TODO: record all phases + + Vec_Int_t* vImpl2Bmiter; + Vec_Int_t* vSpec2Bmiter; + + Vec_Int_t* vBI; + Vec_Int_t* vBO; + 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; + +}; + +Bnd_Man_t* pBnd = 0; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +void Bnd_ManSetEqOut( int eq ) { pBnd -> eq_out = eq;} +void Bnd_ManSetEqRes( int eq ) { pBnd -> eq_res = eq;} + +Vec_Int_t* Bnd_ManSpec2Impl( int id ) { return (Vec_Int_t*)Vec_PtrEntry( pBnd -> vBmiter2Impl, Vec_IntEntry( pBnd->vSpec2Bmiter, id ) ); } +int Bnd_ManSpec2ImplNum( int id ) { return Vec_IntSize( (Vec_Int_t*)Vec_PtrEntry( pBnd -> vBmiter2Impl, Vec_IntEntry( pBnd->vSpec2Bmiter, id ) ) ); } + +Vec_Int_t* Bnd_ManImpl2Spec( int id ) { return (Vec_Int_t*)Vec_PtrEntry( pBnd -> vBmiter2Spec, Vec_IntEntry( pBnd->vImpl2Bmiter, id ) ); } +int Bnd_ManImpl2SpecNum( int id ) { return Vec_IntSize( (Vec_Int_t*)Vec_PtrEntry( pBnd -> vBmiter2Spec, Vec_IntEntry( pBnd->vImpl2Bmiter, id ) ) ); } + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +Bnd_Man_t* Bnd_ManStart( Gia_Man_t *pSpec, Gia_Man_t *pImpl, int fVerbose ) +{ + int i; + Bnd_Man_t* p = ABC_CALLOC( Bnd_Man_t, 1 ); + + p -> maxNumClass = Gia_ManCiNum( pSpec ) + Gia_ManAndNotBufNum(pSpec) + Gia_ManAndNum(pImpl) + 2 + Gia_ManCoNum(pSpec) * 2; + // one for constant node and one for dummy + + p -> vBmiter2Spec = Vec_PtrAlloc( p -> maxNumClass ); + p -> vBmiter2Impl = Vec_PtrAlloc( p -> maxNumClass ); + Vec_PtrFill( p -> vBmiter2Spec, p -> maxNumClass, 0 ); + Vec_PtrFill( p -> vBmiter2Impl, p -> maxNumClass, 0 ); + for( i = 0; i < Vec_PtrSize( p -> vBmiter2Impl ); i ++ ) + { + Vec_PtrSetEntry( p -> vBmiter2Spec, i, Vec_IntAlloc(1) ); + Vec_PtrSetEntry( p -> vBmiter2Impl, i, Vec_IntAlloc(1) ); + } + + p -> vSpec2Impl_phase = Vec_BitAlloc( Gia_ManObjNum(pSpec) ); + Vec_BitFill( p -> vSpec2Impl_phase, Gia_ManObjNum(pSpec), 0 ); + + p -> vImpl2Bmiter = Vec_IntAlloc( Gia_ManObjNum(pImpl) ); + Vec_IntFill( p -> vImpl2Bmiter, Gia_ManObjNum(pImpl), p -> maxNumClass - 1 ); + p -> vSpec2Bmiter = Vec_IntAlloc( Gia_ManObjNum(pSpec) ); + Vec_IntFill( p -> vSpec2Bmiter, Gia_ManObjNum(pSpec), p -> maxNumClass - 1); + + p -> vBI = Vec_IntAlloc(16); + p -> vBO = Vec_IntAlloc(16); + 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 -> fVerbose = fVerbose; + + p -> combLoop_spec = 0; + p -> combLoop_impl = 0; + p -> eq_out = 0; + p -> eq_res = 0; + + p -> nChoice_spec = 0; + p -> nChoice_impl = 0; + p -> feedthrough = 0; + + return p; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bnd_ManStop() +{ + assert(pBnd); + + Vec_PtrFree( pBnd-> vBmiter2Spec ); + Vec_PtrFree( pBnd-> vBmiter2Impl ); + Vec_BitFree( pBnd-> vSpec2Impl_phase ); + Vec_IntFree( pBnd-> vImpl2Bmiter ); + Vec_IntFree( pBnd-> vSpec2Bmiter ); + + 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 ); + + ABC_FREE( pBnd ); +} + +int Bnd_ManGetNInternal() { assert(pBnd); return pBnd -> nInternal; } +int Bnd_ManGetNExtra() { assert(pBnd); return pBnd -> nExtra; } + +void Bnd_ManMap( int iLit, int id, int spec ) +{ + + if ( spec ) + { + Vec_IntPush( (Vec_Int_t *)Vec_PtrEntry( pBnd -> vBmiter2Spec, iLit >> 1), id ); + Vec_BitSetEntry( pBnd -> vSpec2Impl_phase, id, iLit & 1 ); + } + else + { + assert( (iLit & 1) == 0 ); + Vec_IntPush( (Vec_Int_t *)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_Int_t *)Vec_PtrEntry( vBmiter2Spec, id_repr ); + vIds_impl_repr = (Vec_Int_t *)Vec_PtrEntry( vBmiter2Impl, id_repr ); + vIds_spec_obj = (Vec_Int_t *)Vec_PtrEntry( vBmiter2Spec, id_obj ); + vIds_impl_obj = (Vec_Int_t *)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) ); + } + } + + 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 *vSpec, *vImpl; + int i, j, id; + + pBnd -> nMerged_impl = 0; + pBnd -> nMerged_spec = 0; + + + for( i = 0; i < Vec_PtrSize(vBmiter2Spec); i++ ) + { + vSpec = (Vec_Int_t *)Vec_PtrEntry( vBmiter2Spec, i ); + vImpl = (Vec_Int_t *)Vec_PtrEntry( vBmiter2Impl, i ); + + Vec_IntForEachEntry( vSpec, id, j ) + { + // vSpec2Bmiter + Vec_IntSetEntry( pBnd->vSpec2Bmiter, id, i ); + } + + Vec_IntForEachEntry( vImpl, id, j ) + { + // vImpl2Bmiter + Vec_IntSetEntry( pBnd->vImpl2Bmiter, id, i ); + } + + // count number of nodes merged into the same circuit + 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_Int_t *)Vec_PtrEntry( vBmiter2Spec, j); + vIds_impl = (Vec_Int_t *)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:\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() +{ + 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"); + } + + printf("The outsides of spec and impl are %sEQ.\n", p->eq_out ? "" : "NOT " ); + printf("The patched impl is %sEQ. to spec (and impl)\n", p->eq_res ? "" : "NOT " ); + + // #internal + // nBI, nBO + // nBI_miss, nBO_miss + // nEI, nEO, nExtra + // #spec, #impl, #patched + // combLoop_spec, combLoop_impl + // #choice_impl + // #choice_spec + // #feedthrough + // 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\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->nChoice_impl, + p->nChoice_spec, + warning, + p->eq_out, p->eq_res + ); + + printf("#Choice Spec\t%d\n", p->nChoice_spec); + printf("#Choice Impl\t%d\n", p->nChoice_impl); + + + +} + +/**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. + Can be called even if Bnd_Man_t is not created] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Bnd_ManCheckBound( Gia_Man_t * p, int fVerbose ) +{ + int i; + Gia_Obj_t *pObj; + int valid = 1; + int nBI = 0, nBO = 0, nInternal = 0; + + if ( fVerbose ) 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 + 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 + 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; + } + } + } + + nBI = Gia_ManBufNum(p) - nBO; + + if ( !valid ) + { + printf("invalid boundary\n"); + return 0; + } + else if ( nBI == 0 ) + { + printf("no boundary\n"); + return 0; + } + else + { + if ( fVerbose ) + { + printf("valid boundary ("); + printf("#BI = %d\t#BO = %d\t", nBI, Gia_ManBufNum(p)- nBI); + printf("#Internal = %d)\n", nInternal ); + } + if ( pBnd ) + { + pBnd -> nBI = nBI; + pBnd -> nBO = nBO; + pBnd -> nInternal = nInternal; + } + return nBI; + } +} + + +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 [check if combnational loop exist in the extended boundary] + + 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 [find the extended boundary in spec + and compute the corresponding boundary in impl] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Bnd_ManFindBound( Gia_Man_t * p, Gia_Man_t * pImpl ) +{ + Vec_Int_t *vFlag; + 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_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, Gia_ObjFanin0(pObj) ) ); + } + else + { + Vec_IntPush( vBO, Gia_ObjId(p, pObj) ); + } + cnt++; + } + + // compute EO, travse with flag 1 + Vec_IntForEachEntry( vBO, id, i ) + { + if ( Bnd_ManSpec2ImplNum(id) == 0 ) // BO not matched + { + Vec_PtrPush( vQ, Gia_ManObj(p, id) ); + } + else + { + Vec_IntPush(vEO_spec, id); + } + } + if ( pBnd -> fVerbose ) printf("%d BO doesn't match. ", Vec_PtrSize(vQ) ); + pBnd -> nBO_miss = Vec_PtrSize(vQ); + + int cnt_extra = - Vec_PtrSize(vQ); + while( Vec_PtrSize(vQ) > 0 ) + { + pObj = (Gia_Obj_t *)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 ( Bnd_ManSpec2ImplNum(id) != 0 ) // 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 ); + if ( pBnd -> fVerbose ) printf("%d AO found\n", Vec_IntSize(vAO) ); + + + // mark TFOC of BO with flag 1 to prevent them from being selected into EI + // 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 = (Gia_Obj_t *)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 ( Bnd_ManSpec2ImplNum(id) == 0 ) // BO not matched + { + Vec_PtrPush( vQ, Gia_ManObj(p, id) ); + } + else + { + Vec_IntPush(vEI_spec, id); + } + } + if ( pBnd -> fVerbose ) printf("%d BI doesn't match. ", 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 = (Gia_Obj_t *)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 && Bnd_ManSpec2ImplNum(id) != 0 ) // 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 ); + } + if ( pBnd -> fVerbose ) 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( Bnd_ManSpec2Impl(id) , 0 ) ); + Vec_BitPush( vEI_phase, Vec_BitEntry( vSpec2Impl_phase, id ) ); + } + Vec_IntForEachEntry( vEO_spec, id, i ) + { + Vec_IntPush( vEO_impl, Vec_IntEntry( Bnd_ManSpec2Impl(id), 0 ) ); + Vec_BitPush( vEO_phase, Vec_BitEntry( vSpec2Impl_phase, id ) ); + } + + + // count number of choice of boundary + Vec_IntForEachEntry( vEO_spec, id, i ) + { + pBnd -> nChoice_impl += Bnd_ManSpec2ImplNum( id ) - 1; + } + Vec_IntForEachEntry( vEO_impl, id, i ) + { + pBnd -> nChoice_spec += Bnd_ManImpl2SpecNum( id ) - 1; + } + + // print + if ( pBnd -> fVerbose ) + { + printf("#EI = %d\t#EO = %d\t#Extra Node = %d\n", Vec_IntSize(vEI_spec) , Vec_IntSize(vEO_spec), cnt_extra ); + Bnd_ManPrintBound(); + } + + // check boundary has comb loop + if ( !Bnd_ManCheckExtBound( p, vEI_spec, vEO_spec ) ) + { + + 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; + Vec_Int_t * vValue; + 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_ManFillValue(p); + Gia_ManConst0(p) -> Value = 0; + + + // 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 ) + { + pObj -> Value = Gia_ManAppendCi( pNew ); + } + 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 ) ) + { + Gia_ManObj( p, id ) -> Value ^= 1; + } + } + + // add aig nodes + Gia_ManForEachAnd(p, pObj, i) + { + if ( pObj -> Value != ~0 ) 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 ) + { + 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 ); + return pNew; + +} + +Gia_Man_t* Bnd_ManGenSpecOut( Gia_Man_t* p ) +{ + if ( pBnd -> fVerbose ) printf("Generating spec_out with given boundary.\n"); + Gia_Man_t *pNew = Bnd_ManCutBoundary( p, pBnd->vEI_spec, pBnd->vEO_spec, 0, 0 ); + return pNew; +} +Gia_Man_t* Bnd_ManGenImplOut( Gia_Man_t* p) +{ + if ( pBnd -> fVerbose ) printf("Generating impl_out with given boundary.\n"); + Gia_Man_t *pNew = Bnd_ManCutBoundary( p, pBnd->vEI_impl, pBnd->vEO_impl, pBnd->vEI_phase, pBnd->vEO_phase ); + if (!pNew) pBnd -> combLoop_impl = 1; + return pNew; +} + +void Bnd_AddNodeRec( Gia_Man_t *p, Gia_Man_t *pNew, Gia_Obj_t *pObj, int fSkipStrash ) +{ + // TODO does this mean constant zero node? + if ( pObj -> Value != ~0 ) return; + + for( int i = 0; i < Gia_ObjFaninNum(p, pObj); i++ ) + { + Bnd_AddNodeRec( p, pNew, Gia_ObjFanin(pObj, i), fSkipStrash ); + } + + if ( Gia_ObjIsAnd(pObj) ) + { + if ( fSkipStrash ) + { + if ( Gia_ObjIsBuf(pObj) ) pObj -> Value = Gia_ManAppendBuf( pNew, Gia_ObjFanin0Copy(pObj) ); + else pObj -> Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } + else + { + pObj -> Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } + } + else + { + assert( Gia_ObjIsCo(pObj) ); + // if ( Gia_ObjIsCi(pObj) ) printf("Ci with value ~0 encountered (id = %d)\n", Gia_ObjId(p, pObj) ); + pObj -> Value = Gia_ObjFanin0Copy(pObj); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [perform ECO directly (not used)] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t* Bnd_ManGenPatched( Gia_Man_t *pOut, Gia_Man_t *pSpec, Gia_Man_t *pPatch ) +{ + + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, id, cnt; + Vec_Int_t *vBI_patch, *vBO_patch; + + 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_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; + 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) ); + + + // 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, 0 ); + + // 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, 0 ); + + // 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"); + Vec_IntForEachEntry( vBO_patch, id, i ) + { + pObj = Gia_ManObj( pPatch, id ); + Bnd_AddNodeRec( pPatch, pNew, pObj, 0 ); + + // 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, 0 ); + + // 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, 0 ); + 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 ); + + return pNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [recover bounadry] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t* Bnd_ManGenPatched1( Gia_Man_t *pOut, Gia_Man_t *pSpec ) +{ + + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, id; + + pNew = Gia_ManStart( Gia_ManObjNum(pOut) + Gia_ManObjNum( pSpec ) ); + pNew -> pName = ABC_ALLOC( char, strlen(pOut->pName)+3); + sprintf( pNew -> pName, "%s_p", pOut -> pName ); + + Gia_ManFillValue(pOut); + Gia_ManFillValue(pSpec); + Gia_ManConst0(pOut)->Value = 0; + Gia_ManConst0(pSpec)->Value = 0; + + + // add Impl (real) PI + for ( i = 0; i < Gia_ManCiNum(pSpec); i++ ) + { + pObj = Gia_ManCi(pOut, i); + pObj -> Value = Gia_ManAppendCi( pNew ); + } + + // add Impl EI to CI + // printf("adding EI to CI in Impl\n"); + for ( i = 0; i < Vec_IntSize( pBnd -> vEI_spec ); i++ ) + { + pObj = Gia_ManCo(pOut, i + Gia_ManCoNum(pSpec) ); + Bnd_AddNodeRec( pOut, pNew, pObj, 1 ); + + // set Spec EI + Gia_ManObj( pSpec, Vec_IntEntry(pBnd -> vEI_spec, i) ) -> Value = pObj -> Value; + // printf(" %d",pObj -> Value); + } + // printf("\n"); + + // add Spec EO to EI + // add BI -> BO -> EO to maintain the order of bufs + // Vec_IntForEachEntry( pBnd -> vBI, id, i ) + // { + // pObj = Gia_ManObj( pSpec, id ); + // Bnd_AddNodeRec( pSpec, pNew, pObj, 1 ); + // } + // Vec_IntForEachEntry( pBnd -> vBO, id, i ) + // { + // pObj = Gia_ManObj( pSpec, id ); + // Bnd_AddNodeRec( pSpec, pNew, pObj, 1 ); + // } + Gia_ManForEachBuf( pSpec, pObj, i ) + { + Bnd_AddNodeRec( pSpec, pNew, pObj, 1 ); + } + Vec_IntForEachEntry( pBnd -> vEO_spec, id, i ) + { + pObj = Gia_ManObj( pSpec, id ); + Bnd_AddNodeRec( pSpec, pNew, pObj, 1 ); + + // set impl EO (PI) + Gia_ManCi( pOut, i + Gia_ManCiNum(pSpec) ) -> Value = pObj -> Value; + // printf(" %d",pObj -> Value); + } + // printf("\n"); + + // add Impl (real) PO to EO + // printf("adding CO to EO in Impl\n"); + for ( i = 0; i < Gia_ManCoNum(pSpec); i++ ) + { + pObj = Gia_ManCo( pOut, i ); + Bnd_AddNodeRec( pOut, pNew, pObj, 1 ); + Gia_ManAppendCo( pNew, pObj->Value ); + // printf(" %d",pObj -> Value); + } + // printf("\n"); + + + // clean up + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + + pBnd -> nNode_patched = Gia_ManAndNum( pNew ); + + return pNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [perform eco with recovered boundary. + bnd_man is not used] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t* Bnd_ManGenPatched2( Gia_Man_t *pImpl, Gia_Man_t *pPatch, int fSkipStrash, int fVerbose ) +{ + + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + int i, nBI, nBI_patch, cnt; + Vec_Int_t* vLit; + + + // check boundary first + nBI = Bnd_ManCheckBound( pImpl, fVerbose ); + nBI_patch = Bnd_ManCheckBound( pPatch, fVerbose ); + if ( 0 == nBI_patch || Gia_ManBufNum(pImpl) != Gia_ManBufNum(pPatch) || nBI != nBI_patch ) + { + Abc_Print( -1, "Abc_CommandAbc9StrEco(): The given boundary is invalid.\n" ); + return 0; + } + + // prepare new network + pNew = Gia_ManStart( Gia_ManObjNum(pImpl) + Gia_ManObjNum( pPatch ) ); + pNew -> pName = ABC_ALLOC( char, strlen(pImpl->pName)+3); + sprintf( pNew -> pName, "%s_p", pImpl -> pName ); + if ( !fSkipStrash ) + { + Gia_ManHashAlloc( pNew ); + } + Gia_ManFillValue(pImpl); + Gia_ManFillValue(pPatch); + Gia_ManConst0(pImpl)->Value = 0; + Gia_ManConst0(pPatch)->Value = 0; + + vLit = Vec_IntAlloc( Gia_ManBufNum(pImpl) ); + + // add Impl (real) CI + Gia_ManForEachCi( pImpl, pObj, i ) + { + pObj -> Value = Gia_ManAppendCi( pNew ); + } + + // add Impl BI to CI + cnt = 0; + Gia_ManForEachBuf( pImpl, pObj, i ) + { + Bnd_AddNodeRec( pImpl, pNew, pObj, fSkipStrash ); + Vec_IntPush( vLit, pObj -> Value ); + cnt ++; + if ( cnt >= nBI ) break; + } + + // set BI in patch + // add patch BO to BI + cnt = 0; + Gia_ManForEachBuf( pPatch, pObj, i ) + { + if ( cnt < nBI ) + { + pObj -> Value = Vec_IntEntry( vLit, cnt ); + } + else + { + Bnd_AddNodeRec( pPatch, pNew, pObj, fSkipStrash ); + Vec_IntPush( vLit, pObj -> Value ); + } + cnt ++; + if ( cnt == nBI ) Vec_IntClear( vLit ); + } + + // set BO in impl + cnt = 0; + Gia_ManForEachBuf( pImpl, pObj, i ) + { + cnt ++; + if ( cnt <= nBI) continue; + pObj -> Value = Vec_IntEntry( vLit, cnt-nBI-1 ); + } + + // add impl CO to BO + Gia_ManForEachCo( pImpl, pObj, i ) + { + Bnd_AddNodeRec( pImpl, pNew, pObj, fSkipStrash ); + Gia_ManAppendCo( pNew, pObj -> Value ); + } + + // clean up + if ( !fSkipStrash ) + { + Gia_ManHashStop( pNew ); + } + Vec_IntFree( vLit ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + + return pNew; +} + + +Gia_Man_t* Bnd_ManStackGias( Gia_Man_t *pSpec, Gia_Man_t *pImpl ) +{ + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj; + + int i, iLit; + if ( Gia_ManBufNum(pSpec) == 0 ) { + printf( "The spec AIG should have a boundary.\n" ); + return NULL; + } + if ( Gia_ManBufNum(pImpl) != 0 ) { + printf( "The impl AIG should have no boundary.\n" ); + return NULL; + } + + assert( Gia_ManBufNum(pSpec) > 0 ); + assert( Gia_ManBufNum(pImpl) == 0 ); + assert( Gia_ManRegNum(pSpec) == 0 ); + assert( Gia_ManRegNum(pImpl) == 0 ); + assert( Gia_ManCiNum(pSpec) == Gia_ManCiNum(pImpl) ); + assert( Gia_ManCoNum(pSpec) == Gia_ManCoNum(pImpl) ); + + pNew = Gia_ManStart( Gia_ManObjNum(pSpec) + Gia_ManObjNum(pImpl) ); + pNew->pName = ABC_ALLOC( char, strlen(pSpec->pName) + 10 ); + sprintf( pNew->pName, "%s_stack", pSpec->pName ); + + Gia_ManHashStart( pNew ); + Gia_ManConst0(pSpec)->Value = 0; + Gia_ManConst0(pImpl)->Value = 0; + + for( int i = 0; i < Gia_ManCiNum(pSpec); i++ ) + { + int iLit = Gia_ManCi(pSpec, i)->Value = Gia_ManCi(pImpl, i) -> Value = Gia_ManAppendCi(pNew); + + pObj = Gia_ManCi(pSpec, i); + Bnd_ManMap( iLit, Gia_ObjId( pSpec, pObj ), 1 ); + + pObj = Gia_ManCi(pImpl, i); + Bnd_ManMap( iLit, Gia_ObjId( pImpl, pObj) , 0 ); + } + + // record the corresponding impl node of each lit + Gia_ManForEachAnd( pImpl, pObj, i ) + { + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( pBnd ) Bnd_ManMap( pObj -> Value, Gia_ObjId(pImpl, pObj), 0 ); + } + + Vec_Int_t* vFlag = Vec_IntAlloc( Gia_ManObjNum( pSpec ) ); + Vec_IntFill( vFlag, Gia_ManObjNum(pSpec), 0 ); + int count = 0; + Gia_ManForEachBuf( pSpec, pObj, i ) + { + if ( count < pBnd -> nBI ) + { + // it's BI, don't record buf + Vec_IntSetEntry( vFlag, Gia_ObjId( pSpec, pObj ), 1 ); + } + else + { + // it's BO, don't record buf's fanin + Vec_IntSetEntry( vFlag, Gia_ObjId( pSpec, Gia_ObjFanin0( pObj ) ), 1 ); + } + count++; + } + + // record hashed equivalent nodes + Gia_ManForEachAnd( pSpec, pObj, i ) + { + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( Vec_IntEntry( vFlag, Gia_ObjId( pSpec, pObj ) ) == 0 ) + { + Bnd_ManMap( pObj -> Value, Gia_ObjId(pSpec, pObj), 1 ); + } + } + Vec_IntFree( vFlag ); + + Gia_ManForEachCo( pImpl, pObj, i ) + { + iLit = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + Gia_ManForEachCo( pSpec, pObj, i ) + { + iLit = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + + // miter + // Gia_ManForEachCo( pImpl, pObj, i ) + // { + // iLit = Gia_ManHashXor( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin0Copy(Gia_ManCo(pSpec,i)) ); + // Gia_ManAppendCo( pNew, iLit ); + // } + + + Gia_ManHashStop( pNew ); + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + return pNew; +} + +int Bnd_ManCheckCoMerged( Gia_Man_t* p ) +{ + int nCO = Gia_ManCoNum(p)/2; + + Gia_Obj_t* pObj1; + Gia_Obj_t* pObj2; + + for ( int i = 0; i < nCO; i++ ) + { + pObj1 = Gia_ManCo(p, i); + pObj2 = Gia_ManCo(p, i + nCO); + if ( Gia_ObjFaninLit0p(p, pObj1) != Gia_ObjFaninLit0p(p, pObj2) ) return 0; + } + return 1; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +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 dbedca099..92eb2ac89 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -30,6 +30,9 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// + +extern Bnd_Man_t* pBnd; + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -5674,7 +5677,7 @@ Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p ) ***********************************************************************/ 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; @@ -5692,7 +5695,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) ); @@ -5702,28 +5705,124 @@ 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; - Gia_ManForEachCi( p1, pObj, i ) - pObj->Value = Gia_ManCi(p2, i)->Value = Gia_ManAppendCi( pNew ); - Gia_ManForEachAnd( p2, pObj, i ) - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - Gia_ManForEachAnd( p1, pObj, i ) { - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - if ( Gia_ObjIsBuf(pObj) ) - Vec_IntPush( vLits, pObj->Value ); + + + for( int i = 0; i < Gia_ManCiNum(p1); i++ ) + { + int iLit = Gia_ManCi(p1, i)->Value = Gia_ManCi(p2, i) -> Value = Gia_ManAppendCi(pNew); + + pObj = Gia_ManCi(p1, i); + if ( pBnd ) Bnd_ManMap( iLit, Gia_ObjId( p1, pObj ), 1 ); + + pObj = Gia_ManCi(p2, i); + if ( pBnd ) Bnd_ManMap( iLit, Gia_ObjId( p2, pObj) , 0 ); + } + + // record the corresponding impl node of each lit + Gia_ManForEachAnd( p2, pObj, i ) + { + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( pBnd ) Bnd_ManMap( pObj -> Value, Gia_ObjId(p2, pObj), 0 ); + } + + // record hashed equivalent nodes + Gia_ManForEachAnd( p1, pObj, i ) + { + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + if ( pBnd ) Bnd_ManMap( pObj -> Value, Gia_ObjId(p1, pObj), 1 ); + } + Gia_ManForEachCo( p2, 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 ); + { + iLit = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + Gia_ManForEachCo( p1, pObj, i ) + { + iLit = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + + // Vec_IntForEachEntry( vLits, iLit, i ) + // Gia_ManAppendCo( pNew, iLit ); + // Vec_IntFree( vLits ); Gia_ManHashStop( pNew ); pNew = Gia_ManCleanup( pTemp = pNew ); Gia_ManStop( pTemp ); 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; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaFx.c b/src/aig/gia/giaFx.c index 032ae5fc4..c20241ed1 100644 --- a/src/aig/gia/giaFx.c +++ b/src/aig/gia/giaFx.c @@ -150,6 +150,13 @@ Vec_Wrd_t * Gia_ManComputeTruths( Gia_Man_t * p, int nCutSize, int nLutNum, int // collect and sort fanins vLeaves.nCap = vLeaves.nSize = Gia_ObjLutSize( p, i ); vLeaves.pArray = Gia_ObjLutFanins( p, i ); + if( !Vec_IntCheckUniqueSmall(&vLeaves) ) + { + Vec_IntUniqify(&vLeaves); + Vec_IntWriteEntry(p->vMapping, Vec_IntEntry(p->vMapping, i), vLeaves.nSize); + for ( k = 0; k < vLeaves.nSize; k++ ) + Vec_IntWriteEntry(p->vMapping, Vec_IntEntry(p->vMapping, i) + 1 + k, vLeaves.pArray[k]); + } assert( Vec_IntCheckUniqueSmall(&vLeaves) ); Vec_IntSelectSort( Vec_IntArray(&vLeaves), Vec_IntSize(&vLeaves) ); if ( !fReverse ) diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 7498630a8..f2d403ded 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -1254,7 +1254,7 @@ void Gia_ManDfsSlacksPrint( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -void Gia_ManWriteNamesInter( FILE * pFile, char c, int n, int Start, int Skip, int nRegs ) +void Gia_ManWriteNamesInter( FILE * pFile, char c, int n, int Start, int Skip, int nRegs, int fReverse ) { int Length = Start, i, fFirst = 1; char pName[100]; @@ -1318,9 +1318,9 @@ void Gia_ManDumpInterface2( Gia_Man_t * p, FILE * pFile ) fprintf( pFile, "_inst" ); fprintf( pFile, " (\n " ); - Gia_ManWriteNamesInter( pFile, 'i', Gia_ManCiNum(p), 4, 4, Gia_ManRegNum(p) ); + Gia_ManWriteNamesInter( pFile, 'i', Gia_ManCiNum(p), 4, 4, Gia_ManRegNum(p), 0 ); fprintf( pFile, ",\n " ); - Gia_ManWriteNamesInter( pFile, 'o', Gia_ManCoNum(p), 4, 4, Gia_ManRegNum(p) ); + Gia_ManWriteNamesInter( pFile, 'o', Gia_ManCoNum(p), 4, 4, Gia_ManRegNum(p), 0 ); fprintf( pFile, "\n );\n\n" ); fprintf( pFile, "endmodule\n\n" ); @@ -1387,16 +1387,17 @@ char * Gia_ObjGetDumpName( Vec_Ptr_t * vNames, char c, int i, int d ) sprintf( pBuffer, "%c%0*d%c", c, d, i, c ); return pBuffer; } -void Gia_ManWriteNames( FILE * pFile, char c, int n, Vec_Ptr_t * vNames, int Start, int Skip, Vec_Bit_t * vObjs ) +void Gia_ManWriteNames( FILE * pFile, char c, int n, Vec_Ptr_t * vNames, int Start, int Skip, Vec_Bit_t * vObjs, int fReverse ) { int Digits = Abc_Base10Log( n ); int Length = Start, i, fFirst = 1; char * pName; for ( i = 0; i < n; i++ ) { - if ( vObjs && !Vec_BitEntry(vObjs, i) ) + int k = fReverse ? n-1-i : i; + if ( vObjs && !Vec_BitEntry(vObjs, k) ) continue; - pName = Gia_ObjGetDumpName( vNames, c, i, Digits ); + pName = Gia_ObjGetDumpName( vNames, c, k, Digits ); Length += strlen(pName) + 2; if ( Length > 60 ) { @@ -1413,12 +1414,12 @@ void Gia_ManDumpVerilog( Gia_Man_t * p, char * pFileName, Vec_Int_t * vObjs, int if ( fInterComb ) { if ( fAssign ) { - extern void Gia_ManDumpInterfaceAssign( Gia_Man_t * p, char * pFileName, int fReverse ); - Gia_ManDumpInterfaceAssign( p, pFileName, fReverse ); + extern void Gia_ManDumpInterfaceAssign( Gia_Man_t * p, char * pFileName ); + Gia_ManDumpInterfaceAssign( p, pFileName ); } else { - extern void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName, int fReverse ); - Gia_ManDumpInterface( p, pFileName, fReverse ); + extern void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName ); + Gia_ManDumpInterface( p, pFileName ); } } else @@ -1464,26 +1465,26 @@ void Gia_ManDumpVerilogNoInter( Gia_Man_t * p, char * pFileName, Vec_Int_t * vOb if ( fVerBufs ) { fprintf( pFile, " (\n " ); - Gia_ManWriteNames( pFile, 'a', Gia_ManPiNum(p), NULL, 4, 4, NULL ); + Gia_ManWriteNames( pFile, 'a', Gia_ManPiNum(p), NULL, 4, 4, NULL, 0 ); fprintf( pFile, ",\n " ); - Gia_ManWriteNames( pFile, 'y', Gia_ManPoNum(p), NULL, 4, 4, NULL ); + Gia_ManWriteNames( pFile, 'y', Gia_ManPoNum(p), NULL, 4, 4, NULL, 0 ); fprintf( pFile, "\n );\n\n" ); fprintf( pFile, " input " ); - Gia_ManWriteNames( pFile, 'a', Gia_ManPiNum(p), NULL, 8, 4, NULL ); + Gia_ManWriteNames( pFile, 'a', Gia_ManPiNum(p), NULL, 8, 4, NULL, 0 ); fprintf( pFile, ";\n\n" ); fprintf( pFile, " output " ); - Gia_ManWriteNames( pFile, 'y', Gia_ManPoNum(p), NULL, 9, 4, NULL ); + Gia_ManWriteNames( pFile, 'y', Gia_ManPoNum(p), NULL, 9, 4, NULL, 0 ); fprintf( pFile, ";\n\n" ); fprintf( pFile, " wire " ); - Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL ); + Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL, 0 ); fprintf( pFile, ";\n\n" ); fprintf( pFile, " wire " ); - Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL ); + Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL, 0 ); fprintf( pFile, ";\n\n" ); Gia_ManForEachPi( p, pObj, i ) @@ -1503,32 +1504,32 @@ void Gia_ManDumpVerilogNoInter( Gia_Man_t * p, char * pFileName, Vec_Int_t * vOb else { fprintf( pFile, " (\n " ); - Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 4, 4, NULL ); + Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 4, 4, NULL, 0 ); fprintf( pFile, ",\n " ); - Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 4, 4, NULL ); + Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 4, 4, NULL, 0 ); fprintf( pFile, "\n );\n\n" ); fprintf( pFile, " input " ); - Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL ); + Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL, 0 ); fprintf( pFile, ";\n\n" ); fprintf( pFile, " output " ); - Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL ); + Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL, 0 ); fprintf( pFile, ";\n\n" ); } if ( Vec_BitCount(vUsed) ) { fprintf( pFile, " wire " ); - Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed ); + Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed, 0 ); fprintf( pFile, ";\n\n" ); } if ( Vec_BitCount(vInvs) ) { fprintf( pFile, " wire " ); - Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs ); + Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs, 0 ); fprintf( pFile, ";\n\n" ); } @@ -1644,26 +1645,26 @@ void Gia_ManDumpVerilogNoInterAssign( Gia_Man_t * p, char * pFileName, Vec_Int_t if ( fVerBufs ) { fprintf( pFile, " (\n " ); - Gia_ManWriteNames( pFile, 'a', Gia_ManPiNum(p), NULL, 4, 4, NULL ); + Gia_ManWriteNames( pFile, 'a', Gia_ManPiNum(p), NULL, 4, 4, NULL, 0 ); fprintf( pFile, ",\n " ); - Gia_ManWriteNames( pFile, 'y', Gia_ManPoNum(p), NULL, 4, 4, NULL ); + Gia_ManWriteNames( pFile, 'y', Gia_ManPoNum(p), NULL, 4, 4, NULL, 0 ); fprintf( pFile, "\n );\n\n" ); fprintf( pFile, " input " ); - Gia_ManWriteNames( pFile, 'a', Gia_ManPiNum(p), NULL, 8, 4, NULL ); + Gia_ManWriteNames( pFile, 'a', Gia_ManPiNum(p), NULL, 8, 4, NULL, 0 ); fprintf( pFile, ";\n\n" ); fprintf( pFile, " output " ); - Gia_ManWriteNames( pFile, 'y', Gia_ManPoNum(p), NULL, 9, 4, NULL ); + Gia_ManWriteNames( pFile, 'y', Gia_ManPoNum(p), NULL, 9, 4, NULL, 0 ); fprintf( pFile, ";\n\n" ); fprintf( pFile, " wire " ); - Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL ); + Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL, 0 ); fprintf( pFile, ";\n\n" ); fprintf( pFile, " wire " ); - Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL ); + Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL, 0 ); fprintf( pFile, ";\n\n" ); Gia_ManForEachPi( p, pObj, i ) @@ -1683,32 +1684,32 @@ void Gia_ManDumpVerilogNoInterAssign( Gia_Man_t * p, char * pFileName, Vec_Int_t else { fprintf( pFile, " (\n " ); - Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 4, 4, NULL ); + Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 4, 4, NULL, 0 ); fprintf( pFile, ",\n " ); - Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 4, 4, NULL ); + Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 4, 4, NULL, 0 ); fprintf( pFile, "\n );\n\n" ); fprintf( pFile, " input " ); - Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL ); + Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL, 0 ); fprintf( pFile, ";\n\n" ); fprintf( pFile, " output " ); - Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL ); + Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL, 0 ); fprintf( pFile, ";\n\n" ); } if ( Vec_BitCount(vUsed) ) { fprintf( pFile, " wire " ); - Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed ); + Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed, 0 ); fprintf( pFile, ";\n\n" ); } if ( Vec_BitCount(vInvs) ) { fprintf( pFile, " wire " ); - Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs ); + Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs, 0 ); fprintf( pFile, ";\n\n" ); } @@ -1838,7 +1839,7 @@ Vec_Int_t * Gia_ManCountSymbsAll( Vec_Ptr_t * vNames ) } return vArray; } -void Gia_ManDumpIoList( Gia_Man_t * p, FILE * pFile, int fOuts ) +void Gia_ManDumpIoList( Gia_Man_t * p, FILE * pFile, int fOuts, int fReverse ) { Vec_Ptr_t * vNames = fOuts ? p->vNamesOut : p->vNamesIn; if ( vNames == NULL ) @@ -1849,13 +1850,18 @@ void Gia_ManDumpIoList( Gia_Man_t * p, FILE * pFile, int fOuts ) int iName, Size, i; Vec_IntForEachEntryDouble( vArray, iName, Size, i ) { + if ( fReverse ) + { + iName = Vec_IntEntry(vArray, Vec_IntSize(vArray)-2-i); + Size = Vec_IntEntry(vArray, Vec_IntSize(vArray)-1-i); + } if ( i ) fprintf( pFile, ", " ); Gia_ManPrintOneName( pFile, (char *)Vec_PtrEntry(vNames, iName), Size ); } Vec_IntFree( vArray ); } } -void Gia_ManDumpIoRanges( Gia_Man_t * p, FILE * pFile, int fOuts, int fReverse ) +void Gia_ManDumpIoRanges( Gia_Man_t * p, FILE * pFile, int fOuts ) { Vec_Ptr_t * vNames = fOuts ? p->vNamesOut : p->vNamesIn; if ( p->vNamesOut == NULL ) @@ -1874,7 +1880,7 @@ void Gia_ManDumpIoRanges( Gia_Man_t * p, FILE * pFile, int fOuts, int fReverse ) int NumEnd = Gia_ManReadRangeNum( pNameLast, Size ); fprintf( pFile, " %s ", fOuts ? "output" : "input" ); if ( NumBeg != -1 && iName < iNameNext-1 ) - fprintf( pFile, "[%d:%d] ", fReverse ? NumBeg : NumEnd, fReverse ? NumEnd : NumBeg ); + fprintf( pFile, "[%d:%d] ", NumEnd, NumBeg ); Gia_ManPrintOneName( pFile, pName, Size ); fprintf( pFile, ";\n" ); } @@ -1893,7 +1899,7 @@ void Gia_ManDumpIoRanges( Gia_Man_t * p, FILE * pFile, int fOuts, int fReverse ) SeeAlso [] ***********************************************************************/ -void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName, int fReverse ) +void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName ) { Gia_Obj_t * pObj; Vec_Bit_t * vInvs, * vUsed; @@ -1916,45 +1922,45 @@ void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName, int fReverse ) Gia_ManDumpModuleName( pFile, p->pName ); fprintf( pFile, "_wrapper" ); fprintf( pFile, " ( " ); - Gia_ManDumpIoList( p, pFile, 0 ); + Gia_ManDumpIoList( p, pFile, 0, 0 ); fprintf( pFile, ", " ); - Gia_ManDumpIoList( p, pFile, 1 ); + Gia_ManDumpIoList( p, pFile, 1, 0 ); fprintf( pFile, " );\n\n" ); - Gia_ManDumpIoRanges( p, pFile, 0, fReverse ); - Gia_ManDumpIoRanges( p, pFile, 1, fReverse ); + Gia_ManDumpIoRanges( p, pFile, 0 ); + Gia_ManDumpIoRanges( p, pFile, 1 ); fprintf( pFile, "\n" ); fprintf( pFile, " wire " ); - Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL ); + Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL, 0 ); fprintf( pFile, ";\n\n" ); fprintf( pFile, " wire " ); - Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL ); + Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL, 0 ); fprintf( pFile, ";\n\n" ); fprintf( pFile, " assign { " ); - Gia_ManWriteNames( pFile, 'x', Gia_ManCiNum(p), p->vNamesIn, 8, 4, NULL ); + Gia_ManWriteNames( pFile, 'x', Gia_ManCiNum(p), p->vNamesIn, 8, 4, NULL, 1 ); fprintf( pFile, " } = { " ); - Gia_ManDumpIoList( p, pFile, 0 ); + Gia_ManDumpIoList( p, pFile, 0, 1 ); fprintf( pFile, " };\n\n" ); fprintf( pFile, " assign { " ); - Gia_ManDumpIoList( p, pFile, 1 ); + Gia_ManDumpIoList( p, pFile, 1, 1 ); fprintf( pFile, " } = { " ); - Gia_ManWriteNames( pFile, 'z', Gia_ManCoNum(p), p->vNamesOut, 9, 4, NULL ); + Gia_ManWriteNames( pFile, 'z', Gia_ManCoNum(p), p->vNamesOut, 9, 4, NULL, 1 ); fprintf( pFile, " };\n\n" ); if ( Vec_BitCount(vUsed) ) { fprintf( pFile, " wire " ); - Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed ); + Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed, 0 ); fprintf( pFile, ";\n\n" ); } if ( Vec_BitCount(vInvs) ) { fprintf( pFile, " wire " ); - Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs ); + Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs, 0 ); fprintf( pFile, ";\n\n" ); } @@ -2004,7 +2010,7 @@ void Gia_ManDumpInterface( Gia_Man_t * p, char * pFileName, int fReverse ) Vec_BitFree( vInvs ); Vec_BitFree( vUsed ); } -void Gia_ManDumpInterfaceAssign( Gia_Man_t * p, char * pFileName, int fReverse ) +void Gia_ManDumpInterfaceAssign( Gia_Man_t * p, char * pFileName ) { Gia_Obj_t * pObj; Vec_Bit_t * vInvs, * vUsed; @@ -2027,45 +2033,45 @@ void Gia_ManDumpInterfaceAssign( Gia_Man_t * p, char * pFileName, int fReverse ) Gia_ManDumpModuleName( pFile, p->pName ); fprintf( pFile, "_wrapper" ); fprintf( pFile, " ( " ); - Gia_ManDumpIoList( p, pFile, 0 ); + Gia_ManDumpIoList( p, pFile, 0, 0 ); fprintf( pFile, ", " ); - Gia_ManDumpIoList( p, pFile, 1 ); + Gia_ManDumpIoList( p, pFile, 1, 0 ); fprintf( pFile, " );\n\n" ); - Gia_ManDumpIoRanges( p, pFile, 0, fReverse ); - Gia_ManDumpIoRanges( p, pFile, 1, fReverse ); + Gia_ManDumpIoRanges( p, pFile, 0 ); + Gia_ManDumpIoRanges( p, pFile, 1 ); fprintf( pFile, "\n" ); fprintf( pFile, " wire " ); - Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL ); + Gia_ManWriteNames( pFile, 'x', Gia_ManPiNum(p), p->vNamesIn, 8, 4, NULL, 0 ); fprintf( pFile, ";\n\n" ); fprintf( pFile, " wire " ); - Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL ); + Gia_ManWriteNames( pFile, 'z', Gia_ManPoNum(p), p->vNamesOut, 9, 4, NULL, 0 ); fprintf( pFile, ";\n\n" ); fprintf( pFile, " assign { " ); - Gia_ManWriteNames( pFile, 'x', Gia_ManCiNum(p), p->vNamesIn, 8, 4, NULL ); + Gia_ManWriteNames( pFile, 'x', Gia_ManCiNum(p), p->vNamesIn, 8, 4, NULL, 1 ); fprintf( pFile, " } = { " ); - Gia_ManDumpIoList( p, pFile, 0 ); + Gia_ManDumpIoList( p, pFile, 0, 1 ); fprintf( pFile, " };\n\n" ); fprintf( pFile, " assign { " ); - Gia_ManDumpIoList( p, pFile, 1 ); + Gia_ManDumpIoList( p, pFile, 1, 1 ); fprintf( pFile, " } = { " ); - Gia_ManWriteNames( pFile, 'z', Gia_ManCoNum(p), p->vNamesOut, 9, 4, NULL ); + Gia_ManWriteNames( pFile, 'z', Gia_ManCoNum(p), p->vNamesOut, 9, 4, NULL, 1 ); fprintf( pFile, " };\n\n" ); if ( Vec_BitCount(vUsed) ) { fprintf( pFile, " wire " ); - Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed ); + Gia_ManWriteNames( pFile, 'n', Gia_ManObjNum(p), NULL, 7, 4, vUsed, 0 ); fprintf( pFile, ";\n\n" ); } if ( Vec_BitCount(vInvs) ) { fprintf( pFile, " wire " ); - Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs ); + Gia_ManWriteNames( pFile, 'i', Gia_ManObjNum(p), NULL, 7, 4, vInvs, 0 ); fprintf( pFile, ";\n\n" ); } @@ -2117,6 +2123,93 @@ void Gia_ManDumpInterfaceAssign( Gia_Man_t * p, char * pFileName, int fReverse ) } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManDumpNandLit( FILE * pFile, int nIns, int Lit, int nDigits ) +{ + if ( Lit == 0 ) + fprintf( pFile, "1\'b0" ); + else if ( Lit == 1 ) + fprintf( pFile, "1\'b1" ); + else if ( Abc_Lit2Var(Lit) <= nIns ) + fprintf( pFile, "%cn%0*d", (char)(Abc_LitIsCompl(Lit)? '~':' '), nDigits, Abc_Lit2Var(Lit) ); + else + fprintf( pFile, "%cn%0*d", (char)(Abc_LitIsCompl(Lit)? ' ':'~'), nDigits, Abc_Lit2Var(Lit) ); +} +void Gia_ManDumpVerilogNand( Gia_Man_t * p, char * pFileName ) +{ + Gia_Obj_t * pObj; int i, nPis = Gia_ManPiNum(p); + int nDigits = Abc_Base10Log( Gia_ManObjNum(p) ); + int nDigitsI = Abc_Base10Log( Gia_ManPiNum(p) ); + int nDigitsO = Abc_Base10Log( Gia_ManPoNum(p) ); + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open output file \"%s\".\n", pFileName ); + return; + } + assert( Gia_ManRegNum(p) == 0 ); + fprintf( pFile, "module " ); + Gia_ManDumpModuleName( pFile, p->pName ); + fprintf( pFile, "_wrapper" ); + fprintf( pFile, " ( " ); + if ( p->vNamesIn ) { + Gia_ManDumpIoList( p, pFile, 0, 0 ); + fprintf( pFile, ", " ); + Gia_ManDumpIoList( p, pFile, 1, 0 ); + fprintf( pFile, " );\n\n" ); + Gia_ManDumpIoRanges( p, pFile, 0 ); + Gia_ManDumpIoRanges( p, pFile, 1 ); + } + else { + fprintf( pFile, "\n " ); + Gia_ManForEachPi( p, pObj, i ) + fprintf( pFile, "%s, ", Gia_ObjGetDumpName(NULL, 'x', i, nDigitsI) ); + fprintf( pFile, "\n " ); + Gia_ManForEachPo( p, pObj, i ) + fprintf( pFile, "%s%s ", Gia_ObjGetDumpName(NULL, 'z', i, nDigitsO), i < Gia_ManPoNum(p)-1 ? ",":"" ); + fprintf( pFile, "\n);\n\n" ); + fprintf( pFile, " input" ); + Gia_ManForEachPi( p, pObj, i ) + fprintf( pFile, " %s%s", Gia_ObjGetDumpName(NULL, 'x', i, nDigitsI), i < Gia_ManPiNum(p)-1 ? ",":"" ); + fprintf( pFile, ";\n" ); + fprintf( pFile, " output" ); + Gia_ManForEachPo( p, pObj, i ) + fprintf( pFile, " %s%s", Gia_ObjGetDumpName(NULL, 'z', i, nDigitsO), i < Gia_ManPoNum(p)-1 ? ",":"" ); + fprintf( pFile, ";\n" ); + } + fprintf( pFile, "\n" ); + Gia_ManForEachPi( p, pObj, i ) + fprintf( pFile, " wire n%0*d = %s;\n", nDigits, i+1, p->vNamesIn ? (char *)Vec_PtrEntry(p->vNamesIn, i) : Gia_ObjGetDumpName(p->vNamesIn, 'x', i, nDigitsI) ); + fprintf( pFile, "\n" ); + Gia_ManForEachAnd( p, pObj, i ) + { + fprintf( pFile, " wire n%0*d = ~(", nDigits, i ); + Gia_ManDumpNandLit( pFile, nPis, Gia_ObjFaninLit0(pObj, i), nDigits ); + fprintf( pFile, " & " ); + Gia_ManDumpNandLit( pFile, nPis, Gia_ObjFaninLit1(pObj, i), nDigits ); + fprintf( pFile, ");\n" ); + } + fprintf( pFile, "\n" ); + Gia_ManForEachPo( p, pObj, i ) + { + fprintf( pFile, " assign %s = ", p->vNamesOut ? (char *)Vec_PtrEntry(p->vNamesOut, i) : Gia_ObjGetDumpName(p->vNamesOut, 'z', i, nDigitsO) ); + Gia_ManDumpNandLit( pFile, nPis, Gia_ObjFaninLit0p(p, pObj), nDigits ); + fprintf( pFile, ";\n" ); + } + fprintf( pFile, "\nendmodule\n\n" ); + fclose( pFile ); +} + /**Function************************************************************* Synopsis [Generate hierarchical design.] @@ -2189,6 +2282,8 @@ void Gia_GenSandwich( char ** pFNames, int nFNames, char * pFileName ) fprintf( pFile, "endmodule\n" ); fclose( pFile ); for ( i = 0; i < nFNames; i++ ) { + Vec_PtrFreeFree( pGias[i]->vNamesIn ); pGias[i]->vNamesIn = NULL; + Vec_PtrFreeFree( pGias[i]->vNamesOut ); pGias[i]->vNamesOut = NULL; Gia_ManDumpVerilog( pGias[i], Extra_FileNameGenericAppend(pGias[i]->pSpec, ".v"), NULL, 0, 0, 1, 0, 0 ); printf( "Dumped Verilog file \"%s\"\n", Extra_FileNameGenericAppend(pGias[i]->pSpec, ".v") ); } 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 a14a3a8bc..b9535f423 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -219,6 +219,7 @@ static int Abc_CommandInter ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandBb2Wb ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandOutdec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandNodeDup ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandWrap ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTestColor ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -599,6 +600,8 @@ static int Abc_CommandAbc9ProdAdd ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9AddFlop ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9BMiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9GenHie ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9BRecover ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9StrEco ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Test ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -996,6 +999,7 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Various", "bb2wb", Abc_CommandBb2Wb, 0 ); Cmd_CommandAdd( pAbc, "Various", "outdec", Abc_CommandOutdec, 1 ); Cmd_CommandAdd( pAbc, "Various", "nodedup", Abc_CommandNodeDup, 1 ); + Cmd_CommandAdd( pAbc, "Various", "wrap", Abc_CommandWrap, 0 ); Cmd_CommandAdd( pAbc, "Various", "testcolor", Abc_CommandTestColor, 0 ); Cmd_CommandAdd( pAbc, "Various", "test", Abc_CommandTest, 0 ); // Cmd_CommandAdd( pAbc, "Various", "qbf_solve", Abc_CommandTest, 0 ); @@ -1380,6 +1384,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&addflop", Abc_CommandAbc9AddFlop, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&bmiter", Abc_CommandAbc9BMiter, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&gen_hie", Abc_CommandAbc9GenHie, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&brecover", Abc_CommandAbc9BRecover, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&str_eco", Abc_CommandAbc9StrEco, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&test", Abc_CommandAbc9Test, 0 ); { @@ -14459,6 +14465,67 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandWrap( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + char * pFileName = NULL, * pFileName2 = NULL; + FILE * pFile = NULL, * pFile2 = NULL; + int c; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF ) + { + switch ( c ) + { + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc != globalUtilOptind + 2 ) + { + Abc_Print( 1,"Two file names are expected on the command line.\n" ); + return 0; + } + pFileName = argv[globalUtilOptind]; + pFileName2 = argv[globalUtilOptind+1]; + pFile = fopen( pFileName, "rb" ); + pFile2 = fopen( pFileName2, "wb" ); + if ( pFile && pFile2 ) + { + char Buffer[1000]; + while ( fgets( Buffer, 1000, pFile ) != NULL ) + { + if ( Buffer[strlen(Buffer)-1] == '\n' ) + Buffer[strlen(Buffer)-1] = 0; + if ( Buffer[strlen(Buffer)-1] == '\r' ) + Buffer[strlen(Buffer)-1] = 0; + fprintf( pFile2, " printf(\"%s\\n\");\n", Buffer ); + } + } + if ( pFile ) fclose(pFile); + if ( pFile2 ) fclose(pFile2); + return 0; + +usage: + Abc_Print( -2, "usage: wrap [-h] \n" ); + Abc_Print( -2, "\t wrapping lines\n" ); + Abc_Print( -2, "\t : input text file\n"); + Abc_Print( -2, "\t : output text file\n"); + return 1; + +} + /**Function************************************************************* Synopsis [] @@ -32081,8 +32148,9 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv ) char * pFileName; char ** pArgvNew; int c, nArgcNew; - int fUnique = 0; + int fUnique = 0; int fVerilog = 0; + int fVerNand = 0; int fInter = 0; int fInterComb = 0; int fAssign = 0; @@ -32094,7 +32162,7 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv ) int fSkipComment = 0; int fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "upicabmlnrsvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "upqicabmlnrsvh" ) ) != EOF ) { switch ( c ) { @@ -32104,6 +32172,9 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'p': fVerilog ^= 1; break; + case 'q': + fVerNand ^= 1; + break; case 'i': fInter ^= 1; break; @@ -32159,6 +32230,8 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_AigerWriteSimple( pGia, pFileName ); Gia_ManStop( pGia ); } + else if ( fVerNand ) + Gia_ManDumpVerilogNand( pAbc->pGia, pFileName ); else if ( fVerilog ) Gia_ManDumpVerilog( pAbc->pGia, pFileName, NULL, fVerBufs, fInter, fInterComb, fAssign, fReverse ); else if ( fMiniAig ) @@ -32170,10 +32243,11 @@ int Abc_CommandAbc9Write( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &w [-upicabmlnrsvh] \n" ); + Abc_Print( -2, "usage: &w [-upqicabmlnsvh] \n" ); Abc_Print( -2, "\t writes the current AIG into the AIGER file\n" ); Abc_Print( -2, "\t-u : toggle writing canonical AIG structure [default = %s]\n", fUnique? "yes" : "no" ); Abc_Print( -2, "\t-p : toggle writing Verilog with 'and' and 'not' [default = %s]\n", fVerilog? "yes" : "no" ); + Abc_Print( -2, "\t-q : toggle writing Verilog with NAND-gates [default = %s]\n", fVerNand? "yes" : "no" ); Abc_Print( -2, "\t-i : toggle writing the interface module in Verilog [default = %s]\n", fInter? "yes" : "no" ); Abc_Print( -2, "\t-c : toggle writing the interface module in Verilog [default = %s]\n", fInterComb? "yes" : "no" ); Abc_Print( -2, "\t-a : toggle writing the interface module with assign-statements [default = %s]\n", fAssign? "yes" : "no" ); @@ -32181,7 +32255,7 @@ usage: Abc_Print( -2, "\t-m : toggle writing MiniAIG rather than AIGER [default = %s]\n", fMiniAig? "yes" : "no" ); Abc_Print( -2, "\t-l : toggle writing MiniLUT rather than AIGER [default = %s]\n", fMiniLut? "yes" : "no" ); Abc_Print( -2, "\t-n : toggle writing \'\\n\' after \'c\' in the AIGER file [default = %s]\n", fWriteNewLine? "yes": "no" ); - Abc_Print( -2, "\t-r : toggle reversing the order of input/output bits [default = %s]\n", fReverse? "yes": "no" ); + //Abc_Print( -2, "\t-r : toggle reversing the order of input/output bits [default = %s]\n", fReverse? "yes": "no" ); Abc_Print( -2, "\t-s : toggle skipping the timestamp in the output file [default = %s]\n", fSkipComment? "yes": "no" ); Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); @@ -34423,11 +34497,11 @@ usage: ***********************************************************************/ int Abc_CommandAbc9ReadSim( Abc_Frame_t * pAbc, int argc, char ** argv ) { - int c, fOutputs = 0, nWords = 4, fTruth = 0, fVerbose = 0; + int c, fOutputs = 0, nWords = 4, fTruth = 0, fReverse = 0, fVerbose = 0; char ** pArgvNew; int nArgcNew; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Wtovh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "Wtrovh" ) ) != EOF ) { switch ( c ) { @@ -34445,6 +34519,9 @@ int Abc_CommandAbc9ReadSim( Abc_Frame_t * pAbc, int argc, char ** argv ) case 't': fTruth ^= 1; break; + case 'r': + fReverse ^= 1; + break; case 'o': fOutputs ^= 1; break; @@ -34475,7 +34552,7 @@ int Abc_CommandAbc9ReadSim( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } Vec_WrdFreeP( &pAbc->pGia->vSimsPi ); - pAbc->pGia->vSimsPi = Vec_WrdStartTruthTables( Gia_ManCiNum(pAbc->pGia) ); + pAbc->pGia->vSimsPi = fReverse ? Vec_WrdStartTruthTablesRev( Gia_ManCiNum(pAbc->pGia) ) : Vec_WrdStartTruthTables( Gia_ManCiNum(pAbc->pGia) ); Vec_WrdFreeP( &pAbc->pGia->vSimsPo ); pAbc->pGia->vSimsPo = Gia_ManSimPatSimOut( pAbc->pGia, pAbc->pGia->vSimsPi, 1 ); return 0; @@ -34518,10 +34595,11 @@ int Abc_CommandAbc9ReadSim( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &sim_read [-W num] [-tovh] \n" ); + Abc_Print( -2, "usage: &sim_read [-W num] [-trovh] \n" ); Abc_Print( -2, "\t reads simulation patterns from file\n" ); Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", nWords ); Abc_Print( -2, "\t-t : toggle creating exhaustive simulation info [default = %s]\n", fTruth? "yes": "no" ); + Abc_Print( -2, "\t-r : toggle reversing MSB and LSB input variables [default = %s]\n", fReverse? "yes": "no" ); Abc_Print( -2, "\t-o : toggle reading output information [default = %s]\n", fOutputs? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); @@ -38081,7 +38159,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 ) { @@ -38234,6 +38312,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; @@ -38298,6 +38379,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; @@ -51961,11 +52043,21 @@ int Abc_CommandAbc9BMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) char * FileName = NULL; FILE * pFile = NULL; int c, fVerbose = 0; + int bi = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + // TODO: use a flag to block Bnd_Man + 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; @@ -52010,8 +52102,9 @@ int Abc_CommandAbc9BMiter( Abc_Frame_t * pAbc, int argc, char ** argv ) 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"); @@ -52078,6 +52171,360 @@ usage: Abc_Print( -2, "\t (the PO count of should not be less than the PI count of )\n"); return 1;} +extern Bnd_Man_t* pBnd; +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9BRecover( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ); + extern void Cec4_ManSetParams( Cec_ParFra_t * pPars ); + extern Gia_Man_t * Gia_ManBoundaryMiter( Gia_Man_t * p1, Gia_Man_t * p2, int fVerbose ); + Gia_Man_t *pSpec, *pImpl_out = 0, *pSpec_out = 0, *pMiter, *pPatched = 0, *pTemp, *pBmiter; + char * FileName = NULL; + FILE * pFile = NULL; + int c, fVerbose = 0, success = 1, fEq = 1, fEqOut = 1; + + // params + Gps_Par_t Pars, * pPars = &Pars; + memset( pPars, 0, sizeof(Gps_Par_t) ); + Cec_ParCec_t ParsCec, *pParsCec = &ParsCec; + Cec_ManCecSetDefaultParams( pParsCec ); + Cec_ParFra_t ParsFra, *pParsFra = &ParsFra; + Cec4_ManSetParams( pParsFra ); + pParsFra -> fBMiterInfo = 1; + + // parse options + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vhCkeo" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + pParsFra->fVerbose ^= 1; + break; + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pParsFra->nBTLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pParsFra->nBTLimit < 0 ) + goto usage; + break; + case 'k': + pParsFra ->fUseCones ^= 1; + break; + case 'e': + fEq ^= 1; + break; + case 'o': + fEqOut ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9BRecover(): There is no AIG.\n" ); + return 0; + } + if ( argc != globalUtilOptind + 1 ) + { + printf("%d\n", argc-globalUtilOptind); + Abc_Print( -1, "Abc_CommandAbc9BRecover(): AIG should be given on the command line.\n" ); + return 0; + } + + // read spec + FileName = argv[globalUtilOptind]; + if ( (pFile = fopen( FileName, "r" )) == NULL ) + { + Abc_Print( -1, "Cannot open input file \"%s\". ", FileName ); + if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", ".blif", ".pla", ".eqn", ".bench" )) ) + Abc_Print( 1, "Did you mean \"%s\"?", FileName ); + Abc_Print( 1, "\n" ); + return 1; + } + fclose( pFile ); + pSpec = Gia_AigerRead( FileName, 0, 1, 0 ); + if ( pSpec == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9BRecover(): Cannot read the file name on the command line.\n" ); + return 0; + } + if ( Gia_ManBufNum(pSpec) == 0 ) + { + Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec should be hierarchical.\n" ); + Gia_ManStop(pSpec); + return 0; + } + + // start boundary manager + pBnd = Bnd_ManStart( pSpec, pAbc->pGia, fVerbose ); + + // check boundary + if ( 0 == Bnd_ManCheckBound( pSpec, fVerbose ) ) + { + Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec has invalid boundary.\n" ); + success = 0; + } + + if ( success ) + { + // create bmiter, run fraig, record mapping + pBmiter = Bnd_ManStackGias( pSpec, pAbc->pGia ); + pTemp = Cec4_ManSimulateTest( pBmiter, pParsFra ); + + // every output should be equivalent + // else, terminate the command (TODO?) + if ( !Bnd_ManCheckCoMerged( pTemp ) ) + { + Abc_Print( -1, "Abc_CommandAbc9BRecover(): The given spec and impl cannot be proved equivalent.\n" ); + success = 0; + } + + Gia_ManStop(pBmiter); + Gia_ManStop(pTemp); + } + + if ( success ) + { + // find + Bnd_ManFindBound( pSpec, pAbc->pGia ); + + // create spec_out and + pSpec_out = Bnd_ManGenSpecOut( pSpec ); + if ( !pSpec_out ) success = 0; + pImpl_out = Bnd_ManGenImplOut( pAbc->pGia ); + if ( !pImpl_out ) success = 0; + + // Gia_AigerWrite( pSpec_out, "spec_out.aig", 0, 0, 0 ); + // Gia_AigerWrite( pImpl_out, "impl_out.aig", 0, 0, 0 ); + // Gia_ManPrintStats( pSpec_out, pPars ); + // Gia_ManPrintStats( pImpl_out, pPars ); + + if ( !success ) + { + printf("Abc_CommandAbc9BRecover(): The generated boundary is invalid. The circuit is not changed.\n"); + } + } + + if ( success ) + { + + // check if spec_out and imnpl_out are equivalent + if ( fVerbose ) + { + if ( fEqOut ) + { + printf("Checking the equivalence of spec_out and impl_out\n"); + pMiter = Gia_ManMiter( pSpec_out, pImpl_out, 0, 1, 0, 0, 0 ); + Bnd_ManSetEqOut( Cec_ManVerify( pMiter, pParsCec ) ); + Gia_ManStop( pMiter ); + } + else + { + printf("Skip checking the equivalence of spec_out and impl_out\n"); + } + } + + // generate patched impl + if ( fVerbose ) printf("Generating patched impl\n"); + pPatched = Bnd_ManGenPatched1( pImpl_out, pSpec ); + + // // generate patched spec just for debugging + // printf("Generating patched spec\n"); + // pTemp = Bnd_ManGenPatched( pSpec_out, pAbc->pGia, pPatch ); + // printf("Checking the equivalence of patched spec and patched impl\n"); + // pMiter = Gia_ManMiter( pTemp, pPatched, 0, 1, 0, 0, 0 ); + // Cec_ManVerify( pMiter, pParsCec ); + // Gia_ManStop( pMiter ); + // printf("Checking the equivalence of patched spec and patch\n"); + // pMiter = Gia_ManMiter( pTemp, pPatch, 0, 1, 0, 0, 0 ); + // Cec_ManVerify( pMiter, pParsCec ); + // Gia_ManStop( pMiter ); + + // Gia_ManStop( pTemp ); + + // check if patched is equiv to spec + if ( fVerbose ) + { + if ( fEq ) printf("Checking the equivalence of patched impl and spec\n"); + else printf("Skip checking the equivalence of patched impl and spec\n"); + } + if ( fEq ) + { + pMiter = Gia_ManMiter( pSpec, pPatched, 0, 1, 0, 0, 0 ); + success = Cec_ManVerify( pMiter, pParsCec ); + Bnd_ManSetEqRes( success ); + if ( !success ) + { + printf("Failed. The generated AIG is not equivalent.\n"); + } + Gia_ManStop( pMiter ); + } + + } + + if ( fVerbose ) Bnd_ManPrintStats(); + + Gia_ManStop( pSpec ); + if ( pSpec_out ) Gia_ManStop( pSpec_out ); + if ( pImpl_out ) Gia_ManStop( pImpl_out ); + if ( success ) + { + if ( fEq ) printf("Success. The generated hierarchical impl is equivalent. (box size: %d -> %d)\n", Bnd_ManGetNInternal(), Bnd_ManGetNInternal() + Bnd_ManGetNExtra() ); + else printf("Success. But the equivalence in unknown (box size: %d -> %d)\n", Bnd_ManGetNInternal(), Bnd_ManGetNInternal() + Bnd_ManGetNExtra() ); + } + if (pPatched) Abc_FrameUpdateGia( pAbc, pPatched ); + Bnd_ManStop(); + + return 0; + +usage: + Abc_Print( -2, "usage: &brecover -I [-vh] \n" ); + Abc_Print( -2, "\t recover boundary using SAT-Sweeping\n" ); + Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t-k : toggle using logic cones in the SAT solver [default = %s]\n", pParsFra->fUseCones? "yes": "no" ); + Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pParsFra->nBTLimit ); + Abc_Print( -2, "\t-e : toggle checking the equivalence of the result [default = %s]\n", fEq? "yes": "no" ); + Abc_Print( -2, "\t-o : toggle checking the equivalence of the outsides in verbose [default = %s]\n", fEqOut? "yes": "no" ); + Abc_Print( -2, "\t : the implementation aig. (should be equivalent to spec)\n"); + Abc_Print( -2, "\t : the modified spec. (should be a hierarchical AIG)\n"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +int Abc_CommandAbc9StrEco( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern Gia_Man_t * Cec4_ManSimulateTest( Gia_Man_t * p, Cec_ParFra_t * pPars ); + extern void Cec4_ManSetParams( Cec_ParFra_t * pPars ); + Gia_Man_t *pMiter, *pPatch, *pPatched; + char * FileName = NULL; + FILE * pFile = NULL; + int c, success = 1; + int fVerbose = 0, fSkipStrash = 0; + + // params + Gps_Par_t Pars, * pPars = &Pars; + memset( pPars, 0, sizeof(Gps_Par_t) ); + Cec_ParCec_t ParsCec, *pParsCec = &ParsCec; + Cec_ManCecSetDefaultParams( pParsCec ); + Cec_ParFra_t ParsFra, *pParsFra = &ParsFra; + Cec4_ManSetParams( pParsFra ); + pParsFra -> fBMiterInfo = 1; + + // parse options + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vsh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 's': + fSkipStrash ^= 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 + 1 ) + { + printf("%d\n", argc-globalUtilOptind); + Abc_Print( -1, "Abc_CommandAbc9StrEco(): AIG should be given on the command line.\n" ); + return 0; + } + + // read patch + 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 ); + 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; + } + + // generate patched impl + if ( fVerbose ) printf("Generating patched impl\n"); + pPatched = Bnd_ManGenPatched2( pAbc->pGia, pPatch, fSkipStrash, fVerbose ); + + if ( pPatched ) + { + // check if patched is equiv to patch + if ( fVerbose ) printf("Checking the equivalence of patched impl and patch\n"); + pMiter = Gia_ManMiter( pPatch, pPatched, 0, 1, 0, 0, 0 ); + success = Cec_ManVerify( pMiter, pParsCec ); + if( !success ) + { + printf("Failed. The patched circuit is not equivalent.\n"); + } + Gia_ManStop( pMiter ); + Abc_FrameUpdateGia( pAbc, pPatched ); + } + + Gia_ManStop( pPatch ); + if ( success ) + { + printf("Success. The patched circuit is equivalent.\n"); + } + + return 0; + +usage: + Abc_Print( -2, "usage: &str_eco -I [-vh] \n" ); + Abc_Print( -2, "\t SAT-sweeping-based ECO\n" ); + Abc_Print( -2, "\t-v : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" ); + Abc_Print( -2, "\t-s : toggles skipping structural hash [default = %s]\n", fSkipStrash? "yes": "no" ); + Abc_Print( -2, "\t-h : print the command usage\n"); + Abc_Print( -2, "\t : the implementation aig. (should be equivalent to spec)\n"); + Abc_Print( -2, "\t : the modified spec. (should be a hierarchical AIG)\n"); + return 1; +} /**Function************************************************************* 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/base/wlc/wlc.c b/src/base/wlc/wlc.c index 3ba9be96d..91656efc8 100644 --- a/src/base/wlc/wlc.c +++ b/src/base/wlc/wlc.c @@ -677,7 +677,7 @@ Gia_Man_t * Wlc_ManGenTree( int nInputs, int Value, int nBits, int fVerbose ) ***********************************************************************/ Gia_Man_t * Wlc_ManGenProd( int nInputs, int fVerbose ) { - extern void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds ); + extern void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds, int fVerbose ); extern void Wlc_BlastMultiplier3( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds ); Vec_Int_t * vIns = Vec_IntAlloc( 2*nInputs ); Gia_Man_t * pTemp, * pNew; @@ -693,7 +693,7 @@ Gia_Man_t * Wlc_ManGenProd( int nInputs, int fVerbose ) // Vec_IntPush( vIns, Vec_IntEntry(vIns, i) ); Gia_ManHashAlloc( pNew ); - Wlc_BlastBooth( pNew, Vec_IntArray(vIns), Vec_IntArray(vIns)+nInputs, nInputs, nInputs, NULL, 0, 0, &vProds ); + Wlc_BlastBooth( pNew, Vec_IntArray(vIns), Vec_IntArray(vIns)+nInputs, nInputs, nInputs, NULL, 0, 0, &vProds, 0 ); //Wlc_BlastMultiplier3( pNew, Vec_IntArray(vIns), Vec_IntArray(vIns)+nInputs, nInputs, nInputs, NULL, 0, 0, &vProds ); //Vec_WecPrint( vProds, 0 ); Wlc_ManGenTreeOne( pNew, vProds, 1, fVerbose ); diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index 47d08da62..d3b2b3a05 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -1050,7 +1050,7 @@ void Wlc_BlastReduceMatrix2( Gia_Man_t * pNew, Vec_Wec_t * vProds, Vec_Int_t * v } -void Wlc_BlastMultiplier3( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds ) +void Wlc_BlastMultiplier3( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds, int fVerbose ) { Vec_Wec_t * vProds = Vec_WecStart( nArgA + nArgB ); Vec_Wec_t * vLevels = Vec_WecStart( nArgA + nArgB ); @@ -1064,13 +1064,17 @@ void Wlc_BlastMultiplier3( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA } if ( fSigned ) { - Vec_WecPush( vProds, nArgA, 1 ); - Vec_WecPush( vLevels, nArgA, 0 ); + Vec_WecPush( vProds, nArgB-1, 1 ); + Vec_WecPush( vLevels, nArgB-1, 0 ); + + Vec_WecPush( vProds, nArgA-1, 1 ); + Vec_WecPush( vLevels, nArgA-1, 0 ); Vec_WecPush( vProds, nArgA+nArgB-1, 1 ); Vec_WecPush( vLevels, nArgA+nArgB-1, 0 ); } - + if ( fVerbose ) + Vec_WecPrint( vProds, 0 ); if ( pvProds ) *pvProds = Vec_WecDup(vProds); else @@ -1117,7 +1121,7 @@ void Wlc_BlastDecoder( Gia_Man_t * pNew, int * pNum, int nNum, Vec_Int_t * vTmp, Vec_IntPush( vRes, iMint ); } } -void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds ) +void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds, int fVerbose ) { Vec_Wec_t * vProds = Vec_WecStart( nArgA + nArgB + 3 ); Vec_Wec_t * vLevels = Vec_WecStart( nArgA + nArgB + 3 ); @@ -1194,7 +1198,10 @@ void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int Vec_WecPush( vProds, k, Neg ); Vec_WecPush( vLevels, k, 0 ); } - //Vec_WecPrint( vProds, 0 ); + //Vec_WecShrink( vProds, nArgA + nArgB ); + //Vec_WecShrink( vLevels, nArgA + nArgB ); + if ( fVerbose ) + Vec_WecPrint( vProds, 0 ); //Wlc_BlastPrintMatrix( pNew, vProds, 1 ); //printf( "Cutoff ID for partial products = %d.\n", Gia_ManObjNum(pNew) ); if ( pvProds ) @@ -1832,9 +1839,9 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn ) if ( Wlc_NtkCountConstBits(pArg0, nRangeMax) < Wlc_NtkCountConstBits(pArg1, nRangeMax) ) ABC_SWAP( int *, pArg0, pArg1 ); if ( pPar->fBooth ) - Wlc_BlastBooth( pNew, pArg0, pArg1, nRange0, nRange1, vRes, fSigned, pPar->fCla, NULL ); + Wlc_BlastBooth( pNew, pArg0, pArg1, nRange0, nRange1, vRes, fSigned, pPar->fCla, NULL, pParIn->fVerbose ); else if ( pPar->fCla ) - Wlc_BlastMultiplier3( pNew, pArg0, pArg1, nRange0, nRange1, vRes, Wlc_ObjIsSignedFanin01(p, pObj), pPar->fCla, NULL ); + Wlc_BlastMultiplier3( pNew, pArg0, pArg1, nRange0, nRange1, vRes, Wlc_ObjIsSignedFanin01(p, pObj), pPar->fCla, NULL, pParIn->fVerbose ); else Wlc_BlastMultiplier( pNew, pArg0, pArg1, nRangeMax, nRangeMax, vTemp2, vRes, fSigned ); //Wlc_BlastMultiplierC( pNew, pArg0, pArg1, nRangeMax, nRangeMax, vTemp2, vRes, fSigned ); diff --git a/src/base/wln/wlnBlast.c b/src/base/wln/wlnBlast.c index 776cdd902..c3281a2e0 100644 --- a/src/base/wln/wlnBlast.c +++ b/src/base/wln/wlnBlast.c @@ -69,7 +69,7 @@ void Rtl_NtkBlastNode( Gia_Man_t * pNew, int Type, int nIns, Vec_Int_t * vDatas, extern int Wlc_BlastAdder( Gia_Man_t * pNew, int * pAdd0, int * pAdd1, int nBits, int Carry ); // result is in pAdd0 extern void Wlc_BlastSubtract( Gia_Man_t * pNew, int * pAdd0, int * pAdd1, int nBits, int Carry ); // result is in pAdd0 extern int Wlc_NtkCountConstBits( int * pArray, int nSize ); - extern void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds ); + extern void Wlc_BlastBooth( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds, int fVerbose ); extern void Wlc_BlastMultiplier3( Gia_Man_t * pNew, int * pArgA, int * pArgB, int nArgA, int nArgB, Vec_Int_t * vRes, int fSigned, int fCla, Vec_Wec_t ** pvProds ); extern void Wlc_BlastZeroCondition( Gia_Man_t * pNew, int * pDiv, int nDiv, Vec_Int_t * vRes ); extern void Wlc_BlastDividerTop( Gia_Man_t * pNew, int * pNum, int nNum, int * pDiv, int nDiv, int fQuo, Vec_Int_t * vRes, int fNonRest ); @@ -303,7 +303,7 @@ void Rtl_NtkBlastNode( Gia_Man_t * pNew, int Type, int nIns, Vec_Int_t * vDatas, if ( Wlc_NtkCountConstBits(Vec_IntArray(vArg0), Vec_IntSize(vArg0)) < Wlc_NtkCountConstBits(Vec_IntArray(vArg1), Vec_IntSize(vArg1)) ) ABC_SWAP( Vec_Int_t, *vArg0, *vArg1 ) if ( fBooth ) - Wlc_BlastBooth( pNew, Vec_IntArray(vArg0), Vec_IntArray(vArg1), Vec_IntSize(vArg0), Vec_IntSize(vArg1), vRes, fSigned, fCla, NULL ); + Wlc_BlastBooth( pNew, Vec_IntArray(vArg0), Vec_IntArray(vArg1), Vec_IntSize(vArg0), Vec_IntSize(vArg1), vRes, fSigned, fCla, NULL, 0 ); else Wlc_BlastMultiplier3( pNew, Vec_IntArray(vArg0), Vec_IntArray(vArg1), Vec_IntSize(vArg0), Vec_IntSize(vArg1), vRes, fSigned, fCla, NULL ); if ( nRange > Vec_IntSize(vRes) ) 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/misc/vec/vecWrd.h b/src/misc/vec/vecWrd.h index aa16771ef..b0d16efe6 100644 --- a/src/misc/vec/vecWrd.h +++ b/src/misc/vec/vecWrd.h @@ -195,6 +195,32 @@ static inline Vec_Wrd_t * Vec_WrdStartTruthTables( int nVars ) } return p; } +static inline Vec_Wrd_t * Vec_WrdStartTruthTablesRev( int nVars ) +{ + Vec_Wrd_t * p; + unsigned Masks[5] = { 0xAAAAAAAA, 0xCCCCCCCC, 0xF0F0F0F0, 0xFF00FF00, 0xFFFF0000 }; + int i, k, nWords; + nWords = nVars <= 6 ? 1 : (1 << (nVars - 6)); + p = Vec_WrdStart( nWords * nVars ); + for ( i = 0; i < nVars; i++ ) + { + unsigned * pTruth = (unsigned *)(p->pArray + nWords * (nVars-1-i)); + if ( i < 5 ) + { + for ( k = 0; k < 2*nWords; k++ ) + pTruth[k] = Masks[i]; + } + else + { + for ( k = 0; k < 2*nWords; k++ ) + if ( k & (1 << (i-5)) ) + pTruth[k] = ~(unsigned)0; + else + pTruth[k] = 0; + } + } + return p; +} static inline int Vec_WrdShiftOne( Vec_Wrd_t * p, int nWords ) { int i, nObjs = p->nSize/nWords; diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index d11bca3c3..c9aa96658 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -120,6 +120,8 @@ struct Cec_ParFra_t_ int fVeryVerbose; // verbose stats 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 281deb0e9..b198c7ffe 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -219,6 +219,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************************************************************* @@ -1781,8 +1782,10 @@ void Gia_ManRemoveWrongChoices( Gia_Man_t * p ) } //Abc_Print( 1, "Removed %d wrong choices.\n", Counter ); } + 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; @@ -1878,8 +1881,16 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p if ( pRepr == NULL ) continue; } + int id_obj = Gia_ObjId( p, pObj ); + int id_repr = Gia_ObjId( p, pRepr ); + if ( Abc_Lit2Var(pObj->Value) == Abc_Lit2Var(pRepr->Value) ) { + if ( pPars->fBMiterInfo ) + { + 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 ) @@ -1887,8 +1898,26 @@ 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 (pPars->fBMiterInfo){ + + 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 ); + + + } } + + if ( pPars->fBMiterInfo ) + { + // print + Bnd_ManFinalizeMappings(); + // Bnd_ManPrintMappings(); + } + if ( p->iPatsPi > 0 ) { abctime clk2 = Abc_Clock(); @@ -1937,6 +1966,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 ); + return pNew; } void Cec4_ManSimulateTest2( Gia_Man_t * p, int nConfs, int fVerbose ) diff --git a/src/sat/bsat2/Alg.h b/src/sat/bsat2/Alg.h index 3e0745f1d..87004fce8 100644 --- a/src/sat/bsat2/Alg.h +++ b/src/sat/bsat2/Alg.h @@ -21,7 +21,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_Alg_h #define Minisat_Alg_h -#include "Vec.h" +#include "sat/bsat2/Vec.h" + +ABC_NAMESPACE_CXX_HEADER_START namespace Minisat { @@ -81,4 +83,6 @@ static inline void append(const vec& from, vec& to){ copy(from, to, true); //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/Alloc.h b/src/sat/bsat2/Alloc.h index 7f506cb5a..a9786a9a8 100644 --- a/src/sat/bsat2/Alloc.h +++ b/src/sat/bsat2/Alloc.h @@ -21,8 +21,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_Alloc_h #define Minisat_Alloc_h -#include "XAlloc.h" -#include "Vec.h" +#include "sat/bsat2/XAlloc.h" +#include "sat/bsat2/Vec.h" + +ABC_NAMESPACE_CXX_HEADER_START namespace Minisat { @@ -128,4 +130,6 @@ RegionAllocator::alloc(int size) //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/Dimacs.h b/src/sat/bsat2/Dimacs.h index f26f152be..0e7ad925a 100644 --- a/src/sat/bsat2/Dimacs.h +++ b/src/sat/bsat2/Dimacs.h @@ -23,8 +23,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include -#include "ParseUtils.h" -#include "SolverTypes.h" +#include "sat/bsat2/ParseUtils.h" +#include "sat/bsat2/SolverTypes.h" + +ABC_NAMESPACE_CXX_HEADER_START namespace Minisat { @@ -86,4 +88,6 @@ static void parse_DIMACS(gzFile input_stream, Solver& S) { //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/Heap.h b/src/sat/bsat2/Heap.h index e5b4ddb56..ae50c4b57 100644 --- a/src/sat/bsat2/Heap.h +++ b/src/sat/bsat2/Heap.h @@ -21,7 +21,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_Heap_h #define Minisat_Heap_h -#include "Vec.h" +#include "sat/bsat2/Vec.h" + +ABC_NAMESPACE_CXX_HEADER_START namespace Minisat { @@ -146,4 +148,6 @@ class Heap { //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/IntTypes.h b/src/sat/bsat2/IntTypes.h index 1c011e83a..fdcd3d9f7 100644 --- a/src/sat/bsat2/IntTypes.h +++ b/src/sat/bsat2/IntTypes.h @@ -44,4 +44,6 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA //================================================================================================= +#include + #endif diff --git a/src/sat/bsat2/MainSat.cpp b/src/sat/bsat2/MainSat.cpp index 1f61f9eec..855466263 100644 --- a/src/sat/bsat2/MainSat.cpp +++ b/src/sat/bsat2/MainSat.cpp @@ -23,11 +23,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include "misc/zlib/zlib.h" -#include "System.h" -#include "ParseUtils.h" -#include "Options.h" -#include "Dimacs.h" -#include "Solver.h" +#include "sat/bsat2/System.h" +#include "sat/bsat2/ParseUtils.h" +#include "sat/bsat2/Options.h" +#include "sat/bsat2/Dimacs.h" +#include "sat/bsat2/Solver.h" + +ABC_NAMESPACE_IMPL_START using namespace Minisat; @@ -195,3 +197,6 @@ extern "C" int MainSat(int argc, char** argv) exit(0); } } + + +ABC_NAMESPACE_IMPL_END diff --git a/src/sat/bsat2/MainSimp.cpp b/src/sat/bsat2/MainSimp.cpp index 4a8909210..2d0ad109e 100644 --- a/src/sat/bsat2/MainSimp.cpp +++ b/src/sat/bsat2/MainSimp.cpp @@ -27,11 +27,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #endif -#include "System.h" -#include "ParseUtils.h" -#include "Options.h" -#include "Dimacs.h" -#include "SimpSolver.h" +#include "sat/bsat2/System.h" +#include "sat/bsat2/ParseUtils.h" +#include "sat/bsat2/Options.h" +#include "sat/bsat2/Dimacs.h" +#include "sat/bsat2/SimpSolver.h" + +ABC_NAMESPACE_IMPL_START using namespace Minisat; @@ -204,3 +206,6 @@ extern "C" int MainSimp(int argc, char** argv) exit(0); } } + + +ABC_NAMESPACE_IMPL_END diff --git a/src/sat/bsat2/Map.h b/src/sat/bsat2/Map.h index 1dd22a06d..374e76c9b 100644 --- a/src/sat/bsat2/Map.h +++ b/src/sat/bsat2/Map.h @@ -20,8 +20,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_Map_h #define Minisat_Map_h -#include "IntTypes.h" -#include "Vec.h" +#include "sat/bsat2/IntTypes.h" +#include "sat/bsat2/Vec.h" + +ABC_NAMESPACE_CXX_HEADER_START namespace Minisat { @@ -190,4 +192,6 @@ class Map { //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/Options.cpp b/src/sat/bsat2/Options.cpp index b30cff0e5..a0a3817d8 100644 --- a/src/sat/bsat2/Options.cpp +++ b/src/sat/bsat2/Options.cpp @@ -17,9 +17,11 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#include "Sort.h" -#include "Options.h" -#include "ParseUtils.h" +#include "sat/bsat2/Sort.h" +#include "sat/bsat2/Options.h" +#include "sat/bsat2/ParseUtils.h" + +ABC_NAMESPACE_IMPL_START using namespace Minisat; @@ -43,10 +45,12 @@ int Minisat::parseOptions(int& argc, char** argv, bool strict) } if (!parsed_ok) + { if (strict && match(argv[i], "-")) { fprintf(stderr, "ERROR! Unknown flag \"%s\". Use '--%shelp' for help.\n", argv[i], Option::getHelpPrefixString()); return 0; } // exit(0); else argv[j++] = argv[i]; + } } } @@ -91,3 +95,5 @@ int Minisat::printUsageAndExit (int argc, char** argv, bool verbose) return 0; } + +ABC_NAMESPACE_IMPL_END diff --git a/src/sat/bsat2/Options.h b/src/sat/bsat2/Options.h index 439cb8f21..00d46d352 100644 --- a/src/sat/bsat2/Options.h +++ b/src/sat/bsat2/Options.h @@ -25,9 +25,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include -#include "IntTypes.h" -#include "Vec.h" -#include "ParseUtils.h" +#include "sat/bsat2/IntTypes.h" +#include "sat/bsat2/Vec.h" +#include "sat/bsat2/ParseUtils.h" + +ABC_NAMESPACE_CXX_HEADER_START namespace Minisat { @@ -60,7 +62,7 @@ class Option struct OptionLt { bool operator()(const Option* x, const Option* y) { int test1 = strcmp(x->category, y->category); - return test1 < 0 || test1 == 0 && strcmp(x->type_name, y->type_name) < 0; + return test1 < 0 || ( test1 == 0 && strcmp(x->type_name, y->type_name) < 0 ); } }; @@ -384,4 +386,6 @@ class BoolOption : public Option //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/ParseUtils.h b/src/sat/bsat2/ParseUtils.h index 8e0f9c890..b7325f174 100644 --- a/src/sat/bsat2/ParseUtils.h +++ b/src/sat/bsat2/ParseUtils.h @@ -26,6 +26,8 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include "misc/zlib/zlib.h" +ABC_NAMESPACE_CXX_HEADER_START + namespace Minisat { //------------------------------------------------------------------------------------------------- @@ -119,4 +121,6 @@ static bool eagerMatch(B& in, const char* str) { //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/Queue.h b/src/sat/bsat2/Queue.h index 11b429115..8ff65b87b 100644 --- a/src/sat/bsat2/Queue.h +++ b/src/sat/bsat2/Queue.h @@ -21,7 +21,9 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_Queue_h #define Minisat_Queue_h -#include "Vec.h" +#include "sat/bsat2/Vec.h" + +ABC_NAMESPACE_CXX_HEADER_START namespace Minisat { @@ -66,4 +68,6 @@ public: //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/SimpSolver.cpp b/src/sat/bsat2/SimpSolver.cpp index 5a7a006c2..c07ec5b97 100644 --- a/src/sat/bsat2/SimpSolver.cpp +++ b/src/sat/bsat2/SimpSolver.cpp @@ -18,9 +18,11 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#include "Sort.h" -#include "SimpSolver.h" -#include "System.h" +#include "sat/bsat2/Sort.h" +#include "sat/bsat2/SimpSolver.h" +#include "sat/bsat2/System.h" + +ABC_NAMESPACE_IMPL_START using namespace Minisat; @@ -228,10 +230,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, vec& ou if (var(qs[i]) != v){ for (j = 0; j < ps.size(); j++) if (var(ps[j]) == var(qs[i])) + { if (ps[j] == ~qs[i]) return false; else goto next; + } out_clause.push(qs[i]); } next:; @@ -262,10 +266,12 @@ bool SimpSolver::merge(const Clause& _ps, const Clause& _qs, Var v, int& size) if (var(__qs[i]) != v){ for (int j = 0; j < ps.size(); j++) if (var(__ps[j]) == var(__qs[i])) + { if (__ps[j] == ~__qs[i]) return false; else goto next; + } size++; } next:; @@ -718,3 +724,5 @@ void SimpSolver::garbageCollect() ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); to.moveTo(ca); } + +ABC_NAMESPACE_IMPL_END \ No newline at end of file diff --git a/src/sat/bsat2/SimpSolver.h b/src/sat/bsat2/SimpSolver.h index e24b0e430..ad02c6dff 100644 --- a/src/sat/bsat2/SimpSolver.h +++ b/src/sat/bsat2/SimpSolver.h @@ -21,9 +21,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_SimpSolver_h #define Minisat_SimpSolver_h -#include "Queue.h" -#include "Solver.h" +#include "sat/bsat2/Queue.h" +#include "sat/bsat2/Solver.h" +ABC_NAMESPACE_CXX_HEADER_START namespace Minisat { @@ -194,4 +195,6 @@ inline lbool SimpSolver::solveLimited (const vec& assumps, bool do_simp, bo //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/Solver.cpp b/src/sat/bsat2/Solver.cpp index 0f8b415a9..602692a8b 100644 --- a/src/sat/bsat2/Solver.cpp +++ b/src/sat/bsat2/Solver.cpp @@ -20,8 +20,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include -#include "Sort.h" -#include "Solver.h" +#include "sat/bsat2/Sort.h" +#include "sat/bsat2/Solver.h" + +ABC_NAMESPACE_IMPL_START using namespace Minisat; @@ -209,7 +211,7 @@ void Solver::cancelUntil(int level) { for (int c = trail.size()-1; c >= trail_lim[level]; c--){ Var x = var(trail[c]); assigns [x] = l_Undef; - if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last()) + if (phase_saving > 1 || ((phase_saving == 1) && c > trail_lim.last())) polarity[x] = sign(trail[c]); insertVarOrder(x); } qhead = trail_lim[level]; @@ -657,7 +659,7 @@ lbool Solver::search(int nof_conflicts) }else{ // NO CONFLICT - if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){ + if ( (nof_conflicts >= 0 && conflictC >= nof_conflicts) || !withinBudget()){ // Reached bound on number of conflicts: progress_estimate = progressEstimate(); cancelUntil(0); @@ -922,3 +924,5 @@ void Solver::garbageCollect() ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size); to.moveTo(ca); } + +ABC_NAMESPACE_IMPL_END diff --git a/src/sat/bsat2/Solver.h b/src/sat/bsat2/Solver.h index fc0bb4ba2..9c9a30ee3 100644 --- a/src/sat/bsat2/Solver.h +++ b/src/sat/bsat2/Solver.h @@ -21,12 +21,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_Solver_h #define Minisat_Solver_h -#include "Vec.h" -#include "Heap.h" -#include "Alg.h" -#include "Options.h" -#include "SolverTypes.h" +#include "sat/bsat2/Vec.h" +#include "sat/bsat2/Heap.h" +#include "sat/bsat2/Alg.h" +#include "sat/bsat2/Options.h" +#include "sat/bsat2/SolverTypes.h" +ABC_NAMESPACE_CXX_HEADER_START namespace Minisat { @@ -370,4 +371,6 @@ inline void Solver::toDimacs (const char* file, Lit p, Lit q, Lit r){ ve //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/SolverTypes.h b/src/sat/bsat2/SolverTypes.h index f34deca1c..64fbe980e 100644 --- a/src/sat/bsat2/SolverTypes.h +++ b/src/sat/bsat2/SolverTypes.h @@ -24,11 +24,13 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include -#include "IntTypes.h" -#include "Alg.h" -#include "Vec.h" -#include "Map.h" -#include "Alloc.h" +#include "sat/bsat2/IntTypes.h" +#include "sat/bsat2/Alg.h" +#include "sat/bsat2/Vec.h" +#include "sat/bsat2/Map.h" +#include "sat/bsat2/Alloc.h" + +ABC_NAMESPACE_CXX_HEADER_START namespace Minisat { @@ -404,4 +406,6 @@ inline void Clause::strengthen(Lit p) //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/Sort.h b/src/sat/bsat2/Sort.h index cc96486d8..7ce99ea46 100644 --- a/src/sat/bsat2/Sort.h +++ b/src/sat/bsat2/Sort.h @@ -21,11 +21,12 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #ifndef Minisat_Sort_h #define Minisat_Sort_h -#include "Vec.h" +#include "sat/bsat2/Vec.h" //================================================================================================= // Some sorting algorithms for vec's +ABC_NAMESPACE_CXX_HEADER_START namespace Minisat { @@ -95,4 +96,6 @@ template void sort(vec& v) { //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/System.cpp b/src/sat/bsat2/System.cpp index c2d6259e2..2c64e7fea 100644 --- a/src/sat/bsat2/System.cpp +++ b/src/sat/bsat2/System.cpp @@ -18,13 +18,15 @@ DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE. **************************************************************************************************/ -#include "System.h" +#include "sat/bsat2/System.h" #if defined(__linux__) #include #include +ABC_NAMESPACE_IMPL_START + using namespace Minisat; // TODO: split the memory reading functions into two: one for reading high-watermark of RSS, and @@ -72,24 +74,40 @@ double Minisat::memUsedPeak() { double peak = memReadPeak() / 1024; return peak == 0 ? memUsed() : peak; } +ABC_NAMESPACE_IMPL_END + #elif defined(__FreeBSD__) +ABC_NAMESPACE_IMPL_START + double Minisat::memUsed(void) { struct rusage ru; getrusage(RUSAGE_SELF, &ru); return (double)ru.ru_maxrss / 1024; } double MiniSat::memUsedPeak(void) { return memUsed(); } +ABC_NAMESPACE_IMPL_END #elif defined(__APPLE__) #include +ABC_NAMESPACE_IMPL_START + double Minisat::memUsed(void) { malloc_statistics_t t; malloc_zone_statistics(NULL, &t); return (double)t.max_size_in_use / (1024*1024); } +ABC_NAMESPACE_IMPL_END + #else + +ABC_NAMESPACE_IMPL_START + double Minisat::memUsed() { return 0; } double Minisat::memUsedPeak() { return 0; } + +ABC_NAMESPACE_IMPL_END + #endif + diff --git a/src/sat/bsat2/System.h b/src/sat/bsat2/System.h index d776c880c..f5ed5fa13 100644 --- a/src/sat/bsat2/System.h +++ b/src/sat/bsat2/System.h @@ -22,13 +22,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #define Minisat_System_h #if defined(__linux__) -#include +//#include #endif -#include "IntTypes.h" +#include "sat/bsat2/IntTypes.h" //------------------------------------------------------------------------------------------------- +ABC_NAMESPACE_CXX_HEADER_START + namespace Minisat { static inline double cpuTime(void); // CPU-time in seconds. @@ -37,24 +39,35 @@ extern double memUsedPeak(); // Peak-memory in mega bytes (returns 0 for } +ABC_NAMESPACE_CXX_HEADER_END + //------------------------------------------------------------------------------------------------- // Implementation of inline functions: #if defined(_MSC_VER) || defined(__MINGW32__) #include +ABC_NAMESPACE_CXX_HEADER_START + static inline double Minisat::cpuTime(void) { return (double)clock() / CLOCKS_PER_SEC; } +ABC_NAMESPACE_CXX_HEADER_END + #else #include #include #include +ABC_NAMESPACE_CXX_HEADER_START + static inline double Minisat::cpuTime(void) { struct rusage ru; getrusage(RUSAGE_SELF, &ru); return (double)ru.ru_utime.tv_sec + (double)ru.ru_utime.tv_usec / 1000000; } -#endif +ABC_NAMESPACE_CXX_HEADER_END + +#endif + #endif diff --git a/src/sat/bsat2/Vec.h b/src/sat/bsat2/Vec.h index f0e07d016..f5f5499ea 100644 --- a/src/sat/bsat2/Vec.h +++ b/src/sat/bsat2/Vec.h @@ -24,8 +24,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include -#include "IntTypes.h" -#include "XAlloc.h" +#include "sat/bsat2/IntTypes.h" +#include "sat/bsat2/XAlloc.h" + +ABC_NAMESPACE_CXX_HEADER_START namespace Minisat { @@ -91,7 +93,6 @@ public: void moveTo(vec& dest) { dest.clear(true); dest.data = data; dest.sz = sz; dest.cap = cap; data = NULL; sz = 0; cap = 0; } }; - template void vec::capacity(int min_cap) { if (cap >= min_cap) return; @@ -127,4 +128,6 @@ void vec::clear(bool dealloc) { //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/XAlloc.h b/src/sat/bsat2/XAlloc.h index 1da176028..fdebe502a 100644 --- a/src/sat/bsat2/XAlloc.h +++ b/src/sat/bsat2/XAlloc.h @@ -24,6 +24,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA #include #include +#include + +ABC_NAMESPACE_CXX_HEADER_START + namespace Minisat { //================================================================================================= @@ -42,4 +46,6 @@ static inline void* xrealloc(void *ptr, size_t size) //================================================================================================= } +ABC_NAMESPACE_CXX_HEADER_END + #endif diff --git a/src/sat/bsat2/module.make b/src/sat/bsat2/module.make index ddd11b1b9..87cdc11ca 100644 --- a/src/sat/bsat2/module.make +++ b/src/sat/bsat2/module.make @@ -1,6 +1,4 @@ SRC += src/sat/bsat2/AbcApi.cpp \ - src/sat/bsat2/MainSat.cpp \ - src/sat/bsat2/MainSimp.cpp \ src/sat/bsat2/Options.cpp \ src/sat/bsat2/SimpSolver.cpp \ src/sat/bsat2/Solver.cpp \