luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Bug fix in 'dsd_tune' when processing cells with 0-input LUTs.

This commit is contained in:
Alan Mishchenko 2015-05-15 22:36:11 -07:00
parent 37b6b5f1f8
commit 14b7a520a1
1 changed files with 7 additions and 2 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

9
src/map/if/ifTune.c
View File

@ -1111,9 +1111,10 @@ int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat )
int i, f, v, nLits, pLits[IFN_INS+2], pLits2[IFN_INS+2];
// assign new variables
int nSatVars = sat_solver_nvars(pSat);
for ( i = 0; i < p->nObjs-1; i++ )
// for ( i = 0; i < p->nObjs-1; i++ )
for ( i = 0; i < p->nObjs; i++ )
p->Nodes[i].Var = nSatVars++;
p->Nodes[p->nObjs-1].Var = 0xFFFF;
//p->Nodes[p->nObjs-1].Var = 0xFFFF;
sat_solver_setnvars( pSat, nSatVars );
// verify variable values
for ( i = 0; i < p->nVars; i++ )
@ -1237,6 +1238,10 @@ int Ifn_NtkAddClauses( Ifn_Ntk_t * p, int * pValues, sat_solver * pSat )
else assert( 0 );
//printf( "\n" );
}
// add last clause (not needed if the root node is IFN_DSD_PRIME)
pLits[0] = Abc_Var2Lit( p->Nodes[p->nObjs-1].Var, pValues[p->nObjs-1]==0 );
if ( !Ifn_AddClause( pSat, pLits, pLits + 1 ) )
return 0;
return 1;
}