diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/gia/gia.h | 2 | ||||
-rw-r--r-- | src/aig/gia/giaAiger.c | 2 | ||||
-rw-r--r-- | src/aig/gia/giaDup.c | 5 | ||||
-rw-r--r-- | src/aig/gia/giaHash.c | 34 | ||||
-rw-r--r-- | src/aig/gia/giaRex.c | 2 | ||||
-rw-r--r-- | src/aig/gia/giaTim.c | 2 | ||||
-rw-r--r-- | src/base/abci/abc.c | 4 | ||||
-rw-r--r-- | src/base/cba/cbaBlast.c | 2 | ||||
-rw-r--r-- | src/base/wlc/wlcBlast.c | 15 |
9 files changed, 41 insertions, 27 deletions
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index 81a6d11a..58b00db2 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -1204,7 +1204,7 @@ 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 ); extern Gia_Man_t * Gia_ManDupAndOr( Gia_Man_t * p, int nOuts, int fUseOr, int fCompl ); -extern Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fVerbose ); +extern Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fGiaSimple, int fVerbose ); extern Gia_Man_t * Gia_ManMiter2( Gia_Man_t * p, char * pInit, int fVerbose ); extern Gia_Man_t * Gia_ManTransformMiter( Gia_Man_t * p ); extern Gia_Man_t * Gia_ManTransformMiter2( Gia_Man_t * p ); diff --git a/src/aig/gia/giaAiger.c b/src/aig/gia/giaAiger.c index 2aadf07f..8e7423aa 100644 --- a/src/aig/gia/giaAiger.c +++ b/src/aig/gia/giaAiger.c @@ -848,7 +848,7 @@ Gia_Man_t * Gia_AigerReadFromMemory( char * pContents, int nFileSize, int fGiaSi } } pInit[i] = 0; - pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 1 ); + pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, fGiaSimple, 1 ); pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0; Gia_ManStop( pTemp ); ABC_FREE( pInit ); diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c index 66b80ace..3ffb948e 100644 --- a/src/aig/gia/giaDup.c +++ b/src/aig/gia/giaDup.c @@ -2618,7 +2618,7 @@ Gia_Man_t * Gia_ManTransformTwoWord2DualOutput( Gia_Man_t * p ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fVerbose ) +Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fGiaSimple, int fVerbose ) { Gia_Man_t * pNew; Gia_Obj_t * pObj; @@ -2635,6 +2635,7 @@ Gia_Man_t * Gia_ManDupZeroUndc( Gia_Man_t * p, char * pInit, int fVerbose ) pNew = Gia_ManStart( Gia_ManObjNum(p) ); pNew->pName = Abc_UtilStrsav( p->pName ); pNew->pSpec = Abc_UtilStrsav( p->pSpec ); + pNew->fGiaSimple = fGiaSimple; Gia_ManConst0(p)->Value = 0; // create primary inputs Gia_ManForEachPi( p, pObj, i ) @@ -2707,7 +2708,7 @@ Gia_Man_t * Gia_ManMiter2( Gia_Man_t * pStart, char * pInit, int fVerbose ) for ( i = 0; i < Gia_ManPiNum(pStart); i++ ) assert( pInit[i] == 'x' || pInit[i] == 'X' ); // normalize the manager - pUndc = Gia_ManDupZeroUndc( pStart, pInit + Gia_ManPiNum(pStart), fVerbose ); + pUndc = Gia_ManDupZeroUndc( pStart, pInit + Gia_ManPiNum(pStart), 0, fVerbose ); // create new init string pInitNew = ABC_ALLOC( char, Gia_ManPiNum(pUndc)+1 ); for ( i = 0; i < Gia_ManPiNum(pStart); i++ ) diff --git a/src/aig/gia/giaHash.c b/src/aig/gia/giaHash.c index 5bfdbae2..d4a47ac5 100644 --- a/src/aig/gia/giaHash.c +++ b/src/aig/gia/giaHash.c @@ -666,10 +666,15 @@ int Gia_ManHashAndTry( Gia_Man_t * p, int iLit0, int iLit1 ) ***********************************************************************/ int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 ) { - int fCompl = Abc_LitIsCompl(iLit0) ^ Abc_LitIsCompl(iLit1); - int iTemp0 = Gia_ManHashAnd( p, Abc_LitRegular(iLit0), Abc_LitNot(Abc_LitRegular(iLit1)) ); - int iTemp1 = Gia_ManHashAnd( p, Abc_LitRegular(iLit1), Abc_LitNot(Abc_LitRegular(iLit0)) ); - return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl ); + if ( p->fGiaSimple ) + return Gia_ManHashOr(p, Gia_ManHashAnd(p, iLit0, Abc_LitNot(iLit1)), Gia_ManHashAnd(p, Abc_LitNot(iLit0), iLit1) ); + else + { + int fCompl = Abc_LitIsCompl(iLit0) ^ Abc_LitIsCompl(iLit1); + int iTemp0 = Gia_ManHashAnd( p, Abc_LitRegular(iLit0), Abc_LitNot(Abc_LitRegular(iLit1)) ); + int iTemp1 = Gia_ManHashAnd( p, Abc_LitRegular(iLit1), Abc_LitNot(Abc_LitRegular(iLit0)) ); + return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl ); + } } /**Function************************************************************* @@ -685,14 +690,19 @@ int Gia_ManHashXor( Gia_Man_t * p, int iLit0, int iLit1 ) ***********************************************************************/ int Gia_ManHashMux( Gia_Man_t * p, int iCtrl, int iData1, int iData0 ) { - int iTemp0, iTemp1, fCompl = 0; - if ( iData0 > iData1 ) - iData0 ^= iData1, iData1 ^= iData0, iData0 ^= iData1, iCtrl = Abc_LitNot(iCtrl); - if ( Abc_LitIsCompl(iData1) ) - iData0 = Abc_LitNot(iData0), iData1 = Abc_LitNot(iData1), fCompl = 1; - iTemp0 = Gia_ManHashAnd( p, Abc_LitNot(iCtrl), iData0 ); - iTemp1 = Gia_ManHashAnd( p, iCtrl, iData1 ); - return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl ); + if ( p->fGiaSimple ) + return Gia_ManHashOr(p, Gia_ManHashAnd(p, iCtrl, iData1), Gia_ManHashAnd(p, Abc_LitNot(iCtrl), iData0) ); + else + { + int iTemp0, iTemp1, fCompl = 0; + if ( iData0 > iData1 ) + iData0 ^= iData1, iData1 ^= iData0, iData0 ^= iData1, iCtrl = Abc_LitNot(iCtrl); + if ( Abc_LitIsCompl(iData1) ) + iData0 = Abc_LitNot(iData0), iData1 = Abc_LitNot(iData1), fCompl = 1; + iTemp0 = Gia_ManHashAnd( p, Abc_LitNot(iCtrl), iData0 ); + iTemp1 = Gia_ManHashAnd( p, iCtrl, iData1 ); + return Abc_LitNotCond( Gia_ManHashAnd( p, Abc_LitNot(iTemp0), Abc_LitNot(iTemp1) ), !fCompl ); + } } /**Function************************************************************* diff --git a/src/aig/gia/giaRex.c b/src/aig/gia/giaRex.c index 2eacc8d7..ebfc9401 100644 --- a/src/aig/gia/giaRex.c +++ b/src/aig/gia/giaRex.c @@ -309,7 +309,7 @@ Gia_Man_t * Gia_ManRex2Gia( char * pStrInit, int fOrder, int fVerbose ) Gia_ManStop( pTemp ); // add initial state - pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 0 ); + pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 0, 0 ); Gia_ManStop( pTemp ); Vec_StrFree( vInit ); /* diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c index 40573025..71b9a475 100644 --- a/src/aig/gia/giaTim.c +++ b/src/aig/gia/giaTim.c @@ -871,7 +871,7 @@ Gia_Man_t * Gia_ManDupCollapse( Gia_Man_t * p, Gia_Man_t * pBoxes, Vec_Int_t * v pInit[i] = 'X'; } pInit[i] = 0; - pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 1 ); + pNew = Gia_ManDupZeroUndc( pTemp = pNew, pInit, 0, 1 ); pNew->nConstrs = pTemp->nConstrs; pTemp->nConstrs = 0; Gia_ManStop( pTemp ); ABC_FREE( pInit ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 551961c9..e1d69bf1 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -26761,7 +26761,7 @@ int Abc_CommandAbc9Get( Abc_Frame_t * pAbc, int argc, char ** argv ) Aig_ManStop( pAig ); // perform undc/zero pInits = Abc_NtkCollectLatchValuesStr( pAbc->pNtkCur ); - pGia = Gia_ManDupZeroUndc( pTemp = pGia, pInits, fVerbose ); + pGia = Gia_ManDupZeroUndc( pTemp = pGia, pInits, 0, fVerbose ); Gia_ManStop( pTemp ); ABC_FREE( pInits ); } @@ -32141,7 +32141,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_Man_t * pTemp; if ( !pPars->fSilent ) Abc_Print( 1, "Assuming the current network is a single-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit ); - pTemp = Gia_ManTransformToDual( pAbc->pGia ); + pTemp = Gia_ManDemiterToDual( pAbc->pGia ); pAbc->Status = Cec_ManVerify( pTemp, pPars ); ABC_SWAP( Abc_Cex_t *, pAbc->pGia->pCexComb, pTemp->pCexComb ); Gia_ManStop( pTemp ); diff --git a/src/base/cba/cbaBlast.c b/src/base/cba/cbaBlast.c index 322d4372..490a36eb 100644 --- a/src/base/cba/cbaBlast.c +++ b/src/base/cba/cbaBlast.c @@ -1013,7 +1013,7 @@ Gia_Man_t * Cba_NtkBlast( Cba_Ntk_t * p, int fSeq ) { Gia_ManSetRegNum( pNew, Vec_StrSize(vInit) ); Vec_StrPush( vInit, '\0' ); - pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 1 ); + pNew = Gia_ManDupZeroUndc( pTemp = pNew, Vec_StrArray(vInit), 0, 1 ); Gia_ManDupRemapLiterals( vBits, pTemp ); Gia_ManStop( pTemp ); Vec_StrFreeP( &vInit ); diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index adce0d57..65940176 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -274,10 +274,10 @@ void Wlc_BlastFullAdder( Gia_Man_t * pNew, int a, int b, int c, int * pc, int * { int And1 = Gia_ManHashAnd(pNew, a, b); int And1_= Gia_ManHashAnd(pNew, Abc_LitNot(a), Abc_LitNot(b)); - int Xor = Abc_LitNot(Gia_ManHashOr(pNew, And1, And1_)); + int Xor = Gia_ManHashAnd(pNew, Abc_LitNot(And1), Abc_LitNot(And1_)); int And2 = Gia_ManHashAnd(pNew, c, Xor); int And2_= Gia_ManHashAnd(pNew, Abc_LitNot(c), Abc_LitNot(Xor)); - *ps = Abc_LitNot(Gia_ManHashOr(pNew, And2, And2_)); + *ps = Gia_ManHashAnd(pNew, Abc_LitNot(And2), Abc_LitNot(And2_)); *pc = Gia_ManHashOr (pNew, And1, And2); } } @@ -1209,9 +1209,12 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple assert( nFFins == nFFouts ); Gia_ManSetRegNum( pNew, nFFins ); // finalize AIG - pNew = Gia_ManCleanup( pTemp = pNew ); - Gia_ManDupRemapLiterals( vBits, pTemp ); - Gia_ManStop( pTemp ); + if ( !fGiaSimple ) + { + pNew = Gia_ManCleanup( pTemp = pNew ); + Gia_ManDupRemapLiterals( vBits, pTemp ); + Gia_ManStop( pTemp ); + } // transform AIG with init state if ( p->pInits ) { @@ -1222,7 +1225,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple } else { - pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, 1 ); + pNew = Gia_ManDupZeroUndc( pTemp = pNew, p->pInits, fGiaSimple, 1 ); Gia_ManDupRemapLiterals( vBits, pTemp ); Gia_ManStop( pTemp ); } |