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

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START
Aig_Man_t
Saig_ManDupOrpos (Aig_Man_t *pAig)
 DECLARATIONS ///. More...
 
Aig_Man_tSaig_ManCreateEquivMiter (Aig_Man_t *pAig, Vec_Int_t *vPairs)
 
Aig_Man_tSaig_ManTrimPis (Aig_Man_t *p)
 
Aig_Obj_tSaig_ManAbstractionDfs_rec (Aig_Man_t *pNew, Aig_Obj_t *pObj)
 
Aig_Man_tSaig_ManDupAbstraction (Aig_Man_t *p, Vec_Int_t *vFlops)
 
int Saig_ManVerifyCex (Aig_Man_t *pAig, Abc_Cex_t *p)
 
int Saig_ManVerifyCexNoClear (Aig_Man_t *pAig, Abc_Cex_t *p)
 
Vec_Int_tSaig_ManReturnFailingState (Aig_Man_t *pAig, Abc_Cex_t *p, int fNextOne)
 
Abc_Cex_tSaig_ManExtendCex (Aig_Man_t *pAig, Abc_Cex_t *p)
 
int Saig_ManFindFailedPoCex (Aig_Man_t *pAig, Abc_Cex_t *p)
 
Aig_Man_tSaig_ManDupWithPhase (Aig_Man_t *pAig, Vec_Int_t *vInit)
 
void Saig_ManDupCones_rec (Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vNodes, Vec_Ptr_t *vRoots)
 
Aig_Man_tSaig_ManDupCones (Aig_Man_t *pAig, int *pPos, int nPos)
 

Function Documentation

Aig_Obj_t* Saig_ManAbstractionDfs_rec ( Aig_Man_t pNew,
Aig_Obj_t pObj 
)

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

Synopsis [Duplicates the AIG manager recursively.]

Description []

SideEffects []

SeeAlso []

Definition at line 185 of file saigDup.c.

186 {
187  if ( pObj->pData )
188  return (Aig_Obj_t *)pObj->pData;
191  return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ));
192 }
void * pData
Definition: aig.h:87
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Definition: aig.h:69
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
Aig_Obj_t * Saig_ManAbstractionDfs_rec(Aig_Man_t *pNew, Aig_Obj_t *pObj)
Definition: saigDup.c:185
Aig_Man_t* Saig_ManCreateEquivMiter ( Aig_Man_t pAig,
Vec_Int_t vPairs 
)

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

Synopsis [Duplicates while ORing the POs of sequential circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 91 of file saigDup.c.

92 {
93  Aig_Man_t * pAigNew;
94  Aig_Obj_t * pObj, * pObj2, * pMiter;
95  int i;
96  if ( pAig->nConstrs > 0 )
97  {
98  printf( "The AIG manager should have no constraints.\n" );
99  return NULL;
100  }
101  // start the new manager
102  pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
103  pAigNew->pName = Abc_UtilStrsav( pAig->pName );
104  pAigNew->nConstrs = pAig->nConstrs;
105  // map the constant node
106  Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
107  // create variables for PIs
108  Aig_ManForEachCi( pAig, pObj, i )
109  pObj->pData = Aig_ObjCreateCi( pAigNew );
110  // add internal nodes of this frame
111  Aig_ManForEachNode( pAig, pObj, i )
112  pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
113  // create POs
114  assert( Vec_IntSize(vPairs) % 2 == 0 );
115  Aig_ManForEachObjVec( vPairs, pAig, pObj, i )
116  {
117  pObj2 = Aig_ManObj( pAig, Vec_IntEntry(vPairs, ++i) );
118  pMiter = Aig_Exor( pAigNew, (Aig_Obj_t *)pObj->pData, (Aig_Obj_t *)pObj2->pData );
119  pMiter = Aig_NotCond( pMiter, pObj->fPhase ^ pObj2->fPhase );
120  Aig_ObjCreateCo( pAigNew, pMiter );
121  }
122  // transfer to register outputs
123  Saig_ManForEachLi( pAig, pObj, i )
124  Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
125  Aig_ManCleanup( pAigNew );
126  Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
127  return pAigNew;
128 }
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
#define Aig_ManForEachObjVec(vIds, p, pObj, i)
Definition: aig.h:408
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
void * pData
Definition: aig.h:87
Aig_Obj_t * Aig_Exor(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:220
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
static Aig_Obj_t * Aig_ManObj(Aig_Man_t *p, int i)
Definition: aig.h:270
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Definition: aig.h:69
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
unsigned int fPhase
Definition: aig.h:78
#define assert(ex)
Definition: util_old.h:213
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
Aig_Man_t* Saig_ManDupAbstraction ( Aig_Man_t p,
Vec_Int_t vFlops 
)

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

Synopsis [Performs abstraction of the AIG to preserve the included flops.]

Description []

SideEffects []

SeeAlso []

Definition at line 205 of file saigDup.c.

206 {
207  Aig_Man_t * pNew;//, * pTemp;
208  Aig_Obj_t * pObj, * pObjLi, * pObjLo;
209  int i, Entry;
210  Aig_ManCleanData( p );
211  // start the new manager
212  pNew = Aig_ManStart( 5000 );
213  pNew->pName = Abc_UtilStrsav( p->pName );
214  // map the constant node
215  Aig_ManConst1(p)->pData = Aig_ManConst1( pNew );
216  // label included flops
217  Vec_IntForEachEntry( vFlops, Entry, i )
218  {
219  pObjLi = Saig_ManLi( p, Entry );
220  assert( pObjLi->fMarkA == 0 );
221  pObjLi->fMarkA = 1;
222  pObjLo = Saig_ManLo( p, Entry );
223  assert( pObjLo->fMarkA == 0 );
224  pObjLo->fMarkA = 1;
225  }
226  // create variables for PIs
227  assert( p->vCiNumsOrig == NULL );
228  pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManCiNum(p) );
229  Aig_ManForEachCi( p, pObj, i )
230  if ( !pObj->fMarkA )
231  {
232  pObj->pData = Aig_ObjCreateCi( pNew );
233  Vec_IntPush( pNew->vCiNumsOrig, i );
234  }
235  // create variables for LOs
236  Aig_ManForEachCi( p, pObj, i )
237  if ( pObj->fMarkA )
238  {
239  pObj->fMarkA = 0;
240  pObj->pData = Aig_ObjCreateCi( pNew );
241  Vec_IntPush( pNew->vCiNumsOrig, i );
242  }
243  // add internal nodes
244 // Aig_ManForEachNode( p, pObj, i )
245 // pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
246  // create POs
247  Saig_ManForEachPo( p, pObj, i )
248  {
250  Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
251  }
252  // create LIs
253  Aig_ManForEachCo( p, pObj, i )
254  if ( pObj->fMarkA )
255  {
256  pObj->fMarkA = 0;
258  Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
259  }
260  Aig_ManSetRegNum( pNew, Vec_IntSize(vFlops) );
261  Aig_ManSeqCleanup( pNew );
262  // remove PIs without fanout
263 // pNew = Saig_ManTrimPis( pTemp = pNew );
264 // Aig_ManStop( pTemp );
265  return pNew;
266 }
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Llb_Mgr_t * p
Definition: llb3Image.c:950
int Aig_ManSeqCleanup(Aig_Man_t *p)
Definition: aigScl.c:158
void * pData
Definition: aig.h:87
static Aig_Obj_t * Saig_ManLo(Aig_Man_t *p, int i)
Definition: saig.h:79
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
unsigned int fMarkA
Definition: aig.h:79
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
if(last==0)
Definition: sparse_int.h:34
static Aig_Obj_t * Saig_ManLi(Aig_Man_t *p, int i)
Definition: saig.h:80
Definition: aig.h:69
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
Aig_Obj_t * Saig_ManAbstractionDfs_rec(Aig_Man_t *pNew, Aig_Obj_t *pObj)
Definition: saigDup.c:185
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
#define assert(ex)
Definition: util_old.h:213
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
void Aig_ManCleanData(Aig_Man_t *p)
Definition: aigUtil.c:205
Aig_Man_t* Saig_ManDupCones ( Aig_Man_t pAig,
int *  pPos,
int  nPos 
)

Definition at line 543 of file saigDup.c.

544 {
545  Aig_Man_t * pAigNew;
546  Vec_Ptr_t * vLeaves, * vNodes, * vRoots;
547  Aig_Obj_t * pObj;
548  int i;
549 
550  // collect initial POs
551  vLeaves = Vec_PtrAlloc( 100 );
552  vNodes = Vec_PtrAlloc( 100 );
553  vRoots = Vec_PtrAlloc( 100 );
554  for ( i = 0; i < nPos; i++ )
555  Vec_PtrPush( vRoots, Aig_ManCo(pAig, pPos[i]) );
556 
557  // mark internal nodes
558  Aig_ManIncrementTravId( pAig );
559  Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
560  Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
561  Saig_ManDupCones_rec( pAig, pObj, vLeaves, vNodes, vRoots );
562 
563  // start the new manager
564  pAigNew = Aig_ManStart( Vec_PtrSize(vNodes) );
565  pAigNew->pName = Abc_UtilStrsav( pAig->pName );
566  // map the constant node
567  Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
568  // create PIs
569  Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
570  pObj->pData = Aig_ObjCreateCi( pAigNew );
571  // create LOs
572  Vec_PtrForEachEntryStart( Aig_Obj_t *, vRoots, pObj, i, nPos )
573  Saig_ObjLiToLo(pAig, pObj)->pData = Aig_ObjCreateCi( pAigNew );
574  // create internal nodes
575  Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
576  pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
577  // create COs
578  Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
579  Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
580  // finalize
581  Aig_ManSetRegNum( pAigNew, Vec_PtrSize(vRoots)-nPos );
582  Vec_PtrFree( vLeaves );
583  Vec_PtrFree( vNodes );
584  Vec_PtrFree( vRoots );
585  return pAigNew;
586 
587 }
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition: vecPtr.h:57
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
void Saig_ManDupCones_rec(Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vNodes, Vec_Ptr_t *vRoots)
Definition: saigDup.c:524
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigUtil.c:44
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
static Aig_Obj_t * Saig_ObjLiToLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:87
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Definition: aig.h:69
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
void Saig_ManDupCones_rec ( Aig_Man_t p,
Aig_Obj_t pObj,
Vec_Ptr_t vLeaves,
Vec_Ptr_t vNodes,
Vec_Ptr_t vRoots 
)

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

Synopsis [Copy an AIG structure related to the selected POs.]

Description []

SideEffects []

SeeAlso []

Definition at line 524 of file saigDup.c.

525 {
526  if ( Aig_ObjIsTravIdCurrent(p, pObj) )
527  return;
528  Aig_ObjSetTravIdCurrent(p, pObj);
529  if ( Aig_ObjIsNode(pObj) )
530  {
531  Saig_ManDupCones_rec( p, Aig_ObjFanin0(pObj), vLeaves, vNodes, vRoots );
532  Saig_ManDupCones_rec( p, Aig_ObjFanin1(pObj), vLeaves, vNodes, vRoots );
533  Vec_PtrPush( vNodes, pObj );
534  }
535  else if ( Aig_ObjIsCo(pObj) )
536  Saig_ManDupCones_rec( p, Aig_ObjFanin0(pObj), vLeaves, vNodes, vRoots );
537  else if ( Saig_ObjIsLo(p, pObj) )
538  Vec_PtrPush( vRoots, Saig_ObjLoToLi(p, pObj) );
539  else if ( Saig_ObjIsPi(p, pObj) )
540  Vec_PtrPush( vLeaves, pObj );
541  else assert( 0 );
542 }
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
static Llb_Mgr_t * p
Definition: llb3Image.c:950
void Saig_ManDupCones_rec(Aig_Man_t *p, Aig_Obj_t *pObj, Vec_Ptr_t *vLeaves, Vec_Ptr_t *vNodes, Vec_Ptr_t *vRoots)
Definition: saigDup.c:524
static int Aig_ObjIsTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:295
static Aig_Obj_t * Saig_ObjLoToLi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:86
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
static void Aig_ObjSetTravIdCurrent(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: aig.h:293
static int Aig_ObjIsNode(Aig_Obj_t *pObj)
Definition: aig.h:280
#define assert(ex)
Definition: util_old.h:213
static int Saig_ObjIsPi(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:82
static int Aig_ObjIsCo(Aig_Obj_t *pObj)
Definition: aig.h:276
ABC_NAMESPACE_IMPL_START Aig_Man_t* Saig_ManDupOrpos ( Aig_Man_t pAig)

DECLARATIONS ///.

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

FileName [saigDup.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Sequential AIG package.]

Synopsis [Various duplication procedures.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

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

Synopsis [Duplicates while ORing the POs of sequential circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file saigDup.c.

46 {
47  Aig_Man_t * pAigNew;
48  Aig_Obj_t * pObj, * pMiter;
49  int i;
50  if ( pAig->nConstrs > 0 )
51  {
52  printf( "The AIG manager should have no constraints.\n" );
53  return NULL;
54  }
55  // start the new manager
56  pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
57  pAigNew->pName = Abc_UtilStrsav( pAig->pName );
58  pAigNew->nConstrs = pAig->nConstrs;
59  // map the constant node
60  Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
61  // create variables for PIs
62  Aig_ManForEachCi( pAig, pObj, i )
63  pObj->pData = Aig_ObjCreateCi( pAigNew );
64  // add internal nodes of this frame
65  Aig_ManForEachNode( pAig, pObj, i )
66  pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
67  // create PO of the circuit
68  pMiter = Aig_ManConst0( pAigNew );
69  Saig_ManForEachPo( pAig, pObj, i )
70  pMiter = Aig_Or( pAigNew, pMiter, Aig_ObjChild0Copy(pObj) );
71  Aig_ObjCreateCo( pAigNew, pMiter );
72  // transfer to register outputs
73  Saig_ManForEachLi( pAig, pObj, i )
74  Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
75  Aig_ManCleanup( pAigNew );
76  Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
77  return pAigNew;
78 }
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
void * pData
Definition: aig.h:87
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
static Aig_Obj_t * Aig_ManConst0(Aig_Man_t *p)
Definition: aig.h:263
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:259
Definition: aig.h:69
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
Aig_Man_t* Saig_ManDupWithPhase ( Aig_Man_t pAig,
Vec_Int_t vInit 
)

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

Synopsis [Duplicates while ORing the POs of sequential circuit.]

Description []

SideEffects []

SeeAlso []

Definition at line 480 of file saigDup.c.

481 {
482  Aig_Man_t * pAigNew;
483  Aig_Obj_t * pObj;
484  int i;
485  assert( Aig_ManRegNum(pAig) <= Vec_IntSize(vInit) );
486  // start the new manager
487  pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
488  pAigNew->pName = Abc_UtilStrsav( pAig->pName );
489  pAigNew->nConstrs = pAig->nConstrs;
490  // map the constant node
491  Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
492  // create variables for PIs
493  Aig_ManForEachCi( pAig, pObj, i )
494  pObj->pData = Aig_ObjCreateCi( pAigNew );
495  // update the flop variables
496  Saig_ManForEachLo( pAig, pObj, i )
497  pObj->pData = Aig_NotCond( (Aig_Obj_t *)pObj->pData, Vec_IntEntry(vInit, i) );
498  // add internal nodes of this frame
499  Aig_ManForEachNode( pAig, pObj, i )
500  pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
501  // transfer to register outputs
502  Saig_ManForEachPo( pAig, pObj, i )
503  Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
504  // update the flop variables
505  Saig_ManForEachLi( pAig, pObj, i )
506  Aig_ObjCreateCo( pAigNew, Aig_NotCond(Aig_ObjChild0Copy(pObj), Vec_IntEntry(vInit, i)) );
507  // finalize
508  Aig_ManCleanup( pAigNew );
509  Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
510  return pAigNew;
511 }
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
void * pData
Definition: aig.h:87
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
static int Aig_ManNodeNum(Aig_Man_t *p)
Definition: aig.h:256
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Definition: aig.h:69
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
#define assert(ex)
Definition: util_old.h:213
static Aig_Obj_t * Aig_NotCond(Aig_Obj_t *p, int c)
Definition: aig.h:248
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
int Aig_ManCleanup(Aig_Man_t *p)
Definition: aigMan.c:265
Abc_Cex_t* Saig_ManExtendCex ( Aig_Man_t pAig,
Abc_Cex_t p 
)

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

Synopsis [Resimulates the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 382 of file saigDup.c.

383 {
384  Abc_Cex_t * pNew;
385  Aig_Obj_t * pObj, * pObjRi, * pObjRo;
386  int RetValue, i, k, iBit = 0;
387  // create new counter-example
388  pNew = Abc_CexAlloc( 0, Aig_ManCiNum(pAig), p->iFrame + 1 );
389  pNew->iPo = p->iPo;
390  pNew->iFrame = p->iFrame;
391  // simulate the AIG
392  Aig_ManCleanMarkB(pAig);
393  Aig_ManConst1(pAig)->fMarkB = 1;
394  Saig_ManForEachLo( pAig, pObj, i )
395  pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
396  for ( i = 0; i <= p->iFrame; i++ )
397  {
398  Saig_ManForEachPi( pAig, pObj, k )
399  pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
400  ///////// write PI+LO values ////////////
401  Aig_ManForEachCi( pAig, pObj, k )
402  if ( pObj->fMarkB )
403  Abc_InfoSetBit(pNew->pData, Aig_ManCiNum(pAig)*i + k);
404  /////////////////////////////////////////
405  Aig_ManForEachNode( pAig, pObj, k )
406  pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
407  (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
408  Aig_ManForEachCo( pAig, pObj, k )
409  pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
410  if ( i == p->iFrame )
411  break;
412  Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
413  pObjRo->fMarkB = pObjRi->fMarkB;
414  }
415  assert( iBit == p->nBits );
416  RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
417  Aig_ManCleanMarkB(pAig);
418  if ( RetValue == 0 )
419  printf( "Saig_ManExtendCex(): The counter-example is invalid!!!\n" );
420  return pNew;
421 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
unsigned int fMarkB
Definition: aig.h:80
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
void Aig_ManCleanMarkB(Aig_Man_t *p)
Definition: aigUtil.c:167
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
Abc_Cex_t * Saig_ManExtendCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition: saigDup.c:382
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
for(p=first;p->value< newval;p=p->next)
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
if(last==0)
Definition: sparse_int.h:34
Definition: aig.h:69
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
#define assert(ex)
Definition: util_old.h:213
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
int Saig_ManFindFailedPoCex ( Aig_Man_t pAig,
Abc_Cex_t p 
)

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

Synopsis [Resimulates the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 434 of file saigDup.c.

435 {
436  Aig_Obj_t * pObj, * pObjRi, * pObjRo;
437  int RetValue, i, k, iBit = 0;
438  Aig_ManCleanMarkB(pAig);
439  Aig_ManConst1(pAig)->fMarkB = 1;
440  Saig_ManForEachLo( pAig, pObj, i )
441  pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
442  for ( i = 0; i <= p->iFrame; i++ )
443  {
444  Saig_ManForEachPi( pAig, pObj, k )
445  pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
446  Aig_ManForEachNode( pAig, pObj, k )
447  pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
448  (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
449  Aig_ManForEachCo( pAig, pObj, k )
450  pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
451  if ( i == p->iFrame )
452  break;
453  Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
454  pObjRo->fMarkB = pObjRi->fMarkB;
455  }
456  assert( iBit == p->nBits );
457  // remember the number of failed output
458  RetValue = -1;
459  Saig_ManForEachPo( pAig, pObj, i )
460  if ( pObj->fMarkB )
461  {
462  RetValue = i;
463  break;
464  }
465  Aig_ManCleanMarkB(pAig);
466  return RetValue;
467 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
unsigned int fMarkB
Definition: aig.h:80
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
void Aig_ManCleanMarkB(Aig_Man_t *p)
Definition: aigUtil.c:167
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
for(p=first;p->value< newval;p=p->next)
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
if(last==0)
Definition: sparse_int.h:34
Definition: aig.h:69
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
#define assert(ex)
Definition: util_old.h:213
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
Vec_Int_t* Saig_ManReturnFailingState ( Aig_Man_t pAig,
Abc_Cex_t p,
int  fNextOne 
)

Definition at line 345 of file saigDup.c.

346 {
347  Aig_Obj_t * pObj;
348  Vec_Int_t * vState;
349  int i, RetValue = Saig_ManVerifyCexNoClear( pAig, p );
350  if ( RetValue == 0 )
351  {
352  Aig_ManCleanMarkB(pAig);
353  printf( "CEX does fail the given sequential miter.\n" );
354  return NULL;
355  }
356  vState = Vec_IntAlloc( Aig_ManRegNum(pAig) );
357  if ( fNextOne )
358  {
359  Saig_ManForEachLi( pAig, pObj, i )
360  Vec_IntPush( vState, pObj->fMarkB );
361  }
362  else
363  {
364  Saig_ManForEachLo( pAig, pObj, i )
365  Vec_IntPush( vState, pObj->fMarkB );
366  }
367  Aig_ManCleanMarkB(pAig);
368  return vState;
369 }
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 Aig_ManCleanMarkB(Aig_Man_t *p)
Definition: aigUtil.c:167
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
else
Definition: sparse_int.h:55
Definition: aig.h:69
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
int Saig_ManVerifyCexNoClear(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition: saigDup.c:318
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Aig_Man_t* Saig_ManTrimPis ( Aig_Man_t p)

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

Synopsis [Trims the model by removing PIs without fanout.]

Description []

SideEffects []

SeeAlso []

Definition at line 141 of file saigDup.c.

142 {
143  Aig_Man_t * pNew;
144  Aig_Obj_t * pObj;
145  int i, fAllPisHaveNoRefs;
146  // check the refs of PIs
147  fAllPisHaveNoRefs = 1;
148  Saig_ManForEachPi( p, pObj, i )
149  if ( pObj->nRefs )
150  fAllPisHaveNoRefs = 0;
151  // start the new manager
152  pNew = Aig_ManStart( Aig_ManObjNum(p) );
153  pNew->pName = Abc_UtilStrsav( p->pName );
154  pNew->nConstrs = p->nConstrs;
155  // start mapping of the CI numbers
156  pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManCiNum(p) );
157  // map const and primary inputs
158  Aig_ManCleanData( p );
159  Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
160  Aig_ManForEachCi( p, pObj, i )
161  if ( fAllPisHaveNoRefs || pObj->nRefs || Saig_ObjIsLo(p, pObj) )
162  {
163  pObj->pData = Aig_ObjCreateCi( pNew );
164  Vec_IntPush( pNew->vCiNumsOrig, Vec_IntEntry(p->vCiNumsOrig, i) );
165  }
166  Aig_ManForEachNode( p, pObj, i )
167  pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
168  Aig_ManForEachCo( p, pObj, i )
169  pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
170  Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
171  return pNew;
172 }
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition: aigObj.c:66
static int Saig_ObjIsLo(Aig_Man_t *p, Aig_Obj_t *pObj)
Definition: saig.h:84
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Aig_ManObjNum(Aig_Man_t *p)
Definition: aig.h:258
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition: aigMan.c:47
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition: aig.h:393
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition: aigObj.c:45
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition: aigOper.c:104
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition: aigMan.c:438
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
if(last==0)
Definition: sparse_int.h:34
static Aig_Obj_t * Aig_ObjChild1Copy(Aig_Obj_t *pObj)
Definition: aig.h:313
Definition: aig.h:69
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
static Aig_Obj_t * Aig_ObjChild0Copy(Aig_Obj_t *pObj)
Definition: aig.h:312
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
void Aig_ManCleanData(Aig_Man_t *p)
Definition: aigUtil.c:205
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
int Saig_ManVerifyCex ( Aig_Man_t pAig,
Abc_Cex_t p 
)

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

Synopsis [Resimulates the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 279 of file saigDup.c.

280 {
281  Aig_Obj_t * pObj, * pObjRi, * pObjRo;
282  int RetValue, i, k, iBit = 0;
283  Aig_ManCleanMarkB(pAig);
284  Aig_ManConst1(pAig)->fMarkB = 1;
285  Saig_ManForEachLo( pAig, pObj, i )
286  pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
287  for ( i = 0; i <= p->iFrame; i++ )
288  {
289  Saig_ManForEachPi( pAig, pObj, k )
290  pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
291  Aig_ManForEachNode( pAig, pObj, k )
292  pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
293  (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
294  Aig_ManForEachCo( pAig, pObj, k )
295  pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
296  if ( i == p->iFrame )
297  break;
298  Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
299  pObjRo->fMarkB = pObjRi->fMarkB;
300  }
301  assert( iBit == p->nBits );
302  RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
303  Aig_ManCleanMarkB(pAig);
304  return RetValue;
305 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
unsigned int fMarkB
Definition: aig.h:80
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
void Aig_ManCleanMarkB(Aig_Man_t *p)
Definition: aigUtil.c:167
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
for(p=first;p->value< newval;p=p->next)
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
if(last==0)
Definition: sparse_int.h:34
Definition: aig.h:69
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
#define assert(ex)
Definition: util_old.h:213
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
int Saig_ManVerifyCexNoClear ( Aig_Man_t pAig,
Abc_Cex_t p 
)

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

Synopsis [Resimulates the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 318 of file saigDup.c.

319 {
320  Aig_Obj_t * pObj, * pObjRi, * pObjRo;
321  int RetValue, i, k, iBit = 0;
322  Aig_ManCleanMarkB(pAig);
323  Aig_ManConst1(pAig)->fMarkB = 1;
324  Saig_ManForEachLo( pAig, pObj, i )
325  pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
326  for ( i = 0; i <= p->iFrame; i++ )
327  {
328  Saig_ManForEachPi( pAig, pObj, k )
329  pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
330  Aig_ManForEachNode( pAig, pObj, k )
331  pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
332  (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
333  Aig_ManForEachCo( pAig, pObj, k )
334  pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
335  if ( i == p->iFrame )
336  break;
337  Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
338  pObjRo->fMarkB = pObjRi->fMarkB;
339  }
340  assert( iBit == p->nBits );
341  RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
342  //Aig_ManCleanMarkB(pAig);
343  return RetValue;
344 }
static Llb_Mgr_t * p
Definition: llb3Image.c:950
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition: saig.h:101
unsigned int fMarkB
Definition: aig.h:80
static Aig_Obj_t * Aig_ObjFanin0(Aig_Obj_t *pObj)
Definition: aig.h:308
void Aig_ManCleanMarkB(Aig_Man_t *p)
Definition: aigUtil.c:167
#define Aig_ManForEachCo(p, pObj, i)
Definition: aig.h:398
static Aig_Obj_t * Aig_ObjFanin1(Aig_Obj_t *pObj)
Definition: aig.h:309
for(p=first;p->value< newval;p=p->next)
#define Aig_ManForEachNode(p, pObj, i)
Definition: aig.h:413
if(last==0)
Definition: sparse_int.h:34
Definition: aig.h:69
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
static int Aig_ObjFaninC0(Aig_Obj_t *pObj)
Definition: aig.h:306
static Aig_Obj_t * Aig_ManConst1(Aig_Man_t *p)
Definition: aig.h:264
static Aig_Obj_t * Aig_ManCo(Aig_Man_t *p, int i)
Definition: aig.h:267
static int Aig_ObjFaninC1(Aig_Obj_t *pObj)
Definition: aig.h:307
#define assert(ex)
Definition: util_old.h:213
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91