/**CFile*********************************************************************** FileName [restrRestructure.c] PackageName [restr] Synopsis [This file contains a main procedure that restructures an STG and transforms it into a new multilevel circuit.] Description [This file contains a main procedure that restructures an STG and transforms it into a new multilevel circuit. Please refer to "A symbolic algorithm for low power sequential synthesis," ISLPED 97, for more details.] SeeAlso [restrHammingD.c restrFaninout.c restrCProj.c] Author [Balakrishna Kumthekar ] Copyright [This file was created at the University of Colorado at Boulder. The University of Colorado at Boulder makes no warranty about the suitability of this software for any purpose. It is presented on an AS IS basis.] ******************************************************************************/ #include "restrInt.h" /*---------------------------------------------------------------------------*/ /* Constant declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Type declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Structure declarations */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Variable declarations */ /*---------------------------------------------------------------------------*/ extern int restrCreatedPart; extern int restrCreatedFsm; extern boolean restrVerbose; /*---------------------------------------------------------------------------*/ /* Macro declarations */ /*---------------------------------------------------------------------------*/ /**AutomaticStart*************************************************************/ /*---------------------------------------------------------------------------*/ /* Static function prototypes */ /*---------------------------------------------------------------------------*/ static array_t * BuildFunctions(graph_t *partition, array_t *rootNames); 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); 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); static st_table * CreateNameToMvfTable(bdd_manager *ddManager, array_t *outBdds, array_t *nextBdds, array_t *outputArray, array_t *tranFunArray); static st_table * CreateCareTable(Ntk_Network_t *network, mdd_t *reachMdd); static enum st_retval StMvfFree(char *key, char *value, char *arg); static void CountEquivalentClasses(bdd_manager *ddManager, bdd_node *equivRel, bdd_node *initBdd, bdd_node **xVars, bdd_node **uVars, int nVars); static array_t * GetBddArrayFromMvfArray(array_t *mvfArray); 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); static array_t * ExtractTransitionFuns(bdd_manager *ddManager, bdd_node *finalTR, bdd_node **yVars, int nVars); static array_t * GetBddArrayFromNameArray(Fsm_Fsm_t *fsm, array_t *nameArray); static void ExpandReachableSet(bdd_manager *ddManager, bdd_node **reachable, bdd_node *equivRel, bdd_node **xVars, bdd_node **uVars, int nVars); static graph_t * CreateNewPartition(Ntk_Network_t *network, bdd_manager *ddManager, array_t *outBdds, array_t *nextBdds, array_t *outputArray, array_t *tranFunArray); 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); /**AutomaticEnd***************************************************************/ /*---------------------------------------------------------------------------*/ /* Definition of exported functions */ /*---------------------------------------------------------------------------*/ /*---------------------------------------------------------------------------*/ /* Definition of internal functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [This function performs the complete task of STG restructuring and logic implementation.] Description [The STG restructuring process proceeds as follows: First a state equivalence relation E(x,y) is derived from the current STG of the finite state machine. If the parameter nonReachEquiv is set E(x,y) is used to extend the set of reachable states R(x) to include those states equivalent to R(x) but unreachable. This sometimes provides extra flexibility when choosing an edge. To perform the restructuring transformation, edges are first added (clearly driven by E(x,y)) to the original STG and then undesirable edges are removed, in such a way that the functional behavior of the machine is not affected. We say that the original STG is transformed into an augmented STG. The steady state probabilities of the STG are computed using Markovian analysis. The edges of the augmented STG are then labeled by a cost function which depends on the absolute transition probability and hamming distance between the ends of the edge. After the appropriate heuristic is applied, the new (restructured) STG is then translated in to a multi-level boolean network. heuristic takes on four options: ham: Hamming distance based heuristic is used, fanin: Fanin oriented heuristic, faninout: Fanin-Fanout oriented heuristic, cproj: C-Projection. For more information please refer to "A symbolic algorithm for low power sequential synthesis," ISLPED 97. equivClasses prints the number of equivalent classes in the STG. inputProb is optional. If not specified, equiprobabale primary inputs are assumed. Else, the table contains the pair, (PI_name,prob), where prob is the probability of the PI signal being 1. synthInfo specifies synthesis specific options. For more information look at synth.h] The BDD variable order at the end of the algorithm is dumped into orderFileName. SideEffects [Network partition and FSM data structure are hooked to the network if necessary. They are however, cleared at the end of this procedure.] SeeAlso [Synth_InitializeInfo] ******************************************************************************/ int RestrCommandRestructureFsm( Fsm_Fsm_t *fsm, RestructureHeuristic heuristic, char *orderFileName, boolean equivClasses, boolean nonReachEquiv, boolean eqvMethod, st_table *inputProb, Synth_InfoData_t *synthInfo) { graph_t *partition; Ntk_Network_t *network1; bdd_manager *ddManager; array_t *outputArray, *tranFunArray; array_t *outBdds, *nextBdds; array_t *tranRelationPair; array_t *newStateVars; st_table *careTable; int i; int nVars, nPi; int noRestruct = 0; boolean status; bdd_node *Lambda, *productTranRel, *prunedTR, *initialTR; bdd_node *equivRel; bdd_node *stateProbs; bdd_node *finalTR = NIL(bdd_node); bdd_node **xVars,**yVars,**uVars,**vVars; bdd_node **piVars; bdd_node *ddTemp, *reachable, *initBdd; bdd_node *newInit; mdd_t *reachStates, *mddTemp; mdd_t *careMdd; FILE *outFile; network1 = Fsm_FsmReadNetwork(fsm); ddManager = (bdd_manager *)Ntk_NetworkReadMddManager(network1); /* Get the bdd_node for primary, present and next state variables.*/ piVars = RestrBddNodeArrayFromIdArray(ddManager, Fsm_FsmReadInputVars(fsm)); xVars = RestrBddNodeArrayFromIdArray(ddManager, Fsm_FsmReadPresentStateVars(fsm)); yVars = RestrBddNodeArrayFromIdArray(ddManager, Fsm_FsmReadNextStateVars(fsm)); /* Create new state variables for duplicate machine. */ newStateVars = RestrCreateNewStateVars(network1, ddManager,xVars,yVars); uVars = RestrBddNodeArrayFromIdArray(ddManager, array_fetch(array_t *, newStateVars, 0)); vVars = RestrBddNodeArrayFromIdArray(ddManager, array_fetch(array_t *, newStateVars, 1)); /* Free memory: Delete the id array for new state variables.*/ array_free(array_fetch(array_t *,newStateVars,0)); array_free(array_fetch(array_t *,newStateVars,1)); array_free(newStateVars); /* outputArray is the list of primary outputs. It is my responsibility to free it later. Both outputArray and tranFunArray are char * arrays. Get the BDDs for output functions and transition functions. Duplicate functions are returned.*/ /* tranFunArray should not be freed */ outputArray = RestrGetOutputArray(network1); tranFunArray = Fsm_FsmReadNextStateFunctionNames(fsm); outBdds = GetBddArrayFromNameArray(fsm,outputArray); nextBdds = GetBddArrayFromNameArray(fsm,tranFunArray); nVars = array_n(Fsm_FsmReadNextStateVars(fsm)); nPi = array_n(Fsm_FsmReadInputVars(fsm)); /* Compute Lambda = AND (out1 xnor out1$NTK2) and Transition relation. out1$NTK2 is the corresponding primary output (of output1) in the duplicate machine.*/ if (restrVerbose) { fprintf(vis_stdout,"** restr info: Computing product output ... "); } Lambda = RestrCreateProductOutput(ddManager,outBdds,xVars, uVars, nVars); if (restrVerbose) { fprintf(vis_stdout,"Done.\n"); } if (restrVerbose) { fprintf(vis_stdout,"** restr info: Computing TR of product machine ... "); } /* Compute the transition relation for both the single FSM and the product machine. tranRelationPair[0] is the TR of single FSM and tranRelationPair[1] is the TR of product machine. TR(x,w,y) = \prod_{i=0}^{i=n-1} (y_i \equiv f_i(w,x)) productTR(x,u,w,y,v) = TR(x,w,y) * TR(u,w,v) */ tranRelationPair = RestrComputeTRWithIds(ddManager,nextBdds,xVars, yVars, uVars,vVars,nVars); if (restrVerbose) { fprintf(vis_stdout,"Done.\n"); } productTranRel = array_fetch(bdd_node *,tranRelationPair,1); /* Compute the state equivalence relation for the FSM */ /* The support of equivRel is xVars and uVars. */ if (restrVerbose) { fprintf(vis_stdout,"** restr info: Computing the equivalence relation ... "); } if (eqvMethod) { equivRel = RestrComputeEquivRelationUsingCofactors(ddManager,Lambda, productTranRel, xVars, yVars, uVars, vVars, piVars, nVars, nPi, restrVerbose); bdd_recursive_deref(ddManager,Lambda); } else { equivRel = RestrGetEquivRelation(ddManager,Lambda,productTranRel, xVars,yVars,uVars,vVars, piVars,nVars,nPi,restrVerbose); bdd_recursive_deref(ddManager,Lambda); } if (restrVerbose) { fprintf(vis_stdout,"Done.\n"); } /* Delete the product transition relation, as we no longer need it. */ bdd_recursive_deref(ddManager,productTranRel); /* Compute the initial states */ mddTemp = Fsm_FsmComputeInitialStates(fsm); initBdd = bdd_extract_node_as_is(mddTemp); bdd_ref(initBdd); mdd_free(mddTemp); /* Compute the reachable states. */ reachStates = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000, Fsm_Rch_Default_c,0,0, NIL(array_t),FALSE, NIL(array_t)); reachable = bdd_extract_node_as_is(reachStates); bdd_ref(reachable); mdd_free(reachStates); /* Check to see if there are any usable equivalence classes */ if (bdd_count_minterm(ddManager,equivRel,2*nVars) == pow(2.0,nVars)) { fprintf(vis_stdout,"** restr info: Number of equivalence classes equals "); fprintf(vis_stdout,"number of possible states. \n"); fprintf(vis_stdout,"** restr info: Restructuring will not help.\n"); fprintf(vis_stdout,"** restr info: Proceeding with synthesis.\n"); bdd_recursive_deref(ddManager,equivRel); /* Do not perform restructuring */ noRestruct = 1; } /* Expand the reachable set R(x) to include those states which are equivalent to R(x) but unreachable. */ if(nonReachEquiv && !noRestruct) { ExpandReachableSet(ddManager,&reachable,equivRel,xVars,uVars,nVars); } if (noRestruct) { /* Only synthesize the network */ bdd_recursive_deref(ddManager,equivRel); bdd_recursive_deref(ddManager, array_fetch(bdd_node *,tranRelationPair,0)); array_free(tranRelationPair); } else { /* Constrain the original TR */ initialTR = array_fetch(bdd_node *, tranRelationPair, 0); /* bdd_ref(prunedTR = bdd_bdd_and(ddManager,initialTR,reachable)); */ bdd_ref(prunedTR = initialTR); bdd_recursive_deref(ddManager,initialTR); array_free(tranRelationPair); finalTR = PerformRestructure(ddManager,prunedTR,equivRel,reachable, initBdd,piVars,xVars,yVars,uVars, vVars,inputProb,nVars,nPi,heuristic, equivClasses,&outBdds,&newInit, &stateProbs); /* equivRel is dereferenced in the above procedure */ if (prunedTR == finalTR) { fprintf(vis_stdout,"** restr info: Restructuring produces no changes. \n"); fprintf(vis_stdout,"** restr info: Proceeding with synthesis. \n"); bdd_recursive_deref(ddManager,stateProbs); noRestruct = 1; } bdd_recursive_deref(ddManager,prunedTR); bdd_recursive_deref(ddManager,initBdd); /* reachable can be deleted after computing the new reachable states. Also need to perform markov analysis to find final bit change. */ initBdd = newInit; if (!noRestruct) { arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) { bdd_recursive_deref(ddManager,ddTemp); } array_free(nextBdds); nextBdds = ExtractTransitionFuns(ddManager,finalTR,yVars,nVars); } } /* Create a partition for the new view of the fsm/network */ if (!noRestruct) { partition = CreateNewPartition(network1,ddManager,outBdds,nextBdds, outputArray,tranFunArray); array_free(outBdds); array_free(nextBdds); /* Create the FSM and perform markov ananlysis */ /* finalTR, stateProbs and reachabale are deleted in CreateNewFsm */ fsm = CreateNewFsm(network1,partition,ddManager,finalTR,initBdd, reachable,stateProbs,xVars,yVars,piVars, inputProb,nVars,nPi); } else { /* Remove the outBdds, nextBdds */ arrayForEachItem(bdd_node *, outBdds, i, ddTemp) { bdd_recursive_deref(ddManager,ddTemp); } arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) { bdd_recursive_deref(ddManager,ddTemp); } array_free(outBdds); array_free(nextBdds); } /* First create the care table for next state and primary output functions. */ careMdd = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000, Fsm_Rch_Default_c,0,0, NIL(array_t),FALSE, NIL(array_t)); careTable = CreateCareTable(network1,careMdd); /* Synthesize the restructured FSM */ status = Synth_SynthesizeFsm(fsm,careTable,synthInfo,0); /* Clean up */ if (!noRestruct) { Ntk_NetworkFreeApplInfo(network1,RESTR_PART_NETWORK_APPL_KEY); Ntk_NetworkFreeApplInfo(network1,RESTR_FSM_NETWORK_APPL_KEY); } mdd_free(careMdd); st_free_table(careTable); /* Dump the current BDD variable order, for future use. */ if(orderFileName) { outFile = fopen(orderFileName,"w"); if(outFile) { int size = array_n(mdd_ret_mvar_list(ddManager)); int index; mvar_type var; for(i = 0; i < size;i++) { index = bdd_get_id_from_level(ddManager,i); var = mdd_get_var_by_id(ddManager,index); fprintf(outFile,"%s\n",var.name); } fclose(outFile); } else { fprintf(vis_stderr,"** restr error: Cannot open %s .\n",orderFileName); } } /* Clean up */ for(i = 0; i < nVars; i++) { bdd_recursive_deref(ddManager,xVars[i]); bdd_recursive_deref(ddManager,yVars[i]); bdd_recursive_deref(ddManager,uVars[i]); bdd_recursive_deref(ddManager,vVars[i]); } for(i = 0 ; i < nPi; i++) { bdd_recursive_deref(ddManager,piVars[i]); } FREE(xVars); FREE(yVars); FREE(uVars); FREE(vVars); FREE(piVars); array_free(outputArray); return (status); } /*---------------------------------------------------------------------------*/ /* Definition of static functions */ /*---------------------------------------------------------------------------*/ /**Function******************************************************************** Synopsis [Returns an array of Mvfs given node names.] SideEffects [None] SeeAlso [] ******************************************************************************/ static array_t * BuildFunctions( graph_t *partition, array_t *rootNames) { char *name; vertex_t *vertexPtr; Mvf_Function_t *mvf1; int i; array_t *result; result = array_alloc(Mvf_Function_t *,0); arrayForEachItem(char *,rootNames,i,name) { vertexPtr = Part_PartitionFindVertexByName(partition,name); mvf1 = Mvf_FunctionDuplicate(Part_VertexReadFunction(vertexPtr)); array_insert(Mvf_Function_t *,result,i,mvf1); } return result; } /**Function******************************************************************** Synopsis [Performs markovian analysis.] Description [Returns a pair of ADDs. The ADD for steady state probabilities is at index 0 and the one-step transition probability is returned in index 1. bddTr is the BDD of the transition relation representing the STG. init is an ADD of initial probability vector.] SideEffects [None] SeeAlso [] ******************************************************************************/ 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) { bdd_node *temp1, *temp, *q, *Correction; bdd_node **result, *tr; bdd_node **xAddVars, **yAddVars; bdd_node *initG, *NewG; bdd_node *inputCube,*xCube; bdd_node *newTr, *probMatrix; int iter = 0; int i; double max,relTol = 0.0001; /* Initialize variables */ result = ALLOC(bdd_node *, 2); xAddVars = ALLOC(bdd_node *, nVars); yAddVars = ALLOC(bdd_node *, nVars); for (i = 0; i < nVars; i++) { bdd_ref(xAddVars[i] = bdd_add_ith_var(mgr, bdd_node_read_index(x[i]))); bdd_ref(yAddVars[i] = bdd_add_ith_var(mgr, bdd_node_read_index(y[i]))); } bdd_ref(tr = bdd_bdd_to_add(mgr, bddTr)); /* Create the input cube for abstraction */ bdd_ref(temp1 = bdd_bdd_compute_cube(mgr, pi, NIL(int), nPi)); bdd_ref(inputCube = bdd_bdd_to_add(mgr, temp1)); bdd_recursive_deref(mgr, temp1); /* Compute the one-step transition probability matrix. */ if (inputProb) { bdd_ref(probMatrix = Mark_addInProb(mgr,tr,inputCube,inputProb)); bdd_recursive_deref(mgr,inputCube); bdd_recursive_deref(mgr,tr); } else { bdd_ref(Correction = bdd_add_const(mgr,(1.0/(double)(1 << nPi)))); bdd_ref(q = bdd_add_exist_abstract(mgr,tr,inputCube)); bdd_recursive_deref(mgr,inputCube); bdd_recursive_deref(mgr,tr); /* apply correction to the transition relation matrix and print it */ bdd_ref(probMatrix = bdd_add_apply(mgr, bdd_add_times, q, Correction)); bdd_recursive_deref(mgr,Correction); bdd_recursive_deref(mgr,q); } result[1] = probMatrix; /* Prepare the initial prob. vector. and the transition prob. matrix. */ initG = bdd_add_swap_variables(mgr,init,xAddVars,yAddVars,nVars); bdd_ref(initG); /* Put transition prob. matrix in appropriate form (transpose). */ newTr = bdd_add_swap_variables(mgr,probMatrix,xAddVars,yAddVars,nVars); bdd_ref(newTr); /* Calculate the x-cube for abstraction */ bdd_ref(xCube = bdd_add_compute_cube(mgr,xAddVars,NIL(int),nVars)); /* Loop until convergence */ do { iter++; bdd_ref(temp = bdd_add_matrix_multiply(mgr,newTr,initG,yAddVars,nVars)); bdd_ref(temp1 = bdd_add_exist_abstract(mgr,temp,xCube)); bdd_ref(NewG = bdd_add_apply(mgr,bdd_add_divide,temp,temp1)); bdd_recursive_deref(mgr,temp); bdd_recursive_deref(mgr,temp1); temp = NewG; bdd_ref(q = bdd_add_swap_variables(mgr,temp,xAddVars,yAddVars,nVars)); max = bdd_add_value(bdd_add_find_max(mgr,initG)); if(bdd_equal_sup_norm(mgr,q,initG,relTol*max,0)) { bdd_recursive_deref(mgr,initG); bdd_recursive_deref(mgr,q); bdd_recursive_deref(mgr,xCube); bdd_recursive_deref(mgr,newTr); bdd_ref(temp1 = bdd_add_apply(mgr,bdd_add_times,probMatrix,temp)); if (restrVerbose) { fprintf(vis_stdout,"** restr info: Average state bit change = %f\n", RestrAverageBitChange(mgr,temp1,x,y,nVars)); } bdd_recursive_deref(mgr,temp1); for(i = 0;i < nVars; i++) { bdd_recursive_deref(mgr,xAddVars[i]); bdd_recursive_deref(mgr,yAddVars[i]); } FREE(xAddVars); FREE(yAddVars); result[0] = temp; return result; } bdd_recursive_deref(mgr,initG); bdd_recursive_deref(mgr,temp); initG = q; } while (1); } /* end of AddPowerSolve */ /**Function******************************************************************** Synopsis [This routine performs the preprocessing steps of markovian analysis and the augmented STG computation. After the preprocessing steps the core restructuring steps are performed. Returns the BDD of the restructured STG.] SideEffects [outBdds, newInit are changed to reflect the restructured finite state machine. Steady state probabilities are returned in stateProbs] SeeAlso [] ******************************************************************************/ 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) { /* equivRel is a function of uVars and xVars */ /* prunedTR is a funciton of xVars, piVars and yVars */ bdd_node *possessedProbMatrix; bdd_node *possessedTR = NIL(bdd_node); bdd_node *addPTR; bdd_node *finalTR; bdd_node *ddTemp; bdd_node *localStateProbs = NIL(bdd_node); if(equivClasses) { CountEquivalentClasses(ddManager,equivRel,initBdd,xVars,uVars,nVars); } /* Change the support of equivRel */ bdd_ref(ddTemp = bdd_bdd_swap_variables(ddManager,equivRel,xVars,yVars, nVars)); bdd_recursive_deref(ddManager,equivRel); bdd_ref(equivRel = bdd_bdd_swap_variables(ddManager,ddTemp,uVars,vVars, nVars)); bdd_recursive_deref(ddManager, ddTemp); /* The support of possessedTR is xVars and yVars and inputs. * If there exists an edge between x and y, and y == v, then * the following function adds an edge between x and v. These new * edges are referred to as ghost edges. */ if (heuristic != RestrCProjection_c) { possessedTR = RestrComputeTrWithGhostEdges(ddManager, yVars, vVars, prunedTR, equivRel, nVars); } /* stateProbs will not be used in the case of CProj and hammingD methods. We can still compute the stateProbs to find the initial average bit change on the state lines. */ *stateProbs = DoMarkovPowerAnalysis(ddManager,prunedTR, initBdd,piVars,xVars, yVars,inputProb,nVars,nPi); if (!(heuristic == RestrCProjection_c || heuristic == RestrHammingD_c)) { bdd_node *temp, *cube; bdd_ref(cube = bdd_bdd_compute_cube(ddManager,piVars,NIL(int),nPi)); bdd_ref(temp = bdd_bdd_exist_abstract(ddManager,possessedTR,cube)); bdd_ref(addPTR = bdd_bdd_to_add(ddManager,temp)); bdd_recursive_deref(ddManager,temp); bdd_ref(temp = bdd_bdd_to_add(ddManager, possessedTR)); bdd_recursive_deref(ddManager, possessedTR); /* possessedProbMatrix is a weighted augmented STG where the weights are the transition probabilities */ if (inputProb) { bdd_ref(possessedProbMatrix = Mark_addInProb(ddManager,temp,cube, inputProb)); } else { /* Assume equi probable primary inputs */ bdd_node *q, *Correction; bdd_node *inputCube; bdd_ref(inputCube = bdd_bdd_to_add(ddManager,cube)); bdd_ref(Correction = bdd_add_const(ddManager, (1.0/(double)(1 << nPi)))); bdd_ref(q = bdd_add_exist_abstract(ddManager,temp,inputCube)); bdd_ref(possessedProbMatrix = bdd_add_apply(ddManager, bdd_add_times, q, Correction)); bdd_recursive_deref(ddManager,Correction); bdd_recursive_deref(ddManager,q); bdd_recursive_deref(ddManager,inputCube); } bdd_recursive_deref(ddManager,cube); bdd_recursive_deref(ddManager,temp); localStateProbs = *stateProbs; } switch(heuristic) { case RestrCProjection_c: finalTR = RestrMinimizeFsmByCProj(ddManager,equivRel, prunedTR,initBdd, xVars,yVars,uVars,vVars,piVars, nVars,nPi,outBdds,newInit); break; case RestrFanin_c: case RestrFaninFanout_c: ddTemp = bdd_read_background(ddManager); bdd_set_background(ddManager, bdd_read_plus_infinity(ddManager)); /* addPTR and possessedProbMatrix are deleted in the following * procedure. */ finalTR = RestrMinimizeFsmByFaninFanout(ddManager,equivRel, prunedTR, &addPTR,&possessedProbMatrix,initBdd, reachable,localStateProbs,piVars,xVars, yVars, uVars,vVars, nVars, nPi,heuristic,outBdds,newInit); /* Replace the original background value */ bdd_set_background(ddManager,ddTemp); break; case RestrHammingD_c: default : /* BALA, testing ... */ /* Remove the edges out of the initial state. */ { /* bdd_node *outEdges; */ /* bdd_ref(outEdges = bdd_bdd_and(ddManager,prunedTR,initBdd)); */ /* bdd_ref(adjustedTR = bdd_bdd_and(ddManager,prunedTR, */ /* bdd_not_bdd_node(outEdges))); */ /* finalTR = RestrSelectLeastHammingDStates(ddManager,adjustedTR, */ /* possessedTR,xVars, */ /* yVars,vVars,nVars,nPi); */ finalTR = RestrSelectLeastHammingDStates(ddManager,prunedTR, possessedTR,xVars, yVars,vVars,nVars,nPi); bdd_recursive_deref(ddManager,possessedTR); bdd_ref(*newInit = initBdd); break; } } bdd_recursive_deref(ddManager,equivRel); return finalTR; } /**Function******************************************************************** Synopsis [Returns a table of (rootNames,rootMvfs). The parameters outBdds and nextBdds aare arrays of bdd_node *. outputArray and tranFunArray are arrays of strings and are in one-to-one correspondence with outBdds and nextBdds.] SideEffects [None] SeeAlso [] ******************************************************************************/ static st_table * CreateNameToMvfTable( bdd_manager *ddManager, array_t *outBdds, array_t *nextBdds, array_t *outputArray, array_t *tranFunArray) { st_table *nameToMvf; bdd_node *ddTemp; int i; /* Initialize variables */ nameToMvf = st_init_table(strcmp, st_strhash); arrayForEachItem(bdd_node *, outBdds, i, ddTemp) { bdd_node *temp; mdd_t *regular, *complement; Mvf_Function_t *mvf; char *name; bdd_ref(temp = bdd_not_bdd_node(ddTemp)); regular = bdd_construct_bdd_t(ddManager,ddTemp); complement = bdd_construct_bdd_t(ddManager,temp); mvf = (Mvf_Function_t *)array_alloc(mdd_t *, 0); array_insert(mdd_t *, mvf, 0, complement); array_insert(mdd_t *, mvf, 1, regular); name = array_fetch(char *, outputArray, i); st_insert(nameToMvf,name,(char *)mvf); } arrayForEachItem(bdd_node *, nextBdds, i, ddTemp) { bdd_node *temp; mdd_t *regular, *complement; Mvf_Function_t *mvf; char *name; bdd_ref(temp = bdd_not_bdd_node(ddTemp)); regular = bdd_construct_bdd_t(ddManager,ddTemp); complement = bdd_construct_bdd_t(ddManager,temp); mvf = (Mvf_Function_t *)array_alloc(mdd_t *, 0); array_insert(mdd_t *, mvf, 0, complement); array_insert(mdd_t *, mvf, 1, regular); name = array_fetch(char *, tranFunArray, i); st_insert(nameToMvf,name,(char *)mvf); } return nameToMvf; } /**Function******************************************************************** Synopsis [Create a (name,mdd_t*) table.] SideEffects [None] SeeAlso [] ******************************************************************************/ static st_table * CreateCareTable( Ntk_Network_t *network, mdd_t *reachMdd) { lsGen gen; Ntk_Node_t *node; st_table *careTable; careTable = st_init_table(strcmp, st_strhash); Ntk_NetworkForEachPrimaryOutput(network, gen, node) { char *name; name = Ntk_NodeReadName(node); st_insert(careTable,name,(char *)reachMdd); } Ntk_NetworkForEachLatch(network,gen,node){ char *name; name = Ntk_NodeReadName(Ntk_LatchReadDataInput(node)); st_insert(careTable,name,(char *)reachMdd); } return careTable; } /**Function******************************************************************** Synopsis [Routine to free members of an st_table.] SideEffects [None] SeeAlso [] ******************************************************************************/ static enum st_retval StMvfFree( char *key, char *value, char *arg) { /* This will free the memory associated with the array also */ Mvf_FunctionFree((Mvf_Function_t *)value); return(ST_CONTINUE); } /* end of StMvfFree */ /**Function******************************************************************** Synopsis [Routine to count number of equivalence classes in a relation.] SideEffects [None] SeeAlso [] ******************************************************************************/ static void CountEquivalentClasses( bdd_manager *ddManager, bdd_node *equivRel, bdd_node *initBdd, bdd_node **xVars, bdd_node **uVars, int nVars) { bdd_node *resultXU,*uCube; bdd_node *oneInitState,*classes; oneInitState = bdd_bdd_pick_one_minterm(ddManager,initBdd,xVars,nVars); bdd_ref(oneInitState); bdd_ref(resultXU = bdd_bdd_cprojection(ddManager,equivRel,oneInitState)); bdd_recursive_deref(ddManager,oneInitState); #ifdef RESTR_DIAG { /* The following is valid only when equivRel is the equivalence relation on the complete set of states.*/ bdd_node *xCube,*tautology; bdd_node *one; one = bdd_read_one(ddManager); bdd_ref(xCube = bdd_bdd_compute_cube(ddManager,xVars,NIL(int),nVars)); bdd_ref(tautology = bdd_bdd_exist_abstract(ddManager,resultXU,xCube)); assert(tautology == one); bdd_recursive_deref(ddManager,tautology); bdd_recursive_deref(ddManager,xCube); } #endif #ifdef RESTR_DIAG { bdd_node *uCube,*zero,*classes; bdd_node *oneClass,*temp,*rep; int i; zero = bdd_not_bdd_node(bdd_read_one(ddManager)); /* Extract the classes */ bdd_ref(uCube = bdd_bdd_compute_cube(ddManager,uVars,NIL(int),nVars)); bdd_ref(classes = bdd_bdd_exist_abstract(ddManager,resultXU,uCube)); bdd_recursive_deref(ddManager,uCube); i = 0; (void) fprintf(vis_stdout,"\n** restr diag: EQUIVALENT CLASSES:\n"); while (classes != zero) { i++; bdd_ref(rep = bdd_bdd_pick_one_minterm(ddManager,classes, xVars,nVars)); (void) fprintf(vis_stdout,"** restr diag: Class %d\n",i); (void) fprintf(vis_stdout,"** restr diag: Class representative:\n"); RestrPrintBddNode(ddManager,rep); /* Extract the complete class now */ bdd_ref(temp = bdd_bdd_cofactor(ddManager,resultXU,rep)); bdd_ref(oneClass = bdd_bdd_swap_variables(ddManager,temp,uVars, xVars,nVars)); bdd_recursive_deref(ddManager,temp); (void) fprintf(vis_stdout,"** restr diag: Class members:\n"); RestrPrintBddNode(ddManager,oneClass); bdd_recursive_deref(ddManager,oneClass); /* Remove rep from classes */ bdd_ref(temp = bdd_bdd_and(ddManager,classes,bdd_not_bdd_node(rep))); bdd_recursive_deref(ddManager,rep); bdd_recursive_deref(ddManager,classes); classes = temp; } (void) fprintf(vis_stdout,"** restr diag: Number of classes = %d\n",i); } #endif /* Compute uCube and extract the u variables from resultXU */ bdd_ref(uCube = bdd_bdd_compute_cube(ddManager,uVars,NIL(int),nVars)); bdd_ref(classes = bdd_bdd_exist_abstract(ddManager,resultXU,uCube)); bdd_recursive_deref(ddManager,uCube); bdd_recursive_deref(ddManager,resultXU); fprintf(vis_stdout, "** restr info: Number of Equivalence Classes = %g\n", bdd_count_minterm(ddManager,classes,nVars)); bdd_recursive_deref(ddManager,classes); } /**Function******************************************************************** Synopsis [Convert an array of Mvf_Function_t * to an array of bdd_node *] SideEffects [None] SeeAlso [] ******************************************************************************/ static array_t * GetBddArrayFromMvfArray(array_t *mvfArray) { int i; array_t *bddArray; Mvf_Function_t *mvf; bddArray = array_alloc(bdd_node *,0); arrayForEachItem(Mvf_Function_t *, mvfArray,i,mvf) { mdd_t *mddTemp; bdd_node *ddNode; mddTemp = array_fetch(mdd_t *, mvf, 1); ddNode = bdd_extract_node_as_is(mddTemp); bdd_ref(ddNode); array_insert_last(bdd_node *, bddArray, ddNode); } return bddArray; } /**Function******************************************************************** Synopsis [Perform markovian analysis. The ADD for steady state probabilities of the STG is returned.] SideEffects [None] SeeAlso [] ******************************************************************************/ 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) { bdd_node **result, *stateProbs; bdd_node *init; bdd_ref(init = bdd_bdd_to_add(ddManager,initBdd)); if (restrVerbose) (void) fprintf(vis_stdout,"** restr info: Initial average state bit change:\n"); result = AddPowerSolve(ddManager,prunedTR,init,xVars,yVars, piVars,inputProb,nVars,nPi); bdd_recursive_deref(ddManager,result[1]); stateProbs = result[0]; bdd_recursive_deref(ddManager,init); FREE(result); return stateProbs; } /**Function******************************************************************** Synopsis [Given a relation R(X,Y) returns the array of functions y_i=f(X).] SideEffects [None] SeeAlso [] ******************************************************************************/ static array_t * ExtractTransitionFuns( bdd_manager *ddManager, bdd_node *finalTR, bdd_node **yVars, int nVars) { bdd_node *completeCube, *extractCube; bdd_node *fun, *tranFun; array_t *allTranFuns; int i; allTranFuns = array_alloc(bdd_node *,0); completeCube = bdd_bdd_compute_cube(ddManager,yVars,NIL(int),nVars); bdd_ref(completeCube); for(i = 0;i < nVars; i++) { extractCube = bdd_bdd_cofactor(ddManager,completeCube,yVars[i]); bdd_ref(extractCube); fun = bdd_bdd_exist_abstract(ddManager,finalTR,extractCube); bdd_ref(fun); bdd_recursive_deref(ddManager,extractCube); tranFun = bdd_bdd_cofactor(ddManager,fun,yVars[i]); bdd_ref(tranFun); #ifdef RESTR_DIAG { /* The following is to test if there are multiple edges out of a state with the same input label: in short to check if the relation is deterministic or not. */ bdd_node *yBar,*yNot,*inter; bdd_ref(yNot = bdd_not_bdd_node(yVars[i])); bdd_ref(yBar = bdd_bdd_cofactor(ddManager,fun,yNot)); bdd_recursive_deref(ddManager,yNot); bdd_ref(inter = bdd_bdd_and(ddManager,yBar,tranFun)); yNot = bdd_not_bdd_node(bdd_read_one(ddManager)); assert(inter == yNot); bdd_recursive_deref(ddManager,inter); bdd_recursive_deref(ddManager,yBar); } #endif bdd_recursive_deref(ddManager,fun); array_insert_last(bdd_node *,allTranFuns,tranFun); } bdd_recursive_deref(ddManager,completeCube); return allTranFuns; } /**Function******************************************************************** Synopsis [Returns an array of BDDs given the node names of a network.] SideEffects [None] SeeAlso [] ******************************************************************************/ static array_t * GetBddArrayFromNameArray( Fsm_Fsm_t *fsm, array_t *nameArray) { graph_t *partition; array_t *bdds,*mvfs; partition = Fsm_FsmReadPartition(fsm); mvfs = BuildFunctions(partition,nameArray); bdds = GetBddArrayFromMvfArray(mvfs); Mvf_FunctionArrayFree(mvfs); return bdds; } /**Function******************************************************************** Synopsis [Expand the reachable set R(x) to include those states which are equivalent to R(x) but potentially not reachable.] SideEffects [reachable is updated.] SeeAlso [] ******************************************************************************/ static void ExpandReachableSet( bdd_manager *ddManager, bdd_node **reachable, bdd_node *equivRel, bdd_node **xVars, bdd_node **uVars, int nVars) { bdd_node *xcube,*potUnReach,*extReach; bdd_node *temp1; bdd_ref(xcube = bdd_bdd_compute_cube(ddManager,xVars,NIL(int),nVars)); /* potUnReach = \exists_x (E(x,u) * R(x)) */ bdd_ref(potUnReach = bdd_bdd_and_abstract(ddManager,*reachable, equivRel,xcube)); bdd_recursive_deref(ddManager,xcube); /* temp1(x) = potUnReach(u) */ bdd_ref(temp1 = bdd_bdd_swap_variables(ddManager,potUnReach,uVars, xVars,nVars)); bdd_recursive_deref(ddManager,potUnReach); /* extReach(x) = R(x) + potUnReach(x) */ bdd_ref(extReach = bdd_bdd_or(ddManager,*reachable,temp1)); bdd_recursive_deref(ddManager,temp1); bdd_recursive_deref(ddManager,*reachable); *reachable = extReach; } /**Function******************************************************************** Synopsis [Create a partition for the new view of the fsm/network] SideEffects [The new view is attached to the network.] SeeAlso [CreateNewFsm] ******************************************************************************/ static graph_t * CreateNewPartition( Ntk_Network_t *network, bdd_manager *ddManager, array_t *outBdds, array_t *nextBdds, array_t *outputArray, array_t *tranFunArray) { st_table *nameToMvf; graph_t *partition; /* Create a table of next state and output Mvfs with their names as key to the table. This table is used to create a partition for the network. */ nameToMvf = CreateNameToMvfTable(ddManager,outBdds,nextBdds, outputArray,tranFunArray); /* Delete the old partition and old fsm as we dont need it any more */ if (restrCreatedPart) { Ntk_NetworkFreeApplInfo(network,RESTR_PART_NETWORK_APPL_KEY); restrCreatedPart = 0; } if (restrCreatedFsm) { Ntk_NetworkFreeApplInfo(network,RESTR_FSM_NETWORK_APPL_KEY); restrCreatedFsm = 0; } /* Create a new partition from the new root functions */ partition = Part_NetworkCreatePartitionFromMvfs(network,nameToMvf); Ntk_NetworkAddApplInfo(network, RESTR_PART_NETWORK_APPL_KEY, (Ntk_ApplInfoFreeFn) Part_PartitionFreeCallback, (void *) partition); st_foreach(nameToMvf,StMvfFree,NIL(char)); st_free_table(nameToMvf); return partition; } /**Function******************************************************************** Synopsis [Create the FSM data structure for the restructured STG and perform markov analysis to estimate the final state average bit change.] SideEffects [reachable,initBdd,stateProbs,finalTR are dereferenced in this function.] SeeAlso [CreateNewPatition] ******************************************************************************/ 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) { Fsm_Fsm_t *fsm; mdd_t *reachStates; mdd_t *mddTemp; bdd_node *ddTemp; bdd_node **markovResult; /* Create a new Fsm for the restructured network. */ fsm = Fsm_FsmCreateFromNetworkWithPartition(network, Part_PartitionDuplicate(partition)); assert(fsm != NIL(Fsm_Fsm_t)); Ntk_NetworkAddApplInfo(network, RESTR_FSM_NETWORK_APPL_KEY, (Ntk_ApplInfoFreeFn) Fsm_FsmFreeCallback, (void *) fsm); /* We need to update the initial states as the Fsm_FsmCreateFromNetworkWithPartition will pick up old initial state from the network. Fsm_FsmSetInitialStates deletes old inital states. */ mddTemp = bdd_construct_bdd_t(ddManager,initBdd); Fsm_FsmSetInitialStates(fsm,mddTemp); /* Compute the new reachable states */ reachStates = Fsm_FsmComputeReachableStates(fsm,0,0,0,0,0,0,1000, Fsm_Rch_Default_c,0,0, NIL(array_t),FALSE, NIL(array_t)); bdd_recursive_deref(ddManager,reachable); reachable = bdd_extract_node_as_is(reachStates); bdd_ref(reachable); mdd_free(reachStates); /* Constrain the transition relation */ bdd_ref(ddTemp = bdd_bdd_constrain(ddManager,finalTR,reachable)); bdd_recursive_deref(ddManager,finalTR); finalTR = ddTemp; /* Use the state probs. of the original STG as the initial guess to compute the state probs. of the restructured STG. */ if (restrVerbose) (void) fprintf(vis_stdout,"** restr info: Final average state bit change:\n"); markovResult = AddPowerSolve(ddManager, finalTR, stateProbs, xVars, yVars,piVars,inputProb,nVars,nPi); bdd_recursive_deref(ddManager, markovResult[0]); bdd_recursive_deref(ddManager, markovResult[1]); FREE(markovResult); bdd_recursive_deref(ddManager,stateProbs); bdd_recursive_deref(ddManager,finalTR); bdd_recursive_deref(ddManager,reachable); return fsm; }