source: vis_dev/vis-2.3/src/maig/maigUtil.c @ 54

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

vis2.3
File size: 14.5 KB
Line 
1/**CFile***********************************************************************
2
3  FileName    [maigUtil.c]
4
5  PackageName [maig]
6
7  Synopsis    [Utilities for Multi-Valued AndInv graph]
8
9  Author      [Mohammad Awedh]
10
11  Copyright [ This file was created at the University of Colorado at
12  Boulder.  The University of Colorado at Boulder makes no warranty
13  about the suitability of this software for any purpose.  It is
14  presented on an AS IS basis.]
15
16******************************************************************************/
17
18#include "maigInt.h"
19#include "mvfaig.h"
20#include "mvfaigInt.h"
21#include "ctlspInt.h"
22#include "ctlsp.h"
23#include "ntk.h"
24
25static char rcsid[] UNUSED = "$Id: maigUtil.c,v 1.20 2005/05/18 18:11:59 jinh Exp $";
26
27/*---------------------------------------------------------------------------*/
28/* Constant declarations                                                     */
29/*---------------------------------------------------------------------------*/
30
31/*---------------------------------------------------------------------------*/
32/* Stucture declarations                                                     */
33/*---------------------------------------------------------------------------*/
34
35
36/*---------------------------------------------------------------------------*/
37/* Type declarations                                                         */
38/*---------------------------------------------------------------------------*/
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
57static int NoOfBitEncode(int n);
58static bAigEdge_t Case(mAig_Manager_t * mgr, array_t * encodeList, int index);
59static int mCommandmAigTest(void);
60
61/**AutomaticEnd***************************************************************/
62
63 
64/*---------------------------------------------------------------------------*/
65/* Definition of exported functions                                          */
66/*---------------------------------------------------------------------------*/
67
68/**Function********************************************************************
69
70  Synopsis    [Initialize maig package]
71
72  SideEffects [none]
73
74  SeeAlso     [mAig_End]
75
76******************************************************************************/
77void
78mAig_Init(void)
79{
80  Cmd_CommandAdd("_mAig_test",
81                 (int(*)(Hrc_Manager_t **, int, char **))  mCommandmAigTest,
82                 0);
83}
84
85
86/**Function********************************************************************
87
88  Synopsis    [End maig package]
89
90  SideEffects []
91
92  SeeAlso     [mAig_Init]
93
94******************************************************************************/
95void
96mAig_End(void)
97{
98}
99
100/**Function********************************************************************
101
102  Synopsis    []
103
104  Description []
105
106  SideEffects []
107
108******************************************************************************/
109array_t *
110mAig_ArrayDuplicate(
111  array_t *mAigArray)
112{
113  int      i;
114  int      length = array_n(mAigArray);
115  array_t *result = array_alloc(mAigEdge_t *, length);
116  for (i = 0; i < length; i++) {
117    mAigEdge_t *tempMAig = array_fetch(mAigEdge_t *, mAigArray, i);
118    array_insert(mAigEdge_t *, result, i, tempMAig);
119  }
120
121  return (result);
122}
123
124/**Function********************************************************************
125
126  Synopsis    [Creates a new mAig manager]
127
128  SideEffects []
129
130  SeeAlso     []
131
132******************************************************************************/
133mAig_Manager_t *
134mAig_initAig(void)
135{
136  return bAig_initAig(5000); /* Initial number of nodes in the bAIG greaph*/
137}
138
139/**Function********************************************************************
140
141  Synopsis    [Quit mAig manager]
142
143  SideEffects []
144
145  SeeAlso     []
146
147******************************************************************************/
148void
149mAig_quit(
150  mAig_Manager_t *manager)
151{
152 bAig_quit(manager);
153}
154
155/**Function********************************************************************
156
157  Synopsis    [Build the binary representation of multi-valued variable that
158  equal to constant.]
159
160  Description [It builds the binary And/Inverter graph of a multi-valued
161  variable of value equal to constant.]
162 
163  SideEffects []
164
165  SeeAlso     [Case]
166
167******************************************************************************/
168mAigEdge_t
169mAig_EquC(
170  mAig_Manager_t * mgr,
171  mAigEdge_t     mVarId,
172  int            constant)
173{
174  array_t *mVarList    = mAigReadMulVarList(mgr);
175  mAigMvar_t mVar      = array_fetch(mAigMvar_t, mVarList, mVarId);
176  array_t  *encodeList = array_alloc(bAigEdge_t, 0);
177  int i;
178  bAigEdge_t bVarId;
179  for(i=0; i< mVar.values; i++){
180    if( i == constant){
181      array_insert_last(bAigEdge_t, encodeList, mAig_One);     
182    }
183    else{
184      array_insert_last(bAigEdge_t, encodeList, mAig_Zero);
185    } /* if */
186  } /* for */
187  bVarId = Case(mgr, encodeList, mVar.bVars + mVar.encodeLength-1); /* Build the bAig grpah */
188  array_free(encodeList);
189  return bVarId; 
190}
191
192/**Function********************************************************************
193
194  Synopsis [Creates Multi-valued Variable]
195
196  Description [Creates Multi-valued variable of name 'name' and value 'value',
197               and returns the Id for this variable. It creates the binary
198               variable that are used to rpresent this multi-valued variable.]
199
200  SideEffects []
201
202  SeeAlso     [bAig_CreateVarNode]
203
204******************************************************************************/
205mAigEdge_t
206mAig_CreateVar(
207  mAig_Manager_t * mgr,
208  char           * name,
209  int            value)
210{
211  array_t *mVarList    = mAigReadMulVarList(mgr);
212  array_t *bVarList    = mAigReadBinVarList(mgr);
213
214  int         noBits      = NoOfBitEncode(value);
215  int         i, startBvar, startMvar;
216  /*
217  char        bName[100];
218  */
219  char        *bName = ALLOC(char, strlen(name) + 10);
220  mAigMvar_t  mVar;   
221  mAigBvar_t  bVar; 
222
223  assert(mVarList != NIL(array_t));
224  assert(bVarList != NIL(array_t));
225
226  startBvar = array_n(bVarList);
227  startMvar = array_n(mVarList);
228
229  /* Create Multi-valued variable */
230  mVar.mVarId       = startMvar;
231  mVar.bVars        = startBvar;
232  mVar.values       = value;
233  mVar.name         = name;
234  mVar.encodeLength = noBits;
235 
236  array_insert_last(mAigMvar_t, mVarList, mVar);
237
238  /* Create binary Variables of the Multi-valued variable */
239  for (i=0; i<noBits; i++){
240    sprintf(bName, "%s_%d", name, i);
241    bVar.node = bAig_CreateVarNode(mgr,  util_strsav(bName));
242
243    bVar.mVarId = mVar.mVarId; 
244    array_insert_last(mAigBvar_t, bVarList, bVar);
245  } /* for */
246  return (mVar.mVarId);
247}
248
249/**Function********************************************************************
250
251  Synopsis [Creates Multi-valued Variable from multi-valued logic]
252
253  Description [Creates Multi-valued variable of name 'name' and value 'value',
254               and returns the Id for this variable. It creates the binary
255               variable that are used to rpresent this multi-valued variable.]
256
257  SideEffects []
258
259  SeeAlso     [bAig_CreateVarNode]
260
261******************************************************************************/
262mAigEdge_t
263mAig_CreateVarFromAig(
264  mAig_Manager_t * mgr,
265  char           * name,
266  array_t        *mvfAig)
267{
268  array_t *mVarList    = mAigReadMulVarList(mgr);
269  array_t *bVarList    = mAigReadBinVarList(mgr);
270
271  int noBits, value, index1;
272  int startBvar, startMvar;
273  int i, j, divider, orFlag;
274  bAigEdge_t v, resultOn, resultOff;
275  mAigMvar_t  mVar;   
276  mAigBvar_t  bVar; 
277
278  assert(mVarList != NIL(array_t));
279  assert(bVarList != NIL(array_t));
280
281  value = array_n(mvfAig);
282  noBits = NoOfBitEncode(value);
283  startBvar = array_n(bVarList);
284  startMvar = array_n(mVarList);
285
286  /* Create Multi-valued variable */
287  mVar.mVarId       = startMvar;
288  mVar.bVars        = startBvar;
289  mVar.values       = value;
290  mVar.name         = name;
291  mVar.encodeLength = noBits;
292 
293  array_insert_last(mAigMvar_t, mVarList, mVar);
294
295  for(i=0, index1=mVar.bVars; i<mVar.encodeLength; i++) {
296
297    resultOn = bAig_Zero;
298    resultOff = bAig_Zero;
299/*    divider = (int)pow(2.0, (double)(i)); */
300    divider = (int)pow(2.0, (double)(mVar.encodeLength-i-1));
301    orFlag = 1;
302    for(j=0; j<value; j++) {
303      if(j%divider == 0)orFlag = !orFlag;
304      v = array_fetch(bAigEdge_t, mvfAig, j);
305      if(orFlag){
306        resultOn = bAig_Or(mgr, resultOn, v);
307      }
308      else {
309        resultOff = bAig_Or(mgr, resultOff, v);
310      }
311    }
312    bVar.node = resultOn;
313    bVar.mVarId = mVar.mVarId; 
314    array_insert_last(mAigBvar_t, bVarList, bVar);
315    index1++;
316  }
317  return (mVar.mVarId);
318}
319
320/*---------------------------------------------------------------------------*/
321/* Definition of internal functions                                          */
322/*---------------------------------------------------------------------------*/
323
324/**Function********************************************************************
325
326  Synopsis    [Return the Binary Variables List]
327
328  Description []
329
330  SideEffects []
331
332  SeeAlso     []
333
334******************************************************************************/
335array_t * 
336mAigReadBinVarList(
337    mAig_Manager_t * manager)
338{
339  return (manager->bVarList);
340}
341
342/**Function********************************************************************
343
344  Synopsis    [Retunrs the Multi-Valued variables List]
345
346  Description []
347
348  SideEffects []
349
350  SeeAlso     []
351
352******************************************************************************/
353array_t *
354mAigReadMulVarList(
355    mAig_Manager_t * manager)
356{
357  return (manager->mVarList);
358}
359
360/*---------------------------------------------------------------------------*/
361/* Definition of static functions                                            */
362/*---------------------------------------------------------------------------*/
363
364
365/**Function********************************************************************
366
367  Synopsis    [Returns no. of Bit encoding needed for n]
368
369  Description []
370
371  SideEffects []
372
373  SeeAlso     []
374
375******************************************************************************/
376static int
377NoOfBitEncode(
378   int n)
379{
380    int i = 0;
381    int j = 1;
382
383    if (n < 2) return 1; /* Takes care of mv.values <= 1 */
384
385    while (j < n) {
386        j = j * 2;
387        i++;
388    }
389    return i;
390}
391
392
393/**Function********************************************************************
394
395  Synopsis    [Returns the binary And/Inverter graph of a multi-valued
396               variable.]
397
398  Description [The encodingList array has bAig_Zero in all its entries except
399  the enrty at which the multi-valued variable equal to the required value.
400  At which the value is bAig_One.]
401
402  SideEffects []
403
404  SeeAlso     [mAig_EquC]
405
406******************************************************************************/
407static bAigEdge_t
408Case(
409  mAig_Manager_t * mgr,
410  array_t *       encodeList,
411  int             index)
412{
413  array_t       *bVarList    = mAigReadBinVarList(mgr);
414  mAigBvar_t    bVar; 
415  array_t       *newEncodeList;
416  int           encodeLen = array_n(encodeList); 
417  bAigEdge_t    andResult1, andResult2, orResult, result;
418  bAigEdge_t    node1, node2;
419  int i; 
420  int count=0;
421
422  if (encodeLen == 1){
423    return array_fetch(bAigEdge_t, encodeList, 0);
424  }
425  bVar   = array_fetch(mAigBvar_t, bVarList, index); 
426  newEncodeList =  array_alloc(bAigEdge_t, 0);
427
428  for (i=0; i< (encodeLen/2); i++){
429     node1 = array_fetch(bAigEdge_t, encodeList, count++);
430     node2 = array_fetch(bAigEdge_t, encodeList, count++);
431 
432     /*  performs ITE operator */
433     andResult1 = bAig_And(mgr, bVar.node,           node2);
434     andResult2 = bAig_And(mgr, bAig_Not(bVar.node), node1);
435     orResult   = bAig_Or (mgr, andResult1,          andResult2);
436   
437     array_insert_last(bAigEdge_t, newEncodeList, orResult);
438   
439  }
440  if (encodeLen %2){ /* Odd */
441     node1 = array_fetch(bAigEdge_t, encodeList, count);
442     array_insert_last(bAigEdge_t, newEncodeList, node1);
443  }
444  result = Case(mgr, newEncodeList, index-1);
445  array_free(newEncodeList);
446  return result;
447}
448
449
450/**Function********************************************************************
451
452  Synopsis    []
453
454  CommandName [_mAig_test]
455
456  SideEffects []
457
458******************************************************************************/
459static int
460mCommandmAigTest(void)
461{
462  array_t *mVarList;
463  array_t *bVarList;
464
465  MvfAig_Function_t * aa;
466  MvfAig_Function_t * bb;
467  MvfAig_Function_t * cc;
468
469  mAigMvar_t mVar;   
470  mAigBvar_t bVar; 
471
472  int i;
473
474  mAig_Manager_t *manager = mAig_initAig();
475  mAigEdge_t      node1, node2, node3, node4, node5, node6;
476
477  node1 = mAig_CreateVar(manager,"a",5); /* var a of 5 values */
478  node2 = mAig_CreateVar(manager,"b",6); /* var b of 6 values */
479  node3 = mAig_CreateVar(manager,"c",2); /* var c of 2 values */
480
481  aa = MvfAig_FunctionCreateFromVariable(manager, node1);
482  bb = MvfAig_FunctionCreateFromVariable(manager, node2);
483  cc = MvfAig_FunctionCreateFromVariable(manager, node3);
484
485  mVarList    = mAigReadMulVarList(manager);
486  bVarList    = mAigReadBinVarList(manager); 
487  fprintf(vis_stdout,"mValist: \n");
488  for (i=0; i< array_n(mVarList); i++){
489    mVar   = array_fetch(mAigMvar_t, mVarList, i);
490    fprintf(vis_stdout,"mVarId=%d name=%s bVarId=%d values:%d\n",  mVar.mVarId, mVar.name, mVar.bVars, mVar.values);
491  }
492
493  fprintf(vis_stdout,"bValist: \n");
494  for (i=0; i< array_n(bVarList); i++){
495    bVar   = array_fetch(mAigBvar_t, bVarList, i);
496    fprintf(vis_stdout,"mVar ID=%d bVar ID=%ld \n",  bVar.mVarId, bVar.node);
497  }
498
499  node4 = array_fetch(bAigEdge_t, aa, 3);
500  node5 = array_fetch(bAigEdge_t, bb, 2);
501  node6 = mAig_Or(manager, node4, node5);
502
503  node4 = array_fetch(bAigEdge_t, cc, 0);
504  node5 = bAig_Eq(manager, node6, node4);
505
506  fprintf(vis_stdout,"%ld %ld %ld %ld %ld %ld\n",node1, node2, node3, node4, node5, node6);
507  fprintf(vis_stdout,"Nodes Array:\n\n");
508  for (i=0; i< manager->nodesArraySize ; i++)
509    fprintf(vis_stdout,"Node #%d  value=%ld \n",i,manager->NodesArray[i]);
510
511  fprintf(vis_stdout,"\n\nName List:\n");
512  for (i=0; i< 20; i++)
513    fprintf(vis_stdout,"index %d  Name %s \n",i, manager->nameList[i]);
514
515  bAig_PrintDot(vis_stdout, manager);
516
517  return 0;
518
519}
Note: See TracBrowser for help on using the repository browser.