From 236d412255e5007adac97c05e759bfd5069bc1c1 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 7 May 2016 19:47:02 -0700 Subject: Experiments with CEC for arithmetic circuits. --- src/aig/gia/gia.h | 6 + src/aig/gia/giaBalLut.c | 4 +- src/aig/gia/giaDfs.c | 2 +- src/aig/gia/giaDup.c | 490 +++++++++++++++--- src/aig/gia/giaFadds.c | 1109 ----------------------------------------- src/aig/gia/giaHash.c | 1 + src/aig/gia/giaMuxes.c | 2 +- src/aig/gia/giaPolyn.c | 516 ------------------- src/aig/gia/giaShow.c | 4 +- src/aig/gia/module.make | 2 - src/base/abci/abc.c | 274 +++++++++- src/base/wlc/wlc.h | 1 + src/base/wlc/wlcBlast.c | 1 + src/base/wlc/wlcNtk.c | 5 + src/base/wlc/wlcReadVer.c | 1 + src/misc/vec/vecInt.h | 27 + src/proof/acec/acec.c | 52 ++ src/proof/acec/acec.h | 68 +++ src/proof/acec/acecCore.c | 60 +++ src/proof/acec/acecFadds.c | 1183 ++++++++++++++++++++++++++++++++++++++++++++ src/proof/acec/acecInt.h | 76 +++ src/proof/acec/acecOrder.c | 178 +++++++ src/proof/acec/acecPolyn.c | 371 ++++++++++++++ src/proof/acec/acecUtil.c | 87 ++++ src/proof/acec/module.make | 5 + 25 files changed, 2827 insertions(+), 1698 deletions(-) delete mode 100644 src/aig/gia/giaFadds.c delete mode 100644 src/aig/gia/giaPolyn.c create mode 100644 src/proof/acec/acec.c create mode 100644 src/proof/acec/acec.h create mode 100644 src/proof/acec/acecCore.c create mode 100644 src/proof/acec/acecFadds.c create mode 100644 src/proof/acec/acecInt.h create mode 100644 src/proof/acec/acecOrder.c create mode 100644 src/proof/acec/acecPolyn.c create mode 100644 src/proof/acec/acecUtil.c create mode 100644 src/proof/acec/module.make (limited to 'src') diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 82e82cb2..390dbafb 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1149,6 +1149,7 @@ extern Gia_Man_t * Gia_ManDupCofAllInt( Gia_Man_t * p, Vec_Int_t * vSigs extern Gia_Man_t * Gia_ManDupCofAll( Gia_Man_t * p, int nFanLim, int fVerbose ); /*=== giaDfs.c ============================================================*/ extern void Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vSupp ); +extern void Gia_ManCollectAnds_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vNodes ); extern void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes, Vec_Int_t * vLeaves ); extern Vec_Int_t * Gia_ManCollectNodesCis( Gia_Man_t * p, int * pNodes, int nNodes ); extern int Gia_ManSuppSize( Gia_Man_t * p, int * pNodes, int nNodes ); @@ -1209,10 +1210,15 @@ extern Gia_Man_t * Gia_ManTransformToDual( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias ); extern Gia_Man_t * Gia_ManDupWithConstraints( Gia_Man_t * p, Vec_Int_t * vPoTypes ); extern Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis ); +extern Gia_Man_t * Gia_ManDupAndCones( Gia_Man_t * p, int * pAnds, int nAnds, int fTrimPis ); extern Gia_Man_t * Gia_ManDupOneHot( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupLevelized( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupFromVecs( Gia_Man_t * p, Vec_Int_t * vCis, Vec_Int_t * vAnds, Vec_Int_t * vCos, int nRegs ); extern Gia_Man_t * Gia_ManDupSliced( Gia_Man_t * p, int nSuppMax ); +extern Gia_Man_t * Gia_ManDupDemiter( Gia_Man_t * p, int fVerbose ); +extern Gia_Man_t * Gia_ManDemiterToDual( Gia_Man_t * p ); +extern int Gia_ManDemiterDual( Gia_Man_t * p, Gia_Man_t ** pp0, Gia_Man_t ** pp1 ); +extern int Gia_ManDemiterTwoWords( Gia_Man_t * p, Gia_Man_t ** pp0, Gia_Man_t ** pp1 ); /*=== giaEdge.c ==========================================================*/ extern void Gia_ManEdgeFromArray( Gia_Man_t * p, Vec_Int_t * vArray ); extern Vec_Int_t * Gia_ManEdgeToArray( Gia_Man_t * p ); diff --git a/src/aig/gia/giaBalLut.c b/src/aig/gia/giaBalLut.c index 73d2a6fb..4402e36f 100644 --- a/src/aig/gia/giaBalLut.c +++ b/src/aig/gia/giaBalLut.c @@ -568,7 +568,7 @@ static inline void Vec_IntSelectSortCostLit( Vec_Int_t * vSuper, Vec_Int_t * vCo ABC_SWAP( int, pArray[i], pArray[best_i] ); } } -static inline void Vec_IntPushOrderCost( Vec_Int_t * vSuper, Vec_Int_t * vCosts, int iLit ) +static inline void Vec_IntPushOrderCost2( Vec_Int_t * vSuper, Vec_Int_t * vCosts, int iLit ) { int i, nSize, * pArray; Vec_IntPush( vSuper, iLit ); @@ -853,7 +853,7 @@ static inline int Gia_ManBalanceGate( Gia_Man_t * pNew, Gia_Obj_t * pObj, Vec_In else iLit = Gia_ManHashAnd( pNew, iBest, kBest ); Bal_ManSetGateLevel( p, pObj, iLit ); - Vec_IntPushOrderCost( vSuper, p->vCosts, iLit ); + Vec_IntPushOrderCost2( vSuper, p->vCosts, iLit ); } } // consider trivial case diff --git a/src/aig/gia/giaDfs.c b/src/aig/gia/giaDfs.c index 60edef81..12cae940 100644 --- a/src/aig/gia/giaDfs.c +++ b/src/aig/gia/giaDfs.c @@ -136,7 +136,7 @@ void Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vN Gia_Obj_t * pObj = Gia_ManObj( p, pNodes[i] ); if ( Gia_ObjIsCo(pObj) ) Gia_ManCollectAnds_rec( p, Gia_ObjFaninId0(pObj, pNodes[i]), vNodes ); - else + else if ( Gia_ObjIsAnd(pObj) ) Gia_ManCollectAnds_rec( p, pNodes[i], vNodes ); } } diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index e204fb55..a01c93fd 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -2949,6 +2949,65 @@ Gia_Man_t * Gia_ManDupCones( Gia_Man_t * p, int * pPos, int nPos, int fTrimPis ) Vec_PtrFree( vRoots ); return pNew; +} +Gia_Man_t * Gia_ManDupAndCones( Gia_Man_t * p, int * pAnds, int nAnds, int fTrimPis ) +{ + Gia_Man_t * pNew; + Vec_Ptr_t * vLeaves, * vNodes, * vRoots; + Gia_Obj_t * pObj; + int i; + + // collect initial POs + vLeaves = Vec_PtrAlloc( 100 ); + vNodes = Vec_PtrAlloc( 100 ); + vRoots = Vec_PtrAlloc( 100 ); + for ( i = 0; i < nAnds; i++ ) +// Vec_PtrPush( vRoots, Gia_ManPo(p, pPos[i]) ); + Vec_PtrPush( vRoots, Gia_ManObj(p, pAnds[i]) ); + + // mark internal nodes + Gia_ManIncrementTravId( p ); + Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) ); + Vec_PtrForEachEntry( Gia_Obj_t *, vRoots, pObj, i ) + Gia_ManDupCones_rec( p, pObj, vLeaves, vNodes, vRoots ); + Vec_PtrSort( vLeaves, (int (*)(void))Gia_ObjCompareByCioId ); + + // start the new manager +// Gia_ManFillValue( p ); + pNew = Gia_ManStart( Vec_PtrSize(vLeaves) + Vec_PtrSize(vNodes) + Vec_PtrSize(vRoots) + 1); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + // map the constant node + Gia_ManConst0(p)->Value = 0; + // create PIs + if ( fTrimPis ) + { + Vec_PtrForEachEntry( Gia_Obj_t *, vLeaves, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + } + else + { + Gia_ManForEachPi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + } + // create LOs +// Vec_PtrForEachEntryStart( Gia_Obj_t *, vRoots, pObj, i, nPos ) +// Gia_ObjRiToRo(p, pObj)->Value = Gia_ManAppendCi( pNew ); + // create internal nodes + Vec_PtrForEachEntry( Gia_Obj_t *, vNodes, pObj, i ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + // create COs + Vec_PtrForEachEntry( Gia_Obj_t *, vRoots, pObj, i ) +// Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManAppendCo( pNew, pObj->Value ); + // finalize +// Gia_ManSetRegNum( pNew, Vec_PtrSize(vRoots)-nPos ); + Gia_ManSetRegNum( pNew, 0 ); + Vec_PtrFree( vLeaves ); + Vec_PtrFree( vNodes ); + Vec_PtrFree( vRoots ); + return pNew; + } /**Function************************************************************* @@ -3235,65 +3294,6 @@ int Gia_ManSortByValue( Gia_Obj_t ** pp1, Gia_Obj_t ** pp2 ) return 0; } -/**Function************************************************************* - - Synopsis [Decomposes the miter outputs.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Gia_Man_t * Gia_ManDupDemiter( Gia_Man_t * p, int fVerbose ) -{ - Vec_Int_t * vSuper; - Vec_Ptr_t * vSuperPtr; - Gia_Man_t * pNew, * pTemp; - Gia_Obj_t * pObj, * pObjPo; - int i, iLit; - assert( Gia_ManPoNum(p) == 1 ); - // decompose - pObjPo = Gia_ManPo( p, 0 ); - vSuper = Vec_IntAlloc( 100 ); - Gia_ManDupWithConstrCollectAnd_rec( p, Gia_ObjFanin0(pObjPo), vSuper, 1 ); - assert( Vec_IntSize(vSuper) > 1 ); - // report the result - printf( "The miter is %s-decomposable into %d parts.\n", Gia_ObjFaninC0(pObjPo) ? "OR":"AND", Vec_IntSize(vSuper) ); - // create levels - Gia_ManLevelNum( p ); - Vec_IntForEachEntry( vSuper, iLit, i ) - Gia_ManObj(p, Abc_Lit2Var(iLit))->Value = Gia_ObjLevelId(p, Abc_Lit2Var(iLit)); - // create pointer array - vSuperPtr = Vec_PtrAlloc( Vec_IntSize(vSuper) ); - Vec_IntForEachEntry( vSuper, iLit, i ) - Vec_PtrPush( vSuperPtr, Gia_Lit2Obj(p, iLit) ); - Vec_PtrSort( vSuperPtr, (int (*)(void))Gia_ManSortByValue ); - // create new manager - pNew = Gia_ManStart( Gia_ManObjNum(p) ); - pNew->pName = Abc_UtilStrsav( p->pName ); - pNew->pSpec = Abc_UtilStrsav( p->pSpec ); - Gia_ManConst0(p)->Value = 0; - Gia_ManHashAlloc( pNew ); - Gia_ManForEachCi( p, pObj, i ) - pObj->Value = Gia_ManAppendCi( pNew ); - Gia_ManForEachAnd( p, pObj, i ) - pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - // create the outputs - Vec_PtrForEachEntry( Gia_Obj_t *, vSuperPtr, pObj, i ) - Gia_ManAppendCo( pNew, Gia_ObjLitCopy(p, Gia_Obj2Lit(p, pObj)) ^ Gia_ObjFaninC0(pObjPo) ); - Gia_ManForEachRi( p, pObj, i ) - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); - // rehash - pNew = Gia_ManCleanup( pTemp = pNew ); - Gia_ManStop( pTemp ); - Vec_IntFree( vSuper ); - Vec_PtrFree( vSuperPtr ); - return pNew; -} - /**Function************************************************************* Synopsis [Decomposes the miter outputs.] @@ -3583,6 +3583,378 @@ Gia_Man_t * Gia_ManIsoStrashReduce( Gia_Man_t * p, Vec_Ptr_t ** pvPosEquivs, int return pNew; } +/**Function************************************************************* + + Synopsis [Decomposes the miter outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManDupDemiter( Gia_Man_t * p, int fVerbose ) +{ + Vec_Int_t * vSuper; + Vec_Ptr_t * vSuperPtr; + Gia_Man_t * pNew, * pTemp; + Gia_Obj_t * pObj, * pObjPo; + int i, iLit; + assert( Gia_ManPoNum(p) == 1 ); + // decompose + pObjPo = Gia_ManPo( p, 0 ); + vSuper = Vec_IntAlloc( 100 ); + Gia_ManDupWithConstrCollectAnd_rec( p, Gia_ObjFanin0(pObjPo), vSuper, 1 ); + assert( Vec_IntSize(vSuper) > 1 ); + // report the result + printf( "The miter is %s-decomposable into %d parts.\n", Gia_ObjFaninC0(pObjPo) ? "OR":"AND", Vec_IntSize(vSuper) ); + // create levels + Gia_ManLevelNum( p ); + Vec_IntForEachEntry( vSuper, iLit, i ) + Gia_ManObj(p, Abc_Lit2Var(iLit))->Value = Gia_ObjLevelId(p, Abc_Lit2Var(iLit)); + // create pointer array + vSuperPtr = Vec_PtrAlloc( Vec_IntSize(vSuper) ); + Vec_IntForEachEntry( vSuper, iLit, i ) + Vec_PtrPush( vSuperPtr, Gia_Lit2Obj(p, iLit) ); + Vec_PtrSort( vSuperPtr, (int (*)(void))Gia_ManSortByValue ); + // create new manager + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManHashAlloc( pNew ); + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + // create the outputs + Vec_PtrForEachEntry( Gia_Obj_t *, vSuperPtr, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjLitCopy(p, Gia_Obj2Lit(p, pObj)) ^ Gia_ObjFaninC0(pObjPo) ); + Gia_ManForEachRi( p, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + // rehash + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManStop( pTemp ); + Vec_IntFree( vSuper ); + Vec_PtrFree( vSuperPtr ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManSetMark0Dfs_rec( Gia_Man_t * p, int iObj ) +{ + Gia_Obj_t * pObj; + pObj = Gia_ManObj( p, iObj ); + if ( pObj->fMark0 ) + return; + pObj->fMark0 = 1; + if ( !Gia_ObjIsAnd(pObj) ) + return; + Gia_ManSetMark0Dfs_rec( p, Gia_ObjFaninId0(pObj, iObj) ); + Gia_ManSetMark0Dfs_rec( p, Gia_ObjFaninId1(pObj, iObj) ); +} +void Gia_ManSetMark1Dfs_rec( Gia_Man_t * p, int iObj ) +{ + Gia_Obj_t * pObj; + pObj = Gia_ManObj( p, iObj ); + if ( pObj->fMark1 ) + return; + pObj->fMark1 = 1; + if ( !Gia_ObjIsAnd(pObj) ) + return; + Gia_ManSetMark1Dfs_rec( p, Gia_ObjFaninId0(pObj, iObj) ); + Gia_ManSetMark1Dfs_rec( p, Gia_ObjFaninId1(pObj, iObj) ); +} + +int Gia_ManCountMark0Dfs_rec( Gia_Man_t * p, int iObj ) +{ + Gia_Obj_t * pObj; + if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) + return 0; + Gia_ObjSetTravIdCurrentId(p, iObj); + pObj = Gia_ManObj( p, iObj ); + if ( !Gia_ObjIsAnd(pObj) ) + return pObj->fMark0; + return Gia_ManCountMark0Dfs_rec( p, Gia_ObjFaninId0(pObj, iObj) ) + + Gia_ManCountMark0Dfs_rec( p, Gia_ObjFaninId1(pObj, iObj) ) + pObj->fMark0; +} +int Gia_ManCountMark0Dfs( Gia_Man_t * p, int iObj ) +{ + Gia_ManIncrementTravId( p ); + return Gia_ManCountMark0Dfs_rec( p, iObj ); +} +int Gia_ManCountMark1Dfs_rec( Gia_Man_t * p, int iObj ) +{ + Gia_Obj_t * pObj; + if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) + return 0; + Gia_ObjSetTravIdCurrentId(p, iObj); + pObj = Gia_ManObj( p, iObj ); + if ( !Gia_ObjIsAnd(pObj) ) + return pObj->fMark1; + return Gia_ManCountMark1Dfs_rec( p, Gia_ObjFaninId0(pObj, iObj) ) + + Gia_ManCountMark1Dfs_rec( p, Gia_ObjFaninId1(pObj, iObj) ) + pObj->fMark1; +} +int Gia_ManCountMark1Dfs( Gia_Man_t * p, int iObj ) +{ + Gia_ManIncrementTravId( p ); + return Gia_ManCountMark1Dfs_rec( p, iObj ); +} + +int Gia_ManDecideWhereToAdd( Gia_Man_t * p, Vec_Int_t * vPart[2], Gia_Obj_t * pFan[2] ) +{ + int Count0 = 1, Count1 = 0; + assert( Vec_IntSize(vPart[0]) == Vec_IntSize(vPart[1]) ); + if ( Vec_IntSize(vPart[0]) > 0 ) + { + Count0 = Gia_ManCountMark0Dfs(p, Gia_ObjId(p, pFan[0])) + Gia_ManCountMark1Dfs(p, Gia_ObjId(p, pFan[1])); + Count1 = Gia_ManCountMark0Dfs(p, Gia_ObjId(p, pFan[1])) + Gia_ManCountMark1Dfs(p, Gia_ObjId(p, pFan[0])); + } + return Count0 < Count1; +} +void Gia_ManCollectTopXors_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXors ) +{ + Gia_Obj_t * pFan0, * pFan1; + int iObj = Gia_ObjId( p, pObj ); + if ( Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) || !Gia_ObjIsAnd(pObj) ) + { + Vec_IntPushUnique( vXors, Gia_ObjId(p, pObj) ); + return; + } + if ( Gia_ObjFaninC0(pObj) ) + Vec_IntPushUnique( vXors, Gia_ObjFaninId0(pObj, iObj) ); + else + Gia_ManCollectTopXors_rec( p, Gia_ObjFanin0(pObj), vXors ); + if ( Gia_ObjFaninC1(pObj) ) + Vec_IntPushUnique( vXors, Gia_ObjFaninId1(pObj, iObj) ); + else + Gia_ManCollectTopXors_rec( p, Gia_ObjFanin1(pObj), vXors ); +} +Vec_Int_t * Gia_ManCollectTopXors( Gia_Man_t * p, Vec_Int_t * vPolar ) +{ + int i, iObj, iObj2, fFlip, * pPerm, Count1 = 0; + Vec_Int_t * vXors, * vSizes, * vPart[2], * vOrder; + Gia_Obj_t * pFan[2], * pObj = Gia_ManCo(p, 0); + assert( Gia_ManCoNum(p) == 1 ); + Vec_IntClear( vPolar ); + if ( !Gia_ObjFaninC0(pObj) ) + return NULL; + vXors = Vec_IntAlloc( 100 ); + pObj = Gia_ObjFanin0(pObj); + if ( Gia_ObjIsAnd(pObj) ) + Gia_ManCollectTopXors_rec( p, pObj, vXors ); + else + Vec_IntPush( vXors, Gia_ObjId(p, pObj) ); + // order by support size + vSizes = Vec_IntAlloc( 100 ); + Vec_IntForEachEntry( vXors, iObj, i ) + Vec_IntPush( vSizes, Gia_ManSuppSize(p, &iObj, 1) ); + pPerm = Abc_MergeSortCost( Vec_IntArray(vSizes), Vec_IntSize(vSizes) ); + Vec_IntClear( vSizes ); + for ( i = 0; i < Vec_IntSize(vXors); i++ ) + Vec_IntPush( vSizes, Vec_IntEntry(vXors, pPerm[i]) ); + ABC_FREE( pPerm ); + Vec_IntClear( vXors ); + Vec_IntAppend( vXors, vSizes ); + Vec_IntFree( vSizes ); + Vec_IntReverseOrder( vXors ); // from MSB to LSB + // divide into groups + Gia_ManCleanMark01(p); + vPart[0] = Vec_IntAlloc( 100 ); + vPart[1] = Vec_IntAlloc( 100 ); + Gia_ManForEachObjVec( vXors, p, pObj, i ) + { + int fCompl = 0; + if ( !Gia_ObjRecognizeExor(pObj, &pFan[0], &pFan[1]) ) + pFan[0] = pObj, pFan[1] = Gia_ManConst0(p), Count1++; + else + { + fCompl ^= Gia_IsComplement(pFan[0]); + fCompl ^= Gia_IsComplement(pFan[1]); + pFan[0] = Gia_Regular(pFan[0]); + pFan[1] = Gia_Regular(pFan[1]); + } + Vec_IntPushTwo( vPolar, 0, fCompl ); + fFlip = Gia_ManDecideWhereToAdd( p, vPart, pFan ); + Vec_IntPush( vPart[0], Gia_ObjId(p, pFan[fFlip]) ); + Vec_IntPush( vPart[1], Gia_ObjId(p, pFan[!fFlip]) ); + Gia_ManSetMark0Dfs_rec( p, Gia_ObjId(p, pFan[fFlip]) ); + Gia_ManSetMark1Dfs_rec( p, Gia_ObjId(p, pFan[!fFlip]) ); + } + printf( "Detected %d single-output XOR miters and %d other miters.\n", Vec_IntSize(vXors) - Count1, Count1 ); + Vec_IntFree( vXors ); + Gia_ManCleanMark01(p); + // create new order + vOrder = Vec_IntAlloc( 100 ); + Vec_IntForEachEntryTwo( vPart[0], vPart[1], iObj, iObj2, i ) + Vec_IntPushTwo( vOrder, iObj, iObj2 ); + Vec_IntFree( vPart[0] ); + Vec_IntFree( vPart[1] ); + Vec_IntReverseOrder( vOrder ); // from LSB to MSB + Vec_IntReverseOrder( vPolar ); + //Vec_IntPrint( vOrder ); + return vOrder; +} +Gia_Man_t * Gia_ManDemiterToDual( Gia_Man_t * p ) +{ + Gia_Man_t * pNew; Gia_Obj_t * pObj; int i; + Vec_Int_t * vNodes, * vPolar = Vec_IntAlloc( 100 ); + Vec_Int_t * vOrder = Gia_ManCollectTopXors( p, vPolar ); + if ( vOrder == NULL ) + { + Vec_IntFree( vPolar ); + printf( "Cannot demiter because the top-most gate is an AND-gate.\n" ); + return NULL; + } + assert( Vec_IntSize(vOrder) == Vec_IntSize(vPolar) ); + vNodes = Vec_IntAlloc( Gia_ManObjNum(p) ); + Gia_ManIncrementTravId( p ); + Gia_ManCollectAnds( p, Vec_IntArray(vOrder), Vec_IntSize(vOrder), vNodes, NULL ); + pNew = Gia_ManStart( 1 + Gia_ManCiNum(p) + Vec_IntSize(vNodes) + Vec_IntSize(vOrder) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachObjVec( vOrder, p, pObj, i ) + Gia_ManAppendCo( pNew, Abc_LitNotCond(pObj->Value, Vec_IntEntry(vPolar, i)) ); + Vec_IntFree( vPolar ); + Vec_IntFree( vNodes ); + Vec_IntFree( vOrder ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Collect nodes reachable from odd/even outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCollectDfs_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vNodes ) +{ + Gia_Obj_t * pObj; + if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) + return; + Gia_ObjSetTravIdCurrentId(p, iObj); + pObj = Gia_ManObj( p, iObj ); + if ( !Gia_ObjIsAnd(pObj) ) + return; + Gia_ManCollectDfs_rec( p, Gia_ObjFaninId0(pObj, iObj), vNodes ); + Gia_ManCollectDfs_rec( p, Gia_ObjFaninId1(pObj, iObj), vNodes ); + Vec_IntPush( vNodes, iObj ); +} +Vec_Int_t * Gia_ManCollectReach( Gia_Man_t * p, int fOdd ) +{ + int i, iDriver; + Vec_Int_t * vNodes = Vec_IntAlloc( Gia_ManObjNum(p) ); + Gia_ManIncrementTravId( p ); + Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) ); + Gia_ManForEachCoDriverId( p, iDriver, i ) + if ( (i & 1) == fOdd ) + Gia_ManCollectDfs_rec( p, iDriver, vNodes ); + return vNodes; +} +int Gia_ManDemiterDual( Gia_Man_t * p, Gia_Man_t ** pp0, Gia_Man_t ** pp1 ) +{ + Gia_Obj_t * pObj; + int i, fOdd; + assert( Gia_ManRegNum(p) == 0 ); + assert( Gia_ManCoNum(p) % 2 == 0 ); + *pp0 = *pp1 = NULL; + for ( fOdd = 0; fOdd < 2; fOdd++ ) + { + Vec_Int_t * vNodes = Gia_ManCollectReach( p, fOdd ); + Gia_Man_t * pNew = Gia_ManStart( 1 + Gia_ManCiNum(p) + Vec_IntSize(vNodes) + Gia_ManCoNum(p)/2 ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachPi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + if ( (i & 1) == fOdd ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Vec_IntFree( vNodes ); + if ( fOdd ) + *pp1 = pNew; + else + *pp0 = pNew; + } + return 1; +} + +/**Function************************************************************* + + Synopsis [Collect nodes reachable from first/second half of outputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManCollectReach2( Gia_Man_t * p, int fSecond ) +{ + int i, iDriver; + Vec_Int_t * vNodes = Vec_IntAlloc( Gia_ManObjNum(p) ); + Gia_ManIncrementTravId( p ); + Gia_ObjSetTravIdCurrent( p, Gia_ManConst0(p) ); + Gia_ManForEachCoDriverId( p, iDriver, i ) + if ( (i < Gia_ManCoNum(p)/2) ^ fSecond ) + Gia_ManCollectDfs_rec( p, iDriver, vNodes ); + return vNodes; +} +int Gia_ManDemiterTwoWords( Gia_Man_t * p, Gia_Man_t ** pp0, Gia_Man_t ** pp1 ) +{ + Gia_Obj_t * pObj; + int i, fSecond; + assert( Gia_ManRegNum(p) == 0 ); + assert( Gia_ManCoNum(p) % 2 == 0 ); + *pp0 = *pp1 = NULL; + for ( fSecond = 0; fSecond < 2; fSecond++ ) + { + Vec_Int_t * vNodes = Gia_ManCollectReach2( p, fSecond ); + Gia_Man_t * pNew = Gia_ManStart( 1 + Gia_ManCiNum(p) + Vec_IntSize(vNodes) + Gia_ManCoNum(p)/2 ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + Gia_ManForEachPi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + if ( (i < Gia_ManCoNum(p)/2) ^ fSecond ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Vec_IntFree( vNodes ); + if ( fSecond ) + *pp1 = pNew; + else + *pp0 = pNew; + } + return 1; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaFadds.c b/src/aig/gia/giaFadds.c deleted file mode 100644 index 4014814a..00000000 --- a/src/aig/gia/giaFadds.c +++ /dev/null @@ -1,1109 +0,0 @@ -/**CFile**************************************************************** - - FileName [giaFadds.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Scalable AIG package.] - - Synopsis [Extraction of full-adders.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: giaFadds.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "gia.h" -#include "misc/vec/vecWec.h" -#include "misc/tim/tim.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -#define Dtc_ForEachCut( pList, pCut, i ) for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += pCut[0] + 1 ) -#define Dtc_ForEachFadd( vFadds, i ) for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ ) - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [Derive GIA with boxes containing adder-chains.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_ManIllustrateBoxes( Gia_Man_t * p ) -{ - Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime; - int nBoxes = Tim_ManBoxNum( pManTime ); - int i, k, curCi, curCo, nBoxIns, nBoxOuts; - Gia_Obj_t * pObj; - // walk through the boxes - curCi = Tim_ManPiNum(pManTime); - curCo = 0; - for ( i = 0; i < nBoxes; i++ ) - { - nBoxIns = Tim_ManBoxInputNum(pManTime, i); - nBoxOuts = Tim_ManBoxOutputNum(pManTime, i); - printf( "Box %4d [%d x %d] : ", i, nBoxIns, nBoxOuts ); - printf( "Input obj IDs = " ); - for ( k = 0; k < nBoxIns; k++ ) - { - pObj = Gia_ManCo( p, curCo + k ); - printf( "%d ", Gia_ObjId(p, pObj) ); - } - printf( " Output obj IDs = " ); - for ( k = 0; k < nBoxOuts; k++ ) - { - pObj = Gia_ManCi( p, curCi + k ); - printf( "%d ", Gia_ObjId(p, pObj) ); - } - curCo += nBoxIns; - curCi += nBoxOuts; - printf( "\n" ); - } - curCo += Tim_ManPoNum(pManTime); - // verify counts - assert( curCi == Gia_ManCiNum(p) ); - assert( curCo == Gia_ManCoNum(p) ); -} - -/**Function************************************************************* - - Synopsis [Detecting FADDs in the AIG.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Dtc_ManCutMergeOne( int * pCut0, int * pCut1, int * pCut ) -{ - int i, k; - for ( k = 0; k <= pCut1[0]; k++ ) - pCut[k] = pCut1[k]; - for ( i = 1; i <= pCut0[0]; i++ ) - { - for ( k = 1; k <= pCut1[0]; k++ ) - if ( pCut0[i] == pCut1[k] ) - break; - if ( k <= pCut1[0] ) - continue; - if ( pCut[0] == 3 ) - return 0; - pCut[1+pCut[0]++] = pCut0[i]; - } - assert( pCut[0] == 2 || pCut[0] == 3 ); - if ( pCut[1] > pCut[2] ) - ABC_SWAP( int, pCut[1], pCut[2] ); - assert( pCut[1] < pCut[2] ); - if ( pCut[0] == 2 ) - return 1; - if ( pCut[2] > pCut[3] ) - ABC_SWAP( int, pCut[2], pCut[3] ); - if ( pCut[1] > pCut[2] ) - ABC_SWAP( int, pCut[1], pCut[2] ); - assert( pCut[1] < pCut[2] ); - assert( pCut[2] < pCut[3] ); - return 1; -} -int Dtc_ManCutCheckEqual( Vec_Int_t * vCuts, int * pCutNew ) -{ - int * pList = Vec_IntArray( vCuts ); - int i, k, * pCut; - Dtc_ForEachCut( pList, pCut, i ) - { - for ( k = 0; k <= pCut[0]; k++ ) - if ( pCut[k] != pCutNew[k] ) - break; - if ( k > pCut[0] ) - return 1; - } - return 0; -} -int Dtc_ObjComputeTruth_rec( Gia_Obj_t * pObj ) -{ - int Truth0, Truth1; - if ( pObj->Value ) - return pObj->Value; - assert( Gia_ObjIsAnd(pObj) ); - Truth0 = Dtc_ObjComputeTruth_rec( Gia_ObjFanin0(pObj) ); - Truth1 = Dtc_ObjComputeTruth_rec( Gia_ObjFanin1(pObj) ); - return (pObj->Value = (Gia_ObjFaninC0(pObj) ? ~Truth0 : Truth0) & (Gia_ObjFaninC1(pObj) ? ~Truth1 : Truth1)); -} -void Dtc_ObjCleanTruth_rec( Gia_Obj_t * pObj ) -{ - if ( !pObj->Value ) - return; - pObj->Value = 0; - if ( !Gia_ObjIsAnd(pObj) ) - return; - Dtc_ObjCleanTruth_rec( Gia_ObjFanin0(pObj) ); - Dtc_ObjCleanTruth_rec( Gia_ObjFanin1(pObj) ); -} -int Dtc_ObjComputeTruth( Gia_Man_t * p, int iObj, int * pCut, int * pTruth ) -{ - unsigned Truth, Truths[3] = { 0xAA, 0xCC, 0xF0 }; int i; - for ( i = 1; i <= pCut[0]; i++ ) - Gia_ManObj(p, pCut[i])->Value = Truths[i-1]; - Truth = 0xFF & Dtc_ObjComputeTruth_rec( Gia_ManObj(p, iObj) ); - Dtc_ObjCleanTruth_rec( Gia_ManObj(p, iObj) ); - if ( pTruth ) - *pTruth = Truth; - if ( Truth == 0x96 || Truth == 0x69 ) - return 1; - if ( Truth == 0xE8 || Truth == 0xD4 || Truth == 0xB2 || Truth == 0x71 || - Truth == 0x17 || Truth == 0x2B || Truth == 0x4D || Truth == 0x8E ) - return 2; - return 0; -} -void Dtc_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_Int_t * vCuts, Vec_Int_t * vCutsXor, Vec_Int_t * vCutsMaj ) -{ - Vec_Int_t * vTemp; - int i, k, c, Type, * pCut0, * pCut1, pCut[4]; - Vec_IntFill( vCuts, 2, 1 ); - Vec_IntPush( vCuts, iObj ); - Dtc_ForEachCut( pList0, pCut0, i ) - Dtc_ForEachCut( pList1, pCut1, k ) - { - if ( !Dtc_ManCutMergeOne(pCut0, pCut1, pCut) ) - continue; - if ( Dtc_ManCutCheckEqual(vCuts, pCut) ) - continue; - Vec_IntAddToEntry( vCuts, 0, 1 ); - for ( c = 0; c <= pCut[0]; c++ ) - Vec_IntPush( vCuts, pCut[c] ); - if ( pCut[0] != 3 ) - continue; - Type = Dtc_ObjComputeTruth( p, iObj, pCut, NULL ); - if ( Type == 0 ) - continue; - vTemp = Type == 1 ? vCutsXor : vCutsMaj; - for ( c = 1; c <= pCut[0]; c++ ) - Vec_IntPush( vTemp, pCut[c] ); - Vec_IntPush( vTemp, iObj ); - } -} -void Dtc_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvCutsXor, Vec_Int_t ** pvCutsMaj, int fVerbose ) -{ - Gia_Obj_t * pObj; - int * pList0, * pList1, i, nCuts = 0; - Vec_Int_t * vTemp = Vec_IntAlloc( 1000 ); - Vec_Int_t * vCutsXor = Vec_IntAlloc( Gia_ManAndNum(p) ); - Vec_Int_t * vCutsMaj = Vec_IntAlloc( Gia_ManAndNum(p) ); - Vec_Int_t * vCuts = Vec_IntAlloc( 30 * Gia_ManAndNum(p) ); - Vec_IntFill( vCuts, Gia_ManObjNum(p), 0 ); - Gia_ManCleanValue( p ); - Gia_ManForEachCi( p, pObj, i ) - { - Vec_IntWriteEntry( vCuts, Gia_ObjId(p, pObj), Vec_IntSize(vCuts) ); - Vec_IntPush( vCuts, 1 ); - Vec_IntPush( vCuts, 1 ); - Vec_IntPush( vCuts, Gia_ObjId(p, pObj) ); - } - Gia_ManForEachAnd( p, pObj, i ) - { - pList0 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId0(pObj, i)) ); - pList1 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId1(pObj, i)) ); - Dtc_ManCutMerge( p, i, pList0, pList1, vTemp, vCutsXor, vCutsMaj ); - Vec_IntWriteEntry( vCuts, i, Vec_IntSize(vCuts) ); - Vec_IntAppend( vCuts, vTemp ); - nCuts += Vec_IntEntry( vTemp, 0 ); - } - if ( fVerbose ) - printf( "Nodes = %d. Cuts = %d. Cuts/Node = %.2f. Ints/Node = %.2f.\n", - Gia_ManAndNum(p), nCuts, 1.0*nCuts/Gia_ManAndNum(p), 1.0*Vec_IntSize(vCuts)/Gia_ManAndNum(p) ); - Vec_IntFree( vTemp ); - Vec_IntFree( vCuts ); - *pvCutsXor = vCutsXor; - *pvCutsMaj = vCutsMaj; -} -Vec_Int_t * Dtc_ManFindCommonCuts( Gia_Man_t * p, Vec_Int_t * vCutsXor, Vec_Int_t * vCutsMaj ) -{ - int * pCuts0 = Vec_IntArray(vCutsXor); - int * pCuts1 = Vec_IntArray(vCutsMaj); - int * pLimit0 = Vec_IntLimit(vCutsXor); - int * pLimit1 = Vec_IntLimit(vCutsMaj); int i; - Vec_Int_t * vFadds = Vec_IntAlloc( 1000 ); - assert( Vec_IntSize(vCutsXor) % 4 == 0 ); - assert( Vec_IntSize(vCutsMaj) % 4 == 0 ); - while ( pCuts0 < pLimit0 && pCuts1 < pLimit1 ) - { - for ( i = 0; i < 3; i++ ) - if ( pCuts0[i] != pCuts1[i] ) - break; - if ( i == 3 ) - { - for ( i = 0; i < 4; i++ ) - Vec_IntPush( vFadds, pCuts0[i] ); - Vec_IntPush( vFadds, pCuts1[3] ); - pCuts0 += 4; - pCuts1 += 4; - } - else if ( pCuts0[i] < pCuts1[i] ) - pCuts0 += 4; - else if ( pCuts0[i] > pCuts1[i] ) - pCuts1 += 4; - } - assert( Vec_IntSize(vFadds) % 5 == 0 ); - return vFadds; -} -void Dtc_ManPrintFadds( Vec_Int_t * vFadds ) -{ - int i; - Dtc_ForEachFadd( vFadds, i ) - { - printf( "%6d : ", i ); - printf( "%6d ", Vec_IntEntry(vFadds, 5*i+0) ); - printf( "%6d ", Vec_IntEntry(vFadds, 5*i+1) ); - printf( "%6d ", Vec_IntEntry(vFadds, 5*i+2) ); - printf( " -> " ); - printf( "%6d ", Vec_IntEntry(vFadds, 5*i+3) ); - printf( "%6d ", Vec_IntEntry(vFadds, 5*i+4) ); - printf( "\n" ); - } -} -int Dtc_ManCompare( int * pCut0, int * pCut1 ) -{ - if ( pCut0[0] < pCut1[0] ) return -1; - if ( pCut0[0] > pCut1[0] ) return 1; - if ( pCut0[1] < pCut1[1] ) return -1; - if ( pCut0[1] > pCut1[1] ) return 1; - if ( pCut0[2] < pCut1[2] ) return -1; - if ( pCut0[2] > pCut1[2] ) return 1; - return 0; -} -int Dtc_ManCompare2( int * pCut0, int * pCut1 ) -{ - if ( pCut0[4] < pCut1[4] ) return -1; - if ( pCut0[4] > pCut1[4] ) return 1; - return 0; -} -// returns array of 5-tuples containing inputs/sum/cout of each full adder -Vec_Int_t * Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose ) -{ - Vec_Int_t * vCutsXor, * vCutsMaj, * vFadds; - Dtc_ManComputeCuts( p, &vCutsXor, &vCutsMaj, fVerbose ); - qsort( Vec_IntArray(vCutsXor), Vec_IntSize(vCutsXor)/4, 16, (int (*)(const void *, const void *))Dtc_ManCompare ); - qsort( Vec_IntArray(vCutsMaj), Vec_IntSize(vCutsMaj)/4, 16, (int (*)(const void *, const void *))Dtc_ManCompare ); - vFadds = Dtc_ManFindCommonCuts( p, vCutsXor, vCutsMaj ); - qsort( Vec_IntArray(vFadds), Vec_IntSize(vFadds)/5, 20, (int (*)(const void *, const void *))Dtc_ManCompare2 ); - if ( fVerbose ) - printf( "XOR3 cuts = %d. MAJ cuts = %d. Full-adders = %d.\n", Vec_IntSize(vCutsXor)/4, Vec_IntSize(vCutsMaj)/4, Vec_IntSize(vFadds)/5 ); - //Dtc_ManPrintFadds( vFadds ); - Vec_IntFree( vCutsXor ); - Vec_IntFree( vCutsMaj ); - return vFadds; -} - -/**Function************************************************************* - - Synopsis [Map each MAJ into the topmost MAJ of its chain.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -// maps MAJ nodes into FADD indexes -Vec_Int_t * Gia_ManCreateMap( Gia_Man_t * p, Vec_Int_t * vFadds ) -{ - Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) ); int i; - Dtc_ForEachFadd( vFadds, i ) - Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+4), i ); - return vMap; -} -// find chain length (for each MAJ, how many FADDs are rooted in its first input) -int Gia_ManFindChains_rec( Gia_Man_t * p, int iMaj, Vec_Int_t * vFadds, Vec_Int_t * vMap, Vec_Int_t * vLength ) -{ - assert( Vec_IntEntry(vMap, iMaj) >= 0 ); // MAJ - if ( Vec_IntEntry(vLength, iMaj) >= 0 ) - return Vec_IntEntry(vLength, iMaj); - assert( Gia_ObjIsAnd(Gia_ManObj(p, iMaj)) ); - { - int iFadd = Vec_IntEntry( vMap, iMaj ); - int iXor0 = Vec_IntEntry( vFadds, 5*iFadd+0 ); - int iXor1 = Vec_IntEntry( vFadds, 5*iFadd+1 ); - int iXor2 = Vec_IntEntry( vFadds, 5*iFadd+2 ); - int iLen0 = Vec_IntEntry( vMap, iXor0 ) == -1 ? 0 : Gia_ManFindChains_rec( p, iXor0, vFadds, vMap, vLength ); - int iLen1 = Vec_IntEntry( vMap, iXor1 ) == -1 ? 0 : Gia_ManFindChains_rec( p, iXor1, vFadds, vMap, vLength ); - int iLen2 = Vec_IntEntry( vMap, iXor2 ) == -1 ? 0 : Gia_ManFindChains_rec( p, iXor2, vFadds, vMap, vLength ); - int iLen = Abc_MaxInt( iLen0, Abc_MaxInt(iLen1, iLen2) ); - if ( iLen0 < iLen ) - { - if ( iLen == iLen1 ) - { - ABC_SWAP( int, Vec_IntArray(vFadds)[5*iFadd+0], Vec_IntArray(vFadds)[5*iFadd+1] ); - } - else if ( iLen == iLen2 ) - { - ABC_SWAP( int, Vec_IntArray(vFadds)[5*iFadd+0], Vec_IntArray(vFadds)[5*iFadd+2] ); - } - } - Vec_IntWriteEntry( vLength, iMaj, iLen + 1 ); - return iLen + 1; - } -} -// for each FADD find the longest chain and reorder its inputs -void Gia_ManFindChains( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vMap ) -{ - int i; - // for each FADD find the longest chain rooted in it - Vec_Int_t * vLength = Vec_IntStartFull( Gia_ManObjNum(p) ); - Dtc_ForEachFadd( vFadds, i ) - Gia_ManFindChains_rec( p, Vec_IntEntry(vFadds, 5*i+4), vFadds, vMap, vLength ); - Vec_IntFree( vLength ); -} -// collect one carry-chain -void Gia_ManCollectOneChain( Gia_Man_t * p, Vec_Int_t * vFadds, int iFaddTop, Vec_Int_t * vMap, Vec_Int_t * vChain ) -{ - int iFadd; - Vec_IntClear( vChain ); - for ( iFadd = iFaddTop; iFadd >= 0 && - !Gia_ObjIsTravIdCurrentId(p, Vec_IntEntry(vFadds, 5*iFadd+3)) && - !Gia_ObjIsTravIdCurrentId(p, Vec_IntEntry(vFadds, 5*iFadd+4)); - iFadd = Vec_IntEntry(vMap, Vec_IntEntry(vFadds, 5*iFadd+0)) ) - { - Vec_IntPush( vChain, iFadd ); - } - Vec_IntReverseOrder( vChain ); -} -void Gia_ManMarkWithTravId_rec( Gia_Man_t * p, int Id ) -{ - Gia_Obj_t * pObj; - if ( Gia_ObjIsTravIdCurrentId(p, Id) ) - return; - Gia_ObjSetTravIdCurrentId(p, Id); - pObj = Gia_ManObj( p, Id ); - if ( Gia_ObjIsAnd(pObj) ) - Gia_ManMarkWithTravId_rec( p, Gia_ObjFaninId0(pObj, Id) ); - if ( Gia_ObjIsAnd(pObj) ) - Gia_ManMarkWithTravId_rec( p, Gia_ObjFaninId1(pObj, Id) ); -} -// returns mapping of each MAJ into the topmost elements of its chain -Vec_Wec_t * Gia_ManCollectTopmost( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vMap, int nFaddMin ) -{ - int i, j, iFadd; - Vec_Int_t * vChain = Vec_IntAlloc( 100 ); - Vec_Wec_t * vChains = Vec_WecAlloc( Vec_IntSize(vFadds)/5 ); - // erase elements appearing as FADD inputs - Vec_Bit_t * vMarksTop = Vec_BitStart( Vec_IntSize(vFadds)/5 ); - Dtc_ForEachFadd( vFadds, i ) - if ( (iFadd = Vec_IntEntry(vMap, Vec_IntEntry(vFadds, 5*i+0))) >= 0 ) - Vec_BitWriteEntry( vMarksTop, iFadd, 1 ); - // compress the remaining ones - Gia_ManIncrementTravId( p ); - Dtc_ForEachFadd( vFadds, i ) - { - if ( Vec_BitEntry(vMarksTop, i) ) - continue; - Gia_ManCollectOneChain( p, vFadds, i, vMap, vChain ); - if ( Vec_IntSize(vChain) < nFaddMin ) - continue; - Vec_IntAppend( Vec_WecPushLevel(vChains), vChain ); - Vec_IntForEachEntry( vChain, iFadd, j ) - { - assert( !Gia_ObjIsTravIdCurrentId(p, Vec_IntEntry(vFadds, 5*iFadd+3)) ); - assert( !Gia_ObjIsTravIdCurrentId(p, Vec_IntEntry(vFadds, 5*iFadd+4)) ); - Gia_ManMarkWithTravId_rec( p, Vec_IntEntry(vFadds, 5*iFadd+3) ); - Gia_ManMarkWithTravId_rec( p, Vec_IntEntry(vFadds, 5*iFadd+4) ); - } - } - // cleanup - Vec_BitFree( vMarksTop ); - Vec_IntFree( vChain ); - return vChains; -} -// prints chains beginning in majority nodes contained in vTops -void Gia_ManPrintChains( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vMap, Vec_Wec_t * vChains ) -{ - Vec_Int_t * vChain; - int i, k, iFadd, Count = 0; - Vec_WecForEachLevel( vChains, vChain, i ) - { - Count += Vec_IntSize(vChain); - if ( i < 10 ) - { - printf( "Chain %4d : %4d ", i, Vec_IntSize(vChain) ); - Vec_IntForEachEntry( vChain, iFadd, k ) - { - printf( "%d(%d) ", iFadd, Vec_IntEntry(vFadds, 5*iFadd+4) ); - if ( k != Vec_IntSize(vChain) - 1 ) - printf( "-> " ); - if ( k > 6 ) - { - printf( "..." ); - break; - } - } - printf( "\n" ); - } - else if ( i == 10 ) - printf( "...\n" ); - - } - printf( "Total chains = %d. Total full-adders = %d.\n", Vec_WecSize(vChains), Count ); -} -// map SUM bits and topmost MAJ into topmost FADD number -Vec_Int_t * Gia_ManFindMapping( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vMap, Vec_Wec_t * vChains ) -{ - Vec_Int_t * vChain; - int i, k, iFadd = -1; - Vec_Int_t * vMap2Chain = Vec_IntStartFull( Gia_ManObjNum(p) ); - Vec_WecForEachLevel( vChains, vChain, i ) - { - assert( Vec_IntSize(vChain) > 0 ); - Vec_IntForEachEntry( vChain, iFadd, k ) - { - //printf( "Chain %d: setting SUM %d (obj %d)\n", i, k, Vec_IntEntry(vFadds, 5*iFadd+3) ); - assert( Vec_IntEntry(vMap2Chain, Vec_IntEntry(vFadds, 5*iFadd+3)) == -1 ); - Vec_IntWriteEntry( vMap2Chain, Vec_IntEntry(vFadds, 5*iFadd+3), i ); - } - //printf( "Chain %d: setting CARRY (obj %d)\n", i, Vec_IntEntry(vFadds, 5*iFadd+4) ); - assert( Vec_IntEntry(vMap2Chain, Vec_IntEntry(vFadds, 5*iFadd+4)) == -1 ); - Vec_IntWriteEntry( vMap2Chain, Vec_IntEntry(vFadds, 5*iFadd+4), i ); - } - return vMap2Chain; -} - -/**Function************************************************************* - - Synopsis [Derive GIA with boxes containing adder-chains.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Vec_Int_t * Gia_ManCollectTruthTables( Gia_Man_t * p, Vec_Int_t * vFadds ) -{ - int i, k, Type, Truth, pCut[4] = {3}; - Vec_Int_t * vTruths = Vec_IntAlloc( 2*Vec_IntSize(vFadds)/5 ); - Gia_ManCleanValue( p ); - Dtc_ForEachFadd( vFadds, i ) - { - for ( k = 0; k < 3; k++ ) - pCut[k+1] = Vec_IntEntry( vFadds, 5*i+k ); - Type = Dtc_ObjComputeTruth( p, Vec_IntEntry(vFadds, 5*i+3), pCut, &Truth ); - assert( Type == 1 ); - Vec_IntPush( vTruths, Truth ); - Type = Dtc_ObjComputeTruth( p, Vec_IntEntry(vFadds, 5*i+4), pCut, &Truth ); - assert( Type == 2 ); - Vec_IntPush( vTruths, Truth ); - } - return vTruths; -} -float * Gia_ManGenerateDelayTableFloat( int nIns, int nOuts ) -{ - int i, Total = nIns * nOuts; - float * pDelayTable = ABC_ALLOC( float, Total + 3 ); - pDelayTable[0] = 0; - pDelayTable[1] = nIns; - pDelayTable[2] = nOuts; - for ( i = 0; i < Total; i++ ) - pDelayTable[i+3] = 1; - pDelayTable[i+3 - nIns] = -ABC_INFINITY; - return pDelayTable; -} -Tim_Man_t * Gia_ManGenerateTim( int nPis, int nPos, int nBoxes, int nIns, int nOuts ) -{ - Tim_Man_t * pMan; - int i, curPi, curPo; - Vec_Ptr_t * vDelayTables = Vec_PtrAlloc( 1 ); - Vec_PtrPush( vDelayTables, Gia_ManGenerateDelayTableFloat(nIns, nOuts) ); - pMan = Tim_ManStart( nPis + nOuts * nBoxes, nPos + nIns * nBoxes ); - Tim_ManSetDelayTables( pMan, vDelayTables ); - curPi = nPis; - curPo = 0; - for ( i = 0; i < nBoxes; i++ ) - { - Tim_ManCreateBox( pMan, curPo, nIns, curPi, nOuts, 0, 0 ); - curPi += nOuts; - curPo += nIns; - } - curPo += nPos; - assert( curPi == Tim_ManCiNum(pMan) ); - assert( curPo == Tim_ManCoNum(pMan) ); - //Tim_ManPrint( pMan ); - return pMan; -} -Gia_Man_t * Gia_ManGenerateExtraAig( int nBoxes, int nIns, int nOuts ) -{ - Gia_Man_t * pNew = Gia_ManStart( nBoxes * 20 ); - int i, k, pInLits[16], pOutLits[16]; - assert( nIns < 16 && nOuts < 16 ); - for ( i = 0; i < nIns; i++ ) - pInLits[i] = Gia_ManAppendCi( pNew ); - pOutLits[0] = Gia_ManAppendXor( pNew, Gia_ManAppendXor(pNew, pInLits[0], pInLits[1]), pInLits[2] ); - pOutLits[1] = Gia_ManAppendMaj( pNew, pInLits[0], pInLits[1], pInLits[2] ); - for ( i = 0; i < nBoxes; i++ ) - for ( k = 0; k < nOuts; k++ ) - Gia_ManAppendCo( pNew, pOutLits[k] ); - return pNew; -} -void Gia_ManDupFadd( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vChain, Vec_Int_t * vFadds, Vec_Int_t * vMap, Vec_Wec_t * vChains, Vec_Int_t * vMap2Chain, Vec_Int_t * vTruths ) -{ - extern void Gia_ManDupWithFaddBoxes_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vFadds, Vec_Int_t * vMap, Vec_Wec_t * vChains, Vec_Int_t * vMap2Chain, Vec_Int_t * vTruths ); - int i, k, iFadd = -1, iCiLit, pLits[3]; - Gia_Obj_t * pObj; - // construct FADD inputs - Vec_IntForEachEntry( vChain, iFadd, i ) - for ( k = 0; k < 3; k++ ) - { - if ( i && !k ) continue; - pObj = Gia_ManObj( p, Vec_IntEntry(vFadds, 5*iFadd+k) ); - Gia_ManDupWithFaddBoxes_rec( pNew, p, pObj, vFadds, vMap, vChains, vMap2Chain, vTruths ); - } - // construct boxes - iCiLit = 0; - Vec_IntForEachEntry( vChain, iFadd, i ) - { - int iXorTruth = Vec_IntEntry( vTruths, 2*iFadd+0 ); - int iMajTruth = Vec_IntEntry( vTruths, 2*iFadd+1 ); - for ( k = 0; k < 3; k++ ) - { - pObj = Gia_ManObj( p, Vec_IntEntry(vFadds, 5*iFadd+k) ); - pLits[k] = (!k && iCiLit) ? iCiLit : pObj->Value; - assert( pLits[k] >= 0 ); - } - // normalize truth table - // if ( Truth == 0xE8 || Truth == 0xD4 || Truth == 0xB2 || Truth == 0x71 || - // Truth == 0x17 || Truth == 0x2B || Truth == 0x4D || Truth == 0x8E ) - if ( iMajTruth == 0x4D ) - pLits[0] = Abc_LitNot(pLits[0]), iMajTruth = 0x8E, iXorTruth = 0xFF & ~iXorTruth; - else if ( iMajTruth == 0xD4 ) - pLits[0] = Abc_LitNot(pLits[0]), iMajTruth = 0xE8, iXorTruth = 0xFF & ~iXorTruth; - else if ( iMajTruth == 0x2B ) - pLits[1] = Abc_LitNot(pLits[1]), iMajTruth = 0x8E, iXorTruth = 0xFF & ~iXorTruth; - else if ( iMajTruth == 0xB2 ) - pLits[1] = Abc_LitNot(pLits[1]), iMajTruth = 0xE8, iXorTruth = 0xFF & ~iXorTruth; - if ( iMajTruth == 0x8E ) - pLits[2] = Abc_LitNot(pLits[2]), iMajTruth = 0xE8, iXorTruth = 0xFF & ~iXorTruth; - else if ( iMajTruth == 0x71 ) - pLits[2] = Abc_LitNot(pLits[2]), iMajTruth = 0x17, iXorTruth = 0xFF & ~iXorTruth; - else assert( iMajTruth == 0xE8 || iMajTruth == 0x17 ); - // normalize carry-in - if ( Abc_LitIsCompl(pLits[0]) ) - { - for ( k = 0; k < 3; k++ ) - pLits[k] = Abc_LitNot(pLits[k]); - iXorTruth = 0xFF & ~iXorTruth; - iMajTruth = 0xFF & ~iMajTruth; - } - // add COs - assert( !Abc_LitIsCompl(pLits[0]) ); - for ( k = 0; k < 3; k++ ) - Gia_ManAppendCo( pNew, pLits[k] ); - // create CI - assert( iXorTruth == 0x96 || iXorTruth == 0x69 ); - pObj = Gia_ManObj( p, Vec_IntEntry(vFadds, 5*iFadd+3) ); - pObj->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), (int)(iXorTruth == 0x69) ); - // create CI - assert( iMajTruth == 0xE8 || iMajTruth == 0x17 ); - iCiLit = Abc_LitNotCond( Gia_ManAppendCi(pNew), (int)(iMajTruth == 0x17) ); - } - // assign carry out - assert( iFadd == Vec_IntEntryLast(vChain) ); - pObj = Gia_ManObj( p, Vec_IntEntry(vFadds, 5*iFadd+4) ); - pObj->Value = iCiLit; -} -void Gia_ManDupWithFaddBoxes_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vFadds, Vec_Int_t * vMap, Vec_Wec_t * vChains, Vec_Int_t * vMap2Chain, Vec_Int_t * vTruths ) -{ - int iChain; - if ( ~pObj->Value ) - return; - assert( Gia_ObjIsAnd(pObj) ); - iChain = Vec_IntEntry( vMap2Chain, Gia_ObjId(p, pObj) ); -/* - assert( iChain == -1 ); - if ( iChain >= 0 ) - { - Gia_ManDupFadd( pNew, p, Vec_WecEntry(vChains, iChain), vFadds, vMap, vChains, vMap2Chain, vTruths ); - assert( ~pObj->Value ); - return; - } -*/ - Gia_ManDupWithFaddBoxes_rec( pNew, p, Gia_ObjFanin0(pObj), vFadds, vMap, vChains, vMap2Chain, vTruths ); - Gia_ManDupWithFaddBoxes_rec( pNew, p, Gia_ObjFanin1(pObj), vFadds, vMap, vChains, vMap2Chain, vTruths ); - pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); -} -Gia_Man_t * Gia_ManDupWithNaturalBoxes( Gia_Man_t * p, int nFaddMin, int fVerbose ) -{ - abctime clk = Abc_Clock(); - Gia_Man_t * pNew;//, * pTemp; - Vec_Int_t * vFadds, * vMap, * vMap2Chain, * vTruths, * vChain; - Vec_Wec_t * vChains; - Gia_Obj_t * pObj; - int i, nBoxes; - if ( Gia_ManBoxNum(p) > 0 ) - { - printf( "Currently natural carry-chains cannot be detected when boxes are present.\n" ); - return NULL; - } - assert( Gia_ManBoxNum(p) == 0 ); - - // detect FADDs - vFadds = Gia_ManDetectFullAdders( p, fVerbose ); - assert( Vec_IntSize(vFadds) % 5 == 0 ); - // map MAJ into its FADD - vMap = Gia_ManCreateMap( p, vFadds ); - // for each FADD, find the longest chain and reorder its inputs - Gia_ManFindChains( p, vFadds, vMap ); - // returns the set of topmost MAJ nodes - vChains = Gia_ManCollectTopmost( p, vFadds, vMap, nFaddMin ); - if ( fVerbose ) - Gia_ManPrintChains( p, vFadds, vMap, vChains ); - if ( Vec_WecSize(vChains) == 0 ) - { - Vec_IntFree( vFadds ); - Vec_IntFree( vMap ); - Vec_WecFree( vChains ); - return Gia_ManDup( p ); - } - // returns mapping of each MAJ into the topmost elements of its chain - vMap2Chain = Gia_ManFindMapping( p, vFadds, vMap, vChains ); - // compute truth tables for FADDs - vTruths = Gia_ManCollectTruthTables( p, vFadds ); - if ( fVerbose ) - Abc_PrintTime( 1, "Carry-chain detection time", Abc_Clock() - clk ); - - // duplicate - clk = Abc_Clock(); - 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; - Gia_ManForEachCi( p, pObj, i ) - pObj->Value = Gia_ManAppendCi( pNew ); - Vec_WecForEachLevel( vChains, vChain, i ) - Gia_ManDupFadd( pNew, p, vChain, vFadds, vMap, vChains, vMap2Chain, vTruths ); - Gia_ManForEachCo( p, pObj, i ) - Gia_ManDupWithFaddBoxes_rec( pNew, p, Gia_ObjFanin0(pObj), vFadds, vMap, vChains, vMap2Chain, vTruths ); - Gia_ManForEachCo( p, pObj, i ) - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); - if ( Gia_ManRegNum(p) ) - { - if ( fVerbose ) - printf( "Warning: Sequential design is coverted into combinational one by adding white boxes.\n" ); - pNew->nRegs = 0; - } - assert( !Gia_ManHasDangling(pNew) ); - - // cleanup - Vec_IntFree( vFadds ); - Vec_IntFree( vMap ); - Vec_WecFree( vChains ); - Vec_IntFree( vMap2Chain ); - Vec_IntFree( vTruths ); - - // other information - nBoxes = (Gia_ManCiNum(pNew) - Gia_ManCiNum(p)) / 2; - assert( nBoxes == (Gia_ManCoNum(pNew) - Gia_ManCoNum(p)) / 3 ); - pNew->pManTime = Gia_ManGenerateTim( Gia_ManCiNum(p), Gia_ManCoNum(p), nBoxes, 3, 2 ); - pNew->pAigExtra = Gia_ManGenerateExtraAig( nBoxes, 3, 2 ); -/* - // normalize - pNew = Gia_ManDupNormalize( pTemp = pNew, 0 ); - pNew->pManTime = pTemp->pManTime; pTemp->pManTime = NULL; - pNew->pAigExtra = pTemp->pAigExtra; pTemp->pAigExtra = NULL; - Gia_ManStop( pTemp ); -*/ - //pNew = Gia_ManDupCollapse( pTemp = pNew, pNew->pAigExtra, NULL ); - //Gia_ManStop( pTemp ); - - //Gia_ManIllustrateBoxes( pNew ); - if ( fVerbose ) - Abc_PrintTime( 1, "AIG with boxes construction time", Abc_Clock() - clk ); - return pNew; -} - -/**Function************************************************************* - - Synopsis [Converting AIG with annotated carry-chains into AIG with boxes.] - - Description [Assumes that annotations are pObj->fMark0 or pObj->fMark1. - Only one of these can be set to 1. If fMark0 (fMark1) is set to 1, - the first (second) input of an AND-gate is chained.] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -int Gia_ObjFanin0CopyCarry( Vec_Int_t * vCarries, Gia_Obj_t * pObj, int Id ) -{ - if ( vCarries == NULL || Vec_IntEntry(vCarries, Gia_ObjFaninId0(pObj, Id)) == -1 ) - return Gia_ObjFanin0Copy(pObj); - return Abc_LitNotCond( Vec_IntEntry(vCarries, Gia_ObjFaninId0(pObj, Id)), Gia_ObjFaninC0(pObj) ); -} -int Gia_ObjFanin1CopyCarry( Vec_Int_t * vCarries, Gia_Obj_t * pObj, int Id ) -{ - if ( vCarries == NULL || Vec_IntEntry(vCarries, Gia_ObjFaninId1(pObj, Id)) == -1 ) - return Gia_ObjFanin1Copy(pObj); - return Abc_LitNotCond( Vec_IntEntry(vCarries, Gia_ObjFaninId1(pObj, Id)), Gia_ObjFaninC1(pObj) ); -} -Gia_Man_t * Gia_ManDupWithArtificalFaddBoxes( Gia_Man_t * p, int fUseFanout, int fXorTrick ) -{ - Gia_Man_t * pNew; - Gia_Obj_t * pObj; - int nBoxes = Gia_ManBoxNum(p); - int i, nRealPis, nRealPos; - Vec_Int_t * vCarries = NULL; - // make sure two chains do not overlap - Gia_ManCleanPhase( p ); - Gia_ManForEachCi( p, pObj, i ) - assert( !pObj->fMark0 && !pObj->fMark1 ); - Gia_ManForEachCo( p, pObj, i ) - assert( !pObj->fMark0 && !pObj->fMark1 ); - Gia_ManForEachAnd( p, pObj, i ) - { - assert( !pObj->fMark0 || !pObj->fMark1 ); - if ( pObj->fMark0 ) - { - assert( Gia_ObjFanin0(pObj)->fPhase == 0 ); - Gia_ObjFanin0(pObj)->fPhase = 1; - } - if ( pObj->fMark1 ) - { - assert( Gia_ObjFanin1(pObj)->fPhase == 0 ); - Gia_ObjFanin1(pObj)->fPhase = 1; - } - } - // create mapping for carry-chains - if ( !fUseFanout ) - vCarries = Vec_IntStartFull( Gia_ManObjNum(p) ); - // create references and discount carries - if ( vCarries ) - { - Gia_ManCreateRefs( p ); - Gia_ManForEachAnd( p, pObj, i ) - if ( pObj->fMark0 ) - Gia_ObjRefFanin0Dec( p, pObj ); - else if ( pObj->fMark1 ) - Gia_ObjRefFanin1Dec( p, pObj ); - } - // if AIG already has (natural) FADD boxes, it should not un-normalized - 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; - Gia_ManForEachObj1( p, pObj, i ) - { - if ( Gia_ObjIsCi(pObj) ) - pObj->Value = Gia_ManAppendCi( pNew ); - else if ( Gia_ObjIsCo(pObj) ) - pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); - else if ( !pObj->fMark0 && !pObj->fMark1 ) // AND-gate - pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - else // AND-gate with chain - { - int iCiLit, iOtherLit, iLit0, iLit1, iLit2, iXorLit; - assert( pObj->fMark0 != pObj->fMark1 ); - iCiLit = pObj->fMark0 ? Gia_ObjFanin0CopyCarry(vCarries, pObj, i) : Gia_ObjFanin1CopyCarry(vCarries, pObj, i); - iOtherLit = pObj->fMark0 ? Gia_ObjFanin1Copy(pObj) : Gia_ObjFanin0Copy(pObj); - assert( iCiLit >= 0 && iOtherLit >= 0 ); - iLit0 = Abc_LitNotCond( iCiLit, Abc_LitIsCompl(iCiLit) ); - iLit1 = Abc_LitNotCond( iOtherLit, Abc_LitIsCompl(iCiLit) ); - iLit2 = Abc_LitNotCond( 0, Abc_LitIsCompl(iCiLit) ); - // add COs - assert( !Abc_LitIsCompl(iLit0) ); - Gia_ManAppendCo( pNew, iLit0 ); - Gia_ManAppendCo( pNew, iLit1 ); - Gia_ManAppendCo( pNew, iLit2 ); - // add CI (unused sum bit) - iXorLit = Gia_ManAppendCi(pNew); - // add CI (carry bit) - pObj->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), Abc_LitIsCompl(iCiLit) ); - if ( vCarries && pObj->fPhase ) - { - Vec_IntWriteEntry( vCarries, i, pObj->Value ); - if ( Gia_ObjRefNum(p, pObj) > 0 ) - { - if ( fXorTrick ) - pObj->Value = Gia_ManAppendAnd( pNew, Abc_LitNotCond(iXorLit, !Abc_LitIsCompl(iCiLit)), iOtherLit ); - else - pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); - } - } - nBoxes++; - } - } - Gia_ManCleanPhase( p ); - Vec_IntFreeP( &vCarries ); - ABC_FREE( p->pRefs ); - assert( !Gia_ManHasDangling(pNew) ); - // other information -// nBoxes += (Gia_ManCiNum(pNew) - Gia_ManCiNum(p)) / 2; -// assert( nBoxes == Gia_ManBoxNum(p) + (Gia_ManCoNum(pNew) - Gia_ManCoNum(p)) / 3 ); - nRealPis = Gia_ManBoxNum(p) ? Tim_ManPiNum((Tim_Man_t *)p->pManTime) : Gia_ManCiNum(p); - nRealPos = Gia_ManBoxNum(p) ? Tim_ManPoNum((Tim_Man_t *)p->pManTime) : Gia_ManCoNum(p); - pNew->pManTime = Gia_ManGenerateTim( nRealPis, nRealPos, nBoxes, 3, 2 ); - pNew->pAigExtra = Gia_ManGenerateExtraAig( nBoxes, 3, 2 ); - // optionally normalize the AIG - return pNew; -} -Gia_Man_t * Gia_ManDupWithArtificalFaddBoxesTest( Gia_Man_t * p ) -{ - Gia_Man_t * pNew; - Gia_Obj_t * pObj; - int i; - // label some and-gates - Gia_ManCleanMark01( p ); - Gia_ManForEachAnd( p, pObj, i ) - { - pObj->fMark0 = i % 5; - pObj->fMark1 = i % 7; - if ( pObj->fMark0 && pObj->fMark1 ) - pObj->fMark0 = pObj->fMark1 = 0; - } - - // output new AIG - pNew = Gia_ManDupWithArtificalFaddBoxes( p, 0, 0 ); - Gia_ManCleanMark01( p ); - return pNew; -} - -/**Function************************************************************* - - Synopsis [Adds artificial carry chains to the manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -// computes AIG delay information when boxes are used -int Gia_ManFindAnnotatedDelay( Gia_Man_t * p, int DelayC, int * pnBoxes, int fIgnoreBoxDelays ) -{ - Gia_Obj_t * pObj; - int nRealPis = Gia_ManBoxNum(p) ? Tim_ManPiNum((Tim_Man_t *)p->pManTime) : Gia_ManCiNum(p); - int * pDelays = Vec_IntArray(p->vLevels); - int i, k, iBox, iBoxOutId, Delay, Delay0, Delay1, DelayMax = 0, nBoxes = 0; - Vec_IntFill( p->vLevels, Gia_ManObjNum(p), 0 ); - Gia_ManForEachObj1( p, pObj, i ) - { - if ( Gia_ObjIsCi(pObj) ) - { - if ( fIgnoreBoxDelays ) - continue; - // check if it is real PI - iBoxOutId = Gia_ObjCioId(pObj) - nRealPis; - if ( iBoxOutId < 0 ) - continue; - // if it is a box output, find box number - iBox = iBoxOutId / 2; - assert( iBox < Gia_ManBoxNum(p) ); - // check find the maximum delay of the box inputs - Delay = 0; - for ( k = 0; k < 3; k++ ) - { - int Id = Gia_ObjId( p, Gia_ManCo(p, iBox*3+k) ); - assert( Id < i ); - Delay = Abc_MaxInt( Delay, pDelays[Id] ); - } - // consider outputs - if ( iBoxOutId & 1 ) // carry output - Delay += DelayC; - else // sum output - Delay += 100; - pDelays[i] = Delay; - continue; - } - if ( Gia_ObjIsCo(pObj) ) - { - pDelays[i] = pDelays[Gia_ObjFaninId0(pObj, i)]; - DelayMax = Abc_MaxInt( DelayMax, pDelays[i] ); - continue; - } - assert( !pObj->fMark0 || !pObj->fMark1 ); - Delay0 = pDelays[Gia_ObjFaninId0(pObj, i)]; - Delay1 = pDelays[Gia_ObjFaninId1(pObj, i)]; - if ( pObj->fMark0 ) - { - Delay = Abc_MaxInt( Delay0 + DelayC, Delay1 + 100 ); - nBoxes++; - } - else if ( pObj->fMark1 ) - { - Delay = Abc_MaxInt( Delay1 + DelayC, Delay0 + 100 ); - nBoxes++; - } - else - Delay = Abc_MaxInt( Delay0 + 100, Delay1 + 100 ); - pDelays[i] = Delay; - } - if ( pnBoxes ) - *pnBoxes = nBoxes; - return DelayMax; -} -// check if the object is already used in some chain -static inline int Gia_ObjIsUsed( Gia_Obj_t * pObj ) -{ - return pObj->fMark0 || pObj->fMark1 || pObj->fPhase; -} -// finds internal node that can begin a new chain -int Gia_ManFindChainStart( Gia_Man_t * p ) -{ - Gia_Obj_t * pObj; - int * pDelays = Vec_IntArray(p->vLevels); - int i, iMax = -1, DelayMax = 0; - Gia_ManForEachAnd( p, pObj, i ) - { - if ( Gia_ObjIsUsed(pObj) ) - continue; - if ( DelayMax > pDelays[i] ) - continue; - DelayMax = pDelays[i]; - iMax = i; - } - return iMax; -} -// finds a sequence of internal nodes that creates a new chain -int Gia_ManFindPath( Gia_Man_t * p, int DelayC, int nPathMin, int nPathMax, Vec_Int_t * vPath ) -{ - Gia_Obj_t * pObj, * pFanin0, * pFanin1; - int * pDelays = Vec_IntArray(p->vLevels); - int i, iLit, iMax = Gia_ManFindChainStart( p ); - if ( iMax == -1 ) - return -1; - Vec_IntClear( vPath ); - pObj = Gia_ManObj(p, iMax); - assert( Gia_ObjIsAnd(pObj) ); - while ( Gia_ObjIsAnd(pObj) ) - { - assert( !Gia_ObjIsUsed(pObj) ); - pFanin0 = Gia_ObjFanin0(pObj); - pFanin1 = Gia_ObjFanin1(pObj); - if ( Gia_ObjIsUsed(pFanin0) && Gia_ObjIsUsed(pFanin1) ) - break; - if ( Gia_ObjIsUsed(pFanin0) ) - { - Vec_IntPush( vPath, Abc_Var2Lit(Gia_ObjId(p, pObj), 1) ); - pObj = pFanin1; - } - else if ( Gia_ObjIsUsed(pFanin1) ) - { - Vec_IntPush( vPath, Abc_Var2Lit(Gia_ObjId(p, pObj), 0) ); - pObj = pFanin0; - } - else - { - if ( pDelays[Gia_ObjId(p, pFanin1)] > pDelays[Gia_ObjId(p, pFanin0)] ) - { - Vec_IntPush( vPath, Abc_Var2Lit(Gia_ObjId(p, pObj), 1) ); - pObj = pFanin1; - } - else - { - Vec_IntPush( vPath, Abc_Var2Lit(Gia_ObjId(p, pObj), 0) ); - pObj = pFanin0; - } - } - } - if ( Vec_IntSize(vPath) < nPathMin ) - { - Gia_ManObj(p, iMax)->fPhase = 1; - return 0; - } - // label nodes - if ( Vec_IntSize(vPath) > nPathMax ) - Vec_IntShrink( vPath, nPathMax ); - Vec_IntForEachEntry( vPath, iLit, i ) - { - pObj = Gia_ManObj( p, Abc_Lit2Var(iLit) ); - if ( Abc_LitIsCompl(iLit) ) - { - assert( pObj->fMark1 == 0 ); - pObj->fMark1 = 1; - assert( Gia_ObjFanin1(pObj)->fPhase == 0 ); - Gia_ObjFanin1(pObj)->fPhase = 1; - } - else - { - assert( pObj->fMark0 == 0 ); - pObj->fMark0 = 1; - assert( Gia_ObjFanin0(pObj)->fPhase == 0 ); - Gia_ObjFanin0(pObj)->fPhase = 1; - } - } - return Vec_IntSize(vPath); -} -// iteratively create the given number of chains -int Gia_ManIteratePaths( Gia_Man_t * p, int DelayC, int nPathMin, int nPathMax, int nPathLimit, int fIgnoreBoxDelays, int fVerbose ) -{ - Gia_Obj_t * pObj; - Vec_Int_t * vPath = Vec_IntAlloc( 100 ); - int i, RetValue, nBoxes, MaxDelay, nPaths = 0; - assert( p->vLevels == NULL ); - p->vLevels = Vec_IntStart( Gia_ManObjNum(p) ); - Gia_ManCleanMark01( p ); - Gia_ManCleanPhase( p ); - Gia_ManForEachCi( p, pObj, i ) - pObj->fPhase = 1; - if ( fVerbose ) - printf( "Running path detection: BoxDelay = %d, PathMin = %d, PathMax = %d, PathLimit = %d.\n", DelayC, nPathMin, nPathMax, nPathLimit ); - for ( i = 0; i < nPathLimit; i++ ) - { - MaxDelay = Gia_ManFindAnnotatedDelay( p, DelayC, &nBoxes, fIgnoreBoxDelays ); - RetValue = Gia_ManFindPath( p, DelayC, nPathMin, nPathMax, vPath ); - if ( RetValue == -1 ) - break; - nPaths += (RetValue > 0); - if ( fVerbose ) - printf( "Iter %5d : Paths = %2d. Boxes = %2d. Total boxes = %6d. Max delay = %5d.\n", i, nPaths, RetValue, nBoxes, MaxDelay ); - } - Vec_IntFree( vPath ); - Vec_IntFreeP( &p->vLevels ); - Gia_ManCleanPhase( p ); - return 1; -} -// annotate artificial chains and then put them into boxes -Gia_Man_t * Gia_ManDupWithArtificialBoxes( Gia_Man_t * p, int DelayC, int nPathMin, int nPathMax, int nPathLimit, int fUseFanout, int fXorTrick, int fIgnoreBoxDelays, int fVerbose ) -{ - Gia_Man_t * pNew; -/* - if ( Gia_ManBoxNum(p) > 0 ) - { - printf( "Currently artifical carry-chains cannot be detected when natural ones are present.\n" ); - return NULL; - } -*/ - Gia_ManIteratePaths( p, DelayC, nPathMin, nPathMax, nPathLimit, fIgnoreBoxDelays, fVerbose ); - pNew = Gia_ManDupWithArtificalFaddBoxes( p, fUseFanout, fXorTrick ); - Gia_ManCleanMark01( p ); - return pNew; -} - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c index 58c65b99..725f03af 100644 --- a/src/aig/gia/giaHash.c +++ b/src/aig/gia/giaHash.c @@ -575,6 +575,7 @@ int Gia_ManHashMuxReal( Gia_Man_t * p, int iLitC, int iLit1, int iLit0 ) ***********************************************************************/ int Gia_ManHashAnd( Gia_Man_t * p, int iLit0, int iLit1 ) { +// return Gia_ManAppendAnd2( p, iLit0, iLit1 ); if ( iLit0 < 2 ) return iLit0 ? iLit1 : 0; if ( iLit1 < 2 ) diff --git a/src/aig/gia/giaMuxes.c b/src/aig/gia/giaMuxes.c index 3a55d6ca..c38cbf43 100644 --- a/src/aig/gia/giaMuxes.c +++ b/src/aig/gia/giaMuxes.c @@ -100,7 +100,7 @@ Gia_Man_t * Gia_ManDupMuxes( Gia_Man_t * p, int Limit ) Gia_Obj_t * pObj, * pFan0, * pFan1, * pFanC, * pSiblNew, * pObjNew; int i; assert( p->pMuxes == NULL ); - assert( Limit >= 2 ); + assert( Limit >= 1 ); // allows to create AIG with XORs without MUXes ABC_FREE( p->pRefs ); Gia_ManCreateRefs( p ); // start the new manager diff --git a/src/aig/gia/giaPolyn.c b/src/aig/gia/giaPolyn.c deleted file mode 100644 index 4e8d7378..00000000 --- a/src/aig/gia/giaPolyn.c +++ /dev/null @@ -1,516 +0,0 @@ -/**CFile**************************************************************** - - FileName [giaPolyn.c] - - SystemName [ABC: Logic synthesis and verification system.] - - PackageName [Scalable AIG package.] - - Synopsis [Polynomial manipulation.] - - Author [Alan Mishchenko] - - Affiliation [UC Berkeley] - - Date [Ver. 1.0. Started - June 20, 2005.] - - Revision [$Id: giaPolyn.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] - -***********************************************************************/ - -#include "gia.h" -#include "misc/vec/vecWec.h" -#include "misc/vec/vecHsh.h" -#include "misc/vec/vecQue.h" - -ABC_NAMESPACE_IMPL_START - - -//////////////////////////////////////////////////////////////////////// -/// DECLARATIONS /// -//////////////////////////////////////////////////////////////////////// - -/* -!a -> 1 - a -a & b -> ab -a | b -> a + b - ab -a ^ b -> a + b - 2ab -MUX(a, b, c) -> ab | (1 - a)c = ab + (1-a)c - ab(1-a)c = ab + c - ac - -!a & b -> (1 - a)b = b - ab - a & !b -> a(1 - b) = a - ab -!a & !b -> 1 - a - b + ab -!(a & b) -> 1 - ab -*/ - -//////////////////////////////////////////////////////////////////////// -/// FUNCTION DEFINITIONS /// -//////////////////////////////////////////////////////////////////////// - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -void Gia_PolynAddNew( Hsh_VecMan_t * pHash, Vec_Int_t * vCoef, int Coef, Vec_Int_t * vProd, Vec_Wec_t * vMap ) -{ - int i, Lit, Value; - //Vec_IntPrint( vProd ); - - Value = Hsh_VecManAdd( pHash, vProd ); - if ( Value == Vec_IntSize(vCoef) ) - { - Vec_IntPush( vCoef, 0 ); - Vec_IntForEachEntry( vProd, Lit, i ) - Vec_WecPush( vMap, Abc_Lit2Var(Lit), Value ); - } - assert( Value < Vec_IntSize(vCoef) ); - Vec_IntAddToEntry( vCoef, Value, Coef ); -} -int Gia_PolynTransform1( Hsh_VecMan_t * pHash, Vec_Int_t * vCoef, int Coef, Vec_Int_t * vProd, Vec_Wec_t * vMap, int Id ) -{ - int i, Lit; - Vec_IntForEachEntry( vProd, Lit, i ) - if ( Abc_Lit2Var(Lit) == Id ) - break; - assert( i < Vec_IntSize(vProd) ); - if ( !Abc_LitIsCompl(Lit) ) - return 0; - // update array - Vec_IntWriteEntry( vProd, i, Abc_LitNot(Lit) ); - Gia_PolynAddNew( pHash, vCoef, Coef, vProd, vMap ); - Vec_IntWriteEntry( vProd, i, Lit ); - return 1; -} -void Gia_PolynTransform( Hsh_VecMan_t * pHash, Vec_Int_t * vCoef, int Coef, Vec_Int_t * vProd, Vec_Wec_t * vMap, int Id, int Lit0, int Lit1, Vec_Int_t * vTemp ) -{ - int pArray[2] = { Lit0, Lit1 }; - Vec_Int_t vTwo = { 2, 2, pArray }; - - int Var0 = Abc_Lit2Var( Lit0 ); - int Var1 = Abc_Lit2Var( Lit1 ); - int i, Lit = Vec_IntPop(vProd); - - assert( Abc_Lit2Var(Lit) == Id ); - if ( Abc_LitIsCompl(Lit) ) - { - Gia_PolynAddNew( pHash, vCoef, Coef, vProd, vMap ); - Coef = -Coef; - } - - assert( Var0 < Var1 ); - Vec_IntForEachEntry( vProd, Lit, i ) - if ( Abc_LitNot(Lit) == Lit0 || Abc_LitNot(Lit) == Lit1 ) - return; - assert( Vec_IntCap(vTemp) >= Vec_IntSize(vTemp) + 2 ); - - // merge inputs - Vec_IntTwoMerge2Int( vProd, &vTwo, vTemp ); -/* - printf( "\n" ); - Vec_IntPrint( vProd ); - Vec_IntPrint( &vTwo ); - Vec_IntPrint( vTemp ); - printf( "\n" ); -*/ - // create new - Gia_PolynAddNew( pHash, vCoef, Coef, vTemp, vMap ); -} -int Gia_PolynPrint( Hsh_VecMan_t * pHash, Vec_Int_t * vCoef ) -{ - Vec_Int_t * vProd; - int Value, Coef, Lit, i, Count = 0; - Vec_IntForEachEntry( vCoef, Coef, Value ) - { - if ( Coef == 0 ) - continue; - vProd = Hsh_VecReadEntry( pHash, Value ); - printf( "(%d)", Coef ); - Vec_IntForEachEntry( vProd, Lit, i ) - printf( "*%d", Lit ); - printf( " " ); - Count++; - } - printf( "\n" ); - return Count; -} -void Gia_PolynTest( Gia_Man_t * pGia ) -{ - Hsh_VecMan_t * pHash = Hsh_VecManStart( 1000000 ); - Vec_Int_t * vCoef = Vec_IntAlloc( 1000000 ); - Vec_Wec_t * vMap = Vec_WecStart( Gia_ManObjNum(pGia) ); - Vec_Int_t * vTemp = Vec_IntAlloc( 100000 ); - Vec_Int_t * vThisOne, * vProd; - Gia_Obj_t * pObj; - int i, k, Value, Coef, Count; - abctime clk = Abc_Clock(); - - assert( Gia_ManPoNum(pGia) < 32 ); - - // add constant - Value = Hsh_VecManAdd( pHash, vTemp ); - assert( Value == 0 ); - Vec_IntPush( vCoef, 0 ); - - // start the outputs - Gia_ManForEachPo( pGia, pObj, i ) - { - assert( Gia_ObjFaninId0p(pGia, pObj) > 0 ); - Vec_IntFill( vTemp, 1, Gia_ObjFaninLit0p(pGia, pObj) ); - Value = Hsh_VecManAdd( pHash, vTemp ); - //assert( Value == i + 1 ); - Vec_IntPush( vCoef, 1 << i ); - Vec_WecPush( vMap, Gia_ObjFaninId0p(pGia, pObj), Value ); - } - assert( Vec_IntSize(vCoef) == Hsh_VecSize(pHash) ); - - Gia_PolynPrint( pHash, vCoef ); - - // substitute - Gia_ManForEachAndReverse( pGia, pObj, i ) - { - vThisOne = Vec_WecEntry( vMap, i ); - assert( Vec_IntSize(vThisOne) > 0 ); - Vec_IntForEachEntry( vThisOne, Value, k ) - { - vProd = Hsh_VecReadEntry( pHash, Value ); - Coef = Vec_IntEntry( vCoef, Value ); - if ( Coef == 0 ) - continue; - Gia_PolynTransform( pHash, vCoef, Coef, vProd, vMap, i, Gia_ObjFaninLit0p(pGia, pObj), Gia_ObjFaninLit1p(pGia, pObj), vTemp ); - Vec_IntWriteEntry( vCoef, Value, 0 ); - } - Vec_IntErase( vThisOne ); - } - - // inputs - Gia_ManForEachCiReverse( pGia, pObj, i ) - { - vThisOne = Vec_WecEntry( vMap, Gia_ObjId(pGia, pObj) ); - if ( Vec_IntSize(vThisOne) == 0 ) - continue; - assert( Vec_IntSize(vThisOne) > 0 ); - Vec_IntForEachEntry( vThisOne, Value, k ) - { - vProd = Hsh_VecReadEntry( pHash, Value ); - Coef = Vec_IntEntry( vCoef, Value ); - if ( Coef == 0 ) - continue; - if ( Gia_PolynTransform1( pHash, vCoef, Coef, vProd, vMap, Gia_ObjId(pGia, pObj) ) ) - Vec_IntWriteEntry( vCoef, Value, 0 ); - } - Vec_IntErase( vThisOne ); - } - - Count = Gia_PolynPrint( pHash, vCoef ); - printf( "Entries = %d. Useful = %d. ", Vec_IntSize(vCoef), Count ); - Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); - - Hsh_VecManStop( pHash ); - Vec_IntFree( vCoef ); - Vec_WecFree( vMap ); - Vec_IntFree( vTemp ); -} - - - - - -typedef struct Pln_Man_t_ Pln_Man_t; -struct Pln_Man_t_ -{ - Gia_Man_t * pGia; // AIG manager - Hsh_VecMan_t * pHashC; // hash table for constants - Hsh_VecMan_t * pHashM; // hash table for monomials - Vec_Que_t * vQue; // queue by largest node - Vec_Flt_t * vCounts; // largest node - Vec_Int_t * vCoefs; // coefficients for each monomial - Vec_Int_t * vTempC[2]; // polynomial representation - Vec_Int_t * vTempM[4]; // polynomial representation - int nBuilds; // builds -}; - -/**Function************************************************************* - - Synopsis [Computation manager.] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -Pln_Man_t * Pln_ManAlloc( Gia_Man_t * pGia ) -{ - Pln_Man_t * p = ABC_CALLOC( Pln_Man_t, 1 ); - p->pGia = pGia; - p->pHashC = Hsh_VecManStart( 1000 ); - p->pHashM = Hsh_VecManStart( 1000 ); - p->vQue = Vec_QueAlloc( 1000 ); - p->vCounts = Vec_FltAlloc( 1000 ); - p->vCoefs = Vec_IntAlloc( 1000 ); - p->vTempC[0] = Vec_IntAlloc( 100 ); - p->vTempC[1] = Vec_IntAlloc( 100 ); - p->vTempM[0] = Vec_IntAlloc( 100 ); - p->vTempM[1] = Vec_IntAlloc( 100 ); - p->vTempM[2] = Vec_IntAlloc( 100 ); - p->vTempM[3] = Vec_IntAlloc( 100 ); - Vec_QueSetPriority( p->vQue, Vec_FltArrayP(p->vCounts) ); - // add 0-constant and 1-monomial - Hsh_VecManAdd( p->pHashC, p->vTempC[0] ); - Hsh_VecManAdd( p->pHashM, p->vTempM[0] ); - Vec_FltPush( p->vCounts, 0 ); - Vec_IntPush( p->vCoefs, 0 ); - return p; -} -void Pln_ManStop( Pln_Man_t * p ) -{ - Hsh_VecManStop( p->pHashC ); - Hsh_VecManStop( p->pHashM ); - Vec_QueFree( p->vQue ); - Vec_FltFree( p->vCounts ); - Vec_IntFree( p->vCoefs ); - Vec_IntFree( p->vTempC[0] ); - Vec_IntFree( p->vTempC[1] ); - Vec_IntFree( p->vTempM[0] ); - Vec_IntFree( p->vTempM[1] ); - Vec_IntFree( p->vTempM[2] ); - Vec_IntFree( p->vTempM[3] ); - ABC_FREE( p ); -} -void Pln_ManPrintFinal( Pln_Man_t * p ) -{ - Vec_Int_t * vArray; - int k, Entry, iMono, iConst, Count = 0; - Vec_IntForEachEntry( p->vCoefs, iConst, iMono ) - { - if ( iConst == 0 ) - continue; - - Count++; - - if ( Vec_IntSize(p->vCoefs) > 1000 ) - continue; - - vArray = Hsh_VecReadEntry( p->pHashC, iConst ); - Vec_IntForEachEntry( vArray, Entry, k ) - printf( "%s%s2^%d", k ? " + " : "", Entry < 0 ? "-" : "+", Abc_AbsInt(Entry)-1 ); - - vArray = Hsh_VecReadEntry( p->pHashM, iMono ); - Vec_IntForEachEntry( vArray, Entry, k ) - printf( " * %d", Entry ); - printf( "\n" ); - } - printf( "HashC = %d. HashM = %d. Total = %d. Used = %d.\n", Hsh_VecSize(p->pHashC), Hsh_VecSize(p->pHashM), p->nBuilds, Count ); -} - -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static inline void Gia_PolynMergeConstOne( Vec_Int_t * vConst, int New ) -{ - int i, Old; - assert( New != 0 ); - Vec_IntForEachEntry( vConst, Old, i ) - { - assert( Old != 0 ); - if ( Old == New ) // A == B - { - Vec_IntDrop( vConst, i ); - Gia_PolynMergeConstOne( vConst, New > 0 ? New + 1 : New - 1 ); - return; - } - if ( Abc_AbsInt(Old) == Abc_AbsInt(New) ) // A == -B - { - Vec_IntDrop( vConst, i ); - return; - } - if ( Old + New == 1 || Old + New == -1 ) // sign(A) != sign(B) && abs(abs(A)-abs(B)) == 1 - { - int Value = Abc_MinInt( Abc_AbsInt(Old), Abc_AbsInt(New) ); - Vec_IntDrop( vConst, i ); - Gia_PolynMergeConstOne( vConst, (Old + New == 1) ? Value : -Value ); - return; - } - } - Vec_IntPushUniqueOrder( vConst, New ); -} -static inline void Gia_PolynMergeConst( Vec_Int_t * vConst, Pln_Man_t * p, int iConstAdd ) -{ - int i, New; - Vec_Int_t * vConstAdd = Hsh_VecReadEntry( p->pHashC, iConstAdd ); - Vec_IntForEachEntry( vConstAdd, New, i ) - { - Gia_PolynMergeConstOne( vConst, New ); - vConstAdd = Hsh_VecReadEntry( p->pHashC, iConstAdd ); - } -} -static inline void Gia_PolynBuildAdd( Pln_Man_t * p, Vec_Int_t * vTempC, Vec_Int_t * vTempM ) -{ - int iConst, iMono = vTempM ? Hsh_VecManAdd(p->pHashM, vTempM) : 0; - p->nBuilds++; - if ( iMono == Vec_IntSize(p->vCoefs) ) // new monomial - { - iConst = Hsh_VecManAdd( p->pHashC, vTempC ); - Vec_IntPush( p->vCoefs, iConst ); - Vec_FltPush( p->vCounts, Vec_IntEntryLast(vTempM) ); - Vec_QuePush( p->vQue, iMono ); -// Vec_QueUpdate( p->vQue, iMono ); - return; - } - // this monomial exists - iConst = Vec_IntEntry( p->vCoefs, iMono ); - if ( iConst ) - Gia_PolynMergeConst( vTempC, p, iConst ); - iConst = Hsh_VecManAdd( p->pHashC, vTempC ); - Vec_IntWriteEntry( p->vCoefs, iMono, iConst ); -} -void Gia_PolynBuildOne( Pln_Man_t * p, int iMono ) -{ - Gia_Obj_t * pObj; - Vec_Int_t * vArray, * vConst; - int iFan0, iFan1; - int k, iConst, iDriver; - - assert( Vec_IntSize(p->vCoefs) == Hsh_VecSize(p->pHashM) ); - vArray = Hsh_VecReadEntry( p->pHashM, iMono ); - iDriver = Vec_IntEntryLast( vArray ); - pObj = Gia_ManObj( p->pGia, iDriver ); - if ( !Gia_ObjIsAnd(pObj) ) - return; - - iConst = Vec_IntEntry( p->vCoefs, iMono ); - if ( iConst == 0 ) - return; - Vec_IntWriteEntry( p->vCoefs, iMono, 0 ); - - iFan0 = Gia_ObjFaninId0p(p->pGia, pObj); - iFan1 = Gia_ObjFaninId1p(p->pGia, pObj); - for ( k = 0; k < 4; k++ ) - { - Vec_IntClear( p->vTempM[k] ); - Vec_IntAppend( p->vTempM[k], vArray ); - Vec_IntPop( p->vTempM[k] ); - if ( k == 1 || k == 3 ) - Vec_IntPushUniqueOrder( p->vTempM[k], iFan0 ); // x - if ( k == 2 || k == 3 ) - Vec_IntPushUniqueOrder( p->vTempM[k], iFan1 ); // y - } - - vConst = Hsh_VecReadEntry( p->pHashC, iConst ); - for ( k = 0; k < 2; k++ ) - Vec_IntAppendMinus( p->vTempC[k], vConst, k ); - - if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) // C * (1 - x) * (1 - y) - { - Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[0] ); // C * 1 - Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[1] ); // -C * x - vConst = Hsh_VecReadEntry( p->pHashC, iConst ); - for ( k = 0; k < 2; k++ ) - Vec_IntAppendMinus( p->vTempC[k], vConst, k ); - Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[2] ); // -C * y - Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[3] ); // C * x * y - } - else if ( Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) ) // C * (1 - x) * y - { - Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[2] ); // C * y - Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[3] ); // -C * x * y - } - else if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) // C * x * (1 - y) - { - Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[1] ); // C * x - Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[3] ); // -C * x * y - } - else - Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[3] ); // C * x * y -} -int Gia_PolyFindNext2( Pln_Man_t * p ) -{ - Gia_Obj_t * pObj; - Vec_Int_t * vArray; - int Max = 0, iBest = 0, iConst, iMono, iDriver; - Vec_IntForEachEntryStart( p->vCoefs, iConst, iMono, 1 ) - { - if ( iConst == 0 ) - continue; - vArray = Hsh_VecReadEntry( p->pHashM, iMono ); - iDriver = Vec_IntEntryLast( vArray ); - pObj = Gia_ManObj( p->pGia, iDriver ); - if ( !Gia_ObjIsAnd(pObj) ) - continue; - if ( Max < Vec_IntEntryLast(vArray) ) - { - Max = Vec_IntEntryLast(vArray); - iBest = iMono; - } - } - //Vec_IntPrint( Hsh_VecReadEntry(p->pHashM, iBest) ); - return iBest; -} -int Gia_PolyFindNext( Pln_Man_t * p ) -{ - int iBest = Vec_QueSize(p->vQue) ? Vec_QuePop(p->vQue) : 0; - //Vec_IntPrint( Hsh_VecReadEntry(p->pHashM, iBest) ); - return iBest; -} -void Gia_PolynBuildTest( Gia_Man_t * pGia ) -{ - abctime clk = Abc_Clock();//, clk2 = 0; - Gia_Obj_t * pObj; - int i, iMono, iDriver; - Pln_Man_t * p = Pln_ManAlloc( pGia ); - Gia_ManForEachCoReverse( pGia, pObj, i ) - { - Vec_IntFill( p->vTempC[0], 1, i+1 ); // 2^i - Vec_IntFill( p->vTempC[1], 1, -i-1 ); // -2^i - - iDriver = Gia_ObjFaninId0p( pGia, pObj ); - Vec_IntFill( p->vTempM[0], 1, iDriver ); // Driver - - if ( Gia_ObjFaninC0(pObj) ) - { - Gia_PolynBuildAdd( p, p->vTempC[0], NULL ); // C - Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[0] ); // -C * Driver - } - else - Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[0] ); // C * Driver - } - while ( 1 ) - { - //abctime temp = Abc_Clock(); - iMono = Gia_PolyFindNext(p); - if ( !iMono ) - break; - Gia_PolynBuildOne( p, iMono ); - //clk2 += Abc_Clock() - temp; - } - Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); - //Abc_PrintTime( 1, "Time2", clk2 ); - Pln_ManPrintFinal( p ); - Pln_ManStop( p ); -} - - - -//////////////////////////////////////////////////////////////////////// -/// END OF FILE /// -//////////////////////////////////////////////////////////////////////// - - -ABC_NAMESPACE_IMPL_END - diff --git a/src/aig/gia/giaShow.c b/src/aig/gia/giaShow.c index fdb6c52e..6224d37f 100644 --- a/src/aig/gia/giaShow.c +++ b/src/aig/gia/giaShow.c @@ -50,9 +50,9 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold ) int LevelMax, Prev, Level, i; int fConstIsUsed = 0; - if ( Gia_ManAndNum(pMan) > 200 ) + if ( Gia_ManAndNum(pMan) > 300 ) { - fprintf( stdout, "Cannot visualize AIG with more than 200 nodes.\n" ); + fprintf( stdout, "Cannot visualize AIG with more than 300 nodes.\n" ); return; } if ( (pFile = fopen( pFileName, "w" )) == NULL ) diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 7da2858e..273597a4 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -23,7 +23,6 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaEra.c \ src/aig/gia/giaEra2.c \ src/aig/gia/giaEsop.c \ - src/aig/gia/giaFadds.c \ src/aig/gia/giaFalse.c \ src/aig/gia/giaFanout.c \ src/aig/gia/giaForce.c \ @@ -52,7 +51,6 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaPack.c \ src/aig/gia/giaPat.c \ src/aig/gia/giaPf.c \ - src/aig/gia/giaPolyn.c \ src/aig/gia/giaQbf.c \ src/aig/gia/giaResub.c \ src/aig/gia/giaRetime.c \ diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index b88fa79d..6d6e16f5 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -43,6 +43,7 @@ #include "opt/ret/retInt.h" #include "sat/cnf/cnf.h" #include "proof/cec/cec.h" +#include "proof/acec/acec.h" #include "proof/pdr/pdr.h" #include "misc/tim/tim.h" #include "bdd/llb/llb.h" @@ -464,6 +465,8 @@ static int Abc_CommandAbc9Bmci ( Abc_Frame_t * pAbc, int argc, cha static int Abc_CommandAbc9PoXsim ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Demiter ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Fadds ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Polyn ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandAbc9Acec ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Esop ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Exorcism ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandAbc9Mfs ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -1092,6 +1095,8 @@ void Abc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "ABC9", "&poxsim", Abc_CommandAbc9PoXsim, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&demiter", Abc_CommandAbc9Demiter, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&fadds", Abc_CommandAbc9Fadds, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&polyn", Abc_CommandAbc9Polyn, 0 ); + Cmd_CommandAdd( pAbc, "ABC9", "&acec", Abc_CommandAbc9Acec, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&esop", Abc_CommandAbc9Esop, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&exorcism", Abc_CommandAbc9Exorcism, 0 ); Cmd_CommandAdd( pAbc, "ABC9", "&mfs", Abc_CommandAbc9Mfs, 0 ); @@ -27760,6 +27765,7 @@ usage: Abc_Print( -2, "\t-c : toggle collapsing hierarchical AIG [default = %s]\n", fCollapse? "yes": "no" ); Abc_Print( -2, "\t-m : toggle converting to larger gates [default = %s]\n", fAddMuxes? "yes": "no" ); Abc_Print( -2, "\t-L num : create MUX when sum of refs does not exceed this limit [default = %d]\n", Limit ); + Abc_Print( -2, "\t (use L = 1 to create AIG with XORs but without MUXes)\n" ); Abc_Print( -2, "\t-r : toggle rehashing AIG while preserving mapping [default = %s]\n", fRehashMap? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); return 1; @@ -39054,14 +39060,22 @@ usage: ***********************************************************************/ int Abc_CommandAbc9Demiter( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern Gia_Man_t * Gia_ManDupDemiter( Gia_Man_t * p, int fVerbose ); Gia_Man_t * pTemp; - int c, fVerbose = 0; + int c, fDumpFiles = 0, fDumpFilesTwo = 0, fDual = 0, fVerbose = 0; Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "ftdvh" ) ) != EOF ) { switch ( c ) { + case 'f': + fDumpFiles ^= 1; + break; + case 't': + fDumpFilesTwo ^= 1; + break; + case 'd': + fDual ^= 1; + break; case 'v': fVerbose ^= 1; break; @@ -39076,20 +39090,57 @@ int Abc_CommandAbc9Demiter( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_Print( -1, "Abc_CommandAbc9Demiter(): There is no AIG.\n" ); return 0; } + if ( fDumpFiles || fDumpFilesTwo ) + { + char pName0[1000] = "miter_part0.aig"; + char pName1[1000] = "miter_part1.aig"; + Gia_Man_t * pPart1, * pPart2; + if ( Gia_ManPoNum(pAbc->pGia) % 2 != 0 ) + { + Abc_Print( -1, "Abc_CommandAbc9Demiter(): Does not look like a dual-output miter.\n" ); + return 0; + } + if ( fDumpFilesTwo ) + Gia_ManDemiterTwoWords( pAbc->pGia, &pPart1, &pPart2 ); + else + Gia_ManDemiterDual( pAbc->pGia, &pPart1, &pPart2 ); + if ( pAbc->pGia->pSpec ) + { + char * pGen = Extra_FileNameGeneric(pAbc->pGia->pSpec); + sprintf( pName0, "%s_1.aig", pGen ); + sprintf( pName1, "%s_2.aig", pGen ); + ABC_FREE( pGen ); + } + Gia_AigerWrite( pPart1, pName0, 0, 0 ); + Gia_AigerWrite( pPart2, pName1, 0, 0 ); + Gia_ManStop( pPart1 ); + Gia_ManStop( pPart2 ); + if ( fDumpFilesTwo ) + printf( "Two parts of the two-word miter are dumped into files \"%s\" and \"%s\".\n", pName0, pName1 ); + else + printf( "Two parts of the dual-output miter are dumped into files \"%s\" and \"%s\".\n", pName0, pName1 ); + return 0; + } if ( Gia_ManPoNum(pAbc->pGia) != 1 ) { Abc_Print( -1, "Abc_CommandAbc9Demiter(): Miter should have one output.\n" ); return 0; } - pTemp = Gia_ManDupDemiter( pAbc->pGia, fVerbose ); + if ( fDual ) + pTemp = Gia_ManDemiterToDual( pAbc->pGia ); + else + pTemp = Gia_ManDupDemiter( pAbc->pGia, fVerbose ); Abc_FrameUpdateGia( pAbc, pTemp ); if ( fVerbose ) Gia_ManPrintStatsMiter( pTemp, 0 ); return 0; usage: - Abc_Print( -2, "usage: &demiter [-vh]\n" ); - Abc_Print( -2, "\t decomposes a single-output miter\n" ); + Abc_Print( -2, "usage: &demiter [-ftdvh]\n" ); + Abc_Print( -2, "\t decomposes a miter (by default, tries to extract an OR gate)\n" ); + Abc_Print( -2, "\t-f : write files with two sides of a dual-output miter [default = %s]\n", fDumpFiles? "yes": "no" ); + Abc_Print( -2, "\t-t : write files with two sides of a two-word miter [default = %s]\n", fDumpFilesTwo? "yes": "no" ); + Abc_Print( -2, "\t-d : take single-output and decompose into dual-output [default = %s]\n", fDual? "yes": "no" ); 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"); return 1; @@ -39237,6 +39288,217 @@ usage: return 1; } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Polyn( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose ); + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF ) + { + switch ( c ) + { + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Esop(): There is no AIG.\n" ); + return 0; + } + Gia_PolynBuild( pAbc->pGia, NULL, fVerbose ); + return 0; + +usage: + Abc_Print( -2, "usage: &polyn [-vh]\n" ); + Abc_Print( -2, "\t derives algebraic polynomial from AIG\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"); + return 1; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Abc_CommandAbc9Acec( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + FILE * pFile; + Cec_ParCec_t ParsCec, * pPars = &ParsCec; + Gia_Man_t * pSecond; + char * FileName, * pTemp; + char ** pArgvNew; + int c, nArgcNew, fMiter = 0, fDualOutput = 0, fTwoOutput = 0; + Cec_ManCecSetDefaultParams( pPars ); + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "CTnmdtvh" ) ) != EOF ) + { + switch ( c ) + { + case 'C': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" ); + goto usage; + } + pPars->nBTLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->nBTLimit < 0 ) + goto usage; + break; + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" ); + goto usage; + } + pPars->TimeLimit = atoi(argv[globalUtilOptind]); + globalUtilOptind++; + if ( pPars->TimeLimit < 0 ) + goto usage; + break; + case 'n': + pPars->fNaive ^= 1; + break; + case 'm': + fMiter ^= 1; + break; + case 'd': + fDualOutput ^= 1; + break; + case 't': + fTwoOutput ^= 1; + break; + case 'v': + pPars->fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( fMiter ) + { + Gia_Man_t * pGia0, * pGia1, * pDual; + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Acec(): There is no AIG.\n" ); + return 1; + } + if ( fDualOutput ) + { + if ( Gia_ManPoNum(pAbc->pGia) & 1 ) + { + Abc_Print( -1, "The dual-output miter should have an even number of outputs.\n" ); + return 1; + } + if ( !pPars->fSilent ) + Abc_Print( 1, "Assuming the current network is a double-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit ); + Gia_ManDemiterDual( pAbc->pGia, &pGia0, &pGia1 ); + pAbc->Status = Gia_PolynCec( pGia0, pGia1, pPars ); + } + else if ( fTwoOutput ) + { + if ( Gia_ManPoNum(pAbc->pGia) & 1 ) + { + Abc_Print( -1, "The dual-output miter should have an even number of outputs.\n" ); + return 1; + } + if ( !pPars->fSilent ) + Abc_Print( 1, "Assuming the current network is a two-word miter. (Conflict limit = %d.)\n", pPars->nBTLimit ); + Gia_ManDemiterTwoWords( pAbc->pGia, &pGia0, &pGia1 ); + pAbc->Status = Gia_PolynCec( pGia0, pGia1, pPars ); + } + else + { + if ( !pPars->fSilent ) + Abc_Print( 1, "Assuming the current network is a single-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit ); + pDual = Gia_ManDemiterToDual( pAbc->pGia ); + Gia_ManDemiterDual( pDual, &pGia0, &pGia1 ); + Gia_ManStop( pDual ); + pAbc->Status = Gia_PolynCec( pGia0, pGia1, pPars ); + } + Abc_FrameReplaceCex( pAbc, &pGia0->pCexComb ); + Gia_ManStop( pGia0 ); + Gia_ManStop( pGia1 ); + return 0; + } + + pArgvNew = argv + globalUtilOptind; + nArgcNew = argc - globalUtilOptind; + if ( nArgcNew != 1 ) + { + if ( pAbc->pGia->pSpec == NULL ) + { + Abc_Print( -1, "File name is not given on the command line.\n" ); + return 1; + } + FileName = pAbc->pGia->pSpec; + } + else + FileName = pArgvNew[0]; + // fix the wrong symbol + for ( pTemp = FileName; *pTemp; pTemp++ ) + if ( *pTemp == '>' ) + *pTemp = '\\'; + if ( (pFile = fopen( FileName, "r" )) == NULL ) + { + Abc_Print( -1, "Cannot open input file \"%s\". ", FileName ); + if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", NULL, NULL, NULL, NULL )) ) + Abc_Print( 1, "Did you mean \"%s\"?", FileName ); + Abc_Print( 1, "\n" ); + return 1; + } + fclose( pFile ); + pSecond = Gia_AigerRead( FileName, 0, 0 ); + if ( pSecond == NULL ) + { + Abc_Print( -1, "Reading AIGER has failed.\n" ); + return 0; + } + pAbc->Status = Gia_PolynCec( pAbc->pGia, pSecond, pPars ); + Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb ); + Gia_ManStop( pSecond ); + return 0; + +usage: + Abc_Print( -2, "usage: &acec [-CT num] [-nmdtvh]\n" ); + Abc_Print( -2, "\t combinational equivalence checking for arithmetic circuits\n" ); + Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit ); + Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit ); + Abc_Print( -2, "\t-n : toggle using naive SAT-based checking [default = %s]\n", pPars->fNaive? "yes":"no"); + Abc_Print( -2, "\t-m : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits"); + Abc_Print( -2, "\t-d : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no"); + Abc_Print( -2, "\t-t : toggle using two-word miter [default = %s]\n", fTwoOutput? "yes":"no"); + Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no"); + Abc_Print( -2, "\t-h : print the command usage\n"); + return 1; +} + /**Function************************************************************* Synopsis [] diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index f3a4f7aa..453cb157 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -125,6 +125,7 @@ typedef struct Wlc_Ntk_t_ Wlc_Ntk_t; struct Wlc_Ntk_t_ { char * pName; // model name + char * pSpec; // input file name Vec_Int_t vPis; // primary inputs Vec_Int_t vPos; // primary outputs Vec_Int_t vCis; // combinational inputs diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index 3a3d614b..6ddd7a60 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -1327,6 +1327,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds ) } assert( Vec_PtrSize(pNew->vNamesOut) == Gia_ManCoNum(pNew) ); */ + pNew->pSpec = Abc_UtilStrsav( p->pSpec ? p->pSpec : p->pName ); return pNew; } diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c index 2f3b07bf..442ddb83 100644 --- a/src/base/wlc/wlcNtk.c +++ b/src/base/wlc/wlcNtk.c @@ -223,6 +223,7 @@ void Wlc_NtkFree( Wlc_Ntk_t * p ) ABC_FREE( p->pInits ); ABC_FREE( p->pObjs ); ABC_FREE( p->pName ); + ABC_FREE( p->pSpec ); ABC_FREE( p ); } int Wlc_NtkMemUsage( Wlc_Ntk_t * p ) @@ -587,6 +588,8 @@ Wlc_Ntk_t * Wlc_NtkDupDfs( Wlc_Ntk_t * p ) if ( p->pInits ) pNew->pInits = Abc_UtilStrsav( p->pInits ); Vec_IntFree( vFanins ); + if ( p->pSpec ) + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); return pNew; } void Wlc_NtkTransferNames( Wlc_Ntk_t * pNew, Wlc_Ntk_t * p ) @@ -658,6 +661,8 @@ Wlc_Ntk_t * Wlc_NtkDupSingleNodes( Wlc_Ntk_t * p ) } Vec_IntFree( vFanins ); Wlc_NtkTransferNames( pNew, p ); + if ( p->pSpec ) + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); return pNew; } diff --git a/src/base/wlc/wlcReadVer.c b/src/base/wlc/wlcReadVer.c index 30525df4..0aedef30 100644 --- a/src/base/wlc/wlcReadVer.c +++ b/src/base/wlc/wlcReadVer.c @@ -1264,6 +1264,7 @@ Wlc_Ntk_t * Wlc_ReadVer( char * pFileName ) finish: Wlc_PrsPrintErrorMessage( p ); Wlc_PrsStop( p ); + pNtk->pSpec = Abc_UtilStrsav( pFileName ); return pNtk; } diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h index e0e2ba7f..f09b8783 100644 --- a/src/misc/vec/vecInt.h +++ b/src/misc/vec/vecInt.h @@ -804,6 +804,24 @@ static inline void Vec_IntPushOrder( Vec_Int_t * p, int Entry ) break; p->pArray[i+1] = Entry; } +static inline void Vec_IntPushOrderCost( Vec_Int_t * p, int Entry, Vec_Int_t * vCost ) +{ + int i; + if ( p->nSize == p->nCap ) + { + if ( p->nCap < 16 ) + Vec_IntGrow( p, 16 ); + else + Vec_IntGrow( p, 2 * p->nCap ); + } + p->nSize++; + for ( i = p->nSize-2; i >= 0; i-- ) + if ( Vec_IntEntry(vCost, p->pArray[i]) > Vec_IntEntry(vCost, Entry) ) + p->pArray[i+1] = p->pArray[i]; + else + break; + p->pArray[i+1] = Entry; +} /**Function************************************************************* @@ -855,6 +873,15 @@ static inline int Vec_IntPushUniqueOrder( Vec_Int_t * p, int Entry ) Vec_IntPushOrder( p, Entry ); return 0; } +static inline int Vec_IntPushUniqueOrderCost( Vec_Int_t * p, int Entry, Vec_Int_t * vCost ) +{ + int i; + for ( i = 0; i < p->nSize; i++ ) + if ( p->pArray[i] == Entry ) + return 1; + Vec_IntPushOrderCost( p, Entry, vCost ); + return 0; +} /**Function************************************************************* diff --git a/src/proof/acec/acec.c b/src/proof/acec/acec.c new file mode 100644 index 00000000..4237ef18 --- /dev/null +++ b/src/proof/acec/acec.c @@ -0,0 +1,52 @@ +/**CFile**************************************************************** + + FileName [acec.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [CEC for arithmetic circuits.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: acec.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "acecInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/acec/acec.h b/src/proof/acec/acec.h new file mode 100644 index 00000000..3f05e5e6 --- /dev/null +++ b/src/proof/acec/acec.h @@ -0,0 +1,68 @@ +/**CFile**************************************************************** + + FileName [acec.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [CEC for arithmetic circuits.] + + Synopsis [External declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: acec.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__proof__acec__acec_h +#define ABC__proof__acec__acec_h + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// ITERATORS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== acecCore.c ========================================================*/ +extern int Gia_PolynCec( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Cec_ParCec_t * pPars ); +/*=== acecMiter.c ========================================================*/ +extern int Gia_ManDemiterDual( Gia_Man_t * p, Gia_Man_t ** pp0, Gia_Man_t ** pp1 ); +extern int Gia_ManDemiterXor( Gia_Man_t * p, Gia_Man_t ** pp0, Gia_Man_t ** pp1 ); + + +ABC_NAMESPACE_HEADER_END + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/proof/acec/acecCore.c b/src/proof/acec/acecCore.c new file mode 100644 index 00000000..bfece8dc --- /dev/null +++ b/src/proof/acec/acecCore.c @@ -0,0 +1,60 @@ +/**CFile**************************************************************** + + FileName [acecCore.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [CEC for arithmetic circuits.] + + Synopsis [Core procedures.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: acecCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "acecInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_PolynCec( Gia_Man_t * pGia0, Gia_Man_t * pGia1, Cec_ParCec_t * pPars ) +{ + Vec_Int_t * vOrder0 = Gia_PolynReorder( pGia0, pPars->fVerbose ); + Vec_Int_t * vOrder1 = Gia_PolynReorder( pGia1, pPars->fVerbose ); + Gia_PolynBuild( pGia0, vOrder0, pPars->fVerbose ); + Gia_PolynBuild( pGia1, vOrder1, pPars->fVerbose ); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/acec/acecFadds.c b/src/proof/acec/acecFadds.c new file mode 100644 index 00000000..3d526dbf --- /dev/null +++ b/src/proof/acec/acecFadds.c @@ -0,0 +1,1183 @@ +/**CFile**************************************************************** + + FileName [acecFadds.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [CEC for arithmetic circuits.] + + Synopsis [Detecting half-adders and full-adders.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: acecFadds.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "acecInt.h" +#include "misc/vec/vecWec.h" +#include "misc/tim/tim.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +#define Dtc_ForEachCut( pList, pCut, i ) for ( i = 0, pCut = pList + 1; i < pList[0]; i++, pCut += pCut[0] + 1 ) +#define Dtc_ForEachFadd( vFadds, i ) for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ ) + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [Detecting HADDs in the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose ) +{ + Vec_Int_t * vHadds = Vec_IntAlloc( 1000 ); + Gia_Obj_t * pObj, * pFan0, * pFan1; + int i, iLit, iFan0, iFan1, fComplDiff, Count, Counts[5] = {0}; + ABC_FREE( p->pRefs ); + Gia_ManCreateRefs( p ); + Gia_ManHashStart( p ); + Gia_ManForEachAnd( p, pObj, i ) + { + if ( !Gia_ObjRecognizeExor(pObj, &pFan0, &pFan1) ) + continue; + Count = 0; + if ( Gia_ObjRefNumId(p, Gia_ObjFaninId0(pObj, i)) > 1 ) + Vec_IntPushTwo( vHadds, i, Gia_ObjFaninId0(pObj, i) ), Count++; + if ( Gia_ObjRefNumId(p, Gia_ObjFaninId1(pObj, i)) > 1 ) + Vec_IntPushTwo( vHadds, i, Gia_ObjFaninId1(pObj, i) ), Count++; + iFan0 = Gia_ObjId( p, pFan0 ); + iFan1 = Gia_ObjId( p, pFan1 ); + fComplDiff = (Gia_ObjFaninC0(Gia_ObjFanin0(pObj)) ^ Gia_ObjFaninC1(Gia_ObjFanin0(pObj))); + assert( fComplDiff == (Gia_ObjFaninC0(Gia_ObjFanin1(pObj)) ^ Gia_ObjFaninC1(Gia_ObjFanin1(pObj))) ); + if ( fComplDiff ) + { + if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 0), Abc_Var2Lit(iFan1, 0))) ) + Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++; + if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 1), Abc_Var2Lit(iFan1, 1))) ) + Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++; + } + else + { + if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 0), Abc_Var2Lit(iFan1, 1))) ) + Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++; + if ( (iLit = Gia_ManHashLookupInt(p, Abc_Var2Lit(iFan0, 1), Abc_Var2Lit(iFan1, 0))) ) + Vec_IntPushTwo( vHadds, i, Abc_Lit2Var(iLit) ), Count++; + } + Counts[Count]++; + } + Gia_ManHashStop( p ); + ABC_FREE( p->pRefs ); + if ( fVerbose ) + { + int iXor, iAnd; + printf( "Found %d half-adders with XOR gates: ", Vec_IntSize(vHadds)/2 ); + for ( i = 0; i <= 4; i++ ) + printf( "%d=%d ", i, Counts[i] ); + printf( "\n" ); + + Vec_IntForEachEntryDouble( vHadds, iXor, iAnd, i ) + printf( "%3d : %5d %5d\n", i, iXor, iAnd ); + } + return vHadds; +} + +/**Function************************************************************* + + Synopsis [Derive GIA with boxes containing adder-chains.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManIllustrateBoxes( Gia_Man_t * p ) +{ + Tim_Man_t * pManTime = (Tim_Man_t *)p->pManTime; + int nBoxes = Tim_ManBoxNum( pManTime ); + int i, k, curCi, curCo, nBoxIns, nBoxOuts; + Gia_Obj_t * pObj; + // walk through the boxes + curCi = Tim_ManPiNum(pManTime); + curCo = 0; + for ( i = 0; i < nBoxes; i++ ) + { + nBoxIns = Tim_ManBoxInputNum(pManTime, i); + nBoxOuts = Tim_ManBoxOutputNum(pManTime, i); + printf( "Box %4d [%d x %d] : ", i, nBoxIns, nBoxOuts ); + printf( "Input obj IDs = " ); + for ( k = 0; k < nBoxIns; k++ ) + { + pObj = Gia_ManCo( p, curCo + k ); + printf( "%d ", Gia_ObjId(p, pObj) ); + } + printf( " Output obj IDs = " ); + for ( k = 0; k < nBoxOuts; k++ ) + { + pObj = Gia_ManCi( p, curCi + k ); + printf( "%d ", Gia_ObjId(p, pObj) ); + } + curCo += nBoxIns; + curCi += nBoxOuts; + printf( "\n" ); + } + curCo += Tim_ManPoNum(pManTime); + // verify counts + assert( curCi == Gia_ManCiNum(p) ); + assert( curCo == Gia_ManCoNum(p) ); +} + +/**Function************************************************************* + + Synopsis [Detecting FADDs in the AIG.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Dtc_ManCutMergeOne( int * pCut0, int * pCut1, int * pCut ) +{ + int i, k; + for ( k = 0; k <= pCut1[0]; k++ ) + pCut[k] = pCut1[k]; + for ( i = 1; i <= pCut0[0]; i++ ) + { + for ( k = 1; k <= pCut1[0]; k++ ) + if ( pCut0[i] == pCut1[k] ) + break; + if ( k <= pCut1[0] ) + continue; + if ( pCut[0] == 3 ) + return 0; + pCut[1+pCut[0]++] = pCut0[i]; + } + assert( pCut[0] == 2 || pCut[0] == 3 ); + if ( pCut[1] > pCut[2] ) + ABC_SWAP( int, pCut[1], pCut[2] ); + assert( pCut[1] < pCut[2] ); + if ( pCut[0] == 2 ) + return 1; + if ( pCut[2] > pCut[3] ) + ABC_SWAP( int, pCut[2], pCut[3] ); + if ( pCut[1] > pCut[2] ) + ABC_SWAP( int, pCut[1], pCut[2] ); + assert( pCut[1] < pCut[2] ); + assert( pCut[2] < pCut[3] ); + return 1; +} +int Dtc_ManCutCheckEqual( Vec_Int_t * vCuts, int * pCutNew ) +{ + int * pList = Vec_IntArray( vCuts ); + int i, k, * pCut; + Dtc_ForEachCut( pList, pCut, i ) + { + for ( k = 0; k <= pCut[0]; k++ ) + if ( pCut[k] != pCutNew[k] ) + break; + if ( k > pCut[0] ) + return 1; + } + return 0; +} +int Dtc_ObjComputeTruth_rec( Gia_Obj_t * pObj ) +{ + int Truth0, Truth1; + if ( pObj->Value ) + return pObj->Value; + assert( Gia_ObjIsAnd(pObj) ); + Truth0 = Dtc_ObjComputeTruth_rec( Gia_ObjFanin0(pObj) ); + Truth1 = Dtc_ObjComputeTruth_rec( Gia_ObjFanin1(pObj) ); + return (pObj->Value = (Gia_ObjFaninC0(pObj) ? ~Truth0 : Truth0) & (Gia_ObjFaninC1(pObj) ? ~Truth1 : Truth1)); +} +void Dtc_ObjCleanTruth_rec( Gia_Obj_t * pObj ) +{ + if ( !pObj->Value ) + return; + pObj->Value = 0; + if ( !Gia_ObjIsAnd(pObj) ) + return; + Dtc_ObjCleanTruth_rec( Gia_ObjFanin0(pObj) ); + Dtc_ObjCleanTruth_rec( Gia_ObjFanin1(pObj) ); +} +int Dtc_ObjComputeTruth( Gia_Man_t * p, int iObj, int * pCut, int * pTruth ) +{ + unsigned Truth, Truths[3] = { 0xAA, 0xCC, 0xF0 }; int i; + for ( i = 1; i <= pCut[0]; i++ ) + Gia_ManObj(p, pCut[i])->Value = Truths[i-1]; + Truth = 0xFF & Dtc_ObjComputeTruth_rec( Gia_ManObj(p, iObj) ); + Dtc_ObjCleanTruth_rec( Gia_ManObj(p, iObj) ); + if ( pTruth ) + *pTruth = Truth; + if ( Truth == 0x96 || Truth == 0x69 ) + return 1; + if ( Truth == 0xE8 || Truth == 0xD4 || Truth == 0xB2 || Truth == 0x71 || + Truth == 0x17 || Truth == 0x2B || Truth == 0x4D || Truth == 0x8E ) + return 2; + return 0; +} +void Dtc_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_Int_t * vCuts, Vec_Int_t * vCutsXor, Vec_Int_t * vCutsMaj ) +{ + int fVerbose = 0; + Vec_Int_t * vTemp; + int i, k, c, Type, * pCut0, * pCut1, pCut[4]; + Vec_IntFill( vCuts, 2, 1 ); + Vec_IntPush( vCuts, iObj ); + Dtc_ForEachCut( pList0, pCut0, i ) + Dtc_ForEachCut( pList1, pCut1, k ) + { + if ( !Dtc_ManCutMergeOne(pCut0, pCut1, pCut) ) + continue; + if ( Dtc_ManCutCheckEqual(vCuts, pCut) ) + continue; + Vec_IntAddToEntry( vCuts, 0, 1 ); + for ( c = 0; c <= pCut[0]; c++ ) + Vec_IntPush( vCuts, pCut[c] ); + if ( pCut[0] != 3 ) + continue; + Type = Dtc_ObjComputeTruth( p, iObj, pCut, NULL ); + if ( Type == 0 ) + continue; + vTemp = Type == 1 ? vCutsXor : vCutsMaj; + if ( fVerbose ) + printf( "%d = %s(", iObj, Type == 1 ? "XOR" : "MAJ" ); + for ( c = 1; c <= pCut[0]; c++ ) + { + if ( fVerbose ) + printf( " %d", pCut[c] ); + Vec_IntPush( vTemp, pCut[c] ); + } + if ( fVerbose ) + printf( " )\n" ); + Vec_IntPush( vTemp, iObj ); + } +} +void Dtc_ManComputeCuts( Gia_Man_t * p, Vec_Int_t ** pvCutsXor, Vec_Int_t ** pvCutsMaj, int fVerbose ) +{ + Gia_Obj_t * pObj; + int * pList0, * pList1, i, nCuts = 0; + Vec_Int_t * vTemp = Vec_IntAlloc( 1000 ); + Vec_Int_t * vCutsXor = Vec_IntAlloc( Gia_ManAndNum(p) ); + Vec_Int_t * vCutsMaj = Vec_IntAlloc( Gia_ManAndNum(p) ); + Vec_Int_t * vCuts = Vec_IntAlloc( 30 * Gia_ManAndNum(p) ); + Vec_IntFill( vCuts, Gia_ManObjNum(p), 0 ); + Gia_ManCleanValue( p ); + Gia_ManForEachCi( p, pObj, i ) + { + Vec_IntWriteEntry( vCuts, Gia_ObjId(p, pObj), Vec_IntSize(vCuts) ); + Vec_IntPush( vCuts, 1 ); + Vec_IntPush( vCuts, 1 ); + Vec_IntPush( vCuts, Gia_ObjId(p, pObj) ); + } + Gia_ManForEachAnd( p, pObj, i ) + { + pList0 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId0(pObj, i)) ); + pList1 = Vec_IntEntryP( vCuts, Vec_IntEntry(vCuts, Gia_ObjFaninId1(pObj, i)) ); + Dtc_ManCutMerge( p, i, pList0, pList1, vTemp, vCutsXor, vCutsMaj ); + Vec_IntWriteEntry( vCuts, i, Vec_IntSize(vCuts) ); + Vec_IntAppend( vCuts, vTemp ); + nCuts += Vec_IntEntry( vTemp, 0 ); + } + if ( fVerbose ) + printf( "Nodes = %d. Cuts = %d. Cuts/Node = %.2f. Ints/Node = %.2f.\n", + Gia_ManAndNum(p), nCuts, 1.0*nCuts/Gia_ManAndNum(p), 1.0*Vec_IntSize(vCuts)/Gia_ManAndNum(p) ); + Vec_IntFree( vTemp ); + Vec_IntFree( vCuts ); + *pvCutsXor = vCutsXor; + *pvCutsMaj = vCutsMaj; +} +Vec_Int_t * Dtc_ManFindCommonCuts( Gia_Man_t * p, Vec_Int_t * vCutsXor, Vec_Int_t * vCutsMaj ) +{ + int * pCuts0 = Vec_IntArray(vCutsXor); + int * pCuts1 = Vec_IntArray(vCutsMaj); + int * pLimit0 = Vec_IntLimit(vCutsXor); + int * pLimit1 = Vec_IntLimit(vCutsMaj); int i; + Vec_Int_t * vFadds = Vec_IntAlloc( 1000 ); + assert( Vec_IntSize(vCutsXor) % 4 == 0 ); + assert( Vec_IntSize(vCutsMaj) % 4 == 0 ); + while ( pCuts0 < pLimit0 && pCuts1 < pLimit1 ) + { + for ( i = 0; i < 3; i++ ) + if ( pCuts0[i] != pCuts1[i] ) + break; + if ( i == 3 ) + { + for ( i = 0; i < 4; i++ ) + Vec_IntPush( vFadds, pCuts0[i] ); + Vec_IntPush( vFadds, pCuts1[3] ); + pCuts0 += 4; + pCuts1 += 4; + } + else if ( pCuts0[i] < pCuts1[i] ) + pCuts0 += 4; + else if ( pCuts0[i] > pCuts1[i] ) + pCuts1 += 4; + } + assert( Vec_IntSize(vFadds) % 5 == 0 ); + return vFadds; +} +void Dtc_ManPrintFadds( Vec_Int_t * vFadds ) +{ + int i; + Dtc_ForEachFadd( vFadds, i ) + { + printf( "%6d : ", i ); + printf( "%6d ", Vec_IntEntry(vFadds, 5*i+0) ); + printf( "%6d ", Vec_IntEntry(vFadds, 5*i+1) ); + printf( "%6d ", Vec_IntEntry(vFadds, 5*i+2) ); + printf( " -> " ); + printf( "%6d ", Vec_IntEntry(vFadds, 5*i+3) ); + printf( "%6d ", Vec_IntEntry(vFadds, 5*i+4) ); + printf( "\n" ); + } +} +int Dtc_ManCompare( int * pCut0, int * pCut1 ) +{ + if ( pCut0[0] < pCut1[0] ) return -1; + if ( pCut0[0] > pCut1[0] ) return 1; + if ( pCut0[1] < pCut1[1] ) return -1; + if ( pCut0[1] > pCut1[1] ) return 1; + if ( pCut0[2] < pCut1[2] ) return -1; + if ( pCut0[2] > pCut1[2] ) return 1; + return 0; +} +int Dtc_ManCompare2( int * pCut0, int * pCut1 ) +{ + if ( pCut0[4] < pCut1[4] ) return -1; + if ( pCut0[4] > pCut1[4] ) return 1; + return 0; +} +// returns array of 5-tuples containing inputs/sum/cout of each full adder +Vec_Int_t * Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose ) +{ + Vec_Int_t * vCutsXor, * vCutsMaj, * vFadds; + Dtc_ManComputeCuts( p, &vCutsXor, &vCutsMaj, fVerbose ); + qsort( Vec_IntArray(vCutsXor), Vec_IntSize(vCutsXor)/4, 16, (int (*)(const void *, const void *))Dtc_ManCompare ); + qsort( Vec_IntArray(vCutsMaj), Vec_IntSize(vCutsMaj)/4, 16, (int (*)(const void *, const void *))Dtc_ManCompare ); + vFadds = Dtc_ManFindCommonCuts( p, vCutsXor, vCutsMaj ); + qsort( Vec_IntArray(vFadds), Vec_IntSize(vFadds)/5, 20, (int (*)(const void *, const void *))Dtc_ManCompare2 ); + if ( fVerbose ) + printf( "XOR3 cuts = %d. MAJ cuts = %d. Full-adders = %d.\n", Vec_IntSize(vCutsXor)/4, Vec_IntSize(vCutsMaj)/4, Vec_IntSize(vFadds)/5 ); + if ( fVerbose ) + Dtc_ManPrintFadds( vFadds ); + Vec_IntFree( vCutsXor ); + Vec_IntFree( vCutsMaj ); + return vFadds; +} + +/**Function************************************************************* + + Synopsis [Map each MAJ into the topmost MAJ of its chain.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +// maps MAJ nodes into FADD indexes +Vec_Int_t * Gia_ManCreateMap( Gia_Man_t * p, Vec_Int_t * vFadds ) +{ + Vec_Int_t * vMap = Vec_IntStartFull( Gia_ManObjNum(p) ); int i; + Dtc_ForEachFadd( vFadds, i ) + Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+4), i ); + return vMap; +} +// find chain length (for each MAJ, how many FADDs are rooted in its first input) +int Gia_ManFindChains_rec( Gia_Man_t * p, int iMaj, Vec_Int_t * vFadds, Vec_Int_t * vMap, Vec_Int_t * vLength ) +{ + assert( Vec_IntEntry(vMap, iMaj) >= 0 ); // MAJ + if ( Vec_IntEntry(vLength, iMaj) >= 0 ) + return Vec_IntEntry(vLength, iMaj); + assert( Gia_ObjIsAnd(Gia_ManObj(p, iMaj)) ); + { + int iFadd = Vec_IntEntry( vMap, iMaj ); + int iXor0 = Vec_IntEntry( vFadds, 5*iFadd+0 ); + int iXor1 = Vec_IntEntry( vFadds, 5*iFadd+1 ); + int iXor2 = Vec_IntEntry( vFadds, 5*iFadd+2 ); + int iLen0 = Vec_IntEntry( vMap, iXor0 ) == -1 ? 0 : Gia_ManFindChains_rec( p, iXor0, vFadds, vMap, vLength ); + int iLen1 = Vec_IntEntry( vMap, iXor1 ) == -1 ? 0 : Gia_ManFindChains_rec( p, iXor1, vFadds, vMap, vLength ); + int iLen2 = Vec_IntEntry( vMap, iXor2 ) == -1 ? 0 : Gia_ManFindChains_rec( p, iXor2, vFadds, vMap, vLength ); + int iLen = Abc_MaxInt( iLen0, Abc_MaxInt(iLen1, iLen2) ); + if ( iLen0 < iLen ) + { + if ( iLen == iLen1 ) + { + ABC_SWAP( int, Vec_IntArray(vFadds)[5*iFadd+0], Vec_IntArray(vFadds)[5*iFadd+1] ); + } + else if ( iLen == iLen2 ) + { + ABC_SWAP( int, Vec_IntArray(vFadds)[5*iFadd+0], Vec_IntArray(vFadds)[5*iFadd+2] ); + } + } + Vec_IntWriteEntry( vLength, iMaj, iLen + 1 ); + return iLen + 1; + } +} +// for each FADD find the longest chain and reorder its inputs +void Gia_ManFindChains( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vMap ) +{ + int i; + // for each FADD find the longest chain rooted in it + Vec_Int_t * vLength = Vec_IntStartFull( Gia_ManObjNum(p) ); + Dtc_ForEachFadd( vFadds, i ) + Gia_ManFindChains_rec( p, Vec_IntEntry(vFadds, 5*i+4), vFadds, vMap, vLength ); + Vec_IntFree( vLength ); +} +// collect one carry-chain +void Gia_ManCollectOneChain( Gia_Man_t * p, Vec_Int_t * vFadds, int iFaddTop, Vec_Int_t * vMap, Vec_Int_t * vChain ) +{ + int iFadd; + Vec_IntClear( vChain ); + for ( iFadd = iFaddTop; iFadd >= 0 && + !Gia_ObjIsTravIdCurrentId(p, Vec_IntEntry(vFadds, 5*iFadd+3)) && + !Gia_ObjIsTravIdCurrentId(p, Vec_IntEntry(vFadds, 5*iFadd+4)); + iFadd = Vec_IntEntry(vMap, Vec_IntEntry(vFadds, 5*iFadd+0)) ) + { + Vec_IntPush( vChain, iFadd ); + } + Vec_IntReverseOrder( vChain ); +} +void Gia_ManMarkWithTravId_rec( Gia_Man_t * p, int Id ) +{ + Gia_Obj_t * pObj; + if ( Gia_ObjIsTravIdCurrentId(p, Id) ) + return; + Gia_ObjSetTravIdCurrentId(p, Id); + pObj = Gia_ManObj( p, Id ); + if ( Gia_ObjIsAnd(pObj) ) + Gia_ManMarkWithTravId_rec( p, Gia_ObjFaninId0(pObj, Id) ); + if ( Gia_ObjIsAnd(pObj) ) + Gia_ManMarkWithTravId_rec( p, Gia_ObjFaninId1(pObj, Id) ); +} +// returns mapping of each MAJ into the topmost elements of its chain +Vec_Wec_t * Gia_ManCollectTopmost( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vMap, int nFaddMin ) +{ + int i, j, iFadd; + Vec_Int_t * vChain = Vec_IntAlloc( 100 ); + Vec_Wec_t * vChains = Vec_WecAlloc( Vec_IntSize(vFadds)/5 ); + // erase elements appearing as FADD inputs + Vec_Bit_t * vMarksTop = Vec_BitStart( Vec_IntSize(vFadds)/5 ); + Dtc_ForEachFadd( vFadds, i ) + if ( (iFadd = Vec_IntEntry(vMap, Vec_IntEntry(vFadds, 5*i+0))) >= 0 ) + Vec_BitWriteEntry( vMarksTop, iFadd, 1 ); + // compress the remaining ones + Gia_ManIncrementTravId( p ); + Dtc_ForEachFadd( vFadds, i ) + { + if ( Vec_BitEntry(vMarksTop, i) ) + continue; + Gia_ManCollectOneChain( p, vFadds, i, vMap, vChain ); + if ( Vec_IntSize(vChain) < nFaddMin ) + continue; + Vec_IntAppend( Vec_WecPushLevel(vChains), vChain ); + Vec_IntForEachEntry( vChain, iFadd, j ) + { + assert( !Gia_ObjIsTravIdCurrentId(p, Vec_IntEntry(vFadds, 5*iFadd+3)) ); + assert( !Gia_ObjIsTravIdCurrentId(p, Vec_IntEntry(vFadds, 5*iFadd+4)) ); + Gia_ManMarkWithTravId_rec( p, Vec_IntEntry(vFadds, 5*iFadd+3) ); + Gia_ManMarkWithTravId_rec( p, Vec_IntEntry(vFadds, 5*iFadd+4) ); + } + } + // cleanup + Vec_BitFree( vMarksTop ); + Vec_IntFree( vChain ); + return vChains; +} +// prints chains beginning in majority nodes contained in vTops +void Gia_ManPrintChains( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vMap, Vec_Wec_t * vChains ) +{ + Vec_Int_t * vChain; + int i, k, iFadd, Count = 0; + Vec_WecForEachLevel( vChains, vChain, i ) + { + Count += Vec_IntSize(vChain); + if ( i < 10 ) + { + printf( "Chain %4d : %4d ", i, Vec_IntSize(vChain) ); + Vec_IntForEachEntry( vChain, iFadd, k ) + { + printf( "%d(%d) ", iFadd, Vec_IntEntry(vFadds, 5*iFadd+4) ); + if ( k != Vec_IntSize(vChain) - 1 ) + printf( "-> " ); + if ( k > 6 ) + { + printf( "..." ); + break; + } + } + printf( "\n" ); + } + else if ( i == 10 ) + printf( "...\n" ); + + } + printf( "Total chains = %d. Total full-adders = %d.\n", Vec_WecSize(vChains), Count ); +} +// map SUM bits and topmost MAJ into topmost FADD number +Vec_Int_t * Gia_ManFindMapping( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vMap, Vec_Wec_t * vChains ) +{ + Vec_Int_t * vChain; + int i, k, iFadd = -1; + Vec_Int_t * vMap2Chain = Vec_IntStartFull( Gia_ManObjNum(p) ); + Vec_WecForEachLevel( vChains, vChain, i ) + { + assert( Vec_IntSize(vChain) > 0 ); + Vec_IntForEachEntry( vChain, iFadd, k ) + { + //printf( "Chain %d: setting SUM %d (obj %d)\n", i, k, Vec_IntEntry(vFadds, 5*iFadd+3) ); + assert( Vec_IntEntry(vMap2Chain, Vec_IntEntry(vFadds, 5*iFadd+3)) == -1 ); + Vec_IntWriteEntry( vMap2Chain, Vec_IntEntry(vFadds, 5*iFadd+3), i ); + } + //printf( "Chain %d: setting CARRY (obj %d)\n", i, Vec_IntEntry(vFadds, 5*iFadd+4) ); + assert( Vec_IntEntry(vMap2Chain, Vec_IntEntry(vFadds, 5*iFadd+4)) == -1 ); + Vec_IntWriteEntry( vMap2Chain, Vec_IntEntry(vFadds, 5*iFadd+4), i ); + } + return vMap2Chain; +} + +/**Function************************************************************* + + Synopsis [Derive GIA with boxes containing adder-chains.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ManCollectTruthTables( Gia_Man_t * p, Vec_Int_t * vFadds ) +{ + int i, k, Type, Truth, pCut[4] = {3}; + Vec_Int_t * vTruths = Vec_IntAlloc( 2*Vec_IntSize(vFadds)/5 ); + Gia_ManCleanValue( p ); + Dtc_ForEachFadd( vFadds, i ) + { + for ( k = 0; k < 3; k++ ) + pCut[k+1] = Vec_IntEntry( vFadds, 5*i+k ); + Type = Dtc_ObjComputeTruth( p, Vec_IntEntry(vFadds, 5*i+3), pCut, &Truth ); + assert( Type == 1 ); + Vec_IntPush( vTruths, Truth ); + Type = Dtc_ObjComputeTruth( p, Vec_IntEntry(vFadds, 5*i+4), pCut, &Truth ); + assert( Type == 2 ); + Vec_IntPush( vTruths, Truth ); + } + return vTruths; +} +float * Gia_ManGenerateDelayTableFloat( int nIns, int nOuts ) +{ + int i, Total = nIns * nOuts; + float * pDelayTable = ABC_ALLOC( float, Total + 3 ); + pDelayTable[0] = 0; + pDelayTable[1] = nIns; + pDelayTable[2] = nOuts; + for ( i = 0; i < Total; i++ ) + pDelayTable[i+3] = 1; + pDelayTable[i+3 - nIns] = -ABC_INFINITY; + return pDelayTable; +} +Tim_Man_t * Gia_ManGenerateTim( int nPis, int nPos, int nBoxes, int nIns, int nOuts ) +{ + Tim_Man_t * pMan; + int i, curPi, curPo; + Vec_Ptr_t * vDelayTables = Vec_PtrAlloc( 1 ); + Vec_PtrPush( vDelayTables, Gia_ManGenerateDelayTableFloat(nIns, nOuts) ); + pMan = Tim_ManStart( nPis + nOuts * nBoxes, nPos + nIns * nBoxes ); + Tim_ManSetDelayTables( pMan, vDelayTables ); + curPi = nPis; + curPo = 0; + for ( i = 0; i < nBoxes; i++ ) + { + Tim_ManCreateBox( pMan, curPo, nIns, curPi, nOuts, 0, 0 ); + curPi += nOuts; + curPo += nIns; + } + curPo += nPos; + assert( curPi == Tim_ManCiNum(pMan) ); + assert( curPo == Tim_ManCoNum(pMan) ); + //Tim_ManPrint( pMan ); + return pMan; +} +Gia_Man_t * Gia_ManGenerateExtraAig( int nBoxes, int nIns, int nOuts ) +{ + Gia_Man_t * pNew = Gia_ManStart( nBoxes * 20 ); + int i, k, pInLits[16], pOutLits[16]; + assert( nIns < 16 && nOuts < 16 ); + for ( i = 0; i < nIns; i++ ) + pInLits[i] = Gia_ManAppendCi( pNew ); + pOutLits[0] = Gia_ManAppendXor( pNew, Gia_ManAppendXor(pNew, pInLits[0], pInLits[1]), pInLits[2] ); + pOutLits[1] = Gia_ManAppendMaj( pNew, pInLits[0], pInLits[1], pInLits[2] ); + for ( i = 0; i < nBoxes; i++ ) + for ( k = 0; k < nOuts; k++ ) + Gia_ManAppendCo( pNew, pOutLits[k] ); + return pNew; +} +void Gia_ManDupFadd( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vChain, Vec_Int_t * vFadds, Vec_Int_t * vMap, Vec_Wec_t * vChains, Vec_Int_t * vMap2Chain, Vec_Int_t * vTruths ) +{ + extern void Gia_ManDupWithFaddBoxes_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vFadds, Vec_Int_t * vMap, Vec_Wec_t * vChains, Vec_Int_t * vMap2Chain, Vec_Int_t * vTruths ); + int i, k, iFadd = -1, iCiLit, pLits[3]; + Gia_Obj_t * pObj; + // construct FADD inputs + Vec_IntForEachEntry( vChain, iFadd, i ) + for ( k = 0; k < 3; k++ ) + { + if ( i && !k ) continue; + pObj = Gia_ManObj( p, Vec_IntEntry(vFadds, 5*iFadd+k) ); + Gia_ManDupWithFaddBoxes_rec( pNew, p, pObj, vFadds, vMap, vChains, vMap2Chain, vTruths ); + } + // construct boxes + iCiLit = 0; + Vec_IntForEachEntry( vChain, iFadd, i ) + { + int iXorTruth = Vec_IntEntry( vTruths, 2*iFadd+0 ); + int iMajTruth = Vec_IntEntry( vTruths, 2*iFadd+1 ); + for ( k = 0; k < 3; k++ ) + { + pObj = Gia_ManObj( p, Vec_IntEntry(vFadds, 5*iFadd+k) ); + pLits[k] = (!k && iCiLit) ? iCiLit : pObj->Value; + assert( pLits[k] >= 0 ); + } + // normalize truth table + // if ( Truth == 0xE8 || Truth == 0xD4 || Truth == 0xB2 || Truth == 0x71 || + // Truth == 0x17 || Truth == 0x2B || Truth == 0x4D || Truth == 0x8E ) + if ( iMajTruth == 0x4D ) + pLits[0] = Abc_LitNot(pLits[0]), iMajTruth = 0x8E, iXorTruth = 0xFF & ~iXorTruth; + else if ( iMajTruth == 0xD4 ) + pLits[0] = Abc_LitNot(pLits[0]), iMajTruth = 0xE8, iXorTruth = 0xFF & ~iXorTruth; + else if ( iMajTruth == 0x2B ) + pLits[1] = Abc_LitNot(pLits[1]), iMajTruth = 0x8E, iXorTruth = 0xFF & ~iXorTruth; + else if ( iMajTruth == 0xB2 ) + pLits[1] = Abc_LitNot(pLits[1]), iMajTruth = 0xE8, iXorTruth = 0xFF & ~iXorTruth; + if ( iMajTruth == 0x8E ) + pLits[2] = Abc_LitNot(pLits[2]), iMajTruth = 0xE8, iXorTruth = 0xFF & ~iXorTruth; + else if ( iMajTruth == 0x71 ) + pLits[2] = Abc_LitNot(pLits[2]), iMajTruth = 0x17, iXorTruth = 0xFF & ~iXorTruth; + else assert( iMajTruth == 0xE8 || iMajTruth == 0x17 ); + // normalize carry-in + if ( Abc_LitIsCompl(pLits[0]) ) + { + for ( k = 0; k < 3; k++ ) + pLits[k] = Abc_LitNot(pLits[k]); + iXorTruth = 0xFF & ~iXorTruth; + iMajTruth = 0xFF & ~iMajTruth; + } + // add COs + assert( !Abc_LitIsCompl(pLits[0]) ); + for ( k = 0; k < 3; k++ ) + Gia_ManAppendCo( pNew, pLits[k] ); + // create CI + assert( iXorTruth == 0x96 || iXorTruth == 0x69 ); + pObj = Gia_ManObj( p, Vec_IntEntry(vFadds, 5*iFadd+3) ); + pObj->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), (int)(iXorTruth == 0x69) ); + // create CI + assert( iMajTruth == 0xE8 || iMajTruth == 0x17 ); + iCiLit = Abc_LitNotCond( Gia_ManAppendCi(pNew), (int)(iMajTruth == 0x17) ); + } + // assign carry out + assert( iFadd == Vec_IntEntryLast(vChain) ); + pObj = Gia_ManObj( p, Vec_IntEntry(vFadds, 5*iFadd+4) ); + pObj->Value = iCiLit; +} +void Gia_ManDupWithFaddBoxes_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vFadds, Vec_Int_t * vMap, Vec_Wec_t * vChains, Vec_Int_t * vMap2Chain, Vec_Int_t * vTruths ) +{ + int iChain; + if ( ~pObj->Value ) + return; + assert( Gia_ObjIsAnd(pObj) ); + iChain = Vec_IntEntry( vMap2Chain, Gia_ObjId(p, pObj) ); +/* + assert( iChain == -1 ); + if ( iChain >= 0 ) + { + Gia_ManDupFadd( pNew, p, Vec_WecEntry(vChains, iChain), vFadds, vMap, vChains, vMap2Chain, vTruths ); + assert( ~pObj->Value ); + return; + } +*/ + Gia_ManDupWithFaddBoxes_rec( pNew, p, Gia_ObjFanin0(pObj), vFadds, vMap, vChains, vMap2Chain, vTruths ); + Gia_ManDupWithFaddBoxes_rec( pNew, p, Gia_ObjFanin1(pObj), vFadds, vMap, vChains, vMap2Chain, vTruths ); + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); +} +Gia_Man_t * Gia_ManDupWithNaturalBoxes( Gia_Man_t * p, int nFaddMin, int fVerbose ) +{ + abctime clk = Abc_Clock(); + Gia_Man_t * pNew;//, * pTemp; + Vec_Int_t * vFadds, * vMap, * vMap2Chain, * vTruths, * vChain; + Vec_Wec_t * vChains; + Gia_Obj_t * pObj; + int i, nBoxes; + if ( Gia_ManBoxNum(p) > 0 ) + { + printf( "Currently natural carry-chains cannot be detected when boxes are present.\n" ); + return NULL; + } + assert( Gia_ManBoxNum(p) == 0 ); + + // detect FADDs + vFadds = Gia_ManDetectFullAdders( p, fVerbose ); + assert( Vec_IntSize(vFadds) % 5 == 0 ); + // map MAJ into its FADD + vMap = Gia_ManCreateMap( p, vFadds ); + // for each FADD, find the longest chain and reorder its inputs + Gia_ManFindChains( p, vFadds, vMap ); + // returns the set of topmost MAJ nodes + vChains = Gia_ManCollectTopmost( p, vFadds, vMap, nFaddMin ); + if ( fVerbose ) + Gia_ManPrintChains( p, vFadds, vMap, vChains ); + if ( Vec_WecSize(vChains) == 0 ) + { + Vec_IntFree( vFadds ); + Vec_IntFree( vMap ); + Vec_WecFree( vChains ); + return Gia_ManDup( p ); + } + // returns mapping of each MAJ into the topmost elements of its chain + vMap2Chain = Gia_ManFindMapping( p, vFadds, vMap, vChains ); + // compute truth tables for FADDs + vTruths = Gia_ManCollectTruthTables( p, vFadds ); + if ( fVerbose ) + Abc_PrintTime( 1, "Carry-chain detection time", Abc_Clock() - clk ); + + // duplicate + clk = Abc_Clock(); + 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; + Gia_ManForEachCi( p, pObj, i ) + pObj->Value = Gia_ManAppendCi( pNew ); + Vec_WecForEachLevel( vChains, vChain, i ) + Gia_ManDupFadd( pNew, p, vChain, vFadds, vMap, vChains, vMap2Chain, vTruths ); + Gia_ManForEachCo( p, pObj, i ) + Gia_ManDupWithFaddBoxes_rec( pNew, p, Gia_ObjFanin0(pObj), vFadds, vMap, vChains, vMap2Chain, vTruths ); + Gia_ManForEachCo( p, pObj, i ) + Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + if ( Gia_ManRegNum(p) ) + { + if ( fVerbose ) + printf( "Warning: Sequential design is coverted into combinational one by adding white boxes.\n" ); + pNew->nRegs = 0; + } + assert( !Gia_ManHasDangling(pNew) ); + + // cleanup + Vec_IntFree( vFadds ); + Vec_IntFree( vMap ); + Vec_WecFree( vChains ); + Vec_IntFree( vMap2Chain ); + Vec_IntFree( vTruths ); + + // other information + nBoxes = (Gia_ManCiNum(pNew) - Gia_ManCiNum(p)) / 2; + assert( nBoxes == (Gia_ManCoNum(pNew) - Gia_ManCoNum(p)) / 3 ); + pNew->pManTime = Gia_ManGenerateTim( Gia_ManCiNum(p), Gia_ManCoNum(p), nBoxes, 3, 2 ); + pNew->pAigExtra = Gia_ManGenerateExtraAig( nBoxes, 3, 2 ); +/* + // normalize + pNew = Gia_ManDupNormalize( pTemp = pNew, 0 ); + pNew->pManTime = pTemp->pManTime; pTemp->pManTime = NULL; + pNew->pAigExtra = pTemp->pAigExtra; pTemp->pAigExtra = NULL; + Gia_ManStop( pTemp ); +*/ + //pNew = Gia_ManDupCollapse( pTemp = pNew, pNew->pAigExtra, NULL ); + //Gia_ManStop( pTemp ); + + //Gia_ManIllustrateBoxes( pNew ); + if ( fVerbose ) + Abc_PrintTime( 1, "AIG with boxes construction time", Abc_Clock() - clk ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Converting AIG with annotated carry-chains into AIG with boxes.] + + Description [Assumes that annotations are pObj->fMark0 or pObj->fMark1. + Only one of these can be set to 1. If fMark0 (fMark1) is set to 1, + the first (second) input of an AND-gate is chained.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ObjFanin0CopyCarry( Vec_Int_t * vCarries, Gia_Obj_t * pObj, int Id ) +{ + if ( vCarries == NULL || Vec_IntEntry(vCarries, Gia_ObjFaninId0(pObj, Id)) == -1 ) + return Gia_ObjFanin0Copy(pObj); + return Abc_LitNotCond( Vec_IntEntry(vCarries, Gia_ObjFaninId0(pObj, Id)), Gia_ObjFaninC0(pObj) ); +} +int Gia_ObjFanin1CopyCarry( Vec_Int_t * vCarries, Gia_Obj_t * pObj, int Id ) +{ + if ( vCarries == NULL || Vec_IntEntry(vCarries, Gia_ObjFaninId1(pObj, Id)) == -1 ) + return Gia_ObjFanin1Copy(pObj); + return Abc_LitNotCond( Vec_IntEntry(vCarries, Gia_ObjFaninId1(pObj, Id)), Gia_ObjFaninC1(pObj) ); +} +Gia_Man_t * Gia_ManDupWithArtificalFaddBoxes( Gia_Man_t * p, int fUseFanout, int fXorTrick ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int nBoxes = Gia_ManBoxNum(p); + int i, nRealPis, nRealPos; + Vec_Int_t * vCarries = NULL; + // make sure two chains do not overlap + Gia_ManCleanPhase( p ); + Gia_ManForEachCi( p, pObj, i ) + assert( !pObj->fMark0 && !pObj->fMark1 ); + Gia_ManForEachCo( p, pObj, i ) + assert( !pObj->fMark0 && !pObj->fMark1 ); + Gia_ManForEachAnd( p, pObj, i ) + { + assert( !pObj->fMark0 || !pObj->fMark1 ); + if ( pObj->fMark0 ) + { + assert( Gia_ObjFanin0(pObj)->fPhase == 0 ); + Gia_ObjFanin0(pObj)->fPhase = 1; + } + if ( pObj->fMark1 ) + { + assert( Gia_ObjFanin1(pObj)->fPhase == 0 ); + Gia_ObjFanin1(pObj)->fPhase = 1; + } + } + // create mapping for carry-chains + if ( !fUseFanout ) + vCarries = Vec_IntStartFull( Gia_ManObjNum(p) ); + // create references and discount carries + if ( vCarries ) + { + Gia_ManCreateRefs( p ); + Gia_ManForEachAnd( p, pObj, i ) + if ( pObj->fMark0 ) + Gia_ObjRefFanin0Dec( p, pObj ); + else if ( pObj->fMark1 ) + Gia_ObjRefFanin1Dec( p, pObj ); + } + // if AIG already has (natural) FADD boxes, it should not un-normalized + 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; + Gia_ManForEachObj1( p, pObj, i ) + { + if ( Gia_ObjIsCi(pObj) ) + pObj->Value = Gia_ManAppendCi( pNew ); + else if ( Gia_ObjIsCo(pObj) ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + else if ( !pObj->fMark0 && !pObj->fMark1 ) // AND-gate + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + else // AND-gate with chain + { + int iCiLit, iOtherLit, iLit0, iLit1, iLit2, iXorLit; + assert( pObj->fMark0 != pObj->fMark1 ); + iCiLit = pObj->fMark0 ? Gia_ObjFanin0CopyCarry(vCarries, pObj, i) : Gia_ObjFanin1CopyCarry(vCarries, pObj, i); + iOtherLit = pObj->fMark0 ? Gia_ObjFanin1Copy(pObj) : Gia_ObjFanin0Copy(pObj); + assert( iCiLit >= 0 && iOtherLit >= 0 ); + iLit0 = Abc_LitNotCond( iCiLit, Abc_LitIsCompl(iCiLit) ); + iLit1 = Abc_LitNotCond( iOtherLit, Abc_LitIsCompl(iCiLit) ); + iLit2 = Abc_LitNotCond( 0, Abc_LitIsCompl(iCiLit) ); + // add COs + assert( !Abc_LitIsCompl(iLit0) ); + Gia_ManAppendCo( pNew, iLit0 ); + Gia_ManAppendCo( pNew, iLit1 ); + Gia_ManAppendCo( pNew, iLit2 ); + // add CI (unused sum bit) + iXorLit = Gia_ManAppendCi(pNew); + // add CI (carry bit) + pObj->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), Abc_LitIsCompl(iCiLit) ); + if ( vCarries && pObj->fPhase ) + { + Vec_IntWriteEntry( vCarries, i, pObj->Value ); + if ( Gia_ObjRefNum(p, pObj) > 0 ) + { + if ( fXorTrick ) + pObj->Value = Gia_ManAppendAnd( pNew, Abc_LitNotCond(iXorLit, !Abc_LitIsCompl(iCiLit)), iOtherLit ); + else + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + } + } + nBoxes++; + } + } + Gia_ManCleanPhase( p ); + Vec_IntFreeP( &vCarries ); + ABC_FREE( p->pRefs ); + assert( !Gia_ManHasDangling(pNew) ); + // other information +// nBoxes += (Gia_ManCiNum(pNew) - Gia_ManCiNum(p)) / 2; +// assert( nBoxes == Gia_ManBoxNum(p) + (Gia_ManCoNum(pNew) - Gia_ManCoNum(p)) / 3 ); + nRealPis = Gia_ManBoxNum(p) ? Tim_ManPiNum((Tim_Man_t *)p->pManTime) : Gia_ManCiNum(p); + nRealPos = Gia_ManBoxNum(p) ? Tim_ManPoNum((Tim_Man_t *)p->pManTime) : Gia_ManCoNum(p); + pNew->pManTime = Gia_ManGenerateTim( nRealPis, nRealPos, nBoxes, 3, 2 ); + pNew->pAigExtra = Gia_ManGenerateExtraAig( nBoxes, 3, 2 ); + // optionally normalize the AIG + return pNew; +} +Gia_Man_t * Gia_ManDupWithArtificalFaddBoxesTest( Gia_Man_t * p ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + // label some and-gates + Gia_ManCleanMark01( p ); + Gia_ManForEachAnd( p, pObj, i ) + { + pObj->fMark0 = i % 5; + pObj->fMark1 = i % 7; + if ( pObj->fMark0 && pObj->fMark1 ) + pObj->fMark0 = pObj->fMark1 = 0; + } + + // output new AIG + pNew = Gia_ManDupWithArtificalFaddBoxes( p, 0, 0 ); + Gia_ManCleanMark01( p ); + return pNew; +} + +/**Function************************************************************* + + Synopsis [Adds artificial carry chains to the manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +// computes AIG delay information when boxes are used +int Gia_ManFindAnnotatedDelay( Gia_Man_t * p, int DelayC, int * pnBoxes, int fIgnoreBoxDelays ) +{ + Gia_Obj_t * pObj; + int nRealPis = Gia_ManBoxNum(p) ? Tim_ManPiNum((Tim_Man_t *)p->pManTime) : Gia_ManCiNum(p); + int * pDelays = Vec_IntArray(p->vLevels); + int i, k, iBox, iBoxOutId, Delay, Delay0, Delay1, DelayMax = 0, nBoxes = 0; + Vec_IntFill( p->vLevels, Gia_ManObjNum(p), 0 ); + Gia_ManForEachObj1( p, pObj, i ) + { + if ( Gia_ObjIsCi(pObj) ) + { + if ( fIgnoreBoxDelays ) + continue; + // check if it is real PI + iBoxOutId = Gia_ObjCioId(pObj) - nRealPis; + if ( iBoxOutId < 0 ) + continue; + // if it is a box output, find box number + iBox = iBoxOutId / 2; + assert( iBox < Gia_ManBoxNum(p) ); + // check find the maximum delay of the box inputs + Delay = 0; + for ( k = 0; k < 3; k++ ) + { + int Id = Gia_ObjId( p, Gia_ManCo(p, iBox*3+k) ); + assert( Id < i ); + Delay = Abc_MaxInt( Delay, pDelays[Id] ); + } + // consider outputs + if ( iBoxOutId & 1 ) // carry output + Delay += DelayC; + else // sum output + Delay += 100; + pDelays[i] = Delay; + continue; + } + if ( Gia_ObjIsCo(pObj) ) + { + pDelays[i] = pDelays[Gia_ObjFaninId0(pObj, i)]; + DelayMax = Abc_MaxInt( DelayMax, pDelays[i] ); + continue; + } + assert( !pObj->fMark0 || !pObj->fMark1 ); + Delay0 = pDelays[Gia_ObjFaninId0(pObj, i)]; + Delay1 = pDelays[Gia_ObjFaninId1(pObj, i)]; + if ( pObj->fMark0 ) + { + Delay = Abc_MaxInt( Delay0 + DelayC, Delay1 + 100 ); + nBoxes++; + } + else if ( pObj->fMark1 ) + { + Delay = Abc_MaxInt( Delay1 + DelayC, Delay0 + 100 ); + nBoxes++; + } + else + Delay = Abc_MaxInt( Delay0 + 100, Delay1 + 100 ); + pDelays[i] = Delay; + } + if ( pnBoxes ) + *pnBoxes = nBoxes; + return DelayMax; +} +// check if the object is already used in some chain +static inline int Gia_ObjIsUsed( Gia_Obj_t * pObj ) +{ + return pObj->fMark0 || pObj->fMark1 || pObj->fPhase; +} +// finds internal node that can begin a new chain +int Gia_ManFindChainStart( Gia_Man_t * p ) +{ + Gia_Obj_t * pObj; + int * pDelays = Vec_IntArray(p->vLevels); + int i, iMax = -1, DelayMax = 0; + Gia_ManForEachAnd( p, pObj, i ) + { + if ( Gia_ObjIsUsed(pObj) ) + continue; + if ( DelayMax > pDelays[i] ) + continue; + DelayMax = pDelays[i]; + iMax = i; + } + return iMax; +} +// finds a sequence of internal nodes that creates a new chain +int Gia_ManFindPath( Gia_Man_t * p, int DelayC, int nPathMin, int nPathMax, Vec_Int_t * vPath ) +{ + Gia_Obj_t * pObj, * pFanin0, * pFanin1; + int * pDelays = Vec_IntArray(p->vLevels); + int i, iLit, iMax = Gia_ManFindChainStart( p ); + if ( iMax == -1 ) + return -1; + Vec_IntClear( vPath ); + pObj = Gia_ManObj(p, iMax); + assert( Gia_ObjIsAnd(pObj) ); + while ( Gia_ObjIsAnd(pObj) ) + { + assert( !Gia_ObjIsUsed(pObj) ); + pFanin0 = Gia_ObjFanin0(pObj); + pFanin1 = Gia_ObjFanin1(pObj); + if ( Gia_ObjIsUsed(pFanin0) && Gia_ObjIsUsed(pFanin1) ) + break; + if ( Gia_ObjIsUsed(pFanin0) ) + { + Vec_IntPush( vPath, Abc_Var2Lit(Gia_ObjId(p, pObj), 1) ); + pObj = pFanin1; + } + else if ( Gia_ObjIsUsed(pFanin1) ) + { + Vec_IntPush( vPath, Abc_Var2Lit(Gia_ObjId(p, pObj), 0) ); + pObj = pFanin0; + } + else + { + if ( pDelays[Gia_ObjId(p, pFanin1)] > pDelays[Gia_ObjId(p, pFanin0)] ) + { + Vec_IntPush( vPath, Abc_Var2Lit(Gia_ObjId(p, pObj), 1) ); + pObj = pFanin1; + } + else + { + Vec_IntPush( vPath, Abc_Var2Lit(Gia_ObjId(p, pObj), 0) ); + pObj = pFanin0; + } + } + } + if ( Vec_IntSize(vPath) < nPathMin ) + { + Gia_ManObj(p, iMax)->fPhase = 1; + return 0; + } + // label nodes + if ( Vec_IntSize(vPath) > nPathMax ) + Vec_IntShrink( vPath, nPathMax ); + Vec_IntForEachEntry( vPath, iLit, i ) + { + pObj = Gia_ManObj( p, Abc_Lit2Var(iLit) ); + if ( Abc_LitIsCompl(iLit) ) + { + assert( pObj->fMark1 == 0 ); + pObj->fMark1 = 1; + assert( Gia_ObjFanin1(pObj)->fPhase == 0 ); + Gia_ObjFanin1(pObj)->fPhase = 1; + } + else + { + assert( pObj->fMark0 == 0 ); + pObj->fMark0 = 1; + assert( Gia_ObjFanin0(pObj)->fPhase == 0 ); + Gia_ObjFanin0(pObj)->fPhase = 1; + } + } + return Vec_IntSize(vPath); +} +// iteratively create the given number of chains +int Gia_ManIteratePaths( Gia_Man_t * p, int DelayC, int nPathMin, int nPathMax, int nPathLimit, int fIgnoreBoxDelays, int fVerbose ) +{ + Gia_Obj_t * pObj; + Vec_Int_t * vPath = Vec_IntAlloc( 100 ); + int i, RetValue, nBoxes, MaxDelay, nPaths = 0; + assert( p->vLevels == NULL ); + p->vLevels = Vec_IntStart( Gia_ManObjNum(p) ); + Gia_ManCleanMark01( p ); + Gia_ManCleanPhase( p ); + Gia_ManForEachCi( p, pObj, i ) + pObj->fPhase = 1; + if ( fVerbose ) + printf( "Running path detection: BoxDelay = %d, PathMin = %d, PathMax = %d, PathLimit = %d.\n", DelayC, nPathMin, nPathMax, nPathLimit ); + for ( i = 0; i < nPathLimit; i++ ) + { + MaxDelay = Gia_ManFindAnnotatedDelay( p, DelayC, &nBoxes, fIgnoreBoxDelays ); + RetValue = Gia_ManFindPath( p, DelayC, nPathMin, nPathMax, vPath ); + if ( RetValue == -1 ) + break; + nPaths += (RetValue > 0); + if ( fVerbose ) + printf( "Iter %5d : Paths = %2d. Boxes = %2d. Total boxes = %6d. Max delay = %5d.\n", i, nPaths, RetValue, nBoxes, MaxDelay ); + } + Vec_IntFree( vPath ); + Vec_IntFreeP( &p->vLevels ); + Gia_ManCleanPhase( p ); + return 1; +} +// annotate artificial chains and then put them into boxes +Gia_Man_t * Gia_ManDupWithArtificialBoxes( Gia_Man_t * p, int DelayC, int nPathMin, int nPathMax, int nPathLimit, int fUseFanout, int fXorTrick, int fIgnoreBoxDelays, int fVerbose ) +{ + Gia_Man_t * pNew; +/* + if ( Gia_ManBoxNum(p) > 0 ) + { + printf( "Currently artifical carry-chains cannot be detected when natural ones are present.\n" ); + return NULL; + } +*/ + Gia_ManIteratePaths( p, DelayC, nPathMin, nPathMax, nPathLimit, fIgnoreBoxDelays, fVerbose ); + pNew = Gia_ManDupWithArtificalFaddBoxes( p, fUseFanout, fXorTrick ); + Gia_ManCleanMark01( p ); + return pNew; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/acec/acecInt.h b/src/proof/acec/acecInt.h new file mode 100644 index 00000000..28e8740b --- /dev/null +++ b/src/proof/acec/acecInt.h @@ -0,0 +1,76 @@ +/**CFile**************************************************************** + + FileName [acecInt.h] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [CEC for arithmetic circuits.] + + Synopsis [Internal declarations.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: acecInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#ifndef ABC__proof__acec__acec__int_h +#define ABC__proof__acec__acec__int_h + + +//////////////////////////////////////////////////////////////////////// +/// INCLUDES /// +//////////////////////////////////////////////////////////////////////// + +#include "aig/gia/gia.h" +#include "proof/cec/cec.h" +#include "acec.h" + +//////////////////////////////////////////////////////////////////////// +/// PARAMETERS /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_HEADER_START + + +//////////////////////////////////////////////////////////////////////// +/// BASIC TYPES /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// MACRO DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// ITERATORS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/*=== acecFadds.c ========================================================*/ +extern Vec_Int_t * Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose ); +extern Vec_Int_t * Gia_ManDetectHalfAdders( Gia_Man_t * p, int fVerbose ); +/*=== acecOrder.c ========================================================*/ +extern Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose ); +/*=== acecPolyn.c ========================================================*/ +extern void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose ); +/*=== acecUtil.c ========================================================*/ +extern void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose ); + +ABC_NAMESPACE_HEADER_END + + + +#endif + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + diff --git a/src/proof/acec/acecOrder.c b/src/proof/acec/acecOrder.c new file mode 100644 index 00000000..0cf686c8 --- /dev/null +++ b/src/proof/acec/acecOrder.c @@ -0,0 +1,178 @@ +/**CFile**************************************************************** + + FileName [acecOrder.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [CEC for arithmetic circuits.] + + Synopsis [Node ordering.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: acecOrder.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "acecInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_PolynReorder( Gia_Man_t * pGia, int fVerbose ) +{ + int fDumpLeftOver = 0; + Vec_Int_t * vOrder, * vOrder2; + Gia_Obj_t * pFan0, * pFan1; + int i, k, iDriver, Iter, iXor, iMaj, Entry, fFound; + Vec_Int_t * vFadds = Gia_ManDetectFullAdders( pGia, fVerbose ); + Vec_Int_t * vHadds = Gia_ManDetectHalfAdders( pGia, fVerbose ); + Vec_Int_t * vRecord = Vec_IntAlloc( 100 ); + + Vec_Int_t * vMap = Vec_IntStart( Gia_ManObjNum(pGia) ); + Gia_ManForEachCoDriverId( pGia, iDriver, i ) + Vec_IntWriteEntry( vMap, iDriver, 1 ); + + for ( Iter = 0; ; Iter++ ) + { + int fFoundAll = 0; + printf( "Iteration %d\n", Iter ); + + // find the last one + iDriver = -1; + Vec_IntForEachEntryReverse( vMap, Entry, i ) + if ( Entry ) + { + iDriver = i; + break; + } + + if ( iDriver > 0 && Gia_ObjRecognizeExor(Gia_ManObj(pGia, iDriver), &pFan0, &pFan1) && Vec_IntFind(vFadds, iDriver) == -1 && Vec_IntFind(vHadds, iDriver) == -1 ) + { + Vec_IntWriteEntry( vMap, iDriver, 0 ); + Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pFan0), 1 ); + Vec_IntWriteEntry( vMap, Gia_ObjId(pGia, pFan1), 1 ); + Vec_IntPush( vRecord, iDriver ); + printf( "Recognizing %d => XOR(%d %d)\n", iDriver, Gia_ObjId(pGia, pFan0), Gia_ObjId(pGia, pFan1) ); + } + + // check if we can extract FADDs + do { + fFound = 0; + for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ ) + { + iXor = Vec_IntEntry(vFadds, 5*i+3); + iMaj = Vec_IntEntry(vFadds, 5*i+4); + if ( Vec_IntEntry(vMap, iXor) && Vec_IntEntry(vMap, iMaj) ) + { + Vec_IntWriteEntry( vMap, iXor, 0 ); + Vec_IntWriteEntry( vMap, iMaj, 0 ); + Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+0), 1 ); + Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+1), 1 ); + Vec_IntWriteEntry( vMap, Vec_IntEntry(vFadds, 5*i+2), 1 ); + Vec_IntPush( vRecord, iXor ); + Vec_IntPush( vRecord, iMaj ); + fFound = 1; + fFoundAll = 1; + printf( "Recognizing (%d %d) => FA(%d %d %d)\n", iXor, iMaj, Vec_IntEntry(vFadds, 5*i+0), Vec_IntEntry(vFadds, 5*i+1), Vec_IntEntry(vFadds, 5*i+2) ); + } + } + } while ( fFound ); + // check if we can extract HADDs + do { + fFound = 0; + Vec_IntForEachEntryDouble( vHadds, iXor, iMaj, i ) + { + if ( Vec_IntEntry(vMap, iXor) && Vec_IntEntry(vMap, iMaj) ) + { + Gia_Obj_t * pAnd = Gia_ManObj( pGia, iMaj ); + Vec_IntWriteEntry( vMap, iXor, 0 ); + Vec_IntWriteEntry( vMap, iMaj, 0 ); + Vec_IntWriteEntry( vMap, Gia_ObjFaninId0(pAnd, iMaj), 1 ); + Vec_IntWriteEntry( vMap, Gia_ObjFaninId1(pAnd, iMaj), 1 ); + Vec_IntPush( vRecord, iXor ); + Vec_IntPush( vRecord, iMaj ); + fFound = 1; + fFoundAll = 1; + printf( "Recognizing (%d %d) => HA(%d %d)\n", iXor, iMaj, Gia_ObjFaninId0(pAnd, iMaj), Gia_ObjFaninId1(pAnd, iMaj) ); + } + } + } while ( fFound ); + if ( fFoundAll == 0 ) + break; + } + + //Vec_IntPrint( vRecord ); + printf( "Remaining: " ); + Vec_IntForEachEntry( vMap, Entry, i ) + if ( Entry ) + printf( "%d ", i ); + printf( "\n" ); + + // collect remaining nodes + k = 0; + Vec_IntForEachEntry( vMap, Entry, i ) + if ( Entry && Gia_ObjIsAnd(Gia_ManObj(pGia, i)) ) + Vec_IntWriteEntry( vMap, k++, i ); + Vec_IntShrink( vMap, k ); + + // dump remaining nodes as an AIG + if ( fDumpLeftOver ) + { + Gia_Man_t * pNew = Gia_ManDupAndCones( pGia, Vec_IntArray(vMap), Vec_IntSize(vMap), 0 ); + Gia_AigerWrite( pNew, "leftover.aig", 0, 0 ); + Gia_ManStop( pNew ); + } + + // collect nodes + vOrder = Vec_IntAlloc( Gia_ManAndNum(pGia) ); + Gia_ManIncrementTravId( pGia ); + Gia_ManCollectAnds( pGia, Vec_IntArray(vMap), Vec_IntSize(vMap), vOrder, NULL ); + Vec_IntForEachEntryReverse( vRecord, Entry, i ) + Gia_ManCollectAnds_rec( pGia, Entry, vOrder ); + assert( Vec_IntSize(vOrder) == Gia_ManAndNum(pGia) ); + + // remap order + vOrder2 = Vec_IntStart( Gia_ManObjNum(pGia) ); + Vec_IntForEachEntry( vOrder, Entry, i ) + Vec_IntWriteEntry( vOrder2, Entry, i+1 ); + Vec_IntFree( vOrder ); + + Vec_IntFree( vMap ); + Vec_IntFree( vRecord ); + Vec_IntFree( vFadds ); + Vec_IntFree( vHadds ); + return vOrder2; +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/acec/acecPolyn.c b/src/proof/acec/acecPolyn.c new file mode 100644 index 00000000..df6ef2a2 --- /dev/null +++ b/src/proof/acec/acecPolyn.c @@ -0,0 +1,371 @@ +/**CFile**************************************************************** + + FileName [acecPolyn.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [CEC for arithmetic circuits.] + + Synopsis [Polynomial extraction.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: acecPolyn.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "acecInt.h" +#include "misc/vec/vecWec.h" +#include "misc/vec/vecHsh.h" +#include "misc/vec/vecQue.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +/* +!a -> 1 - a +a & b -> ab +a | b -> a + b - ab +a ^ b -> a + b - 2ab +MUX(a, b, c) -> ab | (1 - a)c = ab + (1-a)c - ab(1-a)c = ab + c - ac + +!a & b -> (1 - a)b = b - ab + a & !b -> a(1 - b) = a - ab +!a & !b -> 1 - a - b + ab +*/ + +typedef struct Pln_Man_t_ Pln_Man_t; +struct Pln_Man_t_ +{ + Gia_Man_t * pGia; // AIG manager + Hsh_VecMan_t * pHashC; // hash table for constants + Hsh_VecMan_t * pHashM; // hash table for monomials + Vec_Que_t * vQue; // queue by largest node + Vec_Flt_t * vCounts; // largest node + Vec_Int_t * vCoefs; // coefficients for each monomial + Vec_Int_t * vTempC[2]; // polynomial representation + Vec_Int_t * vTempM[4]; // polynomial representation + Vec_Int_t * vOrder; // order of collapsing + int nBuilds; // builds +}; + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + + + +/**Function************************************************************* + + Synopsis [Computation manager.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Pln_Man_t * Pln_ManAlloc( Gia_Man_t * pGia, Vec_Int_t * vOrder ) +{ + Pln_Man_t * p = ABC_CALLOC( Pln_Man_t, 1 ); + p->pGia = pGia; + p->pHashC = Hsh_VecManStart( 1000 ); + p->pHashM = Hsh_VecManStart( 1000 ); + p->vQue = Vec_QueAlloc( 1000 ); + p->vCounts = Vec_FltAlloc( 1000 ); + p->vCoefs = Vec_IntAlloc( 1000 ); + p->vTempC[0] = Vec_IntAlloc( 100 ); + p->vTempC[1] = Vec_IntAlloc( 100 ); + p->vTempM[0] = Vec_IntAlloc( 100 ); + p->vTempM[1] = Vec_IntAlloc( 100 ); + p->vTempM[2] = Vec_IntAlloc( 100 ); + p->vTempM[3] = Vec_IntAlloc( 100 ); + p->vOrder = vOrder ? vOrder : Vec_IntStartNatural( Gia_ManObjNum(pGia) ); + assert( Vec_IntSize(p->vOrder) == Gia_ManObjNum(pGia) ); + Vec_QueSetPriority( p->vQue, Vec_FltArrayP(p->vCounts) ); + // add 0-constant and 1-monomial + Hsh_VecManAdd( p->pHashC, p->vTempC[0] ); + Hsh_VecManAdd( p->pHashM, p->vTempM[0] ); + Vec_FltPush( p->vCounts, 0 ); + Vec_IntPush( p->vCoefs, 0 ); + return p; +} +void Pln_ManStop( Pln_Man_t * p ) +{ + Hsh_VecManStop( p->pHashC ); + Hsh_VecManStop( p->pHashM ); + Vec_QueFree( p->vQue ); + Vec_FltFree( p->vCounts ); + Vec_IntFree( p->vCoefs ); + Vec_IntFree( p->vTempC[0] ); + Vec_IntFree( p->vTempC[1] ); + Vec_IntFree( p->vTempM[0] ); + Vec_IntFree( p->vTempM[1] ); + Vec_IntFree( p->vTempM[2] ); + Vec_IntFree( p->vTempM[3] ); + Vec_IntFree( p->vOrder ); + ABC_FREE( p ); +} +void Pln_ManPrintFinal( Pln_Man_t * p ) +{ + Vec_Int_t * vArray; + int k, Entry, iMono, iConst, Count = 0; + Vec_IntForEachEntry( p->vCoefs, iConst, iMono ) + { + if ( iConst == 0 ) + continue; + + Count++; + + if ( Count > 40 ) + continue; + + vArray = Hsh_VecReadEntry( p->pHashC, iConst ); + Vec_IntForEachEntry( vArray, Entry, k ) + printf( "%s%d", Entry < 0 ? "-" : "+", (1 << (Abc_AbsInt(Entry)-1)) ); + + vArray = Hsh_VecReadEntry( p->pHashM, iMono ); + Vec_IntForEachEntry( vArray, Entry, k ) + printf( " * %d", Entry ); + printf( "\n" ); + } + printf( "HashC = %d. HashM = %d. Total = %d. Used = %d.\n", Hsh_VecSize(p->pHashC), Hsh_VecSize(p->pHashM), p->nBuilds, Count ); +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static inline void Gia_PolynMergeConstOne( Vec_Int_t * vConst, int New ) +{ + int i, Old; + assert( New != 0 ); + Vec_IntForEachEntry( vConst, Old, i ) + { + assert( Old != 0 ); + if ( Old == New ) // A == B + { + Vec_IntDrop( vConst, i ); + Gia_PolynMergeConstOne( vConst, New > 0 ? New + 1 : New - 1 ); + return; + } + if ( Abc_AbsInt(Old) == Abc_AbsInt(New) ) // A == -B + { + Vec_IntDrop( vConst, i ); + return; + } + if ( Old + New == 1 || Old + New == -1 ) // sign(A) != sign(B) && abs(abs(A)-abs(B)) == 1 + { + int Value = Abc_MinInt( Abc_AbsInt(Old), Abc_AbsInt(New) ); + Vec_IntDrop( vConst, i ); + Gia_PolynMergeConstOne( vConst, (Old + New == 1) ? Value : -Value ); + return; + } + } + Vec_IntPushUniqueOrder( vConst, New ); +} +static inline void Gia_PolynMergeConst( Vec_Int_t * vConst, Pln_Man_t * p, int iConstAdd ) +{ + int i, New; + Vec_Int_t * vConstAdd = Hsh_VecReadEntry( p->pHashC, iConstAdd ); + Vec_IntForEachEntry( vConstAdd, New, i ) + { + Gia_PolynMergeConstOne( vConst, New ); + vConstAdd = Hsh_VecReadEntry( p->pHashC, iConstAdd ); + } +} +static inline void Gia_PolynBuildAdd( Pln_Man_t * p, Vec_Int_t * vTempC, Vec_Int_t * vTempM ) +{ + int iConst, iMono = vTempM ? Hsh_VecManAdd(p->pHashM, vTempM) : 0; + p->nBuilds++; + if ( iMono == Vec_IntSize(p->vCoefs) ) // new monomial + { + iConst = Hsh_VecManAdd( p->pHashC, vTempC ); + Vec_IntPush( p->vCoefs, iConst ); +// Vec_FltPush( p->vCounts, Vec_IntEntryLast(vTempM) ); + Vec_FltPush( p->vCounts, (float)Vec_IntEntry(p->vOrder, Vec_IntEntryLast(vTempM)) ); + Vec_QuePush( p->vQue, iMono ); +// Vec_QueUpdate( p->vQue, iMono ); + return; + } + // this monomial exists + iConst = Vec_IntEntry( p->vCoefs, iMono ); + if ( iConst ) + Gia_PolynMergeConst( vTempC, p, iConst ); + iConst = Hsh_VecManAdd( p->pHashC, vTempC ); + Vec_IntWriteEntry( p->vCoefs, iMono, iConst ); +} +void Gia_PolynBuildOne( Pln_Man_t * p, int iMono ) +{ + Gia_Obj_t * pObj; + Vec_Int_t * vArray, * vConst; + int iFan0, iFan1; + int k, iConst, iDriver; + + assert( Vec_IntSize(p->vCoefs) == Hsh_VecSize(p->pHashM) ); + vArray = Hsh_VecReadEntry( p->pHashM, iMono ); + iDriver = Vec_IntEntryLast( vArray ); + pObj = Gia_ManObj( p->pGia, iDriver ); + if ( !Gia_ObjIsAnd(pObj) ) + return; + + iConst = Vec_IntEntry( p->vCoefs, iMono ); + if ( iConst == 0 ) + return; + Vec_IntWriteEntry( p->vCoefs, iMono, 0 ); + + iFan0 = Gia_ObjFaninId0p(p->pGia, pObj); + iFan1 = Gia_ObjFaninId1p(p->pGia, pObj); + for ( k = 0; k < 4; k++ ) + { + Vec_IntClear( p->vTempM[k] ); + Vec_IntAppend( p->vTempM[k], vArray ); + Vec_IntPop( p->vTempM[k] ); + if ( k == 1 || k == 3 ) + Vec_IntPushUniqueOrderCost( p->vTempM[k], iFan0, p->vOrder ); // x +// Vec_IntPushUniqueOrder( p->vTempM[k], iFan0 ); // x + if ( k == 2 || k == 3 ) + Vec_IntPushUniqueOrderCost( p->vTempM[k], iFan1, p->vOrder ); // y +// Vec_IntPushUniqueOrder( p->vTempM[k], iFan1 ); // y + } + + vConst = Hsh_VecReadEntry( p->pHashC, iConst ); + for ( k = 0; k < 2; k++ ) + Vec_IntAppendMinus( p->vTempC[k], vConst, k ); + + if ( Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) // C * (1 - x) * (1 - y) + { + Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[0] ); // C * 1 + Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[1] ); // -C * x + vConst = Hsh_VecReadEntry( p->pHashC, iConst ); + for ( k = 0; k < 2; k++ ) + Vec_IntAppendMinus( p->vTempC[k], vConst, k ); + Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[2] ); // -C * y + Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[3] ); // C * x * y + } + else if ( Gia_ObjFaninC0(pObj) && !Gia_ObjFaninC1(pObj) ) // C * (1 - x) * y + { + Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[2] ); // C * y + Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[3] ); // -C * x * y + } + else if ( !Gia_ObjFaninC0(pObj) && Gia_ObjFaninC1(pObj) ) // C * x * (1 - y) + { + Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[1] ); // C * x + Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[3] ); // -C * x * y + } + else + Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[3] ); // C * x * y +} +int Gia_PolyFindNext2( Pln_Man_t * p ) +{ + Gia_Obj_t * pObj; + Vec_Int_t * vArray; + int Max = 0, iBest = 0, iConst, iMono, iDriver; + Vec_IntForEachEntryStart( p->vCoefs, iConst, iMono, 1 ) + { + if ( iConst == 0 ) + continue; + vArray = Hsh_VecReadEntry( p->pHashM, iMono ); + iDriver = Vec_IntEntryLast( vArray ); + pObj = Gia_ManObj( p->pGia, iDriver ); + if ( !Gia_ObjIsAnd(pObj) ) + continue; + if ( Max < Vec_IntEntryLast(vArray) ) + { + Max = Vec_IntEntryLast(vArray); + iBest = iMono; + } + } + //Vec_IntPrint( Hsh_VecReadEntry(p->pHashM, iBest) ); + return iBest; +} +int Gia_PolyFindNext( Pln_Man_t * p ) +{ + int iBest = Vec_QueSize(p->vQue) ? Vec_QuePop(p->vQue) : 0; + //Vec_IntPrint( Hsh_VecReadEntry(p->pHashM, iBest) ); + return iBest; +} +void Gia_PolynBuild( Gia_Man_t * pGia, Vec_Int_t * vOrder, int fVerbose ) +{ + abctime clk = Abc_Clock();//, clk2 = 0; + Gia_Obj_t * pObj; + Vec_Bit_t * vPres = Vec_BitStart( Gia_ManObjNum(pGia) ); + int i, iMono, iDriver, LevPrev, LevCur, Iter, Line = 0; + Pln_Man_t * p = Pln_ManAlloc( pGia, vOrder ); + Gia_ManForEachCoReverse( pGia, pObj, i ) + { + Vec_IntFill( p->vTempC[0], 1, i+1 ); // 2^i + Vec_IntFill( p->vTempC[1], 1, -i-1 ); // -2^i + + iDriver = Gia_ObjFaninId0p( pGia, pObj ); + Vec_IntFill( p->vTempM[0], 1, iDriver ); // Driver + + if ( Gia_ObjFaninC0(pObj) ) + { + Gia_PolynBuildAdd( p, p->vTempC[0], NULL ); // C + Gia_PolynBuildAdd( p, p->vTempC[1], p->vTempM[0] ); // -C * Driver + } + else + Gia_PolynBuildAdd( p, p->vTempC[0], p->vTempM[0] ); // C * Driver + } + LevPrev = -1; + for ( Iter = 0; ; Iter++ ) + { + Vec_Int_t * vTempM; + //abctime temp = Abc_Clock(); + iMono = Gia_PolyFindNext(p); + if ( !iMono ) + break; + + // report + vTempM = Hsh_VecReadEntry( p->pHashM, iMono ); + //printf( "Removing var %d\n", Vec_IntEntryLast(vTempM) ); + +// LevCur = Vec_IntEntryLast(vTempM); + LevCur = Vec_IntEntry(p->vOrder, Vec_IntEntryLast(vTempM)); + if ( LevPrev != LevCur ) + { + if ( Vec_BitEntry( vPres, LevCur & 0xFF ) ) + printf( "Repeating entry %d\n", LevCur & 0xFF ); + else + Vec_BitSetEntry( vPres, LevCur & 0xFF, 1 ); + + printf( "Line %5d Iter %6d : Cur = %8x. Obj = %5d. HashC =%8d. HashM =%8d. Total =%8d. Used =%8d.\n", + Line++, Iter, LevCur, LevCur & 0xFF, Hsh_VecSize(p->pHashC), Hsh_VecSize(p->pHashM), p->nBuilds, -1 ); + } + LevPrev = LevCur; + + Gia_PolynBuildOne( p, iMono ); + //clk2 += Abc_Clock() - temp; + } + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); + //Abc_PrintTime( 1, "Time2", clk2 ); + Pln_ManPrintFinal( p ); + Pln_ManStop( p ); + Vec_BitFree( vPres ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/acec/acecUtil.c b/src/proof/acec/acecUtil.c new file mode 100644 index 00000000..26087f92 --- /dev/null +++ b/src/proof/acec/acecUtil.c @@ -0,0 +1,87 @@ +/**CFile**************************************************************** + + FileName [acecUtil.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [CEC for arithmetic circuits.] + + Synopsis [Various utilities.] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: acecUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "acecInt.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_PolynCollectXors_rec( Gia_Man_t * pGia, int iObj, Vec_Int_t * vXors ) +{ + Gia_Obj_t * pObj = Gia_ManObj( pGia, iObj ); + if ( Gia_ObjIsTravIdCurrent(pGia, pObj) ) + return; + Gia_ObjSetTravIdCurrent(pGia, pObj); + if ( !Gia_ObjIsAnd(pObj) || !Gia_ObjIsXor(pObj) ) + return; + Vec_IntPush( vXors, iObj ); + Gia_PolynCollectXors_rec( pGia, Gia_ObjFaninId0(pObj, iObj), vXors ); + Gia_PolynCollectXors_rec( pGia, Gia_ObjFaninId1(pObj, iObj), vXors ); +} +void Gia_PolynAnalyzeXors( Gia_Man_t * pGia, int fVerbose ) +{ + int i, iDriver, Count = 0; + Vec_Int_t * vXors = Vec_IntAlloc( 100 ); + if ( pGia->pMuxes == NULL ) + { + printf( "AIG does not have XORs extracted.\n" ); + return; + } + assert( pGia->pMuxes ); + Gia_ManForEachCoDriverId( pGia, iDriver, i ) + { + Vec_IntClear( vXors ); + Gia_ManIncrementTravId( pGia ); + Gia_PolynCollectXors_rec( pGia, iDriver, vXors ); + //printf( "%3d : ", i ); + //Vec_IntPrint( vXors ); + printf( "%d=%d ", i, Vec_IntSize(vXors) ); + Count += Vec_IntSize(vXors); + } + printf( "Total = %d.\n", Count ); + Vec_IntFree( vXors ); +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/proof/acec/module.make b/src/proof/acec/module.make new file mode 100644 index 00000000..20da6358 --- /dev/null +++ b/src/proof/acec/module.make @@ -0,0 +1,5 @@ +SRC += src/proof/acec/acecCore. \ + src/proof/acec/acecFadds.c \ + src/proof/acec/acecOrder.c \ + src/proof/acec/acecPolyn.c \ + src/proof/acec/acecUtil.c -- cgit v1.2.3