diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-01-27 09:54:35 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-01-27 09:54:35 -0800 |
| commit | 0f22046bcb71ba096fedfc6a75b6bc7fd4090e70 (patch) | |
| tree | b5b5642f8651b024a5176a4e26870d565ca9c514 /src/map | |
| parent | 8ff4b79fc2f5d62c98af94e761535095d3fd8d8e (diff) | |
| download | abc-0f22046bcb71ba096fedfc6a75b6bc7fd4090e70.tar.gz abc-0f22046bcb71ba096fedfc6a75b6bc7fd4090e70.tar.bz2 abc-0f22046bcb71ba096fedfc6a75b6bc7fd4090e70.zip | |
New assertions and bug fix in DSD balancing.
Diffstat (limited to 'src/map')
| -rw-r--r-- | src/map/if/ifDelay.c | 6 | ||||
| -rw-r--r-- | src/map/if/ifDsd.c | 13 |
2 files changed, 11 insertions, 8 deletions
diff --git a/src/map/if/ifDelay.c b/src/map/if/ifDelay.c index 5afb77eb..cb25e767 100644 --- a/src/map/if/ifDelay.c +++ b/src/map/if/ifDelay.c @@ -204,9 +204,9 @@ int If_CutSopBalanceEvalInt( Vec_Int_t * vCover, int * pTimes, int * pFaninLits, { Literal = 3 & (Entry >> (k << 1)); if ( Literal == 1 ) // neg literal - nLits++, Delay = If_LogCounterAddAig( pCounterAnd, &nCounterAnd, pFaninLitsAnd, pTimes[k], Abc_LitNot(pFaninLits[k]), vAig, nSuppAll, 0, 0 ); + nLits++, Delay = If_LogCounterAddAig( pCounterAnd, &nCounterAnd, pFaninLitsAnd, pTimes[k], vAig ? Abc_LitNot(pFaninLits[k]) : -1, vAig, nSuppAll, 0, 0 ); else if ( Literal == 2 ) // pos literal - nLits++, Delay = If_LogCounterAddAig( pCounterAnd, &nCounterAnd, pFaninLitsAnd, pTimes[k], pFaninLits[k], vAig, nSuppAll, 0, 0 ); + nLits++, Delay = If_LogCounterAddAig( pCounterAnd, &nCounterAnd, pFaninLitsAnd, pTimes[k], vAig ? pFaninLits[k] : -1, vAig, nSuppAll, 0, 0 ); else if ( Literal != 0 ) assert( 0 ); } @@ -216,7 +216,7 @@ int If_CutSopBalanceEvalInt( Vec_Int_t * vCover, int * pTimes, int * pFaninLits, iRes = If_LogCreateAndXorMulti( vAig, pFaninLitsAnd, nCounterAnd, nSuppAll, 0 ); else *pArea += nLits == 1 ? 0 : nLits - 1; - Delay = If_LogCounterAddAig( pCounterOr, &nCounterOr, pFaninLitsOr, Delay, Abc_LitNot(iRes), vAig, nSuppAll, 0, 0 ); + Delay = If_LogCounterAddAig( pCounterOr, &nCounterOr, pFaninLitsOr, Delay, vAig ? Abc_LitNot(iRes) : -1, vAig, nSuppAll, 0, 0 ); } assert( nCounterOr > 0 ); if ( vAig ) diff --git a/src/map/if/ifDsd.c b/src/map/if/ifDsd.c index d97cd9be..9b09ce95 100644 --- a/src/map/if/ifDsd.c +++ b/src/map/if/ifDsd.c @@ -2211,7 +2211,7 @@ int If_CutDsdBalanceEval_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pnSup if ( If_DsdObjType(pObj) == IF_DSD_VAR ) { int iCutVar = Abc_Lit2Var( pPermLits[*pnSupp] ); - if ( vAig ) + if ( vAig ) *piLit = Abc_Var2Lit( iCutVar, Abc_LitIsCompl(pPermLits[*pnSupp]) ); (*pnSupp)++; return pTimes[iCutVar]; @@ -2224,7 +2224,8 @@ int If_CutDsdBalanceEval_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pnSup Delays[i] = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea, pPermLits ); if ( Delays[i] == -1 ) return -1; - pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) ); + if ( vAig ) + pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) ); } if ( vAig ) *piLit = If_LogCreateMux( vAig, pFaninLits[0], pFaninLits[1], pFaninLits[2], nSuppAll ); @@ -2243,7 +2244,8 @@ int If_CutDsdBalanceEval_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pnSup Delays[i] = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea, pPermLits ); if ( Delays[i] == -1 ) return -1; - pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) ); + if ( vAig ) + pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) ); } return If_CutSopBalanceEvalInt( vCover, Delays, pFaninLits, vAig, piLit, nSuppAll, pArea ); } @@ -2258,8 +2260,9 @@ int If_CutDsdBalanceEval_rec( If_DsdMan_t * p, int Id, int * pTimes, int * pnSup Delay = If_CutDsdBalanceEval_rec( p, Abc_Lit2Var(iFanin), pTimes, pnSupp, vAig, pFaninLits+i, nSuppAll, pArea, pPermLits ); if ( Delay == -1 ) return -1; - pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) ); - Result = If_LogCounterAddAig( pCounter, &nCounter, pFaninLits, Delay, pFaninLits[i], vAig, nSuppAll, fXor, fXorFunc ); + if ( vAig ) + pFaninLits[i] = Abc_LitNotCond( pFaninLits[i], Abc_LitIsCompl(iFanin) ); + Result = If_LogCounterAddAig( pCounter, &nCounter, pFaninLits, Delay, vAig ? pFaninLits[i] : -1, vAig, nSuppAll, fXor, fXorFunc ); } assert( nCounter > 0 ); if ( fXor ) |