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

Go to the source code of this file.

Data Structures

struct  Rf2_Obj_t_
 
struct  Rf2_Man_t_
 

Typedefs

typedef
typedefABC_NAMESPACE_IMPL_START
struct Rf2_Obj_t_ 
Rf2_Obj_t
 DECLARATIONS ///. More...
 

Functions

static Rf2_Obj_tRf2_ManObj (Rf2_Man_t *p, Gia_Obj_t *pObj, int f)
 
static Vec_Int_tRf2_ObjVec (Rf2_Man_t *p, Gia_Obj_t *pObj)
 
static unsigned * Rf2_ObjA (Rf2_Man_t *p, Gia_Obj_t *pObj)
 
static unsigned * Rf2_ObjN (Rf2_Man_t *p, Gia_Obj_t *pObj)
 
static void Rf2_ObjClear (Rf2_Man_t *p, Gia_Obj_t *pObj)
 
static void Rf2_ObjStart (Rf2_Man_t *p, Gia_Obj_t *pObj, int i)
 
static void Rf2_ObjCopy (Rf2_Man_t *p, Gia_Obj_t *pObj, Gia_Obj_t *pFanin)
 
static void Rf2_ObjDeriveAnd (Rf2_Man_t *p, Gia_Obj_t *pObj, int One)
 
static void Rf2_ObjPrint (Rf2_Man_t *p, Gia_Obj_t *pRoot)
 
Rf2_Man_tRf2_ManStart (Gia_Man_t *pGia)
 FUNCTION DEFINITIONS ///. More...
 
void Rf2_ManStop (Rf2_Man_t *p, int fProfile)
 
double Rf2_ManMemoryUsage (Rf2_Man_t *p)
 
void Rf2_ManCollect_rec (Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vObjs)
 
void Rf2_ManCollect (Rf2_Man_t *p)
 
int Rf2_ManSensitize (Rf2_Man_t *p)
 
void Rf2_ManVerifyUsingTerSim (Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Int_t *vMap, Vec_Int_t *vObjs, Vec_Int_t *vRes)
 
void Rf2_ManGatherFanins_rec (Rf2_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vFanins, int Depth, int RootId, int fFirst)
 
void Rf2_ManGatherFanins (Rf2_Man_t *p, int Depth)
 
static int Rf2_ManCountPpis (Rf2_Man_t *p)
 
static void Rf2_ManPrintVector (Vec_Int_t *p, int Num)
 
static void Rf2_ManProcessVector (Vec_Int_t *p, int Limit)
 
int Rf2_ManAssignJustIds (Rf2_Man_t *p)
 
static void Rf2_ManPrintVectorSpecial (Rf2_Man_t *p, Vec_Int_t *vVec)
 
Vec_Int_tRf2_ManPropagate (Rf2_Man_t *p, int Limit)
 
void Rf2_ManBounds (Rf2_Man_t *p)
 
Vec_Int_tRf2_ManRefine (Rf2_Man_t *p, Abc_Cex_t *pCex, Vec_Int_t *vMap, int fPropFanout, int fVerbose)
 

Typedef Documentation

typedef typedefABC_NAMESPACE_IMPL_START struct Rf2_Obj_t_ Rf2_Obj_t

DECLARATIONS ///.

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

FileName [absRef2.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Abstraction package.]

Synopsis [Refinement manager to compute all justifying subsets.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

]

Definition at line 75 of file absRefJ.c.

Function Documentation

int Rf2_ManAssignJustIds ( Rf2_Man_t p)

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

Synopsis [Assigns a unique justifification ID for each PPI.]

Description []

SideEffects []

SeeAlso []

Definition at line 636 of file absRefJ.c.

637 {
638  Gia_Obj_t * pObj;
639  int nPpis = Rf2_ManCountPpis( p );
640  int nGroupSize = (nPpis / 30) + (nPpis % 30 > 0);
641  int i, k = 0;
642  Vec_VecClear( p->vGrp2Ppi );
643  Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
644  if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI
645  Vec_VecPushInt( p->vGrp2Ppi, (k++ / nGroupSize), i );
646  printf( "Considering %d PPIs combined into %d groups of size %d.\n", k, (k-1)/nGroupSize+1, nGroupSize );
647  return (k-1)/nGroupSize+1;
648 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Definition: gia.h:75
static void Vec_VecClear(Vec_Vec_t *p)
Definition: vecVec.h:437
static int Rf2_ManCountPpis(Rf2_Man_t *p)
Definition: absRefJ.c:545
static void Vec_VecPushInt(Vec_Vec_t *p, int Level, int Entry)
Definition: vecVec.h:468
if(last==0)
Definition: sparse_int.h:34
static int size
Definition: cuddSign.c:86
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441
void Rf2_ManBounds ( Rf2_Man_t p)

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

Synopsis [Performs justification propagation.]

Description []

SideEffects []

SeeAlso []

Definition at line 792 of file absRefJ.c.

793 {
794  Gia_Obj_t * pObj;
795  int f, i, iBit = p->pCex->nRegs;
796  // init constant
797  pObj = Gia_ManConst0(p->pGia);
798  pObj->fMark0 = 0;
799  Rf2_ObjStart( p, pObj, Vec_IntSize(p->vMap) + Vec_IntSize(p->vObjs) );
800  // iterate through the timeframes
801  for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis )
802  {
803  // initialize frontier values and init justification sets
804  Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
805  {
806  assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) );
807  pObj->fMark0 = Abc_InfoHasBit( p->pCex->pData, iBit + i );
808  Rf2_ObjStart( p, pObj, i );
809  }
810  // propagate internal nodes
811  Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i )
812  {
813  pObj->fMark0 = 0;
814  Rf2_ObjClear( p, pObj );
815  if ( Gia_ObjIsRo(p->pGia, pObj) )
816  {
817  if ( f == 0 )
818  {
819  Rf2_ObjStart( p, pObj, Vec_IntSize(p->vMap) + i );
820  continue;
821  }
822  pObj->fMark0 = Gia_ObjRoToRi(p->pGia, pObj)->fMark0;
823  Rf2_ObjCopy( p, pObj, Gia_ObjRoToRi(p->pGia, pObj) );
824  continue;
825  }
826  if ( Gia_ObjIsCo(pObj) )
827  {
828  pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj));
829  Rf2_ObjCopy( p, pObj, Gia_ObjFanin0(pObj) );
830  continue;
831  }
832  assert( Gia_ObjIsAnd(pObj) );
833  pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
834  if ( pObj->fMark0 == 1 )
835  Rf2_ObjDeriveAnd( p, pObj, 1 );
836  else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 && (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 )
837  Rf2_ObjDeriveAnd( p, pObj, 0 );
838  else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 )
839  Rf2_ObjCopy( p, pObj, Gia_ObjFanin0(pObj) );
840  else
841  Rf2_ObjCopy( p, pObj, Gia_ObjFanin1(pObj) );
842  }
843  }
844  assert( iBit == p->pCex->nBits );
845  if ( Gia_ManPo(p->pGia, 0)->fMark0 != 1 )
846  printf( "Output value is incorrect.\n" );
847 
848  printf( "Bounds: \n" );
849  Rf2_ObjPrint( p, Gia_ManPo(p->pGia, 0) );
850 }
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
static void Rf2_ObjCopy(Rf2_Man_t *p, Gia_Obj_t *pObj, Gia_Obj_t *pFanin)
Definition: absRefJ.c:151
Definition: gia.h:75
static void Rf2_ObjPrint(Rf2_Man_t *p, Gia_Obj_t *pRoot)
Definition: absRefJ.c:178
static void Rf2_ObjStart(Rf2_Man_t *p, Gia_Obj_t *pObj, int i)
Definition: absRefJ.c:139
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 void Rf2_ObjDeriveAnd(Rf2_Man_t *p, Gia_Obj_t *pObj, int One)
Definition: absRefJ.c:156
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
unsigned fMark0
Definition: gia.h:79
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
#define assert(ex)
Definition: util_old.h:213
static void Rf2_ObjClear(Rf2_Man_t *p, Gia_Obj_t *pObj)
Definition: absRefJ.c:135
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
void Rf2_ManCollect ( Rf2_Man_t p)

Definition at line 282 of file absRefJ.c.

283 {
284  Gia_Obj_t * pObj = NULL;
285  int i;
286  // mark const/PIs/PPIs
287  Gia_ManIncrementTravId( p->pGia );
288  Gia_ObjSetTravIdCurrent( p->pGia, Gia_ManConst0(p->pGia) );
289  Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
290  {
291  assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) );
292  Gia_ObjSetTravIdCurrent( p->pGia, pObj );
293  }
294  // collect objects
295  Vec_IntClear( p->vObjs );
296  Rf2_ManCollect_rec( p->pGia, Gia_ManPo(p->pGia, 0), p->vObjs );
297  Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i )
298  if ( Gia_ObjIsRo(p->pGia, pObj) )
299  Rf2_ManCollect_rec( p->pGia, Gia_ObjRoToRi(p->pGia, pObj), p->vObjs );
300  // the last object should be a CO
301  assert( Gia_ObjIsCo(pObj) );
302 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
void Rf2_ManCollect_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vObjs)
Definition: absRefJ.c:266
Definition: gia.h:75
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 void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
if(last==0)
Definition: sparse_int.h:34
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
#define assert(ex)
Definition: util_old.h:213
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition: giaUtil.c:149
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
void Rf2_ManCollect_rec ( Gia_Man_t p,
Gia_Obj_t pObj,
Vec_Int_t vObjs 
)

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

Synopsis [Collect internal objects to be used in value propagation.]

Description [Resulting array vObjs contains RO, AND, PO/RI in a topo order.]

SideEffects []

SeeAlso []

Definition at line 266 of file absRefJ.c.

267 {
268  if ( Gia_ObjIsTravIdCurrent(p, pObj) )
269  return;
270  Gia_ObjSetTravIdCurrent(p, pObj);
271  if ( Gia_ObjIsCo(pObj) )
272  Rf2_ManCollect_rec( p, Gia_ObjFanin0(pObj), vObjs );
273  else if ( Gia_ObjIsAnd(pObj) )
274  {
275  Rf2_ManCollect_rec( p, Gia_ObjFanin0(pObj), vObjs );
276  Rf2_ManCollect_rec( p, Gia_ObjFanin1(pObj), vObjs );
277  }
278  else if ( !Gia_ObjIsRo(p, pObj) )
279  assert( 0 );
280  Vec_IntPush( vObjs, Gia_ObjId(p, pObj) );
281 }
static int Gia_ObjIsTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:533
void Rf2_ManCollect_rec(Gia_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vObjs)
Definition: absRefJ.c:266
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 void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
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 int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
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 Rf2_ManCountPpis ( Rf2_Man_t p)
inlinestatic

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

Synopsis [Sort, make dup- and containment-free, and filter.]

Description []

SideEffects []

SeeAlso []

Definition at line 545 of file absRefJ.c.

546 {
547  Gia_Obj_t * pObj;
548  int i, Counter = 0;
549  Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
550  if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI
551  Counter++;
552  return Counter;
553 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Definition: gia.h:75
if(last==0)
Definition: sparse_int.h:34
static int Counter
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441
void Rf2_ManGatherFanins ( Rf2_Man_t p,
int  Depth 
)

Definition at line 475 of file absRefJ.c.

476 {
477  Vec_Int_t * vUsed;
478  Vec_Int_t * vVec;
479  Gia_Obj_t * pObj;
480  int i, k, Entry;
481  // mark PPIs
482  Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
483  {
484  vVec = Rf2_ObjVec( p, pObj );
485  assert( Vec_IntSize(vVec) == 0 );
486  Vec_IntPush( vVec, 0 );
487  }
488  // collect internal
489  Vec_IntClear( p->vFanins );
490  Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
491  {
492  if ( Gia_ObjIsPi(p->pGia, pObj) )
493  continue;
494  Gia_ManIncrementTravId( p->pGia );
495  Rf2_ManGatherFanins_rec( p, pObj, p->vFanins, Depth, i, 1 );
496  }
497 
498  vUsed = Vec_IntStart( Vec_IntSize(p->vMap) );
499 
500  // evaluate collected
501  printf( "\nMap (%d): ", Vec_IntSize(p->vMap) );
502  Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
503  {
504  vVec = Rf2_ObjVec( p, pObj );
505  if ( Vec_IntSize(vVec) > 1 )
506  printf( "%d=%d ", i, Vec_IntSize(vVec) - 1 );
507  Vec_IntForEachEntryStart( vVec, Entry, k, 1 )
508  Vec_IntAddToEntry( vUsed, Entry, 1 );
509  Vec_IntClear( vVec );
510  }
511  printf( "\n" );
512  // evaluate internal
513  printf( "Int (%d): ", Vec_IntSize(p->vFanins) );
514  Gia_ManForEachObjVec( p->vFanins, p->pGia, pObj, i )
515  {
516  vVec = Rf2_ObjVec( p, pObj );
517  if ( Vec_IntSize(vVec) > 1 )
518  printf( "%d=%d ", i, Vec_IntSize(vVec) );
519  if ( Vec_IntSize(vVec) > 1 )
520  Vec_IntForEachEntry( vVec, Entry, k )
521  Vec_IntAddToEntry( vUsed, Entry, 1 );
522  Vec_IntClear( vVec );
523  }
524  printf( "\n" );
525  // evaluate PPIs
526  Vec_IntForEachEntry( vUsed, Entry, k )
527  printf( "%d ", Entry );
528  printf( "\n" );
529 
530  Vec_IntFree( vUsed );
531 }
static Vec_Int_t * Rf2_ObjVec(Rf2_Man_t *p, Gia_Obj_t *pObj)
Definition: absRefJ.c:121
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Definition: gia.h:75
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
static void Vec_IntAddToEntry(Vec_Int_t *p, int i, int Addition)
Definition: bblif.c:302
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
#define Vec_IntForEachEntryStart(vVec, Entry, i, Start)
Definition: vecInt.h:56
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
void Rf2_ManGatherFanins_rec(Rf2_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vFanins, int Depth, int RootId, int fFirst)
Definition: absRefJ.c:444
#define assert(ex)
Definition: util_old.h:213
void Gia_ManIncrementTravId(Gia_Man_t *p)
Definition: giaUtil.c:149
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441
static int Depth
Definition: dsdProc.c:56
void Rf2_ManGatherFanins_rec ( Rf2_Man_t p,
Gia_Obj_t pObj,
Vec_Int_t vFanins,
int  Depth,
int  RootId,
int  fFirst 
)

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

Synopsis [Computes the refinement for a given counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 444 of file absRefJ.c.

445 {
446  if ( Gia_ObjIsTravIdCurrent(p->pGia, pObj) )
447  return;
448  Gia_ObjSetTravIdCurrent(p->pGia, pObj);
449  if ( pObj->fPhase && !fFirst )
450  {
451  Vec_Int_t * vVec = Rf2_ObjVec( p, pObj );
452 // if ( Vec_IntEntry( vVec, 0 ) == 0 )
453 // return;
454  if ( Vec_IntSize(vVec) == 0 )
455  Vec_IntPush( vFanins, Gia_ObjId(p->pGia, pObj) );
456  Vec_IntPushUnique( vVec, RootId );
457  if ( Depth == 0 )
458  return;
459  }
460  if ( Gia_ObjIsPi(p->pGia, pObj) || Gia_ObjIsConst0(pObj) )
461  return;
462  if ( Gia_ObjIsRo(p->pGia, pObj) )
463  {
464  assert( pObj->fPhase );
465  pObj = Gia_ObjRoToRi(p->pGia, pObj);
466  Rf2_ManGatherFanins_rec( p, Gia_ObjFanin0(pObj), vFanins, Depth - 1, RootId, 0 );
467  }
468  else if ( Gia_ObjIsAnd(pObj) )
469  {
470  Rf2_ManGatherFanins_rec( p, Gia_ObjFanin0(pObj), vFanins, Depth - pObj->fPhase, RootId, 0 );
471  Rf2_ManGatherFanins_rec( p, Gia_ObjFanin1(pObj), vFanins, Depth - pObj->fPhase, RootId, 0 );
472  }
473  else assert( 0 );
474 }
static Vec_Int_t * Rf2_ObjVec(Rf2_Man_t *p, Gia_Obj_t *pObj)
Definition: absRefJ.c:121
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static int Gia_ObjIsTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:533
static int Gia_ObjIsConst0(Gia_Obj_t *pObj)
Definition: gia.h:430
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 void Gia_ObjSetTravIdCurrent(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:531
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
unsigned fPhase
Definition: gia.h:85
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
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
void Rf2_ManGatherFanins_rec(Rf2_Man_t *p, Gia_Obj_t *pObj, Vec_Int_t *vFanins, int Depth, int RootId, int fFirst)
Definition: absRefJ.c:444
#define assert(ex)
Definition: util_old.h:213
static int Vec_IntPushUnique(Vec_Int_t *p, int Entry)
Definition: vecInt.h:832
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441
static int Depth
Definition: dsdProc.c:56
double Rf2_ManMemoryUsage ( Rf2_Man_t p)

Definition at line 249 of file absRefJ.c.

250 {
251  return (double)(sizeof(Rf2_Man_t) + sizeof(Vec_Int_t) * Gia_ManObjNum(p->pGia));
252 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
typedefABC_NAMESPACE_HEADER_START struct Rf2_Man_t_ Rf2_Man_t
INCLUDES ///.
Definition: absRefJ.h:40
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static Rf2_Obj_t* Rf2_ManObj ( Rf2_Man_t p,
Gia_Obj_t pObj,
int  f 
)
inlinestatic

Definition at line 113 of file absRefJ.c.

114 {
115  assert( Gia_ObjIsConst0(pObj) || pObj->Value );
116  assert( (int)pObj->Value < p->nObjsFrame );
117  assert( f >= 0 && f <= p->pCex->iFrame );
118  return p->pObjs + f * p->nObjsFrame + pObj->Value;
119 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Gia_ObjIsConst0(Gia_Obj_t *pObj)
Definition: gia.h:430
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
static void Rf2_ManPrintVector ( Vec_Int_t p,
int  Num 
)
inlinestatic

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

Synopsis [Sort, make dup- and containment-free, and filter.]

Description []

SideEffects []

SeeAlso []

Definition at line 566 of file absRefJ.c.

567 {
568  int i, k, Entry;
569  Vec_IntForEachEntry( p, Entry, i )
570  {
571  for ( k = 0; k < Num; k++ )
572  printf( "%c", '0' + ((Entry>>k) & 1) );
573  printf( "\n" );
574  }
575 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
static void Rf2_ManPrintVectorSpecial ( Rf2_Man_t p,
Vec_Int_t vVec 
)
inlinestatic

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

Synopsis [Sort, make dup- and containment-free, and filter.]

Description []

SideEffects []

SeeAlso []

Definition at line 661 of file absRefJ.c.

662 {
663  Gia_Obj_t * pObj;
664  int nPpis = Rf2_ManCountPpis( p );
665  int nGroupSize = (nPpis / 30) + (nPpis % 30 > 0);
666  int s, i, k, Entry, Counter;
667 
668  Vec_IntForEachEntry( vVec, Entry, s )
669  {
670  k = 0;
671  Counter = 0;
672  Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
673  {
674  if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI
675  {
676  if ( (Entry >> (k++ / nGroupSize)) & 1 )
677  printf( "1" ), Counter++;
678  else
679  printf( "0" );
680  }
681  else
682  printf( "-" );
683  }
684  printf( " %3d \n", Counter );
685  }
686 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Definition: gia.h:75
static int Rf2_ManCountPpis(Rf2_Man_t *p)
Definition: absRefJ.c:545
static int Counter
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441
static void Rf2_ManProcessVector ( Vec_Int_t p,
int  Limit 
)
inlinestatic

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

Synopsis [Sort, make dup- and containment-free, and filter.]

Description []

SideEffects []

SeeAlso []

Definition at line 588 of file absRefJ.c.

589 {
590 // int Start = Vec_IntSize(p);
591  int Start = 0;
592  int i, j, k, Entry, Entry2;
593 // printf( "%d", Vec_IntSize(p) );
594  if ( Start > 5 )
595  {
596  printf( "Before: \n" );
597  Rf2_ManPrintVector( p, 31 );
598  }
599 
600  k = 0;
601  Vec_IntForEachEntry( p, Entry, i )
602  if ( Gia_WordCountOnes((unsigned)Entry) <= Limit )
603  Vec_IntWriteEntry( p, k++, Entry );
604  Vec_IntShrink( p, k );
605  Vec_IntSort( p, 0 );
606  k = 0;
607  Vec_IntForEachEntry( p, Entry, i )
608  {
609  Vec_IntForEachEntryStop( p, Entry2, j, i )
610  if ( (Entry2 & Entry) == Entry2 ) // Entry2 is a subset of Entry
611  break;
612  if ( j == i ) // Entry is not contained in any Entry2
613  Vec_IntWriteEntry( p, k++, Entry );
614  }
615  Vec_IntShrink( p, k );
616 // printf( "->%d ", Vec_IntSize(p) );
617  if ( Start > 5 )
618  {
619  printf( "After: \n" );
620  Rf2_ManPrintVector( p, 31 );
621  k = 0;
622  }
623 }
#define Vec_IntForEachEntryStop(vVec, Entry, i, Stop)
Definition: vecInt.h:58
static void Rf2_ManPrintVector(Vec_Int_t *p, int Num)
Definition: absRefJ.c:566
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Gia_WordCountOnes(unsigned uWord)
Definition: gia.h:313
static void Vec_IntSort(Vec_Int_t *p, int fReverse)
Definition: vecInt.h:1293
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
if(last==0)
Definition: sparse_int.h:34
static void Vec_IntShrink(Vec_Int_t *p, int nSizeNew)
Definition: bblif.c:435
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Vec_Int_t* Rf2_ManPropagate ( Rf2_Man_t p,
int  Limit 
)

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

Synopsis [Performs justification propagation.]

Description []

SideEffects []

SeeAlso []

Definition at line 699 of file absRefJ.c.

700 {
701  Vec_Int_t * vVec, * vVec0, * vVec1;
702  Gia_Obj_t * pObj;
703  int f, i, k, j, Entry, Entry2, iBit = p->pCex->nRegs;
704  // init constant
705  pObj = Gia_ManConst0(p->pGia);
706  pObj->fMark0 = 0;
707  Vec_IntFill( Rf2_ObjVec(p, pObj), 1, 0 );
708  // iterate through the timeframes
709  for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis )
710  {
711  // initialize frontier values and init justification sets
712  Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
713  {
714  assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) );
715  pObj->fMark0 = Abc_InfoHasBit( p->pCex->pData, iBit + i );
716  Vec_IntFill( Rf2_ObjVec(p, pObj), 1, 0 );
717  }
718  // assign justification sets for PPis
719  Vec_VecForEachLevelInt( p->vGrp2Ppi, vVec, i )
720  Vec_IntForEachEntry( vVec, Entry, k )
721  {
722  assert( i < 31 );
723  pObj = Gia_ManObj( p->pGia, Vec_IntEntry(p->vMap, Entry) );
724  assert( Vec_IntSize(Rf2_ObjVec(p, pObj)) == 1 );
725  Vec_IntAddToEntry( Rf2_ObjVec(p, pObj), 0, (1 << i) );
726  }
727  // propagate internal nodes
728  Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i )
729  {
730  pObj->fMark0 = 0;
731  vVec = Rf2_ObjVec(p, pObj);
732  Vec_IntClear( vVec );
733  if ( Gia_ObjIsRo(p->pGia, pObj) )
734  {
735  if ( f == 0 )
736  {
737  Vec_IntPush( vVec, 0 );
738  continue;
739  }
740  pObj->fMark0 = Gia_ObjRoToRi(p->pGia, pObj)->fMark0;
741  vVec0 = Rf2_ObjVec( p, Gia_ObjRoToRi(p->pGia, pObj) );
742  Vec_IntAppend( vVec, vVec0 );
743  continue;
744  }
745  if ( Gia_ObjIsCo(pObj) )
746  {
747  pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj));
748  vVec0 = Rf2_ObjVec( p, Gia_ObjFanin0(pObj) );
749  Vec_IntAppend( vVec, vVec0 );
750  continue;
751  }
752  assert( Gia_ObjIsAnd(pObj) );
753  vVec0 = Rf2_ObjVec(p, Gia_ObjFanin0(pObj));
754  vVec1 = Rf2_ObjVec(p, Gia_ObjFanin1(pObj));
755  pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
756  if ( pObj->fMark0 == 1 )
757  {
758  Vec_IntForEachEntry( vVec0, Entry, k )
759  Vec_IntForEachEntry( vVec1, Entry2, j )
760  Vec_IntPush( vVec, Entry | Entry2 );
761  Rf2_ManProcessVector( vVec, Limit );
762  }
763  else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 && (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 )
764  {
765  Vec_IntAppend( vVec, vVec0 );
766  Vec_IntAppend( vVec, vVec1 );
767  Rf2_ManProcessVector( vVec, Limit );
768  }
769  else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 )
770  Vec_IntAppend( vVec, vVec0 );
771  else
772  Vec_IntAppend( vVec, vVec1 );
773  }
774  }
775  assert( iBit == p->pCex->nBits );
776  if ( Gia_ManPo(p->pGia, 0)->fMark0 != 1 )
777  printf( "Output value is incorrect.\n" );
778  return Rf2_ObjVec(p, Gia_ManPo(p->pGia, 0));
779 }
static Vec_Int_t * Rf2_ObjVec(Rf2_Man_t *p, Gia_Obj_t *pObj)
Definition: absRefJ.c:121
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
#define Vec_VecForEachLevelInt(vGlob, vVec, i)
Definition: vecVec.h:71
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Definition: gia.h:75
static void Rf2_ManProcessVector(Vec_Int_t *p, int Limit)
Definition: absRefJ.c:588
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
static void Vec_IntAddToEntry(Vec_Int_t *p, int i, int Addition)
Definition: bblif.c:302
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 Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
if(last==0)
Definition: sparse_int.h:34
else
Definition: sparse_int.h:55
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static void Vec_IntAppend(Vec_Int_t *vVec1, Vec_Int_t *vVec2)
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
unsigned fMark0
Definition: gia.h:79
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
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_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Vec_Int_t* Rf2_ManRefine ( Rf2_Man_t p,
Abc_Cex_t pCex,
Vec_Int_t vMap,
int  fPropFanout,
int  fVerbose 
)

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

Synopsis [Computes the refinement for a given counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 863 of file absRefJ.c.

864 {
865  Vec_Int_t * vJusts;
866 // Vec_Int_t * vSelected = Vec_IntAlloc( 100 );
867  Vec_Int_t * vSelected = NULL;
868  clock_t clk, clk2 = clock();
869  int nGroups;
870  p->nCalls++;
871  // initialize
872  p->pCex = pCex;
873  p->vMap = vMap;
874  p->fPropFanout = fPropFanout;
875  p->fVerbose = fVerbose;
876  // collects used objects
877  Rf2_ManCollect( p );
878  // collect reconvergence points
879 // Rf2_ManGatherFanins( p, 2 );
880  // propagate justification IDs
881  nGroups = Rf2_ManAssignJustIds( p );
882  vJusts = Rf2_ManPropagate( p, 32 );
883 
884 // printf( "\n" );
885 // Rf2_ManPrintVector( vJusts, nGroups );
886  Rf2_ManPrintVectorSpecial( p, vJusts );
887  if ( Vec_IntSize(vJusts) == 0 )
888  {
889  printf( "Empty set of justifying subsets.\n" );
890  return NULL;
891  }
892 
893 // p->nMapWords = Abc_BitWordNum( Vec_IntSize(p->vMap) + Vec_IntSize(p->vObjs) + 1 ); // Map + Flops + Const
894 // Rf2_ManBounds( p );
895 
896  // select the result
897 // Abc_PrintTime( 1, "Time", clock() - clk2 );
898 
899  // verify (empty) refinement
900  clk = clock();
901 // Rf2_ManVerifyUsingTerSim( p->pGia, p->pCex, p->vMap, p->vObjs, vSelected );
902 // Vec_IntUniqify( vSelected );
903 // Vec_IntReverseOrder( vSelected );
904  p->timeVer += clock() - clk;
905  p->timeTotal += clock() - clk2;
906 // p->nRefines += Vec_IntSize(vSelected);
907  return vSelected;
908 }
void Rf2_ManCollect(Rf2_Man_t *p)
Definition: absRefJ.c:282
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
int Rf2_ManAssignJustIds(Rf2_Man_t *p)
Definition: absRefJ.c:636
Vec_Int_t * Rf2_ManPropagate(Rf2_Man_t *p, int Limit)
Definition: absRefJ.c:699
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
static void Rf2_ManPrintVectorSpecial(Rf2_Man_t *p, Vec_Int_t *vVec)
Definition: absRefJ.c:661
int Rf2_ManSensitize ( Rf2_Man_t p)

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

Synopsis [Performs sensitization analysis.]

Description []

SideEffects []

SeeAlso []

Definition at line 315 of file absRefJ.c.

316 {
317  Rf2_Obj_t * pRnm, * pRnm0, * pRnm1;
318  Gia_Obj_t * pObj;
319  int f, i, iBit = p->pCex->nRegs;
320  // const0 is initialized automatically in all timeframes
321  for ( f = 0; f <= p->pCex->iFrame; f++, iBit += p->pCex->nPis )
322  {
323  Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
324  {
325  assert( Gia_ObjIsCi(pObj) || Gia_ObjIsAnd(pObj) );
326  pRnm = Rf2_ManObj( p, pObj, f );
327  pRnm->Value = Abc_InfoHasBit( p->pCex->pData, iBit + i );
328  if ( !Gia_ObjIsPi(p->pGia, pObj) ) // this is PPI
329  {
330  assert( pObj->Value > 0 );
331  pRnm->Prio = pObj->Value;
332  pRnm->fPPi = 1;
333  }
334  }
335  Gia_ManForEachObjVec( p->vObjs, p->pGia, pObj, i )
336  {
337  assert( Gia_ObjIsRo(p->pGia, pObj) || Gia_ObjIsAnd(pObj) || Gia_ObjIsCo(pObj) );
338  pRnm = Rf2_ManObj( p, pObj, f );
339  assert( !pRnm->fPPi );
340  if ( Gia_ObjIsRo(p->pGia, pObj) )
341  {
342  if ( f == 0 )
343  continue;
344  pRnm0 = Rf2_ManObj( p, Gia_ObjRoToRi(p->pGia, pObj), f-1 );
345  pRnm->Value = pRnm0->Value;
346  pRnm->Prio = pRnm0->Prio;
347  continue;
348  }
349  if ( Gia_ObjIsCo(pObj) )
350  {
351  pRnm0 = Rf2_ManObj( p, Gia_ObjFanin0(pObj), f );
352  pRnm->Value = (pRnm0->Value ^ Gia_ObjFaninC0(pObj));
353  pRnm->Prio = pRnm0->Prio;
354  continue;
355  }
356  assert( Gia_ObjIsAnd(pObj) );
357  pRnm0 = Rf2_ManObj( p, Gia_ObjFanin0(pObj), f );
358  pRnm1 = Rf2_ManObj( p, Gia_ObjFanin1(pObj), f );
359  pRnm->Value = (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) & (pRnm1->Value ^ Gia_ObjFaninC1(pObj));
360  if ( pRnm->Value == 1 )
361  pRnm->Prio = Abc_MaxInt( pRnm0->Prio, pRnm1->Prio );
362  else if ( (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) == 0 && (pRnm1->Value ^ Gia_ObjFaninC1(pObj)) == 0 )
363  pRnm->Prio = Abc_MinInt( pRnm0->Prio, pRnm1->Prio ); // choice
364  else if ( (pRnm0->Value ^ Gia_ObjFaninC0(pObj)) == 0 )
365  pRnm->Prio = pRnm0->Prio;
366  else
367  pRnm->Prio = pRnm1->Prio;
368  }
369  }
370  assert( iBit == p->pCex->nBits );
371  pRnm = Rf2_ManObj( p, Gia_ManPo(p->pGia, 0), p->pCex->iFrame );
372  if ( pRnm->Value != 1 )
373  printf( "Output value is incorrect.\n" );
374  return pRnm->Prio;
375 }
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
typedefABC_NAMESPACE_IMPL_START struct Rf2_Obj_t_ Rf2_Obj_t
DECLARATIONS ///.
Definition: absRefJ.c:75
static int Abc_MaxInt(int a, int b)
Definition: abc_global.h:238
Definition: gia.h:75
static int Abc_MinInt(int a, int b)
Definition: abc_global.h:239
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 Rf2_Obj_t * Rf2_ManObj(Rf2_Man_t *p, Gia_Obj_t *pObj, int f)
Definition: absRefJ.c:113
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
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
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441
Rf2_Man_t* Rf2_ManStart ( Gia_Man_t pGia)

FUNCTION DEFINITIONS ///.

MACRO DEFINITIONS ///.

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

Synopsis [Creates a new manager.]

Description []

SideEffects []

SeeAlso []

Definition at line 211 of file absRefJ.c.

212 {
213  Rf2_Man_t * p;
214  assert( Gia_ManPoNum(pGia) == 1 );
215  p = ABC_CALLOC( Rf2_Man_t, 1 );
216  p->pGia = pGia;
217  p->vObjs = Vec_IntAlloc( 1000 );
218  p->vFanins = Vec_IntAlloc( 1000 );
219  p->pvVecs = ABC_CALLOC( Vec_Int_t, Gia_ManObjNum(pGia) );
220  p->vGrp2Ppi = Vec_VecStart( 100 );
221  Gia_ManCleanMark0(pGia);
222  Gia_ManCleanMark1(pGia);
223  return p;
224 }
static int Gia_ManPoNum(Gia_Man_t *p)
Definition: gia.h:386
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition: giaUtil.c:215
void Gia_ManCleanMark1(Gia_Man_t *p)
Definition: giaUtil.c:272
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
static Vec_Vec_t * Vec_VecStart(int nSize)
Definition: vecVec.h:168
typedefABC_NAMESPACE_HEADER_START struct Rf2_Man_t_ Rf2_Man_t
INCLUDES ///.
Definition: absRefJ.h:40
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
#define assert(ex)
Definition: util_old.h:213
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
void Rf2_ManStop ( Rf2_Man_t p,
int  fProfile 
)

Definition at line 225 of file absRefJ.c.

226 {
227  if ( !p ) return;
228  // print runtime statistics
229  if ( fProfile && p->nCalls )
230  {
231  double MemGia = sizeof(Gia_Man_t) + sizeof(Gia_Obj_t) * p->pGia->nObjsAlloc + sizeof(int) * p->pGia->nTravIdsAlloc;
232  double MemOther = sizeof(Rf2_Man_t) + sizeof(Rf2_Obj_t) * p->nObjsAlloc + sizeof(int) * Vec_IntCap(p->vObjs);
233  clock_t timeOther = p->timeTotal - p->timeFwd - p->timeBwd - p->timeVer;
234  printf( "Abstraction refinement runtime statistics:\n" );
235  ABC_PRTP( "Sensetization", p->timeFwd, p->timeTotal );
236  ABC_PRTP( "Justification", p->timeBwd, p->timeTotal );
237  ABC_PRTP( "Verification ", p->timeVer, p->timeTotal );
238  ABC_PRTP( "Other ", timeOther, p->timeTotal );
239  ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
240  printf( "Total calls = %d. Average refine = %.1f. GIA mem = %.3f MB. Other mem = %.3f MB.\n",
241  p->nCalls, 1.0*p->nRefines/p->nCalls, MemGia/(1<<20), MemOther/(1<<20) );
242  }
243  Vec_IntFree( p->vObjs );
244  Vec_IntFree( p->vFanins );
245  Vec_VecFree( p->vGrp2Ppi );
246  ABC_FREE( p->pvVecs );
247  ABC_FREE( p );
248 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
abctime timeOther
Definition: llb3Image.c:82
typedefABC_NAMESPACE_IMPL_START struct Rf2_Obj_t_ Rf2_Obj_t
DECLARATIONS ///.
Definition: absRefJ.c:75
static void Vec_VecFree(Vec_Vec_t *p)
Definition: vecVec.h:347
Definition: gia.h:75
#define ABC_PRTP(a, t, T)
Definition: abc_global.h:223
static int Vec_IntCap(Vec_Int_t *p)
Definition: vecInt.h:368
#define ABC_FREE(obj)
Definition: abc_global.h:232
typedefABC_NAMESPACE_HEADER_START struct Rf2_Man_t_ Rf2_Man_t
INCLUDES ///.
Definition: absRefJ.h:40
struct Gia_Man_t_ Gia_Man_t
Definition: gia.h:94
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
void Rf2_ManVerifyUsingTerSim ( Gia_Man_t p,
Abc_Cex_t pCex,
Vec_Int_t vMap,
Vec_Int_t vObjs,
Vec_Int_t vRes 
)

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

Synopsis [Performs refinement.]

Description []

SideEffects []

SeeAlso []

Definition at line 390 of file absRefJ.c.

391 {
392  Gia_Obj_t * pObj;
393  int i, f, iBit = pCex->nRegs;
395  for ( f = 0; f <= pCex->iFrame; f++, iBit += pCex->nPis )
396  {
397  Gia_ManForEachObjVec( vMap, p, pObj, i )
398  {
399  pObj->Value = Abc_InfoHasBit( pCex->pData, iBit + i );
400  if ( !Gia_ObjIsPi(p, pObj) )
401  Gia_ObjTerSimSetX( pObj );
402  else if ( pObj->Value )
403  Gia_ObjTerSimSet1( pObj );
404  else
405  Gia_ObjTerSimSet0( pObj );
406  }
407  Gia_ManForEachObjVec( vRes, p, pObj, i ) // vRes is subset of vMap
408  {
409  if ( pObj->Value )
410  Gia_ObjTerSimSet1( pObj );
411  else
412  Gia_ObjTerSimSet0( pObj );
413  }
414  Gia_ManForEachObjVec( vObjs, p, pObj, i )
415  {
416  if ( Gia_ObjIsCo(pObj) )
417  Gia_ObjTerSimCo( pObj );
418  else if ( Gia_ObjIsAnd(pObj) )
419  Gia_ObjTerSimAnd( pObj );
420  else if ( f == 0 )
421  Gia_ObjTerSimSet0( pObj );
422  else
423  Gia_ObjTerSimRo( p, pObj );
424  }
425  }
426  Gia_ManForEachObjVec( vMap, p, pObj, i )
427  pObj->Value = 0;
428  pObj = Gia_ManPo( p, 0 );
429  if ( !Gia_ObjTerSimGet1(pObj) )
430  Abc_Print( 1, "\nRefinement verification has failed!!!\n" );
431 }
static void Gia_ObjTerSimCo(Gia_Obj_t *pObj)
Definition: gia.h:797
static void Gia_ObjTerSimRo(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:808
static void Gia_ObjTerSimSet0(Gia_Obj_t *pObj)
Definition: gia.h:770
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
Definition: gia.h:75
if(last==0)
Definition: sparse_int.h:34
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
static int Gia_ObjTerSimGet1(Gia_Obj_t *pObj)
Definition: gia.h:776
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
static void Gia_ObjTerSimSet1(Gia_Obj_t *pObj)
Definition: gia.h:771
unsigned Value
Definition: gia.h:87
static void Gia_ObjTerSimSetX(Gia_Obj_t *pObj)
Definition: gia.h:772
static void Gia_ObjTerSimAnd(Gia_Obj_t *pObj)
Definition: gia.h:785
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441
static unsigned* Rf2_ObjA ( Rf2_Man_t p,
Gia_Obj_t pObj 
)
inlinestatic

Definition at line 127 of file absRefJ.c.

128 {
129  return (unsigned *)Vec_IntArray(Rf2_ObjVec(p, pObj));
130 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
static Vec_Int_t * Rf2_ObjVec(Rf2_Man_t *p, Gia_Obj_t *pObj)
Definition: absRefJ.c:121
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static void Rf2_ObjClear ( Rf2_Man_t p,
Gia_Obj_t pObj 
)
inlinestatic

Definition at line 135 of file absRefJ.c.

136 {
137  Vec_IntFill( Rf2_ObjVec(p, pObj), 2*p->nMapWords, 0 );
138 }
static Vec_Int_t * Rf2_ObjVec(Rf2_Man_t *p, Gia_Obj_t *pObj)
Definition: absRefJ.c:121
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static void Vec_IntFill(Vec_Int_t *p, int nSize, int Fill)
Definition: bblif.c:356
static void Rf2_ObjCopy ( Rf2_Man_t p,
Gia_Obj_t pObj,
Gia_Obj_t pFanin 
)
inlinestatic

Definition at line 151 of file absRefJ.c.

152 {
153  assert( Vec_IntSize(Rf2_ObjVec(p, pObj)) == 2*p->nMapWords );
154  memcpy( Rf2_ObjA(p, pObj), Rf2_ObjA(p, pFanin), sizeof(unsigned) * 2 * p->nMapWords );
155 }
static Vec_Int_t * Rf2_ObjVec(Rf2_Man_t *p, Gia_Obj_t *pObj)
Definition: absRefJ.c:121
static Llb_Mgr_t * p
Definition: llb3Image.c:950
char * memcpy()
static unsigned * Rf2_ObjA(Rf2_Man_t *p, Gia_Obj_t *pObj)
Definition: absRefJ.c:127
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define assert(ex)
Definition: util_old.h:213
static void Rf2_ObjDeriveAnd ( Rf2_Man_t p,
Gia_Obj_t pObj,
int  One 
)
inlinestatic

Definition at line 156 of file absRefJ.c.

157 {
158  unsigned * pInfo, * pInfo0, * pInfo1;
159  int i;
160  assert( Gia_ObjIsAnd(pObj) );
161  assert( One == (int)pObj->fMark0 );
162  assert( One == (int)(Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) );
163  assert( One == (int)(Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) );
164  assert( Vec_IntSize(Rf2_ObjVec(p, pObj)) == 2*p->nMapWords );
165 
166  pInfo = Rf2_ObjA( p, pObj );
167  pInfo0 = Rf2_ObjA( p, Gia_ObjFanin0(pObj) );
168  pInfo1 = Rf2_ObjA( p, Gia_ObjFanin1(pObj) );
169  for ( i = 0; i < p->nMapWords; i++ )
170  pInfo[i] = One ? (pInfo0[i] & pInfo1[i]) : (pInfo0[i] | pInfo1[i]);
171 
172  pInfo = Rf2_ObjN( p, pObj );
173  pInfo0 = Rf2_ObjN( p, Gia_ObjFanin0(pObj) );
174  pInfo1 = Rf2_ObjN( p, Gia_ObjFanin1(pObj) );
175  for ( i = 0; i < p->nMapWords; i++ )
176  pInfo[i] = One ? (pInfo0[i] | pInfo1[i]) : (pInfo0[i] & pInfo1[i]);
177 }
static Vec_Int_t * Rf2_ObjVec(Rf2_Man_t *p, Gia_Obj_t *pObj)
Definition: absRefJ.c:121
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
static unsigned * Rf2_ObjN(Rf2_Man_t *p, Gia_Obj_t *pObj)
Definition: absRefJ.c:131
static unsigned * Rf2_ObjA(Rf2_Man_t *p, Gia_Obj_t *pObj)
Definition: absRefJ.c:127
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
unsigned fMark0
Definition: gia.h:79
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_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
static unsigned* Rf2_ObjN ( Rf2_Man_t p,
Gia_Obj_t pObj 
)
inlinestatic

Definition at line 131 of file absRefJ.c.

132 {
133  return (unsigned *)Vec_IntArray(Rf2_ObjVec(p, pObj)) + p->nMapWords;
134 }
static int * Vec_IntArray(Vec_Int_t *p)
Definition: vecInt.h:328
static Vec_Int_t * Rf2_ObjVec(Rf2_Man_t *p, Gia_Obj_t *pObj)
Definition: absRefJ.c:121
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static void Rf2_ObjPrint ( Rf2_Man_t p,
Gia_Obj_t pRoot 
)
inlinestatic

Definition at line 178 of file absRefJ.c.

179 {
180  Gia_Obj_t * pObj;
181  unsigned * pInfo;
182  int i;
183  pInfo = Rf2_ObjA( p, pRoot );
184  Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
185  if ( !Gia_ObjIsPi(p->pGia, pObj) )
186  printf( "%d", Abc_InfoHasBit(pInfo, i) );
187  printf( "\n" );
188  pInfo = Rf2_ObjN( p, pRoot );
189  Gia_ManForEachObjVec( p->vMap, p->pGia, pObj, i )
190  if ( !Gia_ObjIsPi(p->pGia, pObj) )
191  printf( "%d", !Abc_InfoHasBit(pInfo, i) );
192  printf( "\n" );
193 
194 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Definition: gia.h:75
static unsigned * Rf2_ObjN(Rf2_Man_t *p, Gia_Obj_t *pObj)
Definition: absRefJ.c:131
if(last==0)
Definition: sparse_int.h:34
static unsigned * Rf2_ObjA(Rf2_Man_t *p, Gia_Obj_t *pObj)
Definition: absRefJ.c:127
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition: gia.h:988
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441
static void Rf2_ObjStart ( Rf2_Man_t p,
Gia_Obj_t pObj,
int  i 
)
inlinestatic

Definition at line 139 of file absRefJ.c.

140 {
141  Vec_Int_t * vVec = Rf2_ObjVec(p, pObj);
142  int w;
143  Vec_IntClear( vVec );
144  for ( w = 0; w < p->nMapWords; w++ )
145  Vec_IntPush( vVec, 0 );
146  for ( w = 0; w < p->nMapWords; w++ )
147  Vec_IntPush( vVec, ~0 );
148  Abc_InfoSetBit( Rf2_ObjA(p, pObj), i );
149  Abc_InfoXorBit( Rf2_ObjN(p, pObj), i );
150 }
static Vec_Int_t * Rf2_ObjVec(Rf2_Man_t *p, Gia_Obj_t *pObj)
Definition: absRefJ.c:121
static Llb_Mgr_t * p
Definition: llb3Image.c:950
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
static void Abc_InfoXorBit(unsigned *p, int i)
Definition: abc_global.h:260
static unsigned * Rf2_ObjN(Rf2_Man_t *p, Gia_Obj_t *pObj)
Definition: absRefJ.c:131
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static unsigned * Rf2_ObjA(Rf2_Man_t *p, Gia_Obj_t *pObj)
Definition: absRefJ.c:127
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
static void Vec_IntClear(Vec_Int_t *p)
Definition: bblif.c:452
static Vec_Int_t* Rf2_ObjVec ( Rf2_Man_t p,
Gia_Obj_t pObj 
)
inlinestatic

Definition at line 121 of file absRefJ.c.

122 {
123  return p->pvVecs + Gia_ObjId(p->pGia, pObj);
124 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410