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

Merge remote-tracking branch 'origin/master' into yosys-flow

This commit is contained in:
aletempiac 2024-05-02 10:23:16 +02:00
parent 714ab458b7 516c38bb44
commit 5708841672
7 changed files with 69 additions and 15 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

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

1
src/base/abci/abcMap.c
View File

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

10
src/base/cmd/cmd.c
View File

@ -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 <direct.h>
#include <io.h>
@ -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 );

2
src/map/mio/mio.h
View File

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

8
src/map/scl/sclLibScl.c
View File

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

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