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

Small fixes and a change to &cec to allow two files names given as command-line arguments.

This commit is contained in:
Alan Mishchenko 2017-01-21 11:59:01 +08:00
parent b193ef056d
commit a28be94ac7
4 changed files with 103 additions and 54 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
src/aig/gia/giaIf.c
View File

@ -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();
}

2
src/aig/gia/giaTim.c
View File

@ -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 );

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

@ -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 )
{
if ( pAbc->pGia->pSpec == NULL )
{
Abc_Print( -1, "File name is not given on the command line.\n" );
return 1;
}
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" );
Abc_Print( -1, "Abc_CommandAbc9Cec(): Wrong number of command-line arguments.\n" );
return 1;
}
fclose( pFile );
pSecond = Gia_AigerRead( FileName, 0, 0, 0 );
if ( pSecond == NULL )
if ( nArgcNew == 2 )
{
Abc_Print( -1, "Reading AIGER has failed.\n" );
return 0;
char * pFileNames[2] = { pArgvNew[0], pArgvNew[1] }, * pTemp;
int n;
for ( n = 0; n < 2; n++ )
{
// 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;
}
}
}
else
{
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 );

14
src/base/abci/abcVerify.c
View File

@ -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 );