src/grab/grabBMC.c

Go to the documentation of this file.

#include "grabInt.h"
#include "bmcInt.h"

/*---------------------------------------------------------------------------*/
/* Constant declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Structure declarations                                                    */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Type declarations                                                         */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Variable declarations                                                     */
/*---------------------------------------------------------------------------*/

/*---------------------------------------------------------------------------*/
/* Macro declarations                                                        */
/*---------------------------------------------------------------------------*/

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

static bAigEdge_t GrabConvertBddToBaig(bAig_Manager_t *bAigManager, bdd_t *fn, st_table *bddidToNames);
static st_table * GrabBddGetSupportBaigNames(mdd_manager *mddManager, mdd_t *f);
static char * GrabBddIdToBaigNames(mdd_manager *mddManager, int bddid);

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

boolean
Bmc_AbstractCheckAbstractTraces(
  Ntk_Network_t *network,
  array_t *synOnionRings,
  st_table *absLatches,
  int verbose, 
  int dbgLevel,
  int printInputs)
{
  int               pathLength = array_n(synOnionRings) -1;
  mAig_Manager_t    *maigManager = Ntk_NetworkReadMAigManager(network);
  st_table          *nodeToMvfAigTable = NIL(st_table); 
  BmcCnfClauses_t   *cnfClauses;
  FILE              *cnfFile;
  BmcOption_t       *options;
  array_t           *result;
  int               i;
  boolean           CexExit = FALSE;
  
  nodeToMvfAigTable =
    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
  if (nodeToMvfAigTable == NIL(st_table)){
    fprintf(vis_stderr, 
            "** bmc error: please run buid_partiton_maigs first\n");
    return CexExit;
  }

  options = BmcOptionAlloc();
  if (verbose) { 
    options->dbgLevel = dbgLevel;
    options->printInputs = printInputs;
  }
  options->satInFile = BmcCreateTmpFile();
  if (options->satInFile == NIL(char)){
    BmcOptionFree(options);
    return CexExit;
  }

  /* create SAT Solver output file */
  options->satOutFile = BmcCreateTmpFile();
  if (options->satOutFile == NIL(char)){
    BmcOptionFree(options);
    fprintf(vis_stderr, "** bmc error: Cannot allocate a temp file name\n");
    return CexExit;
  }
  cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);  
  if (cnfFile == NIL(FILE)) {
    BmcOptionFree(options);
    fprintf(vis_stderr, "** bmc error: Cannot create CNF output file %s\n",
            options->satInFile);
    return CexExit;
  }

  /* Unroll the model exactly 'pathLength' time frames
   */
  cnfClauses = BmcCnfClausesAlloc();
  BmcCnfGenerateClausesForPath(network, 0, pathLength, BMC_INITIAL_STATES,
                               cnfClauses, nodeToMvfAigTable, absLatches);

  /* Generate the constraints from the abstract paths
   *   (1) build a bAigEdge_t (graph) for each ring
   *   (2) add all the cnf clauses that describe this graph
   *   (3) make the output bAigEdge_t equals to 1
  */
  {
    bAigEdge_t  bAigState;
    mdd_manager *mddManager = Ntk_NetworkReadMddManager(network);
    array_t     *clause = array_alloc(int, 1);
    mdd_t       *ring;

    arrayForEachItem(mdd_t *, synOnionRings, i, ring) {
      st_table *bddidTobAigNames;
      bddidTobAigNames = GrabBddGetSupportBaigNames(mddManager, ring);
      bAigState = GrabConvertBddToBaig(maigManager, ring, bddidTobAigNames);
      {
        st_generator *stgen;
        long tmpId;
        char *tmpStr;
        st_foreach_item(bddidTobAigNames, stgen, &tmpId, &tmpStr) {
          FREE(tmpStr);
        }
        st_free_table(bddidTobAigNames);
      }
      array_insert(int, clause, 0, BmcGenerateCnfFormulaForAigFunction(
                                  maigManager, bAigState, i, cnfClauses));
      BmcCnfInsertClause(cnfClauses, clause);
    } 
   
    array_free(clause);
  } 

  /* Call the SAT solver 
   */
  BmcWriteClauses(maigManager, cnfFile, cnfClauses, options); 
  fclose(cnfFile);
  result = BmcCheckSAT(options);
  if(result != NIL(array_t)){
    if (verbose >= 1 && dbgLevel ==1) {
      fprintf(vis_stdout,"Found Counterexample of length = %d\n", pathLength);
      BmcPrintCounterExample(network, nodeToMvfAigTable, cnfClauses,
                             result, pathLength+1, absLatches, options, 
                             NIL(array_t));
    }
    if (verbose >=1 && dbgLevel == 2) {
      BmcPrintCounterExampleAiger(network, nodeToMvfAigTable, cnfClauses,
                             result, pathLength+1, absLatches, options,
                             NIL(array_t));
    }   
    CexExit = TRUE;
  }  

  /* free all used memories */
  BmcCnfClausesFree(cnfClauses);
  array_free(result);
  BmcOptionFree(options);

  return CexExit;
}


boolean
Bmc_AbstractCheckAbstractTracesWithFineGrain(
  Ntk_Network_t *network,
  st_table *coiBnvTable,
  array_t *synOnionRings,
  st_table *absLatches,
  st_table *absBnvs)
{
  boolean             result;
  mAigManagerState_t  oldMaigState;  /* to store the previous AIG */
  mAig_Manager_t      *maigManager;
  lsGen               lsgen;
  Ntk_Node_t          *node;
  int                 mAigId;
  int                 i;
  st_generator        *stgen;
  st_table            *leaves;
  array_t             *roots, *combInputs;

  /* save the existing maigManager */
  oldMaigState.manager = Ntk_NetworkReadMAigManager(network);
  oldMaigState.nodeToMvfAigTable =  
    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
  oldMaigState.nodeToMAigIdTable = st_init_table(st_ptrcmp, st_ptrhash);
  Ntk_NetworkForEachNode(network, lsgen, node) {
    mAigId = Ntk_NodeReadMAigId(node);
    st_insert(oldMaigState.nodeToMAigIdTable, node, (char *)(long)mAigId);
    Ntk_NodeSetMAigId(node, ntmaig_UNUSED);
  }

  /* create a new maigManager */
  maigManager = mAig_initAig();
  Ntk_NetworkSetMAigManager(network, maigManager);
  Ntk_NetworkSetApplInfo(network, MVFAIG_NETWORK_APPL_KEY,
                         (Ntk_ApplInfoFreeFn) ntmAig_MvfAigTableFreeCallback,
                         (void *) st_init_table(st_ptrcmp, st_ptrhash));

  /* roots are the visible latches, and the visible bnvs (some bnvs
   * may not be in the transitive fan-in cone of the visible latches
   */
  roots = array_alloc(Ntk_Node_t *, 0);
  st_foreach_item(absLatches, stgen, &node, NIL(char *)) {
    array_insert_last(Ntk_Node_t *, roots, Ntk_LatchReadDataInput(node));
    array_insert_last(Ntk_Node_t *, roots, Ntk_LatchReadInitialInput(node));
  }
  st_foreach_item(absBnvs, stgen, &node, NIL(char *)) {
    array_insert_last(Ntk_Node_t *, roots, node);
  }

  combInputs = Ntk_NodeComputeTransitiveFaninNodes(network, roots, 
                                                   TRUE, /* stopAtLatches */
                                                   FALSE /* combInputsOnly*/
                                                   );

  /* leaves are the combinational inputs or the invisible bnvs */
  leaves = st_init_table(st_ptrcmp, st_ptrhash);
  arrayForEachItem(Ntk_Node_t *, combInputs, i, node) {
    if ( Ntk_NodeTestIsCombInput(node) ||
         ( st_is_member(coiBnvTable, node) &&
           !st_is_member(absBnvs, node) ) ) {
      st_insert(leaves, node, (char *) ntmaig_UNUSED);
      Ntk_NodeSetMAigId(node, mAig_CreateVar(maigManager,
                                             Ntk_NodeReadName(node),
                   Var_VariableReadNumValues(Ntk_NodeReadVariable(node))));
    }
  }
  st_foreach_item(absLatches, stgen, &node, NIL(char *)) {
    if (!st_is_member(leaves, node)) {
      st_insert(leaves, node, (char *) ntmaig_UNUSED);
      Ntk_NodeSetMAigId(node, mAig_CreateVar(maigManager,
                                             Ntk_NodeReadName(node),
                   Var_VariableReadNumValues(Ntk_NodeReadVariable(node))));
    }
  }
  array_free(combInputs);

#if 1
  /* THIS SEEMS UNNECESSARY---IT'S HERE TO AVOID ERRORS IN CALLING
   * ntmaig_NetworkBuildMvfAigs()
   */
  Ntk_NetworkForEachCombInput(network, lsgen, node) {
    if (Ntk_NodeReadMAigId(node) == NTK_UNASSIGNED_MAIG_ID) {
      Ntk_NodeSetMAigId(node, mAig_CreateVar(maigManager,
                                             Ntk_NodeReadName(node),
                   Var_VariableReadNumValues(Ntk_NodeReadVariable(node))));
    } 
  }
#endif

  /* build the new AIG graph */
  ntmaig_NetworkBuildMvfAigs(network, roots, leaves);

  array_free(roots);
  st_free_table(leaves);


  /* check the existence of the abstract path on the new AIG graph */
  result = Bmc_AbstractCheckAbstractTraces(network,
                                           synOnionRings,
                                           absLatches,
                                           0, 0, 0);

  /* restore the previous maigManager */
  mAig_quit(maigManager);
  Ntk_NetworkFreeApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
  Ntk_NetworkSetMAigManager(network, oldMaigState.manager);
  Ntk_NetworkSetApplInfo(network, MVFAIG_NETWORK_APPL_KEY,
                         (Ntk_ApplInfoFreeFn) ntmAig_MvfAigTableFreeCallback,
                         (void *) oldMaigState.nodeToMvfAigTable);
  st_foreach_item(oldMaigState.nodeToMAigIdTable, stgen, &node,
                  &mAigId) {
    Ntk_NodeSetMAigId(node, mAigId);
  }
  st_free_table(oldMaigState.nodeToMAigIdTable);

  return result;
}

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

static bAigEdge_t
GrabConvertBddToBaig(
   bAig_Manager_t *bAigManager,
   bdd_t          *fn,
   st_table       *bddidToNames)
{
  bdd_gen     *gen;
  bdd_node    *node, *thenNode, *elseNode, *funcNode;
  bdd_manager *bddManager = bdd_get_manager(fn);
  bdd_node    *one  = bdd_read_one(bddManager);
  /*bdd_node    *zero = bdd_read_logic_zero(bddManager);*/
  int         is_complemented;
  int         flag;
  bAigEdge_t  var, left, right, result;
  char        *name;
  st_table    *bddTObaigTable;
  
  bddTObaigTable = st_init_table(st_numcmp, st_numhash);

  if (fn == NULL){
    return bAig_NULL;
  }
  
  st_insert(bddTObaigTable, (char *) (long) bdd_regular(one),  
            (char *) bAig_One);

  funcNode = bdd_get_node(fn, &is_complemented);
  
  if (bdd_is_constant(funcNode)){
    flag = st_lookup(bddTObaigTable, 
                     (char *) (long) (funcNode),
                     &result);
    assert(flag);
    st_free_table(bddTObaigTable);

    if (is_complemented)
      return bAig_Not(result);
    else
      return result;
  }
  
  foreach_bdd_node(fn, gen, node){
    /* if the node has been processed, skip it. (the constant ONE
     * should be the only node falls into this category).
     */
    if (st_is_member(bddTObaigTable, (char *) (long) bdd_regular(node)))
      continue;
    
    /*  bdd_node_read_index() return the current level's bddId */
    if (bddidToNames) {
      flag = st_lookup(bddidToNames, (char *)(long)bdd_node_read_index(node),
                       &name);
      assert(flag);
      name = util_strsav(name);
    }else {
      char tempString[1024];
      sprintf(tempString, "BDD%d", bdd_node_read_index(node));
      name = util_strsav(tempString);
    }

    /*  Create or Retrieve the bAigEdge_t  w.r.t. 'name' */
    var  = bAig_CreateVarNode(bAigManager, name);
    FREE(name);

    thenNode  = bdd_bdd_T(node);
    flag = st_lookup(bddTObaigTable, (char *) (long) bdd_regular(thenNode),
                     &left);
    assert(flag);
      
    elseNode  = bdd_bdd_E(node);
    flag = st_lookup(bddTObaigTable, (char *) (long) bdd_regular(elseNode),
                      &right);
    assert(flag);

    /* should we test here whether elseNode is complemented arc? */
    if (bdd_is_complement(elseNode))
      right = bAig_Not(right);

    result =  bAig_Or(bAigManager, bAig_And(bAigManager, var, left),
                                   bAig_And(bAigManager, bAig_Not(var), right));
    st_insert(bddTObaigTable, (char *) (long) bdd_regular(node),
              (char *) (long) result);
  }
  flag = st_lookup(bddTObaigTable, (char *) (long) bdd_regular(funcNode),
                    &result);  
  assert(flag);
  st_free_table(bddTObaigTable);

  if (is_complemented){
    return bAig_Not(result);
  } else {
    return result;
  }
} /* end of bAig_bddtobAig() */


static st_table *
GrabBddGetSupportBaigNames(
  mdd_manager *mddManager,
  mdd_t *f)
{
  int        numOfVars = bdd_num_vars(mddManager);
  st_table  *bddidTObaigNames = st_init_table(st_numcmp, st_numhash);
  var_set_t *vset;
  int        i;

  vset = bdd_get_support(f);
  for (i=0; i<numOfVars; i++) {
    if (var_set_get_elt(vset, i) == 1) {
      st_insert(bddidTObaigNames, (char *)(long)i, 
                GrabBddIdToBaigNames(mddManager, i));
    }
  }
  var_set_free(vset);

  return bddidTObaigNames;
}

static char *
GrabBddIdToBaigNames(
  mdd_manager *mddManager,
  int            bddid)
{
  array_t *mvar_list = mdd_ret_mvar_list(mddManager);
  array_t *bvar_list = mdd_ret_bvar_list(mddManager);
  bvar_type bv;
  mvar_type mv;
  int     mddid, index, id;
  char    *nodeName;
  char    baigName[1024];

  /* 1. from bddid, get mddid and the index of this bddid in the mddid 
   */
  bv = array_fetch(bvar_type, bvar_list, bddid);
  mddid = bv.mvar_id;
  mv = array_fetch(mvar_type, mvar_list, mddid);
  arrayForEachItem(int, mv.bvars, index, id) {
    if (id == bddid) 
      break;
  }
  assert(index <= mv.encode_length -1);
  
  /* 2. assumptions: (1) mv.name = nodeName,  
   *                 (2) index is the same for MDD and MAIG
   */
  nodeName = mv.name;
  
  /* 3. the baigEdge_t's name is ("%s_%d",nodeName,index)
   */
  sprintf(baigName, "%s_%d", nodeName, index);

  return util_strsav(baigName);
}