ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
saigDup.c File Reference
#include "saig.h"
Include dependency graph for saigDup.c:

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START Aig_Man_t * Saig_ManDupOrpos (Aig_Man_t *pAig)
 DECLARATIONS ///.
 
Aig_Man_t * Saig_ManCreateEquivMiter (Aig_Man_t *pAig, Vec_Int_t *vPairs, int fAddOuts)
 
Aig_Man_t * Saig_ManTrimPis (Aig_Man_t *p)
 
Aig_Obj_t * Saig_ManAbstractionDfs_rec (Aig_Man_t *pNew, Aig_Obj_t *pObj)
 
Aig_Man_t * Saig_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_t * Saig_ManReturnFailingState (Aig_Man_t *pAig, Abc_Cex_t *p, int fNextOne)
 
Abc_Cex_t * Saig_ManExtendCex (Aig_Man_t *pAig, Abc_Cex_t *p)
 
int Saig_ManFindFailedPoCex (Aig_Man_t *pAig, Abc_Cex_t *p)
 
Aig_Man_t * Saig_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_t * Saig_ManDupCones (Aig_Man_t *pAig, int *pPos, int nPos)
 
int Aig_ManVerifyUsingBdds (Aig_Man_t *pInit, Saig_ParBbr_t *pPars)
 
void Bbr_ManSetDefaultParams (Saig_ParBbr_t *p)
 

Function Documentation

◆ Aig_ManVerifyUsingBdds()

int Aig_ManVerifyUsingBdds ( Aig_Man_t * pInit,
Saig_ParBbr_t * pPars )

Definition at line 592 of file saigDup.c.

592{ return 0; }
Here is the caller graph for this function:

◆ Bbr_ManSetDefaultParams()

void Bbr_ManSetDefaultParams ( Saig_ParBbr_t * p)

Definition at line 593 of file saigDup.c.

593{}
Here is the caller graph for this function:

◆ Saig_ManAbstractionDfs_rec()

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 187 of file saigDup.c.

188{
189 if ( pObj->pData )
190 return (Aig_Obj_t *)pObj->pData;
191 Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
192 Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin1(pObj) );
193 return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ));
194}
Aig_And
Aig_Obj_t * Aig_And(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:104
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Saig_ManAbstractionDfs_rec
Aig_Obj_t * Saig_ManAbstractionDfs_rec(Aig_Man_t *pNew, Aig_Obj_t *pObj)
Definition saigDup.c:187
Aig_Obj_t_::pData
void * pData
Definition aig.h:87
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManCreateEquivMiter()

Aig_Man_t * Saig_ManCreateEquivMiter ( Aig_Man_t * pAig,
Vec_Int_t * vPairs,
int fAddOuts )

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 if ( fAddOuts )
124 Saig_ManForEachLi( pAig, pObj, i )
125 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
126 Aig_ManCleanup( pAigNew );
127 if ( fAddOuts )
128 Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
129 return pAigNew;
130}
Aig_ManSetRegNum
void Aig_ManSetRegNum(Aig_Man_t *p, int nRegs)
Definition aigMan.c:438
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
Aig_ObjCreateCo
Aig_Obj_t * Aig_ObjCreateCo(Aig_Man_t *p, Aig_Obj_t *pDriver)
Definition aigObj.c:66
Aig_Exor
Aig_Obj_t * Aig_Exor(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:220
Aig_ManStart
Aig_Man_t * Aig_ManStart(int nNodesMax)
DECLARATIONS ///.
Definition aigMan.c:47
Aig_ManForEachNode
#define Aig_ManForEachNode(p, pObj, i)
Definition aig.h:413
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Aig_ManCleanup
int Aig_ManCleanup(Aig_Man_t *p)
Definition aigMan.c:265
Aig_ObjCreateCi
Aig_Obj_t * Aig_ObjCreateCi(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigObj.c:45
Aig_ManForEachObjVec
#define Aig_ManForEachObjVec(vIds, p, pObj, i)
Definition aig.h:408
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition saig.h:98
Aig_Obj_t_::fPhase
unsigned int fPhase
Definition aig.h:78
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDupAbstraction()

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 207 of file saigDup.c.

208{
209 Aig_Man_t * pNew;//, * pTemp;
210 Aig_Obj_t * pObj, * pObjLi, * pObjLo;
211 int i, Entry;
212 Aig_ManCleanData( p );
213 // start the new manager
214 pNew = Aig_ManStart( 5000 );
215 pNew->pName = Abc_UtilStrsav( p->pName );
216 // map the constant node
217 Aig_ManConst1(p)->pData = Aig_ManConst1( pNew );
218 // label included flops
219 Vec_IntForEachEntry( vFlops, Entry, i )
220 {
221 pObjLi = Saig_ManLi( p, Entry );
222 assert( pObjLi->fMarkA == 0 );
223 pObjLi->fMarkA = 1;
224 pObjLo = Saig_ManLo( p, Entry );
225 assert( pObjLo->fMarkA == 0 );
226 pObjLo->fMarkA = 1;
227 }
228 // create variables for PIs
229 assert( p->vCiNumsOrig == NULL );
230 pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManCiNum(p) );
231 Aig_ManForEachCi( p, pObj, i )
232 if ( !pObj->fMarkA )
233 {
234 pObj->pData = Aig_ObjCreateCi( pNew );
235 Vec_IntPush( pNew->vCiNumsOrig, i );
236 }
237 // create variables for LOs
238 Aig_ManForEachCi( p, pObj, i )
239 if ( pObj->fMarkA )
240 {
241 pObj->fMarkA = 0;
242 pObj->pData = Aig_ObjCreateCi( pNew );
243 Vec_IntPush( pNew->vCiNumsOrig, i );
244 }
245 // add internal nodes
246// Aig_ManForEachNode( p, pObj, i )
247// pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
248 // create POs
249 Saig_ManForEachPo( p, pObj, i )
250 {
251 Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
252 Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
253 }
254 // create LIs
255 Aig_ManForEachCo( p, pObj, i )
256 if ( pObj->fMarkA )
257 {
258 pObj->fMarkA = 0;
259 Saig_ManAbstractionDfs_rec( pNew, Aig_ObjFanin0(pObj) );
260 Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
261 }
262 Aig_ManSetRegNum( pNew, Vec_IntSize(vFlops) );
263 Aig_ManSeqCleanup( pNew );
264 // remove PIs without fanout
265// pNew = Saig_ManTrimPis( pTemp = pNew );
266// Aig_ManStop( pTemp );
267 return pNew;
268}
Aig_ManSeqCleanup
int Aig_ManSeqCleanup(Aig_Man_t *p)
Definition aigScl.c:158
Aig_ManForEachCo
#define Aig_ManForEachCo(p, pObj, i)
Definition aig.h:398
Aig_ManCleanData
void Aig_ManCleanData(Aig_Man_t *p)
Definition aigUtil.c:205
p
Cube * p
Definition exorList.c:222
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition saig.h:93
Aig_Obj_t_::fMarkA
unsigned int fMarkA
Definition aig.h:79
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDupCones()

Aig_Man_t * Saig_ManDupCones ( Aig_Man_t * pAig,
int * pPos,
int nPos )

Definition at line 545 of file saigDup.c.

546{
547 Aig_Man_t * pAigNew;
548 Vec_Ptr_t * vLeaves, * vNodes, * vRoots;
549 Aig_Obj_t * pObj;
550 int i;
551
552 // collect initial POs
553 vLeaves = Vec_PtrAlloc( 100 );
554 vNodes = Vec_PtrAlloc( 100 );
555 vRoots = Vec_PtrAlloc( 100 );
556 for ( i = 0; i < nPos; i++ )
557 Vec_PtrPush( vRoots, Aig_ManCo(pAig, pPos[i]) );
558
559 // mark internal nodes
560 Aig_ManIncrementTravId( pAig );
561 Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
562 Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
563 Saig_ManDupCones_rec( pAig, pObj, vLeaves, vNodes, vRoots );
564
565 // start the new manager
566 pAigNew = Aig_ManStart( Vec_PtrSize(vNodes) );
567 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
568 // map the constant node
569 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
570 // create PIs
571 Vec_PtrForEachEntry( Aig_Obj_t *, vLeaves, pObj, i )
572 pObj->pData = Aig_ObjCreateCi( pAigNew );
573 // create LOs
574 Vec_PtrForEachEntryStart( Aig_Obj_t *, vRoots, pObj, i, nPos )
575 Saig_ObjLiToLo(pAig, pObj)->pData = Aig_ObjCreateCi( pAigNew );
576 // create internal nodes
577 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
578 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
579 // create COs
580 Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
581 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
582 // finalize
583 Aig_ManSetRegNum( pAigNew, Vec_PtrSize(vRoots)-nPos );
584 Vec_PtrFree( vLeaves );
585 Vec_PtrFree( vNodes );
586 Vec_PtrFree( vRoots );
587 return pAigNew;
588
589}
Aig_ManIncrementTravId
void Aig_ManIncrementTravId(Aig_Man_t *p)
DECLARATIONS ///.
Definition aigUtil.c:44
Saig_ManDupCones_rec
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:526
Vec_PtrForEachEntryStart
#define Vec_PtrForEachEntryStart(Type, vVec, pEntry, i, Start)
Definition vecPtr.h:57
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDupCones_rec()

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 526 of file saigDup.c.

527{
528 if ( Aig_ObjIsTravIdCurrent(p, pObj) )
529 return;
530 Aig_ObjSetTravIdCurrent(p, pObj);
531 if ( Aig_ObjIsNode(pObj) )
532 {
533 Saig_ManDupCones_rec( p, Aig_ObjFanin0(pObj), vLeaves, vNodes, vRoots );
534 Saig_ManDupCones_rec( p, Aig_ObjFanin1(pObj), vLeaves, vNodes, vRoots );
535 Vec_PtrPush( vNodes, pObj );
536 }
537 else if ( Aig_ObjIsCo(pObj) )
538 Saig_ManDupCones_rec( p, Aig_ObjFanin0(pObj), vLeaves, vNodes, vRoots );
539 else if ( Saig_ObjIsLo(p, pObj) )
540 Vec_PtrPush( vRoots, Saig_ObjLoToLi(p, pObj) );
541 else if ( Saig_ObjIsPi(p, pObj) )
542 Vec_PtrPush( vLeaves, pObj );
543 else assert( 0 );
544}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDupOrpos()

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_Or
Aig_Obj_t * Aig_Or(Aig_Man_t *p, Aig_Obj_t *p0, Aig_Obj_t *p1)
Definition aigOper.c:259
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManDupWithPhase()

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 482 of file saigDup.c.

483{
484 Aig_Man_t * pAigNew;
485 Aig_Obj_t * pObj;
486 int i;
487 assert( Aig_ManRegNum(pAig) <= Vec_IntSize(vInit) );
488 // start the new manager
489 pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) );
490 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
491 pAigNew->nConstrs = pAig->nConstrs;
492 // map the constant node
493 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
494 // create variables for PIs
495 Aig_ManForEachCi( pAig, pObj, i )
496 pObj->pData = Aig_ObjCreateCi( pAigNew );
497 // update the flop variables
498 Saig_ManForEachLo( pAig, pObj, i )
499 pObj->pData = Aig_NotCond( (Aig_Obj_t *)pObj->pData, Vec_IntEntry(vInit, i) );
500 // add internal nodes of this frame
501 Aig_ManForEachNode( pAig, pObj, i )
502 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
503 // transfer to register outputs
504 Saig_ManForEachPo( pAig, pObj, i )
505 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
506 // update the flop variables
507 Saig_ManForEachLi( pAig, pObj, i )
508 Aig_ObjCreateCo( pAigNew, Aig_NotCond(Aig_ObjChild0Copy(pObj), Vec_IntEntry(vInit, i)) );
509 // finalize
510 Aig_ManCleanup( pAigNew );
511 Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
512 return pAigNew;
513}
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition saig.h:96
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManExtendCex()

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 384 of file saigDup.c.

385{
386 Abc_Cex_t * pNew;
387 Aig_Obj_t * pObj, * pObjRi, * pObjRo;
388 int RetValue, i, k, iBit = 0;
389 // create new counter-example
390 pNew = Abc_CexAlloc( 0, Aig_ManCiNum(pAig), p->iFrame + 1 );
391 pNew->iPo = p->iPo;
392 pNew->iFrame = p->iFrame;
393 // simulate the AIG
394 Aig_ManCleanMarkB(pAig);
395 Aig_ManConst1(pAig)->fMarkB = 1;
396 Saig_ManForEachLo( pAig, pObj, i )
397 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
398 for ( i = 0; i <= p->iFrame; i++ )
399 {
400 Saig_ManForEachPi( pAig, pObj, k )
401 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
403 Aig_ManForEachCi( pAig, pObj, k )
404 if ( pObj->fMarkB )
405 Abc_InfoSetBit(pNew->pData, Aig_ManCiNum(pAig)*i + k);
407 Aig_ManForEachNode( pAig, pObj, k )
408 pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
409 (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
410 Aig_ManForEachCo( pAig, pObj, k )
411 pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
412 if ( i == p->iFrame )
413 break;
414 Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
415 pObjRo->fMarkB = pObjRi->fMarkB;
416 }
417 assert( iBit == p->nBits );
418 RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
419 Aig_ManCleanMarkB(pAig);
420 if ( RetValue == 0 )
421 printf( "Saig_ManExtendCex(): The counter-example is invalid!!!\n" );
422 return pNew;
423}
Aig_ManCleanMarkB
void Aig_ManCleanMarkB(Aig_Man_t *p)
Definition aigUtil.c:167
Saig_ManForEachLiLo
#define Saig_ManForEachLiLo(p, pObjLi, pObjLo, i)
Definition saig.h:101
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition saig.h:91
Aig_Obj_t_::fMarkB
unsigned int fMarkB
Definition aig.h:80
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition utilCex.c:51
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition utilCex.h:39
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManFindFailedPoCex()

int Saig_ManFindFailedPoCex ( Aig_Man_t * pAig,
Abc_Cex_t * p )

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

Synopsis [Resimulates the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 436 of file saigDup.c.

437{
438 Aig_Obj_t * pObj, * pObjRi, * pObjRo;
439 int RetValue, i, k, iBit = 0;
440 Aig_ManCleanMarkB(pAig);
441 Aig_ManConst1(pAig)->fMarkB = 1;
442 Saig_ManForEachLo( pAig, pObj, i )
443 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
444 for ( i = 0; i <= p->iFrame; i++ )
445 {
446 Saig_ManForEachPi( pAig, pObj, k )
447 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
448 Aig_ManForEachNode( pAig, pObj, k )
449 pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
450 (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
451 Aig_ManForEachCo( pAig, pObj, k )
452 pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
453 if ( i == p->iFrame )
454 break;
455 Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
456 pObjRo->fMarkB = pObjRi->fMarkB;
457 }
458 assert( iBit == p->nBits );
459 // remember the number of failed output
460 RetValue = -1;
461 Saig_ManForEachPo( pAig, pObj, i )
462 if ( pObj->fMarkB )
463 {
464 RetValue = i;
465 break;
466 }
467 Aig_ManCleanMarkB(pAig);
468 return RetValue;
469}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManReturnFailingState()

Vec_Int_t * Saig_ManReturnFailingState ( Aig_Man_t * pAig,
Abc_Cex_t * p,
int fNextOne )

Definition at line 347 of file saigDup.c.

348{
349 Aig_Obj_t * pObj;
350 Vec_Int_t * vState;
351 int i, RetValue = Saig_ManVerifyCexNoClear( pAig, p );
352 if ( RetValue == 0 )
353 {
354 Aig_ManCleanMarkB(pAig);
355 printf( "CEX does fail the given sequential miter.\n" );
356 return NULL;
357 }
358 vState = Vec_IntAlloc( Aig_ManRegNum(pAig) );
359 if ( fNextOne )
360 {
361 Saig_ManForEachLi( pAig, pObj, i )
362 Vec_IntPush( vState, pObj->fMarkB );
363 }
364 else
365 {
366 Saig_ManForEachLo( pAig, pObj, i )
367 Vec_IntPush( vState, pObj->fMarkB );
368 }
369 Aig_ManCleanMarkB(pAig);
370 return vState;
371}
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Saig_ManVerifyCexNoClear
int Saig_ManVerifyCexNoClear(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition saigDup.c:320
Here is the call graph for this function:

◆ Saig_ManTrimPis()

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 143 of file saigDup.c.

144{
145 Aig_Man_t * pNew;
146 Aig_Obj_t * pObj;
147 int i, fAllPisHaveNoRefs;
148 // check the refs of PIs
149 fAllPisHaveNoRefs = 1;
150 Saig_ManForEachPi( p, pObj, i )
151 if ( pObj->nRefs )
152 fAllPisHaveNoRefs = 0;
153 // start the new manager
154 pNew = Aig_ManStart( Aig_ManObjNum(p) );
155 pNew->pName = Abc_UtilStrsav( p->pName );
156 pNew->nConstrs = p->nConstrs;
157 // start mapping of the CI numbers
158 pNew->vCiNumsOrig = Vec_IntAlloc( Aig_ManCiNum(p) );
159 // map const and primary inputs
160 Aig_ManCleanData( p );
161 Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
162 Aig_ManForEachCi( p, pObj, i )
163 if ( fAllPisHaveNoRefs || pObj->nRefs || Saig_ObjIsLo(p, pObj) )
164 {
165 pObj->pData = Aig_ObjCreateCi( pNew );
166 Vec_IntPush( pNew->vCiNumsOrig, Vec_IntEntry(p->vCiNumsOrig, i) );
167 }
168 Aig_ManForEachNode( p, pObj, i )
169 pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
170 Aig_ManForEachCo( p, pObj, i )
171 pObj->pData = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
172 Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
173 return pNew;
174}
Aig_Obj_t_::nRefs
unsigned int nRefs
Definition aig.h:81
Here is the call graph for this function:

◆ Saig_ManVerifyCex()

int Saig_ManVerifyCex ( Aig_Man_t * pAig,
Abc_Cex_t * p )

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

Synopsis [Resimulates the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 281 of file saigDup.c.

282{
283 Aig_Obj_t * pObj, * pObjRi, * pObjRo;
284 int RetValue, i, k, iBit = 0;
285 Aig_ManCleanMarkB(pAig);
286 Aig_ManConst1(pAig)->fMarkB = 1;
287 Saig_ManForEachLo( pAig, pObj, i )
288 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
289 for ( i = 0; i <= p->iFrame; i++ )
290 {
291 Saig_ManForEachPi( pAig, pObj, k )
292 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
293 Aig_ManForEachNode( pAig, pObj, k )
294 pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
295 (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
296 Aig_ManForEachCo( pAig, pObj, k )
297 pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
298 if ( i == p->iFrame )
299 break;
300 Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
301 pObjRo->fMarkB = pObjRi->fMarkB;
302 }
303 assert( iBit == p->nBits );
304 RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
305 Aig_ManCleanMarkB(pAig);
306 return RetValue;
307}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Saig_ManVerifyCexNoClear()

int Saig_ManVerifyCexNoClear ( Aig_Man_t * pAig,
Abc_Cex_t * p )

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

Synopsis [Resimulates the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 320 of file saigDup.c.

321{
322 Aig_Obj_t * pObj, * pObjRi, * pObjRo;
323 int RetValue, i, k, iBit = 0;
324 Aig_ManCleanMarkB(pAig);
325 Aig_ManConst1(pAig)->fMarkB = 1;
326 Saig_ManForEachLo( pAig, pObj, i )
327 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
328 for ( i = 0; i <= p->iFrame; i++ )
329 {
330 Saig_ManForEachPi( pAig, pObj, k )
331 pObj->fMarkB = Abc_InfoHasBit(p->pData, iBit++);
332 Aig_ManForEachNode( pAig, pObj, k )
333 pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
334 (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
335 Aig_ManForEachCo( pAig, pObj, k )
336 pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
337 if ( i == p->iFrame )
338 break;
339 Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
340 pObjRo->fMarkB = pObjRi->fMarkB;
341 }
342 assert( iBit == p->nBits );
343 RetValue = Aig_ManCo(pAig, p->iPo)->fMarkB;
344 //Aig_ManCleanMarkB(pAig);
345 return RetValue;
346}
Here is the call graph for this function:
Here is the caller graph for this function: