VIS
|
00001 00027 #include "restrInt.h" 00028 00029 /*---------------------------------------------------------------------------*/ 00030 /* Constant declarations */ 00031 /*---------------------------------------------------------------------------*/ 00032 00033 00034 /*---------------------------------------------------------------------------*/ 00035 /* Type declarations */ 00036 /*---------------------------------------------------------------------------*/ 00037 00038 00039 /*---------------------------------------------------------------------------*/ 00040 /* Structure declarations */ 00041 /*---------------------------------------------------------------------------*/ 00042 00043 /*---------------------------------------------------------------------------*/ 00044 /* Variable declarations */ 00045 /*---------------------------------------------------------------------------*/ 00046 extern int restrCreatedPart; 00047 extern int restrCreatedFsm; 00048 extern boolean restrVerbose; 00049 00050 /*---------------------------------------------------------------------------*/ 00051 /* Macro declarations */ 00052 /*---------------------------------------------------------------------------*/ 00053 00054 00057 /*---------------------------------------------------------------------------*/ 00058 /* Static function prototypes */ 00059 /*---------------------------------------------------------------------------*/ 00060 00061 static array_t * BuildFunctions(graph_t *partition, array_t *rootNames); 00062 static bdd_node ** AddPowerSolve(bdd_manager *mgr, bdd_node *bddTr, bdd_node *init, bdd_node **x, bdd_node **y, bdd_node **pi, st_table *inputProb, int nVars, int nPi); 00063 static bdd_node * PerformRestructure(bdd_manager *ddManager, bdd_node *prunedTR, bdd_node *equivRel, bdd_node *reachable, bdd_node *initBdd, bdd_node **piVars, bdd_node **xVars, bdd_node **yVars, bdd_node **uVars, bdd_node **vVars, st_table *inputProb, int nVars, int nPi, RestructureHeuristic heuristic, boolean equivClasses, array_t **outBdds, bdd_node **newInit, bdd_node **stateProbs); 00064 static st_table * CreateNameToMvfTable(bdd_manager *ddManager, array_t *outBdds, array_t *nextBdds, array_t *outputArray, array_t *tranFunArray); 00065 static st_table * CreateCareTable(Ntk_Network_t *network, mdd_t *reachMdd); 00066 static enum st_retval StMvfFree(char *key, char *value, char *arg); 00067 static void CountEquivalentClasses(bdd_manager *ddManager, bdd_node *equivRel, bdd_node *initBdd, bdd_node **xVars, bdd_node **uVars, int nVars); 00068 static array_t * GetBddArrayFromMvfArray(array_t *mvfArray); 00069 static bdd_node * DoMarkovPowerAnalysis(bdd_manager *ddManager, bdd_node *prunedTR, bdd_node *initBdd, bdd_node **piVars, bdd_node **xVars, bdd_node **yVars, st_table *inputProb, int nVars, int nPi); 00070 static array_t * ExtractTransitionFuns(bdd_manager *ddManager, bdd_node *finalTR, bdd_node **yVars, int nVars); 00071 static array_t * GetBddArrayFromNameArray(Fsm_Fsm_t *fsm, array_t *nameArray); 00072 static void ExpandReachableSet(bdd_manager *ddManager, bdd_node **reachable, bdd_node *equivRel, bdd_node **xVars, bdd_node **uVars, int nVars); 00073 static graph_t * CreateNewPartition(Ntk_Network_t *network, bdd_manager *ddManager, array_t *outBdds, array_t *nextBdds, array_t *outputArray, array_t *tranFunArray); 00074 static Fsm_Fsm_t * CreateNewFsm(Ntk_Network_t *network, graph_t *partition, bdd_manager *ddManager, bdd_node *finalTR, bdd_node *initBdd, bdd_node *reachable, bdd_node *stateProbs, bdd_node **xVars, bdd_node **yVars, bdd_node **piVars, st_table *inputProb, int nVars, int nPi); 00075 00079 /*---------------------------------------------------------------------------*/ 00080 /* Definition of exported functions */ 00081 /*---------------------------------------------------------------------------*/ 00082 00083 /*---------------------------------------------------------------------------*/ 00084 /* Definition of internal functions */ 00085 /*---------------------------------------------------------------------------*/ 00086 00134 int 00135 RestrCommandRestructureFsm( 00136 Fsm_Fsm_t *fsm, 00137 RestructureHeuristic heuristic, 00138 char *orderFileName, 00139 boolean equivClasses, 00140 boolean nonReachEquiv, 00141 boolean eqvMethod, 00142 st_table *inputProb, 00143 Synth_InfoData_t *synthInfo) 00144 { 00145 00146 graph_t *partition; 00147 Ntk_Network_t *network1; 00148 bdd_manager *ddManager; 00149 00150 array_t *outputArray, *tranFunArray; 00151 array_t *outBdds, *nextBdds; 00152 array_t *tranRelationPair; 00153 array_t *newStateVars; 00154 00155 st_table *careTable; 00156 00157 int i; 00158 int nVars, nPi; 00159 int noRestruct = 0; 00160 boolean status; 00161 00162 bdd_node *Lambda, *productTranRel, *prunedTR, *initialTR; 00163 bdd_node *equivRel; 00164 bdd_node *stateProbs; 00165 bdd_node *finalTR = NIL(bdd_node); 00166 bdd_node **xVars,**yVars,**uVars,**vVars; 00167 bdd_node **piVars; 00168 bdd_node *ddTemp, *reachable, *initBdd; 00169 bdd_node *newInit; 00170 00171 mdd_t *reachStates, *mddTemp; 00172 mdd_t *careMdd; 00173 00174 FILE *outFile; 00175 00176 network1 = Fsm_FsmReadNetwork(fsm); 00177 ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(network1); 00178 00179 /* Get the bdd_node for primary, present and next state variables.*/ 00180 piVars = RestrBddNodeArrayFromIdArray(ddManager, 00181 Fsm_FsmReadInputVars(fsm)); 00182 xVars = RestrBddNodeArrayFromIdArray(ddManager, 00183 Fsm_FsmReadPresentStateVars(fsm)); 00184 yVars = RestrBddNodeArrayFromIdArray(ddManager, 00185 Fsm_FsmReadNextStateVars(fsm)); 00186 /* Create new state variables for duplicate machine. */ 00187 newStateVars = RestrCreateNewStateVars(network1, ddManager,xVars,yVars); 00188 uVars = RestrBddNodeArrayFromIdArray(ddManager, 00189 array_fetch(array_t *, 00190 newStateVars, 0)); 00191 vVars = RestrBddNodeArrayFromIdArray(ddManager, 00192 array_fetch(array_t *, 00193 newStateVars, 1)); 00194 00195 /* Free memory: Delete the id array for new state variables.*/ 00196 array_free(array_fetch(array_t *,newStateVars,0)); 00197 array_free(array_fetch(array_t *,newStateVars,1)); 00198 array_free(newStateVars); 00199 00200 /* outputArray is the list of primary outputs. It is my responsibility to 00201 free it later. Both outputArray and tranFunArray are char * arrays. Get the 00202 BDDs for output functions and transition functions. Duplicate functions are 00203 returned.*/ 00204 00205 /* tranFunArray should not be freed */ 00206 outputArray = RestrGetOutputArray(network1); 00207 tranFunArray = Fsm_FsmReadNextStateFunctionNames(fsm); 00208 outBdds = GetBddArrayFromNameArray(fsm,outputArray); 00209 nextBdds = GetBddArrayFromNameArray(fsm,tranFunArray); 00210 00211 nVars = array_n(Fsm_FsmReadNextStateVars(fsm)); 00212 nPi = array_n(Fsm_FsmReadInputVars(fsm)); 00213 00214 /* Compute Lambda = AND (out1 xnor out1$NTK2) and Transition relation. 00215 out1$NTK2 is the corresponding primary output (of output1) in the duplicate 00216 machine.*/ 00217 if (restrVerbose) { 00218 fprintf(vis_stdout,"** restr info: Computing product output ... "); 00219 } 00220 Lambda = RestrCreateProductOutput(ddManager,outBdds,xVars, uVars, nVars); 00221 if (restrVerbose) { 00222 fprintf(vis_stdout,"Done.\n"); 00223 } 00224 00225 if (restrVerbose) { 00226 fprintf(vis_stdout,"** restr info: Computing TR of product machine ... "); 00227 } 00228 /* Compute the transition relation for both the single FSM and the product 00229 machine. tranRelationPair[0] is the TR of single FSM and 00230 tranRelationPair[1] is the TR of product machine. 00231 TR(x,w,y) = \prod_{i=0}^{i=n-1} (y_i \equiv f_i(w,x)) 00232 productTR(x,u,w,y,v) = TR(x,w,y) * TR(u,w,v) */ 00233 tranRelationPair = RestrComputeTRWithIds(ddManager,nextBdds,xVars, yVars, 00234 uVars,vVars,nVars); 00235 if (restrVerbose) { 00236 fprintf(vis_stdout,"Done.\n"); 00237 } 00238 00239 productTranRel = array_fetch(bdd_node *,tranRelationPair,1); 00240 00241 /* Compute the state equivalence relation for the FSM */ 00242 /* The support of equivRel is xVars and uVars. */ 00243 if (restrVerbose) { 00244 fprintf(vis_stdout,"** restr info: Computing the equivalence relation ... "); 00245 } 00246 00247 if (eqvMethod) { 00248 equivRel = RestrComputeEquivRelationUsingCofactors(ddManager,Lambda, 00249 productTranRel, 00250 xVars, yVars, uVars, 00251 vVars, piVars, 00252 nVars, nPi, 00253 restrVerbose); 00254 bdd_recursive_deref(ddManager,Lambda); 00255 } else { 00256 equivRel = RestrGetEquivRelation(ddManager,Lambda,productTranRel, 00257 xVars,yVars,uVars,vVars, 00258 piVars,nVars,nPi,restrVerbose); 00259 bdd_recursive_deref(ddManager,Lambda); 00260 } 00261 if (restrVerbose) { 00262 fprintf(vis_stdout,"Done.\n"); 00263 } 00264 /* Delete the product transition relation, as we no longer need it. */ 00265 bdd_recursive_deref(ddManager,productTranRel); 00266 00267 /* Compute the initial states */ 00268 mddTemp = Fsm_FsmComputeInitialStates(fsm); 00269 initBdd = bdd_extract_node_as_is(mddTemp); 00270 bdd_ref(initBdd); 00271 mdd_free(mddTemp); 00272 00273 /* Compute the reachable states. */ 00274 reachStates = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000, 00275 Fsm_Rch_Default_c,0,0, 00276 NIL(array_t),FALSE, NIL(array_t)); 00277 00278 reachable = bdd_extract_node_as_is(reachStates); 00279 bdd_ref(reachable); 00280 mdd_free(reachStates); 00281 00282 /* Check to see if there are any usable equivalence classes */ 00283 if (bdd_count_minterm(ddManager,equivRel,2*nVars) == pow(2.0,nVars)) { 00284 fprintf(vis_stdout,"** restr info: Number of equivalence classes equals "); 00285 fprintf(vis_stdout,"number of possible states. \n"); 00286 fprintf(vis_stdout,"** restr info: Restructuring will not help.\n"); 00287 fprintf(vis_stdout,"** restr info: Proceeding with synthesis.\n"); 00288 bdd_recursive_deref(ddManager,equivRel); 00289 /* Do not perform restructuring */ 00290 noRestruct = 1; 00291 } 00292 00293 /* Expand the reachable set R(x) to include those states which are equivalent 00294 to R(x) but unreachable. */ 00295 if(nonReachEquiv && !noRestruct) { 00296 ExpandReachableSet(ddManager,&reachable,equivRel,xVars,uVars,nVars); 00297 } 00298 00299 if (noRestruct) { 00300 /* Only synthesize the network */ 00301 bdd_recursive_deref(ddManager,equivRel); 00302 bdd_recursive_deref(ddManager, 00303 array_fetch(bdd_node *,tranRelationPair,0)); 00304 array_free(tranRelationPair); 00305 } else { 00306 /* Constrain the original TR */ 00307 initialTR = array_fetch(bdd_node *, tranRelationPair, 0); 00308 /* bdd_ref(prunedTR = bdd_bdd_and(ddManager,initialTR,reachable)); */ 00309 bdd_ref(prunedTR = initialTR); 00310 bdd_recursive_deref(ddManager,initialTR); 00311 array_free(tranRelationPair); 00312 00313 finalTR = PerformRestructure(ddManager,prunedTR,equivRel,reachable, 00314 initBdd,piVars,xVars,yVars,uVars, 00315 vVars,inputProb,nVars,nPi,heuristic, 00316 equivClasses,&outBdds,&newInit, 00317 &stateProbs); 00318 /* equivRel is dereferenced in the above procedure */ 00319 if (prunedTR == finalTR) { 00320 fprintf(vis_stdout,"** restr info: Restructuring produces no changes. \n"); 00321 fprintf(vis_stdout,"** restr info: Proceeding with synthesis. \n"); 00322 bdd_recursive_deref(ddManager,stateProbs); 00323 noRestruct = 1; 00324 } 00325 00326 bdd_recursive_deref(ddManager,prunedTR); 00327 bdd_recursive_deref(ddManager,initBdd); 00328 00329 /* reachable can be deleted after computing the new reachable states. Also 00330 need to perform markov analysis to find final bit change. */ 00331 initBdd = newInit; 00332 if (!noRestruct) { 00333 arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) { 00334 bdd_recursive_deref(ddManager,ddTemp); 00335 } 00336 array_free(nextBdds); 00337 nextBdds = ExtractTransitionFuns(ddManager,finalTR,yVars,nVars); 00338 } 00339 } 00340 00341 /* Create a partition for the new view of the fsm/network */ 00342 if (!noRestruct) { 00343 partition = CreateNewPartition(network1,ddManager,outBdds,nextBdds, 00344 outputArray,tranFunArray); 00345 array_free(outBdds); 00346 array_free(nextBdds); 00347 /* Create the FSM and perform markov ananlysis */ 00348 /* finalTR, stateProbs and reachabale are deleted in CreateNewFsm */ 00349 fsm = CreateNewFsm(network1,partition,ddManager,finalTR,initBdd, 00350 reachable,stateProbs,xVars,yVars,piVars, 00351 inputProb,nVars,nPi); 00352 } else { 00353 /* Remove the outBdds, nextBdds */ 00354 arrayForEachItem(bdd_node *, outBdds, i, ddTemp) { 00355 bdd_recursive_deref(ddManager,ddTemp); 00356 } 00357 arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) { 00358 bdd_recursive_deref(ddManager,ddTemp); 00359 } 00360 array_free(outBdds); 00361 array_free(nextBdds); 00362 } 00363 00364 /* First create the care table for next state and primary output 00365 functions. */ 00366 careMdd = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000, 00367 Fsm_Rch_Default_c,0,0, 00368 NIL(array_t),FALSE, NIL(array_t)); 00369 00370 careTable = CreateCareTable(network1,careMdd); 00371 00372 /* Synthesize the restructured FSM */ 00373 status = Synth_SynthesizeFsm(fsm,careTable,synthInfo,0); 00374 00375 /* Clean up */ 00376 if (!noRestruct) { 00377 Ntk_NetworkFreeApplInfo(network1,RESTR_PART_NETWORK_APPL_KEY); 00378 Ntk_NetworkFreeApplInfo(network1,RESTR_FSM_NETWORK_APPL_KEY); 00379 } 00380 mdd_free(careMdd); 00381 st_free_table(careTable); 00382 00383 /* Dump the current BDD variable order, for future use. */ 00384 if(orderFileName) { 00385 outFile = fopen(orderFileName,"w"); 00386 if(outFile) { 00387 int size = array_n(mdd_ret_mvar_list(ddManager)); 00388 int index; 00389 mvar_type var; 00390 for(i = 0; i < size;i++) { 00391 index = bdd_get_id_from_level(ddManager,i); 00392 var = mdd_get_var_by_id(ddManager,index); 00393 fprintf(outFile,"%s\n",var.name); 00394 } 00395 fclose(outFile); 00396 } else { 00397 fprintf(vis_stderr,"** restr error: Cannot open %s .\n",orderFileName); 00398 } 00399 } 00400 00401 /* Clean up */ 00402 for(i = 0; i < nVars; i++) { 00403 bdd_recursive_deref(ddManager,xVars[i]); 00404 bdd_recursive_deref(ddManager,yVars[i]); 00405 bdd_recursive_deref(ddManager,uVars[i]); 00406 bdd_recursive_deref(ddManager,vVars[i]); 00407 } 00408 for(i = 0 ; i < nPi; i++) { 00409 bdd_recursive_deref(ddManager,piVars[i]); 00410 } 00411 FREE(xVars); 00412 FREE(yVars); 00413 FREE(uVars); 00414 FREE(vVars); 00415 FREE(piVars); 00416 00417 array_free(outputArray); 00418 00419 return (status); 00420 } 00421 00422 00423 /*---------------------------------------------------------------------------*/ 00424 /* Definition of static functions */ 00425 /*---------------------------------------------------------------------------*/ 00426 00436 static array_t * 00437 BuildFunctions( 00438 graph_t *partition, 00439 array_t *rootNames) 00440 { 00441 char *name; 00442 vertex_t *vertexPtr; 00443 Mvf_Function_t *mvf1; 00444 int i; 00445 array_t *result; 00446 00447 result = array_alloc(Mvf_Function_t *,0); 00448 arrayForEachItem(char *,rootNames,i,name) { 00449 vertexPtr = Part_PartitionFindVertexByName(partition,name); 00450 mvf1 = Mvf_FunctionDuplicate(Part_VertexReadFunction(vertexPtr)); 00451 array_insert(Mvf_Function_t *,result,i,mvf1); 00452 } 00453 00454 return result; 00455 } 00456 00471 static bdd_node ** 00472 AddPowerSolve( 00473 bdd_manager *mgr, 00474 bdd_node *bddTr, 00475 bdd_node *init, 00476 bdd_node **x, 00477 bdd_node **y, 00478 bdd_node **pi, 00479 st_table *inputProb, 00480 int nVars, 00481 int nPi) 00482 { 00483 bdd_node *temp1, *temp, *q, *Correction; 00484 bdd_node **result, *tr; 00485 bdd_node **xAddVars, **yAddVars; 00486 bdd_node *initG, *NewG; 00487 bdd_node *inputCube,*xCube; 00488 bdd_node *newTr, *probMatrix; 00489 int iter = 0; 00490 int i; 00491 double max,relTol = 0.0001; 00492 00493 /* Initialize variables */ 00494 result = ALLOC(bdd_node *, 2); 00495 xAddVars = ALLOC(bdd_node *, nVars); 00496 yAddVars = ALLOC(bdd_node *, nVars); 00497 for (i = 0; i < nVars; i++) { 00498 bdd_ref(xAddVars[i] = bdd_add_ith_var(mgr, bdd_node_read_index(x[i]))); 00499 bdd_ref(yAddVars[i] = bdd_add_ith_var(mgr, bdd_node_read_index(y[i]))); 00500 } 00501 bdd_ref(tr = bdd_bdd_to_add(mgr, bddTr)); 00502 00503 /* Create the input cube for abstraction */ 00504 bdd_ref(temp1 = bdd_bdd_compute_cube(mgr, pi, NIL(int), nPi)); 00505 bdd_ref(inputCube = bdd_bdd_to_add(mgr, temp1)); 00506 bdd_recursive_deref(mgr, temp1); 00507 00508 /* Compute the one-step transition probability matrix. */ 00509 if (inputProb) { 00510 bdd_ref(probMatrix = Mark_addInProb(mgr,tr,inputCube,inputProb)); 00511 bdd_recursive_deref(mgr,inputCube); 00512 bdd_recursive_deref(mgr,tr); 00513 } 00514 else { 00515 bdd_ref(Correction = bdd_add_const(mgr,(1.0/(double)(1 << nPi)))); 00516 bdd_ref(q = bdd_add_exist_abstract(mgr,tr,inputCube)); 00517 bdd_recursive_deref(mgr,inputCube); 00518 bdd_recursive_deref(mgr,tr); 00519 /* apply correction to the transition relation matrix and print it */ 00520 bdd_ref(probMatrix = bdd_add_apply(mgr, bdd_add_times, q, Correction)); 00521 bdd_recursive_deref(mgr,Correction); 00522 bdd_recursive_deref(mgr,q); 00523 } 00524 result[1] = probMatrix; 00525 00526 /* Prepare the initial prob. vector. and the transition prob. matrix. */ 00527 initG = bdd_add_swap_variables(mgr,init,xAddVars,yAddVars,nVars); 00528 bdd_ref(initG); 00529 /* Put transition prob. matrix in appropriate form (transpose). */ 00530 newTr = bdd_add_swap_variables(mgr,probMatrix,xAddVars,yAddVars,nVars); 00531 bdd_ref(newTr); 00532 00533 /* Calculate the x-cube for abstraction */ 00534 bdd_ref(xCube = bdd_add_compute_cube(mgr,xAddVars,NIL(int),nVars)); 00535 00536 /* Loop until convergence */ 00537 do { 00538 iter++; 00539 bdd_ref(temp = bdd_add_matrix_multiply(mgr,newTr,initG,yAddVars,nVars)); 00540 bdd_ref(temp1 = bdd_add_exist_abstract(mgr,temp,xCube)); 00541 bdd_ref(NewG = bdd_add_apply(mgr,bdd_add_divide,temp,temp1)); 00542 bdd_recursive_deref(mgr,temp); 00543 bdd_recursive_deref(mgr,temp1); 00544 temp = NewG; 00545 bdd_ref(q = bdd_add_swap_variables(mgr,temp,xAddVars,yAddVars,nVars)); 00546 max = bdd_add_value(bdd_add_find_max(mgr,initG)); 00547 00548 if(bdd_equal_sup_norm(mgr,q,initG,relTol*max,0)) { 00549 bdd_recursive_deref(mgr,initG); 00550 bdd_recursive_deref(mgr,q); 00551 bdd_recursive_deref(mgr,xCube); 00552 bdd_recursive_deref(mgr,newTr); 00553 00554 bdd_ref(temp1 = bdd_add_apply(mgr,bdd_add_times,probMatrix,temp)); 00555 if (restrVerbose) { 00556 fprintf(vis_stdout,"** restr info: Average state bit change = %f\n", 00557 RestrAverageBitChange(mgr,temp1,x,y,nVars)); 00558 } 00559 00560 bdd_recursive_deref(mgr,temp1); 00561 for(i = 0;i < nVars; i++) { 00562 bdd_recursive_deref(mgr,xAddVars[i]); 00563 bdd_recursive_deref(mgr,yAddVars[i]); 00564 } 00565 FREE(xAddVars); 00566 FREE(yAddVars); 00567 result[0] = temp; 00568 return result; 00569 } 00570 bdd_recursive_deref(mgr,initG); 00571 bdd_recursive_deref(mgr,temp); 00572 initG = q; 00573 00574 } while (1); 00575 00576 } /* end of AddPowerSolve */ 00577 00591 static bdd_node * 00592 PerformRestructure( 00593 bdd_manager *ddManager, 00594 bdd_node *prunedTR, 00595 bdd_node *equivRel, 00596 bdd_node *reachable, 00597 bdd_node *initBdd, 00598 bdd_node **piVars, 00599 bdd_node **xVars, 00600 bdd_node **yVars, 00601 bdd_node **uVars, 00602 bdd_node **vVars, 00603 st_table *inputProb, 00604 int nVars, 00605 int nPi, 00606 RestructureHeuristic heuristic, 00607 boolean equivClasses, 00608 array_t **outBdds, 00609 bdd_node **newInit, 00610 bdd_node **stateProbs) 00611 { 00612 /* equivRel is a function of uVars and xVars */ 00613 /* prunedTR is a funciton of xVars, piVars and yVars */ 00614 00615 bdd_node *possessedProbMatrix; 00616 bdd_node *possessedTR = NIL(bdd_node); 00617 bdd_node *addPTR; 00618 bdd_node *finalTR; 00619 bdd_node *ddTemp; 00620 bdd_node *localStateProbs = NIL(bdd_node); 00621 00622 if(equivClasses) { 00623 CountEquivalentClasses(ddManager,equivRel,initBdd,xVars,uVars,nVars); 00624 } 00625 00626 /* Change the support of equivRel */ 00627 bdd_ref(ddTemp = bdd_bdd_swap_variables(ddManager,equivRel,xVars,yVars, 00628 nVars)); 00629 bdd_recursive_deref(ddManager,equivRel); 00630 bdd_ref(equivRel = bdd_bdd_swap_variables(ddManager,ddTemp,uVars,vVars, 00631 nVars)); 00632 bdd_recursive_deref(ddManager, ddTemp); 00633 00634 /* The support of possessedTR is xVars and yVars and inputs. 00635 * If there exists an edge between x and y, and y == v, then 00636 * the following function adds an edge between x and v. These new 00637 * edges are referred to as ghost edges. 00638 */ 00639 00640 if (heuristic != RestrCProjection_c) { 00641 possessedTR = RestrComputeTrWithGhostEdges(ddManager, yVars, vVars, 00642 prunedTR, equivRel, nVars); 00643 } 00644 00645 /* stateProbs will not be used in the case of CProj and hammingD methods. We 00646 can still compute the stateProbs to find the initial average bit change on 00647 the state lines. */ 00648 *stateProbs = DoMarkovPowerAnalysis(ddManager,prunedTR, 00649 initBdd,piVars,xVars, 00650 yVars,inputProb,nVars,nPi); 00651 00652 if (!(heuristic == RestrCProjection_c || heuristic == RestrHammingD_c)) { 00653 bdd_node *temp, *cube; 00654 00655 bdd_ref(cube = bdd_bdd_compute_cube(ddManager,piVars,NIL(int),nPi)); 00656 bdd_ref(temp = bdd_bdd_exist_abstract(ddManager,possessedTR,cube)); 00657 bdd_ref(addPTR = bdd_bdd_to_add(ddManager,temp)); 00658 bdd_recursive_deref(ddManager,temp); 00659 00660 bdd_ref(temp = bdd_bdd_to_add(ddManager, possessedTR)); 00661 bdd_recursive_deref(ddManager, possessedTR); 00662 00663 /* possessedProbMatrix is a weighted augmented STG where the weights are 00664 the transition probabilities */ 00665 if (inputProb) { 00666 bdd_ref(possessedProbMatrix = Mark_addInProb(ddManager,temp,cube, 00667 inputProb)); 00668 } else { 00669 /* Assume equi probable primary inputs */ 00670 bdd_node *q, *Correction; 00671 bdd_node *inputCube; 00672 00673 bdd_ref(inputCube = bdd_bdd_to_add(ddManager,cube)); 00674 bdd_ref(Correction = bdd_add_const(ddManager, 00675 (1.0/(double)(1 << nPi)))); 00676 bdd_ref(q = bdd_add_exist_abstract(ddManager,temp,inputCube)); 00677 bdd_ref(possessedProbMatrix = bdd_add_apply(ddManager, 00678 bdd_add_times, 00679 q, Correction)); 00680 bdd_recursive_deref(ddManager,Correction); 00681 bdd_recursive_deref(ddManager,q); 00682 bdd_recursive_deref(ddManager,inputCube); 00683 } 00684 bdd_recursive_deref(ddManager,cube); 00685 bdd_recursive_deref(ddManager,temp); 00686 localStateProbs = *stateProbs; 00687 } 00688 00689 switch(heuristic) { 00690 case RestrCProjection_c: 00691 finalTR = RestrMinimizeFsmByCProj(ddManager,equivRel, 00692 prunedTR,initBdd, 00693 xVars,yVars,uVars,vVars,piVars, 00694 nVars,nPi,outBdds,newInit); 00695 break; 00696 case RestrFanin_c: 00697 case RestrFaninFanout_c: 00698 ddTemp = bdd_read_background(ddManager); 00699 bdd_set_background(ddManager, 00700 bdd_read_plus_infinity(ddManager)); 00701 00702 /* addPTR and possessedProbMatrix are deleted in the following 00703 * procedure. */ 00704 finalTR = RestrMinimizeFsmByFaninFanout(ddManager,equivRel, prunedTR, 00705 &addPTR,&possessedProbMatrix,initBdd, 00706 reachable,localStateProbs,piVars,xVars, 00707 yVars, uVars,vVars, 00708 nVars, nPi,heuristic,outBdds,newInit); 00709 00710 /* Replace the original background value */ 00711 bdd_set_background(ddManager,ddTemp); 00712 break; 00713 case RestrHammingD_c: 00714 default : 00715 00716 /* BALA, testing ... */ 00717 /* Remove the edges out of the initial state. */ 00718 { 00719 /* bdd_node *outEdges; */ 00720 00721 /* bdd_ref(outEdges = bdd_bdd_and(ddManager,prunedTR,initBdd)); */ 00722 /* bdd_ref(adjustedTR = bdd_bdd_and(ddManager,prunedTR, */ 00723 /* bdd_not_bdd_node(outEdges))); */ 00724 /* finalTR = RestrSelectLeastHammingDStates(ddManager,adjustedTR, */ 00725 /* possessedTR,xVars, */ 00726 /* yVars,vVars,nVars,nPi); */ 00727 00728 finalTR = RestrSelectLeastHammingDStates(ddManager,prunedTR, 00729 possessedTR,xVars, 00730 yVars,vVars,nVars,nPi); 00731 bdd_recursive_deref(ddManager,possessedTR); 00732 bdd_ref(*newInit = initBdd); 00733 break; 00734 } 00735 } 00736 00737 bdd_recursive_deref(ddManager,equivRel); 00738 return finalTR; 00739 } 00740 00753 static st_table * 00754 CreateNameToMvfTable( 00755 bdd_manager *ddManager, 00756 array_t *outBdds, 00757 array_t *nextBdds, 00758 array_t *outputArray, 00759 array_t *tranFunArray) 00760 { 00761 st_table *nameToMvf; 00762 bdd_node *ddTemp; 00763 int i; 00764 00765 /* Initialize variables */ 00766 nameToMvf = st_init_table(strcmp, st_strhash); 00767 00768 arrayForEachItem(bdd_node *, outBdds, i, ddTemp) { 00769 bdd_node *temp; 00770 mdd_t *regular, *complement; 00771 Mvf_Function_t *mvf; 00772 char *name; 00773 00774 bdd_ref(temp = bdd_not_bdd_node(ddTemp)); 00775 00776 regular = bdd_construct_bdd_t(ddManager,ddTemp); 00777 complement = bdd_construct_bdd_t(ddManager,temp); 00778 00779 mvf = (Mvf_Function_t *)array_alloc(mdd_t *, 0); 00780 array_insert(mdd_t *, mvf, 0, complement); 00781 array_insert(mdd_t *, mvf, 1, regular); 00782 00783 name = array_fetch(char *, outputArray, i); 00784 st_insert(nameToMvf,name,(char *)mvf); 00785 } 00786 00787 arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) { 00788 bdd_node *temp; 00789 mdd_t *regular, *complement; 00790 Mvf_Function_t *mvf; 00791 char *name; 00792 00793 bdd_ref(temp = bdd_not_bdd_node(ddTemp)); 00794 00795 regular = bdd_construct_bdd_t(ddManager,ddTemp); 00796 complement = bdd_construct_bdd_t(ddManager,temp); 00797 00798 mvf = (Mvf_Function_t *)array_alloc(mdd_t *, 0); 00799 array_insert(mdd_t *, mvf, 0, complement); 00800 array_insert(mdd_t *, mvf, 1, regular); 00801 00802 name = array_fetch(char *, tranFunArray, i); 00803 st_insert(nameToMvf,name,(char *)mvf); 00804 } 00805 00806 return nameToMvf; 00807 } 00808 00809 00819 static st_table * 00820 CreateCareTable( 00821 Ntk_Network_t *network, 00822 mdd_t *reachMdd) 00823 { 00824 lsGen gen; 00825 Ntk_Node_t *node; 00826 st_table *careTable; 00827 00828 careTable = st_init_table(strcmp, st_strhash); 00829 Ntk_NetworkForEachPrimaryOutput(network, gen, node) { 00830 char *name; 00831 name = Ntk_NodeReadName(node); 00832 st_insert(careTable,name,(char *)reachMdd); 00833 } 00834 Ntk_NetworkForEachLatch(network,gen,node){ 00835 char *name; 00836 name = Ntk_NodeReadName(Ntk_LatchReadDataInput(node)); 00837 st_insert(careTable,name,(char *)reachMdd); 00838 } 00839 00840 return careTable; 00841 } 00842 00851 static enum st_retval 00852 StMvfFree( 00853 char *key, 00854 char *value, 00855 char *arg) 00856 { 00857 /* This will free the memory associated with the array also */ 00858 Mvf_FunctionFree((Mvf_Function_t *)value); 00859 00860 return(ST_CONTINUE); 00861 00862 } /* end of StMvfFree */ 00863 00864 00874 static void 00875 CountEquivalentClasses( 00876 bdd_manager *ddManager, 00877 bdd_node *equivRel, 00878 bdd_node *initBdd, 00879 bdd_node **xVars, 00880 bdd_node **uVars, 00881 int nVars) 00882 { 00883 bdd_node *resultXU,*uCube; 00884 bdd_node *oneInitState,*classes; 00885 00886 oneInitState = bdd_bdd_pick_one_minterm(ddManager,initBdd,xVars,nVars); 00887 bdd_ref(oneInitState); 00888 00889 bdd_ref(resultXU = bdd_bdd_cprojection(ddManager,equivRel,oneInitState)); 00890 bdd_recursive_deref(ddManager,oneInitState); 00891 00892 #ifdef RESTR_DIAG 00893 { 00894 /* The following is valid only when equivRel is the equivalence relation on 00895 the complete set of states.*/ 00896 bdd_node *xCube,*tautology; 00897 bdd_node *one; 00898 one = bdd_read_one(ddManager); 00899 bdd_ref(xCube = bdd_bdd_compute_cube(ddManager,xVars,NIL(int),nVars)); 00900 bdd_ref(tautology = bdd_bdd_exist_abstract(ddManager,resultXU,xCube)); 00901 assert(tautology == one); 00902 bdd_recursive_deref(ddManager,tautology); 00903 bdd_recursive_deref(ddManager,xCube); 00904 } 00905 #endif 00906 00907 #ifdef RESTR_DIAG 00908 { 00909 bdd_node *uCube,*zero,*classes; 00910 bdd_node *oneClass,*temp,*rep; 00911 int i; 00912 00913 zero = bdd_not_bdd_node(bdd_read_one(ddManager)); 00914 /* Extract the classes */ 00915 bdd_ref(uCube = bdd_bdd_compute_cube(ddManager,uVars,NIL(int),nVars)); 00916 bdd_ref(classes = bdd_bdd_exist_abstract(ddManager,resultXU,uCube)); 00917 bdd_recursive_deref(ddManager,uCube); 00918 00919 i = 0; 00920 (void) fprintf(vis_stdout,"\n** restr diag: EQUIVALENT CLASSES:\n"); 00921 while (classes != zero) { 00922 i++; 00923 bdd_ref(rep = bdd_bdd_pick_one_minterm(ddManager,classes, 00924 xVars,nVars)); 00925 (void) fprintf(vis_stdout,"** restr diag: Class %d\n",i); 00926 (void) fprintf(vis_stdout,"** restr diag: Class representative:\n"); 00927 RestrPrintBddNode(ddManager,rep); 00928 00929 /* Extract the complete class now */ 00930 bdd_ref(temp = bdd_bdd_cofactor(ddManager,resultXU,rep)); 00931 bdd_ref(oneClass = bdd_bdd_swap_variables(ddManager,temp,uVars, 00932 xVars,nVars)); 00933 bdd_recursive_deref(ddManager,temp); 00934 (void) fprintf(vis_stdout,"** restr diag: Class members:\n"); 00935 RestrPrintBddNode(ddManager,oneClass); 00936 bdd_recursive_deref(ddManager,oneClass); 00937 00938 /* Remove rep from classes */ 00939 bdd_ref(temp = bdd_bdd_and(ddManager,classes,bdd_not_bdd_node(rep))); 00940 bdd_recursive_deref(ddManager,rep); 00941 bdd_recursive_deref(ddManager,classes); 00942 classes = temp; 00943 } 00944 (void) fprintf(vis_stdout,"** restr diag: Number of classes = %d\n",i); 00945 } 00946 #endif 00947 00948 /* Compute uCube and extract the u variables from resultXU */ 00949 bdd_ref(uCube = bdd_bdd_compute_cube(ddManager,uVars,NIL(int),nVars)); 00950 bdd_ref(classes = bdd_bdd_exist_abstract(ddManager,resultXU,uCube)); 00951 bdd_recursive_deref(ddManager,uCube); 00952 bdd_recursive_deref(ddManager,resultXU); 00953 00954 fprintf(vis_stdout, "** restr info: Number of Equivalence Classes = %g\n", 00955 bdd_count_minterm(ddManager,classes,nVars)); 00956 00957 bdd_recursive_deref(ddManager,classes); 00958 } 00959 00960 00970 static array_t * 00971 GetBddArrayFromMvfArray(array_t *mvfArray) 00972 { 00973 int i; 00974 array_t *bddArray; 00975 Mvf_Function_t *mvf; 00976 00977 bddArray = array_alloc(bdd_node *,0); 00978 00979 arrayForEachItem(Mvf_Function_t *, mvfArray,i,mvf) { 00980 mdd_t *mddTemp; 00981 bdd_node *ddNode; 00982 00983 mddTemp = array_fetch(mdd_t *, mvf, 1); 00984 ddNode = bdd_extract_node_as_is(mddTemp); 00985 bdd_ref(ddNode); 00986 00987 array_insert_last(bdd_node *, bddArray, ddNode); 00988 } 00989 return bddArray; 00990 } 00991 01002 static bdd_node * 01003 DoMarkovPowerAnalysis( 01004 bdd_manager *ddManager, 01005 bdd_node *prunedTR, 01006 bdd_node *initBdd, 01007 bdd_node **piVars, 01008 bdd_node **xVars, 01009 bdd_node **yVars, 01010 st_table *inputProb, 01011 int nVars, 01012 int nPi) 01013 { 01014 bdd_node **result, *stateProbs; 01015 bdd_node *init; 01016 01017 bdd_ref(init = bdd_bdd_to_add(ddManager,initBdd)); 01018 if (restrVerbose) 01019 (void) fprintf(vis_stdout,"** restr info: Initial average state bit change:\n"); 01020 01021 result = AddPowerSolve(ddManager,prunedTR,init,xVars,yVars, 01022 piVars,inputProb,nVars,nPi); 01023 01024 bdd_recursive_deref(ddManager,result[1]); 01025 stateProbs = result[0]; 01026 bdd_recursive_deref(ddManager,init); 01027 FREE(result); 01028 01029 return stateProbs; 01030 } 01031 01041 static array_t * 01042 ExtractTransitionFuns( 01043 bdd_manager *ddManager, 01044 bdd_node *finalTR, 01045 bdd_node **yVars, 01046 int nVars) 01047 { 01048 bdd_node *completeCube, *extractCube; 01049 bdd_node *fun, *tranFun; 01050 array_t *allTranFuns; 01051 int i; 01052 01053 allTranFuns = array_alloc(bdd_node *,0); 01054 01055 completeCube = bdd_bdd_compute_cube(ddManager,yVars,NIL(int),nVars); 01056 bdd_ref(completeCube); 01057 01058 for(i = 0;i < nVars; i++) { 01059 extractCube = bdd_bdd_cofactor(ddManager,completeCube,yVars[i]); 01060 bdd_ref(extractCube); 01061 fun = bdd_bdd_exist_abstract(ddManager,finalTR,extractCube); 01062 bdd_ref(fun); 01063 bdd_recursive_deref(ddManager,extractCube); 01064 tranFun = bdd_bdd_cofactor(ddManager,fun,yVars[i]); 01065 bdd_ref(tranFun); 01066 01067 #ifdef RESTR_DIAG 01068 { 01069 /* The following is to test if there are multiple edges out of a state 01070 with the same input label: in short to check if the relation is 01071 deterministic or not. */ 01072 01073 bdd_node *yBar,*yNot,*inter; 01074 bdd_ref(yNot = bdd_not_bdd_node(yVars[i])); 01075 bdd_ref(yBar = bdd_bdd_cofactor(ddManager,fun,yNot)); 01076 bdd_recursive_deref(ddManager,yNot); 01077 bdd_ref(inter = bdd_bdd_and(ddManager,yBar,tranFun)); 01078 yNot = bdd_not_bdd_node(bdd_read_one(ddManager)); 01079 assert(inter == yNot); 01080 bdd_recursive_deref(ddManager,inter); 01081 bdd_recursive_deref(ddManager,yBar); 01082 } 01083 #endif 01084 01085 bdd_recursive_deref(ddManager,fun); 01086 array_insert_last(bdd_node *,allTranFuns,tranFun); 01087 } 01088 01089 bdd_recursive_deref(ddManager,completeCube); 01090 return allTranFuns; 01091 } 01092 01102 static array_t * 01103 GetBddArrayFromNameArray( 01104 Fsm_Fsm_t *fsm, 01105 array_t *nameArray) 01106 { 01107 graph_t *partition; 01108 array_t *bdds,*mvfs; 01109 01110 partition = Fsm_FsmReadPartition(fsm); 01111 mvfs = BuildFunctions(partition,nameArray); 01112 bdds = GetBddArrayFromMvfArray(mvfs); 01113 Mvf_FunctionArrayFree(mvfs); 01114 01115 return bdds; 01116 } 01117 01128 static void 01129 ExpandReachableSet( 01130 bdd_manager *ddManager, 01131 bdd_node **reachable, 01132 bdd_node *equivRel, 01133 bdd_node **xVars, 01134 bdd_node **uVars, 01135 int nVars) 01136 { 01137 bdd_node *xcube,*potUnReach,*extReach; 01138 bdd_node *temp1; 01139 01140 bdd_ref(xcube = bdd_bdd_compute_cube(ddManager,xVars,NIL(int),nVars)); 01141 /* potUnReach = \exists_x (E(x,u) * R(x)) */ 01142 bdd_ref(potUnReach = bdd_bdd_and_abstract(ddManager,*reachable, 01143 equivRel,xcube)); 01144 bdd_recursive_deref(ddManager,xcube); 01145 /* temp1(x) = potUnReach(u) */ 01146 bdd_ref(temp1 = bdd_bdd_swap_variables(ddManager,potUnReach,uVars, 01147 xVars,nVars)); 01148 bdd_recursive_deref(ddManager,potUnReach); 01149 /* extReach(x) = R(x) + potUnReach(x) */ 01150 bdd_ref(extReach = bdd_bdd_or(ddManager,*reachable,temp1)); 01151 bdd_recursive_deref(ddManager,temp1); 01152 bdd_recursive_deref(ddManager,*reachable); 01153 *reachable = extReach; 01154 } 01155 01165 static graph_t * 01166 CreateNewPartition( 01167 Ntk_Network_t *network, 01168 bdd_manager *ddManager, 01169 array_t *outBdds, 01170 array_t *nextBdds, 01171 array_t *outputArray, 01172 array_t *tranFunArray) 01173 { 01174 st_table *nameToMvf; 01175 graph_t *partition; 01176 01177 /* Create a table of next state and output Mvfs with their names as key to 01178 the table. This table is used to create a partition for the network. */ 01179 nameToMvf = CreateNameToMvfTable(ddManager,outBdds,nextBdds, 01180 outputArray,tranFunArray); 01181 /* Delete the old partition and old fsm as we dont need it any more */ 01182 if (restrCreatedPart) { 01183 Ntk_NetworkFreeApplInfo(network,RESTR_PART_NETWORK_APPL_KEY); 01184 restrCreatedPart = 0; 01185 } 01186 if (restrCreatedFsm) { 01187 Ntk_NetworkFreeApplInfo(network,RESTR_FSM_NETWORK_APPL_KEY); 01188 restrCreatedFsm = 0; 01189 } 01190 01191 /* Create a new partition from the new root functions */ 01192 partition = Part_NetworkCreatePartitionFromMvfs(network,nameToMvf); 01193 Ntk_NetworkAddApplInfo(network, RESTR_PART_NETWORK_APPL_KEY, 01194 (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback, 01195 (void *) partition); 01196 st_foreach(nameToMvf,StMvfFree,NIL(char)); 01197 st_free_table(nameToMvf); 01198 01199 return partition; 01200 } 01201 01213 static Fsm_Fsm_t * 01214 CreateNewFsm( 01215 Ntk_Network_t *network, 01216 graph_t *partition, 01217 bdd_manager *ddManager, 01218 bdd_node *finalTR, 01219 bdd_node *initBdd, 01220 bdd_node *reachable, 01221 bdd_node *stateProbs, 01222 bdd_node **xVars, 01223 bdd_node **yVars, 01224 bdd_node **piVars, 01225 st_table *inputProb, 01226 int nVars, 01227 int nPi) 01228 { 01229 Fsm_Fsm_t *fsm; 01230 mdd_t *reachStates; 01231 mdd_t *mddTemp; 01232 bdd_node *ddTemp; 01233 bdd_node **markovResult; 01234 01235 /* Create a new Fsm for the restructured network. */ 01236 fsm = Fsm_FsmCreateFromNetworkWithPartition(network, 01237 Part_PartitionDuplicate(partition)); 01238 assert(fsm != NIL(Fsm_Fsm_t)); 01239 Ntk_NetworkAddApplInfo(network, RESTR_FSM_NETWORK_APPL_KEY, 01240 (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback, 01241 (void *) fsm); 01242 /* We need to update the initial states as the 01243 Fsm_FsmCreateFromNetworkWithPartition will pick up old initial state from 01244 the network. Fsm_FsmSetInitialStates deletes old inital states. */ 01245 mddTemp = bdd_construct_bdd_t(ddManager,initBdd); 01246 Fsm_FsmSetInitialStates(fsm,mddTemp); 01247 01248 /* Compute the new reachable states */ 01249 reachStates = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000, 01250 Fsm_Rch_Default_c,0,0, 01251 NIL(array_t),FALSE, NIL(array_t)); 01252 01253 bdd_recursive_deref(ddManager,reachable); 01254 reachable = bdd_extract_node_as_is(reachStates); 01255 bdd_ref(reachable); 01256 mdd_free(reachStates); 01257 01258 /* Constrain the transition relation */ 01259 bdd_ref(ddTemp = bdd_bdd_constrain(ddManager,finalTR,reachable)); 01260 bdd_recursive_deref(ddManager,finalTR); 01261 finalTR = ddTemp; 01262 01263 /* Use the state probs. of the original STG as the initial guess to compute 01264 the state probs. of the restructured STG. */ 01265 if (restrVerbose) 01266 (void) fprintf(vis_stdout,"** restr info: Final average state bit change:\n"); 01267 01268 markovResult = AddPowerSolve(ddManager, finalTR, stateProbs, xVars, 01269 yVars,piVars,inputProb,nVars,nPi); 01270 bdd_recursive_deref(ddManager, markovResult[0]); 01271 bdd_recursive_deref(ddManager, markovResult[1]); 01272 FREE(markovResult); 01273 01274 bdd_recursive_deref(ddManager,stateProbs); 01275 bdd_recursive_deref(ddManager,finalTR); 01276 bdd_recursive_deref(ddManager,reachable); 01277 01278 return fsm; 01279 }