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

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

modify mv table
File size: 22.1 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  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}
403/**Function********************************************************************
404
405  Synopsis    [Implements the _Debug_test command.]
406
407  CommandName [_Debug_test]
408
409  CommandSynopsis [template for implementing commands]
410
411  CommandArguments [\[-h\] \[-v\]]
412 
413  CommandDescription [This command does nothing useful.  It merely serves as a
414  template for the implementation of new commands.<p>
415
416  Command options:<p> 
417
418  <dl>
419  <dt> -h
420  <dd> Print the command usage.
421  </dl>
422
423  <dt> -v
424  <dd> Verbose mode.
425  </dl>
426  ]
427
428  SideEffects []
429
430******************************************************************************/
431static int
432CommandDebug(
433  Hrc_Manager_t ** hmgr,
434  int  argc,
435  char ** argv)
436{
437  int            c;
438  int            verbose = 0;              /* default value */
439
440  /*
441   * Parse command line options.
442   */
443  util_getopt_reset();
444  while ((c = util_getopt(argc, argv, "vh")) != EOF) {
445    switch(c) {
446      case 'v':
447        verbose = 1;
448        break;
449      case 'h':
450        goto usage;
451      default:
452        goto usage;
453    }
454  }
455
456  if (verbose) {
457    (void) fprintf(vis_stdout, "The _Debug_test is under construction.\n");
458  }
459
460  Fsm_Fsm_t   *fsm        = Fsm_HrcManagerReadCurrentFsm(*hmgr);
461  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
462  printf("** DEBUG MODE **\n");
463  Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr);
464  printf("model : %s\n", Hrc_NodeReadModelName(n));
465
466  mdd_t * safe   = getSafe(fsm);
467  mdd_t * forbid = getForbidden(fsm);
468  mdd_t * reach  = getReach(fsm);
469 
470  if(safe == NIL(mdd_t))
471  {
472        printf("call command set_safe before\n");
473        return 1;
474  }
475  if(forbid == NIL(mdd_t))
476  {
477        printf("call command set_forbidden before\n");
478        return 1;
479  }
480
481  FILE*  oFile;
482  oFile = Cmd_FileOpen("safe_prop", "w", NIL(char *), 0);
483 // mdd_FunctionPrintMain(mddManager, safe, "SAFE", oFile);
484//  mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile);
485
486  mdd_t * EFState = mdd_and(reach,safe,1,1);
487//  mdd_t * errorState = mdd_and(reach,forbid,1,1);
488
489  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
490  array_t *careStatesArray = array_alloc(mdd_t *, 0);
491  array_insert(mdd_t *, careStatesArray, 0,mddOne);
492
493  mdd_t * tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
494                   EFState,
495           fsm->fairnessInfo.states,
496           careStatesArray,
497                   0,
498           McDcLevelNone_c);
499
500  mdd_t * EXEFState = mdd_and(reach,tmp_EXEFState,1,1);
501  mdd_FunctionPrintMain(mddManager, EXEFState, "EXEF", oFile);
502
503  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
504                   EXEFState,
505           fsm->fairnessInfo.states,
506           careStatesArray,
507                   0,
508           McDcLevelNone_c);
509  mdd_t * EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
510  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
511  mdd_t * andState =  mdd_xor(EXEFState2,EXEFState);
512  mdd_FunctionPrintMain(mddManager, andState, "XOR2", oFile);
513  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
514                   andState,
515           fsm->fairnessInfo.states,
516           careStatesArray,
517                   0,
518           McDcLevelNone_c);
519  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
520  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
521  andState =  mdd_xor(EXEFState2,andState);
522  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
523  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
524                   andState,
525           fsm->fairnessInfo.states,
526           careStatesArray,
527                   0,
528           McDcLevelNone_c);
529  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
530  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
531  andState =  mdd_xor(EXEFState2,andState);
532  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
533
534
535
536  //mdd_FunctionPrintMain(mddManager, errorState, "ERROR", oFile);
537  //mdd_GetState_Values(mddManager , EFState, stdout);
538  fclose(oFile);
539
540
541
542
543
544  return 0;             /* normal exit */
545
546  usage:
547  (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
548  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
549  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
550  return 1;             /* error exit */
551}
552
553/******************************************/
554/* function that build a bdd for the      */
555/* simple example :                       */
556/*     (state = 0) -> !(state = 1)        */
557/******************************************/
558mdd_t * buildDummyBdd(mdd_manager   *mddManager)
559{
560/** state0 = 0 **/
561 mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
562 mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
563 mdd_t * state0 =  mdd_one(mddManager);
564 state0 = mdd_and(s0,s1,1,1);
565/** state1 = 1 **/
566 mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
567 mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
568 mdd_t * state1 =  mdd_one(mddManager);
569 state1 = mdd_and(ns0,ns1,1,1);
570/** state = 0) -> !(state = 1) **/
571 mdd_t * rel =  mdd_one(mddManager);
572 rel =  mdd_or(state0,state1,0,0);
573 
574 return rel;
575}
576
577
578/**Function********************************************************************
579
580  Synopsis    [Implements the transtion command.]
581
582  CommandName [_transition]
583
584  CommandSynopsis [compute new transition relation]
585
586  CommandArguments [\[-h\] \[-v\]]
587 
588  CommandDescription [This command create a new transition relation that is a
589  and of the Bdd of the old one and an other bdd.
590  <p>
591
592  Command options:<p> 
593
594  <dl>
595  <dt> -h
596  <dd> Print the command usage.
597  </dl>
598
599  <dt> -v
600  <dd> Verbose mode.
601  </dl>
602  ]
603
604  SideEffects [Change the fsm]
605
606******************************************************************************/
607
608static int 
609CommandTransition (Hrc_Manager_t ** hmgr,
610                   int  argc, char ** argv){
611int            c;
612int            verbose = 0;              /* default value */
613
614/*
615 * Parse command line options.
616 */
617util_getopt_reset();
618while ((c = util_getopt(argc, argv, "vh")) != EOF) {
619  switch(c) {
620    case 'v':
621      verbose = 1;
622      break;
623    case 'h':
624      goto usage;
625    default:
626      goto usage;
627  }
628}
629
630if (verbose) {
631  (void) fprintf(vis_stdout, "The _transition is under construction.\n");
632}
633
634Fsm_Fsm_t      *fsm          = NIL(Fsm_Fsm_t);
635Ntk_Network_t  *network      = NIL(Ntk_Network_t);
636mdd_manager    *mddManager; 
637mdd_t          *rel          = NIL(mdd_t);
638graph_t        *partition;
639int            i;
640/******************/
641network      = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
642if(network == NIL(Ntk_Network_t))
643        return 1;
644fsm          = Fsm_HrcManagerReadCurrentFsm(*hmgr);
645if(fsm ==  NIL(Fsm_Fsm_t))
646        return 1;
647mddManager   = Fsm_FsmReadMddManager(fsm);
648
649
650
651/**********   Build cex  ***********/
652/* Here add the function           */
653/* that build the Bdd to and       */
654/* with the transtion relation     */
655/***********************************/
656rel = buildDummyBdd(mddManager);
657if(rel == NIL(mdd_t))
658{
659        fprintf(vis_stdout,"Problem when building the new relation bdd");
660        return 1;
661}
662
663/** Get image_info **/
664Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
665partition = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
666/**** The complete transtion relation ****/
667// array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0);
668/*****************************************/
669/*** For each latch rebuild the transition function ***/
670/*** mvf table is composed of mdd for each possible ***/
671/*** value of the latch                             ***/
672ImgFunctionData_t * functionData = &(imageInfo->functionData);
673array_t *roots = functionData->roots;
674array_t *rangeVarMddIdArray = functionData->rangeVars;
675char * nodeName;
676arrayForEachItem(char *, roots, i, nodeName) {
677        /* The new relation */ 
678        vertex_t *vertex = Part_PartitionFindVertexByName(partition, nodeName);
679    Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
680    int mddId = array_fetch(int, rangeVarMddIdArray, i);
681        mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);
682        mdd_t * n_relation = mdd_and(relation,rel,1,1);
683    /* Build for each possible value */
684        int nbValue = Mvf_FunctionReadNumComponents(mvf) ;
685        int v ;
686        Mvf_Function_t * newMvf = Mvf_FunctionAlloc(mddManager,nbValue);
687        for(v = 0; v<nbValue;v++)
688        {
689                 mdd_t * n_s1 =  mdd_eq_c(mddManager,mddId, v);
690                 mdd_t * n_rel_s1 = mdd_and(n_relation,n_s1,1,1);
691                 mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1);
692                 Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1);
693
694        }
695        /* Replace the function for the latch */
696        Part_VertexSetFunction(vertex, newMvf);
697//      printf("vertex %s changed % d\n",PartVertexReadName(vertex));
698        Mvf_FunctionFree(mvf);
699}
700
701/** Change the fsm **/
702fsm = Fsm_FsmCreateFromNetworkWithPartition(network, partition);
703mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
704Fsm_FsmComputeReachableStates(fsm,0,verbose,
705                                      0,0, 0,
706                                      0, 0, Fsm_Rch_Default_c,
707                                      0,1, NIL(array_t),
708                                      (verbose > 0),  NIL(array_t));
709if(verbose)
710        Fsm_FsmReachabilityPrintResults(fsm,3, 0);
711/** Change Image Info **/
712Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
713                                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
714                                          (void *) partition);
715
716
717return 0;               /* normal exit */
718
719usage:
720(void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
721(void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
722(void) fprintf(vis_stderr, "   -v\t\tverbose\n");
723return 1;               /* error exit */
724
725}
726
727
Note: See TracBrowser for help on using the repository browser.