From b69f439609c248db1f17408d550693fec30cbea5 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 19 Sep 2022 10:48:41 -0700 Subject: Adding args to command %yosys. --- src/base/wln/wlnBlast.c | 13 ++++++++++++- src/base/wln/wlnCom.c | 33 ++++++++++++++++++++++----------- src/base/wln/wlnRtl.c | 13 ++++++++----- src/proof/cec/cecClass.c | 20 ++++++++++++++++++-- 4 files changed, 60 insertions(+), 19 deletions(-) diff --git a/src/base/wln/wlnBlast.c b/src/base/wln/wlnBlast.c index a3ac73c0..887412d6 100644 --- a/src/base/wln/wlnBlast.c +++ b/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 ) diff --git a/src/base/wln/wlnCom.c b/src/base/wln/wlnCom.c index c5411607..09cbe90f 100644 --- a/src/base/wln/wlnCom.c +++ b/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 ] [-bismcvh] \n" ); + Abc_Print( -2, "usage: %%yosys [-T ] [-D ] [-bismcvh] \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" ); diff --git a/src/base/wln/wlnRtl.c b/src/base/wln/wlnRtl.c index fa0f0cd5..51e00eb6 100644 --- a/src/base/wln/wlnRtl.c +++ b/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", diff --git a/src/proof/cec/cecClass.c b/src/proof/cec/cecClass.c index be88b9be..60fdbc89 100644 --- a/src/proof/cec/cecClass.c +++ b/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************************************************************* -- cgit v1.2.3