mirror of https://github.com/YosysHQ/abc.git
Merge remote-tracking branch 'upstream/master' into yosys-experimental
This commit is contained in:
Miodrag Milanovic
commit
180a6adb68
|
|
@ -1480,10 +1480,10 @@ Gia_Man_t * Gia_ManGenAdder( int nVars, int fSK, int fBK, int fHC, int fCarries,
|
|||
for ( k = 1; k < nVars; k++ )
|
||||
if ( pStore[i][k] >= 0 )
|
||||
Gia_ManGenPrefix( p, &pLits[2*k], &pLits[2*k+1], pLits[2*pStore[i][k]], pLits[2*pStore[i][k]+1] );
|
||||
for ( k = 0; k < nVars; k++ )
|
||||
Gia_ManAppendCo( p, k ? Gia_ManHashXor(p, pLitsI[2*k], pLits[2*(k-1)+1]) : pLitsI[2*k] );
|
||||
if ( fCarries )
|
||||
Gia_ManAppendCo( p, pLits[2*(k-1)+1] );
|
||||
for ( k = 0; k < nVars; k++ )
|
||||
Gia_ManAppendCo( p, k ? Gia_ManHashXor(p, pLitsI[2*k], pLits[2*(k-1)+1]) : pLitsI[2*k] );
|
||||
ABC_FREE( pStore );
|
||||
ABC_FREE( pLitsI );
|
||||
ABC_FREE( pLits );
|
||||
|
|
|
|||
|
|
@ -42615,7 +42615,87 @@ usage:
|
|||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModule, char * pDefines, int * pAbc_ReadAigerOrVerilogFileStatus )
|
||||
static Vec_Ptr_t * Abc_GiaDupNameVec( Vec_Ptr_t * vNames )
|
||||
{
|
||||
Vec_Ptr_t * vNew;
|
||||
char * pName;
|
||||
int i;
|
||||
if ( vNames == NULL )
|
||||
return NULL;
|
||||
vNew = Vec_PtrAlloc( Vec_PtrSize(vNames) );
|
||||
Vec_PtrForEachEntry( char *, vNames, pName, i )
|
||||
Vec_PtrPush( vNew, pName ? Abc_UtilStrsav(pName) : NULL );
|
||||
return vNew;
|
||||
}
|
||||
|
||||
static Gia_Man_t * Abc_GiaReorderInputsByName( Gia_Man_t * pFirst, Gia_Man_t * pSecond )
|
||||
{
|
||||
Vec_Int_t * vPiPerm;
|
||||
Gia_Man_t * pNew;
|
||||
char * pName1, * pName2;
|
||||
int * pUsed;
|
||||
int i, k, nPis, fDiff = 0;
|
||||
if ( pFirst == NULL || pSecond == NULL || pFirst->vNamesIn == NULL || pSecond->vNamesIn == NULL )
|
||||
return NULL;
|
||||
nPis = Gia_ManPiNum( pFirst );
|
||||
if ( nPis != Gia_ManPiNum(pSecond) )
|
||||
return NULL;
|
||||
if ( Vec_PtrSize(pFirst->vNamesIn) < nPis || Vec_PtrSize(pSecond->vNamesIn) < nPis )
|
||||
return NULL;
|
||||
vPiPerm = Vec_IntAlloc( nPis );
|
||||
pUsed = ABC_CALLOC( int, nPis );
|
||||
for ( i = 0; i < nPis; i++ )
|
||||
{
|
||||
pName1 = (char *)Vec_PtrEntry( pFirst->vNamesIn, i );
|
||||
if ( pName1 == NULL )
|
||||
break;
|
||||
for ( k = 0; k < nPis; k++ )
|
||||
{
|
||||
pName2 = (char *)Vec_PtrEntry( pSecond->vNamesIn, k );
|
||||
if ( pName2 && !pUsed[k] && !strcmp(pName1, pName2) )
|
||||
break;
|
||||
}
|
||||
if ( k == nPis )
|
||||
break;
|
||||
pUsed[k] = 1;
|
||||
Vec_IntPush( vPiPerm, k );
|
||||
fDiff |= (k != i);
|
||||
}
|
||||
ABC_FREE( pUsed );
|
||||
if ( i < nPis || !fDiff )
|
||||
{
|
||||
Vec_IntFree( vPiPerm );
|
||||
return NULL;
|
||||
}
|
||||
pNew = Gia_ManDupPerm( pSecond, vPiPerm );
|
||||
Vec_IntFree( vPiPerm );
|
||||
pNew->vNamesIn = Vec_PtrAlloc( Vec_PtrSize(pSecond->vNamesIn) );
|
||||
for ( i = 0; i < nPis; i++ )
|
||||
{
|
||||
pName1 = (char *)Vec_PtrEntry( pFirst->vNamesIn, i );
|
||||
Vec_PtrPush( pNew->vNamesIn, pName1 ? Abc_UtilStrsav(pName1) : NULL );
|
||||
}
|
||||
for ( i = nPis; i < Vec_PtrSize(pSecond->vNamesIn); i++ )
|
||||
{
|
||||
pName2 = (char *)Vec_PtrEntry( pSecond->vNamesIn, i );
|
||||
Vec_PtrPush( pNew->vNamesIn, pName2 ? Abc_UtilStrsav(pName2) : NULL );
|
||||
}
|
||||
pNew->vNamesOut = Abc_GiaDupNameVec( pSecond->vNamesOut );
|
||||
return pNew;
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
||||
Synopsis []
|
||||
|
||||
Description []
|
||||
|
||||
SideEffects []
|
||||
|
||||
SeeAlso []
|
||||
|
||||
***********************************************************************/
|
||||
static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileName2, char * pTopModule, char * pDefines, int * pAbc_ReadAigerOrVerilogFileStatus )
|
||||
{
|
||||
FILE * pFile;
|
||||
Gia_Man_t * pGia;
|
||||
|
|
@ -42646,14 +42726,20 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModu
|
|||
fVerilog = fSystemVerilog || Extra_FileIsType( pFileName, ".v", NULL, NULL );
|
||||
if ( fVerilog )
|
||||
{
|
||||
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
|
||||
Aig_Man_t * pAig = NULL;
|
||||
char pCommand[2000];
|
||||
int RetValue;
|
||||
int fSystemVerilog2 = pFileName2 && Extra_FileIsType( pFileName2, ".sv", NULL, NULL );
|
||||
// Save the original filename before changing it
|
||||
pOrigFileName = pFileName;
|
||||
snprintf( pCommand, sizeof(pCommand),
|
||||
"yosys -qp \"read_verilog %s%s %s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; techmap; memory -nomap; memory_map; dffunmap; opt_clean; opt_expr; aigmap; write_aiger -symbols _temp_.aig\"",
|
||||
"yosys -qp \"read_verilog %s%s %s%s%s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; techmap; memory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols _temp_.aig\"",
|
||||
pDefines ? "-D" : "", pDefines ? pDefines : "",
|
||||
fSystemVerilog ? "-sv " : "", pFileName, pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "" );
|
||||
(fSystemVerilog || fSystemVerilog2) ? "-sv " : "", pFileName,
|
||||
pFileName2 ? " " : "", pFileName2 ? pFileName2 : "",
|
||||
pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "",
|
||||
pFileName2 ? "delete t:\\$scopeinfo; " : "" );
|
||||
#if defined(__wasm)
|
||||
RetValue = 1;
|
||||
#else
|
||||
|
|
@ -42664,10 +42750,32 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pTopModu
|
|||
Abc_Print( -1, "Yosys command failed: \"%s\".\n", pCommand );
|
||||
return NULL;
|
||||
}
|
||||
pFileName = "_temp_.aig";
|
||||
if ( pFileName2 )
|
||||
{
|
||||
Abc_Ntk_t * pNtk = Io_Read( "_temp_.aig", IO_FILE_AIGER, 1, 0 );
|
||||
if ( pNtk == NULL )
|
||||
{
|
||||
Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", "_temp_.aig" );
|
||||
return NULL;
|
||||
}
|
||||
pAig = Abc_NtkToDar( pNtk, 0, 1 );
|
||||
Abc_NtkDelete( pNtk );
|
||||
if ( pAig == NULL )
|
||||
{
|
||||
Abc_Print( -1, "Converting the AIGER network into an internal AIG has failed.\n" );
|
||||
return NULL;
|
||||
}
|
||||
pGia = Gia_ManFromAig( pAig );
|
||||
Aig_ManStop( pAig );
|
||||
}
|
||||
else
|
||||
{
|
||||
pFileName = "_temp_.aig";
|
||||
pGia = Gia_AigerRead( pFileName, 0, 0, 0 );
|
||||
}
|
||||
}
|
||||
|
||||
pGia = Gia_AigerRead( pFileName, 0, 0, 0 );
|
||||
else
|
||||
pGia = Gia_AigerRead( pFileName, 0, 0, 0 );
|
||||
if ( pGia == NULL )
|
||||
{
|
||||
Abc_Print( -1, "Reading AIGER from file \"%s\" has failed.\n", pFileName );
|
||||
|
|
@ -42699,13 +42807,14 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
{
|
||||
extern void Cec_ManPrintCexSummary( Gia_Man_t * p, Abc_Cex_t * pCex, Cec_ParCec_t * pPars );
|
||||
Cec_ParCec_t ParsCec, * pPars = &ParsCec;
|
||||
FILE * pFile;
|
||||
Gia_Man_t * pGias[2] = {NULL, NULL}, * pMiter;
|
||||
char ** pArgvNew, * pTopModule = NULL, * pDefines = NULL;
|
||||
char ** pArgvNew, * pTopModule = NULL, * pDefines = NULL, * pFileName2 = NULL;
|
||||
int c, nArgcNew, fUseSim = 0, fUseNewX = 0, fUseNewY = 0, fMiter = 0, fDualOutput = 0, fDumpMiter = 0, fSavedSpec = 0;
|
||||
int Abc_ReadAigerOrVerilogFileStatus = 0;
|
||||
Cec_ManCecSetDefaultParams( pPars );
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "CTMDnmdbasxytvwh" ) ) != EOF )
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "CTMDFnmdbasxytvwh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
|
|
@ -42749,6 +42858,15 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
pDefines = argv[globalUtilOptind];
|
||||
globalUtilOptind++;
|
||||
break;
|
||||
case 'F':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-F\" should be followed by a file name.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pFileName2 = argv[globalUtilOptind];
|
||||
globalUtilOptind++;
|
||||
break;
|
||||
case 'n':
|
||||
pPars->fNaive ^= 1;
|
||||
break;
|
||||
|
|
@ -42793,6 +42911,15 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
Abc_Print( 0, "It looks like the current AIG is derived by &st -m. Such AIG contains XOR gates and cannot be verified before &st is applied.\n" );
|
||||
return 1;
|
||||
}
|
||||
if ( pFileName2 )
|
||||
{
|
||||
if ( (pFile = fopen( pFileName2, "r" )) == NULL )
|
||||
{
|
||||
Abc_Print( -1, "Cannot open input file \"%s\".\n", pFileName2 );
|
||||
return 1;
|
||||
}
|
||||
fclose( pFile );
|
||||
}
|
||||
pArgvNew = argv + globalUtilOptind;
|
||||
nArgcNew = argc - globalUtilOptind;
|
||||
if ( fMiter )
|
||||
|
|
@ -42870,7 +42997,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
int n;
|
||||
for ( n = 0; n < 2; n++ )
|
||||
{
|
||||
pGias[n] = Abc_ReadAigerOrVerilogFile( pFileNames[n], pTopModule, pDefines, &Abc_ReadAigerOrVerilogFileStatus );
|
||||
pGias[n] = Abc_ReadAigerOrVerilogFile( pFileNames[n], pFileName2, pTopModule, pDefines, &Abc_ReadAigerOrVerilogFileStatus );
|
||||
if ( pGias[n] == NULL )
|
||||
return Abc_ReadAigerOrVerilogFileStatus;
|
||||
}
|
||||
|
|
@ -42906,10 +43033,22 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
}
|
||||
FileName = pAbc->pGia->pSpec;
|
||||
}
|
||||
pGias[1] = Abc_ReadAigerOrVerilogFile( FileName, pTopModule, pDefines, &Abc_ReadAigerOrVerilogFileStatus );
|
||||
pGias[1] = Abc_ReadAigerOrVerilogFile( FileName, pFileName2, pTopModule, pDefines, &Abc_ReadAigerOrVerilogFileStatus );
|
||||
if ( pGias[1] == NULL )
|
||||
return Abc_ReadAigerOrVerilogFileStatus;
|
||||
}
|
||||
if ( pGias[0] && pGias[1] )
|
||||
{
|
||||
Gia_Man_t * pTemp = Abc_GiaReorderInputsByName( pGias[0], pGias[1] );
|
||||
if ( pTemp )
|
||||
{
|
||||
if ( pPars->fVerbose )
|
||||
Abc_Print( 1, "Reordered primary inputs of the second network using input names.\n" );
|
||||
if ( pGias[1] != pAbc->pGia && pGias[1] != pAbc->pGiaSaved )
|
||||
Gia_ManStop( pGias[1] );
|
||||
pGias[1] = pTemp;
|
||||
}
|
||||
}
|
||||
pPars->pNameSpec = pGias[0] ? (pGias[0]->pSpec ? pGias[0]->pSpec : pGias[0]->pName) : NULL;
|
||||
pPars->pNameImpl = pGias[1] ? (pGias[1]->pSpec ? pGias[1]->pSpec : pGias[1]->pName) : NULL;
|
||||
pPars->vNamesIn = pGias[0] ? pGias[0]->vNamesIn : NULL;
|
||||
|
|
@ -43018,12 +43157,13 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
return 0;
|
||||
|
||||
usage:
|
||||
Abc_Print( -2, "usage: &cec [-CT num] [-M str] [-D str] [-nmdbasxytvwh]\n" );
|
||||
Abc_Print( -2, "usage: &cec [-CT num] [-M str] [-D str] [-F str] [-nmdbasxytvwh]\n" );
|
||||
Abc_Print( -2, "\t new combinational equivalence checker\n" );
|
||||
Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
|
||||
Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", pPars->TimeLimit );
|
||||
Abc_Print( -2, "\t-M str : top module name if Verilog file(s) are used [default = \"not used\"]\n" );
|
||||
Abc_Print( -2, "\t-D str : defines to be used by Yosys for Verilog files [default = \"not used\"]\n" );
|
||||
Abc_Print( -2, "\t-F str : second Verilog/SystemVerilog file read together with each Verilog input [default = \"not used\"]\n" );
|
||||
Abc_Print( -2, "\t-n : toggle using naive SAT-based checking [default = %s]\n", pPars->fNaive? "yes":"no");
|
||||
Abc_Print( -2, "\t-m : toggle miter vs. two circuits [default = %s]\n", fMiter? "miter":"two circuits");
|
||||
Abc_Print( -2, "\t-d : toggle using dual output miter [default = %s]\n", fDualOutput? "yes":"no");
|
||||
|
|
|
|||
|
|
@ -98,6 +98,7 @@ void Cmd_Init( Abc_Frame_t * pAbc )
|
|||
Cmd_CommandAdd( pAbc, "Basic", "quit", CmdCommandQuit, 0 );
|
||||
Cmd_CommandAdd( pAbc, "Basic", "abcrc", CmdCommandAbcrc, 0 );
|
||||
Cmd_CommandAdd( pAbc, "Basic", "history", CmdCommandHistory, 0 );
|
||||
Cmd_CommandAdd( pAbc, "Basic", "hi", CmdCommandHistory, 0 );
|
||||
Cmd_CommandAdd( pAbc, "Basic", "alias", CmdCommandAlias, 0 );
|
||||
Cmd_CommandAdd( pAbc, "Basic", "unalias", CmdCommandUnalias, 0 );
|
||||
Cmd_CommandAdd( pAbc, "Basic", "help", CmdCommandHelp, 0 );
|
||||
|
|
@ -441,38 +442,31 @@ int CmdCommandAbcrc( Abc_Frame_t * pAbc, int argc, char **argv )
|
|||
int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv )
|
||||
{
|
||||
char * pName, * pStr = NULL;
|
||||
int i, c;
|
||||
char ** ppMatches = NULL;
|
||||
int * pIds = NULL;
|
||||
int i;
|
||||
int nPrints = 20;
|
||||
int nPrinted = 0;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
case 'h':
|
||||
goto usage;
|
||||
default :
|
||||
goto usage;
|
||||
}
|
||||
}
|
||||
if ( argc > globalUtilOptind + 2 )
|
||||
if ( argc == 2 && !strcmp(argv[1], "-h") )
|
||||
goto usage;
|
||||
if ( argc > 3 )
|
||||
goto usage;
|
||||
// parse arguments: can be [substring] [number] in either order
|
||||
if ( argc == globalUtilOptind + 1 )
|
||||
if ( argc == 2 )
|
||||
{
|
||||
// one argument: either number or substring
|
||||
pStr = argv[globalUtilOptind];
|
||||
pStr = argv[1];
|
||||
if ( pStr && pStr[0] >= '1' && pStr[0] <= '9' )
|
||||
{
|
||||
nPrints = atoi(pStr);
|
||||
pStr = NULL;
|
||||
}
|
||||
}
|
||||
else if ( argc == globalUtilOptind + 2 )
|
||||
else if ( argc == 3 )
|
||||
{
|
||||
// two arguments: substring and number
|
||||
char * arg1 = argv[globalUtilOptind];
|
||||
char * arg2 = argv[globalUtilOptind + 1];
|
||||
char * arg1 = argv[1];
|
||||
char * arg2 = argv[2];
|
||||
|
||||
// Try to parse second argument as number
|
||||
if ( arg2[0] >= '1' && arg2[0] <= '9' )
|
||||
|
|
@ -500,14 +494,22 @@ int CmdCommandHistory( Abc_Frame_t * pAbc, int argc, char **argv )
|
|||
fprintf( pAbc->Out, "%4d : %s\n", Vec_PtrSize(pAbc->aHistory)-i, pName );
|
||||
}
|
||||
else {
|
||||
// Search string provided, show up to nPrints matching entries
|
||||
Vec_PtrForEachEntry( char *, pAbc->aHistory, pName, i )
|
||||
// Search string provided, select up to nPrints most recent matching entries
|
||||
ppMatches = ABC_ALLOC( char *, nPrints );
|
||||
pIds = ABC_ALLOC( int, nPrints );
|
||||
Vec_PtrForEachEntryReverse( char *, pAbc->aHistory, pName, i )
|
||||
if ( strstr(pName, pStr) )
|
||||
{
|
||||
fprintf( pAbc->Out, "%4d : %s\n", Vec_PtrSize(pAbc->aHistory)-i, pName );
|
||||
pIds[nPrinted] = Vec_PtrSize(pAbc->aHistory)-i;
|
||||
ppMatches[nPrinted] = pName;
|
||||
if ( ++nPrinted >= nPrints )
|
||||
break;
|
||||
}
|
||||
// Print the selected entries in reverse so larger history indices appear first
|
||||
for ( i = nPrinted - 1; i >= 0; i-- )
|
||||
fprintf( pAbc->Out, "%4d : %s\n", pIds[i], ppMatches[i] );
|
||||
ABC_FREE( pIds );
|
||||
ABC_FREE( ppMatches );
|
||||
}
|
||||
return 0;
|
||||
|
||||
|
|
|
|||
|
|
@ -25,7 +25,6 @@
|
|||
#include <ctype.h>
|
||||
|
||||
ABC_NAMESPACE_IMPL_START
|
||||
// proper declaration of isspace
|
||||
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
/// DECLARATIONS ///
|
||||
|
|
@ -393,9 +392,51 @@ int CmdApplyAlias( Abc_Frame_t * pAbc, int *argcp, char ***argvp, int *loop )
|
|||
***********************************************************************/
|
||||
char * CmdHistorySubstitution( Abc_Frame_t * pAbc, char *line, int *changed )
|
||||
{
|
||||
// as of today, no history substitution
|
||||
*changed = 0;
|
||||
return line;
|
||||
char * pBeg = line, * pEnd, * pStr;
|
||||
int iRecall, nSize;
|
||||
while ( *pBeg && isspace((unsigned char)*pBeg) )
|
||||
pBeg++;
|
||||
if ( *pBeg == 0 )
|
||||
{
|
||||
*changed = 0;
|
||||
return line;
|
||||
}
|
||||
pEnd = pBeg;
|
||||
while ( *pEnd && !isspace((unsigned char)*pEnd) )
|
||||
pEnd++;
|
||||
if ( *pEnd )
|
||||
{
|
||||
char * pTemp = pEnd;
|
||||
while ( *pTemp && isspace((unsigned char)*pTemp) )
|
||||
pTemp++;
|
||||
if ( *pTemp )
|
||||
{
|
||||
*changed = 0;
|
||||
return line;
|
||||
}
|
||||
}
|
||||
if ( *pBeg < '1' || *pBeg > '9' )
|
||||
{
|
||||
*changed = 0;
|
||||
return line;
|
||||
}
|
||||
for ( pStr = pBeg; pStr < pEnd; pStr++ )
|
||||
if ( *pStr < '0' || *pStr > '9' )
|
||||
{
|
||||
*changed = 0;
|
||||
return line;
|
||||
}
|
||||
iRecall = atoi( pBeg );
|
||||
nSize = Vec_PtrSize( pAbc->aHistory );
|
||||
if ( iRecall < 1 || iRecall > nSize )
|
||||
{
|
||||
fprintf( pAbc->Err, "History entry %d does not exist.\n", iRecall );
|
||||
line[0] = 0;
|
||||
*changed = 0;
|
||||
return line;
|
||||
}
|
||||
*changed = 1;
|
||||
return (char *)Vec_PtrEntry( pAbc->aHistory, nSize - iRecall );
|
||||
}
|
||||
|
||||
/**Function*************************************************************
|
||||
|
|
@ -905,4 +946,3 @@ void Cmd_CommandSGen( Abc_Frame_t * pAbc, int nParts, int nIters, int fVerbose )
|
|||
/// END OF FILE ///
|
||||
////////////////////////////////////////////////////////////////////////
|
||||
ABC_NAMESPACE_IMPL_END
|
||||
|
||||
|
|
|
|||
|
|
@ -56,6 +56,7 @@ SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.
|
|||
#endif
|
||||
|
||||
#include "base/abc/abc.h"
|
||||
#include "base/cmd/cmdInt.h"
|
||||
#include "mainInt.h"
|
||||
#include "base/wlc/wlc.h"
|
||||
|
||||
|
|
@ -363,9 +364,15 @@ int Abc_RealMain( int argc, char * argv[] )
|
|||
// execute commands given by the user
|
||||
while ( !feof(stdin) )
|
||||
{
|
||||
int did_subst;
|
||||
// print command line prompt and
|
||||
// get the command from the user
|
||||
sCommand = Abc_UtilsGetUsersInput( pAbc );
|
||||
sCommand = CmdHistorySubstitution( pAbc, sCommand, &did_subst );
|
||||
if ( sCommand == NULL )
|
||||
break;
|
||||
if ( did_subst )
|
||||
fprintf( pAbc->Out, "%s\n", sCommand );
|
||||
|
||||
// execute the user's command
|
||||
fStatus = Cmd_CommandExecute( pAbc, sCommand );
|
||||
|
|
|
|||
|
|
@ -1856,29 +1856,26 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
|
|||
Wlc_Obj_t * pFanin = Wlc_ObjFanin0(p, pObj);
|
||||
int End = Wlc_ObjRangeEnd(pObj);
|
||||
int Beg = Wlc_ObjRangeBeg(pObj);
|
||||
if ( End >= Beg )
|
||||
int Low = Abc_MinInt( End, Beg );
|
||||
int High = Abc_MaxInt( End, Beg );
|
||||
assert( nRange == High - Low + 1 );
|
||||
if ( pFanin->End >= pFanin->Beg )
|
||||
{
|
||||
if ( pFanin->End >= pFanin->Beg )
|
||||
assert( pFanin->Beg <= Low && High <= pFanin->End );
|
||||
for ( k = 0; k < nRange; k++ )
|
||||
{
|
||||
assert( nRange == End - Beg + 1 );
|
||||
assert( pFanin->Beg <= Beg && End <= pFanin->End );
|
||||
for ( k = Beg; k <= End; k++ )
|
||||
Vec_IntPush( vRes, pFans0[k - pFanin->Beg] );
|
||||
}
|
||||
else
|
||||
{
|
||||
assert( nRange == End - Beg + 1 );
|
||||
assert( pFanin->End <= Beg && End <= pFanin->Beg );
|
||||
for ( k = Beg; k <= End; k++ )
|
||||
Vec_IntPush( vRes, pFans0[k - pFanin->End] );
|
||||
int Label = End >= Beg ? Beg + k : Beg - k;
|
||||
Vec_IntPush( vRes, pFans0[Label - pFanin->Beg] );
|
||||
}
|
||||
}
|
||||
else
|
||||
{
|
||||
assert( nRange == Beg - End + 1 );
|
||||
assert( pFanin->End <= End && Beg <= pFanin->Beg );
|
||||
for ( k = End; k <= Beg; k++ )
|
||||
Vec_IntPush( vRes, pFans0[k - pFanin->End] );
|
||||
assert( pFanin->End <= Low && High <= pFanin->Beg );
|
||||
for ( k = 0; k < nRange; k++ )
|
||||
{
|
||||
int Label = End >= Beg ? Beg + k : Beg - k;
|
||||
Vec_IntPush( vRes, pFans0[pFanin->Beg - Label] );
|
||||
}
|
||||
}
|
||||
}
|
||||
else if ( pObj->Type == WLC_OBJ_BIT_CONCAT )
|
||||
|
|
|
|||
|
|
@ -93,11 +93,12 @@ void Wln_End( Abc_Frame_t * pAbc )
|
|||
int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
|
||||
{
|
||||
extern Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, char * pLibrary, int fVerbose );
|
||||
extern Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose );
|
||||
extern Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pFileName2, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose );
|
||||
extern Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fCollapse, int fVerbose );
|
||||
|
||||
FILE * pFile;
|
||||
char * pFileName = NULL;
|
||||
char * pFileName2= NULL;
|
||||
char * pTopModule= NULL;
|
||||
char * pDefines = NULL;
|
||||
char * pLibrary = NULL;
|
||||
|
|
@ -111,7 +112,7 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
int fSetUndef = 0;
|
||||
int c, fVerbose = 0;
|
||||
Extra_UtilGetoptReset();
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "TMDLbdisumlcvh" ) ) != EOF )
|
||||
while ( ( c = Extra_UtilGetopt( argc, argv, "TMDLFbdisumlcvh" ) ) != EOF )
|
||||
{
|
||||
switch ( c )
|
||||
{
|
||||
|
|
@ -151,6 +152,15 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
pLibrary = argv[globalUtilOptind];
|
||||
globalUtilOptind++;
|
||||
break;
|
||||
case 'F':
|
||||
if ( globalUtilOptind >= argc )
|
||||
{
|
||||
Abc_Print( -1, "Command line switch \"-F\" should be followed by a file name.\n" );
|
||||
goto usage;
|
||||
}
|
||||
pFileName2 = argv[globalUtilOptind];
|
||||
globalUtilOptind++;
|
||||
break;
|
||||
case 'b':
|
||||
fBlast ^= 1;
|
||||
break;
|
||||
|
|
@ -200,10 +210,24 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
return 0;
|
||||
}
|
||||
fclose( pFile );
|
||||
if ( pFileName2 )
|
||||
{
|
||||
if ( (pFile = fopen( pFileName2, "r" )) == NULL )
|
||||
{
|
||||
Abc_Print( 1, "Cannot open input file \"%s\".\n", pFileName2 );
|
||||
return 0;
|
||||
}
|
||||
fclose( pFile );
|
||||
}
|
||||
|
||||
// perform reading
|
||||
if ( pLibrary )
|
||||
{
|
||||
if ( pFileName2 )
|
||||
{
|
||||
Abc_Print( 1, "Command line switch \"-F\" only applies in the default bit-blasting path.\n" );
|
||||
return 0;
|
||||
}
|
||||
Abc_Ntk_t * pNtk = NULL;
|
||||
if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
|
||||
pNtk = Wln_ReadMappedSystemVerilog( pFileName, pTopModule, pDefines, pLibrary, fVerbose );
|
||||
|
|
@ -220,11 +244,18 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
{
|
||||
Gia_Man_t * pNew = NULL;
|
||||
if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
|
||||
pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
|
||||
pNew = Wln_BlastSystemVerilog( pFileName, pFileName2, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
|
||||
else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) )
|
||||
pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
|
||||
pNew = Wln_BlastSystemVerilog( pFileName, pFileName2, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
|
||||
else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) )
|
||||
pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
|
||||
{
|
||||
if ( pFileName2 )
|
||||
{
|
||||
Abc_Print( 1, "Command line switch \"-F\" is only supported when the main input is Verilog/SystemVerilog.\n" );
|
||||
return 0;
|
||||
}
|
||||
pNew = Wln_BlastSystemVerilog( pFileName, NULL, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
|
||||
}
|
||||
else
|
||||
{
|
||||
printf( "Abc_CommandYosys(): Unknown file extension.\n" );
|
||||
|
|
@ -234,6 +265,11 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
}
|
||||
else
|
||||
{
|
||||
if ( pFileName2 )
|
||||
{
|
||||
Abc_Print( 1, "Command line switch \"-F\" only applies in the default bit-blasting path.\n" );
|
||||
return 0;
|
||||
}
|
||||
Rtl_Lib_t * pLib = NULL;
|
||||
if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
|
||||
pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose );
|
||||
|
|
@ -250,12 +286,13 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
|
|||
}
|
||||
return 0;
|
||||
usage:
|
||||
Abc_Print( -2, "usage: %%yosys [-TM <module>] [-D <defines>] [-L <liberty_file>] [-bdisumlcvh] <file_name>\n" );
|
||||
Abc_Print( -2, "usage: %%yosys [-TM <module>] [-D <defines>] [-L <liberty_file>] [-F <file>] [-bdisumlcvh] <file_name>\n" );
|
||||
Abc_Print( -2, "\t reads Verilog or SystemVerilog using Yosys\n" );
|
||||
Abc_Print( -2, "\t-T : specify the top module name (default uses \"-auto-top\")\n" );
|
||||
Abc_Print( -2, "\t-M : specify the top module name (default uses \"-auto-top\") (equivalent to \"-T\")\n" );
|
||||
Abc_Print( -2, "\t-D : specify defines to be used by Yosys (default \"not used\")\n" );
|
||||
Abc_Print( -2, "\t-L : specify the Liberty library to read a mapped design (default \"not used\")\n" );
|
||||
Abc_Print( -2, "\t-F : specify a second Verilog/SystemVerilog file for the default bit-blasting flow (default \"not used\")\n" );
|
||||
Abc_Print( -2, "\t-b : toggle bit-blasting the design into an AIG using Yosys (this switch has no effect)\n" );
|
||||
Abc_Print( -2, "\t-d : toggle bit-blasting the design into an AIG using Yosys [default = %s]\n", !fDontBlast? "yes": "no" );
|
||||
Abc_Print( -2, "\t-i : toggle inverting the outputs (useful for miters) [default = %s]\n", fInvert? "yes": "no" );
|
||||
|
|
|
|||
|
|
@ -19,6 +19,9 @@
|
|||
***********************************************************************/
|
||||
|
||||
#include "wln.h"
|
||||
#include "aig/aig/aig.h"
|
||||
#include "aig/gia/giaAig.h"
|
||||
#include "base/io/ioAbc.h"
|
||||
#include "base/main/main.h"
|
||||
|
||||
#ifdef WIN32
|
||||
|
|
@ -171,30 +174,54 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * p
|
|||
unlink( pFileTemp );
|
||||
return pNtk;
|
||||
}
|
||||
Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose )
|
||||
Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pFileName2, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose )
|
||||
{
|
||||
Gia_Man_t * pGia = NULL;
|
||||
char Command[1000];
|
||||
char * pFileTemp = "_temp_.aig";
|
||||
int fRtlil = strstr(pFileName, ".rtl") != NULL;
|
||||
int fSVlog = strstr(pFileName, ".sv") != NULL;
|
||||
sprintf( Command, "%s -qp \"%s %s%s %s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; %s%smemory -nomap; memory_map; dffunmap; opt_clean; opt_expr; aigmap; write_aiger -symbols %s\"",
|
||||
int fSVlog = strstr(pFileName, ".sv") != NULL || (pFileName2 && strstr(pFileName2, ".sv") != NULL);
|
||||
sprintf( Command, "%s -qp \"%s %s%s %s%s%s%s; hierarchy %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; %s%smemory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols %s\"",
|
||||
Wln_GetYosysName(),
|
||||
fRtlil ? "read_rtlil" : "read_verilog",
|
||||
pDefines ? "-D" : "",
|
||||
pDefines ? pDefines : "",
|
||||
fSVlog ? "-sv " : "",
|
||||
pFileName,
|
||||
pFileName2 ? " " : "",
|
||||
pFileName2 ? pFileName2 : "",
|
||||
pTopModule ? "-top " : "-auto-top",
|
||||
pTopModule ? pTopModule : "",
|
||||
fTechMap ? (fLibInDir ? "techmap -map techmap.v; " : "techmap; ") : "",
|
||||
fSetUndef ? "setundef -init -zero; " : "",
|
||||
pFileName2 ? "delete t:\\$scopeinfo; " : "",
|
||||
pFileTemp );
|
||||
if ( fVerbose )
|
||||
printf( "%s\n", Command );
|
||||
if ( !Wln_ConvertToRtl(Command, pFileTemp) )
|
||||
return NULL;
|
||||
pGia = Gia_AigerRead( pFileTemp, 0, fSkipStrash, 0 );
|
||||
if ( pFileName2 )
|
||||
{
|
||||
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
|
||||
Aig_Man_t * pAig = NULL;
|
||||
Abc_Ntk_t * pNtk = Io_Read( pFileTemp, IO_FILE_AIGER, 1, 0 );
|
||||
if ( pNtk == NULL )
|
||||
{
|
||||
printf( "Reading AIGER from file \"%s\" has failed.\n", pFileTemp );
|
||||
return NULL;
|
||||
}
|
||||
pAig = Abc_NtkToDar( pNtk, 0, 1 );
|
||||
Abc_NtkDelete( pNtk );
|
||||
if ( pAig == NULL )
|
||||
{
|
||||
printf( "Converting the AIGER network into an internal AIG has failed.\n" );
|
||||
return NULL;
|
||||
}
|
||||
pGia = fSkipStrash ? Gia_ManFromAigSimple(pAig) : Gia_ManFromAig(pAig);
|
||||
Aig_ManStop( pAig );
|
||||
}
|
||||
else
|
||||
pGia = Gia_AigerRead( pFileTemp, 0, fSkipStrash, 0 );
|
||||
if ( pGia == NULL )
|
||||
{
|
||||
printf( "Converting to AIG has failed.\n" );
|
||||
|
|
|
|||
|
|
@ -41,6 +41,39 @@ static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc )
|
|||
static inline void Wlc_AbcFreeNtk( Abc_Frame_t * pAbc ) { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(pAbc)); }
|
||||
static inline void Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk ) { Wlc_AbcFreeNtk(pAbc); pAbc->pAbcWlc = pNtk; }
|
||||
|
||||
static string Ufar_GetStatusName( Wlc_Ntk_t * pNtk )
|
||||
{
|
||||
if ( pNtk == NULL || Wlc_NtkPoNum(pNtk) == 0 )
|
||||
return "result";
|
||||
if ( Wlc_NtkPoNum(pNtk) == 1 )
|
||||
return Wlc_ObjName( pNtk, Wlc_ObjId(pNtk, Wlc_NtkPo(pNtk, 0)) );
|
||||
|
||||
string Name0 = Wlc_ObjName( pNtk, Wlc_ObjId(pNtk, Wlc_NtkPo(pNtk, 0)) );
|
||||
string Name1 = Wlc_ObjName( pNtk, Wlc_ObjId(pNtk, Wlc_NtkPo(pNtk, 1)) );
|
||||
return Name0 + "_xor_" + Name1;
|
||||
}
|
||||
|
||||
static void Ufar_DumpStatusLog( const string & FileName, int RetValue, const string & StatusName )
|
||||
{
|
||||
FILE * pFile;
|
||||
if ( FileName.empty() || FileName == "none" )
|
||||
return;
|
||||
pFile = fopen( FileName.c_str(), "wb" );
|
||||
if ( pFile == NULL )
|
||||
{
|
||||
cout << "Cannot open file \"" << FileName << "\" for writing." << endl;
|
||||
return;
|
||||
}
|
||||
if ( RetValue == 1 )
|
||||
fprintf( pFile, "STATUS: UNSAT " );
|
||||
else if ( RetValue == 0 )
|
||||
fprintf( pFile, "STATUS: SAT " );
|
||||
else
|
||||
fprintf( pFile, "STATUS: ABORTED " );
|
||||
fprintf( pFile, "%s\n", StatusName.c_str() );
|
||||
fclose( pFile );
|
||||
}
|
||||
|
||||
|
||||
void Ufar_Init(Abc_Frame_t *pAbc)
|
||||
{
|
||||
|
|
@ -146,6 +179,7 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
|
|||
opt_mgr.AddOpt("--crossonly", ufar_manager.params.fCrossOnly ? "yes" : "no", "", "allow UIF pairs only across LHS/RHS cones of the miter");
|
||||
opt_mgr.AddOpt("--crossstats", "no", "", "print multiplier counts in LHS/RHS/shared cones and exit");
|
||||
opt_mgr.AddOpt("--dump", "none", "str", "specify file name");
|
||||
opt_mgr.AddOpt("--dump-log", "none", "str", "write status log");
|
||||
opt_mgr.AddOpt("--dump-first-aig", "none", "str", "dump first internal bit-blasted AIG and exit");
|
||||
opt_mgr.AddOpt("--dump-abs", "none", "str", "specify file name");
|
||||
opt_mgr.AddOpt("--par", "none", "str", "use parallel solvers");
|
||||
|
|
@ -254,6 +288,8 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
|
|||
|
||||
// ufar_manager.DumpParams();
|
||||
LogT::prefix = "UIF_PROVE";
|
||||
string dumpLogFile = opt_mgr["--dump-log"] ? opt_mgr.GetOptVal("--dump-log") : "";
|
||||
string statusName = Ufar_GetStatusName( Wlc_AbcGetNtk(pAbc) );
|
||||
|
||||
set<unsigned> set_op_types;
|
||||
set_op_types.insert(WLC_OBJ_ARI_MULTI);
|
||||
|
|
@ -372,6 +408,7 @@ static int Abc_CommandProveUsingUif( Abc_Frame_t * pAbc, int argc, char ** argv
|
|||
} else {
|
||||
LOG(0) << "Undecided by UIF.";
|
||||
}
|
||||
Ufar_DumpStatusLog( dumpLogFile, ret, statusName );
|
||||
|
||||
gettimeofday(&t2, NULL);
|
||||
unsigned tTotal = elapsed_time_usec(t1, t2);
|
||||
|
|
|
|||
Loading…
Reference in New Issue