- Generated on Wed Oct 12 2011 00:34:49 for VIS by
1.7.3
|
VIS
|
00001 00030 #include "grabInt.h" 00031 00032 /*---------------------------------------------------------------------------*/ 00033 /* Constant declarations */ 00034 /*---------------------------------------------------------------------------*/ 00035 00036 /*---------------------------------------------------------------------------*/ 00037 /* Structure declarations */ 00038 /*---------------------------------------------------------------------------*/ 00039 00040 /*---------------------------------------------------------------------------*/ 00041 /* Type declarations */ 00042 /*---------------------------------------------------------------------------*/ 00043 00044 /*---------------------------------------------------------------------------*/ 00045 /* Variable declarations */ 00046 /*---------------------------------------------------------------------------*/ 00047 static jmp_buf timeOutEnv; 00048 00049 /*---------------------------------------------------------------------------*/ 00050 /* Macro declarations */ 00051 /*---------------------------------------------------------------------------*/ 00052 00055 /*---------------------------------------------------------------------------*/ 00056 /* Static function prototypes */ 00057 /*---------------------------------------------------------------------------*/ 00058 00059 static int CommandGrab(Hrc_Manager_t ** hmgr, int argc, char ** argv); 00060 static void TimeOutHandle(void); 00061 00064 /*---------------------------------------------------------------------------*/ 00065 /* Definition of exported functions */ 00066 /*---------------------------------------------------------------------------*/ 00067 00079 void 00080 Grab_Init(void) 00081 { 00082 /* 00083 * Add a command to the global command table. By using the leading 00084 * underscore, the command will be listed under "help -a" but not "help". 00085 */ 00086 Cmd_CommandAdd("_grab_test", CommandGrab, 0); 00087 } 00088 00089 00099 void 00100 Grab_End(void) 00101 { 00102 00103 } 00104 00105 00155 void 00156 Grab_NetworkCheckInvariants( 00157 Ntk_Network_t *network, 00158 array_t *InvariantFormulaArray, 00159 char *refineAlgorithm, 00160 int fineGrainFlag, 00161 int refineMinFlag, 00162 int useArdcFlag, 00163 int cexType, 00164 int verbosity, 00165 int dbgLevel, 00166 int printInputs, 00167 FILE *debugFile, 00168 int useMore, 00169 char *driverName) 00170 { 00171 mdd_manager *mddManager = NIL(mdd_manager); 00172 graph_t *partition; 00173 Ctlp_Formula_t *invFormula; 00174 Ctlsp_Formula_t *invFormula_sp; 00175 array_t *invStatesArray; 00176 array_t *resultArray; 00177 st_table *absLatchTable, *absBnvTable; 00178 st_table *coiLatchTable, *coiBnvTable; 00179 Fsm_Fsm_t *absFsm; 00180 array_t *visibleVarMddIds, *invisibleVarMddIds; 00181 int concreteLatchCount, abstractLatchCount; 00182 int concreteBnvCount, abstractBnvCount; 00183 st_table *nodeToFaninNumberTable; 00184 mdd_t *rchStates, *invStates = NIL(mdd_t); /*=mdd_one(mddManager);*/ 00185 array_t *SORs, *save_SORs; 00186 boolean refineDirection, runMinimization, isLastStep; 00187 int staticOrderFlag, partitionFlag; 00188 int cexLength, refineIteration; 00189 array_t *addedVarsAtCurrentLevel = NIL(array_t); 00190 array_t *addedBnvsAtCurrentLevel = NIL(array_t); 00191 int auxValue1, auxValue2, flag, i; 00192 00193 long startTime, endTime, totalTime; 00194 long mcStartTime, mcEndTime, mcTime; 00195 long sorEndTime, sorTime; 00196 long conEndTime, conTime; 00197 long dirStartTime, dirEndTime, dirTime; 00198 long refStartTime, refEndTime, refTime; 00199 long miniStartTime, miniEndTime, miniTime; 00200 00201 00202 if ( strcmp(refineAlgorithm, "GRAB") ) { 00203 fprintf(vis_stdout, 00204 "** ci error: Abstraction refinement method %s not available\n", 00205 refineAlgorithm); 00206 return; 00207 } 00208 00209 /* if the mddIds haven't been assigned to the network nodes, 00210 * we assign them incrementally (i.e., staticOrderFlag==1). 00211 */ 00212 mddManager = Ntk_NetworkReadMddManager(network); 00213 if (mddManager == NIL(mdd_manager)) 00214 staticOrderFlag = 1; 00215 else 00216 staticOrderFlag = 0; 00217 00218 if (staticOrderFlag) { 00219 GrabNtkClearAllMddIds(network); 00220 mddManager = Ntk_NetworkInitializeMddManager(network); 00221 if (verbosity >= 2) 00222 bdd_dynamic_reordering(mddManager, BDD_REORDER_SIFT, 00223 BDD_REORDER_VERBOSITY); 00224 else 00225 bdd_dynamic_reordering(mddManager, BDD_REORDER_SIFT, 00226 BDD_REORDER_NO_VERBOSITY); 00227 } 00228 00229 /* if the partition hasn't been created, we create the partition 00230 * incrementally (i.e., partitionFlag==1) 00231 */ 00232 partition = Part_NetworkReadPartition(network); 00233 if (partition == NIL(graph_t)) 00234 partitionFlag = GRAB_PARTITION_BUILD; 00235 else 00236 partitionFlag = GRAB_PARTITION_NOCHANGE; 00237 00238 /* used by the refinement algorithm as a tie-breaker */ 00239 nodeToFaninNumberTable = st_init_table(st_ptrcmp, st_ptrhash); 00240 00241 /*************************************************************************** 00242 * check the invariants 00243 ***************************************************************************/ 00244 resultArray = array_alloc(int, array_n(InvariantFormulaArray)); 00245 00246 arrayForEachItem(Ctlp_Formula_t *, InvariantFormulaArray, i, invFormula) { 00247 invFormula_sp = Ctlsp_CtlFormulaToCtlsp(invFormula); 00248 00249 /* this is required for the following code to function correctly */ 00250 visibleVarMddIds = invisibleVarMddIds = NIL(array_t); 00251 invStatesArray = SORs = save_SORs = NIL(array_t); 00252 00253 mcTime = sorTime = conTime = dirTime = refTime = miniTime = 0; 00254 startTime = util_cpu_ctime(); 00255 00256 /* record the number of latches in the cone-of-influence */ 00257 coiLatchTable = GrabComputeCOIAbstraction(network, invFormula); 00258 concreteLatchCount = st_count(coiLatchTable); 00259 /* build the initial abstract model */ 00260 absLatchTable = GrabComputeInitialAbstraction(network, invFormula); 00261 abstractLatchCount = st_count(absLatchTable); 00262 if (verbosity >= 3) { 00263 GrabPrintNodeHashTable("InitialAbstractLatches", absLatchTable); 00264 } 00265 00266 /* initialize the abs./concrete table for boolean network variables*/ 00267 coiBnvTable = st_init_table(st_ptrcmp, st_ptrhash); 00268 abstractBnvCount = concreteBnvCount = 0; 00269 if (fineGrainFlag == 1) { 00270 absBnvTable = st_init_table(st_ptrcmp, st_ptrhash); 00271 }else { 00272 absBnvTable = NIL(st_table); 00273 } 00274 /* if the concrete partition is available, retrieve form it the 00275 * bnvs; otherwise, we incrementally create bnvs (for the current 00276 * absLatches only)---this is designed for performance concerns */ 00277 if (partitionFlag == GRAB_PARTITION_NOCHANGE) { 00278 Part_PartitionReadOrCreateBnvs(network, coiLatchTable, coiBnvTable); 00279 concreteBnvCount = st_count(coiBnvTable); 00280 } 00281 00282 /* Outer Loop---Over Refinements For Different SOR Lengths 00283 */ 00284 refineIteration = 0; 00285 isLastStep = 0; 00286 while(1) { 00287 long grabStartTime = util_cpu_ctime(); 00288 00289 /* Build the Abstract Finite State Machine */ 00290 absFsm = GrabCreateAbstractFsm(network, coiBnvTable, absLatchTable, 00291 absBnvTable, partitionFlag, TRUE); 00292 concreteBnvCount = st_count(coiBnvTable); 00293 invisibleVarMddIds = GrabGetInvisibleVarMddIds(absFsm, absLatchTable, 00294 absBnvTable); 00295 visibleVarMddIds = GrabGetVisibleVarMddIds(absFsm, absLatchTable); 00296 /* sanity check */ 00297 isLastStep = (array_n(invisibleVarMddIds)==0); 00298 if (isLastStep) { 00299 assert(abstractLatchCount == concreteLatchCount); 00300 } 00301 00302 /* Compute The Invariant States If They Are Not Available */ 00303 if (invStatesArray == NIL(array_t)) { 00304 mdd_t * tautology = mdd_one(mddManager); 00305 array_t *careSetArray = array_alloc(mdd_t *, 0); 00306 array_insert(mdd_t *, careSetArray, 0, tautology); 00307 invStates = Mc_FsmEvaluateFormula(absFsm, invFormula, tautology, 00308 NIL(Fsm_Fairness_t), careSetArray, 00309 MC_NO_EARLY_TERMINATION, 00310 NIL(Fsm_HintsArray_t), Mc_None_c, 00311 McVerbosityNone_c, McDcLevelNone_c, 00312 0, McGSH_EL_c); 00313 mdd_array_free(careSetArray); 00314 invStatesArray = array_alloc(mdd_t *, 0); 00315 array_insert(mdd_t *, invStatesArray, 0, invStates); 00316 } 00317 00318 /* Conduct Forward Reachability Analysis */ 00319 rchStates = GrabFsmComputeReachableStates(absFsm, 00320 absLatchTable, 00321 absBnvTable, 00322 invStatesArray, 00323 verbosity); 00324 00325 mcEndTime = util_cpu_ctime(); 00326 mcTime += (mcEndTime - grabStartTime); 00327 if (verbosity >= 1) { 00328 fprintf(vis_stdout, 00329 "-- grab: absLatch [%d/%d], absBnv [%d/%d], mc time is %5g s\n", 00330 abstractLatchCount, concreteLatchCount, 00331 abstractBnvCount, concreteBnvCount, 00332 (double)(mcEndTime-grabStartTime)/1000.0); 00333 } 00334 00335 /* if bad states cannot be reached, the property is true; 00336 * if absFsm is concrete, the property is false 00337 */ 00338 flag = mdd_lequal(rchStates, invStates, 1, 1); 00339 mdd_free(rchStates); 00340 if (flag || isLastStep) { 00341 /* set the debugging info, if necessary */ 00342 if (!flag) 00343 SORs = mdd_array_duplicate(Fsm_FsmReadReachabilityOnionRings(absFsm)); 00344 Fsm_FsmSubsystemFree(absFsm); 00345 absFsm = NIL(Fsm_Fsm_t); 00346 array_free(invisibleVarMddIds); 00347 array_free(visibleVarMddIds); 00348 break; 00349 } 00350 00351 /* Build The Synchronous Onion Rings (SORs) */ 00352 Fsm_FsmFreeImageInfo(absFsm); 00353 SORs = GrabFsmComputeSynchronousOnionRings(absFsm, absLatchTable, 00354 absBnvTable, NIL(array_t), 00355 invStates, cexType, 00356 verbosity); 00357 sorEndTime = util_cpu_ctime(); 00358 sorTime += (sorEndTime - mcEndTime); 00359 00360 /* Concretize Multiple Counter-Examples */ 00361 cexLength = array_n(SORs)-1; 00362 flag = !Bmc_AbstractCheckAbstractTraces(network, SORs, coiLatchTable, 00363 0, dbgLevel, printInputs); 00364 conEndTime = util_cpu_ctime(); 00365 conTime += (conEndTime - sorEndTime); 00366 if (!flag) { 00367 if (verbosity >= 1) 00368 fprintf(vis_stdout, 00369 "-- grab: find length-%d concrete counter-examples\n", 00370 cexLength); 00371 Fsm_FsmSubsystemFree(absFsm); 00372 absFsm = NIL(Fsm_Fsm_t); 00373 array_free(invisibleVarMddIds); 00374 array_free(visibleVarMddIds); 00375 break; 00376 }else { 00377 if (verbosity >= 2) 00378 fprintf(vis_stdout, 00379 "-- grab: find length-%d spurious counter-examples\n", 00380 cexLength); 00381 } 00382 00383 /* Innor Loop---Over Refinements For The Same SOR Length 00384 */ 00385 save_SORs = mdd_array_duplicate(SORs); 00386 addedVarsAtCurrentLevel = array_alloc(int, 0); 00387 addedBnvsAtCurrentLevel = array_alloc(int, 0); 00388 refineDirection = 1; 00389 runMinimization = 0; 00390 00391 while (1) { 00392 00393 int skip_refinement = 0; 00394 00395 /* Get the appropriate refinement direction: 00396 * runMinimization==1 --> BOOLEAN 00397 * fineGrainFlag==0 --> SEQUENTIAL 00398 * coiBnvTable is empty --> SEQUENTIAL 00399 * refineDirection==0 --> BOOLEAN 00400 */ 00401 if ( !runMinimization && refineDirection) { 00402 if ( fineGrainFlag && st_count(coiBnvTable)>0 ) { 00403 dirStartTime = util_cpu_ctime(); 00404 #if 0 00405 refineDirection = !GrabTestRefinementSetSufficient(network, 00406 save_SORs, 00407 absLatchTable, 00408 verbosity); 00409 #endif 00410 runMinimization = (refineDirection==0); 00411 dirEndTime = util_cpu_ctime(); 00412 dirTime += (dirEndTime - dirStartTime); 00413 } 00414 } 00415 00416 if (verbosity >= 3 && refineDirection==0) 00417 fprintf(vis_stdout, "refinement is in %s direction\n", 00418 (refineDirection? "both":"boolean")); 00419 00420 /* Minimize the refinement set of latches */ 00421 if (runMinimization) { 00422 int n_latches = st_count(absLatchTable); 00423 int break_flag; 00424 if (refineMinFlag && array_n(addedVarsAtCurrentLevel) > 1) { 00425 miniStartTime = util_cpu_ctime(); 00426 GrabMinimizeLatchRefinementSet(network, 00427 &absLatchTable, 00428 &absBnvTable, 00429 addedVarsAtCurrentLevel, 00430 &addedBnvsAtCurrentLevel, 00431 save_SORs, 00432 verbosity); 00433 abstractLatchCount = st_count(absLatchTable); 00434 abstractBnvCount = absBnvTable? st_count(absBnvTable):st_count(coiBnvTable); 00435 array_free(addedVarsAtCurrentLevel); 00436 addedVarsAtCurrentLevel = array_alloc(int, 0); 00437 miniEndTime = util_cpu_ctime(); 00438 miniTime += (miniEndTime - miniStartTime); 00439 } 00440 00441 /* if the refinement set of bnvs is also sufficient, break */ 00442 break_flag = 1; 00443 if (fineGrainFlag && st_count(coiBnvTable)>0) { 00444 dirStartTime = util_cpu_ctime(); 00445 break_flag = GrabTestRefinementBnvSetSufficient(network, 00446 coiBnvTable, 00447 save_SORs, 00448 absLatchTable, 00449 absBnvTable, 00450 verbosity); 00451 dirEndTime = util_cpu_ctime(); 00452 dirTime += (dirEndTime - dirStartTime); 00453 } 00454 if (break_flag) { 00455 if (verbosity >= 1) 00456 fprintf(vis_stdout, 00457 "-- grab: remove length-%d spurious counter-examples\n\n", 00458 cexLength); 00459 break; 00460 } 00461 00462 /* Otherwise, skip this refinement step, because the 00463 * current absFsm is not well-defined (some latches have 00464 * been droped) 00465 */ 00466 SORs = mdd_array_duplicate(save_SORs); 00467 if (n_latches > st_count(absLatchTable)) 00468 skip_refinement = 1; 00469 00470 refineDirection = 0; 00471 runMinimization = 0; 00472 } 00473 00474 /* compute the refinement (by Grab) 00475 */ 00476 if (!skip_refinement) { 00477 array_t *addedVars = array_alloc(int, 0); 00478 array_t *addedBnvs = array_alloc(int, 0); 00479 auxValue1 = st_count(absLatchTable) + 00480 ((absBnvTable==NIL(st_table))? 0:st_count(absBnvTable)); 00481 00482 refStartTime = util_cpu_ctime(); 00483 00484 /* create the abstract fsm */ 00485 Fsm_FsmSubsystemFree(absFsm); 00486 absFsm = GrabCreateAbstractFsm(network, coiBnvTable, absLatchTable, 00487 absBnvTable, 00488 GRAB_PARTITION_NOCHANGE, 00489 FALSE); 00490 /* pick refinement variables */ 00491 GrabRefineAbstractionByGrab(absFsm, 00492 SORs, 00493 absLatchTable, 00494 absBnvTable, 00495 addedVars, 00496 addedBnvs, 00497 refineDirection, 00498 nodeToFaninNumberTable, 00499 verbosity); 00500 array_append(addedVarsAtCurrentLevel, addedVars); 00501 array_append(addedBnvsAtCurrentLevel, addedBnvs); 00502 array_free(addedVars); 00503 array_free(addedBnvs); 00504 /* Sanity check! */ 00505 auxValue2 = st_count(absLatchTable) + 00506 ((absBnvTable==NIL(st_table))? 0:st_count(absBnvTable)); 00507 assert(auxValue1 < auxValue2); 00508 00509 abstractLatchCount = st_count(absLatchTable); 00510 abstractBnvCount = absBnvTable? st_count(absBnvTable):st_count(coiBnvTable); 00511 00512 refEndTime = util_cpu_ctime(); 00513 refTime += (refEndTime - refStartTime); 00514 if (verbosity >= 3) { 00515 fprintf(vis_stdout, 00516 "-- grab: absLatch [%d/%d], absBnv [%d/%d], ref time is %5g s\n", 00517 abstractLatchCount, concreteLatchCount, 00518 abstractBnvCount, concreteBnvCount, 00519 (double)(refEndTime - refStartTime)/1000.0); 00520 } 00521 00522 refineIteration++; 00523 } 00524 00525 /* Create The Refined Abstract FSM */ 00526 Fsm_FsmSubsystemFree(absFsm); 00527 array_free(invisibleVarMddIds); 00528 array_free(visibleVarMddIds); 00529 absFsm = GrabCreateAbstractFsm(network, coiBnvTable, absLatchTable, 00530 absBnvTable, partitionFlag, TRUE); 00531 invisibleVarMddIds = GrabGetInvisibleVarMddIds(absFsm, absLatchTable, 00532 absBnvTable); 00533 visibleVarMddIds = GrabGetVisibleVarMddIds(absFsm, absLatchTable); 00534 concreteBnvCount = st_count(coiBnvTable); 00535 /* sanity check */ 00536 isLastStep = (array_n(invisibleVarMddIds)==0); 00537 if (isLastStep) { 00538 assert(abstractLatchCount == concreteLatchCount); 00539 } 00540 00541 /* Reduce The Current SORs (with forward reachability analysis) */ 00542 mcStartTime = util_cpu_ctime(); 00543 rchStates = GrabFsmComputeConstrainedReachableStates(absFsm, 00544 absLatchTable, 00545 absBnvTable, 00546 SORs, 00547 verbosity); 00548 mdd_array_free(SORs); 00549 SORs = NIL(array_t); 00550 mcEndTime = util_cpu_ctime(); 00551 mcTime += (mcEndTime - mcStartTime); 00552 if (verbosity >= 2) { 00553 fprintf(vis_stdout, 00554 "-- grab: absLatch [%d/%d], absBnv [%d/%d], mc time is %5g s\n", 00555 abstractLatchCount, concreteLatchCount, 00556 abstractBnvCount, concreteBnvCount, 00557 (double)(mcEndTime-mcStartTime)/1000.0); 00558 } 00559 00560 /* if bad states is no longer reachable, break out */ 00561 flag = mdd_lequal(rchStates, invStates, 1, 1); 00562 mdd_free(rchStates); 00563 if (isLastStep || flag) { 00564 if (!isLastStep && refineDirection == 1) { 00565 runMinimization = 1; 00566 refineDirection = 0; 00567 continue; 00568 }else 00569 break; 00570 } 00571 00572 /* Build the new SORs (with backward reachability analysis) */ 00573 Fsm_FsmFreeImageInfo(absFsm); 00574 SORs = GrabFsmComputeSynchronousOnionRings(absFsm, 00575 absLatchTable, 00576 absBnvTable, 00577 NIL(array_t), 00578 invStates, 00579 cexType, 00580 verbosity); 00581 sorEndTime = util_cpu_ctime(); 00582 sorTime += (sorEndTime - mcEndTime); 00583 00584 } /* End of the Inner Loop */ 00585 00586 00587 /* Minimize The Refinement Set of Boolean Network Variables (BNVs) 00588 */ 00589 if (fineGrainFlag==1 && refineMinFlag 00590 && array_n(addedBnvsAtCurrentLevel)>1) { 00591 00592 miniStartTime = util_cpu_ctime(); 00593 GrabMinimizeBnvRefinementSet(network, 00594 coiBnvTable, 00595 absLatchTable, 00596 &absBnvTable, 00597 addedBnvsAtCurrentLevel, 00598 save_SORs, 00599 verbosity); 00600 abstractLatchCount = st_count(absLatchTable); 00601 abstractBnvCount = st_count(absBnvTable); 00602 miniEndTime = util_cpu_ctime(); 00603 miniTime += (miniEndTime - miniStartTime); 00604 } 00605 mdd_array_free(save_SORs); 00606 00607 /* Clean-ups 00608 */ 00609 Fsm_FsmSubsystemFree(absFsm); 00610 absFsm = NIL(Fsm_Fsm_t); 00611 array_free(invisibleVarMddIds); 00612 array_free(visibleVarMddIds); 00613 array_free(addedVarsAtCurrentLevel); 00614 array_free(addedBnvsAtCurrentLevel); 00615 addedVarsAtCurrentLevel = NIL(array_t); 00616 addedBnvsAtCurrentLevel = NIL(array_t); 00617 00618 } /* End of the Outer Loop */ 00619 00620 endTime = util_cpu_ctime(); 00621 totalTime = endTime - startTime; 00622 00623 /* Print out the debugging information */ 00624 if (dbgLevel > 0) { 00625 FILE *tmpFile = vis_stdout; 00626 extern FILE *vis_stdpipe; 00627 00628 if (debugFile) 00629 vis_stdpipe = debugFile; 00630 else if (useMore) 00631 vis_stdpipe = popen("more", "w"); 00632 else 00633 vis_stdpipe = vis_stdout; 00634 vis_stdout = vis_stdpipe; 00635 00636 if (flag) { 00637 fprintf(vis_stdout, "# %s: formula passed --- ", driverName); 00638 Ctlp_FormulaPrint(vis_stdout, invFormula); 00639 fprintf(vis_stdout, "\n"); 00640 }else { 00641 if(dbgLevel != 2) 00642 { 00643 fprintf(vis_stdout, "# %s: formula p%d failed --- ", driverName, i+1); 00644 Ctlp_FormulaPrint(vis_stdout, invFormula); 00645 fprintf(vis_stdout, "\n# %s: calling debugger\n", driverName); 00646 } 00647 flag = !Bmc_AbstractCheckAbstractTraces(network, SORs, coiLatchTable, 00648 1, dbgLevel, printInputs); 00649 } 00650 00651 if (vis_stdout != tmpFile && vis_stdout != debugFile) 00652 (void)pclose(vis_stdpipe); 00653 vis_stdout = tmpFile; 00654 } 00655 00656 if (verbosity >= 2 ) { 00657 fprintf(vis_stdout, "\n-- grab: total cpu time = %5g\n", 00658 (double)totalTime/1000.0); 00659 if (verbosity >= 3) { 00660 fprintf(vis_stdout, "-- grab: mc time = %5.1f\t(%3.1f%%)\n", 00661 (double)mcTime/1000.0, (100.0*mcTime/totalTime)); 00662 fprintf(vis_stdout, "-- grab: sor time = %5.1f\t(%3.1f%%)\n", 00663 (double)sorTime/1000.0, (100.0*sorTime/totalTime)); 00664 fprintf(vis_stdout, "-- grab: con time = %5.1f\t(%3.1f%%)\n", 00665 (double)conTime/1000.0, (100.0*conTime/totalTime)); 00666 fprintf(vis_stdout, "-- grab: ref time = %5.1f\t(%3.1f%%)\n", 00667 (double)refTime/1000.0, (100.0*refTime/totalTime)); 00668 fprintf(vis_stdout, "-- grab: min time = %5.1f\t(%3.1f%%)\n", 00669 (double)miniTime/1000.0,(100.0*miniTime/totalTime)); 00670 fprintf(vis_stdout, "-- grab: dir time = %5.1f\t(%3.1f%%)\n", 00671 (double)dirTime/1000.0, (100.0*dirTime/totalTime)); 00672 } 00673 } 00674 00675 if (verbosity >= 1) { 00676 if (concreteLatchCount > 0) { 00677 fprintf(vis_stdout, "-- grab: abs latch percentage = %d %%\n", 00678 100 * abstractLatchCount/concreteLatchCount ); 00679 } 00680 if (verbosity >= 3) { 00681 fprintf(vis_stdout, "-- grab: abs latch = %d\n", abstractLatchCount); 00682 fprintf(vis_stdout, "-- grab: coi latch = %d\n", concreteLatchCount); 00683 } 00684 if (concreteBnvCount > 0) { 00685 fprintf(vis_stdout, "-- grab: abs bnv percentage = %d %%\n", 00686 (100 * abstractBnvCount/concreteBnvCount) ); 00687 if (verbosity >= 3) { 00688 fprintf(vis_stdout, "-- grab: abs bnv = %d\n", abstractBnvCount); 00689 fprintf(vis_stdout, "-- grab: coi bnv = %d\n", concreteBnvCount); 00690 } 00691 abstractBnvCount += abstractLatchCount; 00692 concreteBnvCount += concreteLatchCount; 00693 fprintf(vis_stdout, "-- grab: total abs var percentage = %d %%\n", 00694 (100 * abstractBnvCount/concreteBnvCount) ); 00695 if (verbosity >= 3) { 00696 fprintf(vis_stdout, "-- grab: abs var = %d\n", 00697 abstractBnvCount); 00698 fprintf(vis_stdout, "-- grab: coi var = %d\n", 00699 concreteBnvCount); 00700 } 00701 } 00702 fprintf(vis_stdout, "-- grab: total refinement iterations = %d\n", 00703 refineIteration); 00704 fprintf(vis_stdout, "-- grab: total image computations %d\n", 00705 Img_GetNumberOfImageComputation(Img_Forward_c)); 00706 fprintf(vis_stdout, "-- grab: total preimage computations %d\n", 00707 Img_GetNumberOfImageComputation(Img_Backward_c)); 00708 00709 if (verbosity >= 3) { 00710 GrabPrintNodeHashTable("AbstractLatchRankings", absLatchTable); 00711 if (fineGrainFlag) 00712 GrabPrintNodeHashTable("AbstractBnvRankings", absBnvTable); 00713 } 00714 } 00715 00716 /* Clean-up's 00717 */ 00718 st_free_table(coiLatchTable); 00719 st_free_table(absLatchTable); 00720 st_free_table(coiBnvTable); 00721 if (fineGrainFlag) { 00722 st_free_table(absBnvTable); 00723 } 00724 mdd_array_free(invStatesArray); 00725 if (!flag) mdd_array_free(SORs); 00726 00727 Ctlsp_FormulaFree(invFormula_sp); 00728 00729 /* Store the verification results in an array (1--passed, 0--failed) */ 00730 array_insert(int, resultArray, i, flag); 00731 } 00732 00733 /* print whether the set of invariants passed or failed 00734 */ 00735 fprintf(vis_stdout, "\n# %s: Summary of invariant pass/fail\n", driverName); 00736 arrayForEachItem(Ctlp_Formula_t *, InvariantFormulaArray, i, invFormula) { 00737 flag = array_fetch(int, resultArray, i); 00738 if (flag) { 00739 (void) fprintf(vis_stdout, "# %s: formula passed --- ", driverName); 00740 Ctlp_FormulaPrint(vis_stdout, (invFormula)); 00741 fprintf(vis_stdout, "\n"); 00742 } else { 00743 (void) fprintf(vis_stdout, "# %s: formula failed --- ", driverName); 00744 Ctlp_FormulaPrint(vis_stdout, (invFormula)); 00745 fprintf(vis_stdout, "\n"); 00746 } 00747 } 00748 00749 /* free the current partition and mdd manager if necessary */ 00750 if (partitionFlag) { 00751 Ntk_NetworkFreeApplInfo(network, PART_NETWORK_APPL_KEY); 00752 } 00753 if (staticOrderFlag) { 00754 mdd_quit(mddManager); 00755 Ntk_NetworkSetMddManager(network, NIL(mdd_manager)); 00756 GrabNtkClearAllMddIds(network); 00757 } 00758 st_free_table(nodeToFaninNumberTable); 00759 array_free(resultArray); 00760 00761 } 00762 00763 00764 /*---------------------------------------------------------------------------*/ 00765 /* Definition of internal functions */ 00766 /*---------------------------------------------------------------------------*/ 00767 00768 00769 /*---------------------------------------------------------------------------*/ 00770 /* Definition of static functions */ 00771 /*---------------------------------------------------------------------------*/ 00772 00913 static int 00914 CommandGrab( 00915 Hrc_Manager_t ** hmgr, 00916 int argc, 00917 char ** argv) 00918 { 00919 int c, verbosity; 00920 char InvFileName[256]; 00921 FILE *FP, *dbgFile; 00922 array_t *InvariantFormulaArray; 00923 Ntk_Network_t *network; 00924 static int timeOutPeriod = 0; 00925 00926 char refineAlgorithm[256]; 00927 int cexType = 0; 00928 int refineMinFlag; 00929 int fineGrainFlag; 00930 int useArdcFlag = 0; 00931 long startTime, endTime; 00932 00933 char *dbgFileName = NIL(char); 00934 int dbgLevel, printInputs, useMore; 00935 00936 startTime = util_cpu_ctime(); 00937 00938 Img_ResetNumberOfImageComputation(Img_Both_c); 00939 00940 /* the default setting is Grab+, 00941 * Generational Refinement of Ariadne's Bundle of SORs 00942 */ 00943 strcpy(refineAlgorithm, "GRAB"); 00944 cexType = GRAB_CEX_SOR; 00945 fineGrainFlag = 1; 00946 refineMinFlag = 1; 00947 verbosity = 0; 00948 00949 dbgLevel = 0; 00950 printInputs = 0; 00951 useMore = 0; 00952 00953 /* 00954 * Parse command line options. 00955 */ 00956 util_getopt_reset(); 00957 while ((c = util_getopt(argc, argv, "a:c:d:F:M:imt:v:f:h")) != EOF) { 00958 switch(c) { 00959 case 'a': 00960 strcpy(refineAlgorithm, util_optarg); 00961 break; 00962 case 'F': 00963 fineGrainFlag = atoi(util_optarg); 00964 break; 00965 case 'M': 00966 refineMinFlag = atoi(util_optarg); 00967 break; 00968 case 'c': 00969 cexType = atoi(util_optarg); 00970 break; 00971 case 'D': 00972 useArdcFlag = 1; 00973 break; 00974 case 't': 00975 timeOutPeriod = atoi(util_optarg); 00976 break; 00977 case 'v': 00978 verbosity = atoi(util_optarg); 00979 break; 00980 case 'd': 00981 dbgLevel = atoi(util_optarg); 00982 break; 00983 case 'i': 00984 printInputs = 1; 00985 break; 00986 case 'm': 00987 useMore = 1; 00988 break; 00989 case 'f': 00990 dbgFileName = util_strsav(util_optarg); 00991 break; 00992 case 'h': 00993 goto usage; 00994 default: 00995 goto usage; 00996 } 00997 } 00998 00999 if (strcmp(refineAlgorithm, "GRAB")) { 01000 fprintf(vis_stdout, "\nunknown refinement algorithm: %s\n", 01001 refineAlgorithm); 01002 goto usage; 01003 } 01004 01005 /* Make sure the flattened network is available 01006 */ 01007 network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); 01008 if (network == NIL(Ntk_Network_t)) { 01009 fprintf(vis_stdout, "%s\n", error_string()); 01010 error_init(); 01011 return 1; 01012 } 01013 01014 /* Make sure the AIG graph is available 01015 */ 01016 if (Ntk_NetworkReadMAigManager(network) == NIL(mAig_Manager_t)) { 01017 fprintf(vis_stderr, 01018 "** grab error: please run buid_partiton_maigs first\n"); 01019 return 1; 01020 } 01021 01022 /* Open the InvFile. (It must contain a single invariant property) 01023 */ 01024 if (argc - util_optind == 0) { 01025 (void) fprintf(vis_stderr, 01026 "** grab error: file containing inv formula not provided\n"); 01027 goto usage; 01028 }else if (argc - util_optind > 1) { 01029 (void) fprintf(vis_stderr, "** grab error: too many arguments\n"); 01030 goto usage; 01031 } 01032 strcpy(InvFileName, argv[util_optind]); 01033 01034 /* Parsing the InvFile 01035 */ 01036 FP = Cmd_FileOpen(InvFileName, "r", NIL(char *), 0); 01037 if (FP == NIL(FILE)) { 01038 (void) fprintf(vis_stdout, "** grab error: error in opening file %s\n", 01039 InvFileName); 01040 return 1; 01041 } 01042 InvariantFormulaArray = Ctlp_FileParseFormulaArray(FP); 01043 fclose(FP); 01044 if (InvariantFormulaArray == NIL(array_t)) { 01045 (void) fprintf(vis_stdout, 01046 "** grab error: error in parsing formulas from file %s\n", 01047 InvFileName); 01048 return 1; 01049 } 01050 01051 if (dbgFileName != NIL(char)) 01052 dbgFile = Cmd_FileOpen(dbgFileName, "r", NIL(char *), 0); 01053 else 01054 dbgFile = NIL(FILE); 01055 01056 01057 /* Set time out processing (if timeOutPeriod is set) 01058 */ 01059 if (timeOutPeriod > 0) { 01060 (void) signal(SIGALRM, (void(*)(int))TimeOutHandle); 01061 (void) alarm(timeOutPeriod); 01062 if (setjmp(timeOutEnv) > 0) { 01063 fprintf(vis_stdout, 01064 "\n# GRAB: abstract-refine - timeout occurred after %d seconds.\n", 01065 timeOutPeriod); 01066 (void) fprintf(vis_stdout, "# GRAB: data may be corrupted.\n"); 01067 endTime = util_cpu_ctime(); 01068 fprintf(vis_stdout, "# GRAB: elapsed time is %5.1f.\n", 01069 (double)(endTime - startTime)/1000.0); 01070 if (verbosity) { 01071 fprintf(vis_stdout, 01072 "-- total %d image computations and %d preimage computations\n", 01073 Img_GetNumberOfImageComputation(Img_Forward_c), 01074 Img_GetNumberOfImageComputation(Img_Backward_c)); 01075 } 01076 alarm(0); 01077 return 1; 01078 } 01079 } 01080 01081 /* Check invariants with the abstraction refinement algorithm GRAB 01082 */ 01083 Grab_NetworkCheckInvariants(network, 01084 InvariantFormulaArray, 01085 refineAlgorithm, 01086 fineGrainFlag, 01087 refineMinFlag, 01088 useArdcFlag, 01089 cexType, 01090 verbosity, 01091 dbgLevel, 01092 printInputs, 01093 dbgFile, 01094 useMore, 01095 "GRAB" 01096 ); 01097 01098 01099 /* Total cost 01100 */ 01101 if (verbosity >= 2) { 01102 endTime = util_cpu_ctime(); 01103 fprintf(vis_stdout, "# GRAB: elapsed time is %5.1f.\n", 01104 (double)(endTime - startTime)/1000.0); 01105 fprintf(vis_stdout, 01106 "-- total %d image computations and %d preimage computations\n", 01107 Img_GetNumberOfImageComputation(Img_Forward_c), 01108 Img_GetNumberOfImageComputation(Img_Backward_c)); 01109 } 01110 01111 alarm(0); 01112 return 0; /* normal exit */ 01113 01114 01115 usage: 01116 01117 (void) fprintf(vis_stderr, "usage: _grab_test [-a refine_algorithm] [-c cex_type] [-d dbg_level] [-F finegrain_flag] [-M refmin_flag] [-i] [-m] [-t period] [-v verbosity_level] [-f dbg_out] [-h] <invar_file>\n"); 01118 (void) fprintf(vis_stderr, " -a <refine_algorithm>\n"); 01119 (void) fprintf(vis_stderr, " refine_algorithm = GRAB => the GRAB refinement method (Default)\n"); 01120 (void) fprintf(vis_stderr, " -c <cex_type>\n"); 01121 (void) fprintf(vis_stderr, " cex_type = 0 => minterm state counter-example\n"); 01122 (void) fprintf(vis_stderr, " cex_type = 1 => cube state counter-example\n"); 01123 (void) fprintf(vis_stderr, " cex_type = 2 => synchronous onion rings (Default)\n"); 01124 (void) fprintf(vis_stderr, " -d <dbg_level>\n"); 01125 (void) fprintf(vis_stderr, " debug_level = 0 => no debugging (Default)\n"); 01126 (void) fprintf(vis_stderr, " debug_level = 1 => print path to state failing invariant\n"); 01127 (void) fprintf(vis_stderr, " -F <finegrain_flag>\n"); 01128 (void) fprintf(vis_stderr, " finegrain_flag = 0 => disable fine-grain abstraction\n"); 01129 (void) fprintf(vis_stderr, " finegrain_flag = 1 => enable fine-grain abstraction (Default)\n"); 01130 (void) fprintf(vis_stderr, " -M <refinemin_flag>\n"); 01131 (void) fprintf(vis_stderr, " refinemin_flag = 0 => disable greedy refinement minimization\n"); 01132 (void) fprintf(vis_stderr, " refinemin_flag = 1 => enable greedy refinement minimization (Default)\n"); 01133 (void) fprintf(vis_stderr, " -i \tPrint input values in debug traces.\n"); 01134 (void) fprintf(vis_stderr, " -m pipe debugger output through UNIX utility more\n"); 01135 (void) fprintf(vis_stderr, " -t <period> Time out period.\n"); 01136 (void) fprintf(vis_stderr, " -v <verbosity_level>\n"); 01137 (void) fprintf(vis_stderr, " verbosity_level = 0 => no feedback (Default)\n"); 01138 (void) fprintf(vis_stderr, " verbosity_level = 1 => code status\n"); 01139 (void) fprintf(vis_stderr, " verbosity_level = 2 => code status and CPU usage profile\n"); 01140 (void) fprintf(vis_stderr, " -f <dbg_out>\n"); 01141 (void) fprintf(vis_stderr, " write error trace to dbg_out\n"); 01142 (void) fprintf(vis_stderr, " <invar_file> The input file containing invariants to be checked.\n"); 01143 (void) fprintf(vis_stderr, " -h\t\t print the command usage\n"); 01144 01145 return 1; /* error exit */ 01146 } 01147 01148 01161 static void 01162 TimeOutHandle(void) 01163 { 01164 longjmp(timeOutEnv, 1); 01165 }
1.7.3