source: vis_dev/vis-2.3/src/baig/baig.h @ 40

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

vis2.3
File size: 21.3 KB
Line 
1/**CHeaderFile*****************************************************************
2
3  FileName    [baig.h]
4
5  PackageName [baig]
6
7  Synopsis    [Binary AND/INVERTER graph]
8
9  Description [External functions and data strucures of the binary AND/INVERTER graph package]
10
11  SeeAlso     [baigInt.h]
12
13  Author      [Mohammad Awedh]
14
15  Copyright [This file was created at the University of Colorado at
16  Boulder.  The University of Colorado at Boulder makes no warranty
17  about the suitability of this software for any purpose.  It is
18  presented on an AS IS basis.]
19
20  Revision    [$Id: baig.h,v 1.29 2009/04/12 00:14:03 fabio Exp $]
21
22
23******************************************************************************/
24
25#ifndef _BAIG
26#define _BAIG
27
28#include "st.h"
29#include "ntk.h"
30#include "bdd.h"
31#include "mdd.h"
32#include "sat.h"
33#include "ctlsp.h"
34/*Bing:*/
35#include "puresat.h"
36
37
38/*---------------------------------------------------------------------------*/
39/* Constant declarations                                                     */
40/*---------------------------------------------------------------------------*/
41
42#ifndef TRUE
43#define TRUE 1
44#endif
45
46#ifndef FALSE
47#define FALSE 0
48#endif
49
50#define bAigInvertBit      0x1                        /* This bit is set to indicate inverted edge*/
51
52#define bAigArrayMaxSize   (1 << 27)  /* Maximum size of the node array */
53
54#define ZERO_NODE_INDEX    0                          /* Reserve this index for constant Zero node*/
55#define bAig_Zero          (ZERO_NODE_INDEX)          /* Constatnt Zero node */
56#define bAig_One           (bAig_Not(bAig_Zero))      /* Constatnt One node  */
57
58#define bAig_NULL          2
59/*Bing*/
60#define bAigNodeSize       12 /*8*/                          /* Array is used to implement the bAig graph.
61                                                         Each node occupies bAigNodeSize array elements. */
62#define bAigFirstNodeIndex   bAigNodeSize             /* The first node index. */
63
64#define bAig_HashTableSize 481931
65
66#define  bAigValue     0   /* Index of the decision level. */ 
67#define  bAigFlags     1   /* Index of flag for this node.*/
68#define  bAigLeft      2   /* Index of the left child */ 
69#define  bAigRight     3   /* Index of the right child */ 
70#define  bAigNFanout   4   /* Index of number of fanout.*/
71#define  bAigFanout    5   /* Index of fanout pointer for this node.*/
72#define  bAigCanonical 6   /* Index of canonical node for this node.*/
73#define  bAigNext      7   /* Index of dummy for this node.*/
74
75/*Bing:*/
76#define  bAigClass     8
77
78/*---------------------------------------------------------------------------*/
79/* Type declarations                                                         */
80/*---------------------------------------------------------------------------*/
81
82typedef char                     nameType_t;
83typedef long                     bAigEdge_t;
84typedef struct bAigManagerStruct bAig_Manager_t;
85typedef struct bAigTimeFrameStruct      bAigTimeFrame_t;
86
87/*---------------------------------------------------------------------------*/
88/* Structure declarations                                                    */
89/*---------------------------------------------------------------------------*/
90
91/**Struct**********************************************************************
92
93  Synopsis    [And/Inverter graph manager.]
94
95  Description []
96
97******************************************************************************/
98struct bAigManagerStruct {
99  bAigEdge_t *NodesArray;       /* contains pointers to nodes of type
100                                   bAig_Node_t */
101  long        nodesArraySize;    /* contains the current number of nodes */
102  long        maxNodesArraySize; /* Nodes Array maximum size */
103
104  bAigEdge_t *HashTable;        /* Hash table */
105  st_table   *SymbolTable;      /* Symbol table to store variables and their
106                                   indices */
107  char       **nameList;        /* This table contains the name of each node.
108                                   nodeID is used to access the node's name. */
109  array_t    *mVarList;         /* List of mVarId of each variable */ 
110  array_t    *bVarList;         /* List of bVardId (bAig_t) of the binary value
111                                   encoding for multi-valued variables. */
112  int        allocatedFlags;
113  int        *bddIdArray;
114  bdd_t      **bddArray;
115  bdd_t      **relArray;
116  st_table   *id2aig;
117
118  struct bAigTimeFrameStruct *timeframe;
119  struct bAigTimeFrameStruct *timeframeWOI;
120  struct satLiteralDBStruct *literals;
121  char *dummy;
122 
123  /* Bing: for interpolation */
124  bAigEdge_t **  HashTableArray;
125  st_table **    SymbolTableArray;
126  int NumOfTable;
127
128  int class_; /* one is C1, 2 is C2 or for multiCut it is the timeframe */
129  IP_Manager_t * ipm;
130  satArray_t * assertArray;
131  bAigEdge_t  InitState, IPState;
132  /*RTree_t *root;*/
133  int IP,test2LevelMini;
134  satArray_t * assertArray2, *EqArray, *CoiAssertArray;
135};
136
137/**Struct**********************************************************************
138
139  Synopsis    [A struct to save unrolled system]
140
141******************************************************************************/
142struct bAigTimeFrameStruct {
143  int nInputs;                 /* the number of inputs */
144  int nOutputs;                /* the number of outputs */
145  int nLatches;                /* the number of latchs */
146  int nInternals;              /* the numebr of internal nodes */
147  int currentTimeframe;        /* the number of unrolled timeframe */
148  bAigEdge_t **inputs;         /* the array to save input of each unrolled timeframe */
149  bAigEdge_t **outputs;        /* the array to save output of each unrolled timeframe */
150  bAigEdge_t **latchInputs;    /* the array to save latch input of each unrolled timeframe */
151  bAigEdge_t **internals;      /* the array to save internal node of each unrolled timeframe */
152  /* we need this array to build property */
153  /* based on internal node, there might be */
154  /* the way to improve this. */
155  bAigEdge_t *oriLatchInputs;  /* the array to save latch input of original system */
156  bAigEdge_t *oribLatchInputs; /* the array to save latch input of original system */
157  bAigEdge_t *oriInputs;       /* the array to save input of original system */
158  bAigEdge_t *oribInputs;      /* the array to save input of original system */
159  st_table *li2index;          /* It maps the latch input aig to index which can identify i'th latch input through latchInputs[i][index] */
160  st_table *o2index;           /* It maps the output aig to index which can identify i'th latch input through outputs[i][index] */
161  st_table *i2index;           /* It maps the input aig to index which can identify i'th latch input through inputs[i][index] */
162  st_table *pi2index;          /* It maps the input aig to index which can identify i'th latch input through inputs[i][index] */
163  array_t *latchArr;
164  array_t *inputArr;
165  array_t *outputArr;
166  array_t *iindexArray;
167  array_t *assertedArray;
168  int nbInputs;                /* the number of input bits */
169  int nbLatches;               /* the number of latche bits */
170  bAigEdge_t **binputs;        /* the array to save input bit of each unrolled timeframe */
171  bAigEdge_t **blatchInputs;   /* the array to save latch input bit of each unrolled timeframe */
172  st_table *bli2index;         /* It maps the latch input bit of aig to index which can identify i'th latch input through blatchInputs[i][index] */
173  st_table *bpi2index;         /* It maps the input bit of aig to index which can identify i'th latch input through binputs[i][index] */
174
175  /*Bing:*/
176  st_table *libli2eq;
177  st_table *idx2name;
178  st_table *MultiLatchTable;   /* stores var corresponding to multiple latches */
179};
180
181/**Struct**********************************************************************
182
183  Synopsis    [A struct to save transition relation of AIG ]
184
185******************************************************************************/
186typedef struct bAigTransitionStruct     bAigTransition_t;
187struct bAigTransitionStruct {
188  Ntk_Network_t     *network;
189  bAig_Manager_t    *manager;
190  satManager_t *allsat;   /** to save the sat manager for allsat process **/
191  satManager_t *lifting;  /** to save the sat manager for lifting process **/
192  int nInputs;           
193  int nLatches;         
194  bAigEdge_t objective;
195  bAigEdge_t *inputs;         
196  bAigEdge_t *cstates;   
197  bAigEdge_t *nstates;
198  bAigEdge_t *initials;
199  bAigEdge_t *n2c;
200  bAigEdge_t *c2n;
201  bAigEdge_t *cobj;
202  int csize;
203  int istates;
204  bAigEdge_t *tstates;   
205  bAigEdge_t *coiStates;  /* to identified the next states variables in froniter set **/ 
206
207  int *vinputs;     /** to save the value of primary inputs **/ 
208  int *vtstates;    /** to save the value of tstates variable during lifting **/
209  int objValue;
210  int latestBlockingClause;
211  int iteration;
212  struct satArrayStruct *unassigned;
213  struct satArrayStruct *tVariables;
214  struct satArrayStruct *auxObj;
215  struct satArrayStruct *objArr; /** to save the next state variable used to build objective */
216
217  struct satArrayStruct *reached;
218  struct satArrayStruct *frontier;
219  struct satArrayStruct *originalFrontier;
220  int avgLits;
221  int sum;
222  int period;
223  int interval;
224  int nBlocked;
225
226  int method;
227  int interface;
228  int inclusionInitial;
229  int constrain;
230  int verbose;
231  int reductionUsingUnsat;
232  int disableLifting;
233};
234
235
236/*---------------------------------------------------------------------------*/
237/* Variable declarations                                                     */
238/*---------------------------------------------------------------------------*/
239
240/*---------------------------------------------------------------------------*/
241/* Macro declarations                                                        */
242/*---------------------------------------------------------------------------*/
243
244/**Macro***********************************************************************
245
246  Synopsis     [Returns the class of a node]
247
248  Description  []
249
250  SideEffects [none]
251
252  SeeAlso      []
253
254******************************************************************************/
255/*Bing:*/
256#define bAig_Class(node) (\
257 manager->NodesArray[bAig_NonInvertedEdge(node)+bAigClass]\
258)
259
260/**Macro***********************************************************************
261
262  Synopsis     [Performs the 'Not' Logical operator]
263
264  Description  [This macro inverts the edge going to a node which corresponds
265                to NOT operator]
266
267  SideEffects [none]
268
269  SeeAlso      []
270
271******************************************************************************/
272#define bAig_Not(node) (                         \
273        (bAigEdge_t) ((node) ^ (bAigInvertBit))  \
274)
275
276/**Macro***********************************************************************
277
278  Synopsis     [Returns the non inverted edge.]
279
280  Description  [This macro returns the non inverted edge.  It clears the least
281  significant bit of the edge if it is set.]
282
283  SideEffects  [none]
284
285  SeeAlso      []
286
287******************************************************************************/
288#define bAig_NonInvertedEdge(edge) ( \
289        (edge) & ~(bAigInvertBit)    \
290)
291
292/**Macro***********************************************************************
293
294  Synopsis     [Returns true if the edge is inverted.]
295
296  Description  []
297
298  SideEffects [none]
299
300  SeeAlso      []
301
302******************************************************************************/
303#define bAig_IsInverted(edge) (   \
304        (edge) & (bAigInvertBit)  \
305)
306
307/**Macro***********************************************************************
308
309  Synopsis    [Return right child of aig node]
310
311  Description []
312
313  SideEffects [none]
314
315  SeeAlso     []
316
317******************************************************************************/
318#define rightChild(node)(\
319(manager->NodesArray[bAig_NonInvertedEdge(node)+bAigRight])\
320)
321
322/**Macro***********************************************************************
323
324  Synopsis    [Return left child of aig node]
325
326  Description []
327
328  SideEffects [none]
329
330  SeeAlso     []
331
332******************************************************************************/
333#define leftChild(node)(\
334(manager->NodesArray[bAig_NonInvertedEdge(node)+bAigLeft])\
335)
336
337/**Macro***********************************************************************
338
339  Synopsis    []
340
341  Description []
342
343  SideEffects [none]
344
345  SeeAlso     []
346
347******************************************************************************/
348#define fanout(node)(\
349manager->NodesArray[bAig_NonInvertedEdge(node)+bAigFanout]\
350)
351
352/**Macro***********************************************************************
353
354  Synopsis    []
355
356  Description []
357
358  SideEffects [none]
359
360  SeeAlso     []
361
362******************************************************************************/
363#define nFanout(node)(\
364manager->NodesArray[bAig_NonInvertedEdge(node)+bAigNFanout]\
365)
366
367/**Macro***********************************************************************
368
369  Synopsis    []
370
371  Description []
372
373  SideEffects [none]
374
375  SeeAlso     []
376
377******************************************************************************/
378#define flags(node)(\
379manager->NodesArray[bAig_NonInvertedEdge(node)+bAigFlags]\
380)
381
382/**Macro***********************************************************************
383
384  Synopsis    []
385
386  Description []
387
388  SideEffects [none]
389
390  SeeAlso     []
391
392******************************************************************************/
393#define canonical(node)(\
394manager->NodesArray[bAig_NonInvertedEdge(node)+bAigCanonical]\
395)
396
397
398/**Macro***********************************************************************
399
400  Synopsis    [return next of aig]
401
402  Description [This is used to build hash table for structural hashing]
403
404  SideEffects [none]
405
406  SeeAlso     []
407
408******************************************************************************/
409#define next(node)(\
410manager->NodesArray[bAig_NonInvertedEdge(node)+bAigNext]\
411)
412
413/**Macro***********************************************************************
414
415  Synopsis    [return value of aig node]
416
417  Description []
418
419  SideEffects [none]
420
421  SeeAlso     []
422
423******************************************************************************/
424#define aig_value(node)(\
425(manager->NodesArray[bAig_NonInvertedEdge(node)+bAigValue])\
426)
427
428/**Macro***********************************************************************
429
430  Synopsis    [The node ID]
431
432  Description [Node ID is a unique number for each node and can be found by
433              dividing the edge going to this node by bAigNodeSize.]
434
435  SideEffects [none]
436
437  SeeAlso     []
438
439******************************************************************************/
440/*#define bAigNodeID(edge)(\
441bAig_NonInvertedEdge(edge)>>3 \
442)*/
443
444/*Bing:*/
445#define bAigNodeID(edge)(\
446bAig_NonInvertedEdge(edge)/bAigNodeSize \
447)
448
449
450/**Macro***********************************************************************
451
452  Synopsis    [Hash function for the hash table.]
453
454  Description []
455
456  SideEffects [none]
457
458  SeeAlso     []
459
460******************************************************************************/
461#define HashTableFunction(left, right) \
462( (bAigEdge_t)\
463((( (bAigEdge_t) (left)) << 3) + \
464(( (bAigEdge_t) (right)) << 3)) % bAig_HashTableSize \
465)
466
467
468/**Macro***********************************************************************
469
470  Synopsis    [Traverse fanout of AIG ]
471
472  Description []
473
474  SideEffects [none]
475
476  SeeAlso     []
477
478******************************************************************************/
479#define bAigEdgeForEachFanout(                             \
480        manager,     /* bAig_Manager_t */                  \
481        v,           /* bAigEdge_t */                      \
482        cur,         /* bAigEdge_t for fanout */           \
483        ii,                                                \
484        iii,                                               \
485        pfan                                               \
486)                                                          \
487for(ii=0, iii=nFanout(v), pfan=(bAigEdge_t *)fanout(v);    \
488    (ii<iii) && (cur = pfan[ii]);                          \
489    ii++)
490
491
492/**Macro***********************************************************************
493
494  Synopsis    [Is AIG node a variable node]
495
496  Description []
497
498  SideEffects [none]
499
500  SeeAlso     []
501
502******************************************************************************/
503#define bAigIsVar(manager, v)                              \
504    (leftChild(v) == bAig_NULL)
505
506
507/**Macro***********************************************************************
508
509  Synopsis    [Check whether two nodes are same or not]
510
511  Description [Check whether two nodes are same or not, accounting for
512  complementation.  The two nodes may only differ in the LSB.]
513
514  SideEffects [none]
515
516  SeeAlso     []
517
518******************************************************************************/
519#define bAigCompareNode(l, r)                              \
520  (((l) | 1) == ((r) | 1))
521
522
523/**Macro***********************************************************************
524
525  Synopsis    [Swap AIG nodes ]
526
527  Description [Swap two AIG nodes by a sequence of exclusive ORs.]
528
529  SideEffects [none]
530
531  SeeAlso     []
532
533******************************************************************************/
534#define bAigSwap(l, r)                                     \
535  {(l) ^= (r); (r) ^= (l); (l) ^= (r);}
536
537
538/**AutomaticStart*************************************************************/
539
540/*---------------------------------------------------------------------------*/
541/* Function prototypes                                                       */
542/*---------------------------------------------------------------------------*/
543
544EXTERN void bAig_BddSweepMain(Ntk_Network_t *network, array_t *nodeArray);
545EXTERN void bAig_BddSweepSub(bAig_Manager_t *manager, mdd_manager *mgr, bAigEdge_t v, st_table *bdd2vertex, int sizeLimit, int *newBddIdIndex);
546EXTERN void bAig_BuildAigBFSManner(Ntk_Network_t *network, mAig_Manager_t *manager, st_table *leaves, int sweep);
547EXTERN void bAig_BddSweepForceMain(Ntk_Network_t *network, array_t *nodeArray);
548EXTERN void bAig_BddSweepForceSub(bAig_Manager_t *manager, mdd_manager *mgr, bAigEdge_t v, st_table *bdd2vertex, int sizeLimit, int *newBddIdIndex);
549EXTERN void bAig_Init(void);
550EXTERN void bAig_End(void);
551EXTERN bAig_Manager_t * bAig_initAig(int maxSize);
552EXTERN void bAig_quit(bAig_Manager_t *manager);
553EXTERN void bAig_NodePrint(bAig_Manager_t *manager, bAigEdge_t node);
554EXTERN nameType_t * bAig_NodeReadName(bAig_Manager_t *manager, bAigEdge_t node);
555EXTERN void bAig_NodeSetName(bAig_Manager_t *manager, bAigEdge_t node, nameType_t *name);
556EXTERN int bAig_NodeReadIndexOfRightChild(bAig_Manager_t *manager, bAigEdge_t nodeIndex);
557EXTERN bAigEdge_t bAig_NodeReadIndexOfLeftChild(bAig_Manager_t *manager, bAigEdge_t nodeIndex);
558EXTERN bAigEdge_t bAig_GetCanonical(bAig_Manager_t *manager, bAigEdge_t nodeIndex);
559EXTERN int bAig_Merge(bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2);
560EXTERN void bAig_PrintNode(bAig_Manager_t *manager, bAigEdge_t i);
561EXTERN bAigEdge_t bAig_And(bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2);
562EXTERN bAigEdge_t bAig_And2(bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2);
563EXTERN bAigEdge_t bAig_Or(bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2);
564EXTERN bAigEdge_t bAig_Xor(bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2);
565EXTERN bAigEdge_t bAig_Eq(bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2);
566EXTERN bAigEdge_t bAig_Then(bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2);
567EXTERN bAigEdge_t bAig_CreateNode(bAig_Manager_t *manager, bAigEdge_t nodeIndex1, bAigEdge_t nodeIndex2);
568EXTERN bAigEdge_t bAig_FindNodeByName(bAig_Manager_t *manager, nameType_t *name);
569EXTERN bAigEdge_t bAig_CreateVarNode(bAig_Manager_t *manager, nameType_t *name);
570EXTERN int bAig_isVarNode(bAig_Manager_t *manager, bAigEdge_t node);
571EXTERN bAigEdge_t bAig_bddTobAig(bAig_Manager_t *bAigManager, bdd_t *fn);
572EXTERN int bAig_PrintDot(FILE *fp, bAig_Manager_t *manager);
573EXTERN bAigEdge_t bAig_And4(bAig_Manager_t *manager, bAigEdge_t l, bAigEdge_t r);
574EXTERN bAigEdge_t bAig_And3(bAig_Manager_t *manager, bAigEdge_t l, bAigEdge_t r);
575EXTERN void bAig_SetMaskTransitiveFanin(bAig_Manager_t *manager, int v, unsigned int mask);
576EXTERN void bAig_ResetMaskTransitiveFanin(bAig_Manager_t *manager, int v, unsigned int mask, unsigned int resetMask);
577EXTERN void bAig_ExpandTimeFrame(Ntk_Network_t *network, mAig_Manager_t *manager, int bound, int withInitialState);
578EXTERN void bAig_FreeTimeFrame(bAigTimeFrame_t *timeframe);
579EXTERN bAigTimeFrame_t * bAig_InitTimeFrame(Ntk_Network_t *network, mAig_Manager_t *manager, int withInitialState);
580EXTERN void bAig_CreateNewNode(mAig_Manager_t *manager, st_table *node2MvfAigTable, Ntk_Node_t *node, bAigEdge_t *bli, bAigEdge_t *li, int *bindex, int *index);
581EXTERN bAigEdge_t bAig_ExpandForEachCone(mAig_Manager_t *manager, bAigEdge_t v, st_table *old2new);
582EXTERN void bAig_CheckConnect(bAig_Manager_t *manager, int from, int to);
583EXTERN int bAig_CheckConnectFanin(bAig_Manager_t *manager, int from, int to);
584EXTERN int bAig_CheckConnectFanout(bAig_Manager_t *manager, int from, int to);
585EXTERN int bAig_GetValueOfNode(bAig_Manager_t *manager, bAigEdge_t v);
586EXTERN void bAig_GetCOIForNode(Ntk_Node_t *node, st_table *table);
587EXTERN void bAig_GetCOIForNodeMain(Ntk_Network_t * network, char *name);
588EXTERN void bAig_CheckLatchStatus(Ntk_Network_t * network, bAig_Manager_t *manager);
589EXTERN void bAig_PrintNodeAigStatus(bAig_Manager_t *manager, Ntk_Node_t *node);
590EXTERN void bAig_PrintNodeAigStatusWithName(Ntk_Network_t * network, bAig_Manager_t *manager, char *name);
591EXTERN bAigEdge_t bAig_CreatebAigForInvariant( Ntk_Network_t *network, bAig_Manager_t *manager, Ctlsp_Formula_t *inv);
592
593/**AutomaticEnd***************************************************************/
594
595#endif /* _BAIG */
Note: See TracBrowser for help on using the repository browser.