#include "restrInt.h"

Include dependency graph for restrCProj.c:

Functions
bdd_node *	RestrMinimizeFsmByCProj (bdd_manager ddManager, bdd_node equivRel, bdd_node originalTR, bdd_node initBdd, bdd_node xVars, bdd_node yVars, bdd_node uVars, bdd_node vVars, bdd_node piVars, int nVars, int nPi, array_t outBdds, bdd_node **newInit)

Function Documentation

bdd_node* RestrMinimizeFsmByCProj	(	bdd_manager *	ddManager,
		bdd_node *	equivRel,
		bdd_node *	originalTR,
		bdd_node *	initBdd,
		bdd_node **	xVars,
		bdd_node **	yVars,
		bdd_node **	uVars,
		bdd_node **	vVars,
		bdd_node **	piVars,
		int	nVars,
		int	nPi,
		array_t **	outBdds,
		bdd_node **	newInit
	)

CFile***********************************************************************

FileName [restrCProj.c]

PackageName [restr]

Synopsis [This file contains functions that implement the STG restructuring based on compatible projection.]

Description [This file contains functions that implement the STG restructuring based on compatible projection. Please refer to "A symbolic algorithm for low power sequential synthesis," ISLPED 97, for more details.]

SeeAlso [restrHammingD.c restrFaninout.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.]AutomaticStart AutomaticEnd Function********************************************************************

Synopsis [This routine implements the STG restructuring based on compatible projection.]

Description [This routine implements the STG restructuring based on compatible projection. The BDD for the monolithic transition relation of the restructured STG is returned.

Please refer to "A Symbolic Algorithm for Low-Power Sequential Synthesis," ISLPED 97. for more details.

equivRel is the BDD of the equivalnece relation of the FSM, originalTR is the monolithic transition relation, initBdd is the BDD for the initial state, piVars are the BDD variables for primary inputs, nVars are the numbers of state variables and nPi are the number of primary inputs. outBdd is an array of BDDs for the primary outputs of the sequential circuit.]

SideEffects [outBdds and newInit are changed to reflect the restructured STG.]

SeeAlso [RestrSelectLeastHammingDStates RestrMinimizeFsmByFaninFanout]

Definition at line 95 of file restrCProj.c.

{
  bdd_node *resultYV, *temp, *temp1, *temp2;
  bdd_node *result, *resultXU;
  bdd_node *xCube, *yCube;
  bdd_node *oneInitState;
  array_t *newOutBdds;
  int i;

  /* Select one state from the set of initial states. This is redundant in case
     of circuits described in blif format.*/
  oneInitState = bdd_bdd_pick_one_minterm(ddManager,initBdd,xVars,nVars);
  bdd_ref(oneInitState);

  temp = bdd_bdd_swap_variables(ddManager,oneInitState,xVars,vVars,nVars);
  bdd_ref(temp);
  bdd_recursive_deref(ddManager,oneInitState);

  /* Select a representative for each equivalence class. The vVars encode the
   * representative for each class. resultYV has yVars and vVars in its
   * support. equivRel is a function of yVars and vVars.
   */
  resultYV = bdd_bdd_cprojection(ddManager, equivRel, temp);
  bdd_ref(resultYV);
  bdd_recursive_deref(ddManager,temp);

  temp = bdd_bdd_swap_variables(ddManager,resultYV,yVars,xVars,nVars);
  bdd_ref(temp);
  resultXU = bdd_bdd_swap_variables(ddManager,temp,vVars,uVars,nVars);
  bdd_ref(resultXU);
  bdd_recursive_deref(ddManager, temp);

  /* Change the initBdd accordingly
   * initBdd^{new} = [\exists_x (initBdd(x) * result(x,u))]_{u=x}
   */
  xCube = bdd_bdd_compute_cube(ddManager,xVars,NIL(int),nVars);
  bdd_ref(xCube);
  bdd_ref(temp1 = bdd_bdd_and_abstract(ddManager,initBdd,resultXU,
                                       xCube));
  bdd_ref(*newInit = bdd_bdd_swap_variables(ddManager,temp1,uVars,
                                            xVars,nVars));
  bdd_recursive_deref(ddManager,temp1);

  /* compute the new TR.
   * TR^{new}(x,w,y) = 
   *    [\exists_{xy}(result(x,u) * TR(x,w,y) * result(y,v))]_{u=x,v=y}
   * result is the new restructured/minimized TR.
   */
  bdd_ref(yCube = bdd_bdd_compute_cube(ddManager,yVars,NIL(int),nVars));
  bdd_ref(temp = bdd_bdd_and_abstract(ddManager,resultYV,originalTR,yCube));
  bdd_recursive_deref(ddManager,resultYV);
  bdd_recursive_deref(ddManager,yCube);

  bdd_ref(result = bdd_bdd_and_abstract(ddManager,temp,resultXU,xCube));
  bdd_recursive_deref(ddManager,temp);

  bdd_ref(temp = bdd_bdd_swap_variables(ddManager,result,uVars,
                                        xVars,nVars));
  bdd_recursive_deref(ddManager,result);
  bdd_ref(result = bdd_bdd_swap_variables(ddManager,temp,vVars,
                                          yVars,nVars));
  bdd_recursive_deref(ddManager,temp);

  /* Change the outputs accordingly
   * lambda^{new}_i(x,w) = [\exists_x (lambda_i(x,w) * result(x,u))]_{u=x}
   *
   * lambda_i(x,w) is the ith primary output.
   */
  newOutBdds = array_alloc(bdd_node *,0);
  arrayForEachItem(bdd_node *,*outBdds,i,temp) {
    temp1 = bdd_bdd_and_abstract(ddManager,temp,resultXU,xCube);
    bdd_ref(temp1);
    temp2 = bdd_bdd_swap_variables(ddManager,temp1,uVars,xVars,nVars);
    bdd_ref(temp2);
    bdd_recursive_deref(ddManager,temp1);
    array_insert_last(bdd_node *,newOutBdds,temp2);
  }
  bdd_recursive_deref(ddManager, xCube);
  bdd_recursive_deref(ddManager,resultXU);

#ifdef RESTR_DIAG
  {
    int flag1,flag2;

    (void) fprintf(vis_stdout,"Old transition relation ...\n");
    flag1 = RestrTestIsDeterministic(ddManager,originalTR,initBdd,
                                     xVars,yVars,nVars);
    (void) fprintf(vis_stdout,"New transition relation ...\n");
    flag2 = RestrTestIsDeterministic(ddManager,result,*newInit,
                                     xVars,yVars,nVars);
  }
#endif
  
  /* Delete the old array */
  arrayForEachItem(bdd_node *,*outBdds,i,temp) {
    bdd_recursive_deref(ddManager,temp);
  }
  array_free(*outBdds);
  *outBdds = newOutBdds;
  
  return result;

}

Here is the call graph for this function:

Here is the caller graph for this function:

src/restr/restrCProj.c File Reference

Functions

Function Documentation