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