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

Minor tuning in 'satclp'.

This commit is contained in:
Alan Mishchenko 2015-10-22 11:45:23 -07:00
parent 2c37498bfb
commit 1332dc419f
3 changed files with 21 additions and 13 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
src/base/abci/abc.c
View File

@ -3177,7 +3177,7 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pNtkRes == NULL ) if ( pNtkRes == NULL )
{ {
Abc_Print( -1, "Collapsing has failed.\n" ); Abc_Print( -1, "Collapsing has failed.\n" );
return 1; return 0;
} }
// replace the current network // replace the current network
Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes ); Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@ -8290,7 +8290,7 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( !Abc_NtkToSop(pNtk, fMode, nCubeLimit) ) if ( !Abc_NtkToSop(pNtk, fMode, nCubeLimit) )
{ {
Abc_Print( -1, "Converting to SOP has failed.\n" ); Abc_Print( -1, "Converting to SOP has failed.\n" );
return 1; return 0;
} }
return 0; return 0;

2
src/base/abci/abcCollapse.c
View File

@ -298,7 +298,7 @@ Vec_Str_t * Abc_NtkClpOne( Abc_Ntk_t * pNtk, int iCo, int nCubeLim, int nBTLimit
extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose ); extern Vec_Str_t * Bmc_CollapseOne( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose );
Gia_Man_t * pGia = Abc_NtkClpOneGia( pNtk, iCo, vSupp ); Gia_Man_t * pGia = Abc_NtkClpOneGia( pNtk, iCo, vSupp );
if ( fVerbose ) if ( fVerbose )
printf( "Output %d: \n", iCo ); printf( "Output %4d: Supp = %4d. Cone =%6d.\n", iCo, Vec_IntSize(vSupp), Gia_ManAndNum(pGia) );
vSop = Bmc_CollapseOne( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose ); vSop = Bmc_CollapseOne( pGia, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose );
Gia_ManStop( pGia ); Gia_ManStop( pGia );
if ( vSop == NULL ) if ( vSop == NULL )

28
src/sat/bmc/bmcClp.c
View File

@ -624,17 +624,25 @@ cleanup:
vRes = vSop[fComplete[1]]; vSop[fComplete[1]] = NULL; vRes = vSop[fComplete[1]]; vSop[fComplete[1]] = NULL;
if ( iCube > 1 ) if ( iCube > 1 )
Bmc_CollapseIrredundant( vRes, Vec_StrSize(vRes)/(nVars +3), nVars ); Bmc_CollapseIrredundant( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
if ( fVeryVerbose ) }
if ( fVeryVerbose )
{
int fProfile = 0;
printf( "Processed output with %d supp vars. ", nVars );
if ( vRes == NULL )
printf( "The resulting SOP exceeded %d cubes.\n", nCubeLim );
else
printf( "The best cover contains %d cubes.\n", iCube );
Abc_PrintTime( 1, "Onset minterm", Time[0][0] );
Abc_PrintTime( 1, "Onset expand ", Time[0][1] );
Abc_PrintTime( 1, "Offset minterm", Time[1][0] );
Abc_PrintTime( 1, "Offset expand ", Time[1][1] );
if ( fProfile )
{ {
printf( "Processed output with %d supp vars and %d cubes.\n", nVars, Vec_StrSize(vRes)/(nVars +3) ); Abc_PrintTime( 1, "Expand check1 ", clkCheck1 ); clkCheck1 = 0;
Abc_PrintTime( 1, "Onset minterm", Time[0][0] ); Abc_PrintTime( 1, "Expand check2 ", clkCheck2 ); clkCheck2 = 0;
Abc_PrintTime( 1, "Onset expand ", Time[0][1] ); Abc_PrintTime( 1, "Expand sat ", clkCheckS ); clkCheckS = 0;
Abc_PrintTime( 1, "Offset minterm", Time[1][0] ); Abc_PrintTime( 1, "Expand unsat ", clkCheckU ); clkCheckU = 0;
Abc_PrintTime( 1, "Offset expand ", Time[1][1] );
//Abc_PrintTime( 1, "Expand check1 ", clkCheck1 ); clkCheck1 = 0;
//Abc_PrintTime( 1, "Expand check2 ", clkCheck2 ); clkCheck2 = 0;
//Abc_PrintTime( 1, "Expand sat ", clkCheckS ); clkCheckS = 0;
//Abc_PrintTime( 1, "Expand unsat ", clkCheckU ); clkCheckU = 0;
} }
} }
Vec_StrFreeP( &vSop[0] ); Vec_StrFreeP( &vSop[0] );