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

Go to the source code of this file.

Functions

static
ABC_NAMESPACE_IMPL_START void 
Gia_ManCorrSpecReduce_rec (Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj, int f, int nPrefix)
 DECLARATIONS ///. More...
 
static int Gia_ManCorrSpecReal (Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj, int f, int nPrefix)
 FUNCTION DEFINITIONS ///. More...
 
Gia_Man_tGia_ManCorrSpecReduce (Gia_Man_t *p, int nFrames, int fScorr, Vec_Int_t **pvOutputs, int fRings)
 
Gia_Man_tGia_ManCorrSpecReduceInit (Gia_Man_t *p, int nFrames, int nPrefix, int fScorr, Vec_Int_t **pvOutputs, int fRings)
 
void Cec_ManStartSimInfo (Vec_Ptr_t *vInfo, int nFlops)
 
void Gia_ManCorrRemapSimInfo (Gia_Man_t *p, Vec_Ptr_t *vInfo)
 
Vec_Int_tGia_ManCorrCreateRemapping (Gia_Man_t *p)
 
void Gia_ManCorrPerformRemapping (Vec_Int_t *vPairs, Vec_Ptr_t *vInfo)
 
int Cec_ManLoadCounterExamplesTry (Vec_Ptr_t *vInfo, Vec_Ptr_t *vPres, int iBit, int *pLits, int nLits)
 
int Cec_ManLoadCounterExamples (Vec_Ptr_t *vInfo, Vec_Int_t *vCexStore, int iStart)
 
int Cec_ManLoadCounterExamples2 (Vec_Ptr_t *vInfo, Vec_Int_t *vCexStore, int iStart)
 
int Cec_ManResimulateCounterExamples (Cec_ManSim_t *pSim, Vec_Int_t *vCexStore, int nFrames)
 
int Cec_ManResimulateCounterExamplesComb (Cec_ManSim_t *pSim, Vec_Int_t *vCexStore)
 
int Gia_ManCheckRefinements (Gia_Man_t *p, Vec_Str_t *vStatus, Vec_Int_t *vOutputs, Cec_ManSim_t *pSim, int fRings)
 
void Gia_ManCorrReduce_rec (Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj)
 
Gia_Man_tGia_ManCorrReduce (Gia_Man_t *p)
 
void Cec_ManRefinedClassPrintStats (Gia_Man_t *p, Vec_Str_t *vStatus, int iIter, abctime Time)
 MACRO DEFINITIONS ///. More...
 
void Cec_ManLSCorrespondenceBmc (Gia_Man_t *pAig, Cec_ParCor_t *pPars, int nPrefs)
 
int Cec_ManLSCorrAnalyzeDependence (Gia_Man_t *p, Vec_Int_t *vEquivs, Vec_Str_t *vStatus)
 
int Cec_ManLSCorrespondenceClasses (Gia_Man_t *pAig, Cec_ParCor_t *pPars)
 
unsigned * Cec_ManComputeInitState (Gia_Man_t *pAig, int nFrames)
 
void Cec_ManPrintFlopEquivs (Gia_Man_t *p)
 
Gia_Man_tCec_ManLSCorrespondence (Gia_Man_t *pAig, Cec_ParCor_t *pPars)
 

Function Documentation

unsigned* Cec_ManComputeInitState ( Gia_Man_t pAig,
int  nFrames 
)

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

Synopsis [Computes new initial state.]

Description []

SideEffects []

SeeAlso []

Definition at line 1068 of file cecCorr.c.

1069 {
1070  Gia_Obj_t * pObj, * pObjRo, * pObjRi;
1071  unsigned * pInitState;
1072  int i, f;
1073  Gia_ManRandom( 1 );
1074 // Abc_Print( 1, "Simulating %d timeframes.\n", nFrames );
1075  Gia_ManForEachRo( pAig, pObj, i )
1076  pObj->fMark1 = 0;
1077  for ( f = 0; f < nFrames; f++ )
1078  {
1079  Gia_ManConst0(pAig)->fMark1 = 0;
1080  Gia_ManForEachPi( pAig, pObj, i )
1081  pObj->fMark1 = Gia_ManRandom(0) & 1;
1082  Gia_ManForEachAnd( pAig, pObj, i )
1083  pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj)) &
1084  (Gia_ObjFanin1(pObj)->fMark1 ^ Gia_ObjFaninC1(pObj));
1085  Gia_ManForEachRi( pAig, pObj, i )
1086  pObj->fMark1 = (Gia_ObjFanin0(pObj)->fMark1 ^ Gia_ObjFaninC0(pObj));
1087  Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, i )
1088  pObjRo->fMark1 = pObjRi->fMark1;
1089  }
1090  pInitState = ABC_CALLOC( unsigned, Abc_BitWordNum(Gia_ManRegNum(pAig)) );
1091  Gia_ManForEachRo( pAig, pObj, i )
1092  {
1093  if ( pObj->fMark1 )
1094  Abc_InfoSetBit( pInitState, i );
1095 // Abc_Print( 1, "%d", pObj->fMark1 );
1096  }
1097 // Abc_Print( 1, "\n" );
1098  Gia_ManCleanMark1( pAig );
1099  return pInitState;
1100 }
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
unsigned fMark1
Definition: gia.h:84
for(p=first;p->value< newval;p=p->next)
Definition: gia.h:75
void Gia_ManCleanMark1(Gia_Man_t *p)
Definition: giaUtil.c:272
unsigned Gia_ManRandom(int fReset)
FUNCTION DEFINITIONS ///.
Definition: giaUtil.c:49
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition: gia.h:1042
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
int Cec_ManLoadCounterExamples ( Vec_Ptr_t vInfo,
Vec_Int_t vCexStore,
int  iStart 
)

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

Synopsis [Performs bitpacking of counter-examples.]

Description []

SideEffects []

SeeAlso []

Definition at line 458 of file cecCorr.c.

459 {
460  Vec_Int_t * vPat;
461  Vec_Ptr_t * vPres;
462  int nWords = Vec_PtrReadWordsSimInfo(vInfo);
463  int nBits = 32 * nWords;
464  int k, nSize, kMax = 0;//, iBit = 1;
465  vPat = Vec_IntAlloc( 100 );
466  vPres = Vec_PtrAllocSimInfo( Vec_PtrSize(vInfo), nWords );
467  Vec_PtrCleanSimInfo( vPres, 0, nWords );
468  while ( iStart < Vec_IntSize(vCexStore) )
469  {
470  // skip the output number
471  iStart++;
472  // get the number of items
473  nSize = Vec_IntEntry( vCexStore, iStart++ );
474  if ( nSize <= 0 )
475  continue;
476  // extract pattern
477  Vec_IntClear( vPat );
478  for ( k = 0; k < nSize; k++ )
479  Vec_IntPush( vPat, Vec_IntEntry( vCexStore, iStart++ ) );
480  // add pattern to storage
481  for ( k = 1; k < nBits; k++ )
482  if ( Cec_ManLoadCounterExamplesTry( vInfo, vPres, k, (int *)Vec_IntArray(vPat), Vec_IntSize(vPat) ) )
483  break;
484  kMax = Abc_MaxInt( kMax, k );
485  if ( k == nBits-1 )
486  break;
487  }
488  Vec_PtrFree( vPres );
489  Vec_IntFree( vPat );
490  return iStart;
491 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static void Vec_PtrCleanSimInfo(Vec_Ptr_t *vInfo, int iWord, int nWords)
Definition: vecPtr.h:968
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
int nWords
Definition: abcNpn.c:127
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
int Cec_ManLoadCounterExamplesTry(Vec_Ptr_t *vInfo, Vec_Ptr_t *vPres, int iBit, int *pLits, int nLits)
Definition: cecCorr.c:424
static int Vec_PtrReadWordsSimInfo(Vec_Ptr_t *p)
Definition: vecPtr.h:952
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
static Vec_Ptr_t * Vec_PtrAllocSimInfo(int nEntries, int nWords)
Definition: vecPtr.h:929
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
int Cec_ManLoadCounterExamples2 ( Vec_Ptr_t vInfo,
Vec_Int_t vCexStore,
int  iStart 
)

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

Synopsis [Performs bitpacking of counter-examples.]

Description []

SideEffects []

SeeAlso []

Definition at line 504 of file cecCorr.c.

505 {
506  unsigned * pInfo;
507  int nBits = 32 * Vec_PtrReadWordsSimInfo(vInfo);
508  int k, iLit, nLits, Out, iBit = 1;
509  while ( iStart < Vec_IntSize(vCexStore) )
510  {
511  // skip the output number
512 // iStart++;
513  Out = Vec_IntEntry( vCexStore, iStart++ );
514 // Abc_Print( 1, "iBit = %d. Out = %d.\n", iBit, Out );
515  // get the number of items
516  nLits = Vec_IntEntry( vCexStore, iStart++ );
517  if ( nLits <= 0 )
518  continue;
519  // add pattern to storage
520  for ( k = 0; k < nLits; k++ )
521  {
522  iLit = Vec_IntEntry( vCexStore, iStart++ );
523  pInfo = (unsigned *)Vec_PtrEntry( vInfo, Abc_Lit2Var(iLit) );
524  if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(iLit) )
525  Abc_InfoXorBit( pInfo, iBit );
526  }
527  if ( ++iBit == nBits )
528  break;
529  }
530 // Abc_Print( 1, "added %d bits\n", iBit-1 );
531  return iStart;
532 }
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
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static int Vec_PtrReadWordsSimInfo(Vec_Ptr_t *p)
Definition: vecPtr.h:952
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
int Cec_ManLoadCounterExamplesTry ( Vec_Ptr_t vInfo,
Vec_Ptr_t vPres,
int  iBit,
int *  pLits,
int  nLits 
)

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

Synopsis [Packs one counter-examples into the array of simulation info.]

Description []

SideEffects []

SeeAlso []

                               ` 

Definition at line 424 of file cecCorr.c.

425 {
426  unsigned * pInfo, * pPres;
427  int i;
428  for ( i = 0; i < nLits; i++ )
429  {
430  pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
431  pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
432  if ( Abc_InfoHasBit( pPres, iBit ) &&
433  Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
434  return 0;
435  }
436  for ( i = 0; i < nLits; i++ )
437  {
438  pInfo = (unsigned *)Vec_PtrEntry(vInfo, Abc_Lit2Var(pLits[i]));
439  pPres = (unsigned *)Vec_PtrEntry(vPres, Abc_Lit2Var(pLits[i]));
440  Abc_InfoSetBit( pPres, iBit );
441  if ( Abc_InfoHasBit( pInfo, iBit ) == Abc_LitIsCompl(pLits[i]) )
442  Abc_InfoXorBit( pInfo, iBit );
443  }
444  return 1;
445 }
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
static int Abc_LitIsCompl(int Lit)
Definition: abc_global.h:265
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
static int Abc_Lit2Var(int Lit)
Definition: abc_global.h:264
int Cec_ManLSCorrAnalyzeDependence ( Gia_Man_t p,
Vec_Int_t vEquivs,
Vec_Str_t vStatus 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 839 of file cecCorr.c.

840 {
841  Gia_Obj_t * pObj, * pObjRo;
842  int i, Iter, iObj, iRepr, fPrev, Total, Count0, Count1;
843  assert( Vec_StrSize(vStatus) * 2 == Vec_IntSize(vEquivs) );
844  Total = 0;
845  Gia_ManForEachObj( p, pObj, i )
846  {
847  assert( pObj->fMark1 == 0 );
848  if ( Gia_ObjHasRepr(p, i) )
849  Total++;
850  }
851  Count0 = 0;
852  for ( i = 0; i < Vec_StrSize(vStatus); i++ )
853  {
854  iRepr = Vec_IntEntry(vEquivs, 2*i);
855  iObj = Vec_IntEntry(vEquivs, 2*i+1);
856  assert( iRepr == Gia_ObjRepr(p, iObj) );
857  if ( Vec_StrEntry(vStatus, i) != 1 ) // disproved or undecided
858  {
859  Gia_ManObj(p, iObj)->fMark1 = 1;
860  Count0++;
861  }
862  }
863  for ( Iter = 0; Iter < 100; Iter++ )
864  {
865  int fChanges = 0;
866  Gia_ManForEachObj1( p, pObj, i )
867  {
868  if ( Gia_ObjIsCi(pObj) )
869  continue;
870  assert( Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) );
871 // fPrev = pObj->fMark1;
872  if ( Gia_ObjIsAnd(pObj) )
873  pObj->fMark1 |= Gia_ObjFanin0(pObj)->fMark1 | Gia_ObjFanin1(pObj)->fMark1;
874  else
875  pObj->fMark1 |= Gia_ObjFanin0(pObj)->fMark1;
876 // fChanges += fPrev ^ pObj->fMark1;
877  }
878  Gia_ManForEachRiRo( p, pObj, pObjRo, i )
879  {
880  fPrev = pObjRo->fMark1;
881  pObjRo->fMark1 = pObj->fMark1;
882  fChanges += fPrev ^ pObjRo->fMark1;
883  }
884  if ( fChanges == 0 )
885  break;
886  }
887  Count1 = 0;
888  Gia_ManForEachObj( p, pObj, i )
889  {
890  if ( pObj->fMark1 && Gia_ObjHasRepr(p, i) )
891  Count1++;
892  pObj->fMark1 = 0;
893  }
894  printf( "%5d -> %5d (%3d) ", Count0, Count1, Iter );
895  return 0;
896 }
unsigned fMark1
Definition: gia.h:84
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Definition: gia.h:75
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition: gia.h:1042
static char Vec_StrEntry(Vec_Str_t *p, int i)
Definition: vecStr.h:336
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
static int Vec_StrSize(Vec_Str_t *p)
Definition: bblif.c:600
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
#define assert(ex)
Definition: util_old.h:213
#define Gia_ManForEachObj1(p, pObj, i)
Definition: gia.h:986
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
static int Gia_ObjRepr(Gia_Man_t *p, int Id)
Definition: gia.h:887
static int Gia_ObjHasRepr(Gia_Man_t *p, int Id)
Definition: gia.h:891
Gia_Man_t* Cec_ManLSCorrespondence ( Gia_Man_t pAig,
Cec_ParCor_t pPars 
)

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

Synopsis [Top-level procedure for register correspondence.]

Description []

SideEffects []

SeeAlso []

Definition at line 1147 of file cecCorr.c.

1148 {
1149  Gia_Man_t * pNew, * pTemp;
1150  unsigned * pInitState;
1151  int RetValue;
1152  ABC_FREE( pAig->pReprs );
1153  ABC_FREE( pAig->pNexts );
1154  if ( pPars->nPrefix == 0 )
1155  {
1156  RetValue = Cec_ManLSCorrespondenceClasses( pAig, pPars );
1157  if ( RetValue == 0 )
1158  return Gia_ManDup( pAig );
1159  }
1160  else
1161  {
1162  // compute the cycles AIG
1163  pInitState = Cec_ManComputeInitState( pAig, pPars->nPrefix );
1164  pTemp = Gia_ManDupFlip( pAig, (int *)pInitState );
1165  ABC_FREE( pInitState );
1166  // compute classes of this AIG
1167  RetValue = Cec_ManLSCorrespondenceClasses( pTemp, pPars );
1168  // transfer the class info
1169  pAig->pReprs = pTemp->pReprs; pTemp->pReprs = NULL;
1170  pAig->pNexts = pTemp->pNexts; pTemp->pNexts = NULL;
1171  // perform additional BMC
1172  pPars->fUseCSat = 0;
1173  pPars->nBTLimit = Abc_MaxInt( pPars->nBTLimit, 1000 );
1174  Cec_ManLSCorrespondenceBmc( pAig, pPars, pPars->nPrefix );
1175 /*
1176  // transfer the class info back
1177  pTemp->pReprs = pAig->pReprs; pAig->pReprs = NULL;
1178  pTemp->pNexts = pAig->pNexts; pAig->pNexts = NULL;
1179  // continue refining
1180  RetValue = Cec_ManLSCorrespondenceClasses( pTemp, pPars );
1181  // transfer the class info
1182  pAig->pReprs = pTemp->pReprs; pTemp->pReprs = NULL;
1183  pAig->pNexts = pTemp->pNexts; pTemp->pNexts = NULL;
1184 */
1185  Gia_ManStop( pTemp );
1186  }
1187  // derive reduced AIG
1188  if ( pPars->fMakeChoices )
1189  {
1190  pNew = Gia_ManEquivToChoices( pAig, 1 );
1191 // Gia_ManHasChoices_very_old( pNew );
1192  }
1193  else
1194  {
1195 // Gia_ManEquivImprove( pAig );
1196  pNew = Gia_ManCorrReduce( pAig );
1197  pNew = Gia_ManSeqCleanup( pTemp = pNew );
1198  Gia_ManStop( pTemp );
1199  //Gia_AigerWrite( pNew, "reduced.aig", 0, 0 );
1200  }
1201  // report the results
1202  if ( pPars->fVerbose )
1203  {
1204  Abc_Print( 1, "NBeg = %d. NEnd = %d. (Gain = %6.2f %%). RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n",
1205  Gia_ManAndNum(pAig), Gia_ManAndNum(pNew),
1206  100.0*(Gia_ManAndNum(pAig)-Gia_ManAndNum(pNew))/(Gia_ManAndNum(pAig)?Gia_ManAndNum(pAig):1),
1207  Gia_ManRegNum(pAig), Gia_ManRegNum(pNew),
1208  100.0*(Gia_ManRegNum(pAig)-Gia_ManRegNum(pNew))/(Gia_ManRegNum(pAig)?Gia_ManRegNum(pAig):1) );
1209  }
1210  if ( pPars->nPrefix && (Gia_ManAndNum(pNew) < Gia_ManAndNum(pAig) || Gia_ManRegNum(pNew) < Gia_ManRegNum(pAig)) )
1211  Abc_Print( 1, "The reduced AIG was produced using %d-th invariants and will not verify.\n", pPars->nPrefix );
1212  // print verbose info about equivalences
1213  if ( pPars->fVerboseFlops )
1214  {
1215  if ( pAig->vNamesIn == NULL )
1216  Abc_Print( 1, "Flop output names are not available. Use command \"&get -n\".\n" );
1217  else
1218  Cec_ManPrintFlopEquivs( pAig );
1219  }
1220  return pNew;
1221 }
Gia_Man_t * Gia_ManDup(Gia_Man_t *p)
Definition: giaDup.c:552
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
int * pNexts
Definition: gia.h:122
int fUseCSat
Definition: cec.h:146
int nPrefix
Definition: cec.h:138
int Cec_ManLSCorrespondenceClasses(Gia_Man_t *pAig, Cec_ParCor_t *pPars)
Definition: cecCorr.c:909
Gia_Man_t * Gia_ManCorrReduce(Gia_Man_t *p)
Definition: cecCorr.c:690
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
int fVerboseFlops
Definition: cec.h:150
int fVerbose
Definition: cec.h:152
Gia_Man_t * Gia_ManEquivToChoices(Gia_Man_t *p, int nSnapshots)
Definition: giaEquiv.c:1629
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
Gia_Man_t * Gia_ManSeqCleanup(Gia_Man_t *p)
Definition: giaScl.c:183
void Cec_ManLSCorrespondenceBmc(Gia_Man_t *pAig, Cec_ParCor_t *pPars, int nPrefs)
Definition: cecCorr.c:771
unsigned * Cec_ManComputeInitState(Gia_Man_t *pAig, int nFrames)
Definition: cecCorr.c:1068
int fMakeChoices
Definition: cec.h:145
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
void Cec_ManPrintFlopEquivs(Gia_Man_t *p)
Definition: cecCorr.c:1113
Gia_Man_t * Gia_ManDupFlip(Gia_Man_t *p, int *pInitState)
Definition: giaDup.c:460
#define ABC_FREE(obj)
Definition: abc_global.h:232
int nBTLimit
Definition: cec.h:139
Definition: gia.h:95
Gia_Rpr_t * pReprs
Definition: gia.h:121
Vec_Ptr_t * vNamesIn
Definition: gia.h:155
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
void Cec_ManLSCorrespondenceBmc ( Gia_Man_t pAig,
Cec_ParCor_t pPars,
int  nPrefs 
)

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

Synopsis [Runs BMC for the equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 771 of file cecCorr.c.

772 {
773  Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
774  Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
775  Vec_Str_t * vStatus;
776  Vec_Int_t * vOutputs;
777  Vec_Int_t * vCexStore;
778  Cec_ManSim_t * pSim;
779  Gia_Man_t * pSrm;
780  int fChanges, RetValue;
781  // prepare simulation manager
782  Cec_ManSimSetDefaultParams( pParsSim );
783  pParsSim->nWords = pPars->nWords;
784  pParsSim->nFrames = pPars->nRounds;
785  pParsSim->fVerbose = pPars->fVerbose;
786  pParsSim->fLatchCorr = pPars->fLatchCorr;
787  pParsSim->fSeqSimulate = 1;
788  pSim = Cec_ManSimStart( pAig, pParsSim );
789  // prepare SAT solving
790  Cec_ManSatSetDefaultParams( pParsSat );
791  pParsSat->nBTLimit = pPars->nBTLimit;
792  pParsSat->fVerbose = pPars->fVerbose;
793  fChanges = 1;
794  while ( fChanges )
795  {
796  abctime clkBmc = Abc_Clock();
797  fChanges = 0;
798  pSrm = Gia_ManCorrSpecReduceInit( pAig, pPars->nFrames, nPrefs, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
799  if ( Gia_ManPoNum(pSrm) == 0 )
800  {
801  Gia_ManStop( pSrm );
802  Vec_IntFree( vOutputs );
803  break;
804  }
805  pParsSat->nBTLimit *= 10;
806  if ( pPars->fUseCSat )
807  vCexStore = Tas_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
808  else
809  vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
810  // refine classes with these counter-examples
811  if ( Vec_IntSize(vCexStore) )
812  {
813  RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nPrefs );
814  Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
815  fChanges = 1;
816  }
817  if ( pPars->fVerbose )
818  Cec_ManRefinedClassPrintStats( pAig, vStatus, -1, Abc_Clock() - clkBmc );
819  // recycle
820  Vec_IntFree( vCexStore );
821  Vec_StrFree( vStatus );
822  Gia_ManStop( pSrm );
823  Vec_IntFree( vOutputs );
824  }
825  Cec_ManSimStop( pSim );
826 }
int nRounds
Definition: cec.h:136
int fVerbose
Definition: cec.h:73
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
int fLatchCorr
Definition: cec.h:70
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
int fUseCSat
Definition: cec.h:146
int fSeqSimulate
Definition: cec.h:69
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_Int_t * Cec_ManSatSolveMiter(Gia_Man_t *pAig, Cec_ParSat_t *pPars, Vec_Str_t **pvStatus)
Definition: cecSolve.c:1026
void Cec_ManRefinedClassPrintStats(Gia_Man_t *p, Vec_Str_t *vStatus, int iIter, abctime Time)
MACRO DEFINITIONS ///.
Definition: cecCorr.c:725
int fUseRings
Definition: cec.h:144
void Cec_ManSimStop(Cec_ManSim_t *p)
Definition: cecMan.c:232
static abctime Abc_Clock()
Definition: abc_global.h:279
int fLatchCorr
Definition: cec.h:142
int fVerbose
Definition: cec.h:152
int Gia_ManCheckRefinements(Gia_Man_t *p, Vec_Str_t *vStatus, Vec_Int_t *vOutputs, Cec_ManSim_t *pSim, int fRings)
Definition: cecCorr.c:612
Cec_ManSim_t * Cec_ManSimStart(Gia_Man_t *pAig, Cec_ParSim_t *pPars)
Definition: cecMan.c:198
void Cec_ManSimSetDefaultParams(Cec_ParSim_t *p)
Definition: cecCore.c:70
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
int nFrames
Definition: cec.h:137
int nWords
Definition: cec.h:135
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
int nFrames
Definition: cec.h:62
int nBTLimit
Definition: cec.h:139
Definition: gia.h:95
typedefABC_NAMESPACE_HEADER_START struct Cec_ParSat_t_ Cec_ParSat_t
INCLUDES ///.
Definition: cec.h:43
Gia_Man_t * Gia_ManCorrSpecReduceInit(Gia_Man_t *p, int nFrames, int nPrefix, int fScorr, Vec_Int_t **pvOutputs, int fRings)
Definition: cecCorr.c:223
int nWords
Definition: cec.h:61
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
int Cec_ManResimulateCounterExamples(Cec_ManSim_t *pSim, Vec_Int_t *vCexStore, int nFrames)
Definition: cecCorr.c:545
ABC_INT64_T abctime
Definition: abc_global.h:278
void Cec_ManSatSetDefaultParams(Cec_ParSat_t *p)
DECLARATIONS ///.
Definition: cecCore.c:45
Vec_Int_t * Tas_ManSolveMiterNc(Gia_Man_t *pGia, int nConfs, Vec_Str_t **pvStatus, int fVerbose)
Definition: giaCTas.c:1517
int Cec_ManLSCorrespondenceClasses ( Gia_Man_t pAig,
Cec_ParCor_t pPars 
)

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

Synopsis [Internal procedure for register correspondence.]

Description []

SideEffects []

SeeAlso []

Definition at line 909 of file cecCorr.c.

910 {
911  int nIterMax = 100000;
912  int nAddFrames = 1; // additional timeframes to simulate
913  int fRunBmcFirst = 1;
914  Vec_Str_t * vStatus;
915  Vec_Int_t * vOutputs;
916  Vec_Int_t * vCexStore;
917  Cec_ParSim_t ParsSim, * pParsSim = &ParsSim;
918  Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
919  Cec_ManSim_t * pSim;
920  Gia_Man_t * pSrm;
921  int r, RetValue;
922  abctime clkTotal = Abc_Clock();
923  abctime clkSat = 0, clkSim = 0, clkSrm = 0;
924  abctime clk2, clk = Abc_Clock();
925  if ( Gia_ManRegNum(pAig) == 0 )
926  {
927  Abc_Print( 1, "Cec_ManLatchCorrespondence(): Not a sequential AIG.\n" );
928  return 0;
929  }
930  Gia_ManRandom( 1 );
931  // prepare simulation manager
932  Cec_ManSimSetDefaultParams( pParsSim );
933  pParsSim->nWords = pPars->nWords;
934  pParsSim->nFrames = pPars->nFrames;
935  pParsSim->fVerbose = pPars->fVerbose;
936  pParsSim->fLatchCorr = pPars->fLatchCorr;
937  pParsSim->fConstCorr = pPars->fConstCorr;
938  pParsSim->fSeqSimulate = 1;
939  // create equivalence classes of registers
940  pSim = Cec_ManSimStart( pAig, pParsSim );
941  if ( pAig->pReprs == NULL )
942  {
943  Cec_ManSimClassesPrepare( pSim, pPars->nLevelMax );
944  Cec_ManSimClassesRefine( pSim );
945  }
946  // prepare SAT solving
947  Cec_ManSatSetDefaultParams( pParsSat );
948  pParsSat->nBTLimit = pPars->nBTLimit;
949  pParsSat->fVerbose = pPars->fVerbose;
950  // limit the number of conflicts in the circuit-based solver
951  if ( pPars->fUseCSat )
952  pParsSat->nBTLimit = Abc_MinInt( pParsSat->nBTLimit, 1000 );
953  if ( pPars->fVerbose )
954  {
955  Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n",
956  Gia_ManObjNum(pAig), Gia_ManAndNum(pAig),
957  pPars->nBTLimit, pPars->nFrames, pPars->fLatchCorr, pPars->fUseRings, pPars->fUseCSat );
958  Cec_ManRefinedClassPrintStats( pAig, NULL, 0, Abc_Clock() - clk );
959  }
960  // check the base case
961  if ( fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) )
962  Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
963  if ( pPars->pFunc )
964  {
965  ((int (*)(void *))pPars->pFunc)( pPars->pData );
966  ((int (*)(void *))pPars->pFunc)( pPars->pData );
967  }
968  if ( pPars->nStepsMax == 0 )
969  {
970  Abc_Print( 1, "Stopped signal correspondence after BMC.\n" );
971  Cec_ManSimStop( pSim );
972  return 1;
973  }
974  // perform refinement of equivalence classes
975  for ( r = 0; r < nIterMax; r++ )
976  {
977  if ( pPars->nStepsMax == r )
978  {
979  Cec_ManSimStop( pSim );
980  Abc_Print( 1, "Stopped signal correspondence after %d refiment iterations.\n", r );
981  return 1;
982  }
983  clk = Abc_Clock();
984  // perform speculative reduction
985  clk2 = Abc_Clock();
986  pSrm = Gia_ManCorrSpecReduce( pAig, pPars->nFrames, !pPars->fLatchCorr, &vOutputs, pPars->fUseRings );
987  assert( Gia_ManRegNum(pSrm) == 0 && Gia_ManPiNum(pSrm) == Gia_ManRegNum(pAig)+(pPars->nFrames+!pPars->fLatchCorr)*Gia_ManPiNum(pAig) );
988  clkSrm += Abc_Clock() - clk2;
989  if ( Gia_ManCoNum(pSrm) == 0 )
990  {
991  Vec_IntFree( vOutputs );
992  Gia_ManStop( pSrm );
993  break;
994  }
995 //Gia_DumpAiger( pSrm, "corrsrm", r, 2 );
996  // found counter-examples to speculation
997  clk2 = Abc_Clock();
998  if ( pPars->fUseCSat )
999  vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
1000  else
1001  vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
1002  Gia_ManStop( pSrm );
1003  clkSat += Abc_Clock() - clk2;
1004  if ( Vec_IntSize(vCexStore) == 0 )
1005  {
1006  Vec_IntFree( vCexStore );
1007  Vec_StrFree( vStatus );
1008  Vec_IntFree( vOutputs );
1009  break;
1010  }
1011 // Cec_ManLSCorrAnalyzeDependence( pAig, vOutputs, vStatus );
1012 
1013  // refine classes with these counter-examples
1014  clk2 = Abc_Clock();
1015  RetValue = Cec_ManResimulateCounterExamples( pSim, vCexStore, pPars->nFrames + 1 + nAddFrames );
1016  Vec_IntFree( vCexStore );
1017  clkSim += Abc_Clock() - clk2;
1018  Gia_ManCheckRefinements( pAig, vStatus, vOutputs, pSim, pPars->fUseRings );
1019  if ( pPars->fVerbose )
1020  Cec_ManRefinedClassPrintStats( pAig, vStatus, r+1, Abc_Clock() - clk );
1021  Vec_StrFree( vStatus );
1022  Vec_IntFree( vOutputs );
1023 //Gia_ManEquivPrintClasses( pAig, 1, 0 );
1024  if ( pPars->pFunc )
1025  ((int (*)(void *))pPars->pFunc)( pPars->pData );
1026  // quit if const is no longer there
1027  if ( pPars->fStopWhenGone && Gia_ManPoNum(pAig) == 1 && !Gia_ObjIsConst( pAig, Gia_ObjFaninId0p(pAig, Gia_ManPo(pAig, 0)) ) )
1028  {
1029  printf( "Iterative refinement is stopped after iteration %d\n", r );
1030  printf( "because the property output is no longer a candidate constant.\n" );
1031  Cec_ManSimStop( pSim );
1032  return 0;
1033  }
1034  }
1035  if ( pPars->fVerbose )
1036  Cec_ManRefinedClassPrintStats( pAig, NULL, r+1, Abc_Clock() - clk );
1037  // check the overflow
1038  if ( r == nIterMax )
1039  Abc_Print( 1, "The refinement was not finished. The result may be incorrect.\n" );
1040  Cec_ManSimStop( pSim );
1041  // check the base case
1042  if ( !fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) )
1043  Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
1044  clkTotal = Abc_Clock() - clkTotal;
1045  // report the results
1046  if ( pPars->fVerbose )
1047  {
1048  ABC_PRTP( "Srm ", clkSrm, clkTotal );
1049  ABC_PRTP( "Sat ", clkSat, clkTotal );
1050  ABC_PRTP( "Sim ", clkSim, clkTotal );
1051  ABC_PRTP( "Other", clkTotal-clkSat-clkSrm-clkSim, clkTotal );
1052  Abc_PrintTime( 1, "TOTAL", clkTotal );
1053  }
1054  return 1;
1055 }
int fVerbose
Definition: cec.h:73
Gia_Man_t * Gia_ManCorrSpecReduce(Gia_Man_t *p, int nFrames, int fScorr, Vec_Int_t **pvOutputs, int fRings)
Definition: cecCorr.c:106
int Cec_ManSimClassesPrepare(Cec_ManSim_t *p, int LevelMax)
Definition: cecClass.c:851
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
int fLatchCorr
Definition: cec.h:70
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
int fUseCSat
Definition: cec.h:146
int fSeqSimulate
Definition: cec.h:69
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_Int_t * Cec_ManSatSolveMiter(Gia_Man_t *pAig, Cec_ParSat_t *pPars, Vec_Str_t **pvStatus)
Definition: cecSolve.c:1026
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
void * pData
Definition: cec.h:154
void Cec_ManRefinedClassPrintStats(Gia_Man_t *p, Vec_Str_t *vStatus, int iIter, abctime Time)
MACRO DEFINITIONS ///.
Definition: cecCorr.c:725
int fUseRings
Definition: cec.h:144
int fConstCorr
Definition: cec.h:143
void Cec_ManSimStop(Cec_ManSim_t *p)
Definition: cecMan.c:232
static abctime Abc_Clock()
Definition: abc_global.h:279
int fLatchCorr
Definition: cec.h:142
int fVerbose
Definition: cec.h:152
int Gia_ManCheckRefinements(Gia_Man_t *p, Vec_Str_t *vStatus, Vec_Int_t *vOutputs, Cec_ManSim_t *pSim, int fRings)
Definition: cecCorr.c:612
Cec_ManSim_t * Cec_ManSimStart(Gia_Man_t *pAig, Cec_ParSim_t *pPars)
Definition: cecMan.c:198
Vec_Int_t * Cbs_ManSolveMiterNc(Gia_Man_t *pGia, int nConfs, Vec_Str_t **pvStatus, int fVerbose)
Definition: giaCSat.c:998
unsigned Gia_ManRandom(int fReset)
FUNCTION DEFINITIONS ///.
Definition: giaUtil.c:49
#define ABC_PRTP(a, t, T)
Definition: abc_global.h:223
void Cec_ManSimSetDefaultParams(Cec_ParSim_t *p)
Definition: cecCore.c:70
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
int fConstCorr
Definition: cec.h:71
void Cec_ManLSCorrespondenceBmc(Gia_Man_t *pAig, Cec_ParCor_t *pPars, int nPrefs)
Definition: cecCorr.c:771
static void Vec_StrFree(Vec_Str_t *p)
Definition: bblif.c:616
int nFrames
Definition: cec.h:137
static int Gia_ObjIsConst(Gia_Man_t *p, int Id)
Definition: gia.h:915
int nLevelMax
Definition: cec.h:140
int fStopWhenGone
Definition: cec.h:149
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
int nWords
Definition: cec.h:135
void * pFunc
Definition: cec.h:155
int Cec_ManSimClassesRefine(Cec_ManSim_t *p)
Definition: cecClass.c:908
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
int nFrames
Definition: cec.h:62
int nBTLimit
Definition: cec.h:139
Definition: gia.h:95
static int Gia_ObjFaninId0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:463
typedefABC_NAMESPACE_HEADER_START struct Cec_ParSat_t_ Cec_ParSat_t
INCLUDES ///.
Definition: cec.h:43
Gia_Rpr_t * pReprs
Definition: gia.h:121
#define assert(ex)
Definition: util_old.h:213
int nWords
Definition: cec.h:61
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
int nStepsMax
Definition: cec.h:141
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
int Cec_ManResimulateCounterExamples(Cec_ManSim_t *pSim, Vec_Int_t *vCexStore, int nFrames)
Definition: cecCorr.c:545
ABC_INT64_T abctime
Definition: abc_global.h:278
void Cec_ManSatSetDefaultParams(Cec_ParSat_t *p)
DECLARATIONS ///.
Definition: cecCore.c:45
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
void Cec_ManPrintFlopEquivs ( Gia_Man_t p)

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

Synopsis [Prints flop equivalences.]

Description []

SideEffects []

SeeAlso []

Definition at line 1113 of file cecCorr.c.

1114 {
1115  Gia_Obj_t * pObj, * pRepr;
1116  int i;
1117  assert( p->vNamesIn != NULL );
1118  Gia_ManForEachRo( p, pObj, i )
1119  {
1120  if ( Gia_ObjIsConst(p, Gia_ObjId(p, pObj)) )
1121  Abc_Print( 1, "Original flop %s is proved equivalent to constant.\n", Vec_PtrEntry(p->vNamesIn, Gia_ObjCioId(pObj)) );
1122  else if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
1123  {
1124  if ( Gia_ObjIsCi(pRepr) )
1125  Abc_Print( 1, "Original flop %s is proved equivalent to flop %s.\n",
1126  Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pObj) ),
1127  Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pRepr) ) );
1128  else
1129  Abc_Print( 1, "Original flop %s is proved equivalent to internal node %d.\n",
1130  Vec_PtrEntry( p->vNamesIn, Gia_ObjCioId(pObj) ), Gia_ObjId(p, pRepr) );
1131  }
1132  }
1133 }
Definition: gia.h:75
static int Gia_ObjIsConst(Gia_Man_t *p, int Id)
Definition: gia.h:915
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static Gia_Obj_t * Gia_ObjReprObj(Gia_Man_t *p, int Id)
Definition: gia.h:886
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
#define assert(ex)
Definition: util_old.h:213
Vec_Ptr_t * vNamesIn
Definition: gia.h:155
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
static int Gia_ObjCioId(Gia_Obj_t *pObj)
Definition: gia.h:411
void Cec_ManRefinedClassPrintStats ( Gia_Man_t p,
Vec_Str_t vStatus,
int  iIter,
abctime  Time 
)

MACRO DEFINITIONS ///.

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

Synopsis [Prints statistics during solving.]

Description []

SideEffects []

SeeAlso []

Definition at line 725 of file cecCorr.c.

726 {
727  int nLits, CounterX = 0, Counter0 = 0, Counter = 0;
728  int i, Entry, nProve = 0, nDispr = 0, nFail = 0;
729  for ( i = 1; i < Gia_ManObjNum(p); i++ )
730  {
731  if ( Gia_ObjIsNone(p, i) )
732  CounterX++;
733  else if ( Gia_ObjIsConst(p, i) )
734  Counter0++;
735  else if ( Gia_ObjIsHead(p, i) )
736  Counter++;
737  }
738  CounterX -= Gia_ManCoNum(p);
739  nLits = Gia_ManCiNum(p) + Gia_ManAndNum(p) - Counter - CounterX;
740  if ( iIter == -1 )
741  Abc_Print( 1, "BMC : " );
742  else
743  Abc_Print( 1, "%3d : ", iIter );
744  Abc_Print( 1, "c =%8d cl =%7d lit =%8d ", Counter0, Counter, nLits );
745  if ( vStatus )
746  Vec_StrForEachEntry( vStatus, Entry, i )
747  {
748  if ( Entry == 1 )
749  nProve++;
750  else if ( Entry == 0 )
751  nDispr++;
752  else if ( Entry == -1 )
753  nFail++;
754  }
755  Abc_Print( 1, "p =%6d d =%6d f =%6d ", nProve, nDispr, nFail );
756  Abc_Print( 1, "%c ", Gia_ObjIsConst( p, Gia_ObjFaninId0p(p, Gia_ManPo(p, 0)) ) ? '+' : '-' );
757  Abc_PrintTime( 1, "T", Time );
758 }
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
#define Vec_StrForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecStr.h:54
static int Gia_ObjIsHead(Gia_Man_t *p, int Id)
Definition: gia.h:916
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
static int Gia_ManAndNum(Gia_Man_t *p)
Definition: gia.h:389
static int Gia_ObjIsConst(Gia_Man_t *p, int Id)
Definition: gia.h:915
static int Counter
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
static int Gia_ObjIsNone(Gia_Man_t *p, int Id)
Definition: gia.h:917
static int Gia_ObjFaninId0p(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:463
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static int Gia_ManCoNum(Gia_Man_t *p)
Definition: gia.h:384
int Cec_ManResimulateCounterExamples ( Cec_ManSim_t pSim,
Vec_Int_t vCexStore,
int  nFrames 
)

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

Synopsis [Resimulates counter-examples derived by the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 545 of file cecCorr.c.

546 {
547  Vec_Int_t * vPairs;
548  Vec_Ptr_t * vSimInfo;
549  int RetValue = 0, iStart = 0;
550  vPairs = Gia_ManCorrCreateRemapping( pSim->pAig );
551  Gia_ManCreateValueRefs( pSim->pAig );
552 // pSim->pPars->nWords = 63;
553  pSim->pPars->nFrames = nFrames;
554  vSimInfo = Vec_PtrAllocSimInfo( Gia_ManRegNum(pSim->pAig) + Gia_ManPiNum(pSim->pAig) * nFrames, pSim->pPars->nWords );
555  while ( iStart < Vec_IntSize(vCexStore) )
556  {
557  Cec_ManStartSimInfo( vSimInfo, Gia_ManRegNum(pSim->pAig) );
558  iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
559 // iStart = Cec_ManLoadCounterExamples2( vSimInfo, vCexStore, iStart );
560 // Gia_ManCorrRemapSimInfo( pSim->pAig, vSimInfo );
561  Gia_ManCorrPerformRemapping( vPairs, vSimInfo );
562  RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
563 // Cec_ManSeqResimulateInfo( pSim->pAig, vSimInfo, NULL );
564  }
565 //Gia_ManEquivPrintOne( pSim->pAig, 85, 0 );
566  assert( iStart == Vec_IntSize(vCexStore) );
567  Vec_PtrFree( vSimInfo );
568  Vec_IntFree( vPairs );
569  return RetValue;
570 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
void Cec_ManStartSimInfo(Vec_Ptr_t *vInfo, int nFlops)
Definition: cecCorr.c:292
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Gia_Man_t * pAig
Definition: cecInt.h:115
void Gia_ManCreateValueRefs(Gia_Man_t *p)
Definition: giaUtil.c:687
int Cec_ManLoadCounterExamples(Vec_Ptr_t *vInfo, Vec_Int_t *vCexStore, int iStart)
Definition: cecCorr.c:458
void Gia_ManCorrPerformRemapping(Vec_Int_t *vPairs, Vec_Ptr_t *vInfo)
Definition: cecCorr.c:395
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
int nFrames
Definition: cec.h:62
Cec_ParSim_t * pPars
Definition: cecInt.h:116
#define assert(ex)
Definition: util_old.h:213
int nWords
Definition: cec.h:61
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
int Cec_ManSeqResimulate(Cec_ManSim_t *p, Vec_Ptr_t *vInfo)
Definition: cecSeq.c:137
static Vec_Ptr_t * Vec_PtrAllocSimInfo(int nEntries, int nWords)
Definition: vecPtr.h:929
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Vec_Int_t * Gia_ManCorrCreateRemapping(Gia_Man_t *p)
Definition: cecCorr.c:362
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
int Cec_ManResimulateCounterExamplesComb ( Cec_ManSim_t pSim,
Vec_Int_t vCexStore 
)

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

Synopsis [Resimulates counter-examples derived by the SAT solver.]

Description []

SideEffects []

SeeAlso []

Definition at line 583 of file cecCorr.c.

584 {
585  Vec_Ptr_t * vSimInfo;
586  int RetValue = 0, iStart = 0;
587  Gia_ManCreateValueRefs( pSim->pAig );
588  pSim->pPars->nFrames = 1;
589  vSimInfo = Vec_PtrAllocSimInfo( Gia_ManCiNum(pSim->pAig), pSim->pPars->nWords );
590  while ( iStart < Vec_IntSize(vCexStore) )
591  {
592  Cec_ManStartSimInfo( vSimInfo, 0 );
593  iStart = Cec_ManLoadCounterExamples( vSimInfo, vCexStore, iStart );
594  RetValue |= Cec_ManSeqResimulate( pSim, vSimInfo );
595  }
596  assert( iStart == Vec_IntSize(vCexStore) );
597  Vec_PtrFree( vSimInfo );
598  return RetValue;
599 }
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
void Cec_ManStartSimInfo(Vec_Ptr_t *vInfo, int nFlops)
Definition: cecCorr.c:292
Gia_Man_t * pAig
Definition: cecInt.h:115
void Gia_ManCreateValueRefs(Gia_Man_t *p)
Definition: giaUtil.c:687
int Cec_ManLoadCounterExamples(Vec_Ptr_t *vInfo, Vec_Int_t *vCexStore, int iStart)
Definition: cecCorr.c:458
static int Gia_ManCiNum(Gia_Man_t *p)
Definition: gia.h:383
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
int nFrames
Definition: cec.h:62
Cec_ParSim_t * pPars
Definition: cecInt.h:116
#define assert(ex)
Definition: util_old.h:213
int nWords
Definition: cec.h:61
int Cec_ManSeqResimulate(Cec_ManSim_t *p, Vec_Ptr_t *vInfo)
Definition: cecSeq.c:137
static Vec_Ptr_t * Vec_PtrAllocSimInfo(int nEntries, int nWords)
Definition: vecPtr.h:929
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
void Cec_ManStartSimInfo ( Vec_Ptr_t vInfo,
int  nFlops 
)

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

Synopsis [Initializes simulation info for lcorr/scorr counter-examples.]

Description []

SideEffects []

SeeAlso []

Definition at line 292 of file cecCorr.c.

293 {
294  unsigned * pInfo;
295  int k, w, nWords;
296  nWords = Vec_PtrReadWordsSimInfo( vInfo );
297  assert( nFlops <= Vec_PtrSize(vInfo) );
298  for ( k = 0; k < nFlops; k++ )
299  {
300  pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
301  for ( w = 0; w < nWords; w++ )
302  pInfo[w] = 0;
303  }
304  for ( k = nFlops; k < Vec_PtrSize(vInfo); k++ )
305  {
306  pInfo = (unsigned *)Vec_PtrEntry( vInfo, k );
307  for ( w = 0; w < nWords; w++ )
308  pInfo[w] = Gia_ManRandom( 0 );
309  }
310 }
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
int nWords
Definition: abcNpn.c:127
unsigned Gia_ManRandom(int fReset)
FUNCTION DEFINITIONS ///.
Definition: giaUtil.c:49
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static int Vec_PtrReadWordsSimInfo(Vec_Ptr_t *p)
Definition: vecPtr.h:952
#define assert(ex)
Definition: util_old.h:213
int Gia_ManCheckRefinements ( Gia_Man_t p,
Vec_Str_t vStatus,
Vec_Int_t vOutputs,
Cec_ManSim_t pSim,
int  fRings 
)

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

Synopsis [Updates equivalence classes by marking those that timed out.]

Description [Returns 1 if all ndoes are proved.]

SideEffects []

SeeAlso []

Definition at line 612 of file cecCorr.c.

613 {
614  int i, status, iRepr, iObj;
615  int Counter = 0;
616  assert( 2 * Vec_StrSize(vStatus) == Vec_IntSize(vOutputs) );
617  Vec_StrForEachEntry( vStatus, status, i )
618  {
619  iRepr = Vec_IntEntry( vOutputs, 2*i );
620  iObj = Vec_IntEntry( vOutputs, 2*i+1 );
621  if ( status == 1 )
622  continue;
623  if ( status == 0 )
624  {
625  if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
626  Counter++;
627 // if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
628 // Abc_Print( 1, "Gia_ManCheckRefinements(): Disproved equivalence (%d,%d) is not refined!\n", iRepr, iObj );
629 // if ( Gia_ObjHasSameRepr(p, iRepr, iObj) )
630 // Cec_ManSimClassRemoveOne( pSim, iObj );
631  continue;
632  }
633  if ( status == -1 )
634  {
635 // if ( !Gia_ObjFailed( p, iObj ) )
636 // Abc_Print( 1, "Gia_ManCheckRefinements(): Failed equivalence is not marked as failed!\n" );
637 // Gia_ObjSetFailed( p, iRepr );
638 // Gia_ObjSetFailed( p, iObj );
639 // if ( fRings )
640 // Cec_ManSimClassRemoveOne( pSim, iRepr );
641  Cec_ManSimClassRemoveOne( pSim, iObj );
642  continue;
643  }
644  }
645 // if ( Counter )
646 // Abc_Print( 1, "Gia_ManCheckRefinements(): Could not refine %d nodes.\n", Counter );
647  return 1;
648 }
#define Vec_StrForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecStr.h:54
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static int Counter
static int Vec_StrSize(Vec_Str_t *p)
Definition: bblif.c:600
static int Gia_ObjHasSameRepr(Gia_Man_t *p, int i, int k)
Definition: gia.h:920
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define assert(ex)
Definition: util_old.h:213
int Cec_ManSimClassRemoveOne(Cec_ManSim_t *p, int i)
Definition: cecClass.c:308
Vec_Int_t* Gia_ManCorrCreateRemapping ( Gia_Man_t p)

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

Synopsis [Collects information about remapping.]

Description []

SideEffects []

SeeAlso []

Definition at line 362 of file cecCorr.c.

363 {
364  Vec_Int_t * vPairs;
365  Gia_Obj_t * pObj, * pRepr;
366  int i;
367  vPairs = Vec_IntAlloc( 100 );
368  Gia_ManForEachRo( p, pObj, i )
369  {
370  // skip ROs without representatives
371  pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
372  if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) )
373 // if ( pRepr == NULL || Gia_ObjIsConst0(pRepr) || Gia_ObjIsFailedPair(p, Gia_ObjId(p, pRepr), Gia_ObjId(p, pObj)) )
374  continue;
375  assert( Gia_ObjIsRo(p, pRepr) );
376 // Abc_Print( 1, "%d -> %d ", Gia_ObjId(p,pObj), Gia_ObjId(p, pRepr) );
377  // remember the pair
378  Vec_IntPush( vPairs, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) );
379  Vec_IntPush( vPairs, i );
380  }
381  return vPairs;
382 }
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static int Gia_ObjIsConst0(Gia_Obj_t *pObj)
Definition: gia.h:430
Definition: gia.h:75
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static int Gia_ObjIsRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:443
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
static Gia_Obj_t * Gia_ObjReprObj(Gia_Man_t *p, int Id)
Definition: gia.h:886
static int Gia_ObjFailed(Gia_Man_t *p, int Id)
Definition: gia.h:900
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
#define assert(ex)
Definition: util_old.h:213
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
static int Gia_ObjCioId(Gia_Obj_t *pObj)
Definition: gia.h:411
void Gia_ManCorrPerformRemapping ( Vec_Int_t vPairs,
Vec_Ptr_t vInfo 
)

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

Synopsis [Remaps simulation info from SRM to the original AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 395 of file cecCorr.c.

396 {
397  unsigned * pInfoObj, * pInfoRepr;
398  int w, i, iObj, iRepr, nWords;
399  nWords = Vec_PtrReadWordsSimInfo( vInfo );
400  Vec_IntForEachEntry( vPairs, iRepr, i )
401  {
402  iObj = Vec_IntEntry( vPairs, ++i );
403  pInfoObj = (unsigned *)Vec_PtrEntry( vInfo, iObj );
404  pInfoRepr = (unsigned *)Vec_PtrEntry( vInfo, iRepr );
405  for ( w = 0; w < nWords; w++ )
406  {
407  assert( pInfoObj[w] == 0 );
408  pInfoObj[w] = pInfoRepr[w];
409  }
410  }
411 }
int nWords
Definition: abcNpn.c:127
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static int Vec_PtrReadWordsSimInfo(Vec_Ptr_t *p)
Definition: vecPtr.h:952
#define assert(ex)
Definition: util_old.h:213
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Gia_Man_t* Gia_ManCorrReduce ( Gia_Man_t p)

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

Synopsis [Reduces AIG using equivalence classes.]

Description []

SideEffects []

SeeAlso []

Definition at line 690 of file cecCorr.c.

691 {
692  Gia_Man_t * pNew;
693  Gia_Obj_t * pObj;
694  int i;
695  Gia_ManSetPhase( p );
696  pNew = Gia_ManStart( Gia_ManObjNum(p) );
697  pNew->pName = Abc_UtilStrsav( p->pName );
698  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
699  Gia_ManFillValue( p );
700  Gia_ManConst0(p)->Value = 0;
701  Gia_ManForEachCi( p, pObj, i )
702  pObj->Value = Gia_ManAppendCi(pNew);
703  Gia_ManHashAlloc( pNew );
704  Gia_ManForEachCo( p, pObj, i )
705  Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
706  Gia_ManForEachCo( p, pObj, i )
707  Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
708  Gia_ManHashStop( pNew );
709  Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
710  return pNew;
711 }
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
void Gia_ManSetRegNum(Gia_Man_t *p, int nRegs)
Definition: giaMan.c:628
Definition: gia.h:75
#define Gia_ManForEachCi(p, pObj, i)
Definition: gia.h:1016
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
char * pName
Definition: gia.h:97
char * pSpec
Definition: gia.h:98
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
void Gia_ManFillValue(Gia_Man_t *p)
Definition: giaUtil.c:328
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
void Gia_ManCorrReduce_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: cecCorr.c:662
Definition: gia.h:95
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
void Gia_ManSetPhase(Gia_Man_t *p)
Definition: giaUtil.c:379
unsigned Value
Definition: gia.h:87
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
void Gia_ManCorrReduce_rec ( Gia_Man_t pNew,
Gia_Man_t p,
Gia_Obj_t pObj 
)

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

Synopsis [Duplicates the AIG in the DFS order.]

Description []

SideEffects []

SeeAlso []

Definition at line 662 of file cecCorr.c.

663 {
664  Gia_Obj_t * pRepr;
665  if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
666  {
667  Gia_ManCorrReduce_rec( pNew, p, pRepr );
668  pObj->Value = Abc_LitNotCond( pRepr->Value, Gia_ObjPhaseReal(pRepr) ^ Gia_ObjPhaseReal(pObj) );
669  return;
670  }
671  if ( ~pObj->Value )
672  return;
673  assert( Gia_ObjIsAnd(pObj) );
674  Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin0(pObj) );
675  Gia_ManCorrReduce_rec( pNew, p, Gia_ObjFanin1(pObj) );
676  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
677 }
static int Gia_ObjPhaseReal(Gia_Obj_t *pObj)
Definition: gia.h:416
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Definition: gia.h:75
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
static int Gia_ObjFanin1Copy(Gia_Obj_t *pObj)
Definition: gia.h:482
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
static int Gia_ObjFanin0Copy(Gia_Obj_t *pObj)
Definition: gia.h:481
static Gia_Obj_t * Gia_ObjReprObj(Gia_Man_t *p, int Id)
Definition: gia.h:886
void Gia_ManCorrReduce_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: cecCorr.c:662
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
void Gia_ManCorrRemapSimInfo ( Gia_Man_t p,
Vec_Ptr_t vInfo 
)

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

Synopsis [Remaps simulation info from SRM to the original AIG.]

Description []

SideEffects []

SeeAlso []

Definition at line 323 of file cecCorr.c.

324 {
325  Gia_Obj_t * pObj, * pRepr;
326  unsigned * pInfoObj, * pInfoRepr;
327  int i, w, nWords;
328  nWords = Vec_PtrReadWordsSimInfo( vInfo );
329  Gia_ManForEachRo( p, pObj, i )
330  {
331  // skip ROs without representatives
332  pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
333  if ( pRepr == NULL || Gia_ObjFailed(p, Gia_ObjId(p,pObj)) )
334  continue;
335  pInfoObj = (unsigned *)Vec_PtrEntry( vInfo, i );
336  for ( w = 0; w < nWords; w++ )
337  assert( pInfoObj[w] == 0 );
338  // skip ROs with constant representatives
339  if ( Gia_ObjIsConst0(pRepr) )
340  continue;
341  assert( Gia_ObjIsRo(p, pRepr) );
342 // Abc_Print( 1, "%d -> %d ", i, Gia_ObjId(p, pRepr) );
343  // transfer info from the representative
344  pInfoRepr = (unsigned *)Vec_PtrEntry( vInfo, Gia_ObjCioId(pRepr) - Gia_ManPiNum(p) );
345  for ( w = 0; w < nWords; w++ )
346  pInfoObj[w] = pInfoRepr[w];
347  }
348 // Abc_Print( 1, "\n" );
349 }
static int Gia_ObjIsConst0(Gia_Obj_t *pObj)
Definition: gia.h:430
int nWords
Definition: abcNpn.c:127
Definition: gia.h:75
static int Gia_ObjIsRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:443
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
static void * Vec_PtrEntry(Vec_Ptr_t *p, int i)
Definition: vecPtr.h:362
static Gia_Obj_t * Gia_ObjReprObj(Gia_Man_t *p, int Id)
Definition: gia.h:886
static int Vec_PtrReadWordsSimInfo(Vec_Ptr_t *p)
Definition: vecPtr.h:952
static int Gia_ObjFailed(Gia_Man_t *p, int Id)
Definition: gia.h:900
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
#define assert(ex)
Definition: util_old.h:213
static int Gia_ManPiNum(Gia_Man_t *p)
Definition: gia.h:385
static int Gia_ObjCioId(Gia_Obj_t *pObj)
Definition: gia.h:411
static int Gia_ManCorrSpecReal ( Gia_Man_t pNew,
Gia_Man_t p,
Gia_Obj_t pObj,
int  f,
int  nPrefix 
)
inlinestatic

FUNCTION DEFINITIONS ///.

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

Synopsis [Computes the real value of the literal w/o spec reduction.]

Description []

SideEffects []

SeeAlso []

Definition at line 47 of file cecCorr.c.

48 {
49  if ( Gia_ObjIsAnd(pObj) )
50  {
51  Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f, nPrefix );
52  Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin1(pObj), f, nPrefix );
53  return Gia_ManHashAnd( pNew, Gia_ObjFanin0CopyF(p, f, pObj), Gia_ObjFanin1CopyF(p, f, pObj) );
54  }
55  if ( f == 0 )
56  {
57  assert( Gia_ObjIsRo(p, pObj) );
58  return Gia_ObjCopyF(p, f, pObj);
59  }
60  assert( f && Gia_ObjIsRo(p, pObj) );
61  pObj = Gia_ObjRoToRi( p, pObj );
62  Gia_ManCorrSpecReduce_rec( pNew, p, Gia_ObjFanin0(pObj), f-1, nPrefix );
63  return Gia_ObjFanin0CopyF( p, f-1, pObj );
64 }
static int Gia_ObjFanin1CopyF(Gia_Man_t *p, int f, Gia_Obj_t *pObj)
Definition: gia.h:492
static ABC_NAMESPACE_IMPL_START void Gia_ManCorrSpecReduce_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj, int f, int nPrefix)
DECLARATIONS ///.
Definition: cecCorr.c:77
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
static int Gia_ObjIsRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:443
static Gia_Obj_t * Gia_ObjRoToRi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:446
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
#define assert(ex)
Definition: util_old.h:213
static int Gia_ObjFanin0CopyF(Gia_Man_t *p, int f, Gia_Obj_t *pObj)
Definition: gia.h:491
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
static int Gia_ObjCopyF(Gia_Man_t *p, int f, Gia_Obj_t *pObj)
Definition: gia.h:485
Gia_Man_t* Gia_ManCorrSpecReduce ( Gia_Man_t p,
int  nFrames,
int  fScorr,
Vec_Int_t **  pvOutputs,
int  fRings 
)

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

Synopsis [Derives SRM for signal correspondence.]

Description []

SideEffects []

SeeAlso []

Definition at line 106 of file cecCorr.c.

107 {
108  Gia_Man_t * pNew, * pTemp;
109  Gia_Obj_t * pObj, * pRepr;
110  Vec_Int_t * vXorLits;
111  int f, i, iPrev, iObj, iPrevNew, iObjNew;
112  assert( nFrames > 0 );
113  assert( Gia_ManRegNum(p) > 0 );
114  assert( p->pReprs != NULL );
115  Vec_IntFill( &p->vCopies, (nFrames+fScorr)*Gia_ManObjNum(p), -1 );
116  Gia_ManSetPhase( p );
117  pNew = Gia_ManStart( nFrames * Gia_ManObjNum(p) );
118  pNew->pName = Abc_UtilStrsav( p->pName );
119  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
120  Gia_ManHashAlloc( pNew );
121  Gia_ObjSetCopyF( p, 0, Gia_ManConst0(p), 0 );
122  Gia_ManForEachRo( p, pObj, i )
123  Gia_ObjSetCopyF( p, 0, pObj, Gia_ManAppendCi(pNew) );
124  Gia_ManForEachRo( p, pObj, i )
125  if ( (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
126  Gia_ObjSetCopyF( p, 0, pObj, Gia_ObjCopyF(p, 0, pRepr) );
127  for ( f = 0; f < nFrames+fScorr; f++ )
128  {
129  Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
130  Gia_ManForEachPi( p, pObj, i )
131  Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
132  }
133  *pvOutputs = Vec_IntAlloc( 1000 );
134  vXorLits = Vec_IntAlloc( 1000 );
135  if ( fRings )
136  {
137  Gia_ManForEachObj1( p, pObj, i )
138  {
139  if ( Gia_ObjIsConst( p, i ) )
140  {
141  iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
142  iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) );
143  if ( iObjNew != 0 )
144  {
145  Vec_IntPush( *pvOutputs, 0 );
146  Vec_IntPush( *pvOutputs, i );
147  Vec_IntPush( vXorLits, iObjNew );
148  }
149  }
150  else if ( Gia_ObjIsHead( p, i ) )
151  {
152  iPrev = i;
153  Gia_ClassForEachObj1( p, i, iObj )
154  {
155  iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
156  iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
157  iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
158  iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
159  if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
160  {
161  Vec_IntPush( *pvOutputs, iPrev );
162  Vec_IntPush( *pvOutputs, iObj );
163  Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) );
164  }
165  iPrev = iObj;
166  }
167  iObj = i;
168  iPrevNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iPrev), nFrames, 0 );
169  iObjNew = Gia_ManCorrSpecReal( pNew, p, Gia_ManObj(p, iObj), nFrames, 0 );
170  iPrevNew = Abc_LitNotCond( iPrevNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iPrev)) );
171  iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pObj) ^ Gia_ObjPhase(Gia_ManObj(p, iObj)) );
172  if ( iPrevNew != iObjNew && iPrevNew != 0 && iObjNew != 1 )
173  {
174  Vec_IntPush( *pvOutputs, iPrev );
175  Vec_IntPush( *pvOutputs, iObj );
176  Vec_IntPush( vXorLits, Gia_ManHashAnd(pNew, iPrevNew, Abc_LitNot(iObjNew)) );
177  }
178  }
179  }
180  }
181  else
182  {
183  Gia_ManForEachObj1( p, pObj, i )
184  {
185  pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
186  if ( pRepr == NULL )
187  continue;
188  iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, nFrames, 0 );
189  iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, nFrames, 0 );
190  iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
191  if ( iPrevNew != iObjNew )
192  {
193  Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
194  Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
195  Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
196  }
197  }
198  }
199  Vec_IntForEachEntry( vXorLits, iObjNew, i )
200  Gia_ManAppendCo( pNew, iObjNew );
201  Vec_IntFree( vXorLits );
202  Gia_ManHashStop( pNew );
203  Vec_IntErase( &p->vCopies );
204 //Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
205  pNew = Gia_ManCleanup( pTemp = pNew );
206 //Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) );
207  Gia_ManStop( pTemp );
208  return pNew;
209 }
static void Gia_ObjSetCopyF(Gia_Man_t *p, int f, Gia_Obj_t *pObj, int iLit)
Definition: gia.h:486
static int Gia_ObjPhase(Gia_Obj_t *pObj)
Definition: gia.h:415
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
int Gia_ManHashXor(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:658
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
static int Gia_ObjIsHead(Gia_Man_t *p, int Id)
Definition: gia.h:916
static void Vec_IntErase(Vec_Int_t *p)
Definition: vecInt.h:266
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
for(p=first;p->value< newval;p=p->next)
Definition: gia.h:75
char * pName
Definition: gia.h:97
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static int Gia_ObjIsConst(Gia_Man_t *p, int Id)
Definition: gia.h:915
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
if(last==0)
Definition: sparse_int.h:34
char * pSpec
Definition: gia.h:98
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
#define Gia_ClassForEachObj1(p, i, iObj)
Definition: gia.h:933
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
static Gia_Obj_t * Gia_ObjReprObj(Gia_Man_t *p, int Id)
Definition: gia.h:886
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
Definition: gia.h:95
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
static int Gia_ManCorrSpecReal(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj, int f, int nPrefix)
FUNCTION DEFINITIONS ///.
Definition: cecCorr.c:47
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
Gia_Rpr_t * pReprs
Definition: gia.h:121
#define assert(ex)
Definition: util_old.h:213
void Gia_ManSetPhase(Gia_Man_t *p)
Definition: giaUtil.c:379
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
#define Gia_ManForEachObj1(p, pObj, i)
Definition: gia.h:986
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
Vec_Int_t vCopies
Definition: gia.h:138
static int Gia_ObjCopyF(Gia_Man_t *p, int f, Gia_Obj_t *pObj)
Definition: gia.h:485
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
void Gia_ManCorrSpecReduce_rec ( Gia_Man_t pNew,
Gia_Man_t p,
Gia_Obj_t pObj,
int  f,
int  nPrefix 
)
static

DECLARATIONS ///.

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

FileName [cecCorr.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Combinational equivalence checking.]

Synopsis [Latch/signal correspondence computation.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]

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

Synopsis [Recursively performs speculative reduction for the object.]

Description []

SideEffects []

SeeAlso []

Definition at line 77 of file cecCorr.c.

78 {
79  Gia_Obj_t * pRepr;
80  int iLitNew;
81  if ( ~Gia_ObjCopyF(p, f, pObj) )
82  return;
83  if ( f >= nPrefix && (pRepr = Gia_ObjReprObj(p, Gia_ObjId(p, pObj))) )
84  {
85  Gia_ManCorrSpecReduce_rec( pNew, p, pRepr, f, nPrefix );
86  iLitNew = Abc_LitNotCond( Gia_ObjCopyF(p, f, pRepr), Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
87  Gia_ObjSetCopyF( p, f, pObj, iLitNew );
88  return;
89  }
90  assert( Gia_ObjIsCand(pObj) );
91  iLitNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix );
92  Gia_ObjSetCopyF( p, f, pObj, iLitNew );
93 }
static void Gia_ObjSetCopyF(Gia_Man_t *p, int f, Gia_Obj_t *pObj, int iLit)
Definition: gia.h:486
static int Gia_ObjPhase(Gia_Obj_t *pObj)
Definition: gia.h:415
static int Gia_ObjIsCand(Gia_Obj_t *pObj)
Definition: gia.h:429
static ABC_NAMESPACE_IMPL_START void Gia_ManCorrSpecReduce_rec(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj, int f, int nPrefix)
DECLARATIONS ///.
Definition: cecCorr.c:77
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Definition: gia.h:75
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
static Gia_Obj_t * Gia_ObjReprObj(Gia_Man_t *p, int Id)
Definition: gia.h:886
static int Gia_ManCorrSpecReal(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj, int f, int nPrefix)
FUNCTION DEFINITIONS ///.
Definition: cecCorr.c:47
#define assert(ex)
Definition: util_old.h:213
static int Gia_ObjCopyF(Gia_Man_t *p, int f, Gia_Obj_t *pObj)
Definition: gia.h:485
Gia_Man_t* Gia_ManCorrSpecReduceInit ( Gia_Man_t p,
int  nFrames,
int  nPrefix,
int  fScorr,
Vec_Int_t **  pvOutputs,
int  fRings 
)

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

Synopsis [Derives SRM for signal correspondence.]

Description []

SideEffects []

SeeAlso []

Definition at line 223 of file cecCorr.c.

224 {
225  Gia_Man_t * pNew, * pTemp;
226  Gia_Obj_t * pObj, * pRepr;
227  Vec_Int_t * vXorLits;
228  int f, i, iPrevNew, iObjNew;
229  assert( (!fScorr && nFrames > 1) || (fScorr && nFrames > 0) || nPrefix );
230  assert( Gia_ManRegNum(p) > 0 );
231  assert( p->pReprs != NULL );
232  Vec_IntFill( &p->vCopies, (nFrames+nPrefix+fScorr)*Gia_ManObjNum(p), -1 );
233  Gia_ManSetPhase( p );
234  pNew = Gia_ManStart( (nFrames+nPrefix) * Gia_ManObjNum(p) );
235  pNew->pName = Abc_UtilStrsav( p->pName );
236  pNew->pSpec = Abc_UtilStrsav( p->pSpec );
237  Gia_ManHashAlloc( pNew );
238  Gia_ManForEachRo( p, pObj, i )
239  {
240  Gia_ManAppendCi(pNew);
241  Gia_ObjSetCopyF( p, 0, pObj, 0 );
242  }
243  for ( f = 0; f < nFrames+nPrefix+fScorr; f++ )
244  {
245  Gia_ObjSetCopyF( p, f, Gia_ManConst0(p), 0 );
246  Gia_ManForEachPi( p, pObj, i )
247  Gia_ObjSetCopyF( p, f, pObj, Gia_ManAppendCi(pNew) );
248  }
249  *pvOutputs = Vec_IntAlloc( 1000 );
250  vXorLits = Vec_IntAlloc( 1000 );
251  for ( f = nPrefix; f < nFrames+nPrefix; f++ )
252  {
253  Gia_ManForEachObj1( p, pObj, i )
254  {
255  pRepr = Gia_ObjReprObj( p, Gia_ObjId(p,pObj) );
256  if ( pRepr == NULL )
257  continue;
258  iPrevNew = Gia_ObjIsConst(p, i)? 0 : Gia_ManCorrSpecReal( pNew, p, pRepr, f, nPrefix );
259  iObjNew = Gia_ManCorrSpecReal( pNew, p, pObj, f, nPrefix );
260  iObjNew = Abc_LitNotCond( iObjNew, Gia_ObjPhase(pRepr) ^ Gia_ObjPhase(pObj) );
261  if ( iPrevNew != iObjNew )
262  {
263  Vec_IntPush( *pvOutputs, Gia_ObjId(p, pRepr) );
264  Vec_IntPush( *pvOutputs, Gia_ObjId(p, pObj) );
265  Vec_IntPush( vXorLits, Gia_ManHashXor(pNew, iPrevNew, iObjNew) );
266  }
267  }
268  }
269  Vec_IntForEachEntry( vXorLits, iObjNew, i )
270  Gia_ManAppendCo( pNew, iObjNew );
271  Vec_IntFree( vXorLits );
272  Gia_ManHashStop( pNew );
273  Vec_IntErase( &p->vCopies );
274 //Abc_Print( 1, "Before sweeping = %d\n", Gia_ManAndNum(pNew) );
275  pNew = Gia_ManCleanup( pTemp = pNew );
276 //Abc_Print( 1, "After sweeping = %d\n", Gia_ManAndNum(pNew) );
277  Gia_ManStop( pTemp );
278  return pNew;
279 }
static void Gia_ObjSetCopyF(Gia_Man_t *p, int f, Gia_Obj_t *pObj, int iLit)
Definition: gia.h:486
static int Gia_ObjPhase(Gia_Obj_t *pObj)
Definition: gia.h:415
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
int Gia_ManHashXor(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:658
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
static void Vec_IntErase(Vec_Int_t *p)
Definition: vecInt.h:266
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
for(p=first;p->value< newval;p=p->next)
Definition: gia.h:75
char * pName
Definition: gia.h:97
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static int Gia_ObjIsConst(Gia_Man_t *p, int Id)
Definition: gia.h:915
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
char * pSpec
Definition: gia.h:98
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
static Gia_Obj_t * Gia_ObjReprObj(Gia_Man_t *p, int Id)
Definition: gia.h:886
Definition: gia.h:95
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
static int Gia_ManCorrSpecReal(Gia_Man_t *pNew, Gia_Man_t *p, Gia_Obj_t *pObj, int f, int nPrefix)
FUNCTION DEFINITIONS ///.
Definition: cecCorr.c:47
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
Gia_Rpr_t * pReprs
Definition: gia.h:121
#define assert(ex)
Definition: util_old.h:213
void Gia_ManSetPhase(Gia_Man_t *p)
Definition: giaUtil.c:379
void Gia_ManHashAlloc(Gia_Man_t *p)
Definition: giaHash.c:99
#define Gia_ManForEachObj1(p, pObj, i)
Definition: gia.h:986
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
Vec_Int_t vCopies
Definition: gia.h:138
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387