ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
cecPat.c File Reference
#include "cecInt.h"
Include dependency graph for cecPat.c:

Go to the source code of this file.

Functions

int Cec_ManPatComputePattern_rec (Cec_ManSat_t *pSat, Gia_Man_t *p, Gia_Obj_t *pObj)
 
void Cec_ManPatComputePattern1_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vPat)
 
void Cec_ManPatComputePattern2_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vPat)
 
int Cec_ManPatComputePattern3_rec (Gia_Man_t *p, Gia_Obj_t *pObj)
 
void Cec_ManPatVerifyPattern (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vPat)
 
void Cec_ManPatComputePattern4_rec (Gia_Man_t *p, Gia_Obj_t *pObj)
 
void Cec_ManPatCleanMark0 (Gia_Man_t *p, Gia_Obj_t *pObj)
 
void Cec_ManPatSavePattern (Cec_ManPat_t *pMan, Cec_ManSat_t *p, Gia_Obj_t *pObj)
 
void Cec_ManPatSavePatternCSat (Cec_ManPat_t *pMan, Vec_Int_t *vPat)
 
int Cec_ManPatCollectTry (Vec_Ptr_t *vInfo, Vec_Ptr_t *vPres, int iBit, int *pLits, int nLits)
 
Vec_Ptr_t * Cec_ManPatCollectPatterns (Cec_ManPat_t *pMan, int nInputs, int nWordsInit)
 
Vec_Ptr_t * Cec_ManPatPackPatterns (Vec_Int_t *vCexStore, int nInputs, int nRegs, int nWordsInit)
 

Function Documentation

◆ Cec_ManPatCleanMark0()

void Cec_ManPatCleanMark0 ( Gia_Man_t * p,
Gia_Obj_t * pObj )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 341 of file cecPat.c.

342{
343 assert( Gia_ObjIsCo(pObj) );
344 Gia_ManIncrementTravId( p );
345 Cec_ManPatComputePattern4_rec( p, Gia_ObjFanin0(pObj) );
346}
Cec_ManPatComputePattern4_rec
void Cec_ManPatComputePattern4_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition cecPat.c:317
p
Cube * p
Definition exorList.c:222
Gia_ManIncrementTravId
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition giaUtil.c:190
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:

◆ Cec_ManPatCollectPatterns()

Vec_Ptr_t * Cec_ManPatCollectPatterns ( Cec_ManPat_t * pMan,
int nInputs,
int nWordsInit )

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

Synopsis [Packs patterns into array of simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 455 of file cecPat.c.

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}
nWords
int nWords
Definition abcNpn.c:127
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_PRT
#define ABC_PRT(a, t)
Definition abc_global.h:255
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Cec_ManPatPrintStats
void Cec_ManPatPrintStats(Cec_ManPat_t *p)
Definition cecMan.c:151
Cec_ManPatCollectTry
int Cec_ManPatCollectTry(Vec_Ptr_t *vInfo, Vec_Ptr_t *vPres, int iBit, int *pLits, int nLits)
Definition cecPat.c:421
Gia_ManRandomInfo
void Gia_ManRandomInfo(Vec_Ptr_t *vInfo, int iInputStart, int iWordStart, int iWordStop)
Definition giaUtil.c:85
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cec_ManPatCollectTry()

int Cec_ManPatCollectTry ( Vec_Ptr_t * vInfo,
Vec_Ptr_t * vPres,
int iBit,
int * pLits,
int nLits )

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

Synopsis [Packs patterns into array of simulation info.]

Description []

SideEffects []

SeeAlso [] 

                               `

Definition at line 421 of file cecPat.c.

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}
Here is the caller graph for this function:

◆ Cec_ManPatComputePattern1_rec()

void Cec_ManPatComputePattern1_rec ( Gia_Man_t * p,
Gia_Obj_t * pObj,
Vec_Int_t * vPat )

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

Synopsis [Derives satisfying assignment.]

Description []

SideEffects []

SeeAlso []

Definition at line 170 of file cecPat.c.

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}
Cec_ManPatComputePattern1_rec
void Cec_ManPatComputePattern1_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vPat)
Definition cecPat.c:170
Gia_Obj_t_::fMark1
unsigned fMark1
Definition gia.h:86
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cec_ManPatComputePattern2_rec()

void Cec_ManPatComputePattern2_rec ( Gia_Man_t * p,
Gia_Obj_t * pObj,
Vec_Int_t * vPat )

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

Synopsis [Derives satisfying assignment.]

Description []

SideEffects []

SeeAlso []

Definition at line 208 of file cecPat.c.

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}
Cec_ManPatComputePattern2_rec
void Cec_ManPatComputePattern2_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vPat)
Definition cecPat.c:208
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cec_ManPatComputePattern3_rec()

int Cec_ManPatComputePattern3_rec ( Gia_Man_t * p,
Gia_Obj_t * pObj )

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

Synopsis [Derives satisfying assignment.]

Description []

SideEffects []

SeeAlso []

Definition at line 246 of file cecPat.c.

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}
Cec_ManPatComputePattern3_rec
int Cec_ManPatComputePattern3_rec(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition cecPat.c:246
GIA_UND
#define GIA_UND
Definition gia.h:923
Gia_Obj_t_::fMark0
unsigned fMark0
Definition gia.h:81
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cec_ManPatComputePattern4_rec()

void Cec_ManPatComputePattern4_rec ( Gia_Man_t * p,
Gia_Obj_t * pObj )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 317 of file cecPat.c.

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}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cec_ManPatComputePattern_rec()

int Cec_ManPatComputePattern_rec ( Cec_ManSat_t * pSat,
Gia_Man_t * p,
Gia_Obj_t * pObj )

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

Synopsis [Derives satisfying assignment.]

Description []

SideEffects []

SeeAlso []

Definition at line 140 of file cecPat.c.

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}
Cec_ObjSatVarValue
int Cec_ObjSatVarValue(Cec_ManSat_t *p, Gia_Obj_t *pObj)
FUNCTION DEFINITIONS ///.
Definition cecSolve.c:48
Cec_ManPatComputePattern_rec
int Cec_ManPatComputePattern_rec(Cec_ManSat_t *pSat, Gia_Man_t *p, Gia_Obj_t *pObj)
Definition cecPat.c:140
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cec_ManPatPackPatterns()

Vec_Ptr_t * Cec_ManPatPackPatterns ( Vec_Int_t * vCexStore,
int nInputs,
int nRegs,
int nWordsInit )

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

Synopsis [Packs patterns into array of simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 513 of file cecPat.c.

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}
Here is the call graph for this function:

◆ Cec_ManPatSavePattern()

void Cec_ManPatSavePattern ( Cec_ManPat_t * pMan,
Cec_ManSat_t * p,
Gia_Obj_t * pObj )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 359 of file cecPat.c.

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}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Cec_ManPatSavePatternCSat()

void Cec_ManPatSavePatternCSat ( Cec_ManPat_t * pMan,
Vec_Int_t * vPat )

Definition at line 402 of file cecPat.c.

403{
404 // sort pattern
405 Vec_IntSort( vPat, 0 );
406 // save pattern
407 Cec_ManPatStore( pMan, vPat );
408}
Here is the caller graph for this function:

◆ Cec_ManPatVerifyPattern()

void Cec_ManPatVerifyPattern ( Gia_Man_t * p,
Gia_Obj_t * pObj,
Vec_Int_t * vPat )

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

Synopsis [Derives satisfying assignment.]

Description []

SideEffects []

SeeAlso []

Definition at line 278 of file cecPat.c.

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}
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
GIA_ONE
#define GIA_ONE
Definition gia.h:922
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the call graph for this function: