source: vis_dev/vis-2.3/src/restr/restrCProj.c @ 43

Last change on this file since 43 was 14, checked in by cecile, 13 years ago

vis2.3
File size: 8.0 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [restrCProj.c]
4
5  PackageName [restr]
6
7  Synopsis [This file contains functions that implement the STG restructuring
8  based on compatible projection.]
9
10  Description [This file contains functions that implement the STG
11  restructuring based on compatible projection.  Please refer to "A symbolic
12  algorithm for low power sequential synthesis," ISLPED 97, for more details.]
13
14  SeeAlso     [restrHammingD.c restrFaninout.c]
15
16  Author      [Balakrishna Kumthekar]
17
18  Copyright   [This file was created at the University of Colorado at
19  Boulder.  The University of Colorado at Boulder makes no warranty
20  about the suitability of this software for any purpose.  It is
21  presented on an AS IS basis.]
22
23******************************************************************************/
24
25#include "restrInt.h"
26
27/*---------------------------------------------------------------------------*/
28/* Constant declarations                                                     */
29/*---------------------------------------------------------------------------*/
30
31
32/*---------------------------------------------------------------------------*/
33/* Type declarations                                                         */
34/*---------------------------------------------------------------------------*/
35
36
37/*---------------------------------------------------------------------------*/
38/* Structure declarations                                                    */
39/*---------------------------------------------------------------------------*/
40
41/*---------------------------------------------------------------------------*/
42/* Variable declarations                                                     */
43/*---------------------------------------------------------------------------*/
44
45
46/*---------------------------------------------------------------------------*/
47/* Macro declarations                                                        */
48/*---------------------------------------------------------------------------*/
49
50
51/**AutomaticStart*************************************************************/
52
53/*---------------------------------------------------------------------------*/
54/* Static function prototypes                                                */
55/*---------------------------------------------------------------------------*/
56
57
58/**AutomaticEnd***************************************************************/
59
60
61/*---------------------------------------------------------------------------*/
62/* Definition of exported functions                                          */
63/*---------------------------------------------------------------------------*/
64
65/*---------------------------------------------------------------------------*/
66/* Definition of internal functions                                          */
67/*---------------------------------------------------------------------------*/
68
69/**Function********************************************************************
70
71  Synopsis [This routine implements the STG restructuring based on compatible
72  projection.]
73
74  Description [This routine implements the STG restructuring based on
75  compatible projection. The BDD for the monolithic transition relation of the
76  restructured STG is returned.
77
78  Please refer to "A Symbolic Algorithm for Low-Power Sequential Synthesis,"
79  ISLPED 97. for more details.
80
81  <tt>equivRel</tt> is the BDD of the equivalnece relation of the FSM,
82  <tt>originalTR</tt> is the monolithic transition relation, <tt>initBdd</tt>
83  is the BDD for the initial state, <tt>piVars</tt> are the BDD variables for
84  primary inputs, <tt>nVars are the numbers of state variables and <tt>nPi</tt>
85  are the number of primary inputs. <tt>outBdd</tt> is an array of BDDs for the
86  primary outputs of the sequential circuit.]
87
88  SideEffects [<tt>outBdds</tt> and <tt>newInit</tt> are changed to reflect the
89  restructured STG.]
90
91  SeeAlso     [RestrSelectLeastHammingDStates RestrMinimizeFsmByFaninFanout]
92
93******************************************************************************/
94bdd_node *
95RestrMinimizeFsmByCProj(
96  bdd_manager   *ddManager,
97  bdd_node      *equivRel,
98  bdd_node      *originalTR,
99  bdd_node      *initBdd,
100  bdd_node      **xVars,
101  bdd_node      **yVars,
102  bdd_node      **uVars,
103  bdd_node      **vVars,
104  bdd_node      **piVars,
105  int           nVars,
106  int           nPi,
107  array_t       **outBdds,
108  bdd_node      **newInit)
109
110{
111  bdd_node *resultYV, *temp, *temp1, *temp2;
112  bdd_node *result, *resultXU;
113  bdd_node *xCube, *yCube;
114  bdd_node *oneInitState;
115  array_t *newOutBdds;
116  int i;
117
118  /* Select one state from the set of initial states. This is redundant in case
119     of circuits described in blif format.*/
120  oneInitState = bdd_bdd_pick_one_minterm(ddManager,initBdd,xVars,nVars);
121  bdd_ref(oneInitState);
122
123  temp = bdd_bdd_swap_variables(ddManager,oneInitState,xVars,vVars,nVars);
124  bdd_ref(temp);
125  bdd_recursive_deref(ddManager,oneInitState);
126
127  /* Select a representative for each equivalence class. The vVars encode the
128   * representative for each class. resultYV has yVars and vVars in its
129   * support. equivRel is a function of yVars and vVars.
130   */
131  resultYV = bdd_bdd_cprojection(ddManager, equivRel, temp);
132  bdd_ref(resultYV);
133  bdd_recursive_deref(ddManager,temp);
134
135  temp = bdd_bdd_swap_variables(ddManager,resultYV,yVars,xVars,nVars);
136  bdd_ref(temp);
137  resultXU = bdd_bdd_swap_variables(ddManager,temp,vVars,uVars,nVars);
138  bdd_ref(resultXU);
139  bdd_recursive_deref(ddManager, temp);
140
141  /* Change the initBdd accordingly
142   * initBdd^{new} = [\exists_x (initBdd(x) * result(x,u))]_{u=x}
143   */
144  xCube = bdd_bdd_compute_cube(ddManager,xVars,NIL(int),nVars);
145  bdd_ref(xCube);
146  bdd_ref(temp1 = bdd_bdd_and_abstract(ddManager,initBdd,resultXU,
147                                       xCube));
148  bdd_ref(*newInit = bdd_bdd_swap_variables(ddManager,temp1,uVars,
149                                            xVars,nVars));
150  bdd_recursive_deref(ddManager,temp1);
151
152  /* compute the new TR.
153   * TR^{new}(x,w,y) =
154   *    [\exists_{xy}(result(x,u) * TR(x,w,y) * result(y,v))]_{u=x,v=y}
155   * result is the new restructured/minimized TR.
156   */
157  bdd_ref(yCube = bdd_bdd_compute_cube(ddManager,yVars,NIL(int),nVars));
158  bdd_ref(temp = bdd_bdd_and_abstract(ddManager,resultYV,originalTR,yCube));
159  bdd_recursive_deref(ddManager,resultYV);
160  bdd_recursive_deref(ddManager,yCube);
161
162  bdd_ref(result = bdd_bdd_and_abstract(ddManager,temp,resultXU,xCube));
163  bdd_recursive_deref(ddManager,temp);
164
165  bdd_ref(temp = bdd_bdd_swap_variables(ddManager,result,uVars,
166                                        xVars,nVars));
167  bdd_recursive_deref(ddManager,result);
168  bdd_ref(result = bdd_bdd_swap_variables(ddManager,temp,vVars,
169                                          yVars,nVars));
170  bdd_recursive_deref(ddManager,temp);
171
172  /* Change the outputs accordingly
173   * lambda^{new}_i(x,w) = [\exists_x (lambda_i(x,w) * result(x,u))]_{u=x}
174   *
175   * lambda_i(x,w) is the ith primary output.
176   */
177  newOutBdds = array_alloc(bdd_node *,0);
178  arrayForEachItem(bdd_node *,*outBdds,i,temp) {
179    temp1 = bdd_bdd_and_abstract(ddManager,temp,resultXU,xCube);
180    bdd_ref(temp1);
181    temp2 = bdd_bdd_swap_variables(ddManager,temp1,uVars,xVars,nVars);
182    bdd_ref(temp2);
183    bdd_recursive_deref(ddManager,temp1);
184    array_insert_last(bdd_node *,newOutBdds,temp2);
185  }
186  bdd_recursive_deref(ddManager, xCube);
187  bdd_recursive_deref(ddManager,resultXU);
188
189#ifdef RESTR_DIAG
190  {
191    int flag1,flag2;
192
193    (void) fprintf(vis_stdout,"Old transition relation ...\n");
194    flag1 = RestrTestIsDeterministic(ddManager,originalTR,initBdd,
195                                     xVars,yVars,nVars);
196    (void) fprintf(vis_stdout,"New transition relation ...\n");
197    flag2 = RestrTestIsDeterministic(ddManager,result,*newInit,
198                                     xVars,yVars,nVars);
199  }
200#endif
201 
202  /* Delete the old array */
203  arrayForEachItem(bdd_node *,*outBdds,i,temp) {
204    bdd_recursive_deref(ddManager,temp);
205  }
206  array_free(*outBdds);
207  *outBdds = newOutBdds;
208 
209  return result;
210
211}
212
213/*---------------------------------------------------------------------------*/
214/* Definition of static functions                                            */
215/*---------------------------------------------------------------------------*/
Note: See TracBrowser for help on using the repository browser.