abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
bmcCexCut.c File Reference
#include "bmc.h"
#include "aig/gia/giaAig.h"

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START int Bmc_GiaGenerateJust_rec (Gia_Man_t *p, int iFrame, int iObj, Vec_Bit_t *vValues, Vec_Bit_t *vJustis)
 DECLARATIONS ///. More...
 
void Bmc_GiaGenerateJustNonRec (Gia_Man_t *p, int iFrame, Vec_Bit_t *vValues, Vec_Bit_t *vJustis)
 
void Bmc_GiaGenerateJust (Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Bit_t **pvValues, Vec_Bit_t **pvJustis)
 
Gia_Man_tBmc_GiaGenerateGiaOne (Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Bit_t **pvInits, int iFrBeg, int iFrEnd)
 
Gia_Man_tBmc_GiaGenerateGiaAllFrames (Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Bit_t **pvInits, int iFrBeg, int iFrEnd)
 
Gia_Man_tBmc_GiaGenerateGiaAllOne (Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Bit_t **pvInits, int iFrBeg, int iFrEnd)
 
Gia_Man_tBmc_GiaTargetStates (Gia_Man_t *p, Abc_Cex_t *pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fUseOne, int fAllFrames, int fVerbose)
 
Aig_Man_tBmc_AigTargetStates (Aig_Man_t *p, Abc_Cex_t *pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fUseOne, int fAllFrames, int fVerbose)
 

Function Documentation

Aig_Man_t* Bmc_AigTargetStates ( Aig_Man_t p,
Abc_Cex_t pCex,
int  iFrBeg,
int  iFrEnd,
int  fCombOnly,
int  fUseOne,
int  fAllFrames,
int  fVerbose 
)

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

Synopsis [Generate AIG for target bad states.]

Description []

SideEffects []

SeeAlso []

Definition at line 513 of file bmcCexCut.c.

514 {
515  Aig_Man_t * pAig;
516  Gia_Man_t * pGia, * pRes;
517  pGia = Gia_ManFromAigSimple( p );
518  if ( !Gia_ManVerifyCex( pGia, pCex, 0 ) )
519  {
520  Abc_Print( 1, "Current CEX does not fail AIG \"%s\".\n", p->pName );
521  Gia_ManStop( pGia );
522  return NULL;
523  }
524  pRes = Bmc_GiaTargetStates( pGia, pCex, iFrBeg, iFrEnd, fCombOnly, fUseOne, fAllFrames, fVerbose );
525  Gia_ManStop( pGia );
526  pAig = Gia_ManToAigSimple( pRes );
527  Gia_ManStop( pRes );
528  return pAig;
529 }
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition: giaAig.c:367
int Gia_ManVerifyCex(Gia_Man_t *pAig, Abc_Cex_t *p, int fDualOut)
DECLARATIONS ///.
Definition: giaCex.c:44
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
Gia_Man_t * Bmc_GiaTargetStates(Gia_Man_t *p, Abc_Cex_t *pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fUseOne, int fAllFrames, int fVerbose)
Definition: bmcCexCut.c:461
Gia_Man_t * Gia_ManFromAigSimple(Aig_Man_t *p)
Definition: giaAig.c:171
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Definition: gia.h:95
Gia_Man_t* Bmc_GiaGenerateGiaAllFrames ( Gia_Man_t p,
Abc_Cex_t pCex,
Vec_Bit_t **  pvInits,
int  iFrBeg,
int  iFrEnd 
)

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

Synopsis [Generates all frames from G to the last one.]

Description []

SideEffects []

SeeAlso []

Definition at line 237 of file bmcCexCut.c.

238 {
239  Vec_Bit_t * vInitEnd;
240  Gia_Man_t * pNew, * pTemp;
241  Gia_Obj_t * pObj, * pObjRo, * pObjRi;
242  int f, i, k, iBitOld, iBit = 0, fCompl0, fCompl1;
243 
244  // skip trough the first iFrEnd frames
246  Gia_ManForEachRo( p, pObj, k )
247  pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
248  *pvInits = Vec_BitStart( Gia_ManRegNum(p) );
249  for ( i = 0; i < iFrEnd; i++ )
250  {
251  // remember values in frame iFrBeg
252  if ( i == iFrBeg )
253  Gia_ManForEachRo( p, pObjRo, k )
254  if ( pObjRo->fMark0 )
255  Vec_BitWriteEntry( *pvInits, k, 1 );
256  // simulate other values
257  Gia_ManForEachPi( p, pObj, k )
258  pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
259  Gia_ManForEachAnd( p, pObj, k )
260  pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
261  (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
262  Gia_ManForEachCo( p, pObj, k )
263  pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
264  Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
265  pObjRo->fMark0 = pObjRi->fMark0;
266  }
267  assert( i == iFrEnd );
268  vInitEnd = Vec_BitStart( Gia_ManRegNum(p) );
269  Gia_ManForEachRo( p, pObjRo, k )
270  if ( pObjRo->fMark0 )
271  Vec_BitWriteEntry( vInitEnd, k, 1 );
272 
273  // create new AIG manager
274  pNew = Gia_ManStart( 10000 );
275  pNew->pName = Abc_UtilStrsav( p->pName );
276  Gia_ManForEachRo( p, pObjRo, k )
277  Gia_ManAppendCi(pNew);
278  Gia_ManHashStart( pNew );
279 
280  Gia_ManConst0(p)->Value = 1;
281  Gia_ManForEachPi( p, pObj, k )
282  pObj->Value = 1;
283 
284  iBitOld = iBit;
285  for ( f = iFrEnd; f <= pCex->iFrame; f++ )
286  {
287  // set up correct init state
288  Gia_ManForEachRo( p, pObjRo, k )
289  pObjRo->fMark0 = Vec_BitEntry( vInitEnd, k );
290  // simulate it for a few frames
291  iBit = iBitOld;
292  for ( i = iFrEnd; i < f; i++ )
293  {
294  Gia_ManForEachPi( p, pObj, k )
295  pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
296  Gia_ManForEachAnd( p, pObj, k )
297  pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
298  (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
299  Gia_ManForEachCo( p, pObj, k )
300  pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
301  Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
302  pObjRo->fMark0 = pObjRi->fMark0;
303  }
304  // start creating values
305  Gia_ManForEachRo( p, pObjRo, k )
306  pObjRo->Value = Abc_LitNotCond( Gia_Obj2Lit(pNew, Gia_ManPi(pNew, k)), !pObjRo->fMark0 );
307  for ( i = f; i <= pCex->iFrame; i++ )
308  {
309  Gia_ManForEachPi( p, pObj, k )
310  pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
311  Gia_ManForEachAnd( p, pObj, k )
312  {
313  fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
314  fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
315  pObj->fMark0 = fCompl0 & fCompl1;
316  if ( pObj->fMark0 )
317  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
318  else if ( !fCompl0 && !fCompl1 )
319  pObj->Value = Gia_ManHashOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
320  else if ( !fCompl0 )
321  pObj->Value = Gia_ObjFanin0(pObj)->Value;
322  else if ( !fCompl1 )
323  pObj->Value = Gia_ObjFanin1(pObj)->Value;
324  else assert( 0 );
325  assert( pObj->Value > 0 );
326  }
327  Gia_ManForEachCo( p, pObj, k )
328  {
329  pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
330  pObj->Value = Gia_ObjFanin0(pObj)->Value;
331  assert( pObj->Value > 0 );
332  }
333  if ( i == pCex->iFrame )
334  break;
335  Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
336  {
337  pObjRo->fMark0 = pObjRi->fMark0;
338  pObjRo->Value = pObjRi->Value;
339  }
340  }
341  assert( iBit == pCex->nBits );
342  // create PO
343  Gia_ManAppendCo( pNew, Gia_ManPo(p, pCex->iPo)->Value );
344  }
345  Gia_ManHashStop( pNew );
346  Vec_BitFree( vInitEnd );
347 
348  // cleanup
349  pNew = Gia_ManCleanup( pTemp = pNew );
350  Gia_ManStop( pTemp );
351  return pNew;
352 }
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition: giaUtil.c:215
static void Vec_BitWriteEntry(Vec_Bit_t *p, int i, int Entry)
Definition: vecBit.h:304
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
for(p=first;p->value< newval;p=p->next)
Definition: gia.h:75
typedefABC_NAMESPACE_HEADER_START struct Vec_Bit_t_ Vec_Bit_t
INCLUDES ///.
Definition: vecBit.h:42
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition: gia.h:1042
static Vec_Bit_t * Vec_BitStart(int nSize)
Definition: vecBit.h:102
static Gia_Obj_t * Gia_ManPi(Gia_Man_t *p, int v)
Definition: gia.h:405
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
if(last==0)
Definition: sparse_int.h:34
void Gia_ManHashStart(Gia_Man_t *p)
Definition: giaHash.c:117
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
unsigned fMark0
Definition: gia.h:79
Definition: gia.h:95
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
static int Vec_BitEntry(Vec_Bit_t *p, int i)
Definition: vecBit.h:287
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
static void Vec_BitFree(Vec_Bit_t *p)
Definition: vecBit.h:167
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
int Gia_ManHashOr(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:611
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
static int Gia_Obj2Lit(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:433
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
Gia_Man_t* Bmc_GiaGenerateGiaAllOne ( Gia_Man_t p,
Abc_Cex_t pCex,
Vec_Bit_t **  pvInits,
int  iFrBeg,
int  iFrEnd 
)

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

Synopsis [Generates one frame.]

Description []

SideEffects []

SeeAlso []

Definition at line 365 of file bmcCexCut.c.

366 {
367  Gia_Man_t * pNew, * pTemp;
368  Gia_Obj_t * pObj, * pObjRo, * pObjRi;
369  int i, k, iBit = 0, fCompl0, fCompl1;
370 
371  // skip trough the first iFrEnd frames
373  Gia_ManForEachRo( p, pObj, k )
374  pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
375  *pvInits = Vec_BitStart( Gia_ManRegNum(p) );
376  for ( i = 0; i < iFrEnd; i++ )
377  {
378  // remember values in frame iFrBeg
379  if ( i == iFrBeg )
380  Gia_ManForEachRo( p, pObjRo, k )
381  if ( pObjRo->fMark0 )
382  Vec_BitWriteEntry( *pvInits, k, 1 );
383  // simulate other values
384  Gia_ManForEachPi( p, pObj, k )
385  pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
386  Gia_ManForEachAnd( p, pObj, k )
387  pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
388  (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
389  Gia_ManForEachCo( p, pObj, k )
390  pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
391  Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
392  pObjRo->fMark0 = pObjRi->fMark0;
393  }
394  assert( i == iFrEnd );
395 
396  // create new AIG manager
397  pNew = Gia_ManStart( 10000 );
398  pNew->pName = Abc_UtilStrsav( p->pName );
399  Gia_ManConst0(p)->Value = 1;
400  Gia_ManForEachPi( p, pObj, k )
401  pObj->Value = 1;
402  Gia_ManForEachRo( p, pObjRo, k )
403  pObjRo->Value = Abc_LitNotCond( Gia_ManAppendCi(pNew), !pObjRo->fMark0 );
404  Gia_ManHashStart( pNew );
405  for ( i = iFrEnd; i <= pCex->iFrame; i++ )
406  {
407  Gia_ManForEachPi( p, pObj, k )
408  pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
409  Gia_ManForEachAnd( p, pObj, k )
410  {
411  fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
412  fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
413  pObj->fMark0 = fCompl0 & fCompl1;
414  if ( pObj->fMark0 )
415  pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
416  else if ( !fCompl0 && !fCompl1 )
417  pObj->Value = Gia_ManHashOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
418  else if ( !fCompl0 )
419  pObj->Value = Gia_ObjFanin0(pObj)->Value;
420  else if ( !fCompl1 )
421  pObj->Value = Gia_ObjFanin1(pObj)->Value;
422  else assert( 0 );
423  assert( pObj->Value > 0 );
424  }
425  Gia_ManForEachCo( p, pObj, k )
426  {
427  pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
428  pObj->Value = Gia_ObjFanin0(pObj)->Value;
429  assert( pObj->Value > 0 );
430  }
431  if ( i == pCex->iFrame )
432  break;
433  Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
434  {
435  pObjRo->fMark0 = pObjRi->fMark0;
436  pObjRo->Value = pObjRi->Value;
437  }
438  }
439  Gia_ManHashStop( pNew );
440  assert( iBit == pCex->nBits );
441 
442  // create PO
443  Gia_ManAppendCo( pNew, Gia_ManPo(p, pCex->iPo)->Value );
444  // cleanup
445  pNew = Gia_ManCleanup( pTemp = pNew );
446  Gia_ManStop( pTemp );
447  return pNew;
448 }
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition: giaUtil.c:215
static void Vec_BitWriteEntry(Vec_Bit_t *p, int i, int Entry)
Definition: vecBit.h:304
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
for(p=first;p->value< newval;p=p->next)
Definition: gia.h:75
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition: gia.h:1042
static Vec_Bit_t * Vec_BitStart(int nSize)
Definition: vecBit.h:102
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
if(last==0)
Definition: sparse_int.h:34
void Gia_ManHashStart(Gia_Man_t *p)
Definition: giaHash.c:117
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
unsigned fMark0
Definition: gia.h:79
Definition: gia.h:95
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
#define assert(ex)
Definition: util_old.h:213
unsigned Value
Definition: gia.h:87
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
int Gia_ManHashOr(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:611
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
Gia_Man_t* Bmc_GiaGenerateGiaOne ( Gia_Man_t p,
Abc_Cex_t pCex,
Vec_Bit_t **  pvInits,
int  iFrBeg,
int  iFrEnd 
)

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

Synopsis []

Description []

SideEffects []

SeeAlso []

Definition at line 192 of file bmcCexCut.c.

193 {
194  Vec_Bit_t * vValues;
195  Vec_Bit_t * vJustis;
196  Gia_Man_t * pNew;
197  Gia_Obj_t * pObj;
198  int k, Cube = 1, Counter = 0;
199  Bmc_GiaGenerateJust( p, pCex, &vValues, &vJustis );
200  // collect flop values in frame iFrBeg
201  *pvInits = Vec_BitStart( Gia_ManRegNum(p) );
202  Gia_ManForEachRo( p, pObj, k )
203  if ( Vec_BitEntry(vValues, Gia_ManObjNum(p) * iFrBeg + Gia_ObjId(p, pObj)) )
204  Vec_BitWriteEntry( *pvInits, k, 1 );
205  // create GIA with justified values in iFrEnd
206  pNew = Gia_ManStart( 2 * Gia_ManRegNum(p) + 2 );
207  pNew->pName = Abc_UtilStrsav( p->pName );
208  Gia_ManForEachRo( p, pObj, k )
209  {
210  int Literal = Gia_ManAppendCi(pNew);
211  if ( !Vec_BitEntry(vJustis, Gia_ManObjNum(p) * iFrEnd + Gia_ObjId(p, pObj)) )
212  continue;
213  if ( Vec_BitEntry(vValues, Gia_ManObjNum(p) * iFrEnd + Gia_ObjId(p, pObj)) )
214  Cube = Gia_ManAppendAnd( pNew, Cube, Literal );
215  else
216  Cube = Gia_ManAppendAnd( pNew, Cube, Abc_LitNot(Literal) );
217  Counter++;
218  }
219 // printf( "Only %d flops (out of %d) belong to the care set.\n", Counter, Gia_ManRegNum(p) );
220  Gia_ManAppendCo( pNew, Cube );
221  Vec_BitFree( vValues );
222  Vec_BitFree( vJustis );
223  return pNew;
224 }
static int Gia_ManAppendAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: gia.h:592
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
static void Vec_BitWriteEntry(Vec_Bit_t *p, int i, int Entry)
Definition: vecBit.h:304
Definition: gia.h:75
typedefABC_NAMESPACE_HEADER_START struct Vec_Bit_t_ Vec_Bit_t
INCLUDES ///.
Definition: vecBit.h:42
static Vec_Bit_t * Vec_BitStart(int nSize)
Definition: vecBit.h:102
void Bmc_GiaGenerateJust(Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Bit_t **pvValues, Vec_Bit_t **pvJustis)
Definition: bmcCexCut.c:106
if(last==0)
Definition: sparse_int.h:34
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
static int Counter
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
Definition: gia.h:95
static int Vec_BitEntry(Vec_Bit_t *p, int i)
Definition: vecBit.h:287
static void Vec_BitFree(Vec_Bit_t *p)
Definition: vecBit.h:167
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387
void Bmc_GiaGenerateJust ( Gia_Man_t p,
Abc_Cex_t pCex,
Vec_Bit_t **  pvValues,
Vec_Bit_t **  pvJustis 
)

Definition at line 106 of file bmcCexCut.c.

107 {
108  Vec_Bit_t * vValues = Vec_BitStart( Gia_ManObjNum(p) * (pCex->iFrame + 1) );
109  Vec_Bit_t * vJustis = Vec_BitStart( Gia_ManObjNum(p) * (pCex->iFrame + 1) );
110  Gia_Obj_t * pObj;
111  int i, k, iBit = 0, fCompl0, fCompl1, fJusti0, fJusti1, Shift;
112 
115  Gia_ManForEachRi( p, pObj, k )
116  pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
117  for ( Shift = i = 0; i <= pCex->iFrame; i++, Shift += Gia_ManObjNum(p) )
118  {
119  Gia_ManForEachObj( p, pObj, k )
120  {
121  if ( Gia_ObjIsAnd(pObj) )
122  {
123  fCompl0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
124  fCompl1 = Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj);
125  fJusti0 = Gia_ObjFanin0(pObj)->fMark1;
126  fJusti1 = Gia_ObjFanin1(pObj)->fMark1;
127  pObj->fMark0 = fCompl0 & fCompl1;
128  if ( pObj->fMark0 )
129  pObj->fMark1 = fJusti0 & fJusti1;
130  else if ( !fCompl0 && !fCompl1 )
131  pObj->fMark1 = fJusti0 | fJusti1;
132  else if ( !fCompl0 )
133  pObj->fMark1 = fJusti0;
134  else if ( !fCompl1 )
135  pObj->fMark1 = fJusti1;
136  else assert( 0 );
137  }
138  else if ( Gia_ObjIsCi(pObj) )
139  {
140  if ( Gia_ObjIsPi(p, pObj) )
141  {
142  pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++);
143  pObj->fMark1 = 1;
144  }
145  else
146  {
147  pObj->fMark0 = Gia_ObjRoToRi(p, pObj)->fMark0;
148  pObj->fMark1 = Gia_ObjRoToRi(p, pObj)->fMark1;
149  }
150  }
151  else if ( Gia_ObjIsCo(pObj) )
152  {
153  pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
154  pObj->fMark1 = Gia_ObjFanin0(pObj)->fMark1;
155  }
156  else if ( Gia_ObjIsConst0(pObj) )
157  pObj->fMark1 = 1;
158  else assert( 0 );
159  if ( pObj->fMark0 )
160  Vec_BitWriteEntry( vValues, Shift + k, 1 );
161  if ( pObj->fMark1 )
162  Vec_BitWriteEntry( vJustis, Shift + k, 1 );
163  }
164  }
165  assert( iBit == pCex->nBits );
168  // perform backward traversal to mark just nodes
169  pObj = Gia_ManPo( p, pCex->iPo );
170  assert( Vec_BitEntry(vJustis, Gia_ManObjNum(p) * pCex->iFrame + Gia_ObjId(p, pObj)) == 0 );
171 // Bmc_GiaGenerateJust_rec( p, pCex->iFrame, Gia_ObjId(p, pObj), vValues, vJustis );
172  Vec_BitWriteEntry(vJustis, Gia_ManObjNum(p) * pCex->iFrame + Gia_ObjId(p, pObj), 1);
173  Bmc_GiaGenerateJustNonRec( p, pCex->iFrame, vValues, vJustis );
174  assert( Vec_BitEntry(vJustis, Gia_ManObjNum(p) * pCex->iFrame + Gia_ObjId(p, pObj)) == 1 );
175 
176  // return the result
177  *pvValues = vValues;
178  *pvJustis = vJustis;
179 }
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition: giaUtil.c:215
static int Gia_ObjIsConst0(Gia_Obj_t *pObj)
Definition: gia.h:430
unsigned fMark1
Definition: gia.h:84
static void Vec_BitWriteEntry(Vec_Bit_t *p, int i, int Entry)
Definition: vecBit.h:304
for(p=first;p->value< newval;p=p->next)
Definition: gia.h:75
void Gia_ManCleanMark1(Gia_Man_t *p)
Definition: giaUtil.c:272
typedefABC_NAMESPACE_HEADER_START struct Vec_Bit_t_ Vec_Bit_t
INCLUDES ///.
Definition: vecBit.h:42
static Vec_Bit_t * Vec_BitStart(int nSize)
Definition: vecBit.h:102
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
static Gia_Obj_t * Gia_ObjRoToRi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:446
void Bmc_GiaGenerateJustNonRec(Gia_Man_t *p, int iFrame, Vec_Bit_t *vValues, Vec_Bit_t *vJustis)
Definition: bmcCexCut.c:74
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
unsigned fMark0
Definition: gia.h:79
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
static int Vec_BitEntry(Vec_Bit_t *p, int i)
Definition: vecBit.h:287
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
#define assert(ex)
Definition: util_old.h:213
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441
ABC_NAMESPACE_IMPL_START int Bmc_GiaGenerateJust_rec ( Gia_Man_t p,
int  iFrame,
int  iObj,
Vec_Bit_t vValues,
Vec_Bit_t vJustis 
)

DECLARATIONS ///.

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

FileName [bmcCexCut.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis [Derives characterization of bad states.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

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

Synopsis [Generate justifying assignments.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file bmcCexCut.c.

47 {
48  Gia_Obj_t * pObj;
49  int Shift = Gia_ManObjNum(p) * iFrame;
50  if ( iFrame < 0 )
51  return 0;
52  assert( iFrame >= 0 );
53  if ( Vec_BitEntry( vJustis, Shift + iObj ) )
54  return 0;
55  Vec_BitWriteEntry( vJustis, Shift + iObj, 1 );
56  pObj = Gia_ManObj( p, iObj );
57  if ( Gia_ObjIsCo(pObj) )
58  return Bmc_GiaGenerateJust_rec( p, iFrame, Gia_ObjFaninId0(pObj, iObj), vValues, vJustis );
59  if ( Gia_ObjIsCi(pObj) )
60  return Bmc_GiaGenerateJust_rec( p, iFrame-1, Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)), vValues, vJustis );
61  assert( Gia_ObjIsAnd(pObj) );
62  if ( Vec_BitEntry( vValues, Shift + iObj ) )
63  {
64  Bmc_GiaGenerateJust_rec( p, iFrame, Gia_ObjFaninId0(pObj, iObj), vValues, vJustis );
65  Bmc_GiaGenerateJust_rec( p, iFrame, Gia_ObjFaninId1(pObj, iObj), vValues, vJustis );
66  }
67  else if ( Vec_BitEntry( vValues, Shift + Gia_ObjFaninId0(pObj, iObj) ) == Gia_ObjFaninC0(pObj) )
68  Bmc_GiaGenerateJust_rec( p, iFrame, Gia_ObjFaninId0(pObj, iObj), vValues, vJustis );
69  else if ( Vec_BitEntry( vValues, Shift + Gia_ObjFaninId1(pObj, iObj) ) == Gia_ObjFaninC1(pObj) )
70  Bmc_GiaGenerateJust_rec( p, iFrame, Gia_ObjFaninId1(pObj, iObj), vValues, vJustis );
71  else assert( 0 );
72  return 0;
73 }
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
static void Vec_BitWriteEntry(Vec_Bit_t *p, int i, int Entry)
Definition: vecBit.h:304
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Definition: gia.h:75
ABC_NAMESPACE_IMPL_START int Bmc_GiaGenerateJust_rec(Gia_Man_t *p, int iFrame, int iObj, Vec_Bit_t *vValues, Vec_Bit_t *vJustis)
DECLARATIONS ///.
Definition: bmcCexCut.c:46
static Gia_Obj_t * Gia_ObjRoToRi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:446
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
static int Vec_BitEntry(Vec_Bit_t *p, int i)
Definition: vecBit.h:287
#define assert(ex)
Definition: util_old.h:213
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:461
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
void Bmc_GiaGenerateJustNonRec ( Gia_Man_t p,
int  iFrame,
Vec_Bit_t vValues,
Vec_Bit_t vJustis 
)

Definition at line 74 of file bmcCexCut.c.

75 {
76  Gia_Obj_t * pObj;
77  int i, k, Shift = Gia_ManObjNum(p) * iFrame;
78  for ( i = iFrame; i >= 0; i--, Shift -= Gia_ManObjNum(p) )
79  {
80  Gia_ManForEachObjReverse( p, pObj, k )
81  {
82  if ( k == 0 || Gia_ObjIsPi(p, pObj) )
83  continue;
84  if ( !Vec_BitEntry( vJustis, Shift + k ) )
85  continue;
86  if ( Gia_ObjIsAnd(pObj) )
87  {
88  if ( Vec_BitEntry( vValues, Shift + k ) )
89  {
90  Vec_BitWriteEntry( vJustis, Shift + Gia_ObjFaninId0(pObj, k), 1 );
91  Vec_BitWriteEntry( vJustis, Shift + Gia_ObjFaninId1(pObj, k), 1 );
92  }
93  else if ( Vec_BitEntry( vValues, Shift + Gia_ObjFaninId0(pObj, k) ) == Gia_ObjFaninC0(pObj) )
94  Vec_BitWriteEntry( vJustis, Shift + Gia_ObjFaninId0(pObj, k), 1 );
95  else if ( Vec_BitEntry( vValues, Shift + Gia_ObjFaninId1(pObj, k) ) == Gia_ObjFaninC1(pObj) )
96  Vec_BitWriteEntry( vJustis, Shift + Gia_ObjFaninId1(pObj, k), 1 );
97  else assert( 0 );
98  }
99  else if ( Gia_ObjIsCo(pObj) )
100  Vec_BitWriteEntry( vJustis, Shift + Gia_ObjFaninId0(pObj, k), 1 );
101  else if ( Gia_ObjIsCi(pObj) && i )
102  Vec_BitWriteEntry( vJustis, Shift - Gia_ManObjNum(p) + Gia_ObjId(p, Gia_ObjRoToRi(p, pObj)), 1 );
103  }
104  }
105 }
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
#define Gia_ManForEachObjReverse(p, pObj, i)
Definition: gia.h:994
static void Vec_BitWriteEntry(Vec_Bit_t *p, int i, int Entry)
Definition: vecBit.h:304
Definition: gia.h:75
static Gia_Obj_t * Gia_ObjRoToRi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:446
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
static int Vec_BitEntry(Vec_Bit_t *p, int i)
Definition: vecBit.h:287
#define assert(ex)
Definition: util_old.h:213
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:461
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441
Gia_Man_t* Bmc_GiaTargetStates ( Gia_Man_t p,
Abc_Cex_t pCex,
int  iFrBeg,
int  iFrEnd,
int  fCombOnly,
int  fUseOne,
int  fAllFrames,
int  fVerbose 
)

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

Synopsis [Generate GIA for target bad states.]

Description []

SideEffects []

SeeAlso []

Definition at line 461 of file bmcCexCut.c.

462 {
463  Gia_Man_t * pNew, * pTemp;
464  Vec_Bit_t * vInitNew;
465 
466  if ( iFrBeg < 0 )
467  { printf( "Starting frame is less than 0.\n" ); return NULL; }
468  if ( iFrEnd < 0 )
469  { printf( "Stopping frame is less than 0.\n" ); return NULL; }
470  if ( iFrBeg > pCex->iFrame )
471  { printf( "Starting frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
472  if ( iFrEnd > pCex->iFrame )
473  { printf( "Stopping frame is more than the last frame of CEX (%d).\n", pCex->iFrame ); return NULL; }
474  if ( iFrBeg > iFrEnd )
475  { printf( "Starting frame (%d) should be less than stopping frame (%d).\n", iFrBeg, iFrEnd ); return NULL; }
476  assert( iFrBeg >= 0 && iFrBeg <= pCex->iFrame );
477  assert( iFrEnd >= 0 && iFrEnd <= pCex->iFrame );
478  assert( iFrBeg < iFrEnd );
479 
480  if ( fUseOne )
481  pNew = Bmc_GiaGenerateGiaOne( p, pCex, &vInitNew, iFrBeg, iFrEnd );
482  else if ( fAllFrames )
483  pNew = Bmc_GiaGenerateGiaAllFrames( p, pCex, &vInitNew, iFrBeg, iFrEnd );
484  else
485  pNew = Bmc_GiaGenerateGiaAllOne( p, pCex, &vInitNew, iFrBeg, iFrEnd );
486 
487  if ( !fCombOnly )
488  {
489  // create new GIA
490  pNew = Gia_ManDupWithNewPo( p, pTemp = pNew );
491  Gia_ManStop( pTemp );
492 
493  // create new initial state
494  pNew = Gia_ManDupFlip( pTemp = pNew, Vec_BitArray(vInitNew) );
495  Gia_ManStop( pTemp );
496  }
497 
498  Vec_BitFree( vInitNew );
499  return pNew;
500 }
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
typedefABC_NAMESPACE_HEADER_START struct Vec_Bit_t_ Vec_Bit_t
INCLUDES ///.
Definition: vecBit.h:42
static int * Vec_BitArray(Vec_Bit_t *p)
Definition: vecBit.h:223
Gia_Man_t * Gia_ManDupWithNewPo(Gia_Man_t *p1, Gia_Man_t *p2)
Definition: giaDup.c:1816
Gia_Man_t * Gia_ManDupFlip(Gia_Man_t *p, int *pInitState)
Definition: giaDup.c:460
Definition: gia.h:95
Gia_Man_t * Bmc_GiaGenerateGiaAllOne(Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Bit_t **pvInits, int iFrBeg, int iFrEnd)
Definition: bmcCexCut.c:365
static void Vec_BitFree(Vec_Bit_t *p)
Definition: vecBit.h:167
#define assert(ex)
Definition: util_old.h:213
Gia_Man_t * Bmc_GiaGenerateGiaAllFrames(Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Bit_t **pvInits, int iFrBeg, int iFrEnd)
Definition: bmcCexCut.c:237
Gia_Man_t * Bmc_GiaGenerateGiaOne(Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Bit_t **pvInits, int iFrBeg, int iFrEnd)
Definition: bmcCexCut.c:192