source: vis_dev/vis-2.3/src/spfd/spfdSpfd.c @ 23

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

vis2.3
File size: 16.2 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [spfdSpfd.c]
4
5  PackageName [spfd]
6
7  Synopsis [Routines to perform SPFD computation.]
8
9  Description [Routines to perform SPFD computation.]
10
11  SeeAlso     [spfdProg.c]
12
13  Author      [Balakrishna Kumthekar]
14
15  Copyright [This file was created at the University of Colorado at Boulder.
16  The University of Colorado at Boulder makes no warranty about the suitability
17  of this software for any purpose.  It is presented on an AS IS basis.]
18
19******************************************************************************/
20
21#include "spfdInt.h"
22
23/*---------------------------------------------------------------------------*/
24/* Constant declarations                                                     */
25/*---------------------------------------------------------------------------*/
26
27
28/*---------------------------------------------------------------------------*/
29/* Type declarations                                                         */
30/*---------------------------------------------------------------------------*/
31
32
33/*---------------------------------------------------------------------------*/
34/* Structure declarations                                                    */
35/*---------------------------------------------------------------------------*/
36
37
38/*---------------------------------------------------------------------------*/
39/* Variable declarations                                                     */
40/*---------------------------------------------------------------------------*/
41
42
43/*---------------------------------------------------------------------------*/
44/* Macro declarations                                                        */
45/*---------------------------------------------------------------------------*/
46
47
48/**AutomaticStart*************************************************************/
49
50/*---------------------------------------------------------------------------*/
51/* Static function prototypes                                                */
52/*---------------------------------------------------------------------------*/
53
54static bdd_node * ComputeAuxRel(SpfdApplData_t *applData, bdd_node *faninRel, Ntk_Node_t *from, int piSwap);
55
56/**AutomaticEnd***************************************************************/
57
58
59/*---------------------------------------------------------------------------*/
60/* Definition of exported functions                                          */
61/*---------------------------------------------------------------------------*/
62
63
64/*---------------------------------------------------------------------------*/
65/* Definition of internal functions                                          */
66/*---------------------------------------------------------------------------*/
67
68/**Function********************************************************************
69
70  Synopsis [Given two functions represented by bdd1 and bdd0, compute
71  its SPFD.]
72
73  SideEffects [None]
74
75******************************************************************************/
76bdd_node *
77SpfdNodeComputeSpfdFromOnAndOffSet(
78  SpfdApplData_t *applData,
79  Ntk_Node_t *regNode,
80  bdd_node *bdd1,
81  bdd_node *bdd0)
82{
83  bdd_manager *ddManager = applData->ddManager;
84  int numFanin = Ntk_NodeReadNumFanins(regNode);
85  bdd_node **yVars,**yAuxVars;
86  bdd_node *ddTemp,*rel,*spfd;
87  Ntk_Node_t *fanin;
88  int j,clean;
89
90  /* If bdd1 and bdd0 are not specified, replace bdd1 and bdd0 by the
91     node's local ON-set and OFF-set respectively */
92  clean = 0;
93  if (bdd1 == NIL(bdd_node) ||
94      bdd0 == NIL(bdd_node)) {
95    Ntk_Network_t *network;
96    network = Ntk_NodeReadNetwork(regNode);
97    bdd_ref(bdd1 = SpfdNodeReadLocalBdd(network,regNode));
98    bdd_ref(bdd0 = bdd_not_bdd_node(bdd1));
99    /* Delete bdd1 and bdd0 at the end.*/
100    clean = 1;
101  }
102 
103  /* Array of variables for swapping */
104  numFanin = Ntk_NodeReadNumFanins(regNode);
105  yVars = ALLOC(bdd_node *,numFanin);
106  yAuxVars = ALLOC(bdd_node *,numFanin);
107  Ntk_NodeForEachFanin(regNode,j,fanin) {
108    yVars[j] = bdd_bdd_ith_var(ddManager,Ntk_NodeReadMddId(fanin));
109    yAuxVars[j] = bdd_bdd_ith_var(ddManager,
110                                  SpfdNodeReadAuxId(applData,fanin));
111  }
112
113  /* spfd is bdd1(y) * bdd0(y') + bdd1(y') * bdd0(y) */
114  bdd_ref(ddTemp = bdd_bdd_swap_variables(ddManager,bdd0,
115                                          yVars,yAuxVars,numFanin));
116  bdd_ref(rel = bdd_bdd_and(ddManager,bdd1,ddTemp));
117  bdd_recursive_deref(ddManager,ddTemp);
118     
119  bdd_ref(ddTemp = bdd_bdd_swap_variables(ddManager,rel,
120                                          yVars,yAuxVars,numFanin));
121  bdd_ref(spfd = bdd_bdd_or(ddManager,rel,ddTemp));
122  bdd_recursive_deref(ddManager,rel);
123  bdd_recursive_deref(ddManager,ddTemp);
124  FREE(yVars);
125  FREE(yAuxVars);
126
127  if (clean) {
128    bdd_recursive_deref(ddManager,bdd1);
129    bdd_recursive_deref(ddManager,bdd0);
130  }
131  return spfd;
132} /* End of SpfdNodeComputeSpfdFromOnAndOffSet */
133
134
135/**Function********************************************************************
136
137  Synopsis [Compute the SPFD of 'from', as the union of SPFDs of its
138  fanout wires.]
139
140  SideEffects [None]
141
142******************************************************************************/
143bdd_node *
144SpfdNodeComputeSpfdFromFanouts(
145  SpfdApplData_t *applData,
146  Ntk_Node_t *from)
147{
148  bdd_manager *ddManager = applData->ddManager;
149  st_table *currBddReq;
150  st_table *wireTable,*wiresRemoved;
151  array_t *ordArray;
152  bdd_node *result,*var,*varAux,*ddTemp,*ddTemp2;
153  bdd_node *wireSpfd,*toSpfd,*fromSpfd,*xCube;
154  bdd_node *step1,*faninRel,*faninRelAux,*inter,*final;
155  bdd_node **firstCompose,**secondCompose;
156  bdd_node *logicZero;
157  Ntk_Node_t *fanin,*to;
158  int index,i,j;
159  int size,piSwap;
160
161
162  if (Ntk_NodeReadNumFanouts(from) < 1) {
163    (void) fprintf(vis_stdout,
164                   "** spfd error: Node %s has no fanouts.\n",
165                   Ntk_NodeReadName(from));
166    return NIL(bdd_node);
167  }
168  currBddReq = applData->currBddReq;
169  xCube = applData->currXCube;
170  logicZero = bdd_read_logic_zero(ddManager);
171
172  /* Compute the characteristic function of the fanin relation:
173   faninRel = \prod y_i == f_i(X) */
174  faninRel = SpfdComputeNodeArrayRelation(applData,currBddReq,NIL(array_t),
175                                          Ntk_NodeReadFanins(from),
176                                          TRUE,&piSwap);
177 
178  /* Convert faninRel(y,pi) to faninRel(\hat{y},pi) */
179  faninRelAux = ComputeAuxRel(applData,faninRel,from,piSwap);
180   
181  /* Compute SPFD wire by wire according to the order specified for
182     each fanout node. */
183  wireTable = applData->currWireTable;
184  wiresRemoved = applData->wiresRemoved;
185  bdd_ref(fromSpfd = logicZero);
186  Ntk_NodeForEachFanout(from,j,to) {
187
188    bdd_ref(result = bdd_read_one(ddManager));
189    ordArray = SpfdNodeReadFaninOrder(applData,to);
190    arrayForEachItem(Ntk_Node_t *,ordArray,i,fanin) {
191      var = bdd_bdd_ith_var(ddManager,Ntk_NodeReadMddId(fanin));
192      index = SpfdNodeReadAuxId(applData,fanin);
193      varAux = bdd_bdd_ith_var(ddManager,index);
194       
195      if (fanin != from) {
196        /* XNOR */
197        bdd_ref(ddTemp = bdd_bdd_xnor(ddManager,var,varAux));
198      } else {
199        /* XOR */
200        bdd_ref(ddTemp = bdd_bdd_xor(ddManager,var,varAux));
201      }
202      bdd_ref(ddTemp2 = bdd_bdd_and(ddManager,result,ddTemp));
203      bdd_recursive_deref(ddManager,result);
204      bdd_recursive_deref(ddManager,ddTemp);
205      result = ddTemp2;
206       
207      if (fanin == from)
208        break;
209    }
210     
211    /* Compute AND of result and the SPFD of 'to'. */
212    toSpfd = SpfdNodeReadSpfd(applData,to);
213    if (toSpfd == NIL(bdd_node)) {
214      (void) fprintf(vis_stderr,
215                     "** spfd error: Spfd expected but not found.\n");
216      (void) fprintf(vis_stderr, "To node:\n");
217      Ntk_NodePrint(vis_stderr, to, TRUE, TRUE);
218      (void) fprintf(vis_stderr, "From node:\n");
219      Ntk_NodePrint(vis_stderr, from, TRUE, TRUE);
220      fflush(vis_stderr);
221      assert(0);
222    }
223    bdd_ref(wireSpfd = bdd_bdd_and(ddManager,toSpfd,result));
224    bdd_recursive_deref(ddManager,result);
225
226    /* Convert wireSpfd from fanout space to fanin space */
227    /* Prepare the vectors for composition */
228    size = bdd_num_vars(ddManager);
229    firstCompose = ALLOC(bdd_node *,size);
230    secondCompose = ALLOC(bdd_node *,size);
231    for (i = 0; i < size; i++) {
232      firstCompose[i] = bdd_bdd_ith_var(ddManager,i);
233      secondCompose[i] = bdd_bdd_ith_var(ddManager,i);
234    }
235     
236    arrayForEachItem(Ntk_Node_t *,ordArray,i,fanin) {
237      int id,auxId;
238       
239      id = Ntk_NodeReadMddId(fanin);
240      auxId = SpfdNodeReadAuxId(applData,fanin);
241      st_lookup(currBddReq,(char *)fanin,(char **)&firstCompose[id]);
242      secondCompose[auxId] = firstCompose[id];
243    }
244     
245    /* Perform the steps of compose --> existential abstraction twice */
246    bdd_ref(step1 = bdd_bdd_vector_compose(ddManager,wireSpfd,firstCompose));
247    bdd_recursive_deref(ddManager,wireSpfd);
248    FREE(firstCompose);
249    bdd_ref(inter = bdd_bdd_and_abstract(ddManager,faninRel,step1,xCube));
250    bdd_recursive_deref(ddManager,step1);
251   
252    /* The second of compose --> existential abstraction steps */
253    bdd_ref(ddTemp = bdd_bdd_vector_compose(ddManager,inter,secondCompose));
254    bdd_recursive_deref(ddManager,inter);
255    FREE(secondCompose);
256    bdd_ref(final = bdd_bdd_and_abstract(ddManager,faninRelAux,
257                                         ddTemp,xCube));
258    bdd_recursive_deref(ddManager,ddTemp);
259
260    /* Now 'final' is in the fanin space */
261    if (final == logicZero) {
262      st_table *sinkTable;
263      Ntk_Node_t *tempNode;
264      boolean add;
265
266      /* Check if this wire has already been removed. If yes, skip */
267      add = TRUE;
268      if (st_lookup(wiresRemoved,(char *)from,&sinkTable) &&
269          st_lookup(sinkTable,(char *)to,&tempNode)) {
270        add = FALSE;
271      }
272
273      if (add) {
274        if (spfdVerbose > 2)
275          (void) fprintf(vis_stdout,
276                         "** spfd info: wire %s --> %s has empty spfd.\n",
277                         Ntk_NodeReadName(from),Ntk_NodeReadName(to));
278       
279        /* Add to the wireTable */
280        if (st_lookup(wireTable,(char *)from,&sinkTable)) {
281          st_insert(sinkTable,(char *)to,(char *)to);
282        } else {
283          sinkTable = st_init_table(st_ptrcmp,st_ptrhash);
284          st_insert(sinkTable,(char *)to,(char *)to);
285          st_insert(wireTable,(char *)from,(char *)sinkTable);
286        }
287      }
288    }
289   
290    bdd_ref(ddTemp = bdd_bdd_or(ddManager,fromSpfd,final));
291    bdd_recursive_deref(ddManager,fromSpfd);
292    bdd_recursive_deref(ddManager,final);
293   
294    fromSpfd = ddTemp;
295  }
296  bdd_recursive_deref(ddManager,faninRel);
297  bdd_recursive_deref(ddManager,faninRelAux);
298   
299  /* Swap variables for fromSpfd if necessary */
300  if (piSwap) { /* If we have used alternate PI ids */
301    ddTemp = SpfdSwapPiAndAltPi(applData,fromSpfd);
302    bdd_recursive_deref(ddManager,fromSpfd);
303    fromSpfd = ddTemp;
304  }
305 
306  return fromSpfd;
307 
308} /* End of SpfdNodeComputeSpfdFromFanouts */
309
310
311/**Function********************************************************************
312
313  Synopsis [Compute the strongly connected components in the SPFD of
314  regNode. 'tempVars' are extra variables required during this
315  computation. For detailed description please refer to:
316
317  Subarnarekha Sinha and Robert K. Brayton. Implementation and use of
318  SPFDs in optimizaing Boolean networks. In International Conference
319  on Computer Aided Design, 1998.]
320
321  SideEffects [None]
322
323******************************************************************************/
324st_table *
325SpfdNodeComputeSCCs(
326  SpfdApplData_t *applData,
327  Ntk_Node_t *regNode,
328  bdd_node **tempVars)
329{
330  bdd_manager *ddManager = applData->ddManager;
331  st_table *inUseVars = applData->currInUseVars;
332  Ntk_Node_t *fanin;
333  st_table *SCC;
334  bdd_node *spfd,*spfd2,*auxCube;
335  bdd_node *ddTemp1,*ddTemp2,*logicZero,*faninCube;
336  bdd_node *Ny,*E1y,*E0y;
337  bdd_node *from,*To,*new_,*reached;
338  bdd_node **faninVars,**auxVars;
339  int i,numFanin,varsAllocated;
340
341  numFanin = Ntk_NodeReadNumFanins(regNode);
342  SCC = st_init_table(st_ptrcmp,st_ptrhash);
343  spfd = SpfdNodeReadSpfd(applData,regNode);
344  logicZero = bdd_read_logic_zero(ddManager);
345
346  if (spfd == logicZero)
347    return SCC;
348 
349  varsAllocated = 0;
350  /* Allocate variables if necessary */
351  if (tempVars == NIL(bdd_node *)) {
352    tempVars = SpfdAllocateTemporaryVariables(ddManager,inUseVars,numFanin);
353    varsAllocated = 1;
354  }
355 
356  faninVars = ALLOC(bdd_node *,numFanin);
357  auxVars = ALLOC(bdd_node *,numFanin);
358  Ntk_NodeForEachFanin(regNode,i,fanin) {
359    faninVars[i] = bdd_bdd_ith_var(ddManager,Ntk_NodeReadMddId(fanin));
360    auxVars[i] = bdd_bdd_ith_var(ddManager,
361                                 SpfdNodeReadAuxId(applData,fanin));
362  }
363
364  bdd_ref(auxCube = bdd_bdd_compute_cube(ddManager,auxVars,
365                                         NIL(int),numFanin));
366  /* Compute spfd2 = \exists_{\hat{y}} spfd(y,\hat{y}) *
367     spfd(\hat{y},\tilde{y}) */
368  bdd_ref(ddTemp1 = bdd_bdd_swap_variables(ddManager,spfd,faninVars,
369                                           auxVars,numFanin));
370  bdd_ref(ddTemp2 = bdd_bdd_swap_variables(ddManager,ddTemp1,faninVars,
371                                           tempVars,numFanin));
372  bdd_recursive_deref(ddManager,ddTemp1);
373  bdd_ref(spfd2 = bdd_bdd_and_abstract(ddManager,spfd,ddTemp2,auxCube));
374  bdd_recursive_deref(ddManager,ddTemp2);
375
376  /* SCC computation */
377  bdd_ref(faninCube = bdd_bdd_compute_cube(ddManager,faninVars,
378                                           NIL(int),numFanin));
379  /* Compute N(y) = \exists_{\hat{y}} spfd(y,\hat{y}) */
380  bdd_ref(Ny = bdd_bdd_exist_abstract(ddManager,spfd,auxCube));
381  bdd_recursive_deref(ddManager,auxCube);
382
383  while (Ny != logicZero) {
384    /* To compute E1(y) perform the fixpoint image computation */
385    bdd_ref(from = bdd_bdd_pick_one_minterm(ddManager,Ny,faninVars,numFanin));
386    bdd_ref(reached = from);
387    do {
388      bdd_ref(ddTemp1 = bdd_bdd_and_abstract(ddManager,spfd2,from,faninCube));
389      bdd_recursive_deref(ddManager,from);
390      bdd_ref(To = bdd_bdd_swap_variables(ddManager,ddTemp1,tempVars,
391                                          faninVars,numFanin));
392      bdd_recursive_deref(ddManager,ddTemp1);
393      bdd_ref(new_ = bdd_bdd_and(ddManager,To,bdd_not_bdd_node(reached)));
394      bdd_recursive_deref(ddManager,To);
395      bdd_ref(ddTemp1 = bdd_bdd_or(ddManager,reached,new_));
396      bdd_recursive_deref(ddManager,reached);
397      reached = ddTemp1;
398      from = new_;
399    } while (new_ != logicZero);
400
401    E1y = reached;
402   
403    /* E_0(y) = \exists_{\hat{y}} spfd(y,\hat{y}) * E_1(y) */
404    bdd_ref(ddTemp1 = bdd_bdd_and_abstract(ddManager,spfd,E1y,faninCube));
405    bdd_ref(E0y = bdd_bdd_swap_variables(ddManager,ddTemp1,auxVars,
406                                         faninVars,numFanin));
407    bdd_recursive_deref(ddManager,ddTemp1);
408   
409    /* Update Ny: Ny = Ny * (E1y + E0y)' */
410    bdd_ref(ddTemp1 = bdd_bdd_or(ddManager,E1y,E0y));
411    bdd_ref(ddTemp2 = bdd_bdd_and(ddManager,Ny,bdd_not_bdd_node(ddTemp1)));
412    bdd_recursive_deref(ddManager,ddTemp1);
413    bdd_recursive_deref(ddManager,Ny);
414    Ny = ddTemp2;
415
416    /* Store E1y and E0y in an st_table */
417    st_insert(SCC,(char *)E1y,(char *)E0y);
418  }
419  bdd_recursive_deref(ddManager,faninCube);
420  bdd_recursive_deref(ddManager,Ny);
421 
422  FREE(auxVars);
423  FREE(faninVars);
424
425  if (varsAllocated) {
426    long id;
427    for (i = 0; i < numFanin; i++) {
428      id = (long) bdd_node_read_index(tempVars[i]);
429      st_delete(inUseVars,&id,NIL(char *));
430    }
431    FREE(tempVars);
432  }
433 
434  return SCC;
435
436} /* End of SpfdNodeComputeSCCs */
437
438/*---------------------------------------------------------------------------*/
439/* Definition of static functions                                            */
440/*---------------------------------------------------------------------------*/
441
442/**Function********************************************************************
443
444  Synopsis [Convert faninRel which is interms of Y, to Y', the
445  auxillary variables.]
446
447  SideEffects [None]
448
449******************************************************************************/
450static bdd_node *
451ComputeAuxRel(
452  SpfdApplData_t *applData,
453  bdd_node *faninRel,
454  Ntk_Node_t *from,
455  int piSwap)
456{
457  bdd_node **fromVars,**toVars;
458  int numFi = Ntk_NodeReadNumFanins(from);
459  int k,altId;
460  Ntk_Node_t *fanin;
461  bdd_node *faninRelAux;
462  st_table *piAltVars;
463  bdd_manager *ddManager = applData->ddManager;
464 
465  piAltVars = applData->currPiAltVars;
466 
467  /* Collect variables for swapping. */
468  fromVars = ALLOC(bdd_node *,numFi);
469  toVars = ALLOC(bdd_node *,numFi);
470  Ntk_NodeForEachFanin(from,k,fanin) {
471    int id = Ntk_NodeReadMddId(fanin);
472    if (piSwap && st_lookup(piAltVars,(char *)(long)id,&altId)) {
473      fromVars[k] = bdd_bdd_ith_var(ddManager,altId);
474    } else {
475      fromVars[k] = bdd_bdd_ith_var(ddManager,id);
476    }
477    toVars[k] = bdd_bdd_ith_var(ddManager,SpfdNodeReadAuxId(applData,fanin));
478  }
479  bdd_ref(faninRelAux = bdd_bdd_swap_variables(ddManager,faninRel,fromVars,
480                                               toVars,numFi));
481  FREE(fromVars);
482  FREE(toVars);
483
484  return faninRelAux;
485 
486} /* End of ComputeAuxRel */
Note: See TracBrowser for help on using the repository browser.