1 /**CFile**************************************************************** 2 3 FileName [acbCom.c] 4 5 SystemName [ABC: Logic synthesis and verification system.] 6 7 PackageName [Hierarchical word-level netlist.] 8 9 Synopsis [Command handlers.] 10 11 Author [Alan Mishchenko] 12 13 Affiliation [UC Berkeley] 14 15 Date [Ver. 1.0. Started - November 29, 2014.] 16 17 Revision [$Id: acbCom.c,v 1.00 2014/11/29 00:00:00 alanmi Exp $] 18 19 ***********************************************************************/ 20 21 #include "acb.h" 22 #include "proof/cec/cec.h" 23 #include "base/main/mainInt.h" 24 25 ABC_NAMESPACE_IMPL_START 26 27 #if 0 28 29 //////////////////////////////////////////////////////////////////////// 30 /// DECLARATIONS /// 31 //////////////////////////////////////////////////////////////////////// 32 33 static int Acb_CommandRead ( Abc_Frame_t * pAbc, int argc, char ** argv ); 34 static int Acb_CommandWrite ( Abc_Frame_t * pAbc, int argc, char ** argv ); 35 static int Acb_CommandPs ( Abc_Frame_t * pAbc, int argc, char ** argv ); 36 static int Acb_CommandPut ( Abc_Frame_t * pAbc, int argc, char ** argv ); 37 static int Acb_CommandGet ( Abc_Frame_t * pAbc, int argc, char ** argv ); 38 static int Acb_CommandClp ( Abc_Frame_t * pAbc, int argc, char ** argv ); 39 static int Acb_CommandBlast ( Abc_Frame_t * pAbc, int argc, char ** argv ); 40 static int Acb_CommandCec ( Abc_Frame_t * pAbc, int argc, char ** argv ); 41 static int Acb_CommandTest ( Abc_Frame_t * pAbc, int argc, char ** argv ); 42 43 static inline Acb_Man_t * Acb_AbcGetMan( Abc_Frame_t * pAbc ) { return (Acb_Man_t *)pAbc->pAbcCba; } 44 static inline void Acb_AbcFreeMan( Abc_Frame_t * pAbc ) { if ( pAbc->pAbcCba ) Acb_ManFree(Acb_AbcGetMan(pAbc)); } 45 static inline void Acb_AbcUpdateMan( Abc_Frame_t * pAbc, Acb_Man_t * p ) { Acb_AbcFreeMan(pAbc); pAbc->pAbcCba = p; } 46 47 //////////////////////////////////////////////////////////////////////// 48 /// FUNCTION DEFINITIONS /// 49 //////////////////////////////////////////////////////////////////////// 50 51 /**Function******************************************************************** 52 53 Synopsis [] 54 55 Description [] 56 57 SideEffects [] 58 59 SeeAlso [] 60 61 ******************************************************************************/ 62 void 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 75 /**Function******************************************************************** 76 77 Synopsis [] 78 79 Description [] 80 81 SideEffects [] 82 83 SeeAlso [] 84 85 ******************************************************************************/ 86 void Acb_End( Abc_Frame_t * pAbc ) 87 { 88 Acb_AbcFreeMan( pAbc ); 89 } 90 91 92 /**Function******************************************************************** 93 94 Synopsis [] 95 96 Description [] 97 98 SideEffects [] 99 100 SeeAlso [] 101 102 ******************************************************************************/ 103 int 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; 109 Extra_UtilGetoptReset(); 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; 177 usage: 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 187 /**Function******************************************************************** 188 189 Synopsis [] 190 191 Description [] 192 193 SideEffects [] 194 195 SeeAlso [] 196 197 ******************************************************************************/ 198 int 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; 204 Extra_UtilGetoptReset(); 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; 252 usage: 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 262 /**Function******************************************************************** 263 264 Synopsis [] 265 266 Description [] 267 268 SideEffects [] 269 270 SeeAlso [] 271 272 ******************************************************************************/ 273 int 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; 281 Extra_UtilGetoptReset(); 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]); 293 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; 331 usage: 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 343 /**Function******************************************************************** 344 345 Synopsis [] 346 347 Description [] 348 349 SideEffects [] 350 351 SeeAlso [] 352 353 ******************************************************************************/ 354 int 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; 359 Extra_UtilGetoptReset(); 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; 392 usage: 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 402 /**Function******************************************************************** 403 404 Synopsis [] 405 406 Description [] 407 408 SideEffects [] 409 410 SeeAlso [] 411 412 ******************************************************************************/ 413 int 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; 417 Extra_UtilGetoptReset(); 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; 460 usage: 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 469 /**Function******************************************************************** 470 471 Synopsis [] 472 473 Description [] 474 475 SideEffects [] 476 477 SeeAlso [] 478 479 ******************************************************************************/ 480 int 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; 484 Extra_UtilGetoptReset(); 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; 506 usage: 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 514 /**Function******************************************************************** 515 516 Synopsis [] 517 518 Description [] 519 520 SideEffects [] 521 522 SeeAlso [] 523 524 ******************************************************************************/ 525 int 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; 530 Extra_UtilGetoptReset(); 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; 560 usage: 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 569 /**Function******************************************************************** 570 571 Synopsis [] 572 573 Description [] 574 575 SideEffects [] 576 577 SeeAlso [] 578 579 ******************************************************************************/ 580 int 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; 588 Cec_ManCecSetDefaultParams( pPars ); 589 Extra_UtilGetoptReset(); 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; 676 usage: 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 684 /**Function******************************************************************** 685 686 Synopsis [] 687 688 Description [] 689 690 SideEffects [] 691 692 SeeAlso [] 693 694 ******************************************************************************/ 695 int Acb_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv ) 696 { 697 Acb_Man_t * p = Acb_AbcGetMan(pAbc); 698 int c, fVerbose = 0; 699 Extra_UtilGetoptReset(); 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; 719 usage: 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 729 //////////////////////////////////////////////////////////////////////// 730 /// END OF FILE /// 731 //////////////////////////////////////////////////////////////////////// 732 733 734 ABC_NAMESPACE_IMPL_END 735 736