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

Go to the source code of this file.

Data Structures

struct  Gia_Sim2_t_
 

Typedefs

typedef
typedefABC_NAMESPACE_IMPL_START
struct Gia_Sim2_t_ 		Gia_Sim2_t
 DECLARATIONS ///. More...
 

Functions

static unsigned * Gia_Sim2Data (Gia_Sim2_t *p, int i)
 
void Gia_ManResetRandom (Gia_ParSim_t *pPars)
 
void Gia_Sim2Delete (Gia_Sim2_t *p)
 FUNCTION DEFINITIONS ///. More...
 
Gia_Sim2_t * Gia_Sim2Create (Gia_Man_t *pAig, Gia_ParSim_t *pPars)
 
static void Gia_Sim2InfoRandom (Gia_Sim2_t *p, unsigned *pInfo)
 
static void Gia_Sim2InfoZero (Gia_Sim2_t *p, unsigned *pInfo)
 
static void Gia_Sim2InfoOne (Gia_Sim2_t *p, unsigned *pInfo)
 
static void Gia_Sim2InfoCopy (Gia_Sim2_t *p, unsigned *pInfo, unsigned *pInfo0)
 
static void Gia_Sim2SimulateCo (Gia_Sim2_t *p, Gia_Obj_t *pObj)
 
static void Gia_Sim2SimulateNode (Gia_Sim2_t *p, Gia_Obj_t *pObj)
 
static void Gia_Sim2InfoTransfer (Gia_Sim2_t *p)
 
static void Gia_Sim2SimulateRound (Gia_Sim2_t *p)
 
int Gia_Sim2CompareEqual (unsigned *p0, unsigned *p1, int nWords, int fCompl)
 
int Gia_Sim2CompareZero (unsigned *p0, int nWords, int fCompl)
 
void Gia_Sim2ClassCreate (Gia_Man_t *p, Vec_Int_t *vClass)
 
int Gia_Sim2ClassRefineOne (Gia_Sim2_t *p, int i)
 
int Gia_Sim2HashKey (unsigned *pSim, int nWords, int nTableSize)
 
void Gia_Sim2ProcessRefined (Gia_Sim2_t *p, Vec_Int_t *vRefined)
 
void Gia_Sim2InfoRefineEquivs (Gia_Sim2_t *p)
 
static int Gia_Sim2InfoIsZero (Gia_Sim2_t *p, unsigned *pInfo)
 
static int Gia_Sim2CheckPos (Gia_Sim2_t *p, int *piPo, int *piPat)
 
Abc_Cex_t * Gia_Sim2GenerateCounter (Gia_Man_t *pAig, int iFrame, int iOut, int nWords, int iPat)
 
int Gia_ManSimSimulateEquiv (Gia_Man_t *pAig, Gia_ParSim_t *pPars)
 

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Gia_Sim2_t_ Gia_Sim2_t

DECLARATIONS ///.

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

FileName [giaSim.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Scalable AIG package.]

Synopsis [Fast sequential simulator.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 20, 2005.]

Revision [

Id:
giaSim.c,v 1.00 2005/06/20 00:00:00 alanmi Exp

]

Definition at line 30 of file giaSim2.c.

Function Documentation

void Gia_ManResetRandom ( Gia_ParSim_t *  pPars)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 579 of file giaSim.c.

580 {
581  int i;
582  Gia_ManRandom( 1 );
583  for ( i = 0; i < pPars->RandSeed; i++ )
584  Gia_ManRandom( 0 );
585 }
Gia_ParSim_t_::RandSeed
int RandSeed
Definition: gia.h:243
Gia_ManRandom
unsigned Gia_ManRandom(int fReset)
FUNCTION DEFINITIONS ///.
Definition: giaUtil.c:49
int Gia_ManSimSimulateEquiv ( Gia_Man_t *  pAig,
Gia_ParSim_t *  pPars 
)

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

Synopsis [Performs simulation to refine equivalence classes.]

Description [Returns 1 if counter-example is detected.]

SideEffects []

SeeAlso []

Definition at line 638 of file giaSim2.c.

639 {
640  Gia_Sim2_t * p;
641  Gia_Obj_t * pObj;
642  abctime clkTotal = Abc_Clock();
643  int i, RetValue = 0, iOut, iPat;
644  abctime nTimeToStop = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
645  assert( pAig->pReprs && pAig->pNexts );
646  ABC_FREE( pAig->pCexSeq );
647  p = Gia_Sim2Create( pAig, pPars );
648  Gia_ManResetRandom( pPars );
649  Gia_ManForEachRo( p->pAig, pObj, i )
650  Gia_Sim2InfoZero( p, Gia_Sim2Data(p, Gia_ObjValue(pObj)) );
651  for ( i = 0; i < pPars->nIters; i++ )
652  {
653  Gia_Sim2SimulateRound( p );
654  if ( pPars->fVerbose )
655  {
656  Abc_Print( 1, "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
657  if ( pAig->pReprs && pAig->pNexts )
658  Abc_Print( 1, "Lits = %4d. ", Gia_ManEquivCountLitsAll(pAig) );
659  Abc_Print( 1, "Time = %7.2f sec\r", (1.0*Abc_Clock()-clkTotal)/CLOCKS_PER_SEC );
660  }
661  if ( pPars->fCheckMiter && Gia_Sim2CheckPos( p, &iOut, &iPat ) )
662  {
663  Gia_ManResetRandom( pPars );
664  pPars->iOutFail = iOut;
665  pAig->pCexSeq = Gia_Sim2GenerateCounter( pAig, i, iOut, p->nWords, iPat );
666  Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", iOut, pAig->pName, i );
667  if ( !Gia_ManVerifyCex( pAig, pAig->pCexSeq, 0 ) )
668  {
669 // Abc_Print( 1, "\n" );
670  Abc_Print( 1, "\nGenerated counter-example is INVALID. " );
671 // Abc_Print( 1, "\n" );
672  }
673  else
674  {
675 // Abc_Print( 1, "\n" );
676 // if ( pPars->fVerbose )
677 // Abc_Print( 1, "\nGenerated counter-example is verified correctly. " );
678 // Abc_Print( 1, "\n" );
679  }
680  RetValue = 1;
681  break;
682  }
683  if ( pAig->pReprs && pAig->pNexts )
684  Gia_Sim2InfoRefineEquivs( p );
685  if ( Abc_Clock() > nTimeToStop )
686  {
687  i++;
688  break;
689  }
690  if ( i < pPars->nIters - 1 )
691  Gia_Sim2InfoTransfer( p );
692  }
693  Gia_Sim2Delete( p );
694  if ( pAig->pCexSeq == NULL )
695  Abc_Print( 1, "No bug detected after simulating %d frames with %d words. ", i, pPars->nWords );
696  Abc_PrintTime( 1, "Time", Abc_Clock() - clkTotal );
697  return RetValue;
698 }
Gia_Sim2SimulateRound
static void Gia_Sim2SimulateRound(Gia_Sim2_t *p)
Definition: giaSim2.c:276
Gia_Sim2InfoTransfer
static void Gia_Sim2InfoTransfer(Gia_Sim2_t *p)
Definition: giaSim2.c:252
Gia_Sim2Delete
void Gia_Sim2Delete(Gia_Sim2_t *p)
FUNCTION DEFINITIONS ///.
Definition: giaSim2.c:60
Gia_ParSim_t_::nWords
int nWords
Definition: gia.h:241
Gia_ManVerifyCex
int Gia_ManVerifyCex(Gia_Man_t *pAig, Abc_Cex_t *p, int fDualOut)
DECLARATIONS ///.
Definition: giaCex.c:44
Gia_Man_t_::pNexts
int * pNexts
Definition: gia.h:122
Gia_Sim2InfoRefineEquivs
void Gia_Sim2InfoRefineEquivs(Gia_Sim2_t *p)
Definition: giaSim2.c:516
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Gia_ObjValue
static int Gia_ObjValue(Gia_Obj_t *pObj)
Definition: gia.h:413
Gia_Sim2InfoZero
static void Gia_Sim2InfoZero(Gia_Sim2_t *p, unsigned *pInfo)
Definition: giaSim2.c:137
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Gia_Sim2Create
Gia_Sim2_t * Gia_Sim2Create(Gia_Man_t *pAig, Gia_ParSim_t *pPars)
Definition: giaSim2.c:79
for
for(p=first;p->value< newval;p=p->next)
Gia_Obj_t_
Definition: gia.h:75
Gia_ParSim_t_::fVerbose
int fVerbose
Definition: gia.h:246
Gia_Sim2Data
static unsigned * Gia_Sim2Data(Gia_Sim2_t *p, int i)
Definition: giaSim2.c:41
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Gia_Man_t_::pName
char * pName
Definition: gia.h:97
Gia_ParSim_t_::fCheckMiter
int fCheckMiter
Definition: gia.h:245
Gia_Sim2GenerateCounter
Abc_Cex_t * Gia_Sim2GenerateCounter(Gia_Man_t *pAig, int iFrame, int iOut, int nWords, int iPat)
Definition: giaSim2.c:604
Gia_ManEquivCountLitsAll
int Gia_ManEquivCountLitsAll(Gia_Man_t *p)
Definition: giaEquiv.c:160
Gia_ParSim_t_::nIters
int nIters
Definition: gia.h:242
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Gia_Sim2_t
typedefABC_NAMESPACE_IMPL_START struct Gia_Sim2_t_ Gia_Sim2_t
DECLARATIONS ///.
Definition: giaSim2.c:30
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Gia_Sim2CheckPos
static int Gia_Sim2CheckPos(Gia_Sim2_t *p, int *piPo, int *piPat)
Definition: giaSim2.c:576
Gia_ManResetRandom
void Gia_ManResetRandom(Gia_ParSim_t *pPars)
Definition: giaSim.c:579
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
Gia_Man_t_::pReprs
Gia_Rpr_t * pReprs
Definition: gia.h:121
assert
#define assert(ex)
Definition: util_old.h:213
Gia_ParSim_t_::iOutFail
int iOutFail
Definition: gia.h:247
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Gia_Man_t_::pCexSeq
Abc_Cex_t * pCexSeq
Definition: gia.h:136
Gia_ParSim_t_::TimeLimit
int TimeLimit
Definition: gia.h:244
static int Gia_Sim2CheckPos ( Gia_Sim2_t *  p,
int *  piPo,
int *  piPat 
)
inlinestatic

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

Synopsis [Returns index of the PO and pattern that failed it.]

Description []

SideEffects []

SeeAlso []

Definition at line 576 of file giaSim2.c.

577 {
578  Gia_Obj_t * pObj;
579  int i, iPat;
580  Gia_ManForEachPo( p->pAig, pObj, i )
581  {
582  iPat = Gia_Sim2InfoIsZero( p, Gia_Sim2Data( p, Gia_ObjValue(pObj) ) );
583  if ( iPat >= 0 )
584  {
585  *piPo = i;
586  *piPat = iPat;
587  return 1;
588  }
589  }
590  return 0;
591 }
Gia_Sim2InfoIsZero
static int Gia_Sim2InfoIsZero(Gia_Sim2_t *p, unsigned *pInfo)
Definition: giaSim2.c:556
Llb_Mgr_t_::pAig
Aig_Man_t * pAig
Definition: llb3Image.c:49
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Gia_ObjValue
static int Gia_ObjValue(Gia_Obj_t *pObj)
Definition: gia.h:413
Gia_Obj_t_
Definition: gia.h:75
Gia_Sim2Data
static unsigned * Gia_Sim2Data(Gia_Sim2_t *p, int i)
Definition: giaSim2.c:41
Gia_ManForEachPo
#define Gia_ManForEachPo(p, pObj, i)
Definition: gia.h:1036
void Gia_Sim2ClassCreate ( Gia_Man_t *  p,
Vec_Int_t *  vClass 
)

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

Synopsis [Creates equivalence class.]

Description []

SideEffects []

SeeAlso []

Definition at line 367 of file giaSim2.c.

368 {
369  int Repr = GIA_VOID, EntPrev = -1, Ent, i;
370  assert( Vec_IntSize(vClass) > 0 );
371  Vec_IntForEachEntry( vClass, Ent, i )
372  {
373  if ( i == 0 )
374  {
375  Repr = Ent;
376  Gia_ObjSetRepr( p, Ent, GIA_VOID );
377  EntPrev = Ent;
378  }
379  else
380  {
381  assert( Repr < Ent );
382  Gia_ObjSetRepr( p, Ent, Repr );
383  Gia_ObjSetNext( p, EntPrev, Ent );
384  EntPrev = Ent;
385  }
386  }
387  Gia_ObjSetNext( p, EntPrev, 0 );
388 }
Gia_ObjSetRepr
static void Gia_ObjSetRepr(Gia_Man_t *p, int Id, int Num)
Definition: gia.h:888
Gia_ObjSetNext
static void Gia_ObjSetNext(Gia_Man_t *p, int Id, int Num)
Definition: gia.h:913
GIA_VOID
#define GIA_VOID
Definition: gia.h:45
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
int Gia_Sim2ClassRefineOne ( Gia_Sim2_t *  p,
int  i 
)

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

Synopsis [Refines one equivalence class.]

Description []

SideEffects []

SeeAlso []

Definition at line 401 of file giaSim2.c.

402 {
403  Gia_Obj_t * pObj0, * pObj1;
404  unsigned * pSim0, * pSim1;
405  int Ent;
406  Vec_IntClear( p->vClassOld );
407  Vec_IntClear( p->vClassNew );
408  Vec_IntPush( p->vClassOld, i );
409  pObj0 = Gia_ManObj( p->pAig, i );
410  pSim0 = Gia_Sim2Data( p, i );
411  Gia_ClassForEachObj1( p->pAig, i, Ent )
412  {
413  pObj1 = Gia_ManObj( p->pAig, Ent );
414  pSim1 = Gia_Sim2Data( p, Ent );
415  if ( Gia_Sim2CompareEqual( pSim0, pSim1, p->nWords, Gia_ObjPhase(pObj0) ^ Gia_ObjPhase(pObj1) ) )
416  Vec_IntPush( p->vClassOld, Ent );
417  else
418  Vec_IntPush( p->vClassNew, Ent );
419  }
420  if ( Vec_IntSize( p->vClassNew ) == 0 )
421  return 0;
422  Gia_Sim2ClassCreate( p->pAig, p->vClassOld );
423  Gia_Sim2ClassCreate( p->pAig, p->vClassNew );
424  if ( Vec_IntSize(p->vClassNew) > 1 )
425  return 1 + Gia_Sim2ClassRefineOne( p, Vec_IntEntry(p->vClassNew,0) );
426  return 1;
427 }
Gia_Sim2ClassRefineOne
int Gia_Sim2ClassRefineOne(Gia_Sim2_t *p, int i)
Definition: giaSim2.c:401
Gia_ObjPhase
static int Gia_ObjPhase(Gia_Obj_t *pObj)
Definition: gia.h:415
Llb_Mgr_t_::pAig
Aig_Man_t * pAig
Definition: llb3Image.c:49
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Gia_Sim2CompareEqual
int Gia_Sim2CompareEqual(unsigned *p0, unsigned *p1, int nWords, int fCompl)
Definition: giaSim2.c:307
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Gia_Obj_t_
Definition: gia.h:75
Gia_Sim2Data
static unsigned * Gia_Sim2Data(Gia_Sim2_t *p, int i)
Definition: giaSim2.c:41
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Gia_ClassForEachObj1
#define Gia_ClassForEachObj1(p, i, iObj)
Definition: gia.h:933
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Vec_IntClear
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
Gia_Sim2ClassCreate
void Gia_Sim2ClassCreate(Gia_Man_t *p, Vec_Int_t *vClass)
Definition: giaSim2.c:367
int Gia_Sim2CompareEqual ( unsigned *  p0,
unsigned *  p1,
int  nWords,
int  fCompl 
)

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

Synopsis [Compares simulation info of two nodes.]

Description []

SideEffects []

SeeAlso []

Definition at line 307 of file giaSim2.c.

308 {
309  int w;
310  if ( !fCompl )
311  {
312  for ( w = 0; w < nWords; w++ )
313  if ( p0[w] != p1[w] )
314  return 0;
315  return 1;
316  }
317  else
318  {
319  for ( w = 0; w < nWords; w++ )
320  if ( p0[w] != ~p1[w] )
321  return 0;
322  return 1;
323  }
324 }
nWords
int nWords
Definition: abcNpn.c:127
int Gia_Sim2CompareZero ( unsigned *  p0,
int  nWords,
int  fCompl 
)

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

Synopsis [Compares simulation info of one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 337 of file giaSim2.c.

338 {
339  int w;
340  if ( !fCompl )
341  {
342  for ( w = 0; w < nWords; w++ )
343  if ( p0[w] != 0 )
344  return 0;
345  return 1;
346  }
347  else
348  {
349  for ( w = 0; w < nWords; w++ )
350  if ( p0[w] != ~0 )
351  return 0;
352  return 1;
353  }
354 }
nWords
int nWords
Definition: abcNpn.c:127
Gia_Sim2_t* Gia_Sim2Create ( Gia_Man_t *  pAig,
Gia_ParSim_t *  pPars 
)

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

Synopsis [Creates fast simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 79 of file giaSim2.c.

80 {
81  Gia_Sim2_t * p;
82  Gia_Obj_t * pObj;
83  int i;
84  p = ABC_CALLOC( Gia_Sim2_t, 1 );
85  p->pAig = pAig;
86  p->pPars = pPars;
87  p->nWords = pPars->nWords;
88  p->pDataSim = ABC_ALLOC( unsigned, p->nWords * Gia_ManObjNum(p->pAig) );
89  if ( !p->pDataSim )
90  {
91  Abc_Print( 1, "Simulator could not allocate %.2f GB for simulation info.\n",
92  4.0 * p->nWords * Gia_ManObjNum(p->pAig) / (1<<30) );
93  Gia_Sim2Delete( p );
94  return NULL;
95  }
96  p->vClassOld = Vec_IntAlloc( 100 );
97  p->vClassNew = Vec_IntAlloc( 100 );
98  if ( pPars->fVerbose )
99  Abc_Print( 1, "Memory: AIG = %7.2f MB. SimInfo = %7.2f MB.\n",
100  12.0*Gia_ManObjNum(p->pAig)/(1<<20), 4.0*p->nWords*Gia_ManObjNum(p->pAig)/(1<<20) );
101  // prepare AIG
102  Gia_ManSetPhase( pAig );
103  Gia_ManForEachObj( pAig, pObj, i )
104  pObj->Value = i;
105  return p;
106 }
Gia_Sim2Delete
void Gia_Sim2Delete(Gia_Sim2_t *p)
FUNCTION DEFINITIONS ///.
Definition: giaSim2.c:60
Gia_ParSim_t_::nWords
int nWords
Definition: gia.h:241
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Gia_Obj_t_
Definition: gia.h:75
Gia_ParSim_t_::fVerbose
int fVerbose
Definition: gia.h:246
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Gia_Sim2_t
typedefABC_NAMESPACE_IMPL_START struct Gia_Sim2_t_ Gia_Sim2_t
DECLARATIONS ///.
Definition: giaSim2.c:30
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Gia_ManSetPhase
void Gia_ManSetPhase(Gia_Man_t *p)
Definition: giaUtil.c:379
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static unsigned* Gia_Sim2Data ( Gia_Sim2_t *  p,
int  i 
)
inlinestatic

Definition at line 41 of file giaSim2.c.

41 { return p->pDataSim + i * p->nWords; }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Gia_Sim2Delete ( Gia_Sim2_t *  p)

FUNCTION DEFINITIONS ///.

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 60 of file giaSim2.c.

61 {
62  Vec_IntFreeP( &p->vClassOld );
63  Vec_IntFreeP( &p->vClassNew );
64  ABC_FREE( p->pDataSim );
65  ABC_FREE( p );
66 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_IntFreeP
static void Vec_IntFreeP(Vec_Int_t **p)
Definition: vecInt.h:289
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Abc_Cex_t* Gia_Sim2GenerateCounter ( Gia_Man_t *  pAig,
int  iFrame,
int  iOut,
int  nWords,
int  iPat 
)

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

Synopsis [Returns the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 604 of file giaSim2.c.

605 {
606  Abc_Cex_t * p;
607  unsigned * pData;
608  int f, i, w, Counter;
609  p = Abc_CexAlloc( Gia_ManRegNum(pAig), Gia_ManPiNum(pAig), iFrame+1 );
610  p->iFrame = iFrame;
611  p->iPo = iOut;
612  // fill in the binary data
613  Counter = p->nRegs;
614  pData = ABC_ALLOC( unsigned, nWords );
615  for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
616  for ( i = 0; i < Gia_ManPiNum(pAig); i++ )
617  {
618  for ( w = nWords-1; w >= 0; w-- )
619  pData[w] = Gia_ManRandom( 0 );
620  if ( Abc_InfoHasBit( pData, iPat ) )
621  Abc_InfoSetBit( p->pData, Counter + i );
622  }
623  ABC_FREE( pData );
624  return p;
625 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
nWords
int nWords
Definition: abcNpn.c:127
Gia_ManRandom
unsigned Gia_ManRandom(int fReset)
FUNCTION DEFINITIONS ///.
Definition: giaUtil.c:49
Counter
static int Counter
Definition: extraBddMisc.c:1877
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Gia_ManPiNum
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
int Gia_Sim2HashKey ( unsigned *  pSim,
int  nWords,
int  nTableSize 
)

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

Synopsis [Computes hash key of the simuation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 440 of file giaSim2.c.

441 {
442  static int s_Primes[16] = {
443  1291, 1699, 1999, 2357, 2953, 3313, 3907, 4177,
444  4831, 5147, 5647, 6343, 6899, 7103, 7873, 8147 };
445  unsigned uHash = 0;
446  int i;
447  if ( pSim[0] & 1 )
448  for ( i = 0; i < nWords; i++ )
449  uHash ^= ~pSim[i] * s_Primes[i & 0xf];
450  else
451  for ( i = 0; i < nWords; i++ )
452  uHash ^= pSim[i] * s_Primes[i & 0xf];
453  return (int)(uHash % nTableSize);
454 
455 }
nWords
int nWords
Definition: abcNpn.c:127
s_Primes
static int s_Primes[MAX_PRIMES]
Definition: fxuPair.c:30
static void Gia_Sim2InfoCopy ( Gia_Sim2_t *  p,
unsigned *  pInfo,
unsigned *  pInfo0 
)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 173 of file giaSim2.c.

174 {
175  int w;
176  for ( w = p->nWords-1; w >= 0; w-- )
177  pInfo[w] = pInfo0[w];
178 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Gia_Sim2InfoIsZero ( Gia_Sim2_t *  p,
unsigned *  pInfo 
)
inlinestatic

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

Synopsis [Returns index of the first pattern that failed.]

Description []

SideEffects []

SeeAlso []

Definition at line 556 of file giaSim2.c.

557 {
558  int w;
559  for ( w = 0; w < p->nWords; w++ )
560  if ( pInfo[w] )
561  return 32*w + Gia_WordFindFirstBit( pInfo[w] );
562  return -1;
563 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Gia_WordFindFirstBit
static int Gia_WordFindFirstBit(unsigned uWord)
Definition: gia.h:321
static void Gia_Sim2InfoOne ( Gia_Sim2_t *  p,
unsigned *  pInfo 
)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 155 of file giaSim2.c.

156 {
157  int w;
158  for ( w = p->nWords-1; w >= 0; w-- )
159  pInfo[w] = ~0;
160 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static void Gia_Sim2InfoRandom ( Gia_Sim2_t *  p,
unsigned *  pInfo 
)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 119 of file giaSim2.c.

120 {
121  int w;
122  for ( w = p->nWords-1; w >= 0; w-- )
123  pInfo[w] = Gia_ManRandom( 0 );
124 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Gia_ManRandom
unsigned Gia_ManRandom(int fReset)
FUNCTION DEFINITIONS ///.
Definition: giaUtil.c:49
void Gia_Sim2InfoRefineEquivs ( Gia_Sim2_t *  p)

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

Synopsis [Refines equivalences after one simulation round.]

Description []

SideEffects []

SeeAlso []

Definition at line 516 of file giaSim2.c.

517 {
518  Vec_Int_t * vRefined;
519  Gia_Obj_t * pObj;
520  unsigned * pSim;
521  int i, Count = 0;
522  // process constant candidates
523  vRefined = Vec_IntAlloc( 100 );
524  Gia_ManForEachObj1( p->pAig, pObj, i )
525  {
526  if ( !Gia_ObjIsConst(p->pAig, i) )
527  continue;
528  pSim = Gia_Sim2Data( p, i );
529 //Extra_PrintBinary( stdout, pSim, 32 * p->nWords ); printf( "\n" );
530  if ( !Gia_Sim2CompareZero( pSim, p->nWords, Gia_ObjPhase(pObj) ) )
531  {
532  Vec_IntPush( vRefined, i );
533  Count++;
534  }
535  }
536  Gia_Sim2ProcessRefined( p, vRefined );
537  Vec_IntFree( vRefined );
538  // process other classes
539  Gia_ManForEachClass( p->pAig, i )
540  Count += Gia_Sim2ClassRefineOne( p, i );
541 // if ( Count )
542 // printf( "Refined %d times.\n", Count );
543 }
Gia_Sim2ClassRefineOne
int Gia_Sim2ClassRefineOne(Gia_Sim2_t *p, int i)
Definition: giaSim2.c:401
Gia_ObjPhase
static int Gia_ObjPhase(Gia_Obj_t *pObj)
Definition: gia.h:415
Llb_Mgr_t_::pAig
Aig_Man_t * pAig
Definition: llb3Image.c:49
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Gia_Obj_t_
Definition: gia.h:75
Gia_Sim2ProcessRefined
void Gia_Sim2ProcessRefined(Gia_Sim2_t *p, Vec_Int_t *vRefined)
Definition: giaSim2.c:468
Gia_Sim2Data
static unsigned * Gia_Sim2Data(Gia_Sim2_t *p, int i)
Definition: giaSim2.c:41
Gia_Sim2CompareZero
int Gia_Sim2CompareZero(unsigned *p0, int nWords, int fCompl)
Definition: giaSim2.c:337
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Gia_ObjIsConst
static int Gia_ObjIsConst(Gia_Man_t *p, int Id)
Definition: gia.h:915
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Gia_ManForEachClass
#define Gia_ManForEachClass(p, i)
Definition: gia.h:927
Gia_ManForEachObj1
#define Gia_ManForEachObj1(p, pObj, i)
Definition: gia.h:986
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static void Gia_Sim2InfoTransfer ( Gia_Sim2_t *  p)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 252 of file giaSim2.c.

253 {
254  Gia_Obj_t * pObjRo, * pObjRi;
255  unsigned * pInfo0, * pInfo1;
256  int i;
257  Gia_ManForEachRiRo( p->pAig, pObjRi, pObjRo, i )
258  {
259  pInfo0 = Gia_Sim2Data( p, Gia_ObjValue(pObjRo) );
260  pInfo1 = Gia_Sim2Data( p, Gia_ObjValue(pObjRi) );
261  Gia_Sim2InfoCopy( p, pInfo0, pInfo1 );
262  }
263 }
Llb_Mgr_t_::pAig
Aig_Man_t * pAig
Definition: llb3Image.c:49
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Gia_ObjValue
static int Gia_ObjValue(Gia_Obj_t *pObj)
Definition: gia.h:413
Gia_Obj_t_
Definition: gia.h:75
Gia_Sim2Data
static unsigned * Gia_Sim2Data(Gia_Sim2_t *p, int i)
Definition: giaSim2.c:41
Gia_ManForEachRiRo
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition: gia.h:1042
Gia_Sim2InfoCopy
static void Gia_Sim2InfoCopy(Gia_Sim2_t *p, unsigned *pInfo, unsigned *pInfo0)
Definition: giaSim2.c:173
static void Gia_Sim2InfoZero ( Gia_Sim2_t *  p,
unsigned *  pInfo 
)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 137 of file giaSim2.c.

138 {
139  int w;
140  for ( w = p->nWords-1; w >= 0; w-- )
141  pInfo[w] = 0;
142 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Gia_Sim2ProcessRefined ( Gia_Sim2_t *  p,
Vec_Int_t *  vRefined 
)

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

Synopsis [Refines nodes belonging to candidate constant class.]

Description []

SideEffects []

SeeAlso []

Definition at line 468 of file giaSim2.c.

469 {
470  unsigned * pSim;
471  int * pTable, nTableSize, i, k, Key;
472  if ( Vec_IntSize(vRefined) == 0 )
473  return;
474  nTableSize = Abc_PrimeCudd( 1000 + Vec_IntSize(vRefined) / 3 );
475  pTable = ABC_CALLOC( int, nTableSize );
476  Vec_IntForEachEntry( vRefined, i, k )
477  {
478  pSim = Gia_Sim2Data( p, i );
479  Key = Gia_Sim2HashKey( pSim, p->nWords, nTableSize );
480  if ( pTable[Key] == 0 )
481  {
482  assert( Gia_ObjRepr(p->pAig, i) == 0 );
483  assert( Gia_ObjNext(p->pAig, i) == 0 );
484  Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
485  }
486  else
487  {
488  Gia_ObjSetNext( p->pAig, pTable[Key], i );
489  Gia_ObjSetRepr( p->pAig, i, Gia_ObjRepr(p->pAig, pTable[Key]) );
490  if ( Gia_ObjRepr(p->pAig, i) == GIA_VOID )
491  Gia_ObjSetRepr( p->pAig, i, pTable[Key] );
492  assert( Gia_ObjRepr(p->pAig, i) > 0 );
493  }
494  pTable[Key] = i;
495  }
496 /*
497  Vec_IntForEachEntry( vRefined, i, k )
498  {
499  if ( Gia_ObjIsHead( p->pAig, i ) )
500  Gia_Sim2ClassRefineOne( p, i );
501  }
502 */
503  ABC_FREE( pTable );
504 }
Abc_PrimeCudd
static int Abc_PrimeCudd(unsigned int p)
Definition: abc_global.h:383
Llb_Mgr_t_::pAig
Aig_Man_t * pAig
Definition: llb3Image.c:49
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Gia_Sim2Data
static unsigned * Gia_Sim2Data(Gia_Sim2_t *p, int i)
Definition: giaSim2.c:41
Gia_ObjSetRepr
static void Gia_ObjSetRepr(Gia_Man_t *p, int Id, int Num)
Definition: gia.h:888
Gia_Sim2HashKey
int Gia_Sim2HashKey(unsigned *pSim, int nWords, int nTableSize)
Definition: giaSim2.c:440
Gia_ObjNext
static int Gia_ObjNext(Gia_Man_t *p, int Id)
Definition: gia.h:912
Gia_ObjSetNext
static void Gia_ObjSetNext(Gia_Man_t *p, int Id, int Num)
Definition: gia.h:913
GIA_VOID
#define GIA_VOID
Definition: gia.h:45
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Gia_ObjRepr
static int Gia_ObjRepr(Gia_Man_t *p, int Id)
Definition: gia.h:887
static void Gia_Sim2SimulateCo ( Gia_Sim2_t *  p,
Gia_Obj_t *  pObj 
)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 191 of file giaSim2.c.

192 {
193  unsigned * pInfo = Gia_Sim2Data( p, Gia_ObjValue(pObj) );
194  unsigned * pInfo0 = Gia_Sim2Data( p, Gia_ObjFaninId0(pObj, Gia_ObjValue(pObj)) );
195  int w;
196  if ( Gia_ObjFaninC0(pObj) )
197  for ( w = p->nWords-1; w >= 0; w-- )
198  pInfo[w] = ~pInfo0[w];
199  else
200  for ( w = p->nWords-1; w >= 0; w-- )
201  pInfo[w] = pInfo0[w];
202 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Gia_ObjValue
static int Gia_ObjValue(Gia_Obj_t *pObj)
Definition: gia.h:413
Gia_Sim2Data
static unsigned * Gia_Sim2Data(Gia_Sim2_t *p, int i)
Definition: giaSim2.c:41
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Gia_ObjFaninId0
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
static void Gia_Sim2SimulateNode ( Gia_Sim2_t *  p,
Gia_Obj_t *  pObj 
)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 215 of file giaSim2.c.

216 {
217  unsigned * pInfo = Gia_Sim2Data( p, Gia_ObjValue(pObj) );
218  unsigned * pInfo0 = Gia_Sim2Data( p, Gia_ObjFaninId0(pObj, Gia_ObjValue(pObj)) );
219  unsigned * pInfo1 = Gia_Sim2Data( p, Gia_ObjFaninId1(pObj, Gia_ObjValue(pObj)) );
220  int w;
221  if ( Gia_ObjFaninC0(pObj) )
222  {
223  if ( Gia_ObjFaninC1(pObj) )
224  for ( w = p->nWords-1; w >= 0; w-- )
225  pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
226  else
227  for ( w = p->nWords-1; w >= 0; w-- )
228  pInfo[w] = ~pInfo0[w] & pInfo1[w];
229  }
230  else
231  {
232  if ( Gia_ObjFaninC1(pObj) )
233  for ( w = p->nWords-1; w >= 0; w-- )
234  pInfo[w] = pInfo0[w] & ~pInfo1[w];
235  else
236  for ( w = p->nWords-1; w >= 0; w-- )
237  pInfo[w] = pInfo0[w] & pInfo1[w];
238  }
239 }
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Gia_ObjValue
static int Gia_ObjValue(Gia_Obj_t *pObj)
Definition: gia.h:413
Gia_Sim2Data
static unsigned * Gia_Sim2Data(Gia_Sim2_t *p, int i)
Definition: giaSim2.c:41
Gia_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Gia_ObjFaninId1
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:461
Gia_ObjFaninId0
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
static void Gia_Sim2SimulateRound ( Gia_Sim2_t *  p)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 276 of file giaSim2.c.

277 {
278  Gia_Obj_t * pObj;
279  int i;
280  pObj = Gia_ManConst0(p->pAig);
281  assert( Gia_ObjValue(pObj) == 0 );
282  Gia_Sim2InfoZero( p, Gia_Sim2Data(p, Gia_ObjValue(pObj)) );
283  Gia_ManForEachPi( p->pAig, pObj, i )
284  Gia_Sim2InfoRandom( p, Gia_Sim2Data(p, Gia_ObjValue(pObj)) );
285  Gia_ManForEachAnd( p->pAig, pObj, i )
286  {
287  assert( Gia_ObjValue(pObj) == i );
288  Gia_Sim2SimulateNode( p, pObj );
289  }
290  Gia_ManForEachCo( p->pAig, pObj, i )
291  Gia_Sim2SimulateCo( p, pObj );
292 }
Llb_Mgr_t_::pAig
Aig_Man_t * pAig
Definition: llb3Image.c:49
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Gia_ObjValue
static int Gia_ObjValue(Gia_Obj_t *pObj)
Definition: gia.h:413
Gia_Sim2InfoZero
static void Gia_Sim2InfoZero(Gia_Sim2_t *p, unsigned *pInfo)
Definition: giaSim2.c:137
Gia_Obj_t_
Definition: gia.h:75
Gia_Sim2Data
static unsigned * Gia_Sim2Data(Gia_Sim2_t *p, int i)
Definition: giaSim2.c:41
Gia_Sim2SimulateCo
static void Gia_Sim2SimulateCo(Gia_Sim2_t *p, Gia_Obj_t *pObj)
Definition: giaSim2.c:191
Gia_Sim2SimulateNode
static void Gia_Sim2SimulateNode(Gia_Sim2_t *p, Gia_Obj_t *pObj)
Definition: giaSim2.c:215
Gia_Sim2InfoRandom
static void Gia_Sim2InfoRandom(Gia_Sim2_t *p, unsigned *pInfo)
Definition: giaSim2.c:119
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
assert
#define assert(ex)
Definition: util_old.h:213