abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
cecPat.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [cecPat.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [Combinational equivalence checking.]
8 
9  Synopsis [Simulation pattern manager.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: cecPat.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "cecInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 /**Function*************************************************************
35 
36  Synopsis []
37 
38  Description []
39 
40  SideEffects []
41 
42  SeeAlso []
43 
44 ***********************************************************************/
45 static inline void Cec_ManPatStoreNum( Cec_ManPat_t * p, int Num )
46 {
47  unsigned x = (unsigned)Num;
48  assert( Num >= 0 );
49  while ( x & ~0x7f )
50  {
51  Vec_StrPush( p->vStorage, (char)((x & 0x7f) | 0x80) );
52  x >>= 7;
53  }
54  Vec_StrPush( p->vStorage, (char)x );
55 }
56 
57 /**Function*************************************************************
58 
59  Synopsis []
60 
61  Description []
62 
63  SideEffects []
64 
65  SeeAlso []
66 
67 ***********************************************************************/
68 static inline int Cec_ManPatRestoreNum( Cec_ManPat_t * p )
69 {
70  int ch, i, x = 0;
71  for ( i = 0; (ch = Vec_StrEntry(p->vStorage, p->iStart++)) & 0x80; i++ )
72  x |= (ch & 0x7f) << (7 * i);
73  return x | (ch << (7 * i));
74 }
75 
76 /**Function*************************************************************
77 
78  Synopsis []
79 
80  Description []
81 
82  SideEffects []
83 
84  SeeAlso []
85 
86 ***********************************************************************/
87 static inline void Cec_ManPatStore( Cec_ManPat_t * p, Vec_Int_t * vPat )
88 {
89  int i, Number, NumberPrev;
90  assert( Vec_IntSize(vPat) > 0 );
91  Cec_ManPatStoreNum( p, Vec_IntSize(vPat) );
92  NumberPrev = Vec_IntEntry( vPat, 0 );
93  Cec_ManPatStoreNum( p, NumberPrev );
94  Vec_IntForEachEntryStart( vPat, Number, i, 1 )
95  {
96  assert( NumberPrev < Number );
97  Cec_ManPatStoreNum( p, Number - NumberPrev );
98  NumberPrev = Number;
99  }
100 }
101 
102 /**Function*************************************************************
103 
104  Synopsis []
105 
106  Description []
107 
108  SideEffects []
109 
110  SeeAlso []
111 
112 ***********************************************************************/
113 static inline void Cec_ManPatRestore( Cec_ManPat_t * p, Vec_Int_t * vPat )
114 {
115  int i, Size, Number;
116  Vec_IntClear( vPat );
117  Size = Cec_ManPatRestoreNum( p );
118  Number = Cec_ManPatRestoreNum( p );
119  Vec_IntPush( vPat, Number );
120  for ( i = 1; i < Size; i++ )
121  {
122  Number += Cec_ManPatRestoreNum( p );
123  Vec_IntPush( vPat, Number );
124  }
125  assert( Vec_IntSize(vPat) == Size );
126 }
127 
128 
129 /**Function*************************************************************
130 
131  Synopsis [Derives satisfying assignment.]
132 
133  Description []
134 
135  SideEffects []
136 
137  SeeAlso []
138 
139 ***********************************************************************/
140 int Cec_ManPatComputePattern_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj )
141 {
142  int Counter = 0;
143  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
144  return 0;
145  Gia_ObjSetTravIdCurrent(p, pObj);
146  if ( Gia_ObjIsCi(pObj) )
147  {
148  pObj->fMark1 = Cec_ObjSatVarValue( pSat, pObj );
149  return 1;
150  }
151  assert( Gia_ObjIsAnd(pObj) );
152  Counter += Cec_ManPatComputePattern_rec( pSat, p, Gia_ObjFanin0(pObj) );
153  Counter += Cec_ManPatComputePattern_rec( pSat, p, Gia_ObjFanin1(pObj) );
154  pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) &
155  (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj));
156  return Counter;
157 }
158 
159 /**Function*************************************************************
160 
161  Synopsis [Derives satisfying assignment.]
162 
163  Description []
164 
165  SideEffects []
166 
167  SeeAlso []
168 
169 ***********************************************************************/
170 void Cec_ManPatComputePattern1_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPat )
171 {
172  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
173  return;
174  Gia_ObjSetTravIdCurrent(p, pObj);
175  if ( Gia_ObjIsCi(pObj) )
176  {
177  Vec_IntPush( vPat, Abc_Var2Lit( Gia_ObjCioId(pObj), pObj->fMark1==0 ) );
178  return;
179  }
180  assert( Gia_ObjIsAnd(pObj) );
181  if ( pObj->fMark1 == 1 )
182  {
183  Cec_ManPatComputePattern1_rec( p, Gia_ObjFanin0(pObj), vPat );
184  Cec_ManPatComputePattern1_rec( p, Gia_ObjFanin1(pObj), vPat );
185  }
186  else
187  {
188  assert( (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) == 0 ||
189  (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj)) == 0 );
190  if ( (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) == 0 )
191  Cec_ManPatComputePattern1_rec( p, Gia_ObjFanin0(pObj), vPat );
192  else
193  Cec_ManPatComputePattern1_rec( p, Gia_ObjFanin1(pObj), vPat );
194  }
195 }
196 
197 /**Function*************************************************************
198 
199  Synopsis [Derives satisfying assignment.]
200 
201  Description []
202 
203  SideEffects []
204 
205  SeeAlso []
206 
207 ***********************************************************************/
208 void Cec_ManPatComputePattern2_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPat )
209 {
210  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
211  return;
212  Gia_ObjSetTravIdCurrent(p, pObj);
213  if ( Gia_ObjIsCi(pObj) )
214  {
215  Vec_IntPush( vPat, Abc_Var2Lit( Gia_ObjCioId(pObj), pObj->fMark1==0 ) );
216  return;
217  }
218  assert( Gia_ObjIsAnd(pObj) );
219  if ( pObj->fMark1 == 1 )
220  {
221  Cec_ManPatComputePattern2_rec( p, Gia_ObjFanin0(pObj), vPat );
222  Cec_ManPatComputePattern2_rec( p, Gia_ObjFanin1(pObj), vPat );
223  }
224  else
225  {
226  assert( (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) == 0 ||
227  (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj)) == 0 );
228  if ( (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj)) == 0 )
229  Cec_ManPatComputePattern2_rec( p, Gia_ObjFanin1(pObj), vPat );
230  else
231  Cec_ManPatComputePattern2_rec( p, Gia_ObjFanin0(pObj), vPat );
232  }
233 }
234 
235 /**Function*************************************************************
236 
237  Synopsis [Derives satisfying assignment.]
238 
239  Description []
240 
241  SideEffects []
242 
243  SeeAlso []
244 
245 ***********************************************************************/
246 int Cec_ManPatComputePattern3_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
247 {
248  int Value0, Value1, Value;
249  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
250  return (pObj->fMark1 << 1) | pObj->fMark0;
251  Gia_ObjSetTravIdCurrent(p, pObj);
252  if ( Gia_ObjIsCi(pObj) )
253  {
254  pObj->fMark0 = 1;
255  pObj->fMark1 = 1;
256  return GIA_UND;
257  }
258  assert( Gia_ObjIsAnd(pObj) );
259  Value0 = Cec_ManPatComputePattern3_rec( p, Gia_ObjFanin0(pObj) );
260  Value1 = Cec_ManPatComputePattern3_rec( p, Gia_ObjFanin1(pObj) );
261  Value = Gia_XsimAndCond( Value0, Gia_ObjFaninC0(pObj), Value1, Gia_ObjFaninC1(pObj) );
262  pObj->fMark0 = (Value & 1);
263  pObj->fMark1 = ((Value >> 1) & 1);
264  return Value;
265 }
266 
267 /**Function*************************************************************
268 
269  Synopsis [Derives satisfying assignment.]
270 
271  Description []
272 
273  SideEffects []
274 
275  SeeAlso []
276 
277 ***********************************************************************/
278 void Cec_ManPatVerifyPattern( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vPat )
279 {
280  Gia_Obj_t * pTemp;
281  int i, Value;
282  Gia_ManIncrementTravId( p );
283  Vec_IntForEachEntry( vPat, Value, i )
284  {
285  pTemp = Gia_ManCi( p, Abc_Lit2Var(Value) );
286 // assert( Abc_LitIsCompl(Value) != (int)pTemp->fMark1 );
287  if ( pTemp->fMark1 )
288  {
289  pTemp->fMark0 = 0;
290  pTemp->fMark1 = 1;
291  }
292  else
293  {
294  pTemp->fMark0 = 1;
295  pTemp->fMark1 = 0;
296  }
297  Gia_ObjSetTravIdCurrent( p, pTemp );
298  }
299  Value = Cec_ManPatComputePattern3_rec( p, Gia_ObjFanin0(pObj) );
300  Value = Gia_XsimNotCond( Value, Gia_ObjFaninC0(pObj) );
301  if ( Value != GIA_ONE )
302  Abc_Print( 1, "Cec_ManPatVerifyPattern(): Verification failed.\n" );
303  assert( Value == GIA_ONE );
304 }
305 
306 /**Function*************************************************************
307 
308  Synopsis []
309 
310  Description []
311 
312  SideEffects []
313 
314  SeeAlso []
315 
316 ***********************************************************************/
317 void Cec_ManPatComputePattern4_rec( Gia_Man_t * p, Gia_Obj_t * pObj )
318 {
319  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
320  return;
321  Gia_ObjSetTravIdCurrent(p, pObj);
322  pObj->fMark0 = 0;
323  if ( Gia_ObjIsCi(pObj) )
324  return;
325  assert( Gia_ObjIsAnd(pObj) );
326  Cec_ManPatComputePattern4_rec( p, Gia_ObjFanin0(pObj) );
327  Cec_ManPatComputePattern4_rec( p, Gia_ObjFanin1(pObj) );
328 }
329 
330 /**Function*************************************************************
331 
332  Synopsis []
333 
334  Description []
335 
336  SideEffects []
337 
338  SeeAlso []
339 
340 ***********************************************************************/
341 void Cec_ManPatCleanMark0( Gia_Man_t * p, Gia_Obj_t * pObj )
342 {
343  assert( Gia_ObjIsCo(pObj) );
344  Gia_ManIncrementTravId( p );
345  Cec_ManPatComputePattern4_rec( p, Gia_ObjFanin0(pObj) );
346 }
347 
348 /**Function*************************************************************
349 
350  Synopsis []
351 
352  Description []
353 
354  SideEffects []
355 
356  SeeAlso []
357 
358 ***********************************************************************/
359 void Cec_ManPatSavePattern( Cec_ManPat_t * pMan, Cec_ManSat_t * p, Gia_Obj_t * pObj )
360 {
361  Vec_Int_t * vPat;
362  int nPatLits;
363  abctime clkTotal = Abc_Clock();
364 // abctime clk;
365  assert( Gia_ObjIsCo(pObj) );
366  pMan->nPats++;
367  pMan->nPatsAll++;
368  // compute values in the cone of influence
369 //clk = Abc_Clock();
370  Gia_ManIncrementTravId( p->pAig );
371  nPatLits = Cec_ManPatComputePattern_rec( p, p->pAig, Gia_ObjFanin0(pObj) );
372  assert( (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) == 1 );
373  pMan->nPatLits += nPatLits;
374  pMan->nPatLitsAll += nPatLits;
375 //pMan->timeFind += Abc_Clock() - clk;
376  // compute sensitizing path
377 //clk = Abc_Clock();
378  Vec_IntClear( pMan->vPattern1 );
379  Gia_ManIncrementTravId( p->pAig );
380  Cec_ManPatComputePattern1_rec( p->pAig, Gia_ObjFanin0(pObj), pMan->vPattern1 );
381  // compute sensitizing path
382  Vec_IntClear( pMan->vPattern2 );
383  Gia_ManIncrementTravId( p->pAig );
384  Cec_ManPatComputePattern2_rec( p->pAig, Gia_ObjFanin0(pObj), pMan->vPattern2 );
385  // compare patterns
386  vPat = Vec_IntSize(pMan->vPattern1) < Vec_IntSize(pMan->vPattern2) ? pMan->vPattern1 : pMan->vPattern2;
387  pMan->nPatLitsMin += Vec_IntSize(vPat);
388  pMan->nPatLitsMinAll += Vec_IntSize(vPat);
389 //pMan->timeShrink += Abc_Clock() - clk;
390  // verify pattern using ternary simulation
391 //clk = Abc_Clock();
392 // Cec_ManPatVerifyPattern( p->pAig, pObj, vPat );
393 //pMan->timeVerify += Abc_Clock() - clk;
394  // sort pattern
395 //clk = Abc_Clock();
396  Vec_IntSort( vPat, 0 );
397 //pMan->timeSort += Abc_Clock() - clk;
398  // save pattern
399  Cec_ManPatStore( pMan, vPat );
400  pMan->timeTotal += Abc_Clock() - clkTotal;
401 }
402 void Cec_ManPatSavePatternCSat( Cec_ManPat_t * pMan, Vec_Int_t * vPat )
403 {
404  // sort pattern
405  Vec_IntSort( vPat, 0 );
406  // save pattern
407  Cec_ManPatStore( pMan, vPat );
408 }
409 
410 /**Function*************************************************************
411 
412  Synopsis [Packs patterns into array of simulation info.]
413 
414  Description []
415 
416  SideEffects []
417 
418  SeeAlso []
419 
420 *************************************`**********************************/
421 int Cec_ManPatCollectTry( Vec_Ptr_t * vInfo, Vec_Ptr_t * vPres, int iBit, int * pLits, int nLits )
422 {
423  unsigned * pInfo, * pPres;
424  int i;
425  for ( i = 0; i < nLits; i++ )
426  {
427  pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
428  pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
429  if ( Abc_InfoHasBit( pPres, iBit ) &&
430  Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
431  return 0;
432  }
433  for ( i = 0; i < nLits; i++ )
434  {
435  pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
436  pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
437  Abc_InfoSetBit( pPres, iBit );
438  if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
439  Abc_InfoXorBit( pInfo, iBit );
440  }
441  return 1;
442 }
443 
444 /**Function*************************************************************
445 
446  Synopsis [Packs patterns into array of simulation info.]
447 
448  Description []
449 
450  SideEffects []
451 
452  SeeAlso []
453 
454 ***********************************************************************/
455 Vec_Ptr_t * Cec_ManPatCollectPatterns( Cec_ManPat_t * pMan, int nInputs, int nWordsInit )
456 {
457  Vec_Int_t * vPat = pMan->vPattern1;
458  Vec_Ptr_t * vInfo, * vPres;
459  int k, kMax = -1, nPatterns = 0;
460  int iStartOld = pMan->iStart;
461  int nWords = nWordsInit;
462  int nBits = 32 * nWords;
463  abctime clk = Abc_Clock();
464  vInfo = Vec_PtrAllocSimInfo( nInputs, nWords );
465  Gia_ManRandomInfo( vInfo, 0, 0, nWords );
466  vPres = Vec_PtrAllocSimInfo( nInputs, nWords );
467  Vec_PtrCleanSimInfo( vPres, 0, nWords );
468  while ( pMan->iStart < Vec_StrSize(pMan->vStorage) )
469  {
470  nPatterns++;
471  Cec_ManPatRestore( pMan, vPat );
472  for ( k = 1; k < nBits; k++, k += ((k % (32 * nWordsInit)) == 0) )
473  if ( Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
474  break;
475  kMax = Abc_MaxInt( kMax, k );
476  if ( k == nBits-1 )
477  {
478  Vec_PtrReallocSimInfo( vInfo );
479  Gia_ManRandomInfo( vInfo, 0, nWords, 2*nWords );
480  Vec_PtrReallocSimInfo( vPres );
481  Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords );
482  nWords *= 2;
483  nBits *= 2;
484  }
485  }
486  Vec_PtrFree( vPres );
487  pMan->nSeries = Vec_PtrReadWordsSimInfo(vInfo) / nWordsInit;
488  pMan->timePack += Abc_Clock() - clk;
489  pMan->timeTotal += Abc_Clock() - clk;
490  pMan->iStart = iStartOld;
491  if ( pMan->fVerbose )
492  {
493  Abc_Print( 1, "Total = %5d. Max used = %5d. Full = %5d. Series = %d. ",
494  nPatterns, kMax, nWordsInit*32, pMan->nSeries );
495  ABC_PRT( "Time", Abc_Clock() - clk );
496  Cec_ManPatPrintStats( pMan );
497  }
498  return vInfo;
499 }
500 
501 
502 /**Function*************************************************************
503 
504  Synopsis [Packs patterns into array of simulation info.]
505 
506  Description []
507 
508  SideEffects []
509 
510  SeeAlso []
511 
512 ***********************************************************************/
513 Vec_Ptr_t * Cec_ManPatPackPatterns( Vec_Int_t * vCexStore, int nInputs, int nRegs, int nWordsInit )
514 {
515  Vec_Int_t * vPat;
516  Vec_Ptr_t * vInfo, * vPres;
517  int k, nSize, iStart, kMax = 0, nPatterns = 0;
518  int nWords = nWordsInit;
519  int nBits = 32 * nWords;
520 // int RetValue;
521  assert( nRegs <= nInputs );
522  vPat = Vec_IntAlloc( 100 );
523 
524  vInfo = Vec_PtrAllocSimInfo( nInputs, nWords );
525  Vec_PtrCleanSimInfo( vInfo, 0, nWords );
526  Gia_ManRandomInfo( vInfo, nRegs, 0, nWords );
527 
528  vPres = Vec_PtrAllocSimInfo( nInputs, nWords );
529  Vec_PtrCleanSimInfo( vPres, 0, nWords );
530  iStart = 0;
531  while ( iStart < Vec_IntSize(vCexStore) )
532  {
533  nPatterns++;
534  // skip the output number
535  iStart++;
536  // get the number of items
537  nSize = Vec_IntEntry( vCexStore, iStart++ );
538  if ( nSize <= 0 )
539  continue;
540  // extract pattern
541  Vec_IntClear( vPat );
542  for ( k = 0; k < nSize; k++ )
543  Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
544  // add pattern to storage
545  for ( k = 1; k < nBits; k++, k += ((k % (32 * nWordsInit)) == 0) )
546  if ( Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
547  break;
548 
549 // k = kMax + 1;
550 // RetValue = Cec_ManPatCollectTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) );
551 // assert( RetValue == 1 );
552 
553  kMax = Abc_MaxInt( kMax, k );
554  if ( k == nBits-1 )
555  {
556  Vec_PtrReallocSimInfo( vInfo );
557  Vec_PtrCleanSimInfo( vInfo, nWords, 2*nWords );
558  Gia_ManRandomInfo( vInfo, nRegs, nWords, 2*nWords );
559 
560  Vec_PtrReallocSimInfo( vPres );
561  Vec_PtrCleanSimInfo( vPres, nWords, 2*nWords );
562  nWords *= 2;
563  nBits *= 2;
564  }
565  }
566 // Abc_Print( 1, "packed %d patterns into %d vectors (out of %d)\n", nPatterns, kMax, nBits );
567  Vec_PtrFree( vPres );
568  Vec_IntFree( vPat );
569  return vInfo;
570 }
571 
572 ////////////////////////////////////////////////////////////////////////
573 /// END OF FILE ///
574 ////////////////////////////////////////////////////////////////////////
575 
576 
577 ABC_NAMESPACE_IMPL_END
578 
Cec_ManPatSavePattern
void Cec_ManPatSavePattern(Cec_ManPat_t *pMan, Cec_ManSat_t *p, Gia_Obj_t *pObj)
Definition: cecPat.c:359
Vec_IntArray
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
Cec_ManPatPackPatterns
Vec_Ptr_t * Cec_ManPatPackPatterns(Vec_Int_t *vCexStore, int nInputs, int nRegs, int nWordsInit)
Definition: cecPat.c:513
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Cec_ManPatComputePattern_rec
int Cec_ManPatComputePattern_rec(Cec_ManSat_t *pSat, Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: cecPat.c:140
GIA_UND
#define GIA_UND
Definition: gia.h:749
Cec_ManPatStoreNum
static ABC_NAMESPACE_IMPL_START void Cec_ManPatStoreNum(Cec_ManPat_t *p, int Num)
DECLARATIONS ///.
Definition: cecPat.c:45
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
Gia_ManCi
static Gia_Obj_t * Gia_ManCi(Gia_Man_t *p, int v)
Definition: gia.h:403
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Cec_ManPatComputePattern1_rec
void Cec_ManPatComputePattern1_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vPat)
Definition: cecPat.c:170
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Cec_ManPatRestore
static void Cec_ManPatRestore(Cec_ManPat_t *p, Vec_Int_t *vPat)
Definition: cecPat.c:113
Gia_ObjIsTravIdCurrent
static int Gia_ObjIsTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:533
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Abc_InfoXorBit
static void Abc_InfoXorBit(unsigned *p, int i)
Definition: abc_global.h:260
Gia_ManRandomInfo
void Gia_ManRandomInfo(Vec_Ptr_t *vInfo, int iInputStart, int iWordStart, int iWordStop)
Definition: giaUtil.c:80
Abc_Var2Lit
static int Abc_Var2Lit(int Var, int fCompl)
Definition: abc_global.h:263
Vec_PtrCleanSimInfo
static void Vec_PtrCleanSimInfo(Vec_Ptr_t *vInfo, int iWord, int nWords)
Definition: vecPtr.h:968
Cec_ManSat_t_::pAig
Gia_Man_t * pAig
Definition: cecInt.h:80
Gia_XsimNotCond
static int Gia_XsimNotCond(int Value, int fCompl)
Definition: gia.h:751
Gia_Obj_t_::fMark1
unsigned fMark1
Definition: gia.h:84
Gia_XsimAndCond
static int Gia_XsimAndCond(int Value0, int fCompl0, int Value1, int fCompl1)
Definition: gia.h:759
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Abc_MaxInt
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Vec_StrPush
static void Vec_StrPush(Vec_Str_t *p, char Entry)
Definition: vecStr.h:535
Cec_ManPatSavePatternCSat
void Cec_ManPatSavePatternCSat(Cec_ManPat_t *pMan, Vec_Int_t *vPat)
Definition: cecPat.c:402
Vec_IntSort
static void Vec_IntSort(Vec_Int_t *p, int fReverse)
Definition: vecInt.h:1293
nWords
int nWords
Definition: abcNpn.c:127
Gia_Obj_t_
Definition: gia.h:75
Abc_LitIsCompl
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
Vec_StrEntry
static char Vec_StrEntry(Vec_Str_t *p, int i)
Definition: vecStr.h:336
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Cec_ManPatVerifyPattern
void Cec_ManPatVerifyPattern(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vPat)
Definition: cecPat.c:278
Cec_ManPatCleanMark0
void Cec_ManPatCleanMark0(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: cecPat.c:341
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Cec_ManPatPrintStats
void Cec_ManPatPrintStats(Cec_ManPat_t *p)
Definition: cecMan.c:150
Gia_ObjSetTravIdCurrent
static void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
Cec_ManPat_t
typedefABC_NAMESPACE_HEADER_START struct Cec_ManPat_t_ Cec_ManPat_t
INCLUDES ///.
Definition: cecInt.h:48
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Cec_ManPatComputePattern3_rec
int Cec_ManPatComputePattern3_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: cecPat.c:246
Counter
static int Counter
Definition: extraBddMisc.c:1877
Vec_IntForEachEntryStart
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Cec_ManPatCollectPatterns
Vec_Ptr_t * Cec_ManPatCollectPatterns(Cec_ManPat_t *pMan, int nInputs, int nWordsInit)
Definition: cecPat.c:455
Gia_ObjIsCo
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Cec_ManPatComputePattern2_rec
void Cec_ManPatComputePattern2_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vPat)
Definition: cecPat.c:208
Vec_PtrEntry
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Vec_StrSize
static int Vec_StrSize(Vec_Str_t *p)
Definition: bblif.c:600
Cec_ManSat_t_
Definition: cecInt.h:75
Vec_PtrReadWordsSimInfo
static int Vec_PtrReadWordsSimInfo(Vec_Ptr_t *p)
Definition: vecPtr.h:952
Cec_ObjSatVarValue
int Cec_ObjSatVarValue(Cec_ManSat_t *p, Gia_Obj_t *pObj)
FUNCTION DEFINITIONS ///.
Definition: cecSolve.c:48
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Cec_ManPatCollectTry
int Cec_ManPatCollectTry(Vec_Ptr_t *vInfo, Vec_Ptr_t *vPres, int iBit, int *pLits, int nLits)
Definition: cecPat.c:421
Gia_Obj_t_::fMark0
unsigned fMark0
Definition: gia.h:79
Gia_Man_t_
Definition: gia.h:95
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Cec_ManPatComputePattern4_rec
void Cec_ManPatComputePattern4_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: cecPat.c:317
Abc_Lit2Var
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Vec_PtrReallocSimInfo
static void Vec_PtrReallocSimInfo(Vec_Ptr_t *vInfo)
Definition: vecPtr.h:1035
assert
#define assert(ex)
Definition: util_old.h:213
Cec_ManPatStore
static void Cec_ManPatStore(Cec_ManPat_t *p, Vec_Int_t *vPat)
Definition: cecPat.c:87
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition: giaUtil.c:149
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_ObjIsCi
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Gia_ObjCioId
static int Gia_ObjCioId(Gia_Obj_t *pObj)
Definition: gia.h:411
Vec_PtrAllocSimInfo
static Vec_Ptr_t * Vec_PtrAllocSimInfo(int nEntries, int nWords)
Definition: vecPtr.h:929
Cec_ManPatRestoreNum
static int Cec_ManPatRestoreNum(Cec_ManPat_t *p)
Definition: cecPat.c:68
GIA_ONE
#define GIA_ONE
Definition: gia.h:748
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223