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

Dumping miter statistics.

This commit is contained in:
Alan Mishchenko 2024-04-22 22:06:07 -04:00
parent 6699c07b92
commit c14d5f3906
3 changed files with 58 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -38250,7 +38250,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500, nMaxNodes = 0;
Cec4_ManSetParams( pPars );
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMrmdckngxysopwqvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMFrmdckngxysopwqvh" ) ) != EOF )
{
switch ( c )
{
@ -38364,6 +38364,15 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nMaxNodes < 0 )
goto usage;
break;
case 'F':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
goto usage;
}
pPars->pDumpName = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'r':
pPars->fRewriting ^= 1;
break;
@ -38405,7 +38414,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
break;
case 'q':
pPars->fBMiterInfo ^= 1;
break;
break;
case 'v':
pPars->fVerbose ^= 1;
break;
@ -38445,7 +38454,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
return 0;
usage:
Abc_Print( -2, "usage: &fraig [-JWRILDCNPM <num>] [-rmdckngxysopwvh]\n" );
Abc_Print( -2, "usage: &fraig [-JWRILDCNPM <num>] [-F filename] [-rmdckngxysopwvh]\n" );
Abc_Print( -2, "\t performs combinational SAT sweeping\n" );
Abc_Print( -2, "\t-J num : the solver type [default = %d]\n", pPars->jType );
Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
@ -38457,6 +38466,7 @@ usage:
Abc_Print( -2, "\t-N num : the min number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle );
Abc_Print( -2, "\t-P num : the number of pattern generation iterations [default = %d]\n", pPars->nGenIters );
Abc_Print( -2, "\t-M num : the node count limit to call the old sweeper [default = %d]\n", nMaxNodes );
Abc_Print( -2, "\t-F file: the file name to dump primary output information [default = none]\n" );
Abc_Print( -2, "\t-r : toggle the use of AIG rewriting [default = %s]\n", pPars->fRewriting? "yes": "no" );
Abc_Print( -2, "\t-m : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" );
Abc_Print( -2, "\t-d : toggle using double output miters [default = %s]\n", pPars->fDualOut? "yes": "no" );

1
src/proof/cec/cec.h
View File

@ -122,6 +122,7 @@ struct Cec_ParFra_t_
int iOutFail; // the failed output
int fBMiterInfo; // printing BMiter information
int nPO; // number of po in original design given a bmiter
char * pDumpName; // file name to dump statistics
};
// combinational equivalence checking parameters

44
src/proof/cec/cecSatG2.c
View File

@ -1783,6 +1783,48 @@ void Gia_ManRemoveWrongChoices( Gia_Man_t * p )
//Abc_Print( 1, "Removed %d wrong choices.\n", Counter );
}
void Cec4_ManSimulateDumpInfo( Cec4_Man_t * pMan )
{
Gia_Obj_t * pObj; int i, k, nWords = pMan->pAig->nSimWords, nOuts[2] = {0};
Vec_Wrd_t * vSims = NULL, * vSimsPi = NULL;
FILE * pFile = fopen( pMan->pPars->pDumpName, "wb" );
if ( pFile == NULL ) {
printf( "Cannot open file \"%s\" for writing primary output information.\n", pMan->pPars->pDumpName );
return;
}
vSimsPi = Vec_WrdDup( pMan->pAig->vSimsPi );
memmove( Vec_WrdArray(vSimsPi), Vec_WrdArray(vSimsPi) + nWords, Gia_ManCiNum(pMan->pAig) * nWords );
Vec_WrdShrink( vSimsPi, Gia_ManCiNum(pMan->pAig) * nWords );
if ( Abc_TtIsConst0(Vec_WrdArray(vSimsPi), Gia_ManCiNum(pMan->pAig) * nWords) ) {
Vec_WrdFree( vSimsPi );
vSimsPi = Vec_WrdStartRandom( Gia_ManCiNum(pMan->pAig) * nWords );
}
vSims = Gia_ManSimPatSimOut( pMan->pAig, vSimsPi, 1 );
assert( nWords * Gia_ManCiNum(pMan->pAig) == Vec_WrdSize(vSimsPi) );
Gia_ManForEachCo( pMan->pAig, pObj, i )
{
void Extra_PrintHex2( FILE * pFile, unsigned * pTruth, int nVars );
word * pSims = Vec_WrdEntryP( vSims, nWords*i );
//Extra_PrintHex2( stdout, (unsigned *)pSims, 8 ); printf( "\n" );
fprintf( pFile, "%d ", i );
if ( Gia_ObjFaninLit0p(pMan->pNew, Gia_ManCo(pMan->pNew, i)) == 0 )
nOuts[0]++;
else if ( Abc_TtIsConst0(pSims, nWords) )
fprintf( pFile, "-" );
else {
int iPat = Abc_TtFindFirstBit2(pSims, nWords);
for ( k = 0; k < Gia_ManPiNum(pMan->pAig); k++ )
fprintf( pFile, "%d", Abc_TtGetBit(Vec_WrdEntryP(vSimsPi, nWords*k), iPat) );
nOuts[1]++;
}
fprintf( pFile, "\n" );
}
printf( "Information about %d sat, %d unsat, and %d undecided primary outputs was written into file \"%s\".\n",
nOuts[1], nOuts[0], Gia_ManCoNum(pMan->pAig)-nOuts[1]-nOuts[0], pMan->pPars->pDumpName );
fclose( pFile );
Vec_WrdFree( vSims );
Vec_WrdFree( vSimsPi );
}
int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** ppNew, int fSimOnly )
{
@ -1954,6 +1996,8 @@ finalize:
ABC_FREE( pBase );
printf( "Dumped miter \"%s\" with %d pairs.\n", pFileName, pMan->vPairs ? Vec_IntSize(pMan->vPairs)/2 : -1 );
}
if ( pPars->pDumpName )
Cec4_ManSimulateDumpInfo( pMan );
Cec4_ManDestroy( pMan );
//Gia_ManStaticFanoutStop( p );
//Gia_ManEquivPrintClasses( p, 1, 0 );