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

Last change on this file was 104, checked in by cecile, 12 years ago

add begining for composition
File size: 37.2 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);
67static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
68static int CommandBuildCexBdd(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
69static int CommandComposeWithCex(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
70
71
72
73/**AutomaticEnd***************************************************************/
74
75
76/*---------------------------------------------------------------------------*/
77/* Definition of exported functions                                          */
78/*---------------------------------------------------------------------------*/
79
80/**Function********************************************************************
81
82  Synopsis    [Initializes the test package.]
83
84  SideEffects []
85
86  SeeAlso     [Debug_End]
87
88******************************************************************************/
89void
90Debug_Init(void)
91{
92  /*
93   * Add a command to the global command table.  By using the leading
94   * underscore, the command will be listed under "help -a" but not "help".
95   */
96  Cmd_CommandAdd("_debug_test",  CommandDebug, /* doesn't changes_network */ 0);
97  Cmd_CommandAdd("_transition",  CommandTransition, 1);
98  Cmd_CommandAdd("_sat_debug",   CommandSatDebug, 0);
99  Cmd_CommandAdd("_createAbn",   CommandCreateAbnormal, 1);
100  Cmd_CommandAdd("_cexbdd",      CommandBuildCexBdd, 0);
101  Cmd_CommandAdd("print_network_cnf",  CommandGenerateNetworkCNF, 0);
102  Cmd_CommandAdd("_compose",  CommandComposeWithCex, 1);
103
104}
105
106
107/**Function********************************************************************
108
109  Synopsis    [Ends the test package.]
110
111  SideEffects []
112
113  SeeAlso     [Debug_Init]
114
115******************************************************************************/
116void
117Debug_End(void)
118{
119  /*
120   * For example, free any global memory (if any) which the test package is
121   * responsible for.
122   */
123}
124
125
126/*---------------------------------------------------------------------------*/
127/* Definition of internal functions                                          */
128/*---------------------------------------------------------------------------*/
129
130
131/*---------------------------------------------------------------------------*/
132/* Definition of static functions                                            */
133/*---------------------------------------------------------------------------*/
134
135
136static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr, int  argc, char ** argv)
137{
138  Ntk_Network_t * ntk;
139  int c,verbose = 0;
140  array_t * excludes = NIL(array_t);
141  Dbg_Abnormal_t * abnormal;
142  ntk = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
143  char * subs;
144  if (ntk == NIL(Ntk_Network_t)) {
145        (void) fprintf(vis_stdout, "** abn error: No network\n");
146        return 1;
147  }
148  while ((c = util_getopt(argc, argv, "vhs:")) != EOF) {
149        switch(c) {
150        case 'h':
151          goto usage;
152                case 'v':
153                        verbose = 1;
154                        break;
155        case 's':
156            subs =  util_strsav(util_optarg);
157            excludes = array_alloc(char*,0);
158            array_insert_last(char*,excludes,subs);
159            break;
160        default :
161          goto usage;
162                }
163 }
164  abnormal = Dbg_DebugAbnormalAlloc(ntk);
165  abnormal->verbose = verbose;
166    printf("SUBS %s \n",subs);
167  Dbg_AddAbnormalPredicatetoNetwork(abnormal,excludes);
168  printf("\t # Abnormal predicate created  %d\n", array_n(abnormal->abnormal));
169    return 0;
170  usage : 
171   (void) fprintf(vis_stderr, "usage: _createAbn [-h] [-v verboseLevel] [-s substystem excludes\n");
172  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");
173  (void) fprintf(vis_stderr, "   -v  \t verbosity\n");
174  (void) fprintf(vis_stderr, "   -s <subsystemName> \texclude the abnormal predicate\
175  for this subssytem\n");
176  return 1;
177}
178
179/**Function********************************************************************
180
181  Synopsis    [Implements the _sat_debug command.]
182
183  CommandName [_sat_debug]
184
185  CommandSynopsis [locate faulty candidates]
186
187  CommandArguments [\[-h\] \[-v\]]
188 
189  CommandDescription [This command compute the fault candidates of a given
190  properties.<p>
191
192  Command options:<p> 
193
194  <dl>
195  <dt> -h
196  <dd> Print the command usage.
197  </dl>
198
199  <dt> -v
200  <dd> Verbose mode.
201  </dl>
202  ]
203
204  SideEffects []
205
206******************************************************************************/
207static int 
208CommandSatDebug(
209Hrc_Manager_t ** hmgr, 
210int argc, 
211char ** argv){
212int            c,i;
213int            verbose = 0;              /* default value */
214BmcOption_t      * options = BmcOptionAlloc();
215Ntk_Network_t    * network;
216bAig_Manager_t   * manager;
217array_t          * formulaArray;
218array_t          * LTLformulaArray;
219array_t          * faultNodes = array_alloc(Ntk_Node_t*,0);
220
221/*
222 * Parse command line options.
223 */
224if ((options = ParseBmcOptions(argc, argv)) == NIL(BmcOption_t)) {
225     return 1;
226}
227
228
229
230if (verbose) {
231  (void) fprintf(vis_stdout, "The _sat_debug command is under construction.\n");
232}
233/*
234 *  Read the network
235 */
236network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
237if (network == NIL(Ntk_Network_t)) {
238  (void) fprintf(vis_stdout, "** _sat_debug error: No network\n");
239  BmcOptionFree(options);
240  return 1;
241}
242manager = Ntk_NetworkReadMAigManager(network);
243if (manager == NIL(mAig_Manager_t)) {
244  (void) fprintf(vis_stdout, "** _sat_debug error: run build_partition_maigs command first\n");
245  BmcOptionFree(options);
246  return 1;
247}
248
249Dbg_Abnormal_t * abn = Dbg_NetworkReadAbnormal(network);
250if(abn == NIL(Dbg_Abnormal_t)){
251  (void) fprintf(vis_stdout, "_sat_debug error: Build Abnormal predicate.\n");
252  return 1;
253}
254if(verbose)
255  printf("abnormal %d \n",array_n(Dbg_ReadAbn(abn)));
256
257
258formulaArray  = Ctlsp_FileParseFormulaArray(options->ltlFile);
259if (formulaArray == NIL(array_t)) {
260  (void) fprintf(vis_stderr,
261           "** bmc error: error in parsing CTL* Fromula from file\n");
262  BmcOptionFree(options);
263  return 1;
264}
265if (array_n(formulaArray) == 0) {
266  (void) fprintf(vis_stderr, "** bmc error: No formula in file\n");
267  BmcOptionFree(options);
268  Ctlsp_FormulaArrayFree(formulaArray);
269  return 1;
270}
271LTLformulaArray = Ctlsp_FormulaArrayConvertToLTL(formulaArray);
272Ctlsp_FormulaArrayFree(formulaArray);
273if (LTLformulaArray ==  NIL(array_t)){
274  (void) fprintf(vis_stdout, "** bmc error: Invalid LTL formula\n");
275  BmcOptionFree(options);
276  return 1;
277}
278Ctlsp_Formula_t *ltlFormula  = array_fetch(Ctlsp_Formula_t *, LTLformulaArray, 0);
279
280
281 /*
282    Compute the cone of influence
283        here : a list of state variables (latches)
284    TODO refine to COI of the property
285  */
286        st_table        *CoiTable =  generateAllLatches(network);
287  /*
288      Generate clauses for each time frame.  This is the old way of generating
289      clauses in BMC.
290    */
291        if(verbose)
292        {       
293                (void) fprintf(vis_stdout, "------      COI       ----\n");
294                printLatch(CoiTable);
295                (void) fprintf(vis_stdout, "--------------------------\n");
296    }
297    BmcCnfClauses_t* cnfClauses =  Dbg_GenerateCNF(network,options,CoiTable);
298
299
300    //Generate ltl CNF
301    // BmcGenerateCnfForLtl Génére la formule borné et retourne un index
302    // aprÚs il faut ajouter l'objectif de l'index avec boucle ou pas ...
303    // cf. BmcLtlVerifyGeneralLtl
304    Ctlsp_FormulaPrint(vis_stdout, ltlFormula);
305    fprintf(vis_stdout, "\n");
306    int k = options->maxK;
307    int l;
308    // return the clause number
309    int noLoopIndex = BmcGenerateCnfForLtl(network, ltlFormula, 0, k, k, cnfClauses);    printf("LTL %d  \n",noLoopIndex);
310   
311
312        array_t *objClause = NIL(array_t);
313        objClause = array_alloc(int, 0);   
314        array_insert_last(int, objClause, noLoopIndex);
315        BmcCnfInsertClause(cnfClauses, objClause);
316    array_free(objClause);
317
318        //Add Abnormal
319    st_table * nodeToMvfAigTable =  NIL(st_table);
320    nodeToMvfAigTable =
321    (st_table *) Ntk_NetworkReadApplInfo(network, MVFAIG_NETWORK_APPL_KEY);
322    assert(nodeToMvfAigTable != NIL(st_table));
323
324    Dbg_InitAbn(abn,manager, nodeToMvfAigTable,k,cnfClauses);
325
326    //loop abnormal
327    int aIndex;
328    Ntk_Node_t * abnNode;
329    Dbg_ForEachAbnormal(abn,aIndex,abnNode){
330      char * nodeName =  Ntk_NodeReadName(abnNode);
331    //set abnormal for each step
332      array_t * cnfIndexArray = array_fetch(array_t*,abn->abnCnfIndexArray,aIndex);
333      int cnfIndex;
334      int step;
335      bAigEdge_t* abnBAig = array_fetch(bAigEdge_t*,abn->abnAigArray, aIndex);
336      array_t * cnfVal = array_alloc(int,0);
337      arrayForEachItem(int, cnfIndexArray, step, cnfIndex){
338        int abnIndex = BmcGenerateCnfFormulaForAigFunction(manager,abnBAig[1],step,cnfClauses);
339        array_insert(int,cnfClauses->clauseArray,cnfIndex,abnIndex);
340        array_insert_last(int,cnfVal,abnIndex);
341        FILE *cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0);
342        BmcWriteClauses(manager, cnfFile, cnfClauses, options);
343        fclose(cnfFile);
344        printf("AINDEX %d\n",aIndex);
345        if(aIndex == 0)
346        {
347        FILE *cnfFile = Cmd_FileOpen("test_aks.cnf", "w", NIL(char *), 0);
348        BmcWriteClauses(manager, cnfFile, cnfClauses, options);
349        fclose(cnfFile);
350         
351        }
352      }//end for each step
353
354      //SAT procedure
355      //assig assig input from cex
356      //TODO build cex correctly
357      int res = Dbg_SatCheck("assig",options->satInFile,options->verbosityLevel);
358      // Build set of FaultCandidates
359      if (res == SAT_SAT)
360      {
361        char * realNodeName = util_strsav(nodeName);
362        realNodeName[strlen(nodeName)-3] = '\0';
363        printf("Real = %s\n", realNodeName);
364        Ntk_Node_t * realNode =  Ntk_NetworkFindNodeByName(network,realNodeName);
365        array_insert_last(Ntk_Node_t*,faultNodes,realNode);
366      }
367
368      arrayForEachItem(int, cnfIndexArray, step, cnfIndex){
369        int abnIndex = array_fetch(int,cnfVal,step);       
370        array_insert(int,cnfClauses->clauseArray,cnfIndex,-abnIndex);
371      }
372   }
373
374         if(verbose)
375                (void) fprintf(vis_stdout, "The _sat_debug generates %d clauses with %d\
376                latches \n",cnfClauses->noOfClauses,st_count(CoiTable));
377 
378   
379        (void) fprintf(vis_stdout,"Number of Fault candidates %d\n",
380    array_n(faultNodes));
381        (void) fprintf(vis_stdout,"gates : \n");
382
383
384    printNodeArray(faultNodes);
385
386   
387Ctlsp_FormulaArrayFree(LTLformulaArray);   
388BmcCnfClausesFree(cnfClauses);
389BmcOptionFree(options);
390array_free(faultNodes);
391return 0;
392}
393
394/**Function********************************************************************
395
396  Synopsis    [Implements the generate_network_cnf.]
397
398  CommandName [generate_network_cnf]
399
400  CommandSynopsis [generate a CNF view of the network]
401
402  CommandArguments [\[-h\] \[-v\] \[-k\]  [fileName] ]
403 
404  CommandDescription [This command generate a CNF of the network in DMACS form.
405  The network may be unroll within k steps.
406  <p>
407
408  Command options:<p> 
409
410  <dl>
411  <dt> -h
412  <dd> Print the command usage.
413  </dl>
414
415  <dt> -v
416  <dd> Verbose mode.
417  </dl>
418
419  <dt> -k
420  <dd> number of steps (default 1).
421  </dl>
422  ]
423
424  SideEffects []
425
426******************************************************************************/
427
428static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int  argc, char ** argv)
429{
430  BmcOption_t  *options = BmcOptionAlloc();
431  int c;
432  unsigned int i;
433  Ntk_Network_t * network;
434  bAig_Manager_t   * manager;
435  char *  outName = NIL(char);
436   FILE *cnfFile;
437  if (!options){
438    return 1;
439  }
440  options->dbgOut = 0;
441  /*
442   * Parse command line options.
443   */
444  util_getopt_reset();
445  while ((c = util_getopt(argc, argv, "hv:k:")) != EOF) {
446    switch(c) {
447    case 'h':
448      goto usage;
449    case 'k':
450      options->maxK = atoi(util_optarg);
451      break;
452    case 'v':
453      for (i = 0; i < strlen(util_optarg); i++) {
454        if (!isdigit((int)util_optarg[i])) {
455          goto usage;
456        }
457      }
458      options->verbosityLevel = (Bmc_VerbosityLevel) atoi(util_optarg);
459      break;
460    default:
461      goto usage;
462    }
463  }
464   if (argc - util_optind != 0)
465   {
466     outName  = util_strsav(argv[util_optind]);
467     /* create SAT Solver input file */
468     options->cnfFileName= outName;
469     options->satInFile = options->cnfFileName;
470     cnfFile = Cmd_FileOpen(options->satInFile, "w", NIL(char *), 0); 
471  }
472 
473 
474/*
475 *  Read the network
476 */
477network = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
478if (network == NIL(Ntk_Network_t)) {
479  (void) fprintf(vis_stdout, "** generate_network_cnf error: No network\n");
480  BmcOptionFree(options);
481  return 1;
482}
483manager = Ntk_NetworkReadMAigManager(network);
484if (manager == NIL(mAig_Manager_t)) {
485  (void) fprintf(vis_stdout, "** generate_network_cnf error: run build_partition_maigs command first\n");
486  BmcOptionFree(options);
487  return 1;
488}
489
490 /*
491    Compute the cone of influence
492        here : a list of state variables (latches)
493  */
494st_table        *CoiTable =  generateAllLatches(network);
495
496if(options->verbosityLevel)
497{       
498        (void) fprintf(vis_stdout, "------      COI       ----\n");
499        printLatch(CoiTable);
500        (void) fprintf(vis_stdout, "--------------------------\n");
501}
502BmcCnfClauses_t* cnfClauses =  Dbg_GenerateCNF(network,options,CoiTable);
503  if(outName != NIL(char))
504  {
505    BmcWriteClauses(manager, cnfFile, cnfClauses, options);
506    fclose(cnfFile);
507  }
508  else
509     BmcWriteClauses(manager, vis_stdout, cnfClauses, options);
510
511if(options->verbosityLevel)
512{       
513        (void) fprintf(vis_stdout, "CNF generated for %d steps", options->maxK);
514    (void) fprintf(vis_stdout, " %d clauses with %d latche(s).\n",cnfClauses->noOfClauses,
515    st_count(CoiTable));
516} 
517   
518BmcOptionFree(options);
519 return 0;
520 usage:
521  (void) fprintf(vis_stderr, "usage: bmc [-h][-k maximum_length][-v verbosity_level] <cnf_file>\n");
522  (void) fprintf(vis_stderr, "   -h \tprint the command usage\n");
523  (void) fprintf(vis_stderr, "   -k \tmaximum length of counterexample to be checked (default is 1)\n");
524  (void) fprintf(vis_stderr, "   -v <verbosity_level>\n");
525  (void) fprintf(vis_stderr, "       verbosity_level = 0 => no feedback (Default)\n");
526  (void) fprintf(vis_stderr, "       verbosity_level = 1 => code status\n");
527  (void) fprintf(vis_stderr, "       verbosity_level = 2 => code status and CPU usage profile\n");
528  (void) fprintf(vis_stderr, "   <cnf_file> The output file containing CNF of the network.\n");
529
530  BmcOptionFree(options);
531  return 1;
532}
533
534/**Function********************************************************************
535
536  Synopsis    [Implements the _Debug_test command.]
537
538  CommandName [_Debug_test]
539
540  CommandSynopsis [template for implementing commands]
541
542  CommandArguments [\[-h\] \[-v\]]
543 
544  CommandDescription [This command does nothing useful.  It merely serves as a
545  template for the implementation of new commands.<p>
546
547  Command options:<p> 
548
549  <dl>
550  <dt> -h
551  <dd> Print the command usage.
552  </dl>
553
554  <dt> -v
555  <dd> Verbose mode.
556  </dl>
557  ]
558
559  SideEffects []
560
561******************************************************************************/
562static int
563CommandDebug(
564  Hrc_Manager_t ** hmgr,
565  int  argc,
566  char ** argv)
567{
568  int            c;
569  int            verbose = 0;              /* default value */
570
571  /*
572   * Parse command line options.
573   */
574  util_getopt_reset();
575  while ((c = util_getopt(argc, argv, "vh")) != EOF) {
576    switch(c) {
577      case 'v':
578        verbose = 1;
579        break;
580      case 'h':
581        goto usage;
582      default:
583        goto usage;
584    }
585  }
586
587  if (verbose) {
588    (void) fprintf(vis_stdout, "The _Debug_test is under construction.\n");
589  }
590
591  Fsm_Fsm_t   *fsm        = Fsm_HrcManagerReadCurrentFsm(*hmgr);
592  mdd_manager *mddManager = Fsm_FsmReadMddManager(fsm);
593  printf("** DEBUG MODE **\n");
594  Hrc_Node_t * n = Hrc_ManagerReadRootNode(*hmgr);
595  printf("model : %s\n", Hrc_NodeReadModelName(n));
596
597  mdd_t * safe   = getSafe(fsm);
598  mdd_t * forbid = getForbidden(fsm);
599  mdd_t * reach  = getReach(fsm);
600 
601  if(safe == NIL(mdd_t))
602  {
603        printf("call command set_safe before\n");
604        return 1;
605  }
606  if(forbid == NIL(mdd_t))
607  {
608        printf("call command set_forbidden before\n");
609        return 1;
610  }
611
612  FILE*  oFile;
613  oFile = Cmd_FileOpen("safe_prop", "w", NIL(char *), 0);
614 // mdd_FunctionPrintMain(mddManager, safe, "SAFE", oFile);
615//  mdd_FunctionPrintMain(mddManager, reach, "REACH", oFile);
616
617  mdd_t * EFState = mdd_and(reach,safe,1,1);
618//  mdd_t * errorState = mdd_and(reach,forbid,1,1);
619
620  mdd_t *mddOne = mdd_one(Fsm_FsmReadMddManager(fsm));
621  array_t *careStatesArray = array_alloc(mdd_t *, 0);
622  array_insert(mdd_t *, careStatesArray, 0,mddOne);
623
624  mdd_t * tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
625                   EFState,
626           fsm->fairnessInfo.states,
627           careStatesArray,
628                   0,
629           McDcLevelNone_c);
630
631  mdd_t * EXEFState = mdd_and(reach,tmp_EXEFState,1,1);
632  mdd_FunctionPrintMain(mddManager, EXEFState, "EXEF", oFile);
633
634  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
635                   EXEFState,
636           fsm->fairnessInfo.states,
637           careStatesArray,
638                   0,
639           McDcLevelNone_c);
640  mdd_t * EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
641  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
642  mdd_t * andState =  mdd_xor(EXEFState2,EXEFState);
643  mdd_FunctionPrintMain(mddManager, andState, "XOR2", oFile);
644  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
645                   andState,
646           fsm->fairnessInfo.states,
647           careStatesArray,
648                   0,
649           McDcLevelNone_c);
650  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
651  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
652  andState =  mdd_xor(EXEFState2,andState);
653  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
654  tmp_EXEFState = Mc_FsmEvaluateEXFormula( fsm,
655                   andState,
656           fsm->fairnessInfo.states,
657           careStatesArray,
658                   0,
659           McDcLevelNone_c);
660  EXEFState2 = mdd_and(reach,tmp_EXEFState,1,1);
661  mdd_FunctionPrintMain(mddManager, EXEFState2, "EXEF2", oFile);
662  andState =  mdd_xor(EXEFState2,andState);
663  mdd_FunctionPrintMain(mddManager, andState, "XOR", oFile);
664
665
666
667  //mdd_FunctionPrintMain(mddManager, errorState, "ERROR", oFile);
668  //mdd_GetState_Values(mddManager , EFState, stdout);
669  fclose(oFile);
670
671
672
673
674
675  return 0;             /* normal exit */
676
677  usage:
678  (void) fprintf(vis_stderr, "usage: _Debug_test [-h] [-v]\n");
679  (void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
680  (void) fprintf(vis_stderr, "   -v\t\tverbose\n");
681  return 1;             /* error exit */
682}
683
684/******************************************/
685/* function that build a bdd for the      */
686/* simple example :                       */
687/*     (state = 0) -> !(state = 1)        */
688/******************************************/
689mdd_t * buildDummyBdd(mdd_manager   *mddManager)
690{
691/** state0 = 0 **/
692 mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
693 mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
694 mdd_t * state0 =  mdd_one(mddManager);
695 state0 = mdd_and(s0,s1,1,1);
696/** state1 = 1 **/
697 mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
698 mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
699 mdd_t * state1 =  mdd_one(mddManager);
700 state1 = mdd_and(ns0,ns1,1,1);
701/** state = 0) -> !(state = 1) **/
702 mdd_t * rel =  mdd_one(mddManager);
703 rel =  mdd_or(state0,state1,0,0);
704 
705 return rel;
706}
707mdd_t * buildDummy2(mdd_manager * mddManager)
708{
709 mdd_t * rel = NIL(mdd_t);
710 mdd_t * state0 = mdd_one(mddManager);
711 mdd_t * state2 = mdd_one(mddManager);
712 mdd_t * state3 = mdd_one(mddManager);
713  // state0 = s0
714 mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
715 mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
716 state0 = mdd_and(s0,s1,1,1);
717  // state2 = s2
718 s0 =  mdd_eq_c(mddManager,0, 0);
719 s1 =  mdd_eq_c(mddManager,2, 1);
720 state2 = mdd_and(s0,s1,1,1);
721  // state3 = s3
722 s0 =  mdd_eq_c(mddManager,0, 1);
723 s1 =  mdd_eq_c(mddManager,2, 1);
724 state3 = mdd_and(s0,s1,1,1);
725// Build transition relation
726
727 array_t * mvarVal = array_alloc(int,0);
728 array_insert_last(int, mvarVal,2);
729 array_t * val = array_alloc(int,0);
730 array_t * mvarName = array_alloc(char*,0);
731 array_insert_last(char*, mvarName,"S1");
732 int e1Id = mdd_create_variables(mddManager,mvarVal,mvarName,NIL(array_t));
733 array_insert(char*, mvarName,0,"I");
734 int e0Id = mdd_create_variables(mddManager,mvarVal,mvarName,NIL(array_t));
735 array_insert_last(int, val,1);
736 mdd_t * e1 = mdd_literal(mddManager, e1Id,val);
737 mdd_t * e0 = mdd_literal(mddManager, e0Id,val);
738 mdd_t * tmp2 = mdd_and(e1,e0,0,0);
739mdd_t *  ne2_1 = mdd_or(e1,tmp2,1,1);
740mdd_t *  ne2_0 = mdd_and(e1,e0,0,1);
741
742array_insert(char*, mvarName,0,"Next_SI");
743int id = mdd_create_variables(mddManager,mvarVal,mvarName,NIL(array_t));
744Mvf_Function_t * mvf = Mvf_FunctionAlloc(mddManager, 2);
745Mvf_FunctionAddMintermsToComponent(mvf,1,ne2_1);
746Mvf_FunctionAddMintermsToComponent(mvf,0,ne2_0);
747mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, id);
748
749//bdd_print(relation);
750mdd_FunctionPrintMain (mddManager ,relation,"news",vis_stdout);
751 //bdd_ite
752 return rel;
753
754}
755
756/**Function********************************************************************
757
758  Synopsis    [Implements the transtion command.]
759
760  CommandName [_transition]
761
762  CommandSynopsis [compute new transition relation]
763
764  CommandArguments [\[-h\] \[-v\]]
765 
766  CommandDescription [This command create a new transition relation that is a
767  and of the Bdd of the old one and another bdd.
768  <p>
769
770  Command options:<p> 
771
772  <dl>
773  <dt> -h
774  <dd> Print the command usage.
775  </dl>
776
777  <dt> -v
778  <dd> Verbose mode.
779  </dl>
780  ]
781
782  SideEffects [Change the fsm]
783
784******************************************************************************/
785
786static int 
787CommandTransition (Hrc_Manager_t ** hmgr,
788                   int  argc, char ** argv){
789int            c;
790int            verbose = 0;              /* default value */
791
792/*
793 * Parse command line options.
794 */
795util_getopt_reset();
796while ((c = util_getopt(argc, argv, "vh")) != EOF) {
797  switch(c) {
798    case 'v':
799      verbose = 1;
800      break;
801    case 'h':
802      goto usage;
803    default:
804      goto usage;
805  }
806}
807
808if (verbose) {
809  (void) fprintf(vis_stdout, "The _transition is under construction.\n");
810}
811
812Fsm_Fsm_t      *fsm          = NIL(Fsm_Fsm_t);
813Ntk_Network_t  *network      = NIL(Ntk_Network_t);
814mdd_manager    *mddManager; 
815mdd_t          *rel          = NIL(mdd_t);
816graph_t        *partition;
817int            i;
818/******************/
819network      = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
820if(network == NIL(Ntk_Network_t))
821        return 1;
822fsm          = Fsm_HrcManagerReadCurrentFsm(*hmgr);
823if(fsm ==  NIL(Fsm_Fsm_t))
824        return 1;
825mddManager   = Fsm_FsmReadMddManager(fsm);
826
827
828
829/**********   Build cex  ***********/
830/* Here add the function           */
831/* that build the Bdd to and       */
832/* with the transtion relation     */
833/***********************************/
834rel = buildDummyBdd(mddManager);
835if(rel == NIL(mdd_t))
836{
837        fprintf(vis_stdout,"Problem when building the new relation bdd\n");
838        return 1;
839}
840if (verbose)
841  mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout);
842
843
844/** Get image_info **/
845Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
846partition = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
847/**** The complete transtion relation ****/
848// array_t * transRelation = Img_GetPartitionedTransitionRelation(imageInfo, 0);
849/*****************************************/
850/*** For each latch rebuild the transition function ***/
851/*** mvf table is composed of mdd for each possible ***/
852/*** value of the latch                             ***/
853ImgFunctionData_t * functionData = &(imageInfo->functionData);
854array_t *roots = functionData->roots;
855array_t *rangeVarMddIdArray = functionData->rangeVars;
856char * nodeName;
857arrayForEachItem(char *, roots, i, nodeName) {
858 
859        /* The new relation */ 
860        vertex_t *vertex = Part_PartitionFindVertexByName(partition, nodeName);
861    Mvf_Function_t *mvf = Part_VertexReadFunction(vertex);
862    int mddId = array_fetch(int, rangeVarMddIdArray, i);
863        mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);
864    if(verbose){
865      int x;
866      mdd_t * comp;
867
868      Mvf_FunctionForEachComponent( mvf, x, comp){
869        printf("%s,%d mdd %d ",nodeName,x,mddId);
870        mdd_FunctionPrintMain (mddManager ,comp,"MVF",vis_stdout);
871      }
872    }
873
874        mdd_t * n_relation = mdd_and(relation,rel,1,1);
875    /* Build for each possible value */
876        int nbValue = Mvf_FunctionReadNumComponents(mvf) ;
877        int v ;
878        Mvf_Function_t * newMvf = Mvf_FunctionAlloc(mddManager,nbValue);
879        for(v = 0; v<nbValue;v++)
880        {
881                 mdd_t * n_s1 =  mdd_eq_c(mddManager,mddId, v);
882                 mdd_t * n_rel_s1 = mdd_and(n_relation,n_s1,1,1);
883                 mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1);
884                 Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1);
885
886
887        }
888        /* Replace the function for the latch */
889        Part_VertexSetFunction(vertex, newMvf);
890//      printf("vertex %s changed % d\n",PartVertexReadName(vertex));
891}
892
893/** Change the fsm and the network with a new partition and the new fsm **/
894Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
895                                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
896                                          (void *) partition);
897fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t));
898mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
899mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose,
900                                      0,0, 0,
901                                      0, 0, Fsm_Rch_Default_c,
902                                      0,1, NIL(array_t),
903                                      (verbose > 0),  NIL(array_t));
904fsm->reachabilityInfo.initialStates = init;
905fsm->reachabilityInfo.reachableStates = reach;
906if(verbose)
907        Fsm_FsmReachabilityPrintResults(fsm,3, 0);
908
909Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY,
910                         (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
911                         (void *) fsm);
912
913return 0;               /* normal exit */
914
915usage:
916(void) fprintf(vis_stderr, "usage: _transition [-h] [-v]\n");
917(void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
918(void) fprintf(vis_stderr, "   -v\t\tverbose\n");
919return 1;               /* error exit */
920
921}
922
923static int 
924CommandBuildCexBdd(Hrc_Manager_t ** hmgr,
925                   int  argc, char ** argv){
926int            c;
927int            verbose = 0;              /* default value */
928
929/*
930 * Parse command line options.
931 */
932util_getopt_reset();
933while ((c = util_getopt(argc, argv, "vh")) != EOF) {
934  switch(c) {
935    case 'v':
936      verbose = 1;
937      break;
938    case 'h':
939      goto usage;
940    default:
941      goto usage;
942  }
943}
944
945if (verbose) {
946  (void) fprintf(vis_stdout, "The _cexBdd is under construction.\n");
947}
948
949Fsm_Fsm_t      *fsm          = NIL(Fsm_Fsm_t);
950Ntk_Network_t  *network      = NIL(Ntk_Network_t);
951mdd_manager    *mddManager; 
952Hrc_Manager_t  *hmgrCex       = NIL(Hrc_Manager_t);
953Fsm_Fsm_t      *fsmCex        = NIL(Fsm_Fsm_t);
954Ntk_Network_t  *networkCex    = NIL(Ntk_Network_t);
955mdd_t          *rel           = NIL(mdd_t);
956int            i;
957/******************/
958network      = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
959if(network == NIL(Ntk_Network_t))
960        return 1;
961fsm          = Fsm_HrcManagerReadCurrentFsm(*hmgr);
962if(fsm ==  NIL(Fsm_Fsm_t))
963        return 1;
964mddManager   = Fsm_FsmReadMddManager(fsm);
965
966mdd_t * initOrig  = Fsm_FsmComputeInitialStates(fsm);
967mdd_FunctionPrintMain (mddManager ,initOrig,"INIT_ORG",vis_stdout);
968
969/**********   Build cex  ***********/
970/* Here add the function           */
971/* that build the Bdd to and       */
972/* with the transtion relation     */
973/***********************************/
974//rel = buildDummyBdd(mddManager);
975 graph_t * part = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
976 vertex_t * v_s2 = Part_PartitionFindVertexByName(part, "cex.s2");
977Mvf_Function_t * newMvf  = Mvf_FunctionAlloc( mddManager,2);
978 mdd_t * s0 =  mdd_eq_c(mddManager,20, 0);
979 mdd_t * s1 =  mdd_eq_c(mddManager,22, 0);
980 mdd_t * state0 =  mdd_one(mddManager);
981 mdd_t * state1 =  mdd_one(mddManager);
982 state0 = mdd_and(s0,s1,1,1);
983 mdd_t * state12 = mdd_and(s0,s1,0,1);
984 state1 = mdd_not(state0);
985  array_insert(mdd_t *, newMvf, 1, state0);
986  array_insert(mdd_t *, newMvf, 0, state1);
987 mdd_t * ns1 =  mdd_eq_c(mddManager,17, 1);
988Mvf_Function_t * newNS  = Mvf_FunctionAlloc( mddManager,2);
989Mvf_FunctionAddMintermsToComponent(newNS,1, mdd_and(state0,ns1,1,1));
990Mvf_FunctionAddMintermsToComponent(newNS,0, mdd_and(state1,ns1,1,0));
991
992mdd_FunctionPrintMain(mddManager,Mvf_FunctionComputeDomain(newNS),"NS",vis_stdout);
993vertex_t * vert;
994vert = Part_PartitionFindVertexByName(part,"cex.s2");
995Part_VertexSetFunction(vert, newNS);
996
997vert = Part_PartitionFindVertexByName(part,"cex.s3");
998 mdd_t * ns1S3 =  mdd_eq_c(mddManager,14, 1);
999Mvf_Function_t * newS3  = Mvf_FunctionAlloc( mddManager,2);
1000Mvf_FunctionAddMintermsToComponent(newS3,1, mdd_and(state12,ns1S3,1,1));
1001Mvf_FunctionAddMintermsToComponent(newS3,0, mdd_and(state12,ns1S3,0,0));
1002Part_VertexSetFunction(vert, newS3);
1003
1004// Initial state
1005mdd_t * ns1Init =  mdd_eq_c(mddManager,3, 1);
1006
1007Mvf_Function_t * newNSInit  = Mvf_FunctionAlloc(mddManager,2);
1008Mvf_FunctionAddMintermsToComponent(newNSInit,1, mdd_and(state0,ns1Init,1,1));
1009Mvf_FunctionAddMintermsToComponent(newNSInit,0, mdd_and(state1,ns1Init,1,0));
1010mdd_FunctionPrintMain(mddManager,Mvf_FunctionComputeDomain(newNSInit),"NSINIT",vis_stdout);
1011Part_VertexSetFunction(Part_PartitionFindVertexByName(part,"cex.s2$INIT"),
1012newNSInit);
1013
1014
1015
1016
1017 /** Change the fsm and the network with a new partition and the new fsm **/
1018Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
1019                                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
1020                                          (void *) part);
1021fsm = Fsm_FsmCreateFromNetworkWithPartition(network, part);
1022
1023
1024mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
1025//mdd_t * n_init =  Mvf_MddComposeWithFunction(init, 17 , newMvf);
1026mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose,
1027                                      0,0, 0,
1028                                      0, 0, Fsm_Rch_Default_c,
1029                                      0,1, NIL(array_t),
1030                                      (verbose > 0),  NIL(array_t));
1031fsm->reachabilityInfo.initialStates = init;
1032fsm->reachabilityInfo.reachableStates = reach;
1033       
1034   
1035   
1036Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY,
1037                         (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
1038                         (void *) fsm); 
1039
1040Img_ImageInfoUpdateVariables(fsm->imageInfo,
1041                                 fsm->partition,
1042                                 fsm->fsmData.presentStateVars,
1043                                 fsm->fsmData.inputVars,
1044                                 fsm->fsmData.presentStateCube,
1045                                 fsm->fsmData.inputCube);
1046Fsm_FsmReachabilityPrintResults(fsm,3, 0);
1047//
1048//
1049mdd_FunctionPrintMain (mddManager ,init,"INIT",vis_stdout);
1050
1051return 0;               /* normal exit */
1052
1053usage:
1054(void) fprintf(vis_stderr, "usage: _BddCex [-h] [-v]\n");
1055(void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
1056(void) fprintf(vis_stderr, "   -v\t\tverbose\n");
1057return 1;               /* error exit */
1058
1059}
1060
1061
1062static int CommandComposeWithCex(Hrc_Manager_t ** hmgr,int  argc, char ** argv)
1063{
1064
1065  char * cexName;
1066  char * cexModelName;
1067  char * rootName;
1068  char * newName;
1069  FILE * cexFile;
1070  Hrc_Node_t * rootNode;
1071  Hrc_Node_t * cexNode;
1072  Hrc_Model_t * rootModel;
1073  Hrc_Model_t * cexModel;
1074  Hrc_Model_t * newModel;
1075  Hrc_Manager_t *  hmgrCex;
1076 // Ntk_Network_t * networkCex;
1077  array_t *cexActualInputArray, *cexActualOutputArray;
1078  array_t *actualInputArray, *actualOutputArray;
1079
1080  rootNode = Hrc_ManagerReadRootNode(*hmgr);
1081  if(rootNode == NIL(Hrc_Node_t)){
1082        printf("Please build the network first\n");
1083        return 1;
1084  }
1085  rootName = Hrc_NodeReadModelName(rootNode);
1086  rootModel =  Hrc_ManagerFindModelByName(*hmgr,rootName);
1087  if (argc - util_optind > 0)
1088   {
1089     cexName  = util_strsav(argv[util_optind]);
1090     cexFile = Cmd_FileOpen(cexName, "r", NIL(char *), 0); 
1091     if(cexFile == NULL)
1092      (void) fprintf(vis_stderr, "%s not Found\n",cexName);
1093
1094  }
1095  else
1096    goto usage;
1097 
1098
1099 
1100// Read_blif_mv
1101  hmgrCex =  Io_BlifMvRead(cexFile,hmgrCex,0,0,0);
1102  if(hmgrCex == NIL(Hrc_Manager_t)){
1103    fprintf(vis_stderr, "cannot open the hierrachy %\n",cexName);
1104    return 1;
1105  }
1106  st_table * modelTable = Hrc_ManagerReadModelTable(hmgrCex);
1107  if( st_count(modelTable) != 1){
1108    fprintf(vis_stderr, "cannot open more than one cex model\n");
1109    return 1;
1110  }
1111  st_generator *  gen;
1112  Hrc_ManagerForEachModel( hmgrCex,gen,cexModelName,cexModel){}
1113  fprintf(vis_stderr, "Compose %s with %s\n",rootName, cexModelName);
1114 
1115  cexNode = Hrc_ManagerReadRootNode(hmgrCex);
1116  actualInputArray = array_dup(Hrc_NodeReadFormalInputs(rootNode));
1117  actualOutputArray = array_dup(Hrc_NodeReadFormalOutputs(rootNode));
1118  Hrc_ModelAddSubckt(rootModel,cexModel,cexModelName,actualInputArray, actualOutputArray);
1119
1120
1121
1122 
1123 
1124
1125
1126/*
1127 modelName = Hrc_NodeReadModelName(rootNode);
1128 newRootName = ALLOC(char, strlen(cexName)+ strlen(modelName) + 2);
1129 sprintf(newRootName,"%s_%s",modelName,cexName);
1130 Hrc_Model_t * newRootModel = Hrc_ModelAlloc(*hmgr,rootName);
1131*/
1132
1133 fclose(cexFile);
1134 return 0;              /* normal exit */
1135
1136usage:
1137(void) fprintf(vis_stderr, "usage: _compose <cexFileName>\n");
1138return 1;               /* error exit */
1139
1140
1141/*
1142// Read_blif_mv
1143  FILE *fpC;
1144  fpC = Cmd_FileOpen("cex.mv", "r", NIL(char *), 1);
1145  boolean isCanonicalC = 0;
1146  boolean isIncrementalC = 0;
1147  boolean isVerboseC = 0;
1148  hmgrCex =  Io_BlifMvRead(fpC,hmgrCex,isCanonicalC,isIncrementalC,isVerboseC);
1149
1150//flatten_hier
1151  lsList         varNameList = (lsList) NULL;
1152  Hrc_Node_t    *currentNode = Hrc_ManagerReadCurrentNode(hmgrCex);
1153  networkCex = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, varNameList);
1154  Ntk_NetworkSetMddManager(networkCex, mddManager);
1155//static_order
1156  static Ord_NodeMethod nodeMethod = Ord_NodesByDefault_c;;
1157  static Ord_RootMethod rootMethod = Ord_RootsByDefault_c;
1158  static Ord_OrderType  suppliedOrderType = Ord_Unassigned_c;
1159  static Ord_OrderType  generatedOrderType = Ord_InputAndLatch_c;
1160  static boolean        nsAfterSupport = FALSE;
1161  lsList                suppliedNodeList = (lsList) NULL;
1162
1163 Ord_NetworkOrderVariables(networkCex, rootMethod, nodeMethod, nsAfterSupport,
1164                            generatedOrderType, suppliedOrderType,
1165                            suppliedNodeList, isVerboseC);
1166 //build_partition_mdd
1167 char * modelName = Hrc_NodeReadModelName(currentNode);
1168 static Part_PartitionMethod method = Part_Default_c;
1169 graph_t                     *partition;
1170 lsList                      nodeList = lsCreate();
1171 boolean inTermsOfLeaves = FALSE;
1172 partition = Part_NetworkCreatePartition(networkCex, currentNode, modelName, (lsList)0,
1173                                          (lsList)0, NIL(mdd_t), method, nodeList,
1174                                          inTermsOfLeaves, isVerboseC, 0);
1175//    PartPartitionPrint(vis_stdout, partition);
1176  printf(" Cex loaded \n");
1177fsmCex          =  Fsm_FsmCreateFromNetworkWithPartition(networkCex, partition);
1178array_t * nextNamesCex = Fsm_FsmReadNextStateFunctionNames(fsmCex);
1179array_t * nextIdsCex =   Fsm_FsmReadNextStateVars(fsmCex);
1180printf("Next Names\n");
1181printStringArray(nextNamesCex);
1182printf("Next Ids\n");
1183printIntArray(nextIdsCex);
1184
1185mddManager =  Fsm_FsmReadMddManager(fsm);
1186mdd_manager * mddManagerCex =  Fsm_FsmReadMddManager(fsmCex);
1187
1188array_t *mvar_list, *bvar_list;
1189mvar_list = mdd_ret_mvar_list(mddManager);
1190bvar_list = mdd_ret_bvar_list(mddManager);
1191printf("Number of mdd %d , %d\n", array_n(mvar_list),array_n(bvar_list));
1192printf("mddManager = %p mddMangerCex %p \n",mddManager,mddManagerCex);
1193 //mdd_t * init = Fsm_FsmComputeInitialStates(fsmCex);
1194// mdd_FunctionPrintMain (mddManagerCex ,init,"REL",vis_stdout);
1195graph_t * part = Fsm_FsmReadPartition(fsm);
1196printf(" modele %s , cex %s \n",Part_PartitionReadName(part), Part_PartitionReadName(partition));
1197*/
1198
1199   
1200}
Note: See TracBrowser for help on using the repository browser.