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

Adding logfile dump to print_status.

This commit is contained in:
Alan Mishchenko 2019-11-25 17:54:18 +07:00
parent 4deaaa852a
commit 787e3e1d12
2 changed files with 70 additions and 7 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -2819,15 +2819,26 @@ usage:
***********************************************************************/
int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern void Abc_NtkDumpOneCexSpecial( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex );
extern void Abc_NtkPrintPoEquivs( Abc_Ntk_t * pNtk );
Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
int c, fOutStatus = 0, fShort = 1;
char * pLogFileName = NULL;
// set defaults
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "osh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "Losh" ) ) != EOF )
{
switch ( c )
{
case 'L':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-L\" should be followed by a file name.\n" );
goto usage;
}
pLogFileName = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'o':
fOutStatus ^= 1;
break;
@ -2883,7 +2894,32 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
}
if ( pAbc->vStatuses )
{
if ( fShort )
if ( pLogFileName )
{
Abc_Cex_t * pTemp = NULL;
FILE * pFile = fopen( pLogFileName, "wb" );
if ( pFile == NULL )
{
printf( "Cannot open file \"%s\" for writing.\n", pLogFileName );
return 0;
}
Vec_PtrForEachEntry( Abc_Cex_t *, pAbc->vCexVec, pTemp, c )
{
int Status = Vec_IntEntry( pAbc->vStatuses, c );
if ( Status == -1 ) // undec
fprintf( pFile, "STATUS: ABORTED " );
else if ( Status == 0 )
fprintf( pFile, "STATUS: SAT " );
else if ( Status == 1 )
fprintf( pFile, "STATUS: UNSAT " );
fprintf( pFile, "%s\n", Abc_ObjName(Abc_NtkPo(pNtk, c)) );
if ( Status != 0 )
continue;
Abc_NtkDumpOneCexSpecial( pFile, pNtk, pTemp );
}
fclose( pFile );
}
else if ( fShort )
{
printf( "Status array contains %d SAT, %d UNSAT, and %d UNDEC entries (out of %d).",
Vec_IntCountEntry(pAbc->vStatuses, 0), Vec_IntCountEntry(pAbc->vStatuses, 1),
@ -2900,11 +2936,12 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: print_status [-osh]\n" );
Abc_Print( -2, "\t prints verification status\n" );
Abc_Print( -2, "\t-o : toggle printing output status [default = %s]\n", fOutStatus? "yes": "no" );
Abc_Print( -2, "\t-s : toggle using short print-out [default = %s]\n", fShort? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Abc_Print( -2, "usage: print_status [-L file] [-osh]\n" );
Abc_Print( -2, "\t prints verification status\n" );
Abc_Print( -2, "\t-L file : the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
Abc_Print( -2, "\t-o : toggle printing output status [default = %s]\n", fOutStatus? "yes": "no" );
Abc_Print( -2, "\t-s : toggle using short print-out [default = %s]\n", fShort? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
return 1;
}

26
src/base/io/io.c
View File

@ -2326,6 +2326,32 @@ int Abc_NtkCheckSpecialPi( Abc_Ntk_t * pNtk )
SeeAlso []
***********************************************************************/
void Abc_NtkDumpOneCexSpecial( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex )
{
Abc_Cex_t * pCare = NULL; int i, f; Abc_Obj_t * pObj;
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
//fprintf( pFile, "# FALSIFYING OUTPUTS:");
//fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) );
pCare = Bmc_CexCareMinimize( pAig, Saig_ManPiNum(pAig), pCex, 4, 0, 0 );
Aig_ManStop( pAig );
if( pCare == NULL )
{
printf( "Counter-example minimization has failed.\n" );
return;
}
// output flop values (unaffected by the minimization)
Abc_NtkForEachLatch( pNtk, pObj, i )
fprintf( pFile, "CEX: %s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) );
// output PI values (while skipping the minimized ones)
for ( f = 0; f <= pCex->iFrame; f++ )
Abc_NtkForEachPi( pNtk, pObj, i )
if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) )
fprintf( pFile, "CEX: %s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
Abc_CexFreeP( &pCare );
}
void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex,
int fPrintFull, int fNames, int fUseFfNames, int fMinimize, int fUseOldMin,
int fCheckCex, int fUseSatBased, int fHighEffort, int fAiger, int fVerbose )