abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
abcOdc.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [abcOdc.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Network and node package.]
8 
9  Synopsis [Scalable computation of observability don't-cares.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: abcOdc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "base/abc/abc.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 #define ABC_DC_MAX_NODES (1<<15)
31 
32 typedef unsigned short Odc_Lit_t;
33 
34 typedef struct Odc_Obj_t_ Odc_Obj_t; // 16 bytes
35 struct Odc_Obj_t_
36 {
37  Odc_Lit_t iFan0; // first fanin
38  Odc_Lit_t iFan1; // second fanin
39  Odc_Lit_t iNext; // next node in the hash table
40  unsigned short TravId; // the traversal ID
41  unsigned uData; // the computed data
42  unsigned uMask; // the variable mask
43 };
44 
45 struct Odc_Man_t_
46 {
47  // dont'-care parameters
48  int nVarsMax; // the max number of cut variables
49  int nLevels; // the number of ODC levels
50  int fVerbose; // the verbosiness flag
51  int fVeryVerbose;// the verbosiness flag to print per-node stats
52  int nPercCutoff; // cutoff percentage
53 
54  // windowing
55  Abc_Obj_t * pNode; // the node for windowing
56  Vec_Ptr_t * vLeaves; // the number of the cut
57  Vec_Ptr_t * vRoots; // the roots of the cut
58  Vec_Ptr_t * vBranches; // additional inputs
59 
60  // internal AIG package
61  // objects
62  int nPis; // number of PIs (nVarsMax + 32)
63  int nObjs; // number of objects (Const1, PIs, ANDs)
64  int nObjsAlloc; // number of objects allocated
65  Odc_Obj_t * pObjs; // objects
66  Odc_Lit_t iRoot; // the root object
67  unsigned short nTravIds; // the number of travIDs
68  // structural hashing
69  Odc_Lit_t * pTable; // hash table
70  int nTableSize; // hash table size
71  Vec_Int_t * vUsedSpots; // the used spots
72 
73  // truth tables
74  int nBits; // the number of bits
75  int nWords; // the number of words
76  Vec_Ptr_t * vTruths; // truth tables for each node
77  Vec_Ptr_t * vTruthsElem; // elementary truth tables for the PIs
78  unsigned * puTruth; // the place where the resulting truth table does
79 
80  // statistics
81  int nWins; // the number of windows processed
82  int nWinsEmpty; // the number of empty windows
83  int nSimsEmpty; // the number of empty simulation infos
84  int nQuantsOver; // the number of quantification overflows
85  int nWinsFinish; // the number of windows that finished
86  int nTotalDcs; // total percentage of DCs
87 
88  // runtime
89  abctime timeClean; // windowing
90  abctime timeWin; // windowing
91  abctime timeMiter; // computing the miter
92  abctime timeSim; // simulation
93  abctime timeQuant; // quantification
94  abctime timeTruth; // truth table
95  abctime timeTotal; // useful runtime
96  abctime timeAbort; // aborted runtime
97 };
98 
99 
100 // quantity of different objects
101 static inline int Odc_PiNum( Odc_Man_t * p ) { return p->nPis; }
102 static inline int Odc_NodeNum( Odc_Man_t * p ) { return p->nObjs - p->nPis - 1; }
103 static inline int Odc_ObjNum( Odc_Man_t * p ) { return p->nObjs; }
104 
105 // complemented attributes of objects
106 static inline int Odc_IsComplement( Odc_Lit_t Lit ) { return Lit & (Odc_Lit_t)1; }
107 static inline Odc_Lit_t Odc_Regular( Odc_Lit_t Lit ) { return Lit & ~(Odc_Lit_t)1; }
108 static inline Odc_Lit_t Odc_Not( Odc_Lit_t Lit ) { return Lit ^ (Odc_Lit_t)1; }
109 static inline Odc_Lit_t Odc_NotCond( Odc_Lit_t Lit, int c ) { return Lit ^ (Odc_Lit_t)(c!=0); }
110 
111 // specialized Literals
112 static inline Odc_Lit_t Odc_Const0() { return 1; }
113 static inline Odc_Lit_t Odc_Const1() { return 0; }
114 static inline Odc_Lit_t Odc_Var( Odc_Man_t * p, int i ) { assert( i >= 0 && i < p->nPis ); return (i+1) << 1; }
115 static inline int Odc_IsConst( Odc_Lit_t Lit ) { return Lit < (Odc_Lit_t)2; }
116 static inline int Odc_IsTerm( Odc_Man_t * p, Odc_Lit_t Lit ) { return (int)(Lit>>1) <= p->nPis; }
117 
118 // accessing internal storage
119 static inline Odc_Obj_t * Odc_ObjNew( Odc_Man_t * p ) { assert( p->nObjs < p->nObjsAlloc ); return p->pObjs + p->nObjs++; }
120 static inline Odc_Lit_t Odc_Obj2Lit( Odc_Man_t * p, Odc_Obj_t * pObj ) { assert( pObj ); return (pObj - p->pObjs) << 1; }
121 static inline Odc_Obj_t * Odc_Lit2Obj( Odc_Man_t * p, Odc_Lit_t Lit ) { assert( !(Lit & 1) && (int)(Lit>>1) < p->nObjs ); return p->pObjs + (Lit>>1); }
122 
123 // fanins and their complements
124 static inline Odc_Lit_t Odc_ObjChild0( Odc_Obj_t * pObj ) { return pObj->iFan0; }
125 static inline Odc_Lit_t Odc_ObjChild1( Odc_Obj_t * pObj ) { return pObj->iFan1; }
126 static inline Odc_Lit_t Odc_ObjFanin0( Odc_Obj_t * pObj ) { return Odc_Regular(pObj->iFan0); }
127 static inline Odc_Lit_t Odc_ObjFanin1( Odc_Obj_t * pObj ) { return Odc_Regular(pObj->iFan1); }
128 static inline int Odc_ObjFaninC0( Odc_Obj_t * pObj ) { return Odc_IsComplement(pObj->iFan0); }
129 static inline int Odc_ObjFaninC1( Odc_Obj_t * pObj ) { return Odc_IsComplement(pObj->iFan1); }
130 
131 // traversal IDs
132 static inline void Odc_ManIncrementTravId( Odc_Man_t * p ) { p->nTravIds++; }
133 static inline void Odc_ObjSetTravIdCurrent( Odc_Man_t * p, Odc_Obj_t * pObj ) { pObj->TravId = p->nTravIds; }
134 static inline int Odc_ObjIsTravIdCurrent( Odc_Man_t * p, Odc_Obj_t * pObj ) { return (int )((int)pObj->TravId == p->nTravIds); }
135 
136 // truth tables
137 static inline unsigned * Odc_ObjTruth( Odc_Man_t * p, Odc_Lit_t Lit ) { assert( !(Lit & 1) ); return (unsigned *) Vec_PtrEntry(p->vTruths, Lit >> 1); }
138 
139 // iterators
140 #define Odc_ForEachPi( p, Lit, i ) \
141  for ( i = 0; (i < Odc_PiNum(p)) && (((Lit) = Odc_Var(p, i)), 1); i++ )
142 #define Odc_ForEachAnd( p, pObj, i ) \
143  for ( i = 1 + Odc_CiNum(p); (i < Odc_ObjNum(p)) && ((pObj) = (p)->pObjs + i); i++ )
144 
145 
146 ////////////////////////////////////////////////////////////////////////
147 /// FUNCTION DEFINITIONS ///
148 ////////////////////////////////////////////////////////////////////////
149 
150 /**Function*************************************************************
151 
152  Synopsis [Allocates the don't-care manager.]
153 
154  Description [The parameters are the max number of cut variables,
155  the number of fanout levels used for the ODC computation, and verbosiness.]
156 
157  SideEffects []
158 
159  SeeAlso []
160 
161 ***********************************************************************/
162 Odc_Man_t * Abc_NtkDontCareAlloc( int nVarsMax, int nLevels, int fVerbose, int fVeryVerbose )
163 {
164  Odc_Man_t * p;
165  unsigned * pData;
166  int i, k;
167  p = ABC_ALLOC( Odc_Man_t, 1 );
168  memset( p, 0, sizeof(Odc_Man_t) );
169  assert( nVarsMax > 4 && nVarsMax < 16 );
170  assert( nLevels > 0 && nLevels < 10 );
171 
172  srand( 0xABC );
173 
174  // dont'-care parameters
175  p->nVarsMax = nVarsMax;
176  p->nLevels = nLevels;
177  p->fVerbose = fVerbose;
178  p->fVeryVerbose = fVeryVerbose;
179  p->nPercCutoff = 10;
180 
181  // windowing
182  p->vRoots = Vec_PtrAlloc( 128 );
183  p->vBranches = Vec_PtrAlloc( 128 );
184 
185  // internal AIG package
186  // allocate room for objects
187  p->nObjsAlloc = ABC_DC_MAX_NODES;
188  p->pObjs = ABC_ALLOC( Odc_Obj_t, p->nObjsAlloc * sizeof(Odc_Obj_t) );
189  p->nPis = nVarsMax + 32;
190  p->nObjs = 1 + p->nPis;
191  memset( p->pObjs, 0, p->nObjs * sizeof(Odc_Obj_t) );
192  // set the PI masks
193  for ( i = 0; i < 32; i++ )
194  p->pObjs[1 + p->nVarsMax + i].uMask = (1 << i);
195  // allocate hash table
196  p->nTableSize = p->nObjsAlloc/3 + 1;
197  p->pTable = ABC_ALLOC( Odc_Lit_t, p->nTableSize * sizeof(Odc_Lit_t) );
198  memset( p->pTable, 0, p->nTableSize * sizeof(Odc_Lit_t) );
199  p->vUsedSpots = Vec_IntAlloc( 1000 );
200 
201  // truth tables
202  p->nWords = Abc_TruthWordNum( p->nVarsMax );
203  p->nBits = p->nWords * 8 * sizeof(unsigned);
204  p->vTruths = Vec_PtrAllocSimInfo( p->nObjsAlloc, p->nWords );
205  p->vTruthsElem = Vec_PtrAllocSimInfo( p->nVarsMax, p->nWords );
206 
207  // set elementary truth tables
208  Abc_InfoFill( (unsigned *)Vec_PtrEntry(p->vTruths, 0), p->nWords );
209  for ( k = 0; k < p->nVarsMax; k++ )
210  {
211 // pData = Odc_ObjTruth( p, Odc_Var(p, k) );
212  pData = (unsigned *)Vec_PtrEntry( p->vTruthsElem, k );
213  Abc_InfoClear( pData, p->nWords );
214  for ( i = 0; i < p->nBits; i++ )
215  if ( i & (1 << k) )
216  pData[i>>5] |= (1 << (i&31));
217  }
218 
219  // set random truth table for the additional inputs
220  for ( k = p->nVarsMax; k < p->nPis; k++ )
221  {
222  pData = Odc_ObjTruth( p, Odc_Var(p, k) );
223  Abc_InfoRandom( pData, p->nWords );
224  }
225 
226  // set the miter to the unused value
227  p->iRoot = 0xffff;
228  return p;
229 }
230 
231 /**Function*************************************************************
232 
233  Synopsis [Clears the manager.]
234 
235  Description []
236 
237  SideEffects []
238 
239  SeeAlso []
240 
241 ***********************************************************************/
242 void Abc_NtkDontCareClear( Odc_Man_t * p )
243 {
244  abctime clk = Abc_Clock();
245  // clean the structural hashing table
246  if ( Vec_IntSize(p->vUsedSpots) > p->nTableSize/3 ) // more than one third
247  memset( p->pTable, 0, sizeof(Odc_Lit_t) * p->nTableSize );
248  else
249  {
250  int iSpot, i;
251  Vec_IntForEachEntry( p->vUsedSpots, iSpot, i )
252  p->pTable[iSpot] = 0;
253  }
254  Vec_IntClear( p->vUsedSpots );
255  // reset the number of nodes
256  p->nObjs = 1 + p->nPis;
257  // reset the root node
258  p->iRoot = 0xffff;
259 
260 p->timeClean += Abc_Clock() - clk;
261 }
262 
263 /**Function*************************************************************
264 
265  Synopsis [Frees the don't-care manager.]
266 
267  Description []
268 
269  SideEffects []
270 
271  SeeAlso []
272 
273 ***********************************************************************/
274 void Abc_NtkDontCareFree( Odc_Man_t * p )
275 {
276  if ( p->fVerbose )
277  {
278  printf( "Wins = %5d. Empty = %5d. SimsEmpty = %5d. QuantOver = %5d. WinsFinish = %5d.\n",
279  p->nWins, p->nWinsEmpty, p->nSimsEmpty, p->nQuantsOver, p->nWinsFinish );
280  printf( "Ave DCs per window = %6.2f %%. Ave DCs per finished window = %6.2f %%.\n",
281  1.0*p->nTotalDcs/p->nWins, 1.0*p->nTotalDcs/p->nWinsFinish );
282  printf( "Runtime stats of the ODC manager:\n" );
283  ABC_PRT( "Cleaning ", p->timeClean );
284  ABC_PRT( "Windowing ", p->timeWin );
285  ABC_PRT( "Miter ", p->timeMiter );
286  ABC_PRT( "Simulation ", p->timeSim );
287  ABC_PRT( "Quantifying ", p->timeQuant );
288  ABC_PRT( "Truth table ", p->timeTruth );
289  ABC_PRT( "TOTAL ", p->timeTotal );
290  ABC_PRT( "Aborted ", p->timeAbort );
291  }
292  Vec_PtrFree( p->vRoots );
293  Vec_PtrFree( p->vBranches );
294  Vec_PtrFree( p->vTruths );
295  Vec_PtrFree( p->vTruthsElem );
296  Vec_IntFree( p->vUsedSpots );
297  ABC_FREE( p->pObjs );
298  ABC_FREE( p->pTable );
299  ABC_FREE( p );
300 }
301 
302 
303 
304 /**Function*************************************************************
305 
306  Synopsis [Marks the TFO of the collected nodes up to the given level.]
307 
308  Description []
309 
310  SideEffects []
311 
312  SeeAlso []
313 
314 ***********************************************************************/
315 void Abc_NtkDontCareWinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNode )
316 {
317  Abc_Obj_t * pFanout;
318  int i;
319  if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit || pObj == pNode )
320  return;
321  if ( Abc_NodeIsTravIdCurrent(pObj) )
322  return;
323  Abc_NodeSetTravIdCurrent( pObj );
324  ////////////////////////////////////////
325  // try to reduce the runtime
326  if ( Abc_ObjFanoutNum(pObj) > 100 )
327  return;
328  ////////////////////////////////////////
329  Abc_ObjForEachFanout( pObj, pFanout, i )
330  Abc_NtkDontCareWinSweepLeafTfo_rec( pFanout, nLevelLimit, pNode );
331 }
332 
333 /**Function*************************************************************
334 
335  Synopsis [Marks the TFO of the collected nodes up to the given level.]
336 
337  Description []
338 
339  SideEffects []
340 
341  SeeAlso []
342 
343 ***********************************************************************/
344 void Abc_NtkDontCareWinSweepLeafTfo( Odc_Man_t * p )
345 {
346  Abc_Obj_t * pObj;
347  int i;
348  Abc_NtkIncrementTravId( p->pNode->pNtk );
349  Vec_PtrForEachEntry( Abc_Obj_t *, p->vLeaves, pObj, i )
350  Abc_NtkDontCareWinSweepLeafTfo_rec( pObj, p->pNode->Level + p->nLevels, p->pNode );
351 }
352 
353 /**Function*************************************************************
354 
355  Synopsis [Recursively collects the roots.]
356 
357  Description []
358 
359  SideEffects []
360 
361  SeeAlso []
362 
363 ***********************************************************************/
364 void Abc_NtkDontCareWinCollectRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots )
365 {
366  Abc_Obj_t * pFanout;
367  int i;
368  assert( Abc_ObjIsNode(pObj) );
369  assert( Abc_NodeIsTravIdCurrent(pObj) );
370  // check if the node has all fanouts marked
371  Abc_ObjForEachFanout( pObj, pFanout, i )
372  if ( !Abc_NodeIsTravIdCurrent(pFanout) )
373  break;
374  // if some of the fanouts are unmarked, add the node to the root
375  if ( i < Abc_ObjFanoutNum(pObj) )
376  {
377  Vec_PtrPushUnique( vRoots, pObj );
378  return;
379  }
380  // otherwise, call recursively
381  Abc_ObjForEachFanout( pObj, pFanout, i )
382  Abc_NtkDontCareWinCollectRoots_rec( pFanout, vRoots );
383 }
384 
385 /**Function*************************************************************
386 
387  Synopsis [Collects the roots of the window.]
388 
389  Description [Roots of the window are the nodes that have at least
390  one fanout that it not in the TFO of the leaves.]
391 
392  SideEffects []
393 
394  SeeAlso []
395 
396 ***********************************************************************/
397 void Abc_NtkDontCareWinCollectRoots( Odc_Man_t * p )
398 {
399  assert( !Abc_NodeIsTravIdCurrent(p->pNode) );
400  // mark the node with the old traversal ID
401  Abc_NodeSetTravIdCurrent( p->pNode );
402  // collect the roots
403  Vec_PtrClear( p->vRoots );
404  Abc_NtkDontCareWinCollectRoots_rec( p->pNode, p->vRoots );
405 }
406 
407 /**Function*************************************************************
408 
409  Synopsis [Recursively adds missing nodes and leaves.]
410 
411  Description []
412 
413  SideEffects []
414 
415  SeeAlso []
416 
417 ***********************************************************************/
418 int Abc_NtkDontCareWinAddMissing_rec( Odc_Man_t * p, Abc_Obj_t * pObj )
419 {
420  Abc_Obj_t * pFanin;
421  int i;
422  // skip the already collected leaves and branches
423  if ( Abc_NodeIsTravIdCurrent(pObj) )
424  return 1;
425  // if this is not an internal node - make it a new branch
426  if ( !Abc_NodeIsTravIdPrevious(pObj) || Abc_ObjIsCi(pObj) ) //|| (int)pObj->Level <= p->nLevLeaves )
427  {
428  Abc_NodeSetTravIdCurrent( pObj );
429  Vec_PtrPush( p->vBranches, pObj );
430  return Vec_PtrSize(p->vBranches) <= 32;
431  }
432  // visit the fanins of the node
433  Abc_ObjForEachFanin( pObj, pFanin, i )
434  if ( !Abc_NtkDontCareWinAddMissing_rec( p, pFanin ) )
435  return 0;
436  return 1;
437 }
438 
439 /**Function*************************************************************
440 
441  Synopsis [Adds to the window nodes and leaves in the TFI of the roots.]
442 
443  Description []
444 
445  SideEffects []
446 
447  SeeAlso []
448 
449 ***********************************************************************/
450 int Abc_NtkDontCareWinAddMissing( Odc_Man_t * p )
451 {
452  Abc_Obj_t * pObj;
453  int i;
454  // set the leaves
455  Abc_NtkIncrementTravId( p->pNode->pNtk );
456  Vec_PtrForEachEntry( Abc_Obj_t *, p->vLeaves, pObj, i )
457  Abc_NodeSetTravIdCurrent( pObj );
458  // explore from the roots
459  Vec_PtrClear( p->vBranches );
460  Vec_PtrForEachEntry( Abc_Obj_t *, p->vRoots, pObj, i )
461  if ( !Abc_NtkDontCareWinAddMissing_rec( p, pObj ) )
462  return 0;
463  return 1;
464 }
465 
466 /**Function*************************************************************
467 
468  Synopsis [Computes window for the node.]
469 
470  Description []
471 
472  SideEffects []
473 
474  SeeAlso []
475 
476 ***********************************************************************/
477 int Abc_NtkDontCareWindow( Odc_Man_t * p )
478 {
479  // mark the TFO of the collected nodes up to the given level (p->pNode->Level + p->nWinTfoMax)
480  Abc_NtkDontCareWinSweepLeafTfo( p );
481  // find the roots of the window
482  Abc_NtkDontCareWinCollectRoots( p );
483  if ( Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode )
484  {
485 // printf( "Empty window\n" );
486  return 0;
487  }
488  // add the nodes in the TFI of the roots that are not yet in the window
489  if ( !Abc_NtkDontCareWinAddMissing( p ) )
490  {
491 // printf( "Too many branches (%d)\n", Vec_PtrSize(p->vBranches) );
492  return 0;
493  }
494  return 1;
495 }
496 
497 
498 
499 
500 
501 /**Function*************************************************************
502 
503  Synopsis [Performing hashing of two AIG Literals.]
504 
505  Description []
506 
507  SideEffects []
508 
509  SeeAlso []
510 
511 ***********************************************************************/
512 static inline unsigned Odc_HashKey( Odc_Lit_t iFan0, Odc_Lit_t iFan1, int TableSize )
513 {
514  unsigned Key = 0;
515  Key ^= Odc_Regular(iFan0) * 7937;
516  Key ^= Odc_Regular(iFan1) * 2971;
517  Key ^= Odc_IsComplement(iFan0) * 911;
518  Key ^= Odc_IsComplement(iFan1) * 353;
519  return Key % TableSize;
520 }
521 
522 /**Function*************************************************************
523 
524  Synopsis [Checks if the given name node already exists in the table.]
525 
526  Description []
527 
528  SideEffects []
529 
530  SeeAlso []
531 
532 ***********************************************************************/
533 static inline Odc_Lit_t * Odc_HashLookup( Odc_Man_t * p, Odc_Lit_t iFan0, Odc_Lit_t iFan1 )
534 {
535  Odc_Obj_t * pObj;
536  Odc_Lit_t * pEntry;
537  unsigned uHashKey;
538  assert( iFan0 < iFan1 );
539  // get the hash key for this node
540  uHashKey = Odc_HashKey( iFan0, iFan1, p->nTableSize );
541  // remember the spot in the hash table that will be used
542  if ( p->pTable[uHashKey] == 0 )
543  Vec_IntPush( p->vUsedSpots, uHashKey );
544  // find the entry
545  for ( pEntry = p->pTable + uHashKey; *pEntry; pEntry = &pObj->iNext )
546  {
547  pObj = Odc_Lit2Obj( p, *pEntry );
548  if ( pObj->iFan0 == iFan0 && pObj->iFan1 == iFan1 )
549  return pEntry;
550  }
551  return pEntry;
552 }
553 
554 /**Function*************************************************************
555 
556  Synopsis [Finds node by structural hashing or creates a new node.]
557 
558  Description []
559 
560  SideEffects []
561 
562  SeeAlso []
563 
564 ***********************************************************************/
565 static inline Odc_Lit_t Odc_And( Odc_Man_t * p, Odc_Lit_t iFan0, Odc_Lit_t iFan1 )
566 {
567  Odc_Obj_t * pObj;
568  Odc_Lit_t * pEntry;
569  unsigned uMask0, uMask1;
570  int Temp;
571  // consider trivial cases
572  if ( iFan0 == iFan1 )
573  return iFan0;
574  if ( iFan0 == Odc_Not(iFan1) )
575  return Odc_Const0();
576  if ( Odc_Regular(iFan0) == Odc_Const1() )
577  return iFan0 == Odc_Const1() ? iFan1 : Odc_Const0();
578  if ( Odc_Regular(iFan1) == Odc_Const1() )
579  return iFan1 == Odc_Const1() ? iFan0 : Odc_Const0();
580  // canonicize the fanin order
581  if ( iFan0 > iFan1 )
582  Temp = iFan0, iFan0 = iFan1, iFan1 = Temp;
583  // check if a node with these fanins exists
584  pEntry = Odc_HashLookup( p, iFan0, iFan1 );
585  if ( *pEntry )
586  return *pEntry;
587  // create a new node
588  pObj = Odc_ObjNew( p );
589  pObj->iFan0 = iFan0;
590  pObj->iFan1 = iFan1;
591  pObj->iNext = 0;
592  pObj->TravId = 0;
593  // set the mask
594  uMask0 = Odc_Lit2Obj(p, Odc_Regular(iFan0))->uMask;
595  uMask1 = Odc_Lit2Obj(p, Odc_Regular(iFan1))->uMask;
596  pObj->uMask = uMask0 | uMask1;
597  // add to the table
598  *pEntry = Odc_Obj2Lit( p, pObj );
599  return *pEntry;
600 }
601 
602 /**Function*************************************************************
603 
604  Synopsis [Boolean OR.]
605 
606  Description []
607 
608  SideEffects []
609 
610  SeeAlso []
611 
612 ***********************************************************************/
613 static inline Odc_Lit_t Odc_Or( Odc_Man_t * p, Odc_Lit_t iFan0, Odc_Lit_t iFan1 )
614 {
615  return Odc_Not( Odc_And(p, Odc_Not(iFan0), Odc_Not(iFan1)) );
616 }
617 
618 /**Function*************************************************************
619 
620  Synopsis [Boolean XOR.]
621 
622  Description []
623 
624  SideEffects []
625 
626  SeeAlso []
627 
628 ***********************************************************************/
629 static inline Odc_Lit_t Odc_Xor( Odc_Man_t * p, Odc_Lit_t iFan0, Odc_Lit_t iFan1 )
630 {
631  return Odc_Or( p, Odc_And(p, iFan0, Odc_Not(iFan1)), Odc_And(p, Odc_Not(iFan0), iFan1) );
632 }
633 
634 
635 
636 
637 
638 /**Function*************************************************************
639 
640  Synopsis [Transfers the window into the AIG package.]
641 
642  Description []
643 
644  SideEffects []
645 
646  SeeAlso []
647 
648 ***********************************************************************/
649 void * Abc_NtkDontCareTransfer_rec( Odc_Man_t * p, Abc_Obj_t * pNode, Abc_Obj_t * pPivot )
650 {
651  unsigned uData0, uData1;
652  Odc_Lit_t uLit0, uLit1, uRes0, uRes1;
653  assert( !Abc_ObjIsComplement(pNode) );
654  // skip visited objects
655  if ( Abc_NodeIsTravIdCurrent(pNode) )
656  return pNode->pCopy;
657  Abc_NodeSetTravIdCurrent(pNode);
658  assert( Abc_ObjIsNode(pNode) );
659  // consider the case when the node is the pivot
660  if ( pNode == pPivot )
661  return pNode->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)((Odc_Const1() << 16) | Odc_Const0());
662  // compute the cofactors
663  uData0 = (unsigned)(ABC_PTRUINT_T)Abc_NtkDontCareTransfer_rec( p, Abc_ObjFanin0(pNode), pPivot );
664  uData1 = (unsigned)(ABC_PTRUINT_T)Abc_NtkDontCareTransfer_rec( p, Abc_ObjFanin1(pNode), pPivot );
665  // find the 0-cofactor
666  uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 & 0xffff), Abc_ObjFaninC0(pNode) );
667  uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 & 0xffff), Abc_ObjFaninC1(pNode) );
668  uRes0 = Odc_And( p, uLit0, uLit1 );
669  // find the 1-cofactor
670  uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 >> 16), Abc_ObjFaninC0(pNode) );
671  uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 >> 16), Abc_ObjFaninC1(pNode) );
672  uRes1 = Odc_And( p, uLit0, uLit1 );
673  // find the result
674  return pNode->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)((uRes1 << 16) | uRes0);
675 }
676 
677 /**Function*************************************************************
678 
679  Synopsis [Transfers the window into the AIG package.]
680 
681  Description []
682 
683  SideEffects []
684 
685  SeeAlso []
686 
687 ***********************************************************************/
688 int Abc_NtkDontCareTransfer( Odc_Man_t * p )
689 {
690  Abc_Obj_t * pObj;
691  Odc_Lit_t uRes0, uRes1;
692  Odc_Lit_t uLit;
693  unsigned uData;
694  int i;
695  Abc_NtkIncrementTravId( p->pNode->pNtk );
696  // set elementary variables at the leaves
697  Vec_PtrForEachEntry( Abc_Obj_t *, p->vLeaves, pObj, i )
698  {
699  uLit = Odc_Var( p, i );
700  pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)((uLit << 16) | uLit);
701  Abc_NodeSetTravIdCurrent(pObj);
702  }
703  // set elementary variables at the branched
704  Vec_PtrForEachEntry( Abc_Obj_t *, p->vBranches, pObj, i )
705  {
706  uLit = Odc_Var( p, i+p->nVarsMax );
707  pObj->pCopy = (Abc_Obj_t *)(ABC_PTRUINT_T)((uLit << 16) | uLit);
708  Abc_NodeSetTravIdCurrent(pObj);
709  }
710  // compute the AIG for the window
711  p->iRoot = Odc_Const0();
712  Vec_PtrForEachEntry( Abc_Obj_t *, p->vRoots, pObj, i )
713  {
714  uData = (unsigned)(ABC_PTRUINT_T)Abc_NtkDontCareTransfer_rec( p, pObj, p->pNode );
715  // get the cofactors
716  uRes0 = uData & 0xffff;
717  uRes1 = uData >> 16;
718  // compute the miter
719 // assert( uRes0 != uRes1 ); // may be false if the node is redundant w.r.t. this root
720  uLit = Odc_Xor( p, uRes0, uRes1 );
721  p->iRoot = Odc_Or( p, p->iRoot, uLit );
722  }
723  return 1;
724 }
725 
726 
727 /**Function*************************************************************
728 
729  Synopsis [Recursively computes the pair of cofactors.]
730 
731  Description []
732 
733  SideEffects []
734 
735  SeeAlso []
736 
737 ***********************************************************************/
738 unsigned Abc_NtkDontCareCofactors_rec( Odc_Man_t * p, Odc_Lit_t Lit, unsigned uMask )
739 {
740  Odc_Obj_t * pObj;
741  unsigned uData0, uData1;
742  Odc_Lit_t uLit0, uLit1, uRes0, uRes1;
743  assert( !Odc_IsComplement(Lit) );
744  // skip visited objects
745  pObj = Odc_Lit2Obj( p, Lit );
746  if ( Odc_ObjIsTravIdCurrent(p, pObj) )
747  return pObj->uData;
748  Odc_ObjSetTravIdCurrent(p, pObj);
749  // skip objects out of the cone
750  if ( (pObj->uMask & uMask) == 0 )
751  return pObj->uData = ((Lit << 16) | Lit);
752  // consider the case when the node is the var
753  if ( pObj->uMask == uMask && Odc_IsTerm(p, Lit) )
754  return pObj->uData = ((Odc_Const1() << 16) | Odc_Const0());
755  // compute the cofactors
756  uData0 = Abc_NtkDontCareCofactors_rec( p, Odc_ObjFanin0(pObj), uMask );
757  uData1 = Abc_NtkDontCareCofactors_rec( p, Odc_ObjFanin1(pObj), uMask );
758  // find the 0-cofactor
759  uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 & 0xffff), Odc_ObjFaninC0(pObj) );
760  uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 & 0xffff), Odc_ObjFaninC1(pObj) );
761  uRes0 = Odc_And( p, uLit0, uLit1 );
762  // find the 1-cofactor
763  uLit0 = Odc_NotCond( (Odc_Lit_t)(uData0 >> 16), Odc_ObjFaninC0(pObj) );
764  uLit1 = Odc_NotCond( (Odc_Lit_t)(uData1 >> 16), Odc_ObjFaninC1(pObj) );
765  uRes1 = Odc_And( p, uLit0, uLit1 );
766  // find the result
767  return pObj->uData = ((uRes1 << 16) | uRes0);
768 }
769 
770 /**Function*************************************************************
771 
772  Synopsis [Quantifies the branch variables.]
773 
774  Description []
775 
776  SideEffects []
777 
778  SeeAlso []
779 
780 ***********************************************************************/
781 int Abc_NtkDontCareQuantify( Odc_Man_t * p )
782 {
783  Odc_Lit_t uRes0, uRes1;
784  unsigned uData;
785  int i;
786  assert( p->iRoot < 0xffff );
787  assert( Vec_PtrSize(p->vBranches) <= 32 ); // the mask size
788  for ( i = 0; i < Vec_PtrSize(p->vBranches); i++ )
789  {
790  // compute the cofactors w.r.t. this variable
791  Odc_ManIncrementTravId( p );
792  uData = Abc_NtkDontCareCofactors_rec( p, Odc_Regular(p->iRoot), (1 << i) );
793  uRes0 = Odc_NotCond( (Odc_Lit_t)(uData & 0xffff), Odc_IsComplement(p->iRoot) );
794  uRes1 = Odc_NotCond( (Odc_Lit_t)(uData >> 16), Odc_IsComplement(p->iRoot) );
795  // quantify this variable existentially
796  p->iRoot = Odc_Or( p, uRes0, uRes1 );
797  // check the limit
798  if ( Odc_ObjNum(p) > ABC_DC_MAX_NODES/2 )
799  return 0;
800  }
801  assert( p->nObjs <= p->nObjsAlloc );
802  return 1;
803 }
804 
805 
806 
807 /**Function*************************************************************
808 
809  Synopsis [Set elementary truth tables for PIs.]
810 
811  Description []
812 
813  SideEffects []
814 
815  SeeAlso []
816 
817 ***********************************************************************/
818 void Abc_NtkDontCareSimulateSetElem2( Odc_Man_t * p )
819 {
820  unsigned * pData;
821  int i, k;
822  for ( k = 0; k < p->nVarsMax; k++ )
823  {
824  pData = Odc_ObjTruth( p, Odc_Var(p, k) );
825  Abc_InfoClear( pData, p->nWords );
826  for ( i = 0; i < p->nBits; i++ )
827  if ( i & (1 << k) )
828  pData[i>>5] |= (1 << (i&31));
829  }
830 }
831 
832 /**Function*************************************************************
833 
834  Synopsis [Set elementary truth tables for PIs.]
835 
836  Description []
837 
838  SideEffects []
839 
840  SeeAlso []
841 
842 ***********************************************************************/
843 void Abc_NtkDontCareSimulateSetElem( Odc_Man_t * p )
844 {
845  unsigned * pData, * pData2;
846  int k;
847  for ( k = 0; k < p->nVarsMax; k++ )
848  {
849  pData = Odc_ObjTruth( p, Odc_Var(p, k) );
850  pData2 = (unsigned *)Vec_PtrEntry( p->vTruthsElem, k );
851  Abc_InfoCopy( pData, pData2, p->nWords );
852  }
853 }
854 
855 /**Function*************************************************************
856 
857  Synopsis [Set random simulation words for PIs.]
858 
859  Description []
860 
861  SideEffects []
862 
863  SeeAlso []
864 
865 ***********************************************************************/
866 void Abc_NtkDontCareSimulateSetRand( Odc_Man_t * p )
867 {
868  unsigned * pData;
869  int w, k, Number;
870  for ( w = 0; w < p->nWords; w++ )
871  {
872  Number = rand();
873  for ( k = 0; k < p->nVarsMax; k++ )
874  {
875  pData = Odc_ObjTruth( p, Odc_Var(p, k) );
876  pData[w] = (Number & (1<<k)) ? ~0 : 0;
877  }
878  }
879 }
880 
881 /**Function*************************************************************
882 
883  Synopsis [Set random simulation words for PIs.]
884 
885  Description []
886 
887  SideEffects []
888 
889  SeeAlso []
890 
891 ***********************************************************************/
892 int Abc_NtkDontCareCountMintsWord( Odc_Man_t * p, unsigned * puTruth )
893 {
894  int w, Counter = 0;
895  for ( w = 0; w < p->nWords; w++ )
896  if ( puTruth[w] )
897  Counter++;
898  return Counter;
899 }
900 
901 /**Function*************************************************************
902 
903  Synopsis [Simulates one node.]
904 
905  Description []
906 
907  SideEffects []
908 
909  SeeAlso []
910 
911 ***********************************************************************/
912 void Abc_NtkDontCareTruthOne( Odc_Man_t * p, Odc_Lit_t Lit )
913 {
914  Odc_Obj_t * pObj;
915  unsigned * pInfo, * pInfo1, * pInfo2;
916  int k, fComp1, fComp2;
917  assert( !Odc_IsComplement( Lit ) );
918  assert( !Odc_IsTerm( p, Lit ) );
919  // get the truth tables
920  pObj = Odc_Lit2Obj( p, Lit );
921  pInfo = Odc_ObjTruth( p, Lit );
922  pInfo1 = Odc_ObjTruth( p, Odc_ObjFanin0(pObj) );
923  pInfo2 = Odc_ObjTruth( p, Odc_ObjFanin1(pObj) );
924  fComp1 = Odc_ObjFaninC0( pObj );
925  fComp2 = Odc_ObjFaninC1( pObj );
926  // simulate
927  if ( fComp1 && fComp2 )
928  for ( k = 0; k < p->nWords; k++ )
929  pInfo[k] = ~pInfo1[k] & ~pInfo2[k];
930  else if ( fComp1 && !fComp2 )
931  for ( k = 0; k < p->nWords; k++ )
932  pInfo[k] = ~pInfo1[k] & pInfo2[k];
933  else if ( !fComp1 && fComp2 )
934  for ( k = 0; k < p->nWords; k++ )
935  pInfo[k] = pInfo1[k] & ~pInfo2[k];
936  else // if ( fComp1 && fComp2 )
937  for ( k = 0; k < p->nWords; k++ )
938  pInfo[k] = pInfo1[k] & pInfo2[k];
939 }
940 
941 /**Function*************************************************************
942 
943  Synopsis [Computes the truth table.]
944 
945  Description []
946 
947  SideEffects []
948 
949  SeeAlso []
950 
951 ***********************************************************************/
952 void Abc_NtkDontCareSimulate_rec( Odc_Man_t * p, Odc_Lit_t Lit )
953 {
954  Odc_Obj_t * pObj;
955  assert( !Odc_IsComplement(Lit) );
956  // skip terminals
957  if ( Odc_IsTerm(p, Lit) )
958  return;
959  // skip visited objects
960  pObj = Odc_Lit2Obj( p, Lit );
961  if ( Odc_ObjIsTravIdCurrent(p, pObj) )
962  return;
963  Odc_ObjSetTravIdCurrent(p, pObj);
964  // call recursively
965  Abc_NtkDontCareSimulate_rec( p, Odc_ObjFanin0(pObj) );
966  Abc_NtkDontCareSimulate_rec( p, Odc_ObjFanin1(pObj) );
967  // construct the truth table
968  Abc_NtkDontCareTruthOne( p, Lit );
969 }
970 
971 /**Function*************************************************************
972 
973  Synopsis [Computes the truth table of the care set.]
974 
975  Description [Returns the number of ones in the simulation info.]
976 
977  SideEffects []
978 
979  SeeAlso []
980 
981 ***********************************************************************/
982 int Abc_NtkDontCareSimulate( Odc_Man_t * p, unsigned * puTruth )
983 {
984  Odc_ManIncrementTravId( p );
985  Abc_NtkDontCareSimulate_rec( p, Odc_Regular(p->iRoot) );
986  Abc_InfoCopy( puTruth, Odc_ObjTruth(p, Odc_Regular(p->iRoot)), p->nWords );
987  if ( Odc_IsComplement(p->iRoot) )
988  Abc_InfoNot( puTruth, p->nWords );
989  return Extra_TruthCountOnes( puTruth, p->nVarsMax );
990 }
991 
992 /**Function*************************************************************
993 
994  Synopsis [Computes the truth table of the care set.]
995 
996  Description [Returns the number of ones in the simulation info.]
997 
998  SideEffects []
999 
1000  SeeAlso []
1001 
1002 ***********************************************************************/
1003 int Abc_NtkDontCareSimulateBefore( Odc_Man_t * p, unsigned * puTruth )
1004 {
1005  int nIters = 2;
1006  int nRounds, Counter, r;
1007  // decide how many rounds to simulate
1008  nRounds = p->nBits / p->nWords;
1009  Counter = 0;
1010  for ( r = 0; r < nIters; r++ )
1011  {
1012  Abc_NtkDontCareSimulateSetRand( p );
1013  Abc_NtkDontCareSimulate( p, puTruth );
1014  Counter += Abc_NtkDontCareCountMintsWord( p, puTruth );
1015  }
1016  // normalize
1017  Counter = Counter * nRounds / nIters;
1018  return Counter;
1019 }
1020 
1021 /**Function*************************************************************
1022 
1023  Synopsis [Computes ODCs for the node in terms of the cut variables.]
1024 
1025  Description [Returns the number of don't care minterms in the truth table.
1026  In particular, this procedure returns 0 if there is no don't-cares.]
1027 
1028  SideEffects []
1029 
1030  SeeAlso []
1031 
1032 ***********************************************************************/
1033 int Abc_NtkDontCareCompute( Odc_Man_t * p, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, unsigned * puTruth )
1034 {
1035  int nMints, RetValue;
1036  abctime clk, clkTotal = Abc_Clock();
1037 
1038  p->nWins++;
1039 
1040  // set the parameters
1041  assert( !Abc_ObjIsComplement(pNode) );
1042  assert( Abc_ObjIsNode(pNode) );
1043  assert( Vec_PtrSize(vLeaves) <= p->nVarsMax );
1044  p->vLeaves = vLeaves;
1045  p->pNode = pNode;
1046 
1047  // compute the window
1048 clk = Abc_Clock();
1049  RetValue = Abc_NtkDontCareWindow( p );
1050 p->timeWin += Abc_Clock() - clk;
1051  if ( !RetValue )
1052  {
1053 p->timeAbort += Abc_Clock() - clkTotal;
1054  Abc_InfoFill( puTruth, p->nWords );
1055  p->nWinsEmpty++;
1056  return 0;
1057  }
1058 
1059  if ( p->fVeryVerbose )
1060  {
1061  printf( " %5d : ", pNode->Id );
1062  printf( "Leaf = %2d ", Vec_PtrSize(p->vLeaves) );
1063  printf( "Root = %2d ", Vec_PtrSize(p->vRoots) );
1064  printf( "Bran = %2d ", Vec_PtrSize(p->vBranches) );
1065  printf( " | " );
1066  }
1067 
1068  // transfer the window into the AIG package
1069 clk = Abc_Clock();
1070  Abc_NtkDontCareTransfer( p );
1071 p->timeMiter += Abc_Clock() - clk;
1072 
1073  // simulate to estimate the amount of don't-cares
1074 clk = Abc_Clock();
1075  nMints = Abc_NtkDontCareSimulateBefore( p, puTruth );
1076 p->timeSim += Abc_Clock() - clk;
1077  if ( p->fVeryVerbose )
1078  {
1079  printf( "AIG = %5d ", Odc_NodeNum(p) );
1080  printf( "%6.2f %% ", 100.0 * (p->nBits - nMints) / p->nBits );
1081  }
1082 
1083  // if there is less then the given percentage of don't-cares, skip
1084  if ( 100.0 * (p->nBits - nMints) / p->nBits < 1.0 * p->nPercCutoff )
1085  {
1086 p->timeAbort += Abc_Clock() - clkTotal;
1087  if ( p->fVeryVerbose )
1088  printf( "Simulation cutoff.\n" );
1089  Abc_InfoFill( puTruth, p->nWords );
1090  p->nSimsEmpty++;
1091  return 0;
1092  }
1093 
1094  // quantify external variables
1095 clk = Abc_Clock();
1096  RetValue = Abc_NtkDontCareQuantify( p );
1097 p->timeQuant += Abc_Clock() - clk;
1098  if ( !RetValue )
1099  {
1100 p->timeAbort += Abc_Clock() - clkTotal;
1101  if ( p->fVeryVerbose )
1102  printf( "=== Overflow! ===\n" );
1103  Abc_InfoFill( puTruth, p->nWords );
1104  p->nQuantsOver++;
1105  return 0;
1106  }
1107 
1108  // get the truth table
1109 clk = Abc_Clock();
1110  Abc_NtkDontCareSimulateSetElem( p );
1111  nMints = Abc_NtkDontCareSimulate( p, puTruth );
1112 p->timeTruth += Abc_Clock() - clk;
1113  if ( p->fVeryVerbose )
1114  {
1115  printf( "AIG = %5d ", Odc_NodeNum(p) );
1116  printf( "%6.2f %% ", 100.0 * (p->nBits - nMints) / p->nBits );
1117  printf( "\n" );
1118  }
1119 p->timeTotal += Abc_Clock() - clkTotal;
1120  p->nWinsFinish++;
1121  p->nTotalDcs += (int)(100.0 * (p->nBits - nMints) / p->nBits);
1122  return nMints;
1123 }
1124 
1125 
1126 ////////////////////////////////////////////////////////////////////////
1127 /// END OF FILE ///
1128 ////////////////////////////////////////////////////////////////////////
1129 
1130 
1131 ABC_NAMESPACE_IMPL_END
1132 
memset
char * memset()
Abc_NtkDontCareSimulate_rec
void Abc_NtkDontCareSimulate_rec(Odc_Man_t *p, Odc_Lit_t Lit)
Definition: abcOdc.c:952
Odc_Man_t_::vBranches
Vec_Ptr_t * vBranches
Definition: abcOdc.c:58
Abc_NtkDontCareSimulate
int Abc_NtkDontCareSimulate(Odc_Man_t *p, unsigned *puTruth)
Definition: abcOdc.c:982
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Odc_ObjNew
static Odc_Obj_t * Odc_ObjNew(Odc_Man_t *p)
Definition: abcOdc.c:119
Abc_ObjFanin1
static Abc_Obj_t * Abc_ObjFanin1(Abc_Obj_t *pObj)
Definition: abc.h:374
Odc_ObjNum
static int Odc_ObjNum(Odc_Man_t *p)
Definition: abcOdc.c:103
Abc_ObjIsCi
static int Abc_ObjIsCi(Abc_Obj_t *pObj)
Definition: abc.h:351
Odc_Obj_t_::uMask
unsigned uMask
Definition: abcOdc.c:42
Abc_NtkDontCareWindow
int Abc_NtkDontCareWindow(Odc_Man_t *p)
Definition: abcOdc.c:477
Odc_ObjTruth
static unsigned * Odc_ObjTruth(Odc_Man_t *p, Odc_Lit_t Lit)
Definition: abcOdc.c:137
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Odc_Man_t_::nVarsMax
int nVarsMax
Definition: abcOdc.c:48
Abc_NtkDontCareTransfer_rec
void * Abc_NtkDontCareTransfer_rec(Odc_Man_t *p, Abc_Obj_t *pNode, Abc_Obj_t *pPivot)
Definition: abcOdc.c:649
Abc_ObjFaninC1
static int Abc_ObjFaninC1(Abc_Obj_t *pObj)
Definition: abc.h:378
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_PtrPushUnique
static int Vec_PtrPushUnique(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:656
Odc_Or
static Odc_Lit_t Odc_Or(Odc_Man_t *p, Odc_Lit_t iFan0, Odc_Lit_t iFan1)
Definition: abcOdc.c:613
Odc_Man_t_::nTravIds
unsigned short nTravIds
Definition: abcOdc.c:67
Odc_Man_t_::pNode
Abc_Obj_t * pNode
Definition: abcOdc.c:55
Abc_ObjFanoutNum
static int Abc_ObjFanoutNum(Abc_Obj_t *pObj)
Definition: abc.h:365
Odc_Not
static Odc_Lit_t Odc_Not(Odc_Lit_t Lit)
Definition: abcOdc.c:108
Odc_Var
static Odc_Lit_t Odc_Var(Odc_Man_t *p, int i)
Definition: abcOdc.c:114
Odc_Man_t_::timeTruth
abctime timeTruth
Definition: abcOdc.c:94
Odc_ObjSetTravIdCurrent
static void Odc_ObjSetTravIdCurrent(Odc_Man_t *p, Odc_Obj_t *pObj)
Definition: abcOdc.c:133
Abc_InfoFill
static void Abc_InfoFill(unsigned *p, int nWords)
Definition: abc.h:237
Abc_NtkDontCareCofactors_rec
unsigned Abc_NtkDontCareCofactors_rec(Odc_Man_t *p, Odc_Lit_t Lit, unsigned uMask)
Definition: abcOdc.c:738
Odc_Obj_t_::TravId
unsigned short TravId
Definition: abcOdc.c:40
Odc_Obj_t_::iFan0
Odc_Lit_t iFan0
Definition: abcOdc.c:37
ABC_DC_MAX_NODES
#define ABC_DC_MAX_NODES
DECLARATIONS ///.
Definition: abcOdc.c:30
Odc_Man_t_::vLeaves
Vec_Ptr_t * vLeaves
Definition: abcOdc.c:56
Odc_Man_t_::timeTotal
abctime timeTotal
Definition: abcOdc.c:95
Abc_ObjFaninC0
static int Abc_ObjFaninC0(Abc_Obj_t *pObj)
Definition: abc.h:377
Odc_NodeNum
static int Odc_NodeNum(Odc_Man_t *p)
Definition: abcOdc.c:102
Abc_NtkDontCareWinAddMissing
int Abc_NtkDontCareWinAddMissing(Odc_Man_t *p)
Definition: abcOdc.c:450
Odc_Man_t_::nTotalDcs
int nTotalDcs
Definition: abcOdc.c:86
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Odc_ObjFanin1
static Odc_Lit_t Odc_ObjFanin1(Odc_Obj_t *pObj)
Definition: abcOdc.c:127
Odc_Man_t_::nWinsEmpty
int nWinsEmpty
Definition: abcOdc.c:82
Odc_ObjChild1
static Odc_Lit_t Odc_ObjChild1(Odc_Obj_t *pObj)
Definition: abcOdc.c:125
Odc_Man_t_::fVerbose
int fVerbose
Definition: abcOdc.c:50
Odc_Man_t_::timeWin
abctime timeWin
Definition: abcOdc.c:90
Odc_Man_t_::fVeryVerbose
int fVeryVerbose
Definition: abcOdc.c:51
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Abc_TruthWordNum
static int Abc_TruthWordNum(int nVars)
Definition: abc_global.h:256
Odc_Lit2Obj
static Odc_Obj_t * Odc_Lit2Obj(Odc_Man_t *p, Odc_Lit_t Lit)
Definition: abcOdc.c:121
Odc_NotCond
static Odc_Lit_t Odc_NotCond(Odc_Lit_t Lit, int c)
Definition: abcOdc.c:109
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_NodeIsTravIdPrevious
static int Abc_NodeIsTravIdPrevious(Abc_Obj_t *p)
Definition: abc.h:412
Odc_Man_t_::timeMiter
abctime timeMiter
Definition: abcOdc.c:91
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Odc_Man_t_::nPis
int nPis
Definition: abcOdc.c:62
Abc_NtkDontCareCountMintsWord
int Abc_NtkDontCareCountMintsWord(Odc_Man_t *p, unsigned *puTruth)
Definition: abcOdc.c:892
Abc_ObjFanin0
static Abc_Obj_t * Abc_ObjFanin0(Abc_Obj_t *pObj)
Definition: abc.h:373
Odc_Man_t_::timeAbort
abctime timeAbort
Definition: abcOdc.c:96
Odc_HashKey
static unsigned Odc_HashKey(Odc_Lit_t iFan0, Odc_Lit_t iFan1, int TableSize)
Definition: abcOdc.c:512
Abc_Obj_t_::Level
unsigned Level
Definition: abc.h:142
Abc_ObjIsCo
static int Abc_ObjIsCo(Abc_Obj_t *pObj)
Definition: abc.h:352
Odc_Man_t_::iRoot
Odc_Lit_t iRoot
Definition: abcOdc.c:66
Abc_Obj_t_
Definition: abc.h:128
Abc_InfoNot
static void Abc_InfoNot(unsigned *p, int nWords)
Definition: abc.h:238
Abc_NtkDontCareCompute
int Abc_NtkDontCareCompute(Odc_Man_t *p, Abc_Obj_t *pNode, Vec_Ptr_t *vLeaves, unsigned *puTruth)
Definition: abcOdc.c:1033
Abc_ObjIsNode
static int Abc_ObjIsNode(Abc_Obj_t *pObj)
Definition: abc.h:355
Odc_ObjFanin0
static Odc_Lit_t Odc_ObjFanin0(Odc_Obj_t *pObj)
Definition: abcOdc.c:126
Odc_Obj_t_::iNext
Odc_Lit_t iNext
Definition: abcOdc.c:39
Abc_Obj_t_::pCopy
Abc_Obj_t * pCopy
Definition: abc.h:148
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Abc_NtkDontCareTransfer
int Abc_NtkDontCareTransfer(Odc_Man_t *p)
Definition: abcOdc.c:688
Abc_InfoCopy
static void Abc_InfoCopy(unsigned *p, unsigned *q, int nWords)
Definition: abc.h:241
Odc_ObjChild0
static Odc_Lit_t Odc_ObjChild0(Odc_Obj_t *pObj)
Definition: abcOdc.c:124
Odc_Man_t_::nSimsEmpty
int nSimsEmpty
Definition: abcOdc.c:83
Abc_NtkDontCareSimulateSetRand
void Abc_NtkDontCareSimulateSetRand(Odc_Man_t *p)
Definition: abcOdc.c:866
Abc_NtkDontCareQuantify
int Abc_NtkDontCareQuantify(Odc_Man_t *p)
Definition: abcOdc.c:781
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Odc_Man_t_::nPercCutoff
int nPercCutoff
Definition: abcOdc.c:52
Odc_Man_t_::timeSim
abctime timeSim
Definition: abcOdc.c:92
Abc_NtkDontCareWinCollectRoots_rec
void Abc_NtkDontCareWinCollectRoots_rec(Abc_Obj_t *pObj, Vec_Ptr_t *vRoots)
Definition: abcOdc.c:364
Extra_TruthCountOnes
static int Extra_TruthCountOnes(unsigned *pIn, int nVars)
Definition: extra.h:263
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Abc_NtkDontCareWinSweepLeafTfo_rec
void Abc_NtkDontCareWinSweepLeafTfo_rec(Abc_Obj_t *pObj, int nLevelLimit, Abc_Obj_t *pNode)
Definition: abcOdc.c:315
Counter
static int Counter
Definition: extraBddMisc.c:1877
Odc_Man_t_::nObjs
int nObjs
Definition: abcOdc.c:63
Odc_Obj_t_::uData
unsigned uData
Definition: abcOdc.c:41
Abc_InfoClear
static void Abc_InfoClear(unsigned *p, int nWords)
Definition: abc.h:236
Odc_IsComplement
static int Odc_IsComplement(Odc_Lit_t Lit)
Definition: abcOdc.c:106
Odc_HashLookup
static Odc_Lit_t * Odc_HashLookup(Odc_Man_t *p, Odc_Lit_t iFan0, Odc_Lit_t iFan1)
Definition: abcOdc.c:533
Abc_NtkDontCareWinAddMissing_rec
int Abc_NtkDontCareWinAddMissing_rec(Odc_Man_t *p, Abc_Obj_t *pObj)
Definition: abcOdc.c:418
Odc_Regular
static Odc_Lit_t Odc_Regular(Odc_Lit_t Lit)
Definition: abcOdc.c:107
Odc_Man_t_::timeQuant
abctime timeQuant
Definition: abcOdc.c:93
Odc_Obj2Lit
static Odc_Lit_t Odc_Obj2Lit(Odc_Man_t *p, Odc_Obj_t *pObj)
Definition: abcOdc.c:120
Abc_NtkDontCareWinSweepLeafTfo
void Abc_NtkDontCareWinSweepLeafTfo(Odc_Man_t *p)
Definition: abcOdc.c:344
Odc_IsConst
static int Odc_IsConst(Odc_Lit_t Lit)
Definition: abcOdc.c:115
Abc_NtkDontCareSimulateBefore
int Abc_NtkDontCareSimulateBefore(Odc_Man_t *p, unsigned *puTruth)
Definition: abcOdc.c:1003
Abc_NtkDontCareAlloc
Odc_Man_t * Abc_NtkDontCareAlloc(int nVarsMax, int nLevels, int fVerbose, int fVeryVerbose)
FUNCTION DEFINITIONS ///.
Definition: abcOdc.c:162
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Odc_Const0
static Odc_Lit_t Odc_Const0()
Definition: abcOdc.c:112
Odc_And
static Odc_Lit_t Odc_And(Odc_Man_t *p, Odc_Lit_t iFan0, Odc_Lit_t iFan1)
Definition: abcOdc.c:565
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Odc_Man_t_::vTruths
Vec_Ptr_t * vTruths
Definition: abcOdc.c:76
Abc_NtkDontCareTruthOne
void Abc_NtkDontCareTruthOne(Odc_Man_t *p, Odc_Lit_t Lit)
Definition: abcOdc.c:912
Abc_NodeIsTravIdCurrent
static int Abc_NodeIsTravIdCurrent(Abc_Obj_t *p)
Definition: abc.h:411
Odc_IsTerm
static int Odc_IsTerm(Odc_Man_t *p, Odc_Lit_t Lit)
Definition: abcOdc.c:116
Odc_Man_t_::nBits
int nBits
Definition: abcOdc.c:74
Odc_ObjFaninC1
static int Odc_ObjFaninC1(Odc_Obj_t *pObj)
Definition: abcOdc.c:129
Abc_NtkDontCareClear
void Abc_NtkDontCareClear(Odc_Man_t *p)
Definition: abcOdc.c:242
Abc_Obj_t_::pNtk
Abc_Ntk_t * pNtk
Definition: abc.h:130
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Abc_ObjForEachFanout
#define Abc_ObjForEachFanout(pObj, pFanout, i)
Definition: abc.h:526
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Odc_Man_t_::nWins
int nWins
Definition: abcOdc.c:81
Abc_ObjForEachFanin
#define Abc_ObjForEachFanin(pObj, pFanin, i)
Definition: abc.h:524
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Odc_Xor
static Odc_Lit_t Odc_Xor(Odc_Man_t *p, Odc_Lit_t iFan0, Odc_Lit_t iFan1)
Definition: abcOdc.c:629
Abc_Obj_t_::Id
int Id
Definition: abc.h:132
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Odc_Man_t_::nQuantsOver
int nQuantsOver
Definition: abcOdc.c:84
Abc_NtkDontCareSimulateSetElem
void Abc_NtkDontCareSimulateSetElem(Odc_Man_t *p)
Definition: abcOdc.c:843
Abc_NtkIncrementTravId
static void Abc_NtkIncrementTravId(Abc_Ntk_t *p)
Definition: abc.h:406
Odc_ObjIsTravIdCurrent
static int Odc_ObjIsTravIdCurrent(Odc_Man_t *p, Odc_Obj_t *pObj)
Definition: abcOdc.c:134
Odc_Man_t_::puTruth
unsigned * puTruth
Definition: abcOdc.c:78
Odc_Man_t_::vRoots
Vec_Ptr_t * vRoots
Definition: abcOdc.c:57
Abc_NtkDontCareSimulateSetElem2
void Abc_NtkDontCareSimulateSetElem2(Odc_Man_t *p)
Definition: abcOdc.c:818
Abc_NtkDontCareWinCollectRoots
void Abc_NtkDontCareWinCollectRoots(Odc_Man_t *p)
Definition: abcOdc.c:397
Odc_ManIncrementTravId
static void Odc_ManIncrementTravId(Odc_Man_t *p)
Definition: abcOdc.c:132
Odc_Man_t_::vTruthsElem
Vec_Ptr_t * vTruthsElem
Definition: abcOdc.c:77
Odc_Man_t_::pObjs
Odc_Obj_t * pObjs
Definition: abcOdc.c:65
assert
#define assert(ex)
Definition: util_old.h:213
Vec_PtrClear
static void Vec_PtrClear(Vec_Ptr_t *p)
Definition: vecPtr.h:545
Odc_Man_t_
Definition: abcOdc.c:45
Abc_NtkDontCareFree
void Abc_NtkDontCareFree(Odc_Man_t *p)
Definition: abcOdc.c:274
Abc_InfoRandom
static void Abc_InfoRandom(unsigned *p, int nWords)
Definition: abc.h:235
Odc_Man_t_::nObjsAlloc
int nObjsAlloc
Definition: abcOdc.c:64
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
Abc_ObjIsComplement
static int Abc_ObjIsComplement(Abc_Obj_t *p)
Definition: abc.h:322
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Odc_ObjFaninC0
static int Odc_ObjFaninC0(Odc_Obj_t *pObj)
Definition: abcOdc.c:128
Odc_Man_t_::nWinsFinish
int nWinsFinish
Definition: abcOdc.c:85
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Odc_Man_t_::timeClean
abctime timeClean
Definition: abcOdc.c:89
Odc_Const1
static Odc_Lit_t Odc_Const1()
Definition: abcOdc.c:113
Odc_Obj_t_
Definition: abcOdc.c:35
Odc_Man_t_::pTable
Odc_Lit_t * pTable
Definition: abcOdc.c:69
Odc_Lit_t
unsigned short Odc_Lit_t
Definition: abcOdc.c:32
Odc_Man_t_::vUsedSpots
Vec_Int_t * vUsedSpots
Definition: abcOdc.c:71
Odc_Man_t_::nLevels
int nLevels
Definition: abcOdc.c:49
Odc_Man_t_::nTableSize
int nTableSize
Definition: abcOdc.c:70
Odc_Obj_t_::iFan1
Odc_Lit_t iFan1
Definition: abcOdc.c:38
Vec_PtrAllocSimInfo
static Vec_Ptr_t * Vec_PtrAllocSimInfo(int nEntries, int nWords)
Definition: vecPtr.h:929
Abc_NodeSetTravIdCurrent
static void Abc_NodeSetTravIdCurrent(Abc_Obj_t *p)
Definition: abc.h:409
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Odc_PiNum
static int Odc_PiNum(Odc_Man_t *p)
Definition: abcOdc.c:101
Odc_Man_t_::nWords
int nWords
Definition: abcOdc.c:75