Changeset 98


Ignore:
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:
5 edited

Legend:

Unmodified
Added
Removed
  • vis_dev/vis-2.3/src/debug/debug.c

    r96 r98  
    399399  CommandArguments [\[-h\] \[-v\] \[-k\]  [fileName] ]
    400400 
    401   CommandDescription [This command geerate a CNF of the network in DMACS form.
     401  CommandDescription [This command generate a CNF of the network in DMACS form.
    402402  The network may be unroll within k steps.
    403403  <p>
     
    947947Ntk_Network_t  *network      = NIL(Ntk_Network_t);
    948948mdd_manager    *mddManager;
    949 mdd_t          *rel          = NIL(mdd_t);
     949Hrc_Manager_t  *hmgrCex       = NIL(Hrc_Manager_t);
     950Fsm_Fsm_t      *fsmCex        = NIL(Fsm_Fsm_t);
     951Ntk_Network_t  *networkCex    = NIL(Ntk_Network_t);
     952mdd_t          *rel           = NIL(mdd_t);
    950953int            i;
    951954/******************/
     
    958961mddManager   = Fsm_FsmReadMddManager(fsm);
    959962
    960 
     963mdd_t * initOrig  = Fsm_FsmComputeInitialStates(fsm);
     964mdd_FunctionPrintMain (mddManager ,initOrig,"INIT_ORG",vis_stdout);
    961965
    962966/**********   Build cex  ***********/
     
    968972array_t * nextNames = Fsm_FsmReadNextStateFunctionNames(fsm);
    969973array_t * nextIds =   Fsm_FsmReadNextStateVars(fsm);
    970 
     974array_t * currentIds = Fsm_FsmReadPresentStateVars(fsm);
     975printf("Next Names\n");
     976printStringArray(nextNames);
     977printf("Next Ids\n");
     978printIntArray(nextIds);
     979printf("Current Ids\n");
     980printIntArray(currentIds);
     981Img_ImageInfo_t * imageInfo = Fsm_FsmReadOrCreateImageInfo(fsm,1,0);
     982 graph_t * part = Part_PartitionDuplicate(Fsm_FsmReadPartition(fsm));
     983
     984lsGen gen;
     985vertex_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//}
     993vertex_t * v_s2 = Part_PartitionFindVertexByName(part, "cex.s2");
     994Mvf_Function_t*  vertexFunction = PartVertexReadFunction(v_s2);
     995  if (vertexFunction != NIL(Mvf_Function_t)) {
     996printf("number mvf function %d\n",Mvf_FunctionReadNumComponents( vertexFunction));
     997}
     998else
     999  printf("no fonction");
     1000
     1001Mvf_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);
     1010Mvf_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);
     1019FILE * file = fopen("mvf.txt","w");
     1020foreach_vertex(part, gen, vertexPtr) {
     1021fprintf(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}
     1056fclose(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 **/
     1085Ntk_NetworkSetApplInfo(network, PART_NETWORK_APPL_KEY,
     1086                                          (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback,
     1087                                          (void *) part);
     1088fsm = Fsm_FsmCreateFromNetworkWithPartition(network, NIL(graph_t*));
     1089mdd_t * init  = Fsm_FsmComputeInitialStates(fsm);
     1090//mdd_t * n_init =  Mvf_MddComposeWithFunction(init, 17 , newMvf);
     1091mdd_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   
     1102Ntk_NetworkSetApplInfo(network, FSM_NETWORK_APPL_KEY,
     1103                         (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback,
     1104                         (void *) fsm);
     1105
     1106Fsm_FsmReachabilityPrintResults(fsm,3, 0);
     1107//
     1108//
     1109mdd_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");
     1147fsmCex          =  Fsm_FsmCreateFromNetworkWithPartition(networkCex, partition);
     1148array_t * nextNamesCex = Fsm_FsmReadNextStateFunctionNames(fsmCex);
     1149array_t * nextIdsCex =   Fsm_FsmReadNextStateVars(fsmCex);
     1150printf("Next Names\n");
     1151printStringArray(nextNamesCex);
     1152printf("Next Ids\n");
     1153printIntArray(nextIdsCex);
     1154
     1155mddManager =  Fsm_FsmReadMddManager(fsm);
     1156mdd_manager * mddManagerCex =  Fsm_FsmReadMddManager(fsmCex);
     1157
     1158array_t *mvar_list, *bvar_list;
     1159mvar_list = mdd_ret_mvar_list(mddManager);
     1160bvar_list = mdd_ret_bvar_list(mddManager);
     1161printf("Number of mdd %d , %d\n", array_n(mvar_list),array_n(bvar_list));
     1162printf("mddManager = %p mddMangerCex %p \n",mddManager,mddManagerCex);
     1163 //mdd_t * init = Fsm_FsmComputeInitialStates(fsmCex);
     1164// mdd_FunctionPrintMain (mddManagerCex ,init,"REL",vis_stdout);
     1165graph_t * part = Fsm_FsmReadPartition(fsm);
     1166printf(" modele %s , cex %s \n",Part_PartitionReadName(part), Part_PartitionReadName(partition));
     1167*/
    9711168/** 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);
    10051202
    10061203return 0;               /* normal exit */
  • vis_dev/vis-2.3/src/debug/debugInt.h

    r45 r98  
    8383
    8484void printLatch(st_table* CoiTable);
     85void printStringArray(array_t * array);
     86void printIntArray(array_t * array);
    8587st_table * generateAllLatches(Ntk_Network_t * ntk);
    8688void mdd_GetState_Values(mdd_manager *mgr, mdd_t * top, FILE * f);
  • vis_dev/vis-2.3/src/debug/debugUtilities.c

    r44 r98  
    2222}
    2323
    24 
     24void 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}
     34void 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}
    2544st_table * generateAllLatches(Ntk_Network_t * ntk)
    2645{
  • vis_dev/vis-2.3/src/rob/Robust.c

    r30 r98  
    16961696 *  Synopsis    [Generate name of protected register]
    16971697
    1698   Description [Generate file containing names of latches int he golden model that have to be
    1699   protected. ]
     1698  Description [Generate file containing names of latches in the golden model
     1699  that have to be protected. ]
    17001700
    17011701  SideEffects []
  • vis_dev/vis-2.3/src/rob/robCmd.c

    r43 r98  
    14841484Hrc_Node_t * rootNode = Hrc_ManagerReadRootNode(*hmgr);
    14851485if(rootNode == NIL(Hrc_Node_t)){
    1486         printf("Please build the network first");
     1486        printf("Please build the network first\n");
    14871487        return 1;
    14881488}
     
    14911491Hrc_Node_t * goldenNode = Hrc_NodeFindChildByName(rootNode, name);
    14921492if(goldenNode == NIL(Hrc_Node_t)){
    1493         printf("Please build the network first");
     1493        printf("Compose the network with a golden name golden first\n");
    14941494        return 1;
    14951495}
Note: See TracChangeset for help on using the changeset viewer.