Skip to content

A
abc
Commit b69f4396 by Alan Mishchenko
Options

Adding args to command %yosys.

parent 0ed81b34
Showing with 60 additions and 19 deletions
src/base/wln/wlnBlast.c
......@@ -289,9 +289,17 @@ void Rtl_NtkBlastNode( Gia_Man_t * pNew, int Type, int nIns, Vec_Int_t * vDatas,
{
int fBooth = 1;
int fCla = 0;
int fSigned = fSign0 && fSign1;
int fSigned = fSign0 && fSign1;
//int i, iObj;
Vec_IntShrink( vArg0, nSizeArg0 );
Vec_IntShrink( vArg1, nSizeArg1 );
//printf( "Adding %d + %d + %d buffers\n", nSizeArg0, nSizeArg1, nRange );
//Vec_IntForEachEntry( vArg0, iObj, i )
// Vec_IntWriteEntry( vArg0, i, Gia_ManAppendBuf(pNew, iObj) );
//Vec_IntForEachEntry( vArg1, iObj, i )
// Vec_IntWriteEntry( vArg1, i, Gia_ManAppendBuf(pNew, iObj) );
if ( Wlc_NtkCountConstBits(Vec_IntArray(vArg0), Vec_IntSize(vArg0)) < Wlc_NtkCountConstBits(Vec_IntArray(vArg1), Vec_IntSize(vArg1)) )
ABC_SWAP( Vec_Int_t, *vArg0, *vArg1 )
if ( fBooth )
......@@ -303,6 +311,9 @@ void Rtl_NtkBlastNode( Gia_Man_t * pNew, int Type, int nIns, Vec_Int_t * vDatas,
else
Vec_IntShrink( vRes, nRange );
assert( Vec_IntSize(vRes) == nRange );
//Vec_IntForEachEntry( vRes, iObj, i )
// Vec_IntWriteEntry( vRes, i, Gia_ManAppendBuf(pNew, iObj) );
return;
}
if ( Type == ABC_OPER_ARI_DIV || Type == ABC_OPER_ARI_MOD )
......
src/base/wln/wlnCom.c
......@@ -92,12 +92,13 @@ void Wln_End( Abc_Frame_t * pAbc )
******************************************************************************/
int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
{
extern Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, int fSkipStrash, int fInvert, int fTechMap, int fVerbose );
extern Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, int fCollapse, int fVerbose );
extern Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fVerbose );
extern Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fCollapse, int fVerbose );
FILE * pFile;
char * pFileName = NULL;
char * pTopModule= NULL;
char * pDefines = NULL;
int fBlast = 0;
int fInvert = 0;
int fTechMap = 1;
......@@ -105,7 +106,7 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
int fCollapse = 0;
int c, fVerbose = 0;
Extra_UtilGetoptReset();
while ( ( c = Extra_UtilGetopt( argc, argv, "Tbismcvh" ) ) != EOF )
while ( ( c = Extra_UtilGetopt( argc, argv, "TDbismcvh" ) ) != EOF )
{
switch ( c )
{
......@@ -118,6 +119,15 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
pTopModule = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'D':
if ( globalUtilOptind >= argc )
{
Abc_Print( -1, "Command line switch \"-D\" should be followed by a file name.\n" );
goto usage;
}
pDefines = argv[globalUtilOptind];
globalUtilOptind++;
break;
case 'b':
fBlast ^= 1;
break;
......@@ -164,11 +174,11 @@ 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, fSkipStrash, fInvert, fTechMap, fVerbose );
pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fVerbose );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) )
pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose );
pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fVerbose );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) )
pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose );
pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fVerbose );
else
{
printf( "Abc_CommandYosys(): Unknown file extension.\n" );
......@@ -180,11 +190,11 @@ 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( pFileName, pTopModule, fCollapse, fVerbose );
pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) )
pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, fCollapse, fVerbose );
pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose );
else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) )
pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, fCollapse, fVerbose );
pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose );
else
{
printf( "Abc_CommandYosys(): Unknown file extension.\n" );
......@@ -194,11 +204,12 @@ int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
}
return 0;
usage:
Abc_Print( -2, "usage: %%yosys [-T <module>] [-bismcvh] <file_name>\n" );
Abc_Print( -2, "usage: %%yosys [-T <module>] [-D <defines>] [-bismcvh] <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-D : specify defines to be used by Yosys (default \"not used\")\n" );
Abc_Print( -2, "\t-b : toggle bit-blasting the design into an AIG using Yosys [default = %s]\n", fBlast? "yes": "no" );
Abc_Print( -2, "\t-i : toggle interting the outputs (useful for miters) [default = %s]\n", fInvert? "yes": "no" );
Abc_Print( -2, "\t-i : toggle inverting the outputs (useful for miters) [default = %s]\n", fInvert? "yes": "no" );
Abc_Print( -2, "\t-s : toggle no structural hashing during bit-blasting [default = %s]\n", fSkipStrash? "no strash": "strash" );
Abc_Print( -2, "\t-m : toggle using \"techmap\" to blast operators [default = %s]\n", fTechMap? "yes": "no" );
Abc_Print( -2, "\t-c : toggle collapsing design hierarchy using Yosys [default = %s]\n", fCollapse? "yes": "no" );
......
src/base/wln/wlnRtl.c
......@@ -135,7 +135,7 @@ int Wln_ConvertToRtl( char * pCommand, char * pFileTemp )
fclose( pFile );
return 1;
}
Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, int fCollapse, int fVerbose )
Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fCollapse, int fVerbose )
{
Rtl_Lib_t * pNtk = NULL;
char Command[1000];
......@@ -143,8 +143,10 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, int fCol
int fSVlog = strstr(pFileName, ".sv") != NULL;
if ( strstr(pFileName, ".rtl") )
return Rtl_LibReadFile( pFileName, pFileName );
sprintf( Command, "%s -qp \"read_verilog %s%s; hierarchy %s%s; %sproc; write_rtlil %s\"",
Wln_GetYosysName(), fSVlog ? "-sv ":"", pFileName,
sprintf( Command, "%s -qp \"read_verilog %s %s%s; hierarchy %s%s; %sproc; write_rtlil %s\"",
Wln_GetYosysName(),
pDefines ? pDefines : "",
fSVlog ? "-sv ":"", pFileName,
pTopModule ? "-top " : "",
pTopModule ? pTopModule : "",
fCollapse ? "flatten; " : "",
......@@ -163,16 +165,17 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, int fCol
unlink( pFileTemp );
return pNtk;
}
Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, int fSkipStrash, int fInvert, int fTechMap, int fVerbose )
Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, 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; hierarchy %s%s; flatten; proc; %saigmap; write_aiger %s\"",
sprintf( Command, "%s -qp \"%s %s%s%s; hierarchy %s%s; flatten; proc; %saigmap; write_aiger %s\"",
Wln_GetYosysName(),
fRtlil ? "read_rtlil" : "read_verilog",
pDefines ? pDefines : "",
fSVlog ? " -sv ":" ",
pFileName,
pTopModule ? "-top " : "-auto-top",
......
src/proof/cec/cecClass.c
......@@ -265,10 +265,13 @@ void Cec_ManSimClassCreate( Gia_Man_t * p, Vec_Int_t * vClass )
SeeAlso []
***********************************************************************/
int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i )
static int s_Count = 0;
int Cec_ManSimClassRefineOne_rec( Cec_ManSim_t * p, int i )
{
unsigned * pSim0, * pSim1;
int Ent;
s_Count++;
Vec_IntClear( p->vClassOld );
Vec_IntClear( p->vClassNew );
Vec_IntPush( p->vClassOld, i );
......@@ -290,9 +293,22 @@ int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i )
Cec_ManSimClassCreate( p->pAig, p->vClassOld );
Cec_ManSimClassCreate( p->pAig, p->vClassNew );
if ( Vec_IntSize(p->vClassNew) > 1 )
return 1 + Cec_ManSimClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
return 1 + Cec_ManSimClassRefineOne_rec( p, Vec_IntEntry(p->vClassNew,0) );
return 1;
}
int Cec_ManSimClassRefineOne_( Cec_ManSim_t * p, int i )
{
int Res;
s_Count = 0;
Res = Cec_ManSimClassRefineOne_rec( p, i );
if ( s_Count > 10 )
printf( "%d ", s_Count );
return Res;
}
int Cec_ManSimClassRefineOne( Cec_ManSim_t * p, int i )
{
return Cec_ManSimClassRefineOne_rec( p, i );
}
/**Function*************************************************************
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment