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

Last change on this file since 30 was 30, checked in by cecile, 14 years ago

We can now change the transition relation
File size: 13.8 KB
RevLine 
[27]1/**CFile***********************************************************************
2
3  FileName    [debug.c]
4
5  PackageName [debug]
6
[30]7  Synopsis    [Debug package initialization, ending, and the command debug]
[27]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"
[30]33#include "imgInt.h"
34#include "partInt.h"
[27]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 CommandDebug(Hrc_Manager_t ** hmgr, int argc, char ** argv);
[30]64static int CommandTransition(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
[27]65
66
67/**AutomaticEnd***************************************************************/
68
69
70/*---------------------------------------------------------------------------*/
71/* Definition of exported functions                                          */
72/*---------------------------------------------------------------------------*/
73
74/**Function********************************************************************
75
76  Synopsis    [Initializes the test package.]
77
78  SideEffects []
79
80  SeeAlso     [Debug_End]
81
82******************************************************************************/
83void
84Debug_Init(void)
85{
86  /*
87   * Add a command to the global command table.  By using the leading
88   * underscore, the command will be listed under "help -a" but not "help".
89   */
90  Cmd_CommandAdd("_debug_test", CommandDebug, /* doesn't changes_network */ 0);
[30]91  Cmd_CommandAdd("_transition",  CommandTransition,      0);
[27]92
93}
94
95
96/**Function********************************************************************
97
98  Synopsis    [Ends the test package.]
99
100  SideEffects []
101
102  SeeAlso     [Debug_Init]
103
104******************************************************************************/
105void
106Debug_End(void)
107{
108  /*
109   * For example, free any global memory (if any) which the test package is
110   * responsible for.
111   */
112}
113
114
115/*---------------------------------------------------------------------------*/
116/* Definition of internal functions                                          */
117/*---------------------------------------------------------------------------*/
118
119
120/*---------------------------------------------------------------------------*/
121/* Definition of static functions                                            */
122/*---------------------------------------------------------------------------*/
123
124/**Function********************************************************************
125
126  Synopsis    [Implements the _Debug_test command.]
127
128  CommandName [_Debug_test]
129
130  CommandSynopsis [template for implementing commands]
131
132  CommandArguments [\[-h\] \[-v\]]
133 
134  CommandDescription [This command does nothing useful.  It merely serves as a
135  template for the implementation of new commands.<p>
136
137  Command options:<p> 
138
139  <dl>
140  <dt> -h
141  <dd> Print the command usage.
142  </dl>
143
144  <dt> -v
145  <dd> Verbose mode.
146  </dl>
147  ]
148
149  SideEffects []
150
151******************************************************************************/
152static int
153CommandDebug(
154  Hrc_Manager_t ** hmgr,
155  int  argc,
156  char ** argv)
157{
158  int            c;
159  int            verbose = 0;              /* default value */
160
161  /*
162   * Parse command line options.
163   */
164  util_getopt_reset();
165  while ((c = util_getopt(argc, argv, "vh")) != EOF) {
166    switch(c) {
167      case 'v':
168        verbose = 1;
169        break;
170      case 'h':
171        goto usage;
172      default:
173        goto usage;
174    }
175  }
176
177  if (verbose) {
178    (void) fprintf(vis_stdout, "The _Debug_test is under construction.\n");
179  }
180
181  Fsm_Fsm_t   *fsm        = Fsm_HrcManagerReadCurrentFsm(*hmgr);
182  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
183  printf("** DEBUG MODE **\n");
184  Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr);
185  printf("model : %s\n", Hrc_NodeReadModelName(n));
186
187  mdd_t * safe   = getSafe(fsm);
188  mdd_t * forbid = getForbidden(fsm);
189  mdd_t * reach  = getReach(fsm);
190 
191  if(safe == NIL(mdd_t))
192  {
193        printf("call command set_safe before\n");
194        return 1;
195  }
196  if(forbid == NIL(mdd_t))
197  {
198        printf("call command set_forbidden before\n");
199        return 1;
200  }
201
202  FILE*  oFile;
203  oFile = Cmd_FileOpen("safe_prop", "w", NIL(char *), 0);
204 // mdd_FunctionPrintMain(mddManager, safe, "SAFE", oFile);
205//  mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile);
206
207  mdd_t * EFState = mdd_and(reach,safe,1,1);
208//  mdd_t * errorState = mdd_and(reach,forbid,1,1);
209
210  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
211  array_t *careStatesArray = array_alloc(mdd_t *, 0);
212  array_insert(mdd_t *, careStatesArray, 0,mddOne);
213
214  mdd_t * tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
215                   EFState,
216           fsm->fairnessInfo.states,
217           careStatesArray,
218                   0,
219           McDcLevelNone_c);
220
221  mdd_t * EXEFState = mdd_and(reach,tmp_EXEFState,1,1);
222  mdd_FunctionPrintMain(mddManager, EXEFState, "EXEF", oFile);
223
224  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
225                   EXEFState,
226           fsm->fairnessInfo.states,
227           careStatesArray,
228                   0,
229           McDcLevelNone_c);
230  mdd_t * EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
231  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
232  mdd_t * andState =  mdd_xor(EXEFState2,EXEFState);
233  mdd_FunctionPrintMain(mddManager, andState, "XOR2", oFile);
234  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
235                   andState,
236           fsm->fairnessInfo.states,
237           careStatesArray,
238                   0,
239           McDcLevelNone_c);
240  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
241  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
242  andState =  mdd_xor(EXEFState2,andState);
243  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
244  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
245                   andState,
246           fsm->fairnessInfo.states,
247           careStatesArray,
248                   0,
249           McDcLevelNone_c);
250  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
251  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
252  andState =  mdd_xor(EXEFState2,andState);
253  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
254
255
256
257  //mdd_FunctionPrintMain(mddManager, errorState, "ERROR", oFile);
258  //mdd_GetState_Values(mddManager , EFState, stdout);
259  fclose(oFile);
260
261
262
263
264
265  return 0;             /* normal exit */
266
267  usage:
268  (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
269  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
270  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
271  return 1;             /* error exit */
272}
273
[30]274/******************************************/
275/* function that build a bdd for the      */
276/* simple example :                       */
277/*     (state = 0) -> !(state = 1)        */
278/******************************************/
279mdd_t * buildDummyBdd(mdd_manager   *mddManager)
[27]280{
[30]281/** state0 = 0 **/
282 mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
283 mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
284 mdd_t * state0 =  mdd_one(mddManager);
285 state0 = mdd_and(s0,s1,1,1);
286/** state1 = 1 **/
287 mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
288 mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
289 mdd_t * state1 =  mdd_one(mddManager);
290 state1 = mdd_and(ns0,ns1,1,1);
291/** state = 0) -> !(state = 1) **/
292 mdd_t * rel =  mdd_one(mddManager);
293 rel =  mdd_or(state0,state1,0,0);
294 
295 return rel;
296}
[27]297
298
299/**Function********************************************************************
300
[30]301  Synopsis    [Implements the transtion command.]
[27]302
[30]303  CommandName [_transition]
[27]304
[30]305  CommandSynopsis [compute new transition relation]
[27]306
[30]307  CommandArguments [\[-h\] \[-v\]]
308 
309  CommandDescription [This command create a new transition relation that is a
310  and of the Bdd of the old one and an other bdd.
311  <p>
[27]312
[30]313  Command options:<p> 
[27]314
[30]315  <dl>
316  <dt> -h
317  <dd> Print the command usage.
318  </dl>
[27]319
[30]320  <dt> -v
321  <dd> Verbose mode.
322  </dl>
323  ]
[27]324
[30]325  SideEffects [Change the fsm]
[27]326
327******************************************************************************/
328
329static int 
[30]330CommandTransition (Hrc_Manager_t ** hmgr,
[27]331                   int  argc, char ** argv){
[30]332int            c;
333int            verbose = 0;              /* default value */
[27]334
[30]335/*
336 * Parse command line options.
337 */
338util_getopt_reset();
339while ((c = util_getopt(argc, argv, "vh")) != EOF) {
340  switch(c) {
341    case 'v':
342      verbose = 1;
343      break;
344    case 'h':
345      goto usage;
346    default:
347      goto usage;
[27]348  }
[30]349}
[27]350
[30]351if (verbose) {
352  (void) fprintf(vis_stdout, "The _transition is under construction.\n");
353}
[27]354
[30]355Fsm_Fsm_t      *fsm          = NIL(Fsm_Fsm_t);
356Ntk_Network_t  *network      = NIL(Ntk_Network_t);
357mdd_manager    *mddManager; 
358mdd_t          *rel          = NIL(mdd_t);
359graph_t        *partition;
360int            i;
361/******************/
362network      = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
363if(network == NIL(Ntk_Network_t))
364        return 1;
365fsm          = Fsm_HrcManagerReadCurrentFsm(*hmgr);
366if(fsm ==  NIL(Fsm_Fsm_t))
367        return 1;
368mddManager   = Fsm_FsmReadMddManager(fsm);
[27]369
370
371
[30]372/**********   Build cex  ***********/
373/* Here add the function           */
374/* that build the Bdd to and       */
375/* with the transtion relation     */
376/***********************************/
377rel = buildDummyBdd(mddManager);
378if(rel == NIL(mdd_t))
379{
380        fprintf(vis_stdout,"Problem when building the new relation bdd");
381        return 1;
[27]382}
383
[30]384/** Get image_info **/
385Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
386partition = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
387/**** The complete transtion relation ****/
388// array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0);
389/*****************************************/
390/*** For each latch rebuild the transition function ***/
391/*** mvf table is composed of mdd for each possible ***/
392/*** value of the latch                             ***/
393ImgFunctionData_t * functionData = &(imageInfo->functionData);
394array_t *roots = functionData->roots;
395array_t *rangeVarMddIdArray = functionData->rangeVars;
396char * nodeName;
397arrayForEachItem(char *, roots, i, nodeName) {
398        /* The new relation */ 
399        vertex_t *vertex = Part_PartitionFindVertexByName(partition, nodeName);
400    Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
401    int mddId = array_fetch(int, rangeVarMddIdArray, i);
402        mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);
403        mdd_t * n_relation = mdd_and(relation,rel,1,1);
404    /* Build for each possible value */
405        int nbValue = Mvf_FunctionReadNumComponents(mvf) ;
406        int v ;
407        Mvf_Function_t * newMvf = Mvf_FunctionAlloc(mddManager,nbValue);
408        for(v = 0; v<nbValue;v++)
409        {
410                 mdd_t * n_s1 =  mdd_eq_c(mddManager,mddId, v);
411                 mdd_t * n_rel_s1 = mdd_and(n_relation,n_s1,1,1);
412                 mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1);
413                 Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1);
[27]414
[30]415        }
416        /* Replace the function for the latch */
417        Part_VertexSetFunction(vertex, newMvf);
418//      printf("vertex %s changed % d\n",PartVertexReadName(vertex));
419        Mvf_FunctionFree(mvf);
[27]420}
421
[30]422/** Change the fsm **/
423fsm = Fsm_FsmCreateFromNetworkWithPartition(network, partition);
424mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
425Fsm_FsmComputeReachableStates(fsm,0,verbose,
426                                      0,0, 0,
427                                      0, 0, Fsm_Rch_Default_c,
428                                      0,1, NIL(array_t),
429                                      (verbose > 0),  NIL(array_t));
430if(verbose)
431        Fsm_FsmReachabilityPrintResults(fsm,3, 0);
432/** Change Image Info **/
433Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
434                                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
435                                          (void *) partition);
[27]436
437
[30]438return 0;               /* normal exit */
[27]439
[30]440usage:
441(void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
442(void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
443(void) fprintf(vis_stderr, "   -v\t\tverbose\n");
444return 1;               /* error exit */
[27]445
446}
447
448
Note: See TracBrowser for help on using the repository browser.