#include "restrInt.h"
Include dependency graph for restrRestructure.c:
Go to the source code of this file.
Functions | |
| 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) |
| int | RestrCommandRestructureFsm (Fsm_Fsm_t *fsm, RestructureHeuristic heuristic, char *orderFileName, boolean equivClasses, boolean nonReachEquiv, boolean eqvMethod, st_table *inputProb, Synth_InfoData_t *synthInfo) |
Variables | |
| int | restrCreatedPart |
| int | restrCreatedFsm |
| boolean | restrVerbose |
Function Documentation
| 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] |
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 []
Definition at line 472 of file restrRestructure.c.
{
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 */
Here is the call graph for this function:
Here is the caller graph for this function:
| static array_t * BuildFunctions | ( | graph_t * | partition, |
| array_t * | rootNames | ||
| ) | [static] |
AutomaticStart
Function********************************************************************
Synopsis [Returns an array of Mvfs given node names.]
SideEffects [None]
SeeAlso []
Definition at line 437 of file restrRestructure.c.
{
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;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void CountEquivalentClasses | ( | bdd_manager * | ddManager, |
| bdd_node * | equivRel, | ||
| bdd_node * | initBdd, | ||
| bdd_node ** | xVars, | ||
| bdd_node ** | uVars, | ||
| int | nVars | ||
| ) | [static] |
Function********************************************************************
Synopsis [Routine to count number of equivalence classes in a relation.]
SideEffects [None]
SeeAlso []
Definition at line 875 of file restrRestructure.c.
{
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);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static st_table * CreateCareTable | ( | Ntk_Network_t * | network, |
| mdd_t * | reachMdd | ||
| ) | [static] |
Function********************************************************************
Synopsis [Create a (name,mdd_t*) table.]
SideEffects [None]
SeeAlso []
Definition at line 820 of file restrRestructure.c.
{
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;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static st_table * CreateNameToMvfTable | ( | bdd_manager * | ddManager, |
| array_t * | outBdds, | ||
| array_t * | nextBdds, | ||
| array_t * | outputArray, | ||
| array_t * | tranFunArray | ||
| ) | [static] |
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 []
Definition at line 754 of file restrRestructure.c.
{
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;
}
Here is the caller graph for this function:
| 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 | ||
| ) | [static] |
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]
Definition at line 1214 of file restrRestructure.c.
{
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;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static graph_t * CreateNewPartition | ( | Ntk_Network_t * | network, |
| bdd_manager * | ddManager, | ||
| array_t * | outBdds, | ||
| array_t * | nextBdds, | ||
| array_t * | outputArray, | ||
| array_t * | tranFunArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Create a partition for the new view of the fsm/network]
SideEffects [The new view is attached to the network.]
SeeAlso [CreateNewFsm]
Definition at line 1166 of file restrRestructure.c.
{
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;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| 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] |
Function********************************************************************
Synopsis [Perform markovian analysis. The ADD for steady state probabilities of the STG is returned.]
SideEffects [None]
SeeAlso []
Definition at line 1003 of file restrRestructure.c.
{
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;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static void ExpandReachableSet | ( | bdd_manager * | ddManager, |
| bdd_node ** | reachable, | ||
| bdd_node * | equivRel, | ||
| bdd_node ** | xVars, | ||
| bdd_node ** | uVars, | ||
| int | nVars | ||
| ) | [static] |
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 []
Definition at line 1129 of file restrRestructure.c.
{
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;
}
Here is the caller graph for this function:
| static array_t * ExtractTransitionFuns | ( | bdd_manager * | ddManager, |
| bdd_node * | finalTR, | ||
| bdd_node ** | yVars, | ||
| int | nVars | ||
| ) | [static] |
Function********************************************************************
Synopsis [Given a relation R(X,Y) returns the array of functions y_i=f(X).]
SideEffects [None]
SeeAlso []
Definition at line 1042 of file restrRestructure.c.
{
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;
}
Here is the caller graph for this function:
| static array_t * GetBddArrayFromMvfArray | ( | array_t * | mvfArray | ) | [static] |
Function********************************************************************
Synopsis [Convert an array of Mvf_Function_t * to an array of bdd_node *]
SideEffects [None]
SeeAlso []
Definition at line 971 of file restrRestructure.c.
{
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;
}
Here is the caller graph for this function:
| static array_t * GetBddArrayFromNameArray | ( | Fsm_Fsm_t * | fsm, |
| array_t * | nameArray | ||
| ) | [static] |
Function********************************************************************
Synopsis [Returns an array of BDDs given the node names of a network.]
SideEffects [None]
SeeAlso []
Definition at line 1103 of file restrRestructure.c.
{
graph_t *partition;
array_t *bdds,*mvfs;
partition = Fsm_FsmReadPartition(fsm);
mvfs = BuildFunctions(partition,nameArray);
bdds = GetBddArrayFromMvfArray(mvfs);
Mvf_FunctionArrayFree(mvfs);
return bdds;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| 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] |
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 []
Definition at line 592 of file restrRestructure.c.
{
/* 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;
}
Here is the call graph for this function:
Here is the caller graph for this function:
| int RestrCommandRestructureFsm | ( | Fsm_Fsm_t * | fsm, |
| RestructureHeuristic | heuristic, | ||
| char * | orderFileName, | ||
| boolean | equivClasses, | ||
| boolean | nonReachEquiv, | ||
| boolean | eqvMethod, | ||
| st_table * | inputProb, | ||
| Synth_InfoData_t * | synthInfo | ||
| ) |
AutomaticEnd 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]
Definition at line 135 of file restrRestructure.c.
{
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);
}
Here is the call graph for this function:
Here is the caller graph for this function:
| static enum st_retval StMvfFree | ( | char * | key, |
| char * | value, | ||
| char * | arg | ||
| ) | [static] |
Function********************************************************************
Synopsis [Routine to free members of an st_table.]
SideEffects [None]
SeeAlso []
Definition at line 852 of file restrRestructure.c.
{
/* This will free the memory associated with the array also */
Mvf_FunctionFree((Mvf_Function_t *)value);
return(ST_CONTINUE);
} /* end of StMvfFree */
Here is the call graph for this function:
Here is the caller graph for this function:
Variable Documentation
| int restrCreatedFsm |
Definition at line 40 of file restrCmd.c.
| int restrCreatedPart |
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 <kumtheka@colorado.edu>]
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.]
Definition at line 39 of file restrCmd.c.
| boolean restrVerbose |
Definition at line 41 of file restrCmd.c.
