- Generated on Wed Oct 12 2011 00:34:48 for VIS by
1.7.3
|
VIS
|
00001 00036 #include "eqvInt.h" 00037 00038 static char rcsid[] UNUSED = "$Id: eqvCmd.c,v 1.20 2009/04/11 18:26:04 fabio Exp $"; 00039 00040 /*---------------------------------------------------------------------------*/ 00041 /* Variable declarations */ 00042 /*---------------------------------------------------------------------------*/ 00043 static jmp_buf timeOutEnv; 00044 00045 00048 /*---------------------------------------------------------------------------*/ 00049 /* Static function prototypes */ 00050 /*---------------------------------------------------------------------------*/ 00051 00052 static int CommandCombEquivalence(Hrc_Manager_t **hmgr, int argc, char **argv); 00053 static int CommandSeqEquivalence(Hrc_Manager_t **hmgr, int argc, char **argv); 00054 static void TimeOutHandle(void); 00055 00059 /*---------------------------------------------------------------------------*/ 00060 /* Definition of exported functions */ 00061 /*---------------------------------------------------------------------------*/ 00062 00072 void 00073 Eqv_Init(void) 00074 { 00075 Cmd_CommandAdd("comb_verify", CommandCombEquivalence, 0); 00076 Cmd_CommandAdd("seq_verify", CommandSeqEquivalence, 0); 00077 } 00078 00088 void 00089 Eqv_End(void) 00090 { 00091 } 00092 00093 /*---------------------------------------------------------------------------*/ 00094 /* Definition of internal functions */ 00095 /*---------------------------------------------------------------------------*/ 00096 00097 /*---------------------------------------------------------------------------*/ 00098 /* Definition of static functions */ 00099 /*---------------------------------------------------------------------------*/ 00100 00224 static int 00225 CommandCombEquivalence( 00226 Hrc_Manager_t **hmgr, 00227 int argc, 00228 char **argv) 00229 { 00230 static int timeOutPeriod; 00231 static Hrc_Manager_t *hmgr1; 00232 static Hrc_Manager_t *hmgr2; 00233 static Ntk_Network_t *network1; 00234 static Ntk_Network_t *network2; 00235 int c; 00236 int check; 00237 FILE *fp; 00238 FILE *inputFile = NIL(FILE); 00239 char *fileName1; 00240 char *fileName2; 00241 char *name1; 00242 char *name2; 00243 st_generator *gen; 00244 static Part_PartitionMethod partMethod1; 00245 static Part_PartitionMethod partMethod2; 00246 static OFT AssignCommonOrder; 00247 static st_table *inputMap; 00248 static st_table *outputMap; 00249 st_table *rootsTable = NIL(st_table); 00250 st_table *leavesTable = NIL(st_table); 00251 boolean fileFlag = FALSE; 00252 boolean equivalent; 00253 boolean printBddInfo = FALSE; 00254 static boolean execMode; /* FALSE: verify against current network, 00255 TRUE: verify the two given networks */ 00256 boolean isBlif = FALSE; 00257 00258 /* 00259 * These are the default values. These variables must be declared static 00260 * to avoid lint warnings. Since they are static, we must reinitialize 00261 * them outside of the variable declarations. 00262 */ 00263 timeOutPeriod = 0; 00264 hmgr1 = NIL(Hrc_Manager_t); 00265 hmgr2 = NIL(Hrc_Manager_t); 00266 partMethod1 = Part_Default_c; 00267 partMethod2 = Part_Default_c; 00268 AssignCommonOrder = DefaultCommonOrder; 00269 inputMap = NIL(st_table); 00270 outputMap = NIL(st_table); 00271 00272 error_init(); 00273 util_getopt_reset(); 00274 while((c = util_getopt(argc, argv, "bf:o:1:2:ht:i")) != EOF) { 00275 switch(c) { 00276 case 'b': 00277 isBlif = TRUE; 00278 break; 00279 case 'f': 00280 if((inputFile = Cmd_FileOpen(util_optarg, "r", NIL(char *), 1)) == 00281 NIL(FILE)) { 00282 (void) fprintf(vis_stderr, "** eqv error: File %s not found.\n", util_optarg); 00283 goto usage; 00284 } 00285 fileFlag = 1; 00286 break; 00287 case 'o': 00288 /* The following line causes a seg fault, because 00289 FindOrderingMethod() always returns NULL, and currently 00290 only DefaultCommonOrder is used. 00291 AssignCommonOrder = FindOrderingMethod(); 00292 */ 00293 /* The programmer supplies and modifies this function if any new 00294 ordering method is introduced. FindOrderingMethod() should return 00295 the type OFT. */ 00296 break; 00297 case 't': 00298 timeOutPeriod = atoi(util_optarg); 00299 break; 00300 case '1': 00301 if(!strcmp(util_optarg, "total")) { 00302 partMethod1 = Part_Total_c; 00303 } 00304 else 00305 if(!strcmp(util_optarg, "partial")) { 00306 partMethod1 = Part_Partial_c; 00307 } 00308 else 00309 if(!strcmp(util_optarg, "inout")) { 00310 partMethod1 = Part_InOut_c; 00311 } 00312 else { 00313 (void) fprintf(vis_stderr, "** eqv error: Unknown partition method 1\n"); 00314 goto usage; 00315 } 00316 break; 00317 case '2': 00318 if(!strcmp(util_optarg, "total")) { 00319 partMethod2 = Part_Total_c; 00320 } 00321 else 00322 if(!strcmp(util_optarg, "partial")) { 00323 partMethod2 = Part_Partial_c; 00324 } 00325 else 00326 if(!strcmp(util_optarg, "inout")) { 00327 partMethod2 = Part_InOut_c; 00328 } 00329 else { 00330 (void) fprintf(vis_stderr, "** eqv error: Unknown partition method 2\n"); 00331 goto usage; 00332 } 00333 break; 00334 case 'i': 00335 printBddInfo = TRUE; 00336 break; 00337 case 'h': 00338 goto usage; 00339 default : 00340 goto usage; 00341 } 00342 } 00343 if(argc == 1) { 00344 goto usage; 00345 } 00346 00347 if(argc == util_optind+1) { 00348 execMode = FALSE; 00349 } 00350 else 00351 if(argc == util_optind+2) { 00352 execMode = TRUE; 00353 } 00354 else { 00355 error_append("** eqv error: Improper number of arguments.\n"); 00356 (void) fprintf(vis_stderr, "%s", error_string()); 00357 goto usage; 00358 } 00359 if(execMode == FALSE) { 00360 hmgr1 = *hmgr; 00361 if(Hrc_ManagerReadCurrentNode(hmgr1) == NIL(Hrc_Node_t)) { 00362 (void) fprintf(vis_stderr, "** eqv error: The hierarchy manager is empty. Read in design.\n"); 00363 return 1; 00364 } 00365 network1 = (Ntk_Network_t *) Hrc_NodeReadApplInfo( 00366 Hrc_ManagerReadCurrentNode(hmgr1), NTK_HRC_NODE_APPL_KEY); 00367 if(network1 == NIL(Ntk_Network_t)) { 00368 (void) fprintf(vis_stderr, "** eqv error: There is no network. Use flatten_hierarchy.\n"); 00369 return 1; 00370 } 00371 if(Ntk_NetworkReadApplInfo(network1, PART_NETWORK_APPL_KEY) == NIL(void)) { 00372 (void) fprintf(vis_stderr, "** eqv error: Network has not been partitioned. Use build_partition_mdds.\n"); 00373 return 1; 00374 } 00375 fileName2 = argv[util_optind]; 00376 if(isBlif) { 00377 if((hmgr2 = Io_BlifRead(fileName2, FALSE)) == NIL(Hrc_Manager_t)) { 00378 (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2); 00379 goto usage; 00380 } 00381 } 00382 else { 00383 if((fp = Cmd_FileOpen(fileName2, "r", NIL(char *), 1)) == NIL(FILE)) { 00384 (void) fprintf(vis_stderr, "** eqv error: File %s not found\n", fileName2); 00385 return 1; 00386 } 00387 hmgr2 = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE); 00388 fclose(fp); 00389 if(hmgr2 == NIL(Hrc_Manager_t)) { 00390 (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2); 00391 return 1; 00392 } 00393 } 00394 network2 = Ntk_HrcNodeConvertToNetwork(Hrc_ManagerReadCurrentNode(hmgr2), 00395 TRUE, (lsList) NULL); 00396 if(network2 == NIL(Ntk_Network_t)) { 00397 Hrc_ManagerFree(hmgr2); 00398 (void) fprintf(vis_stderr, "** eqv error: Error in network2.\n"); 00399 return 1; 00400 } 00401 00402 } 00403 else { 00404 fileName1 = argv[util_optind]; 00405 fileName2 = argv[util_optind+1]; 00406 if(isBlif) { 00407 if((hmgr1 = Io_BlifRead(fileName1, FALSE)) == NIL(Hrc_Manager_t)) { 00408 (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName1); 00409 return 1; 00410 } 00411 if((hmgr2 = Io_BlifRead(fileName2, FALSE)) == NIL(Hrc_Manager_t)) { 00412 (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2); 00413 if(hmgr1) { 00414 Hrc_ManagerFree(hmgr1); 00415 } 00416 return 1; 00417 } 00418 } 00419 else { 00420 if((fp = Cmd_FileOpen(fileName1, "r", NIL(char *), 1)) == NIL(FILE)) { 00421 (void) fprintf(vis_stderr, "** eqv error: File %s not found\n", fileName1); 00422 return 1; 00423 } 00424 hmgr1 = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE); 00425 fclose(fp); 00426 if(hmgr1 == NIL(Hrc_Manager_t)) { 00427 (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName1); 00428 goto usage; 00429 } 00430 if((fp = Cmd_FileOpen(fileName2, "r", NIL(char *), 1)) == NIL(FILE)) { 00431 (void) fprintf(vis_stderr, "** eqv error: File %s not found\n", fileName2); 00432 if(hmgr1) { 00433 Hrc_ManagerFree(hmgr1); 00434 } 00435 return 1; 00436 } 00437 hmgr2 = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE); 00438 fclose(fp); 00439 if(hmgr2 == NIL(Hrc_Manager_t)) { 00440 (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2); 00441 if(hmgr1) { 00442 Hrc_ManagerFree(hmgr1); 00443 } 00444 return 1; 00445 } 00446 } 00447 network1 = Ntk_HrcNodeConvertToNetwork(Hrc_ManagerReadCurrentNode(hmgr1), 00448 TRUE, (lsList) NULL); 00449 network2 = Ntk_HrcNodeConvertToNetwork(Hrc_ManagerReadCurrentNode(hmgr2), 00450 TRUE, (lsList) NULL); 00451 00452 if((network1 == NIL(Ntk_Network_t)) || (network2 == NIL(Ntk_Network_t))) { 00453 if(network1 == NIL(Ntk_Network_t)) { 00454 (void) fprintf(vis_stderr, "** eqv error: Error in network1.\n"); 00455 } 00456 if(network2 == NIL(Ntk_Network_t)) { 00457 (void) fprintf(vis_stderr, "** eqv error: Error in network2.\n"); 00458 } 00459 Hrc_ManagerFree(hmgr1); 00460 Hrc_ManagerFree(hmgr2); 00461 return 1; 00462 } 00463 if((network1 == NIL(Ntk_Network_t)) || (network2 == NIL(Ntk_Network_t))) { 00464 if(network1 == NIL(Ntk_Network_t)) { 00465 (void) fprintf(vis_stderr, "** eqv error: Error in network1.\n"); 00466 } 00467 if(network2 == NIL(Ntk_Network_t)) { 00468 (void) fprintf(vis_stderr, "** eqv error: Error in network2.\n"); 00469 } 00470 Hrc_ManagerFree(hmgr1); 00471 Hrc_ManagerFree(hmgr2); 00472 return 1; 00473 } 00474 } 00475 00476 if(Ntk_NetworkReadNumCombInputs(network1) != 00477 Ntk_NetworkReadNumCombInputs(network2)) { 00478 error_append("** eqv error: Different number of inputs in the two networks.\n"); 00479 if(!fileFlag) { 00480 if(execMode) { 00481 Hrc_ManagerFree(hmgr1); 00482 Ntk_NetworkFree(network1); 00483 } 00484 Hrc_ManagerFree(hmgr2); 00485 Ntk_NetworkFree(network2); 00486 (void) fprintf(vis_stderr, "%s", error_string()); 00487 return 1; 00488 } 00489 } 00490 00491 if(fileFlag) { 00492 rootsTable = st_init_table(strcmp, st_strhash); 00493 leavesTable = st_init_table(strcmp, st_strhash); 00494 check = ReadRootLeafMap(inputFile, rootsTable, leavesTable); 00495 fclose(inputFile); 00496 switch (check) { 00497 case 0 : /* error */ 00498 st_free_table(rootsTable); 00499 st_free_table(leavesTable); 00500 (void) fprintf(vis_stderr, "** eqv error: No data in the input file.\n"); 00501 if(execMode) { 00502 Hrc_ManagerFree(hmgr1); 00503 Ntk_NetworkFree(network1); 00504 } 00505 Hrc_ManagerFree(hmgr2); 00506 Ntk_NetworkFree(network2); 00507 return 1; 00508 case 1 : /* leaves only */ 00509 st_free_table(rootsTable); 00510 inputMap = MapNamesToNodes(network1, network2, leavesTable); 00511 st_foreach_item(leavesTable, gen, &name1, &name2) { 00512 FREE(name1); 00513 FREE(name2); 00514 } 00515 st_free_table(leavesTable); 00516 if(inputMap == NIL(st_table)) { 00517 (void) fprintf(vis_stderr, "%s", error_string()); 00518 if(execMode) { 00519 Hrc_ManagerFree(hmgr1); 00520 Ntk_NetworkFree(network1); 00521 } 00522 Hrc_ManagerFree(hmgr2); 00523 Ntk_NetworkFree(network2); 00524 return 1; 00525 } 00526 if((outputMap = MapCombOutputsByName(network1, network2)) == 00527 NIL(st_table)) { 00528 st_free_table(inputMap); 00529 if(execMode) { 00530 Hrc_ManagerFree(hmgr1); 00531 Ntk_NetworkFree(network1); 00532 } 00533 Hrc_ManagerFree(hmgr2); 00534 Ntk_NetworkFree(network2); 00535 (void) fprintf(vis_stderr, "%s", error_string()); 00536 return 1; 00537 } 00538 if(!TestRootsAndLeavesAreValid(network1, network2, inputMap, 00539 outputMap)){ 00540 st_free_table(inputMap); 00541 st_free_table(outputMap); 00542 if(execMode) { 00543 Hrc_ManagerFree(hmgr1); 00544 Ntk_NetworkFree(network1); 00545 } 00546 Hrc_ManagerFree(hmgr2); 00547 Ntk_NetworkFree(network2); 00548 (void) fprintf(vis_stderr, "%s", error_string()); 00549 return 1; 00550 } 00551 break; 00552 case 2 : /* roots only */ 00553 st_free_table(leavesTable); 00554 outputMap = MapNamesToNodes(network1, network2, rootsTable); 00555 st_foreach_item(rootsTable, gen, &name1, &name2) { 00556 FREE(name1); 00557 FREE(name2); 00558 } 00559 st_free_table(rootsTable); 00560 if(outputMap ==NIL(st_table)) { 00561 (void) fprintf(vis_stderr, "%s", error_string()); 00562 if(execMode) { 00563 Hrc_ManagerFree(hmgr1); 00564 Ntk_NetworkFree(network1); 00565 } 00566 Hrc_ManagerFree(hmgr2); 00567 Ntk_NetworkFree(network2); 00568 return 1; 00569 } 00570 if((inputMap = MapCombInputsByName(network1, network2)) == 00571 NIL(st_table)) { 00572 st_free_table(outputMap); 00573 if(execMode) { 00574 Hrc_ManagerFree(hmgr1); 00575 Ntk_NetworkFree(network1); 00576 } 00577 Hrc_ManagerFree(hmgr2); 00578 Ntk_NetworkFree(network2); 00579 (void) fprintf(vis_stderr, "%s", error_string()); 00580 return 1; 00581 } 00582 if(!TestRootsAndLeavesAreValid(network1, network2, inputMap, 00583 outputMap)){ 00584 st_free_table(inputMap); 00585 st_free_table(outputMap); 00586 if(execMode) { 00587 Hrc_ManagerFree(hmgr1); 00588 Ntk_NetworkFree(network1); 00589 } 00590 Hrc_ManagerFree(hmgr2); 00591 Ntk_NetworkFree(network2); 00592 return 1; 00593 } 00594 break; 00595 case 3 : /* both leaves and roots */ 00596 inputMap = MapNamesToNodes(network1, network2, leavesTable); 00597 st_foreach_item(leavesTable, gen, &name1, &name2) { 00598 FREE(name1); 00599 FREE(name2); 00600 } 00601 st_free_table(leavesTable); 00602 outputMap = MapNamesToNodes(network1, network2, rootsTable); 00603 st_foreach_item(rootsTable, gen, &name1, &name2) { 00604 FREE(name1); 00605 FREE(name2); 00606 } 00607 st_free_table(rootsTable); 00608 if((inputMap == NIL(st_table)) || (outputMap == NIL(st_table))) { 00609 (void) fprintf(vis_stderr, "%s", error_string()); 00610 if(inputMap) { 00611 st_free_table(inputMap); 00612 } 00613 if(outputMap) { 00614 st_free_table(outputMap); 00615 } 00616 if(execMode) { 00617 Hrc_ManagerFree(hmgr1); 00618 Ntk_NetworkFree(network1); 00619 } 00620 Hrc_ManagerFree(hmgr2); 00621 Ntk_NetworkFree(network2); 00622 return 1; 00623 } 00624 if(!TestRootsAndLeavesAreValid(network1, network2, inputMap, 00625 outputMap)){ 00626 st_free_table(inputMap); 00627 st_free_table(outputMap); 00628 if(execMode) { 00629 Hrc_ManagerFree(hmgr1); 00630 Ntk_NetworkFree(network1); 00631 } 00632 Hrc_ManagerFree(hmgr2); 00633 Ntk_NetworkFree(network2); 00634 (void) fprintf(vis_stderr, "%s", error_string()); 00635 return 1; 00636 } 00637 break; 00638 } 00639 } 00640 else { 00641 inputMap = MapCombInputsByName(network1, network2); 00642 outputMap = MapCombOutputsByName(network1, network2); 00643 if((inputMap == NIL(st_table)) || (outputMap == NIL(st_table))) { 00644 if(inputMap) { 00645 st_free_table(inputMap); 00646 } 00647 if(outputMap) { 00648 st_free_table(outputMap); 00649 } 00650 if(execMode) { 00651 Hrc_ManagerFree(hmgr1); 00652 Ntk_NetworkFree(network1); 00653 } 00654 Hrc_ManagerFree(hmgr2); 00655 Ntk_NetworkFree(network2); 00656 (void) fprintf(vis_stderr, "%s", error_string()); 00657 return 1; 00658 } 00659 } 00660 00661 /* Start the timer before calling the equivalence checker. */ 00662 if (timeOutPeriod > 0){ 00663 (void) signal(SIGALRM, (void(*)(int))TimeOutHandle); 00664 (void) alarm(timeOutPeriod); 00665 if (setjmp(timeOutEnv) > 0) { 00666 (void) fprintf(vis_stderr, "Timeout occurred after %d seconds.\n", timeOutPeriod); 00667 alarm(0); 00668 return 1; 00669 } 00670 } 00671 00672 equivalent = Eqv_NetworkVerifyCombinationalEquivalence(network1, network2, 00673 inputMap, outputMap, 00674 AssignCommonOrder, 00675 partMethod1, 00676 partMethod2); 00677 00678 if(equivalent) { 00679 (void) fprintf(vis_stdout, "Networks are combinationally equivalent.\n\n"); 00680 } 00681 else { 00682 (void) fprintf(vis_stdout, "%s", error_string()); 00683 (void) fprintf(vis_stdout, "Networks are NOT combinationally equivalent.\n\n"); 00684 } 00685 00686 if (printBddInfo) { 00687 bdd_print_stats(Ntk_NetworkReadMddManager(network1), vis_stdout); 00688 } 00689 00690 st_free_table(inputMap); 00691 st_free_table(outputMap); 00692 if(execMode) { 00693 Hrc_ManagerFree(hmgr1); 00694 Ntk_NetworkFree(network1); 00695 } 00696 Hrc_ManagerFree(hmgr2); 00697 Ntk_NetworkFree(network2); 00698 00699 alarm(0); 00700 return 0; /* normal exit */ 00701 00702 usage: 00703 (void) fprintf(vis_stderr, "usage: comb_verify [-b] [-f filename] [-h] [-o ordering method] [-t time]\n"); 00704 (void) fprintf(vis_stderr, " [-1 partMethod1] [-2 partMethod2] [-i] file1 [file2]\n"); 00705 (void) fprintf(vis_stderr, " -b input files are BLIF\n"); 00706 (void) fprintf(vis_stderr, " -f file variable name correspondence file\n"); 00707 (void) fprintf(vis_stderr, " -h print the command usage\n"); 00708 (void) fprintf(vis_stderr, " -o method variable ordering method\n"); 00709 (void) fprintf(vis_stderr, " -t time time out period (in seconds)\n"); 00710 (void) fprintf(vis_stderr, " -1 method partitioning method for network1\n"); 00711 (void) fprintf(vis_stderr, " -2 method partitioning method for network2\n"); 00712 (void) fprintf(vis_stderr, " -i print Bdd statistics\n"); 00713 return 1; /* error exit */ 00714 } 00715 00819 static int 00820 CommandSeqEquivalence( 00821 Hrc_Manager_t **hmgr, 00822 int argc, 00823 char **argv) 00824 { 00825 static int timeOutPeriod; 00826 static Hrc_Manager_t *hmgr1; 00827 static Hrc_Manager_t *hmgr2; 00828 static Ntk_Network_t *network1; 00829 static Ntk_Network_t *network2; 00830 int c; 00831 int check; 00832 FILE *fp; 00833 static FILE *inputFile; 00834 char *fileName1; 00835 char *fileName2; 00836 char *name1; 00837 char *name2; 00838 st_generator *gen; 00839 static Part_PartitionMethod partMethod; 00840 st_table *outputMap = NIL(st_table); 00841 st_table *inputMap = NIL(st_table); 00842 st_table *rootsTable = NIL(st_table); 00843 st_table *leavesTable = NIL(st_table); 00844 static boolean fileFlag; 00845 static boolean execMode; /* FALSE: verify against the current network, 00846 TRUE: verify the two networks */ 00847 static boolean equivalent; 00848 boolean isBlif = FALSE; 00849 boolean printBddInfo = FALSE; 00850 static boolean useBackwardReach; 00851 boolean reordering = FALSE; 00852 00853 /* 00854 * These are the default values. These variables must be declared static 00855 * to avoid lint warnings. Since they are static, we must reinitialize 00856 * them outside of the variable declarations. 00857 */ 00858 timeOutPeriod = 0; 00859 hmgr1 = NIL(Hrc_Manager_t); 00860 hmgr2 = NIL(Hrc_Manager_t); 00861 inputFile = NIL(FILE); 00862 partMethod = Part_Default_c; 00863 fileFlag = FALSE; 00864 equivalent = FALSE; 00865 useBackwardReach = FALSE; 00866 00867 error_init(); 00868 util_getopt_reset(); 00869 while((c = util_getopt(argc, argv, "bBf:p:hFt:ir")) != EOF) { 00870 switch(c) { 00871 case 'b': 00872 isBlif = TRUE; 00873 break; 00874 case 'f': 00875 if((inputFile = Cmd_FileOpen(util_optarg, "r", NIL(char *), 1)) == 00876 NIL(FILE)) { 00877 (void) fprintf(vis_stderr, 00878 "** eqv error: File %s not found.\n", util_optarg); 00879 return 1; 00880 } 00881 fileFlag = 1; 00882 break; 00883 case 'p': 00884 if(!strcmp(util_optarg, "total")) { 00885 partMethod = Part_Total_c; 00886 } else { 00887 if(!strcmp(util_optarg, "partial")) { 00888 partMethod = Part_Partial_c; 00889 } else { 00890 if(!strcmp(util_optarg, "inout")) { 00891 partMethod = Part_InOut_c; 00892 } else { 00893 (void) fprintf(vis_stderr, 00894 "** eqv error: Unknown partition method\n"); 00895 goto usage; 00896 } 00897 } 00898 } 00899 break; 00900 case 't': 00901 timeOutPeriod = atoi(util_optarg); 00902 break; 00903 case 'B': 00904 useBackwardReach = TRUE; 00905 break; 00906 case 'h': 00907 goto usage; 00908 case 'i': 00909 printBddInfo = TRUE; 00910 break; 00911 case 'r': 00912 reordering = TRUE; 00913 break; 00914 default: 00915 goto usage; 00916 } 00917 } 00918 if(argc == 1) { 00919 goto usage; 00920 } 00921 if(argc == util_optind+1) { 00922 execMode = FALSE; 00923 } 00924 else 00925 if(argc == util_optind+2) { 00926 execMode = TRUE; 00927 } 00928 else { 00929 error_append("** eqv error: Improper number of arguments.\n"); 00930 (void) fprintf(vis_stderr, "%s", error_string()); 00931 goto usage; 00932 } 00933 if(execMode == FALSE) { 00934 hmgr1 = *hmgr; 00935 if(Hrc_ManagerReadCurrentNode(hmgr1) == NIL(Hrc_Node_t)) { 00936 (void) fprintf(vis_stderr, "** eqv error: The hierarchy manager is empty. Read in design.\n"); 00937 return 1; 00938 } 00939 network1 = (Ntk_Network_t *) Hrc_NodeReadApplInfo( 00940 Hrc_ManagerReadCurrentNode(hmgr1), NTK_HRC_NODE_APPL_KEY); 00941 if(network1 == NIL(Ntk_Network_t)) { 00942 (void) fprintf(vis_stderr, "** eqv error: There is no network. Use flatten_hierarchy.\n"); 00943 return 1; 00944 } 00945 if(!Ntk_NetworkReadNumLatches(network1)) { 00946 (void) fprintf(vis_stderr, "** eqv error: No latches present in the current network. Use comb_verify.\n"); 00947 return 1; 00948 } 00949 fileName2 = argv[util_optind]; 00950 if(isBlif) { 00951 if((hmgr2 = Io_BlifRead(fileName2, FALSE)) == NIL(Hrc_Manager_t)) { 00952 (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2); 00953 goto usage; 00954 } 00955 } 00956 else { 00957 if((fp = Cmd_FileOpen(fileName2, "r", NIL(char *), 1)) == NIL(FILE)) { 00958 (void) fprintf(vis_stderr, "** eqv error: File %s not found\n", fileName2); 00959 return 1; 00960 } 00961 hmgr2 = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE); 00962 fclose(fp); 00963 if(hmgr2 == NIL(Hrc_Manager_t)) { 00964 (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2); 00965 return 1; 00966 } 00967 } 00968 network2 = Ntk_HrcNodeConvertToNetwork(Hrc_ManagerReadCurrentNode(hmgr2), 00969 TRUE, (lsList) NULL); 00970 if(network2 == NIL(Ntk_Network_t)) { 00971 Hrc_ManagerFree(hmgr2); 00972 (void) fprintf(vis_stderr, "** eqv error: Error in network2.\n"); 00973 return 1; 00974 } 00975 if(!Ntk_NetworkReadNumLatches(network2)) { 00976 (void) fprintf(vis_stderr, "** eqv error: No latches present in %s. Use comb_verify.\n", fileName2); 00977 Hrc_ManagerFree(hmgr2); 00978 Ntk_NetworkFree(network2); 00979 return 1; 00980 } 00981 } 00982 else { 00983 fileName1 = argv[util_optind]; 00984 fileName2 = argv[util_optind+1]; 00985 if(isBlif) { 00986 if((hmgr1 = Io_BlifRead(fileName1, FALSE)) == NIL(Hrc_Manager_t)) { 00987 (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName1); 00988 return 1; 00989 } 00990 if((hmgr2 = Io_BlifRead(fileName2, FALSE)) == NIL(Hrc_Manager_t)) { 00991 (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2); 00992 if(hmgr1) { 00993 Hrc_ManagerFree(hmgr1); 00994 } 00995 return 1; 00996 } 00997 } 00998 else { 00999 if((fp = Cmd_FileOpen(fileName1, "r", NIL(char *), 1)) == NIL(FILE)) { 01000 (void) fprintf(vis_stderr, "** eqv error: File %s not found\n", fileName1); 01001 return 1; 01002 } 01003 hmgr1 = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE); 01004 fclose(fp); 01005 if(hmgr1 == NIL(Hrc_Manager_t)) { 01006 (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName1); 01007 goto usage; 01008 } 01009 if((fp = Cmd_FileOpen(fileName2, "r", NIL(char *), 1)) == NIL(FILE)) { 01010 (void) fprintf(vis_stderr, "** eqv error: File %s not found\n", fileName2); 01011 if(hmgr1) { 01012 Hrc_ManagerFree(hmgr1); 01013 } 01014 return 1; 01015 } 01016 hmgr2 = Io_BlifMvRead(fp, NIL(Hrc_Manager_t), FALSE, FALSE, FALSE); 01017 fclose(fp); 01018 if(hmgr2 == NIL(Hrc_Manager_t)) { 01019 (void) fprintf(vis_stderr, "** eqv error: Error in reading file %s\n", fileName2); 01020 if(hmgr1) { 01021 Hrc_ManagerFree(hmgr1); 01022 } 01023 return 1; 01024 } 01025 } 01026 network1 = Ntk_HrcNodeConvertToNetwork(Hrc_ManagerReadCurrentNode(hmgr1), 01027 TRUE, (lsList) NULL); 01028 network2 = Ntk_HrcNodeConvertToNetwork(Hrc_ManagerReadCurrentNode(hmgr2), 01029 TRUE, (lsList) NULL); 01030 if((network1 == NIL(Ntk_Network_t)) || (network2 == NIL(Ntk_Network_t))) { 01031 if(network1 == NIL(Ntk_Network_t)) { 01032 (void) fprintf(vis_stderr, "** eqv error: Error in network1.\n"); 01033 } 01034 if(network2 == NIL(Ntk_Network_t)) { 01035 (void) fprintf(vis_stderr, "** eqv error: Error in network2.\n"); 01036 } 01037 Hrc_ManagerFree(hmgr1); 01038 Hrc_ManagerFree(hmgr2); 01039 return 1; 01040 } 01041 01042 if(!Ntk_NetworkReadNumLatches(network1)) { 01043 (void) fprintf(vis_stderr, "** eqv error: No latches present in %s. Use comb_verify.\n", fileName1); 01044 Hrc_ManagerFree(hmgr1); 01045 Ntk_NetworkFree(network1); 01046 Hrc_ManagerFree(hmgr2); 01047 Ntk_NetworkFree(network2); 01048 return 1; 01049 } 01050 if(!Ntk_NetworkReadNumLatches(network2)) { 01051 (void) fprintf(vis_stderr, "** eqv error: No latches present in %s. Use comb_verify.\n", fileName2); 01052 Hrc_ManagerFree(hmgr1); 01053 Ntk_NetworkFree(network1); 01054 Hrc_ManagerFree(hmgr2); 01055 Ntk_NetworkFree(network2); 01056 return 1; 01057 } 01058 } 01059 if(Ntk_NetworkReadNumPrimaryInputs(network1) != 01060 Ntk_NetworkReadNumInputs(network1)) { 01061 error_append("** eqv error: Pseudo inputs present in network1. Unable to do verification.\n"); 01062 (void) fprintf(vis_stderr, "%s", error_string()); 01063 if(execMode) { 01064 Hrc_ManagerFree(hmgr1); 01065 Ntk_NetworkFree(network1); 01066 } 01067 Hrc_ManagerFree(hmgr2); 01068 Ntk_NetworkFree(network2); 01069 return 1; 01070 } 01071 if(Ntk_NetworkReadNumPrimaryInputs(network2) != 01072 Ntk_NetworkReadNumInputs(network2)) { 01073 error_append("** eqv error: Pseudo inputs present in network2. Unable to do verification.\n"); 01074 (void) fprintf(vis_stderr, "%s", error_string()); 01075 if(execMode) { 01076 Hrc_ManagerFree(hmgr1); 01077 Ntk_NetworkFree(network1); 01078 } 01079 Hrc_ManagerFree(hmgr2); 01080 Ntk_NetworkFree(network2); 01081 return 1; 01082 } 01083 if(Ntk_NetworkReadNumPrimaryInputs(network1) != 01084 Ntk_NetworkReadNumPrimaryInputs(network2)) { 01085 error_append("** eqv error: Different number of inputs in the two networks.\n"); 01086 (void) fprintf(vis_stderr, "%s", error_string()); 01087 if(execMode) { 01088 Hrc_ManagerFree(hmgr1); 01089 Ntk_NetworkFree(network1); 01090 } 01091 Hrc_ManagerFree(hmgr2); 01092 Ntk_NetworkFree(network2); 01093 return 1; 01094 } 01095 01096 /* Start the timer before calling the equivalence checker. */ 01097 if (timeOutPeriod > 0){ 01098 (void) signal(SIGALRM, (void(*)(int))TimeOutHandle); 01099 (void) alarm(timeOutPeriod); 01100 if (setjmp(timeOutEnv) > 0) { 01101 (void) fprintf(vis_stderr, "Timeout occurred after %d seconds.\n", 01102 timeOutPeriod); 01103 alarm(0); 01104 return 1; 01105 } 01106 } 01107 01108 if(fileFlag) { 01109 rootsTable = st_init_table(strcmp, st_strhash); 01110 leavesTable = st_init_table(strcmp, st_strhash); 01111 check = ReadRootLeafMap(inputFile, rootsTable, leavesTable); 01112 fclose(inputFile); 01113 if(check == 0) { 01114 st_free_table(rootsTable); 01115 st_free_table(leavesTable); 01116 (void) fprintf(vis_stderr, "** eqv error: No data in the input file\n"); 01117 alarm(0); 01118 return 1; 01119 } 01120 switch (check) { 01121 case 1 : 01122 st_free_table(rootsTable); 01123 outputMap = MapPrimaryOutputsByName(network1, network2); 01124 if((outputMap == NIL(st_table)) || !TestLeavesAreValid(network1, 01125 network2, 01126 leavesTable)) { 01127 st_foreach_item(leavesTable, gen, &name1, &name2) { 01128 FREE(name1); 01129 FREE(name2); 01130 } 01131 st_free_table(leavesTable); 01132 if(outputMap) { 01133 st_free_table(outputMap); 01134 } 01135 (void) fprintf(vis_stderr, "%s", error_string()); 01136 if(execMode) { 01137 Hrc_ManagerFree(hmgr1); 01138 Ntk_NetworkFree(network1); 01139 } 01140 Hrc_ManagerFree(hmgr2); 01141 Ntk_NetworkFree(network2); 01142 (void) fprintf(vis_stderr, "%s", error_string()); 01143 alarm(0); 01144 return 1; 01145 } 01146 equivalent = Eqv_NetworkVerifySequentialEquivalence(network1, 01147 network2, 01148 NIL(st_table), 01149 leavesTable, 01150 partMethod, 01151 useBackwardReach, 01152 reordering); 01153 st_foreach_item(leavesTable, gen, &name1, &name2) { 01154 FREE(name1); 01155 FREE(name2); 01156 } 01157 st_free_table(leavesTable); 01158 break; 01159 case 2 : 01160 st_free_table(leavesTable); 01161 inputMap = MapPrimaryInputsByName(network1, network2); 01162 01163 if((inputMap == NIL(st_table)) || !TestRootsAreValid(network1, 01164 network2, 01165 rootsTable)) { 01166 st_foreach_item(rootsTable, gen, &name1, &name2) { 01167 FREE(name1); 01168 FREE(name2); 01169 } 01170 st_free_table(rootsTable); 01171 if(inputMap) { 01172 st_free_table(inputMap); 01173 } 01174 (void) fprintf(vis_stderr, "%s", error_string()); 01175 if(execMode) { 01176 Hrc_ManagerFree(hmgr1); 01177 Ntk_NetworkFree(network1); 01178 } 01179 Hrc_ManagerFree(hmgr2); 01180 Ntk_NetworkFree(network2); 01181 alarm(0); 01182 return 1; 01183 } 01184 equivalent = Eqv_NetworkVerifySequentialEquivalence(network1, 01185 network2, 01186 rootsTable, 01187 NIL(st_table), 01188 partMethod, 01189 useBackwardReach, 01190 reordering); 01191 st_foreach_item(rootsTable, gen, &name1, &name2) { 01192 FREE(name1); 01193 FREE(name2); 01194 } 01195 st_free_table(rootsTable); 01196 break; 01197 case 3 : 01198 if(TestRootsAreValid(network1, network2, rootsTable) && 01199 TestLeavesAreValid(network1, network2, leavesTable)) { 01200 equivalent = Eqv_NetworkVerifySequentialEquivalence(network1, 01201 network2, 01202 rootsTable, 01203 leavesTable, 01204 partMethod, 01205 useBackwardReach, 01206 reordering); 01207 st_foreach_item(rootsTable, gen, &name1, &name2) { 01208 FREE(name1); 01209 FREE(name2); 01210 } 01211 st_free_table(rootsTable); 01212 st_foreach_item(leavesTable, gen, &name1, &name2) { 01213 FREE(name1); 01214 FREE(name2); 01215 } 01216 st_free_table(leavesTable); 01217 } 01218 else { 01219 if(execMode) { 01220 Hrc_ManagerFree(hmgr1); 01221 Ntk_NetworkFree(network1); 01222 } 01223 Hrc_ManagerFree(hmgr2); 01224 Ntk_NetworkFree(network2); 01225 st_foreach_item(rootsTable, gen, &name1, &name2) { 01226 FREE(name1); 01227 FREE(name2); 01228 } 01229 st_free_table(rootsTable); 01230 st_foreach_item(leavesTable, gen, &name1, &name2) { 01231 FREE(name1); 01232 FREE(name2); 01233 } 01234 st_free_table(leavesTable); 01235 (void) fprintf(vis_stderr, "%s", error_string()); 01236 alarm(0); 01237 return 1; 01238 } 01239 } 01240 } 01241 else { 01242 outputMap = MapPrimaryOutputsByName(network1, network2); 01243 inputMap = MapPrimaryInputsByName(network1, network2); 01244 if((inputMap == NIL(st_table)) || (outputMap == NIL(st_table))) { 01245 if(inputMap) { 01246 st_free_table(inputMap); 01247 } 01248 if(outputMap) { 01249 st_free_table(outputMap); 01250 } 01251 if(execMode) { 01252 Hrc_ManagerFree(hmgr1); 01253 Ntk_NetworkFree(network1); 01254 } 01255 Hrc_ManagerFree(hmgr2); 01256 Ntk_NetworkFree(network2); 01257 (void) fprintf(vis_stderr, "%s", error_string()); 01258 alarm(0); 01259 return 1; /* all primary outputs do not match */ 01260 } 01261 st_free_table(inputMap); 01262 st_free_table(outputMap); 01263 equivalent = Eqv_NetworkVerifySequentialEquivalence(network1, network2, 01264 NIL(st_table), 01265 NIL(st_table), 01266 partMethod, 01267 useBackwardReach, 01268 reordering); 01269 } 01270 if(equivalent) { 01271 (void) fprintf(vis_stdout, "Networks are sequentially equivalent.\n\n"); 01272 } 01273 else { 01274 (void) fprintf(vis_stdout, 01275 "Networks are NOT sequentially equivalent.\n\n"); 01276 } 01277 01278 if (printBddInfo) { 01279 bdd_print_stats(Ntk_NetworkReadMddManager(network2), vis_stdout); 01280 } 01281 01282 if(execMode) { 01283 Hrc_ManagerFree(hmgr1); 01284 Ntk_NetworkFree(network1); 01285 } 01286 Hrc_ManagerFree(hmgr2); 01287 Ntk_NetworkFree(network2); 01288 01289 alarm(0); 01290 return 0; /* normal exit */ 01291 01292 usage : 01293 (void) fprintf(vis_stderr, "usage: seq_verify [-b] [-f filename] [-h] [-p partition method] [-t time] [-B]\n\t\t [-i] [-r] file1 [file2]\n"); 01294 (void) fprintf(vis_stderr, " -b input files are BLIF\n"); 01295 (void) fprintf(vis_stderr, " -f file variable name correspondence file\n"); 01296 (void) fprintf(vis_stderr, " -h print the command usage\n"); 01297 (void) fprintf(vis_stderr, " -p method partitioning method for product machine\n"); 01298 (void) fprintf(vis_stderr, " -t time time out period (in seconds)\n"); 01299 (void) fprintf(vis_stderr, " -B use backward image computation\n"); 01300 (void) fprintf(vis_stderr, " -i print BDD statistics\n"); 01301 (void) fprintf(vis_stderr, " -r enable BDD variable reordering\n"); 01302 return 1; /* error exit */ 01303 } 01304 01314 static void 01315 TimeOutHandle(void) 01316 { 01317 longjmp(timeOutEnv, 1); 01318 }
1.7.3