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 ***********************************************************************/
Cec_ManPatStoreNum(Cec_ManPat_t * p,int Num)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 ***********************************************************************/
Cec_ManPatRestoreNum(Cec_ManPat_t * p)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 ***********************************************************************/
Cec_ManPatStore(Cec_ManPat_t * p,Vec_Int_t * vPat)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 ***********************************************************************/
Cec_ManPatRestore(Cec_ManPat_t * p,Vec_Int_t * vPat)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 ***********************************************************************/
Cec_ManPatComputePattern_rec(Cec_ManSat_t * pSat,Gia_Man_t * p,Gia_Obj_t * pObj)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 ***********************************************************************/
Cec_ManPatComputePattern1_rec(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vPat)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 ***********************************************************************/
Cec_ManPatComputePattern2_rec(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vPat)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 ***********************************************************************/
Cec_ManPatComputePattern3_rec(Gia_Man_t * p,Gia_Obj_t * pObj)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 ***********************************************************************/
Cec_ManPatVerifyPattern(Gia_Man_t * p,Gia_Obj_t * pObj,Vec_Int_t * vPat)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 ***********************************************************************/
Cec_ManPatComputePattern4_rec(Gia_Man_t * p,Gia_Obj_t * pObj)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 ***********************************************************************/
Cec_ManPatCleanMark0(Gia_Man_t * p,Gia_Obj_t * pObj)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 ***********************************************************************/
Cec_ManPatSavePattern(Cec_ManPat_t * pMan,Cec_ManSat_t * p,Gia_Obj_t * pObj)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 }
Cec_ManPatSavePatternCSat(Cec_ManPat_t * pMan,Vec_Int_t * vPat)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 *************************************`**********************************/
Cec_ManPatCollectTry(Vec_Ptr_t * vInfo,Vec_Ptr_t * vPres,int iBit,int * pLits,int nLits)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 ***********************************************************************/
Cec_ManPatCollectPatterns(Cec_ManPat_t * pMan,int nInputs,int nWordsInit)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 ***********************************************************************/
Cec_ManPatPackPatterns(Vec_Int_t * vCexStore,int nInputs,int nRegs,int nWordsInit)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
579