source: vis_dev/vis-2.3/src/debug/debug.c @ 36

Last change on this file since 36 was 36, checked in by cecile, 13 years ago

Add Abnormal predicate structures
File size: 19.7 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [debug.c]
4
5  PackageName [debug]
6
7  Synopsis    [Debug package initialization, ending, and the command debug]
8
9  Author      [Cecile B.]
10
11  Copyright   [Copyright (c) 1994-1996 The Regents of the Univ. of California.
12  All rights reserved.
13
14  Permission is hereby granted, without written agreement and without license
15  or royalty fees, to use, copy, modify, and distribute this software and its
16  documentation for any purpose, provided that the above copyright notice and
17  the following two paragraphs appear in all copies of this software.
18
19  IN NO EVENT SHALL THE UNIVERSITY OF CALIFORNIA BE LIABLE TO ANY PARTY FOR
20  DIRECT, INDIRECT, SPECIAL, INCIDENTAL, OR CONSEQUENTIAL DAMAGES ARISING OUT
21  OF THE USE OF THIS SOFTWARE AND ITS DOCUMENTATION, EVEN IF THE UNIVERSITY OF
22  CALIFORNIA HAS BEEN ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
23
24  THE UNIVERSITY OF CALIFORNIA SPECIFICALLY DISCLAIMS ANY WARRANTIES,
25  INCLUDING, BUT NOT LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND
26  FITNESS FOR A PARTICULAR PURPOSE.  THE SOFTWARE PROVIDED HEREUNDER IS ON AN
27  "AS IS" BASIS, AND THE UNIVERSITY OF CALIFORNIA HAS NO OBLIGATION TO PROVIDE
28  MAINTENANCE, SUPPORT, UPDATES, ENHANCEMENTS, OR MODIFICATIONS.]
29
30******************************************************************************/
31
32#include "debugInt.h"
33#include "imgInt.h"
34#include "partInt.h"
35static char rcsid[] UNUSED = "$Id: debug.c,v 1.6 2011/04/12  braun Exp $";
36
37/*---------------------------------------------------------------------------*/
38/* Constant declarations                                                     */
39/*---------------------------------------------------------------------------*/
40
41/*---------------------------------------------------------------------------*/
42/* Structure declarations                                                    */
43/*---------------------------------------------------------------------------*/
44
45/*---------------------------------------------------------------------------*/
46/* Type declarations                                                         */
47/*---------------------------------------------------------------------------*/
48
49/*---------------------------------------------------------------------------*/
50/* Variable declarations                                                     */
51/*---------------------------------------------------------------------------*/
52
53/*---------------------------------------------------------------------------*/
54/* Macro declarations                                                        */
55/*---------------------------------------------------------------------------*/
56
57/**AutomaticStart*************************************************************/
58
59/*---------------------------------------------------------------------------*/
60/* Static function prototypes                                                */
61/*---------------------------------------------------------------------------*/
62
63static int CommandSatDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
64static int CommandDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
65static int CommandTransition(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
66static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
67
68
69/**AutomaticEnd***************************************************************/
70
71
72/*---------------------------------------------------------------------------*/
73/* Definition of exported functions                                          */
74/*---------------------------------------------------------------------------*/
75
76/**Function********************************************************************
77
78  Synopsis    [Initializes the test package.]
79
80  SideEffects []
81
82  SeeAlso     [Debug_End]
83
84******************************************************************************/
85void
86Debug_Init(void)
87{
88  /*
89   * Add a command to the global command table.  By using the leading
90   * underscore, the command will be listed under "help -a" but not "help".
91   */
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);
96
97}
98
99
100/**Function********************************************************************
101
102  Synopsis    [Ends the test package.]
103
104  SideEffects []
105
106  SeeAlso     [Debug_Init]
107
108******************************************************************************/
109void
110Debug_End(void)
111{
112  /*
113   * For example, free any global memory (if any) which the test package is
114   * responsible for.
115   */
116}
117
118
119/*---------------------------------------------------------------------------*/
120/* Definition of internal functions                                          */
121/*---------------------------------------------------------------------------*/
122
123
124/*---------------------------------------------------------------------------*/
125/* Definition of static functions                                            */
126/*---------------------------------------------------------------------------*/
127
128
129static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
130{
131  Ntk_Network_t * ntk;
132  int c,verbose;
133  Dbg_Abnormal_t * abnormal;
134  ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
135  if (ntk == NIL(Ntk_Network_t)) {
136        (void) fprintf(vis_stdout, "** abn error: No network\n");
137        return 1;
138  }
139  while ((c = util_getopt(argc, argv, "vh:m:k:o:")) != EOF) {
140        switch(c) {
141                case 'v':
142                        verbose = 1;
143                        break;
144                }
145 }
146  abnormal = Dbg_DebugAbnormalAlloc(ntk);
147  abnormal->verbose = verbose;
148  Dbg_AddAbnormalPredicatetoNetwork(abnormal);
149}
150/**Function********************************************************************
151
152  Synopsis    [Implements the _sat_debug command.]
153
154  CommandName [_sat_debug]
155
156  CommandSynopsis [locate faulty candidates]
157
158  CommandArguments [\[-h\] \[-v\]]
159 
160  CommandDescription [This command compute the fault candidates of a given
161  properties.<p>
162
163  Command options:<p> 
164
165  <dl>
166  <dt> -h
167  <dd> Print the command usage.
168  </dl>
169
170  <dt> -v
171  <dd> Verbose mode.
172  </dl>
173  ]
174
175  SideEffects []
176
177******************************************************************************/
178
179
180static int 
181CommandSatDebug(
182Hrc_Manager_t ** hmgr, 
183int argc, 
184char ** argv){
185int            c,i;
186int            verbose = 0;              /* default value */
187BmcOption_t  *options = BmcOptionAlloc();
188Ntk_Network_t * network;
189bAig_Manager_t    *manager;
190
191
192/*
193 * Parse command line options.
194 */
195util_getopt_reset();
196while ((c = util_getopt(argc, argv, "vh:m:k:o:")) != EOF) {
197  switch(c) {
198    case 'v':
199      verbose = 1;
200          options->verbosityLevel =  verbose;
201      break;
202    case 'h':
203      goto usage;
204        case 'm':
205      for (i = 0; i < strlen(util_optarg); i++) {
206                if (!isdigit((int)util_optarg[i])) {
207                        goto usage;
208                }
209      }
210      options->minK = atoi(util_optarg);
211      break;
212    case 'k':
213      for (i = 0; i < strlen(util_optarg); i++) {
214                if (!isdigit((int)util_optarg[i])) {
215                        goto usage;
216                }
217      }
218          options->maxK = atoi(util_optarg);
219          break;
220        case 'o':
221      options->cnfFileName = util_strsav(util_optarg);
222      break;   
223
224    default:
225      goto usage;
226  }
227}
228 if (options->minK > options->maxK){
229    (void) fprintf(vis_stderr, "** bmc error: value for -m option must not be greater than vlaue for -k option\n");   
230    goto usage;
231  }
232
233if (verbose) {
234  (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n");
235}
236 /* create SAT Solver input file */
237 if (options->cnfFileName == NIL(char)) {
238    options->satInFile = BmcCreateTmpFile(); 
239}
240 else {
241    options->satInFile = options->cnfFileName;
242 }
243
244/* create SAT Solver output file */
245options->satOutFile = BmcCreateTmpFile();
246if (options->satOutFile == NIL(char)){
247  BmcOptionFree(options);
248 (void) fprintf(vis_stdout, "The _sat_debug problem.\n");
249  return 1;
250}
251
252options->verbosityLevel =  1;
253//options->satSolver
254//options->clauses
255
256 /*
257   * Read the network
258   */
259  network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
260  if (network == NIL(Ntk_Network_t)) {
261    (void) fprintf(vis_stdout, "** bmc error: No network\n");
262    BmcOptionFree(options);
263    return 1;
264  }
265  manager = Ntk_NetworkReadMAigManager(network);
266  if (manager == NIL(mAig_Manager_t)) {
267    (void) fprintf(vis_stdout, "** bmc error: run build_partition_maigs command first\n");
268    BmcOptionFree(options);
269    return 1;
270  }
271  /*
272    We need the bdd when building the transition relation of the automaton
273  */
274  if(options->inductiveStep !=0){
275    Fsm_Fsm_t *designFsm = NIL(Fsm_Fsm_t);
276 
277    designFsm = Fsm_HrcManagerReadCurrentFsm(*hmgr);
278    if (designFsm == NIL(Fsm_Fsm_t)) {
279         (void) fprintf(vis_stdout, "The _sat_debug : Build FSM.\n");
280      return 1;
281    }
282  }
283
284 /*
285    Compute the cone of influence
286        here a list of state variables (latches)
287  */
288        st_table        *CoiTable =  generateAllLatches(network);
289  /*
290      Generate clauses for each time frame.  This is the old way of generating
291      clauses in BMC.
292    */
293    st_table          *nodeToMvfAigTable = NIL(st_table);  /* node to mvfAig */
294        BmcCnfClauses_t   *cnfClauses = NIL(BmcCnfClauses_t);
295    FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
296        /*
297    nodeToMvfAigTable maps each node to its multi-function And/Inv graph
298    */
299        nodeToMvfAigTable =
300        (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
301        assert(nodeToMvfAigTable != NIL(st_table));
302
303        if(verbose)
304        {       
305                (void) fprintf(vis_stdout, "------ node to mvfaig ----\n");
306                printLatch(nodeToMvfAigTable);
307                (void) fprintf(vis_stdout, "------      COI       ----\n");
308                printLatch(CoiTable);
309                (void) fprintf(vis_stdout, "--------------------------\n");
310    }
311    /*
312      Create a clause database
313     */
314    cnfClauses = BmcCnfClausesAlloc();
315    /*
316      Generate clauses for an initialized path of length k
317     */
318    BmcCnfGenerateClausesForPath(network, 0, options->maxK, BMC_INITIAL_STATES,
319                                 cnfClauses, nodeToMvfAigTable, CoiTable);
320         if(verbose)
321                (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\
322                latches %d nodetomvf.\n",cnfClauses->noOfClauses,st_count(CoiTable),st_count(nodeToMvfAigTable));
323       
324   
325        BmcWriteClauses(manager, cnfFile, cnfClauses, options);
326fclose(cnfFile);
327BmcCnfClausesFree(cnfClauses);
328BmcOptionFree(options);
329return 0;
330  usage:
331  (void) fprintf(vis_stderr, "usage: _sat_debug [-h] [-v] [-k max length] [-m \
332  minimum length] [-o cnf_file]\n");
333  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
334  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
335  (void) fprintf(vis_stderr, "   -m \tminimum length of counterexample to be checked (default is 0)\n"); 
336  (void) fprintf(vis_stderr, "   -k \tmaximum length of counterexample to be checked (default is 1)\n");
337  (void) fprintf(vis_stderr, "   -o <cnf_file> contains CNF of the counterexample\n"); 
338  return 1;             /* error exit */
339
340}
341/**Function********************************************************************
342
343  Synopsis    [Implements the _Debug_test command.]
344
345  CommandName [_Debug_test]
346
347  CommandSynopsis [template for implementing commands]
348
349  CommandArguments [\[-h\] \[-v\]]
350 
351  CommandDescription [This command does nothing useful.  It merely serves as a
352  template for the implementation of new commands.<p>
353
354  Command options:<p> 
355
356  <dl>
357  <dt> -h
358  <dd> Print the command usage.
359  </dl>
360
361  <dt> -v
362  <dd> Verbose mode.
363  </dl>
364  ]
365
366  SideEffects []
367
368******************************************************************************/
369static int
370CommandDebug(
371  Hrc_Manager_t ** hmgr,
372  int  argc,
373  char ** argv)
374{
375  int            c;
376  int            verbose = 0;              /* default value */
377
378  /*
379   * Parse command line options.
380   */
381  util_getopt_reset();
382  while ((c = util_getopt(argc, argv, "vh")) != EOF) {
383    switch(c) {
384      case 'v':
385        verbose = 1;
386        break;
387      case 'h':
388        goto usage;
389      default:
390        goto usage;
391    }
392  }
393
394  if (verbose) {
395    (void) fprintf(vis_stdout, "The _Debug_test is under construction.\n");
396  }
397
398  Fsm_Fsm_t   *fsm        = Fsm_HrcManagerReadCurrentFsm(*hmgr);
399  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
400  printf("** DEBUG MODE **\n");
401  Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr);
402  printf("model : %s\n", Hrc_NodeReadModelName(n));
403
404  mdd_t * safe   = getSafe(fsm);
405  mdd_t * forbid = getForbidden(fsm);
406  mdd_t * reach  = getReach(fsm);
407 
408  if(safe == NIL(mdd_t))
409  {
410        printf("call command set_safe before\n");
411        return 1;
412  }
413  if(forbid == NIL(mdd_t))
414  {
415        printf("call command set_forbidden before\n");
416        return 1;
417  }
418
419  FILE*  oFile;
420  oFile = Cmd_FileOpen("safe_prop", "w", NIL(char *), 0);
421 // mdd_FunctionPrintMain(mddManager, safe, "SAFE", oFile);
422//  mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile);
423
424  mdd_t * EFState = mdd_and(reach,safe,1,1);
425//  mdd_t * errorState = mdd_and(reach,forbid,1,1);
426
427  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
428  array_t *careStatesArray = array_alloc(mdd_t *, 0);
429  array_insert(mdd_t *, careStatesArray, 0,mddOne);
430
431  mdd_t * tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
432                   EFState,
433           fsm->fairnessInfo.states,
434           careStatesArray,
435                   0,
436           McDcLevelNone_c);
437
438  mdd_t * EXEFState = mdd_and(reach,tmp_EXEFState,1,1);
439  mdd_FunctionPrintMain(mddManager, EXEFState, "EXEF", oFile);
440
441  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
442                   EXEFState,
443           fsm->fairnessInfo.states,
444           careStatesArray,
445                   0,
446           McDcLevelNone_c);
447  mdd_t * EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
448  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
449  mdd_t * andState =  mdd_xor(EXEFState2,EXEFState);
450  mdd_FunctionPrintMain(mddManager, andState, "XOR2", oFile);
451  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
452                   andState,
453           fsm->fairnessInfo.states,
454           careStatesArray,
455                   0,
456           McDcLevelNone_c);
457  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
458  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
459  andState =  mdd_xor(EXEFState2,andState);
460  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
461  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
462                   andState,
463           fsm->fairnessInfo.states,
464           careStatesArray,
465                   0,
466           McDcLevelNone_c);
467  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
468  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
469  andState =  mdd_xor(EXEFState2,andState);
470  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
471
472
473
474  //mdd_FunctionPrintMain(mddManager, errorState, "ERROR", oFile);
475  //mdd_GetState_Values(mddManager , EFState, stdout);
476  fclose(oFile);
477
478
479
480
481
482  return 0;             /* normal exit */
483
484  usage:
485  (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
486  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
487  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
488  return 1;             /* error exit */
489}
490
491/******************************************/
492/* function that build a bdd for the      */
493/* simple example :                       */
494/*     (state = 0) -> !(state = 1)        */
495/******************************************/
496mdd_t * buildDummyBdd(mdd_manager   *mddManager)
497{
498/** state0 = 0 **/
499 mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
500 mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
501 mdd_t * state0 =  mdd_one(mddManager);
502 state0 = mdd_and(s0,s1,1,1);
503/** state1 = 1 **/
504 mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
505 mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
506 mdd_t * state1 =  mdd_one(mddManager);
507 state1 = mdd_and(ns0,ns1,1,1);
508/** state = 0) -> !(state = 1) **/
509 mdd_t * rel =  mdd_one(mddManager);
510 rel =  mdd_or(state0,state1,0,0);
511 
512 return rel;
513}
514
515
516/**Function********************************************************************
517
518  Synopsis    [Implements the transtion command.]
519
520  CommandName [_transition]
521
522  CommandSynopsis [compute new transition relation]
523
524  CommandArguments [\[-h\] \[-v\]]
525 
526  CommandDescription [This command create a new transition relation that is a
527  and of the Bdd of the old one and an other bdd.
528  <p>
529
530  Command options:<p> 
531
532  <dl>
533  <dt> -h
534  <dd> Print the command usage.
535  </dl>
536
537  <dt> -v
538  <dd> Verbose mode.
539  </dl>
540  ]
541
542  SideEffects [Change the fsm]
543
544******************************************************************************/
545
546static int 
547CommandTransition (Hrc_Manager_t ** hmgr,
548                   int  argc, char ** argv){
549int            c;
550int            verbose = 0;              /* default value */
551
552/*
553 * Parse command line options.
554 */
555util_getopt_reset();
556while ((c = util_getopt(argc, argv, "vh")) != EOF) {
557  switch(c) {
558    case 'v':
559      verbose = 1;
560      break;
561    case 'h':
562      goto usage;
563    default:
564      goto usage;
565  }
566}
567
568if (verbose) {
569  (void) fprintf(vis_stdout, "The _transition is under construction.\n");
570}
571
572Fsm_Fsm_t      *fsm          = NIL(Fsm_Fsm_t);
573Ntk_Network_t  *network      = NIL(Ntk_Network_t);
574mdd_manager    *mddManager; 
575mdd_t          *rel          = NIL(mdd_t);
576graph_t        *partition;
577int            i;
578/******************/
579network      = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
580if(network == NIL(Ntk_Network_t))
581        return 1;
582fsm          = Fsm_HrcManagerReadCurrentFsm(*hmgr);
583if(fsm ==  NIL(Fsm_Fsm_t))
584        return 1;
585mddManager   = Fsm_FsmReadMddManager(fsm);
586
587
588
589/**********   Build cex  ***********/
590/* Here add the function           */
591/* that build the Bdd to and       */
592/* with the transtion relation     */
593/***********************************/
594rel = buildDummyBdd(mddManager);
595if(rel == NIL(mdd_t))
596{
597        fprintf(vis_stdout,"Problem when building the new relation bdd");
598        return 1;
599}
600
601/** Get image_info **/
602Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
603partition = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
604/**** The complete transtion relation ****/
605// array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0);
606/*****************************************/
607/*** For each latch rebuild the transition function ***/
608/*** mvf table is composed of mdd for each possible ***/
609/*** value of the latch                             ***/
610ImgFunctionData_t * functionData = &(imageInfo->functionData);
611array_t *roots = functionData->roots;
612array_t *rangeVarMddIdArray = functionData->rangeVars;
613char * nodeName;
614arrayForEachItem(char *, roots, i, nodeName) {
615        /* The new relation */ 
616        vertex_t *vertex = Part_PartitionFindVertexByName(partition, nodeName);
617    Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
618    int mddId = array_fetch(int, rangeVarMddIdArray, i);
619        mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);
620        mdd_t * n_relation = mdd_and(relation,rel,1,1);
621    /* Build for each possible value */
622        int nbValue = Mvf_FunctionReadNumComponents(mvf) ;
623        int v ;
624        Mvf_Function_t * newMvf = Mvf_FunctionAlloc(mddManager,nbValue);
625        for(v = 0; v<nbValue;v++)
626        {
627                 mdd_t * n_s1 =  mdd_eq_c(mddManager,mddId, v);
628                 mdd_t * n_rel_s1 = mdd_and(n_relation,n_s1,1,1);
629                 mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1);
630                 Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1);
631
632        }
633        /* Replace the function for the latch */
634        Part_VertexSetFunction(vertex, newMvf);
635//      printf("vertex %s changed % d\n",PartVertexReadName(vertex));
636        Mvf_FunctionFree(mvf);
637}
638
639/** Change the fsm **/
640fsm = Fsm_FsmCreateFromNetworkWithPartition(network, partition);
641mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
642Fsm_FsmComputeReachableStates(fsm,0,verbose,
643                                      0,0, 0,
644                                      0, 0, Fsm_Rch_Default_c,
645                                      0,1, NIL(array_t),
646                                      (verbose > 0),  NIL(array_t));
647if(verbose)
648        Fsm_FsmReachabilityPrintResults(fsm,3, 0);
649/** Change Image Info **/
650Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
651                                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
652                                          (void *) partition);
653
654
655return 0;               /* normal exit */
656
657usage:
658(void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
659(void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
660(void) fprintf(vis_stderr, "   -v\t\tverbose\n");
661return 1;               /* error exit */
662
663}
664
665
Note: See TracBrowser for help on using the repository browser.