abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
fraigNode.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [fraigNode.c]
4 
5  PackageName [FRAIG: Functionally reduced AND-INV graphs.]
6 
7  Synopsis [Implementation of the FRAIG node.]
8 
9  Author [Alan Mishchenko <alanmi@eecs.berkeley.edu>]
10 
11  Affiliation [UC Berkeley]
12 
13  Date [Ver. 2.0. Started - October 1, 2004]
14 
15  Revision [$Id: fraigNode.c,v 1.3 2005/07/08 01:01:32 alanmi Exp $]
16 
17 ***********************************************************************/
18 
19 #include "fraigInt.h"
20 
22 
23 
24 ////////////////////////////////////////////////////////////////////////
25 /// DECLARATIONS ///
26 ////////////////////////////////////////////////////////////////////////
27 
28 // returns the complemented attribute of the node
29 #define Fraig_NodeIsSimComplement(p) (Fraig_IsComplement(p)? !(Fraig_Regular(p)->fInv) : (p)->fInv)
30 
31 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 /**Function*************************************************************
36 
37  Synopsis [Creates the constant 1 node.]
38 
39  Description []
40 
41  SideEffects []
42 
43  SeeAlso []
44 
45 ***********************************************************************/
47 {
48  Fraig_Node_t * pNode;
49 
50  // create the node
51  pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes );
52  memset( pNode, 0, sizeof(Fraig_Node_t) );
53 
54  // assign the number and add to the array of nodes
55  pNode->Num = p->vNodes->nSize;
56  Fraig_NodeVecPush( p->vNodes, pNode );
57  pNode->NumPi = -1; // this is not a PI, so its number is -1
58  pNode->Level = 0; // just like a PI, it has 0 level
59  pNode->nRefs = 1; // it is a persistent node, which comes referenced
60  pNode->fInv = 1; // the simulation info is complemented
61 
62  // create the simulation info
63  pNode->puSimR = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims );
64  pNode->puSimD = pNode->puSimR + p->nWordsRand;
65  memset( pNode->puSimR, 0, sizeof(unsigned) * p->nWordsRand );
66  memset( pNode->puSimD, 0, sizeof(unsigned) * p->nWordsDyna );
67 
68  // count the number of ones in the simulation vector
69  pNode->nOnes = p->nWordsRand * sizeof(unsigned) * 8;
70 
71  // insert it into the hash table
72  Fraig_HashTableLookupF0( p, pNode );
73  return pNode;
74 }
75 
76 /**Function*************************************************************
77 
78  Synopsis [Creates a primary input node.]
79 
80  Description []
81 
82  SideEffects []
83 
84  SeeAlso []
85 
86 ***********************************************************************/
88 {
89  Fraig_Node_t * pNode, * pNodeRes;
90  int i;
91  abctime clk;
92 
93  // create the node
94  pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes );
95  memset( pNode, 0, sizeof(Fraig_Node_t) );
96  pNode->puSimR = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims );
97  pNode->puSimD = pNode->puSimR + p->nWordsRand;
98  memset( pNode->puSimD, 0, sizeof(unsigned) * p->nWordsDyna );
99 
100  // assign the number and add to the array of nodes
101  pNode->Num = p->vNodes->nSize;
102  Fraig_NodeVecPush( p->vNodes, pNode );
103 
104  // assign the PI number and add to the array of primary inputs
105  pNode->NumPi = p->vInputs->nSize;
106  Fraig_NodeVecPush( p->vInputs, pNode );
107 
108  pNode->Level = 0; // PI has 0 level
109  pNode->nRefs = 1; // it is a persistent node, which comes referenced
110  pNode->fInv = 0; // the simulation info of the PI is not complemented
111 
112  // derive the simulation info for the new node
113 clk = Abc_Clock();
114  // set the random simulation info for the primary input
115  pNode->uHashR = 0;
116  for ( i = 0; i < p->nWordsRand; i++ )
117  {
118  // generate the simulation info
119  pNode->puSimR[i] = FRAIG_RANDOM_UNSIGNED;
120  // for reasons that take very long to explain, it makes sense to have (0000000...)
121  // pattern in the set (this helps if we need to return the counter-examples)
122  if ( i == 0 )
123  pNode->puSimR[i] <<= 1;
124  // compute the hash key
125  pNode->uHashR ^= pNode->puSimR[i] * s_FraigPrimes[i];
126  }
127  // count the number of ones in the simulation vector
128  pNode->nOnes = Fraig_BitStringCountOnes( pNode->puSimR, p->nWordsRand );
129 
130  // set the systematic simulation info for the primary input
131  pNode->uHashD = 0;
132  for ( i = 0; i < p->iWordStart; i++ )
133  {
134  // generate the simulation info
135  pNode->puSimD[i] = FRAIG_RANDOM_UNSIGNED;
136  // compute the hash key
137  pNode->uHashD ^= pNode->puSimD[i] * s_FraigPrimes[i];
138  }
139 p->timeSims += Abc_Clock() - clk;
140 
141  // insert it into the hash table
142  pNodeRes = Fraig_HashTableLookupF( p, pNode );
143  assert( pNodeRes == NULL );
144  // add to the runtime of simulation
145  return pNode;
146 }
147 
148 /**Function*************************************************************
149 
150  Synopsis [Creates a new node.]
151 
152  Description [This procedure should be called to create the constant
153  node and the PI nodes first.]
154 
155  SideEffects []
156 
157  SeeAlso []
158 
159 ***********************************************************************/
161 {
162  Fraig_Node_t * pNode;
163  abctime clk;
164 
165  // create the node
166  pNode = (Fraig_Node_t *)Fraig_MemFixedEntryFetch( p->mmNodes );
167  memset( pNode, 0, sizeof(Fraig_Node_t) );
168 
169  // assign the children
170  pNode->p1 = p1; Fraig_Ref(p1); Fraig_Regular(p1)->nRefs++;
171  pNode->p2 = p2; Fraig_Ref(p2); Fraig_Regular(p2)->nRefs++;
172 
173  // assign the number and add to the array of nodes
174  pNode->Num = p->vNodes->nSize;
175  Fraig_NodeVecPush( p->vNodes, pNode );
176 
177  // assign the PI number
178  pNode->NumPi = -1;
179 
180  // compute the level of this node
181  pNode->Level = 1 + Abc_MaxInt(Fraig_Regular(p1)->Level, Fraig_Regular(p2)->Level);
183  pNode->fFailTfo = Fraig_Regular(p1)->fFailTfo | Fraig_Regular(p2)->fFailTfo;
184 
185  // derive the simulation info
186 clk = Abc_Clock();
187  // allocate memory for the simulation info
188  pNode->puSimR = (unsigned *)Fraig_MemFixedEntryFetch( p->mmSims );
189  pNode->puSimD = pNode->puSimR + p->nWordsRand;
190  // derive random simulation info
191  pNode->uHashR = 0;
192  Fraig_NodeSimulate( pNode, 0, p->nWordsRand, 1 );
193  // derive dynamic simulation info
194  pNode->uHashD = 0;
195  Fraig_NodeSimulate( pNode, 0, p->iWordStart, 0 );
196  // count the number of ones in the random simulation info
197  pNode->nOnes = Fraig_BitStringCountOnes( pNode->puSimR, p->nWordsRand );
198  if ( pNode->fInv )
199  pNode->nOnes = p->nWordsRand * 32 - pNode->nOnes;
200  // add to the runtime of simulation
201 p->timeSims += Abc_Clock() - clk;
202 
203 #ifdef FRAIG_ENABLE_FANOUTS
204  // create the fanout info
207 #endif
208  return pNode;
209 }
210 
211 
212 /**Function*************************************************************
213 
214  Synopsis [Simulates the node.]
215 
216  Description [Simulates the random or dynamic simulation info through
217  the node. Uses phases of the children to determine their real simulation
218  info. Uses phase of the node to determine the way its simulation info
219  is stored. The resulting info is guaranteed to be 0 for the first pattern.]
220 
221  SideEffects [This procedure modified the hash value of the simulation info.]
222 
223  SeeAlso []
224 
225 ***********************************************************************/
226 void Fraig_NodeSimulate( Fraig_Node_t * pNode, int iWordStart, int iWordStop, int fUseRand )
227 {
228  unsigned * pSims, * pSims1, * pSims2;
229  unsigned uHash;
230  int fCompl, fCompl1, fCompl2, i;
231 
232  assert( !Fraig_IsComplement(pNode) );
233 
234  // get hold of the simulation information
235  pSims = fUseRand? pNode->puSimR : pNode->puSimD;
236  pSims1 = fUseRand? Fraig_Regular(pNode->p1)->puSimR : Fraig_Regular(pNode->p1)->puSimD;
237  pSims2 = fUseRand? Fraig_Regular(pNode->p2)->puSimR : Fraig_Regular(pNode->p2)->puSimD;
238 
239  // get complemented attributes of the children using their random info
240  fCompl = pNode->fInv;
241  fCompl1 = Fraig_NodeIsSimComplement(pNode->p1);
242  fCompl2 = Fraig_NodeIsSimComplement(pNode->p2);
243 
244  // simulate
245  uHash = 0;
246  if ( fCompl1 && fCompl2 )
247  {
248  if ( fCompl )
249  for ( i = iWordStart; i < iWordStop; i++ )
250  {
251  pSims[i] = (pSims1[i] | pSims2[i]);
252  uHash ^= pSims[i] * s_FraigPrimes[i];
253  }
254  else
255  for ( i = iWordStart; i < iWordStop; i++ )
256  {
257  pSims[i] = ~(pSims1[i] | pSims2[i]);
258  uHash ^= pSims[i] * s_FraigPrimes[i];
259  }
260  }
261  else if ( fCompl1 && !fCompl2 )
262  {
263  if ( fCompl )
264  for ( i = iWordStart; i < iWordStop; i++ )
265  {
266  pSims[i] = (pSims1[i] | ~pSims2[i]);
267  uHash ^= pSims[i] * s_FraigPrimes[i];
268  }
269  else
270  for ( i = iWordStart; i < iWordStop; i++ )
271  {
272  pSims[i] = (~pSims1[i] & pSims2[i]);
273  uHash ^= pSims[i] * s_FraigPrimes[i];
274  }
275  }
276  else if ( !fCompl1 && fCompl2 )
277  {
278  if ( fCompl )
279  for ( i = iWordStart; i < iWordStop; i++ )
280  {
281  pSims[i] = (~pSims1[i] | pSims2[i]);
282  uHash ^= pSims[i] * s_FraigPrimes[i];
283  }
284  else
285  for ( i = iWordStart; i < iWordStop; i++ )
286  {
287  pSims[i] = (pSims1[i] & ~pSims2[i]);
288  uHash ^= pSims[i] * s_FraigPrimes[i];
289  }
290  }
291  else // if ( !fCompl1 && !fCompl2 )
292  {
293  if ( fCompl )
294  for ( i = iWordStart; i < iWordStop; i++ )
295  {
296  pSims[i] = ~(pSims1[i] & pSims2[i]);
297  uHash ^= pSims[i] * s_FraigPrimes[i];
298  }
299  else
300  for ( i = iWordStart; i < iWordStop; i++ )
301  {
302  pSims[i] = (pSims1[i] & pSims2[i]);
303  uHash ^= pSims[i] * s_FraigPrimes[i];
304  }
305  }
306 
307  if ( fUseRand )
308  pNode->uHashR ^= uHash;
309  else
310  pNode->uHashD ^= uHash;
311 }
312 
313 
314 ////////////////////////////////////////////////////////////////////////
315 /// END OF FILE ///
316 ////////////////////////////////////////////////////////////////////////
317 
319 
char * memset()
void Fraig_NodeVecPush(Fraig_NodeVec_t *p, Fraig_Node_t *Entry)
Definition: fraigVec.c:189
typedefABC_NAMESPACE_HEADER_START struct Fraig_ManStruct_t_ Fraig_Man_t
INCLUDES ///.
Definition: fraig.h:40
ABC_NAMESPACE_IMPL_START void Fraig_NodeAddFaninFanout(Fraig_Node_t *pFanin, Fraig_Node_t *pFanout)
DECLARATIONS ///.
Definition: fraigFanout.c:45
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Fraig_NodeSimulate(Fraig_Node_t *pNode, int iWordStart, int iWordStop, int fUseRand)
Definition: fraigNode.c:226
Fraig_Node_t * Fraig_NodeCreate(Fraig_Man_t *p, Fraig_Node_t *p1, Fraig_Node_t *p2)
Definition: fraigNode.c:160
unsigned * puSimD
Definition: fraigInt.h:248
static abctime Abc_Clock()
Definition: abc_global.h:279
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Fraig_Node_t * p2
Definition: fraigInt.h:233
#define Fraig_Ref(p)
Definition: fraig.h:113
unsigned * puSimR
Definition: fraigInt.h:247
#define FRAIG_RANDOM_UNSIGNED
Definition: fraigInt.h:76
Fraig_Node_t * Fraig_HashTableLookupF0(Fraig_Man_t *pMan, Fraig_Node_t *pNode)
Definition: fraigTable.c:193
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Fraig_Node_t * p1
Definition: fraigInt.h:232
#define Fraig_IsComplement(p)
GLOBAL VARIABLES ///.
Definition: fraig.h:107
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
#define Fraig_NodeIsSimComplement(p)
DECLARATIONS ///.
Definition: fraigNode.c:29
int Fraig_BitStringCountOnes(unsigned *pString, int nWords)
Definition: fraigUtil.c:288
Fraig_Node_t * Fraig_NodeCreatePi(Fraig_Man_t *p)
Definition: fraigNode.c:87
unsigned fFailTfo
Definition: fraigInt.h:227
Fraig_Node_t * Fraig_HashTableLookupF(Fraig_Man_t *pMan, Fraig_Node_t *pNode)
Definition: fraigTable.c:136
#define Fraig_Regular(p)
Definition: fraig.h:108
char * Fraig_MemFixedEntryFetch(Fraig_MemFixed_t *p)
Definition: fraigMem.c:131
#define assert(ex)
Definition: util_old.h:213
ABC_INT64_T abctime
Definition: abc_global.h:278
Fraig_Node_t * Fraig_NodeCreateConst(Fraig_Man_t *p)
FUNCTION DEFINITIONS ///.
Definition: fraigNode.c:46
int s_FraigPrimes[FRAIG_MAX_PRIMES]
DECLARATIONS ///.
Definition: fraigPrime.c:30