abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
bmcCexCut.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [bmcCexCut.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [SAT-based bounded model checking.]
8 
9  Synopsis [Derives characterization of bad states.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: bmcCexCut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "bmc.h"
22 #include "aig/gia/giaAig.h"
23 
24 ABC_NAMESPACE_IMPL_START
25 
26 
27 ////////////////////////////////////////////////////////////////////////
28 /// DECLARATIONS ///
29 ////////////////////////////////////////////////////////////////////////
30 
31 ////////////////////////////////////////////////////////////////////////
32 /// FUNCTION DEFINITIONS ///
33 ////////////////////////////////////////////////////////////////////////
34 
35 /**Function*************************************************************
36 
37  Synopsis [Generate justifying assignments.]
38 
39  Description []
40 
41  SideEffects []
42 
43  SeeAlso []
44 
45 ***********************************************************************/
46 int Bmc_GiaGenerateJust_rec( Gia_Man_t * p, int iFrame, int iObj, Vec_Bit_t * vValues, Vec_Bit_t * vJustis )
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 }
74 void Bmc_GiaGenerateJustNonRec( Gia_Man_t * p, int iFrame, Vec_Bit_t * vValues, Vec_Bit_t * vJustis )
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 }
106 void Bmc_GiaGenerateJust( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** pvValues, Vec_Bit_t ** pvJustis )
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 
113  Gia_ManCleanMark0(p);
114  Gia_ManCleanMark1(p);
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 );
166  Gia_ManCleanMark0(p);
167  Gia_ManCleanMark1(p);
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 }
180 
181 /**Function*************************************************************
182 
183  Synopsis []
184 
185  Description []
186 
187  SideEffects []
188 
189  SeeAlso []
190 
191 ***********************************************************************/
192 Gia_Man_t * Bmc_GiaGenerateGiaOne( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** pvInits, int iFrBeg, int iFrEnd )
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 }
225 
226 /**Function*************************************************************
227 
228  Synopsis [Generates all frames from G to the last one.]
229 
230  Description []
231 
232  SideEffects []
233 
234  SeeAlso []
235 
236 ***********************************************************************/
237 Gia_Man_t * Bmc_GiaGenerateGiaAllFrames( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** pvInits, int iFrBeg, int iFrEnd )
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
245  Gia_ManCleanMark0(p);
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 }
353 
354 /**Function*************************************************************
355 
356  Synopsis [Generates one frame.]
357 
358  Description []
359 
360  SideEffects []
361 
362  SeeAlso []
363 
364 ***********************************************************************/
365 Gia_Man_t * Bmc_GiaGenerateGiaAllOne( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Bit_t ** pvInits, int iFrBeg, int iFrEnd )
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
372  Gia_ManCleanMark0(p);
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 }
449 
450 /**Function*************************************************************
451 
452  Synopsis [Generate GIA for target bad states.]
453 
454  Description []
455 
456  SideEffects []
457 
458  SeeAlso []
459 
460 ***********************************************************************/
461 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 )
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 }
501 
502 /**Function*************************************************************
503 
504  Synopsis [Generate AIG for target bad states.]
505 
506  Description []
507 
508  SideEffects []
509 
510  SeeAlso []
511 
512 ***********************************************************************/
513 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 )
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 }
530 
531 ////////////////////////////////////////////////////////////////////////
532 /// END OF FILE ///
533 ////////////////////////////////////////////////////////////////////////
534 
535 
536 ABC_NAMESPACE_IMPL_END
537 
Gia_ManAppendAnd
static int Gia_ManAppendAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: gia.h:592
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition: giaMan.c:77
Gia_ManToAigSimple
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition: giaAig.c:367
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition: gia.h:1022
Gia_ManVerifyCex
int Gia_ManVerifyCex(Gia_Man_t *pAig, Abc_Cex_t *p, int fDualOut)
DECLARATIONS ///.
Definition: giaCex.c:44
Gia_ObjFaninC1
static int Gia_ObjFaninC1(Gia_Obj_t *pObj)
Definition: gia.h:452
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
Gia_ManAppendCo
static int Gia_ManAppendCo(Gia_Man_t *p, int iLit0)
Definition: gia.h:703
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
Gia_ManPo
static Gia_Obj_t * Gia_ManPo(Gia_Man_t *p, int v)
Definition: gia.h:406
Gia_ManAppendCi
static int Gia_ManAppendCi(Gia_Man_t *p)
Definition: gia.h:583
Gia_ManCleanMark0
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition: giaUtil.c:215
Gia_ObjIsConst0
static int Gia_ObjIsConst0(Gia_Obj_t *pObj)
Definition: gia.h:430
Bmc_GiaTargetStates
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_ManFromAigSimple
Gia_Man_t * Gia_ManFromAigSimple(Aig_Man_t *p)
Definition: giaAig.c:171
Gia_ManForEachObjReverse
#define Gia_ManForEachObjReverse(p, pObj, i)
Definition: gia.h:994
Gia_Obj_t_::fMark1
unsigned fMark1
Definition: gia.h:84
Vec_BitWriteEntry
static void Vec_BitWriteEntry(Vec_Bit_t *p, int i, int Entry)
Definition: vecBit.h:304
Gia_ManObj
static Gia_Obj_t * Gia_ManObj(Gia_Man_t *p, int v)
Definition: gia.h:402
Abc_LitNotCond
static int Abc_LitNotCond(int Lit, int c)
Definition: abc_global.h:267
Gia_Obj_t_
Definition: gia.h:75
Gia_ManCleanMark1
void Gia_ManCleanMark1(Gia_Man_t *p)
Definition: giaUtil.c:272
Vec_Bit_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Bit_t_ Vec_Bit_t
INCLUDES ///.
Definition: vecBit.h:42
Vec_BitArray
static int * Vec_BitArray(Vec_Bit_t *p)
Definition: vecBit.h:223
Gia_ManForEachRiRo
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition: gia.h:1042
Vec_BitStart
static Vec_Bit_t * Vec_BitStart(int nSize)
Definition: vecBit.h:102
Gia_ManPi
static Gia_Obj_t * Gia_ManPi(Gia_Man_t *p, int v)
Definition: gia.h:405
Gia_ObjFanin0
static Gia_Obj_t * Gia_ObjFanin0(Gia_Obj_t *pObj)
Definition: gia.h:454
Gia_Man_t_::pName
char * pName
Definition: gia.h:97
Bmc_AigTargetStates
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)
Definition: bmcCexCut.c:513
Bmc_GiaGenerateJust_rec
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
Gia_ObjRoToRi
static Gia_Obj_t * Gia_ObjRoToRi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:446
Gia_ManDupWithNewPo
Gia_Man_t * Gia_ManDupWithNewPo(Gia_Man_t *p1, Gia_Man_t *p2)
Definition: giaDup.c:1816
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Bmc_GiaGenerateJust
void Bmc_GiaGenerateJust(Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Bit_t **pvValues, Vec_Bit_t **pvJustis)
Definition: bmcCexCut.c:106
Bmc_GiaGenerateJustNonRec
void Bmc_GiaGenerateJustNonRec(Gia_Man_t *p, int iFrame, Vec_Bit_t *vValues, Vec_Bit_t *vJustis)
Definition: bmcCexCut.c:74
Gia_ManHashStart
void Gia_ManHashStart(Gia_Man_t *p)
Definition: giaHash.c:117
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
DECLARATIONS ///.
Definition: giaMan.c:52
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition: gia.h:1002
Gia_ObjId
static int Gia_ObjId(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:410
Counter
static int Counter
Definition: extraBddMisc.c:1877
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition: gia.h:1034
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Gia_ObjIsCo
static int Gia_ObjIsCo(Gia_Obj_t *pObj)
Definition: gia.h:421
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Abc_LitNot
static int Abc_LitNot(int Lit)
Definition: abc_global.h:266
Gia_Obj_t_::fMark0
unsigned fMark0
Definition: gia.h:79
Gia_ManDupFlip
Gia_Man_t * Gia_ManDupFlip(Gia_Man_t *p, int *pInitState)
Definition: giaDup.c:460
Gia_Man_t_
Definition: gia.h:95
Gia_ObjIsAnd
static int Gia_ObjIsAnd(Gia_Obj_t *pObj)
Definition: gia.h:422
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition: gia.h:984
Gia_ManConst0
static Gia_Obj_t * Gia_ManConst0(Gia_Man_t *p)
Definition: gia.h:400
Vec_BitEntry
static int Vec_BitEntry(Vec_Bit_t *p, int i)
Definition: vecBit.h:287
Gia_ObjFanin1
static Gia_Obj_t * Gia_ObjFanin1(Gia_Obj_t *pObj)
Definition: gia.h:455
Bmc_GiaGenerateGiaAllOne
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
Vec_BitFree
static void Vec_BitFree(Vec_Bit_t *p)
Definition: vecBit.h:167
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition: gia.h:1038
assert
#define assert(ex)
Definition: util_old.h:213
Gia_Obj_t_::Value
unsigned Value
Definition: gia.h:87
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition: gia.h:1040
Bmc_GiaGenerateGiaAllFrames
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_ObjFaninC0
static int Gia_ObjFaninC0(Gia_Obj_t *pObj)
Definition: gia.h:451
Gia_ObjIsCi
static int Gia_ObjIsCi(Gia_Obj_t *pObj)
Definition: gia.h:420
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition: giaScl.c:84
Abc_UtilStrsav
char * Abc_UtilStrsav(char *s)
Definition: starter.c:47
Gia_ObjFaninId1
static int Gia_ObjFaninId1(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:461
Gia_ManHashOr
int Gia_ManHashOr(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:611
Bmc_GiaGenerateGiaOne
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
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition: giaHash.c:572
Gia_Obj2Lit
static int Gia_Obj2Lit(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:433
Gia_ManObjNum
static int Gia_ManObjNum(Gia_Man_t *p)
Definition: gia.h:388
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition: giaHash.c:142
Gia_ObjFaninId0
static int Gia_ObjFaninId0(Gia_Obj_t *pObj, int ObjId)
Definition: gia.h:460
Gia_ObjIsPi
static int Gia_ObjIsPi(Gia_Man_t *p, Gia_Obj_t *pObj)
Definition: gia.h:441
Gia_ManRegNum
static int Gia_ManRegNum(Gia_Man_t *p)
Definition: gia.h:387