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

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

add debug code source
File size: 16.6 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [debug.c]
4
5  PackageName [debug]
6
7  Synopsis    [Test package initialization, ending, and the command test.]
8
9  Author      [Originated from SIS.]
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
34static char rcsid[] UNUSED = "$Id: debug.c,v 1.6 2011/04/12  braun Exp $";
35
36/*---------------------------------------------------------------------------*/
37/* Constant declarations                                                     */
38/*---------------------------------------------------------------------------*/
39
40/*---------------------------------------------------------------------------*/
41/* Structure declarations                                                    */
42/*---------------------------------------------------------------------------*/
43
44/*---------------------------------------------------------------------------*/
45/* Type declarations                                                         */
46/*---------------------------------------------------------------------------*/
47
48/*---------------------------------------------------------------------------*/
49/* Variable declarations                                                     */
50/*---------------------------------------------------------------------------*/
51
52/*---------------------------------------------------------------------------*/
53/* Macro declarations                                                        */
54/*---------------------------------------------------------------------------*/
55
56/**AutomaticStart*************************************************************/
57
58/*---------------------------------------------------------------------------*/
59/* Static function prototypes                                                */
60/*---------------------------------------------------------------------------*/
61
62static int CommandDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
63static int Commandtransition(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
64
65
66/**AutomaticEnd***************************************************************/
67
68
69/*---------------------------------------------------------------------------*/
70/* Definition of exported functions                                          */
71/*---------------------------------------------------------------------------*/
72
73/**Function********************************************************************
74
75  Synopsis    [Initializes the test package.]
76
77  SideEffects []
78
79  SeeAlso     [Debug_End]
80
81******************************************************************************/
82void
83Debug_Init(void)
84{
85  /*
86   * Add a command to the global command table.  By using the leading
87   * underscore, the command will be listed under "help -a" but not "help".
88   */
89  Cmd_CommandAdd("_debug_test", CommandDebug, /* doesn't changes_network */ 0);
90  Cmd_CommandAdd("transition",  Commandtransition,      0);
91
92}
93
94
95/**Function********************************************************************
96
97  Synopsis    [Ends the test package.]
98
99  SideEffects []
100
101  SeeAlso     [Debug_Init]
102
103******************************************************************************/
104void
105Debug_End(void)
106{
107  /*
108   * For example, free any global memory (if any) which the test package is
109   * responsible for.
110   */
111}
112
113
114/*---------------------------------------------------------------------------*/
115/* Definition of internal functions                                          */
116/*---------------------------------------------------------------------------*/
117
118
119/*---------------------------------------------------------------------------*/
120/* Definition of static functions                                            */
121/*---------------------------------------------------------------------------*/
122
123/**Function********************************************************************
124
125  Synopsis    [Implements the _Debug_test command.]
126
127  CommandName [_Debug_test]
128
129  CommandSynopsis [template for implementing commands]
130
131  CommandArguments [\[-h\] \[-v\]]
132 
133  CommandDescription [This command does nothing useful.  It merely serves as a
134  template for the implementation of new commands.<p>
135
136  Command options:<p> 
137
138  <dl>
139  <dt> -h
140  <dd> Print the command usage.
141  </dl>
142
143  <dt> -v
144  <dd> Verbose mode.
145  </dl>
146  ]
147
148  SideEffects []
149
150******************************************************************************/
151static int
152CommandDebug(
153  Hrc_Manager_t ** hmgr,
154  int  argc,
155  char ** argv)
156{
157  int            c;
158  int            verbose = 0;              /* default value */
159
160  /*
161   * Parse command line options.
162   */
163  util_getopt_reset();
164  while ((c = util_getopt(argc, argv, "vh")) != EOF) {
165    switch(c) {
166      case 'v':
167        verbose = 1;
168        break;
169      case 'h':
170        goto usage;
171      default:
172        goto usage;
173    }
174  }
175
176  if (verbose) {
177    (void) fprintf(vis_stdout, "The _Debug_test is under construction.\n");
178  }
179
180  Fsm_Fsm_t   *fsm        = Fsm_HrcManagerReadCurrentFsm(*hmgr);
181  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
182  printf("** DEBUG MODE **\n");
183  Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr);
184  printf("model : %s\n", Hrc_NodeReadModelName(n));
185
186  mdd_t * safe   = getSafe(fsm);
187  mdd_t * forbid = getForbidden(fsm);
188  mdd_t * reach  = getReach(fsm);
189 
190  if(safe == NIL(mdd_t))
191  {
192        printf("call command set_safe before\n");
193        return 1;
194  }
195  if(forbid == NIL(mdd_t))
196  {
197        printf("call command set_forbidden before\n");
198        return 1;
199  }
200
201  FILE*  oFile;
202  oFile = Cmd_FileOpen("safe_prop", "w", NIL(char *), 0);
203 // mdd_FunctionPrintMain(mddManager, safe, "SAFE", oFile);
204//  mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile);
205
206  mdd_t * EFState = mdd_and(reach,safe,1,1);
207//  mdd_t * errorState = mdd_and(reach,forbid,1,1);
208
209  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
210  array_t *careStatesArray = array_alloc(mdd_t *, 0);
211  array_insert(mdd_t *, careStatesArray, 0,mddOne);
212
213  mdd_t * tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
214                   EFState,
215           fsm->fairnessInfo.states,
216           careStatesArray,
217                   0,
218           McDcLevelNone_c);
219
220  mdd_t * EXEFState = mdd_and(reach,tmp_EXEFState,1,1);
221  mdd_FunctionPrintMain(mddManager, EXEFState, "EXEF", oFile);
222
223  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
224                   EXEFState,
225           fsm->fairnessInfo.states,
226           careStatesArray,
227                   0,
228           McDcLevelNone_c);
229  mdd_t * EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
230  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
231  mdd_t * andState =  mdd_xor(EXEFState2,EXEFState);
232  mdd_FunctionPrintMain(mddManager, andState, "XOR2", oFile);
233  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
234                   andState,
235           fsm->fairnessInfo.states,
236           careStatesArray,
237                   0,
238           McDcLevelNone_c);
239  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
240  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
241  andState =  mdd_xor(EXEFState2,andState);
242  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
243  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
244                   andState,
245           fsm->fairnessInfo.states,
246           careStatesArray,
247                   0,
248           McDcLevelNone_c);
249  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
250  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
251  andState =  mdd_xor(EXEFState2,andState);
252  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
253
254
255
256  //mdd_FunctionPrintMain(mddManager, errorState, "ERROR", oFile);
257  //mdd_GetState_Values(mddManager , EFState, stdout);
258  fclose(oFile);
259
260
261
262
263
264  return 0;             /* normal exit */
265
266  usage:
267  (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
268  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
269  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
270  return 1;             /* error exit */
271}
272
273
274
275/**Function********************************************************************
276
277  Synopsis [Returns a BDD array from an Mvf array]
278
279  SideEffects [None]
280
281  SeeAlso     []
282
283******************************************************************************/
284static array_t *
285markGetBddArray(array_t *mvfArray,  mdd_manager* mddManager)
286{
287    int           i,phase;
288    array_t *bddArray;
289    Mvf_Function_t *mvf;
290
291    FILE*  oFile;
292  oFile = Cmd_FileOpen("trans.bdd", "w", NIL(char *), 0);
293
294    bddArray = array_alloc(bdd_node *,0);
295 printf("mvf array : %d \n" , array_n(mvfArray));
296
297    arrayForEachItem(Mvf_Function_t *, mvfArray,i,mvf) {
298        mdd_t     *mddTemp;
299        bdd_node    *ddNode;
300
301        mddTemp = array_fetch(mdd_t *, mvf, 1);
302        ddNode = (bdd_node *) bdd_get_node(mddTemp,&phase);
303        bdd_ref(ddNode);
304    mdd_FunctionPrintMain(mddManager, mddTemp, "TRANS", oFile);
305    printf("\n");
306        ddNode = phase ? bdd_not_bdd_node(ddNode) : ddNode;
307    printf("%d --->",i);
308    bdd_print(mddTemp);
309    printf("\n");
310        array_insert_last(bdd_node *, bddArray, ddNode);
311    }
312    fclose(oFile);
313    return bddArray;
314}
315
316/**Function********************************************************************
317
318  Synopsis [Returns a BDD array given an integer array of variable indices.]
319
320  SideEffects [None]
321
322  SeeAlso     []
323
324******************************************************************************/
325static bdd_node **
326BddNodeArrayFromIdArray(
327  bdd_manager   *ddManager,
328  array_t       *idArray)
329{
330    bdd_node **xvars;
331    int i,id;
332    int nvars = array_n(idArray);
333
334    xvars = ALLOC(bdd_node *, nvars);
335    if (xvars == NULL)
336        return NULL;
337
338    for(i = 0; i < nvars; i++) {
339        id = array_fetch(int,idArray,i);
340        xvars[i] = bdd_bdd_ith_var(ddManager,id);
341        bdd_ref(xvars[i]);
342    }
343    return xvars;
344}
345/**Function********************************************************************
346
347  Synopsis [Compute the relation between an array of function and a
348  corresponding array of variables. A BDD is returned which represents
349  AND(i=0 -> i<nVars)(yVars[i]==nextBdds). ]
350
351  SideEffects []
352
353  SeeAlso     []
354
355******************************************************************************/
356static bdd_node *
357computeTransitionRelationWithIds(
358  bdd_manager   *ddManager,
359  array_t       *nextBdds,
360  bdd_node      **yVars,
361  int           nVars)
362{
363    bdd_node    *ddtemp1, *ddtemp2;
364    bdd_node    *oldTR, *fn;
365    int                  i;
366
367
368    oldTR = bdd_read_one(ddManager);
369
370    for(i = 0; i < nVars; i++) {
371        ddtemp2  = array_fetch(bdd_node *, nextBdds, i);
372
373    bdd_print(ddtemp2);
374        fn = bdd_bdd_xnor(ddManager,ddtemp2,yVars[i]);
375        bdd_ref(fn);
376        ddtemp1 = bdd_bdd_and(ddManager,oldTR,fn);
377        bdd_ref(ddtemp1);
378        bdd_recursive_deref(ddManager,fn);
379        bdd_recursive_deref(ddManager,oldTR);
380        oldTR = ddtemp1;
381    }
382    return oldTR;
383}
384/*
385static mdd_t *
386computeTransitionRelationWithIds_mdd(
387  mdd_manager   *ddManager,
388  array_t       *nextBdds,
389  mdd_t **yVars,
390  int           nVars)
391{
392    mdd_t       *ddtemp1, *ddtemp2;
393    mdd_t       *oldTR, *fn;
394    int                  i;
395
396
397    oldTR = mdd_one(ddManager);
398
399    for(i = 0; i < nVars; i++) {
400        ddtemp2  = array_fetch(mdd_t *, nextBdds, i);
401
402        fn = mdd_xnor(ddtemp2,yVars[i],1,1);
403        ddtemp1 = mdd_and(oldTR,fn,1,1);
404        mdd_free(oldTR);
405        oldTR = ddtemp1;
406    }
407
408        mdd_ref(ddtemp1);
409        mdd_free(fn);
410    return oldTR;
411}
412*/
413
414static int 
415Commandtransition (Hrc_Manager_t ** hmgr,
416                   int  argc, char ** argv){
417  Fsm_Fsm_t   *fsm        = Fsm_HrcManagerReadCurrentFsm(*hmgr);
418  Ntk_Network_t *network = Fsm_FsmReadNetwork(fsm);
419  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
420  printf("** TRANSITION RELATION **\n");
421  Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr);
422  printf("model : %s\n", Hrc_NodeReadModelName(n));
423
424   graph_t *partition;
425   bdd_node *tranRelation;
426   bdd_node **xVars,**yVars, **piVars;
427
428   
429   array_t *tranFunArray, *leaveIds;
430   array_t *nextBdds, *nextMvfs;
431   int nVars, nPi;
432
433   
434    /*
435     * tranFunArray is a list of next state funs.
436     */
437
438    tranFunArray = Fsm_FsmReadNextStateFunctionNames(fsm);
439    char *name;
440    int i;
441    arrayForEachItem(char*, tranFunArray, i, name){
442      Ntk_Node_t * latch = Ntk_NetworkFindNodeByName(network, name);
443      printf("%s : mddid : %d\n",name , Ntk_NodeReadMddId(latch) );
444      //int c =   Ntk_NodeReadMddId(latch);
445    }
446
447 array_t         *psVarsArray = Fsm_FsmReadPresentStateVars(fsm);
448  int                  arrSize = array_n( psVarsArray );
449
450  for ( i = 0 ; i < arrSize ; ++i ) {
451    int      mddId = array_fetch( int, psVarsArray, i );
452    mvar_type mVar = array_fetch(mvar_type, 
453                                 mdd_ret_mvar_list(mddManager),mddId);
454    printf("%s : mddid %d\n", mVar.name, mddId);
455  }
456
457 array_t *nsVarsArray  =  Fsm_FsmReadNextStateVars(fsm);
458arrSize = array_n( nsVarsArray );
459
460  for ( i = 0 ; i < arrSize ; ++i ) {
461    int      mddId = array_fetch( int, nsVarsArray, i );
462    mvar_type mVar = array_fetch(mvar_type, 
463                                 mdd_ret_mvar_list(mddManager),mddId);
464    printf("%s : mddid %d\n", mVar.name, mddId);
465  }
466
467
468    leaveIds = array_join(Fsm_FsmReadInputVars(fsm),
469                          Fsm_FsmReadPresentStateVars(fsm));
470    /*
471     * Get the BDDs for transition functions.Duplicate functions are returned.
472     */
473    partition = Fsm_FsmReadPartition(fsm);
474    nextMvfs = Part_PartitionBuildFunctions(partition,tranFunArray,leaveIds,
475                                            NIL(mdd_t));
476
477    array_free(leaveIds);
478    array_free(tranFunArray);
479
480 Mvf_Function_t *mvf = array_fetch(Mvf_Function_t *,nextMvfs,1);
481 mdd_t * recupdd = array_fetch(mdd_t *, mvf, 0);
482 printf("plop\n");
483 bdd_print(recupdd);
484/** Build cex **/
485
486/** state0 **/
487 mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
488 printf("****************\n");
489 bdd_print (s0);
490 mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
491 printf("****************\n");
492 bdd_print (s1);
493 mdd_t * and =  mdd_one(mddManager);
494 and = mdd_and(s0,s1,1,1);
495 mdd_t* reach = mdd_one(mddManager);
496 reach = Fsm_FsmReadReachableStates(fsm);
497 mdd_t * state0 =  mdd_and(and,reach,1,1);
498/** next state1 **/
499 mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
500 mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
501 mdd_t * state1 = mdd_and(ns0,ns1,1,1);
502/** new rel **/
503 mdd_t * rel =  mdd_or(state0,state1,0,0);
504
505
506
507
508// Get image_info
509
510  Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
511
512   Img_PrintPartitionedTransitionRelation(mddManager,imageInfo, 0);
513
514array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0);
515 arrayForEachItem(mdd_t *, transRelation, i, recupdd){
516 printf("****************\n");
517
518    bdd_print(recupdd);
519}
520  mdd_t* new_rel = mdd_and(recupdd,rel,1,1);
521FILE * oFile = fopen("relation.bdd","w");
522 mdd_FunctionPrintMain(mddManager, recupdd, "TRANS", oFile);
523 mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile);
524 mdd_FunctionPrintMain(mddManager, rel, "REL", oFile);
525 mdd_FunctionPrintMain(mddManager, new_rel, "new_rel", oFile);
526
527fclose(oFile);
528array_insert(mdd_t*,transRelation,0,new_rel);
529Img_ReplacePartitionedTransitionRelation(imageInfo, transRelation,0);
530 printf("****************\n");
531
532Img_PrintPartitionedTransitionRelation(mddManager,imageInfo, 0);
533
534 arrayForEachItem(mdd_t *, transRelation, i, recupdd){
535 printf("****************\n");
536 FsmResetReachabilityFields(fsm, 0);
537
538    bdd_print(recupdd);
539}
540
541/*
542FILE * dotFile = fopen("relation.dot","w");
543
544mdd_dump_dot(reach,NIL(char),dotFile);
545fclose(dotFile);
546*/
547//    nextBdds = markGetBddArray(nextMvfs,mddManager);
548
549    Mvf_FunctionArrayFree(nextMvfs);
550/*
551 // Get the DdNodes for all the variables.
552
553    piVars = BddNodeArrayFromIdArray(mddManager,
554                                         Fsm_FsmReadInputVars(fsm));
555    xVars = BddNodeArrayFromIdArray(mddManager,
556                                        Fsm_FsmReadPresentStateVars(fsm));
557    yVars = BddNodeArrayFromIdArray(mddManager,
558                                        Fsm_FsmReadNextStateVars(fsm));
559
560    nVars = array_n(Fsm_FsmReadNextStateVars(fsm));
561    nPi = array_n(Fsm_FsmReadInputVars(fsm));
562
563    // Compute the transition relation
564    tranRelation = computeTransitionRelationWithIds(mddManager, nextBdds,
565                                                    yVars, nVars);
566 */
567/*
568 FILE*  oFile;
569  oFile = Cmd_FileOpen("trans.bdd", "w", NIL(char *), 0);
570mdd_FunctionPrintMain(mddManager, tranRelation, "TRANS", oFile);
571 fclose(oFile);
572 */
573  return 0;
574}
575
576
Note: See TracBrowser for help on using the repository browser.