Changeset 35 for vis_dev/vis-2.3


Ignore:
Timestamp:
Jan 3, 2012, 11:12:40 AM (13 years ago)
Author:
cecile
Message:

modify mv table

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

Legend:

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

    r30 r35  
    77  Synopsis    [Debug package initialization, ending, and the command debug]
    88
    9   Author      [Originated from SIS.]
     9  Author      [Cecile B.]
    1010
    1111  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
     
    6161/*---------------------------------------------------------------------------*/
    6262
     63static int CommandSatDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
    6364static int CommandDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
    6465static int CommandTransition(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
     66static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
    6567
    6668
     
    8890   * underscore, the command will be listed under "help -a" but not "help".
    8991   */
    90   Cmd_CommandAdd("_debug_test", CommandDebug, /* doesn't changes_network */ 0);
    91   Cmd_CommandAdd("_transition",  CommandTransition,      0);
     92  Cmd_CommandAdd("_debug_test",  CommandDebug, /* doesn't changes_network */ 0);
     93  Cmd_CommandAdd("_transition",  CommandTransition, 1);
     94  Cmd_CommandAdd("_sat_debug",   CommandSatDebug, 0);
     95  Cmd_CommandAdd("_createAbn",   CommandCreateAbnormal, 1);
    9296
    9397}
     
    122126/*---------------------------------------------------------------------------*/
    123127
     128
     129static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int  argc, char ** argv)
     130{
     131  Ntk_Network_t * ntk;
     132  ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
     133  if (ntk == NIL(Ntk_Network_t)) {
     134        (void) fprintf(vis_stdout, "** abn error: No network\n");
     135        return 1;
     136  }
     137  lsGen gen;
     138  Ntk_Node_t* node;
     139
     140  (void) fprintf(vis_stdout, "** NODE **\n");
     141  Ntk_NetworkForEachNode(ntk,gen,node){
     142          if(Ntk_NodeTestIsCombinational(node)){
     143                if(Ntk_NodeReadNumFanins(node) > 1 && Ntk_NodeReadNumFanouts(node)> 0)
     144                {
     145                  if(strcmp(Ntk_NodeReadName(node),"_n2")==0)
     146                  {
     147                        char * nodeName = util_strsav(Ntk_NodeReadName(node));
     148                printf("%s \n",  nodeName);
     149                        (void) fprintf(vis_stdout, "** read table\n");
     150                        Tbl_Table_t    *table =  Ntk_NodeReadTable(node);
     151
     152                        Tbl_TableWriteBlifMvToFile(table,2,vis_stdout);
     153                        // Build new variables abnormal  and  input
     154                        //abn
     155                        char * abnName = (char *) malloc(strlen(nodeName) + 5);
     156                        sprintf(abnName,"abn_%s",Ntk_NodeReadName(node));
     157                        Var_Variable_t * abn = Var_VariableAlloc(NIL(Hrc_Node_t),abnName);
     158                        Ntk_Node_t * newNode = Ntk_NodeCreateInNetwork(ntk, abnName,abn);
     159                        Ntk_NodeDeclareAsPrimaryInput(newNode);
     160                        //new free inputs
     161                        char * iName = (char *) malloc(strlen(nodeName) + 3);
     162                        sprintf(iName,"i_%s",Ntk_NodeReadName(node));
     163                        Var_Variable_t * i = Var_VariableAlloc(NIL(Hrc_Node_t),iName);
     164                        Ntk_Node_t * newNode2 = Ntk_NodeCreateInNetwork(ntk, iName, i);
     165                        Ntk_NodeDeclareAsPrimaryInput(newNode2);
     166                        //Add in the table
     167                        Tbl_TableAddColumn(table,abn,0);
     168                        int abnIndex = Tbl_TableReadVarIndex(table, abn, 0);
     169                        Tbl_TableAddColumn(table,i,0);
     170                        int iIndex = Tbl_TableReadVarIndex(table, i, 0);
     171
     172                        //For each row already there in the table
     173                        int rowNum;
     174                        for(rowNum = 0; rowNum <  Tbl_TableReadNumRows(table);rowNum++){
     175                                Tbl_Entry_t *abnEntry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
     176                                Tbl_EntrySetValue(abnEntry,0,0);
     177                                Tbl_TableSetEntry(table, abnEntry, rowNum, abnIndex, 0);
     178                                Tbl_Entry_t *iEntry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
     179                                Tbl_EntrySetValue(iEntry,0,1);
     180                                Tbl_TableSetEntry(table, iEntry, rowNum, iIndex, 0);
     181                        }
     182                        //the new row
     183                        int r = Tbl_TableAddRow(table);
     184
     185                        int colNum;
     186                    for (colNum = 0; colNum < Tbl_TableReadNumInputs(table); colNum++) {
     187                                Tbl_Entry_t * entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
     188                                printf("entry : colNum %d \n",colNum);
     189                                if(colNum == abnIndex || colNum == iIndex)
     190                                        Tbl_EntrySetValue(entry,1,1);
     191                                else
     192                                        Tbl_EntrySetValue(entry,0,1);
     193                            Tbl_TableSetEntry(table, entry, r, colNum, 0);
     194                        }
     195                        for (colNum = 0; colNum < Tbl_TableReadNumOutputs(table); colNum++){
     196                                Tbl_Entry_t * entry = Tbl_EntryAlloc(Tbl_EntryNormal_c);
     197                                Tbl_EntrySetValue(entry,1,1);
     198                            Tbl_TableSetEntry(table, entry, r, colNum, 1);
     199                        }
     200                         printf("---------------\n");
     201                         Tbl_TablePrintStats(table, vis_stdout);
     202                         Tbl_TableWriteBlifMvToFile(table,0,vis_stdout);
     203                         free(abnName);
     204                         free(iName);
     205                  }
     206                }
     207         }
     208  }
     209  // TODO
     210  //Remplacer l'ancien network par le nouveau
     211}
     212/**Function********************************************************************
     213
     214  Synopsis    [Implements the _sat_debug command.]
     215
     216  CommandName [_sat_debug]
     217
     218  CommandSynopsis [locate faulty candidates]
     219
     220  CommandArguments [\[-h\] \[-v\]]
     221 
     222  CommandDescription [This command compute the fault candidates of a given
     223  properties.<p>
     224
     225  Command options:<p> 
     226
     227  <dl>
     228  <dt> -h
     229  <dd> Print the command usage.
     230  </dl>
     231
     232  <dt> -v
     233  <dd> Verbose mode.
     234  </dl>
     235  ]
     236
     237  SideEffects []
     238
     239******************************************************************************/
     240
     241
     242static int
     243CommandSatDebug(
     244Hrc_Manager_t ** hmgr,
     245int argc,
     246char ** argv){
     247int            c,i;
     248int            verbose = 0;              /* default value */
     249BmcOption_t  *options = BmcOptionAlloc();
     250Ntk_Network_t * network;
     251bAig_Manager_t    *manager;
     252
     253
     254/*
     255 * Parse command line options.
     256 */
     257util_getopt_reset();
     258while ((c = util_getopt(argc, argv, "vh:m:k:o:")) != EOF) {
     259  switch(c) {
     260    case 'v':
     261      verbose = 1;
     262          options->verbosityLevel =  verbose;
     263      break;
     264    case 'h':
     265      goto usage;
     266        case 'm':
     267      for (i = 0; i < strlen(util_optarg); i++) {
     268                if (!isdigit((int)util_optarg[i])) {
     269                        goto usage;
     270                }
     271      }
     272      options->minK = atoi(util_optarg);
     273      break;
     274    case 'k':
     275      for (i = 0; i < strlen(util_optarg); i++) {
     276                if (!isdigit((int)util_optarg[i])) {
     277                        goto usage;
     278                }
     279      }
     280          options->maxK = atoi(util_optarg);
     281          break;
     282        case 'o':
     283      options->cnfFileName = util_strsav(util_optarg);
     284      break;   
     285
     286    default:
     287      goto usage;
     288  }
     289}
     290 if (options->minK > options->maxK){
     291    (void) fprintf(vis_stderr, "** bmc error: value for -m option must not be greater than vlaue for -k option\n");   
     292    goto usage;
     293  }
     294
     295if (verbose) {
     296  (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n");
     297}
     298 /* create SAT Solver input file */
     299 if (options->cnfFileName == NIL(char)) {
     300    options->satInFile = BmcCreateTmpFile();
     301}
     302 else {
     303    options->satInFile = options->cnfFileName;
     304 }
     305
     306/* create SAT Solver output file */
     307options->satOutFile = BmcCreateTmpFile();
     308if (options->satOutFile == NIL(char)){
     309  BmcOptionFree(options);
     310 (void) fprintf(vis_stdout, "The _sat_debug problem.\n");
     311  return 1;
     312}
     313
     314options->verbosityLevel =  1;
     315//options->satSolver
     316//options->clauses
     317
     318 /*
     319   * Read the network
     320   */
     321  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
     322  if (network == NIL(Ntk_Network_t)) {
     323    (void) fprintf(vis_stdout, "** bmc error: No network\n");
     324    BmcOptionFree(options);
     325    return 1;
     326  }
     327  manager = Ntk_NetworkReadMAigManager(network);
     328  if (manager == NIL(mAig_Manager_t)) {
     329    (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
     330    BmcOptionFree(options);
     331    return 1;
     332  }
     333  /*
     334    We need the bdd when building the transition relation of the automaton
     335  */
     336  if(options->inductiveStep !=0){
     337    Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t);
     338 
     339    designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
     340    if (designFsm == NIL(Fsm_Fsm_t)) {
     341         (void) fprintf(vis_stdout, "The _sat_debug : Build FSM.\n");
     342      return 1;
     343    }
     344  }
     345
     346 /*
     347    Compute the cone of influence
     348        here a list of state variables (latches)
     349  */
     350        st_table        *CoiTable =  generateAllLatches(network);
     351  /*
     352      Generate clauses for each time frame.  This is the old way of generating
     353      clauses in BMC.
     354    */
     355    st_table          *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
     356        BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
     357    FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
     358        /*
     359    nodeToMvfAigTable maps each node to its multi-function And/Inv graph
     360    */
     361        nodeToMvfAigTable =
     362        (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
     363        assert(nodeToMvfAigTable != NIL(st_table));
     364
     365        if(verbose)
     366        {       
     367                (void) fprintf(vis_stdout, "------ node to mvfaig ----\n");
     368                printLatch(nodeToMvfAigTable);
     369                (void) fprintf(vis_stdout, "------      COI       ----\n");
     370                printLatch(CoiTable);
     371                (void) fprintf(vis_stdout, "--------------------------\n");
     372    }
     373    /*
     374      Create a clause database
     375     */
     376    cnfClauses = BmcCnfClausesAlloc();
     377    /*
     378      Generate clauses for an initialized path of length k
     379     */
     380    BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES,
     381                                 cnfClauses, nodeToMvfAigTable, CoiTable);
     382         if(verbose)
     383                (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\
     384                latches %d nodetomvf.\n",cnfClauses->noOfClauses,st_count(CoiTable),st_count(nodeToMvfAigTable));
     385       
     386   
     387        BmcWriteClauses(manager, cnfFile, cnfClauses, options);
     388fclose(cnfFile);
     389BmcCnfClausesFree(cnfClauses);
     390BmcOptionFree(options);
     391return 0;
     392  usage:
     393  (void) fprintf(vis_stderr, "usage: _sat_debug [-h] [-v] [-k max length] [-m \
     394  minimum length] [-o cnf_file]\n");
     395  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
     396  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
     397  (void) fprintf(vis_stderr, "   -m \tminimum length of counterexample to be checked (default is 0)\n"); 
     398  (void) fprintf(vis_stderr, "   -k \tmaximum length of counterexample to be checked (default is 1)\n");
     399  (void) fprintf(vis_stderr, "   -o <cnf_file> contains CNF of the counterexample\n"); 
     400  return 1;             /* error exit */
     401
     402}
    124403/**Function********************************************************************
    125404
  • vis_dev/vis-2.3/src/debug/debug.h

    r27 r35  
    8383/*---------------------------------------------------------------------------*/
    8484
    85 
     85void printLatch(st_table* CoiTable);
     86st_table * generateAllLatches(Ntk_Network_t * ntk);
    8687void mdd_GetState_Values(mdd_manager *mgr, mdd_t * top, FILE * f);
    8788EXTERN void Debug_Init(void);
  • vis_dev/vis-2.3/src/debug/debug.make

    r27 r35  
    1 CSRC += debug.c
     1CSRC += debug.c debugUtilities.c
    22HEADERS += debug.h debugInt.h
    33
  • vis_dev/vis-2.3/src/debug/debugUtilities.c

    r30 r35  
    1 #include "Debug.h"
     1#include "debug.h"
     2void printLatch(st_table* CoiTable)
     3{
     4// COI contents
     5   printf("*** COI ***\n");
     6   st_generator    *stGen;
     7   Ntk_Node_t * latch;
     8   st_foreach_item(CoiTable, stGen, &latch, NULL) {
     9        printf("%s\n",Ntk_NodeReadName(latch));
     10  }
     11}
     12
     13
     14st_table * generateAllLatches(Ntk_Network_t * ntk)
     15{
     16    st_table        *CoiTable = st_init_table(st_ptrcmp, st_ptrhash);
     17        lsGen           gen ;
     18        Ntk_Node_t              *node;
     19
     20        Ntk_NetworkForEachNode(ntk,gen, node){
     21                if (Ntk_NodeTestIsLatch(node)){
     22                        st_insert(CoiTable, (char *) node, Ntk_NodeReadName(node));
     23                }
     24        }
     25        return CoiTable;
     26
     27}
     28
    229
    330void mdd_GetState_Values(
Note: See TracChangeset for help on using the changeset viewer.