abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
Functions
utilCex.c File Reference
#include <stdio.h>
#include <string.h>
#include <stdlib.h>
#include <assert.h>
#include "misc/vec/vec.h"
#include "utilCex.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START
Abc_Cex_t * 		Abc_CexAlloc (int nRegs, int nRealPis, int nFrames)
 DECLARATIONS ///. More...
 
Abc_Cex_t * Abc_CexAllocFull (int nRegs, int nRealPis, int nFrames)
 
Abc_Cex_t * Abc_CexMakeTriv (int nRegs, int nTruePis, int nTruePos, int iFrameOut)
 
Abc_Cex_t * Abc_CexCreate (int nRegs, int nPis, 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)
 
static int Abc_CexOnes32 (unsigned i)
 
int Abc_CexCountOnes (Abc_Cex_t *p)
 

Function Documentation

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

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 }
memset
char * memset()
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
nWords
int nWords
Definition: abcNpn.c:127
Abc_BitWordNum
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Abc_Cex_t* Abc_CexAllocFull ( int  nRegs,
int  nRealPis,
int  nFrames 
)

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 }
memset
char * memset()
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
nWords
int nWords
Definition: abcNpn.c:127
Abc_BitWordNum
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
int Abc_CexCountOnes ( Abc_Cex_t *  p)

Definition at line 548 of file utilCex.c.

549 {
550  int nWords = Abc_BitWordNum( p->nBits );
551  int i, Count = 0;
552  for ( i = 0; i < nWords; i++ )
553  Count += Abc_CexOnes32( p->pData[i] );
554  return Count;
555 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
nWords
int nWords
Definition: abcNpn.c:127
Abc_CexOnes32
static int Abc_CexOnes32(unsigned i)
Definition: utilCex.c:541
Abc_BitWordNum
static int Abc_BitWordNum(int nBits)
Definition: abc_global.h:255
Abc_Cex_t* Abc_CexCreate ( int  nRegs,
int  nPis,
int *  pArray,
int  iFrame,
int  iPo,
int  fSkipRegs 
)

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
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Abc_Cex_t* Abc_CexDeriveFromCombModel ( int *  pModel,
int  nPis,
int  nRegs,
int  iPo 
)

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 }
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
Abc_Cex_t* Abc_CexDup ( Abc_Cex_t *  p,
int  nRegsNew 
)

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 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
void Abc_CexFree ( Abc_Cex_t *  p)

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

Synopsis [Frees the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 371 of file utilCex.c.

372 {
373  if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
374  return;
375  ABC_FREE( p );
376 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
void Abc_CexFreeP ( Abc_Cex_t **  p)

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

Synopsis [Frees the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 350 of file utilCex.c.

351 {
352  if ( *p == NULL )
353  return;
354  if ( *p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
355  *p = NULL;
356  else
357  ABC_FREE( *p );
358 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Abc_Cex_t* Abc_CexMakeTriv ( int  nRegs,
int  nTruePis,
int  nTruePos,
int  iFrameOut 
)

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 }
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
assert
#define assert(ex)
Definition: util_old.h:213
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Abc_Cex_t* Abc_CexMerge ( Abc_Cex_t *  pCex,
Abc_Cex_t *  pPart,
int  iFrBeg,
int  iFrEnd 
)

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 }
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
assert
#define assert(ex)
Definition: util_old.h:213
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
static int Abc_CexOnes32 ( unsigned  i)
inlinestatic

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

Synopsis [Count the number of 1s in the CEX.]

Description []

SideEffects []

SeeAlso []

Definition at line 541 of file utilCex.c.

542 {
543  i = i - ((i >> 1) & 0x55555555);
544  i = (i & 0x33333333) + ((i >> 2) & 0x33333333);
545  i = ((i + (i >> 4)) & 0x0F0F0F0F);
546  return (i*(0x01010101))>>24;
547 }
Abc_Cex_t* Abc_CexPermute ( Abc_Cex_t *  p,
Vec_Int_t *  vMapOld2New 
)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 487 of file utilCex.c.

488 {
489  Abc_Cex_t * pCex;
490  int i, iNew;
491  assert( Vec_IntSize(vMapOld2New) == p->nPis );
492  pCex = Abc_CexAlloc( p->nRegs, p->nPis, p->iFrame+1 );
493  pCex->iPo = p->iPo;
494  pCex->iFrame = p->iFrame;
495  for ( i = p->nRegs; i < p->nBits; i++ )
496  if ( Abc_InfoHasBit(p->pData, i) )
497  {
498  iNew = p->nRegs + p->nPis * ((i - p->nRegs) / p->nPis) + Vec_IntEntry( vMapOld2New, (i - p->nRegs) % p->nPis );
499  Abc_InfoSetBit( pCex->pData, iNew );
500  }
501  return pCex;
502 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
Vec_IntEntry
static int Vec_IntEntry(Vec_Int_t *p, int i)
Definition: bblif.c:268
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
assert
#define assert(ex)
Definition: util_old.h:213
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Abc_Cex_t* Abc_CexPermuteTwo ( Abc_Cex_t *  p,
Vec_Int_t *  vPermOld,
Vec_Int_t *  vPermNew 
)

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

Synopsis [Derives permuted CEX using two canonical permutations.]

Description []

SideEffects []

SeeAlso []

Definition at line 515 of file utilCex.c.

516 {
517  Abc_Cex_t * pCex;
518  Vec_Int_t * vPerm;
519  int i, eOld, eNew;
520  assert( Vec_IntSize(vPermOld) == p->nPis );
521  assert( Vec_IntSize(vPermNew) == p->nPis );
522  vPerm = Vec_IntStartFull( p->nPis );
523  Vec_IntForEachEntryTwo( vPermOld, vPermNew, eOld, eNew, i )
524  Vec_IntWriteEntry( vPerm, eOld, eNew );
525  pCex = Abc_CexPermute( p, vPerm );
526  Vec_IntFree( vPerm );
527  return pCex;
528 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Vec_IntStartFull
static Vec_Int_t * Vec_IntStartFull(int nSize)
Definition: vecInt.h:119
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Vec_IntForEachEntryTwo
#define Vec_IntForEachEntryTwo(vVec1, vVec2, Entry1, Entry2, i)
Definition: vecInt.h:64
Vec_IntSize
static int Vec_IntSize(Vec_Int_t *p)
Definition: bblif.c:252
assert
#define assert(ex)
Definition: util_old.h:213
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Abc_CexPermute
Abc_Cex_t * Abc_CexPermute(Abc_Cex_t *p, Vec_Int_t *vMapOld2New)
Definition: utilCex.c:487
void Abc_CexPrint ( Abc_Cex_t *  p)

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

Synopsis [Prints out the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 311 of file utilCex.c.

312 {
313  int i, f, k;
314  if ( p == NULL )
315  {
316  printf( "The counter example is NULL.\n" );
317  return;
318  }
319  if ( p == (Abc_Cex_t *)(ABC_PTRINT_T)1 )
320  {
321  printf( "The counter example is present but not available (pointer has value \"1\").\n" );
322  return;
323  }
324  Abc_CexPrintStats( p );
325  printf( "State : " );
326  for ( k = 0; k < p->nRegs; k++ )
327  printf( "%d", Abc_InfoHasBit(p->pData, k) );
328  printf( "\n" );
329  for ( f = 0; f <= p->iFrame; f++ )
330  {
331  printf( "Frame %3d : ", f );
332  for ( i = 0; i < p->nPis; i++ )
333  printf( "%d", Abc_InfoHasBit(p->pData, k++) );
334  printf( "\n" );
335  }
336  assert( k == p->nBits );
337 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Abc_CexPrintStats
void Abc_CexPrintStats(Abc_Cex_t *p)
Definition: utilCex.c:256
assert
#define assert(ex)
Definition: util_old.h:213
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
void Abc_CexPrintStats ( Abc_Cex_t *  p)

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 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Counter
static int Counter
Definition: extraBddMisc.c:1877
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
void Abc_CexPrintStatsInputs ( Abc_Cex_t *  p,
int  nInputs 
)

Definition at line 275 of file utilCex.c.

276 {
277  int k, Counter = 0, Counter2 = 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  for ( k = 0; k < p->nBits; k++ )
289  {
290  Counter += Abc_InfoHasBit(p->pData, k);
291  if ( (k - p->nRegs) % p->nPis < nInputs )
292  Counter2 += Abc_InfoHasBit(p->pData, k);
293  }
294  printf( "CEX: Po =%4d Frame =%4d FF = %d PI = %d Bit =%8d 1s =%8d (%5.2f %%) 1sIn =%8d (%5.2f %%)\n",
295  p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits,
296  Counter, 100.0 * Counter / (p->nBits - p->nRegs),
297  Counter2, 100.0 * Counter2 / (p->nBits - p->nRegs - (p->iFrame + 1) * (p->nPis - nInputs)) );
298 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Counter
static int Counter
Definition: extraBddMisc.c:1877
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Abc_Cex_t* Abc_CexTransformPhase ( Abc_Cex_t *  p,
int  nPisOld,
int  nPosOld,
int  nRegsOld 
)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 390 of file utilCex.c.

391 {
392  Abc_Cex_t * pCex;
393  int nFrames = p->nPis / nPisOld;
394  int nPosNew = nPosOld * nFrames;
395  assert( p->nPis % nPisOld == 0 );
396  assert( p->iPo < nPosNew );
397  pCex = Abc_CexDup( p, nRegsOld );
398  pCex->nPis = nPisOld;
399  pCex->iPo = -1;
400  pCex->iFrame = (p->iFrame + 1) * nFrames - 1;
401  pCex->nBits = p->nBits;
402  return pCex;
403 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_CexDup
Abc_Cex_t * Abc_CexDup(Abc_Cex_t *p, int nRegsNew)
Definition: utilCex.c:145
assert
#define assert(ex)
Definition: util_old.h:213
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Abc_Cex_t* Abc_CexTransformTempor ( Abc_Cex_t *  p,
int  nPisOld,
int  nPosOld,
int  nRegsOld 
)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 416 of file utilCex.c.

417 {
418  Abc_Cex_t * pCex;
419  int i, k, iBit = nRegsOld, nFrames = p->nPis / nPisOld - 1;
420  assert( p->iFrame > 0 ); // otherwise tempor did not properly check for failures in the prefix
421  assert( p->nPis % nPisOld == 0 );
422  pCex = Abc_CexAlloc( nRegsOld, nPisOld, nFrames + p->iFrame + 1 );
423  pCex->iPo = p->iPo;
424  pCex->iFrame = nFrames + p->iFrame;
425  for ( i = 0; i < nFrames; i++ )
426  for ( k = 0; k < nPisOld; k++, iBit++ )
427  if ( Abc_InfoHasBit(p->pData, p->nRegs + (i+1)*nPisOld + k) )
428  Abc_InfoSetBit( pCex->pData, iBit );
429  for ( i = 0; i <= p->iFrame; i++ )
430  for ( k = 0; k < nPisOld; k++, iBit++ )
431  if ( Abc_InfoHasBit(p->pData, p->nRegs + i*p->nPis + k) )
432  Abc_InfoSetBit( pCex->pData, iBit );
433  assert( iBit == pCex->nBits );
434  return pCex;
435 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
assert
#define assert(ex)
Definition: util_old.h:213
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Abc_Cex_t* Abc_CexTransformUndc ( Abc_Cex_t *  p,
char *  pInit 
)

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

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

Description []

SideEffects []

SeeAlso []

Definition at line 448 of file utilCex.c.

449 {
450  Abc_Cex_t * pCex;
451  int nFlops = strlen(pInit);
452  int i, f, iBit, iAddPi = 0, nAddPis = 0;
453  // count how many flops got a new PI
454  for ( i = 0; i < nFlops; i++ )
455  nAddPis += (int)(pInit[i] == 'x');
456  // create new CEX
457  pCex = Abc_CexAlloc( nFlops, p->nPis - nAddPis, p->iFrame + 1 );
458  pCex->iPo = p->iPo;
459  pCex->iFrame = p->iFrame;
460  for ( iBit = 0; iBit < nFlops; iBit++ )
461  {
462  if ( pInit[iBit] == '1' || (pInit[iBit] == 'x' && Abc_InfoHasBit(p->pData, p->nRegs + p->nPis - nAddPis + iAddPi)) )
463  Abc_InfoSetBit( pCex->pData, iBit );
464  iAddPi += (int)(pInit[iBit] == 'x');
465  }
466  assert( iAddPi == nAddPis );
467  // add timeframes
468  for ( f = 0; f <= p->iFrame; f++ )
469  for ( i = 0; i < pCex->nPis; i++, iBit++ )
470  if ( Abc_InfoHasBit(p->pData, p->nRegs + p->nPis * f + i) )
471  Abc_InfoSetBit( pCex->pData, iBit );
472  assert( iBit == pCex->nBits );
473  return pCex;
474 }
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
assert
#define assert(ex)
Definition: util_old.h:213
strlen
int strlen()
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39