Changeset 98
- Timestamp:
- Jul 15, 2012, 2:15:06 PM (12 years ago)
- Location:
- vis_dev/vis-2.3/src
- Files:
-
- 5 edited
Legend:
- Unmodified
- Added
- Removed
-
vis_dev/vis-2.3/src/debug/debug.c
r96 r98 399 399 CommandArguments [\[-h\] \[-v\] \[-k\] [fileName] ] 400 400 401 CommandDescription [This command ge erate a CNF of the network in DMACS form.401 CommandDescription [This command generate a CNF of the network in DMACS form. 402 402 The network may be unroll within k steps. 403 403 <p> … … 947 947 Ntk_Network_t *network = NIL(Ntk_Network_t); 948 948 mdd_manager *mddManager; 949 mdd_t *rel = NIL(mdd_t); 949 Hrc_Manager_t *hmgrCex = NIL(Hrc_Manager_t); 950 Fsm_Fsm_t *fsmCex = NIL(Fsm_Fsm_t); 951 Ntk_Network_t *networkCex = NIL(Ntk_Network_t); 952 mdd_t *rel = NIL(mdd_t); 950 953 int i; 951 954 /******************/ … … 958 961 mddManager = Fsm_FsmReadMddManager(fsm); 959 962 960 963 mdd_t * initOrig = Fsm_FsmComputeInitialStates(fsm); 964 mdd_FunctionPrintMain (mddManager ,initOrig,"INIT_ORG",vis_stdout); 961 965 962 966 /********** Build cex ***********/ … … 968 972 array_t * nextNames = Fsm_FsmReadNextStateFunctionNames(fsm); 969 973 array_t * nextIds = Fsm_FsmReadNextStateVars(fsm); 970 974 array_t * currentIds = Fsm_FsmReadPresentStateVars(fsm); 975 printf("Next Names\n"); 976 printStringArray(nextNames); 977 printf("Next Ids\n"); 978 printIntArray(nextIds); 979 printf("Current Ids\n"); 980 printIntArray(currentIds); 981 Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0); 982 graph_t * part = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm)); 983 984 lsGen gen; 985 vertex_t *vertexPtr; 986 987 988 //foreach_vertex(part, gen, vertexPtr) { 989 // if (PartVertexReadName(vertexPtr) != NIL(char)) { 990 // (void) fprintf(vis_stdout, "%s\n", PartVertexReadName(vertexPtr)); 991 // } 992 //} 993 vertex_t * v_s2 = Part_PartitionFindVertexByName(part, "cex.s2"); 994 Mvf_Function_t* vertexFunction = PartVertexReadFunction(v_s2); 995 if (vertexFunction != NIL(Mvf_Function_t)) { 996 printf("number mvf function %d\n",Mvf_FunctionReadNumComponents( vertexFunction)); 997 } 998 else 999 printf("no fonction"); 1000 1001 Mvf_Function_t * newMvf = Mvf_FunctionAlloc( mddManager,2); 1002 mdd_t * s0 = mdd_eq_c(mddManager,20, 0); 1003 mdd_t * s1 = mdd_eq_c(mddManager,22, 0); 1004 mdd_t * state0 = mdd_one(mddManager); 1005 mdd_t * state1 = mdd_one(mddManager); 1006 state0 = mdd_and(s0,s1,1,1); 1007 state1 = mdd_not(state0); 1008 array_insert(mdd_t *, newMvf, 1, state0); 1009 array_insert(mdd_t *, newMvf, 0, state1); 1010 Mvf_Function_t * newMvf2 = Mvf_FunctionAlloc( mddManager,2); 1011 mdd_t * s0_2 = mdd_eq_c(mddManager,20, 1); 1012 mdd_t * s1_2 = mdd_eq_c(mddManager,22, 0); 1013 mdd_t * state0_2 = mdd_one(mddManager); 1014 mdd_t * state1_2 = mdd_one(mddManager); 1015 state0_2 = mdd_and(s0_2,s1_2,1,1); 1016 state1_2 = mdd_not(state0_2); 1017 array_insert(mdd_t *, newMvf2, 1, state0_2); 1018 array_insert(mdd_t *, newMvf2, 0, state1_2); 1019 FILE * file = fopen("mvf.txt","w"); 1020 foreach_vertex(part, gen, vertexPtr) { 1021 fprintf(file,"********* (%s , %d) ***************\n", PartVertexReadName(vertexPtr),Part_VertexReadMddId(vertexPtr) ); 1022 Mvf_Function_t * fun = PartVertexReadFunction(vertexPtr); 1023 mdd_t * oldMvf0 = Mvf_FunctionReadComponent(fun,0); 1024 mdd_FunctionPrintMain (mddManager ,oldMvf0,"OLD_0",file); 1025 mdd_t * oldMvf1 = Mvf_FunctionReadComponent(fun,1); 1026 mdd_FunctionPrintMain (mddManager ,oldMvf1,"OLD_1",file); 1027 1028 if(Part_VertexReadMddId(vertexPtr) == 17) 1029 { 1030 Mvf_Function_t * newMvf = Mvf_FunctionAlloc( mddManager,2); 1031 1032 mdd_t * new0 = Mvf_FunctionReadComponent(fun,0); 1033 new0 = mdd_and(new0,state1,1,1); 1034 mdd_t * new1 = Mvf_FunctionReadComponent(fun,1); 1035 new1 = mdd_and(new1,state0,1,1); 1036 array_insert(mdd_t *, newMvf, 1, new1); 1037 array_insert(mdd_t *, newMvf, 0, new0); 1038 mdd_FunctionPrintMain (mddManager ,new0,"NEW_0",file); 1039 mdd_FunctionPrintMain (mddManager ,new1,"NEW_1",file); 1040 Part_VertexSetFunction(vertexPtr, newMvf); 1041 } 1042 else{ 1043 Mvf_Function_t * newFun = Mvf_FunctionComposeWithFunction(fun,17,newMvf); 1044 Mvf_Function_t * newFun1 = Mvf_FunctionComposeWithFunction(fun,2,newMvf); 1045 //Mvf_Function_t * newFun2 = Mvf_FunctionComposeWithFunction(fun,14,newMvf2); 1046 mdd_t * new0 = Mvf_FunctionReadComponent(newFun,0); 1047 mdd_FunctionPrintMain (mddManager ,new0,"NEW_0",file); 1048 mdd_t * new1 = Mvf_FunctionReadComponent(newFun,1); 1049 mdd_FunctionPrintMain (mddManager ,new1,"NEW_1",file); 1050 1051 Part_VertexSetFunction(vertexPtr, newFun); 1052 Part_VertexSetFunction(vertexPtr, newFun1); 1053 // Part_VertexSetFunction(vertexPtr, newFun2); 1054 } 1055 } 1056 fclose(file); 1057 1058 1059 1060 1061 array_t * psVars = fsm->fsmData.presentStateVars; 1062 int numLatches = array_n(psVars); 1063 1064 1065 for (i=0; i<numLatches; i++){ 1066 int latchMddId = array_fetch(int, psVars, i); 1067 Ntk_Node_t *latch = Ntk_NetworkFindNodeByMddId(network, latchMddId); 1068 Ntk_Node_t *initNode = Ntk_LatchReadInitialInput(latch); 1069 vertex_t *initVertex = Part_PartitionFindVertexByName(part, 1070 Ntk_NodeReadName(initNode)); 1071 Mvf_Function_t * fun = PartVertexReadFunction(initVertex); 1072 printf("%d-- %d - %s %s %s(%d)\n",i, latchMddId,Ntk_NodeReadName(latch),Ntk_NodeReadName(initNode), 1073 Part_VertexReadName(initVertex),Mvf_FunctionReadNumComponents( fun) ); 1074 1075 mdd_t * oldMvf0 = Mvf_FunctionReadComponent(fun,0); 1076 mdd_FunctionPrintMain (mddManager ,oldMvf0,"OLD_0",vis_stdout); 1077 mdd_t * oldMvf1 = Mvf_FunctionReadComponent(fun,1); 1078 mdd_FunctionPrintMain (mddManager ,oldMvf1,"OLD_1",vis_stdout); 1079 1080 1081 } 1082 1083 1084 /** Change the fsm and the network with a new partition and the new fsm **/ 1085 Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY, 1086 (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback, 1087 (void *) part); 1088 fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t*)); 1089 mdd_t * init = Fsm_FsmComputeInitialStates(fsm); 1090 //mdd_t * n_init = Mvf_MddComposeWithFunction(init, 17 , newMvf); 1091 mdd_t * reach = Fsm_FsmComputeReachableStates(fsm,0,verbose, 1092 0,0, 0, 1093 0, 0, Fsm_Rch_Default_c, 1094 0,1, NIL(array_t), 1095 (verbose > 0), NIL(array_t)); 1096 //mdd_t * n_reach = Mvf_MddComposeWithFunction(reach, 17 , newMvf); 1097 //fsm->reachabilityInfo.initialStates = n_init; 1098 //fsm->reachabilityInfo.reachableStates = n_reach; 1099 // 1100 // 1101 1102 Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY, 1103 (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback, 1104 (void *) fsm); 1105 1106 Fsm_FsmReachabilityPrintResults(fsm,3, 0); 1107 // 1108 // 1109 mdd_FunctionPrintMain (mddManager ,init,"INIT",vis_stdout); 1110 1111 /* 1112 // Read_blif_mv 1113 FILE *fpC; 1114 fpC = Cmd_FileOpen("cex.mv", "r", NIL(char *), 1); 1115 boolean isCanonicalC = 0; 1116 boolean isIncrementalC = 0; 1117 boolean isVerboseC = 0; 1118 hmgrCex = Io_BlifMvRead(fpC,hmgrCex,isCanonicalC,isIncrementalC,isVerboseC); 1119 1120 //flatten_hier 1121 lsList varNameList = (lsList) NULL; 1122 Hrc_Node_t *currentNode = Hrc_ManagerReadCurrentNode(hmgrCex); 1123 networkCex = Ntk_HrcNodeConvertToNetwork(currentNode, TRUE, varNameList); 1124 Ntk_NetworkSetMddManager(networkCex, mddManager); 1125 //static_order 1126 static Ord_NodeMethod nodeMethod = Ord_NodesByDefault_c;; 1127 static Ord_RootMethod rootMethod = Ord_RootsByDefault_c; 1128 static Ord_OrderType suppliedOrderType = Ord_Unassigned_c; 1129 static Ord_OrderType generatedOrderType = Ord_InputAndLatch_c; 1130 static boolean nsAfterSupport = FALSE; 1131 lsList suppliedNodeList = (lsList) NULL; 1132 1133 Ord_NetworkOrderVariables(networkCex, rootMethod, nodeMethod, nsAfterSupport, 1134 generatedOrderType, suppliedOrderType, 1135 suppliedNodeList, isVerboseC); 1136 //build_partition_mdd 1137 char * modelName = Hrc_NodeReadModelName(currentNode); 1138 static Part_PartitionMethod method = Part_Default_c; 1139 graph_t *partition; 1140 lsList nodeList = lsCreate(); 1141 boolean inTermsOfLeaves = FALSE; 1142 partition = Part_NetworkCreatePartition(networkCex, currentNode, modelName, (lsList)0, 1143 (lsList)0, NIL(mdd_t), method, nodeList, 1144 inTermsOfLeaves, isVerboseC, 0); 1145 // PartPartitionPrint(vis_stdout, partition); 1146 printf(" Cex loaded \n"); 1147 fsmCex = Fsm_FsmCreateFromNetworkWithPartition(networkCex, partition); 1148 array_t * nextNamesCex = Fsm_FsmReadNextStateFunctionNames(fsmCex); 1149 array_t * nextIdsCex = Fsm_FsmReadNextStateVars(fsmCex); 1150 printf("Next Names\n"); 1151 printStringArray(nextNamesCex); 1152 printf("Next Ids\n"); 1153 printIntArray(nextIdsCex); 1154 1155 mddManager = Fsm_FsmReadMddManager(fsm); 1156 mdd_manager * mddManagerCex = Fsm_FsmReadMddManager(fsmCex); 1157 1158 array_t *mvar_list, *bvar_list; 1159 mvar_list = mdd_ret_mvar_list(mddManager); 1160 bvar_list = mdd_ret_bvar_list(mddManager); 1161 printf("Number of mdd %d , %d\n", array_n(mvar_list),array_n(bvar_list)); 1162 printf("mddManager = %p mddMangerCex %p \n",mddManager,mddManagerCex); 1163 //mdd_t * init = Fsm_FsmComputeInitialStates(fsmCex); 1164 // mdd_FunctionPrintMain (mddManagerCex ,init,"REL",vis_stdout); 1165 graph_t * part = Fsm_FsmReadPartition(fsm); 1166 printf(" modele %s , cex %s \n",Part_PartitionReadName(part), Part_PartitionReadName(partition)); 1167 */ 971 1168 /** state0 = s0 **/ 972 mdd_t * s0 = mdd_eq_c(mddManager,0, 0);973 mdd_t * s1 = mdd_eq_c(mddManager,2, 0);974 mdd_t * state0 = mdd_one(mddManager);975 state0 = mdd_and(s0,s1,1,1);976 / ** Next state1 = s2 + !s2 **/977 978 mdd_t * ns0 = mdd_eq_c(mddManager,1, 1);979 mdd_t * ns1 = mdd_eq_c(mddManager,3, 0);980 mdd_t * state1 = mdd_one(mddManager);981 state1 = mdd_and(ns0,ns1,1,1);982 state1 = mdd_or(state1,state1,1,0);983 984 / ** state = s0) -> !(Nextstate = s2) + (Nextstae = s2) **/985 rel = mdd_one(mddManager);986 rel = mdd_or(state0,state1,0,0);987 / **********/988 / ** state0 = s2 **/989 mdd_t * s02 = mdd_eq_c(mddManager,0, 0);990 mdd_t * s12 = mdd_eq_c(mddManager,2, 1);991 mdd_t * state02 = mdd_one(mddManager);992 state02 = mdd_and(s02,s12,1,1);993 / ** Next state1 = s3 **/994 995 mdd_t * ns02 = mdd_eq_c(mddManager,1, 1);996 mdd_t * ns12 = mdd_eq_c(mddManager,3, 1);997 mdd_t * state12 = mdd_one(mddManager);998 state12 = mdd_and(ns02,ns12,1,1);999 1000 / ** state = s0) -> !(Nextstate = s3) **/1001 mdd_t * new_rel = mdd_one(mddManager);1002 new_rel = mdd_or(state02,state12,0,0);1003 rel = mdd_and(new_rel,rel,1,1);1004 mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout);1169 // mdd_t * s0 = mdd_eq_c(mddManager,0, 0); 1170 // mdd_t * s1 = mdd_eq_c(mddManager,2, 0); 1171 // mdd_t * state0 = mdd_one(mddManager); 1172 // state0 = mdd_and(s0,s1,1,1); 1173 ///** Next state1 = s2 + !s2 **/ 1174 // 1175 // mdd_t * ns0 = mdd_eq_c(mddManager,1, 1); 1176 // mdd_t * ns1 = mdd_eq_c(mddManager,3, 0); 1177 // mdd_t * state1 = mdd_one(mddManager); 1178 // state1 = mdd_and(ns0,ns1,1,1); 1179 // state1 = mdd_or(state1,state1,1,0); 1180 // 1181 ///** state = s0) -> !(Nextstate = s2) + (Nextstae = s2) **/ 1182 // rel = mdd_one(mddManager); 1183 // rel = mdd_or(state0,state1,0,0); 1184 ///**********/ 1185 ///** state0 = s2 **/ 1186 // mdd_t * s02 = mdd_eq_c(mddManager,0, 0); 1187 // mdd_t * s12 = mdd_eq_c(mddManager,2, 1); 1188 // mdd_t * state02 = mdd_one(mddManager); 1189 // state02 = mdd_and(s02,s12,1,1); 1190 ///** Next state1 = s3 **/ 1191 // 1192 // mdd_t * ns02 = mdd_eq_c(mddManager,1, 1); 1193 // mdd_t * ns12 = mdd_eq_c(mddManager,3, 1); 1194 // mdd_t * state12 = mdd_one(mddManager); 1195 // state12 = mdd_and(ns02,ns12,1,1); 1196 // 1197 ///** state = s0) -> !(Nextstate = s3) **/ 1198 // mdd_t * new_rel = mdd_one(mddManager); 1199 // new_rel = mdd_or(state02,state12,0,0); 1200 // rel = mdd_and(new_rel,rel,1,1); 1201 // mdd_FunctionPrintMain (mddManager ,rel,"REL",vis_stdout); 1005 1202 1006 1203 return 0; /* normal exit */ -
vis_dev/vis-2.3/src/debug/debugInt.h
r45 r98 83 83 84 84 void printLatch(st_table* CoiTable); 85 void printStringArray(array_t * array); 86 void printIntArray(array_t * array); 85 87 st_table * generateAllLatches(Ntk_Network_t * ntk); 86 88 void mdd_GetState_Values(mdd_manager *mgr, mdd_t * top, FILE * f); -
vis_dev/vis-2.3/src/debug/debugUtilities.c
r44 r98 22 22 } 23 23 24 24 void printStringArray(array_t * array) 25 { 26 27 int i; 28 char * data; 29 arrayForEachItem(char *, array, i, data) 30 { 31 printf("%s\n",data); 32 } 33 } 34 void printIntArray(array_t * array) 35 { 36 37 int i; 38 int data; 39 arrayForEachItem(int, array, i, data) 40 { 41 printf("%d\n",data); 42 } 43 } 25 44 st_table * generateAllLatches(Ntk_Network_t * ntk) 26 45 { -
vis_dev/vis-2.3/src/rob/Robust.c
r30 r98 1696 1696 * Synopsis [Generate name of protected register] 1697 1697 1698 Description [Generate file containing names of latches in t he golden model that have to be1699 protected. ]1698 Description [Generate file containing names of latches in the golden model 1699 that have to be protected. ] 1700 1700 1701 1701 SideEffects [] -
vis_dev/vis-2.3/src/rob/robCmd.c
r43 r98 1484 1484 Hrc_Node_t * rootNode = Hrc_ManagerReadRootNode(*hmgr); 1485 1485 if(rootNode == NIL(Hrc_Node_t)){ 1486 printf("Please build the network first ");1486 printf("Please build the network first\n"); 1487 1487 return 1; 1488 1488 } … … 1491 1491 Hrc_Node_t * goldenNode = Hrc_NodeFindChildByName(rootNode, name); 1492 1492 if(goldenNode == NIL(Hrc_Node_t)){ 1493 printf(" Please build the network first");1493 printf("Compose the network with a golden name golden first\n"); 1494 1494 return 1; 1495 1495 }
Note: See TracChangeset
for help on using the changeset viewer.