src/eqv/eqvVerify.c

Go to the documentation of this file.

#include "eqvInt.h"

static char rcsid[] UNUSED = "$Id: eqvVerify.c,v 1.10 2009/04/11 01:40:06 fabio Exp $";

/*---------------------------------------------------------------------------*/
/* Static function prototypes                                                */
/*---------------------------------------------------------------------------*/


/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

boolean
Eqv_NetworkVerifyCombinationalEquivalence(
  Ntk_Network_t *network1,
  Ntk_Network_t *network2,
  st_table *leavesMap,  /* the mapping between the inputs of the networks;
                         * hash table from Ntk_Node_t * to Ntk_Node_t * */
  st_table *rootsMap,   /* the mapping between the outputs of the networks;
                         * hash table from Ntk_Node_t * to Ntk_Node_t * */
  OFT AssignCommonOrder,
  Part_PartitionMethod method1,
  Part_PartitionMethod method2)
{
  mdd_manager *mddMgr;
  lsList leavesList1, leavesList2;
  lsList rootsList1, rootsList2;
  st_table *leaves1, *leaves2;
  array_t *roots1, *roots2;
  st_generator *gen;
  lsGen listGen;
  graph_t *rootsToLeaves1, *rootsToLeaves2;
  Ntk_Node_t *node1, *node2;
  char *name1, *name2, *name;
  Mvf_Function_t *func1, *func2;
  int num, i, j;
  array_t *mvfRoots1, *mvfRoots2;
  boolean equivalent = TRUE;
  lsList dummy = (lsList) 0;
  int mddId1, mddId2;
  vertex_t *vertex;
  lsGeneric data;
  boolean partValid = FALSE;
  mdd_manager *mgr;
  int mddId;
  array_t *mddIdArray;
  mdd_t *aMinterm, *diff;
  char *mintermName;
  mdd_t *comp1, *comp2;
  int numComponents;

  /* First check whether a partition is registered with network1 */
  if(Ntk_NetworkReadApplInfo(network1, PART_NETWORK_APPL_KEY) != NIL(void)) {
    /*
     * Check whether the registered partition can be used to compute the roots
     * in terms of the leaves. If it can be used, then i won't create a new
     * one.
     */
    partValid = TestPartitionIsValid(network1, rootsMap, leavesMap);
    /*
     * If a partition already exists, an mddManager also exists.
     * So, don't allocate a new one.
     */
    mddMgr = Ntk_NetworkReadMddManager(network1);
  }
  else {
    mddMgr = Ntk_NetworkInitializeMddManager(network1);
  }
  assert(mddMgr != NIL(mdd_manager));
  Ntk_NetworkSetMddManager(network2, mddMgr);
  (*AssignCommonOrder)(network1, network2, leavesMap);

  /* Create lists of leaves and roots for creating partitions. */
  leavesList1 = lsCreate();
  leavesList2 = lsCreate();
  st_foreach_item(leavesMap, gen, &node1, &node2) {
    mddId1 = Ntk_NodeReadMddId(node1);
    mddId2 = Ntk_NodeReadMddId(node2);
    assert(mddId1 == mddId2);
    lsNewEnd(leavesList1, (lsGeneric) node1, LS_NH);
    lsNewEnd(leavesList2, (lsGeneric) node2, LS_NH);
  }

  rootsList1 = lsCreate();
  rootsList2 = lsCreate();
  st_foreach_item(rootsMap, gen, &node1, &node2) {
    lsNewEnd(rootsList1, (lsGeneric) node1, LS_NH);
    lsNewEnd(rootsList2, (lsGeneric) node2, LS_NH);
  }

  if(partValid) {
    rootsToLeaves1 = Part_NetworkReadPartition(network1);
  }
  else {
    rootsToLeaves1 = Part_NetworkCreatePartition(network1, NIL(Hrc_Node_t),
                                                 "dummy", rootsList1,
                                                 leavesList1, NIL(mdd_t),
                                                 method1, dummy,
                                                 FALSE, FALSE, TRUE);
  }

  /*
   * Generate arrays of root and leaf vertices in the first partition
   * to pass as arguments to Part_PartitionCollapse().
   */
  roots1 = array_alloc(vertex_t *, 0);
  lsForEachItem(rootsList1, listGen, data) {
    name = Ntk_NodeReadName((Ntk_Node_t *) data);
    vertex = Part_PartitionFindVertexByName(rootsToLeaves1, name);
    assert(vertex != NIL(vertex_t));
    array_insert_last(vertex_t *, roots1, vertex);
  }
  leaves1 = st_init_table(st_ptrcmp, st_ptrhash);
  lsForEachItem(leavesList1, listGen, data) {
    name = Ntk_NodeReadName((Ntk_Node_t *) data);
    vertex = Part_PartitionFindVertexByName(rootsToLeaves1, name);
/*    assert(vertex != NIL(vertex_t)); */
    if(vertex != NIL(vertex_t)) {
      /*
       * If a leaf is not actually in the support of the roots then
       * it will not be present in the partition.
       */
      mddId = Part_VertexReadMddId(vertex);
      st_insert(leaves1, (char *) vertex, (char *) (long) mddId);
    }
  }

  lsDestroy(rootsList1, (void (*) (lsGeneric)) 0);
  lsDestroy(leavesList1, (void (*) (lsGeneric)) 0);
  rootsToLeaves2 = Part_NetworkCreatePartition(network2, NIL(Hrc_Node_t),
                                               "dummy", rootsList2,
                                               leavesList2, NIL(mdd_t),
                                               method2, dummy, FALSE,
                                               FALSE, TRUE);

  /*
   * Generate arrays of root and leaf vertices in the second partition
   * to pass as arguments to Part_PartitionCollapse().
   */
  roots2 = array_alloc(vertex_t *, 0);
  lsForEachItem(rootsList2, listGen, data) {
    name = Ntk_NodeReadName((Ntk_Node_t *) data);
    vertex = Part_PartitionFindVertexByName(rootsToLeaves2, name);
    assert(vertex != NIL(vertex_t));
    array_insert_last(vertex_t *, roots2, vertex);
  }
  leaves2 = st_init_table(st_ptrcmp, st_ptrhash);
  lsForEachItem(leavesList2, listGen, data) {
    name = Ntk_NodeReadName((Ntk_Node_t *) data);
    vertex = Part_PartitionFindVertexByName(rootsToLeaves2, name);
/*    assert(vertex != NIL(vertex_t)); */
    if(vertex != NIL(vertex_t)) {
      /*
       * If a leaf is not actually in the support of the roots then
       * it will not be present in the partition.
       */
      mddId = Part_VertexReadMddId(vertex);
      st_insert(leaves2, (char *) vertex, (char *) (long) mddId);
    }
  }
  lsDestroy(rootsList2, (void (*) (lsGeneric)) 0);
  lsDestroy(leavesList2, (void (*) (lsGeneric)) 0);
  assert(Part_PartitionReadMddManager(rootsToLeaves1) ==
         Part_PartitionReadMddManager(rootsToLeaves2));

  mvfRoots1 = Part_PartitionCollapse(rootsToLeaves1, roots1, leaves1, NIL(mdd_t));
  mvfRoots2 = Part_PartitionCollapse(rootsToLeaves2, roots2, leaves2, NIL(mdd_t));

  assert(array_n(mvfRoots1) == array_n(mvfRoots2));
  num = array_n(mvfRoots1);
  mddIdArray = array_alloc(int, 0);
  st_foreach_item_int(leaves1, gen, &vertex, &mddId) {
    array_insert_last(int, mddIdArray, mddId);
  }

  /*
   * For each pair of corresponding outputs in the two arrays mvfRoots1 and
   * mvfRoots2, I will compute the mdd representing all the input combinations
   * for which they are different. For each pair, I will print one input
   * combination for which they are different.
   */

  for(i = 0; i<num; ++i) {
    func1 = array_fetch(Mvf_Function_t *, mvfRoots1, i);
    func2 = array_fetch(Mvf_Function_t *, mvfRoots2, i);
    if(!Mvf_FunctionTestIsEqualToFunction(func1, func2)) {
      mgr = Mvf_FunctionReadMddManager(func1);
      assert(mgr == Mvf_FunctionReadMddManager(func2));
      numComponents = Mvf_FunctionReadNumComponents(func1);
      for(j=0; j<numComponents; ++j) {
        comp1 = Mvf_FunctionReadComponent(func1, j);
        comp2 = Mvf_FunctionReadComponent(func2, j);
        diff = mdd_xor(comp1, comp2);
        if(!mdd_is_tautology(diff, 0)) {
          aMinterm = Mc_ComputeAMinterm(diff, mddIdArray, mddMgr);
          mintermName = Mc_MintermToString(aMinterm, mddIdArray, network1);
          vertex = array_fetch(vertex_t *, roots1, i);
          name1 = Part_VertexReadName(vertex);
          vertex = array_fetch(vertex_t *, roots2, i);
          name2 = Part_VertexReadName(vertex);
          (void) fprintf(vis_stdout, "%s from network1 and %s from network2 differ on input values\n%s",
                         name1, name2, mintermName);
          FREE(mintermName);
          mdd_free(aMinterm);
          mdd_free(diff);
          break;
        }
        mdd_free(diff);
      }
      equivalent = FALSE;
    }
  }
  array_free(mddIdArray);
  if(!partValid) {
    Part_PartitionFree(rootsToLeaves1);
  }
  Part_PartitionFree(rootsToLeaves2);
  array_free(roots1);
  array_free(roots2);
  st_free_table(leaves1);
  st_free_table(leaves2);
  arrayForEachItem(Mvf_Function_t *, mvfRoots1, i, func1) {
    Mvf_FunctionFree(func1);
  }
  array_free(mvfRoots1);
  arrayForEachItem(Mvf_Function_t *, mvfRoots2, i, func2) {
    Mvf_FunctionFree(func2);
  }
  array_free(mvfRoots2);
  Ntk_NetworkSetMddManager(network2, NIL(mdd_manager));
  /*
   * This is needed because Ntk_NetworkFree() will be called on both network1
   * and network2.
   */
  return equivalent;
}

boolean
Eqv_NetworkVerifySequentialEquivalence(
  Ntk_Network_t *network1,
  Ntk_Network_t *network2,
  st_table *rootsTable,    /* the mapping between the outputs of the networks;
                            * hash table from char * to char * */
  st_table *leavesTable,   /* the mapping between the inputs of the networks;
                            * hash table from char * to char * */
  Part_PartitionMethod partMethod,
  boolean useBackwardReach,
  boolean reordering)
{
  array_t *roots;
  st_table *leaves;
  lsList rootsList;
  lsList rootsPartList = (lsList) 0;
  st_table *outputMap = NIL(st_table);
  Ntk_Node_t *node1, *node2, *node;
  char *name1, *name2, *temp;
  st_generator *gen;
  lsGen listGen;
  graph_t *partition;
  vertex_t *vertex;
  mdd_manager *mddMgr;
  array_t *mvfArray;
  Mvf_Function_t *mvf1, *mvf2;
  mdd_t *badStates, *initialStates;
  mdd_t *mddTemp, *mdd1, *mdd2, *tautology;
  mdd_t *mddComp1, *mddComp2;
  int n, i, j, numComponents;
  int id;
  array_t *inputIdArray;
  lsList dummy = (lsList) 0;
  lsGeneric data;
  Ntk_Node_t *input;
  Fsm_Fsm_t *modelFsm;
  array_t *onionRings;
  array_t *aPath;
  boolean inequivalent;
  boolean rootsFlag = (rootsTable == NIL(st_table)) ? FALSE : TRUE;
  array_t *careStatesArray = array_alloc(mdd_t *, 0);

  /* If rootsFlag is FALSE, all primary outputs are to be verified */
  if(rootsFlag == FALSE) {
    outputMap = MapPrimaryOutputsByName(network1, network2);
  }

  /*
   * If leavesFlag is FALSE, the primary inputs in the two networks are
   * assumed to have same names. In the network returned by
   * Ntk_NetworkAppendNetwork(), the two corresponding nodes will be merged.
   * If leavesFlag is TRUE, the name correspondence between the primary inputs
   * in the two networks is specified in leavesTable.
   */
  if(leavesTable == NIL(st_table)) {
    st_table *emptyTable = st_init_table(strcmp, st_strhash);
    Ntk_NetworkAppendNetwork(network2, network1, emptyTable);
    st_free_table(emptyTable);
  }
  else {
    Ntk_NetworkAppendNetwork(network2, network1, leavesTable);
  }

  /*
   * network1 has been appended to the erstwhile network2, and the new network
   * is now called network2.
   */

  mddMgr = Ntk_NetworkInitializeMddManager(network2);

  Ord_NetworkOrderVariables(network2, Ord_RootsByDefault_c,
                            Ord_NodesByDefault_c, FALSE, Ord_InputAndLatch_c,
                            Ord_Unassigned_c, dummy, FALSE);

  if (reordering)
    Ntk_NetworkSetDynamicVarOrderingMethod(network2, BDD_REORDER_SIFT,
                                           BDD_REORDER_VERBOSITY);
  /*
   * Ntk_NetworkAppendNetwork() adds $NTK2 to the names of all the
   * appended nodes. I want to find the appended nodes in new network2
   * corresponding to the roots in network1. I will add all these nodes to
   * rootsList. I will also add all the roots of the erstwhile network2, which
   * exist in the network2 also. rootsList will finally contain all the nodes
   * in network2 whose mdds have to be created by Part_Partition Collapse().
   */

  rootsList = lsCreate();
  if(rootsFlag == FALSE) {
    st_foreach_item(outputMap, gen, &node1, &node2) {
      name1 = Ntk_NodeReadName(node1);
      temp = util_strcat3(name1, "$NTK2", "");
      name1 = temp;
      node1 = Ntk_NetworkFindNodeByName(network2, name1);
      assert(node1 != NIL(Ntk_Node_t));
      FREE(name1);
      lsNewEnd(rootsList, (lsGeneric) node1, LS_NH);
      lsNewEnd(rootsList, (lsGeneric) node2, LS_NH);
    }
  }
  else {
    st_foreach_item(rootsTable, gen, &name1, &name2) {
      /* I am finding the node in the new network2 */
      temp = util_strcat3(name1, "$NTK2", "");
      name1 = temp;
      node1 = Ntk_NetworkFindNodeByName(network2, name1);
      FREE(name1);
      lsNewEnd(rootsList, (lsGeneric) node1, LS_NH);
      node2 = Ntk_NetworkFindNodeByName(network2, name2);
      lsNewEnd(rootsList, (lsGeneric) node2, LS_NH);
    }
  }
  if(outputMap) {
    st_free_table(outputMap);
  }
  /* rootsPartList is the list of nodes which will passed to
   * Part_NetworkCreatePartition(). I want all the next state functions i.e.
   * latch data inputs as well as everything in rootsList to be in
   * rootsPartList. If rootsFlag is FALSE, rootsPartList is simply passed as
   * (lsList) 0.
   */
  if(rootsFlag) {
    rootsPartList = lsCreate();
    Ntk_NetworkForEachCombOutput(network2, listGen, node) {
      if(Ntk_NodeTestIsLatchDataInput(node) ||
         Ntk_NodeTestIsLatchInitialInput(node)){
        lsNewEnd(rootsPartList, (lsGeneric) node, LS_NH);
      }
    }
    lsForEachItem(rootsList, listGen, node) {
      if(!Ntk_NodeTestIsLatchDataInput(node) &&
         !Ntk_NodeTestIsLatchInitialInput(node)) {
        lsNewEnd(rootsPartList, (lsGeneric) node, LS_NH);
      }
    }
  }
  partition = Part_NetworkCreatePartition(network2, NIL(Hrc_Node_t), "dummy",
                                          rootsPartList,
                                          (lsList) 0, NIL(mdd_t), partMethod,
                                          dummy, FALSE, FALSE, TRUE);

  Ntk_NetworkAddApplInfo(network2, PART_NETWORK_APPL_KEY,
                         (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
                         (void *) partition);
  if(rootsPartList) {
    lsDestroy(rootsPartList, (void (*) (lsGeneric)) 0);
  }
  /* Create roots and leaves for Part_PartitionCollapse().
   */
  roots = array_alloc(vertex_t *, 0);
  lsForEachItem(rootsList, listGen, data) {
    name1 = Ntk_NodeReadName((Ntk_Node_t *) data);
    vertex = Part_PartitionFindVertexByName(partition, name1);
    assert(vertex != NIL(vertex_t));
    array_insert_last(vertex_t *, roots, vertex);
  }
  lsDestroy(rootsList, (void (*) (lsGeneric)) 0);
  leaves = st_init_table(st_ptrcmp, st_ptrhash);
  Ntk_NetworkForEachCombInput(network2, listGen, node1) {
    name1 = Ntk_NodeReadName(node1);
    vertex = Part_PartitionFindVertexByName(partition, name1);
    if(vertex != NIL(vertex_t)) {
      /* A combinational input might not be present in the support of any
         node in rootsPartList. If so, it will not be present in the partition
         also. */
      st_insert(leaves, (char *) vertex, (char *) (long) 0);
    }
  }
  mvfArray = Part_PartitionCollapse(partition, roots, leaves, NIL(mdd_t));
  array_free(roots);
  st_free_table(leaves);
  n = array_n(mvfArray);
  assert(n%2 == 0);
  n = n/2;
  assert(mddMgr != NULL);

/* In mvfArray, the mvfs of corresponding nodes occur one after the other,
   * because of the way rootsList was created. badStates will ultimately
   * contain all the states for which  any pair of corresponding nodes differ
   * for some input.
   */
  badStates = mdd_zero(mddMgr);
  for(i=0; i<n; i++) {
    mvf1 = array_fetch(Mvf_Function_t *, mvfArray, 2*i);
    mvf2 = array_fetch(Mvf_Function_t *, mvfArray, 2*i +1);
    numComponents = Mvf_FunctionReadNumComponents(mvf1);
    mdd2 = mdd_zero(mddMgr);
    /*
     * Hopefully, mddMgr of the partition is the same as the mddMgr of the
     * MVFs.
     */
    for(j=0; j<numComponents; j++) {
      mddComp1 = Mvf_FunctionObtainComponent(mvf1, j);
      mddComp2 = Mvf_FunctionObtainComponent(mvf2, j);
      mdd1 = mdd_and(mddComp1, mddComp2, 1, 1);
      mdd_free(mddComp1);
      mdd_free(mddComp2);
      mddTemp = mdd_or(mdd2, mdd1, 1, 1);
      mdd_free(mdd1);
      mdd_free(mdd2);
      mdd2 = mddTemp;
    }

   /*
    * At this point, mdd2 represents the set of input and present state
    * combinations in which mvf1 and mvf2 produce the same value. I want the
    * set for which mvf1 and mvf2 are different.
    */
    mddTemp = mdd_or(badStates, mdd2, 1, 0);
    mdd_free(mdd2);
    mdd_free(badStates);
    badStates = mddTemp;
  }
  arrayForEachItem(Mvf_Function_t *, mvfArray, i, mvf1) {
    Mvf_FunctionFree(mvf1);
  }
  array_free(mvfArray);
  /* existentially quantify out the input variables */
  inputIdArray = array_alloc(int, 0);

  Ntk_NetworkForEachPrimaryInput(network2, listGen, input) {
    id = Ntk_NodeReadMddId(input);
    assert(id >= 0);
    array_insert_last(int, inputIdArray, id);
  }

  mddTemp = mdd_smooth(mddMgr, badStates, inputIdArray);
  mdd_free(badStates);
  badStates = mddTemp;
  array_free(inputIdArray);
  modelFsm = Fsm_FsmCreateFromNetworkWithPartition(network2, NIL(graph_t));
  assert(modelFsm != NIL(Fsm_Fsm_t));
  Ntk_NetworkAddApplInfo(network2, FSM_NETWORK_APPL_KEY,
                         (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
                         (void *) modelFsm);

  onionRings = array_alloc(mdd_t *, 0);
  initialStates = Fsm_FsmComputeInitialStates(modelFsm);
  tautology = mdd_one(mddMgr);

  /* Model checking function */
  if (useBackwardReach == TRUE) {
    array_insert(mdd_t *, careStatesArray, 0, tautology);
    inequivalent = Mc_FsmComputeStatesReachingToSet(modelFsm, badStates,
                        careStatesArray, initialStates,
                        onionRings, McVerbosityNone_c, McDcLevelNone_c);
    array_free(careStatesArray);
    mdd_free(badStates);
    mdd_free(tautology);

    if (inequivalent) {
      mdd_t *outerOnionRing = array_fetch_last(mdd_t *, onionRings);
      mdd_t *badInitialStates = mdd_and(initialStates, outerOnionRing, 1, 1);
      array_t *psVarMddIdArray = Fsm_FsmReadPresentStateVars(modelFsm);
      mdd_t *aBadInitialState = Mc_ComputeAMinterm(initialStates, psVarMddIdArray, mddMgr);
      mdd_free(badInitialStates);
      aPath = Mc_BuildPathToCore(aBadInitialState, onionRings, modelFsm,
                                 McGreaterOrEqualZero_c);
      (void) Mc_PrintPath(aPath, modelFsm, TRUE); /* TRUE -> print inputs on path */
      mdd_free(aBadInitialState);
      mdd_free(initialStates);
      mdd_array_free(aPath);
      mdd_array_free(onionRings);
      return FALSE;
    }
    else {
      mdd_free(initialStates);
      return TRUE;
    }
  }
  else { /* do forward search */
    array_insert(mdd_t *, careStatesArray, 0, tautology);
    inequivalent = Mc_FsmComputeStatesReachableFromSet(modelFsm, initialStates,
                        careStatesArray, badStates, onionRings,
                        McVerbosityNone_c, McDcLevelNone_c);
    array_free(careStatesArray);
    mdd_free(tautology);
    mdd_free(initialStates);

    if (inequivalent) {
      mdd_t *outerOnionRing = array_fetch_last(mdd_t *, onionRings);
      mdd_t *reachableBadStates = mdd_and(badStates, outerOnionRing, 1, 1);
      array_t *psVarMddIdArray = Fsm_FsmReadPresentStateVars(modelFsm);
      mdd_t *aBadReachableState = Mc_ComputeAMinterm(reachableBadStates, psVarMddIdArray, mddMgr);
      mdd_free(reachableBadStates);
      psVarMddIdArray = Fsm_FsmReadPresentStateVars(modelFsm);
      aPath = Mc_BuildPathFromCore(aBadReachableState, onionRings, modelFsm,
                                 McGreaterOrEqualZero_c);
      (void) Mc_PrintPath(aPath, modelFsm, TRUE); /* TRUE -> print inputs on path */
      mdd_free(aBadReachableState);
      mdd_free(badStates);
      mdd_array_free(aPath);
      mdd_array_free(onionRings);
      return FALSE;
    }
    else {
      mdd_free(badStates);
      return TRUE;
    }
  }
}

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


/*---------------------------------------------------------------------------*/
/* Definition of static functions                                            */
/*---------------------------------------------------------------------------*/