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

Go to the source code of this file.

Functions

ABC_NAMESPACE_IMPL_START Abc_Cex_t * Bmc_CexCareExtendToObjects (Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexCare)
 DECLARATIONS ///.
 
void Bmc_CexCarePropagateFwdOne (Gia_Man_t *p, Abc_Cex_t *pCex, int f, Vec_Int_t *vPriosIn)
 
void Bmc_CexCarePropagateFwd (Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Int_t *vPriosIn, Vec_Int_t *vPriosFf)
 
void Bmc_CexCarePropagateBwdOne (Gia_Man_t *p, Abc_Cex_t *pCex, int f, Abc_Cex_t *pCexMin)
 
Abc_Cex_t * Bmc_CexCarePropagateBwd (Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Int_t *vPriosIn, Vec_Int_t *vPriosFf)
 
Abc_Cex_t * Bmc_CexCareTotal (Abc_Cex_t **pCexes, int nCexes)
 
Abc_Cex_t * Bmc_CexCareMinimizeAig (Gia_Man_t *p, int nRealPis, Abc_Cex_t *pCex, int nTryCexes, int fCheck, int fVerbose)
 
Abc_Cex_t * Bmc_CexCareMinimize (Aig_Man_t *p, int nRealPis, Abc_Cex_t *pCex, int nTryCexes, int fCheck, int fVerbose)
 
Abc_Cex_t * Bmc_CexCareSatBasedMinimize (Aig_Man_t *p, int nRealPis, Abc_Cex_t *pCex, int fHighEffort, int fCheck, int fVerbose)
 
int Bmc_CexCareVerify (Aig_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexMin, int fVerbose)
 
int Bmc_CexCareVerifyAnyPo (Aig_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexMin, int fVerbose)
 

Function Documentation

◆ Bmc_CexCareExtendToObjects()

ABC_NAMESPACE_IMPL_START Abc_Cex_t * Bmc_CexCareExtendToObjects ( Gia_Man_t * p,
Abc_Cex_t * pCex,
Abc_Cex_t * pCexCare )

DECLARATIONS ///.

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

FileName [bmcCexCare.c]

SystemName [ABC: Logic synthesis and verification system.]

PackageName [SAT-based bounded model checking.]

Synopsis [Computing care set of the counter-example.]

Author [Alan Mishchenko]

Affiliation [UC Berkeley]

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

Revision [

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

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

Synopsis [Takes CEX and its care-set. Returns care-set of all objects.]

Description []

SideEffects []

SeeAlso []

Definition at line 46 of file bmcCexCare.c.

47{
48 Abc_Cex_t * pNew;
49 Gia_Obj_t * pObj;
50 int i, k;
51 assert( pCex->nPis == pCexCare->nPis );
52 assert( pCex->nRegs == pCexCare->nRegs );
53 assert( pCex->nBits == pCexCare->nBits );
54 // start the counter-example
55 pNew = Abc_CexAlloc( pCex->nRegs, Gia_ManObjNum(p), pCex->iFrame + 1 );
56 pNew->iFrame = pCex->iFrame;
57 pNew->iPo = pCex->iPo;
58 // initialize terminary simulation
59 Gia_ObjTerSimSet0( Gia_ManConst0(p) );
60 Gia_ManForEachRi( p, pObj, k )
61 Gia_ObjTerSimSet0( pObj );
62 for ( i = 0; i <= pCex->iFrame; i++ )
63 {
64 Gia_ManForEachPi( p, pObj, k )
65 {
66 if ( !Abc_InfoHasBit( pCexCare->pData, pCexCare->nRegs + i * pCexCare->nPis + k ) )
67 Gia_ObjTerSimSetX( pObj );
68 else if ( Abc_InfoHasBit( pCex->pData, pCex->nRegs + i * pCex->nPis + k ) )
69 Gia_ObjTerSimSet1( pObj );
70 else
71 Gia_ObjTerSimSet0( pObj );
72 }
73 Gia_ManForEachRo( p, pObj, k )
74 Gia_ObjTerSimRo( p, pObj );
75 Gia_ManForEachAnd( p, pObj, k )
76 Gia_ObjTerSimAnd( pObj );
77 Gia_ManForEachCo( p, pObj, k )
78 Gia_ObjTerSimCo( pObj );
79 // add cares to the exdended counter-example
80 Gia_ManForEachObj( p, pObj, k )
81 if ( !Gia_ObjTerSimGetX(pObj) )
82 Abc_InfoSetBit( pNew->pData, pNew->nRegs + pNew->nPis * i + k );
83 }
84 pObj = Gia_ManPo( p, pCex->iPo );
85 assert( Gia_ObjTerSimGet1(pObj) );
86 return pNew;
87}
p
Cube * p
Definition exorList.c:222
Gia_ManForEachRo
#define Gia_ManForEachRo(p, pObj, i)
Definition gia.h:1252
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_Obj_t
struct Gia_Obj_t_ Gia_Obj_t
Definition gia.h:76
Gia_ManForEachObj
#define Gia_ManForEachObj(p, pObj, i)
MACRO DEFINITIONS ///.
Definition gia.h:1190
Gia_ManForEachCo
#define Gia_ManForEachCo(p, pObj, i)
Definition gia.h:1236
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition gia.h:1254
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
assert
#define assert(ex)
Definition util_old.h:213
Here is the call graph for this function:

◆ Bmc_CexCareMinimize()

Abc_Cex_t * Bmc_CexCareMinimize ( Aig_Man_t * p,
int nRealPis,
Abc_Cex_t * pCex,
int nTryCexes,
int fCheck,
int fVerbose )

Definition at line 426 of file bmcCexCare.c.

427{
428 Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
429 Abc_Cex_t * pCexMin = Bmc_CexCareMinimizeAig( pGia, nRealPis, pCex, nTryCexes, fCheck, fVerbose );
430 Gia_ManStop( pGia );
431 return pCexMin;
432}
Bmc_CexCareMinimizeAig
Abc_Cex_t * Bmc_CexCareMinimizeAig(Gia_Man_t *p, int nRealPis, Abc_Cex_t *pCex, int nTryCexes, int fCheck, int fVerbose)
Definition bmcCexCare.c:254
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
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_CexCareMinimizeAig()

Abc_Cex_t * Bmc_CexCareMinimizeAig ( Gia_Man_t * p,
int nRealPis,
Abc_Cex_t * pCex,
int nTryCexes,
int fCheck,
int fVerbose )

Definition at line 254 of file bmcCexCare.c.

255{
256 //int nTryCexes = 4; // belongs to range [1;4]
257 Abc_Cex_t * pCexBest, * pCexMin[4] = {NULL};
258 int k, f, i, nOnesBest, nOnesCur, Counter = 0;
259 Vec_Int_t * vPriosIn, * vPriosFf;
260 if ( pCex->nPis != Gia_ManPiNum(p) )
261 {
262 printf( "Given CEX does to have same number of inputs as the AIG.\n" );
263 return NULL;
264 }
265 if ( pCex->nRegs != Gia_ManRegNum(p) )
266 {
267 printf( "Given CEX does to have same number of flops as the AIG.\n" );
268 return NULL;
269 }
270 if ( !(pCex->iPo >= 0 && pCex->iPo < Gia_ManPoNum(p)) )
271 {
272 printf( "Given CEX has PO whose index is out of range for the AIG.\n" );
273 return NULL;
274 }
275 assert( pCex->nPis == Gia_ManPiNum(p) );
276 assert( pCex->nRegs == Gia_ManRegNum(p) );
277 assert( pCex->iPo >= 0 && pCex->iPo < Gia_ManPoNum(p) );
278 if ( fVerbose )
279 {
280 printf( "Original : " );
281 Bmc_CexPrint( pCex, nRealPis, 0 );
282 }
283 vPriosIn = Vec_IntAlloc( pCex->nPis * (pCex->iFrame + 1) );
284 vPriosFf = Vec_IntAlloc( pCex->nRegs * (pCex->iFrame + 1) );
285 for ( k = 0; k < nTryCexes; k++ )
286 {
287 Counter = 0;
288 Vec_IntFill( vPriosIn, pCex->nPis * (pCex->iFrame + 1), 0 );
289/*
290 if ( k == 0 )
291 {
292 for ( f = 0; f <= pCex->iFrame; f++ )
293 for ( i = nRealPis; i < Gia_ManPiNum(p); i++ )
294 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
295 for ( f = 0; f <= pCex->iFrame; f++ )
296 for ( i = 0; i < nRealPis; i++ )
297 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
298 }
299 else if ( k == 1 )
300 {
301 for ( f = pCex->iFrame; f >= 0; f-- )
302 for ( i = nRealPis; i < Gia_ManPiNum(p); i++ )
303 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
304 for ( f = pCex->iFrame; f >= 0; f-- )
305 for ( i = 0; i < nRealPis; i++ )
306 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
307 }
308 else if ( k == 2 )
309 {
310 for ( f = 0; f <= pCex->iFrame; f++ )
311 for ( i = Gia_ManPiNum(p) - 1; i >= nRealPis; i-- )
312 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
313 for ( f = 0; f <= pCex->iFrame; f++ )
314 for ( i = nRealPis - 1; i >= 0; i-- )
315 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
316 }
317 else if ( k == 3 )
318 {
319 for ( f = pCex->iFrame; f >= 0; f-- )
320 for ( i = Gia_ManPiNum(p) - 1; i >= nRealPis; i-- )
321 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
322 for ( f = pCex->iFrame; f >= 0; f-- )
323 for ( i = nRealPis - 1; i >= 0; i-- )
324 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
325 }
326 else assert( 0 );
327*/
328 if ( k == 0 )
329 {
330 for ( f = pCex->iFrame; f >= 0; f-- )
331 for ( i = Gia_ManPiNum(p) - 1; i >= nRealPis; i-- )
332 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
333 for ( f = pCex->iFrame; f >= 0; f-- )
334 for ( i = nRealPis - 1; i >= 0; i-- )
335 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
336 }
337 else if ( k == 1 )
338 {
339 for ( f = pCex->iFrame; f >= 0; f-- )
340 for ( i = Gia_ManPiNum(p) - 1; i >= nRealPis; i-- )
341 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
342 for ( f = pCex->iFrame; f >= 0; f-- )
343 for ( i = 0; i < nRealPis; i++ )
344 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
345 }
346 else if ( k == 2 )
347 {
348 for ( f = pCex->iFrame; f >= 0; f-- )
349 for ( i = nRealPis; i < Gia_ManPiNum(p); i++ )
350 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
351 for ( f = pCex->iFrame; f >= 0; f-- )
352 for ( i = nRealPis - 1; i >= 0; i-- )
353 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
354 }
355 else if ( k == 3 )
356 {
357 for ( f = pCex->iFrame; f >= 0; f-- )
358 for ( i = nRealPis; i < Gia_ManPiNum(p); i++ )
359 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
360 for ( f = pCex->iFrame; f >= 0; f-- )
361 for ( i = 0; i < nRealPis; i++ )
362 Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
363 }
364 else assert( 0 );
365
366 assert( Counter == pCex->nPis * (pCex->iFrame + 1) );
367 Bmc_CexCarePropagateFwd( p, pCex, vPriosIn, vPriosFf );
368 assert( Vec_IntSize(vPriosFf) == pCex->nRegs * (pCex->iFrame + 1) );
369 if ( !Abc_LitIsCompl(Gia_ManPo(p, pCex->iPo)->Value) )
370 {
371 printf( "Counter-example is invalid.\n" );
372 Vec_IntFree( vPriosIn );
373 Vec_IntFree( vPriosFf );
374 return NULL;
375 }
376 pCexMin[k] = Bmc_CexCarePropagateBwd( p, pCex, vPriosIn, vPriosFf );
377 if ( fVerbose )
378 {
379 if ( k == 0 )
380 printf( "PI- PPI-: " );
381 else if ( k == 1 )
382 printf( "PI+ PPI-: " );
383 else if ( k == 2 )
384 printf( "PI- PPI+: " );
385 else if ( k == 3 )
386 printf( "PI+ PPI+: " );
387 else assert( 0 );
388 Bmc_CexPrint( pCexMin[k], nRealPis, 0 );
389 }
390 }
391 Vec_IntFree( vPriosIn );
392 Vec_IntFree( vPriosFf );
393 // select the best one
394 pCexBest = pCexMin[0];
395 nOnesBest = Abc_CexCountOnes(pCexMin[0]);
396 for ( k = 1; k < nTryCexes; k++ )
397 {
398 if ( pCexMin[k] == NULL )
399 continue;
400 nOnesCur = Abc_CexCountOnes(pCexMin[k]);
401 if ( nOnesBest > nOnesCur )
402 {
403 nOnesBest = nOnesCur;
404 pCexBest = pCexMin[k];
405 }
406 }
407 if ( fVerbose )
408 {
409 //Abc_Cex_t * pTotal = Bmc_CexCareTotal( pCexMin, nTryCexes );
410 printf( "Final : " );
411 Bmc_CexPrint( pCexBest, nRealPis, 0 );
412 //printf( "Total : " );
413 //Bmc_CexPrint( pTotal, nRealPis, 0 );
414 //Abc_CexFreeP( &pTotal );
415 }
416 for ( k = 0; k < nTryCexes; k++ )
417 if ( pCexMin[k] && pCexBest != pCexMin[k] )
418 Abc_CexFreeP( &pCexMin[k] );
419 // verify and return
420 if ( !Bmc_CexVerify( p, pCex, pCexBest ) )
421 printf( "Counter-example verification has failed.\n" );
422 else if ( fCheck )
423 printf( "Counter-example verification succeeded.\n" );
424 return pCexBest;
425}
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Bmc_CexCarePropagateFwd
void Bmc_CexCarePropagateFwd(Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Int_t *vPriosIn, Vec_Int_t *vPriosFf)
Definition bmcCexCare.c:128
Bmc_CexCarePropagateBwd
Abc_Cex_t * Bmc_CexCarePropagateBwd(Gia_Man_t *p, Abc_Cex_t *pCex, Vec_Int_t *vPriosIn, Vec_Int_t *vPriosFf)
Definition bmcCexCare.c:206
Bmc_CexPrint
void Bmc_CexPrint(Abc_Cex_t *pCex, int nRealPis, int fVerbose)
Definition bmcCexTools.c:307
Bmc_CexVerify
int Bmc_CexVerify(Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexCare)
Definition bmcCexTools.c:346
Abc_CexFreeP
void Abc_CexFreeP(Abc_Cex_t **p)
Definition utilCex.c:361
Abc_CexCountOnes
int Abc_CexCountOnes(Abc_Cex_t *p)
Definition utilCex.c:559
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_CexCarePropagateBwd()

Abc_Cex_t * Bmc_CexCarePropagateBwd ( Gia_Man_t * p,
Abc_Cex_t * pCex,
Vec_Int_t * vPriosIn,
Vec_Int_t * vPriosFf )

Definition at line 206 of file bmcCexCare.c.

207{
208 Abc_Cex_t * pCexMin;
209 Gia_Obj_t * pObjRo, * pObjRi;
210 int f, i;
211 pCexMin = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 );
212 pCexMin->iPo = pCex->iPo;
213 pCexMin->iFrame = pCex->iFrame;
214 Gia_ManForEachCo( p, pObjRi, i )
215 pObjRi->fPhase = 0;
216 for ( f = pCex->iFrame; f >= 0; f-- )
217 {
218 Gia_ManPo(p, pCex->iPo)->fPhase = (int)(f == pCex->iFrame);
219 Gia_ManForEachRo( p, pObjRo, i )
220 pObjRo->Value = Vec_IntEntry( vPriosFf, f * pCex->nRegs + i );
221 Bmc_CexCarePropagateFwdOne( p, pCex, f, vPriosIn );
222 Bmc_CexCarePropagateBwdOne( p, pCex, f, pCexMin );
223 Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
224 pObjRi->fPhase = pObjRo->fPhase;
225 }
226 return pCexMin;
227}
Bmc_CexCarePropagateFwdOne
void Bmc_CexCarePropagateFwdOne(Gia_Man_t *p, Abc_Cex_t *pCex, int f, Vec_Int_t *vPriosIn)
Definition bmcCexCare.c:100
Bmc_CexCarePropagateBwdOne
void Bmc_CexCarePropagateBwdOne(Gia_Man_t *p, Abc_Cex_t *pCex, int f, Abc_Cex_t *pCexMin)
Definition bmcCexCare.c:155
Gia_ManForEachRiRo
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition gia.h:1256
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Gia_Obj_t_::fPhase
unsigned fPhase
Definition gia.h:87
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_CexCarePropagateBwdOne()

void Bmc_CexCarePropagateBwdOne ( Gia_Man_t * p,
Abc_Cex_t * pCex,
int f,
Abc_Cex_t * pCexMin )

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

Synopsis [Backward propagation.]

Description []

SideEffects []

SeeAlso []

Definition at line 155 of file bmcCexCare.c.

156{
157 Gia_Obj_t * pObj, * pFan0, * pFan1;
158 int i, Phase0, Phase1;
159 Gia_ManForEachCi( p, pObj, i )
160 pObj->fPhase = 0;
161 Gia_ManForEachCo( p, pObj, i )
162 if ( pObj->fPhase )
163 Gia_ObjFanin0(pObj)->fPhase = 1;
164 Gia_ManForEachAndReverse( p, pObj, i )
165 {
166 if ( !pObj->fPhase )
167 continue;
168 pFan0 = Gia_ObjFanin0(pObj);
169 pFan1 = Gia_ObjFanin1(pObj);
170 Phase0 = Abc_LitIsCompl(pFan0->Value) ^ Gia_ObjFaninC0(pObj);
171 Phase1 = Abc_LitIsCompl(pFan1->Value) ^ Gia_ObjFaninC1(pObj);
172 if ( Phase0 && Phase1 )
173 {
174 pFan0->fPhase = 1;
175 pFan1->fPhase = 1;
176 }
177 else if ( Phase0 )
178 pFan1->fPhase = 1;
179 else if ( Phase1 )
180 pFan0->fPhase = 1;
181 else // if ( !Phase0 && !Phase1 )
182 {
183 if ( pFan0->fPhase || pFan1->fPhase )
184 continue;
185 if ( Gia_ObjIsPi(p, pFan0) )
186 pFan0->fPhase = 1;
187 else if ( Gia_ObjIsPi(p, pFan1) )
188 pFan1->fPhase = 1;
189// else if ( Gia_ObjIsAnd(pFan0) && Txs_ObjIsJust(p, pFan0) )
190// pFan0->fPhase = 1;
191// else if ( Gia_ObjIsAnd(pFan1) && Txs_ObjIsJust(p, pFan1) )
192// pFan1->fPhase = 1;
193 else
194 {
195 if ( Abc_Lit2Var(pFan0->Value) > Abc_Lit2Var(pFan1->Value) )
196 pFan0->fPhase = 1;
197 else
198 pFan1->fPhase = 1;
199 }
200 }
201 }
202 Gia_ManForEachPi( p, pObj, i )
203 if ( pObj->fPhase )
204 Abc_InfoSetBit( pCexMin->pData, pCexMin->nRegs + pCexMin->nPis * f + i );
205}
Gia_ManForEachAndReverse
#define Gia_ManForEachAndReverse(p, pObj, i)
Definition gia.h:1222
Gia_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
Here is the caller graph for this function:

◆ Bmc_CexCarePropagateFwd()

void Bmc_CexCarePropagateFwd ( Gia_Man_t * p,
Abc_Cex_t * pCex,
Vec_Int_t * vPriosIn,
Vec_Int_t * vPriosFf )

Definition at line 128 of file bmcCexCare.c.

129{
130 Gia_Obj_t * pObjRo, * pObjRi;
131 int i, f, ValueMax = Abc_Var2Lit( pCex->nPis * (pCex->iFrame + 1), 0 );
132 Gia_ManConst0( p )->Value = ValueMax;
133 Gia_ManForEachRi( p, pObjRi, i )
134 pObjRi->Value = ValueMax;
135 Vec_IntClear( vPriosFf );
136 for ( f = 0; f <= pCex->iFrame; f++ )
137 {
138 Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
139 Vec_IntPush( vPriosFf, (pObjRo->Value = pObjRi->Value) );
140 Bmc_CexCarePropagateFwdOne( p, pCex, f, vPriosIn );
141 }
142}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_CexCarePropagateFwdOne()

void Bmc_CexCarePropagateFwdOne ( Gia_Man_t * p,
Abc_Cex_t * pCex,
int f,
Vec_Int_t * vPriosIn )

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

Synopsis [Forward propagation.]

Description []

SideEffects []

SeeAlso []

Definition at line 100 of file bmcCexCare.c.

101{
102 Gia_Obj_t * pObj;
103 int Prio, Prio0, Prio1;
104 int i, Phase0, Phase1;
105 assert( Vec_IntSize(vPriosIn) == pCex->nPis * (pCex->iFrame + 1) );
106 Gia_ManForEachPi( p, pObj, i )
107 pObj->Value = Vec_IntEntry( vPriosIn, f * pCex->nPis + i );
108 Gia_ManForEachAnd( p, pObj, i )
109 {
110 Prio0 = Abc_Lit2Var(Gia_ObjFanin0(pObj)->Value);
111 Prio1 = Abc_Lit2Var(Gia_ObjFanin1(pObj)->Value);
112 Phase0 = Abc_LitIsCompl(Gia_ObjFanin0(pObj)->Value) ^ Gia_ObjFaninC0(pObj);
113 Phase1 = Abc_LitIsCompl(Gia_ObjFanin1(pObj)->Value) ^ Gia_ObjFaninC1(pObj);
114 if ( Phase0 && Phase1 )
115 Prio = Abc_MinInt(Prio0, Prio1);
116 else if ( Phase0 )
117 Prio = Prio1;
118 else if ( Phase1 )
119 Prio = Prio0;
120 else // if ( !Phase0 && !Phase1 )
121 Prio = Abc_MaxInt(Prio0, Prio1);
122 pObj->Value = Abc_Var2Lit( Prio, Phase0 && Phase1 );
123 pObj->fPhase = 0;
124 }
125 Gia_ManForEachCo( p, pObj, i )
126 pObj->Value = Abc_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );
127}
Here is the caller graph for this function:

◆ Bmc_CexCareSatBasedMinimize()

Abc_Cex_t * Bmc_CexCareSatBasedMinimize ( Aig_Man_t * p,
int nRealPis,
Abc_Cex_t * pCex,
int fHighEffort,
int fCheck,
int fVerbose )

Definition at line 433 of file bmcCexCare.c.

434{
435 Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
436 Abc_Cex_t * pCexMin = Bmc_CexCareSatBasedMinimizeAig( pGia, pCex, fHighEffort, fVerbose );
437 if ( pCexMin == NULL )
438 {
439 Gia_ManStop( pGia );
440 return NULL;
441 }
442 // unfortunately, cannot verify - ternary simulation does not work
443 Gia_ManStop( pGia );
444 return pCexMin;
445}
Bmc_CexCareSatBasedMinimizeAig
Abc_Cex_t * Bmc_CexCareSatBasedMinimizeAig(Gia_Man_t *p, Abc_Cex_t *pCex, int fHighEffort, int fVerbose)
Definition giaCex.c:517
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_CexCareTotal()

Abc_Cex_t * Bmc_CexCareTotal ( Abc_Cex_t ** pCexes,
int nCexes )

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

Synopsis [Computes the care set of the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 240 of file bmcCexCare.c.

241{
242 int i, k, nWords = Abc_BitWordNum( pCexes[0]->nBits );
243 Abc_Cex_t * pCexMin = Abc_CexAlloc( pCexes[0]->nRegs, pCexes[0]->nPis, pCexes[0]->iFrame + 1 );
244 pCexMin->iPo = pCexes[0]->iPo;
245 pCexMin->iFrame = pCexes[0]->iFrame;
246 for ( i = 0; i < nWords; i++ )
247 {
248 pCexMin->pData[i] = pCexes[0]->pData[i];
249 for ( k = 1; k < nCexes; k++ )
250 pCexMin->pData[i] &= pCexes[k]->pData[i];
251 }
252 return pCexMin;
253}
nWords
int nWords
Definition abcNpn.c:127
Here is the call graph for this function:

◆ Bmc_CexCareVerify()

int Bmc_CexCareVerify ( Aig_Man_t * p,
Abc_Cex_t * pCex,
Abc_Cex_t * pCexMin,
int fVerbose )

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

Synopsis [Verifies the care set of the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 458 of file bmcCexCare.c.

459{
460 int result;
461 Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
462 if ( fVerbose )
463 {
464 printf( "Original : " );
465 Bmc_CexPrint( pCex, Gia_ManPiNum(pGia), 0 );
466 printf( "Minimized: " );
467 Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 );
468 }
469 result = Bmc_CexVerify( pGia, pCex, pCexMin );
470 if ( !result )
471 printf( "Counter-example verification has failed.\n" );
472 else
473 printf( "Counter-example verification succeeded.\n" );
474 Gia_ManStop( pGia );
475 return result;
476}
Here is the call graph for this function:
Here is the caller graph for this function:

◆ Bmc_CexCareVerifyAnyPo()

int Bmc_CexCareVerifyAnyPo ( Aig_Man_t * p,
Abc_Cex_t * pCex,
Abc_Cex_t * pCexMin,
int fVerbose )

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

Synopsis [Verifies the care set of the counter-example.]

Description []

SideEffects []

SeeAlso []

Definition at line 497 of file bmcCexCare.c.

498{
499 int iPo;
500 Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
501 if ( fVerbose )
502 {
503 printf( "Original : " );
504 Bmc_CexPrint( pCex, Gia_ManPiNum(pGia), 0 );
505 printf( "Minimized: " );
506 Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 );
507 }
508 iPo = Bmc_CexVerifyAnyPo( pGia, pCex, pCexMin );
509 if ( iPo < 0 )
510 printf( "Counter-example verification has failed.\n" );
511 else
512 printf( "Counter-example verification succeeded.\n" );
513 Gia_ManStop( pGia );
514 return iPo;
515}
Bmc_CexVerifyAnyPo
int Bmc_CexVerifyAnyPo(Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexCare)
Definition bmcCexTools.c:388
Here is the call graph for this function: