Updating %ysoys to abstract modules/instances.

This commit is contained in:
Alan Mishchenko 2026-07-25 15:53:55 -07:00
parent 3ed7e4179a
commit 57ad5cd47b
4 changed files with 329 additions and 59 deletions

View File

@ -65,6 +65,7 @@
#include "opt/fret/fretime.h"
#include "opt/nwk/nwkMerge.h"
#include "base/acb/acbPar.h"
#include "base/wln/wln.h"
#include "misc/extra/extra.h"
#include "opt/eslim/eSLIM.h"
@ -43459,13 +43460,17 @@ static void Abc_GiaTransferNamesIfMatch( Gia_Man_t * pGia, Gia_Man_t * pGiaNames
SeeAlso []
***********************************************************************/
static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileName2, char * pTopModule, char * pDefines, int * pAbc_ReadAigerOrVerilogFileStatus )
static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileName2, char * pTopModule, Vec_Ptr_t * vDefines, Vec_Ptr_t * vBoxes, Vec_Ptr_t * vInsts, int * pAbc_ReadAigerOrVerilogFileStatus )
{
FILE * pFile;
Gia_Man_t * pGia;
char * pTemp;
char * pOrigFileName = NULL;
char * pFileTemp = NULL;
char * pDefines = NULL;
char * pBoxes = NULL;
char * pExposes = NULL;
char * pInsts = NULL;
int fVerilog, fSystemVerilog;
*pAbc_ReadAigerOrVerilogFileStatus = 0;
@ -43493,8 +43498,9 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam
{
extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
Aig_Man_t * pAig = NULL;
char pCommand[2000];
char * pCommand;
char * pFileBase;
int nCommand;
int RetValue;
int fSystemVerilog2 = pFileName2 && Extra_FileIsType( pFileName2, ".sv", NULL, NULL );
// Save the original filename before changing it
@ -43504,14 +43510,35 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam
pFileTemp = ABC_ALLOC( char, strlen(pFileBase) + 5 );
sprintf( pFileTemp, "%s.aig", pFileBase );
ABC_FREE( pFileBase );
snprintf( pCommand, sizeof(pCommand),
"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 %s\"",
pDefines ? "-D" : "", pDefines ? pDefines : "",
(fSystemVerilog || fSystemVerilog2) ? "-sv " : "", pFileName,
pFileName2 ? " " : "", pFileName2 ? pFileName2 : "",
pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "",
pFileName2 ? "delete t:\\$scopeinfo; " : "",
pFileTemp );
pDefines = Wln_YosysBuildDefines( vDefines );
pBoxes = Wln_YosysBuildBoxCommands( vBoxes, 0 );
pExposes = Wln_YosysBuildBoxCommands( vBoxes, 1 );
pInsts = Wln_YosysBuildInstCommands( vInsts );
nCommand = strlen("yosys") + (pDefines ? strlen(pDefines) : 0) + (pBoxes ? strlen(pBoxes) : 0) + (pExposes ? strlen(pExposes) : 0) + 2 * (pInsts ? strlen(pInsts) : 0) + strlen(pFileName) + (pFileName2 ? strlen(pFileName2) : 0) + 2 * (pTopModule ? strlen(pTopModule) : 0) + strlen(pFileTemp) + 700;
pCommand = ABC_ALLOC( char, nCommand );
if ( pBoxes || pInsts )
snprintf( pCommand, nCommand,
"yosys -qp \"read_verilog %s %s%s%s%s; hierarchy -check %s%s; %s%shierarchy -check %s%s; proc; memory -nomap; %smemory_map; opt; async2sync; opt; setundef -undriven -expose; setundef -zero; dffunmap; techmap; opt; dffunmap; flatten; %s%sopt_clean; opt_expr; setundef -undriven -expose; setundef -zero; aigmap; write_aiger -symbols %s\"",
pDefines ? pDefines : "",
(fSystemVerilog || fSystemVerilog2) ? "-sv " : "", pFileName,
pFileName2 ? " " : "", pFileName2 ? pFileName2 : "",
pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "",
pBoxes ? pBoxes : "",
pInsts ? pInsts : "",
pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "",
pInsts ? pInsts : "",
pExposes ? pExposes : "",
pFileName2 ? "delete t:\\$scopeinfo; " : "",
pFileTemp );
else
snprintf( pCommand, nCommand,
"yosys -qp \"read_verilog %s %s%s%s%s; hierarchy -check %s%s; flatten; proc; opt; async2sync; opt; setundef -undriven -zero; techmap; memory -nomap; memory_map; dffunmap; opt_clean; opt_expr; %saigmap; write_aiger -symbols %s\"",
pDefines ? pDefines : "",
(fSystemVerilog || fSystemVerilog2) ? "-sv " : "", pFileName,
pFileName2 ? " " : "", pFileName2 ? pFileName2 : "",
pTopModule ? "-top " : "-auto-top", pTopModule ? pTopModule : "",
pFileName2 ? "delete t:\\$scopeinfo; " : "",
pFileTemp );
#if defined(__wasm)
RetValue = 1;
#else
@ -43520,9 +43547,23 @@ static Gia_Man_t * Abc_ReadAigerOrVerilogFile( char * pFileName, char * pFileNam
if ( RetValue != 0 )
{
Abc_Print( -1, "Yosys command failed: \"%s\".\n", pCommand );
ABC_FREE( pCommand );
ABC_FREE( pDefines );
ABC_FREE( pBoxes );
ABC_FREE( pExposes );
ABC_FREE( pInsts );
ABC_FREE( pFileTemp );
return NULL;
}
ABC_FREE( pCommand );
ABC_FREE( pDefines );
ABC_FREE( pBoxes );
ABC_FREE( pExposes );
ABC_FREE( pInsts );
pDefines = NULL;
pBoxes = NULL;
pExposes = NULL;
pInsts = NULL;
if ( pFileName2 )
{
Gia_Man_t * pGiaNames = NULL;
@ -43591,12 +43632,15 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
Cec_ParCec_t ParsCec, * pPars = &ParsCec;
FILE * pFile;
Gia_Man_t * pGias[2] = {NULL, NULL}, * pMiter;
char ** pArgvNew, * pTopModule = NULL, * pDefines = NULL, * pFileName2 = NULL;
char ** pArgvNew, * pTopModule = NULL, * pFileName2 = NULL;
Vec_Ptr_t * vDefines = Vec_PtrAlloc( 0 );
Vec_Ptr_t * vBoxes = Vec_PtrAlloc( 0 );
Vec_Ptr_t * vInsts = Vec_PtrAlloc( 0 );
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, "CTMDFnmdbasxytvwh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "CTMDIBFnmdbasxytvwh" ) ) != EOF )
{
switch ( c )
{
@ -43637,7 +43681,25 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( -1, "Command line switch \"-D\" should be followed by defines.\n" );
goto usage;
}
pDefines = argv[globalUtilOptind];
Vec_PtrPush( vDefines, argv[globalUtilOptind] );
globalUtilOptind++;
break;
case 'B':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-B\" should be followed by a module pattern.\n" );
goto usage;
}
Vec_PtrPush( vBoxes, argv[globalUtilOptind] );
globalUtilOptind++;
break;
case 'I':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-I\" should be followed by an instance pattern.\n" );
goto usage;
}
Vec_PtrPush( vInsts, argv[globalUtilOptind] );
globalUtilOptind++;
break;
case 'F':
@ -43691,6 +43753,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pAbc->pGia && pAbc->pGia->nXors )
{
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" );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 1;
}
if ( pFileName2 )
@ -43698,6 +43763,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( (pFile = fopen( pFileName2, "r" )) == NULL )
{
Abc_Print( -1, "Cannot open input file \"%s\".\n", pFileName2 );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 1;
}
fclose( pFile );
@ -43709,6 +43777,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
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" );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 1;
}
if ( fDualOutput )
@ -43716,6 +43787,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( Gia_ManPoNum(pAbc->pGia) & 1 )
{
Abc_Print( -1, "The dual-output miter should have an even number of outputs.\n" );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 1;
}
if ( !pPars->fSilent )
@ -43740,6 +43814,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
else
Abc_Print( 1, "Networks are UNDECIDED. " );
Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 0;
}
// handle the case when the output is disproved by an all-0 primary input pattern
@ -43766,11 +43843,17 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
}
}
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 0;
}
if ( nArgcNew > 2 )
{
Abc_Print( -1, "Abc_CommandAbc9Cec(): Wrong number of command-line arguments.\n" );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 1;
}
if ( nArgcNew == 2 )
@ -43779,9 +43862,14 @@ 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], pFileName2, pTopModule, pDefines, &Abc_ReadAigerOrVerilogFileStatus );
pGias[n] = Abc_ReadAigerOrVerilogFile( pFileNames[n], pFileName2, pTopModule, vDefines, vBoxes, vInsts, &Abc_ReadAigerOrVerilogFileStatus );
if ( pGias[n] == NULL )
{
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return Abc_ReadAigerOrVerilogFileStatus;
}
}
}
else if ( fSavedSpec )
@ -43789,6 +43877,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pAbc->pGiaSaved == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Cec(): There is no saved specification.\n" );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 1;
}
pGias[0] = pAbc->pGia;
@ -43800,6 +43891,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pAbc->pGia == NULL )
{
Abc_Print( -1, "Abc_CommandAbc9Cec(): There is no current AIG.\n" );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 1;
}
pGias[0] = pAbc->pGia;
@ -43811,13 +43905,21 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( pAbc->pGia->pSpec == NULL )
{
Abc_Print( -1, "File name is not given on the command line.\n" );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 1;
}
FileName = pAbc->pGia->pSpec;
}
pGias[1] = Abc_ReadAigerOrVerilogFile( FileName, pFileName2, pTopModule, pDefines, &Abc_ReadAigerOrVerilogFileStatus );
pGias[1] = Abc_ReadAigerOrVerilogFile( FileName, pFileName2, pTopModule, vDefines, vBoxes, vInsts, &Abc_ReadAigerOrVerilogFileStatus );
if ( pGias[1] == NULL )
{
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return Abc_ReadAigerOrVerilogFileStatus;
}
}
if ( pGias[0] && pGias[1] )
{
@ -43875,6 +43977,9 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( fUseSim && Gia_ManCiNum(pMiter) > 40 )
{
Abc_Print( -1, "This type of CEC can only be applied to AIGs with no more than 40 inputs.\n" );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 0;
}
if ( fUseSim )
@ -43945,15 +44050,20 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
Gia_ManStop( pGias[0] );
if ( pGias[1] != pAbc->pGiaSaved )
Gia_ManStop( pGias[1] );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 0;
usage:
Abc_Print( -2, "usage: &cec [-CT num] [-M str] [-D str] [-F str] [-nmdbasxytvwh]\n" );
Abc_Print( -2, "usage: &cec [-CT num] [-M str] [-D str] [-B str] [-I 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-D str : possibly repeated defines used by Yosys for Verilog files [default = \"not used\"]\n" );
Abc_Print( -2, "\t-B str : possibly repeated module patterns to box in Verilog AIG output [default = \"not used\"]\n" );
Abc_Print( -2, "\t-I str : possibly repeated instance/cell patterns to box in Verilog AIG output [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");
@ -43967,6 +44077,9 @@ usage:
Abc_Print( -2, "\t-v : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes":"no");
Abc_Print( -2, "\t-w : toggle printing SAT solver statistics [default = %s]\n", pPars->fVeryVerbose? "yes":"no");
Abc_Print( -2, "\t-h : print the command usage\n");
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 1;
}

View File

@ -250,6 +250,10 @@ extern Vec_Int_t * Wln_NtkRetime( Wln_Ntk_t * p, int fIgnoreIO, int fSkipSimp
extern void Wln_NtkRetimeCreateDelayInfo( Wln_Ntk_t * pNtk );
/*=== wlcWriteVer.c ========================================================*/
extern void Wln_WriteVer( Wln_Ntk_t * p, char * pFileName );
/*=== wlnRtl.c ========================================================*/
extern char * Wln_YosysBuildDefines( Vec_Ptr_t * vDefines );
extern char * Wln_YosysBuildBoxCommands( Vec_Ptr_t * vBoxes, int fExpose );
extern char * Wln_YosysBuildInstCommands( Vec_Ptr_t * vInsts );
/*=== wlcRead.c ========================================================*/
typedef struct Rtl_Lib_t_ Rtl_Lib_t;
@ -263,4 +267,3 @@ ABC_NAMESPACE_HEADER_END
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////

View File

@ -92,9 +92,9 @@ 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 ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, char * pLibrary, int fVerbose );
extern Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose );
extern Rtl_Lib_t * Wln_ReadSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, int fCollapse, int fVerbose );
extern Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, Vec_Ptr_t * vDefines, char * pLibrary, int fVerbose );
extern Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, Vec_Ptr_t * vDefines, Vec_Ptr_t * vBoxes, Vec_Ptr_t * vInsts, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose );
extern Rtl_Lib_t * Wln_ReadSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, Vec_Ptr_t * vDefines, int fCollapse, int fVerbose );
FILE * pFile;
char * pFileName = NULL;
@ -103,7 +103,9 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
int nFileNames = 0;
int fFileNamesAlloc = 0;
char * pTopModule= NULL;
char * pDefines = NULL;
Vec_Ptr_t * vDefines = Vec_PtrAlloc( 0 );
Vec_Ptr_t * vBoxes = Vec_PtrAlloc( 0 );
Vec_Ptr_t * vInsts = Vec_PtrAlloc( 0 );
char * pLibrary = NULL;
int fBlast = 0;
int fDontBlast = 0;
@ -115,7 +117,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, "TMDLFbdisumlcvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "TMDIBLFbdisumlcvh" ) ) != EOF )
{
switch ( c )
{
@ -140,10 +142,28 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
case 'D':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-D\" should be followed by a file name.\n" );
Abc_Print( -1, "Command line switch \"-D\" should be followed by defines.\n" );
goto usage;
}
pDefines = argv[globalUtilOptind];
Vec_PtrPush( vDefines, argv[globalUtilOptind] );
globalUtilOptind++;
break;
case 'B':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-B\" should be followed by a module pattern.\n" );
goto usage;
}
Vec_PtrPush( vBoxes, argv[globalUtilOptind] );
globalUtilOptind++;
break;
case 'I':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-I\" should be followed by an instance pattern.\n" );
goto usage;
}
Vec_PtrPush( vInsts, argv[globalUtilOptind] );
globalUtilOptind++;
break;
case 'L':
@ -201,6 +221,9 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
if ( nFileNames < 1 )
{
printf( "Abc_CommandReadWlc(): Input file name(s) should be given on the command line.\n" );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 0;
}
ppFileNames = pFileName2 ? ABC_ALLOC( char *, nFileNames + 1 ) : argv + globalUtilOptind;
@ -223,6 +246,9 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "\n" );
if ( fFileNamesAlloc )
ABC_FREE( ppFileNames );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 0;
}
fclose( pFile );
@ -238,23 +264,39 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "Multiple input files are supported only for Verilog/SystemVerilog files.\n" );
if ( fFileNamesAlloc )
ABC_FREE( ppFileNames );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 0;
}
}
if ( (Vec_PtrSize(vBoxes) > 0 || Vec_PtrSize(vInsts) > 0) && (pLibrary || fDontBlast) )
{
Abc_Print( -1, "Command line switches \"-B\" and \"-I\" are only supported when bit-blasting into an AIG.\n" );
if ( fFileNamesAlloc )
ABC_FREE( ppFileNames );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 1;
}
// perform reading
if ( pLibrary )
{
Abc_Ntk_t * pNtk = NULL;
if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
pNtk = Wln_ReadMappedSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, pLibrary, fVerbose );
pNtk = Wln_ReadMappedSystemVerilog( ppFileNames, nFileNames, pTopModule, vDefines, pLibrary, fVerbose );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) )
pNtk = Wln_ReadMappedSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, pLibrary, fVerbose );
pNtk = Wln_ReadMappedSystemVerilog( ppFileNames, nFileNames, pTopModule, vDefines, pLibrary, fVerbose );
else
{
printf( "Abc_CommandYosys(): Unknown file extension.\n" );
if ( fFileNamesAlloc )
ABC_FREE( ppFileNames );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 0;
}
Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
@ -263,9 +305,9 @@ 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( ppFileNames, nFileNames, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
pNew = Wln_BlastSystemVerilog( ppFileNames, nFileNames, pTopModule, vDefines, vBoxes, vInsts, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) )
pNew = Wln_BlastSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
pNew = Wln_BlastSystemVerilog( ppFileNames, nFileNames, pTopModule, vDefines, vBoxes, vInsts, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) )
{
if ( nFileNames > 1 )
@ -273,15 +315,21 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "Multiple input files are supported only for Verilog/SystemVerilog files.\n" );
if ( fFileNamesAlloc )
ABC_FREE( ppFileNames );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 0;
}
pNew = Wln_BlastSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
pNew = Wln_BlastSystemVerilog( ppFileNames, nFileNames, pTopModule, vDefines, vBoxes, vInsts, fSkipStrash, fInvert, fTechMap, fLibInDir, fSetUndef, fVerbose );
}
else
{
printf( "Abc_CommandYosys(): Unknown file extension.\n" );
if ( fFileNamesAlloc )
ABC_FREE( ppFileNames );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 0;
}
Abc_FrameUpdateGia( pAbc, pNew );
@ -290,9 +338,9 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
{
Rtl_Lib_t * pLib = NULL;
if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fCollapse, fVerbose );
pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, vDefines, fCollapse, fVerbose );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) )
pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fCollapse, fVerbose );
pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, vDefines, fCollapse, fVerbose );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) )
{
if ( nFileNames > 1 )
@ -300,28 +348,39 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "Multiple input files are supported only for Verilog/SystemVerilog files.\n" );
if ( fFileNamesAlloc )
ABC_FREE( ppFileNames );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 0;
}
pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, pDefines, fCollapse, fVerbose );
pLib = Wln_ReadSystemVerilog( ppFileNames, nFileNames, pTopModule, vDefines, fCollapse, fVerbose );
}
else
{
printf( "Abc_CommandYosys(): Unknown file extension.\n" );
if ( fFileNamesAlloc )
ABC_FREE( ppFileNames );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 0;
}
Wln_AbcUpdateRtl( pAbc, pLib );
}
if ( fFileNamesAlloc )
ABC_FREE( ppFileNames );
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 0;
usage:
Abc_Print( -2, "usage: %%yosys [-TM <module>] [-D <defines>] [-L <liberty_file>] [-F <file>] [-bdisumlcvh] <file_name> [file_name...]\n" );
Abc_Print( -2, "usage: %%yosys [-TM <module>] [-D <defines>] [-B <module_pattern>] [-I <instance_pattern>] [-L <liberty_file>] [-F <file>] [-bdisumlcvh] <file_name> [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-D : specify possibly repeated defines to be used by Yosys (default \"not used\")\n" );
Abc_Print( -2, "\t-B : specify possibly repeated module patterns to box in AIG output (default \"not used\")\n" );
Abc_Print( -2, "\t-I : specify possibly repeated instance/cell patterns to box in AIG output (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 an additional Verilog/SystemVerilog file (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" );
@ -334,6 +393,9 @@ usage:
Abc_Print( -2, "\t-u : toggle replacing undefined/reset-X with zero using Yosys setundef [default = %s]\n", fSetUndef? "yes": "no" );
Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
Abc_Print( -2, "\t-h : print the command usage\n");
Vec_PtrFree( vDefines );
Vec_PtrFree( vBoxes );
Vec_PtrFree( vInsts );
return 1;
}

View File

@ -146,6 +146,63 @@ static int Wln_FileNamesHasSv( char ** ppFileNames, int nFileNames )
return 1;
return 0;
}
char * Wln_YosysBuildDefines( Vec_Ptr_t * vDefines )
{
char * pDefine, * pDefines;
int i, nChars = 1;
if ( vDefines == NULL || Vec_PtrSize(vDefines) == 0 )
return NULL;
Vec_PtrForEachEntry( char *, vDefines, pDefine, i )
nChars += strlen(pDefine) + 4;
pDefines = ABC_ALLOC( char, nChars );
pDefines[0] = 0;
Vec_PtrForEachEntry( char *, vDefines, pDefine, i )
{
if ( i )
strcat( pDefines, " " );
strcat( pDefines, "-D" );
strcat( pDefines, pDefine );
}
return pDefines;
}
char * Wln_YosysBuildBoxCommands( Vec_Ptr_t * vBoxes, int fExpose )
{
char * pBox, * pBoxes;
const char * pPrefix = fExpose ? "expose -evert t:" : "blackbox ";
int i, nChars = 1;
if ( vBoxes == NULL || Vec_PtrSize(vBoxes) == 0 )
return NULL;
Vec_PtrForEachEntry( char *, vBoxes, pBox, i )
nChars += strlen(pPrefix) + strlen(pBox) + 2;
pBoxes = ABC_ALLOC( char, nChars );
pBoxes[0] = 0;
Vec_PtrForEachEntry( char *, vBoxes, pBox, i )
{
strcat( pBoxes, pPrefix );
strcat( pBoxes, pBox );
strcat( pBoxes, "; " );
}
return pBoxes;
}
char * Wln_YosysBuildInstCommands( Vec_Ptr_t * vInsts )
{
char * pInst, * pInsts;
const char * pPrefix = "expose -evert c:";
int i, nChars = 1;
if ( vInsts == NULL || Vec_PtrSize(vInsts) == 0 )
return NULL;
Vec_PtrForEachEntry( char *, vInsts, pInst, i )
nChars += strlen(pPrefix) + strlen(pInst) + 2;
pInsts = ABC_ALLOC( char, nChars );
pInsts[0] = 0;
Vec_PtrForEachEntry( char *, vInsts, pInst, i )
{
strcat( pInsts, pPrefix );
strcat( pInsts, pInst );
strcat( pInsts, "; " );
}
return pInsts;
}
int Wln_ConvertToRtl( char * pCommand, char * pFileTemp )
{
#if defined(__wasm)
@ -166,21 +223,21 @@ int Wln_ConvertToRtl( char * pCommand, char * pFileTemp )
return 1;
#endif
}
Rtl_Lib_t * Wln_ReadSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, int fCollapse, int fVerbose )
Rtl_Lib_t * Wln_ReadSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, Vec_Ptr_t * vDefines, int fCollapse, int fVerbose )
{
Rtl_Lib_t * pNtk = NULL;
char * pFileNames, * pCommand;
char * pFileNames, * pCommand, * pDefines;
char * pFileTemp = "_temp_.rtlil";
int fSVlog = Wln_FileNamesHasSv(ppFileNames, nFileNames);
int nCommand;
if ( nFileNames == 1 && strstr(ppFileNames[0], ".rtl") )
return Rtl_LibReadFile( ppFileNames[0], ppFileNames[0] );
pFileNames = Wln_FileNamesJoin( ppFileNames, nFileNames );
pDefines = Wln_YosysBuildDefines( vDefines );
nCommand = strlen(Wln_GetYosysName()) + strlen(pFileNames) + (pDefines ? strlen(pDefines) : 0) + (pTopModule ? strlen(pTopModule) : 0) + strlen(pFileTemp) + 200;
pCommand = ABC_ALLOC( char, nCommand );
sprintf( pCommand, "%s -qp \"read_verilog %s%s %s%s; hierarchy %s%s; %sproc; memory -nomap; memory_map; write_rtlil %s\"",
sprintf( pCommand, "%s -qp \"read_verilog %s %s%s; hierarchy -check %s%s; %sproc; memory -nomap; memory_map; write_rtlil %s\"",
Wln_GetYosysName(),
pDefines ? "-D" : "",
pDefines ? pDefines : "",
fSVlog ? "-sv " : "",
pFileNames,
@ -193,10 +250,12 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char ** ppFileNames, int nFileNames, char * p
if ( !Wln_ConvertToRtl(pCommand, pFileTemp) )
{
ABC_FREE( pCommand );
ABC_FREE( pDefines );
ABC_FREE( pFileNames );
return NULL;
}
ABC_FREE( pCommand );
ABC_FREE( pDefines );
ABC_FREE( pFileNames );
pNtk = Rtl_LibReadFile( pFileTemp, ppFileNames[0] );
if ( pNtk == NULL )
@ -208,10 +267,10 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char ** ppFileNames, int nFileNames, char * p
unlink( pFileTemp );
return pNtk;
}
Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose )
Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, Vec_Ptr_t * vDefines, Vec_Ptr_t * vBoxes, Vec_Ptr_t * vInsts, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fSetUndef, int fVerbose )
{
Gia_Man_t * pGia = NULL;
char * pFileNames, * pCommand;
char * pFileNames, * pCommand, * pDefines, * pBoxes, * pExposes, * pInsts;
char * pFileTemp, * pFileBase;
int fRtlil = nFileNames == 1 && strstr(ppFileNames[0], ".rtl") != NULL;
int fSVlog = Wln_FileNamesHasSv(ppFileNames, nFileNames);
@ -222,31 +281,62 @@ Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char *
sprintf( pFileTemp, "%s.aig", pFileBase );
ABC_FREE( pFileBase );
pFileNames = Wln_FileNamesJoin( ppFileNames, nFileNames );
nCommand = strlen(Wln_GetYosysName()) + strlen(pFileNames) + (pDefines ? strlen(pDefines) : 0) + (pTopModule ? strlen(pTopModule) : 0) + strlen(pFileTemp) + 500;
pDefines = Wln_YosysBuildDefines( vDefines );
pBoxes = Wln_YosysBuildBoxCommands( vBoxes, 0 );
pExposes = Wln_YosysBuildBoxCommands( vBoxes, 1 );
pInsts = Wln_YosysBuildInstCommands( vInsts );
nCommand = strlen(Wln_GetYosysName()) + strlen(pFileNames) + (pDefines ? strlen(pDefines) : 0) + (pBoxes ? strlen(pBoxes) : 0) + (pExposes ? strlen(pExposes) : 0) + 2 * (pInsts ? strlen(pInsts) : 0) + 2 * (pTopModule ? strlen(pTopModule) : 0) + strlen(pFileTemp) + 700;
pCommand = ABC_ALLOC( char, nCommand );
sprintf( pCommand, "%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; %saigmap; write_aiger -symbols %s\"",
Wln_GetYosysName(),
fRtlil ? "read_rtlil" : "read_verilog",
pDefines ? "-D" : "",
pDefines ? pDefines : "",
fSVlog ? "-sv " : "",
pFileNames,
pTopModule ? "-top " : "-auto-top",
pTopModule ? pTopModule : "",
fTechMap ? (fLibInDir ? "techmap -map techmap.v; " : "techmap; ") : "",
fSetUndef ? "setundef -init -zero; " : "",
nFileNames > 1 ? "delete t:\\$scopeinfo; " : "",
pFileTemp );
if ( pBoxes || pInsts )
sprintf( pCommand, "%s -qp \"%s %s %s%s; hierarchy -check %s%s; %s%shierarchy -check %s%s; proc; memory -nomap; %smemory_map; opt; async2sync; opt; setundef -undriven -expose; setundef -zero; %sdffunmap; %sopt; dffunmap; flatten; %s%sopt_clean; opt_expr; setundef -undriven -expose; setundef -zero; aigmap; write_aiger -symbols %s\"",
Wln_GetYosysName(),
fRtlil ? "read_rtlil" : "read_verilog",
pDefines ? pDefines : "",
fSVlog ? "-sv " : "",
pFileNames,
pTopModule ? "-top " : "-auto-top",
pTopModule ? pTopModule : "",
pBoxes ? pBoxes : "",
pInsts ? pInsts : "",
pTopModule ? "-top " : "-auto-top",
pTopModule ? pTopModule : "",
pInsts ? pInsts : "",
fSetUndef ? "setundef -init -zero; " : "",
fTechMap ? (fLibInDir ? "techmap -map techmap.v; " : "techmap; ") : "",
pExposes ? pExposes : "",
nFileNames > 1 ? "delete t:\\$scopeinfo; " : "",
pFileTemp );
else
sprintf( pCommand, "%s -qp \"%s %s %s%s; hierarchy -check %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 ? pDefines : "",
fSVlog ? "-sv " : "",
pFileNames,
pTopModule ? "-top " : "-auto-top",
pTopModule ? pTopModule : "",
fTechMap ? (fLibInDir ? "techmap -map techmap.v; " : "techmap; ") : "",
fSetUndef ? "setundef -init -zero; " : "",
nFileNames > 1 ? "delete t:\\$scopeinfo; " : "",
pFileTemp );
if ( fVerbose )
printf( "%s\n", pCommand );
if ( !Wln_ConvertToRtl(pCommand, pFileTemp) )
{
ABC_FREE( pCommand );
ABC_FREE( pDefines );
ABC_FREE( pBoxes );
ABC_FREE( pExposes );
ABC_FREE( pInsts );
ABC_FREE( pFileNames );
ABC_FREE( pFileTemp );
return NULL;
}
ABC_FREE( pCommand );
ABC_FREE( pDefines );
ABC_FREE( pBoxes );
ABC_FREE( pExposes );
ABC_FREE( pInsts );
ABC_FREE( pFileNames );
pGia = Gia_AigerRead( pFileTemp, 0, fSkipStrash, 0 );
if ( pGia == NULL )
@ -269,21 +359,21 @@ Gia_Man_t * Wln_BlastSystemVerilog( char ** ppFileNames, int nFileNames, char *
}
return pGia;
}
Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, char * pDefines, char * pLibrary, int fVerbose )
Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char ** ppFileNames, int nFileNames, char * pTopModule, Vec_Ptr_t * vDefines, char * pLibrary, int fVerbose )
{
Abc_Ntk_t * pNtk = NULL;
char * pFileNames, * pCommand;
char * pFileNames, * pCommand, * pDefines;
char * pFileTemp = "_temp_.blif";
int fSVlog = Wln_FileNamesHasSv(ppFileNames, nFileNames);
int nCommand;
pFileNames = Wln_FileNamesJoin( ppFileNames, nFileNames );
pDefines = Wln_YosysBuildDefines( vDefines );
nCommand = strlen(Wln_GetYosysName()) + strlen(pLibrary) + strlen(pFileNames) + (pDefines ? strlen(pDefines) : 0) + 2 * (pTopModule ? strlen(pTopModule) : 0) + strlen(pFileTemp) + 300;
pCommand = ABC_ALLOC( char, nCommand );
sprintf( pCommand, "%s -qp \"read_liberty -lib %s; read %s %s%s %s; hierarchy %s%s; flatten; proc; memory -nomap; memory_map; write_blif %s%s -impltf -gates %s\"",
sprintf( pCommand, "%s -qp \"read_liberty -lib %s; read %s %s %s; hierarchy -check %s%s; flatten; proc; memory -nomap; memory_map; write_blif %s%s -impltf -gates %s\"",
Wln_GetYosysName(),
pLibrary,
fSVlog ? "-sv " : "-vlog95",
pDefines ? "-D" : "",
pDefines ? pDefines : "",
pFileNames,
pTopModule ? "-top " : "-auto-top",
@ -296,10 +386,12 @@ Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char ** ppFileNames, int nFileNames, ch
if ( !Wln_ConvertToRtl(pCommand, pFileTemp) )
{
ABC_FREE( pCommand );
ABC_FREE( pDefines );
ABC_FREE( pFileNames );
return NULL;
}
ABC_FREE( pCommand );
ABC_FREE( pDefines );
ABC_FREE( pFileNames );
pCommand = ABC_ALLOC( char, strlen(pLibrary) + 20 );
sprintf( pCommand, "read_lib %s", pLibrary );