ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
acbCom.c
Go to the documentation of this file.
1
20
21#include "acb.h"
22#include "proof/cec/cec.h"
23#include "base/main/mainInt.h"
24
26
27#if 0
28
32
33static int Acb_CommandRead ( Abc_Frame_t * pAbc, int argc, char ** argv );
34static int Acb_CommandWrite ( Abc_Frame_t * pAbc, int argc, char ** argv );
35static int Acb_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv );
36static int Acb_CommandPut ( Abc_Frame_t * pAbc, int argc, char ** argv );
37static int Acb_CommandGet ( Abc_Frame_t * pAbc, int argc, char ** argv );
38static int Acb_CommandClp ( Abc_Frame_t * pAbc, int argc, char ** argv );
39static int Acb_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv );
40static int Acb_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv );
41static int Acb_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv );
42
43static inline Acb_Man_t * Acb_AbcGetMan( Abc_Frame_t * pAbc ) { return (Acb_Man_t *)pAbc->pAbcCba; }
44static inline void Acb_AbcFreeMan( Abc_Frame_t * pAbc ) { if ( pAbc->pAbcCba ) Acb_ManFree(Acb_AbcGetMan(pAbc)); }
45static inline void Acb_AbcUpdateMan( Abc_Frame_t * pAbc, Acb_Man_t * p ) { Acb_AbcFreeMan(pAbc); pAbc->pAbcCba = p; }
46
50
62void Acb_Init( Abc_Frame_t * pAbc )
63{
64 Cmd_CommandAdd( pAbc, "New word level", "@read", Acb_CommandRead, 0 );
65 Cmd_CommandAdd( pAbc, "New word level", "@write", Acb_CommandWrite, 0 );
66 Cmd_CommandAdd( pAbc, "New word level", "@ps", Acb_CommandPs, 0 );
67 Cmd_CommandAdd( pAbc, "New word level", "@put", Acb_CommandPut, 0 );
68 Cmd_CommandAdd( pAbc, "New word level", "@get", Acb_CommandGet, 0 );
69 Cmd_CommandAdd( pAbc, "New word level", "@clp", Acb_CommandClp, 0 );
70 Cmd_CommandAdd( pAbc, "New word level", "@blast", Acb_CommandBlast, 0 );
71 Cmd_CommandAdd( pAbc, "New word level", "@cec", Acb_CommandCec, 0 );
72 Cmd_CommandAdd( pAbc, "New word level", "@test", Acb_CommandTest, 0 );
73}
74
86void Acb_End( Abc_Frame_t * pAbc )
87{
88 Acb_AbcFreeMan( pAbc );
89}
90
91
103int Acb_CommandRead( Abc_Frame_t * pAbc, int argc, char ** argv )
104{
105 FILE * pFile;
106 Acb_Man_t * p = NULL;
107 char * pFileName = NULL;
108 int c, fTest = 0, fDfs = 0, fVerbose = 0;
110 while ( ( c = Extra_UtilGetopt( argc, argv, "tdvh" ) ) != EOF )
111 {
112 switch ( c )
113 {
114 case 't':
115 fTest ^= 1;
116 break;
117 case 'd':
118 fDfs ^= 1;
119 break;
120 case 'v':
121 fVerbose ^= 1;
122 break;
123 case 'h':
124 goto usage;
125 default:
126 goto usage;
127 }
128 }
129 if ( argc != globalUtilOptind + 1 )
130 {
131 printf( "Acb_CommandRead(): Input file name should be given on the command line.\n" );
132 return 0;
133 }
134 // get the file name
135 pFileName = argv[globalUtilOptind];
136 if ( (pFile = fopen( pFileName, "r" )) == NULL )
137 {
138 Abc_Print( 1, "Cannot open input file \"%s\". ", pFileName );
139 if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".blif", ".smt", ".acb", NULL )) )
140 Abc_Print( 1, "Did you mean \"%s\"?", pFileName );
141 Abc_Print( 1, "\n" );
142 return 0;
143 }
144 fclose( pFile );
145 if ( fTest )
146 {
147 if ( !strcmp( Extra_FileNameExtension(pFileName), "blif" ) )
148 Prs_ManReadBlifTest( pFileName );
149 else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
150 Prs_ManReadVerilogTest( pFileName );
151 else
152 {
153 printf( "Unrecognized input file extension.\n" );
154 return 0;
155 }
156 return 0;
157 }
158 if ( !strcmp( Extra_FileNameExtension(pFileName), "blif" ) )
159 p = Acb_ManReadBlif( pFileName );
160 else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
161 p = Acb_ManReadVerilog( pFileName );
162 else if ( !strcmp( Extra_FileNameExtension(pFileName), "acb" ) )
163 p = Acb_ManReadCba( pFileName );
164 else
165 {
166 printf( "Unrecognized input file extension.\n" );
167 return 0;
168 }
169 if ( fDfs )
170 {
171 Acb_Man_t * pTemp;
172 p = Acb_ManDup( pTemp = p, Acb_NtkCollectDfs );
173 Acb_ManFree( pTemp );
174 }
175 Acb_AbcUpdateMan( pAbc, p );
176 return 0;
177usage:
178 Abc_Print( -2, "usage: @read [-tdvh] <file_name>\n" );
179 Abc_Print( -2, "\t reads hierarchical design\n" );
180 Abc_Print( -2, "\t-t : toggle testing the parser [default = %s]\n", fTest? "yes": "no" );
181 Abc_Print( -2, "\t-d : toggle computing DFS ordering [default = %s]\n", fDfs? "yes": "no" );
182 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
183 Abc_Print( -2, "\t-h : print the command usage\n");
184 return 1;
185}
186
198int Acb_CommandWrite( Abc_Frame_t * pAbc, int argc, char ** argv )
199{
200 Acb_Man_t * p = Acb_AbcGetMan(pAbc);
201 char * pFileName = NULL;
202 int fInclineCats = 0;
203 int c, fVerbose = 0;
205 while ( ( c = Extra_UtilGetopt( argc, argv, "cvh" ) ) != EOF )
206 {
207 switch ( c )
208 {
209 case 'c':
210 fInclineCats ^= 1;
211 break;
212 case 'v':
213 fVerbose ^= 1;
214 break;
215 case 'h':
216 goto usage;
217 default:
218 goto usage;
219 }
220 }
221 if ( p == NULL )
222 {
223 Abc_Print( 1, "Acb_CommandWrite(): There is no current design.\n" );
224 return 0;
225 }
226
227 if ( argc == globalUtilOptind + 1 )
228 pFileName = argv[globalUtilOptind];
229 else if ( argc == globalUtilOptind && p )
230 {
231 pFileName = Extra_FileNameGenericAppend( Acb_ManSpec(p) ? Acb_ManSpec(p) : Acb_ManName(p), "_out.v" );
232 printf( "Generated output file name \"%s\".\n", pFileName );
233 }
234 else
235 {
236 printf( "Output file name should be given on the command line.\n" );
237 return 0;
238 }
239 // perform writing
240 if ( !strcmp( Extra_FileNameExtension(pFileName), "blif" ) )
241 Acb_ManWriteBlif( pFileName, p );
242 else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
243 Acb_ManWriteVerilog( pFileName, p, fInclineCats );
244 else if ( !strcmp( Extra_FileNameExtension(pFileName), "acb" ) )
245 Acb_ManWriteCba( pFileName, p );
246 else
247 {
248 printf( "Unrecognized output file extension.\n" );
249 return 0;
250 }
251 return 0;
252usage:
253 Abc_Print( -2, "usage: @write [-cvh]\n" );
254 Abc_Print( -2, "\t writes the design into a file in BLIF or Verilog\n" );
255 Abc_Print( -2, "\t-c : toggle inlining input concatenations [default = %s]\n", fInclineCats? "yes": "no" );
256 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
257 Abc_Print( -2, "\t-h : print the command usage\n");
258 return 1;
259}
260
261
273int Acb_CommandPs( Abc_Frame_t * pAbc, int argc, char ** argv )
274{
275 Acb_Man_t * p = Acb_AbcGetMan(pAbc);
276 int nModules = 0;
277 int fShowMulti = 0;
278 int fShowAdder = 0;
279 int fDistrib = 0;
280 int c, fVerbose = 0;
282 while ( ( c = Extra_UtilGetopt( argc, argv, "Mmadvh" ) ) != EOF )
283 {
284 switch ( c )
285 {
286 case 'M':
287 if ( globalUtilOptind >= argc )
288 {
289 Abc_Print( -1, "Command line switch \"-M\" should be followed by an integer.\n" );
290 goto usage;
291 }
292 nModules = atoi(argv[globalUtilOptind]);
294 if ( nModules < 0 )
295 goto usage;
296 break;
297 case 'm':
298 fShowMulti ^= 1;
299 break;
300 case 'a':
301 fShowAdder ^= 1;
302 break;
303 case 'd':
304 fDistrib ^= 1;
305 break;
306 case 'v':
307 fVerbose ^= 1;
308 break;
309 case 'h':
310 goto usage;
311 default:
312 goto usage;
313 }
314 }
315 if ( p == NULL )
316 {
317 Abc_Print( 1, "Acb_CommandPs(): There is no current design.\n" );
318 return 0;
319 }
320 if ( nModules )
321 {
322 Acb_ManPrintStats( p, nModules, fVerbose );
323 return 0;
324 }
325 Acb_NtkPrintStatsFull( Acb_ManRoot(p), fDistrib, fVerbose );
326 if ( fShowMulti )
327 Acb_NtkPrintNodes( Acb_ManRoot(p), ABC_OPER_ARI_MUL );
328 if ( fShowAdder )
329 Acb_NtkPrintNodes( Acb_ManRoot(p), ABC_OPER_ARI_ADD );
330 return 0;
331usage:
332 Abc_Print( -2, "usage: @ps [-M num] [-madvh]\n" );
333 Abc_Print( -2, "\t prints statistics\n" );
334 Abc_Print( -2, "\t-M num : the number of first modules to report [default = %d]\n", nModules );
335 Abc_Print( -2, "\t-m : toggle printing multipliers [default = %s]\n", fShowMulti? "yes": "no" );
336 Abc_Print( -2, "\t-a : toggle printing adders [default = %s]\n", fShowAdder? "yes": "no" );
337 Abc_Print( -2, "\t-d : toggle printing distrubition [default = %s]\n", fDistrib? "yes": "no" );
338 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
339 Abc_Print( -2, "\t-h : print the command usage\n");
340 return 1;
341}
342
354int Acb_CommandPut( Abc_Frame_t * pAbc, int argc, char ** argv )
355{
356 Acb_Man_t * p = Acb_AbcGetMan(pAbc);
357 Gia_Man_t * pGia = NULL;
358 int c, fBarBufs = 1, fSeq = 0, fVerbose = 0;
360 while ( ( c = Extra_UtilGetopt( argc, argv, "bsvh" ) ) != EOF )
361 {
362 switch ( c )
363 {
364 case 'b':
365 fBarBufs ^= 1;
366 break;
367 case 's':
368 fSeq ^= 1;
369 break;
370 case 'v':
371 fVerbose ^= 1;
372 break;
373 case 'h':
374 goto usage;
375 default:
376 goto usage;
377 }
378 }
379 if ( p == NULL )
380 {
381 Abc_Print( 1, "Acb_CommandPut(): There is no current design.\n" );
382 return 0;
383 }
384 pGia = Acb_ManBlast( p, fBarBufs, fSeq, fVerbose );
385 if ( pGia == NULL )
386 {
387 Abc_Print( 1, "Acb_CommandPut(): Conversion to AIG has failed.\n" );
388 return 0;
389 }
390 Abc_FrameUpdateGia( pAbc, pGia );
391 return 0;
392usage:
393 Abc_Print( -2, "usage: @put [-bsvh]\n" );
394 Abc_Print( -2, "\t extracts AIG from the hierarchical design\n" );
395 Abc_Print( -2, "\t-b : toggle using barrier buffers [default = %s]\n", fBarBufs? "yes": "no" );
396 Abc_Print( -2, "\t-s : toggle blasting sequential elements [default = %s]\n", fSeq? "yes": "no" );
397 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
398 Abc_Print( -2, "\t-h : print the command usage\n");
399 return 1;
400}
401
413int Acb_CommandGet( Abc_Frame_t * pAbc, int argc, char ** argv )
414{
415 Acb_Man_t * pNew = NULL, * p = Acb_AbcGetMan(pAbc);
416 int c, fMapped = 0, fVerbose = 0;
418 while ( ( c = Extra_UtilGetopt( argc, argv, "mvh" ) ) != EOF )
419 {
420 switch ( c )
421 {
422 case 'm':
423 fMapped ^= 1;
424 break;
425 case 'v':
426 fVerbose ^= 1;
427 break;
428 case 'h':
429 goto usage;
430 default:
431 goto usage;
432 }
433 }
434 if ( p == NULL )
435 {
436 Abc_Print( 1, "Acb_CommandGet(): There is no current design.\n" );
437 return 0;
438 }
439
440 if ( fMapped )
441 {
442 if ( pAbc->pNtkCur == NULL )
443 {
444 Abc_Print( 1, "Acb_CommandGet(): There is no current mapped design.\n" );
445 return 0;
446 }
447 pNew = Acb_ManInsertAbc( p, pAbc->pNtkCur );
448 }
449 else
450 {
451 if ( pAbc->pGia == NULL )
452 {
453 Abc_Print( 1, "Acb_CommandGet(): There is no current AIG.\n" );
454 return 0;
455 }
456 pNew = Acb_ManInsertGia( p, pAbc->pGia );
457 }
458 Acb_AbcUpdateMan( pAbc, pNew );
459 return 0;
460usage:
461 Abc_Print( -2, "usage: @get [-mvh]\n" );
462 Abc_Print( -2, "\t extracts AIG or mapped network into the hierarchical design\n" );
463 Abc_Print( -2, "\t-m : toggle using mapped network from main-space [default = %s]\n", fMapped? "yes": "no" );
464 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
465 Abc_Print( -2, "\t-h : print the command usage\n");
466 return 1;
467}
468
480int Acb_CommandClp( Abc_Frame_t * pAbc, int argc, char ** argv )
481{
482 Acb_Man_t * pNew = NULL, * p = Acb_AbcGetMan(pAbc);
483 int c, fVerbose = 0;
485 while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
486 {
487 switch ( c )
488 {
489 case 'v':
490 fVerbose ^= 1;
491 break;
492 case 'h':
493 goto usage;
494 default:
495 goto usage;
496 }
497 }
498 if ( p == NULL )
499 {
500 Abc_Print( 1, "Acb_CommandGet(): There is no current design.\n" );
501 return 0;
502 }
503 pNew = Acb_ManCollapse( p );
504 Acb_AbcUpdateMan( pAbc, pNew );
505 return 0;
506usage:
507 Abc_Print( -2, "usage: @clp [-vh]\n" );
508 Abc_Print( -2, "\t collapses the current hierarchical design\n" );
509 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
510 Abc_Print( -2, "\t-h : print the command usage\n");
511 return 1;
512}
513
525int Acb_CommandBlast( Abc_Frame_t * pAbc, int argc, char ** argv )
526{
527 Gia_Man_t * pNew = NULL;
528 Acb_Man_t * p = Acb_AbcGetMan(pAbc);
529 int c, fSeq = 0, fVerbose = 0;
531 while ( ( c = Extra_UtilGetopt( argc, argv, "svh" ) ) != EOF )
532 {
533 switch ( c )
534 {
535 case 's':
536 fSeq ^= 1;
537 break;
538 case 'v':
539 fVerbose ^= 1;
540 break;
541 case 'h':
542 goto usage;
543 default:
544 goto usage;
545 }
546 }
547 if ( p == NULL )
548 {
549 Abc_Print( 1, "Acb_CommandBlast(): There is no current design.\n" );
550 return 0;
551 }
552 pNew = Acb_ManBlast( p, 0, fSeq, fVerbose );
553 if ( pNew == NULL )
554 {
555 Abc_Print( 1, "Acb_CommandBlast(): Bit-blasting has failed.\n" );
556 return 0;
557 }
558 Abc_FrameUpdateGia( pAbc, pNew );
559 return 0;
560usage:
561 Abc_Print( -2, "usage: @blast [-svh]\n" );
562 Abc_Print( -2, "\t performs bit-blasting of the word-level design\n" );
563 Abc_Print( -2, "\t-s : toggle blasting sequential elements [default = %s]\n", fSeq? "yes": "no" );
564 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
565 Abc_Print( -2, "\t-h : print the command usage\n");
566 return 1;
567}
568
580int Acb_CommandCec( Abc_Frame_t * pAbc, int argc, char ** argv )
581{
582 Acb_Man_t * p = Acb_AbcGetMan(pAbc), * pTemp;
583 Gia_Man_t * pFirst, * pSecond, * pMiter;
584 Cec_ParCec_t ParsCec, * pPars = &ParsCec;
585 char * pFileName, * pStr, ** pArgvNew;
586 int c, nArgcNew, fDumpMiter = 0;
587 FILE * pFile;
590 while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
591 {
592 switch ( c )
593 {
594 case 'v':
595 pPars->fVerbose ^= 1;
596 break;
597 case 'h':
598 goto usage;
599 default:
600 goto usage;
601 }
602 }
603 if ( p == NULL )
604 {
605 Abc_Print( 1, "Acb_CommandCec(): There is no current design.\n" );
606 return 0;
607 }
608
609 pArgvNew = argv + globalUtilOptind;
610 nArgcNew = argc - globalUtilOptind;
611 if ( nArgcNew != 1 )
612 {
613 if ( p->pSpec == NULL )
614 {
615 Abc_Print( -1, "File name is not given on the command line.\n" );
616 return 1;
617 }
618 pFileName = p->pSpec;
619 }
620 else
621 pFileName = pArgvNew[0];
622 // fix the wrong symbol
623 for ( pStr = pFileName; *pStr; pStr++ )
624 if ( *pStr == '>' )
625 *pStr = '\\';
626 if ( (pFile = fopen( pFileName, "r" )) == NULL )
627 {
628 Abc_Print( -1, "Cannot open input file \"%s\". ", pFileName );
629 if ( (pFileName = Extra_FileGetSimilarName( pFileName, ".v", ".blif", NULL, NULL, NULL )) )
630 Abc_Print( 1, "Did you mean \"%s\"?", pFileName );
631 Abc_Print( 1, "\n" );
632 return 1;
633 }
634 fclose( pFile );
635
636 // extract AIG from the current design
637 pFirst = Acb_ManBlast( p, 0, 0, 0 );
638 if ( pFirst == NULL )
639 {
640 Abc_Print( -1, "Extracting AIG from the current design has failed.\n" );
641 return 0;
642 }
643 // extract AIG from the second design
644
645 if ( !strcmp( Extra_FileNameExtension(pFileName), "blif" ) )
646 pTemp = Acb_ManReadBlif( pFileName );
647 else if ( !strcmp( Extra_FileNameExtension(pFileName), "v" ) )
648 pTemp = Acb_ManReadVerilog( pFileName );
649 else if ( !strcmp( Extra_FileNameExtension(pFileName), "acb" ) )
650 pTemp = Acb_ManReadCba( pFileName );
651 else assert( 0 );
652 pSecond = Acb_ManBlast( pTemp, 0, 0, 0 );
653 Acb_ManFree( pTemp );
654 if ( pSecond == NULL )
655 {
656 Gia_ManStop( pFirst );
657 Abc_Print( -1, "Extracting AIG from the original design has failed.\n" );
658 return 0;
659 }
660 // compute the miter
661 pMiter = Gia_ManMiter( pFirst, pSecond, 0, 1, 0, 0, pPars->fVerbose );
662 if ( pMiter )
663 {
664 if ( fDumpMiter )
665 {
666 Abc_Print( 0, "The verification miter is written into file \"%s\".\n", "cec_miter.aig" );
667 Gia_AigerWrite( pMiter, "cec_miter.aig", 0, 0, 0 );
668 }
669 pAbc->Status = Cec_ManVerify( pMiter, pPars );
670 //Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
671 Gia_ManStop( pMiter );
672 }
673 Gia_ManStop( pFirst );
674 Gia_ManStop( pSecond );
675 return 0;
676usage:
677 Abc_Print( -2, "usage: @cec [-vh]\n" );
678 Abc_Print( -2, "\t combinational equivalence checking\n" );
679 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
680 Abc_Print( -2, "\t-h : print the command usage\n");
681 return 1;
682}
683
695int Acb_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
696{
697 Acb_Man_t * p = Acb_AbcGetMan(pAbc);
698 int c, fVerbose = 0;
700 while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
701 {
702 switch ( c )
703 {
704 case 'v':
705 fVerbose ^= 1;
706 break;
707 case 'h':
708 goto usage;
709 default:
710 goto usage;
711 }
712 }
713 if ( p == NULL )
714 {
715 Abc_Print( 1, "Acb_CommandTest(): There is no current design.\n" );
716 return 0;
717 }
718 return 0;
719usage:
720 Abc_Print( -2, "usage: @test [-vh]\n" );
721 Abc_Print( -2, "\t experiments with word-level networks\n" );
722 Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
723 Abc_Print( -2, "\t-h : print the command usage\n");
724 return 1;
725}
726
727#endif
728
732
733
735
@ ABC_OPER_ARI_MUL
Definition abcOper.h:101
@ ABC_OPER_ARI_ADD
Definition abcOper.h:99
void Abc_FrameUpdateGia(Abc_Frame_t *pAbc, Gia_Man_t *pNew)
Definition abc.c:824
#define ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_END
typedefABC_NAMESPACE_HEADER_START struct Abc_Frame_t_ Abc_Frame_t
INCLUDES ///.
Definition abcapis.h:38
struct Acb_Man_t_ Acb_Man_t
Definition acb.h:48
void Prs_ManReadVerilogTest(char *pFileName)
void Prs_ManReadBlifTest(char *pFileName)
void Cec_ManCecSetDefaultParams(Cec_ParCec_t *p)
Definition cecCore.c:159
struct Cec_ParCec_t_ Cec_ParCec_t
Definition cec.h:129
int Cec_ManVerify(Gia_Man_t *p, Cec_ParCec_t *pPars)
MACRO DEFINITIONS ///.
Definition cecCec.c:326
void Cmd_CommandAdd(Abc_Frame_t *pAbc, const char *sGroup, const char *sName, Cmd_CommandFuncType pFunc, int fChanges)
Definition cmdApi.c:63
Cube * p
Definition exorList.c:222
int globalUtilOptind
char * Extra_FileGetSimilarName(char *pFileNameWrong, char *pS1, char *pS2, char *pS3, char *pS4, char *pS5)
int Extra_UtilGetopt(int argc, char *argv[], const char *optstring)
ABC_DLL void Extra_UtilGetoptReset()
char * Extra_FileNameGenericAppend(char *pBase, char *pSuffix)
char * Extra_FileNameExtension(char *FileName)
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_Man_t * Gia_ManMiter(Gia_Man_t *pAig0, Gia_Man_t *pAig1, int nInsDup, int fDualOut, int fSeq, int fImplic, int fVerbose)
Definition giaDup.c:2983
void Gia_AigerWrite(Gia_Man_t *p, char *pFileName, int fWriteSymbols, int fCompact, int fWriteNewLine)
Definition giaAiger.c:1595
usage()
Definition main.c:626
int fVerbose
Definition cec.h:140
#define assert(ex)
Definition util_old.h:213
int strcmp()