diff options
| -rw-r--r-- | abclib.dsp | 8 | ||||
| -rw-r--r-- | src/base/main/mainInit.c | 4 | ||||
| -rw-r--r-- | src/base/wlc/wlcCom.c | 220 | ||||
| -rw-r--r-- | src/base/wln/module.make | 2 | ||||
| -rw-r--r-- | src/base/wln/wlnCom.c | 353 | ||||
| -rw-r--r-- | src/base/wln/wlnGuide.c | 73 | ||||
| -rw-r--r-- | src/base/wln/wlnRead.c | 132 | ||||
| -rw-r--r-- | src/base/wln/wlnRtl.c | 2 |
8 files changed, 570 insertions, 224 deletions
@@ -1131,6 +1131,14 @@ SOURCE=.\src\base\wln\wlnBlast.c # End Source File # Begin Source File +SOURCE=.\src\base\wln\wlnCom.c +# End Source File +# Begin Source File + +SOURCE=.\src\base\wln\wlnGuide.c +# End Source File +# Begin Source File + SOURCE=.\src\base\wln\wlnMem.c # End Source File # Begin Source File diff --git a/src/base/main/mainInit.c b/src/base/main/mainInit.c index 693cea90..d3ce672f 100644 --- a/src/base/main/mainInit.c +++ b/src/base/main/mainInit.c @@ -49,6 +49,8 @@ extern void Scl_Init( Abc_Frame_t * pAbc ); extern void Scl_End( Abc_Frame_t * pAbc ); extern void Wlc_Init( Abc_Frame_t * pAbc ); extern void Wlc_End( Abc_Frame_t * pAbc ); +extern void Wln_Init( Abc_Frame_t * pAbc ); +extern void Wln_End( Abc_Frame_t * pAbc ); extern void Bac_Init( Abc_Frame_t * pAbc ); extern void Bac_End( Abc_Frame_t * pAbc ); extern void Cba_Init( Abc_Frame_t * pAbc ); @@ -116,6 +118,7 @@ void Abc_FrameInit( Abc_Frame_t * pAbc ) Load_Init( pAbc ); Scl_Init( pAbc ); Wlc_Init( pAbc ); + Wln_Init( pAbc ); Bac_Init( pAbc ); Cba_Init( pAbc ); Pla_Init( pAbc ); @@ -156,6 +159,7 @@ void Abc_FrameEnd( Abc_Frame_t * pAbc ) Load_End( pAbc ); Scl_End( pAbc ); Wlc_End( pAbc ); + Wln_End( pAbc ); Bac_End( pAbc ); Cba_End( pAbc ); Pla_End( pAbc ); diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c index 2ea17169..dd7a3e32 100644 --- a/src/base/wlc/wlcCom.c +++ b/src/base/wlc/wlcCom.c @@ -54,20 +54,12 @@ static int Abc_CommandInvPut ( Abc_Frame_t * pAbc, int argc, char ** argv ) static int Abc_CommandInvMin ( Abc_Frame_t * pAbc, int argc, char ** argv ); static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandYosys ( Abc_Frame_t * pAbc, int argc, char ** argv ); -static int Abc_CommandSolve ( Abc_Frame_t * pAbc, int argc, char ** argv ); - static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc ) { return (Wlc_Ntk_t *)pAbc->pAbcWlc; } 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 inline Vec_Int_t * Wlc_AbcGetInv( Abc_Frame_t * pAbc ) { return pAbc->pAbcWlcInv; } - -static inline Rtl_Lib_t * Wlc_AbcGetRtl( Abc_Frame_t * pAbc ) { return (Rtl_Lib_t *)pAbc->pAbcRtl; } -static inline void Wlc_AbcFreeRtl( Abc_Frame_t * pAbc ) { if ( pAbc->pAbcRtl ) Rtl_LibFree(Wlc_AbcGetRtl(pAbc)); } -static inline void Wlc_AbcUpdateRtl( Abc_Frame_t * pAbc, Rtl_Lib_t * pLib ) { Wlc_AbcFreeRtl(pAbc); pAbc->pAbcRtl = pLib; } - //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -103,9 +95,6 @@ void Wlc_Init( Abc_Frame_t * pAbc ) Cmd_CommandAdd( pAbc, "Word level", "%show", Abc_CommandShow, 0 ); Cmd_CommandAdd( pAbc, "Word level", "%test", Abc_CommandTest, 0 ); - Cmd_CommandAdd( pAbc, "Word level", "%yosys", Abc_CommandYosys, 0 ); - Cmd_CommandAdd( pAbc, "Word level", "%solve", Abc_CommandSolve, 0 ); - Cmd_CommandAdd( pAbc, "Word level", "inv_ps", Abc_CommandInvPs, 0 ); Cmd_CommandAdd( pAbc, "Word level", "inv_print", Abc_CommandInvPrint, 0 ); Cmd_CommandAdd( pAbc, "Word level", "inv_check", Abc_CommandInvCheck, 0 ); @@ -1982,215 +1971,6 @@ usage: return 1; } - -/**Function******************************************************************** - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -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 ); - - FILE * pFile; - char * pFileName = NULL; - char * pTopModule= NULL; - int fBlast = 0; - int fInvert = 0; - int fTechMap = 1; - int fSkipStrash = 0; - int fCollapse = 0; - int c, fVerbose = 0; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "Tbismcvh" ) ) != EOF ) - { - switch ( c ) - { - case 'T': - if ( globalUtilOptind >= argc ) - { - Abc_Print( -1, "Command line switch \"-T\" should be followed by a file name.\n" ); - goto usage; - } - pTopModule = argv[globalUtilOptind]; - globalUtilOptind++; - break; - case 'b': - fBlast ^= 1; - break; - case 'i': - fInvert ^= 1; - break; - case 's': - fSkipStrash ^= 1; - break; - case 'm': - fTechMap ^= 1; - break; - case 'c': - fCollapse ^= 1; - break; - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; - } - } - if ( argc != globalUtilOptind + 1 ) - { - printf( "Abc_CommandReadWlc(): Input file name should be given on the command line.\n" ); - return 0; - } - // get the file name - pFileName = argv[globalUtilOptind]; - if ( (pFile = fopen( pFileName, "r" )) == NULL ) - { - Abc_Print( 1, "Cannot open input file \"%s\". ", pFileName ); - if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".sv", NULL, NULL, NULL )) ) - Abc_Print( 1, "Did you mean \"%s\"?", pFileName ); - Abc_Print( 1, "\n" ); - return 0; - } - fclose( pFile ); - - // perform reading - if ( fBlast ) - { - Gia_Man_t * pNew = NULL; - if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) - pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose ); - else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) ) - pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose ); - else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) ) - pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose ); - else - { - printf( "Abc_CommandYosys(): Unknown file extension.\n" ); - return 0; - } - Abc_FrameUpdateGia( pAbc, pNew ); - } - else - { - Rtl_Lib_t * pLib = NULL; - if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) - pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, fCollapse, fVerbose ); - else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) ) - pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, fCollapse, fVerbose ); - else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) ) - pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, fCollapse, fVerbose ); - else - { - printf( "Abc_CommandYosys(): Unknown file extension.\n" ); - return 0; - } - Wlc_AbcUpdateRtl( pAbc, pLib ); - } - return 0; -usage: - Abc_Print( -2, "usage: %%yosys [-T <module>] [-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-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-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" ); - 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"); - return 1; -} - -/**Function******************************************************************** - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -******************************************************************************/ -int Abc_CommandSolve( Abc_Frame_t * pAbc, int argc, char ** argv ) -{ - extern void Rtl_LibPrintStats( Rtl_Lib_t * p ); - extern void Rtl_LibPrint( char * pFileName, Rtl_Lib_t * p ); - extern void Rtl_LibNormRanges( Rtl_Lib_t * pLib ); - extern void Rtl_LibOrderWires( Rtl_Lib_t * pLib ); - extern void Rtl_LibOrderCells( Rtl_Lib_t * pLib ); - extern void Rtl_LibBlast( Rtl_Lib_t * pLib ); - extern void Rtl_LibBlast2( Rtl_Lib_t * pLib ); - extern void Rtl_LibReorderModules( Rtl_Lib_t * pLib ); - extern void Rtl_LibSolve( Rtl_Lib_t * pLib ); - extern void Rtl_LibPreprocess( Rtl_Lib_t * pLib ); - - Gia_Man_t * pGia = NULL; - Rtl_Lib_t * pLib = Wlc_AbcGetRtl(pAbc); - int c, fOldBlast = 0, fPrepro = 0, fVerbose = 0; - Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "opvh" ) ) != EOF ) - { - switch ( c ) - { - case 'o': - fOldBlast ^= 1; - break; - case 'p': - fPrepro ^= 1; - break; - case 'v': - fVerbose ^= 1; - break; - case 'h': - goto usage; - default: - goto usage; - } - } - Rtl_LibPrintStats( pLib ); - //Rtl_LibPrint( NULL, pLib ); - Rtl_LibOrderWires( pLib ); - - if ( fOldBlast ) - { - Rtl_LibOrderCells( pLib ); - Rtl_LibBlast( pLib ); - } - else - Rtl_LibBlast2( pLib ); - //Rtl_LibReorderModules( pLib ); - //Rtl_LibPrintStats( pLib ); - - if ( fPrepro ) - Rtl_LibPreprocess( pLib ); - Rtl_LibSolve( pLib ); - - //Rtl_LibPrint( NULL, pLib ); - Wlc_AbcUpdateRtl( pAbc, NULL ); - Gia_ManStopP( &pGia ); - return 0; -usage: - Abc_Print( -2, "usage: %%solve [-opvh]\n" ); - Abc_Print( -2, "\t experiments with word-level networks\n" ); - Abc_Print( -2, "\t-o : toggle using old bit-blasting procedure [default = %s]\n", fOldBlast? "yes": "no" ); - Abc_Print( -2, "\t-p : toggle preprocessing for verification [default = %s]\n", fPrepro? "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"); - return 1; -} - - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/wln/module.make b/src/base/wln/module.make index 7277f30b..c1939126 100644 --- a/src/base/wln/module.make +++ b/src/base/wln/module.make @@ -1,5 +1,7 @@ SRC += src/base/wln/wln.c \ src/base/wln/wlnBlast.c \ + src/base/wln/wlnCom.c \ + src/base/wln/wlnGuide.c \ src/base/wln/wlnMem.c \ src/base/wln/wlnNdr.c \ src/base/wln/wlnNtk.c \ diff --git a/src/base/wln/wlnCom.c b/src/base/wln/wlnCom.c new file mode 100644 index 00000000..3db27785 --- /dev/null +++ b/src/base/wln/wlnCom.c @@ -0,0 +1,353 @@ +/**CFile**************************************************************** + + FileName [wlnCom.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Word-level network.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 23, 2018.] + + Revision [$Id: wlnCom.c,v 1.00 2018/09/23 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "wln.h" +#include "base/main/mainInt.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +static int Abc_CommandYosys ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandSolve ( Abc_Frame_t * pAbc, int argc, char ** argv ); +static int Abc_CommandPrint ( Abc_Frame_t * pAbc, int argc, char ** argv ); + +static inline Rtl_Lib_t * Wln_AbcGetRtl( Abc_Frame_t * pAbc ) { return (Rtl_Lib_t *)pAbc->pAbcRtl; } +static inline void Wln_AbcFreeRtl( Abc_Frame_t * pAbc ) { if ( pAbc->pAbcRtl ) Rtl_LibFree(Wln_AbcGetRtl(pAbc)); } +static inline void Wln_AbcUpdateRtl( Abc_Frame_t * pAbc, Rtl_Lib_t * pLib ) { Wln_AbcFreeRtl(pAbc); pAbc->pAbcRtl = pLib; } + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Wln_Init( Abc_Frame_t * pAbc ) +{ + Cmd_CommandAdd( pAbc, "Word level", "%yosys", Abc_CommandYosys, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%solve", Abc_CommandSolve, 0 ); + Cmd_CommandAdd( pAbc, "Word level", "%print", Abc_CommandPrint, 0 ); +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +void Wln_End( Abc_Frame_t * pAbc ) +{ + Wln_AbcUpdateRtl( pAbc, NULL ); +} + + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +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 ); + + FILE * pFile; + char * pFileName = NULL; + char * pTopModule= NULL; + int fBlast = 0; + int fInvert = 0; + int fTechMap = 1; + int fSkipStrash = 0; + int fCollapse = 0; + int c, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "Tbismcvh" ) ) != EOF ) + { + switch ( c ) + { + case 'T': + if ( globalUtilOptind >= argc ) + { + Abc_Print( -1, "Command line switch \"-T\" should be followed by a file name.\n" ); + goto usage; + } + pTopModule = argv[globalUtilOptind]; + globalUtilOptind++; + break; + case 'b': + fBlast ^= 1; + break; + case 'i': + fInvert ^= 1; + break; + case 's': + fSkipStrash ^= 1; + break; + case 'm': + fTechMap ^= 1; + break; + case 'c': + fCollapse ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( argc != globalUtilOptind + 1 ) + { + printf( "Abc_CommandReadWlc(): Input file name should be given on the command line.\n" ); + return 0; + } + // get the file name + pFileName = argv[globalUtilOptind]; + if ( (pFile = fopen( pFileName, "r" )) == NULL ) + { + Abc_Print( 1, "Cannot open input file \"%s\". ", pFileName ); + if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".sv", NULL, NULL, NULL )) ) + Abc_Print( 1, "Did you mean \"%s\"?", pFileName ); + Abc_Print( 1, "\n" ); + return 0; + } + fclose( pFile ); + + // perform reading + if ( fBlast ) + { + Gia_Man_t * pNew = NULL; + if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) + pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose ); + else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) ) + pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose ); + else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) ) + pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, fSkipStrash, fInvert, fTechMap, fVerbose ); + else + { + printf( "Abc_CommandYosys(): Unknown file extension.\n" ); + return 0; + } + Abc_FrameUpdateGia( pAbc, pNew ); + } + else + { + Rtl_Lib_t * pLib = NULL; + if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) ) + pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, fCollapse, fVerbose ); + else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) ) + pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, fCollapse, fVerbose ); + else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) ) + pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, fCollapse, fVerbose ); + else + { + printf( "Abc_CommandYosys(): Unknown file extension.\n" ); + return 0; + } + Wln_AbcUpdateRtl( pAbc, pLib ); + } + return 0; +usage: + Abc_Print( -2, "usage: %%yosys [-T <module>] [-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-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-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" ); + 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"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Abc_CommandPrint( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Rtl_LibPrintStats( Rtl_Lib_t * p ); + extern void Rtl_LibPrintHieStats( Rtl_Lib_t * p ); + extern void Rtl_LibPrint( char * pFileName, Rtl_Lib_t * p ); + Rtl_Lib_t * pLib = Wln_AbcGetRtl(pAbc); + int c, fHie = 0, fDesign = 0, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "pdvh" ) ) != EOF ) + { + switch ( c ) + { + case 'p': + fHie ^= 1; + break; + case 'd': + fDesign ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pLib == NULL ) + { + printf( "The design is not entered.\n" ); + return 1; + } + Rtl_LibPrintStats( pLib ); + if ( fHie ) + Rtl_LibPrintHieStats( pLib ); + if ( fDesign ) + Rtl_LibPrint( NULL, pLib ); + return 0; +usage: + Abc_Print( -2, "usage: %%print [-pdvh]\n" ); + Abc_Print( -2, "\t print statistics about the hierarchical design\n" ); + Abc_Print( -2, "\t-p : toggle printing of the hierarchy [default = %s]\n", fHie? "yes": "no" ); + Abc_Print( -2, "\t-d : toggle printing of the design [default = %s]\n", fDesign? "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"); + Abc_Print( -2, "\t<file> : text file name with guidance for solving\n"); + return 1; +} + +/**Function******************************************************************** + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +******************************************************************************/ +int Abc_CommandSolve( Abc_Frame_t * pAbc, int argc, char ** argv ) +{ + extern void Rtl_LibBlast( Rtl_Lib_t * pLib ); + extern void Rtl_LibBlast2( Rtl_Lib_t * pLib ); + extern void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk ); + extern void Rtl_LibPreprocess( Rtl_Lib_t * pLib ); + extern void Wln_SolveWithGuidance( char * pFileName, Rtl_Lib_t * p ); + + Rtl_Lib_t * pLib = Wln_AbcGetRtl(pAbc); + int c, fOldBlast = 0, fPrepro = 0, fVerbose = 0; + Extra_UtilGetoptReset(); + while ( ( c = Extra_UtilGetopt( argc, argv, "opvh" ) ) != EOF ) + { + switch ( c ) + { + case 'o': + fOldBlast ^= 1; + break; + case 'p': + fPrepro ^= 1; + break; + case 'v': + fVerbose ^= 1; + break; + case 'h': + goto usage; + default: + goto usage; + } + } + if ( pLib == NULL ) + { + printf( "The design is not entered.\n" ); + return 1; + } + if ( argc == globalUtilOptind + 1 ) + { + char * pFileName = argv[globalUtilOptind]; + FILE * pFile = fopen( pFileName, "r" ); + if ( pFile == NULL ) + { + Abc_Print( -1, "Cannot open file \"%s\" with the input test patterns.\n", pFileName ); + return 0; + } + fclose( pFile ); + printf( "Using guidance from file \"%s\".\n", pFileName ); + Wln_SolveWithGuidance( pFileName, pLib ); + } + else + { + printf( "Solving the miter without guidance.\n" ); + if ( fOldBlast ) + Rtl_LibBlast( pLib ); + else + Rtl_LibBlast2( pLib ); + if ( fPrepro ) + Rtl_LibPreprocess( pLib ); + Rtl_LibSolve( pLib, NULL ); + } + return 0; +usage: + Abc_Print( -2, "usage: %%solve [-opvh] <file>\n" ); + Abc_Print( -2, "\t solving properties for the hierarchical design\n" ); + Abc_Print( -2, "\t-o : toggle using old bit-blasting procedure [default = %s]\n", fOldBlast? "yes": "no" ); + Abc_Print( -2, "\t-p : toggle preprocessing for verification [default = %s]\n", fPrepro? "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"); + Abc_Print( -2, "\t<file> : text file name with guidance for solving\n"); + return 1; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/base/wln/wlnGuide.c b/src/base/wln/wlnGuide.c new file mode 100644 index 00000000..abe9a6d8 --- /dev/null +++ b/src/base/wln/wlnGuide.c @@ -0,0 +1,73 @@ +/**CFile**************************************************************** + + FileName [wln.c] + + SystemName [ABC: Logic synthesis and verification system.] + + PackageName [Word-level network.] + + Synopsis [] + + Author [Alan Mishchenko] + + Affiliation [UC Berkeley] + + Date [Ver. 1.0. Started - September 23, 2018.] + + Revision [$Id: wln.c,v 1.00 2018/09/23 00:00:00 alanmi Exp $] + +***********************************************************************/ + +#include "wln.h" + +ABC_NAMESPACE_IMPL_START + +//////////////////////////////////////////////////////////////////////// +/// DECLARATIONS /// +//////////////////////////////////////////////////////////////////////// + +//////////////////////////////////////////////////////////////////////// +/// FUNCTION DEFINITIONS /// +//////////////////////////////////////////////////////////////////////// + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +Vec_Int_t * Wln_ReadGuidance( char * pFileName, Abc_Nam_t * p ) +{ + char Buffer[1000] = {'\\'}, * pBuffer = Buffer+1; + Vec_Int_t * vTokens = Vec_IntAlloc( 100 ); + FILE * pFile = fopen( pFileName, "rb" ); + while ( fscanf( pFile, "%s", pBuffer ) == 1 ) + { + if ( pBuffer[(int)strlen(pBuffer)-1] == '\r' ) + pBuffer[(int)strlen(pBuffer)-1] = 0; + if ( !strcmp(pBuffer, "prove") && Vec_IntSize(vTokens) % 4 == 3 ) // account for "property" + Vec_IntPush( vTokens, -1 ); + if ( Vec_IntSize(vTokens) % 4 == 2 || Vec_IntSize(vTokens) % 4 == 3 ) + Vec_IntPush( vTokens, Abc_NamStrFindOrAdd(p, Buffer, NULL) ); + else + Vec_IntPush( vTokens, Abc_NamStrFindOrAdd(p, pBuffer, NULL) ); + } + fclose( pFile ); + if ( Vec_IntSize(vTokens) % 4 == 3 ) // account for "property" + Vec_IntPush( vTokens, -1 ); + assert( Vec_IntSize(vTokens) % 4 == 0 ); + return vTokens; +} + +//////////////////////////////////////////////////////////////////////// +/// END OF FILE /// +//////////////////////////////////////////////////////////////////////// + + +ABC_NAMESPACE_IMPL_END + diff --git a/src/base/wln/wlnRead.c b/src/base/wln/wlnRead.c index 62cb70c6..bc4211ac 100644 --- a/src/base/wln/wlnRead.c +++ b/src/base/wln/wlnRead.c @@ -78,6 +78,8 @@ struct Rtl_Ntk_t_ static inline int Rtl_LibNtkNum( Rtl_Lib_t * pLib ) { return Vec_PtrSize(pLib->vNtks); } static inline Rtl_Ntk_t * Rtl_LibNtk( Rtl_Lib_t * pLib, int i ) { return (Rtl_Ntk_t *)Vec_PtrEntry(pLib->vNtks, i); } static inline Rtl_Ntk_t * Rtl_LibTop( Rtl_Lib_t * pLib ) { return Rtl_LibNtk( pLib, Rtl_LibNtkNum(pLib)-1 ); } +static inline char * Rtl_LibStr( Rtl_Lib_t * pLib, int h ) { return Abc_NamStr(pLib->pManName, h); } +static inline int Rtl_LibStrId( Rtl_Lib_t * pLib, char * s ) { return Abc_NamStrFind(pLib->pManName, s); } static inline Rtl_Ntk_t * Rtl_NtkModule( Rtl_Ntk_t * p, int i ) { return Rtl_LibNtk( p->pLib, i ); } @@ -254,6 +256,50 @@ void Rtl_NtkPrintStats( Rtl_Ntk_t * p, int nNameSymbs ) SeeAlso [] ***********************************************************************/ +void Rtl_NtkPrintHieStats( Rtl_Ntk_t * p, int nOffset ) +{ + Vec_Int_t * vFound = Vec_IntAlloc( 100 ); + int i, * pCell; + for ( i = 0; i < 5*(nOffset-1); i++ ) + printf( " " ); + if ( nOffset ) + printf( "|--> " ); + printf( "%s\n", Rtl_NtkName(p) ); + Rtl_NtkForEachCell( p, pCell, i ) + if ( Rtl_CellModule(pCell) >= ABC_INFINITY ) + { + Rtl_Ntk_t * pModel = Rtl_NtkModule( p, Rtl_CellModule(pCell)-ABC_INFINITY ); + assert( pCell[6] == pModel->nInputs+pModel->nOutputs ); + if ( Vec_IntFind(vFound, pModel->NameId) >= 0 ) + continue; + Vec_IntPush( vFound, pModel->NameId ); + Rtl_NtkPrintHieStats( pModel, nOffset+1 ); + } + Vec_IntFree( vFound ); +} +void Rtl_LibPrintHieStats( Rtl_Lib_t * p ) +{ + Rtl_Ntk_t * pNtk; int i; + printf( "Hierarchy found in \"%s\":\n", p->pSpec ); + Vec_PtrForEachEntry( Rtl_Ntk_t *, p->vNtks, pNtk, i ) + { + printf( "\n" ); + printf( "MODULE %d: ", i ); + Rtl_NtkPrintHieStats( pNtk, 0 ); + } +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ Rtl_Lib_t * Rtl_LibAlloc() { Rtl_Lib_t * p = ABC_CALLOC( Rtl_Lib_t, 1 ); @@ -1398,6 +1444,7 @@ Rtl_Lib_t * Rtl_LibReadFile( char * pFileName, char * pFileSpec ) i = Rtl_NtkReadAttribute2( p, i+1 ); Rtl_LibSetParents( p ); Rtl_LibReorderModules( p ); + Rtl_LibOrderWires( p ); return p; } @@ -1733,7 +1780,7 @@ char * Rtl_ShortenName( char * pName, int nSize ) return pName; Buffer[0] = 0; strcat( Buffer, pName ); - Buffer[nSize-4] = ' '; + //Buffer[nSize-4] = ' '; Buffer[nSize-3] = '.'; Buffer[nSize-2] = '.'; Buffer[nSize-1] = '.'; @@ -1941,6 +1988,7 @@ void Rtl_NtkBlastPrepareInputs( Rtl_Ntk_t * p, int * pCell ) } void Rtl_NtkBlast2_rec( Rtl_Ntk_t * p, int iBit, int * pDriver ) { + //char * pName = Rtl_NtkName(p); assert( pDriver[0] != -1 ); if ( pDriver[0] == -3 ) { @@ -1981,6 +2029,7 @@ Gia_Man_t * Rtl_NtkBlast2( Rtl_Ntk_t * p ) int i, b, nBits = Rtl_NtkRangeWires( p ); char Buffer[100]; static int counter = 0; Vec_IntFill( &p->vLits, nBits, -1 ); +printf( "Blasting %s...\r", Rtl_NtkName(p) ); Rtl_NtkMapWires( p, 0 ); Rtl_NtkBlastMap( p, nBits ); assert( p->pGia == NULL ); @@ -2066,11 +2115,11 @@ finish: //Rtl_LibBlast( pLib ); Rtl_LibBlast2( pLib ); } -void Rtl_LibSolve( Rtl_Lib_t * pLib ) +void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk ) { extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose ); abctime clk = Abc_Clock(); int Status; - Rtl_Ntk_t * pTop = Rtl_LibTop( pLib ); + Rtl_Ntk_t * pTop = pNtk ? (Rtl_Ntk_t *)pNtk : Rtl_LibTop( pLib ); Gia_Man_t * pSwp = Cec4_ManSimulateTest3( pTop->pGia, 1000000, 0 ); int RetValue = Gia_ManAndNum(pSwp) == 0; Gia_ManStop( pSwp ); @@ -2092,6 +2141,83 @@ void Rtl_LibSolve( Rtl_Lib_t * pLib ) } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Wln_SolveEqual( Rtl_Lib_t * p, int iNtk1, int iNtk2 ) +{ + Rtl_Ntk_t * pNtk1 = Rtl_LibNtk( p, iNtk1 ); + Rtl_Ntk_t * pNtk2 = Rtl_LibNtk( p, iNtk2 ); + printf( "Proving equivalence of \"%s\" and \"%s\".\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) ); +/* + if ( Gia_ManCiNum(pNtk1->pGia) != Gia_ManCiNum(pNtk2->pGia) || + Gia_ManCoNum(pNtk1->pGia) != Gia_ManCoNum(pNtk2->pGia) ) + { + printf( "The number of inputs/outputs does not match.\n" ); + } + else + { + int Status = Cec_ManVerifyTwo( pNtk1->pGia, pNtk2->pGia, 0 ); + if ( Status == 1 ) + printf( "The networks are equivalence.\n" ); + else + printf( "The networks are NOT equivalent.\n" ); + } +*/ +} +void Wln_SolveInverse( Rtl_Lib_t * p, int iNtk1, int iNtk2 ) +{ + Rtl_Ntk_t * pNtk1 = Rtl_LibNtk( p, iNtk1 ); + Rtl_Ntk_t * pNtk2 = Rtl_LibNtk( p, iNtk2 ); + printf( "Proving inverse equivalence of \"%s\" and \"%s\".\n", Rtl_NtkName(pNtk1), Rtl_NtkName(pNtk2) ); +} +void Wln_SolveProperty( Rtl_Lib_t * p, int iNtk ) +{ + Rtl_Ntk_t * pNtk = Rtl_LibNtk( p, iNtk ); + printf( "Proving property \"%s\".\n", Rtl_NtkName(pNtk) ); + Rtl_LibSolve( p, pNtk ); +} +void Wln_SolveWithGuidance( char * pFileName, Rtl_Lib_t * p ) +{ + extern Vec_Int_t * Wln_ReadGuidance( char * pFileName, Abc_Nam_t * p ); + Vec_Int_t * vGuide = Wln_ReadGuidance( pFileName, p->pManName ); int i; + Vec_IntFillExtra( p->vMap, Abc_NamObjNumMax(p->pManName), -1 ); + Rtl_LibBlast2( p ); + for ( i = 0; i < Vec_IntSize(vGuide); i += 4 ) + { + int Prove = Vec_IntEntry( vGuide, i+0 ); + int Type = Vec_IntEntry( vGuide, i+1 ); + int Name1 = Vec_IntEntry( vGuide, i+2 ); + int Name2 = Vec_IntEntry( vGuide, i+3 ); + int iNtk1 = Rtl_LibFindModule( p, Name1 ); + int iNtk2 = Name2 == -1 ? -1 : Rtl_LibFindModule( p, Name2 ); + if ( Prove != Rtl_LibStrId(p, "prove") ) + printf( "Unknown task in line %d.\n", i/4 ); + else if ( iNtk1 == -1 ) + printf( "Network %s cannot be found in this design.\n", Rtl_LibStr(p, Name1) ); + else + { + if ( Type == Rtl_LibStrId(p, "equal") ) + Wln_SolveEqual( p, iNtk1, iNtk2 ); + else if ( Type == Rtl_LibStrId(p, "inverse") ) + Wln_SolveInverse( p, iNtk1, iNtk2 ); + else if ( Type == Rtl_LibStrId(p, "property") ) + Wln_SolveProperty( p, iNtk1 ); + continue; + } + break; + } + Vec_IntFree( vGuide ); +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/base/wln/wlnRtl.c b/src/base/wln/wlnRtl.c index 97cc9714..fa0f0cd5 100644 --- a/src/base/wln/wlnRtl.c +++ b/src/base/wln/wlnRtl.c @@ -145,7 +145,7 @@ Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, int fCol 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, - pTopModule ? "-top " : "-auto-top", + pTopModule ? "-top " : "", pTopModule ? pTopModule : "", fCollapse ? "flatten; " : "", pFileTemp ); |