1 /**CFile****************************************************************
2
3 FileName [wlcCom.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Verilog parser.]
8
9 Synopsis [Command handlers.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - August 22, 2014.]
16
17 Revision [$Id: wlcCom.c,v 1.00 2014/09/12 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "wlc.h"
22 #include "base/wln/wln.h"
23 #include "base/main/mainInt.h"
24 #include "aig/miniaig/ndr.h"
25
26 ABC_NAMESPACE_IMPL_START
27
28
29 ////////////////////////////////////////////////////////////////////////
30 /// DECLARATIONS ///
31 ////////////////////////////////////////////////////////////////////////
32
33 static int Abc_CommandReadWlc ( Abc_Frame_t * pAbc, int argc, char ** argv );
34 static int Abc_CommandWriteWlc ( Abc_Frame_t * pAbc, int argc, char ** argv );
35 static int Abc_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
36 static int Abc_CommandCone ( Abc_Frame_t * pAbc, int argc, char ** argv );
37 static int Abc_CommandAbs ( Abc_Frame_t * pAbc, int argc, char ** argv );
38 static int Abc_CommandPdrAbs ( Abc_Frame_t * pAbc, int argc, char ** argv );
39 static int Abc_CommandAbs2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
40 static int Abc_CommandMemAbs ( Abc_Frame_t * pAbc, int argc, char ** argv );
41 static int Abc_CommandMemAbs2 ( Abc_Frame_t * pAbc, int argc, char ** argv );
42 static int Abc_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv );
43 static int Abc_CommandBlastMem ( Abc_Frame_t * pAbc, int argc, char ** argv );
44 static int Abc_CommandGraft ( Abc_Frame_t * pAbc, int argc, char ** argv );
45 static int Abc_CommandRetime ( Abc_Frame_t * pAbc, int argc, char ** argv );
46 static int Abc_CommandProfile ( Abc_Frame_t * pAbc, int argc, char ** argv );
47 static int Abc_CommandShortNames ( Abc_Frame_t * pAbc, int argc, char ** argv );
48 static int Abc_CommandShow ( Abc_Frame_t * pAbc, int argc, char ** argv );
49 static int Abc_CommandInvPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
50 static int Abc_CommandInvPrint ( Abc_Frame_t * pAbc, int argc, char ** argv );
51 static int Abc_CommandInvCheck ( Abc_Frame_t * pAbc, int argc, char ** argv );
52 static int Abc_CommandInvGet ( Abc_Frame_t * pAbc, int argc, char ** argv );
53 static int Abc_CommandInvPut ( Abc_Frame_t * pAbc, int argc, char ** argv );
54 static int Abc_CommandInvMin ( Abc_Frame_t * pAbc, int argc, char ** argv );
55 static int Abc_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
56
Wlc_AbcGetNtk(Abc_Frame_t * pAbc)57 static inline Wlc_Ntk_t * Wlc_AbcGetNtk( Abc_Frame_t * pAbc ) { return (Wlc_Ntk_t *)pAbc->pAbcWlc; }
Wlc_AbcFreeNtk(Abc_Frame_t * pAbc)58 static inline void Wlc_AbcFreeNtk( Abc_Frame_t * pAbc ) { if ( pAbc->pAbcWlc ) Wlc_NtkFree(Wlc_AbcGetNtk(pAbc)); }
Wlc_AbcUpdateNtk(Abc_Frame_t * pAbc,Wlc_Ntk_t * pNtk)59 static inline void Wlc_AbcUpdateNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk ) { Wlc_AbcFreeNtk(pAbc); pAbc->pAbcWlc = pNtk; }
60
Wlc_AbcGetInv(Abc_Frame_t * pAbc)61 static inline Vec_Int_t * Wlc_AbcGetInv( Abc_Frame_t * pAbc ) { return pAbc->pAbcWlcInv; }
62
63 ////////////////////////////////////////////////////////////////////////
64 /// FUNCTION DEFINITIONS ///
65 ////////////////////////////////////////////////////////////////////////
66
67 /**Function********************************************************************
68
69 Synopsis []
70
71 Description []
72
73 SideEffects []
74
75 SeeAlso []
76
77 ******************************************************************************/
Wlc_Init(Abc_Frame_t * pAbc)78 void Wlc_Init( Abc_Frame_t * pAbc )
79 {
80 Cmd_CommandAdd( pAbc, "Word level", "%read", Abc_CommandReadWlc, 0 );
81 Cmd_CommandAdd( pAbc, "Word level", "%write", Abc_CommandWriteWlc, 0 );
82 Cmd_CommandAdd( pAbc, "Word level", "%ps", Abc_CommandPs, 0 );
83 Cmd_CommandAdd( pAbc, "Word level", "%cone", Abc_CommandCone, 0 );
84 Cmd_CommandAdd( pAbc, "Word level", "%abs", Abc_CommandAbs, 0 );
85 Cmd_CommandAdd( pAbc, "Word level", "%pdra", Abc_CommandPdrAbs, 0 );
86 Cmd_CommandAdd( pAbc, "Word level", "%abs2", Abc_CommandAbs2, 0 );
87 Cmd_CommandAdd( pAbc, "Word level", "%memabs", Abc_CommandMemAbs, 0 );
88 Cmd_CommandAdd( pAbc, "Word level", "%memabs2", Abc_CommandMemAbs2, 0 );
89 Cmd_CommandAdd( pAbc, "Word level", "%blast", Abc_CommandBlast, 0 );
90 Cmd_CommandAdd( pAbc, "Word level", "%blastmem", Abc_CommandBlastMem, 0 );
91 Cmd_CommandAdd( pAbc, "Word level", "%graft", Abc_CommandGraft, 0 );
92 Cmd_CommandAdd( pAbc, "Word level", "%retime", Abc_CommandRetime, 0 );
93 Cmd_CommandAdd( pAbc, "Word level", "%profile", Abc_CommandProfile, 0 );
94 Cmd_CommandAdd( pAbc, "Word level", "%short_names", Abc_CommandShortNames, 0 );
95 Cmd_CommandAdd( pAbc, "Word level", "%show", Abc_CommandShow, 0 );
96 Cmd_CommandAdd( pAbc, "Word level", "%test", Abc_CommandTest, 0 );
97
98 Cmd_CommandAdd( pAbc, "Word level", "inv_ps", Abc_CommandInvPs, 0 );
99 Cmd_CommandAdd( pAbc, "Word level", "inv_print", Abc_CommandInvPrint, 0 );
100 Cmd_CommandAdd( pAbc, "Word level", "inv_check", Abc_CommandInvCheck, 0 );
101 Cmd_CommandAdd( pAbc, "Word level", "inv_get", Abc_CommandInvGet, 0 );
102 Cmd_CommandAdd( pAbc, "Word level", "inv_put", Abc_CommandInvPut, 0 );
103 Cmd_CommandAdd( pAbc, "Word level", "inv_min", Abc_CommandInvMin, 0 );
104 }
105
106 /**Function********************************************************************
107
108 Synopsis []
109
110 Description []
111
112 SideEffects []
113
114 SeeAlso []
115
116 ******************************************************************************/
Wlc_End(Abc_Frame_t * pAbc)117 void Wlc_End( Abc_Frame_t * pAbc )
118 {
119 Wlc_AbcFreeNtk( pAbc );
120 }
121
122 /**Function********************************************************************
123
124 Synopsis []
125
126 Description []
127
128 SideEffects []
129
130 SeeAlso []
131
132 ******************************************************************************/
Wlc_SetNtk(Abc_Frame_t * pAbc,Wlc_Ntk_t * pNtk)133 void Wlc_SetNtk( Abc_Frame_t * pAbc, Wlc_Ntk_t * pNtk )
134 {
135 Wlc_AbcUpdateNtk( pAbc, pNtk );
136 }
137
138
139 /**Function********************************************************************
140
141 Synopsis []
142
143 Description []
144
145 SideEffects []
146
147 SeeAlso []
148
149 ******************************************************************************/
Abc_CommandReadWlc(Abc_Frame_t * pAbc,int argc,char ** argv)150 int Abc_CommandReadWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
151 {
152 FILE * pFile;
153 Wlc_Ntk_t * pNtk = NULL;
154 char * pFileName = NULL;
155 int fOldParser = 0;
156 int fPrintTree = 0;
157 int c, fVerbose = 0;
158 Extra_UtilGetoptReset();
159 while ( ( c = Extra_UtilGetopt( argc, argv, "opvh" ) ) != EOF )
160 {
161 switch ( c )
162 {
163 case 'o':
164 fOldParser ^= 1;
165 break;
166 case 'p':
167 fPrintTree ^= 1;
168 break;
169 case 'v':
170 fVerbose ^= 1;
171 break;
172 case 'h':
173 goto usage;
174 default:
175 goto usage;
176 }
177 }
178 if ( argc != globalUtilOptind + 1 )
179 {
180 printf( "Abc_CommandReadWlc(): Input file name should be given on the command line.\n" );
181 return 0;
182 }
183 // get the file name
184 pFileName = argv[globalUtilOptind];
185 if ( (pFile = fopen( pFileName, "r" )) == NULL )
186 {
187 Abc_Print( 1, "Cannot open input file \"%s\". ", pFileName );
188 if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".smt", ".smt2", ".ndr", NULL )) )
189 Abc_Print( 1, "Did you mean \"%s\"?", pFileName );
190 Abc_Print( 1, "\n" );
191 return 0;
192 }
193 fclose( pFile );
194
195 // perform reading
196 if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
197 pNtk = Wlc_ReadVer( pFileName, NULL );
198 else if ( !strcmp( Extra_FileNameExtension(pFileName), "smt" ) || !strcmp( Extra_FileNameExtension(pFileName), "smt2" ) )
199 pNtk = Wlc_ReadSmt( pFileName, fOldParser, fPrintTree );
200 else if ( !strcmp( Extra_FileNameExtension(pFileName), "ndr" ) )
201 pNtk = Wlc_ReadNdr( pFileName );
202 else
203 {
204 printf( "Abc_CommandReadWlc(): Unknown file extension.\n" );
205 return 0;
206 }
207 Wlc_AbcUpdateNtk( pAbc, pNtk );
208 return 0;
209 usage:
210 Abc_Print( -2, "usage: %%read [-opvh] <file_name>\n" );
211 Abc_Print( -2, "\t reads word-level design from Verilog file\n" );
212 Abc_Print( -2, "\t-o : toggle using old SMT-LIB parser [default = %s]\n", fOldParser? "yes": "no" );
213 Abc_Print( -2, "\t-p : toggle printing parse SMT-LIB tree [default = %s]\n", fPrintTree? "yes": "no" );
214 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
215 Abc_Print( -2, "\t-h : print the command usage\n");
216 return 1;
217 }
218
219 /**Function********************************************************************
220
221 Synopsis []
222
223 Description []
224
225 SideEffects []
226
227 SeeAlso []
228
229 ******************************************************************************/
Abc_CommandWriteWlc(Abc_Frame_t * pAbc,int argc,char ** argv)230 int Abc_CommandWriteWlc( Abc_Frame_t * pAbc, int argc, char ** argv )
231 {
232 Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
233 char * pFileName = NULL;
234 int fAddCos = 0;
235 int fSplitNodes = 0;
236 int fNoFlops = 0;
237 int c, fVerbose = 0;
238 Extra_UtilGetoptReset();
239 while ( ( c = Extra_UtilGetopt( argc, argv, "anfvh" ) ) != EOF )
240 {
241 switch ( c )
242 {
243 case 'a':
244 fAddCos ^= 1;
245 break;
246 case 'n':
247 fSplitNodes ^= 1;
248 break;
249 case 'f':
250 fNoFlops ^= 1;
251 break;
252 case 'v':
253 fVerbose ^= 1;
254 break;
255 case 'h':
256 goto usage;
257 default:
258 goto usage;
259 }
260 }
261 if ( pNtk == NULL )
262 {
263 Abc_Print( 1, "Abc_CommandWriteWlc(): There is no current design.\n" );
264 return 0;
265 }
266 if ( argc == globalUtilOptind )
267 pFileName = Extra_FileNameGenericAppend( pNtk->pName, "_out.v" );
268 else if ( argc == globalUtilOptind + 1 )
269 pFileName = argv[globalUtilOptind];
270 else
271 {
272 printf( "Output file name should be given on the command line.\n" );
273 return 0;
274 }
275 if ( !strcmp( Extra_FileNameExtension(pFileName), "ndr" ) )
276 Wlc_WriteNdr( pNtk, pFileName );
277 else if ( fSplitNodes )
278 {
279 pNtk = Wlc_NtkDupSingleNodes( pNtk );
280 Wlc_WriteVer( pNtk, pFileName, fAddCos, fNoFlops );
281 Wlc_NtkFree( pNtk );
282 }
283 else
284 Wlc_WriteVer( pNtk, pFileName, fAddCos, fNoFlops );
285
286 return 0;
287 usage:
288 Abc_Print( -2, "usage: %%write [-anfvh]\n" );
289 Abc_Print( -2, "\t writes the design into a file\n" );
290 Abc_Print( -2, "\t-a : toggle adding a CO for each node [default = %s]\n", fAddCos? "yes": "no" );
291 Abc_Print( -2, "\t-n : toggle splitting into individual nodes [default = %s]\n", fSplitNodes? "yes": "no" );
292 Abc_Print( -2, "\t-f : toggle skipping flops when writing file [default = %s]\n",fNoFlops? "yes": "no" );
293 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
294 Abc_Print( -2, "\t-h : print the command usage\n");
295 return 1;
296 }
297
298
299 /**Function********************************************************************
300
301 Synopsis []
302
303 Description []
304
305 SideEffects []
306
307 SeeAlso []
308
309 ******************************************************************************/
Abc_CommandPs(Abc_Frame_t * pAbc,int argc,char ** argv)310 int Abc_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
311 {
312 Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
313 int fShowCones = 0;
314 int fShowMulti = 0;
315 int fShowAdder = 0;
316 int fShowMem = 0;
317 int fDistrib = 0;
318 int fTwoSides = 0;
319 int fAllObjects = 0;
320 int c, fVerbose = 0;
321 Extra_UtilGetoptReset();
322 while ( ( c = Extra_UtilGetopt( argc, argv, "cbamdtovh" ) ) != EOF )
323 {
324 switch ( c )
325 {
326 case 'c':
327 fShowCones ^= 1;
328 break;
329 case 'b':
330 fShowMulti ^= 1;
331 break;
332 case 'a':
333 fShowAdder ^= 1;
334 break;
335 case 'm':
336 fShowMem ^= 1;
337 break;
338 case 'd':
339 fDistrib ^= 1;
340 break;
341 case 't':
342 fTwoSides ^= 1;
343 break;
344 case 'o':
345 fAllObjects ^= 1;
346 break;
347 case 'v':
348 fVerbose ^= 1;
349 break;
350 case 'h':
351 goto usage;
352 default:
353 goto usage;
354 }
355 }
356 if ( pNtk == NULL )
357 {
358 Abc_Print( 1, "Abc_CommandPs(): There is no current design.\n" );
359 return 0;
360 }
361 Wlc_NtkPrintStats( pNtk, fDistrib, fTwoSides, fVerbose );
362 if ( fShowCones )
363 Wlc_NtkProfileCones( pNtk );
364 if ( fShowMulti )
365 Wlc_NtkPrintNodes( pNtk, WLC_OBJ_ARI_MULTI );
366 if ( fShowAdder )
367 Wlc_NtkPrintNodes( pNtk, WLC_OBJ_ARI_ADD );
368 if ( fShowMem )
369 Wlc_NtkPrintMemory( pNtk );
370 if ( fAllObjects )
371 Wlc_NtkPrintObjects( pNtk );
372 return 0;
373 usage:
374 Abc_Print( -2, "usage: %%ps [-cbamdtovh]\n" );
375 Abc_Print( -2, "\t prints statistics\n" );
376 Abc_Print( -2, "\t-c : toggle printing cones [default = %s]\n", fShowCones? "yes": "no" );
377 Abc_Print( -2, "\t-b : toggle printing multipliers [default = %s]\n", fShowMulti? "yes": "no" );
378 Abc_Print( -2, "\t-a : toggle printing adders [default = %s]\n", fShowAdder? "yes": "no" );
379 Abc_Print( -2, "\t-m : toggle printing memories [default = %s]\n", fShowMem? "yes": "no" );
380 Abc_Print( -2, "\t-d : toggle printing distrubition [default = %s]\n", fDistrib? "yes": "no" );
381 Abc_Print( -2, "\t-t : toggle printing stats for LHS and RHS [default = %s]\n", fTwoSides? "yes": "no" );
382 Abc_Print( -2, "\t-o : toggle printing all objects [default = %s]\n", fAllObjects?"yes": "no" );
383 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
384 Abc_Print( -2, "\t-h : print the command usage\n");
385 return 1;
386 }
387
388 /**Function********************************************************************
389
390 Synopsis []
391
392 Description []
393
394 SideEffects []
395
396 SeeAlso []
397
398 ******************************************************************************/
Abc_CommandCone(Abc_Frame_t * pAbc,int argc,char ** argv)399 int Abc_CommandCone( Abc_Frame_t * pAbc, int argc, char ** argv )
400 {
401 Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
402 int c, iOutput = -1, Range = 1, fAllPis = 0, fSeq = 0, fVerbose = 0;
403 char * pName;
404 Extra_UtilGetoptReset();
405 while ( ( c = Extra_UtilGetopt( argc, argv, "ORisvh" ) ) != EOF )
406 {
407 switch ( c )
408 {
409 case 'O':
410 if ( globalUtilOptind >= argc )
411 {
412 Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
413 goto usage;
414 }
415 iOutput = atoi(argv[globalUtilOptind]);
416 globalUtilOptind++;
417 if ( iOutput < 0 )
418 goto usage;
419 break;
420 case 'R':
421 if ( globalUtilOptind >= argc )
422 {
423 Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
424 goto usage;
425 }
426 Range = atoi(argv[globalUtilOptind]);
427 globalUtilOptind++;
428 if ( Range < 0 )
429 goto usage;
430 break;
431 case 'i':
432 fAllPis ^= 1;
433 break;
434 case 's':
435 fSeq ^= 1;
436 break;
437 case 'v':
438 fVerbose ^= 1;
439 break;
440 case 'h':
441 goto usage;
442 default:
443 goto usage;
444 }
445 }
446 if ( pNtk == NULL )
447 {
448 Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" );
449 return 0;
450 }
451 if ( iOutput < 0 || iOutput >= Wlc_NtkCoNum(pNtk) )
452 {
453 Abc_Print( 1, "Abc_CommandCone(): Illegal output index (%d) (should be 0 <= num < %d).\n", iOutput, Wlc_NtkCoNum(pNtk) );
454 return 0;
455 }
456 printf( "Extracting output %d as a %s word-level network.\n", iOutput, fSeq ? "sequential" : "combinational" );
457 pName = Wlc_NtkNewName( pNtk, iOutput, fSeq );
458 Wlc_NtkMarkCone( pNtk, iOutput, Range, fSeq, fAllPis );
459 pNtk = Wlc_NtkDupDfs( pNtk, 1, fSeq );
460 ABC_FREE( pNtk->pName );
461 pNtk->pName = Abc_UtilStrsav( pName );
462 Wlc_AbcUpdateNtk( pAbc, pNtk );
463 return 0;
464 usage:
465 Abc_Print( -2, "usage: %%cone [-OR num] [-isvh]\n" );
466 Abc_Print( -2, "\t extracts logic cone of one or more word-level outputs\n" );
467 Abc_Print( -2, "\t-O num : zero-based index of the first word-level output to extract [default = %d]\n", iOutput );
468 Abc_Print( -2, "\t-R num : total number of word-level outputs to extract [default = %d]\n", Range );
469 Abc_Print( -2, "\t-i : toggle using support composed of all primary inputs [default = %s]\n", fAllPis? "yes": "no" );
470 Abc_Print( -2, "\t-s : toggle performing extracting sequential cones [default = %s]\n", fSeq? "yes": "no" );
471 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
472 Abc_Print( -2, "\t-h : print the command usage\n");
473 return 1;
474 }
475
476 /**Function********************************************************************
477
478 Synopsis []
479
480 Description []
481
482 SideEffects []
483
484 SeeAlso []
485
486 ******************************************************************************/
Abc_CommandPdrAbs(Abc_Frame_t * pAbc,int argc,char ** argv)487 int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
488 {
489 Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
490 Wlc_Par_t Pars, * pPars = &Pars;
491 int c;
492 Wlc_ManSetDefaultParams( pPars );
493 Extra_UtilGetoptReset();
494 while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcdilpqmstuxvwh" ) ) != EOF )
495 {
496 switch ( c )
497 {
498 case 'A':
499 if ( globalUtilOptind >= argc )
500 {
501 Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
502 goto usage;
503 }
504 pPars->nBitsAdd = atoi(argv[globalUtilOptind]);
505 globalUtilOptind++;
506 if ( pPars->nBitsAdd < 0 )
507 goto usage;
508 break;
509 case 'M':
510 if ( globalUtilOptind >= argc )
511 {
512 Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
513 goto usage;
514 }
515 pPars->nBitsMul = atoi(argv[globalUtilOptind]);
516 globalUtilOptind++;
517 if ( pPars->nBitsMul < 0 )
518 goto usage;
519 break;
520 case 'X':
521 if ( globalUtilOptind >= argc )
522 {
523 Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
524 goto usage;
525 }
526 pPars->nBitsMux = atoi(argv[globalUtilOptind]);
527 globalUtilOptind++;
528 if ( pPars->nBitsMux < 0 )
529 goto usage;
530 break;
531 case 'F':
532 if ( globalUtilOptind >= argc )
533 {
534 Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
535 goto usage;
536 }
537 pPars->nBitsFlop = atoi(argv[globalUtilOptind]);
538 globalUtilOptind++;
539 if ( pPars->nBitsFlop < 0 )
540 goto usage;
541 break;
542 case 'I':
543 if ( globalUtilOptind >= argc )
544 {
545 Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
546 goto usage;
547 }
548 pPars->nIterMax = atoi(argv[globalUtilOptind]);
549 globalUtilOptind++;
550 if ( pPars->nIterMax < 0 )
551 goto usage;
552 break;
553 case 'L':
554 if ( globalUtilOptind >= argc )
555 {
556 Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
557 goto usage;
558 }
559 pPars->nLimit = atoi(argv[globalUtilOptind]);
560 globalUtilOptind++;
561 if ( pPars->nLimit < 0 )
562 goto usage;
563 break;
564 case 'a':
565 pPars->fPdra ^= 1;
566 break;
567 case 'b':
568 pPars->fProofRefine ^= 1;
569 break;
570 case 'r':
571 pPars->fHybrid ^= 1;
572 break;
573 case 'x':
574 pPars->fXorOutput ^= 1;
575 break;
576 case 'c':
577 pPars->fCheckClauses ^= 1;
578 break;
579 case 'd':
580 pPars->fAbs2 ^= 1;
581 break;
582 case 'i':
583 pPars->fProofUsePPI ^= 1;
584 break;
585 case 'l':
586 pPars->fLoadTrace ^= 1;
587 break;
588 case 'p':
589 pPars->fPushClauses ^= 1;
590 break;
591 case 'q':
592 pPars->fUseBmc3 ^= 1;
593 break;
594 case 'm':
595 pPars->fMFFC ^= 1;
596 break;
597 case 's':
598 pPars->fShrinkAbs ^= 1;
599 break;
600 case 't':
601 pPars->fShrinkScratch ^= 1;
602 break;
603 case 'u':
604 pPars->fCheckCombUnsat ^= 1;
605 break;
606 case 'v':
607 pPars->fVerbose ^= 1;
608 break;
609 case 'w':
610 pPars->fPdrVerbose ^= 1;
611 break;
612 case 'h':
613 goto usage;
614 default:
615 goto usage;
616 }
617 }
618 if ( pNtk == NULL )
619 {
620 Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" );
621 return 0;
622 }
623 Wlc_NtkPdrAbs( pNtk, pPars );
624 return 0;
625 usage:
626 Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcdilpqmxstuvwh]\n" );
627 Abc_Print( -2, "\t abstraction for word-level networks\n" );
628 Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
629 Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul );
630 Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux );
631 Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop );
632 Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax );
633 Abc_Print( -2, "\t-L num : maximum number of each type of signals [default = %d]\n", pPars->nLimit );
634 Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" );
635 Abc_Print( -2, "\t-a : toggle running pdr with -nct [default = %s]\n", pPars->fPdra? "yes": "no" );
636 Abc_Print( -2, "\t-b : toggle using proof-based refinement [default = %s]\n", pPars->fProofRefine? "yes": "no" );
637 Abc_Print( -2, "\t-r : toggle using both cex-based and proof-based refinement [default = %s]\n", pPars->fHybrid? "yes": "no" );
638 Abc_Print( -2, "\t-c : toggle checking clauses in the reloaded trace [default = %s]\n", pPars->fCheckClauses? "yes": "no" );
639 Abc_Print( -2, "\t-d : toggle using another way of creating abstractions [default = %s]\n", pPars->fAbs2? "yes": "no" );
640 Abc_Print( -2, "\t-i : toggle using PPI values in proof-based refinement [default = %s]\n", pPars->fProofUsePPI? "yes": "no" );
641 Abc_Print( -2, "\t-l : toggle loading previous PDR traces [default = %s]\n", pPars->fLoadTrace? "yes": "no" );
642 Abc_Print( -2, "\t-s : toggle shrinking abstractions with BMC [default = %s]\n", pPars->fShrinkAbs? "yes": "no" );
643 Abc_Print( -2, "\t-t : toggle restarting pdr from scratch after shrinking abstractions with BMC [default = %s]\n", pPars->fShrinkScratch? "yes": "no" );
644 Abc_Print( -2, "\t-u : toggle checking combinationally unsat [default = %s]\n", pPars->fCheckCombUnsat? "yes": "no" );
645 Abc_Print( -2, "\t-p : toggle pushing clauses in the reloaded trace [default = %s]\n", pPars->fPushClauses? "yes": "no" );
646 Abc_Print( -2, "\t-q : toggle running bmc3 in parallel for CEX [default = %s]\n", pPars->fUseBmc3? "yes": "no" );
647 Abc_Print( -2, "\t-m : toggle refining the whole MFFC of a PPI [default = %s]\n", pPars->fMFFC? "yes": "no" );
648 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
649 Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" );
650 Abc_Print( -2, "\t-h : print the command usage\n");
651 return 1;
652 }
653
654
655 /**Function********************************************************************
656
657 Synopsis []
658
659 Description []
660
661 SideEffects []
662
663 SeeAlso []
664
665 ******************************************************************************/
Abc_CommandAbs(Abc_Frame_t * pAbc,int argc,char ** argv)666 int Abc_CommandAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
667 {
668 Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
669 Wlc_Par_t Pars, * pPars = &Pars;
670 int c;
671 Wlc_ManSetDefaultParams( pPars );
672 Extra_UtilGetoptReset();
673 while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILdxvwh" ) ) != EOF )
674 {
675 switch ( c )
676 {
677 case 'A':
678 if ( globalUtilOptind >= argc )
679 {
680 Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
681 goto usage;
682 }
683 pPars->nBitsAdd = atoi(argv[globalUtilOptind]);
684 globalUtilOptind++;
685 if ( pPars->nBitsAdd < 0 )
686 goto usage;
687 break;
688 case 'M':
689 if ( globalUtilOptind >= argc )
690 {
691 Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
692 goto usage;
693 }
694 pPars->nBitsMul = atoi(argv[globalUtilOptind]);
695 globalUtilOptind++;
696 if ( pPars->nBitsMul < 0 )
697 goto usage;
698 break;
699 case 'X':
700 if ( globalUtilOptind >= argc )
701 {
702 Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
703 goto usage;
704 }
705 pPars->nBitsMux = atoi(argv[globalUtilOptind]);
706 globalUtilOptind++;
707 if ( pPars->nBitsMux < 0 )
708 goto usage;
709 break;
710 case 'F':
711 if ( globalUtilOptind >= argc )
712 {
713 Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
714 goto usage;
715 }
716 pPars->nBitsFlop = atoi(argv[globalUtilOptind]);
717 globalUtilOptind++;
718 if ( pPars->nBitsFlop < 0 )
719 goto usage;
720 break;
721 case 'I':
722 if ( globalUtilOptind >= argc )
723 {
724 Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
725 goto usage;
726 }
727 pPars->nIterMax = atoi(argv[globalUtilOptind]);
728 globalUtilOptind++;
729 if ( pPars->nIterMax < 0 )
730 goto usage;
731 break;
732 case 'L':
733 if ( globalUtilOptind >= argc )
734 {
735 Abc_Print( -1, "Command line switch \"-L\" should be followed by an integer.\n" );
736 goto usage;
737 }
738 pPars->nLimit = atoi(argv[globalUtilOptind]);
739 globalUtilOptind++;
740 if ( pPars->nLimit < 0 )
741 goto usage;
742 break;
743 case 'd':
744 pPars->fAbs2 ^= 1;
745 break;
746 case 'x':
747 pPars->fXorOutput ^= 1;
748 break;
749 case 'v':
750 pPars->fVerbose ^= 1;
751 break;
752 case 'w':
753 pPars->fPdrVerbose ^= 1;
754 break;
755 case 'h':
756 goto usage;
757 default:
758 goto usage;
759 }
760 }
761 if ( pNtk == NULL )
762 {
763 Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" );
764 return 0;
765 }
766 Wlc_NtkAbsCore( pNtk, pPars );
767 return 0;
768 usage:
769 Abc_Print( -2, "usage: %%abs [-AMXFIL num] [-dxvwh]\n" );
770 Abc_Print( -2, "\t abstraction for word-level networks\n" );
771 Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
772 Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul );
773 Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux );
774 Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop );
775 Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax );
776 Abc_Print( -2, "\t-L num : maximum number of each type of signals [default = %d]\n", pPars->nLimit );
777 Abc_Print( -2, "\t-d : toggle using another way of creating abstractions [default = %s]\n", pPars->fAbs2? "yes": "no" );
778 Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" );
779 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
780 Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" );
781 Abc_Print( -2, "\t-h : print the command usage\n");
782 return 1;
783 }
784
785 /**Function********************************************************************
786
787 Synopsis []
788
789 Description []
790
791 SideEffects []
792
793 SeeAlso []
794
795 ******************************************************************************/
Abc_CommandAbs2(Abc_Frame_t * pAbc,int argc,char ** argv)796 int Abc_CommandAbs2( Abc_Frame_t * pAbc, int argc, char ** argv )
797 {
798 Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
799 Wlc_Par_t Pars, * pPars = &Pars;
800 int c;
801 Wlc_ManSetDefaultParams( pPars );
802 Extra_UtilGetoptReset();
803 while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFIxvwh" ) ) != EOF )
804 {
805 switch ( c )
806 {
807 case 'A':
808 if ( globalUtilOptind >= argc )
809 {
810 Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
811 goto usage;
812 }
813 pPars->nBitsAdd = atoi(argv[globalUtilOptind]);
814 globalUtilOptind++;
815 if ( pPars->nBitsAdd < 0 )
816 goto usage;
817 break;
818 case 'M':
819 if ( globalUtilOptind >= argc )
820 {
821 Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
822 goto usage;
823 }
824 pPars->nBitsMul = atoi(argv[globalUtilOptind]);
825 globalUtilOptind++;
826 if ( pPars->nBitsMul < 0 )
827 goto usage;
828 break;
829 case 'X':
830 if ( globalUtilOptind >= argc )
831 {
832 Abc_Print( -1, "Command line switch \"-X\" should be followed by an integer.\n" );
833 goto usage;
834 }
835 pPars->nBitsMux = atoi(argv[globalUtilOptind]);
836 globalUtilOptind++;
837 if ( pPars->nBitsMux < 0 )
838 goto usage;
839 break;
840 case 'F':
841 if ( globalUtilOptind >= argc )
842 {
843 Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
844 goto usage;
845 }
846 pPars->nBitsFlop = atoi(argv[globalUtilOptind]);
847 globalUtilOptind++;
848 if ( pPars->nBitsFlop < 0 )
849 goto usage;
850 break;
851 case 'I':
852 if ( globalUtilOptind >= argc )
853 {
854 Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
855 goto usage;
856 }
857 pPars->nIterMax = atoi(argv[globalUtilOptind]);
858 globalUtilOptind++;
859 if ( pPars->nIterMax < 0 )
860 goto usage;
861 break;
862 case 'x':
863 pPars->fXorOutput ^= 1;
864 break;
865 case 'v':
866 pPars->fVerbose ^= 1;
867 break;
868 case 'w':
869 pPars->fPdrVerbose ^= 1;
870 break;
871 case 'h':
872 goto usage;
873 default:
874 goto usage;
875 }
876 }
877 if ( pNtk == NULL )
878 {
879 Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" );
880 return 0;
881 }
882 Wlc_NtkAbsCore2( pNtk, pPars );
883 return 0;
884 usage:
885 Abc_Print( -2, "usage: %%abs2 [-AMXFI num] [-xvwh]\n" );
886 Abc_Print( -2, "\t abstraction for word-level networks\n" );
887 Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
888 Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n", pPars->nBitsMul );
889 Abc_Print( -2, "\t-X num : minimum bit-width of a MUX operator to abstract [default = %d]\n", pPars->nBitsMux );
890 Abc_Print( -2, "\t-F num : minimum bit-width of a flip-flop to abstract [default = %d]\n", pPars->nBitsFlop );
891 Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", pPars->nIterMax );
892 Abc_Print( -2, "\t-x : toggle XORing outputs of word-level miter [default = %s]\n", pPars->fXorOutput? "yes": "no" );
893 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
894 Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", pPars->fPdrVerbose? "yes": "no" );
895 Abc_Print( -2, "\t-h : print the command usage\n");
896 return 1;
897 }
898
899 /**Function********************************************************************
900
901 Synopsis []
902
903 Description []
904
905 SideEffects []
906
907 SeeAlso []
908
909 ******************************************************************************/
Abc_CommandMemAbs(Abc_Frame_t * pAbc,int argc,char ** argv)910 int Abc_CommandMemAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
911 {
912 Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
913 int c, nIterMax = 1000, fDumpAbs = 0, fPdrVerbose = 0, fVerbose = 0;
914 Extra_UtilGetoptReset();
915 while ( ( c = Extra_UtilGetopt( argc, argv, "Idwvh" ) ) != EOF )
916 {
917 switch ( c )
918 {
919 case 'I':
920 if ( globalUtilOptind >= argc )
921 {
922 Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
923 goto usage;
924 }
925 nIterMax = atoi(argv[globalUtilOptind]);
926 globalUtilOptind++;
927 if ( nIterMax <= 0 )
928 goto usage;
929 break;
930 case 'd':
931 fDumpAbs ^= 1;
932 break;
933 case 'w':
934 fPdrVerbose ^= 1;
935 break;
936 case 'v':
937 fVerbose ^= 1;
938 break;
939 case 'h':
940 goto usage;
941 default:
942 goto usage;
943 }
944 }
945 if ( pNtk == NULL )
946 {
947 Abc_Print( 1, "Abc_CommandMemAbs(): There is no current design.\n" );
948 return 0;
949 }
950 Wlc_NtkMemAbstract( pNtk, nIterMax, fDumpAbs, fPdrVerbose, fVerbose );
951 return 0;
952 usage:
953 Abc_Print( -2, "usage: %%memabs [-I num] [-dwvh]\n" );
954 Abc_Print( -2, "\t memory abstraction for word-level networks\n" );
955 Abc_Print( -2, "\t-I num : maximum number of CEGAR iterations [default = %d]\n", nIterMax );
956 Abc_Print( -2, "\t-d : toggle dumping abstraction as an AIG [default = %s]\n",fDumpAbs? "yes": "no" );
957 Abc_Print( -2, "\t-w : toggle printing verbose PDR output [default = %s]\n", fPdrVerbose? "yes": "no" );
958 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
959 Abc_Print( -2, "\t-h : print the command usage\n");
960 return 1;
961 }
962
963 /**Function********************************************************************
964
965 Synopsis []
966
967 Description []
968
969 SideEffects []
970
971 SeeAlso []
972
973 ******************************************************************************/
Abc_CommandMemAbs2(Abc_Frame_t * pAbc,int argc,char ** argv)974 int Abc_CommandMemAbs2( Abc_Frame_t * pAbc, int argc, char ** argv )
975 {
976 Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
977 int c, nFrames = 0, fVerbose = 0;
978 Extra_UtilGetoptReset();
979 while ( ( c = Extra_UtilGetopt( argc, argv, "Fvh" ) ) != EOF )
980 {
981 switch ( c )
982 {
983 case 'F':
984 if ( globalUtilOptind >= argc )
985 {
986 Abc_Print( -1, "Command line switch \"-I\" should be followed by an integer.\n" );
987 goto usage;
988 }
989 nFrames = atoi(argv[globalUtilOptind]);
990 globalUtilOptind++;
991 if ( nFrames <= 0 )
992 goto usage;
993 break;
994 case 'v':
995 fVerbose ^= 1;
996 break;
997 case 'h':
998 goto usage;
999 default:
1000 goto usage;
1001 }
1002 }
1003 if ( pNtk == NULL )
1004 {
1005 Abc_Print( 1, "Abc_CommandMemAbs2(): There is no current design.\n" );
1006 return 0;
1007 }
1008 pNtk = Wlc_NtkAbstractMem( pNtk, nFrames, fVerbose );
1009 Wlc_AbcUpdateNtk( pAbc, pNtk );
1010 return 0;
1011 usage:
1012 Abc_Print( -2, "usage: %%memabs2 [-F num] [-vh]\n" );
1013 Abc_Print( -2, "\t memory abstraction for word-level networks\n" );
1014 Abc_Print( -2, "\t-F num : the number of timeframes [default = %d]\n", nFrames );
1015 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
1016 Abc_Print( -2, "\t-h : print the command usage\n");
1017 return 1;
1018 }
1019
1020 /**Function********************************************************************
1021
1022 Synopsis []
1023
1024 Description []
1025
1026 SideEffects []
1027
1028 SeeAlso []
1029
1030 ******************************************************************************/
Abc_CommandBlast(Abc_Frame_t * pAbc,int argc,char ** argv)1031 int Abc_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
1032 {
1033 extern void Wlc_NtkPrintInputInfo( Wlc_Ntk_t * pNtk );
1034 Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
1035 Gia_Man_t * pNew = NULL; int c, fMiter = 0, fDumpNames = 0, fPrintInputInfo = 0;
1036 Wlc_BstPar_t Par, * pPar = &Par;
1037 Wlc_BstParDefault( pPar );
1038 pPar->nOutputRange = 2;
1039 Extra_UtilGetoptReset();
1040 while ( ( c = Extra_UtilGetopt( argc, argv, "ORAMcombqadestnizvh" ) ) != EOF )
1041 {
1042 switch ( c )
1043 {
1044 case 'O':
1045 if ( globalUtilOptind >= argc )
1046 {
1047 Abc_Print( -1, "Command line switch \"-O\" should be followed by an integer.\n" );
1048 goto usage;
1049 }
1050 pPar->iOutput = atoi(argv[globalUtilOptind]);
1051 globalUtilOptind++;
1052 if ( pPar->iOutput < 0 )
1053 goto usage;
1054 break;
1055 case 'R':
1056 if ( globalUtilOptind >= argc )
1057 {
1058 Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
1059 goto usage;
1060 }
1061 pPar->nOutputRange = atoi(argv[globalUtilOptind]);
1062 globalUtilOptind++;
1063 if ( pPar->nOutputRange < 0 )
1064 goto usage;
1065 break;
1066 case 'A':
1067 if ( globalUtilOptind >= argc )
1068 {
1069 Abc_Print( -1, "Command line switch \"-A\" should be followed by an integer.\n" );
1070 goto usage;
1071 }
1072 pPar->nAdderLimit = atoi(argv[globalUtilOptind]);
1073 globalUtilOptind++;
1074 if ( pPar->nAdderLimit < 0 )
1075 goto usage;
1076 break;
1077 case 'M':
1078 if ( globalUtilOptind >= argc )
1079 {
1080 Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
1081 goto usage;
1082 }
1083 pPar->nMultLimit = atoi(argv[globalUtilOptind]);
1084 globalUtilOptind++;
1085 if ( pPar->nMultLimit < 0 )
1086 goto usage;
1087 break;
1088 case 'c':
1089 pPar->fGiaSimple ^= 1;
1090 break;
1091 case 'o':
1092 pPar->fAddOutputs ^= 1;
1093 break;
1094 case 'm':
1095 pPar->fMulti ^= 1;
1096 break;
1097 case 'b':
1098 pPar->fBooth ^= 1;
1099 break;
1100 case 'q':
1101 pPar->fNonRest ^= 1;
1102 break;
1103 case 'a':
1104 pPar->fCla ^= 1;
1105 break;
1106 case 'd':
1107 pPar->fCreateMiter ^= 1;
1108 break;
1109 case 'e':
1110 pPar->fCreateWordMiter ^= 1;
1111 break;
1112 case 's':
1113 pPar->fDecMuxes ^= 1;
1114 break;
1115 case 't':
1116 pPar->fCreateMiter ^= 1;
1117 fMiter ^= 1;
1118 break;
1119 case 'n':
1120 fDumpNames ^= 1;
1121 break;
1122 case 'i':
1123 fPrintInputInfo ^= 1;
1124 break;
1125 case 'z':
1126 pPar->fSaveFfNames ^= 1;
1127 break;
1128 case 'v':
1129 pPar->fVerbose ^= 1;
1130 break;
1131 case 'h':
1132 goto usage;
1133 default:
1134 goto usage;
1135 }
1136 }
1137 if ( pNtk == NULL )
1138 {
1139 Abc_Print( 1, "Abc_CommandBlast(): There is no current design.\n" );
1140 return 0;
1141 }
1142 if ( pNtk->fAsyncRst )
1143 {
1144 Abc_Print( 1, "Abc_CommandBlast(): Trying to bit-blast network with asynchronous reset.\n" );
1145 return 0;
1146 }
1147 if ( fPrintInputInfo )
1148 Wlc_NtkPrintInputInfo(pNtk);
1149 if ( pPar->fMulti )
1150 {
1151 pPar->vBoxIds = Wlc_NtkCollectMultipliers( pNtk );
1152 if ( pPar->vBoxIds == NULL )
1153 Abc_Print( 1, "Warning: There is no multipliers in the design.\n" );
1154 }
1155 else if ( pPar->nAdderLimit || pPar->nMultLimit )
1156 {
1157 int CountA, CountM;
1158 pPar->vBoxIds = Wlc_NtkCollectAddMult( pNtk, pPar, &CountA, &CountM );
1159 if ( pPar->vBoxIds == NULL )
1160 Abc_Print( 1, "Warning: There is no adders and multipliers that will not be blasted.\n" );
1161 else
1162 Abc_Print( 1, "Warning: %d adders and %d multipliers will not be blasted.\n", CountA, CountM );
1163 }
1164 if ( pPar->iOutput >= 0 && pPar->iOutput + pPar->nOutputRange > Wlc_NtkPoNum(pNtk) )
1165 {
1166 Abc_Print( 1, "Abc_CommandBlast(): The output range [%d:%d] is incorrect.\n", pPar->iOutput, pPar->iOutput + pPar->nOutputRange - 1 );
1167 return 0;
1168 }
1169 // transform
1170 pNew = Wlc_NtkBitBlast( pNtk, pPar );
1171 Vec_IntFreeP( &pPar->vBoxIds );
1172 if ( pNew == NULL )
1173 {
1174 Abc_Print( 1, "Abc_CommandBlast(): Bit-blasting has failed.\n" );
1175 return 0;
1176 }
1177 // generate miter
1178 if ( fMiter )
1179 {
1180 Gia_Man_t * pTemp = pNew;
1181 pNew = Gia_ManTransformMiter( pNew );
1182 Gia_ManStop( pTemp );
1183 Abc_Print( 1, "Bit-blasting created a traditional multi-output miter by XORing POs pair-wise.\n" );
1184 if ( fDumpNames )
1185 {
1186 int i; char * pName;
1187 FILE * pFile = fopen( "pio_name_map.txt", "wb" );
1188 if ( pNew->vNamesIn )
1189 Vec_PtrForEachEntry( char *, pNew->vNamesIn, pName, i )
1190 fprintf( pFile, "i%d %s\n", i, pName );
1191 if ( pNew->vNamesOut )
1192 Vec_PtrForEachEntry( char *, pNew->vNamesOut, pName, i )
1193 fprintf( pFile, "o%d %s\n", i, pName );
1194 fclose( pFile );
1195 Abc_Print( 1, "Finished dumping file \"pio_name_map.txt\" containing PI/PO name mapping.\n" );
1196 }
1197 }
1198 Abc_FrameUpdateGia( pAbc, pNew );
1199 return 0;
1200 usage:
1201 Abc_Print( -2, "usage: %%blast [-ORAM num] [-combqadestnizvh]\n" );
1202 Abc_Print( -2, "\t performs bit-blasting of the word-level design\n" );
1203 Abc_Print( -2, "\t-O num : zero-based index of the first word-level PO to bit-blast [default = %d]\n", pPar->iOutput );
1204 Abc_Print( -2, "\t-R num : the total number of word-level POs to bit-blast [default = %d]\n", pPar->nOutputRange );
1205 Abc_Print( -2, "\t-A num : blast adders smaller than this (0 = unused) [default = %d]\n", pPar->nAdderLimit );
1206 Abc_Print( -2, "\t-M num : blast multipliers smaller than this (0 = unused) [default = %d]\n", pPar->nMultLimit );
1207 Abc_Print( -2, "\t-c : toggle using AIG w/o const propagation and strashing [default = %s]\n", pPar->fGiaSimple? "yes": "no" );
1208 Abc_Print( -2, "\t-o : toggle using additional POs on the word-level boundaries [default = %s]\n", pPar->fAddOutputs? "yes": "no" );
1209 Abc_Print( -2, "\t-m : toggle creating boxes for all multipliers in the design [default = %s]\n", pPar->fMulti? "yes": "no" );
1210 Abc_Print( -2, "\t-b : toggle generating radix-4 Booth multipliers [default = %s]\n", pPar->fBooth? "yes": "no" );
1211 Abc_Print( -2, "\t-q : toggle generating non-restoring square root [default = %s]\n", pPar->fNonRest? "yes": "no" );
1212 Abc_Print( -2, "\t-a : toggle generating carry-look-ahead adder [default = %s]\n", pPar->fCla? "yes": "no" );
1213 Abc_Print( -2, "\t-d : toggle creating dual-output multi-output miter [default = %s]\n", pPar->fCreateMiter? "yes": "no" );
1214 Abc_Print( -2, "\t-e : toggle creating miter with output word bits combined [default = %s]\n", pPar->fCreateWordMiter? "yes": "no" );
1215 Abc_Print( -2, "\t-s : toggle creating decoded MUXes [default = %s]\n", pPar->fDecMuxes? "yes": "no" );
1216 Abc_Print( -2, "\t-t : toggle creating regular multi-output miter [default = %s]\n", fMiter? "yes": "no" );
1217 Abc_Print( -2, "\t-n : toggle dumping signal names into a text file [default = %s]\n", fDumpNames? "yes": "no" );
1218 Abc_Print( -2, "\t-i : toggle to print input names after blasting [default = %s]\n", fPrintInputInfo ? "yes": "no" );
1219 Abc_Print( -2, "\t-z : toggle saving flop names after blasting [default = %s]\n", pPar->fSaveFfNames ? "yes": "no" );
1220 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPar->fVerbose? "yes": "no" );
1221 Abc_Print( -2, "\t-h : print the command usage\n");
1222 return 1;
1223 }
1224
1225 /**Function********************************************************************
1226
1227 Synopsis []
1228
1229 Description []
1230
1231 SideEffects []
1232
1233 SeeAlso []
1234
1235 ******************************************************************************/
Abc_CommandBlastMem(Abc_Frame_t * pAbc,int argc,char ** argv)1236 int Abc_CommandBlastMem( Abc_Frame_t * pAbc, int argc, char ** argv )
1237 {
1238 extern Wlc_Ntk_t * Wlc_NtkMemBlast( Wlc_Ntk_t * p );
1239 Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
1240 int c, fVerbose = 0;
1241 Extra_UtilGetoptReset();
1242 while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
1243 {
1244 switch ( c )
1245 {
1246 case 'v':
1247 fVerbose ^= 1;
1248 break;
1249 case 'h':
1250 goto usage;
1251 default:
1252 goto usage;
1253 }
1254 }
1255 if ( pNtk == NULL )
1256 {
1257 Abc_Print( 1, "Abc_CommandBlastMem(): There is no current design.\n" );
1258 return 0;
1259 }
1260 pNtk = Wlc_NtkMemBlast( pNtk );
1261 Wlc_AbcUpdateNtk( pAbc, pNtk );
1262 return 0;
1263 usage:
1264 Abc_Print( -2, "usage: %%blastmem [-vh]\n" );
1265 Abc_Print( -2, "\t performs blasting of memory read/write ports\n" );
1266 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
1267 Abc_Print( -2, "\t-h : print the command usage\n");
1268 return 1;
1269 }
1270
1271 /**Function********************************************************************
1272
1273 Synopsis []
1274
1275 Description []
1276
1277 SideEffects []
1278
1279 SeeAlso []
1280
1281 ******************************************************************************/
Abc_CommandGraft(Abc_Frame_t * pAbc,int argc,char ** argv)1282 int Abc_CommandGraft( Abc_Frame_t * pAbc, int argc, char ** argv )
1283 {
1284 extern Wlc_Ntk_t * Wlc_NtkGraftMulti( Wlc_Ntk_t * p, int fVerbose );
1285 Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
1286 int c, fVerbose = 0;
1287 Extra_UtilGetoptReset();
1288 while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
1289 {
1290 switch ( c )
1291 {
1292 case 'v':
1293 fVerbose ^= 1;
1294 break;
1295 case 'h':
1296 goto usage;
1297 default:
1298 goto usage;
1299 }
1300 }
1301 if ( pNtk == NULL )
1302 {
1303 Abc_Print( 1, "Abc_CommandGraft(): There is no current design.\n" );
1304 return 0;
1305 }
1306 pNtk = Wlc_NtkGraftMulti( pNtk, fVerbose );
1307 Wlc_AbcUpdateNtk( pAbc, pNtk );
1308 return 0;
1309 usage:
1310 Abc_Print( -2, "usage: %%graft [-vh]\n" );
1311 Abc_Print( -2, "\t detects multipliers in LHS of the miter and moves them to RHS\n" );
1312 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
1313 Abc_Print( -2, "\t-h : print the command usage\n");
1314 return 1;
1315 }
1316
1317 /**Function********************************************************************
1318
1319 Synopsis []
1320
1321 Description []
1322
1323 SideEffects []
1324
1325 SeeAlso []
1326
1327 ******************************************************************************/
Abc_CommandRetime(Abc_Frame_t * pAbc,int argc,char ** argv)1328 int Abc_CommandRetime( Abc_Frame_t * pAbc, int argc, char ** argv )
1329 {
1330 extern void Wln_NtkRetimeTest( char * pFileName, int fSkipSimple, int fVerbose );
1331 FILE * pFile;
1332 char * pFileName = NULL;
1333 int fSkipSimple = 0;
1334 int c, fVerbose = 0;
1335 Extra_UtilGetoptReset();
1336 while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
1337 {
1338 switch ( c )
1339 {
1340 case 's':
1341 fSkipSimple ^= 1;
1342 break;
1343 case 'v':
1344 fVerbose ^= 1;
1345 break;
1346 case 'h':
1347 goto usage;
1348 default:
1349 goto usage;
1350 }
1351 }
1352 if ( pAbc->pNdr )
1353 {
1354 Vec_Int_t * vMoves;
1355 Wln_Ntk_t * pNtk = Wln_NtkFromNdr( pAbc->pNdr );
1356 Wln_NtkRetimeCreateDelayInfo( pNtk );
1357 if ( pNtk == NULL )
1358 {
1359 printf( "Transforming NDR into internal represnetation has failed.\n" );
1360 return 0;
1361 }
1362 vMoves = Wln_NtkRetime( pNtk, fSkipSimple, fVerbose );
1363 Wln_NtkFree( pNtk );
1364 ABC_FREE( pAbc->pNdrArray );
1365 if ( vMoves ) pAbc->pNdrArray = Vec_IntReleaseNewArray( vMoves );
1366 Vec_IntFreeP( &vMoves );
1367 return 0;
1368 }
1369 if ( argc != globalUtilOptind + 1 )
1370 {
1371 printf( "Abc_CommandRetime(): Input file name should be given on the command line.\n" );
1372 return 0;
1373 }
1374 // get the file name
1375 pFileName = argv[globalUtilOptind];
1376 if ( (pFile = fopen( pFileName, "r" )) == NULL )
1377 {
1378 Abc_Print( 1, "Cannot open input file \"%s\". ", pFileName );
1379 if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".ndr", NULL, NULL, NULL, NULL )) )
1380 Abc_Print( 1, "Did you mean \"%s\"?", pFileName );
1381 Abc_Print( 1, "\n" );
1382 return 0;
1383 }
1384 fclose( pFile );
1385 Wln_NtkRetimeTest( pFileName, fSkipSimple, fVerbose );
1386 return 0;
1387 usage:
1388 Abc_Print( -2, "usage: %%retime [-svh]\n" );
1389 Abc_Print( -2, "\t performs retiming for the NDR design\n" );
1390 Abc_Print( -2, "\t-s : toggle printing simple nodes [default = %s]\n", !fSkipSimple? "yes": "no" );
1391 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
1392 Abc_Print( -2, "\t-h : print the command usage\n");
1393 return 1;
1394 }
1395
1396 /**Function********************************************************************
1397
1398 Synopsis []
1399
1400 Description []
1401
1402 SideEffects []
1403
1404 SeeAlso []
1405
1406 ******************************************************************************/
Abc_CommandProfile(Abc_Frame_t * pAbc,int argc,char ** argv)1407 int Abc_CommandProfile( Abc_Frame_t * pAbc, int argc, char ** argv )
1408 {
1409 Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
1410 int c, fVerbose = 0;
1411 Extra_UtilGetoptReset();
1412 while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
1413 {
1414 switch ( c )
1415 {
1416 case 'v':
1417 fVerbose ^= 1;
1418 break;
1419 case 'h':
1420 goto usage;
1421 default:
1422 goto usage;
1423 }
1424 }
1425 if ( pNtk == NULL )
1426 {
1427 Abc_Print( 1, "Abc_CommandProfile(): There is no current design.\n" );
1428 return 0;
1429 }
1430 Wlc_WinProfileArith( pNtk );
1431 return 0;
1432 usage:
1433 Abc_Print( -2, "usage: %%profile [-vh]\n" );
1434 Abc_Print( -2, "\t profiles arithmetic components in the word-level networks\n" );
1435 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
1436 Abc_Print( -2, "\t-h : print the command usage\n");
1437 return 1;
1438 }
1439
1440 /**Function********************************************************************
1441
1442 Synopsis []
1443
1444 Description []
1445
1446 SideEffects []
1447
1448 SeeAlso []
1449
1450 ******************************************************************************/
Abc_CommandShortNames(Abc_Frame_t * pAbc,int argc,char ** argv)1451 int Abc_CommandShortNames( Abc_Frame_t * pAbc, int argc, char ** argv )
1452 {
1453 Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
1454 int c, fVerbose = 0;
1455 Extra_UtilGetoptReset();
1456 while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
1457 {
1458 switch ( c )
1459 {
1460 case 'v':
1461 fVerbose ^= 1;
1462 break;
1463 case 'h':
1464 goto usage;
1465 default:
1466 goto usage;
1467 }
1468 }
1469 if ( pNtk == NULL )
1470 {
1471 Abc_Print( 1, "Abc_CommandProfile(): There is no current design.\n" );
1472 return 0;
1473 }
1474 Wlc_NtkShortNames( pNtk );
1475 return 0;
1476 usage:
1477 Abc_Print( -2, "usage: %%short_names [-vh]\n" );
1478 Abc_Print( -2, "\t derives short names for all objects of the network\n" );
1479 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
1480 Abc_Print( -2, "\t-h : print the command usage\n");
1481 return 1;
1482 }
1483
1484 /**Function*************************************************************
1485
1486 Synopsis []
1487
1488 Description []
1489
1490 SideEffects []
1491
1492 SeeAlso []
1493
1494 ***********************************************************************/
Abc_CommandShow(Abc_Frame_t * pAbc,int argc,char ** argv)1495 int Abc_CommandShow( Abc_Frame_t * pAbc, int argc, char ** argv )
1496 {
1497 extern void Wlc_NtkShow( Wlc_Ntk_t * p, Vec_Int_t * vBold );
1498 Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
1499 int c, fMemory = 0, fVerbose = 0;
1500 // set defaults
1501 Extra_UtilGetoptReset();
1502 while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF )
1503 {
1504 switch ( c )
1505 {
1506 case 'm':
1507 fMemory ^= 1;
1508 break;
1509 case 'v':
1510 fVerbose ^= 1;
1511 break;
1512 default:
1513 goto usage;
1514 }
1515 }
1516 if ( pNtk == NULL )
1517 {
1518 Abc_Print( -1, "Empty network.\n" );
1519 return 1;
1520 }
1521 if ( fMemory )
1522 {
1523 Vec_Int_t * vTemp = Wlc_NtkCollectMemory( pNtk, 1 );
1524 Wlc_NtkShow( pNtk, vTemp );
1525 Vec_IntFree( vTemp );
1526 }
1527 else
1528 Wlc_NtkShow( pNtk, NULL );
1529 return 0;
1530
1531 usage:
1532 Abc_Print( -2, "usage: %%show [-mh]\n" );
1533 Abc_Print( -2, " visualizes the network structure using DOT and GSVIEW\n" );
1534 #ifdef WIN32
1535 Abc_Print( -2, " \"dot.exe\" and \"gsview32.exe\" should be set in the paths\n" );
1536 Abc_Print( -2, " (\"gsview32.exe\" may be in \"C:\\Program Files\\Ghostgum\\gsview\\\")\n" );
1537 #endif
1538 Abc_Print( -2, "\t-m : toggle showing memory subsystem [default = %s]\n", fMemory? "yes": "no" );
1539 Abc_Print( -2, "\t-h : print the command usage\n");
1540 return 1;
1541 }
1542
1543 /**Function********************************************************************
1544
1545 Synopsis []
1546
1547 Description []
1548
1549 SideEffects []
1550
1551 SeeAlso []
1552
1553 ******************************************************************************/
Abc_CommandInvPs(Abc_Frame_t * pAbc,int argc,char ** argv)1554 int Abc_CommandInvPs( Abc_Frame_t * pAbc, int argc, char ** argv )
1555 {
1556 extern Vec_Int_t * Pdr_InvCounts( Vec_Int_t * vInv );
1557 extern void Wlc_NtkPrintInvStats( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv, int fVerbose );
1558 Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
1559 Vec_Int_t * vCounts;
1560 int c, fVerbose = 0;
1561 Extra_UtilGetoptReset();
1562 while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
1563 {
1564 switch ( c )
1565 {
1566 case 'v':
1567 fVerbose ^= 1;
1568 break;
1569 case 'h':
1570 goto usage;
1571 default:
1572 goto usage;
1573 }
1574 }
1575 if ( pNtk == NULL )
1576 {
1577 Abc_Print( 1, "Abc_CommandInvPs(): There is no current design.\n" );
1578 return 0;
1579 }
1580 if ( Wlc_AbcGetInv(pAbc) == NULL )
1581 {
1582 Abc_Print( 1, "Abc_CommandInvPs(): Invariant is not available.\n" );
1583 return 0;
1584 }
1585 vCounts = Pdr_InvCounts( Wlc_AbcGetInv(pAbc) );
1586 Wlc_NtkPrintInvStats( pNtk, vCounts, fVerbose );
1587 Vec_IntFree( vCounts );
1588 return 0;
1589 usage:
1590 Abc_Print( -2, "usage: inv_ps [-vh]\n" );
1591 Abc_Print( -2, "\t prints statistics for inductive invariant\n" );
1592 Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
1593 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
1594 Abc_Print( -2, "\t-h : print the command usage\n");
1595 return 1;
1596 }
1597
1598 /**Function********************************************************************
1599
1600 Synopsis []
1601
1602 Description []
1603
1604 SideEffects []
1605
1606 SeeAlso []
1607
1608 ******************************************************************************/
Abc_CommandInvPrint(Abc_Frame_t * pAbc,int argc,char ** argv)1609 int Abc_CommandInvPrint( Abc_Frame_t * pAbc, int argc, char ** argv )
1610 {
1611 extern void Pdr_InvPrint( Vec_Int_t * vInv, int fVerbose );
1612 int c, fVerbose = 0;
1613 Extra_UtilGetoptReset();
1614 while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
1615 {
1616 switch ( c )
1617 {
1618 case 'v':
1619 fVerbose ^= 1;
1620 break;
1621 case 'h':
1622 goto usage;
1623 default:
1624 goto usage;
1625 }
1626 }
1627 if ( Wlc_AbcGetInv(pAbc) == NULL )
1628 {
1629 Abc_Print( 1, "Abc_CommandInvPs(): Invariant is not available.\n" );
1630 return 0;
1631 }
1632 Pdr_InvPrint( Wlc_AbcGetInv(pAbc), fVerbose );
1633 return 0;
1634 usage:
1635 Abc_Print( -2, "usage: inv_print [-vh]\n" );
1636 Abc_Print( -2, "\t prints the current inductive invariant\n" );
1637 Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
1638 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
1639 Abc_Print( -2, "\t-h : print the command usage\n");
1640 return 1;
1641 }
1642
1643 /**Function********************************************************************
1644
1645 Synopsis []
1646
1647 Description []
1648
1649 SideEffects []
1650
1651 SeeAlso []
1652
1653 ******************************************************************************/
Abc_CommandInvCheck(Abc_Frame_t * pAbc,int argc,char ** argv)1654 int Abc_CommandInvCheck( Abc_Frame_t * pAbc, int argc, char ** argv )
1655 {
1656 abctime clk = Abc_Clock();
1657 extern int Pdr_InvCheck( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose );
1658 int c, nFailed, fVerbose = 0;
1659 Extra_UtilGetoptReset();
1660 while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
1661 {
1662 switch ( c )
1663 {
1664 case 'v':
1665 fVerbose ^= 1;
1666 break;
1667 case 'h':
1668 goto usage;
1669 default:
1670 goto usage;
1671 }
1672 }
1673 if ( pAbc->pGia == NULL )
1674 {
1675 Abc_Print( 1, "Abc_CommandInvMin(): There is no current design.\n" );
1676 return 0;
1677 }
1678 if ( Wlc_AbcGetInv(pAbc) == NULL )
1679 {
1680 Abc_Print( 1, "Abc_CommandInvMin(): There is no saved invariant.\n" );
1681 return 0;
1682 }
1683 if ( Gia_ManRegNum(pAbc->pGia) != Vec_IntEntryLast(Wlc_AbcGetInv(pAbc)) )
1684 {
1685 Abc_Print( 1, "Abc_CommandInvMin(): The number of flops in the invariant and in GIA should be the same.\n" );
1686 return 0;
1687 }
1688 nFailed = Pdr_InvCheck( pAbc->pGia, Wlc_AbcGetInv(pAbc), fVerbose );
1689 if ( nFailed )
1690 printf( "Invariant verification failed for %d clauses (out of %d). ", nFailed, Vec_IntEntry(Wlc_AbcGetInv(pAbc),0) );
1691 else
1692 printf( "Invariant verification succeeded. " );
1693 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
1694 return 0;
1695 usage:
1696 Abc_Print( -2, "usage: inv_check [-vh]\n" );
1697 Abc_Print( -2, "\t checks that the invariant is indeed an inductive invariant\n" );
1698 Abc_Print( -2, "\t (AIG representing the design should be in the &-space)\n" );
1699 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
1700 Abc_Print( -2, "\t-h : print the command usage\n");
1701 return 1;
1702 }
1703
1704 /**Function********************************************************************
1705
1706 Synopsis []
1707
1708 Description []
1709
1710 SideEffects []
1711
1712 SeeAlso []
1713
1714 ******************************************************************************/
Abc_CommandInvGet(Abc_Frame_t * pAbc,int argc,char ** argv)1715 int Abc_CommandInvGet( Abc_Frame_t * pAbc, int argc, char ** argv )
1716 {
1717 extern Abc_Ntk_t * Wlc_NtkGetInv( Wlc_Ntk_t * pNtk, Vec_Int_t * vInv );
1718 Abc_Ntk_t * pMainNtk;
1719 Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
1720 int c, fVerbose = 0;
1721 Extra_UtilGetoptReset();
1722 while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
1723 {
1724 switch ( c )
1725 {
1726 case 'v':
1727 fVerbose ^= 1;
1728 break;
1729 case 'h':
1730 goto usage;
1731 default:
1732 goto usage;
1733 }
1734 }
1735 if ( Wlc_AbcGetInv(pAbc) == NULL )
1736 {
1737 Abc_Print( 1, "Abc_CommandInvGet(): Invariant is not available.\n" );
1738 return 0;
1739 }
1740 // derive the network
1741 pMainNtk = Wlc_NtkGetInv( pNtk, Wlc_AbcGetInv(pAbc) );
1742 // replace the current network
1743 if ( pMainNtk )
1744 Abc_FrameReplaceCurrentNetwork( pAbc, pMainNtk );
1745 return 0;
1746 usage:
1747 Abc_Print( -2, "usage: inv_get [-vh]\n" );
1748 Abc_Print( -2, "\t places invariant found by PDR as the current network in the main-space\n" );
1749 Abc_Print( -2, "\t (in the case of \'sat\' or \'undecided\', inifity clauses are used)\n" );
1750 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
1751 Abc_Print( -2, "\t-h : print the command usage\n");
1752 return 1;
1753 }
1754
1755 /**Function********************************************************************
1756
1757 Synopsis []
1758
1759 Description []
1760
1761 SideEffects []
1762
1763 SeeAlso []
1764
1765 ******************************************************************************/
Abc_CommandInvPut(Abc_Frame_t * pAbc,int argc,char ** argv)1766 int Abc_CommandInvPut( Abc_Frame_t * pAbc, int argc, char ** argv )
1767 {
1768 extern Vec_Int_t * Wlc_NtkGetPut( Abc_Ntk_t * pNtk, Gia_Man_t * pGia );
1769 Vec_Int_t * vInv = NULL;
1770 Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
1771 int c, fVerbose = 0;
1772 Extra_UtilGetoptReset();
1773 while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
1774 {
1775 switch ( c )
1776 {
1777 case 'v':
1778 fVerbose ^= 1;
1779 break;
1780 case 'h':
1781 goto usage;
1782 default:
1783 goto usage;
1784 }
1785 }
1786 if ( pNtk == NULL )
1787 {
1788 Abc_Print( 1, "Abc_CommandInvPut(): There is no current design.\n" );
1789 return 0;
1790 }
1791 if ( pAbc->pGia == NULL )
1792 {
1793 Abc_Print( 1, "Abc_CommandInvPut(): There is no current AIG.\n" );
1794 return 0;
1795 }
1796 // derive the network
1797 vInv = Wlc_NtkGetPut( pNtk, pAbc->pGia );
1798 if ( vInv )
1799 Abc_FrameSetInv( vInv );
1800 return 0;
1801 usage:
1802 Abc_Print( -2, "usage: inv_put [-vh]\n" );
1803 Abc_Print( -2, "\t inputs the current network in the main-space as an invariant\n" );
1804 Abc_Print( -2, "\t (AIG representing the design should be in the &-space)\n" );
1805 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
1806 Abc_Print( -2, "\t-h : print the command usage\n");
1807 return 1;
1808 }
1809
1810 /**Function********************************************************************
1811
1812 Synopsis []
1813
1814 Description []
1815
1816 SideEffects []
1817
1818 SeeAlso []
1819
1820 ******************************************************************************/
Abc_CommandInvMin(Abc_Frame_t * pAbc,int argc,char ** argv)1821 int Abc_CommandInvMin( Abc_Frame_t * pAbc, int argc, char ** argv )
1822 {
1823 extern Vec_Int_t * Pdr_InvMinimize( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose );
1824 extern Vec_Int_t * Pdr_InvMinimizeLits( Gia_Man_t * p, Vec_Int_t * vInv, int fVerbose );
1825 Vec_Int_t * vInv, * vInv2;
1826 int c, fLits = 0, fVerbose = 0;
1827 Extra_UtilGetoptReset();
1828 while ( ( c = Extra_UtilGetopt( argc, argv, "lvh" ) ) != EOF )
1829 {
1830 switch ( c )
1831 {
1832 case 'l':
1833 fLits ^= 1;
1834 break;
1835 case 'v':
1836 fVerbose ^= 1;
1837 break;
1838 case 'h':
1839 goto usage;
1840 default:
1841 goto usage;
1842 }
1843 }
1844 if ( pAbc->pGia == NULL )
1845 {
1846 Abc_Print( 1, "Abc_CommandInvMin(): There is no current design.\n" );
1847 return 0;
1848 }
1849 if ( Wlc_AbcGetInv(pAbc) == NULL )
1850 {
1851 Abc_Print( 1, "Abc_CommandInvMin(): Invariant is not available.\n" );
1852 return 0;
1853 }
1854 vInv = Wlc_AbcGetInv(pAbc);
1855 if ( Gia_ManRegNum(pAbc->pGia) != Vec_IntEntryLast(vInv) )
1856 {
1857 Abc_Print( 1, "Abc_CommandInvMin(): The number of flops in the invariant and in GIA should be the same.\n" );
1858 return 0;
1859 }
1860 if ( fLits )
1861 vInv2 = Pdr_InvMinimizeLits( pAbc->pGia, vInv, fVerbose );
1862 else
1863 vInv2 = Pdr_InvMinimize( pAbc->pGia, vInv, fVerbose );
1864 if ( vInv2 )
1865 Abc_FrameSetInv( vInv2 );
1866 return 0;
1867 usage:
1868 Abc_Print( -2, "usage: inv_min [-lvh]\n" );
1869 Abc_Print( -2, "\t performs minimization of the current invariant\n" );
1870 Abc_Print( -2, "\t (AIG representing the design should be in the &-space)\n" );
1871 Abc_Print( -2, "\t-l : toggle minimizing literals rather than clauses [default = %s]\n", fLits? "yes": "no" );
1872 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
1873 Abc_Print( -2, "\t-h : print the command usage\n");
1874 return 1;
1875 }
1876
1877 /**Function********************************************************************
1878
1879 Synopsis []
1880
1881 Description []
1882
1883 SideEffects []
1884
1885 SeeAlso []
1886
1887 ******************************************************************************/
Abc_CommandTest(Abc_Frame_t * pAbc,int argc,char ** argv)1888 int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
1889 {
1890 extern void Wlc_NtkExploreMem( Wlc_Ntk_t * p, int nFrames );
1891 extern void Wlc_NtkSimulateTest( Wlc_Ntk_t * p );
1892 Wlc_Ntk_t * pNtk = Wlc_AbcGetNtk(pAbc);
1893 int c, fVerbose = 0;
1894 Extra_UtilGetoptReset();
1895 while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
1896 {
1897 switch ( c )
1898 {
1899 case 'v':
1900 fVerbose ^= 1;
1901 break;
1902 case 'h':
1903 goto usage;
1904 default:
1905 goto usage;
1906 }
1907 }
1908 // if ( pNtk == NULL )
1909 // {
1910 // Abc_Print( 1, "Abc_CommandTest(): There is no current design.\n" );
1911 // return 0;
1912 // }
1913
1914 // transform
1915 //pNtk = Wlc_NtkUifNodePairs( pNtk, NULL );
1916 //pNtk = Wlc_NtkAbstractNodes( pNtk, NULL );
1917 //Wlc_AbcUpdateNtk( pAbc, pNtk );
1918 //Wlc_GenerateSmtStdout( pAbc );
1919 //Wlc_NtkSimulateTest( (Wlc_Ntk_t *)pAbc->pAbcWlc );
1920 //pNtk = Wlc_NtkDupSingleNodes( pNtk );
1921 //Wlc_AbcUpdateNtk( pAbc, pNtk );
1922 //Wln_ReadNdrTest();
1923 //pNtk = Wlc_NtkMemAbstractTest( pNtk );
1924 //Wlc_AbcUpdateNtk( pAbc, pNtk );
1925 //Wln_NtkFromWlcTest( pNtk );
1926 Wlc_NtkExploreMem( pNtk, 0 );
1927 return 0;
1928 usage:
1929 Abc_Print( -2, "usage: %%test [-vh]\n" );
1930 Abc_Print( -2, "\t experiments with word-level networks\n" );
1931 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
1932 Abc_Print( -2, "\t-h : print the command usage\n");
1933 return 1;
1934 }
1935
1936 ////////////////////////////////////////////////////////////////////////
1937 /// END OF FILE ///
1938 ////////////////////////////////////////////////////////////////////////
1939
1940
1941 ABC_NAMESPACE_IMPL_END
1942
1943