Ignore:
Timestamp:
Jan 13, 2012, 6:32:51 PM (13 years ago)
Author:
cecile
Message:

Fault candidates OK

Location:
vis_dev/vis-2.3/src/debug
Files:
5 edited

Legend:

Unmodified
Added
Removed
  • vis_dev/vis-2.3/src/debug/debug.c

    r41 r42  
    191191array_t          * LTLformulaArray;
    192192char             * ltlFileName     = NIL(char);
    193 
     193array_t          * faultNodes = array_alloc(Ntk_Node_t*,0);
    194194
    195195/*
     
    286286   
    287287
    288         array_t           *objClause = NIL(array_t);
     288        array_t *objClause = NIL(array_t);
    289289        objClause = array_alloc(int, 0);   
    290290        array_insert_last(int, objClause, noLoopIndex);
     
    295295    st_table * nodeToMvfAigTable =  NIL(st_table);
    296296    nodeToMvfAigTable =
    297 (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
    298 assert(nodeToMvfAigTable != NIL(st_table));
     297    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
     298    assert(nodeToMvfAigTable != NIL(st_table));
    299299
    300300    Dbg_InitAbn(abn,manager, nodeToMvfAigTable,cnfClauses);
    301301
    302       //loop abnormal
     302    //loop abnormal
    303303    int aIndex;
    304304    Ntk_Node_t * abnNode;
    305      Dbg_ForEachAbnormal(abn,aIndex,abnNode){
    306      if(aIndex<=0){
    307      //set abnormal
     305    Dbg_ForEachAbnormal(abn,aIndex,abnNode){
     306      char * nodeName =  Ntk_NodeReadName(abnNode);
     307    //set abnormal
    308308      int cnfIndex = array_fetch(int,abn->abnCnfIndexArray, aIndex);
    309309      bAigEdge_t* abnBAig = array_fetch(bAigEdge_t*,abn->abnAigArray, aIndex);
    310310      int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[1],0,cnfClauses);
    311311      array_insert(int,cnfClauses->clauseArray,cnfIndex,abnIndex);
    312 
    313312      FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
    314313      BmcWriteClauses(manager, cnfFile, cnfClauses, options);
    315314      fclose(cnfFile);
    316 
     315     
    317316      //SAT procedure
    318       int res = Dbg_SatCheck("assig",options->cnfFileName);
    319 
    320         array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex);
    321         }
    322      }
     317      //assig assig input from cex
     318      //TODO build cex correctly
     319      int res = Dbg_SatCheck("assig",options->cnfFileName,options->verbosityLevel);
     320      // Build set of FaultCandidates
     321      if (res == SAT_SAT)
     322      {
     323        char * realNodeName = util_strsav(nodeName);
     324        realNodeName[strlen(nodeName)-4] = '\0';
     325        Ntk_Node_t * realNode =  Ntk_NetworkFindNodeByName(network,realNodeName);
     326        array_insert_last(Ntk_Node_t*,faultNodes,realNode);
     327      }
     328
     329
     330      array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex);
     331   }
    323332
    324333         if(verbose)
    325334                (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\
    326                 latches %d nodetomvf.\n",cnfClauses->noOfClauses,st_count(CoiTable),st_count(nodeToMvfAigTable));
    327        
     335                latches %d \n",cnfClauses->noOfClauses,st_count(CoiTable));
     336 
     337        (void) fprintf(vis_stdout,"Number of Fault candidates %d\n",
     338    array_n(faultNodes));
     339        (void) fprintf(vis_stdout,"gates : \n");
     340    printNodeArray(faultNodes);
     341
     342   
    328343Ctlsp_FormulaArrayFree(LTLformulaArray);   
    329344BmcCnfClausesFree(cnfClauses);
    330345BmcOptionFree(options);
     346array_free(faultNodes);
    331347return 0;
    332348 
  • vis_dev/vis-2.3/src/debug/debug.h

    r41 r42  
    134134EXTERN void Dbg_InitAbn(Dbg_Abnormal_t * abn, bAig_Manager_t   * manager,
    135135st_table * nodeToMvfAigTable, BmcCnfClauses_t *cnfClauses);
    136 EXTERN int Dbg_SatCheck(char * forceAssigName, char * cnfFileName);
     136EXTERN int Dbg_SatCheck(char * forceAssigName, char * cnfFileName, int verbose);
    137137EXTERN BmcCnfClauses_t* Dbg_GenerateCNF(Ntk_Network_t * network,
    138138BmcOption_t * option, st_table  *CoiTable);
     139EXTERN int Dbg_GetDefaultValue(Tbl_Table_t * table);
    139140
    140141
  • vis_dev/vis-2.3/src/debug/debugAbnormal.c

    r41 r42  
    4444  with a new table including the abnormal predicate.
    4545  For a combinatorial node n is tranformed into (abn_n)?i_n:n
    46   If the abnormal predicate is activ then n is replaced by a free input]
     46  If the abnormal predicate is active then n is replaced by a free input.
     47  We assume that the combinatorial gate at on one bit only.]
    4748
    4849  SideEffects [fill the abnormal structure]
     
    6768
    6869                Tbl_Table_t    *table =  Ntk_NodeReadTable(node);
    69                 (void) fprintf(vis_stdout, "** old table\n");
    70                 Tbl_TableWriteBlifMvToFile(table,2,vis_stdout);
     70        if(abnormal->verbose){
     71                  (void) fprintf(vis_stdout, "** old table\n");
     72                  Tbl_TableWriteBlifMvToFile(table,2,vis_stdout);
     73        }
    7174                // Build new variables abnormal  and  input
    7275                Ntk_Node_t * abnNode = Dbg_CreateNewNode(ntk,node,"abn");
     
    8184                Tbl_TableAddColumn(table,i,0);
    8285                int iIndex = Tbl_TableReadVarIndex(table, i, 0);
    83 
    84                 //For each row already there in the table
     86       
    8587                int rowNum;
    8688                for(rowNum = 0; rowNum <  Tbl_TableReadNumRows(table);rowNum++){
     
    9496                //the new row
    9597                int r = Tbl_TableAddRow(table);
    96 
     98       
    9799                int colNum;
    98100            for (colNum = 0; colNum < Tbl_TableReadNumInputs(table); colNum++) {
     
    104106                    Tbl_TableSetEntry(table, entry, r, colNum, 0);
    105107                }
     108        int defaultVal = Dbg_GetDefaultValue(table);
     109        if(defaultVal == -1)
     110        {
     111                (void) fprintf(vis_stdout, "Error default value of the table \
     112            of node %s\n", nodeName);
     113            return;
     114        }
     115        int outVal = (defaultVal +1 )% 2;
     116        if(abnormal->verbose)
     117                (void) fprintf(vis_stdout, "Default value : %d\n",defaultVal);
    106118                for (colNum = 0; colNum < Tbl_TableReadNumOutputs(table); colNum++){
    107119                        Tbl_Entry_t * entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
    108                         Tbl_EntrySetValue(entry,1,1);
     120                        Tbl_EntrySetValue(entry,outVal,outVal);
    109121                    Tbl_TableSetEntry(table, entry, r, colNum, 1);
    110122                }
     123        if(abnormal->verbose){
    111124                 printf("---------------\n");
    112125                 Tbl_TableWriteBlifMvToFile(table,0,vis_stdout);
     126        }
    113127          }
    114128        }
  • vis_dev/vis-2.3/src/debug/debugInt.h

    r41 r42  
    8585st_table * generateAllLatches(Ntk_Network_t * ntk);
    8686void mdd_GetState_Values(mdd_manager *mgr, mdd_t * top, FILE * f);
     87void printNodeArray(array_t * nodeArray);
    8788
    8889/**AutomaticEnd***************************************************************/
  • vis_dev/vis-2.3/src/debug/debugUtilities.c

    r41 r42  
    11#include "debug.h"
     2void printNodeArray(array_t * nodeArray)
     3{
     4  int i;
     5  Ntk_Node_t* node;
     6  arrayForEachItem(Ntk_Node_t *, nodeArray, i, node){
     7    printf("%s\n",Ntk_NodeReadName(node));
     8  }
     9
     10
     11}
     12
    213void printLatch(st_table* CoiTable)
    314{
     
    98109******************************************************************************/
    99110
    100 int Dbg_SatCheck(char * forceAssigName, char * cnfFileName
     111int Dbg_SatCheck(char * forceAssigName, char * cnfFileName,int verbose
    101112)
    102113{
     
    138149   sat_Main(cm);
    139150
     151if(verbose){
    140152   if(cm->status == SAT_UNSAT) {
    141153    if(cm->option->forcedAssignArr)
     
    154166    sat_FreeManager(cm);
    155167  }
     168}
    156169return cm->status;
    157170}
     
    192205
    193206}
     207/**Function********************************************************************
     208 
     209  Synopsis    [Return the default value of a Node]
     210
     211  Description [Given a table of a node , return its default value if it exists
     212  else -1   This function only work for binary gate with only one default
     213  value.]
     214  SideEffects []
     215
     216  SeeAlso     []
     217
     218******************************************************************************/
     219int Dbg_GetDefaultValue(Tbl_Table_t * table)
     220{
     221  Tbl_Entry_t * defEntry;
     222  int defIndex;
     223  lsList * rangeList;
     224  Tbl_TableForEachDefaultEntry(table,defEntry,defIndex)
     225  {
     226    rangeList = Tbl_EntryReadList(defEntry);
     227    int length = lsLength(rangeList);
     228    if ( length  != 1)
     229      return -1;
     230    Tbl_Range_t * range;
     231    int valDefault;
     232    lsGen gen;
     233    Tbl_EntryForEachValue(defEntry,valDefault,gen,range){
     234      return Tbl_RangeEnd(range);
     235    }
     236  }
     237}
     238
Note: See TracChangeset for help on using the changeset viewer.