src/grab/grabGrab.c

Go to the documentation of this file.

#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                                                        */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* 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);

/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/

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<nRow; i++) {
    for (j=0; j<nCol; j++) { 
      SelScores[j] += Scores[i*nCol+j]; 
    }
  }

  /* Other selection criteria:
   * (0) when in the BOOLEAN refinement direction, only add bnvs
   * (2) how many absLatches depending on the invisible var?
   * (3) how much will the invisible var cost?
   */  
  Sel0Scores  = ALLOC(double, nCol);
  Sel2Scores  = ALLOC(double, nCol);
  Sel3Scores  = ALLOC(double, nCol);
  tempArray = ComputeDependence(network, absVarTable, invisibleVarMddIds);
  value0 = lsLength(Ntk_NetworkReadNodes(network));
  for (j=0; j<nCol; j++) {
    mddId = array_fetch(int, invisibleVarMddIds, j);
    node = Ntk_NetworkFindNodeByMddId(network, mddId);
    isLatch = (Ntk_NodeTestIsLatch(node));
    /* when refinement is in the BOOLEAN direction, only add bnvs 
     * otherwise, add either latches or bnvs 
     */
    if (refine_direction==0 && !isLatch)
      Sel0Scores[j] = 1.0;
    else
      Sel0Scores[j] = 0.0;      
    /* dependence */
    value = array_fetch(int, tempArray, j);
    Sel2Scores[j] = ((double)value)/st_count(absVarTable);
    /* cost */
    value = GrabNodeComputeFaninNumberTableItem(network, 
                                                nodeToFaninNumberTable,
                                                node);
    Sel3Scores[j] = 1.0 - ((double)value)/value0; 
  }
  array_free(tempArray);

  /* Print out the 'Scores' matrix when requested
   */
  if (verbose >= 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<nRow; i++) {
      for (j=0; j<nCol; j++) { 
        fprintf(vis_stdout, "%+1.2f ", Scores[i*nCol+j]);  
      } 
      fprintf(vis_stdout, "\n"); 
    }
    /* best score in each row */
    for (i=0; i<nRow; i++) {
      int best_local = 0;
      for (j=0; j<nCol; j++) { 
        if (Scores[i*nCol+best_local] < Scores[i*nCol+j])
          best_local = j;
      }
      fprintf(vis_stdout, "best_local: Scores[%d][%d] = %5g\n",
              i, best_local, Scores[i*nCol+best_local]);
    }
  }

  /* Sorting the invisibleVarMddIds according to the Selection Scores 
   */
  Sel0ScoreTable = st_init_table(st_numcmp, st_numhash);
  SelScoreTable  = st_init_table(st_numcmp, st_numhash);
  Sel2ScoreTable = st_init_table(st_numcmp, st_numhash);
  Sel3ScoreTable = st_init_table(st_numcmp, st_numhash);
  arrayForEachItem(int, invisibleVarMddIds, j, mddId) {
    st_insert(Sel0ScoreTable, (char *)mddId, (char *)(Sel0Scores+j));
    st_insert(SelScoreTable,  (char *)mddId, (char *)(SelScores+j));
    st_insert(Sel2ScoreTable, (char *)mddId, (char *)(Sel2Scores+j));
    st_insert(Sel3ScoreTable, (char *)mddId, (char *)(Sel3Scores+j));
  } 

  array_sort(invisibleVarMddIds, GrabCompareScores);

  if (verbose >= 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);
}

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                                            */
/*---------------------------------------------------------------------------*/

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;
}

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;
}
  
 
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);
}


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;
}