/**CFile*********************************************************************** FileName [absInternal.c] PackageName [abs] Synopsis [Miscelaneous functions to handle caches, don't care conditions, initialization and deallocation of structures, etc] Author [Abelardo Pardo ] Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.] ******************************************************************************/ #include "absInt.h" static char rcsid[] UNUSED = "$Id: absInternal.c,v 1.30 2005/04/16 04:22:21 fabio Exp $"; /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ static int vertexCounter = 0; /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static mdd_t * ComputeEGtrue(Abs_VerificationInfo_t *absInfo, mdd_t *careStates); static void SelectIdentifierVertices(AbsVertexInfo_t *vertexPtr, array_t *result, st_table *visited); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Fill the fields of the data structure storing the information required for the verification process] SideEffects [] ******************************************************************************/ Abs_VerificationInfo_t * Abs_VerificationComputeInfo( Ntk_Network_t *network) { Abs_VerificationInfo_t *absInfo; Ntk_Node_t *nodePtr; graph_t *partition; mdd_manager *mddManager; st_table *table; lsGen lsgen; /* Create the data structure to store all the needed info */ absInfo = AbsVerificationInfoInitialize(); /* Fill the data structure in */ AbsVerificationInfoSetNetwork(absInfo, network); partition = Part_NetworkReadPartition(network); AbsVerificationInfoSetPartition(absInfo, partition); mddManager = Part_PartitionReadMddManager(partition); AbsVerificationInfoSetMddManager(absInfo, mddManager); /* Compute the state variable pairs */ table = st_init_table(st_numcmp, st_numhash); Ntk_NetworkForEachLatch(network, lsgen, nodePtr) { Ntk_Node_t *latchInputPtr; int mddId, mddId2; mddId = Ntk_NodeReadMddId(nodePtr); latchInputPtr = Ntk_NodeReadShadow(nodePtr); mddId2 = Ntk_NodeReadMddId(latchInputPtr); st_insert(table, (char *)(long)mddId, (char *)(long)mddId2); } AbsVerificationInfoSetStateVars(absInfo, table); /* Compute the quantify variables */ table = st_init_table(st_numcmp, st_numhash); Ntk_NetworkForEachInput(network, lsgen, nodePtr) { int mddId; mddId = Ntk_NodeReadMddId(nodePtr); st_insert(table, (char *)(long)mddId, NIL(char)); } AbsVerificationInfoSetQuantifyVars(absInfo, table); /* Initalize the catalog to detect common expressions */ AbsVerificationInfoSetCatalog(absInfo, AbsVertexCatalogInitialize()); return absInfo; } /* End of Abs_VerificationComputeInfo */ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Create a new structure of type VertexInfo and initialize all its fields.] SideEffects [] SeeAlso [AbsVertexInfo_t] ******************************************************************************/ AbsVertexInfo_t * AbsVertexInitialize(void) { AbsVertexInfo_t *result; result = ALLOC(AbsVertexInfo_t, 1); AbsVertexSetType(result, false_c); AbsVertexSetId(result, vertexCounter++); AbsVertexSetSat(result, NIL(mdd_t)); AbsVertexSetRefs(result, 1); AbsVertexSetServed(result, 0); AbsVertexSetPolarity(result, FALSE); AbsVertexSetDepth(result, -1); AbsVertexSetLocalApprox(result, FALSE); AbsVertexSetGlobalApprox(result, FALSE); AbsVertexSetConstant(result, FALSE); AbsVertexSetTrueRefine(result, FALSE); AbsVertexSetLeftKid(result, NIL(AbsVertexInfo_t)); AbsVertexSetRightKid(result, NIL(AbsVertexInfo_t)); result->parent = lsCreate(); /* Not all of these need to be initialized, but to be sure... */ AbsVertexSetSolutions(result, NIL(st_table)); AbsVertexSetVarId(result, 0); AbsVertexSetFpVar(result, NIL(AbsVertexInfo_t)); AbsVertexSetVarId(result, 0); AbsVertexSetGoalSet(result, NIL(mdd_t)); AbsVertexSetRings(result, NIL(array_t)); AbsVertexSetRingApprox(result, NIL(array_t)); AbsVertexSetSubApprox(result, NIL(array_t)); AbsVertexSetUseExtraCareSet(result, FALSE); AbsVertexSetName(result, NIL(char)); AbsVertexSetValue(result, NIL(char)); return result; } /* End of AbsVertexInitialize */ /**Function******************************************************************** Synopsis [Free a structure of type AbsVertexInfo.] Description [optional] SideEffects [] SeeAlso [AbsVertexInfo_t] ******************************************************************************/ void AbsVertexFree( AbsVertexCatalog_t *catalog, AbsVertexInfo_t *v, AbsVertexInfo_t *fromVertex) { /* Decrement the number of references */ AbsVertexReadRefs(v)--; /* Remove the pointer from its parent to itself */ if (fromVertex != NIL(AbsVertexInfo_t)) { AbsVertexInfo_t *result; lsGen listGen; lsHandle item, toDelete; lsGeneric userData; listGen = lsStart(AbsVertexReadParent(v)); toDelete = (lsHandle) 0; while(toDelete == (lsHandle) 0 && lsNext(listGen, &result, &item) == LS_OK) { if (result == fromVertex) { toDelete = item; } } lsFinish(listGen); if (toDelete != (lsHandle)0) { lsRemoveItem(toDelete, &userData); } } /* If it is not the last reference we are done */ if (AbsVertexReadRefs(v) != 0) { return; } /* Vertices that need recursion over the leftKid */ if (AbsVertexReadType(v) == fixedPoint_c || AbsVertexReadType(v) == and_c || AbsVertexReadType(v) == xor_c || AbsVertexReadType(v) == xnor_c || AbsVertexReadType(v) == not_c || AbsVertexReadType(v) == preImage_c) { AbsVertexFree(catalog, AbsVertexReadLeftKid(v), v); } /* Vertices that need recursion over the rightKid */ if (AbsVertexReadType(v) == and_c || AbsVertexReadType(v) == xor_c || AbsVertexReadType(v) == xnor_c) { AbsVertexFree(catalog, AbsVertexReadRightKid(v), v); } /* Remove the vertex from the catalog */ AbsCatalogDelete(catalog, v); /* The variable vertex does not reference the sat set */ if (AbsVertexReadType(v) != variable_c && AbsVertexReadSat(v) != NIL(mdd_t)) { mdd_free(AbsVertexReadSat(v)); } if (AbsVertexReadType(v) == variable_c && AbsVertexReadGoalSet(v) != NIL(mdd_t)) { mdd_free(AbsVertexReadGoalSet(v)); } lsDestroy(AbsVertexReadParent(v), (void (*)(lsGeneric))0); /* Free the union fields depending on the type of vertex */ if (AbsVertexReadType(v) == preImage_c) { if (AbsVertexReadSolutions(v) != NIL(st_table)) { AbsEvalCacheEntry_t *value; bdd_node *key; st_generator *stgen; st_foreach_item(AbsVertexReadSolutions(v), stgen, &key, &value) { AbsCacheEntryFree(value); } st_free_table(AbsVertexReadSolutions(v)); } } else if (AbsVertexReadType(v) == fixedPoint_c) { if (AbsVertexReadRings(v) != NIL(array_t)) { mdd_t *unit; int i; arrayForEachItem(mdd_t *, AbsVertexReadRings(v), i, unit) { mdd_free(unit); } array_free(AbsVertexReadRings(v)); } if (AbsVertexReadRingApprox(v) != NIL(array_t)) { array_free(AbsVertexReadRingApprox(v)); } if (AbsVertexReadSubApprox(v) != NIL(array_t)) { array_free(AbsVertexReadSubApprox(v)); } } else if (AbsVertexReadType(v) == identifier_c) { FREE(AbsVertexReadName(v)); FREE(AbsVertexReadValue(v)); } /* Deallocate the memory for the structure itself */ FREE(v); } /* End of AbsVertexFree */ /**Function******************************************************************** Synopsis [Allocates the data structure to store information about the general verification process.] SideEffects [] SeeAlso [AbsVerificationInfo AbsVertexInfo] ******************************************************************************/ Abs_VerificationInfo_t * AbsVerificationInfoInitialize(void) { Abs_VerificationInfo_t *result; result = ALLOC(Abs_VerificationInfo_t, 1); AbsVerificationInfoSetNetwork(result, NIL(Ntk_Network_t)); AbsVerificationInfoSetPartition(result, NIL(graph_t)); AbsVerificationInfoSetFsm(result, NIL(Fsm_Fsm_t)); AbsVerificationInfoSetNumStateVars(result, 0); AbsVerificationInfoSetApproxFsm(result, NIL(Fsm_Fsm_t)); AbsVerificationInfoSetStateVars(result, NIL(st_table)); AbsVerificationInfoSetQuantifyVars(result, NIL(st_table)); AbsVerificationInfoSetCareSet(result, NIL(mdd_t)); AbsVerificationInfoSetTmpCareSet(result, NIL(mdd_t)); AbsVerificationInfoSetImageCache(result, NIL(st_table)); AbsVerificationInfoSetMddManager(result, NIL(mdd_manager)); AbsVerificationInfoSetCatalog(result, NIL(AbsVertexCatalog_t)); AbsVerificationInfoSetStats(result, AbsStatsInitialize()); AbsVerificationInfoSetOptions(result, NIL(AbsOptions_t)); return result; } /* End of AbsVerificationInfoInitialize */ /**Function******************************************************************** Synopsis [Free the structure storing the verification info.] Description [Some of the fields in this structure are owned by this package and some others are simply pointers to a data structure that is owned by some other package. Refer to the definition of Abs_VerificationInfo_t to know which fields are onwed and which are not.] SideEffects [] SeeAlso [AbsVerificationInfo AbsVertexInfo] ******************************************************************************/ void AbsVerificationInfoFree( Abs_VerificationInfo_t *v) { if (AbsVerificationInfoReadStateVars(v) != NIL(st_table)) { st_free_table(AbsVerificationInfoReadStateVars(v)); } if (AbsVerificationInfoReadQuantifyVars(v) != NIL(st_table)) { st_free_table(AbsVerificationInfoReadQuantifyVars(v)); } if (AbsVerificationInfoReadImageCache(v) != NIL(st_table)) { AbsEvalCacheEntry_t *value; bdd_node *key; st_generator *stgen; st_foreach_item(AbsVerificationInfoReadImageCache(v), stgen, &key, &value) { AbsCacheEntryFree(value); } st_free_table(AbsVerificationInfoReadImageCache(v)); } if (AbsVerificationInfoReadCareSet(v) != NIL(mdd_t)) { mdd_free(AbsVerificationInfoReadCareSet(v)); } if (AbsVerificationInfoReadTmpCareSet(v) != NIL(mdd_t)) { mdd_free(AbsVerificationInfoReadTmpCareSet(v)); } if (AbsVerificationInfoReadCatalog(v) != NIL(AbsVertexCatalog_t)) { AbsVertexCatalogFree(AbsVerificationInfoReadCatalog(v)); } AbsStatsFree(AbsVerificationInfoReadStats(v)); FREE(v); /* * The options field is not freed since it is assumed that it has been * allocated outside the AbsVerificationInitialize procedure */ return; } /* End of AbsVerificationInfoFree */ /**Function******************************************************************** Synopsis [Allocate the structure to store the value of the options.] SideEffects [] SeeAlso [AbsOptions] ******************************************************************************/ AbsOptions_t * AbsOptionsInitialize(void) { AbsOptions_t *result; result = ALLOC(AbsOptions_t, 1); AbsOptionsSetVerbosity(result, 0); AbsOptionsSetTimeOut(result, 0); AbsOptionsSetFileName(result, NIL(char)); AbsOptionsSetReachability(result, FALSE); AbsOptionsSetFairFileName(result, NIL(char)); AbsOptionsSetExact(result, FALSE); AbsOptionsSetPrintStats(result, FALSE); AbsOptionsSetMinimizeIterate(result, FALSE); AbsOptionsSetNegateFormula(result, FALSE); AbsOptionsSetPartApprox(result, FALSE); return result; } /* End of AbsOptionsInitialize */ /**Function******************************************************************** Synopsis [Deallocate the structure storing the value of the options.] SideEffects [] SeeAlso [AbsOptions] ******************************************************************************/ void AbsOptionsFree(AbsOptions_t *unit) { if (AbsOptionsReadFileName(unit) != NIL(char)) { FREE(AbsOptionsReadFileName(unit)); } if (AbsOptionsReadFairFileName(unit) != NIL(char)) { FREE(AbsOptionsReadFairFileName(unit)); } FREE(unit); return; } /* End of AbsOptionsInitialize */ /**Function******************************************************************** Synopsis [Allocate the data structure storing the different statistics measurements collected by the algorithms] SideEffects [] SeeAlso [AbsStats] ******************************************************************************/ AbsStats_t * AbsStatsInitialize(void) { AbsStats_t *result; result = ALLOC(AbsStats_t, 1); AbsStatsSetNumReorderings(result, 0); AbsStatsSetEvalFixedPoint(result, 0); AbsStatsSetEvalAnd(result, 0); AbsStatsSetEvalNot(result, 0); AbsStatsSetEvalPreImage(result, 0); AbsStatsSetEvalIdentifier(result, 0); AbsStatsSetEvalVariable(result, 0); AbsStatsSetRefineFixedPoint(result, 0); AbsStatsSetRefineAnd(result, 0); AbsStatsSetRefineNot(result, 0); AbsStatsSetRefinePreImage(result, 0); AbsStatsSetRefineIdentifier(result, 0); AbsStatsSetRefineVariable(result, 0); AbsStatsSetExactPreImage(result, 0); AbsStatsSetApproxPreImage(result, 0); AbsStatsSetExactImage(result, 0); AbsStatsSetPreImageCacheEntries(result, 0); AbsStatsSetImageCacheEntries(result, 0); AbsStatsSetImageCpuTime(result, 0); AbsStatsSetPreImageCpuTime(result, 0); AbsStatsSetAppPreCpuTime(result, 0); return result; } /* End of AbsStatsInitialize */ /**Function******************************************************************** Synopsis [Function to free the AbsStats structure] SideEffects [] SeeAlso [AbsStats] ******************************************************************************/ void AbsStatsFree( AbsStats_t *unit) { FREE(unit); } /* End of AbsStatsFree */ /**Function******************************************************************** Synopsis [Initalize the entry of the cache for previously computed results] SideEffects [] SeeAlso [AbsEvalCacheEntry] ******************************************************************************/ AbsEvalCacheEntry_t * AbsCacheEntryInitialize(void) { AbsEvalCacheEntry_t *result; result = ALLOC(AbsEvalCacheEntry_t, 1); AbsEvalCacheEntrySetKey(result, NIL(mdd_t)); AbsEvalCacheEntrySetApprox(result, FALSE); AbsEvalCacheEntrySetComplement(result, 0); AbsEvalCacheEntrySetResult(result, NIL(mdd_t)); AbsEvalCacheEntrySetCareSet(result, NIL(mdd_t)); return result; } /* End of AbsCacheEntryInitialize */ /**Function******************************************************************** Synopsis [Function to de-allocate the AbsEvalCacheEntry] SideEffects [] SeeAlso [AbsEvalCacheEntry] ******************************************************************************/ void AbsCacheEntryFree( AbsEvalCacheEntry_t *unit) { mdd_free(AbsEvalCacheEntryReadKey(unit)); mdd_free(AbsEvalCacheEntryReadResult(unit)); mdd_free(AbsEvalCacheEntryReadCareSet(unit)); FREE(unit); } /* End of AbsCacheEntryFree */ /**Function******************************************************************** Synopsis [Insert an item in the evaluation cache] SideEffects [] SeeAlso [AbsEvalCacheEntry] ******************************************************************************/ void AbsEvalCacheInsert( st_table *solutions, mdd_t *key, mdd_t *result, mdd_t *careSet, boolean approx, boolean replace) { AbsEvalCacheEntry_t *entry; int complement; bdd_node *f; entry = NIL(AbsEvalCacheEntry_t); f = bdd_get_node(key, &complement); /* If the replacement is required, delete the element from the table */ if (replace) { st_delete(solutions, &f, &entry); mdd_free(AbsEvalCacheEntryReadKey(entry)); mdd_free(AbsEvalCacheEntryReadResult(entry)); mdd_free(AbsEvalCacheEntryReadCareSet(entry)); } assert(!st_is_member(solutions, (char *)f)); if (entry == NIL(AbsEvalCacheEntry_t)) { entry = AbsCacheEntryInitialize(); } AbsEvalCacheEntrySetKey(entry, mdd_dup(key)); AbsEvalCacheEntrySetApprox(entry, approx); AbsEvalCacheEntrySetComplement(entry, complement); AbsEvalCacheEntrySetResult(entry, mdd_dup(result)); AbsEvalCacheEntrySetCareSet(entry, mdd_dup(careSet)); /* Insert the new entry in the cache */ st_insert(solutions, (char *)f, (char *)entry); return; } /* End of AbsEvalCacheInsert */ /**Function******************************************************************** Synopsis [Lookup a previous evaluation in the cache] SideEffects [] SeeAlso [AbsEvalCacheEntry] ******************************************************************************/ boolean AbsEvalCacheLookup( st_table *solutions, mdd_t *key, mdd_t *careSet, boolean approx, mdd_t **result, boolean *storedApprox) { AbsEvalCacheEntry_t *entry; bdd_node *f; int complement; f = bdd_get_node(key, &complement); if (st_lookup(solutions, f, &entry)) { if (complement == AbsEvalCacheEntryReadComplement(entry) && (approx || !AbsEvalCacheEntryReadApprox(entry)) && mdd_lequal(careSet, AbsEvalCacheEntryReadCareSet(entry), 1, 1)) { *result = AbsEvalCacheEntryReadResult(entry); if (storedApprox != 0) { *storedApprox = AbsEvalCacheEntryReadApprox(entry); } return TRUE; } else { st_delete(solutions, &f, &entry); AbsCacheEntryFree(entry); } } return FALSE; } /* End of AbsEvalCacheLookup */ /**Function******************************************************************** Synopsis [Delete all the entries in the evaluation cache] SideEffects [] SeeAlso [AbsEvalCacheEntry] ******************************************************************************/ void AbsVerificationFlushCache( Abs_VerificationInfo_t *absInfo) { AbsEvalCacheEntry_t *value; st_table *table; bdd_node *key; st_generator *stgen; table = AbsVerificationInfoReadImageCache(absInfo); if (table == NIL(st_table)) { return; } st_foreach_item(table, stgen, &key, &value) { AbsCacheEntryFree(value); } st_free_table(table); AbsVerificationInfoSetImageCache(absInfo, NIL(st_table)); return; } /* End of AbsVerificationFlushCache */ /**Function******************************************************************** Synopsis [Delete all the entries stored in the local evaluation cache that a given vertex has attached to it] SideEffects [] SeeAlso [AbsVertexInfo] ******************************************************************************/ void AbsVertexFlushCache( AbsVertexInfo_t *vertexPtr) { if (AbsVertexReadType(vertexPtr) == preImage_c) { if (AbsVertexReadSolutions(vertexPtr) != NIL(st_table)) { AbsEvalCacheEntry_t *value; bdd_node *key; st_generator *stgen; st_foreach_item(AbsVertexReadSolutions(vertexPtr), stgen, &key, &value) { AbsCacheEntryFree(value); } st_free_table(AbsVertexReadSolutions(vertexPtr)); AbsVertexSetSolutions(vertexPtr, NIL(st_table)); } } if (AbsVertexReadLeftKid(vertexPtr) != NIL(AbsVertexInfo_t)) { AbsVertexFlushCache(AbsVertexReadLeftKid(vertexPtr)); } if (AbsVertexReadRightKid(vertexPtr) != NIL(AbsVertexInfo_t)) { AbsVertexFlushCache(AbsVertexReadRightKid(vertexPtr)); } return; } /* End of AbsVertexFlushCache */ /**Function******************************************************************** Synopsis [Read an image computation from the cache, and if it is not present, invoke the image algorithm and store its result] SideEffects [] SeeAlso [AbsEvalCacheEntry] ******************************************************************************/ mdd_t * AbsImageReadOrCompute( Abs_VerificationInfo_t *absInfo, Img_ImageInfo_t *imageInfo, mdd_t *set, mdd_t *careSet ) { AbsEvalCacheEntry_t *entry; st_table *table; bdd_node *f; mdd_t *result; long cpuTime; int complement; entry = NIL(AbsEvalCacheEntry_t); table = AbsVerificationInfoReadImageCache(absInfo); f = bdd_get_node(set, &complement); /* See if the table has been created */ if (table == NIL(st_table)) { table = st_init_table(st_ptrcmp, st_ptrhash); AbsVerificationInfoSetImageCache(absInfo, table); } else { /* Look up for the operation */ if (st_lookup(table, f, &entry)) { if (complement == AbsEvalCacheEntryReadComplement(entry) && mdd_lequal(careSet, AbsEvalCacheEntryReadCareSet(entry), 1, 1)) { result = mdd_dup(AbsEvalCacheEntryReadResult(entry)); return result; } else { st_delete(table, &f, &entry); mdd_free(AbsEvalCacheEntryReadKey(entry)); mdd_free(AbsEvalCacheEntryReadResult(entry)); mdd_free(AbsEvalCacheEntryReadCareSet(entry)); } } } /* The result has not been found. Compute it and insert it in the cache */ cpuTime = util_cpu_time(); result = Img_ImageInfoComputeFwdWithDomainVars(imageInfo, set, set, careSet); AbsStatsReadImageCpuTime(AbsVerificationInfoReadStats(absInfo))+= util_cpu_time() - cpuTime; AbsStatsReadExactImage(AbsVerificationInfoReadStats(absInfo))++; if (entry == NIL(AbsEvalCacheEntry_t)) { entry = AbsCacheEntryInitialize(); } AbsEvalCacheEntrySetKey(entry, mdd_dup(set)); AbsEvalCacheEntrySetComplement(entry, complement); AbsEvalCacheEntrySetResult(entry, mdd_dup(result)); AbsEvalCacheEntrySetCareSet(entry, mdd_dup(careSet)); /* Insert the new entry in the cache */ st_insert(table, (char *)f, (char *)entry); AbsStatsReadImageCacheEntries(AbsVerificationInfoReadStats(absInfo))++; return result; } /* End of AbsImageReadOrCompute */ /**Function******************************************************************** Synopsis [Procedure to fire the evaluation process for a collection of formulas given in an array] Description [This is the main procedure of the package. The command abs_model_check invokes this function. This procedure invokes the procedure AbsSubFormulaVerify] SideEffects [] ******************************************************************************/ array_t * AbsFormulaArrayVerify( Abs_VerificationInfo_t *absInfo, array_t *formulaArray) { AbsOptions_t *options; AbsVertexInfo_t *formulaPtr; Fsm_Fsm_t *fsm; array_t *result; mdd_manager *mddManager; int fIndex; int numReorderings; /* Initialize some variables */ options = AbsVerificationInfoReadOptions(absInfo); mddManager = AbsVerificationInfoReadMddManager(absInfo); numReorderings = bdd_read_reorderings(mddManager); /* Print the configuration of the system */ if (AbsOptionsReadVerbosity(options) & ABS_VB_PIFF) { (void) fprintf(vis_stdout, "ABS: System with (PI,FF) = (%d,%d)\n", st_count(AbsVerificationInfoReadQuantifyVars(absInfo)), st_count(AbsVerificationInfoReadStateVars(absInfo))); } /* Create the array of results */ result = array_alloc(AbsVerificationResult_t, array_n(formulaArray)); /* Obtain the fsm representing the complete circuit */ fsm = Fsm_FsmCreateFromNetworkWithPartition( AbsVerificationInfoReadNetwork(absInfo), NIL(graph_t)); /* Traverse the array of formulas and verify all of them */ arrayForEachItem(AbsVertexInfo_t *, formulaArray, fIndex, formulaPtr) { Fsm_Fsm_t *localSystem; Fsm_Fsm_t *approxSystem; array_t *stateVarIds; mdd_t *initialStates; mdd_t *careStates; long cpuTime; int numBddVars; int mddId; int i; /* Variable Initialization */ approxSystem = NIL(Fsm_Fsm_t); /* Set the cpu-time lap */ cpuTime = util_cpu_time(); /* Print the labeled operational graph */ if (AbsOptionsReadVerbosity(options) & ABS_VB_GRAPH) { (void) fprintf(vis_stdout, "ABS: === Labeled Operational Graph ===\n"); AbsVertexPrint(formulaPtr, NIL(st_table), TRUE, AbsOptionsReadVerbosity(options)); (void) fprintf(vis_stdout, "ABS: === End of Graph ===\n"); } /* Simplify the system with respect to the given formula */ localSystem = AbsCreateReducedFsm(absInfo, formulaPtr, &approxSystem); if (localSystem == NIL(Fsm_Fsm_t)) { localSystem = fsm; } if (approxSystem == NIL(Fsm_Fsm_t)) { approxSystem = fsm; } AbsVerificationInfoSetFsm(absInfo, localSystem); /* Compute the number of bdd variables needed to encode the state space */ stateVarIds = Fsm_FsmReadPresentStateVars(localSystem); numBddVars = 0; arrayForEachItem(int, stateVarIds, i, mddId) { array_t *mvarList = mdd_ret_mvar_list(mddManager); mvar_type mddVar = array_fetch(mvar_type, mvarList, mddId); numBddVars += mddVar.encode_length; } AbsVerificationInfoSetNumStateVars(absInfo, numBddVars); AbsVerificationInfoSetApproxFsm(absInfo, approxSystem); if (AbsOptionsReadVerbosity(options) & ABS_VB_SIMPLE) { (void) fprintf(vis_stdout, "ABS: System Simplified from %d to %d latches\n", array_n(Fsm_FsmReadPresentStateVars(fsm)), array_n(Fsm_FsmReadPresentStateVars(localSystem))); (void) fprintf(vis_stdout, "ABS: System Approximated by %d of %d latches\n", array_n(Fsm_FsmReadPresentStateVars(approxSystem)), array_n(Fsm_FsmReadPresentStateVars(localSystem))); } /* Compute reachability if requested */ if (AbsOptionsReadReachability(options)) { mdd_t *reachableStates; long cpuTime; cpuTime = util_cpu_time(); reachableStates = Fsm_FsmComputeReachableStates(localSystem, 0, 1, 0, 0, 0, 0, 0,Fsm_Rch_Default_c, 0, 0, NIL(array_t), FALSE, NIL(array_t)); if (AbsOptionsReadVerbosity(options) & ABS_VB_PPROGR) { (void) fprintf(vis_stdout, "ABS: %7.1f secs spent in reachability \n", (util_cpu_time() - cpuTime)/1000.0); } /* Print the number of reachable states */ if (AbsOptionsReadVerbosity(options) & ABS_VB_PRCH) { array_t *sVars; sVars = Fsm_FsmReadPresentStateVars(localSystem); (void) fprintf(vis_stdout, "ABS: System with %.0f reachable states.\n", mdd_count_onset(mddManager, reachableStates, sVars)); } careStates = reachableStates; } /* End of reachability analysis */ else { careStates = mdd_one(mddManager); } /* Compute the initial states */ initialStates = Fsm_FsmComputeInitialStates(localSystem); if (initialStates == NIL(mdd_t)) { (void) fprintf(vis_stdout, "** abs error: Unable to compute initial states.\n"); (void) fprintf(vis_stdout, "ABS: %s\n", error_string()); AbsVerificationInfoFree(absInfo); array_free(result); /* Deallocate the FSM if the system was reduced */ if (localSystem != fsm) { Fsm_FsmFree(localSystem); } return NIL(array_t); } /* Set the don't care information */ if (AbsVerificationInfoReadCareSet(absInfo) != NIL(mdd_t)) { mdd_free(AbsVerificationInfoReadCareSet(absInfo)); } AbsVerificationInfoSetCareSet(absInfo, careStates); if (AbsVerificationInfoReadTmpCareSet(absInfo) != NIL(mdd_t)) { mdd_free(AbsVerificationInfoReadTmpCareSet(absInfo)); } AbsVerificationInfoSetTmpCareSet(absInfo, mdd_one(mddManager)); /* Compute the formula EG(true) if required */ if (AbsOptionsReadEnvelope(options)) { mdd_t *newCareStates; mdd_t *tmp1; newCareStates = ComputeEGtrue(absInfo, careStates); tmp1 = mdd_and(newCareStates, careStates, 1, 1); mdd_free(careStates); mdd_free(newCareStates); careStates = tmp1; AbsVerificationInfoSetCareSet(absInfo, careStates); } /* Print verbosity message */ if (AbsOptionsReadVerbosity(options) & ABS_VB_VTXCNT) { (void) fprintf(vis_stdout, "ABS: === Initial Verification ===\n"); } /* Create the initial evaluation of the formula */ AbsSubFormulaVerify(absInfo, formulaPtr); assert(!AbsVertexReadTrueRefine(formulaPtr)); /* Print verbosity message */ if (AbsOptionsReadVerbosity(options) & ABS_VB_VTXCNT) { (void) fprintf(vis_stdout, "ABS: === End of Initial Verification ===\n"); } /* Print cpu-time information */ if (AbsOptionsReadVerbosity(options) & ABS_VB_PPROGR) { (void) fprintf(vis_stdout, "ABS: Initial verification: %7.1f secs.\n", (util_cpu_time() - cpuTime)/1000.0); } /* Check if the initial states satisfy the formula */ if (mdd_lequal(initialStates, AbsVertexReadSat(formulaPtr), 1, 1)) { array_insert(int, result, fIndex, trueVerification_c); } else { if (AbsVertexReadGlobalApprox(formulaPtr)) { mdd_t *goalSet; mdd_t *refinement; /* * Compute the set of states remaining in the goal. We are assuming * that the parity of the top vertex is negative */ assert(!AbsVertexReadPolarity(formulaPtr)); /* Compute the initial goal set */ goalSet = mdd_and(initialStates, AbsVertexReadSat(formulaPtr), 1, 0); /* Notify that the refinement process is beginning */ if (AbsOptionsReadVerbosity(options) &ABS_VB_PPROGR) { (void) fprintf(vis_stdout, "ABS: Verification has been approximated. "); (void) fprintf(vis_stdout, "Beginning approximation refinement\n"); } /* Print the number of states to refine */ if (AbsOptionsReadVerbosity(options) & ABS_VB_PRINIT) { array_t *sVars; sVars = Fsm_FsmReadPresentStateVars(fsm); (void) fprintf(vis_stdout, "ABS: %.0f states out of %.0f to be refined\n", mdd_count_onset(mddManager, goalSet, sVars), mdd_count_onset(mddManager, initialStates, sVars)); } /* Effectively perform the refinement */ refinement = AbsSubFormulaRefine(absInfo, formulaPtr, goalSet); /* Insert the outcome of the refinement in the solution */ if (mdd_is_tautology(refinement, 0)) { array_insert(int, result, fIndex, trueVerification_c); } else { if (!AbsVertexReadTrueRefine(formulaPtr)) { array_insert(int, result, fIndex, inconclusiveVerification_c); } else { array_insert(int, result, fIndex, falseVerification_c); } } mdd_free(goalSet); mdd_free(refinement); } else { array_insert(int, result, fIndex, falseVerification_c); } } mdd_free(initialStates); /* Print cpu-time information */ if (AbsOptionsReadVerbosity(options) & ABS_VB_PPROGR) { (void) fprintf(vis_stdout, "ABS: Formula #%d verified in %7.1f secs.\n", fIndex + 1, (util_cpu_time() - cpuTime)/1000.0); } /* Print the number of states in the on set of Sat */ if (AbsOptionsReadVerbosity(options) & ABS_VB_TSAT) { array_t *sVars; sVars = Fsm_FsmReadPresentStateVars(localSystem); (void) fprintf(vis_stdout, "ABS: %.0f States in sat of the formula.\n", mdd_count_onset(mddManager, AbsVertexReadSat(formulaPtr), sVars)); } /* Clean up */ AbsVertexFlushCache(formulaPtr); AbsVerificationFlushCache(absInfo); if (approxSystem != fsm) { Fsm_FsmFree(approxSystem); } if (localSystem != fsm) { Fsm_FsmFree(localSystem); } } /* End of the loop over the array of formulas to be verified */ /* Set the number of reorderings in the stats */ AbsStatsSetNumReorderings(AbsVerificationInfoReadStats(absInfo), bdd_read_reorderings(mddManager) - numReorderings); /* Clean up */ Fsm_FsmFree(fsm); return result; } /**Function******************************************************************** Synopsis [Given a FSM and operational graph, simplify the FSM based on topological analysis of the FSM] SideEffects [] ******************************************************************************/ Fsm_Fsm_t * AbsCreateReducedFsm( Abs_VerificationInfo_t *absInfo, AbsVertexInfo_t *vertexPtr, Fsm_Fsm_t **approxFsm) { AbsVertexInfo_t *vPtr; Ntk_Network_t *network; Ntk_Node_t *nodePtr; Fsm_Fsm_t *result; lsGen gen; array_t *vertexArray; array_t *nodeArray; array_t *supportArray; array_t *inputs; array_t *latches; st_table *visited; int i; if (vertexPtr == NIL(AbsVertexInfo_t)) { return NIL(Fsm_Fsm_t); } network = AbsVerificationInfoReadNetwork(absInfo); /* Select the vertices of type "identifier" */ visited = st_init_table(st_ptrcmp, st_ptrhash); vertexArray = array_alloc(AbsVertexInfo_t *, 0); SelectIdentifierVertices(vertexPtr, vertexArray, visited); st_free_table(visited); if (array_n(vertexArray) == 0) { array_free(vertexArray); return NIL(Fsm_Fsm_t); } /* Create the array of network nodes corresponding to the identifiers */ visited = st_init_table(st_ptrcmp, st_ptrhash); nodeArray = array_alloc(Ntk_Node_t *, 0); arrayForEachItem(AbsVertexInfo_t *, vertexArray, i, vPtr) { nodePtr = Ntk_NetworkFindNodeByName(network, AbsVertexReadName(vPtr)); assert(nodePtr != NIL(Ntk_Node_t)); if (!st_is_member(visited, (char *)nodePtr)) { array_insert_last(Ntk_Node_t *, nodeArray, nodePtr); st_insert(visited, (char *)nodePtr, NIL(char)); } } array_free(vertexArray); /* Create the input and array latches to compute the approxFsm */ inputs = array_alloc(Ntk_Node_t *, 0); Ntk_NetworkForEachInput(network, gen, nodePtr) { array_insert_last(Ntk_Node_t *, inputs, nodePtr); } latches = array_alloc(Ntk_Node_t *, 0); Ntk_NetworkForEachLatch(network, gen, nodePtr) { if (st_is_member(visited, (char *)nodePtr)) { array_insert_last(Ntk_Node_t *, latches, nodePtr); } else { array_insert_last(Ntk_Node_t *, inputs, nodePtr); } } st_free_table(visited); /* Obtain the approximated system */ *approxFsm = Fsm_FsmCreateReducedFsm(network, NIL(graph_t), latches, inputs, NIL(array_t)); array_free(inputs); array_free(latches); /* Obtain the transitive fanin of the nodes */ supportArray = Ntk_NodeComputeCombinationalSupport(network, nodeArray, FALSE); array_free(nodeArray); /* If the transitive fanin of the nodes is empty, return */ if (array_n(supportArray) == 0) { array_free(supportArray); return NIL(Fsm_Fsm_t); } /* Divide the nodes between inputs and latches and create the final FSM */ inputs = array_alloc(Ntk_Node_t *, 0); latches = array_alloc(Ntk_Node_t *, 0); arrayForEachItem(Ntk_Node_t *, supportArray, i, nodePtr) { if (Ntk_NodeTestIsInput(nodePtr)) { array_insert_last(Ntk_Node_t *, inputs, nodePtr); } else { assert(Ntk_NodeTestIsLatch(nodePtr)); array_insert_last(Ntk_Node_t *, latches, nodePtr); } } array_free(supportArray); /* If the collection of inputs and latches is the whole FSM, return */ if (array_n(inputs) == Ntk_NetworkReadNumInputs(network) && array_n(latches) == Ntk_NetworkReadNumLatches(network)) { array_free(inputs); array_free(latches); return NIL(Fsm_Fsm_t); } result = Fsm_FsmCreateReducedFsm(network, NIL(graph_t), latches, inputs, NIL(array_t)); /* Clean up */ array_free(inputs); array_free(latches); return result; } /* End of AbsCreateReducedFsm */ /**Function******************************************************************** Synopsis [Check if two functions are identical modulo the don't care function provided] SideEffects [] ******************************************************************************/ boolean AbsMddEqualModCareSet( mdd_t *f, mdd_t *g, mdd_t *careSet) { boolean result = mdd_equal_mod_care_set(f, g, careSet); return result; } /* End of AbsMddEqualModCareSet */ /**Function******************************************************************** Synopsis [Check if function f is contained in function g but taking into account the provided care set] SideEffects [] ******************************************************************************/ boolean AbsMddLEqualModCareSet( mdd_t *f, mdd_t *g, mdd_t *careSet) { boolean result = mdd_lequal_mod_care_set(f, g, 1, 1, careSet); return result; } /* End of AbsMddLEqualModCareSet */ /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Compute the verification of the formula EG(true)] Description [This is provided as an option. The computation of this formula might reduce the state space to be explored. Specifically, it gets rid of states that do not have any successor as well as any other states leading to them. The benefit of this computation is unclear, specially because some tools that read verilog and produce blif-mv might produce a self loop in every state for which no transition is specified. If that is so, there will never be a state without a successor.] SideEffects [] ******************************************************************************/ static mdd_t * ComputeEGtrue( Abs_VerificationInfo_t *absInfo, mdd_t *careStates) { AbsOptions_t *options; AbsVertexInfo_t *vertex; Ctlp_Formula_t *egFormula; Ctlp_Formula_t *trueFormula; mdd_manager *mddManager; array_t *inputTranslation; array_t *outputTranslation; mdd_t *envelope; long cpuTime; cpuTime = util_cpu_time(); options = AbsVerificationInfoReadOptions(absInfo); mddManager = AbsVerificationInfoReadMddManager(absInfo); /* Compute the EG(true) fixed point */ trueFormula = Ctlp_FormulaCreate(Ctlp_TRUE_c, NIL(void), NIL(void)); egFormula = Ctlp_FormulaCreate(Ctlp_EG_c, trueFormula, NIL(void)); /* Translate into the graph representation */ inputTranslation = array_alloc(Ctlp_Formula_t *, 1); array_insert(Ctlp_Formula_t *, inputTranslation, 0, egFormula); outputTranslation = AbsCtlFormulaArrayTranslate(absInfo, inputTranslation, NIL(array_t)); vertex = array_fetch(AbsVertexInfo_t *, outputTranslation, 0); array_free(inputTranslation); array_free(outputTranslation); /* Evaluate the formula */ AbsSubFormulaVerify(absInfo, vertex); envelope = mdd_dup(AbsVertexReadSat(vertex)); /* Clean up */ Ctlp_FormulaFree(egFormula); AbsVertexFree(AbsVerificationInfoReadCatalog(absInfo), vertex, NIL(AbsVertexInfo_t)); /* Print the number of envelope states */ if (AbsOptionsReadVerbosity(options) & ABS_VB_PENV) { array_t *sVars; mdd_t *states; sVars = Fsm_FsmReadPresentStateVars(AbsVerificationInfoReadFsm(absInfo)); states = mdd_and(envelope, careStates, 1, 1); (void) fprintf(vis_stdout, "ABS: Envelope with %.0f care states.\n", mdd_count_onset(mddManager, states, sVars)); mdd_free(states); } if (AbsOptionsReadVerbosity(options) & ABS_VB_PENV) { (void) fprintf(vis_stdout, "ABS: %7.1f secs computing EG(TRUE)\n", (util_cpu_time() - cpuTime)/1000.0); } return envelope; } /* End of ComputeEGtrue */ /**Function******************************************************************** Synopsis [Given a graph, select the set of vertices that represent identifiers] SideEffects [] ******************************************************************************/ static void SelectIdentifierVertices( AbsVertexInfo_t *vertexPtr, array_t *result, st_table *visited) { assert(result != NIL(array_t)); if (vertexPtr == NIL(AbsVertexInfo_t)) { return; } if (st_is_member(visited, (char *)vertexPtr)) { return; } if (AbsVertexReadType(vertexPtr) == identifier_c) { array_insert_last(AbsVertexInfo_t *, result, vertexPtr); st_insert(visited, (char *)vertexPtr, NIL(char)); return; } else { SelectIdentifierVertices(AbsVertexReadLeftKid(vertexPtr), result, visited); SelectIdentifierVertices(AbsVertexReadRightKid(vertexPtr), result, visited); } st_insert(visited, (char *)vertexPtr, NIL(char)); return; } /* End of SelectIdentifierVertices */