ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
Functions
bmcCexCut.c File Reference
#include "bmc.h"
#include "aig/gia/giaAig.h"
Include dependency graph for bmcCexCut.c:

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 ///.
 
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_t * Bmc_GiaGenerateGiaOne (Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Bit_t **pvInits, int iFrBeg, int iFrEnd)
 
Gia_Man_t * Bmc_GiaGenerateGiaAllFrames (Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Bit_t **pvInits, int iFrBeg, int iFrEnd)
 
Gia_Man_t * Bmc_GiaGenerateGiaAllOne (Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Bit_t **pvInits, int iFrBeg, int iFrEnd)
 
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)
 
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 Documentation

◆ 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 )

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}
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
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
p
Cube * p
Definition exorList.c:222
Gia_ManToAigSimple
Aig_Man_t * Gia_ManToAigSimple(Gia_Man_t *p)
Definition giaAig.c:408
Gia_ManFromAigSimple
Gia_Man_t * Gia_ManFromAigSimple(Aig_Man_t *p)
Definition giaAig.c:212
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
Gia_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
Gia_ManVerifyCex
int Gia_ManVerifyCex(Gia_Man_t *pAig, Abc_Cex_t *p, int fDualOut)
DECLARATIONS ///.
Definition giaCex.c:48
Here is the call graph for this function:

◆ Bmc_GiaGenerateGiaAllFrames()

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
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}
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition gia.h:1252
Gia_ManHashStart
void Gia_ManHashStart(Gia_Man_t *p)
Definition giaHash.c:125
Gia_ManForEachAnd
#define Gia_ManForEachAnd(p, pObj, i)
Definition gia.h:1214
Gia_ManForEachPi
#define Gia_ManForEachPi(p, pObj, i)
Definition gia.h:1248
Gia_ManStart
Gia_Man_t * Gia_ManStart(int nObjsMax)
FUNCTION DEFINITIONS ///.
Definition giaMan.c:57
Gia_ManHashOr
int Gia_ManHashOr(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:621
Gia_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManCleanup
Gia_Man_t * Gia_ManCleanup(Gia_Man_t *p)
Definition giaScl.c:84
Gia_ManCleanMark0
void Gia_ManCleanMark0(Gia_Man_t *p)
Definition giaUtil.c:256
Gia_ManHashAnd
int Gia_ManHashAnd(Gia_Man_t *p, int iLit0, int iLit1)
Definition giaHash.c:576
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Gia_ManForEachRiRo
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition gia.h:1256
Gia_ManHashStop
void Gia_ManHashStop(Gia_Man_t *p)
Definition giaHash.c:149
Gia_Man_t_::pName
char * pName
Definition gia.h:99
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Gia_Obj_t_::fMark0
unsigned fMark0
Definition gia.h:81
assert
#define assert(ex)
Definition util_old.h:213
Vec_Bit_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Bit_t_ Vec_Bit_t
INCLUDES ///.
Definition vecBit.h:42
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_GiaGenerateGiaAllOne()

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
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}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_GiaGenerateGiaOne()

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}
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
Cube
struct cube Cube
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_GiaGenerateJust()

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
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}
Bmc_GiaGenerateJustNonRec
void Bmc_GiaGenerateJustNonRec(Gia_Man_t *p, int iFrame, Vec_Bit_t *vValues, Vec_Bit_t *vJustis)
Definition bmcCexCut.c:74
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition gia.h:1190
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition gia.h:1254
Gia_ManCleanMark1
void Gia_ManCleanMark1(Gia_Man_t *p)
Definition giaUtil.c:313
Gia_Obj_t_::fMark1
unsigned fMark1
Definition gia.h:86
Here is the call graph for this function:
Here is the caller graph for this function:

◆ 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 ///.

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}
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
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_GiaGenerateJustNonRec()

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}
Gia_ManForEachObjReverse
#define Gia_ManForEachObjReverse(p, pObj, i)
Definition gia.h:1206
Here is the caller graph for this function:

◆ 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 )

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}
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
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
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_ManDupFlip
Gia_Man_t * Gia_ManDupFlip(Gia_Man_t *p, int *pInitState)
Definition giaDup.c:628
Gia_ManDupWithNewPo
Gia_Man_t * Gia_ManDupWithNewPo(Gia_Man_t *p1, Gia_Man_t *p2)
Definition giaDup.c:2634
Here is the call graph for this function:
Here is the caller graph for this function: