/**CFile*********************************************************************** FileName [grab.c] PackageName [grab] Synopsis [Abstraction refinement for large scale invariant checking.] Description [This file contains the functions to check invariant properties by the GRAB abstraction refinement algorithm. GRAB stands for "Generational Refinement of Ariadne's Bundle," in which the automatic refinement is guided by all shortest abstract counter-examples. For more information, please check the ICCAD'03 paper of Wang et al., "Improving Ariadne's Bundle by Following Multiple Counter-Examples in Abstraction Refinement." ] Author [Chao Wang] Copyright [Copyright (c) 2004 The Regents of the Univ. of Colorado. All rights reserved. Permission is hereby granted, without written agreement and without license or royalty fees, to use, copy, modify, and distribute this software and its documentation for any purpose, provided that the above copyright notice and the following two paragraphs appear in all copies of this software.] ******************************************************************************/ #include "grabInt.h" /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ static jmp_buf timeOutEnv; /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static int CommandGrab(Hrc_Manager_t ** hmgr, int argc, char ** argv); static void TimeOutHandle(void); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Initializes the grab package. The added command is for testing purpose only; the same algorithm can be activated by the check_invariant command.] SideEffects [] SeeAlso [Refine_End] ******************************************************************************/ void Grab_Init(void) { /* * Add a command to the global command table. By using the leading * underscore, the command will be listed under "help -a" but not "help". */ Cmd_CommandAdd("_grab_test", CommandGrab, 0); } /**Function******************************************************************** Synopsis [Ends the grab package.] SideEffects [] SeeAlso [Refine_Init] ******************************************************************************/ void Grab_End(void) { } /**Function******************************************************************** Synopsis [Check invariant formulae with abstraction refinement method Grab.] Description [Check invariant formulae with the GRAB abstraction refinement method. For each formula, an small initial abstract model is constructed, which contains only the state variables mentioned by the formula. The abstract model is then gradually refined by adding more state variables and Boolean network variables (Bnvs), until it is sufficient to decided the property. Bnvs are internal nodes of the circuit---they are selected in order to partition large combinational logic cones into smaller pieces. The selection of refinement variables (both state vars and Bnvs) is based on the analysis of all the shortest counter-examples, which are captured by a data structure called the Synchronous Onion Rings (SORs). For the algorithmic details, please check the ICCAD'03 paper of Wang et al., "Improving Ariadne's Bundle by Following Multiple Counter-Examples in Abstraction Refinement," and the ICCD'04 paper of Wang et al., "Fine-Grain Abstraction and Sequential Don't Cares for Large Scale Model Checking." The existence of a network partition is not mandatory for calling this function. However, if it does exist, it will be used by this function; otherwise, the network partition will be constructed incrementally as the abstract model grows. If the default bdd manager is not available, this function will create one and assign bdd ids incrementally as the abstract model grows. (For extremely large models, it is favorable to let the procedure assign bdd ids and construct the partition incrementally.) The parameter refineAlgorithm specifies the refinement variable selection algorithm---currently, only GRAB is available. When fineGrainFlag is FALSE, only latches are considered as the abstraction "atoms"; When fineGrainFlag is TRUE, both Bnvs and latches are considered "atoms." To disable the greedy minimization of refinement sets, set refineMinFlag to FALSE. The parameter useArdcFlag is not used at this point. By default, all the shortest counter-examples are analyzed (cexType==GRAB_CEX_SOR); when cexType is set to GRAB_CEX_MINTERM or GRAB_CEX_CUBE, only a minterm or cube state path is analyzed---these two options may be helpful if there is too much overhead of computing the entire SORs.] SideEffects [Nothing related to the network is changed: if the default partition and mdd manager are available, they will be left intact; if they are not available, the incrementally created new partition and mdd manager will be freed before exit.] ******************************************************************************/ void Grab_NetworkCheckInvariants( Ntk_Network_t *network, array_t *InvariantFormulaArray, char *refineAlgorithm, int fineGrainFlag, int refineMinFlag, int useArdcFlag, int cexType, int verbosity, int dbgLevel, int printInputs, FILE *debugFile, int useMore, char *driverName) { mdd_manager *mddManager = NIL(mdd_manager); graph_t *partition; Ctlp_Formula_t *invFormula; Ctlsp_Formula_t *invFormula_sp; array_t *invStatesArray; array_t *resultArray; st_table *absLatchTable, *absBnvTable; st_table *coiLatchTable, *coiBnvTable; Fsm_Fsm_t *absFsm; array_t *visibleVarMddIds, *invisibleVarMddIds; int concreteLatchCount, abstractLatchCount; int concreteBnvCount, abstractBnvCount; st_table *nodeToFaninNumberTable; mdd_t *rchStates, *invStates = NIL(mdd_t); /*=mdd_one(mddManager);*/ array_t *SORs, *save_SORs; boolean refineDirection, runMinimization, isLastStep; int staticOrderFlag, partitionFlag; int cexLength, refineIteration; array_t *addedVarsAtCurrentLevel = NIL(array_t); array_t *addedBnvsAtCurrentLevel = NIL(array_t); int auxValue1, auxValue2, flag, i; long startTime, endTime, totalTime; long mcStartTime, mcEndTime, mcTime; long sorEndTime, sorTime; long conEndTime, conTime; long dirStartTime, dirEndTime, dirTime; long refStartTime, refEndTime, refTime; long miniStartTime, miniEndTime, miniTime; if ( strcmp(refineAlgorithm, "GRAB") ) { fprintf(vis_stdout, "** ci error: Abstraction refinement method %s not available\n", refineAlgorithm); return; } /* if the mddIds haven't been assigned to the network nodes, * we assign them incrementally (i.e., staticOrderFlag==1). */ mddManager = Ntk_NetworkReadMddManager(network); if (mddManager == NIL(mdd_manager)) staticOrderFlag = 1; else staticOrderFlag = 0; if (staticOrderFlag) { GrabNtkClearAllMddIds(network); mddManager = Ntk_NetworkInitializeMddManager(network); if (verbosity >= 2) bdd_dynamic_reordering(mddManager, BDD_REORDER_SIFT, BDD_REORDER_VERBOSITY); else bdd_dynamic_reordering(mddManager, BDD_REORDER_SIFT, BDD_REORDER_NO_VERBOSITY); } /* if the partition hasn't been created, we create the partition * incrementally (i.e., partitionFlag==1) */ partition = Part_NetworkReadPartition(network); if (partition == NIL(graph_t)) partitionFlag = GRAB_PARTITION_BUILD; else partitionFlag = GRAB_PARTITION_NOCHANGE; /* used by the refinement algorithm as a tie-breaker */ nodeToFaninNumberTable = st_init_table(st_ptrcmp, st_ptrhash); /*************************************************************************** * check the invariants ***************************************************************************/ resultArray = array_alloc(int, array_n(InvariantFormulaArray)); arrayForEachItem(Ctlp_Formula_t *, InvariantFormulaArray, i, invFormula) { invFormula_sp = Ctlsp_CtlFormulaToCtlsp(invFormula); /* this is required for the following code to function correctly */ visibleVarMddIds = invisibleVarMddIds = NIL(array_t); invStatesArray = SORs = save_SORs = NIL(array_t); mcTime = sorTime = conTime = dirTime = refTime = miniTime = 0; startTime = util_cpu_ctime(); /* record the number of latches in the cone-of-influence */ coiLatchTable = GrabComputeCOIAbstraction(network, invFormula); concreteLatchCount = st_count(coiLatchTable); /* build the initial abstract model */ absLatchTable = GrabComputeInitialAbstraction(network, invFormula); abstractLatchCount = st_count(absLatchTable); if (verbosity >= 3) { GrabPrintNodeHashTable("InitialAbstractLatches", absLatchTable); } /* initialize the abs./concrete table for boolean network variables*/ coiBnvTable = st_init_table(st_ptrcmp, st_ptrhash); abstractBnvCount = concreteBnvCount = 0; if (fineGrainFlag == 1) { absBnvTable = st_init_table(st_ptrcmp, st_ptrhash); }else { absBnvTable = NIL(st_table); } /* if the concrete partition is available, retrieve form it the * bnvs; otherwise, we incrementally create bnvs (for the current * absLatches only)---this is designed for performance concerns */ if (partitionFlag == GRAB_PARTITION_NOCHANGE) { Part_PartitionReadOrCreateBnvs(network, coiLatchTable, coiBnvTable); concreteBnvCount = st_count(coiBnvTable); } /* Outer Loop---Over Refinements For Different SOR Lengths */ refineIteration = 0; isLastStep = 0; while(1) { long grabStartTime = util_cpu_ctime(); /* Build the Abstract Finite State Machine */ absFsm = GrabCreateAbstractFsm(network, coiBnvTable, absLatchTable, absBnvTable, partitionFlag, TRUE); concreteBnvCount = st_count(coiBnvTable); invisibleVarMddIds = GrabGetInvisibleVarMddIds(absFsm, absLatchTable, absBnvTable); visibleVarMddIds = GrabGetVisibleVarMddIds(absFsm, absLatchTable); /* sanity check */ isLastStep = (array_n(invisibleVarMddIds)==0); if (isLastStep) { assert(abstractLatchCount == concreteLatchCount); } /* Compute The Invariant States If They Are Not Available */ if (invStatesArray == NIL(array_t)) { mdd_t * tautology = mdd_one(mddManager); array_t *careSetArray = array_alloc(mdd_t *, 0); array_insert(mdd_t *, careSetArray, 0, tautology); invStates = Mc_FsmEvaluateFormula(absFsm, invFormula, tautology, NIL(Fsm_Fairness_t), careSetArray, MC_NO_EARLY_TERMINATION, NIL(Fsm_HintsArray_t), Mc_None_c, McVerbosityNone_c, McDcLevelNone_c, 0, McGSH_EL_c); mdd_array_free(careSetArray); invStatesArray = array_alloc(mdd_t *, 0); array_insert(mdd_t *, invStatesArray, 0, invStates); } /* Conduct Forward Reachability Analysis */ rchStates = GrabFsmComputeReachableStates(absFsm, absLatchTable, absBnvTable, invStatesArray, verbosity); mcEndTime = util_cpu_ctime(); mcTime += (mcEndTime - grabStartTime); if (verbosity >= 1) { fprintf(vis_stdout, "-- grab: absLatch [%d/%d], absBnv [%d/%d], mc time is %5g s\n", abstractLatchCount, concreteLatchCount, abstractBnvCount, concreteBnvCount, (double)(mcEndTime-grabStartTime)/1000.0); } /* if bad states cannot be reached, the property is true; * if absFsm is concrete, the property is false */ flag = mdd_lequal(rchStates, invStates, 1, 1); mdd_free(rchStates); if (flag || isLastStep) { /* set the debugging info, if necessary */ if (!flag) SORs = mdd_array_duplicate(Fsm_FsmReadReachabilityOnionRings(absFsm)); Fsm_FsmSubsystemFree(absFsm); absFsm = NIL(Fsm_Fsm_t); array_free(invisibleVarMddIds); array_free(visibleVarMddIds); break; } /* Build The Synchronous Onion Rings (SORs) */ Fsm_FsmFreeImageInfo(absFsm); SORs = GrabFsmComputeSynchronousOnionRings(absFsm, absLatchTable, absBnvTable, NIL(array_t), invStates, cexType, verbosity); sorEndTime = util_cpu_ctime(); sorTime += (sorEndTime - mcEndTime); /* Concretize Multiple Counter-Examples */ cexLength = array_n(SORs)-1; flag = !Bmc_AbstractCheckAbstractTraces(network, SORs, coiLatchTable, 0, dbgLevel, printInputs); conEndTime = util_cpu_ctime(); conTime += (conEndTime - sorEndTime); if (!flag) { if (verbosity >= 1) fprintf(vis_stdout, "-- grab: find length-%d concrete counter-examples\n", cexLength); Fsm_FsmSubsystemFree(absFsm); absFsm = NIL(Fsm_Fsm_t); array_free(invisibleVarMddIds); array_free(visibleVarMddIds); break; }else { if (verbosity >= 2) fprintf(vis_stdout, "-- grab: find length-%d spurious counter-examples\n", cexLength); } /* Innor Loop---Over Refinements For The Same SOR Length */ save_SORs = mdd_array_duplicate(SORs); addedVarsAtCurrentLevel = array_alloc(int, 0); addedBnvsAtCurrentLevel = array_alloc(int, 0); refineDirection = 1; runMinimization = 0; while (1) { int skip_refinement = 0; /* Get the appropriate refinement direction: * runMinimization==1 --> BOOLEAN * fineGrainFlag==0 --> SEQUENTIAL * coiBnvTable is empty --> SEQUENTIAL * refineDirection==0 --> BOOLEAN */ if ( !runMinimization && refineDirection) { if ( fineGrainFlag && st_count(coiBnvTable)>0 ) { dirStartTime = util_cpu_ctime(); #if 0 refineDirection = !GrabTestRefinementSetSufficient(network, save_SORs, absLatchTable, verbosity); #endif runMinimization = (refineDirection==0); dirEndTime = util_cpu_ctime(); dirTime += (dirEndTime - dirStartTime); } } if (verbosity >= 3 && refineDirection==0) fprintf(vis_stdout, "refinement is in %s direction\n", (refineDirection? "both":"boolean")); /* Minimize the refinement set of latches */ if (runMinimization) { int n_latches = st_count(absLatchTable); int break_flag; if (refineMinFlag && array_n(addedVarsAtCurrentLevel) > 1) { miniStartTime = util_cpu_ctime(); GrabMinimizeLatchRefinementSet(network, &absLatchTable, &absBnvTable, addedVarsAtCurrentLevel, &addedBnvsAtCurrentLevel, save_SORs, verbosity); abstractLatchCount = st_count(absLatchTable); abstractBnvCount = absBnvTable? st_count(absBnvTable):st_count(coiBnvTable); array_free(addedVarsAtCurrentLevel); addedVarsAtCurrentLevel = array_alloc(int, 0); miniEndTime = util_cpu_ctime(); miniTime += (miniEndTime - miniStartTime); } /* if the refinement set of bnvs is also sufficient, break */ break_flag = 1; if (fineGrainFlag && st_count(coiBnvTable)>0) { dirStartTime = util_cpu_ctime(); break_flag = GrabTestRefinementBnvSetSufficient(network, coiBnvTable, save_SORs, absLatchTable, absBnvTable, verbosity); dirEndTime = util_cpu_ctime(); dirTime += (dirEndTime - dirStartTime); } if (break_flag) { if (verbosity >= 1) fprintf(vis_stdout, "-- grab: remove length-%d spurious counter-examples\n\n", cexLength); break; } /* Otherwise, skip this refinement step, because the * current absFsm is not well-defined (some latches have * been droped) */ SORs = mdd_array_duplicate(save_SORs); if (n_latches > st_count(absLatchTable)) skip_refinement = 1; refineDirection = 0; runMinimization = 0; } /* compute the refinement (by Grab) */ if (!skip_refinement) { array_t *addedVars = array_alloc(int, 0); array_t *addedBnvs = array_alloc(int, 0); auxValue1 = st_count(absLatchTable) + ((absBnvTable==NIL(st_table))? 0:st_count(absBnvTable)); refStartTime = util_cpu_ctime(); /* create the abstract fsm */ Fsm_FsmSubsystemFree(absFsm); absFsm = GrabCreateAbstractFsm(network, coiBnvTable, absLatchTable, absBnvTable, GRAB_PARTITION_NOCHANGE, FALSE); /* pick refinement variables */ GrabRefineAbstractionByGrab(absFsm, SORs, absLatchTable, absBnvTable, addedVars, addedBnvs, refineDirection, nodeToFaninNumberTable, verbosity); array_append(addedVarsAtCurrentLevel, addedVars); array_append(addedBnvsAtCurrentLevel, addedBnvs); array_free(addedVars); array_free(addedBnvs); /* Sanity check! */ auxValue2 = st_count(absLatchTable) + ((absBnvTable==NIL(st_table))? 0:st_count(absBnvTable)); assert(auxValue1 < auxValue2); abstractLatchCount = st_count(absLatchTable); abstractBnvCount = absBnvTable? st_count(absBnvTable):st_count(coiBnvTable); refEndTime = util_cpu_ctime(); refTime += (refEndTime - refStartTime); if (verbosity >= 3) { fprintf(vis_stdout, "-- grab: absLatch [%d/%d], absBnv [%d/%d], ref time is %5g s\n", abstractLatchCount, concreteLatchCount, abstractBnvCount, concreteBnvCount, (double)(refEndTime - refStartTime)/1000.0); } refineIteration++; } /* Create The Refined Abstract FSM */ Fsm_FsmSubsystemFree(absFsm); array_free(invisibleVarMddIds); array_free(visibleVarMddIds); absFsm = GrabCreateAbstractFsm(network, coiBnvTable, absLatchTable, absBnvTable, partitionFlag, TRUE); invisibleVarMddIds = GrabGetInvisibleVarMddIds(absFsm, absLatchTable, absBnvTable); visibleVarMddIds = GrabGetVisibleVarMddIds(absFsm, absLatchTable); concreteBnvCount = st_count(coiBnvTable); /* sanity check */ isLastStep = (array_n(invisibleVarMddIds)==0); if (isLastStep) { assert(abstractLatchCount == concreteLatchCount); } /* Reduce The Current SORs (with forward reachability analysis) */ mcStartTime = util_cpu_ctime(); rchStates = GrabFsmComputeConstrainedReachableStates(absFsm, absLatchTable, absBnvTable, SORs, verbosity); mdd_array_free(SORs); SORs = NIL(array_t); mcEndTime = util_cpu_ctime(); mcTime += (mcEndTime - mcStartTime); if (verbosity >= 2) { fprintf(vis_stdout, "-- grab: absLatch [%d/%d], absBnv [%d/%d], mc time is %5g s\n", abstractLatchCount, concreteLatchCount, abstractBnvCount, concreteBnvCount, (double)(mcEndTime-mcStartTime)/1000.0); } /* if bad states is no longer reachable, break out */ flag = mdd_lequal(rchStates, invStates, 1, 1); mdd_free(rchStates); if (isLastStep || flag) { if (!isLastStep && refineDirection == 1) { runMinimization = 1; refineDirection = 0; continue; }else break; } /* Build the new SORs (with backward reachability analysis) */ Fsm_FsmFreeImageInfo(absFsm); SORs = GrabFsmComputeSynchronousOnionRings(absFsm, absLatchTable, absBnvTable, NIL(array_t), invStates, cexType, verbosity); sorEndTime = util_cpu_ctime(); sorTime += (sorEndTime - mcEndTime); } /* End of the Inner Loop */ /* Minimize The Refinement Set of Boolean Network Variables (BNVs) */ if (fineGrainFlag==1 && refineMinFlag && array_n(addedBnvsAtCurrentLevel)>1) { miniStartTime = util_cpu_ctime(); GrabMinimizeBnvRefinementSet(network, coiBnvTable, absLatchTable, &absBnvTable, addedBnvsAtCurrentLevel, save_SORs, verbosity); abstractLatchCount = st_count(absLatchTable); abstractBnvCount = st_count(absBnvTable); miniEndTime = util_cpu_ctime(); miniTime += (miniEndTime - miniStartTime); } mdd_array_free(save_SORs); /* Clean-ups */ Fsm_FsmSubsystemFree(absFsm); absFsm = NIL(Fsm_Fsm_t); array_free(invisibleVarMddIds); array_free(visibleVarMddIds); array_free(addedVarsAtCurrentLevel); array_free(addedBnvsAtCurrentLevel); addedVarsAtCurrentLevel = NIL(array_t); addedBnvsAtCurrentLevel = NIL(array_t); } /* End of the Outer Loop */ endTime = util_cpu_ctime(); totalTime = endTime - startTime; /* Print out the debugging information */ if (dbgLevel > 0) { FILE *tmpFile = vis_stdout; extern FILE *vis_stdpipe; if (debugFile) vis_stdpipe = debugFile; else if (useMore) vis_stdpipe = popen("more", "w"); else vis_stdpipe = vis_stdout; vis_stdout = vis_stdpipe; if (flag) { fprintf(vis_stdout, "# %s: formula passed --- ", driverName); Ctlp_FormulaPrint(vis_stdout, invFormula); fprintf(vis_stdout, "\n"); }else { if(dbgLevel != 2) { fprintf(vis_stdout, "# %s: formula p%d failed --- ", driverName, i+1); Ctlp_FormulaPrint(vis_stdout, invFormula); fprintf(vis_stdout, "\n# %s: calling debugger\n", driverName); } flag = !Bmc_AbstractCheckAbstractTraces(network, SORs, coiLatchTable, 1, dbgLevel, printInputs); } if (vis_stdout != tmpFile && vis_stdout != debugFile) (void)pclose(vis_stdpipe); vis_stdout = tmpFile; } if (verbosity >= 2 ) { fprintf(vis_stdout, "\n-- grab: total cpu time = %5g\n", (double)totalTime/1000.0); if (verbosity >= 3) { fprintf(vis_stdout, "-- grab: mc time = %5.1f\t(%3.1f%%)\n", (double)mcTime/1000.0, (100.0*mcTime/totalTime)); fprintf(vis_stdout, "-- grab: sor time = %5.1f\t(%3.1f%%)\n", (double)sorTime/1000.0, (100.0*sorTime/totalTime)); fprintf(vis_stdout, "-- grab: con time = %5.1f\t(%3.1f%%)\n", (double)conTime/1000.0, (100.0*conTime/totalTime)); fprintf(vis_stdout, "-- grab: ref time = %5.1f\t(%3.1f%%)\n", (double)refTime/1000.0, (100.0*refTime/totalTime)); fprintf(vis_stdout, "-- grab: min time = %5.1f\t(%3.1f%%)\n", (double)miniTime/1000.0,(100.0*miniTime/totalTime)); fprintf(vis_stdout, "-- grab: dir time = %5.1f\t(%3.1f%%)\n", (double)dirTime/1000.0, (100.0*dirTime/totalTime)); } } if (verbosity >= 1) { if (concreteLatchCount > 0) { fprintf(vis_stdout, "-- grab: abs latch percentage = %d %%\n", 100 * abstractLatchCount/concreteLatchCount ); } if (verbosity >= 3) { fprintf(vis_stdout, "-- grab: abs latch = %d\n", abstractLatchCount); fprintf(vis_stdout, "-- grab: coi latch = %d\n", concreteLatchCount); } if (concreteBnvCount > 0) { fprintf(vis_stdout, "-- grab: abs bnv percentage = %d %%\n", (100 * abstractBnvCount/concreteBnvCount) ); if (verbosity >= 3) { fprintf(vis_stdout, "-- grab: abs bnv = %d\n", abstractBnvCount); fprintf(vis_stdout, "-- grab: coi bnv = %d\n", concreteBnvCount); } abstractBnvCount += abstractLatchCount; concreteBnvCount += concreteLatchCount; fprintf(vis_stdout, "-- grab: total abs var percentage = %d %%\n", (100 * abstractBnvCount/concreteBnvCount) ); if (verbosity >= 3) { fprintf(vis_stdout, "-- grab: abs var = %d\n", abstractBnvCount); fprintf(vis_stdout, "-- grab: coi var = %d\n", concreteBnvCount); } } fprintf(vis_stdout, "-- grab: total refinement iterations = %d\n", refineIteration); fprintf(vis_stdout, "-- grab: total image computations %d\n", Img_GetNumberOfImageComputation(Img_Forward_c)); fprintf(vis_stdout, "-- grab: total preimage computations %d\n", Img_GetNumberOfImageComputation(Img_Backward_c)); if (verbosity >= 3) { GrabPrintNodeHashTable("AbstractLatchRankings", absLatchTable); if (fineGrainFlag) GrabPrintNodeHashTable("AbstractBnvRankings", absBnvTable); } } /* Clean-up's */ st_free_table(coiLatchTable); st_free_table(absLatchTable); st_free_table(coiBnvTable); if (fineGrainFlag) { st_free_table(absBnvTable); } mdd_array_free(invStatesArray); if (!flag) mdd_array_free(SORs); Ctlsp_FormulaFree(invFormula_sp); /* Store the verification results in an array (1--passed, 0--failed) */ array_insert(int, resultArray, i, flag); } /* print whether the set of invariants passed or failed */ fprintf(vis_stdout, "\n# %s: Summary of invariant pass/fail\n", driverName); arrayForEachItem(Ctlp_Formula_t *, InvariantFormulaArray, i, invFormula) { flag = array_fetch(int, resultArray, i); if (flag) { (void) fprintf(vis_stdout, "# %s: formula passed --- ", driverName); Ctlp_FormulaPrint(vis_stdout, (invFormula)); fprintf(vis_stdout, "\n"); } else { (void) fprintf(vis_stdout, "# %s: formula failed --- ", driverName); Ctlp_FormulaPrint(vis_stdout, (invFormula)); fprintf(vis_stdout, "\n"); } } /* free the current partition and mdd manager if necessary */ if (partitionFlag) { Ntk_NetworkFreeApplInfo(network, PART_NETWORK_APPL_KEY); } if (staticOrderFlag) { mdd_quit(mddManager); Ntk_NetworkSetMddManager(network, NIL(mdd_manager)); GrabNtkClearAllMddIds(network); } st_free_table(nodeToFaninNumberTable); array_free(resultArray); } /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Implements the test command for Grab.] CommandName [_grab_test] CommandSynopsis [Performs invairant checking on a flattened network with the GRAB abstraction refinement algorithm.] CommandArguments [ \[-a <refine_algorithm>\] \[-c <cex_type>\] \[-d <dbg_level>\] \[-F\] \[-M\] \[-i\] \[-m\] \[-t <time_out_period>\] \[-v <verbosity_level>\] \[-f <dbg_file>\] \[-h\] <inv_file>] CommandDescription [Performs invairant checking on a flattened network with the GRAB abstraction refinement algorithm. Before calling this command, the user should have created the flattened netowrk by calling the commands flatten_hierarchy and build_partition_maigs. The default BDD manager and network partition are not mandatory for calling this command, though they will be used if available. (In other words, the user doesn't have to run the commands static_order and build_partition_mdds before calling this command.) Regardless of the options, no 'false positive' or 'false negatives' will occurs: the result is correct for the given model. Properties to be verified should be provided as invariant formulae in the file inv_file. Node that the support of any wire referred to in a formula should consist only of latches. For the precise syntax of CTL and LTL formulas, see the VIS CTL and LTL syntax manual.

If a formula does not pass, a proof of failure (referred to as a counter-example) is demonstrated. Whether demostrate the proof or not can be specified (see option -d).

Command options:

-a <refine_algorithm>
Specify the refinement variable selection algorithm.

refine_algorithm must be one of the following:

GRAB: the GRAB refinement method (Default).

-c <cex_type>
Specify the type of abstract counter-examples used in the analysis.

cex_type must be one of the following:

0: minterm state counter-example.

1: cube state counter-example.

2: synchronous onion rings (Default).

-d <dbg_level>
Specify whether to demonstrate a counter-example when the system fails a formula being checked.

dbg_level must be one of the following:

0: No debugging performed. dbg_level=0 is the default.

1: Generate a counter-example (a path to a fair cycle).

-F <finegrain_flag>
Enable or disable the use of fine-grain abstraction.

finegrain_flag must be one of the following:

0: disable fine-grain abstraction.

1: enable fine-grain abstraction (Default).

-M <refinemin_flag>
Enable or disable the use of greedy refinement minimization.

refinemin_flag must be one of the following:

0: disable greedy refinement minimization.

1: enable greedy refinement minimization (Default).

-i
Print input values causing transitions between states during debugging. Both primary and pseudo inputs are printed.

-m
Pipe debugger output through the UNIX utility more.

-t <timeOutPeriod>
Specify the time out period (in seconds) after which the command aborts. By default this option is set to infinity.

-v <verbosity_level>
Specify verbosity level. This sets the amount of feedback on CPU usage and code status.
verbosity_level must be one of the following:

0: No feedback provided. This is the default.

1: Feedback on code location.

2: Feedback on code location and CPU usage.

-f <dbg_out>
Specify the name of the file ot which error trace is written.

-h
Print the command usage.

See also commands : model_check, check_invariant ] SideEffects [] ******************************************************************************/ static int CommandGrab( Hrc_Manager_t ** hmgr, int argc, char ** argv) { int c, verbosity; char InvFileName[256]; FILE *FP, *dbgFile; array_t *InvariantFormulaArray; Ntk_Network_t *network; static int timeOutPeriod = 0; char refineAlgorithm[256]; int cexType = 0; int refineMinFlag; int fineGrainFlag; int useArdcFlag = 0; long startTime, endTime; char *dbgFileName = NIL(char); int dbgLevel, printInputs, useMore; startTime = util_cpu_ctime(); Img_ResetNumberOfImageComputation(Img_Both_c); /* the default setting is Grab+, * Generational Refinement of Ariadne's Bundle of SORs */ strcpy(refineAlgorithm, "GRAB"); cexType = GRAB_CEX_SOR; fineGrainFlag = 1; refineMinFlag = 1; verbosity = 0; dbgLevel = 0; printInputs = 0; useMore = 0; /* * Parse command line options. */ util_getopt_reset(); while ((c = util_getopt(argc, argv, "a:c:d:F:M:imt:v:f:h")) != EOF) { switch(c) { case 'a': strcpy(refineAlgorithm, util_optarg); break; case 'F': fineGrainFlag = atoi(util_optarg); break; case 'M': refineMinFlag = atoi(util_optarg); break; case 'c': cexType = atoi(util_optarg); break; case 'D': useArdcFlag = 1; break; case 't': timeOutPeriod = atoi(util_optarg); break; case 'v': verbosity = atoi(util_optarg); break; case 'd': dbgLevel = atoi(util_optarg); break; case 'i': printInputs = 1; break; case 'm': useMore = 1; break; case 'f': dbgFileName = util_strsav(util_optarg); break; case 'h': goto usage; default: goto usage; } } if (strcmp(refineAlgorithm, "GRAB")) { fprintf(vis_stdout, "\nunknown refinement algorithm: %s\n", refineAlgorithm); goto usage; } /* Make sure the flattened network is available */ network = Ntk_HrcManagerReadCurrentNetwork(*hmgr); if (network == NIL(Ntk_Network_t)) { fprintf(vis_stdout, "%s\n", error_string()); error_init(); return 1; } /* Make sure the AIG graph is available */ if (Ntk_NetworkReadMAigManager(network) == NIL(mAig_Manager_t)) { fprintf(vis_stderr, "** grab error: please run buid_partiton_maigs first\n"); return 1; } /* Open the InvFile. (It must contain a single invariant property) */ if (argc - util_optind == 0) { (void) fprintf(vis_stderr, "** grab error: file containing inv formula not provided\n"); goto usage; }else if (argc - util_optind > 1) { (void) fprintf(vis_stderr, "** grab error: too many arguments\n"); goto usage; } strcpy(InvFileName, argv[util_optind]); /* Parsing the InvFile */ FP = Cmd_FileOpen(InvFileName, "r", NIL(char *), 0); if (FP == NIL(FILE)) { (void) fprintf(vis_stdout, "** grab error: error in opening file %s\n", InvFileName); return 1; } InvariantFormulaArray = Ctlp_FileParseFormulaArray(FP); fclose(FP); if (InvariantFormulaArray == NIL(array_t)) { (void) fprintf(vis_stdout, "** grab error: error in parsing formulas from file %s\n", InvFileName); return 1; } if (dbgFileName != NIL(char)) dbgFile = Cmd_FileOpen(dbgFileName, "r", NIL(char *), 0); else dbgFile = NIL(FILE); /* Set time out processing (if timeOutPeriod is set) */ if (timeOutPeriod > 0) { (void) signal(SIGALRM, (void(*)(int))TimeOutHandle); (void) alarm(timeOutPeriod); if (setjmp(timeOutEnv) > 0) { fprintf(vis_stdout, "\n# GRAB: abstract-refine - timeout occurred after %d seconds.\n", timeOutPeriod); (void) fprintf(vis_stdout, "# GRAB: data may be corrupted.\n"); endTime = util_cpu_ctime(); fprintf(vis_stdout, "# GRAB: elapsed time is %5.1f.\n", (double)(endTime - startTime)/1000.0); if (verbosity) { fprintf(vis_stdout, "-- total %d image computations and %d preimage computations\n", Img_GetNumberOfImageComputation(Img_Forward_c), Img_GetNumberOfImageComputation(Img_Backward_c)); } alarm(0); return 1; } } /* Check invariants with the abstraction refinement algorithm GRAB */ Grab_NetworkCheckInvariants(network, InvariantFormulaArray, refineAlgorithm, fineGrainFlag, refineMinFlag, useArdcFlag, cexType, verbosity, dbgLevel, printInputs, dbgFile, useMore, "GRAB" ); /* Total cost */ if (verbosity >= 2) { endTime = util_cpu_ctime(); fprintf(vis_stdout, "# GRAB: elapsed time is %5.1f.\n", (double)(endTime - startTime)/1000.0); fprintf(vis_stdout, "-- total %d image computations and %d preimage computations\n", Img_GetNumberOfImageComputation(Img_Forward_c), Img_GetNumberOfImageComputation(Img_Backward_c)); } alarm(0); return 0; /* normal exit */ usage: (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] \n"); (void) fprintf(vis_stderr, " -a \n"); (void) fprintf(vis_stderr, " refine_algorithm = GRAB => the GRAB refinement method (Default)\n"); (void) fprintf(vis_stderr, " -c \n"); (void) fprintf(vis_stderr, " cex_type = 0 => minterm state counter-example\n"); (void) fprintf(vis_stderr, " cex_type = 1 => cube state counter-example\n"); (void) fprintf(vis_stderr, " cex_type = 2 => synchronous onion rings (Default)\n"); (void) fprintf(vis_stderr, " -d \n"); (void) fprintf(vis_stderr, " debug_level = 0 => no debugging (Default)\n"); (void) fprintf(vis_stderr, " debug_level = 1 => print path to state failing invariant\n"); (void) fprintf(vis_stderr, " -F \n"); (void) fprintf(vis_stderr, " finegrain_flag = 0 => disable fine-grain abstraction\n"); (void) fprintf(vis_stderr, " finegrain_flag = 1 => enable fine-grain abstraction (Default)\n"); (void) fprintf(vis_stderr, " -M \n"); (void) fprintf(vis_stderr, " refinemin_flag = 0 => disable greedy refinement minimization\n"); (void) fprintf(vis_stderr, " refinemin_flag = 1 => enable greedy refinement minimization (Default)\n"); (void) fprintf(vis_stderr, " -i \tPrint input values in debug traces.\n"); (void) fprintf(vis_stderr, " -m pipe debugger output through UNIX utility more\n"); (void) fprintf(vis_stderr, " -t Time out period.\n"); (void) fprintf(vis_stderr, " -v \n"); (void) fprintf(vis_stderr, " verbosity_level = 0 => no feedback (Default)\n"); (void) fprintf(vis_stderr, " verbosity_level = 1 => code status\n"); (void) fprintf(vis_stderr, " verbosity_level = 2 => code status and CPU usage profile\n"); (void) fprintf(vis_stderr, " -f \n"); (void) fprintf(vis_stderr, " write error trace to dbg_out\n"); (void) fprintf(vis_stderr, " The input file containing invariants to be checked.\n"); (void) fprintf(vis_stderr, " -h\t\t print the command usage\n"); return 1; /* error exit */ } /**Function******************************************************************** Synopsis [Handle function for timeout.] Description [This function is called when the process receives a signal of type alarm. Since alarm is set with elapsed time, this function checks if the CPU time corresponds to the timeout of the command. If not, it reprograms the alarm to fire later and check if the CPU limit has been reached.] SideEffects [] ******************************************************************************/ static void TimeOutHandle(void) { longjmp(timeOutEnv, 1); }