abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
fraigNode.c File Reference
#include "fraigInt.h"

Go to the source code of this file.

Macros

#define Fraig_NodeIsSimComplement(p)   (Fraig_IsComplement(p)? !(Fraig_Regular(p)->fInv) : (p)->fInv)
 DECLARATIONS ///. More...
 

Functions

Fraig_Node_tFraig_NodeCreateConst (Fraig_Man_t *p)
 FUNCTION DEFINITIONS ///. More...
 
Fraig_Node_tFraig_NodeCreatePi (Fraig_Man_t *p)
 
Fraig_Node_tFraig_NodeCreate (Fraig_Man_t *p, Fraig_Node_t *p1, Fraig_Node_t *p2)
 
void Fraig_NodeSimulate (Fraig_Node_t *pNode, int iWordStart, int iWordStop, int fUseRand)
 

Macro Definition Documentation

#define Fraig_NodeIsSimComplement (   p)    (Fraig_IsComplement(p)? !(Fraig_Regular(p)->fInv) : (p)->fInv)

DECLARATIONS ///.

CFile****************************************************************

FileName [fraigNode.c]

PackageName [FRAIG: Functionally reduced AND-INV graphs.]

Synopsis [Implementation of the FRAIG node.]

Author [Alan Mishchenko alanm.nosp@m.i@ee.nosp@m.cs.be.nosp@m.rkel.nosp@m.ey.ed.nosp@m.u]

Affiliation [UC Berkeley]

Date [Ver. 2.0. Started - October 1, 2004]

Revision [

Id:
fraigNode.c,v 1.3 2005/07/08 01:01:32 alanmi Exp

]

Definition at line 29 of file fraigNode.c.

Function Documentation

Fraig_Node_t* Fraig_NodeCreate ( Fraig_Man_t p,
Fraig_Node_t p1,
Fraig_Node_t p2 
)

Function*************************************************************

Synopsis [Creates a new node.]

Description [This procedure should be called to create the constant node and the PI nodes first.]

SideEffects []

SeeAlso []

Definition at line 160 of file fraigNode.c.

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 }
char * memset()
void Fraig_NodeVecPush(Fraig_NodeVec_t *p, Fraig_Node_t *Entry)
Definition: fraigVec.c:189
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
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
Fraig_Node_t * p1
Definition: fraigInt.h:232
#define Fraig_NodeIsSimComplement(p)
DECLARATIONS ///.
Definition: fraigNode.c:29
int Fraig_BitStringCountOnes(unsigned *pString, int nWords)
Definition: fraigUtil.c:288
unsigned fFailTfo
Definition: fraigInt.h:227
#define Fraig_Regular(p)
Definition: fraig.h:108
char * Fraig_MemFixedEntryFetch(Fraig_MemFixed_t *p)
Definition: fraigMem.c:131
ABC_INT64_T abctime
Definition: abc_global.h:278
Fraig_Node_t* Fraig_NodeCreateConst ( Fraig_Man_t p)

FUNCTION DEFINITIONS ///.

Function*************************************************************

Synopsis [Creates the constant 1 node.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file fraigNode.c.

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 }
char * memset()
void Fraig_NodeVecPush(Fraig_NodeVec_t *p, Fraig_Node_t *Entry)
Definition: fraigVec.c:189
static Llb_Mgr_t * p
Definition: llb3Image.c:950
unsigned * puSimD
Definition: fraigInt.h:248
unsigned * puSimR
Definition: fraigInt.h:247
Fraig_Node_t * Fraig_HashTableLookupF0(Fraig_Man_t *pMan, Fraig_Node_t *pNode)
Definition: fraigTable.c:193
char * Fraig_MemFixedEntryFetch(Fraig_MemFixed_t *p)
Definition: fraigMem.c:131
Fraig_Node_t* Fraig_NodeCreatePi ( Fraig_Man_t p)

Function*************************************************************

Synopsis [Creates a primary input node.]

Description []

SideEffects []

SeeAlso []

Definition at line 87 of file fraigNode.c.

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 }
char * memset()
void Fraig_NodeVecPush(Fraig_NodeVec_t *p, Fraig_Node_t *Entry)
Definition: fraigVec.c:189
static Llb_Mgr_t * p
Definition: llb3Image.c:950
unsigned * puSimD
Definition: fraigInt.h:248
static abctime Abc_Clock()
Definition: abc_global.h:279
unsigned * puSimR
Definition: fraigInt.h:247
#define FRAIG_RANDOM_UNSIGNED
Definition: fraigInt.h:76
int Fraig_BitStringCountOnes(unsigned *pString, int nWords)
Definition: fraigUtil.c:288
Fraig_Node_t * Fraig_HashTableLookupF(Fraig_Man_t *pMan, Fraig_Node_t *pNode)
Definition: fraigTable.c:136
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
int s_FraigPrimes[FRAIG_MAX_PRIMES]
DECLARATIONS ///.
Definition: fraigPrime.c:30
void Fraig_NodeSimulate ( Fraig_Node_t pNode,
int  iWordStart,
int  iWordStop,
int  fUseRand 
)

Function*************************************************************

Synopsis [Simulates the node.]

Description [Simulates the random or dynamic simulation info through the node. Uses phases of the children to determine their real simulation info. Uses phase of the node to determine the way its simulation info is stored. The resulting info is guaranteed to be 0 for the first pattern.]

SideEffects [This procedure modified the hash value of the simulation info.]

SeeAlso []

Definition at line 226 of file fraigNode.c.

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 }
unsigned * puSimD
Definition: fraigInt.h:248
Fraig_Node_t * p2
Definition: fraigInt.h:233
unsigned * puSimR
Definition: fraigInt.h:247
Fraig_Node_t * p1
Definition: fraigInt.h:232
#define Fraig_IsComplement(p)
GLOBAL VARIABLES ///.
Definition: fraig.h:107
#define Fraig_NodeIsSimComplement(p)
DECLARATIONS ///.
Definition: fraigNode.c:29
#define Fraig_Regular(p)
Definition: fraig.h:108
#define assert(ex)
Definition: util_old.h:213
int s_FraigPrimes[FRAIG_MAX_PRIMES]
DECLARATIONS ///.
Definition: fraigPrime.c:30