/**CFile*********************************************************************** FileName [grabGrab.c] PackageName [grab] Synopsis [The GRAB algorithm of computing a set of refinement variables.] Description [The computation is based on all the shortest abstract counter-examples.] 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 st_table *Sel0ScoreTable; static st_table *SelScoreTable; static st_table *Sel2ScoreTable; static st_table *Sel3ScoreTable; /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static array_t * GrabFsmComputeExRings(Fsm_Fsm_t *absFsm, st_table *absVarTable, st_table *absBnvTable, array_t *oldRings, int cexType, int verbose); static int GrabCompareScores(const void *ptr1, const void *ptr2); static void GrabMddAppendSupports(mdd_manager *mddManager, mdd_t *mdd1, st_table *supportsTable); static array_t * ComputeDependence(Ntk_Network_t *network, st_table *vertexTable, array_t *leftVars); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Pick a set of refinement variables using Grab.] Description [Pick a set of refinement variables using Grab. When refine_direction is 1, refine in both directions (by adding latches and bnvs); when refine_direction is 0, refine only in the boolean direction (by adding bnvs). The present state variables of absFsm must include all the invisible variables; its next state variables must include only the visible ones. On such a FSM, the preimage may contain some invisible variables in its support. The set of preimages, ExRings, is the set of augmented preimages (with invisible variables in the support). The refinement variable will be put into either addedVars or addedBnvs, depending on which class it bolongs to; at the same time, it will be put into either absVarTable or BnvTable. nodeToFaninNumber is a global variable, whose values are used as tie-breakers.] SideEffects [] ******************************************************************************/ void GrabRefineAbstractionByGrab( Fsm_Fsm_t *absFsm, array_t *SORs, st_table *absVarTable, st_table *BnvTable, array_t *addedVars, array_t *addedBnvs, int refine_direction, st_table *nodeToFaninNumberTable, int verbose) { Ntk_Network_t *network = Fsm_FsmReadNetwork(absFsm); mdd_manager *mddManager = Ntk_NetworkReadMddManager(network); array_t *ExRings; array_t *visibleVarMddIds, *invisibleVarMddIds, *allPSVars; array_t *tempArray; mdd_t *mdd1, *mdd2; char *nodeName; Ntk_Node_t *node; double *Scores, *SelScores, *Sel0Scores, *Sel2Scores, *Sel3Scores; double epd, baseNum; int i, j, nRow, nCol; long mddId, value, value0; boolean isSupport, isLatch; int max_num_of_added_vars; /* compute the preimages (with invisible vars in their support) */ ExRings = GrabFsmComputeExRings(absFsm, absVarTable, BnvTable, SORs, GRAB_CEX_SOR, verbose); assert(ExRings != NIL(array_t)); visibleVarMddIds = GrabGetVisibleVarMddIds(absFsm,absVarTable); invisibleVarMddIds = GrabGetInvisibleVarMddIds(absFsm,absVarTable,BnvTable); allPSVars = array_dup(visibleVarMddIds); array_append(allPSVars, invisibleVarMddIds); assert(array_n(invisibleVarMddIds) > 0 ); /* Compute the normalized number of "winning positions" for each individual * invisibleVar, and store them in 'Scores'! */ nRow = array_n(ExRings); nCol = array_n(invisibleVarMddIds); Scores = ALLOC(double, nRow*nCol); memset(Scores, 0, sizeof(double)*nRow*nCol); /********************************************************* * for each set of abstract states in (mdd1, Ring[j+1] ) *********************************************************/ arrayForEachItem(mdd_t *, ExRings, j, mdd1) { st_table *localSupportsTable = st_init_table(st_numcmp, st_numhash); GrabMddAppendSupports(mddManager, mdd1, localSupportsTable); if (mdd_get_number_of_bdd_vars(mddManager, allPSVars) <= 1023 ) baseNum = mdd_count_onset(mddManager, mdd1, allPSVars); else { mdd_t *stateMdd = mdd_smooth(mddManager, mdd1, invisibleVarMddIds); baseNum = mdd_count_onset(mddManager, stateMdd, visibleVarMddIds); mdd_free(stateMdd); } /*********************************************************** * compute the impact of refining with each invisible var ***********************************************************/ arrayForEachItem(int, invisibleVarMddIds, i, mddId) { /* for debugging purpose. won't affect the algorithm */ Scores[j*nCol+i] = -9E-99; /* give credit simply for the appearance */ isSupport = st_is_member(localSupportsTable, (char *)mddId); if (!isSupport || baseNum==0.0) continue; Scores[j*nCol+i] += 0.001; node = Ntk_NetworkFindNodeByMddId(network, mddId); isLatch = (Ntk_NodeTestIsLatch(node)); if (refine_direction==0 && isLatch) continue; { array_t *universalQVars = array_alloc(int, 0); /* MX */ array_insert_last(int, universalQVars, mddId); mdd2 = mdd_consensus(mddManager, mdd1, universalQVars); array_free(universalQVars); if (mdd_get_number_of_bdd_vars(mddManager, allPSVars) <= 1023) epd = mdd_count_onset(mddManager, mdd2, allPSVars); else { mdd_t *stateMdd = mdd_smooth(mddManager, mdd2, invisibleVarMddIds); epd = mdd_count_onset(mddManager, stateMdd, visibleVarMddIds); mdd_free(stateMdd); } mdd_free(mdd2); Scores[j*nCol+i] = (baseNum - epd)/baseNum; } if (j == 0) Scores[j*nCol+i] /= 10.0; } st_free_table(localSupportsTable); } /* For each column, sum up the score over all the rows. The * selection of refinement variables will be based mainly on these * scores. */ SelScores = ALLOC(double, nCol); memset(SelScores, 0, sizeof(double)*nCol); for (i=0; i= 5) { /* the entire score table */ fprintf(vis_stdout, "\n Scores[%d][%d] = \n", nRow, nCol); arrayForEachItem(int, invisibleVarMddIds, i, mddId) { node = Ntk_NetworkFindNodeByMddId(network, mddId); fprintf(vis_stdout, "%s ", (Ntk_NodeTestIsLatch(node)?" L ":" ")); } fprintf(vis_stdout, "\n"); arrayForEachItem(int, invisibleVarMddIds, i, mddId) { node = Ntk_NetworkFindNodeByMddId(network, mddId); fprintf(vis_stdout, "%5d ", i); } fprintf(vis_stdout, "\n"); for (i=0; i= 4) { fprintf(vis_stdout, " \t Sel0 Sel Sel2 Sel3\n"); arrayForEachItem(int, invisibleVarMddIds, j, mddId) { double *addr; st_lookup(Sel0ScoreTable, (char *)mddId, &addr); i = (int)(addr-Sel0Scores); node = Ntk_NetworkFindNodeByMddId(network, mddId); isLatch = (Ntk_NodeTestIsLatch(node)); fprintf(vis_stdout, "%s[%d]\t %+1.3f %+1.3f %+1.3f %+1.3f %s\n", (isLatch? "L":" "), i, Sel0Scores[i], SelScores[i], Sel2Scores[i], Sel3Scores[i], Ntk_NodeReadName(node) ); /* only output the top 20 variables */ if (j >= 19) break; } } st_free_table(Sel0ScoreTable); st_free_table(SelScoreTable); st_free_table(Sel2ScoreTable); st_free_table(Sel3ScoreTable); /* Now find the best (largest score) invisible Var */ { int num_absBnvs = BnvTable? st_count(BnvTable):0; if ((st_count(absVarTable) + num_absBnvs) < 10) max_num_of_added_vars = 1; else max_num_of_added_vars = 2 + (st_count(absVarTable)+num_absBnvs)/30; } arrayForEachItem(int, invisibleVarMddIds, j, mddId) { if (j >= max_num_of_added_vars) break; node = Ntk_NetworkFindNodeByMddId(network, mddId); nodeName = Ntk_NodeReadName(node); if (Ntk_NodeTestIsLatch(node)) { assert(!st_is_member(absVarTable, node)); st_insert(absVarTable, node, (char *)(long)st_count(absVarTable)); array_insert_last(int, addedVars, mddId); CHKPRINT2( (verbose>=3), " add Latch %s\n", nodeName ); }else if (!Ntk_NodeTestIsLatch(node)) { assert(!st_is_member(BnvTable, node)); st_insert(BnvTable, node, (char *)0); array_insert_last(int, addedBnvs, mddId); CHKPRINT2( (verbose>=3), " add BNV %s\n", nodeName ); } } /* Clean-ups */ array_free(invisibleVarMddIds); array_free(visibleVarMddIds); array_free(allPSVars); mdd_array_free(ExRings); FREE(Scores); FREE(Sel0Scores); FREE(SelScores); FREE(Sel2Scores); FREE(Sel3Scores); } /**Function******************************************************************** Synopsis [Compute the number of fanin nodes] Description [Compute the number of fanin nodes. The result is inserted in the hash table.] SideEffects [] ******************************************************************************/ int GrabNodeComputeFaninNumberTableItem( Ntk_Network_t *network, st_table *nodeToFaninNumberTable, Ntk_Node_t *node) { int count; array_t *roots, *supports; roots = array_alloc(Ntk_Node_t *, 0); if (!st_lookup_int(nodeToFaninNumberTable, node, &count)) { if (Ntk_NodeTestIsLatch(node)) array_insert(Ntk_Node_t *, roots, 0, Ntk_LatchReadDataInput(node)); else array_insert(Ntk_Node_t *, roots, 0, node); supports = Ntk_NodeComputeTransitiveFaninNodes(network, roots, TRUE,FALSE); count = array_n(supports); array_free(supports); st_insert(nodeToFaninNumberTable, node, (char *)(long)count); } array_free(roots); return count; } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Compute the extended Synchronous Onion Rings (SORs).] Description [Compute the extended Synchronous Onion Rings (SORs) on the absFSm whose present state variables includes the invisible variables. The preimages, therefore, may have invisible variables in their support. The result is used only inside GrabRefineAbstractionByGrab.] SideEffects [] ******************************************************************************/ static array_t * GrabFsmComputeExRings( Fsm_Fsm_t *absFsm, st_table *absVarTable, st_table *absBnvTable, array_t *oldRings, int cexType, int verbose) { Img_ImageInfo_t *imageInfo; Ntk_Network_t *network = Fsm_FsmReadNetwork(absFsm); array_t *careStatesArray = array_alloc(mdd_t *, 0); array_t *allPsVars, *invisibleVarMddIds; array_t *onionRings, *synOnionRings; mdd_t *mdd1, *mdd2, *mdd3, *mdd4, *initStates; int i, j, mddId; Ntk_Node_t *node; imageInfo = Fsm_FsmReadOrCreateImageInfo(absFsm, 1, 0); /* Compute the initial states based on all the related latches * (i.e. visible latches and invisible ones that are in the * immediate support) */ allPsVars = GrabGetVisibleVarMddIds(absFsm, absVarTable); invisibleVarMddIds = GrabGetInvisibleVarMddIds(absFsm, absVarTable, absBnvTable); arrayForEachItem(int, invisibleVarMddIds, i, mddId) { node = Ntk_NetworkFindNodeByMddId(network, mddId); if (Ntk_NodeTestIsLatch(node)) array_insert_last(int, allPsVars, mddId); } initStates = GrabComputeInitialStates(network, allPsVars); array_free(allPsVars); array_free(invisibleVarMddIds); onionRings = oldRings; if (onionRings == NIL(array_t)) onionRings = Fsm_FsmReadReachabilityOnionRings(absFsm); assert(onionRings); synOnionRings = array_alloc(mdd_t *, array_n(onionRings)); for (j=array_n(onionRings)-2; j>=0; j--) { mdd1 = array_fetch(mdd_t *, onionRings, j+1); mdd2 = array_fetch(mdd_t *, onionRings, j); array_insert(mdd_t *, careStatesArray, 0, mdd2); mdd3 = Img_ImageInfoComputeEXWithDomainVars(imageInfo, mdd1, mdd1, careStatesArray); mdd4 = mdd_and(mdd2, mdd3, 1, 1); mdd_free(mdd3); array_insert(mdd_t *, synOnionRings, j+1, mdd4); /* when the more accurate initial states is available, use it */ if (j == 0) { mdd1 = mdd_and(mdd4, initStates, 1, 1); if (mdd_is_tautology(mdd1, 0)) { mdd_free(mdd1); mdd1 = mdd_dup(mdd4); } array_insert(mdd_t *, synOnionRings, j, mdd1); } } /* clean-up's */ mdd_free(initStates); array_free(careStatesArray); return synOnionRings; } /**Function******************************************************************** Synopsis [Compare the scores of the two invisible variables.] Description [Compare the scores of the two invisible variables. It is used inside GrabRefineAbstractionByGrab() for sorting the array of invisible variables. Note that the hash tables like Sel0ScoreTable are declareled as static global variables -- they are visible inside this source file.] SideEffects [] ******************************************************************************/ static int GrabCompareScores( const void *ptr1, const void *ptr2) { int item1 = *((int *)ptr1); int item2 = *((int *)ptr2); double *first0, *first, *first2, *first3; double *second0, *second, *second2, *second3; double value0, value, value2, value3; st_lookup(Sel0ScoreTable, (char *)(long)item1, &first0); st_lookup(SelScoreTable, (char *)(long)item1, &first); st_lookup(Sel2ScoreTable, (char *)(long)item1, &first2); st_lookup(Sel3ScoreTable, (char *)(long)item1, &first3); st_lookup(Sel0ScoreTable, (char *)(long)item2, &second0); st_lookup(SelScoreTable, (char *)(long)item2, &second); st_lookup(Sel2ScoreTable, (char *)(long)item2, &second2); st_lookup(Sel3ScoreTable, (char *)(long)item2, &second3); value0 = *second0 - *first0; value = *second - *first; value2 = *second2 - *first2; value3 = *second3 - *first3; if (value0 > 0) return 1; if (value0 < 0) return -1; if (value > 0) return 1; if (value < 0) return -1; return 0; /* Chao: The tie-breakers are not used for this release. We achieved * the best performance on the suite of testing cases at hand * without the tie-breakers. But the code is retained for the * purpose of future experiments. */ if (value2 > 0) return 1; if (value2 < 0) return -1; if (value3 > 0) return 1; if (value3 < 0) return -1; return 0; } /**Function******************************************************************** Synopsis [Add the supporting mddIds into the table.] Description [Add the supporting mddIds into the table.] SideEffects [] ******************************************************************************/ static void GrabMddAppendSupports( mdd_manager *mddManager, mdd_t *mdd1, st_table *supportsTable) { int mddId, k; array_t *supports = mdd_get_support(mddManager, mdd1); arrayForEachItem(int, supports, k, mddId) { if (!st_is_member(supportsTable, (char *)(long)mddId)) st_insert(supportsTable, (char *)(long)mddId, (char *)0); } array_free(supports); } /**Function******************************************************************** Synopsis [Compute the degree of dependence that the abstract model has on the invisible variables.] Description [Compute the degree of dependence that the abstract model has on the invisible variables.] SideEffects [] ******************************************************************************/ static array_t * ComputeDependence( Ntk_Network_t *network, st_table *vertexTable, array_t *leftVars) { array_t *roots, *supports; st_table *supportTable; st_generator *stgen; array_t *dependenceArray = array_alloc(int, array_n(leftVars)); int i,mddId; Ntk_Node_t *node, *node1; int count; /* initialize the scores to 0 */ supportTable = st_init_table(st_ptrcmp, st_ptrhash); arrayForEachItem(int, leftVars, i, mddId) { node = Ntk_NetworkFindNodeByMddId(network, mddId); assert(node); st_insert(supportTable, node, (char *)0); } /* compute the supports of the absFsm */ roots = array_alloc(Ntk_Node_t *, 0); st_foreach_item(vertexTable, stgen, &node, 0) { node = Ntk_LatchReadDataInput(node); array_insert(Ntk_Node_t *, roots, 0, node); supports = Ntk_NodeComputeTransitiveFaninNodes(network, roots, TRUE, FALSE); arrayForEachItem(Ntk_Node_t *, supports, i, node1) { if (st_lookup_int(supportTable, node1, &count)) { count++; st_insert(supportTable, node1, (char *)(long)count); } } array_free(supports); } array_free(roots); /* put into an array */ arrayForEachItem(int, leftVars, i, mddId) { node = Ntk_NetworkFindNodeByMddId(network, mddId); assert(node); st_lookup_int(supportTable, node, &count); array_insert(int, dependenceArray, i, count); } st_free_table(supportTable); return dependenceArray; }