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

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START Abc_Cex_t * Gia_ManCexRemap (Gia_Man_t *p, Abc_Cex_t *pCexAbs, Vec_Int_t *vPis)
 DECLARATIONS ///.
 
int Gia_ManGlaRefine (Gia_Man_t *p, Abc_Cex_t *pCex, int fMinCut, int fVerbose)
 
Vec_Int_t * Gia_ManGetStateAndCheckCex (Gia_Man_t *pAig, Abc_Cex_t *p, int iFrame)
 
void Gia_ManCheckCex (Gia_Man_t *pAig, Abc_Cex_t *p, int iFrame)
 
Gia_Man_t * Gia_ManTransformFlops (Gia_Man_t *p, Vec_Int_t *vFlops, Vec_Int_t *vInit)
 
int Gia_ManNewRefine (Gia_Man_t *p, Abc_Cex_t *pCex, int iFrameStart, int iFrameExtra, int fVerbose)
 

Function Documentation

◆ Gia_ManCexRemap()

ABC_NAMESPACE_IMPL_START Abc_Cex_t * Gia_ManCexRemap ( Gia_Man_t * p,
Abc_Cex_t * pCexAbs,
Vec_Int_t * vPis )

DECLARATIONS ///.

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

FileName [absOut.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Abstraction package.]

Synopsis [Abstraction refinement outside of abstraction engines.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

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

Synopsis [Derive a new counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 45 of file absOut.c.

46{
47 Abc_Cex_t * pCex;
48 int i, f, iPiNum;
49 assert( pCexAbs->iPo == 0 );
50 // start the counter-example
51 pCex = Abc_CexAlloc( Gia_ManRegNum(p), Gia_ManPiNum(p), pCexAbs->iFrame+1 );
52 pCex->iFrame = pCexAbs->iFrame;
53 pCex->iPo = pCexAbs->iPo;
54 // copy the bit data
55 for ( f = 0; f <= pCexAbs->iFrame; f++ )
56 for ( i = 0; i < Vec_IntSize(vPis); i++ )
57 {
58 if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) )
59 {
60 iPiNum = Gia_ObjCioId( Gia_ManObj(p, Vec_IntEntry(vPis, i)) );
61 Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + iPiNum );
62 }
63 }
64 // verify the counter example
65 if ( !Gia_ManVerifyCex( p, pCex, 0 ) )
66 {
67 Abc_Print( 1, "Gia_ManCexRemap(): Counter-example is invalid.\n" );
68 Abc_CexFree( pCex );
69 pCex = NULL;
70 }
71 else
72 {
73 Abc_Print( 1, "Counter-example verification is successful.\n" );
74 Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. \n", pCex->iPo, p->pName, pCex->iFrame );
75 }
76 return pCex;
77}
p
Cube * p
Definition exorList.c:222
Gia_ManVerifyCex
int Gia_ManVerifyCex(Gia_Man_t *pAig, Abc_Cex_t *p, int fDualOut)
DECLARATIONS ///.
Definition giaCex.c:48
Abc_CexFree
void Abc_CexFree(Abc_Cex_t *p)
Definition utilCex.c:382
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
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:

◆ Gia_ManCheckCex()

void Gia_ManCheckCex ( Gia_Man_t * pAig,
Abc_Cex_t * p,
int iFrame )

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

Synopsis [Verify counter-example starting in the given timeframe.]

Description []

SideEffects []

SeeAlso []

Definition at line 298 of file absOut.c.

299{
300 Gia_Obj_t * pObj, * pObjRi, * pObjRo;
301 int RetValue, i, k, iBit = 0;
302 assert( iFrame >= 0 && iFrame <= p->iFrame );
303 Gia_ManCleanMark0(pAig);
304 Gia_ManForEachRo( pAig, pObj, i )
305 pObj->fMark0 = 0;//Abc_InfoHasBit(p->pData, iBit++);
306 for ( i = iFrame, iBit += p->nRegs + Gia_ManPiNum(pAig) * iFrame; i <= p->iFrame; i++ )
307 {
308 Gia_ManForEachPi( pAig, pObj, k )
309 pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
310 Gia_ManForEachAnd( pAig, pObj, k )
311 pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
312 (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
313 Gia_ManForEachCo( pAig, pObj, k )
314 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
315 if ( i == p->iFrame )
316 break;
317 Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
318 pObjRo->fMark0 = pObjRi->fMark0;
319 }
320 assert( iBit == p->nBits );
321 RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
322 Gia_ManCleanMark0(pAig);
323 if ( RetValue == 1 )
324 printf( "Shortened CEX holds for the abstraction of the fast-forwarded model.\n" );
325 else
326 printf( "Shortened CEX does not hold for the abstraction of the fast-forwarded model.\n" );
327}
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition gia.h:1252
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition gia.h:1248
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManCleanMark0
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition giaUtil.c:256
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Gia_ManForEachRiRo
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition gia.h:1256
Gia_Obj_t_::fMark0
unsigned fMark0
Definition gia.h:81
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_ManGetStateAndCheckCex()

Vec_Int_t * Gia_ManGetStateAndCheckCex ( Gia_Man_t * pAig,
Abc_Cex_t * p,
int iFrame )

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

Synopsis [Resimulates the counter-example and returns flop values.]

Description []

SideEffects []

SeeAlso []

Definition at line 251 of file absOut.c.

252{
253 Vec_Int_t * vInit = Vec_IntAlloc( Gia_ManRegNum(pAig) );
254 Gia_Obj_t * pObj, * pObjRi, * pObjRo;
255 int RetValue, i, k, iBit = 0;
256 assert( iFrame >= 0 && iFrame <= p->iFrame );
257 Gia_ManCleanMark0(pAig);
258 Gia_ManForEachRo( pAig, pObj, i )
259 pObj->fMark0 = 0;//Abc_InfoHasBit(p->pData, iBit++);
260 for ( i = 0, iBit = p->nRegs; i <= p->iFrame; i++ )
261 {
262 if ( i == iFrame )
263 {
264 Gia_ManForEachRo( pAig, pObjRo, k )
265 Vec_IntPush( vInit, pObjRo->fMark0 );
266 }
267 Gia_ManForEachPi( pAig, pObj, k )
268 pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
269 Gia_ManForEachAnd( pAig, pObj, k )
270 pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
271 (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
272 Gia_ManForEachCo( pAig, pObj, k )
273 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
274 if ( i == p->iFrame )
275 break;
276 Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
277 pObjRo->fMark0 = pObjRi->fMark0;
278 }
279 assert( iBit == p->nBits );
280 RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
281 if ( RetValue != 1 )
282 Vec_IntFreeP( &vInit );
283 Gia_ManCleanMark0(pAig);
284 return vInit;
285}
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Gia_ManGlaRefine()

int Gia_ManGlaRefine ( Gia_Man_t * p,
Abc_Cex_t * pCex,
int fMinCut,
int fVerbose )

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

Synopsis [Refines gate-level abstraction using the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 90 of file absOut.c.

91{
92 extern void Nwk_ManDeriveMinCut( Gia_Man_t * p, int fVerbose );
93 int fAddOneLayer = 1;
94 Abc_Cex_t * pCexNew = NULL;
95 Gia_Man_t * pAbs;
96 Aig_Man_t * pAig;
97 Abc_Cex_t * pCare;
98 Vec_Int_t * vPis, * vPPis;
99 int f, i, iObjId;
100 abctime clk = Abc_Clock();
101 int nOnes = 0, Counter = 0;
102 if ( p->vGateClasses == NULL )
103 {
104 Abc_Print( 1, "Gia_ManGlaRefine(): Abstraction gate map is missing.\n" );
105 return -1;
106 }
107 // derive abstraction
108 pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
109 Gia_ManStop( pAbs );
110 pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
111 if ( Gia_ManPiNum(pAbs) != pCex->nPis )
112 {
113 Abc_Print( 1, "Gia_ManGlaRefine(): The PI counts in GLA and in CEX do not match.\n" );
114 Gia_ManStop( pAbs );
115 return -1;
116 }
117 if ( !Gia_ManVerifyCex( pAbs, pCex, 0 ) )
118 {
119 Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is invalid.\n" );
120// Gia_ManStop( pAbs );
121// return -1;
122 }
123// else
124// Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is correct.\n" );
125 // get inputs
126 Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, NULL, NULL );
127 assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) );
128 // add missing logic
129 if ( fAddOneLayer )
130 {
131 Gia_Obj_t * pObj;
132 // check if this is a real counter-example
133 Gia_ObjTerSimSet0( Gia_ManConst0(pAbs) );
134 for ( f = 0; f <= pCex->iFrame; f++ )
135 {
136 Gia_ManForEachPi( pAbs, pObj, i )
137 {
138 if ( i >= Vec_IntSize(vPis) ) // PPIs
139 Gia_ObjTerSimSetX( pObj );
140 else if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) )
141 Gia_ObjTerSimSet1( pObj );
142 else
143 Gia_ObjTerSimSet0( pObj );
144 }
145 Gia_ManForEachRo( pAbs, pObj, i )
146 {
147 if ( f == 0 )
148 Gia_ObjTerSimSet0( pObj );
149 else
150 Gia_ObjTerSimRo( pAbs, pObj );
151 }
152 Gia_ManForEachAnd( pAbs, pObj, i )
153 Gia_ObjTerSimAnd( pObj );
154 Gia_ManForEachCo( pAbs, pObj, i )
155 Gia_ObjTerSimCo( pObj );
156 }
157 pObj = Gia_ManPo( pAbs, 0 );
158 if ( Gia_ObjTerSimGet1(pObj) )
159 {
160 pCexNew = Gia_ManCexRemap( p, pCex, vPis );
161 Abc_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame );
162 }
163// else
164// Abc_Print( 1, "CEX is not real.\n" );
165 Gia_ManForEachObj( pAbs, pObj, i )
166 Gia_ObjTerSimSetC( pObj );
167 if ( pCexNew == NULL )
168 {
169 // grow one layer
170 Vec_IntForEachEntry( vPPis, iObjId, i )
171 {
172 assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
173 Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
174 }
175 if ( fVerbose )
176 {
177 Abc_Print( 1, "Additional objects = %d. ", Vec_IntSize(vPPis) );
178 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
179 }
180 }
181 }
182 else
183 {
184 // minimize the CEX
185 pAig = Gia_ManToAigSimple( pAbs );
186 pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, Vec_IntSize(vPis), fVerbose );
187 Aig_ManStop( pAig );
188 if ( pCare == NULL )
189 Abc_Print( 1, "Counter-example minimization has failed.\n" );
190 // add new objects to the map
191 iObjId = -1;
192 for ( f = 0; f <= pCare->iFrame; f++ )
193 for ( i = 0; i < pCare->nPis; i++ )
194 if ( Abc_InfoHasBit( pCare->pData, pCare->nRegs + f * pCare->nPis + i ) )
195 {
196 nOnes++;
197 assert( i >= Vec_IntSize(vPis) );
198 iObjId = Vec_IntEntry( vPPis, i - Vec_IntSize(vPis) );
199 assert( iObjId > 0 && iObjId < Gia_ManObjNum(p) );
200 if ( Vec_IntEntry( p->vGateClasses, iObjId ) > 0 )
201 continue;
202 assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
203 Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
204 // Abc_Print( 1, "Adding object %d.\n", iObjId );
205 // Gia_ObjPrint( p, Gia_ManObj(p, iObjId) );
206 Counter++;
207 }
208 Abc_CexFree( pCare );
209 if ( fVerbose )
210 {
211 Abc_Print( 1, "Essential bits = %d. Additional objects = %d. ", nOnes, Counter );
212 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
213 }
214 // consider the case of SAT
215 if ( iObjId == -1 )
216 {
217 pCexNew = Gia_ManCexRemap( p, pCex, vPis );
218 Abc_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame );
219 }
220 }
221 Vec_IntFree( vPis );
222 Vec_IntFree( vPPis );
223 Gia_ManStop( pAbs );
224 if ( pCexNew )
225 {
226 ABC_FREE( p->pCexSeq );
227 p->pCexSeq = pCexNew;
228 return 0;
229 }
230 // extract abstraction to include min-cut
231 if ( fMinCut )
232 Nwk_ManDeriveMinCut( p, fVerbose );
233 return -1;
234}
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Gia_ManCexRemap
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Gia_ManCexRemap(Gia_Man_t *p, Abc_Cex_t *pCexAbs, Vec_Int_t *vPis)
DECLARATIONS ///.
Definition absOut.c:45
Gia_ManDupAbsGates
Gia_Man_t * Gia_ManDupAbsGates(Gia_Man_t *p, Vec_Int_t *vGateClasses)
Definition absDup.c:220
Gia_ManGlaCollect
void Gia_ManGlaCollect(Gia_Man_t *p, Vec_Int_t *vGateClasses, Vec_Int_t **pvPis, Vec_Int_t **pvPPis, Vec_Int_t **pvFlops, Vec_Int_t **pvNodes)
Definition absDup.c:158
Saig_ManCbaFindCexCareBits
Abc_Cex_t * Saig_ManCbaFindCexCareBits(Aig_Man_t *pAig, Abc_Cex_t *pCex, int nInputs, int fVerbose)
Definition absOldCex.c:718
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition aigMan.c:187
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Gia_ManToAigSimple
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition giaAig.c:408
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition gia.h:1190
Nwk_ManDeriveMinCut
void Nwk_ManDeriveMinCut(Gia_Man_t *p, int fVerbose)
Definition nwkAig.c:218
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Here is the call graph for this function:

◆ Gia_ManNewRefine()

int Gia_ManNewRefine ( Gia_Man_t * p,
Abc_Cex_t * pCex,
int iFrameStart,
int iFrameExtra,
int fVerbose )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 373 of file absOut.c.

374{
375 Gia_Man_t * pAbs, * pNew;
376 Vec_Int_t * vFlops, * vInit;
377 Vec_Int_t * vCopy;
378// abctime clk = Abc_Clock();
379 int RetValue;
380 ABC_FREE( p->pCexSeq );
381 if ( p->vGateClasses == NULL )
382 {
383 Abc_Print( 1, "Gia_ManNewRefine(): Abstraction gate map is missing.\n" );
384 return -1;
385 }
386 vCopy = Vec_IntDup( p->vGateClasses );
387 Abc_Print( 1, "Refining with %d-frame CEX, starting in frame %d, with %d extra frames.\n", pCex->iFrame, iFrameStart, iFrameExtra );
388 // derive abstraction
389 pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
390 Gia_ManStop( pAbs );
391 pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
392 if ( Gia_ManPiNum(pAbs) != pCex->nPis )
393 {
394 Abc_Print( 1, "Gia_ManNewRefine(): The PI counts in GLA and in CEX do not match.\n" );
395 Gia_ManStop( pAbs );
396 Vec_IntFree( vCopy );
397 return -1;
398 }
399 // get the state in frame iFrameStart
400 vInit = Gia_ManGetStateAndCheckCex( pAbs, pCex, iFrameStart );
401 if ( vInit == NULL )
402 {
403 Abc_Print( 1, "Gia_ManNewRefine(): The initial counter-example is invalid.\n" );
404 Gia_ManStop( pAbs );
405 Vec_IntFree( vCopy );
406 return -1;
407 }
408 if ( fVerbose )
409 Abc_Print( 1, "Gia_ManNewRefine(): The initial counter-example is correct.\n" );
410 // get inputs
411 Gia_ManGlaCollect( p, p->vGateClasses, NULL, NULL, &vFlops, NULL );
412// assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) );
413 Gia_ManStop( pAbs );
414//Vec_IntPrint( vFlops );
415//Vec_IntPrint( vInit );
416 // transform the manager to have new init state
417 pNew = Gia_ManTransformFlops( p, vFlops, vInit );
418 Vec_IntFree( vFlops );
419 Vec_IntFree( vInit );
420 // verify abstraction
421 {
422 Gia_Man_t * pAbs = Gia_ManDupAbsGates( pNew, p->vGateClasses );
423 Gia_ManCheckCex( pAbs, pCex, iFrameStart );
424 Gia_ManStop( pAbs );
425 }
426 // transfer abstraction
427 assert( pNew->vGateClasses == NULL );
428 pNew->vGateClasses = Vec_IntDup( p->vGateClasses );
429 // perform abstraction for the new AIG
430 {
431 Abs_Par_t Pars, * pPars = &Pars;
432 Abs_ParSetDefaults( pPars );
433 pPars->nFramesMax = pCex->iFrame - iFrameStart + 1 + iFrameExtra;
434 pPars->fVerbose = fVerbose;
435 RetValue = Gia_ManPerformGla( pNew, pPars );
436 if ( RetValue == 0 ) // spurious SAT
437 {
438 Vec_IntFreeP( &pNew->vGateClasses );
439 pNew->vGateClasses = Vec_IntDup( vCopy );
440 }
441 }
442 // move the abstraction map
443 Vec_IntFreeP( &p->vGateClasses );
444 p->vGateClasses = pNew->vGateClasses;
445 pNew->vGateClasses = NULL;
446 // cleanup
447 Gia_ManStop( pNew );
448 Vec_IntFree( vCopy );
449 return -1;
450}
Gia_ManTransformFlops
Gia_Man_t * Gia_ManTransformFlops(Gia_Man_t *p, Vec_Int_t *vFlops, Vec_Int_t *vInit)
Definition absOut.c:340
Gia_ManGetStateAndCheckCex
Vec_Int_t * Gia_ManGetStateAndCheckCex(Gia_Man_t *pAig, Abc_Cex_t *p, int iFrame)
Definition absOut.c:251
Gia_ManCheckCex
void Gia_ManCheckCex(Gia_Man_t *pAig, Abc_Cex_t *p, int iFrame)
Definition absOut.c:298
Abs_ParSetDefaults
void Abs_ParSetDefaults(Abs_Par_t *p)
DECLARATIONS ///.
Definition absUtil.c:44
Abs_Par_t
typedefABC_NAMESPACE_HEADER_START struct Abs_Par_t_ Abs_Par_t
INCLUDES ///.
Definition abs.h:46
Gia_ManPerformGla
int Gia_ManPerformGla(Gia_Man_t *p, Abs_Par_t *pPars)
Definition absGla.c:1500
Gia_Man_t_::vGateClasses
Vec_Int_t * vGateClasses
Definition gia.h:157
Here is the call graph for this function:

◆ Gia_ManTransformFlops()

Gia_Man_t * Gia_ManTransformFlops ( Gia_Man_t * p,
Vec_Int_t * vFlops,
Vec_Int_t * vInit )

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 340 of file absOut.c.

341{
342 Vec_Bit_t * vInitNew;
343 Gia_Man_t * pNew;
344 Gia_Obj_t * pObj;
345 int i, iFlopId;
346 assert( Vec_IntSize(vInit) == Vec_IntSize(vFlops) );
347 vInitNew = Vec_BitStart( Gia_ManRegNum(p) );
348 Gia_ManForEachObjVec( vFlops, p, pObj, i )
349 {
350 assert( Gia_ObjIsRo(p, pObj) );
351 if ( Vec_IntEntry(vInit, i) == 0 )
352 continue;
353 iFlopId = Gia_ObjCioId(pObj) - Gia_ManPiNum(p);
354 assert( iFlopId >= 0 && iFlopId < Gia_ManRegNum(p) );
355 Vec_BitWriteEntry( vInitNew, iFlopId, 1 );
356 }
357 pNew = Gia_ManDupFlip( p, Vec_BitArray(vInitNew) );
358 Vec_BitFree( vInitNew );
359 return pNew;
360}
Gia_ManDupFlip
Gia_Man_t * Gia_ManDupFlip(Gia_Man_t *p, int *pInitState)
Definition giaDup.c:628
Gia_ManForEachObjVec
#define Gia_ManForEachObjVec(vVec, p, pObj, i)
Definition gia.h:1194
Vec_Bit_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Bit_t_ Vec_Bit_t
INCLUDES ///.
Definition vecBit.h:42
Here is the call graph for this function:
Here is the caller graph for this function: