Changeset 45

Timestamp:

Feb 20, 2012, 6:45:17 PM (12 years ago)

Author:

cecile

Message:

fichier biblio avec lien sur le compte verif

Files:

• biblio (added)
• biblio/biblio.bib (added)
• biblio/verif_biblio.html (added)
• vis_dev/vis-2.3/models/debug/and2.v (modified) (1 diff)
• vis_dev/vis-2.3/src/debug/debug.c (modified) (8 diffs)
• vis_dev/vis-2.3/src/debug/debug.make (modified) (1 diff)
• vis_dev/vis-2.3/src/debug/debugAbnormal.c (modified) (2 diffs)
• vis_dev/vis-2.3/src/debug/debugInt.h (modified) (1 diff)

vis_dev/vis-2.3/models/debug/and2.v

@@ -1 +1 @@
 module andgate(clk,a,b);
 input clk;
-input a;
-input b;
+input [1:0]a;
+input [1:0]b;
 
-reg c;
-reg d;
+reg [1:0]c;
+reg [1:0]d;
 
 initial c = 0;

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

@@ -66 +66 @@
 static int CommandCreateAbnormal(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
 static int CommandGenerateNetworkCNF(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
+static int CommandBuildCexBdd(Hrc_Manager_t ** hmgr,int  argc, char ** argv);
 
 
@@ -95 +96 @@
   Cmd_CommandAdd("_sat_debug",   CommandSatDebug, 0);
   Cmd_CommandAdd("_createAbn",   CommandCreateAbnormal, 1);
+  Cmd_CommandAdd("_cexbdd",      CommandBuildCexBdd, 0);
   Cmd_CommandAdd("print_network_cnf",  CommandGenerateNetworkCNF, 0);
 
@@ -700 +702 @@
  return rel;
 }
-
+mdd_t * buildDummy2(mdd_manager * mddManager)
+{
+ mdd_t * rel = NIL(mdd_t);
+ mdd_t * state0 = mdd_one(mddManager);
+ mdd_t * state2 = mdd_one(mddManager);
+ mdd_t * state3 = mdd_one(mddManager);
+  // state0 = s0 
+ mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
+ mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
+ state0 = mdd_and(s0,s1,1,1);
+  // state2 = s2
+ s0 =  mdd_eq_c(mddManager,0, 0);
+ s1 =  mdd_eq_c(mddManager,2, 1);
+ state2 = mdd_and(s0,s1,1,1);
+  // state3 = s3
+ s0 =  mdd_eq_c(mddManager,0, 1);
+ s1 =  mdd_eq_c(mddManager,2, 1);
+ state3 = mdd_and(s0,s1,1,1);
+// Build transition relation
+
+ array_t * mvarVal = array_alloc(int,0);
+ array_insert_last(int, mvarVal,2);
+ array_t * val = array_alloc(int,0);
+ array_t * mvarName = array_alloc(char*,0);
+ array_insert_last(char*, mvarName,"S1");
+ int e1Id = mdd_create_variables(mddManager,mvarVal,mvarName,NIL(array_t));
+ array_insert(char*, mvarName,0,"I");
+ int e0Id = mdd_create_variables(mddManager,mvarVal,mvarName,NIL(array_t));
+ array_insert_last(int, val,1);
+ mdd_t * e1 = mdd_literal(mddManager, e1Id,val);
+ mdd_t * e0 = mdd_literal(mddManager, e0Id,val);
+ mdd_t * tmp2 = mdd_and(e1,e0,0,0);
+mdd_t *  ne2_1 = mdd_or(e1,tmp2,1,1);
+mdd_t *  ne2_0 = mdd_and(e1,e0,0,1);
+
+array_insert(char*, mvarName,0,"Next_SI");
+int id = mdd_create_variables(mddManager,mvarVal,mvarName,NIL(array_t));
+Mvf_Function_t * mvf = Mvf_FunctionAlloc(mddManager, 2);
+Mvf_FunctionAddMintermsToComponent(mvf,1,ne2_1);
+Mvf_FunctionAddMintermsToComponent(mvf,0,ne2_0);
+mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, id);
+
+//bdd_print(relation);
+mdd_FunctionPrintMain (mddManager ,relation,"news",vis_stdout);
+ //bdd_ite
+ return rel;
+
+}
 
 /**Function********************************************************************
@@ -713 +762 @@
   
   CommandDescription [This command create a new transition relation that is a
-  and of the Bdd of the old one and an other bdd.
+  and of the Bdd of the old one and another bdd.
   <p>
 
@@ -780 +829 @@
 /* with the transtion relation     */
 /***********************************/
-rel = buildDummyBdd(mddManager);
+rel = buildDummy3(mddManager,network);
 if(rel == NIL(mdd_t))
 {
-        fprintf(vis_stdout,"Problem when building the new relation bdd");
+        fprintf(vis_stdout,"Problem when building the new relation bdd\n");
         return 1;
 }
@@ -809 +858 @@
     int mddId = array_fetch(int, rangeVarMddIdArray, i);
         mdd_t *relation = Mvf_FunctionBuildRelationWithVariable(mvf, mddId);
+    mdd_FunctionPrintMain (mddManager ,relation,"MVF",vis_stdout);
+
         mdd_t * n_relation = mdd_and(relation,rel,1,1);
     /* Build for each possible value */
@@ -820 +871 @@
                  mdd_t * n_relation_s1 = mdd_cofactor_minterm(n_rel_s1,n_s1);
                  Mvf_FunctionAddMintermsToComponent(newMvf,v,n_relation_s1);
+
 
         }
@@ -857 +909 @@
 }
 
-
+static int 
+CommandBuildCexBdd(Hrc_Manager_t ** hmgr,
+                   int  argc, char ** argv){
+int            c;
+int            verbose = 0;              /* default value */
+
+/*
+ * Parse command line options.
+ */
+util_getopt_reset();
+while ((c = util_getopt(argc, argv, "vh")) != EOF) {
+  switch(c) {
+    case 'v':
+      verbose = 1;
+      break;
+    case 'h':
+      goto usage;
+    default:
+      goto usage;
+  }
+}
+
+if (verbose) {
+  (void) fprintf(vis_stdout, "The _cexBdd is under construction.\n");
+}
+
+Fsm_Fsm_t      *fsm          = NIL(Fsm_Fsm_t);
+Ntk_Network_t  *network      = NIL(Ntk_Network_t);
+mdd_manager    *mddManager; 
+mdd_t          *rel          = NIL(mdd_t);
+int            i;
+/******************/
+network      = Ntk_HrcManagerReadCurrentNetwork(*hmgr);
+if(network == NIL(Ntk_Network_t))
+        return 1;
+fsm          = Fsm_HrcManagerReadCurrentFsm(*hmgr);
+if(fsm ==  NIL(Fsm_Fsm_t))
+        return 1;
+mddManager   = Fsm_FsmReadMddManager(fsm);
+
+
+
+/**********   Build cex  ***********/
+/* Here add the function           */
+/* that build the Bdd to and       */
+/* with the transtion relation     */
+/***********************************/
+//rel = buildDummyBdd(mddManager);
+array_t * nextNames = Fsm_FsmReadNextStateFunctionNames(fsm);
+array_t * nextIds =   Fsm_FsmReadNextStateVars(fsm);
+
+/** state0 = s0 **/
+ mdd_t * s0 =  mdd_eq_c(mddManager,0, 0);
+ mdd_t * s1 =  mdd_eq_c(mddManager,2, 0);
+ mdd_t * state0 =  mdd_one(mddManager);
+ state0 = mdd_and(s0,s1,1,1);
+/** Next state1 = s2 + !s2  **/
+
+ mdd_t * ns0 =  mdd_eq_c(mddManager,1, 1);
+ mdd_t * ns1 =  mdd_eq_c(mddManager,3, 0);
+ mdd_t * state1 =  mdd_one(mddManager);
+ state1 = mdd_and(ns0,ns1,1,1);
+ state1 = mdd_or(state1,state1,1,0);
+
+/** state = s0) -> !(Nextstate = s2) + (Nextstae = s2) **/
+ rel =  mdd_one(mddManager);
+ rel =  mdd_or(state0,state1,0,0);
+/**********/
+/** state0 = s2 **/
+ mdd_t * s02 =  mdd_eq_c(mddManager,0, 0);
+ mdd_t * s12 =  mdd_eq_c(mddManager,2, 1);
+ mdd_t * state02 =  mdd_one(mddManager);
+ state02 = mdd_and(s02,s12,1,1);
+/** Next state1 = s3  **/
+
+ mdd_t * ns02 =  mdd_eq_c(mddManager,1, 1);
+ mdd_t * ns12 =  mdd_eq_c(mddManager,3, 1);
+ mdd_t * state12 =  mdd_one(mddManager);
+ state12 = mdd_and(ns02,ns12,1,1);
+
+/** state = s0) -> !(Nextstate = s3) **/
+ mdd_t * new_rel =  mdd_one(mddManager);
+ new_rel =  mdd_or(state02,state12,0,0);
+ rel = mdd_and(new_rel,rel,1,1);
+ mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout);
+
+return 0;               /* normal exit */
+
+usage:
+(void) fprintf(vis_stderr, "usage: _BddCex [-h] [-v]\n");
+(void) fprintf(vis_stderr, "   -h\t\tprint the command usage\n");
+(void) fprintf(vis_stderr, "   -v\t\tverbose\n");
+return 1;               /* error exit */
+
+}
+
+

vis_dev/vis-2.3/src/debug/debug.make

@@ -1 @@
-CSRC += debug.c debugUtilities.c debugAbnormal.c
+CSRC += debug.c debugUtilities.c debugAbnormal.c debugNewBdd.c
 HEADERS += debug.h debugInt.h
 

vis_dev/vis-2.3/src/debug/debugAbnormal.c

@@ -5 +5 @@
 
   Description [Create new primary input in the current network at a given
-  output node.  Return the variable created]
+  output node.  Return the node created]
 
   SideEffects [Modify the network]
@@ -12 +12 @@
 
 ******************************************************************************/
-Ntk_Node_t * Dbg_CreateNewNode(Ntk_Network_t * ntk,Ntk_Node_t*
+Ntk_Node_t * Dbg_CreateNewNode(Ntk_Network_t * ntk, Ntk_Node_t*
 node, char * varName  )
 {

vis_dev/vis-2.3/src/debug/debugInt.h

@@ -87 +87 @@
 void printNodeArray(array_t * nodeArray);
 boolean Dbg_TestNodeInSubs(char* nodeName,array_t * subsName);
+mdd_t * buildDummy3(mdd_manager * mddManager,Ntk_Network_t * ntk);
 
 /**AutomaticEnd***************************************************************/