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

Go to the source code of this file.

Data Structures

struct  Ssw_Sml_t_
 DECLARATIONS ///. More...
 

Functions

static unsigned * Ssw_ObjSim (Ssw_Sml_t *p, int Id)
 
static unsigned Ssw_ObjRandomSim ()
 
unsigned Ssw_SmlObjHashWord (Ssw_Sml_t *p, Aig_Obj_t *pObj)
 FUNCTION DEFINITIONS ///. More...
 
int Ssw_SmlObjIsConstWord (Ssw_Sml_t *p, Aig_Obj_t *pObj)
 
int Ssw_SmlObjsAreEqualWord (Ssw_Sml_t *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
 
int Ssw_SmlObjIsConstBit (void *p, Aig_Obj_t *pObj)
 
int Ssw_SmlObjsAreEqualBit (void *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
 
int Ssw_SmlNodeNotEquWeight (Ssw_Sml_t *p, int Left, int Right)
 
int Ssw_SmlCheckXorImplication (Ssw_Sml_t *p, Aig_Obj_t *pObjLi, Aig_Obj_t *pObjLo, Aig_Obj_t *pCand)
 DECLARATIONS ///. More...
 
int Ssw_SmlCountXorImplication (Ssw_Sml_t *p, Aig_Obj_t *pObjLi, Aig_Obj_t *pObjLo, Aig_Obj_t *pCand)
 
int Ssw_SmlCountEqual (Ssw_Sml_t *p, Aig_Obj_t *pObjLi, Aig_Obj_t *pObjLo)
 
int Ssw_SmlNodeIsZero (Ssw_Sml_t *p, Aig_Obj_t *pObj)
 
int Ssw_SmlNodeIsZeroFrame (Ssw_Sml_t *p, Aig_Obj_t *pObj, int f)
 
int Ssw_SmlNodeCountOnesReal (Ssw_Sml_t *p, Aig_Obj_t *pObj)
 
int Ssw_SmlNodeCountOnesRealVec (Ssw_Sml_t *p, Vec_Ptr_t *vObjs)
 
void Ssw_SmlSavePattern0 (Ssw_Man_t *p, int fInit)
 
void Ssw_SmlSavePattern1 (Ssw_Man_t *p, int fInit)
 
int * Ssw_SmlCheckOutputSavePattern (Ssw_Sml_t *p, Aig_Obj_t *pObjPo)
 
int * Ssw_SmlCheckOutput (Ssw_Sml_t *p)
 
void Ssw_SmlAssignRandom (Ssw_Sml_t *p, Aig_Obj_t *pObj)
 
void Ssw_SmlAssignRandomFrame (Ssw_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
 
void Ssw_SmlObjAssignConst (Ssw_Sml_t *p, Aig_Obj_t *pObj, int fConst1, int iFrame)
 
void Ssw_SmlObjAssignConstWord (Ssw_Sml_t *p, Aig_Obj_t *pObj, int fConst1, int iFrame, int iWord)
 
void Ssw_SmlObjSetWord (Ssw_Sml_t *p, Aig_Obj_t *pObj, unsigned Word, int iWord, int iFrame)
 
void Ssw_SmlAssignDist1 (Ssw_Sml_t *p, unsigned *pPat)
 
void Ssw_SmlAssignDist1Plus (Ssw_Sml_t *p, unsigned *pPat)
 
void Ssw_SmlNodeSimulate (Ssw_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
 
int Ssw_SmlNodesCompareInFrame (Ssw_Sml_t *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1, int iFrame0, int iFrame1)
 
void Ssw_SmlNodeCopyFanin (Ssw_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
 
void Ssw_SmlNodeTransferNext (Ssw_Sml_t *p, Aig_Obj_t *pOut, Aig_Obj_t *pIn, int iFrame)
 
void Ssw_SmlNodeTransferFirst (Ssw_Sml_t *p, Aig_Obj_t *pOut, Aig_Obj_t *pIn)
 
void Ssw_SmlInitialize (Ssw_Sml_t *p, int fInit)
 
void Ssw_SmlInitializeSpecial (Ssw_Sml_t *p, Vec_Int_t *vInit)
 
void Ssw_SmlReinitialize (Ssw_Sml_t *p)
 
int Ssw_SmlCheckNonConstOutputs (Ssw_Sml_t *p)
 
void Ssw_SmlSimulateOne (Ssw_Sml_t *p)
 
void Ssw_SmlUnnormalize (Ssw_Sml_t *p)
 
void Ssw_SmlSimulateOneDyn_rec (Ssw_Sml_t *p, Aig_Obj_t *pObj, int f, int *pVisited, int nVisCounter)
 
void Ssw_SmlSimulateOneFrame (Ssw_Sml_t *p)
 
Ssw_Sml_t * Ssw_SmlStart (Aig_Man_t *pAig, int nPref, int nFrames, int nWordsFrame)
 
void Ssw_SmlClean (Ssw_Sml_t *p)
 
Vec_Ptr_t * Ssw_SmlSimDataPointers (Ssw_Sml_t *p)
 
void Ssw_SmlStop (Ssw_Sml_t *p)
 
Ssw_Sml_t * Ssw_SmlSimulateComb (Aig_Man_t *pAig, int nWords)
 
Ssw_Sml_t * Ssw_SmlSimulateSeq (Aig_Man_t *pAig, int nPref, int nFrames, int nWords)
 
void Ssw_SmlResimulateSeq (Ssw_Sml_t *p)
 
int Ssw_SmlNumFrames (Ssw_Sml_t *p)
 
int Ssw_SmlNumWordsTotal (Ssw_Sml_t *p)
 
unsigned * Ssw_SmlSimInfo (Ssw_Sml_t *p, Aig_Obj_t *pObj)
 
Abc_Cex_t * Ssw_SmlGetCounterExample (Ssw_Sml_t *p)
 

Function Documentation

static unsigned Ssw_ObjRandomSim ( )
inlinestatic

Definition at line 46 of file sswSim.c.

46 { return Aig_ManRandom(0); }
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition: aigUtil.c:1157
static unsigned* Ssw_ObjSim ( Ssw_Sml_t *  p,
int  Id 
)
inlinestatic

Definition at line 45 of file sswSim.c.

45 { return p->pData + p->nWordsTotal * Id; }
Ssw_Sml_t_::pData
unsigned pData[0]
Definition: sswSim.c:42
Ssw_Sml_t_::nWordsTotal
int nWordsTotal
Definition: sswSim.c:37
void Ssw_SmlAssignDist1 ( Ssw_Sml_t *  p,
unsigned *  pPat 
)

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

Synopsis [Assings distance-1 simulation info for the PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 623 of file sswSim.c.

624 {
625  Aig_Obj_t * pObj;
626  int f, i, k, Limit, nTruePis;
627  assert( p->nFrames > 0 );
628  if ( p->nFrames == 1 )
629  {
630  // copy the PI info
631  Aig_ManForEachCi( p->pAig, pObj, i )
632  Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 );
633  // flip one bit
634  Limit = Abc_MinInt( Aig_ManCiNum(p->pAig), p->nWordsTotal * 32 - 1 );
635  for ( i = 0; i < Limit; i++ )
636  Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManCi(p->pAig,i)->Id ), i+1 );
637  }
638  else
639  {
640  int fUseDist1 = 0;
641 
642  // copy the PI info for each frame
643  nTruePis = Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig);
644  for ( f = 0; f < p->nFrames; f++ )
645  Saig_ManForEachPi( p->pAig, pObj, i )
646  Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * f + i), f );
647  // copy the latch info
648  k = 0;
649  Saig_ManForEachLo( p->pAig, pObj, i )
650  Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
651 // assert( p->pFrames == NULL || nTruePis * p->nFrames + k == Aig_ManCiNum(p->pFrames) );
652 
653  // flip one bit of the last frame
654  if ( fUseDist1 ) //&& p->nFrames == 2 )
655  {
656  Limit = Abc_MinInt( nTruePis, p->nWordsFrame * 32 - 1 );
657  for ( i = 0; i < Limit; i++ )
658  Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManCi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 );
659  }
660  }
661 }
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
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Ssw_SmlObjAssignConst
void Ssw_SmlObjAssignConst(Ssw_Sml_t *p, Aig_Obj_t *pObj, int fConst1, int iFrame)
Definition: sswSim.c:560
for
for(p=first;p->value< newval;p=p->next)
Abc_MinInt
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
Aig_ManCi
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
if
if(last==0)
Definition: sparse_int.h:34
else
else
Definition: sparse_int.h:55
Aig_Obj_t_
Definition: aig.h:69
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
Ssw_Sml_t_::pAig
Aig_Man_t * pAig
Definition: sswSim.c:33
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
assert
#define assert(ex)
Definition: util_old.h:213
Ssw_Sml_t_::nFrames
int nFrames
Definition: sswSim.c:35
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
void Ssw_SmlAssignDist1Plus ( Ssw_Sml_t *  p,
unsigned *  pPat 
)

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

Synopsis [Assings distance-1 simulation info for the PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 674 of file sswSim.c.

675 {
676  Aig_Obj_t * pObj;
677  int f, i, Limit;
678  assert( p->nFrames > 0 );
679 
680  // copy the pattern into the primary inputs
681  Aig_ManForEachCi( p->pAig, pObj, i )
682  Ssw_SmlObjAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 );
683 
684  // set distance one PIs for the first frame
685  Limit = Abc_MinInt( Saig_ManPiNum(p->pAig), p->nWordsFrame * 32 - 1 );
686  for ( i = 0; i < Limit; i++ )
687  Abc_InfoXorBit( Ssw_ObjSim( p, Aig_ManCi(p->pAig, i)->Id ), i+1 );
688 
689  // create random info for the remaining timeframes
690  for ( f = 1; f < p->nFrames; f++ )
691  Saig_ManForEachPi( p->pAig, pObj, i )
692  Ssw_SmlAssignRandomFrame( p, pObj, f );
693 }
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
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Ssw_SmlObjAssignConst
void Ssw_SmlObjAssignConst(Ssw_Sml_t *p, Aig_Obj_t *pObj, int fConst1, int iFrame)
Definition: sswSim.c:560
for
for(p=first;p->value< newval;p=p->next)
Abc_MinInt
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
Aig_ManCi
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
Aig_Obj_t_
Definition: aig.h:69
Ssw_Sml_t_::pAig
Aig_Man_t * pAig
Definition: sswSim.c:33
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
Ssw_SmlAssignRandomFrame
void Ssw_SmlAssignRandomFrame(Ssw_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: sswSim.c:538
assert
#define assert(ex)
Definition: util_old.h:213
Ssw_Sml_t_::nFrames
int nFrames
Definition: sswSim.c:35
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
void Ssw_SmlAssignRandom ( Ssw_Sml_t *  p,
Aig_Obj_t *  pObj 
)

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

Synopsis [Assigns random patterns to the PI node.]

Description []

SideEffects []

SeeAlso []

Definition at line 513 of file sswSim.c.

514 {
515  unsigned * pSims;
516  int i, f;
517  assert( Aig_ObjIsCi(pObj) );
518  pSims = Ssw_ObjSim( p, pObj->Id );
519  for ( i = 0; i < p->nWordsTotal; i++ )
520  pSims[i] = Ssw_ObjRandomSim();
521  // set the first bit 0 in each frame
522  assert( p->nWordsFrame * p->nFrames == p->nWordsTotal );
523  for ( f = 0; f < p->nFrames; f++ )
524  pSims[p->nWordsFrame*f] <<= 1;
525 }
Ssw_Sml_t_::nWordsFrame
int nWordsFrame
Definition: sswSim.c:36
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Ssw_Sml_t_::nWordsTotal
int nWordsTotal
Definition: sswSim.c:37
Ssw_ObjRandomSim
static unsigned Ssw_ObjRandomSim()
Definition: sswSim.c:46
assert
#define assert(ex)
Definition: util_old.h:213
Ssw_Sml_t_::nFrames
int nFrames
Definition: sswSim.c:35
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
void Ssw_SmlAssignRandomFrame ( Ssw_Sml_t *  p,
Aig_Obj_t *  pObj,
int  iFrame 
)

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

Synopsis [Assigns random patterns to the PI node.]

Description []

SideEffects []

SeeAlso []

Definition at line 538 of file sswSim.c.

539 {
540  unsigned * pSims;
541  int i;
542  assert( iFrame < p->nFrames );
543  assert( Aig_ObjIsCi(pObj) );
544  pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
545  for ( i = 0; i < p->nWordsFrame; i++ )
546  pSims[i] = Ssw_ObjRandomSim();
547 }
Ssw_Sml_t_::nWordsFrame
int nWordsFrame
Definition: sswSim.c:36
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Ssw_ObjRandomSim
static unsigned Ssw_ObjRandomSim()
Definition: sswSim.c:46
assert
#define assert(ex)
Definition: util_old.h:213
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
int Ssw_SmlCheckNonConstOutputs ( Ssw_Sml_t *  p)

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

Synopsis [Check if any of the POs becomes non-constant.]

Description []

SideEffects []

SeeAlso []

Definition at line 980 of file sswSim.c.

981 {
982  Aig_Obj_t * pObj;
983  int i;
984  Saig_ManForEachPo( p->pAig, pObj, i )
985  {
986  if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs )
987  return 0;
988  if ( !Ssw_SmlNodeIsZero(p, pObj) )
989  return 1;
990  }
991  return 0;
992 }
Saig_ManPoNum
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
Ssw_SmlNodeIsZero
int Ssw_SmlNodeIsZero(Ssw_Sml_t *p, Aig_Obj_t *pObj)
Definition: sswSim.c:294
Aig_Obj_t_
Definition: aig.h:69
Ssw_Sml_t_::pAig
Aig_Man_t * pAig
Definition: sswSim.c:33
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
int* Ssw_SmlCheckOutput ( Ssw_Sml_t *  p)

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

Synopsis [Returns 1 if the one of the output is already non-constant 0.]

Description []

SideEffects []

SeeAlso []

Definition at line 482 of file sswSim.c.

483 {
484  Aig_Obj_t * pObj;
485  int i;
486  // make sure the reference simulation pattern does not detect the bug
487  pObj = Aig_ManCo( p->pAig, 0 );
488  assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) );
489  Aig_ManForEachCo( p->pAig, pObj, i )
490  {
491  if ( !Ssw_SmlObjIsConstWord( p, Aig_ObjFanin0(pObj) ) )
492  {
493  // create the counter-example from this pattern
494  return Ssw_SmlCheckOutputSavePattern( p, pObj );
495  }
496  }
497  return NULL;
498 }
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
Ssw_SmlObjIsConstWord
int Ssw_SmlObjIsConstWord(Ssw_Sml_t *p, Aig_Obj_t *pObj)
Definition: sswSim.c:102
Aig_Obj_t_
Definition: aig.h:69
Ssw_Sml_t_::pAig
Aig_Man_t * pAig
Definition: sswSim.c:33
Aig_ObjFaninC0
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
Aig_ManCo
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
Ssw_SmlCheckOutputSavePattern
int * Ssw_SmlCheckOutputSavePattern(Ssw_Sml_t *p, Aig_Obj_t *pObjPo)
Definition: sswSim.c:440
assert
#define assert(ex)
Definition: util_old.h:213
int* Ssw_SmlCheckOutputSavePattern ( Ssw_Sml_t *  p,
Aig_Obj_t *  pObjPo 
)

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

Synopsis [Creates the counter-example from the successful pattern.]

Description []

SideEffects []

SeeAlso []

Definition at line 440 of file sswSim.c.

441 {
442  Aig_Obj_t * pFanin, * pObjPi;
443  unsigned * pSims;
444  int i, k, BestPat, * pModel;
445  // find the word of the pattern
446  pFanin = Aig_ObjFanin0(pObjPo);
447  pSims = Ssw_ObjSim(p, pFanin->Id);
448  for ( i = 0; i < p->nWordsTotal; i++ )
449  if ( pSims[i] )
450  break;
451  assert( i < p->nWordsTotal );
452  // find the bit of the pattern
453  for ( k = 0; k < 32; k++ )
454  if ( pSims[i] & (1 << k) )
455  break;
456  assert( k < 32 );
457  // determine the best pattern
458  BestPat = i * 32 + k;
459  // fill in the counter-example data
460  pModel = ABC_ALLOC( int, Aig_ManCiNum(p->pAig)+1 );
461  Aig_ManForEachCi( p->pAig, pObjPi, i )
462  {
463  pModel[i] = Abc_InfoHasBit(Ssw_ObjSim(p, pObjPi->Id), BestPat);
464 // Abc_Print( 1, "%d", pModel[i] );
465  }
466  pModel[Aig_ManCiNum(p->pAig)] = pObjPo->Id;
467 // Abc_Print( 1, "\n" );
468  return pModel;
469 }
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Ssw_Sml_t_::nWordsTotal
int nWordsTotal
Definition: sswSim.c:37
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Aig_Obj_t_
Definition: aig.h:69
Ssw_Sml_t_::pAig
Aig_Man_t * pAig
Definition: sswSim.c:33
assert
#define assert(ex)
Definition: util_old.h:213
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
int Ssw_SmlCheckXorImplication ( Ssw_Sml_t *  p,
Aig_Obj_t *  pObjLi,
Aig_Obj_t *  pObjLo,
Aig_Obj_t *  pCand 
)

DECLARATIONS ///.

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

Synopsis [Checks implication.]

Description []

SideEffects []

SeeAlso []

Definition at line 202 of file sswSim.c.

203 {
204  unsigned * pSimLi, * pSimLo, * pSimCand;
205  int k;
206  assert( pObjLo->fPhase == 0 );
207  // pObjLi->fPhase may be 1, but the LI simulation data is not complemented!
208  pSimCand = Ssw_ObjSim( p, Aig_Regular(pCand)->Id );
209  pSimLi = Ssw_ObjSim( p, pObjLi->Id );
210  pSimLo = Ssw_ObjSim( p, pObjLo->Id );
211  if ( Aig_Regular(pCand)->fPhase ^ Aig_IsComplement(pCand) )
212  {
213  for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
214  if ( ~pSimCand[k] & (pSimLi[k] ^ pSimLo[k]) )
215  return 0;
216  }
217  else
218  {
219  for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
220  if ( pSimCand[k] & (pSimLi[k] ^ pSimLo[k]) )
221  return 0;
222  }
223  return 1;
224 }
Ssw_Sml_t_::nWordsPref
int nWordsPref
Definition: sswSim.c:38
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
assert
#define assert(ex)
Definition: util_old.h:213
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
void Ssw_SmlClean ( Ssw_Sml_t *  p)

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

Synopsis [Allocates simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 1173 of file sswSim.c.

1174 {
1175  memset( p->pData, 0, sizeof(unsigned) * Aig_ManObjNumMax(p->pAig) * p->nWordsTotal );
1176 }
memset
char * memset()
Ssw_Sml_t_::pData
unsigned pData[0]
Definition: sswSim.c:42
Ssw_Sml_t_::nWordsTotal
int nWordsTotal
Definition: sswSim.c:37
Ssw_Sml_t_::pAig
Aig_Man_t * pAig
Definition: sswSim.c:33
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
int Ssw_SmlCountEqual ( Ssw_Sml_t *  p,
Aig_Obj_t *  pObjLi,
Aig_Obj_t *  pObjLo 
)

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

Synopsis [Counts the number of 1s in the implication.]

Description []

SideEffects []

SeeAlso []

Definition at line 270 of file sswSim.c.

271 {
272  unsigned * pSimLi, * pSimLo;
273  int k, Counter = 0;
274  assert( pObjLo->fPhase == 0 );
275  // pObjLi->fPhase may be 1, but the LI simulation data is not complemented!
276  pSimLi = Ssw_ObjSim( p, pObjLi->Id );
277  pSimLo = Ssw_ObjSim( p, pObjLo->Id );
278  for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
279  Counter += Aig_WordCountOnes( ~(pSimLi[k] ^ pSimLo[k]) );
280  return Counter;
281 }
Ssw_Sml_t_::nWordsPref
int nWordsPref
Definition: sswSim.c:38
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Aig_WordCountOnes
static int Aig_WordCountOnes(unsigned uWord)
Definition: aig.h:229
Counter
static int Counter
Definition: extraBddMisc.c:1877
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
assert
#define assert(ex)
Definition: util_old.h:213
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
int Ssw_SmlCountXorImplication ( Ssw_Sml_t *  p,
Aig_Obj_t *  pObjLi,
Aig_Obj_t *  pObjLo,
Aig_Obj_t *  pCand 
)

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

Synopsis [Counts the number of 1s in the implication.]

Description []

SideEffects []

SeeAlso []

Definition at line 237 of file sswSim.c.

238 {
239  unsigned * pSimLi, * pSimLo, * pSimCand;
240  int k, Counter = 0;
241  assert( pObjLo->fPhase == 0 );
242  // pObjLi->fPhase may be 1, but the LI simulation data is not complemented!
243  pSimCand = Ssw_ObjSim( p, Aig_Regular(pCand)->Id );
244  pSimLi = Ssw_ObjSim( p, pObjLi->Id );
245  pSimLo = Ssw_ObjSim( p, pObjLo->Id );
246  if ( Aig_Regular(pCand)->fPhase ^ Aig_IsComplement(pCand) )
247  {
248  for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
249  Counter += Aig_WordCountOnes(~pSimCand[k] & ~(pSimLi[k] ^ pSimLo[k]));
250  }
251  else
252  {
253  for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
254  Counter += Aig_WordCountOnes(pSimCand[k] & ~(pSimLi[k] ^ pSimLo[k]));
255  }
256  return Counter;
257 }
Ssw_Sml_t_::nWordsPref
int nWordsPref
Definition: sswSim.c:38
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Aig_WordCountOnes
static int Aig_WordCountOnes(unsigned uWord)
Definition: aig.h:229
Counter
static int Counter
Definition: extraBddMisc.c:1877
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
assert
#define assert(ex)
Definition: util_old.h:213
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Abc_Cex_t* Ssw_SmlGetCounterExample ( Ssw_Sml_t *  p)

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

Synopsis [Creates sequential counter-example from the simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 1338 of file sswSim.c.

1339 {
1340  Abc_Cex_t * pCex;
1341  Aig_Obj_t * pObj;
1342  unsigned * pSims;
1343  int iPo, iFrame, iBit, i, k;
1344 
1345  // make sure the simulation manager has it
1346  assert( p->fNonConstOut );
1347 
1348  // find the first output that failed
1349  iPo = -1;
1350  iBit = -1;
1351  iFrame = -1;
1352  Saig_ManForEachPo( p->pAig, pObj, iPo )
1353  {
1354  if ( Ssw_SmlNodeIsZero(p, pObj) )
1355  continue;
1356  pSims = Ssw_ObjSim( p, pObj->Id );
1357  for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
1358  if ( pSims[i] )
1359  {
1360  iFrame = i / p->nWordsFrame;
1361  iBit = 32 * (i % p->nWordsFrame) + Aig_WordFindFirstBit( pSims[i] );
1362  break;
1363  }
1364  break;
1365  }
1366  assert( iPo < Aig_ManCoNum(p->pAig)-Aig_ManRegNum(p->pAig) );
1367  assert( iFrame < p->nFrames );
1368  assert( iBit < 32 * p->nWordsFrame );
1369 
1370  // allocate the counter example
1371  pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
1372  pCex->iPo = iPo;
1373  pCex->iFrame = iFrame;
1374 
1375  // copy the bit data
1376  Saig_ManForEachLo( p->pAig, pObj, k )
1377  {
1378  pSims = Ssw_ObjSim( p, pObj->Id );
1379  if ( Abc_InfoHasBit( pSims, iBit ) )
1380  Abc_InfoSetBit( pCex->pData, k );
1381  }
1382  for ( i = 0; i <= iFrame; i++ )
1383  {
1384  Saig_ManForEachPi( p->pAig, pObj, k )
1385  {
1386  pSims = Ssw_ObjSim( p, pObj->Id );
1387  if ( Abc_InfoHasBit( pSims, 32 * p->nWordsFrame * i + iBit ) )
1388  Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * i + k );
1389  }
1390  }
1391  // verify the counter example
1392  if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
1393  {
1394  Abc_Print( 1, "Ssw_SmlGetCounterExample(): Counter-example is invalid.\n" );
1395  Abc_CexFree( pCex );
1396  pCex = NULL;
1397  }
1398  return pCex;
1399 }
Ssw_Sml_t_::nWordsPref
int nWordsPref
Definition: sswSim.c:38
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
Saig_ManVerifyCex
int Saig_ManVerifyCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition: saigDup.c:279
Ssw_Sml_t_::nWordsFrame
int nWordsFrame
Definition: sswSim.c:36
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Aig_ManCoNum
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
Ssw_SmlNodeIsZero
int Ssw_SmlNodeIsZero(Ssw_Sml_t *p, Aig_Obj_t *pObj)
Definition: sswSim.c:294
Aig_WordFindFirstBit
static int Aig_WordFindFirstBit(unsigned uWord)
Definition: aig.h:237
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Ssw_Sml_t_::fNonConstOut
int fNonConstOut
Definition: sswSim.c:39
Aig_Obj_t_
Definition: aig.h:69
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
Ssw_Sml_t_::pAig
Aig_Man_t * pAig
Definition: sswSim.c:33
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
assert
#define assert(ex)
Definition: util_old.h:213
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Abc_CexFree
void Abc_CexFree(Abc_Cex_t *p)
Definition: utilCex.c:371
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
void Ssw_SmlInitialize ( Ssw_Sml_t *  p,
int  fInit 
)

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

Synopsis [Assings random simulation info for the PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 895 of file sswSim.c.

896 {
897  Aig_Obj_t * pObj;
898  int i;
899  if ( fInit )
900  {
901  assert( Aig_ManRegNum(p->pAig) > 0 );
902  assert( Aig_ManRegNum(p->pAig) <= Aig_ManCiNum(p->pAig) );
903  // assign random info for primary inputs
904  Saig_ManForEachPi( p->pAig, pObj, i )
905  Ssw_SmlAssignRandom( p, pObj );
906  // assign the initial state for the latches
907  Saig_ManForEachLo( p->pAig, pObj, i )
908  Ssw_SmlObjAssignConst( p, pObj, 0, 0 );
909  }
910  else
911  {
912  Aig_ManForEachCi( p->pAig, pObj, i )
913  Ssw_SmlAssignRandom( p, pObj );
914  }
915 }
Ssw_SmlAssignRandom
void Ssw_SmlAssignRandom(Ssw_Sml_t *p, Aig_Obj_t *pObj)
Definition: sswSim.c:513
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Ssw_SmlObjAssignConst
void Ssw_SmlObjAssignConst(Ssw_Sml_t *p, Aig_Obj_t *pObj, int fConst1, int iFrame)
Definition: sswSim.c:560
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
else
else
Definition: sparse_int.h:55
Aig_Obj_t_
Definition: aig.h:69
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
Ssw_Sml_t_::pAig
Aig_Man_t * pAig
Definition: sswSim.c:33
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
assert
#define assert(ex)
Definition: util_old.h:213
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
void Ssw_SmlInitializeSpecial ( Ssw_Sml_t *  p,
Vec_Int_t *  vInit 
)

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

Synopsis [Assings random simulation info for the PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 928 of file sswSim.c.

929 {
930  Aig_Obj_t * pObj;
931  int Entry, i, nRegs;
932  nRegs = Aig_ManRegNum(p->pAig);
933  assert( nRegs > 0 );
934  assert( nRegs <= Aig_ManCiNum(p->pAig) );
935  assert( Vec_IntSize(vInit) == nRegs * p->nWordsFrame );
936  // assign random info for primary inputs
937  Saig_ManForEachPi( p->pAig, pObj, i )
938  Ssw_SmlAssignRandom( p, pObj );
939  // assign the initial state for the latches
940  Vec_IntForEachEntry( vInit, Entry, i )
941  Ssw_SmlObjAssignConstWord( p, Saig_ManLo(p->pAig, i % nRegs), Entry, 0, i / nRegs );
942 }
Ssw_SmlObjAssignConstWord
void Ssw_SmlObjAssignConstWord(Ssw_Sml_t *p, Aig_Obj_t *pObj, int fConst1, int iFrame, int iWord)
Definition: sswSim.c:582
Saig_ManLo
static Aig_Obj_t * Saig_ManLo(Aig_Man_t *p, int i)
Definition: saig.h:79
Ssw_SmlAssignRandom
void Ssw_SmlAssignRandom(Ssw_Sml_t *p, Aig_Obj_t *pObj)
Definition: sswSim.c:513
Ssw_Sml_t_::nWordsFrame
int nWordsFrame
Definition: sswSim.c:36
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Aig_Obj_t_
Definition: aig.h:69
Ssw_Sml_t_::pAig
Aig_Man_t * pAig
Definition: sswSim.c:33
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
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
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
void Ssw_SmlNodeCopyFanin ( Ssw_Sml_t *  p,
Aig_Obj_t *  pObj,
int  iFrame 
)

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

Synopsis [Simulates one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 803 of file sswSim.c.

804 {
805  unsigned * pSims, * pSims0;
806  int fCompl, fCompl0, i;
807  assert( iFrame < p->nFrames );
808  assert( !Aig_IsComplement(pObj) );
809  assert( Aig_ObjIsCo(pObj) );
810  assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
811  // get hold of the simulation information
812  pSims = Ssw_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame;
813  pSims0 = Ssw_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + p->nWordsFrame * iFrame;
814  // get complemented attributes of the children using their random info
815  fCompl = pObj->fPhase;
816  fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
817  // copy information as it is
818  if ( fCompl0 )
819  for ( i = 0; i < p->nWordsFrame; i++ )
820  pSims[i] = ~pSims0[i];
821  else
822  for ( i = 0; i < p->nWordsFrame; i++ )
823  pSims[i] = pSims0[i];
824 }
Aig_ObjChild0
static Aig_Obj_t * Aig_ObjChild0(Aig_Obj_t *pObj)
Definition: aig.h:310
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Ssw_Sml_t_::nWordsFrame
int nWordsFrame
Definition: sswSim.c:36
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Ssw_Sml_t_::nWordsTotal
int nWordsTotal
Definition: sswSim.c:37
Aig_ObjPhaseReal
static int Aig_ObjPhaseReal(Aig_Obj_t *pObj)
Definition: aig.h:299
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
assert
#define assert(ex)
Definition: util_old.h:213
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
int Ssw_SmlNodeCountOnesReal ( Ssw_Sml_t *  p,
Aig_Obj_t *  pObj 
)

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

Synopsis [Counts the number of one's in the pattern of the object.]

Description []

SideEffects []

SeeAlso []

Definition at line 333 of file sswSim.c.

334 {
335  unsigned * pSims;
336  int i, Counter = 0;
337  pSims = Ssw_ObjSim(p, Aig_Regular(pObj)->Id);
338  if ( Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) )
339  {
340  for ( i = 0; i < p->nWordsTotal; i++ )
341  Counter += Aig_WordCountOnes( ~pSims[i] );
342  }
343  else
344  {
345  for ( i = 0; i < p->nWordsTotal; i++ )
346  Counter += Aig_WordCountOnes( pSims[i] );
347  }
348  return Counter;
349 }
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Aig_WordCountOnes
static int Aig_WordCountOnes(unsigned uWord)
Definition: aig.h:229
Ssw_Sml_t_::nWordsTotal
int nWordsTotal
Definition: sswSim.c:37
Counter
static int Counter
Definition: extraBddMisc.c:1877
int Ssw_SmlNodeCountOnesRealVec ( Ssw_Sml_t *  p,
Vec_Ptr_t *  vObjs 
)

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

Synopsis [Counts the number of one's in the pattern of the objects.]

Description []

SideEffects []

SeeAlso []

Definition at line 362 of file sswSim.c.

363 {
364  Aig_Obj_t * pObj;
365  unsigned * pSims, uWord;
366  int i, k, Counter = 0;
367  if ( Vec_PtrSize(vObjs) == 0 )
368  return 0;
369  for ( i = 0; i < p->nWordsTotal; i++ )
370  {
371  uWord = 0;
372  Vec_PtrForEachEntry( Aig_Obj_t *, vObjs, pObj, k )
373  {
374  pSims = Ssw_ObjSim(p, Aig_Regular(pObj)->Id);
375  if ( Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) )
376  uWord |= ~pSims[i];
377  else
378  uWord |= pSims[i];
379  }
380  Counter += Aig_WordCountOnes( uWord );
381  }
382  return Counter;
383 }
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Aig_Regular
static Aig_Obj_t * Aig_Regular(Aig_Obj_t *p)
Definition: aig.h:246
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Aig_WordCountOnes
static int Aig_WordCountOnes(unsigned uWord)
Definition: aig.h:229
Ssw_Sml_t_::nWordsTotal
int nWordsTotal
Definition: sswSim.c:37
Aig_Obj_t_
Definition: aig.h:69
Counter
static int Counter
Definition: extraBddMisc.c:1877
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
int Ssw_SmlNodeIsZero ( Ssw_Sml_t *  p,
Aig_Obj_t *  pObj 
)

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

Synopsis [Returns 1 if simulation info is composed of all zeros.]

Description []

SideEffects []

SeeAlso []

Definition at line 294 of file sswSim.c.

295 {
296  unsigned * pSims;
297  int i;
298  pSims = Ssw_ObjSim(p, pObj->Id);
299  for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
300  if ( pSims[i] )
301  return 0;
302  return 1;
303 }
Ssw_Sml_t_::nWordsPref
int nWordsPref
Definition: sswSim.c:38
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
int Ssw_SmlNodeIsZeroFrame ( Ssw_Sml_t *  p,
Aig_Obj_t *  pObj,
int  f 
)

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

Synopsis [Returns 1 if simulation info is composed of all zeros.]

Description []

SideEffects []

SeeAlso []

Definition at line 316 of file sswSim.c.

317 {
318  unsigned * pSims = Ssw_ObjSim(p, pObj->Id);
319  return pSims[f] == 0;
320 }
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
int Ssw_SmlNodeNotEquWeight ( Ssw_Sml_t *  p,
int  Left,
int  Right 
)

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

Synopsis [Counts the number of 1s in the XOR of simulation data.]

Description []

SideEffects []

SeeAlso []

Definition at line 180 of file sswSim.c.

181 {
182  unsigned * pSimL, * pSimR;
183  int k, Counter = 0;
184  pSimL = Ssw_ObjSim( p, Left );
185  pSimR = Ssw_ObjSim( p, Right );
186  for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
187  Counter += Aig_WordCountOnes( pSimL[k] ^ pSimR[k] );
188  return Counter;
189 }
Ssw_Sml_t_::nWordsPref
int nWordsPref
Definition: sswSim.c:38
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Aig_WordCountOnes
static int Aig_WordCountOnes(unsigned uWord)
Definition: aig.h:229
Counter
static int Counter
Definition: extraBddMisc.c:1877
int Ssw_SmlNodesCompareInFrame ( Ssw_Sml_t *  p,
Aig_Obj_t *  pObj0,
Aig_Obj_t *  pObj1,
int  iFrame0,
int  iFrame1 
)

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

Synopsis [Simulates one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 772 of file sswSim.c.

773 {
774  unsigned * pSims0, * pSims1;
775  int i;
776  assert( iFrame0 < p->nFrames );
777  assert( iFrame1 < p->nFrames );
778  assert( !Aig_IsComplement(pObj0) );
779  assert( !Aig_IsComplement(pObj1) );
780  assert( iFrame0 == 0 || p->nWordsFrame < p->nWordsTotal );
781  assert( iFrame1 == 0 || p->nWordsFrame < p->nWordsTotal );
782  // get hold of the simulation information
783  pSims0 = Ssw_ObjSim(p, pObj0->Id) + p->nWordsFrame * iFrame0;
784  pSims1 = Ssw_ObjSim(p, pObj1->Id) + p->nWordsFrame * iFrame1;
785  // compare
786  for ( i = 0; i < p->nWordsFrame; i++ )
787  if ( pSims0[i] != pSims1[i] )
788  return 0;
789  return 1;
790 }
Ssw_Sml_t_::nWordsFrame
int nWordsFrame
Definition: sswSim.c:36
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Ssw_Sml_t_::nWordsTotal
int nWordsTotal
Definition: sswSim.c:37
assert
#define assert(ex)
Definition: util_old.h:213
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
void Ssw_SmlNodeSimulate ( Ssw_Sml_t *  p,
Aig_Obj_t *  pObj,
int  iFrame 
)

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

Synopsis [Simulates one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 706 of file sswSim.c.

707 {
708  unsigned * pSims, * pSims0, * pSims1;
709  int fCompl, fCompl0, fCompl1, i;
710  assert( iFrame < p->nFrames );
711  assert( !Aig_IsComplement(pObj) );
712  assert( Aig_ObjIsNode(pObj) );
713  assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
714  // get hold of the simulation information
715  pSims = Ssw_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame;
716  pSims0 = Ssw_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + p->nWordsFrame * iFrame;
717  pSims1 = Ssw_ObjSim(p, Aig_ObjFanin1(pObj)->Id) + p->nWordsFrame * iFrame;
718  // get complemented attributes of the children using their random info
719  fCompl = pObj->fPhase;
720  fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
721  fCompl1 = Aig_ObjPhaseReal(Aig_ObjChild1(pObj));
722  // simulate
723  if ( fCompl0 && fCompl1 )
724  {
725  if ( fCompl )
726  for ( i = 0; i < p->nWordsFrame; i++ )
727  pSims[i] = (pSims0[i] | pSims1[i]);
728  else
729  for ( i = 0; i < p->nWordsFrame; i++ )
730  pSims[i] = ~(pSims0[i] | pSims1[i]);
731  }
732  else if ( fCompl0 && !fCompl1 )
733  {
734  if ( fCompl )
735  for ( i = 0; i < p->nWordsFrame; i++ )
736  pSims[i] = (pSims0[i] | ~pSims1[i]);
737  else
738  for ( i = 0; i < p->nWordsFrame; i++ )
739  pSims[i] = (~pSims0[i] & pSims1[i]);
740  }
741  else if ( !fCompl0 && fCompl1 )
742  {
743  if ( fCompl )
744  for ( i = 0; i < p->nWordsFrame; i++ )
745  pSims[i] = (~pSims0[i] | pSims1[i]);
746  else
747  for ( i = 0; i < p->nWordsFrame; i++ )
748  pSims[i] = (pSims0[i] & ~pSims1[i]);
749  }
750  else // if ( !fCompl0 && !fCompl1 )
751  {
752  if ( fCompl )
753  for ( i = 0; i < p->nWordsFrame; i++ )
754  pSims[i] = ~(pSims0[i] & pSims1[i]);
755  else
756  for ( i = 0; i < p->nWordsFrame; i++ )
757  pSims[i] = (pSims0[i] & pSims1[i]);
758  }
759 }
Aig_ObjChild0
static Aig_Obj_t * Aig_ObjChild0(Aig_Obj_t *pObj)
Definition: aig.h:310
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Ssw_Sml_t_::nWordsFrame
int nWordsFrame
Definition: sswSim.c:36
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Ssw_Sml_t_::nWordsTotal
int nWordsTotal
Definition: sswSim.c:37
Aig_ObjChild1
static Aig_Obj_t * Aig_ObjChild1(Aig_Obj_t *pObj)
Definition: aig.h:311
Aig_ObjPhaseReal
static int Aig_ObjPhaseReal(Aig_Obj_t *pObj)
Definition: aig.h:299
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
assert
#define assert(ex)
Definition: util_old.h:213
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
void Ssw_SmlNodeTransferFirst ( Ssw_Sml_t *  p,
Aig_Obj_t *  pOut,
Aig_Obj_t *  pIn 
)

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

Synopsis [Simulates one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 866 of file sswSim.c.

867 {
868  unsigned * pSims0, * pSims1;
869  int i;
870  assert( !Aig_IsComplement(pOut) );
871  assert( !Aig_IsComplement(pIn) );
872  assert( Aig_ObjIsCo(pOut) );
873  assert( Aig_ObjIsCi(pIn) );
874  assert( p->nWordsFrame < p->nWordsTotal );
875  // get hold of the simulation information
876  pSims0 = Ssw_ObjSim(p, pOut->Id) + p->nWordsFrame * (p->nFrames-1);
877  pSims1 = Ssw_ObjSim(p, pIn->Id);
878  // copy information as it is
879  for ( i = 0; i < p->nWordsFrame; i++ )
880  pSims1[i] = pSims0[i];
881 }
Ssw_Sml_t_::nWordsFrame
int nWordsFrame
Definition: sswSim.c:36
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Ssw_Sml_t_::nWordsTotal
int nWordsTotal
Definition: sswSim.c:37
assert
#define assert(ex)
Definition: util_old.h:213
Ssw_Sml_t_::nFrames
int nFrames
Definition: sswSim.c:35
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
void Ssw_SmlNodeTransferNext ( Ssw_Sml_t *  p,
Aig_Obj_t *  pOut,
Aig_Obj_t *  pIn,
int  iFrame 
)

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

Synopsis [Simulates one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 837 of file sswSim.c.

838 {
839  unsigned * pSims0, * pSims1;
840  int i;
841  assert( iFrame < p->nFrames );
842  assert( !Aig_IsComplement(pOut) );
843  assert( !Aig_IsComplement(pIn) );
844  assert( Aig_ObjIsCo(pOut) );
845  assert( Aig_ObjIsCi(pIn) );
846  assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
847  // get hold of the simulation information
848  pSims0 = Ssw_ObjSim(p, pOut->Id) + p->nWordsFrame * iFrame;
849  pSims1 = Ssw_ObjSim(p, pIn->Id) + p->nWordsFrame * (iFrame+1);
850  // copy information as it is
851  for ( i = 0; i < p->nWordsFrame; i++ )
852  pSims1[i] = pSims0[i];
853 }
Ssw_Sml_t_::nWordsFrame
int nWordsFrame
Definition: sswSim.c:36
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Ssw_Sml_t_::nWordsTotal
int nWordsTotal
Definition: sswSim.c:37
assert
#define assert(ex)
Definition: util_old.h:213
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Aig_ObjIsCo
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
int Ssw_SmlNumFrames ( Ssw_Sml_t *  p)

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

Synopsis [Returns the number of frames simulated in the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 1288 of file sswSim.c.

1289 {
1290  return p->nFrames;
1291 }
Ssw_Sml_t_::nFrames
int nFrames
Definition: sswSim.c:35
int Ssw_SmlNumWordsTotal ( Ssw_Sml_t *  p)

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

Synopsis [Returns the total number of simulation words.]

Description []

SideEffects []

SeeAlso []

Definition at line 1304 of file sswSim.c.

1305 {
1306  return p->nWordsTotal;
1307 }
Ssw_Sml_t_::nWordsTotal
int nWordsTotal
Definition: sswSim.c:37
void Ssw_SmlObjAssignConst ( Ssw_Sml_t *  p,
Aig_Obj_t *  pObj,
int  fConst1,
int  iFrame 
)

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

Synopsis [Assigns constant patterns to the PI node.]

Description []

SideEffects []

SeeAlso []

Definition at line 560 of file sswSim.c.

561 {
562  unsigned * pSims;
563  int i;
564  assert( iFrame < p->nFrames );
565  assert( Aig_ObjIsCi(pObj) );
566  pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
567  for ( i = 0; i < p->nWordsFrame; i++ )
568  pSims[i] = fConst1? ~(unsigned)0 : 0;
569 }
Ssw_Sml_t_::nWordsFrame
int nWordsFrame
Definition: sswSim.c:36
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
assert
#define assert(ex)
Definition: util_old.h:213
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
void Ssw_SmlObjAssignConstWord ( Ssw_Sml_t *  p,
Aig_Obj_t *  pObj,
int  fConst1,
int  iFrame,
int  iWord 
)

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

Synopsis [Assigns constant patterns to the PI node.]

Description []

SideEffects []

SeeAlso []

Definition at line 582 of file sswSim.c.

583 {
584  unsigned * pSims;
585  assert( iFrame < p->nFrames );
586  assert( iWord < p->nWordsFrame );
587  assert( Aig_ObjIsCi(pObj) );
588  pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
589  pSims[iWord] = fConst1? ~(unsigned)0 : 0;
590 }
Ssw_Sml_t_::nWordsFrame
int nWordsFrame
Definition: sswSim.c:36
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
assert
#define assert(ex)
Definition: util_old.h:213
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
unsigned Ssw_SmlObjHashWord ( Ssw_Sml_t *  p,
Aig_Obj_t *  pObj 
)

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes hash value of the node using its simulation info.]

Description []

SideEffects []

SeeAlso []

Definition at line 63 of file sswSim.c.

64 {
65  static int s_SPrimes[128] = {
66  1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
67  1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
68  2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
69  2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
70  3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
71  3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
72  4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
73  4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
74  5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
75  6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
76  6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
77  7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
78  8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
79  };
80  unsigned * pSims;
81  unsigned uHash;
82  int i;
83 // assert( p->nWordsTotal <= 128 );
84  uHash = 0;
85  pSims = Ssw_ObjSim(p, pObj->Id);
86  for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
87  uHash ^= pSims[i] * s_SPrimes[i & 0x7F];
88  return uHash;
89 }
Ssw_Sml_t_::nWordsPref
int nWordsPref
Definition: sswSim.c:38
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
int Ssw_SmlObjIsConstBit ( void *  p,
Aig_Obj_t *  pObj 
)

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

Synopsis [Returns 1 if the node appears to be constant 1 candidate.]

Description []

SideEffects []

SeeAlso []

Definition at line 147 of file sswSim.c.

148 {
149  return pObj->fPhase == pObj->fMarkB;
150 }
Aig_Obj_t_::fMarkB
unsigned int fMarkB
Definition: aig.h:80
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
int Ssw_SmlObjIsConstWord ( Ssw_Sml_t *  p,
Aig_Obj_t *  pObj 
)

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

Synopsis [Returns 1 if simulation info is composed of all zeros.]

Description []

SideEffects []

SeeAlso []

Definition at line 102 of file sswSim.c.

103 {
104  unsigned * pSims;
105  int i;
106  pSims = Ssw_ObjSim(p, pObj->Id);
107  for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
108  if ( pSims[i] )
109  return 0;
110  return 1;
111 }
Ssw_Sml_t_::nWordsPref
int nWordsPref
Definition: sswSim.c:38
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
int Ssw_SmlObjsAreEqualBit ( void *  p,
Aig_Obj_t *  pObj0,
Aig_Obj_t *  pObj1 
)

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

Synopsis [Returns 1 if the nodes appear equal.]

Description []

SideEffects []

SeeAlso []

Definition at line 163 of file sswSim.c.

164 {
165  return (pObj0->fPhase == pObj1->fPhase) == (pObj0->fMarkB == pObj1->fMarkB);
166 }
Aig_Obj_t_::fMarkB
unsigned int fMarkB
Definition: aig.h:80
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
int Ssw_SmlObjsAreEqualWord ( Ssw_Sml_t *  p,
Aig_Obj_t *  pObj0,
Aig_Obj_t *  pObj1 
)

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

Synopsis [Returns 1 if simulation infos are equal.]

Description []

SideEffects []

SeeAlso []

Definition at line 124 of file sswSim.c.

125 {
126  unsigned * pSims0, * pSims1;
127  int i;
128  pSims0 = Ssw_ObjSim(p, pObj0->Id);
129  pSims1 = Ssw_ObjSim(p, pObj1->Id);
130  for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
131  if ( pSims0[i] != pSims1[i] )
132  return 0;
133  return 1;
134 }
Ssw_Sml_t_::nWordsPref
int nWordsPref
Definition: sswSim.c:38
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
void Ssw_SmlObjSetWord ( Ssw_Sml_t *  p,
Aig_Obj_t *  pObj,
unsigned  Word,
int  iWord,
int  iFrame 
)

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

Synopsis [Assigns constant patterns to the PI node.]

Description []

SideEffects []

SeeAlso []

Definition at line 603 of file sswSim.c.

604 {
605  unsigned * pSims;
606  assert( iFrame < p->nFrames );
607  assert( Aig_ObjIsCi(pObj) );
608  pSims = Ssw_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
609  pSims[iWord] = Word;
610 }
Ssw_Sml_t_::nWordsFrame
int nWordsFrame
Definition: sswSim.c:36
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
assert
#define assert(ex)
Definition: util_old.h:213
Aig_ObjIsCi
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
void Ssw_SmlReinitialize ( Ssw_Sml_t *  p)

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

Synopsis [Assings random simulation info for the PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 955 of file sswSim.c.

956 {
957  Aig_Obj_t * pObj, * pObjLi, * pObjLo;
958  int i;
959  assert( Aig_ManRegNum(p->pAig) > 0 );
960  assert( Aig_ManRegNum(p->pAig) < Aig_ManCiNum(p->pAig) );
961  // assign random info for primary inputs
962  Saig_ManForEachPi( p->pAig, pObj, i )
963  Ssw_SmlAssignRandom( p, pObj );
964  // copy simulation info into the inputs
965  Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
966  Ssw_SmlNodeTransferFirst( p, pObjLi, pObjLo );
967 }
Ssw_SmlNodeTransferFirst
void Ssw_SmlNodeTransferFirst(Ssw_Sml_t *p, Aig_Obj_t *pOut, Aig_Obj_t *pIn)
Definition: sswSim.c:866
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
Ssw_SmlAssignRandom
void Ssw_SmlAssignRandom(Ssw_Sml_t *p, Aig_Obj_t *pObj)
Definition: sswSim.c:513
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Aig_Obj_t_
Definition: aig.h:69
Ssw_Sml_t_::pAig
Aig_Man_t * pAig
Definition: sswSim.c:33
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
assert
#define assert(ex)
Definition: util_old.h:213
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
void Ssw_SmlResimulateSeq ( Ssw_Sml_t *  p)

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

Synopsis [Performs next round of sequential simulation.]

Description []

SideEffects []

SeeAlso []

Definition at line 1269 of file sswSim.c.

1270 {
1271  Ssw_SmlReinitialize( p );
1272  Ssw_SmlSimulateOne( p );
1273  p->fNonConstOut = Ssw_SmlCheckNonConstOutputs( p );
1274 }
Ssw_SmlReinitialize
void Ssw_SmlReinitialize(Ssw_Sml_t *p)
Definition: sswSim.c:955
Ssw_SmlSimulateOne
void Ssw_SmlSimulateOne(Ssw_Sml_t *p)
Definition: sswSim.c:1005
Ssw_Sml_t_::fNonConstOut
int fNonConstOut
Definition: sswSim.c:39
Ssw_SmlCheckNonConstOutputs
int Ssw_SmlCheckNonConstOutputs(Ssw_Sml_t *p)
Definition: sswSim.c:980
void Ssw_SmlSavePattern0 ( Ssw_Man_t *  p,
int  fInit 
)

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

Synopsis [Generated const 0 pattern.]

Description []

SideEffects []

SeeAlso []

Definition at line 398 of file sswSim.c.

399 {
400  memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
401 }
memset
char * memset()
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Ssw_SmlSavePattern1 ( Ssw_Man_t *  p,
int  fInit 
)

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

Synopsis [[Generated const 1 pattern.]

Description []

SideEffects []

SeeAlso []

Definition at line 414 of file sswSim.c.

415 {
416  Aig_Obj_t * pObj;
417  int i, k, nTruePis;
418  memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords );
419  if ( !fInit )
420  return;
421  // clear the state bits to correspond to all-0 initial state
422  nTruePis = Saig_ManPiNum(p->pAig);
423  k = 0;
424  Saig_ManForEachLo( p->pAig, pObj, i )
425  Abc_InfoXorBit( p->pPatWords, nTruePis * p->nFrames + k++ );
426 }
memset
char * memset()
Llb_Mgr_t_::pAig
Aig_Man_t * pAig
Definition: llb3Image.c:49
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_InfoXorBit
static void Abc_InfoXorBit(unsigned *p, int i)
Definition: abc_global.h:260
Aig_Obj_t_
Definition: aig.h:69
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
Vec_Ptr_t* Ssw_SmlSimDataPointers ( Ssw_Sml_t *  p)

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

Synopsis [Get simulation data.]

Description []

SideEffects []

SeeAlso []

Definition at line 1189 of file sswSim.c.

1190 {
1191  Vec_Ptr_t * vSimInfo;
1192  Aig_Obj_t * pObj;
1193  int i;
1194  vSimInfo = Vec_PtrStart( Aig_ManObjNumMax(p->pAig) );
1195  Aig_ManForEachObj( p->pAig, pObj, i )
1196  Vec_PtrWriteEntry( vSimInfo, i, Ssw_ObjSim(p, i) );
1197  return vSimInfo;
1198 }
Vec_PtrStart
static Vec_Ptr_t * Vec_PtrStart(int nSize)
Definition: vecPtr.h:106
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Aig_Obj_t_
Definition: aig.h:69
Ssw_Sml_t_::pAig
Aig_Man_t * pAig
Definition: sswSim.c:33
Vec_PtrWriteEntry
static void Vec_PtrWriteEntry(Vec_Ptr_t *p, int i, void *Entry)
Definition: vecPtr.h:396
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Aig_ManForEachObj
#define Aig_ManForEachObj(p, pObj, i)
Definition: aig.h:403
unsigned* Ssw_SmlSimInfo ( Ssw_Sml_t *  p,
Aig_Obj_t *  pObj 
)

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

Synopsis [Returns the pointer to the simulation info of the node.]

Description [The simulation info is normalized unless procedure Ssw_SmlUnnormalize() is called in advance.]

SideEffects []

SeeAlso []

Definition at line 1321 of file sswSim.c.

1322 {
1323  assert( !Aig_IsComplement(pObj) );
1324  return Ssw_ObjSim( p, pObj->Id );
1325 }
Aig_IsComplement
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
assert
#define assert(ex)
Definition: util_old.h:213
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Ssw_Sml_t* Ssw_SmlSimulateComb ( Aig_Man_t *  pAig,
int  nWords 
)

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

Synopsis [Performs simulation of the uninitialized circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 1228 of file sswSim.c.

1229 {
1230  Ssw_Sml_t * p;
1231  p = Ssw_SmlStart( pAig, 0, 1, nWords );
1232  Ssw_SmlInitialize( p, 0 );
1233  Ssw_SmlSimulateOne( p );
1234  return p;
1235 }
Ssw_SmlSimulateOne
void Ssw_SmlSimulateOne(Ssw_Sml_t *p)
Definition: sswSim.c:1005
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
nWords
int nWords
Definition: abcNpn.c:127
Ssw_SmlStart
Ssw_Sml_t * Ssw_SmlStart(Aig_Man_t *pAig, int nPref, int nFrames, int nWordsFrame)
Definition: sswSim.c:1148
Ssw_SmlInitialize
void Ssw_SmlInitialize(Ssw_Sml_t *p, int fInit)
Definition: sswSim.c:895
Ssw_Sml_t_
DECLARATIONS ///.
Definition: sswSim.c:31
void Ssw_SmlSimulateOne ( Ssw_Sml_t *  p)

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

Synopsis [Simulates AIG manager.]

Description [Assumes that the PI simulation info is attached.]

SideEffects []

SeeAlso []

Definition at line 1005 of file sswSim.c.

1006 {
1007  Aig_Obj_t * pObj, * pObjLi, * pObjLo;
1008  int f, i;
1009  abctime clk;
1010 clk = Abc_Clock();
1011  for ( f = 0; f < p->nFrames; f++ )
1012  {
1013  // simulate the nodes
1014  Aig_ManForEachNode( p->pAig, pObj, i )
1015  Ssw_SmlNodeSimulate( p, pObj, f );
1016  // copy simulation info into outputs
1017  Saig_ManForEachPo( p->pAig, pObj, i )
1018  Ssw_SmlNodeCopyFanin( p, pObj, f );
1019  // copy simulation info into outputs
1020  Saig_ManForEachLi( p->pAig, pObj, i )
1021  Ssw_SmlNodeCopyFanin( p, pObj, f );
1022  // quit if this is the last timeframe
1023  if ( f == p->nFrames - 1 )
1024  break;
1025  // copy simulation info into the inputs
1026  Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
1027  Ssw_SmlNodeTransferNext( p, pObjLi, pObjLo, f );
1028  }
1029 p->timeSim += Abc_Clock() - clk;
1030 p->nSimRounds++;
1031 }
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
Ssw_SmlNodeTransferNext
void Ssw_SmlNodeTransferNext(Ssw_Sml_t *p, Aig_Obj_t *pOut, Aig_Obj_t *pIn, int iFrame)
Definition: sswSim.c:837
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
if
if(last==0)
Definition: sparse_int.h:34
Aig_Obj_t_
Definition: aig.h:69
Ssw_Sml_t_::pAig
Aig_Man_t * pAig
Definition: sswSim.c:33
Ssw_SmlNodeSimulate
void Ssw_SmlNodeSimulate(Ssw_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: sswSim.c:706
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
Ssw_Sml_t_::nFrames
int nFrames
Definition: sswSim.c:35
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Ssw_SmlNodeCopyFanin
void Ssw_SmlNodeCopyFanin(Ssw_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: sswSim.c:803
void Ssw_SmlSimulateOneDyn_rec ( Ssw_Sml_t *  p,
Aig_Obj_t *  pObj,
int  f,
int *  pVisited,
int  nVisCounter 
)

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

Synopsis [Simulates AIG manager.]

Description [Assumes that the PI simulation info is attached.]

SideEffects []

SeeAlso []

Definition at line 1076 of file sswSim.c.

1077 {
1078 // if ( Aig_ObjIsTravIdCurrent(p->pAig, pObj) )
1079 // return;
1080 // Aig_ObjSetTravIdCurrent(p->pAig, pObj);
1081  if ( pVisited[p->nFrames*pObj->Id+f] == nVisCounter )
1082  return;
1083  pVisited[p->nFrames*pObj->Id+f] = nVisCounter;
1084  if ( Saig_ObjIsPi( p->pAig, pObj ) || Aig_ObjIsConst1(pObj) )
1085  return;
1086  if ( Saig_ObjIsLo( p->pAig, pObj ) )
1087  {
1088  if ( f == 0 )
1089  return;
1090  Ssw_SmlSimulateOneDyn_rec( p, Saig_ObjLoToLi(p->pAig, pObj), f-1, pVisited, nVisCounter );
1091  Ssw_SmlNodeTransferNext( p, Saig_ObjLoToLi(p->pAig, pObj), pObj, f-1 );
1092  return;
1093  }
1094  if ( Saig_ObjIsLi( p->pAig, pObj ) )
1095  {
1096  Ssw_SmlSimulateOneDyn_rec( p, Aig_ObjFanin0(pObj), f, pVisited, nVisCounter );
1097  Ssw_SmlNodeCopyFanin( p, pObj, f );
1098  return;
1099  }
1100  assert( Aig_ObjIsNode(pObj) );
1101  Ssw_SmlSimulateOneDyn_rec( p, Aig_ObjFanin0(pObj), f, pVisited, nVisCounter );
1102  Ssw_SmlSimulateOneDyn_rec( p, Aig_ObjFanin1(pObj), f, pVisited, nVisCounter );
1103  Ssw_SmlNodeSimulate( p, pObj, f );
1104 }
Saig_ObjIsLo
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
Ssw_SmlSimulateOneDyn_rec
void Ssw_SmlSimulateOneDyn_rec(Ssw_Sml_t *p, Aig_Obj_t *pObj, int f, int *pVisited, int nVisCounter)
Definition: sswSim.c:1076
Saig_ObjLoToLi
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
Aig_ObjFanin0
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Ssw_SmlNodeTransferNext
void Ssw_SmlNodeTransferNext(Ssw_Sml_t *p, Aig_Obj_t *pOut, Aig_Obj_t *pIn, int iFrame)
Definition: sswSim.c:837
Aig_ObjFanin1
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Saig_ObjIsLi
static int Saig_ObjIsLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:85
Aig_ObjIsNode
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
Aig_ObjIsConst1
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
Ssw_Sml_t_::pAig
Aig_Man_t * pAig
Definition: sswSim.c:33
Ssw_SmlNodeSimulate
void Ssw_SmlNodeSimulate(Ssw_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: sswSim.c:706
assert
#define assert(ex)
Definition: util_old.h:213
Ssw_Sml_t_::nFrames
int nFrames
Definition: sswSim.c:35
Ssw_SmlNodeCopyFanin
void Ssw_SmlNodeCopyFanin(Ssw_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: sswSim.c:803
Aig_Obj_t_::Id
int Id
Definition: aig.h:85
Saig_ObjIsPi
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
void Ssw_SmlSimulateOneFrame ( Ssw_Sml_t *  p)

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

Synopsis [Simulates AIG manager.]

Description [Assumes that the PI simulation info is attached.]

SideEffects []

SeeAlso []

Definition at line 1117 of file sswSim.c.

1118 {
1119  Aig_Obj_t * pObj, * pObjLi, * pObjLo;
1120  int i;
1121  abctime clk;
1122 clk = Abc_Clock();
1123  // simulate the nodes
1124  Aig_ManForEachNode( p->pAig, pObj, i )
1125  Ssw_SmlNodeSimulate( p, pObj, 0 );
1126  // copy simulation info into outputs
1127  Saig_ManForEachLi( p->pAig, pObj, i )
1128  Ssw_SmlNodeCopyFanin( p, pObj, 0 );
1129  // copy simulation info into the inputs
1130  Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
1131  Ssw_SmlNodeTransferNext( p, pObjLi, pObjLo, 0 );
1132 p->timeSim += Abc_Clock() - clk;
1133 p->nSimRounds++;
1134 }
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
Ssw_SmlNodeTransferNext
void Ssw_SmlNodeTransferNext(Ssw_Sml_t *p, Aig_Obj_t *pOut, Aig_Obj_t *pIn, int iFrame)
Definition: sswSim.c:837
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
Aig_Obj_t_
Definition: aig.h:69
Ssw_Sml_t_::pAig
Aig_Man_t * pAig
Definition: sswSim.c:33
Ssw_SmlNodeSimulate
void Ssw_SmlNodeSimulate(Ssw_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: sswSim.c:706
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Ssw_SmlNodeCopyFanin
void Ssw_SmlNodeCopyFanin(Ssw_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: sswSim.c:803
Ssw_Sml_t* Ssw_SmlSimulateSeq ( Aig_Man_t *  pAig,
int  nPref,
int  nFrames,
int  nWords 
)

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

Synopsis [Performs simulation of the initialized circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 1248 of file sswSim.c.

1249 {
1250  Ssw_Sml_t * p;
1251  p = Ssw_SmlStart( pAig, nPref, nFrames, nWords );
1252  Ssw_SmlInitialize( p, 1 );
1253  Ssw_SmlSimulateOne( p );
1254  p->fNonConstOut = Ssw_SmlCheckNonConstOutputs( p );
1255  return p;
1256 }
Ssw_SmlSimulateOne
void Ssw_SmlSimulateOne(Ssw_Sml_t *p)
Definition: sswSim.c:1005
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
nWords
int nWords
Definition: abcNpn.c:127
Ssw_Sml_t_::fNonConstOut
int fNonConstOut
Definition: sswSim.c:39
Ssw_SmlStart
Ssw_Sml_t * Ssw_SmlStart(Aig_Man_t *pAig, int nPref, int nFrames, int nWordsFrame)
Definition: sswSim.c:1148
Ssw_SmlCheckNonConstOutputs
int Ssw_SmlCheckNonConstOutputs(Ssw_Sml_t *p)
Definition: sswSim.c:980
Ssw_SmlInitialize
void Ssw_SmlInitialize(Ssw_Sml_t *p, int fInit)
Definition: sswSim.c:895
Ssw_Sml_t_
DECLARATIONS ///.
Definition: sswSim.c:31
Ssw_Sml_t* Ssw_SmlStart ( Aig_Man_t *  pAig,
int  nPref,
int  nFrames,
int  nWordsFrame 
)

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

Synopsis [Allocates simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 1148 of file sswSim.c.

1149 {
1150  Ssw_Sml_t * p;
1151  p = (Ssw_Sml_t *)ABC_ALLOC( char, sizeof(Ssw_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
1152  memset( p, 0, sizeof(Ssw_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
1153  p->pAig = pAig;
1154  p->nPref = nPref;
1155  p->nFrames = nPref + nFrames;
1156  p->nWordsFrame = nWordsFrame;
1157  p->nWordsTotal = (nPref + nFrames) * nWordsFrame;
1158  p->nWordsPref = nPref * nWordsFrame;
1159  return p;
1160 }
memset
char * memset()
Ssw_Sml_t_::nWordsPref
int nWordsPref
Definition: sswSim.c:38
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Ssw_Sml_t_::nWordsFrame
int nWordsFrame
Definition: sswSim.c:36
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Ssw_Sml_t_::nWordsTotal
int nWordsTotal
Definition: sswSim.c:37
Ssw_Sml_t_::nPref
int nPref
Definition: sswSim.c:34
Ssw_Sml_t_::pAig
Aig_Man_t * pAig
Definition: sswSim.c:33
Aig_ManObjNumMax
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
Ssw_Sml_t_::nFrames
int nFrames
Definition: sswSim.c:35
Ssw_Sml_t_
DECLARATIONS ///.
Definition: sswSim.c:31
void Ssw_SmlStop ( Ssw_Sml_t *  p)

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

Synopsis [Deallocates simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 1211 of file sswSim.c.

1212 {
1213  ABC_FREE( p );
1214 }
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
void Ssw_SmlUnnormalize ( Ssw_Sml_t *  p)

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

Synopsis [Converts simulation information to be not normallized.]

Description []

SideEffects []

SeeAlso []

Definition at line 1044 of file sswSim.c.

1045 {
1046  Aig_Obj_t * pObj;
1047  unsigned * pSims;
1048  int i, k;
1049  // convert constant 1
1050  pSims = Ssw_ObjSim( p, 0 );
1051  for ( i = 0; i < p->nWordsFrame; i++ )
1052  pSims[i] = ~pSims[i];
1053  // convert internal nodes
1054  Aig_ManForEachNode( p->pAig, pObj, k )
1055  {
1056  if ( pObj->fPhase == 0 )
1057  continue;
1058  pSims = Ssw_ObjSim( p, pObj->Id );
1059  for ( i = 0; i < p->nWordsFrame; i++ )
1060  pSims[i] = ~pSims[i];
1061  }
1062  // PIs/POs are always stored in their natural state
1063 }
Ssw_Sml_t_::nWordsFrame
int nWordsFrame
Definition: sswSim.c:36
Ssw_ObjSim
static unsigned * Ssw_ObjSim(Ssw_Sml_t *p, int Id)
Definition: sswSim.c:45
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
Aig_Obj_t_
Definition: aig.h:69
Ssw_Sml_t_::pAig
Aig_Man_t * pAig
Definition: sswSim.c:33
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition: aig.h:78
Aig_Obj_t_::Id
int Id
Definition: aig.h:85