Changeset 98 for vis_dev/vis-2.3

Timestamp:

Jul 15, 2012, 2:15:06 PM (12 years ago)

Author:

cecile

Message:

add part of cex

Location:

vis_dev/vis-2.3/src

Files:

• debug/debug.c (modified) (4 diffs)
• debug/debugInt.h (modified) (1 diff)
• debug/debugUtilities.c (modified) (1 diff)
• rob/Robust.c (modified) (1 diff)
• rob/robCmd.c (modified) (2 diffs)

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

@@ -399 +399 @@
   CommandArguments [\[-h\] \[-v\] \[-k\]  [fileName] ]
   
-  CommandDescription [This command geerate a CNF of the network in DMACS form.
+  CommandDescription [This command generate a CNF of the network in DMACS form.
   The network may be unroll within k steps.
   <p>
@@ -947 +947 @@
 Ntk_Network_t  *network      = NIL(Ntk_Network_t);
 mdd_manager    *mddManager; 
-mdd_t          *rel          = NIL(mdd_t);
+Hrc_Manager_t  *hmgrCex       = NIL(Hrc_Manager_t);
+Fsm_Fsm_t      *fsmCex        = NIL(Fsm_Fsm_t);
+Ntk_Network_t  *networkCex    = NIL(Ntk_Network_t);
+mdd_t          *rel           = NIL(mdd_t);
 int            i;
 /******************/
@@ -958 +961 @@
 mddManager   = Fsm_FsmReadMddManager(fsm);
 
-
+mdd_t * initOrig  = Fsm_FsmComputeInitialStates(fsm);
+mdd_FunctionPrintMain (mddManager ,initOrig,"INIT_ORG",vis_stdout);
 
 /**********   Build cex  ***********/
@@ -968 +972 @@
 array_t * nextNames = Fsm_FsmReadNextStateFunctionNames(fsm);
 array_t * nextIds =   Fsm_FsmReadNextStateVars(fsm);
-
+array_t * currentIds = Fsm_FsmReadPresentStateVars(fsm);
+printf("Next Names\n");
+printStringArray(nextNames);
+printf("Next Ids\n");
+printIntArray(nextIds);
+printf("Current Ids\n");
+printIntArray(currentIds);
+Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
+ graph_t * part = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
+
+lsGen gen;
+vertex_t *vertexPtr;
+
+
+//foreach_vertex(part, gen, vertexPtr) {
+//      if (PartVertexReadName(vertexPtr) != NIL(char)) {
+//        (void) fprintf(vis_stdout, "%s\n", PartVertexReadName(vertexPtr));
+//      }
+//}
+vertex_t * v_s2 = Part_PartitionFindVertexByName(part, "cex.s2");
+Mvf_Function_t*  vertexFunction = PartVertexReadFunction(v_s2);
+  if (vertexFunction != NIL(Mvf_Function_t)) {
+printf("number mvf function %d\n",Mvf_FunctionReadNumComponents( vertexFunction));
+}
+else
+  printf("no fonction");
+
+Mvf_Function_t * newMvf  = Mvf_FunctionAlloc( mddManager,2);
+ mdd_t * s0 =  mdd_eq_c(mddManager,20, 0);
+ mdd_t * s1 =  mdd_eq_c(mddManager,22, 0);
+ mdd_t * state0 =  mdd_one(mddManager);
+ mdd_t * state1 =  mdd_one(mddManager);
+ state0 = mdd_and(s0,s1,1,1);
+ state1 = mdd_not(state0);
+  array_insert(mdd_t *, newMvf, 1, state0);
+  array_insert(mdd_t *, newMvf, 0, state1);
+Mvf_Function_t * newMvf2  = Mvf_FunctionAlloc( mddManager,2);
+ mdd_t * s0_2 =  mdd_eq_c(mddManager,20, 1);
+ mdd_t * s1_2 =  mdd_eq_c(mddManager,22, 0);
+ mdd_t * state0_2 =  mdd_one(mddManager);
+ mdd_t * state1_2 =  mdd_one(mddManager);
+ state0_2 = mdd_and(s0_2,s1_2,1,1);
+ state1_2 = mdd_not(state0_2);
+  array_insert(mdd_t *, newMvf2, 1, state0_2);
+  array_insert(mdd_t *, newMvf2, 0, state1_2);
+FILE * file = fopen("mvf.txt","w");
+foreach_vertex(part, gen, vertexPtr) {
+fprintf(file,"*********  (%s , %d) ***************\n", PartVertexReadName(vertexPtr),Part_VertexReadMddId(vertexPtr) );
+ Mvf_Function_t * fun = PartVertexReadFunction(vertexPtr);
+ mdd_t * oldMvf0 = Mvf_FunctionReadComponent(fun,0);
+ mdd_FunctionPrintMain (mddManager ,oldMvf0,"OLD_0",file);
+ mdd_t * oldMvf1 = Mvf_FunctionReadComponent(fun,1);
+ mdd_FunctionPrintMain (mddManager ,oldMvf1,"OLD_1",file);
+
+ if(Part_VertexReadMddId(vertexPtr) == 17)
+ {
+ Mvf_Function_t * newMvf  = Mvf_FunctionAlloc( mddManager,2);
+
+   mdd_t * new0 = Mvf_FunctionReadComponent(fun,0);
+   new0 = mdd_and(new0,state1,1,1);
+   mdd_t * new1 = Mvf_FunctionReadComponent(fun,1);
+   new1 = mdd_and(new1,state0,1,1);
+    array_insert(mdd_t *, newMvf, 1, new1);
+    array_insert(mdd_t *, newMvf, 0, new0);
+    mdd_FunctionPrintMain (mddManager ,new0,"NEW_0",file);
+     mdd_FunctionPrintMain (mddManager ,new1,"NEW_1",file);
+    Part_VertexSetFunction(vertexPtr, newMvf);
+ }
+ else{
+  Mvf_Function_t * newFun = Mvf_FunctionComposeWithFunction(fun,17,newMvf);
+  Mvf_Function_t * newFun1 = Mvf_FunctionComposeWithFunction(fun,2,newMvf);
+  //Mvf_Function_t * newFun2 = Mvf_FunctionComposeWithFunction(fun,14,newMvf2);
+ mdd_t * new0 = Mvf_FunctionReadComponent(newFun,0);
+ mdd_FunctionPrintMain (mddManager ,new0,"NEW_0",file);
+ mdd_t * new1 = Mvf_FunctionReadComponent(newFun,1);
+ mdd_FunctionPrintMain (mddManager ,new1,"NEW_1",file);
+
+ Part_VertexSetFunction(vertexPtr, newFun);
+ Part_VertexSetFunction(vertexPtr, newFun1);
+// Part_VertexSetFunction(vertexPtr, newFun2);
+ }
+}
+fclose(file);
+
+
+
+
+  array_t       * psVars = fsm->fsmData.presentStateVars;
+   int  numLatches = array_n(psVars);
+
+
+   for (i=0; i<numLatches; i++){
+    int latchMddId = array_fetch(int, psVars, i);
+    Ntk_Node_t *latch = Ntk_NetworkFindNodeByMddId(network, latchMddId);
+    Ntk_Node_t *initNode   = Ntk_LatchReadInitialInput(latch);
+    vertex_t   *initVertex = Part_PartitionFindVertexByName(part,
+                                Ntk_NodeReadName(initNode));
+    Mvf_Function_t * fun = PartVertexReadFunction(initVertex);
+   printf("%d-- %d - %s %s %s(%d)\n",i, latchMddId,Ntk_NodeReadName(latch),Ntk_NodeReadName(initNode),
+   Part_VertexReadName(initVertex),Mvf_FunctionReadNumComponents( fun) );
+   
+ mdd_t * oldMvf0 = Mvf_FunctionReadComponent(fun,0);
+ mdd_FunctionPrintMain (mddManager ,oldMvf0,"OLD_0",vis_stdout);
+ mdd_t * oldMvf1 = Mvf_FunctionReadComponent(fun,1);
+ mdd_FunctionPrintMain (mddManager ,oldMvf1,"OLD_1",vis_stdout);
+
+
+    }
+
+
+ /** Change the fsm and the network with a new partition and the new fsm **/
+Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
+                                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
+                                          (void *) part);
+fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t*));
+mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
+//mdd_t * n_init =  Mvf_MddComposeWithFunction(init, 17 , newMvf);
+mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose,
+                                      0,0, 0,
+                                      0, 0, Fsm_Rch_Default_c,
+                                      0,1, NIL(array_t),
+                                      (verbose > 0),  NIL(array_t));
+//mdd_t * n_reach =  Mvf_MddComposeWithFunction(reach, 17 , newMvf);
+//fsm->reachabilityInfo.initialStates = n_init;
+//fsm->reachabilityInfo.reachableStates = n_reach;
+//      
+//    
+    
+Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY,
+                         (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
+                         (void *) fsm); 
+
+Fsm_FsmReachabilityPrintResults(fsm,3, 0);
+//
+//
+mdd_FunctionPrintMain (mddManager ,init,"INIT",vis_stdout);
+
+/*
+// Read_blif_mv
+  FILE *fpC;
+  fpC = Cmd_FileOpen("cex.mv", "r", NIL(char *), 1);
+  boolean isCanonicalC = 0;
+  boolean isIncrementalC = 0; 
+  boolean isVerboseC = 0;
+  hmgrCex =  Io_BlifMvRead(fpC,hmgrCex,isCanonicalC,isIncrementalC,isVerboseC);
+
+//flatten_hier
+  lsList         varNameList = (lsList) NULL;
+  Hrc_Node_t    *currentNode = Hrc_ManagerReadCurrentNode(hmgrCex);
+  networkCex = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, varNameList);
+  Ntk_NetworkSetMddManager(networkCex, mddManager);
+//static_order
+  static Ord_NodeMethod nodeMethod = Ord_NodesByDefault_c;;
+  static Ord_RootMethod rootMethod = Ord_RootsByDefault_c;
+  static Ord_OrderType  suppliedOrderType = Ord_Unassigned_c;
+  static Ord_OrderType  generatedOrderType = Ord_InputAndLatch_c;
+  static boolean        nsAfterSupport = FALSE;
+  lsList                suppliedNodeList = (lsList) NULL;
+
+ Ord_NetworkOrderVariables(networkCex, rootMethod, nodeMethod, nsAfterSupport, 
+                            generatedOrderType, suppliedOrderType,
+                            suppliedNodeList, isVerboseC);
+ //build_partition_mdd
+ char * modelName = Hrc_NodeReadModelName(currentNode);
+ static Part_PartitionMethod method = Part_Default_c;
+ graph_t                     *partition;
+ lsList                      nodeList = lsCreate();
+ boolean inTermsOfLeaves = FALSE;
+ partition = Part_NetworkCreatePartition(networkCex, currentNode, modelName, (lsList)0,
+                                          (lsList)0, NIL(mdd_t), method, nodeList,
+                                          inTermsOfLeaves, isVerboseC, 0);
+//    PartPartitionPrint(vis_stdout, partition);
+  printf(" Cex loaded \n");
+fsmCex          =  Fsm_FsmCreateFromNetworkWithPartition(networkCex, partition);
+array_t * nextNamesCex = Fsm_FsmReadNextStateFunctionNames(fsmCex);
+array_t * nextIdsCex =   Fsm_FsmReadNextStateVars(fsmCex);
+printf("Next Names\n");
+printStringArray(nextNamesCex);
+printf("Next Ids\n");
+printIntArray(nextIdsCex);
+
+mddManager =  Fsm_FsmReadMddManager(fsm);
+mdd_manager * mddManagerCex =  Fsm_FsmReadMddManager(fsmCex);
+
+array_t *mvar_list, *bvar_list;
+mvar_list = mdd_ret_mvar_list(mddManager);
+bvar_list = mdd_ret_bvar_list(mddManager);
+printf("Number of mdd %d , %d\n", array_n(mvar_list),array_n(bvar_list));
+printf("mddManager = %p mddMangerCex %p \n",mddManager,mddManagerCex);
+ //mdd_t * init = Fsm_FsmComputeInitialStates(fsmCex);
+// mdd_FunctionPrintMain (mddManagerCex ,init,"REL",vis_stdout);
+graph_t * part = Fsm_FsmReadPartition(fsm);
+printf(" modele %s , cex %s \n",Part_PartitionReadName(part), Part_PartitionReadName(partition));
+*/
 /** 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);
+// 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 */

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

@@ -83 +83 @@
 
 void printLatch(st_table* CoiTable);
+void printStringArray(array_t * array);
+void printIntArray(array_t * array);
 st_table * generateAllLatches(Ntk_Network_t * ntk);
 void mdd_GetState_Values(mdd_manager *mgr, mdd_t * top, FILE * f);

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

@@ -22 +22 @@
 }
 
-
+void printStringArray(array_t * array)
+{
+  
+  int i;
+  char * data;
+  arrayForEachItem(char *, array, i, data)
+  {
+    printf("%s\n",data);
+  }
+} 
+void printIntArray(array_t * array)
+{
+  
+  int i;
+  int data;
+  arrayForEachItem(int, array, i, data)
+  {
+    printf("%d\n",data);
+  }
+} 
 st_table * generateAllLatches(Ntk_Network_t * ntk)
 {

vis_dev/vis-2.3/src/rob/Robust.c

@@ -1696 +1696 @@
  *  Synopsis    [Generate name of protected register]
 
-  Description [Generate file containing names of latches int he golden model that have to be
-  protected. ]
+  Description [Generate file containing names of latches in the golden model 
+  that have to be protected. ]
 
   SideEffects []

vis_dev/vis-2.3/src/rob/robCmd.c

@@ -1484 +1484 @@
 Hrc_Node_t * rootNode = Hrc_ManagerReadRootNode(*hmgr);
 if(rootNode == NIL(Hrc_Node_t)){
-        printf("Please build the network first");
+        printf("Please build the network first\n");
         return 1;
 }
@@ -1491 +1491 @@
 Hrc_Node_t * goldenNode = Hrc_NodeFindChildByName(rootNode, name);
 if(goldenNode == NIL(Hrc_Node_t)){
-        printf("Please build the network first");
+        printf("Compose the network with a golden name golden first\n");
         return 1;
 }