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

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START int Fra_SmlNodeHash (Aig_Obj_t *pObj, int nTableSize)
 DECLARATIONS ///. More...
 
int Fra_SmlNodeIsConst (Aig_Obj_t *pObj)
 
int Fra_SmlNodesAreEqual (Aig_Obj_t *pObj0, Aig_Obj_t *pObj1)
 
int Fra_SmlNodeNotEquWeight (Fra_Sml_t *p, int Left, int Right)
 
int Fra_SmlNodeIsZero (Fra_Sml_t *p, Aig_Obj_t *pObj)
 
int Fra_SmlNodeCountOnes (Fra_Sml_t *p, Aig_Obj_t *pObj)
 
void Fra_SmlSavePattern0 (Fra_Man_t *p, int fInit)
 
void Fra_SmlSavePattern1 (Fra_Man_t *p, int fInit)
 
void Fra_SmlSavePattern (Fra_Man_t *p)
 
void Fra_SmlCheckOutputSavePattern (Fra_Man_t *p, Aig_Obj_t *pObjPo)
 
int Fra_SmlCheckOutput (Fra_Man_t *p)
 
void Fra_SmlAssignRandom (Fra_Sml_t *p, Aig_Obj_t *pObj)
 
void Fra_SmlAssignConst (Fra_Sml_t *p, Aig_Obj_t *pObj, int fConst1, int iFrame)
 
void Fra_SmlInitialize (Fra_Sml_t *p, int fInit)
 
void Fra_SmlAssignDist1 (Fra_Sml_t *p, unsigned *pPat)
 
void Fra_SmlNodeSimulate (Fra_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
 
int Fra_SmlNodesCompareInFrame (Fra_Sml_t *p, Aig_Obj_t *pObj0, Aig_Obj_t *pObj1, int iFrame0, int iFrame1)
 
void Fra_SmlNodeCopyFanin (Fra_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
 
void Fra_SmlNodeTransferNext (Fra_Sml_t *p, Aig_Obj_t *pOut, Aig_Obj_t *pIn, int iFrame)
 
int Fra_SmlCheckNonConstOutputs (Fra_Sml_t *p)
 
void Fra_SmlSimulateOne (Fra_Sml_t *p)
 
void Fra_SmlResimulate (Fra_Man_t *p)
 
void Fra_SmlSimulate (Fra_Man_t *p, int fInit)
 
Fra_Sml_tFra_SmlStart (Aig_Man_t *pAig, int nPref, int nFrames, int nWordsFrame)
 
void Fra_SmlStop (Fra_Sml_t *p)
 
Fra_Sml_tFra_SmlSimulateComb (Aig_Man_t *pAig, int nWords, int fCheckMiter)
 
Vec_Str_tFra_SmlSimulateReadFile (char *pFileName)
 
void Fra_SmlInitializeGiven (Fra_Sml_t *p, Vec_Str_t *vSimInfo)
 
void Fra_SmlPrintOutputs (Fra_Sml_t *p, int nPatterns)
 
Fra_Sml_tFra_SmlSimulateCombGiven (Aig_Man_t *pAig, char *pFileName, int fCheckMiter, int fVerbose)
 
Fra_Sml_tFra_SmlSimulateSeq (Aig_Man_t *pAig, int nPref, int nFrames, int nWords, int fCheckMiter)
 
Abc_Cex_tFra_SmlGetCounterExample (Fra_Sml_t *p)
 
Abc_Cex_tFra_SmlCopyCounterExample (Aig_Man_t *pAig, Aig_Man_t *pFrames, int *pModel)
 

Function Documentation

void Fra_SmlAssignConst ( Fra_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 379 of file fraSim.c.

380 {
381  unsigned * pSims;
382  int i;
383  assert( Aig_ObjIsCi(pObj) || Aig_ObjIsConst1(pObj) );
384  pSims = Fra_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
385  for ( i = 0; i < p->nWordsFrame; i++ )
386  pSims[i] = fConst1? ~(unsigned)0 : 0;
387 }
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
static int Aig_ObjIsConst1(Aig_Obj_t *pObj)
Definition: aig.h:274
int nWordsFrame
Definition: fra.h:176
#define assert(ex)
Definition: util_old.h:213
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
int Id
Definition: aig.h:85
void Fra_SmlAssignDist1 ( Fra_Sml_t p,
unsigned *  pPat 
)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 433 of file fraSim.c.

434 {
435  Aig_Obj_t * pObj;
436  int f, i, k, Limit, nTruePis;
437  assert( p->nFrames > 0 );
438  if ( p->nFrames == 1 )
439  {
440  // copy the PI info
441  Aig_ManForEachCi( p->pAig, pObj, i )
442  Fra_SmlAssignConst( p, pObj, Abc_InfoHasBit(pPat, i), 0 );
443  // flip one bit
444  Limit = Abc_MinInt( Aig_ManCiNum(p->pAig), p->nWordsTotal * 32 - 1 );
445  for ( i = 0; i < Limit; i++ )
446  Abc_InfoXorBit( Fra_ObjSim( p, Aig_ManCi(p->pAig,i)->Id ), i+1 );
447  }
448  else
449  {
450  int fUseDist1 = 0;
451 
452  // copy the PI info for each frame
453  nTruePis = Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig);
454  for ( f = 0; f < p->nFrames; f++ )
455  Aig_ManForEachPiSeq( p->pAig, pObj, i )
456  Fra_SmlAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * f + i), f );
457  // copy the latch info
458  k = 0;
459  Aig_ManForEachLoSeq( p->pAig, pObj, i )
460  Fra_SmlAssignConst( p, pObj, Abc_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
461 // assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManCiNum(p->pManFraig) );
462 
463  // flip one bit of the last frame
464  if ( fUseDist1 ) //&& p->nFrames == 2 )
465  {
466  Limit = Abc_MinInt( nTruePis, p->nWordsFrame * 32 - 1 );
467  for ( i = 0; i < Limit; i++ )
468  Abc_InfoXorBit( Fra_ObjSim( p, Aig_ManCi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 );
469  }
470  }
471 }
int nFrames
Definition: fra.h:175
Aig_Man_t * pAig
Definition: fra.h:173
void Fra_SmlAssignConst(Fra_Sml_t *p, Aig_Obj_t *pObj, int fConst1, int iFrame)
Definition: fraSim.c:379
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
static void Abc_InfoXorBit(unsigned *p, int i)
Definition: abc_global.h:260
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
for(p=first;p->value< newval;p=p->next)
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
static Aig_Obj_t * Aig_ManCi(Aig_Man_t *p, int i)
Definition: aig.h:266
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
if(last==0)
Definition: sparse_int.h:34
else
Definition: sparse_int.h:55
Definition: aig.h:69
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
#define Aig_ManForEachLoSeq(p, pObj, i)
Definition: aig.h:441
#define assert(ex)
Definition: util_old.h:213
int Id
Definition: aig.h:85
#define Aig_ManForEachPiSeq(p, pObj, i)
SEQUENTIAL ITERATORS ///.
Definition: aig.h:438
void Fra_SmlAssignRandom ( Fra_Sml_t p,
Aig_Obj_t pObj 
)

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

Synopsis [Assigns random patterns to the PI node.]

Description []

SideEffects []

SeeAlso []

Definition at line 358 of file fraSim.c.

359 {
360  unsigned * pSims;
361  int i;
362  assert( Aig_ObjIsCi(pObj) );
363  pSims = Fra_ObjSim( p, pObj->Id );
364  for ( i = 0; i < p->nWordsTotal; i++ )
365  pSims[i] = Fra_ObjRandomSim();
366 }
int nWordsTotal
Definition: fra.h:177
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
static unsigned Fra_ObjRandomSim()
Definition: fra.h:258
#define assert(ex)
Definition: util_old.h:213
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
int Id
Definition: aig.h:85
int Fra_SmlCheckNonConstOutputs ( Fra_Sml_t p)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 642 of file fraSim.c.

643 {
644  Aig_Obj_t * pObj;
645  int i;
646  Aig_ManForEachPoSeq( p->pAig, pObj, i )
647  if ( !Fra_SmlNodeIsZero(p, pObj) )
648  return 1;
649  return 0;
650 }
Aig_Man_t * pAig
Definition: fra.h:173
if(last==0)
Definition: sparse_int.h:34
Definition: aig.h:69
#define Aig_ManForEachPoSeq(p, pObj, i)
Definition: aig.h:444
int Fra_SmlNodeIsZero(Fra_Sml_t *p, Aig_Obj_t *pObj)
Definition: fraSim.c:155
int Fra_SmlCheckOutput ( Fra_Man_t p)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 326 of file fraSim.c.

327 {
328  Aig_Obj_t * pObj;
329  int i;
330  // make sure the reference simulation pattern does not detect the bug
331  pObj = Aig_ManCo( p->pManAig, 0 );
332  assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) );
333  Aig_ManForEachCo( p->pManAig, pObj, i )
334  {
335  if ( !Fra_SmlNodeIsConst( Aig_ObjFanin0(pObj) ) )
336  {
337  // create the counter-example from this pattern
339  return 1;
340  }
341  }
342  return 0;
343 }
Aig_Man_t * pManAig
Definition: fra.h:191
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
int Fra_SmlNodeIsConst(Aig_Obj_t *pObj)
Definition: fraSim.c:86
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
Definition: aig.h:69
void Fra_SmlCheckOutputSavePattern(Fra_Man_t *p, Aig_Obj_t *pObjPo)
Definition: fraSim.c:281
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
#define assert(ex)
Definition: util_old.h:213
void Fra_SmlCheckOutputSavePattern ( Fra_Man_t p,
Aig_Obj_t pObjPo 
)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 281 of file fraSim.c.

282 {
283  Aig_Obj_t * pFanin, * pObjPi;
284  unsigned * pSims;
285  int i, k, BestPat, * pModel;
286  // find the word of the pattern
287  pFanin = Aig_ObjFanin0(pObjPo);
288  pSims = Fra_ObjSim(p->pSml, pFanin->Id);
289  for ( i = 0; i < p->pSml->nWordsTotal; i++ )
290  if ( pSims[i] )
291  break;
292  assert( i < p->pSml->nWordsTotal );
293  // find the bit of the pattern
294  for ( k = 0; k < 32; k++ )
295  if ( pSims[i] & (1 << k) )
296  break;
297  assert( k < 32 );
298  // determine the best pattern
299  BestPat = i * 32 + k;
300  // fill in the counter-example data
301  pModel = ABC_ALLOC( int, Aig_ManCiNum(p->pManFraig)+1 );
302  Aig_ManForEachCi( p->pManAig, pObjPi, i )
303  {
304  pModel[i] = Abc_InfoHasBit(Fra_ObjSim(p->pSml, pObjPi->Id), BestPat);
305 // printf( "%d", pModel[i] );
306  }
307  pModel[Aig_ManCiNum(p->pManAig)] = pObjPo->Id;
308 // printf( "\n" );
309  // set the model
310  assert( p->pManFraig->pData == NULL );
311  p->pManFraig->pData = pModel;
312  return;
313 }
Aig_Man_t * pManAig
Definition: fra.h:191
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Fra_Sml_t * pSml
Definition: fra.h:200
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
int nWordsTotal
Definition: fra.h:177
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
Aig_Man_t * pManFraig
Definition: fra.h:192
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Definition: aig.h:69
#define assert(ex)
Definition: util_old.h:213
int Id
Definition: aig.h:85
Abc_Cex_t* Fra_SmlCopyCounterExample ( Aig_Man_t pAig,
Aig_Man_t pFrames,
int *  pModel 
)

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

Synopsis [Generates seq counter-example from the combinational one.]

Description []

SideEffects []

SeeAlso []

Definition at line 1117 of file fraSim.c.

1118 {
1119  Abc_Cex_t * pCex;
1120  Aig_Obj_t * pObj;
1121  int i, nFrames, nTruePis, nTruePos, iPo, iFrame;
1122  // get the number of frames
1123  assert( Aig_ManRegNum(pAig) > 0 );
1124  assert( Aig_ManRegNum(pFrames) == 0 );
1125  nTruePis = Aig_ManCiNum(pAig)-Aig_ManRegNum(pAig);
1126  nTruePos = Aig_ManCoNum(pAig)-Aig_ManRegNum(pAig);
1127  nFrames = Aig_ManCiNum(pFrames) / nTruePis;
1128  assert( nTruePis * nFrames == Aig_ManCiNum(pFrames) );
1129  assert( nTruePos * nFrames == Aig_ManCoNum(pFrames) );
1130  // find the PO that failed
1131  iPo = -1;
1132  iFrame = -1;
1133  Aig_ManForEachCo( pFrames, pObj, i )
1134  if ( pObj->Id == pModel[Aig_ManCiNum(pFrames)] )
1135  {
1136  iPo = i % nTruePos;
1137  iFrame = i / nTruePos;
1138  break;
1139  }
1140  assert( iPo >= 0 );
1141  // allocate the counter example
1142  pCex = Abc_CexAlloc( Aig_ManRegNum(pAig), nTruePis, iFrame + 1 );
1143  pCex->iPo = iPo;
1144  pCex->iFrame = iFrame;
1145 
1146  // copy the bit data
1147  for ( i = 0; i < Aig_ManCiNum(pFrames); i++ )
1148  {
1149  if ( pModel[i] )
1150  Abc_InfoSetBit( pCex->pData, pCex->nRegs + i );
1151  if ( pCex->nRegs + i == pCex->nBits - 1 )
1152  break;
1153  }
1154 
1155  // verify the counter example
1156  if ( !Saig_ManVerifyCex( pAig, pCex ) )
1157  {
1158  printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" );
1159  Abc_CexFree( pCex );
1160  pCex = NULL;
1161  }
1162  return pCex;
1163 
1164 }
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
int Saig_ManVerifyCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition: saigDup.c:279
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
if(last==0)
Definition: sparse_int.h:34
Definition: aig.h:69
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
#define assert(ex)
Definition: util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
void Abc_CexFree(Abc_Cex_t *p)
Definition: utilCex.c:371
Abc_Cex_t* Fra_SmlGetCounterExample ( Fra_Sml_t p)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 1043 of file fraSim.c.

1044 {
1045  Abc_Cex_t * pCex;
1046  Aig_Obj_t * pObj;
1047  unsigned * pSims;
1048  int iPo, iFrame, iBit, i, k;
1049 
1050  // make sure the simulation manager has it
1051  assert( p->fNonConstOut );
1052 
1053  // find the first output that failed
1054  iPo = -1;
1055  iBit = -1;
1056  iFrame = -1;
1057  Aig_ManForEachPoSeq( p->pAig, pObj, iPo )
1058  {
1059  if ( Fra_SmlNodeIsZero(p, pObj) )
1060  continue;
1061  pSims = Fra_ObjSim( p, pObj->Id );
1062  for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
1063  if ( pSims[i] )
1064  {
1065  iFrame = i / p->nWordsFrame;
1066  iBit = 32 * (i % p->nWordsFrame) + Aig_WordFindFirstBit( pSims[i] );
1067  break;
1068  }
1069  break;
1070  }
1071  assert( iPo < Aig_ManCoNum(p->pAig)-Aig_ManRegNum(p->pAig) );
1072  assert( iFrame < p->nFrames );
1073  assert( iBit < 32 * p->nWordsFrame );
1074 
1075  // allocate the counter example
1076  pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Aig_ManCiNum(p->pAig) - Aig_ManRegNum(p->pAig), iFrame + 1 );
1077  pCex->iPo = iPo;
1078  pCex->iFrame = iFrame;
1079 
1080  // copy the bit data
1081  Aig_ManForEachLoSeq( p->pAig, pObj, k )
1082  {
1083  pSims = Fra_ObjSim( p, pObj->Id );
1084  if ( Abc_InfoHasBit( pSims, iBit ) )
1085  Abc_InfoSetBit( pCex->pData, k );
1086  }
1087  for ( i = 0; i <= iFrame; i++ )
1088  {
1089  Aig_ManForEachPiSeq( p->pAig, pObj, k )
1090  {
1091  pSims = Fra_ObjSim( p, pObj->Id );
1092  if ( Abc_InfoHasBit( pSims, 32 * p->nWordsFrame * i + iBit ) )
1093  Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * i + k );
1094  }
1095  }
1096  // verify the counter example
1097  if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
1098  {
1099  printf( "Fra_SmlGetCounterExample(): Counter-example is invalid.\n" );
1100  Abc_CexFree( pCex );
1101  pCex = NULL;
1102  }
1103  return pCex;
1104 }
int fNonConstOut
Definition: fra.h:179
Aig_Man_t * pAig
Definition: fra.h:173
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
int Saig_ManVerifyCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition: saigDup.c:279
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
static int Aig_ManCoNum(Aig_Man_t *p)
Definition: aig.h:252
static int Aig_WordFindFirstBit(unsigned uWord)
Definition: aig.h:237
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Definition: aig.h:69
int nWordsFrame
Definition: fra.h:176
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
#define Aig_ManForEachLoSeq(p, pObj, i)
Definition: aig.h:441
#define assert(ex)
Definition: util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
int nWordsPref
Definition: fra.h:178
void Abc_CexFree(Abc_Cex_t *p)
Definition: utilCex.c:371
#define Aig_ManForEachPoSeq(p, pObj, i)
Definition: aig.h:444
int Id
Definition: aig.h:85
#define Aig_ManForEachPiSeq(p, pObj, i)
SEQUENTIAL ITERATORS ///.
Definition: aig.h:438
int Fra_SmlNodeIsZero(Fra_Sml_t *p, Aig_Obj_t *pObj)
Definition: fraSim.c:155
void Fra_SmlInitialize ( Fra_Sml_t p,
int  fInit 
)

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

Synopsis [Assings random simulation info for the PIs.]

Description []

SideEffects []

SeeAlso []

Definition at line 400 of file fraSim.c.

401 {
402  Aig_Obj_t * pObj;
403  int i;
404  if ( fInit )
405  {
406  assert( Aig_ManRegNum(p->pAig) > 0 );
408  // assign random info for primary inputs
409  Aig_ManForEachPiSeq( p->pAig, pObj, i )
410  Fra_SmlAssignRandom( p, pObj );
411  // assign the initial state for the latches
412  Aig_ManForEachLoSeq( p->pAig, pObj, i )
413  Fra_SmlAssignConst( p, pObj, 0, 0 );
414  }
415  else
416  {
417  Aig_ManForEachCi( p->pAig, pObj, i )
418  Fra_SmlAssignRandom( p, pObj );
419  }
420 }
void Fra_SmlAssignRandom(Fra_Sml_t *p, Aig_Obj_t *pObj)
Definition: fraSim.c:358
Aig_Man_t * pAig
Definition: fra.h:173
void Fra_SmlAssignConst(Fra_Sml_t *p, Aig_Obj_t *pObj, int fConst1, int iFrame)
Definition: fraSim.c:379
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
else
Definition: sparse_int.h:55
Definition: aig.h:69
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
#define Aig_ManForEachLoSeq(p, pObj, i)
Definition: aig.h:441
#define assert(ex)
Definition: util_old.h:213
#define Aig_ManForEachPiSeq(p, pObj, i)
SEQUENTIAL ITERATORS ///.
Definition: aig.h:438
void Fra_SmlInitializeGiven ( Fra_Sml_t p,
Vec_Str_t vSimInfo 
)

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

Synopsis [Assigns simulation patters derived from file.]

Description []

SideEffects []

SeeAlso []

Definition at line 917 of file fraSim.c.

918 {
919  Aig_Obj_t * pObj;
920  unsigned * pSims;
921  int i, k, nPats = Vec_StrSize(vSimInfo) / Aig_ManCiNum(p->pAig);
922  int nPatsPadded = p->nWordsTotal * 32;
923  assert( Aig_ManRegNum(p->pAig) == 0 );
924  assert( Vec_StrSize(vSimInfo) % Aig_ManCiNum(p->pAig) == 0 );
925  assert( nPats <= nPatsPadded );
926  Aig_ManForEachCi( p->pAig, pObj, i )
927  {
928  pSims = Fra_ObjSim( p, pObj->Id );
929  // clean data
930  for ( k = 0; k < p->nWordsTotal; k++ )
931  pSims[k] = 0;
932  // load patterns
933  for ( k = 0; k < nPats; k++ )
934  if ( Vec_StrEntry(vSimInfo, k * Aig_ManCiNum(p->pAig) + i) )
935  Abc_InfoSetBit( pSims, k );
936  // pad the remaining bits with the value of the last pattern
937  for ( ; k < nPatsPadded; k++ )
938  if ( Vec_StrEntry(vSimInfo, (nPats-1) * Aig_ManCiNum(p->pAig) + i) )
939  Abc_InfoSetBit( pSims, k );
940  }
941 }
Aig_Man_t * pAig
Definition: fra.h:173
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
int nWordsTotal
Definition: fra.h:177
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
static char Vec_StrEntry(Vec_Str_t *p, int i)
Definition: vecStr.h:336
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Definition: aig.h:69
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
static int Vec_StrSize(Vec_Str_t *p)
Definition: bblif.c:600
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
#define assert(ex)
Definition: util_old.h:213
int Id
Definition: aig.h:85
void Fra_SmlNodeCopyFanin ( Fra_Sml_t p,
Aig_Obj_t pObj,
int  iFrame 
)

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

Synopsis [Simulates one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 579 of file fraSim.c.

580 {
581  unsigned * pSims, * pSims0;
582  int fCompl, fCompl0, i;
583  assert( !Aig_IsComplement(pObj) );
584  assert( Aig_ObjIsCo(pObj) );
585  assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
586  // get hold of the simulation information
587  pSims = Fra_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame;
588  pSims0 = Fra_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + p->nWordsFrame * iFrame;
589  // get complemented attributes of the children using their random info
590  fCompl = pObj->fPhase;
591  fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
592  // copy information as it is
593 // if ( Aig_ObjFaninC0(pObj) )
594  if ( fCompl0 )
595  for ( i = 0; i < p->nWordsFrame; i++ )
596  pSims[i] = ~pSims0[i];
597  else
598  for ( i = 0; i < p->nWordsFrame; i++ )
599  pSims[i] = pSims0[i];
600 }
static Aig_Obj_t * Aig_ObjChild0(Aig_Obj_t *pObj)
Definition: aig.h:310
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
int nWordsTotal
Definition: fra.h:177
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
static int Aig_ObjPhaseReal(Aig_Obj_t *pObj)
Definition: aig.h:299
int nWordsFrame
Definition: fra.h:176
unsigned int fPhase
Definition: aig.h:78
#define assert(ex)
Definition: util_old.h:213
int Id
Definition: aig.h:85
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
int Fra_SmlNodeCountOnes ( Fra_Sml_t p,
Aig_Obj_t pObj 
)

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

Synopsis [Counts the number of one's in the patten of the output.]

Description []

SideEffects []

SeeAlso []

Definition at line 177 of file fraSim.c.

178 {
179  unsigned * pSims;
180  int i, Counter = 0;
181  pSims = Fra_ObjSim(p, pObj->Id);
182  for ( i = 0; i < p->nWordsTotal; i++ )
183  Counter += Aig_WordCountOnes( pSims[i] );
184  return Counter;
185 }
int nWordsTotal
Definition: fra.h:177
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
static int Aig_WordCountOnes(unsigned uWord)
Definition: aig.h:229
static int Counter
int Id
Definition: aig.h:85
ABC_NAMESPACE_IMPL_START int Fra_SmlNodeHash ( Aig_Obj_t pObj,
int  nTableSize 
)

DECLARATIONS ///.

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

FileName [fraSim.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [New FRAIG package.]

Synopsis []

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - June 30, 2007.]

Revision [

Id:
fraSim.c,v 1.00 2007/06/30 00:00:00 alanmi Exp

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file fraSim.c.

47 {
48  Fra_Man_t * p = (Fra_Man_t *)pObj->pData;
49  static int s_FPrimes[128] = {
50  1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459,
51  1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997,
52  2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543,
53  2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089,
54  3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671,
55  3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243,
56  4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871,
57  4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471,
58  5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073,
59  6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689,
60  6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309,
61  7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933,
62  8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
63  };
64  unsigned * pSims;
65  unsigned uHash;
66  int i;
67 // assert( p->pSml->nWordsTotal <= 128 );
68  uHash = 0;
69  pSims = Fra_ObjSim(p->pSml, pObj->Id);
70  for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ )
71  uHash ^= pSims[i] * s_FPrimes[i & 0x7F];
72  return uHash % nTableSize;
73 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void * pData
Definition: aig.h:87
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
int Id
Definition: aig.h:85
int Fra_SmlNodeIsConst ( Aig_Obj_t pObj)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 86 of file fraSim.c.

87 {
88  Fra_Man_t * p = (Fra_Man_t *)pObj->pData;
89  unsigned * pSims;
90  int i;
91  pSims = Fra_ObjSim(p->pSml, pObj->Id);
92  for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ )
93  if ( pSims[i] )
94  return 0;
95  return 1;
96 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void * pData
Definition: aig.h:87
Fra_Sml_t * pSml
Definition: fra.h:200
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
int nWordsPref
Definition: fra.h:178
int Id
Definition: aig.h:85
int Fra_SmlNodeIsZero ( Fra_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 155 of file fraSim.c.

156 {
157  unsigned * pSims;
158  int i;
159  pSims = Fra_ObjSim(p, pObj->Id);
160  for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
161  if ( pSims[i] )
162  return 0;
163  return 1;
164 }
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
int nWordsPref
Definition: fra.h:178
int Id
Definition: aig.h:85
int Fra_SmlNodeNotEquWeight ( Fra_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 133 of file fraSim.c.

134 {
135  unsigned * pSimL, * pSimR;
136  int k, Counter = 0;
137  pSimL = Fra_ObjSim( p, Left );
138  pSimR = Fra_ObjSim( p, Right );
139  for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
140  Counter += Aig_WordCountOnes( pSimL[k] ^ pSimR[k] );
141  return Counter;
142 }
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
static int Aig_WordCountOnes(unsigned uWord)
Definition: aig.h:229
static int Counter
int nWordsPref
Definition: fra.h:178
int Fra_SmlNodesAreEqual ( Aig_Obj_t pObj0,
Aig_Obj_t pObj1 
)

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

Synopsis [Returns 1 if simulation infos are equal.]

Description []

SideEffects []

SeeAlso []

Definition at line 109 of file fraSim.c.

110 {
111  Fra_Man_t * p = (Fra_Man_t *)pObj0->pData;
112  unsigned * pSims0, * pSims1;
113  int i;
114  pSims0 = Fra_ObjSim(p->pSml, pObj0->Id);
115  pSims1 = Fra_ObjSim(p->pSml, pObj1->Id);
116  for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ )
117  if ( pSims0[i] != pSims1[i] )
118  return 0;
119  return 1;
120 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void * pData
Definition: aig.h:87
Fra_Sml_t * pSml
Definition: fra.h:200
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
int nWordsPref
Definition: fra.h:178
int Id
Definition: aig.h:85
int Fra_SmlNodesCompareInFrame ( Fra_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 550 of file fraSim.c.

551 {
552  unsigned * pSims0, * pSims1;
553  int i;
554  assert( !Aig_IsComplement(pObj0) );
555  assert( !Aig_IsComplement(pObj1) );
556  assert( iFrame0 == 0 || p->nWordsFrame < p->nWordsTotal );
557  assert( iFrame1 == 0 || p->nWordsFrame < p->nWordsTotal );
558  // get hold of the simulation information
559  pSims0 = Fra_ObjSim(p, pObj0->Id) + p->nWordsFrame * iFrame0;
560  pSims1 = Fra_ObjSim(p, pObj1->Id) + p->nWordsFrame * iFrame1;
561  // compare
562  for ( i = 0; i < p->nWordsFrame; i++ )
563  if ( pSims0[i] != pSims1[i] )
564  return 0;
565  return 1;
566 }
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
int nWordsTotal
Definition: fra.h:177
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
int nWordsFrame
Definition: fra.h:176
#define assert(ex)
Definition: util_old.h:213
int Id
Definition: aig.h:85
void Fra_SmlNodeSimulate ( Fra_Sml_t p,
Aig_Obj_t pObj,
int  iFrame 
)

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

Synopsis [Simulates one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 485 of file fraSim.c.

486 {
487  unsigned * pSims, * pSims0, * pSims1;
488  int fCompl, fCompl0, fCompl1, i;
489  assert( !Aig_IsComplement(pObj) );
490  assert( Aig_ObjIsNode(pObj) );
491  assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
492  // get hold of the simulation information
493  pSims = Fra_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame;
494  pSims0 = Fra_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + p->nWordsFrame * iFrame;
495  pSims1 = Fra_ObjSim(p, Aig_ObjFanin1(pObj)->Id) + p->nWordsFrame * iFrame;
496  // get complemented attributes of the children using their random info
497  fCompl = pObj->fPhase;
498  fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
499  fCompl1 = Aig_ObjPhaseReal(Aig_ObjChild1(pObj));
500  // simulate
501  if ( fCompl0 && fCompl1 )
502  {
503  if ( fCompl )
504  for ( i = 0; i < p->nWordsFrame; i++ )
505  pSims[i] = (pSims0[i] | pSims1[i]);
506  else
507  for ( i = 0; i < p->nWordsFrame; i++ )
508  pSims[i] = ~(pSims0[i] | pSims1[i]);
509  }
510  else if ( fCompl0 && !fCompl1 )
511  {
512  if ( fCompl )
513  for ( i = 0; i < p->nWordsFrame; i++ )
514  pSims[i] = (pSims0[i] | ~pSims1[i]);
515  else
516  for ( i = 0; i < p->nWordsFrame; i++ )
517  pSims[i] = (~pSims0[i] & pSims1[i]);
518  }
519  else if ( !fCompl0 && fCompl1 )
520  {
521  if ( fCompl )
522  for ( i = 0; i < p->nWordsFrame; i++ )
523  pSims[i] = (~pSims0[i] | pSims1[i]);
524  else
525  for ( i = 0; i < p->nWordsFrame; i++ )
526  pSims[i] = (pSims0[i] & ~pSims1[i]);
527  }
528  else // if ( !fCompl0 && !fCompl1 )
529  {
530  if ( fCompl )
531  for ( i = 0; i < p->nWordsFrame; i++ )
532  pSims[i] = ~(pSims0[i] & pSims1[i]);
533  else
534  for ( i = 0; i < p->nWordsFrame; i++ )
535  pSims[i] = (pSims0[i] & pSims1[i]);
536  }
537 }
static Aig_Obj_t * Aig_ObjChild0(Aig_Obj_t *pObj)
Definition: aig.h:310
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
int nWordsTotal
Definition: fra.h:177
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
static Aig_Obj_t * Aig_ObjChild1(Aig_Obj_t *pObj)
Definition: aig.h:311
static int Aig_ObjPhaseReal(Aig_Obj_t *pObj)
Definition: aig.h:299
int nWordsFrame
Definition: fra.h:176
unsigned int fPhase
Definition: aig.h:78
#define assert(ex)
Definition: util_old.h:213
int Id
Definition: aig.h:85
void Fra_SmlNodeTransferNext ( Fra_Sml_t p,
Aig_Obj_t pOut,
Aig_Obj_t pIn,
int  iFrame 
)

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

Synopsis [Simulates one node.]

Description []

SideEffects []

SeeAlso []

Definition at line 613 of file fraSim.c.

614 {
615  unsigned * pSims0, * pSims1;
616  int i;
617  assert( !Aig_IsComplement(pOut) );
618  assert( !Aig_IsComplement(pIn) );
619  assert( Aig_ObjIsCo(pOut) );
620  assert( Aig_ObjIsCi(pIn) );
621  assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
622  // get hold of the simulation information
623  pSims0 = Fra_ObjSim(p, pOut->Id) + p->nWordsFrame * iFrame;
624  pSims1 = Fra_ObjSim(p, pIn->Id) + p->nWordsFrame * (iFrame+1);
625  // copy information as it is
626  for ( i = 0; i < p->nWordsFrame; i++ )
627  pSims1[i] = pSims0[i];
628 }
static int Aig_IsComplement(Aig_Obj_t *p)
Definition: aig.h:249
int nWordsTotal
Definition: fra.h:177
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
int nWordsFrame
Definition: fra.h:176
#define assert(ex)
Definition: util_old.h:213
static int Aig_ObjIsCi(Aig_Obj_t *pObj)
Definition: aig.h:275
int Id
Definition: aig.h:85
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
void Fra_SmlPrintOutputs ( Fra_Sml_t p,
int  nPatterns 
)

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

Synopsis [Prints output values.]

Description []

SideEffects []

SeeAlso []

Definition at line 954 of file fraSim.c.

955 {
956  Aig_Obj_t * pObj;
957  unsigned * pSims;
958  int i, k;
959  for ( k = 0; k < nPatterns; k++ )
960  {
961  Aig_ManForEachCo( p->pAig, pObj, i )
962  {
963  pSims = Fra_ObjSim( p, pObj->Id );
964  printf( "%d", Abc_InfoHasBit( pSims, k ) );
965  }
966  printf( "\n" ); ;
967  }
968 }
Aig_Man_t * pAig
Definition: fra.h:173
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
static unsigned * Fra_ObjSim(Fra_Sml_t *p, int Id)
MACRO DEFINITIONS ///.
Definition: fra.h:257
Definition: aig.h:69
int Id
Definition: aig.h:85
void Fra_SmlResimulate ( Fra_Man_t p)

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

Synopsis [Resimulates fraiging manager after finding a counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 703 of file fraSim.c.

704 {
705  int nChanges;
706  abctime clk;
708  Fra_SmlSimulateOne( p->pSml );
709 // if ( p->pPars->fPatScores )
710 // Fra_CleanPatScores( p );
711  if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
712  return;
713 clk = Abc_Clock();
714  nChanges = Fra_ClassesRefine( p->pCla );
715  nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
716  if ( p->pCla->vImps )
717  nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps );
718  if ( p->vOneHots )
719  nChanges += Fra_OneHotRefineUsingCex( p, p->vOneHots );
720 p->timeRef += Abc_Clock() - clk;
721  if ( !p->pPars->nFramesK && nChanges < 1 )
722  printf( "Error: A counter-example did not refine classes!\n" );
723 // assert( nChanges >= 1 );
724 //printf( "Refined classes = %5d. Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges );
725 }
int Fra_ImpRefineUsingCex(Fra_Man_t *p, Vec_Int_t *vImps)
Definition: fraImp.c:575
int Fra_ClassesRefine1(Fra_Cla_t *p, int fRefineNewClass, int *pSkipped)
Definition: fraClass.c:527
Fra_Cla_t * pCla
Definition: fra.h:198
Fra_Par_t * pPars
Definition: fra.h:189
Fra_Sml_t * pSml
Definition: fra.h:200
Vec_Int_t * vOneHots
Definition: fra.h:208
static abctime Abc_Clock()
Definition: abc_global.h:279
void Fra_SmlSimulateOne(Fra_Sml_t *p)
Definition: fraSim.c:663
unsigned * pPatWords
Definition: fra.h:205
int Fra_SmlCheckOutput(Fra_Man_t *p)
Definition: fraSim.c:326
int Fra_OneHotRefineUsingCex(Fra_Man_t *p, Vec_Int_t *vOneHots)
Definition: fraHot.c:266
abctime timeRef
Definition: fra.h:247
void Fra_SmlAssignDist1(Fra_Sml_t *p, unsigned *pPat)
Definition: fraSim.c:433
Vec_Int_t * vImps
Definition: fra.h:163
int Fra_ClassesRefine(Fra_Cla_t *p)
Definition: fraClass.c:493
ABC_INT64_T abctime
Definition: abc_global.h:278
void Fra_SmlSavePattern ( Fra_Man_t p)

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

Synopsis [Copy pattern from the solver into the internal storage.]

Description []

SideEffects []

SeeAlso []

Definition at line 241 of file fraSim.c.

242 {
243  Aig_Obj_t * pObj;
244  int i;
245  memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
246  Aig_ManForEachCi( p->pManFraig, pObj, i )
247 // if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
248  if ( sat_solver_var_value(p->pSat, Fra_ObjSatNum(pObj)) )
249  Abc_InfoSetBit( p->pPatWords, i );
250 
251  if ( p->vCex )
252  {
253  Vec_IntClear( p->vCex );
254  for ( i = 0; i < Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); i++ )
255  Vec_IntPush( p->vCex, Abc_InfoHasBit( p->pPatWords, i ) );
256  for ( i = Aig_ManCiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManCiNum(p->pManFraig); i++ )
257  Vec_IntPush( p->vCex, Abc_InfoHasBit( p->pPatWords, i ) );
258  }
259 
260 /*
261  printf( "Pattern: " );
262  Aig_ManForEachCi( p->pManFraig, pObj, i )
263  printf( "%d", Abc_InfoHasBit( p->pPatWords, i ) );
264  printf( "\n" );
265 */
266 }
char * memset()
Aig_Man_t * pManAig
Definition: fra.h:191
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
static int sat_solver_var_value(sat_solver *s, int v)
Definition: satSolver.h:200
unsigned * pPatWords
Definition: fra.h:205
Aig_Man_t * pManFraig
Definition: fra.h:192
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Vec_Int_t * vCex
Definition: fra.h:206
if(last==0)
Definition: sparse_int.h:34
Definition: aig.h:69
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
int nPatWords
Definition: fra.h:204
static int Fra_ObjSatNum(Aig_Obj_t *pObj)
Definition: fra.h:266
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
void Fra_SmlSavePattern0 ( Fra_Man_t p,
int  fInit 
)

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

Synopsis [Generated const 0 pattern.]

Description []

SideEffects []

SeeAlso []

Definition at line 200 of file fraSim.c.

201 {
202  memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
203 }
char * memset()
unsigned * pPatWords
Definition: fra.h:205
int nPatWords
Definition: fra.h:204
void Fra_SmlSavePattern1 ( Fra_Man_t p,
int  fInit 
)

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

Synopsis [[Generated const 1 pattern.]

Description []

SideEffects []

SeeAlso []

Definition at line 216 of file fraSim.c.

217 {
218  Aig_Obj_t * pObj;
219  int i, k, nTruePis;
220  memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords );
221  if ( !fInit )
222  return;
223  // clear the state bits to correspond to all-0 initial state
224  nTruePis = Aig_ManCiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
225  k = 0;
226  Aig_ManForEachLoSeq( p->pManAig, pObj, i )
227  Abc_InfoXorBit( p->pPatWords, nTruePis * p->nFramesAll + k++ );
228 }
char * memset()
Aig_Man_t * pManAig
Definition: fra.h:191
static void Abc_InfoXorBit(unsigned *p, int i)
Definition: abc_global.h:260
unsigned * pPatWords
Definition: fra.h:205
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
Definition: aig.h:69
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
int nPatWords
Definition: fra.h:204
#define Aig_ManForEachLoSeq(p, pObj, i)
Definition: aig.h:441
void Fra_SmlSimulate ( Fra_Man_t p,
int  fInit 
)

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

Synopsis [Performs simulation of the manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 738 of file fraSim.c.

739 {
740  int fVerbose = 0;
741  int nChanges, nClasses;
742  abctime clk;
743  assert( !fInit || Aig_ManRegNum(p->pManAig) );
744  // start the classes
745  Fra_SmlInitialize( p->pSml, fInit );
746  Fra_SmlSimulateOne( p->pSml );
747  if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
748  return;
749  Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr, 0 );
750 // Fra_ClassesPrint( p->pCla, 0 );
751 if ( fVerbose )
752 printf( "Starting classes = %5d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
753 
754 //return;
755 
756  // refine classes by walking 0/1 patterns
757  Fra_SmlSavePattern0( p, fInit );
759  Fra_SmlSimulateOne( p->pSml );
760  if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
761  return;
762 clk = Abc_Clock();
763  nChanges = Fra_ClassesRefine( p->pCla );
764  nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
765 p->timeRef += Abc_Clock() - clk;
766 if ( fVerbose )
767 printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
768  Fra_SmlSavePattern1( p, fInit );
770  Fra_SmlSimulateOne( p->pSml );
771  if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
772  return;
773 clk = Abc_Clock();
774  nChanges = Fra_ClassesRefine( p->pCla );
775  nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
776 p->timeRef += Abc_Clock() - clk;
777 
778 if ( fVerbose )
779 printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
780  // refine classes by random simulation
781  do {
782  Fra_SmlInitialize( p->pSml, fInit );
783  Fra_SmlSimulateOne( p->pSml );
784  nClasses = Vec_PtrSize(p->pCla->vClasses);
785  if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
786  return;
787 clk = Abc_Clock();
788  nChanges = Fra_ClassesRefine( p->pCla );
789  nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
790 p->timeRef += Abc_Clock() - clk;
791 if ( fVerbose )
792 printf( "Refined classes = %5d. Changes = %4d. Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
793  } while ( (double)nChanges / nClasses > p->pPars->dSimSatur );
794 
795 // if ( p->pPars->fVerbose )
796 // printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n",
797 // Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
798 // Fra_ClassesPrint( p->pCla, 0 );
799 }
void Fra_SmlInitialize(Fra_Sml_t *p, int fInit)
Definition: fraSim.c:400
int Fra_ClassesRefine1(Fra_Cla_t *p, int fRefineNewClass, int *pSkipped)
Definition: fraClass.c:527
Aig_Man_t * pManAig
Definition: fra.h:191
Fra_Cla_t * pCla
Definition: fra.h:198
Vec_Ptr_t * vClasses
Definition: fra.h:154
Fra_Par_t * pPars
Definition: fra.h:189
int Fra_ClassesCountLits(Fra_Cla_t *p)
Definition: fraClass.c:164
Fra_Sml_t * pSml
Definition: fra.h:200
static abctime Abc_Clock()
Definition: abc_global.h:279
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
void Fra_SmlSimulateOne(Fra_Sml_t *p)
Definition: fraSim.c:663
unsigned * pPatWords
Definition: fra.h:205
void Fra_ClassesPrepare(Fra_Cla_t *p, int fLatchCorr, int nMaxLevs)
Definition: fraClass.c:276
int Fra_SmlCheckOutput(Fra_Man_t *p)
Definition: fraSim.c:326
abctime timeRef
Definition: fra.h:247
void Fra_SmlAssignDist1(Fra_Sml_t *p, unsigned *pPat)
Definition: fraSim.c:433
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
int Fra_ClassesRefine(Fra_Cla_t *p)
Definition: fraClass.c:493
#define assert(ex)
Definition: util_old.h:213
ABC_INT64_T abctime
Definition: abc_global.h:278
void Fra_SmlSavePattern1(Fra_Man_t *p, int fInit)
Definition: fraSim.c:216
void Fra_SmlSavePattern0(Fra_Man_t *p, int fInit)
Definition: fraSim.c:200
Fra_Sml_t* Fra_SmlSimulateComb ( Aig_Man_t pAig,
int  nWords,
int  fCheckMiter 
)

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

Synopsis [Performs simulation of the uninitialized circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 856 of file fraSim.c.

857 {
858  Fra_Sml_t * p;
859  p = Fra_SmlStart( pAig, 0, 1, nWords );
860  Fra_SmlInitialize( p, 0 );
861  Fra_SmlSimulateOne( p );
862  if ( fCheckMiter )
864  return p;
865 }
int fNonConstOut
Definition: fra.h:179
void Fra_SmlInitialize(Fra_Sml_t *p, int fInit)
Definition: fraSim.c:400
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Fra_SmlSimulateOne(Fra_Sml_t *p)
Definition: fraSim.c:663
int nWords
Definition: abcNpn.c:127
int Fra_SmlCheckNonConstOutputs(Fra_Sml_t *p)
Definition: fraSim.c:642
Fra_Sml_t * Fra_SmlStart(Aig_Man_t *pAig, int nPref, int nFrames, int nWordsFrame)
Definition: fraSim.c:813
Fra_Sml_t* Fra_SmlSimulateCombGiven ( Aig_Man_t pAig,
char *  pFileName,
int  fCheckMiter,
int  fVerbose 
)

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

Synopsis [Assigns simulation patters derived from file.]

Description []

SideEffects []

SeeAlso []

Definition at line 981 of file fraSim.c.

982 {
983  Vec_Str_t * vSimInfo;
984  Fra_Sml_t * p;
985  int nPatterns;
986  assert( Aig_ManRegNum(pAig) == 0 );
987  // read comb patterns from file
988  vSimInfo = Fra_SmlSimulateReadFile( pFileName );
989  if ( vSimInfo == NULL )
990  return NULL;
991  if ( Vec_StrSize(vSimInfo) % Aig_ManCiNum(pAig) != 0 )
992  {
993  printf( "File \"%s\": The number of binary digits (%d) is not divisible by the number of primary inputs (%d).\n",
994  pFileName, Vec_StrSize(vSimInfo), Aig_ManCiNum(pAig) );
995  Vec_StrFree( vSimInfo );
996  return NULL;
997  }
998  p = Fra_SmlStart( pAig, 0, 1, Abc_BitWordNum(Vec_StrSize(vSimInfo) / Aig_ManCiNum(pAig)) );
999  Fra_SmlInitializeGiven( p, vSimInfo );
1000  nPatterns = Vec_StrSize(vSimInfo) / Aig_ManCiNum(pAig);
1001  Vec_StrFree( vSimInfo );
1002  Fra_SmlSimulateOne( p );
1003  if ( fCheckMiter )
1005  if ( fVerbose )
1006  Fra_SmlPrintOutputs( p, nPatterns );
1007  return p;
1008 }
int fNonConstOut
Definition: fra.h:179
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Fra_SmlSimulateOne(Fra_Sml_t *p)
Definition: fraSim.c:663
void Fra_SmlInitializeGiven(Fra_Sml_t *p, Vec_Str_t *vSimInfo)
Definition: fraSim.c:917
int Fra_SmlCheckNonConstOutputs(Fra_Sml_t *p)
Definition: fraSim.c:642
Vec_Str_t * Fra_SmlSimulateReadFile(char *pFileName)
Definition: fraSim.c:879
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
void Fra_SmlPrintOutputs(Fra_Sml_t *p, int nPatterns)
Definition: fraSim.c:954
static int Vec_StrSize(Vec_Str_t *p)
Definition: bblif.c:600
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
#define assert(ex)
Definition: util_old.h:213
Fra_Sml_t * Fra_SmlStart(Aig_Man_t *pAig, int nPref, int nFrames, int nWordsFrame)
Definition: fraSim.c:813
void Fra_SmlSimulateOne ( Fra_Sml_t p)

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

Synopsis [Simulates AIG manager.]

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

SideEffects []

SeeAlso []

Definition at line 663 of file fraSim.c.

664 {
665  Aig_Obj_t * pObj, * pObjLi, * pObjLo;
666  int f, i;
667  abctime clk;
668 clk = Abc_Clock();
669  for ( f = 0; f < p->nFrames; f++ )
670  {
671  // simulate the nodes
672  Aig_ManForEachNode( p->pAig, pObj, i )
673  Fra_SmlNodeSimulate( p, pObj, f );
674  // copy simulation info into outputs
675  Aig_ManForEachPoSeq( p->pAig, pObj, i )
676  Fra_SmlNodeCopyFanin( p, pObj, f );
677  // quit if this is the last timeframe
678  if ( f == p->nFrames - 1 )
679  break;
680  // copy simulation info into outputs
681  Aig_ManForEachLiSeq( p->pAig, pObj, i )
682  Fra_SmlNodeCopyFanin( p, pObj, f );
683  // copy simulation info into the inputs
684  Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
685  Fra_SmlNodeTransferNext( p, pObjLi, pObjLo, f );
686  }
687 p->timeSim += Abc_Clock() - clk;
688 p->nSimRounds++;
689 }
int nFrames
Definition: fra.h:175
void Fra_SmlNodeSimulate(Fra_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: fraSim.c:485
Aig_Man_t * pAig
Definition: fra.h:173
static abctime Abc_Clock()
Definition: abc_global.h:279
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
#define Aig_ManForEachLiLoSeq(p, pObjLi, pObjLo, k)
Definition: aig.h:450
if(last==0)
Definition: sparse_int.h:34
Definition: aig.h:69
void Fra_SmlNodeCopyFanin(Fra_Sml_t *p, Aig_Obj_t *pObj, int iFrame)
Definition: fraSim.c:579
#define Aig_ManForEachLiSeq(p, pObj, i)
Definition: aig.h:447
void Fra_SmlNodeTransferNext(Fra_Sml_t *p, Aig_Obj_t *pOut, Aig_Obj_t *pIn, int iFrame)
Definition: fraSim.c:613
#define Aig_ManForEachPoSeq(p, pObj, i)
Definition: aig.h:444
ABC_INT64_T abctime
Definition: abc_global.h:278
Vec_Str_t* Fra_SmlSimulateReadFile ( char *  pFileName)

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

Synopsis [Reads simulation patterns from file.]

Description [Each pattern contains the given number (nInputs) of binary digits. No other symbols (except spaces and line endings) are allowed in the file.]

SideEffects []

SeeAlso []

Definition at line 879 of file fraSim.c.

880 {
881  Vec_Str_t * vRes;
882  FILE * pFile;
883  int c;
884  pFile = fopen( pFileName, "rb" );
885  if ( pFile == NULL )
886  {
887  printf( "Cannot open file \"%s\" with simulation patterns.\n", pFileName );
888  return NULL;
889  }
890  vRes = Vec_StrAlloc( 1000 );
891  while ( (c = fgetc(pFile)) != EOF )
892  {
893  if ( c == '0' || c == '1' )
894  Vec_StrPush( vRes, (char)(c - '0') );
895  else if ( c != ' ' && c != '\r' && c != '\n' && c != '\t' )
896  {
897  printf( "File \"%s\" contains symbol (%c) other than \'0\' or \'1\'.\n", pFileName, (char)c );
898  Vec_StrFreeP( &vRes );
899  break;
900  }
901  }
902  fclose( pFile );
903  return vRes;
904 }
static Vec_Str_t * Vec_StrAlloc(int nCap)
Definition: bblif.c:495
static void Vec_StrPush(Vec_Str_t *p, char Entry)
Definition: vecStr.h:535
static void Vec_StrFreeP(Vec_Str_t **p)
Definition: vecStr.h:233
Fra_Sml_t* Fra_SmlSimulateSeq ( Aig_Man_t pAig,
int  nPref,
int  nFrames,
int  nWords,
int  fCheckMiter 
)

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

Synopsis [Performs simulation of the initialized circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 1021 of file fraSim.c.

1022 {
1023  Fra_Sml_t * p;
1024  p = Fra_SmlStart( pAig, nPref, nFrames, nWords );
1025  Fra_SmlInitialize( p, 1 );
1026  Fra_SmlSimulateOne( p );
1027  if ( fCheckMiter )
1029  return p;
1030 }
int fNonConstOut
Definition: fra.h:179
void Fra_SmlInitialize(Fra_Sml_t *p, int fInit)
Definition: fraSim.c:400
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Fra_SmlSimulateOne(Fra_Sml_t *p)
Definition: fraSim.c:663
int nWords
Definition: abcNpn.c:127
int Fra_SmlCheckNonConstOutputs(Fra_Sml_t *p)
Definition: fraSim.c:642
Fra_Sml_t * Fra_SmlStart(Aig_Man_t *pAig, int nPref, int nFrames, int nWordsFrame)
Definition: fraSim.c:813
Fra_Sml_t* Fra_SmlStart ( Aig_Man_t pAig,
int  nPref,
int  nFrames,
int  nWordsFrame 
)

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

Synopsis [Allocates simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 813 of file fraSim.c.

814 {
815  Fra_Sml_t * p;
816  p = (Fra_Sml_t *)ABC_ALLOC( char, sizeof(Fra_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
817  memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
818  p->pAig = pAig;
819  p->nPref = nPref;
820  p->nFrames = nPref + nFrames;
821  p->nWordsFrame = nWordsFrame;
822  p->nWordsTotal = (nPref + nFrames) * nWordsFrame;
823  p->nWordsPref = nPref * nWordsFrame;
824  // constant 1 is initialized to 0 because we store values modulus phase (pObj->fPhase)
825  return p;
826 }
char * memset()
int nFrames
Definition: fra.h:175
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Aig_Man_t * pAig
Definition: fra.h:173
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
int nWordsTotal
Definition: fra.h:177
int nWordsFrame
Definition: fra.h:176
static int Aig_ManObjNumMax(Aig_Man_t *p)
Definition: aig.h:259
int nWordsPref
Definition: fra.h:178
int nPref
Definition: fra.h:174
void Fra_SmlStop ( Fra_Sml_t p)

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

Synopsis [Deallocates simulation manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 839 of file fraSim.c.

840 {
841  ABC_FREE( p );
842 }
#define ABC_FREE(obj)
Definition: abc_global.h:232