diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 5ff1f3fd1..eb2b7480d 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -35021,7 +35021,7 @@ usage: ***********************************************************************/ int Abc_CommandAbc9SimRsb( Abc_Frame_t * pAbc, int argc, char ** argv ) { - extern void Gia_ManSimRsb( Gia_Man_t * p, int nCands, int fVerbose ); + extern int Gia_ManSimRsb( Gia_Man_t * p, int nCands, int fVerbose ); int c, nCands = 32, fVerbose = 0; Extra_UtilGetoptReset(); while ( ( c = Extra_UtilGetopt( argc, argv, "Nvh" ) ) != EOF ) @@ -38259,7 +38259,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 ) { @@ -38373,6 +38373,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; @@ -38414,7 +38423,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; @@ -38454,7 +38463,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &fraig [-JWRILDCNPM ] [-rmdckngxysopwvh]\n" ); + Abc_Print( -2, "usage: &fraig [-JWRILDCNPM ] [-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 ); @@ -38466,6 +38475,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" ); diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c index 8f5e4ee2e..b429b062e 100644 --- a/src/base/abci/abcMap.c +++ b/src/base/abci/abcMap.c @@ -24,6 +24,7 @@ #include "map/mapper/mapper.h" #include "misc/util/utilNam.h" #include "map/scl/sclCon.h" +#include "map/scl/sclLib.h" ABC_NAMESPACE_IMPL_START diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c index a18387acd..4a34f9cfd 100644 --- a/src/base/cmd/cmd.c +++ b/src/base/cmd/cmd.c @@ -51,7 +51,7 @@ static int CmdCommandUnsetVariable ( Abc_Frame_t * pAbc, int argc, char ** argv static int CmdCommandUndo ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int CmdCommandRecall ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int CmdCommandEmpty ( Abc_Frame_t * pAbc, int argc, char ** argv ); -#if defined(WIN32) && !defined(__cplusplus) +#if defined(WIN32) static int CmdCommandScanDir ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int CmdCommandRenameFiles ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int CmdCommandLs ( Abc_Frame_t * pAbc, int argc, char ** argv ); @@ -105,7 +105,7 @@ void Cmd_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Basic", "undo", CmdCommandUndo, 0 ); Cmd_CommandAdd( pAbc, "Basic", "recall", CmdCommandRecall, 0 ); Cmd_CommandAdd( pAbc, "Basic", "empty", CmdCommandEmpty, 0 ); -#if defined(WIN32) && !defined(__cplusplus) +#if defined(WIN32) Cmd_CommandAdd( pAbc, "Basic", "scandir", CmdCommandScanDir, 0 ); Cmd_CommandAdd( pAbc, "Basic", "renamefiles", CmdCommandRenameFiles, 0 ); Cmd_CommandAdd( pAbc, "Basic", "ls", CmdCommandLs, 0 ); @@ -1209,7 +1209,7 @@ usage: #endif -#if defined(WIN32) && !defined(__cplusplus) +#if defined(WIN32) #include #include @@ -1395,10 +1395,10 @@ int CmfFindNumber( char * pName ) ***********************************************************************/ void CnfDupFileUnzip( char * pOldName ) { - extern char * Io_MvLoadFileBz2( char * pFileName, int * pnFileSize ); + extern char * Io_MvLoadFileBz2( char * pFileName, long * pnFileSize ); char pNewName[1000]; FILE * pFile; - int nFileSize; + long nFileSize; char * pBuffer = Io_MvLoadFileBz2( pOldName, &nFileSize ); assert( strlen(pOldName) < 1000 ); sprintf( pNewName, "%s.v", pOldName ); diff --git a/src/map/mio/mio.h b/src/map/mio/mio.h index 18e3b92b0..1a072a502 100644 --- a/src/map/mio/mio.h +++ b/src/map/mio/mio.h @@ -230,8 +230,6 @@ extern void Mio_LibraryMatches2Fetch( Mio_Library_t * pLib, Vec_Ptr /*=== sclUtil.c =========================================================*/ extern Mio_Library_t * Abc_SclDeriveGenlibSimple( void * pScl ); extern Mio_Library_t * Abc_SclDeriveGenlib( void * pScl, void * pMio, float Slew, float Gain, int nGatesMin, int fVerbose ); -extern int Abc_SclHasDelayInfo( void * pScl ); - ABC_NAMESPACE_HEADER_END diff --git a/src/map/scl/sclLibScl.c b/src/map/scl/sclLibScl.c index 1dc57e483..144ec7f55 100644 --- a/src/map/scl/sclLibScl.c +++ b/src/map/scl/sclLibScl.c @@ -570,7 +570,7 @@ int Abc_SclCountValidCells( SC_Lib * p ) n_valid_cells++; return n_valid_cells; } -static void Abc_SclWriteLibrary( Vec_Str_t * vOut, SC_Lib * p, int nExtra ) +static void Abc_SclWriteLibrary( Vec_Str_t * vOut, SC_Lib * p, int nExtra, int fUsePrefix ) { SC_WireLoad * pWL; SC_WireLoadSel * pWLS; @@ -624,13 +624,13 @@ static void Abc_SclWriteLibrary( Vec_Str_t * vOut, SC_Lib * p, int nExtra ) // Write 'cells' vector: n_valid_cells = Abc_SclCountValidCells( p ); Vec_StrPutI( vOut, n_valid_cells + nExtra ); - Abc_SclWriteLibraryCellsOnly( vOut, p, (int)(nExtra > 0) ); + Abc_SclWriteLibraryCellsOnly( vOut, p, fUsePrefix ? 1 : 0 ); } void Abc_SclWriteScl( char * pFileName, SC_Lib * p ) { Vec_Str_t * vOut; vOut = Vec_StrAlloc( 10000 ); - Abc_SclWriteLibrary( vOut, p, 0 ); + Abc_SclWriteLibrary( vOut, p, 0, 0 ); if ( Vec_StrSize(vOut) > 0 ) { FILE * pFile = fopen( pFileName, "wb" ); @@ -870,7 +870,7 @@ SC_Lib * Abc_SclMergeLibraries( SC_Lib * pLib1, SC_Lib * pLib2, int fUsePrefix ) { Vec_Str_t * vOut = Vec_StrAlloc( 10000 ); int n_valid_cells2 = Abc_SclCountValidCells( pLib2 ); - Abc_SclWriteLibrary( vOut, pLib1, n_valid_cells2 ); + Abc_SclWriteLibrary( vOut, pLib1, n_valid_cells2, fUsePrefix ); Abc_SclWriteLibraryCellsOnly( vOut, pLib2, fUsePrefix ? 2 : 0 ); SC_Lib * p = Abc_SclReadFromStr( vOut ); p->pFileName = Abc_UtilStrsav( pLib1->pFileName ); diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h index c9aa96658..10101e6c0 100644 --- a/src/proof/cec/cec.h +++ b/src/proof/cec/cec.h @@ -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 diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index b198c7ffe..554fd550d 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -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 );