From a28be94ac79c0cbb0960565573985838d7a27a79 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 21 Jan 2017 11:59:01 +0800 Subject: Small fixes and a change to &cec to allow two files names given as command-line arguments. --- src/aig/gia/giaIf.c | 16 +++--- src/aig/gia/giaTim.c | 2 + src/base/abci/abc.c | 121 +++++++++++++++++++++++++++++++--------------- src/base/abci/abcVerify.c | 14 ++++-- 4 files changed, 101 insertions(+), 52 deletions(-) (limited to 'src') diff --git a/src/aig/gia/giaIf.c b/src/aig/gia/giaIf.c index ac748f8c..ab80a762 100644 --- a/src/aig/gia/giaIf.c +++ b/src/aig/gia/giaIf.c @@ -544,20 +544,20 @@ void Gia_ManPrintMappingStats( Gia_Man_t * p, char * pDumpFile ) fprintf( pTable, "%d ", Gia_ManAndNum(p) ); fprintf( pTable, "%d ", nLuts ); fprintf( pTable, "%d ", Gia_ManLutLevelWithBoxes(p) ); - fprintf( pTable, "%d ", Gia_ManRegBoxNum(p) ); - fprintf( pTable, "%d ", Gia_ManNonRegBoxNum(p) ); - fprintf( pTable, "%.2f", 1.0*(Abc_Clock() - clk)/CLOCKS_PER_SEC ); + //fprintf( pTable, "%d ", Gia_ManRegBoxNum(p) ); + //fprintf( pTable, "%d ", Gia_ManNonRegBoxNum(p) ); + //fprintf( pTable, "%.2f", 1.0*(Abc_Clock() - clk)/CLOCKS_PER_SEC ); clk = Abc_Clock(); } else { - printf( "This part of the code is currently not used.\n" ); - assert( 0 ); + //printf( "This part of the code is currently not used.\n" ); + //assert( 0 ); fprintf( pTable, " " ); fprintf( pTable, "%d ", nLuts ); - fprintf( pTable, "%d ", LevelMax ); - fprintf( pTable, "%d ", Gia_ManRegBoxNum(p) ); - fprintf( pTable, "%d ", Gia_ManNonRegBoxNum(p) ); + fprintf( pTable, "%d ", Gia_ManLutLevelWithBoxes(p) ); + //fprintf( pTable, "%d ", Gia_ManRegBoxNum(p) ); + //fprintf( pTable, "%d ", Gia_ManNonRegBoxNum(p) ); fprintf( pTable, "%.2f", 1.0*(Abc_Clock() - clk)/CLOCKS_PER_SEC ); clk = Abc_Clock(); } diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c index 71b9a475..29aa93f8 100644 --- a/src/aig/gia/giaTim.c +++ b/src/aig/gia/giaTim.c @@ -584,6 +584,8 @@ int Gia_ManLutLevelWithBoxes( Gia_Man_t * p ) Gia_Obj_t * pObj, * pObjIn; int i, k, j, curCi, curCo, LevelMax; assert( Gia_ManRegNum(p) == 0 ); + if ( pManTime == NULL ) + return Gia_ManLutLevel(p, NULL); // copy const and real PIs Gia_ManCleanLevels( p, Gia_ManObjNum(p) ); Gia_ObjSetLevel( p, Gia_ManConst0(p), 0 ); diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 58a14e81..806a5de7 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -32927,8 +32927,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) { Cec_ParCec_t ParsCec, * pPars = &ParsCec; FILE * pFile; - Gia_Man_t * pSecond, * pMiter; - char * FileName, * pTemp; + Gia_Man_t * pGias[2] = {NULL, NULL}, * pMiter; char ** pArgvNew; int c, nArgcNew, fMiter = 0, fDualOutput = 0, fDumpMiter = 0; Cec_ManCecSetDefaultParams( pPars ); @@ -32983,13 +32982,15 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) goto usage; } } - if ( pAbc->pGia == NULL ) - { - Abc_Print( -1, "Abc_CommandAbc9Cec(): There is no AIG.\n" ); - return 1; - } + pArgvNew = argv + globalUtilOptind; + nArgcNew = argc - globalUtilOptind; if ( fMiter ) { + if ( pAbc->pGia == NULL || nArgcNew != 0 ) + { + Abc_Print( -1, "Abc_CommandAbc9Cec(): A miter cannot be given as an argument of command &cec and should be entered using &r.\n" ); + return 1; + } if ( fDualOutput ) { if ( Gia_ManPoNum(pAbc->pGia) & 1 ) @@ -32998,14 +32999,14 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) return 1; } if ( !pPars->fSilent ) - Abc_Print( 1, "Assuming the current network is a double-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit ); + Abc_Print( 1, "Assuming the current network is a double-output miter.\n" ); pAbc->Status = Cec_ManVerify( pAbc->pGia, pPars ); } else { Gia_Man_t * pTemp; if ( !pPars->fSilent ) - Abc_Print( 1, "Assuming the current network is a single-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit ); + Abc_Print( 1, "Assuming the current network is a single-output miter.\n" ); pTemp = Gia_ManDemiterToDual( pAbc->pGia ); pAbc->Status = Cec_ManVerify( pTemp, pPars ); ABC_SWAP( Abc_Cex_t *, pAbc->pGia->pCexComb, pTemp->pCexComb ); @@ -33014,41 +33015,81 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb ); return 0; } - - pArgvNew = argv + globalUtilOptind; - nArgcNew = argc - globalUtilOptind; - if ( nArgcNew != 1 ) + if ( nArgcNew > 2 ) + { + Abc_Print( -1, "Abc_CommandAbc9Cec(): Wrong number of command-line arguments.\n" ); + return 1; + } + if ( nArgcNew == 2 ) { - if ( pAbc->pGia->pSpec == NULL ) + char * pFileNames[2] = { pArgvNew[0], pArgvNew[1] }, * pTemp; + int n; + for ( n = 0; n < 2; n++ ) { - Abc_Print( -1, "File name is not given on the command line.\n" ); - return 1; + // fix the wrong symbol + for ( pTemp = pFileNames[n]; *pTemp; pTemp++ ) + if ( *pTemp == '>' ) + *pTemp = '\\'; + if ( (pFile = fopen( pFileNames[n], "r" )) == NULL ) + { + Abc_Print( -1, "Cannot open input file \"%s\". ", pFileNames[n] ); + if ( (pFileNames[n] = Extra_FileGetSimilarName( pFileNames[n], ".aig", NULL, NULL, NULL, NULL )) ) + Abc_Print( 1, "Did you mean \"%s\"?", pFileNames[n] ); + Abc_Print( 1, "\n" ); + return 1; + } + fclose( pFile ); + pGias[n] = Gia_AigerRead( pFileNames[n], 0, 0, 0 ); + if ( pGias[n] == NULL ) + { + Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", pFileNames[n] ); + return 0; + } } - FileName = pAbc->pGia->pSpec; } else - FileName = pArgvNew[0]; - // fix the wrong symbol - for ( pTemp = FileName; *pTemp; pTemp++ ) - if ( *pTemp == '>' ) - *pTemp = '\\'; - if ( (pFile = fopen( FileName, "r" )) == NULL ) - { - Abc_Print( -1, "Cannot open input file \"%s\". ", FileName ); - if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", NULL, NULL, NULL, NULL )) ) - Abc_Print( 1, "Did you mean \"%s\"?", FileName ); - Abc_Print( 1, "\n" ); - return 1; - } - fclose( pFile ); - pSecond = Gia_AigerRead( FileName, 0, 0, 0 ); - if ( pSecond == NULL ) { - Abc_Print( -1, "Reading AIGER has failed.\n" ); - return 0; + char * FileName, * pTemp; + if ( pAbc->pGia == NULL ) + { + Abc_Print( -1, "Abc_CommandAbc9Cec(): There is no current AIG.\n" ); + return 1; + } + pGias[0] = pAbc->pGia; + if ( nArgcNew == 1 ) + FileName = pArgvNew[0]; + else + { + assert( nArgcNew == 0 ); + if ( pAbc->pGia->pSpec == NULL ) + { + Abc_Print( -1, "File name is not given on the command line.\n" ); + return 1; + } + FileName = pAbc->pGia->pSpec; + } + // fix the wrong symbol + for ( pTemp = FileName; *pTemp; pTemp++ ) + if ( *pTemp == '>' ) + *pTemp = '\\'; + if ( (pFile = fopen( FileName, "r" )) == NULL ) + { + Abc_Print( -1, "Cannot open input file \"%s\". ", FileName ); + if ( (FileName = Extra_FileGetSimilarName( FileName, ".aig", NULL, NULL, NULL, NULL )) ) + Abc_Print( 1, "Did you mean \"%s\"?", FileName ); + Abc_Print( 1, "\n" ); + return 1; + } + fclose( pFile ); + pGias[1] = Gia_AigerRead( FileName, 0, 0, 0 ); + if ( pGias[1] == NULL ) + { + Abc_Print( -1, "Reading AIGER has failed.\n" ); + return 0; + } } // compute the miter - pMiter = Gia_ManMiter( pAbc->pGia, pSecond, 0, 1, 0, 0, pPars->fVerbose ); + pMiter = Gia_ManMiter( pGias[0], pGias[1], 0, 1, 0, 0, pPars->fVerbose ); if ( pMiter ) { if ( fDumpMiter ) @@ -33057,10 +33098,12 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0 ); } pAbc->Status = Cec_ManVerify( pMiter, pPars ); - Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb ); + Abc_FrameReplaceCex( pAbc, &pGias[0]->pCexComb ); Gia_ManStop( pMiter ); } - Gia_ManStop( pSecond ); + if ( pGias[0] != pAbc->pGia ) + Gia_ManStop( pGias[0] ); + Gia_ManStop( pGias[1] ); return 0; usage: @@ -36178,7 +36221,7 @@ int Abc_CommandAbc9SatLut( Abc_Frame_t * pAbc, int argc, char ** argv ) usage: Abc_Print( -2, "usage: &satlut [-NICDQ num] [-drwvh]\n" ); - Abc_Print( -2, "\t performs SAT-based remapping of the 4-LUT network\n" ); + Abc_Print( -2, "\t performs SAT-based remapping of the LUT-mapped network\n" ); Abc_Print( -2, "\t-N num : the limit on AIG nodes in the window (num <= 128) [default = %d]\n", nNumber ); Abc_Print( -2, "\t-I num : the limit on the number of improved windows [default = %d]\n", nImproves ); Abc_Print( -2, "\t-C num : the limit on the number of conflicts [default = %d]\n", nBTLimit ); diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c index 25d1d113..7199c529 100644 --- a/src/base/abci/abcVerify.c +++ b/src/base/abci/abcVerify.c @@ -122,6 +122,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI ***********************************************************************/ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fVerbose ) { + abctime clk = Abc_Clock(); Prove_Params_t Params, * pParams = &Params; // Fraig_Params_t Params; // Fraig_Man_t * pMan; @@ -170,18 +171,20 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV RetValue = Abc_NtkMiterIsConstant( pMiter ); if ( RetValue == 0 ) { - printf( "Networks are NOT EQUIVALENT after structural hashing.\n" ); + printf( "Networks are NOT EQUIVALENT after structural hashing. " ); // report the error pMiter->pModel = Abc_NtkVerifyGetCleanModel( pMiter, 1 ); Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel ); ABC_FREE( pMiter->pModel ); Abc_NtkDelete( pMiter ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); return; } if ( RetValue == 1 ) { - printf( "Networks are equivalent after structural hashing.\n" ); + printf( "Networks are equivalent after structural hashing. " ); Abc_NtkDelete( pMiter ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); return; } /* @@ -220,18 +223,19 @@ void Abc_NtkCecFraig( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nSeconds, int fV // pParams->fVerbose = 1; RetValue = Abc_NtkIvyProve( &pMiter, pParams ); if ( RetValue == -1 ) - printf( "Networks are undecided (resource limits is reached).\n" ); + printf( "Networks are undecided (resource limits is reached). " ); else if ( RetValue == 0 ) { int * pSimInfo = Abc_NtkVerifySimulatePattern( pMiter, pMiter->pModel ); if ( pSimInfo[0] != 1 ) printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" ); else - printf( "Networks are NOT EQUIVALENT.\n" ); + printf( "Networks are NOT EQUIVALENT. " ); ABC_FREE( pSimInfo ); } else - printf( "Networks are equivalent.\n" ); + printf( "Networks are equivalent. " ); + Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); if ( pMiter->pModel ) Abc_NtkVerifyReportError( pNtk1, pNtk2, pMiter->pModel ); Abc_NtkDelete( pMiter ); -- cgit v1.2.3