ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Classes | Typedefs | Functions
utilCex.h File Reference
This graph shows which files directly or indirectly include this file:

Go to the source code of this file.

Classes

struct  Abc_Cex_t_
 

Typedefs

typedef typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
 INCLUDES ///.
 

Functions

Abc_Cex_t * Abc_CexAlloc (int nRegs, int nTruePis, int nFrames)
 MACRO DEFINITIONS ///.
 
Abc_Cex_t * Abc_CexAllocFull (int nRegs, int nTruePis, int nFrames)
 
Abc_Cex_t * Abc_CexMakeTriv (int nRegs, int nTruePis, int nTruePos, int iFrameOut)
 
Abc_Cex_t * Abc_CexCreate (int nRegs, int nTruePis, int *pArray, int iFrame, int iPo, int fSkipRegs)
 
Abc_Cex_t * Abc_CexDup (Abc_Cex_t *p, int nRegsNew)
 
Abc_Cex_t * Abc_CexDeriveFromCombModel (int *pModel, int nPis, int nRegs, int iPo)
 
Abc_Cex_t * Abc_CexMerge (Abc_Cex_t *pCex, Abc_Cex_t *pPart, int iFrBeg, int iFrEnd)
 
void Abc_CexPrintStats (Abc_Cex_t *p)
 
void Abc_CexPrintStatsInputs (Abc_Cex_t *p, int nInputs)
 
void Abc_CexPrint (Abc_Cex_t *p)
 
void Abc_CexFreeP (Abc_Cex_t **p)
 
void Abc_CexFree (Abc_Cex_t *p)
 
Abc_Cex_t * Abc_CexTransformPhase (Abc_Cex_t *p, int nPisOld, int nPosOld, int nRegsOld)
 
Abc_Cex_t * Abc_CexTransformTempor (Abc_Cex_t *p, int nPisOld, int nPosOld, int nRegsOld)
 
Abc_Cex_t * Abc_CexTransformUndc (Abc_Cex_t *p, char *pInit)
 
Abc_Cex_t * Abc_CexPermute (Abc_Cex_t *p, Vec_Int_t *vMapOld2New)
 
Abc_Cex_t * Abc_CexPermuteTwo (Abc_Cex_t *p, Vec_Int_t *vPermOld, Vec_Int_t *vPermNew)
 
int Abc_CexCountOnes (Abc_Cex_t *p)
 

Typedef Documentation

◆ Abc_Cex_t

typedef typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t

INCLUDES ///.

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

FileName [utilCex.h]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Handling sequential counter-examples.]

Synopsis [Handling sequential counter-examples.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Feburary 13, 2011.]

Revision [

Id
utilCex.h,v 1.00 2011/02/11 00:00:00 alanmi Exp

] PARAMETERS /// BASIC TYPES ///

Definition at line 39 of file utilCex.h.

Function Documentation

◆ Abc_CexAlloc()

Abc_Cex_t * Abc_CexAlloc ( int nRegs,
int nRealPis,
int nFrames )
extern

MACRO DEFINITIONS ///.

FUNCTION DECLARATIONS ///

MACRO DEFINITIONS ///.

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

FileName [utilCex.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [Handling counter-examples.]

Synopsis [Handling counter-examples.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

Date [Ver. 1.0. Started - Feburary 13, 2011.]

Revision [

Id
utilCex.c,v 1.00 2011/02/11 00:00:00 alanmi Exp

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

Synopsis [Allocates a counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 51 of file utilCex.c.

52{
53 Abc_Cex_t * pCex;
54 int nWords = Abc_BitWordNum( nRegs + nRealPis * nFrames );
55 pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
56 memset( pCex, 0, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
57 pCex->nRegs = nRegs;
58 pCex->nPis = nRealPis;
59 pCex->nBits = nRegs + nRealPis * nFrames;
60 return pCex;
61}
nWords
int nWords
Definition abcNpn.c:127
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition utilCex.h:39
memset
char * memset()
Here is the call graph for this function:

◆ Abc_CexAllocFull()

Abc_Cex_t * Abc_CexAllocFull ( int nRegs,
int nTruePis,
int nFrames )
extern

Definition at line 62 of file utilCex.c.

63{
64 Abc_Cex_t * pCex;
65 int nWords = Abc_BitWordNum( nRegs + nRealPis * nFrames );
66 pCex = (Abc_Cex_t *)ABC_ALLOC( char, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
67 memset( pCex, 0xFF, sizeof(Abc_Cex_t) + sizeof(unsigned) * nWords );
68 pCex->nRegs = nRegs;
69 pCex->nPis = nRealPis;
70 pCex->nBits = nRegs + nRealPis * nFrames;
71 return pCex;
72}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_CexCountOnes()

int Abc_CexCountOnes ( Abc_Cex_t * p)
extern

Definition at line 559 of file utilCex.c.

560{
561 int nWords = Abc_BitWordNum( p->nBits );
562 int i, Count = 0;
563 for ( i = 0; i < nWords; i++ )
564 Count += Abc_CexOnes32( p->pData[i] );
565 return Count;
566}
p
Cube * p
Definition exorList.c:222
Here is the caller graph for this function:

◆ Abc_CexCreate()

Abc_Cex_t * Abc_CexCreate ( int nRegs,
int nPis,
int * pArray,
int iFrame,
int iPo,
int fSkipRegs )
extern

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

Synopsis [Derives the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 110 of file utilCex.c.

111{
112 Abc_Cex_t * pCex;
113 int i;
114 pCex = Abc_CexAlloc( nRegs, nPis, iFrame+1 );
115 pCex->iPo = iPo;
116 pCex->iFrame = iFrame;
117 if ( pArray == NULL )
118 return pCex;
119 if ( fSkipRegs )
120 {
121 for ( i = nRegs; i < pCex->nBits; i++ )
122 if ( pArray[i-nRegs] )
123 Abc_InfoSetBit( pCex->pData, i );
124 }
125 else
126 {
127 for ( i = 0; i < pCex->nBits; i++ )
128 if ( pArray[i] )
129 Abc_InfoSetBit( pCex->pData, i );
130 }
131 return pCex;
132}
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition utilCex.c:51
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_CexDeriveFromCombModel()

Abc_Cex_t * Abc_CexDeriveFromCombModel ( int * pModel,
int nPis,
int nRegs,
int iPo )
extern

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

Synopsis [Derives CEX from comb model.]

Description []

SideEffects []

SeeAlso []

Definition at line 173 of file utilCex.c.

174{
175 Abc_Cex_t * pCex;
176 int i;
177 pCex = Abc_CexAlloc( nRegs, nPis, 1 );
178 pCex->iPo = iPo;
179 pCex->iFrame = 0;
180 for ( i = 0; i < nPis; i++ )
181 if ( pModel[i] )
182 pCex->pData[i>>5] |= (1<<(i & 31));
183 return pCex;
184}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_CexDup()

Abc_Cex_t * Abc_CexDup ( Abc_Cex_t * p,
int nRegsNew )
extern

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

Synopsis [Make the trivial counter-example for the trivially asserted output.]

Description []

SideEffects []

SeeAlso []

Definition at line 145 of file utilCex.c.

146{
147 Abc_Cex_t * pCex;
148 int i;
149 if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
150 return p;
151 if ( nRegsNew == -1 )
152 nRegsNew = p->nRegs;
153 pCex = Abc_CexAlloc( nRegsNew, p->nPis, p->iFrame+1 );
154 pCex->iPo = p->iPo;
155 pCex->iFrame = p->iFrame;
156 for ( i = p->nRegs; i < p->nBits; i++ )
157 if ( Abc_InfoHasBit(p->pData, i) )
158 Abc_InfoSetBit( pCex->pData, pCex->nRegs + i - p->nRegs );
159 return pCex;
160}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_CexFree()

void Abc_CexFree ( Abc_Cex_t * p)
extern

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

Synopsis [Frees the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 382 of file utilCex.c.

383{
384 if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
385 return;
386 ABC_FREE( p );
387}
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
Here is the caller graph for this function:

◆ Abc_CexFreeP()

void Abc_CexFreeP ( Abc_Cex_t ** p)
extern

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

Synopsis [Frees the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 361 of file utilCex.c.

362{
363 if ( *p == NULL )
364 return;
365 if ( *p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
366 *p = NULL;
367 else
368 ABC_FREE( *p );
369}
Here is the caller graph for this function:

◆ Abc_CexMakeTriv()

Abc_Cex_t * Abc_CexMakeTriv ( int nRegs,
int nTruePis,
int nTruePos,
int iFrameOut )
extern

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

Synopsis [Make the trivial counter-example for the trivially asserted output.]

Description []

SideEffects []

SeeAlso []

Definition at line 85 of file utilCex.c.

86{
87 Abc_Cex_t * pCex;
88 int iPo, iFrame;
89 assert( nRegs > 0 );
90 iPo = iFrameOut % nTruePos;
91 iFrame = iFrameOut / nTruePos;
92 // allocate the counter example
93 pCex = Abc_CexAlloc( nRegs, nTruePis, iFrame + 1 );
94 pCex->iPo = iPo;
95 pCex->iFrame = iFrame;
96 return pCex;
97}
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:

◆ Abc_CexMerge()

Abc_Cex_t * Abc_CexMerge ( Abc_Cex_t * pCex,
Abc_Cex_t * pPart,
int iFrBeg,
int iFrEnd )
extern

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

Synopsis [Derives CEX from comb model.]

Description []

SideEffects []

SeeAlso []

Definition at line 197 of file utilCex.c.

198{
199 Abc_Cex_t * pNew;
200 int nFramesGain;
201 int i, f, iBit;
202
203 if ( iFrBeg < 0 )
204 { printf( "Starting frame is less than 0.\n" ); return NULL; }
205 if ( iFrEnd < 0 )
206 { printf( "Stopping frame is less than 0.\n" ); return NULL; }
207 if ( iFrBeg > pCex->iFrame )
208 { printf( "Starting frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
209 if ( iFrEnd > pCex->iFrame )
210 { printf( "Stopping frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
211 if ( iFrBeg > iFrEnd )
212 { printf( "Starting frame (%d) should be less than stopping frame (%d).\n", iFrBeg, iFrEnd ); return NULL; }
213 assert( iFrBeg >= 0 && iFrBeg <= pCex->iFrame );
214 assert( iFrEnd >= 0 && iFrEnd <= pCex->iFrame );
215 assert( iFrBeg <= iFrEnd );
216
217 assert( pCex->nPis == pPart->nPis );
218 assert( iFrEnd - iFrBeg + pPart->iPo >= pPart->iFrame );
219
220 nFramesGain = iFrEnd - iFrBeg + pPart->iPo - pPart->iFrame;
221 pNew = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 - nFramesGain );
222 pNew->iPo = pCex->iPo;
223 pNew->iFrame = pCex->iFrame - nFramesGain;
224
225 for ( iBit = 0; iBit < pCex->nRegs; iBit++ )
226 if ( Abc_InfoHasBit(pCex->pData, iBit) )
227 Abc_InfoSetBit( pNew->pData, iBit );
228 for ( f = 0; f < iFrBeg; f++ )
229 for ( i = 0; i < pCex->nPis; i++, iBit++ )
230 if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) )
231 Abc_InfoSetBit( pNew->pData, iBit );
232 for ( f = 0; f < pPart->iFrame; f++ )
233 for ( i = 0; i < pCex->nPis; i++, iBit++ )
234 if ( Abc_InfoHasBit(pPart->pData, pPart->nRegs + pCex->nPis * f + i) )
235 Abc_InfoSetBit( pNew->pData, iBit );
236 for ( f = iFrEnd; f <= pCex->iFrame; f++ )
237 for ( i = 0; i < pCex->nPis; i++, iBit++ )
238 if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) )
239 Abc_InfoSetBit( pNew->pData, iBit );
240 assert( iBit == pNew->nBits );
241
242 return pNew;
243}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_CexPermute()

Abc_Cex_t * Abc_CexPermute ( Abc_Cex_t * p,
Vec_Int_t * vMapOld2New )
extern

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

Synopsis [Derives permuted CEX using permutation of its inputs.]

Description []

SideEffects []

SeeAlso []

Definition at line 498 of file utilCex.c.

499{
500 Abc_Cex_t * pCex;
501 int i, iNew;
502 assert( Vec_IntSize(vMapOld2New) == p->nPis );
503 pCex = Abc_CexAlloc( p->nRegs, p->nPis, p->iFrame+1 );
504 pCex->iPo = p->iPo;
505 pCex->iFrame = p->iFrame;
506 for ( i = p->nRegs; i < p->nBits; i++ )
507 if ( Abc_InfoHasBit(p->pData, i) )
508 {
509 iNew = p->nRegs + p->nPis * ((i - p->nRegs) / p->nPis) + Vec_IntEntry( vMapOld2New, (i - p->nRegs) % p->nPis );
510 Abc_InfoSetBit( pCex->pData, iNew );
511 }
512 return pCex;
513}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_CexPermuteTwo()

Abc_Cex_t * Abc_CexPermuteTwo ( Abc_Cex_t * p,
Vec_Int_t * vPermOld,
Vec_Int_t * vPermNew )
extern

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

Synopsis [Derives permuted CEX using two canonical permutations.]

Description []

SideEffects []

SeeAlso []

Definition at line 526 of file utilCex.c.

527{
528 Abc_Cex_t * pCex;
529 Vec_Int_t * vPerm;
530 int i, eOld, eNew;
531 assert( Vec_IntSize(vPermOld) == p->nPis );
532 assert( Vec_IntSize(vPermNew) == p->nPis );
533 vPerm = Vec_IntStartFull( p->nPis );
534 Vec_IntForEachEntryTwo( vPermOld, vPermNew, eOld, eNew, i )
535 Vec_IntWriteEntry( vPerm, eOld, eNew );
536 pCex = Abc_CexPermute( p, vPerm );
537 Vec_IntFree( vPerm );
538 return pCex;
539}
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Abc_CexPermute
Abc_Cex_t * Abc_CexPermute(Abc_Cex_t *p, Vec_Int_t *vMapOld2New)
Definition utilCex.c:498
Vec_IntForEachEntryTwo
#define Vec_IntForEachEntryTwo(vVec1, vVec2, Entry1, Entry2, i)
Definition vecInt.h:66
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Abc_CexPrint()

void Abc_CexPrint ( Abc_Cex_t * p)
extern

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

Synopsis [Prints out the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 322 of file utilCex.c.

323{
324 int i, f, k;
325 if ( p == NULL )
326 {
327 printf( "The counter example is NULL.\n" );
328 return;
329 }
330 if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
331 {
332 printf( "The counter example is present but not available (pointer has value \"1\").\n" );
333 return;
334 }
335 Abc_CexPrintStats( p );
336 printf( "State : " );
337 for ( k = 0; k < p->nRegs; k++ )
338 printf( "%d", Abc_InfoHasBit(p->pData, k) );
339 printf( "\n" );
340 for ( f = 0; f <= p->iFrame; f++ )
341 {
342 printf( "Frame %3d : ", f );
343 for ( i = 0; i < p->nPis; i++ )
344 printf( "%d", Abc_InfoHasBit(p->pData, k++) );
345 printf( "\n" );
346 }
347 assert( k == p->nBits );
348}
Abc_CexPrintStats
void Abc_CexPrintStats(Abc_Cex_t *p)
Definition utilCex.c:256
Here is the call graph for this function:

◆ Abc_CexPrintStats()

void Abc_CexPrintStats ( Abc_Cex_t * p)
extern

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

Synopsis [Prints out the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 256 of file utilCex.c.

257{
258 int k, Counter = 0;
259 if ( p == NULL )
260 {
261 printf( "The counter example is NULL.\n" );
262 return;
263 }
264 if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
265 {
266 printf( "The counter example is present but not available (pointer has value \"1\").\n" );
267 return;
268 }
269 for ( k = 0; k < p->nBits; k++ )
270 Counter += Abc_InfoHasBit(p->pData, k);
271 printf( "CEX: Po =%4d Frame =%4d FF = %d PI = %d Bit =%8d 1s =%8d (%5.2f %%)\n",
272 p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits,
273 Counter, 100.0 * Counter / (p->nBits - p->nRegs) );
274}
Here is the caller graph for this function:

◆ Abc_CexPrintStatsInputs()

void Abc_CexPrintStatsInputs ( Abc_Cex_t * p,
int nInputs )
extern

Definition at line 275 of file utilCex.c.

276{
277 int k, Counter = 0, CounterPi = 0, CounterPpi = 0;
278 if ( p == NULL )
279 {
280 printf( "The counter example is NULL.\n" );
281 return;
282 }
283 if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
284 {
285 printf( "The counter example is present but not available (pointer has value \"1\").\n" );
286 return;
287 }
288 assert( nRealPis <= p->nPis );
289 for ( k = 0; k < p->nBits; k++ )
290 {
291 Counter += Abc_InfoHasBit(p->pData, k);
292 if ( nRealPis == p->nPis )
293 continue;
294 if ( (k - p->nRegs) % p->nPis < nRealPis )
295 CounterPi += Abc_InfoHasBit(p->pData, k);
296 else
297 CounterPpi += Abc_InfoHasBit(p->pData, k);
298 }
299 printf( "CEX: Po =%4d Fr =%4d FF = %d PI = %d Bit =%7d 1 =%8d (%5.2f %%)",
300 p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits,
301 Counter, 100.0 * Counter / ((p->iFrame + 1) * p->nPis ) );
302 if ( nRealPis < p->nPis )
303 {
304 printf( " 1pi =%8d (%5.2f %%) 1ppi =%8d (%5.2f %%)",
305 CounterPi, 100.0 * CounterPi / ((p->iFrame + 1) * nRealPis ),
306 CounterPpi, 100.0 * CounterPpi / ((p->iFrame + 1) * (p->nPis - nRealPis)) );
307 }
308 printf( "\n" );
309}
Here is the caller graph for this function:

◆ Abc_CexTransformPhase()

Abc_Cex_t * Abc_CexTransformPhase ( Abc_Cex_t * p,
int nPisOld,
int nPosOld,
int nRegsOld )
extern

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

Synopsis [Transform CEX after phase abstraction with nFrames frames.]

Description []

SideEffects []

SeeAlso []

Definition at line 401 of file utilCex.c.

402{
403 Abc_Cex_t * pCex;
404 int nFrames = p->nPis / nPisOld;
405 int nPosNew = nPosOld * nFrames;
406 assert( p->nPis % nPisOld == 0 );
407 assert( p->iPo < nPosNew );
408 pCex = Abc_CexDup( p, nRegsOld );
409 pCex->nPis = nPisOld;
410 pCex->iPo = -1;
411 pCex->iFrame = (p->iFrame + 1) * nFrames - 1;
412 pCex->nBits = p->nBits;
413 return pCex;
414}
Abc_CexDup
Abc_Cex_t * Abc_CexDup(Abc_Cex_t *p, int nRegsNew)
Definition utilCex.c:145
Here is the call graph for this function:

◆ Abc_CexTransformTempor()

Abc_Cex_t * Abc_CexTransformTempor ( Abc_Cex_t * p,
int nPisOld,
int nPosOld,
int nRegsOld )
extern

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

Synopsis [Transform CEX after phase temporal decomposition with nFrames frames.]

Description []

SideEffects []

SeeAlso []

Definition at line 427 of file utilCex.c.

428{
429 Abc_Cex_t * pCex;
430 int i, k, iBit = nRegsOld, nFrames = p->nPis / nPisOld - 1;
431 assert( p->iFrame > 0 ); // otherwise tempor did not properly check for failures in the prefix
432 assert( p->nPis % nPisOld == 0 );
433 pCex = Abc_CexAlloc( nRegsOld, nPisOld, nFrames + p->iFrame + 1 );
434 pCex->iPo = p->iPo;
435 pCex->iFrame = nFrames + p->iFrame;
436 for ( i = 0; i < nFrames; i++ )
437 for ( k = 0; k < nPisOld; k++, iBit++ )
438 if ( Abc_InfoHasBit(p->pData, p->nRegs + (i+1)*nPisOld + k) )
439 Abc_InfoSetBit( pCex->pData, iBit );
440 for ( i = 0; i <= p->iFrame; i++ )
441 for ( k = 0; k < nPisOld; k++, iBit++ )
442 if ( Abc_InfoHasBit(p->pData, p->nRegs + i*p->nPis + k) )
443 Abc_InfoSetBit( pCex->pData, iBit );
444 assert( iBit == pCex->nBits );
445 return pCex;
446}
Here is the call graph for this function:

◆ Abc_CexTransformUndc()

Abc_Cex_t * Abc_CexTransformUndc ( Abc_Cex_t * p,
char * pInit )
extern

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

Synopsis [Transform CEX after "logic; undc; st; zero".]

Description []

SideEffects []

SeeAlso []

Definition at line 459 of file utilCex.c.

460{
461 Abc_Cex_t * pCex;
462 int nFlops = strlen(pInit);
463 int i, f, iBit, iAddPi = 0, nAddPis = 0;
464 // count how many flops got a new PI
465 for ( i = 0; i < nFlops; i++ )
466 nAddPis += (int)(pInit[i] == 'x' || pInit[i] == 'X');
467 // create new CEX
468 pCex = Abc_CexAlloc( nFlops, p->nPis - nAddPis, p->iFrame + 1 );
469 pCex->iPo = p->iPo;
470 pCex->iFrame = p->iFrame;
471 for ( iBit = 0; iBit < nFlops; iBit++ )
472 {
473 if ( pInit[iBit] == '1' || ((pInit[iBit] == 'x' || pInit[iBit] == 'X') && Abc_InfoHasBit(p->pData, p->nRegs + p->nPis - nAddPis + iAddPi)) )
474 Abc_InfoSetBit( pCex->pData, iBit );
475 iAddPi += (int)(pInit[iBit] == 'x' || pInit[iBit] == 'X');
476 }
477 assert( iAddPi == nAddPis );
478 // add timeframes
479 for ( f = 0; f <= p->iFrame; f++ )
480 for ( i = 0; i < pCex->nPis; i++, iBit++ )
481 if ( Abc_InfoHasBit(p->pData, p->nRegs + p->nPis * f + i) )
482 Abc_InfoSetBit( pCex->pData, iBit );
483 assert( iBit == pCex->nBits );
484 return pCex;
485}
strlen
int strlen()
Here is the call graph for this function: