New assertions and bug fix in DSD balancing.

This commit is contained in:
Alan Mishchenko
2015-01-27 09:54:35 -08:00
parent 8ff4b79fc2
commit 0f22046bcb
9 changed files with 90 additions and 16 deletions
+3 -3
View File
@@ -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 )
+8 -5
View File
@@ -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 )