abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions
fsimSim.c File Reference
#include "fsimInt.h"
#include "aig/ssw/ssw.h"

Go to the source code of this file.

Functions

static
ABC_NAMESPACE_IMPL_START void 		Fsim_ManSimInfoRandom (Fsim_Man_t *p, unsigned *pInfo)
 DECLARATIONS ///. More...
 
static void Fsim_ManSimInfoZero (Fsim_Man_t *p, unsigned *pInfo)
 
static int Fsim_ManSimInfoIsZero (Fsim_Man_t *p, unsigned *pInfo)
 
static void Fsim_ManSimInfoOne (Fsim_Man_t *p, unsigned *pInfo)
 
static void Fsim_ManSimInfoCopy (Fsim_Man_t *p, unsigned *pInfo, unsigned *pInfo0)
 
static void Fsim_ManSimulateCi (Fsim_Man_t *p, int iNode, int iCi)
 
static void Fsim_ManSimulateCo (Fsim_Man_t *p, int iCo, int iFan0)
 
static void Fsim_ManSimulateNode (Fsim_Man_t *p, int iNode, int iFan0, int iFan1)
 
static void Fsim_ManSimInfoInit (Fsim_Man_t *p)
 
static void Fsim_ManSimInfoTransfer (Fsim_Man_t *p)
 
static int Fsim_ManRestoreNum (Fsim_Man_t *p)
 
static int Fsim_ManRestoreObj (Fsim_Man_t *p, Fsim_Obj_t *pObj)
 
static void Fsim_ManSimulateRound2 (Fsim_Man_t *p)
 
static void Fsim_ManSimulateRound (Fsim_Man_t *p)
 
void Fsim_ManSimulateRoundTest (Fsim_Man_t *p)
 
static int Fsim_ManCheckPos (Fsim_Man_t *p, int *piPo, int *piPat)
 
Abc_Cex_t * Fsim_ManGenerateCounter (Aig_Man_t *pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t *vCis2Ids)
 
int Fsim_ManSimulate (Aig_Man_t *pAig, Fsim_ParSim_t *pPars)
 

Function Documentation

static int Fsim_ManCheckPos ( Fsim_Man_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 406 of file fsimSim.c.

407 {
408  int i, iPat;
409  for ( i = 0; i < p->nPos; i++ )
410  {
411  iPat = Fsim_ManSimInfoIsZero( p, Fsim_SimDataCo(p, i) );
412  if ( iPat >= 0 )
413  {
414  *piPo = i;
415  *piPat = iPat;
416  return 1;
417  }
418  }
419  return 0;
420 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Fsim_SimDataCo
static unsigned * Fsim_SimDataCo(Fsim_Man_t *p, int i)
Definition: fsimInt.h:99
Fsim_ManSimInfoIsZero
static int Fsim_ManSimInfoIsZero(Fsim_Man_t *p, unsigned *pInfo)
Definition: fsimSim.c:82
Abc_Cex_t* Fsim_ManGenerateCounter ( Aig_Man_t *  pAig,
int  iFrame,
int  iOut,
int  nWords,
int  iPat,
Vec_Int_t *  vCis2Ids 
)

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

Synopsis [Returns the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 433 of file fsimSim.c.

434 {
435  Abc_Cex_t * p;
436  unsigned * pData;
437  int f, i, w, iPioId, Counter;
438  p = Abc_CexAlloc( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), iFrame+1 );
439  p->iFrame = iFrame;
440  p->iPo = iOut;
441  // fill in the binary data
442  Aig_ManRandom( 1 );
443  Counter = p->nRegs;
444  pData = ABC_ALLOC( unsigned, nWords );
445  for ( f = 0; f <= iFrame; f++, Counter += p->nPis )
446  for ( i = 0; i < Aig_ManPiNum(pAig); i++ )
447  {
448  iPioId = Vec_IntEntry( vCis2Ids, i );
449  if ( iPioId >= p->nPis )
450  continue;
451  for ( w = nWords-1; w >= 0; w-- )
452  pData[w] = Aig_ManRandom( 0 );
453  if ( Aig_InfoHasBit( pData, iPat ) )
454  Aig_InfoSetBit( p->pData, Counter + iPioId );
455  }
456  ABC_FREE( pData );
457  return p;
458 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
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
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition: aigUtil.c:1157
nWords
int nWords
Definition: abcNpn.c:127
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Counter
static int Counter
Definition: extraBddMisc.c:1877
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
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
static int Fsim_ManRestoreNum ( Fsim_Man_t *  p)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 259 of file fsimSim.c.

260 {
261  int ch, i, x = 0;
262  for ( i = 0; (ch = *p->pDataCur++) & 0x80; i++ )
263  x |= (ch & 0x7f) << (7 * i);
264  assert( p->pDataCur - p->pDataAig < p->nDataAig );
265  return x | (ch << (7 * i));
266 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
assert
#define assert(ex)
Definition: util_old.h:213
static int Fsim_ManRestoreObj ( Fsim_Man_t *  p,
Fsim_Obj_t *  pObj 
)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 279 of file fsimSim.c.

280 {
281  int iValue = Fsim_ManRestoreNum( p );
282  if ( (iValue & 3) == 3 ) // and
283  {
284  pObj->iNode = (iValue >> 2) + p->iNodePrev;
285  pObj->iFan0 = (pObj->iNode << 1) - Fsim_ManRestoreNum( p );
286  pObj->iFan1 = pObj->iFan0 - Fsim_ManRestoreNum( p );
287  p->iNodePrev = pObj->iNode;
288  }
289  else if ( (iValue & 3) == 1 ) // ci
290  {
291  pObj->iNode = (iValue >> 2) + p->iNodePrev;
292  pObj->iFan0 = 0;
293  pObj->iFan1 = 0;
294  p->iNodePrev = pObj->iNode;
295  }
296  else // if ( (iValue & 1) == 0 ) // co
297  {
298  pObj->iNode = 0;
299  pObj->iFan0 = ((p->iNodePrev << 1) | 1) - (iValue >> 1);
300  pObj->iFan1 = 0;
301  }
302  return 1;
303 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Fsim_ManRestoreNum
static int Fsim_ManRestoreNum(Fsim_Man_t *p)
Definition: fsimSim.c:259
static void Fsim_ManSimInfoCopy ( Fsim_Man_t *  p,
unsigned *  pInfo,
unsigned *  pInfo0 
)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 120 of file fsimSim.c.

121 {
122  int w;
123  for ( w = p->nWords-1; w >= 0; w-- )
124  pInfo[w] = pInfo0[w];
125 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static void Fsim_ManSimInfoInit ( Fsim_Man_t *  p)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 213 of file fsimSim.c.

214 {
215  int iPioNum, i;
216  Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
217  {
218  if ( iPioNum < p->nPis )
219  Fsim_ManSimInfoRandom( p, Fsim_SimDataCi(p, i) );
220  else
221  Fsim_ManSimInfoZero( p, Fsim_SimDataCi(p, i) );
222  }
223 }
Fsim_ManSimInfoZero
static void Fsim_ManSimInfoZero(Fsim_Man_t *p, unsigned *pInfo)
Definition: fsimSim.c:64
Fsim_SimDataCi
static unsigned * Fsim_SimDataCi(Fsim_Man_t *p, int i)
Definition: fsimInt.h:98
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Fsim_ManSimInfoRandom
static ABC_NAMESPACE_IMPL_START void Fsim_ManSimInfoRandom(Fsim_Man_t *p, unsigned *pInfo)
DECLARATIONS ///.
Definition: fsimSim.c:46
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
static int Fsim_ManSimInfoIsZero ( Fsim_Man_t *  p,
unsigned *  pInfo 
)
inlinestatic

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 82 of file fsimSim.c.

83 {
84  int w;
85  for ( w = p->nWords-1; w >= 0; w-- )
86  if ( pInfo[w] )
87  return 32*(w-1) + Aig_WordFindFirstBit( pInfo[w] );
88  return -1;
89 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Aig_WordFindFirstBit
static int Aig_WordFindFirstBit(unsigned uWord)
Definition: aig.h:237
static void Fsim_ManSimInfoOne ( Fsim_Man_t *  p,
unsigned *  pInfo 
)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 102 of file fsimSim.c.

103 {
104  int w;
105  for ( w = p->nWords-1; w >= 0; w-- )
106  pInfo[w] = ~0;
107 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static ABC_NAMESPACE_IMPL_START void Fsim_ManSimInfoRandom ( Fsim_Man_t *  p,
unsigned *  pInfo 
)
inlinestatic

DECLARATIONS ///.

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

FileName [fsimSim.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Fast sequential AIG simulator.]

Synopsis [Simulation procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]FUNCTION DEFINITIONS /// Function*************************************************************

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file fsimSim.c.

47 {
48  int w;
49  for ( w = p->nWords-1; w >= 0; w-- )
50  pInfo[w] = Aig_ManRandom( 0 );
51 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition: aigUtil.c:1157
static void Fsim_ManSimInfoTransfer ( Fsim_Man_t *  p)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 236 of file fsimSim.c.

237 {
238  int iPioNum, i;
239  Vec_IntForEachEntry( p->vCis2Ids, iPioNum, i )
240  {
241  if ( iPioNum < p->nPis )
242  Fsim_ManSimInfoRandom( p, Fsim_SimDataCi(p, i) );
243  else
244  Fsim_ManSimInfoCopy( p, Fsim_SimDataCi(p, i), Fsim_SimDataCo(p, p->nPos+iPioNum-p->nPis) );
245  }
246 }
Fsim_SimDataCi
static unsigned * Fsim_SimDataCi(Fsim_Man_t *p, int i)
Definition: fsimInt.h:98
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Fsim_ManSimInfoRandom
static ABC_NAMESPACE_IMPL_START void Fsim_ManSimInfoRandom(Fsim_Man_t *p, unsigned *pInfo)
DECLARATIONS ///.
Definition: fsimSim.c:46
Fsim_ManSimInfoCopy
static void Fsim_ManSimInfoCopy(Fsim_Man_t *p, unsigned *pInfo, unsigned *pInfo0)
Definition: fsimSim.c:120
Fsim_SimDataCo
static unsigned * Fsim_SimDataCo(Fsim_Man_t *p, int i)
Definition: fsimInt.h:99
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
static void Fsim_ManSimInfoZero ( Fsim_Man_t *  p,
unsigned *  pInfo 
)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 64 of file fsimSim.c.

65 {
66  int w;
67  for ( w = p->nWords-1; w >= 0; w-- )
68  pInfo[w] = 0;
69 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int Fsim_ManSimulate ( Aig_Man_t *  pAig,
Fsim_ParSim_t *  pPars 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 471 of file fsimSim.c.

472 {
473  Fsim_Man_t * p;
474  Sec_MtrStatus_t Status;
475  int i, iOut, iPat;
476  clock_t clk, clkTotal = clock(), clk2, clk2Total = 0;
477  assert( Aig_ManRegNum(pAig) > 0 );
478  if ( pPars->fCheckMiter )
479  {
480  Status = Sec_MiterStatus( pAig );
481  if ( Status.nSat > 0 )
482  {
483  printf( "Miter is trivially satisfiable (output %d).\n", Status.iOut );
484  return 1;
485  }
486  if ( Status.nUndec == 0 )
487  {
488  printf( "Miter is trivially unsatisfiable.\n" );
489  return 0;
490  }
491  }
492  // create manager
493  clk = clock();
494  p = Fsim_ManCreate( pAig );
495  p->nWords = pPars->nWords;
496  if ( pPars->fVerbose )
497  {
498  printf( "Obj = %8d (%8d). Cut = %6d. Front = %6d. FrtMem = %7.2f MB. ",
499  p->nObjs, p->nCis + p->nNodes, p->nCrossCutMax, p->nFront,
500  4.0*p->nWords*(p->nFront)/(1<<20) );
501  ABC_PRT( "Time", clock() - clk );
502  }
503  // create simulation frontier
504  clk = clock();
505  Fsim_ManFront( p, pPars->fCompressAig );
506  if ( pPars->fVerbose )
507  {
508  printf( "Max ID = %8d. Log max ID = %2d. AigMem = %7.2f MB (%5.2f byte/obj). ",
509  p->iNumber, Aig_Base2Log(p->iNumber),
510  1.0*(p->pDataCur-p->pDataAig)/(1<<20),
511  1.0*(p->pDataCur-p->pDataAig)/p->nObjs );
512  ABC_PRT( "Time", clock() - clk );
513  }
514  // perform simulation
515  Aig_ManRandom( 1 );
516  assert( p->pDataSim == NULL );
517  p->pDataSim = ABC_ALLOC( unsigned, p->nWords * p->nFront );
518  p->pDataSimCis = ABC_ALLOC( unsigned, p->nWords * p->nCis );
519  p->pDataSimCos = ABC_ALLOC( unsigned, p->nWords * p->nCos );
520  Fsim_ManSimInfoInit( p );
521  for ( i = 0; i < pPars->nIters; i++ )
522  {
523  Fsim_ManSimulateRound( p );
524  if ( pPars->fVerbose )
525  {
526  printf( "Frame %4d out of %4d and timeout %3d sec. ", i+1, pPars->nIters, pPars->TimeLimit );
527  printf( "Time = %7.2f sec\r", (1.0*clock()-clkTotal)/CLOCKS_PER_SEC );
528  }
529  if ( pPars->fCheckMiter && Fsim_ManCheckPos( p, &iOut, &iPat ) )
530  {
531  assert( pAig->pSeqModel == NULL );
532  pAig->pSeqModel = Fsim_ManGenerateCounter( pAig, i, iOut, p->nWords, iPat, p->vCis2Ids );
533  if ( pPars->fVerbose )
534  printf( "Miter is satisfiable after simulation (output %d).\n", iOut );
535  break;
536  }
537  if ( (clock() - clkTotal)/CLOCKS_PER_SEC >= pPars->TimeLimit )
538  break;
539  clk2 = clock();
540  if ( i < pPars->nIters - 1 )
541  Fsim_ManSimInfoTransfer( p );
542  clk2Total += clock() - clk2;
543  }
544  if ( pAig->pSeqModel == NULL )
545  printf( "No bug detected after %d frames with time limit %d seconds.\n", i+1, pPars->TimeLimit );
546  if ( pPars->fVerbose )
547  {
548  printf( "Maxcut = %8d. AigMem = %7.2f MB. SimMem = %7.2f MB. ",
549  p->nCrossCutMax,
550  p->pDataAig2? 12.0*p->nObjs/(1<<20) : 1.0*(p->pDataCur-p->pDataAig)/(1<<20),
551  4.0*p->nWords*(p->nFront+p->nCis+p->nCos)/(1<<20) );
552  ABC_PRT( "Sim time", clock() - clkTotal );
553 
554 // ABC_PRT( "Additional time", clk2Total );
555 // Fsim_ManSimulateRoundTest( p );
556 // Fsim_ManSimulateRoundTest2( p );
557  }
558  Fsim_ManDelete( p );
559  return pAig->pSeqModel != NULL;
560 
561 }
Fsim_ManSimInfoInit
static void Fsim_ManSimInfoInit(Fsim_Man_t *p)
Definition: fsimSim.c:213
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Fsim_ManSimulateRound
static void Fsim_ManSimulateRound(Fsim_Man_t *p)
Definition: fsimSim.c:346
Fsim_ParSim_t_::nIters
int nIters
Definition: fsim.h:50
Fsim_ManFront
void Fsim_ManFront(Fsim_Man_t *p, int fCompressAig)
FUNCTION DECLARATIONS ///.
Definition: fsimFront.c:245
Fsim_ParSim_t_::fCheckMiter
int fCheckMiter
Definition: fsim.h:52
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Aig_ManRandom
unsigned Aig_ManRandom(int fReset)
Definition: aigUtil.c:1157
Fsim_ManSimInfoTransfer
static void Fsim_ManSimInfoTransfer(Fsim_Man_t *p)
Definition: fsimSim.c:236
Fsim_ParSim_t_::TimeLimit
int TimeLimit
Definition: fsim.h:51
Fsim_ParSim_t_::fCompressAig
int fCompressAig
Definition: fsim.h:55
Fsim_ParSim_t_::fVerbose
int fVerbose
Definition: fsim.h:53
Fsim_Man_t
typedefABC_NAMESPACE_HEADER_START struct Fsim_Man_t_ Fsim_Man_t
INCLUDES ///.
Definition: fsim.h:42
Fsim_ManCheckPos
static int Fsim_ManCheckPos(Fsim_Man_t *p, int *piPo, int *piPat)
Definition: fsimSim.c:406
Fsim_ManDelete
void Fsim_ManDelete(Fsim_Man_t *p)
Definition: fsimMan.c:169
Sec_MiterStatus
Sec_MtrStatus_t Sec_MiterStatus(Aig_Man_t *p)
DECLARATIONS ///.
Definition: saigMiter.c:46
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Fsim_ManGenerateCounter
Abc_Cex_t * Fsim_ManGenerateCounter(Aig_Man_t *pAig, int iFrame, int iOut, int nWords, int iPat, Vec_Int_t *vCis2Ids)
Definition: fsimSim.c:433
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Fsim_ManCreate
Fsim_Man_t * Fsim_ManCreate(Aig_Man_t *pAig)
Definition: fsimMan.c:102
Sec_MtrStatus_t
typedefABC_NAMESPACE_HEADER_START struct Sec_MtrStatus_t_ Sec_MtrStatus_t
INCLUDES ///.
Definition: saig.h:41
assert
#define assert(ex)
Definition: util_old.h:213
Fsim_ParSim_t_::nWords
int nWords
Definition: fsim.h:49
static void Fsim_ManSimulateCi ( Fsim_Man_t *  p,
int  iNode,
int  iCi 
)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 138 of file fsimSim.c.

139 {
140  unsigned * pInfo = Fsim_SimData( p, iNode % p->nFront );
141  unsigned * pInfo0 = Fsim_SimDataCi( p, iCi );
142  int w;
143  for ( w = p->nWords-1; w >= 0; w-- )
144  pInfo[w] = pInfo0[w];
145 }
Fsim_SimDataCi
static unsigned * Fsim_SimDataCi(Fsim_Man_t *p, int i)
Definition: fsimInt.h:98
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Fsim_SimData
static unsigned * Fsim_SimData(Fsim_Man_t *p, int i)
Definition: fsimInt.h:97
static void Fsim_ManSimulateCo ( Fsim_Man_t *  p,
int  iCo,
int  iFan0 
)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 158 of file fsimSim.c.

159 {
160  unsigned * pInfo = Fsim_SimDataCo( p, iCo );
161  unsigned * pInfo0 = Fsim_SimData( p, Fsim_Lit2Var(iFan0) % p->nFront );
162  int w;
163  if ( Fsim_LitIsCompl(iFan0) )
164  for ( w = p->nWords-1; w >= 0; w-- )
165  pInfo[w] = ~pInfo0[w];
166  else //if ( !Fsim_LitIsCompl(iFan0) )
167  for ( w = p->nWords-1; w >= 0; w-- )
168  pInfo[w] = pInfo0[w];
169 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Fsim_SimData
static unsigned * Fsim_SimData(Fsim_Man_t *p, int i)
Definition: fsimInt.h:97
Fsim_LitIsCompl
static int Fsim_LitIsCompl(int Lit)
Definition: fsimInt.h:107
Fsim_Lit2Var
static int Fsim_Lit2Var(int Lit)
Definition: fsimInt.h:106
Fsim_SimDataCo
static unsigned * Fsim_SimDataCo(Fsim_Man_t *p, int i)
Definition: fsimInt.h:99
static void Fsim_ManSimulateNode ( Fsim_Man_t *  p,
int  iNode,
int  iFan0,
int  iFan1 
)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 182 of file fsimSim.c.

183 {
184  unsigned * pInfo = Fsim_SimData( p, iNode % p->nFront );
185  unsigned * pInfo0 = Fsim_SimData( p, Fsim_Lit2Var(iFan0) % p->nFront );
186  unsigned * pInfo1 = Fsim_SimData( p, Fsim_Lit2Var(iFan1) % p->nFront );
187  int w;
188  if ( Fsim_LitIsCompl(iFan0) && Fsim_LitIsCompl(iFan1) )
189  for ( w = p->nWords-1; w >= 0; w-- )
190  pInfo[w] = ~(pInfo0[w] | pInfo1[w]);
191  else if ( Fsim_LitIsCompl(iFan0) && !Fsim_LitIsCompl(iFan1) )
192  for ( w = p->nWords-1; w >= 0; w-- )
193  pInfo[w] = ~pInfo0[w] & pInfo1[w];
194  else if ( !Fsim_LitIsCompl(iFan0) && Fsim_LitIsCompl(iFan1) )
195  for ( w = p->nWords-1; w >= 0; w-- )
196  pInfo[w] = pInfo0[w] & ~pInfo1[w];
197  else //if ( !Fsim_LitIsCompl(iFan0) && !Fsim_LitIsCompl(iFan1) )
198  for ( w = p->nWords-1; w >= 0; w-- )
199  pInfo[w] = pInfo0[w] & pInfo1[w];
200 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Fsim_SimData
static unsigned * Fsim_SimData(Fsim_Man_t *p, int i)
Definition: fsimInt.h:97
Fsim_LitIsCompl
static int Fsim_LitIsCompl(int Lit)
Definition: fsimInt.h:107
Fsim_Lit2Var
static int Fsim_Lit2Var(int Lit)
Definition: fsimInt.h:106
static void Fsim_ManSimulateRound ( Fsim_Man_t *  p)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 346 of file fsimSim.c.

347 {
348  int * pCur, * pEnd;
349  int iCis = 0, iCos = 0;
350  if ( p->pDataAig2 == NULL )
351  {
352  Fsim_ManSimulateRound2( p );
353  return;
354  }
355  if ( Aig_ObjRefs(Aig_ManConst1(p->pAig)) )
356  Fsim_ManSimInfoOne( p, Fsim_SimData(p, 1) );
357  pCur = p->pDataAig2 + 6;
358  pEnd = p->pDataAig2 + 3 * p->nObjs;
359  while ( pCur < pEnd )
360  {
361  if ( pCur[1] == 0 )
362  Fsim_ManSimulateCi( p, pCur[0], iCis++ );
363  else if ( pCur[2] == 0 )
364  Fsim_ManSimulateCo( p, iCos++, pCur[1] );
365  else
366  Fsim_ManSimulateNode( p, pCur[0], pCur[1], pCur[2] );
367  pCur += 3;
368  }
369  assert( iCis == p->nCis );
370  assert( iCos == p->nCos );
371 }
Fsim_ManSimulateCo
static void Fsim_ManSimulateCo(Fsim_Man_t *p, int iCo, int iFan0)
Definition: fsimSim.c:158
Llb_Mgr_t_::pAig
Aig_Man_t * pAig
Definition: llb3Image.c:49
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Fsim_ManSimulateRound2
static void Fsim_ManSimulateRound2(Fsim_Man_t *p)
Definition: fsimSim.c:316
Fsim_SimData
static unsigned * Fsim_SimData(Fsim_Man_t *p, int i)
Definition: fsimInt.h:97
Fsim_ManSimulateNode
static void Fsim_ManSimulateNode(Fsim_Man_t *p, int iNode, int iFan0, int iFan1)
Definition: fsimSim.c:182
Fsim_ManSimInfoOne
static void Fsim_ManSimInfoOne(Fsim_Man_t *p, unsigned *pInfo)
Definition: fsimSim.c:102
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
assert
#define assert(ex)
Definition: util_old.h:213
Aig_ObjRefs
static int Aig_ObjRefs(Aig_Obj_t *pObj)
Definition: aig.h:300
Fsim_ManSimulateCi
static void Fsim_ManSimulateCi(Fsim_Man_t *p, int iNode, int iCi)
Definition: fsimSim.c:138
static void Fsim_ManSimulateRound2 ( Fsim_Man_t *  p)
inlinestatic

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 316 of file fsimSim.c.

317 {
318  Fsim_Obj_t * pObj;
319  int i, iCis = 0, iCos = 0;
320  if ( Aig_ObjRefs(Aig_ManConst1(p->pAig)) )
321  Fsim_ManSimInfoOne( p, Fsim_SimData(p, 1) );
322  Fsim_ManForEachObj( p, pObj, i )
323  {
324  if ( pObj->iFan0 == 0 )
325  Fsim_ManSimulateCi( p, pObj->iNode, iCis++ );
326  else if ( pObj->iFan1 == 0 )
327  Fsim_ManSimulateCo( p, iCos++, pObj->iFan0 );
328  else
329  Fsim_ManSimulateNode( p, pObj->iNode, pObj->iFan0, pObj->iFan1 );
330  }
331  assert( iCis == p->nCis );
332  assert( iCos == p->nCos );
333 }
Fsim_ManSimulateCo
static void Fsim_ManSimulateCo(Fsim_Man_t *p, int iCo, int iFan0)
Definition: fsimSim.c:158
Llb_Mgr_t_::pAig
Aig_Man_t * pAig
Definition: llb3Image.c:49
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Fsim_SimData
static unsigned * Fsim_SimData(Fsim_Man_t *p, int i)
Definition: fsimInt.h:97
Fsim_ManSimulateNode
static void Fsim_ManSimulateNode(Fsim_Man_t *p, int iNode, int iFan0, int iFan1)
Definition: fsimSim.c:182
Fsim_Obj_t
typedefABC_NAMESPACE_HEADER_START struct Fsim_Obj_t_ Fsim_Obj_t
INCLUDES ///.
Definition: fsimInt.h:46
Fsim_ManSimInfoOne
static void Fsim_ManSimInfoOne(Fsim_Man_t *p, unsigned *pInfo)
Definition: fsimSim.c:102
Aig_ManConst1
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
Fsim_ManForEachObj
#define Fsim_ManForEachObj(p, pObj, i)
Definition: fsimInt.h:112
assert
#define assert(ex)
Definition: util_old.h:213
Aig_ObjRefs
static int Aig_ObjRefs(Aig_Obj_t *pObj)
Definition: aig.h:300
Fsim_ManSimulateCi
static void Fsim_ManSimulateCi(Fsim_Man_t *p, int iNode, int iCi)
Definition: fsimSim.c:138
void Fsim_ManSimulateRoundTest ( Fsim_Man_t *  p)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 384 of file fsimSim.c.

385 {
386  Fsim_Obj_t * pObj;
387  int i;
388  clock_t clk = clock();
389  Fsim_ManForEachObj( p, pObj, i )
390  {
391  }
392 // ABC_PRT( "Unpacking time", p->pPars->nIters * (clock() - clk) );
393 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Fsim_Obj_t
typedefABC_NAMESPACE_HEADER_START struct Fsim_Obj_t_ Fsim_Obj_t
INCLUDES ///.
Definition: fsimInt.h:46
Fsim_ManForEachObj
#define Fsim_ManForEachObj(p, pObj, i)
Definition: fsimInt.h:112