diff options
Diffstat (limited to 'src/aig/gia')
| -rw-r--r-- | src/aig/gia/gia.h | 75 | ||||
| -rw-r--r-- | src/aig/gia/giaAig.c | 11 | ||||
| -rw-r--r-- | src/aig/gia/giaDup.c | 304 | ||||
| -rw-r--r-- | src/aig/gia/giaEquiv.c | 29 | ||||
| -rw-r--r-- | src/aig/gia/giaIf.c | 42 | ||||
| -rw-r--r-- | src/aig/gia/giaJf.c | 30 | ||||
| -rw-r--r-- | src/aig/gia/giaKf.c | 14 | ||||
| -rw-r--r-- | src/aig/gia/giaLf.c | 21 | ||||
| -rw-r--r-- | src/aig/gia/giaMf.c | 73 | ||||
| -rw-r--r-- | src/aig/gia/giaMfs.c | 1 | ||||
| -rw-r--r-- | src/aig/gia/giaMini.c | 41 | ||||
| -rw-r--r-- | src/aig/gia/giaNf.c | 17 | ||||
| -rw-r--r-- | src/aig/gia/giaQbf.c | 12 | ||||
| -rw-r--r-- | src/aig/gia/giaSatoko.c | 205 | ||||
| -rw-r--r-- | src/aig/gia/giaShow.c | 1045 | ||||
| -rw-r--r-- | src/aig/gia/giaTim.c | 2 | ||||
| -rw-r--r-- | src/aig/gia/giaTruth.c | 53 | ||||
| -rw-r--r-- | src/aig/gia/giaUtil.c | 4 | ||||
| -rw-r--r-- | src/aig/gia/module.make | 1 |
19 files changed, 1600 insertions, 380 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index bf7bf349..5ad87008 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -194,6 +194,7 @@ struct Gia_Man_t_ int MappedDelay; // delay after mapping // bit-parallel simulation int iPatsPi; + int nSimWords; Vec_Wrd_t * vSims; Vec_Wrd_t * vSimsPi; Vec_Int_t * vClassOld; @@ -311,6 +312,7 @@ struct Jf_Par_t_ int fGenCnf; int fCnfObjIds; int fAddOrCla; + int fCnfMapping; int fPureAig; int fDoAverage; int fCutHashing; @@ -665,21 +667,6 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 ) } return Gia_ObjId( p, pObj ) << 1; } -static inline int Gia_ManAppendAnd2( Gia_Man_t * p, int iLit0, int iLit1 ) -{ - if ( !p->fGiaSimple ) - { - if ( iLit0 < 2 ) - return iLit0 ? iLit1 : 0; - if ( iLit1 < 2 ) - return iLit1 ? iLit0 : 0; - if ( iLit0 == iLit1 ) - return iLit1; - if ( iLit0 == Abc_LitNot(iLit1) ) - return 0; - } - return Gia_ManAppendAnd( p, iLit0, iLit1 ); -} static inline int Gia_ManAppendXorReal( Gia_Man_t * p, int iLit0, int iLit1 ) { Gia_Obj_t * pObj = Gia_ManAppendObj( p ); @@ -780,6 +767,44 @@ static inline int Gia_ManAppendXor( Gia_Man_t * p, int iLit0, int iLit1 ) { return Gia_ManAppendMux( p, iLit0, Abc_LitNot(iLit1), iLit1 ); } + +static inline int Gia_ManAppendAnd2( Gia_Man_t * p, int iLit0, int iLit1 ) +{ + if ( !p->fGiaSimple ) + { + if ( iLit0 < 2 ) + return iLit0 ? iLit1 : 0; + if ( iLit1 < 2 ) + return iLit1 ? iLit0 : 0; + if ( iLit0 == iLit1 ) + return iLit1; + if ( iLit0 == Abc_LitNot(iLit1) ) + return 0; + } + return Gia_ManAppendAnd( p, iLit0, iLit1 ); +} +static inline int Gia_ManAppendOr2( Gia_Man_t * p, int iLit0, int iLit1 ) +{ + return Abc_LitNot(Gia_ManAppendAnd2( p, Abc_LitNot(iLit0), Abc_LitNot(iLit1) )); +} +static inline int Gia_ManAppendMux2( Gia_Man_t * p, int iCtrl, int iData1, int iData0 ) +{ + int iTemp0 = Gia_ManAppendAnd2( p, Abc_LitNot(iCtrl), iData0 ); + int iTemp1 = Gia_ManAppendAnd2( p, iCtrl, iData1 ); + return Abc_LitNotCond( Gia_ManAppendAnd2( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), 1 ); +} +static inline int Gia_ManAppendMaj2( Gia_Man_t * p, int iData0, int iData1, int iData2 ) +{ + int iTemp0 = Gia_ManAppendOr2( p, iData1, iData2 ); + int iTemp1 = Gia_ManAppendAnd2( p, iData0, iTemp0 ); + int iTemp2 = Gia_ManAppendAnd2( p, iData1, iData2 ); + return Gia_ManAppendOr2( p, iTemp1, iTemp2 ); +} +static inline int Gia_ManAppendXor2( Gia_Man_t * p, int iLit0, int iLit1 ) +{ + return Gia_ManAppendMux2( p, iLit0, Abc_LitNot(iLit1), iLit1 ); +} + static inline void Gia_ManPatchCoDriver( Gia_Man_t * p, int iCoIndex, int iLit0 ) { Gia_Obj_t * pObjCo = Gia_ManCo( p, iCoIndex ); @@ -958,24 +983,26 @@ static inline void Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num ) { p static inline int Gia_ObjIsConst( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == 0; } static inline int Gia_ObjIsHead( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) > 0; } -static inline int Gia_ObjIsNone( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) == 0; } -static inline int Gia_ObjIsTail( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) == 0; } +static inline int Gia_ObjIsNone( Gia_Man_t * p, int Id ) { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) <= 0; } +static inline int Gia_ObjIsTail( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) <= 0; } static inline int Gia_ObjIsClass( Gia_Man_t * p, int Id ) { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) || Gia_ObjNext(p, Id) > 0; } static inline int Gia_ObjHasSameRepr( Gia_Man_t * p, int i, int k ) { assert( k ); return i? (Gia_ObjRepr(p, i) == Gia_ObjRepr(p, k) && Gia_ObjRepr(p, i) != GIA_VOID) : Gia_ObjRepr(p, k) == 0; } static inline int Gia_ObjIsFailedPair( Gia_Man_t * p, int i, int k ) { assert( k ); return i? (Gia_ObjFailed(p, i) || Gia_ObjFailed(p, k)) : Gia_ObjFailed(p, k); } -static inline int Gia_ClassIsPair( Gia_Man_t * p, int i ) { assert( Gia_ObjIsHead(p, i) ); assert( Gia_ObjNext(p, i) ); return Gia_ObjNext(p, Gia_ObjNext(p, i)) == 0; } +static inline int Gia_ClassIsPair( Gia_Man_t * p, int i ) { assert( Gia_ObjIsHead(p, i) ); assert( Gia_ObjNext(p, i) ); return Gia_ObjNext(p, Gia_ObjNext(p, i)) <= 0; } static inline void Gia_ClassUndoPair( Gia_Man_t * p, int i ) { assert( Gia_ClassIsPair(p,i) ); Gia_ObjSetRepr(p, Gia_ObjNext(p, i), GIA_VOID); Gia_ObjSetNext(p, i, 0); } #define Gia_ManForEachConst( p, i ) \ for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsConst(p, i) ) {} else #define Gia_ManForEachClass( p, i ) \ for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsHead(p, i) ) {} else +#define Gia_ManForEachClass0( p, i ) \ + for ( i = 0; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsHead(p, i) ) {} else #define Gia_ManForEachClassReverse( p, i ) \ for ( i = Gia_ManObjNum(p) - 1; i > 0; i-- ) if ( !Gia_ObjIsHead(p, i) ) {} else #define Gia_ClassForEachObj( p, i, iObj ) \ - for ( assert(Gia_ObjIsHead(p, i)), iObj = i; iObj; iObj = Gia_ObjNext(p, iObj) ) + for ( assert(Gia_ObjIsHead(p, i)), iObj = i; iObj > 0; iObj = Gia_ObjNext(p, iObj) ) #define Gia_ClassForEachObj1( p, i, iObj ) \ - for ( assert(Gia_ObjIsHead(p, i)), iObj = Gia_ObjNext(p, i); iObj; iObj = Gia_ObjNext(p, iObj) ) + for ( assert(Gia_ObjIsHead(p, i)), iObj = Gia_ObjNext(p, i); iObj > 0; iObj = Gia_ObjNext(p, iObj) ) static inline int Gia_ObjFoffsetId( Gia_Man_t * p, int Id ) { return Vec_IntEntry( p->vFanout, Id ); } @@ -1205,6 +1232,7 @@ extern Gia_Man_t * Gia_ManDupTrimmed( Gia_Man_t * p, int fTrimCis, int f extern Gia_Man_t * Gia_ManDupOntop( Gia_Man_t * p, Gia_Man_t * p2 ); extern Gia_Man_t * Gia_ManDupWithNewPo( Gia_Man_t * p1, Gia_Man_t * p2 ); extern Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits ); +extern Gia_Man_t * Gia_ManPermuteInputs( Gia_Man_t * p, int nPpis, int nExtra ); extern Gia_Man_t * Gia_ManDupDfsClasses( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManDupTopAnd( Gia_Man_t * p, int fVerbose ); extern Gia_Man_t * Gia_ManMiter( Gia_Man_t * pAig0, Gia_Man_t * pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose ); @@ -1219,6 +1247,8 @@ 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_ManDupAndConesLimit( Gia_Man_t * p, int * pAnds, int nAnds, int Level ); +extern Gia_Man_t * Gia_ManDupAndConesLimit2( Gia_Man_t * p, int * pAnds, int nAnds, int Level ); 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 ); @@ -1247,6 +1277,7 @@ extern void Gia_ManOrigIdsInit( Gia_Man_t * p ); extern void Gia_ManOrigIdsStart( Gia_Man_t * p ); extern void Gia_ManOrigIdsRemap( Gia_Man_t * p, Gia_Man_t * pNew ); extern Gia_Man_t * Gia_ManOrigIdsReduce( Gia_Man_t * p, Vec_Int_t * vPairs ); +extern Gia_Man_t * Gia_ManComputeGiaEquivs( Gia_Man_t * pGia, int nConfs, int fVerbose ); extern void Gia_ManEquivFixOutputPairs( Gia_Man_t * p ); extern int Gia_ManCheckTopoOrder( Gia_Man_t * p ); extern int * Gia_ManDeriveNexts( Gia_Man_t * p ); @@ -1379,6 +1410,7 @@ extern int Gia_MmStepReadMemUsage( Gia_MmStep_t * p ); /*=== giaMf.c ===========================================================*/ extern void Mf_ManSetDefaultPars( Jf_Par_t * pPars ); extern Gia_Man_t * Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ); +extern void * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fMapping, int fVerbose ); /*=== giaMini.c ===========================================================*/ extern Gia_Man_t * Gia_ManReadMiniAig( char * pFileName ); extern void Gia_ManWriteMiniAig( Gia_Man_t * pGia, char * pFileName ); @@ -1403,7 +1435,7 @@ extern Gia_Man_t * Gia_ManCleanupOutputs( Gia_Man_t * p, int nOutputs ); extern Gia_Man_t * Gia_ManSeqCleanup( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManSeqStructSweep( Gia_Man_t * p, int fConst, int fEquiv, int fVerbose ); /*=== giaShow.c ===========================================================*/ -extern void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders ); +extern void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders, int fFadds, int fPath ); /*=== giaShrink.c ===========================================================*/ extern Gia_Man_t * Gia_ManMapShrink4( Gia_Man_t * p, int fKeepLevel, int fVerbose ); extern Gia_Man_t * Gia_ManMapShrink6( Gia_Man_t * p, int nFanoutMax, int fKeepLevel, int fVerbose ); @@ -1491,6 +1523,7 @@ extern int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimi extern word Gia_LutComputeTruth6( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTruths ); extern word Gia_ObjComputeTruthTable6Lut( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTemp ); extern word Gia_ObjComputeTruthTable6( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSupp, Vec_Wrd_t * vTruths ); +extern word Gia_ObjComputeTruth6Cis( Gia_Man_t * p, int iLit, Vec_Int_t * vSupp, Vec_Wrd_t * vTemp ); extern void Gia_ObjCollectInternal( Gia_Man_t * p, Gia_Obj_t * pObj ); extern word * Gia_ObjComputeTruthTable( Gia_Man_t * p, Gia_Obj_t * pObj ); extern void Gia_ObjComputeTruthTableStart( Gia_Man_t * p, int nVarsMax ); diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c index 3cf01c70..dfd4a467 100644 --- a/src/aig/gia/giaAig.c +++ b/src/aig/gia/giaAig.c @@ -22,6 +22,7 @@ #include "proof/fra/fra.h" #include "proof/dch/dch.h" #include "opt/dar/dar.h" +#include "opt/dau/dau.h" ABC_NAMESPACE_IMPL_START @@ -576,11 +577,17 @@ Gia_Man_t * Gia_ManCompress2( Gia_Man_t * p, int fUpdateLevel, int fVerbose ) ***********************************************************************/ Gia_Man_t * Gia_ManPerformDch( Gia_Man_t * p, void * pPars ) { - Gia_Man_t * pGia; + int fUseMapping = 0; + Gia_Man_t * pGia, * pGia1; Aig_Man_t * pNew; if ( p->pManTime && p->vLevels == NULL ) Gia_ManLevelWithBoxes( p ); - pNew = Gia_ManToAig( p, 0 ); + if ( fUseMapping && Gia_ManHasMapping(p) ) + pGia1 = (Gia_Man_t *)Dsm_ManDeriveGia( p, 0 ); + else + pGia1 = Gia_ManDup( p ); + pNew = Gia_ManToAig( pGia1, 0 ); + Gia_ManStop( pGia1 ); pNew = Dar_ManChoiceNew( pNew, (Dch_Pars_t *)pPars ); // pGia = Gia_ManFromAig( pNew ); pGia = Gia_ManFromAigChoices( pNew ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 7ced54a4..ee709df4 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -231,6 +231,80 @@ Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ +Gia_Man_t * Gia_ManDupAbs( Gia_Man_t * p, Vec_Int_t * vMapPpi2Ff, Vec_Int_t * vMapFf2Ppi ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int k, Flop, Used; + assert( Vec_IntSize(vMapFf2Ppi) == Vec_IntSize(vMapPpi2Ff) + Vec_IntCountEntry(vMapFf2Ppi, -1) ); + 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; + // create inputs + Gia_ManForEachPi( p, pObj, k ) + pObj->Value = Gia_ManAppendCi(pNew); + Vec_IntForEachEntry( vMapPpi2Ff, Flop, k ) + { + pObj = Gia_ManCi( p, Gia_ManPiNum(p) + Flop ); + pObj->Value = Gia_ManAppendCi(pNew); + } + Vec_IntForEachEntry( vMapFf2Ppi, Used, Flop ) + { + pObj = Gia_ManCi( p, Gia_ManPiNum(p) + Flop ); + if ( Used >= 0 ) + { + assert( pObj->Value != ~0 ); + continue; + } + assert( pObj->Value == ~0 ); + pObj->Value = Gia_ManAppendCi(pNew); + } + Gia_ManForEachCi( p, pObj, k ) + assert( pObj->Value != ~0 ); + // create nodes + Gia_ManForEachPo( p, pObj, k ) + Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(pObj) ); + Vec_IntForEachEntry( vMapFf2Ppi, Used, Flop ) + { + if ( Used >= 0 ) + continue; + pObj = Gia_ManCi( p, Gia_ManPiNum(p) + Flop ); + pObj = Gia_ObjRoToRi( p, pObj ); + Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(pObj) ); + } + // create outputs + Gia_ManForEachPo( p, pObj, k ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Vec_IntForEachEntry( vMapFf2Ppi, Used, Flop ) + { + if ( Used >= 0 ) + continue; + pObj = Gia_ManCi( p, Gia_ManPiNum(p) + Flop ); + pObj = Gia_ObjRoToRi( p, pObj ); + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + } + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) - Vec_IntSize(vMapPpi2Ff) ); + assert( Gia_ManPiNum(pNew) == Gia_ManPiNum(p) + Vec_IntSize(vMapPpi2Ff) ); + assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) ); + assert( Gia_ManPoNum(pNew) == Gia_ManPoNum(p) ); + assert( Gia_ManCoNum(pNew) == Gia_ManCoNum(p) - Vec_IntSize(vMapPpi2Ff) ); + return pNew; +} + + +/**Function************************************************************* + + Synopsis [Duplicates AIG while putting objects in the DFS order.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Gia_Man_t * Gia_ManDupOutputGroup( Gia_Man_t * p, int iOutStart, int iOutStop ) { Gia_Man_t * pNew; @@ -2097,6 +2171,43 @@ Gia_Man_t * Gia_ManDupDfsCiMap( Gia_Man_t * p, int * pCi2Lit, Vec_Int_t * vLits /**Function************************************************************* + Synopsis [Permute inputs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManPermuteInputs( Gia_Man_t * p, int nPpis, int nExtra ) +{ + Gia_Man_t * pNew; + Gia_Obj_t * pObj; + int i; + pNew = Gia_ManStart( Gia_ManObjNum(p) ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManConst0(p)->Value = 0; + for ( i = 0; i < Gia_ManPiNum(p) - nPpis - nExtra; i++ ) // regular PIs + Gia_ManCi(p, i)->Value = Gia_ManAppendCi( pNew ); + for ( i = Gia_ManPiNum(p) - nExtra; i < Gia_ManPiNum(p); i++ ) // extra PIs due to DC values + Gia_ManCi(p, i)->Value = Gia_ManAppendCi( pNew ); + for ( i = Gia_ManPiNum(p) - nPpis - nExtra; i < Gia_ManPiNum(p) - nExtra; i++ ) // pseudo-PIs + Gia_ManCi(p, i)->Value = Gia_ManAppendCi( pNew ); + for ( i = Gia_ManPiNum(p); i < Gia_ManCiNum(p); i++ ) // flop outputs + Gia_ManCi(p, i)->Value = Gia_ManAppendCi( pNew ); + assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) ); + Gia_ManForEachAnd( p, pObj, i ) + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + Gia_ManForEachCo( p, pObj, i ) + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) ); + return pNew; +} + +/**Function************************************************************* + Synopsis [Duplicates AIG in the DFS order.] Description [] @@ -3046,6 +3157,71 @@ Gia_Man_t * Gia_ManDupAndCones( Gia_Man_t * p, int * pAnds, int nAnds, int fTrim return pNew; } +void Gia_ManDupAndConesLimit_rec( Gia_Man_t * pNew, Gia_Man_t * p, int iObj, int Level ) +{ + Gia_Obj_t * pObj = Gia_ManObj(p, iObj); + if ( ~pObj->Value ) + return; + if ( !Gia_ObjIsAnd(pObj) || Gia_ObjLevel(p, pObj) < Level ) + { + pObj->Value = Gia_ManAppendCi( pNew ); + //printf( "PI %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj ); + return; + } + Gia_ManDupAndConesLimit_rec( pNew, p, Gia_ObjFaninId0(pObj, iObj), Level ); + Gia_ManDupAndConesLimit_rec( pNew, p, Gia_ObjFaninId1(pObj, iObj), Level ); + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + //printf( "Obj %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj ); +} +Gia_Man_t * Gia_ManDupAndConesLimit( Gia_Man_t * p, int * pAnds, int nAnds, int Level ) +{ + Gia_Man_t * pNew; + int i; + pNew = Gia_ManStart( 1000 ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManLevelNum( p ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + for ( i = 0; i < nAnds; i++ ) + Gia_ManDupAndConesLimit_rec( pNew, p, pAnds[i], Level ); + for ( i = 0; i < nAnds; i++ ) + Gia_ManAppendCo( pNew, Gia_ManObj(p, pAnds[i])->Value ); + return pNew; +} + +void Gia_ManDupAndConesLimit2_rec( Gia_Man_t * pNew, Gia_Man_t * p, int iObj, int Level ) +{ + Gia_Obj_t * pObj = Gia_ManObj(p, iObj); + if ( ~pObj->Value ) + return; + if ( !Gia_ObjIsAnd(pObj) || Level <= 0 ) + { + pObj->Value = Gia_ManAppendCi( pNew ); + //printf( "PI %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj ); + return; + } + Gia_ManDupAndConesLimit2_rec( pNew, p, Gia_ObjFaninId0(pObj, iObj), Level-1 ); + Gia_ManDupAndConesLimit2_rec( pNew, p, Gia_ObjFaninId1(pObj, iObj), Level-1 ); + pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); + //printf( "Obj %d for %d.\n", Abc_Lit2Var(pObj->Value), iObj ); +} +Gia_Man_t * Gia_ManDupAndConesLimit2( Gia_Man_t * p, int * pAnds, int nAnds, int Level ) +{ + Gia_Man_t * pNew; + int i; + pNew = Gia_ManStart( 1000 ); + pNew->pName = Abc_UtilStrsav( p->pName ); + pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + Gia_ManFillValue( p ); + Gia_ManConst0(p)->Value = 0; + for ( i = 0; i < nAnds; i++ ) + Gia_ManDupAndConesLimit2_rec( pNew, p, pAnds[i], Level ); + for ( i = 0; i < nAnds; i++ ) + Gia_ManAppendCo( pNew, Gia_ManObj(p, pAnds[i])->Value ); + return pNew; + +} /**Function************************************************************* @@ -3377,6 +3553,26 @@ Gia_Man_t * Gia_ManDupOuts( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ +Vec_Wec_t * Gia_ManCreateNodeSupps( Gia_Man_t * p, Vec_Int_t * vNodes, int fVerbose ) +{ + abctime clk = Abc_Clock(); + Gia_Obj_t * pObj; int i, Id; + Vec_Wec_t * vSuppsNo = Vec_WecStart( Vec_IntSize(vNodes) ); + Vec_Wec_t * vSupps = Vec_WecStart( Gia_ManObjNum(p) ); + Gia_ManForEachCiId( p, Id, i ) + Vec_IntPush( Vec_WecEntry(vSupps, Id), i ); + Gia_ManForEachAnd( p, pObj, Id ) + Vec_IntTwoMerge2( Vec_WecEntry(vSupps, Gia_ObjFaninId0(pObj, Id)), + Vec_WecEntry(vSupps, Gia_ObjFaninId1(pObj, Id)), + Vec_WecEntry(vSupps, Id) ); + Gia_ManForEachObjVec( vNodes, p, pObj, i ) + Vec_IntAppend( Vec_WecEntry(vSuppsNo, i), Vec_WecEntry(vSupps, Gia_ObjId(p, pObj)) ); + Vec_WecFree( vSupps ); + if ( fVerbose ) + Abc_PrintTime( 1, "Support computation", Abc_Clock() - clk ); + return vSuppsNo; +} + Vec_Wec_t * Gia_ManCreateCoSupps( Gia_Man_t * p, int fVerbose ) { abctime clk = Abc_Clock(); @@ -3690,6 +3886,81 @@ Gia_Man_t * Gia_ManDupDemiter( Gia_Man_t * p, int fVerbose ) SeeAlso [] ***********************************************************************/ +void Gia_ManDupDemiterOrderXors2( Gia_Man_t * p, Vec_Int_t * vXors ) +{ + int i, iObj, * pPerm; + Vec_Int_t * 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 ); +} +int Gia_ManDupDemiterFindMin( Vec_Wec_t * vSupps, Vec_Int_t * vTakenIns, Vec_Int_t * vTakenOuts ) +{ + Vec_Int_t * vLevel; + int i, k, iObj, iObjBest = -1; + int Count, CountBest = ABC_INFINITY; + Vec_WecForEachLevel( vSupps, vLevel, i ) + { + if ( Vec_IntEntry(vTakenOuts, i) ) + continue; + Count = 0; + Vec_IntForEachEntry( vLevel, iObj, k ) + Count += !Vec_IntEntry(vTakenIns, iObj); + if ( CountBest > Count ) + { + CountBest = Count; + iObjBest = i; + } + } + return iObjBest; +} +void Gia_ManDupDemiterOrderXors( Gia_Man_t * p, Vec_Int_t * vXors ) +{ + extern Vec_Wec_t * Gia_ManCreateNodeSupps( Gia_Man_t * p, Vec_Int_t * vNodes, int fVerbose ); + Vec_Wec_t * vSupps = Gia_ManCreateNodeSupps( p, vXors, 0 ); + Vec_Int_t * vTakenIns = Vec_IntStart( Gia_ManCiNum(p) ); + Vec_Int_t * vTakenOuts = Vec_IntStart( Vec_IntSize(vXors) ); + Vec_Int_t * vOrder = Vec_IntAlloc( Vec_IntSize(vXors) ); + int i, k, iObj; + // add outputs in the order of increasing supports + for ( i = 0; i < Vec_IntSize(vXors); i++ ) + { + int Index = Gia_ManDupDemiterFindMin( vSupps, vTakenIns, vTakenOuts ); + assert( Index >= 0 && Index < Vec_IntSize(vXors) ); + Vec_IntPush( vOrder, Vec_IntEntry(vXors, Index) ); + assert( !Vec_IntEntry( vTakenOuts, Index ) ); + Vec_IntWriteEntry( vTakenOuts, Index, 1 ); + Vec_IntForEachEntry( Vec_WecEntry(vSupps, Index), iObj, k ) + Vec_IntWriteEntry( vTakenIns, iObj, 1 ); + } + Vec_WecFree( vSupps ); + Vec_IntFree( vTakenIns ); + Vec_IntFree( vTakenOuts ); + // reload + Vec_IntClear( vXors ); + Vec_IntAppend( vXors, vOrder ); + Vec_IntFree( vOrder ); +} + + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ void Gia_ManSetMark0Dfs_rec( Gia_Man_t * p, int iObj ) { Gia_Obj_t * pObj; @@ -3781,27 +4052,26 @@ void Gia_ManCollectTopXors_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vXo } Vec_Int_t * Gia_ManCollectTopXors( Gia_Man_t * p ) { - int i, iObj, iObj2, fFlip, * pPerm, Count1 = 0; - Vec_Int_t * vXors, * vSizes, * vPart[2], * vOrder; + int i, iObj, iObj2, fFlip, Count1 = 0; + Vec_Int_t * vXors, * vPart[2], * vOrder; Gia_Obj_t * pFan[2], * pObj = Gia_ManCo(p, 0); - assert( Gia_ManCoNum(p) == 1 ); vXors = Vec_IntAlloc( 100 ); - if ( Gia_ObjFaninC0(pObj) ) - Gia_ManCollectTopXors_rec( p, Gia_ObjFanin0(pObj), vXors ); + if ( Gia_ManCoNum(p) == 1 ) + { + if ( Gia_ObjFaninC0(pObj) ) + Gia_ManCollectTopXors_rec( p, Gia_ObjFanin0(pObj), vXors ); + else + Vec_IntPush( vXors, Gia_ObjId(p, Gia_ObjFanin0(pObj)) ); + } else - Vec_IntPush( vXors, Gia_ObjId(p, Gia_ObjFanin0(pObj)) ); + { + Gia_ManForEachCo( p, pObj, i ) + if ( Gia_ObjFaninId0p(p, pObj) > 0 ) + Vec_IntPush( vXors, Gia_ObjFaninId0p(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 ); + Gia_ManDupDemiterOrderXors( p, vXors ); + //Vec_IntPrint( vXors ); Vec_IntReverseOrder( vXors ); // from MSB to LSB // divide into groups Gia_ManCleanMark01(p); diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c index 584be4cd..f41db898 100644 --- a/src/aig/gia/giaEquiv.c +++ b/src/aig/gia/giaEquiv.c @@ -129,7 +129,7 @@ Gia_Man_t * Gia_ManOrigIdsReduce( Gia_Man_t * p, Vec_Int_t * vPairs ) } Gia_ManHashStop( pNew ); Gia_ManForEachCo( p, pObj, i ) - Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); + pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) ); Vec_IntFree( vMap ); // compute equivalences assert( !p->pReprs && !p->pNexts ); @@ -171,6 +171,31 @@ Gia_Man_t * Gia_ManOrigIdsReduceTest( Gia_Man_t * p, Vec_Int_t * vPairs ) /**Function************************************************************* + Synopsis [Compute equivalence classes of nodes.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Gia_Man_t * Gia_ManComputeGiaEquivs( Gia_Man_t * pGia, int nConfs, int fVerbose ) +{ + Gia_Man_t * pTemp; + Cec_ParFra_t ParsFra, * pPars = &ParsFra; + Cec_ManFraSetDefaultParams( pPars ); + pPars->fUseOrigIds = 1; + pPars->fSatSweeping = 1; + pPars->nBTLimit = nConfs; + pPars->fVerbose = fVerbose; + pTemp = Cec_ManSatSweeping( pGia, pPars, 0 ); + Gia_ManStop( pTemp ); + return Gia_ManOrigIdsReduce( pGia, pGia->vIdsEquiv ); +} + +/**Function************************************************************* + Synopsis [Returns 1 if AIG is not in the required topo order.] Description [] @@ -460,7 +485,7 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem ) if ( fVerbose ) { // int Ent; - Abc_Print( 1, "Const0 = " ); + Abc_Print( 1, "Const0 (%d) = ", Counter0 ); Gia_ManForEachConst( p, i ) Abc_Print( 1, "%d ", i ); Abc_Print( 1, "\n" ); diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index 26f549d0..ab80a762 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -539,33 +539,25 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p, char * pDumpFile ) { sprintf( FileNameOld, "%s", p->pName ); fprintf( pTable, "\n" ); - fprintf( pTable, "%s ", p->pName ); -// fprintf( pTable, "%d ", Gia_ManCiNum(p) ); -// fprintf( pTable, "%d ", Gia_ManCoNum(p) ); -// fprintf( pTable, "%d ", Gia_ManAndNum(p) ); -// fprintf( pTable, "%d ", Gia_ManPiNum(p) - Gia_ManBoxCiNum(p) - Gia_ManRegBoxNum(p) ); -// fprintf( pTable, "%d ", Gia_ManPoNum(p) - Gia_ManBoxCoNum(p) - Gia_ManRegBoxNum(p) ); -// fprintf( pTable, "%d ", Gia_ManClockDomainNum(p) ); - + fprintf( pTable, "%s ", p->pName ); fprintf( pTable, " " ); - fprintf( pTable, "%d ", p->MappedDelay ); - fprintf( pTable, "%d ", p->MappedArea ); - fprintf( pTable, "%d ", nFanins ); - fprintf( pTable, "%d ", LevelMax ); + fprintf( pTable, "%d ", Gia_ManAndNum(p) ); fprintf( pTable, "%d ", nLuts ); -// fprintf( pTable, "%d ", Gia_ManRegBoxNum(p) ); -// fprintf( pTable, "%d ", Gia_ManNonRegBoxNum(p) ); + fprintf( pTable, "%d ", Gia_ManLutLevelWithBoxes(p) ); + //fprintf( pTable, "%d ", Gia_ManRegBoxNum(p) ); + //fprintf( pTable, "%d ", Gia_ManNonRegBoxNum(p) ); + //fprintf( pTable, "%.2f", 1.0*(Abc_Clock() - clk)/CLOCKS_PER_SEC ); clk = Abc_Clock(); } else { - printf( "This part of the code is currently not used.\n" ); - assert( 0 ); + //printf( "This part of the code is currently not used.\n" ); + //assert( 0 ); fprintf( pTable, " " ); fprintf( pTable, "%d ", nLuts ); - fprintf( pTable, "%d ", LevelMax ); - fprintf( pTable, "%d ", Gia_ManRegBoxNum(p) ); - fprintf( pTable, "%d ", Gia_ManNonRegBoxNum(p) ); + fprintf( pTable, "%d ", Gia_ManLutLevelWithBoxes(p) ); + //fprintf( pTable, "%d ", Gia_ManRegBoxNum(p) ); + //fprintf( pTable, "%d ", Gia_ManNonRegBoxNum(p) ); fprintf( pTable, "%.2f", 1.0*(Abc_Clock() - clk)/CLOCKS_PER_SEC ); clk = Abc_Clock(); } @@ -2014,7 +2006,7 @@ void Gia_ManMappingVerify( Gia_Man_t * p ) void Gia_ManTransferMapping( Gia_Man_t * p, Gia_Man_t * pGia ) { Gia_Obj_t * pObj; - int i, k, iFan; + int i, k, iFan, iPlace; if ( !Gia_ManHasMapping(pGia) ) return; Gia_ManMappingVerify( pGia ); @@ -2023,12 +2015,20 @@ void Gia_ManTransferMapping( Gia_Man_t * p, Gia_Man_t * pGia ) Vec_IntFill( p->vMapping, Gia_ManObjNum(p), 0 ); Gia_ManForEachLut( pGia, i ) { + if ( Gia_ObjValue(Gia_ManObj(pGia, i)) == ~0 ) // handle dangling LUT + continue; assert( !Abc_LitIsCompl(Gia_ObjValue(Gia_ManObj(pGia, i))) ); pObj = Gia_ManObj( p, Abc_Lit2Var(Gia_ObjValue(Gia_ManObj(pGia, i))) ); Vec_IntWriteEntry( p->vMapping, Gia_ObjId(p, pObj), Vec_IntSize(p->vMapping) ); + iPlace = Vec_IntSize( p->vMapping ); Vec_IntPush( p->vMapping, Gia_ObjLutSize(pGia, i) ); Gia_LutForEachFanin( pGia, i, iFan, k ) - Vec_IntPush( p->vMapping, Abc_Lit2Var(Gia_ObjValue(Gia_ManObj(pGia, iFan))) ); + { + if ( Gia_ObjValue(Gia_ManObj(pGia, iFan)) == ~0 ) // handle dangling LUT fanin + Vec_IntAddToEntry( p->vMapping, iPlace, -1 ); + else + Vec_IntPush( p->vMapping, Abc_Lit2Var(Gia_ObjValue(Gia_ManObj(pGia, iFan))) ); + } iFan = Abc_Lit2Var( Gia_ObjValue(Gia_ManObj(pGia, Abc_AbsInt(Gia_ObjLutMuxId(pGia, i)))) ); Vec_IntPush( p->vMapping, Gia_ObjLutIsMux(pGia, i) ? -iFan : iFan ); } diff --git a/src/aig/gia/giaJf.c b/src/aig/gia/giaJf.c index 93dac301..205ab408 100644 --- a/src/aig/gia/giaJf.c +++ b/src/aig/gia/giaJf.c @@ -36,6 +36,7 @@ ABC_NAMESPACE_IMPL_START #define JF_LEAF_MAX 8 #define JF_WORD_MAX ((JF_LEAF_MAX > 6) ? 1 << (JF_LEAF_MAX-6) : 1) #define JF_CUT_MAX 16 +#define JF_EPSILON 0.005 typedef struct Jf_Cut_t_ Jf_Cut_t; struct Jf_Cut_t_ @@ -940,15 +941,16 @@ float Jf_CutCompareDelay( Jf_Cut_t * pOld, Jf_Cut_t * pNew ) { if ( pOld->Time != pNew->Time ) return pOld->Time - pNew->Time; if ( pOld->pCut[0] != pNew->pCut[0] ) return pOld->pCut[0] - pNew->pCut[0]; - if ( pOld->Flow != pNew->Flow ) return pOld->Flow - pNew->Flow; +// if ( pOld->Flow != pNew->Flow ) return pOld->Flow - pNew->Flow; + if ( pOld->Flow < pNew->Flow - JF_EPSILON ) return -1; + if ( pOld->Flow > pNew->Flow + JF_EPSILON ) return 1; return 0; } float Jf_CutCompareArea( Jf_Cut_t * pOld, Jf_Cut_t * pNew ) { -// float Epsilon = (float)0.001; -// if ( pOld->Flow > pNew->Flow + Epsilon ) return 1; -// if ( pOld->Flow < pNew->Flow - Epsilon ) return -1; - if ( pOld->Flow != pNew->Flow ) return pOld->Flow - pNew->Flow; +// if ( pOld->Flow != pNew->Flow ) return pOld->Flow - pNew->Flow; + if ( pOld->Flow < pNew->Flow - JF_EPSILON ) return -1; + if ( pOld->Flow > pNew->Flow + JF_EPSILON ) return 1; if ( pOld->pCut[0] != pNew->pCut[0] ) return pOld->pCut[0] - pNew->pCut[0]; if ( pOld->Time != pNew->Time ) return pOld->Time - pNew->Time; return 0; @@ -1256,10 +1258,10 @@ void Jf_ManComputeCuts( Jf_Man_t * p, int fEdge ) } if ( p->pPars->fVerbose ) { - printf( "CutPair = %lu ", p->CutCount[0] ); - printf( "Merge = %lu ", p->CutCount[1] ); - printf( "Eval = %lu ", p->CutCount[2] ); - printf( "Cut = %lu ", p->CutCount[3] ); + printf( "CutPair = %lu ", (long)p->CutCount[0] ); + printf( "Merge = %lu ", (long)p->CutCount[1] ); + printf( "Eval = %lu ", (long)p->CutCount[2] ); + printf( "Cut = %lu ", (long)p->CutCount[3] ); Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart ); printf( "Memory: " ); printf( "Gia = %.2f MB ", Gia_ManMemory(p->pGia) / (1<<20) ); @@ -1367,7 +1369,7 @@ void Jf_ObjComputeBestCut( Jf_Man_t * p, Gia_Obj_t * pObj, int fEdge, int fEla ) if ( fEdge && !fEla ) Jf_CutSetCost(pCut, Jf_CutSize(pCut)); Area = fEla ? Jf_CutArea(p, pCut, fEdge) : Jf_CutFlow(p, pCut) + Jf_CutCost(pCut); - if ( pCutBest == NULL || AreaBest > Area || (AreaBest == Area && TimeBest > (Time = Jf_CutArr(p, pCut))) ) + if ( pCutBest == NULL || AreaBest > Area + JF_EPSILON || (AreaBest > Area - JF_EPSILON && TimeBest > (Time = Jf_CutArr(p, pCut))) ) pCutBest = pCut, AreaBest = Area, TimeBest = Time; } Vec_IntWriteEntry( &p->vArr, iObj, Jf_CutArr(p, pCutBest) ); @@ -1702,11 +1704,11 @@ void Jf_ManPrintStats( Jf_Man_t * p, char * pTitle ) if ( !p->pPars->fVerbose ) return; printf( "%s : ", pTitle ); - printf( "Level =%6lu ", p->pPars->Delay ); - printf( "Area =%9lu ", p->pPars->Area ); - printf( "Edge =%9lu ", p->pPars->Edge ); + printf( "Level =%6lu ", (long)p->pPars->Delay ); + printf( "Area =%9lu ", (long)p->pPars->Area ); + printf( "Edge =%9lu ", (long)p->pPars->Edge ); if ( p->pPars->fGenCnf ) - printf( "Cnf =%9lu ", p->pPars->Clause ); + printf( "Cnf =%9lu ", (long)p->pPars->Clause ); Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart ); fflush( stdout ); } diff --git a/src/aig/gia/giaKf.c b/src/aig/gia/giaKf.c index caa88bfc..a823f726 100644 --- a/src/aig/gia/giaKf.c +++ b/src/aig/gia/giaKf.c @@ -1125,9 +1125,9 @@ void Kf_ManPrintStats( Kf_Man_t * p, char * pTitle ) if ( !p->pPars->fVerbose ) return; printf( "%s : ", pTitle ); - printf( "Level =%6lu ", p->pPars->Delay ); - printf( "Area =%9lu ", p->pPars->Area ); - printf( "Edge =%9lu ", p->pPars->Edge ); + printf( "Level =%6lu ", (long)p->pPars->Delay ); + printf( "Area =%9lu ", (long)p->pPars->Area ); + printf( "Edge =%9lu ", (long)p->pPars->Edge ); Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart ); fflush( stdout ); } @@ -1173,10 +1173,10 @@ void Kf_ManComputeMapping( Kf_Man_t * p ) Kf_ManComputeRefs( p ); if ( p->pPars->fVerbose ) { - printf( "CutPair = %lu ", p->pSett->CutCount[0] ); - printf( "Merge = %lu ", p->pSett->CutCount[1] ); - printf( "Eval = %lu ", p->pSett->CutCount[2] ); - printf( "Cut = %lu ", p->pSett->CutCount[3] ); + printf( "CutPair = %lu ", (long)p->pSett->CutCount[0] ); + printf( "Merge = %lu ", (long)p->pSett->CutCount[1] ); + printf( "Eval = %lu ", (long)p->pSett->CutCount[2] ); + printf( "Cut = %lu ", (long)p->pSett->CutCount[3] ); Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart ); printf( "Memory: " ); printf( "Gia = %.2f MB ", Gia_ManMemory(p->pGia) / (1<<20) ); diff --git a/src/aig/gia/giaLf.c b/src/aig/gia/giaLf.c index 082b1928..2c216a9b 100644 --- a/src/aig/gia/giaLf.c +++ b/src/aig/gia/giaLf.c @@ -36,6 +36,7 @@ ABC_NAMESPACE_IMPL_START #define LF_NO_LEAF 255 #define LF_CUT_WORDS (4+LF_LEAF_MAX/2) #define LF_TT_WORDS ((LF_LEAF_MAX > 6) ? 1 << (LF_LEAF_MAX-6) : 1) +#define LF_EPSILON 0.005 typedef struct Lf_Cut_t_ Lf_Cut_t; struct Lf_Cut_t_ @@ -847,16 +848,16 @@ static inline int Lf_CutCompareDelay( Lf_Cut_t * pCut0, Lf_Cut_t * pCut1 ) if ( pCut0->Delay > pCut1->Delay ) return 1; if ( pCut0->nLeaves < pCut1->nLeaves ) return -1; if ( pCut0->nLeaves > pCut1->nLeaves ) return 1; - if ( pCut0->Flow < pCut1->Flow ) return -1; - if ( pCut0->Flow > pCut1->Flow ) return 1; + if ( pCut0->Flow < pCut1->Flow - LF_EPSILON ) return -1; + if ( pCut0->Flow > pCut1->Flow + LF_EPSILON ) return 1; return 0; } static inline int Lf_CutCompareArea( Lf_Cut_t * pCut0, Lf_Cut_t * pCut1 ) { if ( pCut0->fLate < pCut1->fLate ) return -1; if ( pCut0->fLate > pCut1->fLate ) return 1; - if ( pCut0->Flow < pCut1->Flow ) return -1; - if ( pCut0->Flow > pCut1->Flow ) return 1; + if ( pCut0->Flow < pCut1->Flow - LF_EPSILON ) return -1; + if ( pCut0->Flow > pCut1->Flow + LF_EPSILON ) return 1; if ( pCut0->Delay < pCut1->Delay ) return -1; if ( pCut0->Delay > pCut1->Delay ) return 1; if ( pCut0->nLeaves < pCut1->nLeaves ) return -1; @@ -1304,7 +1305,7 @@ void Lf_ObjMergeOrder( Lf_Man_t * p, int iObj ) p->nCutEqual++; // area cut iCutUsed = 0; - if ( nCutsR > 1 && pCutsR[0]->Flow > pCutsR[1]->Flow )//&& !pCutsR[1]->fLate ) // can remove !fLate + if ( nCutsR > 1 && pCutsR[0]->Flow > pCutsR[1]->Flow + LF_EPSILON )//&& !pCutsR[1]->fLate ) // can remove !fLate { pBest->Cut[1].Handle = Lf_MemSaveCut(&p->vStoreNew, pCutsR[1], iObj); pBest->Delay[1] = pCutsR[1]->Delay; @@ -2012,14 +2013,14 @@ void Lf_ManPrintStats( Lf_Man_t * p, char * pTitle ) if ( !p->pPars->fVerbose ) return; printf( "%s : ", pTitle ); - printf( "Level =%6lu ", p->pPars->Delay ); - printf( "Area =%9lu ", p->pPars->Area ); - printf( "Edge =%9lu ", p->pPars->Edge ); - printf( "LUT =%9lu ", p->pPars->Area+p->nInverters ); + printf( "Level =%6lu ", (long)p->pPars->Delay ); + printf( "Area =%9lu ", (long)p->pPars->Area ); + printf( "Edge =%9lu ", (long)p->pPars->Edge ); + printf( "LUT =%9lu ", (long)p->pPars->Area+p->nInverters ); if ( Vec_FltSize(&p->vSwitches) ) printf( "Swt =%8.1f ", p->Switches ); if ( p->pPars->fUseMux7 ) - printf( "Mux7 =%7lu ", p->pPars->Mux7 ); + printf( "Mux7 =%7lu ", (long)p->pPars->Mux7 ); Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart ); fflush( stdout ); } diff --git a/src/aig/gia/giaMf.c b/src/aig/gia/giaMf.c index 591f5bc5..24c1e6a0 100644 --- a/src/aig/gia/giaMf.c +++ b/src/aig/gia/giaMf.c @@ -37,6 +37,7 @@ ABC_NAMESPACE_IMPL_START #define MF_NO_LEAF 31 #define MF_TT_WORDS ((MF_LEAF_MAX > 6) ? 1 << (MF_LEAF_MAX-6) : 1) #define MF_NO_FUNC 134217727 // (1<<27)-1 +#define MF_EPSILON 0.005 typedef struct Mf_Cut_t_ Mf_Cut_t; struct Mf_Cut_t_ @@ -387,6 +388,8 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla ) Gia_ManForEachCoId( p->pGia, Id, i ) pCnf->pClauses[0][iLit++] = Abc_Var2Lit(pCnfIds[Id], 0); } + if ( p->pPars->fCnfMapping ) + pCnf->vMapping = Vec_IntStart( nVars ); // add clauses for the COs Gia_ManForEachCo( p->pGia, pObj, i ) { @@ -400,6 +403,14 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla ) pCnf->pClauses[iCla++] = pCnf->pClauses[0] + iLit; pCnf->pClauses[0][iLit++] = Abc_Var2Lit(pCnfIds[Id], 1); pCnf->pClauses[0][iLit++] = Abc_Var2Lit(pCnfIds[DriId], Gia_ObjFaninC0(pObj)); + // generate mapping + if ( pCnf->vMapping ) + { + Vec_IntWriteEntry( pCnf->vMapping, pCnfIds[Id], Vec_IntSize(pCnf->vMapping) ); + Vec_IntPush( pCnf->vMapping, 1 ); + Vec_IntPush( pCnf->vMapping, pCnfIds[DriId] ); + Vec_IntPush( pCnf->vMapping, Gia_ObjFaninC0(pObj) ? 0x55555555 : 0xAAAAAAAA ); + } } // add clauses for the mapping Gia_ManForEachAndReverseId( p->pGia, Id ) @@ -426,6 +437,35 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla ) if ( Mf_CubeLit(pCubes[c], k) ) pCnf->pClauses[0][iLit++] = Abc_Var2Lit( pFanins[k], Mf_CubeLit(pCubes[c], k) == 2 ); } + // generate mapping + if ( pCnf->vMapping ) + { + word pTruth[4], * pTruthP = Vec_MemReadEntry(p->vTtMem, iFunc); + assert( p->pPars->nLutSize <= 8 ); + Abc_TtCopy( pTruth, pTruthP, Abc_Truth6WordNum(p->pPars->nLutSize), Abc_LitIsCompl(iFunc) ); + assert( pCnfIds[Id] >= 0 && pCnfIds[Id] < nVars ); + Vec_IntWriteEntry( pCnf->vMapping, pCnfIds[Id], Vec_IntSize(pCnf->vMapping) ); + Vec_IntPush( pCnf->vMapping, Mf_CutSize(pCut) ); + for ( k = 0; k < Mf_CutSize(pCut); k++ ) + Vec_IntPush( pCnf->vMapping, pCnfIds[pCut[k+1]] ); + Vec_IntPush( pCnf->vMapping, (unsigned)pTruth[0] ); + if ( Mf_CutSize(pCut) >= 6 ) + { + Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[0] >> 32) ); + if ( Mf_CutSize(pCut) >= 7 ) + { + Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[1]) ); + Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[1] >> 32) ); + } + if ( Mf_CutSize(pCut) >= 8 ) + { + Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[2]) ); + Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[2] >> 32) ); + Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[3]) ); + Vec_IntPush( pCnf->vMapping, (unsigned)(pTruth[3] >> 32) ); + } + } + } } // constant clause pCnf->pClauses[iCla++] = pCnf->pClauses[0] + iLit; @@ -920,8 +960,8 @@ static inline int Mf_SetLastCutContainsArea( Mf_Cut_t ** pCuts, int nCuts ) } static inline int Mf_CutCompareArea( Mf_Cut_t * pCut0, Mf_Cut_t * pCut1 ) { - if ( pCut0->Flow < pCut1->Flow ) return -1; - if ( pCut0->Flow > pCut1->Flow ) return 1; + if ( pCut0->Flow < pCut1->Flow - MF_EPSILON ) return -1; + if ( pCut0->Flow > pCut1->Flow + MF_EPSILON ) return 1; if ( pCut0->Delay < pCut1->Delay ) return -1; if ( pCut0->Delay > pCut1->Delay ) return 1; if ( pCut0->nLeaves < pCut1->nLeaves ) return -1; @@ -1415,11 +1455,11 @@ void Mf_ManPrintStats( Mf_Man_t * p, char * pTitle ) if ( !p->pPars->fVerbose ) return; printf( "%s : ", pTitle ); - printf( "Level =%6lu ", p->pPars->Delay ); - printf( "Area =%9lu ", p->pPars->Area ); - printf( "Edge =%9lu ", p->pPars->Edge ); + printf( "Level =%6lu ", (long)p->pPars->Delay ); + printf( "Area =%9lu ", (long)p->pPars->Area ); + printf( "Edge =%9lu ", (long)p->pPars->Edge ); if ( p->pPars->fGenCnf ) - printf( "CNF =%9lu ", p->pPars->Clause ); + printf( "CNF =%9lu ", (long)p->pPars->Clause ); Abc_PrintTime( 1, "Time", Abc_Clock() - p->clkStart ); fflush( stdout ); } @@ -1544,7 +1584,7 @@ static inline void Mf_ObjComputeBestCut( Mf_Man_t * p, int iObj ) assert( !Mf_CutIsTriv(pCut, iObj) ); assert( Mf_CutSize(pCut) <= p->pPars->nLutSize ); Flow = p->fUseEla ? Mf_CutAreaDerefed(p, pCut) : Mf_CutFlow(p, pCut, &Time); - if ( pCutBest == NULL || FlowBest > Flow || (FlowBest == Flow && TimeBest > Time) ) + if ( pCutBest == NULL || FlowBest > Flow + MF_EPSILON || (FlowBest > Flow - MF_EPSILON && TimeBest > Time) ) pCutBest = pCut, FlowBest = Flow, TimeBest = Time; } assert( pCutBest != NULL ); @@ -1635,28 +1675,29 @@ Gia_Man_t * Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars ) SeeAlso [] ***********************************************************************/ -Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ) +void * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fMapping, int fVerbose ) { Gia_Man_t * pNew; Jf_Par_t Pars, * pPars = &Pars; assert( nLutSize >= 3 && nLutSize <= 8 ); Mf_ManSetDefaultPars( pPars ); - pPars->fGenCnf = 1; - pPars->fCoarsen = !fCnfObjIds; - pPars->nLutSize = nLutSize; - pPars->fCnfObjIds = fCnfObjIds; - pPars->fAddOrCla = fAddOrCla; - pPars->fVerbose = fVerbose; + pPars->fGenCnf = 1; + pPars->fCoarsen = !fCnfObjIds; + pPars->nLutSize = nLutSize; + pPars->fCnfObjIds = fCnfObjIds; + pPars->fAddOrCla = fAddOrCla; + pPars->fCnfMapping = fMapping; + pPars->fVerbose = fVerbose; pNew = Mf_ManPerformMapping( pGia, pPars ); Gia_ManStopP( &pNew ); // Cnf_DataPrint( (Cnf_Dat_t *)pGia->pData, 1 ); - return (Cnf_Dat_t*)pGia->pData; + return pGia->pData; } void Mf_ManDumpCnf( Gia_Man_t * p, char * pFileName, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ) { abctime clk = Abc_Clock(); Cnf_Dat_t * pCnf; - pCnf = Mf_ManGenerateCnf( p, nLutSize, fCnfObjIds, fAddOrCla, fVerbose ); + pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, nLutSize, fCnfObjIds, fAddOrCla, 0, fVerbose ); Cnf_DataWriteIntoFile( pCnf, pFileName, 0, NULL, NULL ); // if ( fVerbose ) { diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c index 3ff16978..3229e0d0 100644 --- a/src/aig/gia/giaMfs.c +++ b/src/aig/gia/giaMfs.c @@ -451,6 +451,7 @@ Gia_Man_t * Gia_ManPerformMfs( Gia_Man_t * p, Sfm_Par_t * pPars ) nNodes = Sfm_NtkPerform( pNtk, pPars ); if ( nNodes == 0 ) { + if ( p->pManTime ) Abc_Print( 1, "The network is not changed by \"&mfs\".\n" ); pNew = Gia_ManDup( p ); pNew->vMapping = Vec_IntDup( p->vMapping ); diff --git a/src/aig/gia/giaMini.c b/src/aig/gia/giaMini.c index a886311f..67805d44 100644 --- a/src/aig/gia/giaMini.c +++ b/src/aig/gia/giaMini.c @@ -21,6 +21,7 @@ #include "gia.h" #include "opt/dau/dau.h" #include "base/main/main.h" +#include "misc/util/utilTruth.h" #include "aig/miniaig/miniaig.h" #include "aig/miniaig/minilut.h" @@ -247,6 +248,34 @@ Gia_Man_t * Gia_ManFromMiniLut( Mini_Lut_t * p ) /**Function************************************************************* + Synopsis [Marks LUTs that should be complemented.] + + Description [These are LUTs whose all PO fanouts require them + in negative polarity. Other fanouts may require them in + positive polarity.] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Bit_t * Gia_ManFindComplLuts( Gia_Man_t * pGia ) +{ + Gia_Obj_t * pObj; int i; + // mark objects pointed by COs in negative polarity + Vec_Bit_t * vMarks = Vec_BitStart( Gia_ManObjNum(pGia) ); + Gia_ManForEachCo( pGia, pObj, i ) + if ( Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) && Gia_ObjFaninC0(pObj) ) + Vec_BitWriteEntry( vMarks, Gia_ObjFaninId0p(pGia, pObj), 1 ); + // unmark objects pointed by COs in positive polarity + Gia_ManForEachCo( pGia, pObj, i ) + if ( Gia_ObjIsAnd(Gia_ObjFanin0(pObj)) && !Gia_ObjFaninC0(pObj) ) + Vec_BitWriteEntry( vMarks, Gia_ObjFaninId0p(pGia, pObj), 0 ); + return vMarks; +} + +/**Function************************************************************* + Synopsis [Converts GIA into MiniLUT.] Description [] @@ -260,11 +289,13 @@ Mini_Lut_t * Gia_ManToMiniLut( Gia_Man_t * pGia ) { Mini_Lut_t * p; Vec_Wrd_t * vTruths; + Vec_Bit_t * vMarks; Gia_Obj_t * pObj, * pFanin; - int i, k, LutSize, pVars[16]; + int i, k, iFanin, LutSize, pVars[16]; word Truth; assert( Gia_ManHasMapping(pGia) ); LutSize = Gia_ManLutSizeMax( pGia ); + LutSize = Abc_MaxInt( LutSize, 2 ); assert( LutSize >= 2 ); // create the manager p = Mini_LutStart( LutSize ); @@ -274,12 +305,17 @@ Mini_Lut_t * Gia_ManToMiniLut( Gia_Man_t * pGia ) pObj->Value = Mini_LutCreatePi(p); // create internal nodes vTruths = Vec_WrdStart( Gia_ManObjNum(pGia) ); + vMarks = Gia_ManFindComplLuts( pGia ); Gia_ManForEachLut( pGia, i ) { pObj = Gia_ManObj( pGia, i ); Gia_LutForEachFaninObj( pGia, i, pFanin, k ) pVars[k] = pFanin->Value; Truth = Gia_LutComputeTruth6( pGia, i, vTruths ); + Truth = Vec_BitEntry(vMarks, i) ? ~Truth : Truth; + Gia_LutForEachFanin( pGia, i, iFanin, k ) + if ( Vec_BitEntry(vMarks, iFanin) ) + Truth = Abc_Tt6Flip( Truth, k ); pObj->Value = Mini_LutCreateNode( p, Gia_ObjLutSize(pGia, i), pVars, (unsigned *)&Truth ); } Vec_WrdFree( vTruths ); @@ -288,7 +324,7 @@ Mini_Lut_t * Gia_ManToMiniLut( Gia_Man_t * pGia ) { if ( Gia_ObjFanin0(pObj) == Gia_ManConst0(pGia) ) pObj->Value = Mini_LutCreatePo( p, Gia_ObjFaninC0(pObj) ); - else if ( !Gia_ObjFaninC0(pObj) ) + else if ( Gia_ObjFaninC0(pObj) == Vec_BitEntry(vMarks, Gia_ObjFaninId0p(pGia, pObj)) ) pObj->Value = Mini_LutCreatePo( p, Gia_ObjFanin0(pObj)->Value ); else // add inverter LUT { @@ -298,6 +334,7 @@ Mini_Lut_t * Gia_ManToMiniLut( Gia_Man_t * pGia ) pObj->Value = Mini_LutCreatePo( p, LutInv ); } } + Vec_BitFree( vMarks ); // set registers Mini_LutSetRegNum( p, Gia_ManRegNum(pGia) ); //Mini_LutPrintStats( p ); diff --git a/src/aig/gia/giaNf.c b/src/aig/gia/giaNf.c index 6761b617..6f1d0c8d 100644 --- a/src/aig/gia/giaNf.c +++ b/src/aig/gia/giaNf.c @@ -41,6 +41,7 @@ ABC_NAMESPACE_IMPL_START #define NF_CUT_MAX 32 #define NF_NO_LEAF 31 #define NF_NO_FUNC 0x3FFFFFF +#define NF_EPSILON 0.001 typedef struct Nf_Cut_t_ Nf_Cut_t; struct Nf_Cut_t_ @@ -171,7 +172,7 @@ static inline int Nf_CfgCompl( Nf_Cfg_t Cfg, int i ) int Nf_StoCellIsDominated( Mio_Cell2_t * pCell, int * pFans, int * pProf ) { int k; - if ( pCell->AreaF < Abc_Int2Float(pProf[0]) ) + if ( pCell->AreaF + NF_EPSILON < Abc_Int2Float(pProf[0]) ) return 0; for ( k = 0; k < (int)pCell->nFanins; k++ ) if ( pCell->iDelays[Abc_Lit2Var(pFans[k])] < pProf[k+1] ) @@ -802,8 +803,8 @@ static inline int Nf_CutCompareArea( Nf_Cut_t * pCut0, Nf_Cut_t * pCut1 ) { if ( pCut0->Useless < pCut1->Useless ) return -1; if ( pCut0->Useless > pCut1->Useless ) return 1; - if ( pCut0->Flow < pCut1->Flow ) return -1; - if ( pCut0->Flow > pCut1->Flow ) return 1; + if ( pCut0->Flow < pCut1->Flow - NF_EPSILON ) return -1; + if ( pCut0->Flow > pCut1->Flow + NF_EPSILON ) return 1; if ( pCut0->Delay < pCut1->Delay ) return -1; if ( pCut0->Delay > pCut1->Delay ) return 1; if ( pCut0->nLeaves < pCut1->nLeaves ) return -1; @@ -1162,7 +1163,7 @@ void Nf_ManCutMatchOne( Nf_Man_t * p, int iObj, int * pCut, int * pCutSet ) pD->Cfg.fCompl = 0; } - if ( pA->F > AreaF ) + if ( pA->F > AreaF + NF_EPSILON ) { pA->D = Delay; pA->F = AreaF; @@ -1310,7 +1311,7 @@ void Nf_ManCutMatch( Nf_Man_t * p, int iObj ) } //assert( pAp->F < FLT_MAX || pAn->F < FLT_MAX ); // try replacing pos with neg - if ( pAp->D == SCL_INFINITY || (pAp->F > pAn->F + p->InvAreaF && pAn->D + p->InvDelayI <= Required[0]) ) + if ( pAp->D == SCL_INFINITY || (pAp->F > pAn->F + p->InvAreaF + NF_EPSILON && pAn->D + p->InvDelayI <= Required[0]) ) { assert( p->Iter > 0 ); *pAp = *pAn; @@ -1322,7 +1323,7 @@ void Nf_ManCutMatch( Nf_Man_t * p, int iObj ) //printf( "Using inverter to improve area at node %d in phase %d.\n", iObj, 1 ); } // try replacing neg with pos - else if ( pAn->D == SCL_INFINITY || (pAn->F > pAp->F + p->InvAreaF && pAp->D + p->InvDelayI <= Required[1]) ) + else if ( pAn->D == SCL_INFINITY || (pAn->F > pAp->F + p->InvAreaF + NF_EPSILON && pAp->D + p->InvDelayI <= Required[1]) ) { assert( p->Iter > 0 ); *pAn = *pAp; @@ -1778,7 +1779,7 @@ void Nf_ManElaBestMatchOne( Nf_Man_t * p, int iObj, int c, int * pCut, int * pCu pMb->Cfg = Nf_Int2Cfg(0); pMb->fBest = 1; // compare - if ( pRes->F > pMb->F || (pRes->F == pMb->F && pRes->D > pMb->D) ) + if ( pRes->F > pMb->F + NF_EPSILON || (pRes->F > pMb->F - NF_EPSILON && pRes->D > pMb->D) ) *pRes = *pMb; return; } @@ -1814,7 +1815,7 @@ void Nf_ManElaBestMatchOne( Nf_Man_t * p, int iObj, int c, int * pCut, int * pCu // compute area pMb->F = Scl_Int2Flt((int)Nf_MatchRefArea(p, iObj, c, pMb, Required)); // compare - if ( pRes->F > pMb->F || (pRes->F == pMb->F && pRes->D > pMb->D) ) + if ( pRes->F > pMb->F + NF_EPSILON || (pRes->F > pMb->F - NF_EPSILON && pRes->D > pMb->D) ) *pRes = *pMb; } } diff --git a/src/aig/gia/giaQbf.c b/src/aig/gia/giaQbf.c index 4ca0bac3..2dfd83fc 100644 --- a/src/aig/gia/giaQbf.c +++ b/src/aig/gia/giaQbf.c @@ -48,8 +48,6 @@ struct Qbf_Man_t_ abctime clkSat; // SAT solver time }; -extern Cnf_Dat_t * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fAddOrCla, int fVerbose ); - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -192,7 +190,7 @@ int Gia_ManSatEnum( Gia_Man_t * pGia, int nConfLimit, int nTimeOut, int fVerbose int i, iLit, iParVarBeg, Iter; int nSolutions = 0, RetValue = 0; abctime clkStart = Abc_Clock(); - pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 ); + pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGia, 8, 0, 1, 0, 0 ); pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 ); iParVarBeg = pCnf->nVars - Gia_ManPiNum(pGia);// - 1; Cnf_DataFree( pCnf ); @@ -247,7 +245,7 @@ void Gia_QbfDumpFile( Gia_Man_t * pGia, int nPars ) { // original problem: \exists p \forall x \exists y. M(p,x,y) // negated problem: \forall p \exists x \exists y. !M(p,x,y) - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGia, 8, 0, 1, 0, 0 ); Vec_Int_t * vVarMap, * vForAlls, * vExists; Gia_Obj_t * pObj; char * pFileName; @@ -291,7 +289,7 @@ Qbf_Man_t * Gia_QbfAlloc( Gia_Man_t * pGia, int nPars, int fVerbose ) Qbf_Man_t * p; Cnf_Dat_t * pCnf; Gia_ObjFlipFaninC0( Gia_ManPo(pGia, 0) ); - pCnf = Mf_ManGenerateCnf( pGia, 8, 0, 1, 0 ); + pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pGia, 8, 0, 1, 0, 0 ); Gia_ObjFlipFaninC0( Gia_ManPo(pGia, 0) ); p = ABC_CALLOC( Qbf_Man_t, 1 ); p->clkStart = Abc_Clock(); @@ -426,7 +424,7 @@ Gia_Man_t * Gia_QbfCofactor( Gia_Man_t * p, int nPars, Vec_Int_t * vValues, Vec_ /* int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof ) { - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pCof, 8, 0, 1, 0 ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCof, 8, 0, 1, 0, 0 ); int i, iFirstVar = sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof);// - 1; pCnf->pMan = NULL; Cnf_DataLift( pCnf, sat_solver_nvars(p->pSatSyn) ); @@ -459,7 +457,7 @@ void Cnf_SpecialDataLift( Cnf_Dat_t * p, int nVarsPlus, int firstPiVar, int last int Gia_QbfAddCofactor( Qbf_Man_t * p, Gia_Man_t * pCof ) { - Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( pCof, 8, 0, 1, 0 ); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( pCof, 8, 0, 1, 0, 0 ); int i, useold = 0; int iFirstVar = useold ? sat_solver_nvars(p->pSatSyn) + pCnf->nVars - Gia_ManPiNum(pCof) : pCnf->nVars - Gia_ManPiNum(pCof); //-1 pCnf->pMan = NULL; diff --git a/src/aig/gia/giaSatoko.c b/src/aig/gia/giaSatoko.c new file mode 100644 index 00000000..5e04502d --- /dev/null +++ b/src/aig/gia/giaSatoko.c @@ -0,0 +1,205 @@ +/**CFile**************************************************************** + + FileName [giaSatoko.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Scalable AIG package.] + + Synopsis [Interface to Satoko solver.] + + Author [Alan Mishchenko, Bruno Schmitt] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - June 20, 2005.] + + Revision [$Id: giaSatoko.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "gia.h" +#include "sat/cnf/cnf.h" +#include "sat/satoko/satoko.h" +#include "sat/satoko/solver.h" + +ABC_NAMESPACE_IMPL_START + + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManCollectVars_rec( int Var, Vec_Int_t * vMapping, Vec_Int_t * vRes, Vec_Bit_t * vVisit ) +{ + int * pCut, i; + if ( Vec_BitEntry(vVisit, Var) ) + return; + Vec_BitWriteEntry(vVisit, Var, 1); + if ( Vec_IntEntry(vMapping, Var) ) // primary input or constant 0 + { + pCut = Vec_IntEntryP( vMapping, Vec_IntEntry(vMapping, Var) ); + for ( i = 1; i <= pCut[0]; i++ ) + Gia_ManCollectVars_rec( pCut[i], vMapping, vRes, vVisit ); + } + Vec_IntPush( vRes, Var ); +} +Vec_Int_t * Gia_ManCollectVars( int Root, Vec_Int_t * vMapping, int nVars ) +{ + Vec_Int_t * vRes = Vec_IntAlloc( 100 ); + Vec_Bit_t * vVisit = Vec_BitStart( nVars ); + assert( Vec_IntEntry(vMapping, Root) ); + Gia_ManCollectVars_rec( Root, vMapping, vRes, vVisit ); + Vec_BitFree( vVisit ); + return vRes; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +satoko_t * Gia_ManSatokoInit( Cnf_Dat_t * pCnf, satoko_opts_t * opts ) +{ + satoko_t * pSat = satoko_create(); + int i; + //sat_solver_setnvars( pSat, p->nVars ); + for ( i = 0; i < pCnf->nClauses; i++ ) + { + if ( !satoko_add_clause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1]-pCnf->pClauses[i] ) ) + { + satoko_destroy( pSat ); + return NULL; + } + } + satoko_configure(pSat, opts); + return pSat; +} +void Gia_ManSatokoReport( int iOutput, int status, abctime clk ) +{ + if ( iOutput >= 0 ) + Abc_Print( 1, "Output %6d : ", iOutput ); + else + Abc_Print( 1, "Total: " ); + + if ( status == SATOKO_UNDEC ) + Abc_Print( 1, "UNDECIDED " ); + else if ( status == SATOKO_SAT ) + Abc_Print( 1, "SATISFIABLE " ); + else + Abc_Print( 1, "UNSATISFIABLE " ); + + Abc_PrintTime( 1, "Time", clk ); +} +satoko_t * Gia_ManSatokoCreate( Gia_Man_t * p, satoko_opts_t * opts ) +{ + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 1, 0, 0 ); + satoko_t * pSat = Gia_ManSatokoInit( pCnf, opts ); + int status = pSat ? satoko_simplify(pSat) : SATOKO_OK; + Cnf_DataFree( pCnf ); + if ( status == SATOKO_OK ) + return pSat; + satoko_destroy( pSat ); + return NULL; +} +int Gia_ManSatokoCallOne( Gia_Man_t * p, satoko_opts_t * opts, int iOutput ) +{ + abctime clk = Abc_Clock(); + satoko_t * pSat; + int status, Cost = 0; + + pSat = Gia_ManSatokoCreate( p, opts ); + if ( pSat ) + { + status = satoko_solve( pSat ); + Cost = (unsigned)pSat->stats.n_conflicts; + satoko_destroy( pSat ); + } + else + status = SATOKO_UNSAT; + + Gia_ManSatokoReport( iOutput, status, Abc_Clock() - clk ); + return Cost; +} +void Gia_ManSatokoCall( Gia_Man_t * p, satoko_opts_t * opts, int fSplit, int fIncrem ) +{ + int fUseCone = 1; + Gia_Man_t * pOne; + Gia_Obj_t * pRoot; + Vec_Int_t * vCone; + int i, iLit, status; + if ( fIncrem ) + { + abctime clk = Abc_Clock(); + Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8, 0, 0, fUseCone, 0 ); + satoko_t * pSat = Gia_ManSatokoInit( pCnf, opts ); + Gia_ManForEachCo( p, pRoot, i ) + { + abctime clk = Abc_Clock(); + iLit = Abc_Var2Lit( i+1, 0 ); + satoko_assump_push( pSat, iLit ); + if ( fUseCone ) + { + vCone = Gia_ManCollectVars( i+1, pCnf->vMapping, pCnf->nVars ); + satoko_mark_cone( pSat, Vec_IntArray(vCone), Vec_IntSize(vCone) ); + printf( "Cone has %6d vars (out of %6d). ", Vec_IntSize(vCone), pCnf->nVars ); + status = satoko_solve( pSat ); + satoko_unmark_cone( pSat, Vec_IntArray(vCone), Vec_IntSize(vCone) ); + Vec_IntFree( vCone ); + } + else + { + status = satoko_solve( pSat ); + } + satoko_assump_pop( pSat ); + Gia_ManSatokoReport( i, status, Abc_Clock() - clk ); + } + Cnf_DataFree( pCnf ); + satoko_destroy( pSat ); + Abc_PrintTime( 1, "Total time", Abc_Clock() - clk ); + return; + } + if ( fSplit ) + { + abctime clk = Abc_Clock(); + Gia_ManForEachCo( p, pRoot, i ) + { + pOne = Gia_ManDupDfsCone( p, pRoot ); + Gia_ManSatokoCallOne( pOne, opts, i ); + Gia_ManStop( pOne ); + } + Abc_PrintTime( 1, "Total time", Abc_Clock() - clk ); + return; + } + Gia_ManSatokoCallOne( p, opts, -1 ); +} + + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/aig/gia/giaShow.c b/src/aig/gia/giaShow.c index 872ba6ec..3ca31d55 100644 --- a/src/aig/gia/giaShow.c +++ b/src/aig/gia/giaShow.c @@ -21,6 +21,7 @@ #include "gia.h" #include "proof/cec/cec.h" #include "proof/acec/acec.h" +#include "misc/extra/extra.h" ABC_NAMESPACE_IMPL_START @@ -29,155 +30,300 @@ ABC_NAMESPACE_IMPL_START /// DECLARATIONS /// //////////////////////////////////////////////////////////////////////// +#define NODE_MAX 2000 + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// /**Function************************************************************* - Synopsis [] + Synopsis [Writes the graph structure of AIG for DOT.] - Description [] + Description [Useful for graph visualization using tools such as GraphViz: + http://www.graphviz.org/] SideEffects [] SeeAlso [] ***********************************************************************/ -/* -Vec_Int_t * Gia_WriteDotAigMarks( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds ) +void Gia_ShowPath( Gia_Man_t * p, char * pFileName ) { - int i; - Vec_Int_t * vMarks = Vec_IntStart( Gia_ManObjNum(p) ); - for ( i = 0; i < Vec_IntSize(vHadds)/2; i++ ) + FILE * pFile; + Gia_Obj_t * pNode; + Vec_Bit_t * vPath = Vec_BitStart( Gia_ManObjNum(p) ); + int i, k, iFan, LevelMax, nLevels, * pLevels, Level, Prev; + int nLuts = 0, nNodes = 0, nEdges = 0; + assert( Gia_ManHasMapping(p) ); + + // set critical CO drivers + nLevels = Gia_ManLutLevel( p, &pLevels ); + Gia_ManForEachCoDriverId( p, iFan, i ) + if ( pLevels[iFan] == nLevels ) + Vec_BitWriteEntry( vPath, iFan, 1 ); + + // set critical internal nodes + Gia_ManForEachLutReverse( p, i ) + { + nLuts++; + if ( !Vec_BitEntry(vPath, i) ) + continue; + nNodes++; + Gia_LutForEachFanin( p, i, iFan, k ) + { + if ( pLevels[iFan] +1 < pLevels[i] ) + continue; + assert( pLevels[iFan] + 1 == pLevels[i] ); + Vec_BitWriteEntry( vPath, iFan, 1 ); + nEdges++; + //printf( "%d -> %d\n", i, iFan ); + } + } + + if ( nNodes > NODE_MAX ) { - Vec_IntWriteEntry( vMarks, Vec_IntEntry(vHadds, 2*i+0), Abc_Var2Lit(i+1, 0) ); - Vec_IntWriteEntry( vMarks, Vec_IntEntry(vHadds, 2*i+1), Abc_Var2Lit(i+1, 0) ); + ABC_FREE( pLevels ); + Vec_BitFree( vPath ); + fprintf( stdout, "Cannot visualize AIG with more than %d critical nodes.\n", NODE_MAX ); + return; } - for ( i = 0; i < Vec_IntSize(vFadds)/5; i++ ) + if ( (pFile = fopen( pFileName, "w" )) == NULL ) { - Vec_IntWriteEntry( vMarks, Vec_IntEntry(vFadds, 5*i+3), Abc_Var2Lit(i+1, 1) ); - Vec_IntWriteEntry( vMarks, Vec_IntEntry(vFadds, 5*i+4), Abc_Var2Lit(i+1, 1) ); + ABC_FREE( pLevels ); + Vec_BitFree( vPath ); + fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName ); + return; } - return vMarks; -} -int Gia_WriteDotAigLevel_rec( Gia_Man_t * p, Vec_Int_t * vMarks, Vec_Int_t * vFadds, Vec_Int_t * vHadds, int Id, Vec_Int_t * vLevel ) -{ - int Level = Vec_IntEntry(vLevel, Id), Mark = Vec_IntEntry(vMarks, Id); - if ( Level || Mark == -1 ) - return Level; - if ( Mark == 0 ) - { - Gia_Obj_t * pObj = Gia_ManObj( p, Id ); - int Level0 = Gia_WriteDotAigLevel_rec( p, vMarks, vFadds, vHadds, Gia_ObjFaninId0(pObj, Id), vLevel ); - int Level1 = Gia_WriteDotAigLevel_rec( p, vMarks, vFadds, vHadds, Gia_ObjFaninId1(pObj, Id), vLevel ); - Level = Abc_MaxInt(Level0, Level1) + 1; - Vec_IntWriteEntry( vLevel, Id, Level ); - Vec_IntWriteEntry( vMarks, Id, -1 ); - } - else if ( Abc_LitIsCompl(Mark) ) // FA - { - int i, * pFanins = Vec_IntEntryP( vFadds, 5*(Abc_Lit2Var(Mark)-1) ); - assert( pFanins[3] == Id || pFanins[4] == Id ); - for ( i = 0; i < 3; i++ ) - Level = Abc_MaxInt( Level, Gia_WriteDotAigLevel_rec( p, vMarks, vFadds, vHadds, pFanins[i], vLevel ) ); - Vec_IntWriteEntry( vLevel, pFanins[3], Level+1 ); - Vec_IntWriteEntry( vLevel, pFanins[4], Level+1 ); - } - else // HA - { - int * pFanins = Vec_IntEntryP( vHadds, 2*(Abc_Lit2Var(Mark)-1) ); - Gia_Obj_t * pObj = Gia_ManObj( p, pFanins[1] ); - int Level0 = Gia_WriteDotAigLevel_rec( p, vMarks, vFadds, vHadds, Gia_ObjFaninId0(pObj, Id), vLevel ); - int Level1 = Gia_WriteDotAigLevel_rec( p, vMarks, vFadds, vHadds, Gia_ObjFaninId1(pObj, Id), vLevel ); - assert( pFanins[0] == Id || pFanins[1] == Id ); - Level = Abc_MaxInt(Level0, Level1) + 1; - Vec_IntWriteEntry( vLevel, pFanins[0], Level ); - Vec_IntWriteEntry( vLevel, pFanins[1], Level ); + + Vec_IntFreeP( &p->vLevels ); + p->vLevels = Vec_IntAllocArray( pLevels, Gia_ManObjNum(p) ); + + // compute CO levels + LevelMax = 1 + nLevels; + Gia_ManForEachCo( p, pNode, i ) + Vec_IntWriteEntry( p->vLevels, Gia_ObjId(p, pNode), LevelMax ); + + // write the DOT header + fprintf( pFile, "# %s\n", "AIG structure generated by GIA package" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "digraph AIG {\n" ); + fprintf( pFile, "size = \"7.5,10\";\n" ); +// fprintf( pFile, "ranksep = 0.5;\n" ); +// fprintf( pFile, "nodesep = 0.5;\n" ); + fprintf( pFile, "center = true;\n" ); +// fprintf( pFile, "orientation = landscape;\n" ); +// fprintf( pFile, "edge [fontsize = 10];\n" ); +// fprintf( pFile, "edge [dir = none];\n" ); + fprintf( pFile, "edge [dir = back];\n" ); + fprintf( pFile, "\n" ); + + // labels on the left of the picture + fprintf( pFile, "{\n" ); + fprintf( pFile, " node [shape = plaintext];\n" ); + fprintf( pFile, " edge [style = invis];\n" ); + fprintf( pFile, " LevelTitle1 [label=\"\"];\n" ); + fprintf( pFile, " LevelTitle2 [label=\"\"];\n" ); + // generate node names with labels + for ( Level = LevelMax; Level >= 0; Level-- ) + { + // the visible node name + fprintf( pFile, " Level%d", Level ); + fprintf( pFile, " [label = " ); + // label name + fprintf( pFile, "\"" ); + fprintf( pFile, "\"" ); + fprintf( pFile, "];\n" ); } - return Level; -} -int Gia_WriteDotAigLevel( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds, Vec_Int_t ** pvMarks, Vec_Int_t ** pvLevel ) -{ - Vec_Int_t * vMarks = Gia_WriteDotAigMarks( p, vFadds, vHadds ); - Vec_Int_t * vLevel = Vec_IntStart( Gia_ManObjNum(p) ); - int i, Id, Level = 0; - Vec_IntWriteEntry( vMarks, 0, -1 ); - Gia_ManForEachCiId( p, Id, i ) - Vec_IntWriteEntry( vMarks, Id, -1 ); - Gia_ManForEachCoDriverId( p, Id, i ) - Level = Abc_MaxInt( Level, Gia_WriteDotAigLevel_rec(p, vMarks, vFadds, vHadds, Id, vLevel) ); - Gia_ManForEachCoId( p, Id, i ) - Vec_IntWriteEntry( vMarks, Id, -1 ); - *pvMarks = vMarks; - *pvLevel = vLevel; - return Level; -} -*/ -int Gia_WriteDotAigLevel( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds, Vec_Int_t * vRecord, Vec_Int_t ** pvLevel, Vec_Int_t ** pvMarks, Vec_Int_t ** pvRemap, Vec_Int_t ** pvRemap2 ) -{ - Vec_Int_t * vLevel = Vec_IntStart( Gia_ManObjNum(p) ); - Vec_Int_t * vMarks = Vec_IntStart( Gia_ManObjNum(p) ); - Vec_Int_t * vRemap = Vec_IntStartNatural( Gia_ManObjNum(p) ); - Vec_Int_t * vRemap2 = Vec_IntStartNatural( Gia_ManObjNum(p) ); - int i, k, Id, Entry, LevelMax = 0; - - Vec_IntWriteEntry( vMarks, 0, -1 ); - Gia_ManForEachCiId( p, Id, i ) - Vec_IntWriteEntry( vMarks, Id, -1 ); - Gia_ManForEachCoId( p, Id, i ) - Vec_IntWriteEntry( vMarks, Id, -1 ); - - Vec_IntForEachEntry( vRecord, Entry, i ) - { - int Level = 0; - int Node = Abc_Lit2Var2(Entry); - int Attr = Abc_Lit2Att2(Entry); - if ( Attr == 2 ) + + // genetate the sequence of visible/invisible nodes to mark levels + fprintf( pFile, " LevelTitle1 -> LevelTitle2 ->" ); + for ( Level = LevelMax; Level >= 0; Level-- ) + { + // the visible node name + fprintf( pFile, " Level%d", Level ); + // the connector + if ( Level != 0 ) + fprintf( pFile, " ->" ); + else + fprintf( pFile, ";" ); + } + fprintf( pFile, "\n" ); + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate title box on top + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + fprintf( pFile, " LevelTitle1;\n" ); + fprintf( pFile, " title1 [shape=plaintext,\n" ); + fprintf( pFile, " fontsize=20,\n" ); + fprintf( pFile, " fontname = \"Times-Roman\",\n" ); + fprintf( pFile, " label=\"" ); + fprintf( pFile, "%s", "AIG structure visualized by ABC" ); + fprintf( pFile, "\\n" ); + fprintf( pFile, "Benchmark \\\"%s\\\". ", "aig" ); +// fprintf( pFile, "Time was %s. ", Extra_TimeStamp() ); + fprintf( pFile, "\"\n" ); + fprintf( pFile, " ];\n" ); + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate statistics box + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + fprintf( pFile, " LevelTitle2;\n" ); + fprintf( pFile, " title2 [shape=plaintext,\n" ); + fprintf( pFile, " fontsize=18,\n" ); + fprintf( pFile, " fontname = \"Times-Roman\",\n" ); + fprintf( pFile, " label=\"" ); + fprintf( pFile, "The critical path contains %d LUTs with %d critical edges and spans %d levels.", nNodes, nEdges, nLevels ); + fprintf( pFile, "\\n" ); + fprintf( pFile, "\"\n" ); + fprintf( pFile, " ];\n" ); + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate the COs + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + // the labeling node of this level + fprintf( pFile, " Level%d;\n", LevelMax ); + // generate the CO nodes + Gia_ManForEachCo( p, pNode, i ) + { + if ( Gia_ObjLevel(p, Gia_ObjFanin0(pNode)) < nLevels ) + continue; + assert( Gia_ObjLevel(p, Gia_ObjFanin0(pNode)) == nLevels ); + fprintf( pFile, " Node%d [label = \"%d\"", Gia_ObjId(p, pNode), Gia_ObjId(p, pNode) ); + fprintf( pFile, ", shape = %s", "invtriangle" ); + fprintf( pFile, ", color = coral, fillcolor = coral" ); + fprintf( pFile, "];\n" ); + } + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate nodes of each rank + for ( Level = LevelMax - 1; Level > 0; Level-- ) + { + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + // the labeling node of this level + fprintf( pFile, " Level%d;\n", Level ); + Gia_ManForEachObj( p, pNode, i ) { - int * pFanins = Vec_IntEntryP( vFadds, 5*Node ); - for ( k = 0; k < 3; k++ ) - Level = Abc_MaxInt( Level, Vec_IntEntry(vLevel, pFanins[k]) ); - Vec_IntWriteEntry( vLevel, pFanins[3], Level+1 ); - Vec_IntWriteEntry( vLevel, pFanins[4], Level+1 ); - Vec_IntWriteEntry( vMarks, pFanins[4], Entry ); - Vec_IntWriteEntry( vRemap, pFanins[3], pFanins[4] ); - Vec_IntWriteEntry( vRemap2, pFanins[4], pFanins[3] ); - //printf( "Making FA output %d.\n", pFanins[4] ); + if ( (int)Gia_ObjLevel(p, pNode) != Level || !Vec_BitEntry(vPath, i) ) + continue; + fprintf( pFile, " Node%d [label = \"%d:%d\"", i, i, Gia_ObjIsAnd(pNode)? Gia_ObjLutSize(p, i) : 0 ); + fprintf( pFile, ", shape = ellipse" ); + if ( pNode->fMark0 ) + fprintf( pFile, ", style = filled" ); + fprintf( pFile, "];\n" ); } - else if ( Attr == 1 ) + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + } + + // generate the CI nodes + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + // the labeling node of this level + fprintf( pFile, " Level%d;\n", 0 ); + // generate the CI nodes + Gia_ManForEachCi( p, pNode, i ) + { + if ( !Vec_BitEntry(vPath, Gia_ObjId(p, pNode)) ) + continue; + fprintf( pFile, " Node%d [label = \"%d\"", Gia_ObjId(p, pNode), Gia_ObjId(p, pNode) ); + fprintf( pFile, ", shape = %s", "triangle" ); + fprintf( pFile, ", color = coral, fillcolor = coral" ); + fprintf( pFile, "];\n" ); + } + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate invisible edges from the square down + fprintf( pFile, "title1 -> title2 [style = invis];\n" ); + Gia_ManForEachCo( p, pNode, i ) + { + if ( Gia_ObjLevel(p, Gia_ObjFanin0(pNode)) < nLevels ) + continue; + fprintf( pFile, "title2 -> Node%d [style = invis];\n", Gia_ObjId(p, pNode) ); + } + // generate invisible edges among the COs + Prev = -1; + Gia_ManForEachCo( p, pNode, i ) + { + if ( Gia_ObjLevel(p, Gia_ObjFanin0(pNode)) < nLevels ) + continue; + assert( Gia_ObjLevel(p, Gia_ObjFanin0(pNode)) == nLevels ); + if ( Prev >= 0 ) + fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, Gia_ObjId(p, pNode) ); + Prev = Gia_ObjId(p, pNode); + } + // generate invisible edges among the CIs + Prev = -1; + Gia_ManForEachCi( p, pNode, i ) + { + if ( !Vec_BitEntry(vPath, Gia_ObjId(p, pNode)) ) + continue; + if ( Prev >= 0 ) + fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, Gia_ObjId(p, pNode) ); + Prev = Gia_ObjId(p, pNode); + } + + // generate edges + Gia_ManForEachObj( p, pNode, i ) + { + if ( Gia_ObjIsCo(pNode) ) { - int * pFanins = Vec_IntEntryP( vHadds, 2*Node ); - Gia_Obj_t * pObj = Gia_ManObj( p, pFanins[1] ); - int pFaninsIn[2] = { Gia_ObjFaninId0(pObj, pFanins[1]), Gia_ObjFaninId1(pObj, pFanins[1]) }; - for ( k = 0; k < 2; k++ ) - Level = Abc_MaxInt( Level, Vec_IntEntry(vLevel, pFaninsIn[k]) ); - Vec_IntWriteEntry( vLevel, pFanins[0], Level+1 ); - Vec_IntWriteEntry( vLevel, pFanins[1], Level+1 ); - Vec_IntWriteEntry( vMarks, pFanins[1], Entry ); - Vec_IntWriteEntry( vRemap, pFanins[0], pFanins[1] ); - Vec_IntWriteEntry( vRemap2, pFanins[1], pFanins[0] ); - //printf( "Making HA output %d %d.\n", pFanins[0], pFanins[1] ); + if ( Gia_ObjLevel(p, Gia_ObjFanin0(pNode)) == nLevels ) + { + // generate the edge from this node to the next + fprintf( pFile, "Node%d", i ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d", Gia_ObjFaninId0p(p, pNode) ); + fprintf( pFile, " [" ); + fprintf( pFile, "style = %s", "solid" ); + fprintf( pFile, "]" ); + fprintf( pFile, ";\n" ); + } + continue; } - else // if ( Attr == 3 || Attr == 0 ) + if ( !Gia_ObjIsAnd(pNode) || !Vec_BitEntry(vPath, i) ) + continue; + Gia_LutForEachFanin( p, i, iFan, k ) { - Gia_Obj_t * pObj = Gia_ManObj( p, Node ); - int pFaninsIn[2] = { Gia_ObjFaninId0(pObj, Node), Gia_ObjFaninId1(pObj, Node) }; - for ( k = 0; k < 2; k++ ) - Level = Abc_MaxInt( Level, Vec_IntEntry(vLevel, pFaninsIn[k]) ); - Vec_IntWriteEntry( vLevel, Node, Level+1 ); - Vec_IntWriteEntry( vMarks, Node, -1 ); - //printf( "Making node %d.\n", Node ); + if ( pLevels[iFan] + 1 < pLevels[i] ) + continue; + assert( pLevels[iFan] + 1 == pLevels[i] ); + // generate the edge from this node to the next + fprintf( pFile, "Node%d", i ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d", iFan ); + fprintf( pFile, " [" ); + fprintf( pFile, "style = %s", "solid" ); + fprintf( pFile, "]" ); + fprintf( pFile, ";\n" ); } - LevelMax = Abc_MaxInt( LevelMax, Level+1 ); } - *pvLevel = vLevel; - *pvMarks = vMarks; - *pvRemap = vRemap; - *pvRemap2 = vRemap2; - return LevelMax; + + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + fclose( pFile ); + + Vec_IntFreeP( &p->vLevels ); + Vec_BitFree( vPath ); } + /**Function************************************************************* Synopsis [Writes the graph structure of AIG for DOT.] @@ -190,17 +336,16 @@ int Gia_WriteDotAigLevel( Gia_Man_t * p, Vec_Int_t * vFadds, Vec_Int_t * vHadds, SeeAlso [] ***********************************************************************/ -void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int fAdders ) +void Gia_WriteDotAigSimple( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold ) { - Vec_Int_t * vFadds = NULL, * vHadds = NULL, * vRecord = NULL, * vMarks = NULL, * vRemap = NULL, * vRemap2 = NULL; FILE * pFile; Gia_Obj_t * pNode;//, * pTemp, * pPrev; int LevelMax, Prev, Level, i; int fConstIsUsed = 0; - if ( Gia_ManAndNum(pMan) > 1000 ) + if ( Gia_ManAndNum(p) > NODE_MAX ) { - fprintf( stdout, "Cannot visualize AIG with more than 1000 nodes.\n" ); + fprintf( stdout, "Cannot visualize AIG with more than %d nodes.\n", NODE_MAX ); return; } if ( (pFile = fopen( pFileName, "w" )) == NULL ) @@ -211,31 +356,20 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int // mark the nodes if ( vBold ) - Gia_ManForEachObjVec( vBold, pMan, pNode, i ) + Gia_ManForEachObjVec( vBold, p, pNode, i ) pNode->fMark0 = 1; - else if ( pMan->nXors || pMan->nMuxes ) - Gia_ManForEachObj( pMan, pNode, i ) - if ( Gia_ObjIsXor(pNode) || Gia_ObjIsMux(pMan, pNode) ) + else if ( p->nXors || p->nMuxes ) + Gia_ManForEachObj( p, pNode, i ) + if ( Gia_ObjIsXor(pNode) || Gia_ObjIsMux(p, pNode) ) pNode->fMark0 = 1; // compute levels - if ( fAdders ) - { - Vec_IntFreeP( &pMan->vLevels ); - vFadds = Gia_ManDetectFullAdders( pMan, 0, NULL ); - vHadds = Gia_ManDetectHalfAdders( pMan, 0 ); - vRecord = Gia_PolynFindOrder( pMan, vFadds, vHadds, 0, 0 ); - LevelMax = 1 + Gia_WriteDotAigLevel( pMan, vFadds, vHadds, vRecord, &pMan->vLevels, &vMarks, &vRemap, &vRemap2 ); - } - else - LevelMax = 1 + Gia_ManLevelNum( pMan ); - - // set output levels - Gia_ManForEachCo( pMan, pNode, i ) - Vec_IntWriteEntry( pMan->vLevels, Gia_ObjId(pMan, pNode), LevelMax ); + LevelMax = 1 + Gia_ManLevelNum( p ); + Gia_ManForEachCo( p, pNode, i ) + Vec_IntWriteEntry( p->vLevels, Gia_ObjId(p, pNode), LevelMax ); // write the DOT header - fprintf( pFile, "# %s\n", "AIG structure generated by IVY package" ); + fprintf( pFile, "# %s\n", "AIG structure generated by GIA package" ); fprintf( pFile, "\n" ); fprintf( pFile, "digraph AIG {\n" ); fprintf( pFile, "size = \"7.5,10\";\n" ); @@ -309,7 +443,7 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int fprintf( pFile, " fontsize=18,\n" ); fprintf( pFile, " fontname = \"Times-Roman\",\n" ); fprintf( pFile, " label=\"" ); - fprintf( pFile, "The set contains %d logic nodes and spans %d levels.", Gia_ManAndNum(pMan), LevelMax ); + fprintf( pFile, "The AIG contains %d nodes and spans %d levels.", Gia_ManAndNum(p), LevelMax-1 ); fprintf( pFile, "\\n" ); fprintf( pFile, "\"\n" ); fprintf( pFile, " ];\n" ); @@ -323,9 +457,9 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int // the labeling node of this level fprintf( pFile, " Level%d;\n", LevelMax ); // generate the CO nodes - Gia_ManForEachCo( pMan, pNode, i ) + Gia_ManForEachCo( p, pNode, i ) { - if ( Gia_ObjFaninId0p(pMan, pNode) == 0 ) + if ( Gia_ObjFaninId0p(p, pNode) == 0 ) fConstIsUsed = 1; /* if ( fHaig || pNode->pEquiv == NULL ) @@ -336,7 +470,7 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int (Gia_ObjIsLatch(pNode)? "_in":""), pNode->Id, (Gia_ObjIsLatch(pNode)? "_in":""), Gia_Regular(pNode->pEquiv)->Id, Gia_IsComplement(pNode->pEquiv)? "\'":"" ); */ - fprintf( pFile, " Node%d [label = \"%d\"", Gia_ObjId(pMan, pNode), Gia_ObjId(pMan, pNode) ); + fprintf( pFile, " Node%d [label = \"%d\"", Gia_ObjId(p, pNode), Gia_ObjId(p, pNode) ); fprintf( pFile, ", shape = %s", "invtriangle" ); fprintf( pFile, ", color = coral, fillcolor = coral" ); @@ -353,11 +487,9 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int fprintf( pFile, " rank = same;\n" ); // the labeling node of this level fprintf( pFile, " Level%d;\n", Level ); - Gia_ManForEachObj( pMan, pNode, i ) + Gia_ManForEachObj( p, pNode, i ) { - if ( vMarks && Vec_IntEntry(vMarks, i) == 0 ) - continue; - if ( (int)Gia_ObjLevel(pMan, pNode) != Level ) + if ( (int)Gia_ObjLevel(p, pNode) != Level ) continue; /* if ( fHaig || pNode->pEquiv == NULL ) @@ -366,29 +498,14 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int fprintf( pFile, " Node%d [label = \"%d(%d%s)\"", pNode->Id, pNode->Id, Gia_Regular(pNode->pEquiv)->Id, Gia_IsComplement(pNode->pEquiv)? "\'":"" ); */ - if ( vMarks && Vec_IntEntry(vMarks, i) > 0 ) - { - fprintf( pFile, " Node%d [label = \"%d_%d\"", i, Vec_IntEntry(vRemap2, i), i ); - if ( Abc_Lit2Att2(Vec_IntEntry(vMarks, i)) == 2 ) - fprintf( pFile, ", shape = doubleoctagon" ); - else - fprintf( pFile, ", shape = octagon" ); - } - else if ( Gia_ObjIsXor(pNode) ) - { - fprintf( pFile, " Node%d [label = \"%d\"", i, i ); + fprintf( pFile, " Node%d [label = \"%d\"", i, i ); + + if ( Gia_ObjIsXor(pNode) ) fprintf( pFile, ", shape = doublecircle" ); - } - else if ( Gia_ObjIsMux(pMan, pNode) ) - { - fprintf( pFile, " Node%d [label = \"%d\"", i, i ); + else if ( Gia_ObjIsMux(p, pNode) ) fprintf( pFile, ", shape = trapezium" ); - } else - { - fprintf( pFile, " Node%d [label = \"%d\"", i, i ); fprintf( pFile, ", shape = ellipse" ); - } if ( pNode->fMark0 ) fprintf( pFile, ", style = filled" ); @@ -405,7 +522,7 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int // the labeling node of this level fprintf( pFile, " Level%d;\n", 0 ); // generate constant node - if ( fConstIsUsed || pMan->fGiaSimple ) + if ( fConstIsUsed ) { // check if the costant node is present fprintf( pFile, " Node%d [label = \"Const0\"", 0 ); @@ -414,7 +531,7 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int fprintf( pFile, "];\n" ); } // generate the CI nodes - Gia_ManForEachCi( pMan, pNode, i ) + Gia_ManForEachCi( p, pNode, i ) { /* if ( fHaig || pNode->pEquiv == NULL ) @@ -425,7 +542,7 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int (Gia_ObjIsLatch(pNode)? "_out":""), pNode->Id, (Gia_ObjIsLatch(pNode)? "_out":""), Gia_Regular(pNode->pEquiv)->Id, Gia_IsComplement(pNode->pEquiv)? "\'":"" ); */ - fprintf( pFile, " Node%d [label = \"%d\"", Gia_ObjId(pMan, pNode), Gia_ObjId(pMan, pNode) ); + fprintf( pFile, " Node%d [label = \"%d\"", Gia_ObjId(p, pNode), Gia_ObjId(p, pNode) ); fprintf( pFile, ", shape = %s", "triangle" ); fprintf( pFile, ", color = coral, fillcolor = coral" ); @@ -437,73 +554,37 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int // generate invisible edges from the square down fprintf( pFile, "title1 -> title2 [style = invis];\n" ); - Gia_ManForEachCo( pMan, pNode, i ) - fprintf( pFile, "title2 -> Node%d [style = invis];\n", Gia_ObjId(pMan, pNode) ); + Gia_ManForEachCo( p, pNode, i ) + fprintf( pFile, "title2 -> Node%d [style = invis];\n", Gia_ObjId(p, pNode) ); // generate invisible edges among the COs Prev = -1; - Gia_ManForEachCo( pMan, pNode, i ) + Gia_ManForEachCo( p, pNode, i ) { if ( i > 0 ) - fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, Gia_ObjId(pMan, pNode) ); - Prev = Gia_ObjId(pMan, pNode); + fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, Gia_ObjId(p, pNode) ); + Prev = Gia_ObjId(p, pNode); + } + // generate invisible edges among the CIs + Prev = -1; + Gia_ManForEachCi( p, pNode, i ) + { + if ( i > 0 ) + fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, Gia_ObjId(p, pNode) ); + Prev = Gia_ObjId(p, pNode); } // generate edges - Gia_ManForEachObj( pMan, pNode, i ) + Gia_ManForEachObj( p, pNode, i ) { if ( !Gia_ObjIsAnd(pNode) && !Gia_ObjIsCo(pNode) && !Gia_ObjIsBuf(pNode) ) continue; - if ( vMarks && Vec_IntEntry(vMarks, i) == 0 ) - continue; - // consider half/full-adder - if ( vMarks && Vec_IntEntry(vMarks, i) > 0 ) - { - int k, Mark = Vec_IntEntry(vMarks, i); - if ( Abc_Lit2Att2(Mark) == 2 ) // FA - { - int * pFanins = Vec_IntEntryP( vFadds, 5*Abc_Lit2Var2(Mark) ); - if ( pFanins[3] == i ) - continue; - assert( pFanins[4] == i ); - // generate the edge from this node to the next - for ( k = 0; k < 3; k++ ) - { - fprintf( pFile, "Node%d", i ); - fprintf( pFile, " -> " ); - fprintf( pFile, "Node%d", Vec_IntEntry(vRemap, pFanins[k]) ); - fprintf( pFile, " [" ); - fprintf( pFile, "style = %s", "bold" ); - fprintf( pFile, "]" ); - fprintf( pFile, ";\n" ); - } - } - else // HA - { - int * pFanins = Vec_IntEntryP( vHadds, 2*Abc_Lit2Var2(Mark) ); - int pFaninsIn[2] = { Vec_IntEntry(vRemap, Gia_ObjFaninId0(pNode, i)), Vec_IntEntry(vRemap, Gia_ObjFaninId1(pNode, i)) }; - if ( pFanins[0] == i ) - continue; - assert( pFanins[1] == i ); - for ( k = 0; k < 2; k++ ) - { - fprintf( pFile, "Node%d", i ); - fprintf( pFile, " -> " ); - fprintf( pFile, "Node%d", Vec_IntEntry(vRemap, pFaninsIn[k]) ); - fprintf( pFile, " [" ); - fprintf( pFile, "style = %s", "bold" ); - fprintf( pFile, "]" ); - fprintf( pFile, ";\n" ); - } - } - continue; - } // generate the edge from this node to the next fprintf( pFile, "Node%d", i ); fprintf( pFile, " -> " ); - fprintf( pFile, "Node%d", vRemap ? Vec_IntEntry(vRemap, Gia_ObjFaninId0(pNode, i)) : Gia_ObjFaninId0(pNode, i) ); + fprintf( pFile, "Node%d", Gia_ObjFaninId0(pNode, i) ); fprintf( pFile, " [" ); - fprintf( pFile, "style = %s", Gia_ObjFaninC0(pNode)? "dotted" : "bold" ); -// if ( Gia_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL0(pNode) > 0 ) + fprintf( pFile, "style = %s", Gia_ObjFaninC0(pNode)? "dotted" : "solid" ); +// if ( Gia_NtkIsSeq(pNode->p) && Seq_ObjFaninL0(pNode) > 0 ) // fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,0) ); fprintf( pFile, "]" ); fprintf( pFile, ";\n" ); @@ -512,23 +593,23 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int // generate the edge from this node to the next fprintf( pFile, "Node%d", i ); fprintf( pFile, " -> " ); - fprintf( pFile, "Node%d", vRemap ? Vec_IntEntry(vRemap, Gia_ObjFaninId1(pNode, i)) : Gia_ObjFaninId1(pNode, i) ); + fprintf( pFile, "Node%d", Gia_ObjFaninId1(pNode, i) ); fprintf( pFile, " [" ); - fprintf( pFile, "style = %s", Gia_ObjFaninC1(pNode)? "dotted" : "bold" ); -// if ( Gia_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL1(pNode) > 0 ) + fprintf( pFile, "style = %s", Gia_ObjFaninC1(pNode)? "dotted" : "solid" ); +// if ( Gia_NtkIsSeq(pNode->p) && Seq_ObjFaninL1(pNode) > 0 ) // fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,1) ); fprintf( pFile, "]" ); fprintf( pFile, ";\n" ); - if ( !Gia_ObjIsMux(pMan, pNode) ) + if ( !Gia_ObjIsMux(p, pNode) ) continue; // generate the edge from this node to the next fprintf( pFile, "Node%d", i ); fprintf( pFile, " -> " ); - fprintf( pFile, "Node%d", vRemap ? Vec_IntEntry(vRemap, Gia_ObjFaninId2(pMan, i)) : Gia_ObjFaninId2(pMan, i) ); + fprintf( pFile, "Node%d", Gia_ObjFaninId2(p, i) ); fprintf( pFile, " [" ); - fprintf( pFile, "style = %s", Gia_ObjFaninC2(pMan, pNode)? "dotted" : "bold" ); -// if ( Gia_NtkIsSeq(pNode->pMan) && Seq_ObjFaninL1(pNode) > 0 ) + fprintf( pFile, "style = %s", Gia_ObjFaninC2(p, pNode)? "dotted" : "bold" ); +// if ( Gia_NtkIsSeq(pNode->p) && Seq_ObjFaninL1(pNode) > 0 ) // fprintf( pFile, ", label = \"%s\"", Seq_ObjFaninGetInitPrintable(pNode,1) ); fprintf( pFile, "]" ); fprintf( pFile, ";\n" ); @@ -543,7 +624,7 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int fprintf( pFile, "Node%d", pPrev->Id ); fprintf( pFile, " -> " ); fprintf( pFile, "Node%d", pTemp->Id ); - fprintf( pFile, " [style = %s]", Gia_IsComplement(pTemp->pEquiv)? "dotted" : "bold" ); + fprintf( pFile, " [style = %s]", Gia_IsComplement(pTemp->pEquiv)? "dotted" : "solid" ); fprintf( pFile, ";\n" ); pPrev = pTemp; } @@ -551,7 +632,7 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int fprintf( pFile, "Node%d", pPrev->Id ); fprintf( pFile, " -> " ); fprintf( pFile, "Node%d", pNode->Id ); - fprintf( pFile, " [style = %s]", Gia_IsComplement(pPrev->pEquiv)? "dotted" : "bold" ); + fprintf( pFile, " [style = %s]", Gia_IsComplement(pPrev->pEquiv)? "dotted" : "solid" ); fprintf( pFile, ";\n" ); } */ @@ -564,18 +645,461 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int // unmark nodes if ( vBold ) - Gia_ManForEachObjVec( vBold, pMan, pNode, i ) + Gia_ManForEachObjVec( vBold, p, pNode, i ) pNode->fMark0 = 0; - else if ( pMan->nXors || pMan->nMuxes ) - Gia_ManCleanMark0( pMan ); + else if ( p->nXors || p->nMuxes ) + Gia_ManCleanMark0( p ); + + Vec_IntFreeP( &p->vLevels ); +} - Vec_IntFreeP( &vFadds ); - Vec_IntFreeP( &vHadds ); - Vec_IntFreeP( &vRecord ); +/**Function************************************************************* + + Synopsis [Writes the graph structure of AIG for DOT.] - Vec_IntFreeP( &pMan->vLevels ); - Vec_IntFreeP( &vMarks ); - Vec_IntFreeP( &vRemap ); + Description [Useful for graph visualization using tools such as GraphViz: + http://www.graphviz.org/] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +int Gia_ShowAddOut( Vec_Int_t * vAdds, Vec_Int_t * vMapAdds, int Node ) +{ + int iBox = Vec_IntEntry( vMapAdds, Node ); + if ( iBox >= 0 ) + return Vec_IntEntry( vAdds, 6*iBox+4 ); + return Node; +} +void Gia_WriteDotAig( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold, Vec_Int_t * vAdds, Vec_Int_t * vXors, Vec_Int_t * vMapAdds, Vec_Int_t * vMapXors, Vec_Int_t * vOrder ) +{ + FILE * pFile; + Gia_Obj_t * pNode;//, * pTemp, * pPrev; + int LevelMax, Prev, Level, i; + int fConstIsUsed = 0; + int nFadds = Ree_ManCountFadds( vAdds ); + + if ( Gia_ManAndNum(p) > NODE_MAX ) + { + fprintf( stdout, "Cannot visualize AIG with more than %d nodes.\n", NODE_MAX ); + return; + } + if ( (pFile = fopen( pFileName, "w" )) == NULL ) + { + fprintf( stdout, "Cannot open the intermediate file \"%s\".\n", pFileName ); + return; + } + + // mark the nodes + if ( vBold ) + Gia_ManForEachObjVec( vBold, p, pNode, i ) + pNode->fMark0 = 1; + + // compute levels + LevelMax = 1 + p->nLevels; + Gia_ManForEachCo( p, pNode, i ) + Vec_IntWriteEntry( p->vLevels, Gia_ObjId(p, pNode), LevelMax ); + + // write the DOT header + fprintf( pFile, "# %s\n", "AIG structure generated by GIA package" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "digraph AIG {\n" ); + fprintf( pFile, "size = \"7.5,10\";\n" ); +// fprintf( pFile, "ranksep = 0.5;\n" ); +// fprintf( pFile, "nodesep = 0.5;\n" ); + fprintf( pFile, "center = true;\n" ); +// fprintf( pFile, "orientation = landscape;\n" ); +// fprintf( pFile, "edge [fontsize = 10];\n" ); +// fprintf( pFile, "edge [dir = none];\n" ); + fprintf( pFile, "edge [dir = back];\n" ); + fprintf( pFile, "\n" ); + + // labels on the left of the picture + fprintf( pFile, "{\n" ); + fprintf( pFile, " node [shape = plaintext];\n" ); + fprintf( pFile, " edge [style = invis];\n" ); + fprintf( pFile, " LevelTitle1 [label=\"\"];\n" ); + fprintf( pFile, " LevelTitle2 [label=\"\"];\n" ); + // generate node names with labels + for ( Level = LevelMax; Level >= 0; Level-- ) + { + // the visible node name + fprintf( pFile, " Level%d", Level ); + fprintf( pFile, " [label = " ); + // label name + fprintf( pFile, "\"" ); + fprintf( pFile, "\"" ); + fprintf( pFile, "];\n" ); + } + + // genetate the sequence of visible/invisible nodes to mark levels + fprintf( pFile, " LevelTitle1 -> LevelTitle2 ->" ); + for ( Level = LevelMax; Level >= 0; Level-- ) + { + // the visible node name + fprintf( pFile, " Level%d", Level ); + // the connector + if ( Level != 0 ) + fprintf( pFile, " ->" ); + else + fprintf( pFile, ";" ); + } + fprintf( pFile, "\n" ); + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate title box on top + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + fprintf( pFile, " LevelTitle1;\n" ); + fprintf( pFile, " title1 [shape=plaintext,\n" ); + fprintf( pFile, " fontsize=20,\n" ); + fprintf( pFile, " fontname = \"Times-Roman\",\n" ); + fprintf( pFile, " label=\"" ); + fprintf( pFile, "%s", "AIG structure visualized by ABC" ); + fprintf( pFile, "\\n" ); + fprintf( pFile, "Benchmark \\\"%s\\\". ", "aig" ); +// fprintf( pFile, "Time was %s. ", Extra_TimeStamp() ); + fprintf( pFile, "\"\n" ); + fprintf( pFile, " ];\n" ); + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate statistics box + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + fprintf( pFile, " LevelTitle2;\n" ); + fprintf( pFile, " title2 [shape=plaintext,\n" ); + fprintf( pFile, " fontsize=18,\n" ); + fprintf( pFile, " fontname = \"Times-Roman\",\n" ); + fprintf( pFile, " label=\"" ); + fprintf( pFile, "The AIG contains %d nodes, %d full-adders, and %d half-adders, and spans %d levels.", + Gia_ManAndNum(p), nFadds, Vec_IntSize(vAdds)/6-nFadds, LevelMax-1 ); + fprintf( pFile, "\\n" ); + fprintf( pFile, "\"\n" ); + fprintf( pFile, " ];\n" ); + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate the COs + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + // the labeling node of this level + fprintf( pFile, " Level%d;\n", LevelMax ); + // generate the CO nodes + Gia_ManForEachCo( p, pNode, i ) + { + if ( Gia_ObjFaninId0p(p, pNode) == 0 ) + fConstIsUsed = 1; + fprintf( pFile, " Node%d [label = \"%d\"", Gia_ObjId(p, pNode), Gia_ObjId(p, pNode) ); + + fprintf( pFile, ", shape = %s", "invtriangle" ); + fprintf( pFile, ", color = coral, fillcolor = coral" ); + fprintf( pFile, "];\n" ); + } + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate nodes of each rank + for ( Level = LevelMax - 1; Level > 0; Level-- ) + { + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + // the labeling node of this level + fprintf( pFile, " Level%d;\n", Level ); + Gia_ManForEachObjVec( vOrder, p, pNode, i ) + { + int iNode = Gia_ObjId( p, pNode ); + if ( (int)Gia_ObjLevel(p, pNode) != Level ) + continue; +/* + fprintf( pFile, " Node%d [label = \"%d\"", Gia_ObjId(p, pNode), Gia_ObjId(p, pNode) ); + if ( Gia_ObjIsXor(pNode) ) + fprintf( pFile, ", shape = doublecircle" ); + else if ( Gia_ObjIsMux(p, pNode) ) + fprintf( pFile, ", shape = trapezium" ); + else + fprintf( pFile, ", shape = ellipse" ); +*/ + if ( !pNode->fMark0 && Vec_IntEntry(vMapAdds, iNode) >= 0 ) + { + int iBox = Vec_IntEntry(vMapAdds, iNode); + fprintf( pFile, " Node%d [label = \"%d_%d\"", Gia_ShowAddOut(vAdds, vMapAdds, iNode), Vec_IntEntry(vAdds, 6*iBox+3), Vec_IntEntry(vAdds, 6*iBox+4) ); + if ( Vec_IntEntry(vAdds, 6*iBox+2) == 0 ) + fprintf( pFile, ", shape = octagon" ); + else + fprintf( pFile, ", shape = doubleoctagon" ); + } + else if ( Vec_IntEntry(vMapXors, iNode) >= 0 ) + { + fprintf( pFile, " Node%d [label = \"%d\"", iNode, iNode ); + fprintf( pFile, ", shape = doublecircle" ); + } + else if ( Gia_ObjIsXor(pNode) ) + { + fprintf( pFile, " Node%d [label = \"%d\"", iNode, iNode ); + fprintf( pFile, ", shape = doublecircle" ); + } + else if ( Gia_ObjIsMux(p, pNode) ) + { + fprintf( pFile, " Node%d [label = \"%d\"", iNode, iNode ); + fprintf( pFile, ", shape = trapezium" ); + } + else + { + fprintf( pFile, " Node%d [label = \"%d\"", iNode, iNode ); + fprintf( pFile, ", shape = ellipse" ); + } + if ( pNode->fMark0 ) + fprintf( pFile, ", style = filled" ); + fprintf( pFile, "];\n" ); + } + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + } + + // generate the CI nodes + fprintf( pFile, "{\n" ); + fprintf( pFile, " rank = same;\n" ); + // the labeling node of this level + fprintf( pFile, " Level%d;\n", 0 ); + // generate constant node + if ( fConstIsUsed ) + { + // check if the costant node is present + fprintf( pFile, " Node%d [label = \"Const0\"", 0 ); + fprintf( pFile, ", shape = ellipse" ); + fprintf( pFile, ", color = coral, fillcolor = coral" ); + fprintf( pFile, "];\n" ); + } + // generate the CI nodes + Gia_ManForEachCi( p, pNode, i ) + { + fprintf( pFile, " Node%d [label = \"%d\"", Gia_ObjId(p, pNode), Gia_ObjId(p, pNode) ); + + fprintf( pFile, ", shape = %s", "triangle" ); + fprintf( pFile, ", color = coral, fillcolor = coral" ); + fprintf( pFile, "];\n" ); + } + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + + // generate invisible edges from the square down + fprintf( pFile, "title1 -> title2 [style = invis];\n" ); + Gia_ManForEachCo( p, pNode, i ) + fprintf( pFile, "title2 -> Node%d [style = invis];\n", Gia_ObjId(p, pNode) ); + // generate invisible edges among the COs + Prev = -1; + Gia_ManForEachCo( p, pNode, i ) + { + if ( i > 0 ) + fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, Gia_ObjId(p, pNode) ); + Prev = Gia_ObjId(p, pNode); + } + // generate invisible edges among the CIs + Prev = -1; + Gia_ManForEachCi( p, pNode, i ) + { + if ( i > 0 ) + fprintf( pFile, "Node%d -> Node%d [style = invis];\n", Prev, Gia_ObjId(p, pNode) ); + Prev = Gia_ObjId(p, pNode); + } + + // generate edges + Gia_ManForEachCo( p, pNode, i ) + { + int iNode = Gia_ObjId( p, pNode ); + fprintf( pFile, "Node%d", iNode ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d", Gia_ShowAddOut(vAdds, vMapAdds, Gia_ObjFaninId0(pNode, iNode)) ); + fprintf( pFile, " [" ); + fprintf( pFile, "style = %s", Gia_ObjFaninC0(pNode)? "dotted" : "solid" ); + fprintf( pFile, "]" ); + fprintf( pFile, ";\n" ); + } + Gia_ManForEachObjVec( vOrder, p, pNode, i ) + { + int iNode = Gia_ObjId( p, pNode ); + if ( Vec_IntEntry(vMapAdds, Gia_ObjId(p, pNode)) >= 0 ) + { + int k, iBox = Vec_IntEntry(vMapAdds, iNode); + for ( k = 0; k < 3; k++ ) + if ( Vec_IntEntry(vAdds, 6*iBox+k) ) + { + int iBox2 = Vec_IntEntry(vMapAdds, Vec_IntEntry(vAdds, 6*iBox+k)); + int fXor2 = iBox2 >= 0 ? (int)(Vec_IntEntry(vAdds, 6*iBox2+3) == Vec_IntEntry(vAdds, 6*iBox+k)) : 0; + fprintf( pFile, "Node%d", Gia_ShowAddOut(vAdds, vMapAdds, iNode) ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d", Gia_ShowAddOut(vAdds, vMapAdds, Vec_IntEntry(vAdds, 6*iBox+k)) ); + fprintf( pFile, " [" ); + fprintf( pFile, "style = %s", fXor2? "bold" : "solid" ); + fprintf( pFile, "]" ); + fprintf( pFile, ";\n" ); + } + continue; + } + if ( Vec_IntEntry(vMapXors, Gia_ObjId(p, pNode)) >= 0 ) + { + int k, iXor = Vec_IntEntry(vMapXors, iNode); + for ( k = 1; k < 4; k++ ) + if ( Vec_IntEntry(vXors, 4*iXor+k) ) + { + int iXor2 = Vec_IntEntry(vMapXors, Vec_IntEntry(vXors, 4*iXor+k)); + fprintf( pFile, "Node%d", iNode ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d", Gia_ShowAddOut(vAdds, vMapAdds, Vec_IntEntry(vXors, 4*iXor+k)) ); + fprintf( pFile, " [" ); + fprintf( pFile, "style = %s", iXor2 >= 0? "bold" : "solid" ); + fprintf( pFile, "]" ); + fprintf( pFile, ";\n" ); + } + continue; + } + // generate the edge from this node to the next + fprintf( pFile, "Node%d", iNode ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d", Gia_ShowAddOut(vAdds, vMapAdds, Gia_ObjFaninId0(pNode, iNode)) ); + fprintf( pFile, " [" ); + fprintf( pFile, "style = %s", Gia_ObjFaninC0(pNode)? "dotted" : "solid" ); + fprintf( pFile, "]" ); + fprintf( pFile, ";\n" ); + if ( !Gia_ObjIsAnd(pNode) ) + continue; + // generate the edge from this node to the next + fprintf( pFile, "Node%d", iNode ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d", Gia_ShowAddOut(vAdds, vMapAdds, Gia_ObjFaninId1(pNode, iNode)) ); + fprintf( pFile, " [" ); + fprintf( pFile, "style = %s", Gia_ObjFaninC1(pNode)? "dotted" : "solid" ); + fprintf( pFile, "]" ); + fprintf( pFile, ";\n" ); + + if ( !Gia_ObjIsMux(p, pNode) ) + continue; + // generate the edge from this node to the next + fprintf( pFile, "Node%d", iNode ); + fprintf( pFile, " -> " ); + fprintf( pFile, "Node%d", Gia_ShowAddOut(vAdds, vMapAdds, Gia_ObjFaninId2(p, iNode)) ); + fprintf( pFile, " [" ); + fprintf( pFile, "style = %s", Gia_ObjFaninC2(p, pNode)? "dotted" : "solid" ); + fprintf( pFile, "]" ); + fprintf( pFile, ";\n" ); + } + + fprintf( pFile, "}" ); + fprintf( pFile, "\n" ); + fprintf( pFile, "\n" ); + fclose( pFile ); + + // unmark nodes + if ( vBold ) + Gia_ManForEachObjVec( vBold, p, pNode, i ) + pNode->fMark0 = 0; + + Vec_IntFreeP( &p->vLevels ); +} + +/**Function************************************************************* + + Synopsis [Returns DFS ordered array of objects and their levels.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Gia_ShowMapAdds( Gia_Man_t * p, Vec_Int_t * vAdds, int fFadds, Vec_Int_t * vBold ) +{ + Vec_Bit_t * vIsBold = Vec_BitStart( Gia_ManObjNum(p) ); + Vec_Int_t * vMapAdds = Vec_IntStartFull( Gia_ManObjNum(p) ); int i, Entry; + if ( vBold ) + Vec_IntForEachEntry( vBold, Entry, i ) + Vec_BitWriteEntry( vIsBold, Entry, 1 ); + for ( i = 0; 6*i < Vec_IntSize(vAdds); i++ ) + { + if ( fFadds && Vec_IntEntry(vAdds, 6*i+2) == 0 ) + continue; + if ( Vec_BitEntry(vIsBold, Vec_IntEntry(vAdds, 6*i+3)) || Vec_BitEntry(vIsBold, Vec_IntEntry(vAdds, 6*i+4)) ) + continue; + Vec_IntWriteEntry( vMapAdds, Vec_IntEntry(vAdds, 6*i+3), i ); + Vec_IntWriteEntry( vMapAdds, Vec_IntEntry(vAdds, 6*i+4), i ); + } + Vec_BitFree( vIsBold ); + return vMapAdds; +} +Vec_Int_t * Gia_ShowMapXors( Gia_Man_t * p, Vec_Int_t * vXors ) +{ + Vec_Int_t * vMapXors = Vec_IntStartFull( Gia_ManObjNum(p) ); int i; + for ( i = 0; 4*i < Vec_IntSize(vXors); i++ ) + Vec_IntWriteEntry( vMapXors, Vec_IntEntry(vXors, 4*i), i ); + return vMapXors; +} +int Gia_ShowCollectObjs_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vAdds, Vec_Int_t * vXors, Vec_Int_t * vMapAdds, Vec_Int_t * vMapXors, Vec_Int_t * vOrder ) +{ + int Level0, Level1, Level2 = 0, Level = 0; + if ( Gia_ObjIsTravIdCurrent(p, pObj) ) + return Gia_ObjLevel(p, pObj); + Gia_ObjSetTravIdCurrent(p, pObj); + if ( Gia_ObjIsCi(pObj) ) + return 0; + if ( Vec_IntEntry(vMapAdds, Gia_ObjId(p, pObj)) >= 0 ) + { + int iBox = Vec_IntEntry(vMapAdds, Gia_ObjId(p, pObj)); + Gia_ObjSetTravIdCurrentId(p, Vec_IntEntry(vAdds, 6*iBox+3) ); + Gia_ObjSetTravIdCurrentId(p, Vec_IntEntry(vAdds, 6*iBox+4) ); + Level0 = Gia_ShowCollectObjs_rec( p, Gia_ManObj( p, Vec_IntEntry(vAdds, 6*iBox+0) ), vAdds, vXors, vMapAdds, vMapXors, vOrder ); + Level1 = Gia_ShowCollectObjs_rec( p, Gia_ManObj( p, Vec_IntEntry(vAdds, 6*iBox+1) ), vAdds, vXors, vMapAdds, vMapXors, vOrder ); + if ( Vec_IntEntry(vAdds, 6*iBox+2) ) + Level2 = Gia_ShowCollectObjs_rec( p, Gia_ManObj( p, Vec_IntEntry(vAdds, 6*iBox+2) ), vAdds, vXors, vMapAdds, vMapXors, vOrder ); + Level = 1 + Abc_MaxInt( Abc_MaxInt(Level0, Level1), Level2 ); + Gia_ObjSetLevelId( p, Vec_IntEntry(vAdds, 6*iBox+3), Level ); + Gia_ObjSetLevelId( p, Vec_IntEntry(vAdds, 6*iBox+4), Level ); + pObj = Gia_ManObj( p, Vec_IntEntry(vAdds, 6*iBox+4) ); + } + else if ( Vec_IntEntry(vMapXors, Gia_ObjId(p, pObj)) >= 0 ) + { + int iXor = Vec_IntEntry(vMapXors, Gia_ObjId(p, pObj)); + Level0 = Gia_ShowCollectObjs_rec( p, Gia_ManObj( p, Vec_IntEntry(vXors, 4*iXor+1) ), vAdds, vXors, vMapAdds, vMapXors, vOrder ); + Level1 = Gia_ShowCollectObjs_rec( p, Gia_ManObj( p, Vec_IntEntry(vXors, 4*iXor+2) ), vAdds, vXors, vMapAdds, vMapXors, vOrder ); + if ( Vec_IntEntry(vXors, 4*iXor+3) ) + Level2 = Gia_ShowCollectObjs_rec( p, Gia_ManObj( p, Vec_IntEntry(vXors, 4*iXor+3) ), vAdds, vXors, vMapAdds, vMapXors, vOrder ); + Level = 1 + Abc_MaxInt( Abc_MaxInt(Level0, Level1), Level2 ); + Gia_ObjSetLevel( p, pObj, Level ); + } + else + { + assert( !Gia_ObjIsMux(p, pObj) ); + Level0 = Gia_ShowCollectObjs_rec( p, Gia_ObjFanin0(pObj), vAdds, vXors, vMapAdds, vMapXors, vOrder ); + Level1 = Gia_ShowCollectObjs_rec( p, Gia_ObjFanin1(pObj), vAdds, vXors, vMapAdds, vMapXors, vOrder ); + Level = 1 + Abc_MaxInt(Level0, Level1); + Gia_ObjSetLevel( p, pObj, Level ); + } + Vec_IntPush( vOrder, Gia_ObjId(p, pObj) ); + p->nLevels = Abc_MaxInt( p->nLevels, Level ); + return Level; +} +Vec_Int_t * Gia_ShowCollectObjs( Gia_Man_t * p, Vec_Int_t * vAdds, Vec_Int_t * vXors, Vec_Int_t * vMapAdds, Vec_Int_t * vMapXors ) +{ + Gia_Obj_t * pObj; int i; + Vec_Int_t * vOrder = Vec_IntAlloc( 100 ); + Gia_ManCleanLevels( p, Gia_ManObjNum(p) ); + p->nLevels = 0; + Gia_ManIncrementTravId( p ); + Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p)); + Gia_ManForEachCi( p, pObj, i ) + Gia_ObjSetTravIdCurrent(p, pObj); + Gia_ManForEachCo( p, pObj, i ) + Gia_ShowCollectObjs_rec( p, Gia_ObjFanin0(pObj), vAdds, vXors, vMapAdds, vMapXors, vOrder ); + return vOrder; } /**Function************************************************************* @@ -589,15 +1113,23 @@ void Gia_WriteDotAig( Gia_Man_t * pMan, char * pFileName, Vec_Int_t * vBold, int SeeAlso [] ***********************************************************************/ -void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders ) +void Gia_ShowProcess( Gia_Man_t * p, char * pFileName, Vec_Int_t * vBold, Vec_Int_t * vAdds, Vec_Int_t * vXors, int fFadds ) +{ + Vec_Int_t * vMapAdds = Gia_ShowMapAdds( p, vAdds, fFadds, vBold ); + Vec_Int_t * vMapXors = Gia_ShowMapXors( p, vXors ); + Vec_Int_t * vOrder = Gia_ShowCollectObjs( p, vAdds, vXors, vMapAdds, vMapXors ); + Gia_WriteDotAig( p, pFileName, vBold, vAdds, vXors, vMapAdds, vMapXors, vOrder ); + Vec_IntFree( vMapAdds ); + Vec_IntFree( vMapXors ); + Vec_IntFree( vOrder ); +} +void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders, int fFadds, int fPath ) { extern void Abc_ShowFile( char * FileNameDot ); - static int Counter = 0; char FileNameDot[200]; FILE * pFile; - // create the file name -// Gia_ShowGetFileName( pMan->pName, FileNameDot ); - sprintf( FileNameDot, "temp%02d.dot", Counter++ ); + Vec_Int_t * vXors = NULL, * vAdds = fAdders ? Ree_ManComputeCuts( pMan, &vXors, 0 ) : NULL; + sprintf( FileNameDot, "%s", Extra_FileNameGenericAppend(pMan->pName, ".dot") ); // check that the file can be opened if ( (pFile = fopen( FileNameDot, "w" )) == NULL ) { @@ -606,12 +1138,23 @@ void Gia_ManShow( Gia_Man_t * pMan, Vec_Int_t * vBold, int fAdders ) } fclose( pFile ); // generate the file - Gia_WriteDotAig( pMan, FileNameDot, vBold, fAdders ); + if ( fPath ) + Gia_ShowPath( pMan, FileNameDot ); + else if ( fAdders ) + Gia_ShowProcess( pMan, FileNameDot, vBold, vAdds, vXors, fFadds ); + else + Gia_WriteDotAigSimple( pMan, FileNameDot, vBold ); // visualize the file Abc_ShowFile( FileNameDot ); + + Vec_IntFreeP( &vAdds ); + Vec_IntFreeP( &vXors ); } + + + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c index 71b9a475..29aa93f8 100644 --- a/src/aig/gia/giaTim.c +++ b/src/aig/gia/giaTim.c @@ -584,6 +584,8 @@ int Gia_ManLutLevelWithBoxes( Gia_Man_t * p ) Gia_Obj_t * pObj, * pObjIn; int i, k, j, curCi, curCo, LevelMax; assert( Gia_ManRegNum(p) == 0 ); + if ( pManTime == NULL ) + return Gia_ManLutLevel(p, NULL); // copy const and real PIs Gia_ManCleanLevels( p, Gia_ManObjNum(p) ); Gia_ObjSetLevel( p, Gia_ManConst0(p), 0 ); diff --git a/src/aig/gia/giaTruth.c b/src/aig/gia/giaTruth.c index ce06fa0b..ab5f569e 100644 --- a/src/aig/gia/giaTruth.c +++ b/src/aig/gia/giaTruth.c @@ -139,6 +139,59 @@ word Gia_ObjComputeTruthTable6Lut( Gia_Man_t * p, int iObj, Vec_Wrd_t * vTemp ) /**Function************************************************************* + Synopsis [Computes truth table up to 6 inputs in terms of CIs.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +word Gia_ObjComputeTruth6( Gia_Man_t * p, int iObj, Vec_Int_t * vSupp, Vec_Wrd_t * vTemp ) +{ + int i, Fanin; + assert( Vec_WrdSize(vTemp) == Gia_ManObjNum(p) ); + assert( Vec_IntSize(vSupp) <= 6 ); + Gia_ManIncrementTravId( p ); + Vec_IntForEachEntry( vSupp, Fanin, i ) + { + Gia_ObjSetTravIdCurrentId( p, Fanin ); + Vec_WrdWriteEntry( vTemp, Fanin, s_Truth6[i] ); + } + Gia_ObjComputeTruthTable6Lut_rec( p, iObj, vTemp ); + return Vec_WrdEntry( vTemp, iObj ); +} +void Gia_ObjComputeTruth6CisSupport_rec( Gia_Man_t * p, int iObj, Vec_Int_t * vSupp ) +{ + Gia_Obj_t * pObj = Gia_ManObj( p, iObj ); + if ( Gia_ObjIsTravIdCurrentId(p, iObj) ) + return; + Gia_ObjSetTravIdCurrentId(p, iObj); + if ( Gia_ObjIsCi(pObj) ) + { + Vec_IntPushOrder( vSupp, iObj ); + return; + } + assert( Gia_ObjIsAnd(pObj) ); + Gia_ObjComputeTruth6CisSupport_rec( p, Gia_ObjFaninId0p(p, pObj), vSupp ); + Gia_ObjComputeTruth6CisSupport_rec( p, Gia_ObjFaninId1p(p, pObj), vSupp ); +} +word Gia_ObjComputeTruth6Cis( Gia_Man_t * p, int iLit, Vec_Int_t * vSupp, Vec_Wrd_t * vTemp ) +{ + int iObj = Abc_Lit2Var(iLit); + Vec_IntClear( vSupp ); + if ( !iObj ) return Abc_LitIsCompl(iLit) ? ~(word)0 : (word)0; + Gia_ManIncrementTravId( p ); + Gia_ObjComputeTruth6CisSupport_rec( p, iObj, vSupp ); + if ( Vec_IntSize(vSupp) > 6 ) + return 0; + Gia_ObjComputeTruth6( p, iObj, vSupp, vTemp ); + return Abc_LitIsCompl(iLit) ? ~Vec_WrdEntry(vTemp, iObj) : Vec_WrdEntry(vTemp, iObj); +} + +/**Function************************************************************* + Synopsis [Computes truth table up to 6 inputs.] Description [] diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c index eccdbc73..c7af642e 100644 --- a/src/aig/gia/giaUtil.c +++ b/src/aig/gia/giaUtil.c @@ -937,8 +937,8 @@ int Gia_ObjRecognizeExor( Gia_Obj_t * pObj, Gia_Obj_t ** ppFan0, Gia_Obj_t ** pp return 0; if ( Gia_ObjFaninC0(p0) == Gia_ObjFaninC0(p1) || Gia_ObjFaninC1(p0) == Gia_ObjFaninC1(p1) ) return 0; - *ppFan0 = Gia_ObjChild0(p0); - *ppFan1 = Gia_ObjChild1(p0); + if ( ppFan0 ) *ppFan0 = Gia_ObjChild0(p0); + if ( ppFan1 ) *ppFan1 = Gia_ObjChild1(p0); return 1; } diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make index 0066bfd2..0ddf9833 100644 --- a/src/aig/gia/module.make +++ b/src/aig/gia/module.make @@ -59,6 +59,7 @@ SRC += src/aig/gia/giaAig.c \ src/aig/gia/giaSatLE.c \ src/aig/gia/giaSatLut.c \ src/aig/gia/giaSatMap.c \ + src/aig/gia/giaSatoko.c \ src/aig/gia/giaScl.c \ src/aig/gia/giaScript.c \ src/aig/gia/giaShow.c \ |