ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
wlnCom.c
Go to the documentation of this file.
1
20
21#include "wln.h"
22#include "base/main/mainInt.h"
23
25
29
30static int Abc_CommandYosys ( Abc_Frame_t * pAbc, int argc, char ** argv );
31static int Abc_CommandGraft ( Abc_Frame_t * pAbc, int argc, char ** argv );
32static int Abc_CommandHierarchy ( Abc_Frame_t * pAbc, int argc, char ** argv );
33static int Abc_CommandCollapse ( Abc_Frame_t * pAbc, int argc, char ** argv );
34static int Abc_CommandSolve ( Abc_Frame_t * pAbc, int argc, char ** argv );
35static int Abc_CommandPrint ( Abc_Frame_t * pAbc, int argc, char ** argv );
36
37static inline Rtl_Lib_t * Wln_AbcGetRtl( Abc_Frame_t * pAbc ) { return (Rtl_Lib_t *)pAbc->pAbcRtl; }
38static inline void Wln_AbcFreeRtl( Abc_Frame_t * pAbc ) { if ( pAbc->pAbcRtl ) Rtl_LibFree(Wln_AbcGetRtl(pAbc)); }
39static inline void Wln_AbcUpdateRtl( Abc_Frame_t * pAbc, Rtl_Lib_t * pLib ) { Wln_AbcFreeRtl(pAbc); pAbc->pAbcRtl = pLib; }
40
44
56void Wln_Init( Abc_Frame_t * pAbc )
57{
58 Cmd_CommandAdd( pAbc, "Word level", "%yosys", Abc_CommandYosys, 0 );
59 Cmd_CommandAdd( pAbc, "Word level", "%graft", Abc_CommandGraft, 0 );
60 Cmd_CommandAdd( pAbc, "Word level", "%hierarchy", Abc_CommandHierarchy, 0 );
61 Cmd_CommandAdd( pAbc, "Word level", "%collapse", Abc_CommandCollapse, 0 );
62 //Cmd_CommandAdd( pAbc, "Word level", "%solve", Abc_CommandSolve, 0 );
63 Cmd_CommandAdd( pAbc, "Word level", "%print", Abc_CommandPrint, 0 );
64}
65
77void Wln_End( Abc_Frame_t * pAbc )
78{
79 Wln_AbcUpdateRtl( pAbc, NULL );
80}
81
93int Abc_CommandYosys( Abc_Frame_t * pAbc, int argc, char ** argv )
94{
95 extern Abc_Ntk_t * Wln_ReadMappedSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, char * pLibrary, int fVerbose );
96 extern Gia_Man_t * Wln_BlastSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fVerbose );
97 extern Rtl_Lib_t * Wln_ReadSystemVerilog( char * pFileName, char * pTopModule, char * pDefines, int fCollapse, int fVerbose );
98
99 FILE * pFile;
100 char * pFileName = NULL;
101 char * pTopModule= NULL;
102 char * pDefines = NULL;
103 char * pLibrary = NULL;
104 int fBlast = 0;
105 int fInvert = 0;
106 int fTechMap = 1;
107 int fLibInDir = 0;
108 int fSkipStrash = 0;
109 int fCollapse = 0;
110 int c, fVerbose = 0;
112 while ( ( c = Extra_UtilGetopt( argc, argv, "TDLbismlcvh" ) ) != EOF )
113 {
114 switch ( c )
115 {
116 case 'T':
117 if ( globalUtilOptind >= argc )
118 {
119 Abc_Print( -1, "Command line switch \"-T\" should be followed by a file name.\n" );
120 goto usage;
121 }
122 pTopModule = argv[globalUtilOptind];
124 break;
125 case 'D':
126 if ( globalUtilOptind >= argc )
127 {
128 Abc_Print( -1, "Command line switch \"-D\" should be followed by a file name.\n" );
129 goto usage;
130 }
131 pDefines = argv[globalUtilOptind];
133 break;
134 case 'L':
135 if ( globalUtilOptind >= argc )
136 {
137 Abc_Print( -1, "Command line switch \"-L\" should be followed by a file name.\n" );
138 goto usage;
139 }
140 pLibrary = argv[globalUtilOptind];
142 break;
143 case 'b':
144 fBlast ^= 1;
145 break;
146 case 'i':
147 fInvert ^= 1;
148 break;
149 case 's':
150 fSkipStrash ^= 1;
151 break;
152 case 'm':
153 fTechMap ^= 1;
154 break;
155 case 'l':
156 fLibInDir ^= 1;
157 break;
158 case 'c':
159 fCollapse ^= 1;
160 break;
161 case 'v':
162 fVerbose ^= 1;
163 break;
164 case 'h':
165 goto usage;
166 default:
167 goto usage;
168 }
169 }
170 if ( argc != globalUtilOptind + 1 )
171 {
172 printf( "Abc_CommandReadWlc(): Input file name should be given on the command line.\n" );
173 return 0;
174 }
175 // get the file name
176 pFileName = argv[globalUtilOptind];
177 if ( (pFile = fopen( pFileName, "r" )) == NULL )
178 {
179 Abc_Print( 1, "Cannot open input file \"%s\". ", pFileName );
180 if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".sv", NULL, NULL, NULL )) )
181 Abc_Print( 1, "Did you mean \"%s\"?", pFileName );
182 Abc_Print( 1, "\n" );
183 return 0;
184 }
185 fclose( pFile );
186
187 // perform reading
188 if ( pLibrary )
189 {
190 Abc_Ntk_t * pNtk = NULL;
191 if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
192 pNtk = Wln_ReadMappedSystemVerilog( pFileName, pTopModule, pDefines, pLibrary, fVerbose );
193 else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) )
194 pNtk = Wln_ReadMappedSystemVerilog( pFileName, pTopModule, pDefines, pLibrary, fVerbose );
195 else
196 {
197 printf( "Abc_CommandYosys(): Unknown file extension.\n" );
198 return 0;
199 }
200 Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
201 }
202 else if ( fBlast )
203 {
204 Gia_Man_t * pNew = NULL;
205 if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
206 pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fVerbose );
207 else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) )
208 pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fVerbose );
209 else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) )
210 pNew = Wln_BlastSystemVerilog( pFileName, pTopModule, pDefines, fSkipStrash, fInvert, fTechMap, fLibInDir, fVerbose );
211 else
212 {
213 printf( "Abc_CommandYosys(): Unknown file extension.\n" );
214 return 0;
215 }
216 Abc_FrameUpdateGia( pAbc, pNew );
217 }
218 else
219 {
220 Rtl_Lib_t * pLib = NULL;
221 if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
222 pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose );
223 else if ( !strcmp( Extra_FileNameExtension(pFileName), "sv" ) )
224 pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose );
225 else if ( !strcmp( Extra_FileNameExtension(pFileName), "rtlil" ) )
226 pLib = Wln_ReadSystemVerilog( pFileName, pTopModule, pDefines, fCollapse, fVerbose );
227 else
228 {
229 printf( "Abc_CommandYosys(): Unknown file extension.\n" );
230 return 0;
231 }
232 Wln_AbcUpdateRtl( pAbc, pLib );
233 }
234 return 0;
235usage:
236 Abc_Print( -2, "usage: %%yosys [-T <module>] [-D <defines>] [-L <liberty_file>] [-bismlcvh] <file_name>\n" );
237 Abc_Print( -2, "\t reads Verilog or SystemVerilog using Yosys\n" );
238 Abc_Print( -2, "\t-T : specify the top module name (default uses \"-auto-top\")\n" );
239 Abc_Print( -2, "\t-D : specify defines to be used by Yosys (default \"not used\")\n" );
240 Abc_Print( -2, "\t-L : specify the Liberty library to read a mapped design (default \"not used\")\n" );
241 Abc_Print( -2, "\t-b : toggle bit-blasting the design into an AIG using Yosys [default = %s]\n", fBlast? "yes": "no" );
242 Abc_Print( -2, "\t-i : toggle inverting the outputs (useful for miters) [default = %s]\n", fInvert? "yes": "no" );
243 Abc_Print( -2, "\t-s : toggle no structural hashing during bit-blasting [default = %s]\n", fSkipStrash? "no strash": "strash" );
244 Abc_Print( -2, "\t-m : toggle using \"techmap\" to blast operators [default = %s]\n", fTechMap? "yes": "no" );
245 Abc_Print( -2, "\t-l : toggle looking for \"techmap.v\" in the current directory [default = %s]\n", fLibInDir? "yes": "no" );
246 Abc_Print( -2, "\t-c : toggle collapsing design hierarchy using Yosys [default = %s]\n", fCollapse? "yes": "no" );
247 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
248 Abc_Print( -2, "\t-h : print the command usage\n");
249 return 1;
250}
251
263int Abc_CommandGraft( Abc_Frame_t * pAbc, int argc, char ** argv )
264{
265 extern void Wln_LibGraftOne( Rtl_Lib_t * p, char ** pModules, int nModules, int fInv, int fVerbose );
266 Rtl_Lib_t * pLib = Wln_AbcGetRtl(pAbc);
267 char ** pArgvNew; int nArgcNew;
268 int c, fInv = 0, fVerbose = 0;
270 while ( ( c = Extra_UtilGetopt( argc, argv, "ivh" ) ) != EOF )
271 {
272 switch ( c )
273 {
274 case 'i':
275 fInv ^= 1;
276 break;
277 case 'v':
278 fVerbose ^= 1;
279 break;
280 case 'h':
281 goto usage;
282 default:
283 goto usage;
284 }
285 }
286 if ( pLib == NULL )
287 {
288 printf( "The design is not entered.\n" );
289 return 1;
290 }
291 pArgvNew = argv + globalUtilOptind;
292 nArgcNew = argc - globalUtilOptind;
293 if ( nArgcNew != 0 && nArgcNew != 2 )
294 {
295 Abc_Print( -1, "Abc_CommandGraft(): This command expects one AIG file name on the command line.\n" );
296 return 1;
297 }
298 Wln_LibGraftOne( pLib, pArgvNew, nArgcNew, fInv, fVerbose );
299 return 0;
300usage:
301 Abc_Print( -2, "usage: %%graft [-ivh] <module1_name> <module2_name>\n" );
302 Abc_Print( -2, "\t replace instances of module1 by those of module2\n" );
303 Abc_Print( -2, "\t-i : toggle using inverse grafting [default = %s]\n", fInv? "yes": "no" );
304 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
305 Abc_Print( -2, "\t-h : print the command usage\n");
306 return 1;
307}
308
320int Abc_CommandHierarchy( Abc_Frame_t * pAbc, int argc, char ** argv )
321{
322 extern void Wln_LibMarkHierarchy( Rtl_Lib_t * p, char ** ppModule, int nModules, int fVerbose );
323 Rtl_Lib_t * pLib = Wln_AbcGetRtl(pAbc);
324 char ** pArgvNew; int nArgcNew;
325 int c, fVerbose = 0;
327 while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
328 {
329 switch ( c )
330 {
331 case 'v':
332 fVerbose ^= 1;
333 break;
334 case 'h':
335 goto usage;
336 default:
337 goto usage;
338 }
339 }
340 if ( pLib == NULL )
341 {
342 printf( "The design is not entered.\n" );
343 return 1;
344 }
345 pArgvNew = argv + globalUtilOptind;
346 nArgcNew = argc - globalUtilOptind;
347 if ( nArgcNew < 0 )
348 {
349 Abc_Print( -1, "Abc_CommandHierarchy(): This command expects one AIG file name on the command line.\n" );
350 return 1;
351 }
352 Wln_LibMarkHierarchy( pLib, pArgvNew, nArgcNew, fVerbose );
353 return 0;
354usage:
355 Abc_Print( -2, "usage: %%hierarchy [-vh] <module_name>\n" );
356 Abc_Print( -2, "\t marks the module whose instances may later be treated as black boxes\n" );
357 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
358 Abc_Print( -2, "\t-h : print the command usage\n");
359 return 1;
360}
361
373int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
374{
375 extern Gia_Man_t * Rtl_LibCollapse( Rtl_Lib_t * p, char * pTopModule, int fRev, int fVerbose );
376 Gia_Man_t * pNew = NULL;
377 Rtl_Lib_t * pLib = Wln_AbcGetRtl(pAbc);
378 char * pTopModule = NULL;
379 int c, fInv = 0, fRev = 0, fVerbose = 0;
381 while ( ( c = Extra_UtilGetopt( argc, argv, "Tcrvh" ) ) != EOF )
382 {
383 switch ( c )
384 {
385 case 'T':
386 if ( globalUtilOptind >= argc )
387 {
388 Abc_Print( -1, "Command line switch \"-T\" should be followed by a file name.\n" );
389 goto usage;
390 }
391 pTopModule = argv[globalUtilOptind];
393 break;
394 case 'c':
395 fInv ^= 1;
396 break;
397 case 'r':
398 fRev ^= 1;
399 break;
400 case 'v':
401 fVerbose ^= 1;
402 break;
403 case 'h':
404 goto usage;
405 default:
406 goto usage;
407 }
408 }
409 if ( pLib == NULL )
410 {
411 printf( "The design is not entered.\n" );
412 return 1;
413 }
414 pNew = Rtl_LibCollapse( pLib, pTopModule, fRev, fVerbose );
415 if ( fInv )
416 Gia_ManInvertPos( pNew );
417 Abc_FrameUpdateGia( pAbc, pNew );
418 return 0;
419usage:
420 Abc_Print( -2, "usage: %%collapse [-T <module>] [-crvh] <file_name>\n" );
421 Abc_Print( -2, "\t collapse hierarchical design into an AIG\n" );
422 Abc_Print( -2, "\t-T : specify the top module of the design [default = none]\n" );
423 Abc_Print( -2, "\t-c : toggle complementing miter outputs after collapsing [default = %s]\n", fInv? "yes": "no" );
424 Abc_Print( -2, "\t-r : toggle bit order reversal in the word-level IO [default = %s]\n", fRev? "yes": "no" );
425 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
426 Abc_Print( -2, "\t-h : print the command usage\n");
427 return 1;
428}
429
441int Abc_CommandPrint( Abc_Frame_t * pAbc, int argc, char ** argv )
442{
443 extern void Rtl_LibPrintStats( Rtl_Lib_t * p );
444 extern void Rtl_LibPrintHieStats( Rtl_Lib_t * p );
445 extern void Rtl_LibPrint( char * pFileName, Rtl_Lib_t * p );
446 Rtl_Lib_t * pLib = Wln_AbcGetRtl(pAbc);
447 int c, fHie = 0, fDesign = 0, fVerbose = 0;
449 while ( ( c = Extra_UtilGetopt( argc, argv, "pdvh" ) ) != EOF )
450 {
451 switch ( c )
452 {
453 case 'p':
454 fHie ^= 1;
455 break;
456 case 'd':
457 fDesign ^= 1;
458 break;
459 case 'v':
460 fVerbose ^= 1;
461 break;
462 case 'h':
463 goto usage;
464 default:
465 goto usage;
466 }
467 }
468 if ( pLib == NULL )
469 {
470 printf( "The design is not entered.\n" );
471 return 1;
472 }
473 Rtl_LibPrintStats( pLib );
474 if ( fHie )
475 Rtl_LibPrintHieStats( pLib );
476 if ( fDesign )
477 Rtl_LibPrint( NULL, pLib );
478 return 0;
479usage:
480 Abc_Print( -2, "usage: %%print [-pdvh]\n" );
481 Abc_Print( -2, "\t print statistics about the hierarchical design\n" );
482 Abc_Print( -2, "\t-p : toggle printing of the hierarchy [default = %s]\n", fHie? "yes": "no" );
483 Abc_Print( -2, "\t-d : toggle printing of the design [default = %s]\n", fDesign? "yes": "no" );
484 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
485 Abc_Print( -2, "\t-h : print the command usage\n");
486 Abc_Print( -2, "\t<file> : text file name with guidance for solving\n");
487 return 1;
488}
489
501int Abc_CommandSolve( Abc_Frame_t * pAbc, int argc, char ** argv )
502{
503 extern void Rtl_LibBlast( Rtl_Lib_t * pLib );
504 extern void Rtl_LibBlast2( Rtl_Lib_t * pLib, Vec_Int_t * vRoots, int fInv );
505 extern void Rtl_LibSolve( Rtl_Lib_t * pLib, void * pNtk );
506 extern void Rtl_LibPreprocess( Rtl_Lib_t * pLib );
507 extern void Wln_SolveWithGuidance( char * pFileName, Rtl_Lib_t * p );
508
509 Rtl_Lib_t * pLib = Wln_AbcGetRtl(pAbc);
510 int c, fOldBlast = 0, fPrepro = 0, fVerbose = 0;
512 while ( ( c = Extra_UtilGetopt( argc, argv, "opvh" ) ) != EOF )
513 {
514 switch ( c )
515 {
516 case 'o':
517 fOldBlast ^= 1;
518 break;
519 case 'p':
520 fPrepro ^= 1;
521 break;
522 case 'v':
523 fVerbose ^= 1;
524 break;
525 case 'h':
526 goto usage;
527 default:
528 goto usage;
529 }
530 }
531 if ( pLib == NULL )
532 {
533 printf( "The design is not entered.\n" );
534 return 1;
535 }
536 if ( argc == globalUtilOptind + 1 )
537 {
538 char * pFileName = argv[globalUtilOptind];
539 FILE * pFile = fopen( pFileName, "r" );
540 if ( pFile == NULL )
541 {
542 Abc_Print( -1, "Cannot open file \"%s\" with the input test patterns.\n", pFileName );
543 return 0;
544 }
545 fclose( pFile );
546 printf( "Using guidance from file \"%s\".\n", pFileName );
547 Wln_SolveWithGuidance( pFileName, pLib );
548 }
549 else
550 {
551 printf( "Solving the miter without guidance.\n" );
552 if ( fOldBlast )
553 Rtl_LibBlast( pLib );
554 else
555 Rtl_LibBlast2( pLib, NULL, 0 );
556 if ( fPrepro )
557 Rtl_LibPreprocess( pLib );
558 Rtl_LibSolve( pLib, NULL );
559 }
560 return 0;
561usage:
562 Abc_Print( -2, "usage: %%solve [-opvh] <file>\n" );
563 Abc_Print( -2, "\t solving properties for the hierarchical design\n" );
564 Abc_Print( -2, "\t-o : toggle using old bit-blasting procedure [default = %s]\n", fOldBlast? "yes": "no" );
565 Abc_Print( -2, "\t-p : toggle preprocessing for verification [default = %s]\n", fPrepro? "yes": "no" );
566 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
567 Abc_Print( -2, "\t-h : print the command usage\n");
568 Abc_Print( -2, "\t<file> : text file name with guidance for solving\n");
569 return 1;
570}
571
575
576
578
void Abc_FrameUpdateGia(Abc_Frame_t *pAbc, Gia_Man_t *pNew)
Definition abc.c:824
struct Abc_Ntk_t_ Abc_Ntk_t
Definition abc.h:115
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
typedefABC_NAMESPACE_HEADER_START struct Abc_Frame_t_ Abc_Frame_t
INCLUDES ///.
Definition abcapis.h:38
ABC_DLL void Abc_FrameReplaceCurrentNetwork(Abc_Frame_t *p, Abc_Ntk_t *pNet)
Definition mainFrame.c:538
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
void Cmd_CommandAdd(Abc_Frame_t *pAbc, const char *sGroup, const char *sName, Cmd_CommandFuncType pFunc, int fChanges)
Definition cmdApi.c:63
Cube * p
Definition exorList.c:222
int globalUtilOptind
char * Extra_FileGetSimilarName(char *pFileNameWrong, char *pS1, char *pS2, char *pS3, char *pS4, char *pS5)
int Extra_UtilGetopt(int argc, char *argv[], const char *optstring)
ABC_DLL void Extra_UtilGetoptReset()
char * Extra_FileNameExtension(char *FileName)
void Gia_ManInvertPos(Gia_Man_t *pAig)
Definition giaUtil.c:1651
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
usage()
Definition main.c:626
int strcmp()
void Wln_Init(Abc_Frame_t *pAbc)
FUNCTION DEFINITIONS ///.
Definition wlnCom.c:56
void Wln_End(Abc_Frame_t *pAbc)
Definition wlnCom.c:77
void Rtl_LibSolve(Rtl_Lib_t *pLib, void *pNtk)
Definition wlnRead.c:2343
Gia_Man_t * Rtl_LibCollapse(Rtl_Lib_t *p, char *pTopModule, int fRev, int fVerbose)
Definition wlnRead.c:2790
void Rtl_LibPrintHieStats(Rtl_Lib_t *p)
Definition wlnRead.c:286
void Rtl_LibPreprocess(Rtl_Lib_t *pLib)
Definition wlnRead.c:2303
void Rtl_LibBlast2(Rtl_Lib_t *pLib, Vec_Int_t *vRoots, int fInv)
Definition wlnRead.c:2229
void Rtl_LibBlast(Rtl_Lib_t *pLib)
Definition wlnRead.c:1977
void Rtl_LibPrintStats(Rtl_Lib_t *p)
Definition wlnRead.c:386
void Rtl_LibPrint(char *pFileName, Rtl_Lib_t *p)
Definition wlnRead.c:1132
void Wln_LibGraftOne(Rtl_Lib_t *p, char **pModules, int nModules, int fInv, int fVerbose)
Definition wlnRead.c:2847
void Wln_LibMarkHierarchy(Rtl_Lib_t *p, char **ppModule, int nModules, int fVerbose)
Definition wlnRead.c:2925
void Wln_SolveWithGuidance(char *pFileName, Rtl_Lib_t *p)
Definition wlnRead.c:2581
Abc_Ntk_t * Wln_ReadMappedSystemVerilog(char *pFileName, char *pTopModule, char *pDefines, char *pLibrary, int fVerbose)
Definition wlnRtl.c:214
Gia_Man_t * Wln_BlastSystemVerilog(char *pFileName, char *pTopModule, char *pDefines, int fSkipStrash, int fInvert, int fTechMap, int fLibInDir, int fVerbose)
Definition wlnRtl.c:174
Rtl_Lib_t * Wln_ReadSystemVerilog(char *pFileName, char *pTopModule, char *pDefines, int fCollapse, int fVerbose)
Definition wlnRtl.c:142
void Rtl_LibFree(Rtl_Lib_t *p)
Definition wlnRead.c:318
struct Rtl_Lib_t_ Rtl_Lib_t
Definition wln.h:255