ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
bmcCexCare.c
Go to the documentation of this file.
1
20
21#include "bmc.h"
22#include "aig/gia/giaAig.h"
23
24ABC_NAMESPACE_IMPL_START
25
26
30
34
46Abc_Cex_t * Bmc_CexCareExtendToObjects( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )
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}
88
100void Bmc_CexCarePropagateFwdOne( Gia_Man_t * p, Abc_Cex_t * pCex, int f, Vec_Int_t * vPriosIn )
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}
128void Bmc_CexCarePropagateFwd( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vPriosIn, Vec_Int_t * vPriosFf )
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}
143
155void Bmc_CexCarePropagateBwdOne( Gia_Man_t * p, Abc_Cex_t * pCex, int f, Abc_Cex_t * pCexMin )
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}
206Abc_Cex_t * Bmc_CexCarePropagateBwd( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vPriosIn, Vec_Int_t * vPriosFf )
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}
228
240Abc_Cex_t * Bmc_CexCareTotal( Abc_Cex_t ** pCexes, int nCexes )
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}
254Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose )
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}
426Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose )
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}
433Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int fHighEffort, int fCheck, int fVerbose )
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}
446
458int Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose )
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}
477/*
478 {
479 Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
480 Abc_Cex_t * pCex = Bmc_CexCareMinimize( pAig, 3*Saig_ManPiNum(pAig)/4, 4, pAbc->pCex, 1, 1 );
481 Aig_ManStop( pAig );
482 Abc_CexFree( pCex );
483 }
484*/
485
497int Bmc_CexCareVerifyAnyPo( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose )
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}
516
520
521
522ABC_NAMESPACE_IMPL_END
523
nWords
int nWords
Definition abcNpn.c:127
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Bmc_CexCarePropagateFwdOne
void Bmc_CexCarePropagateFwdOne(Gia_Man_t *p, Abc_Cex_t *pCex, int f, Vec_Int_t *vPriosIn)
Definition bmcCexCare.c:100
Bmc_CexCareMinimize
Abc_Cex_t * Bmc_CexCareMinimize(Aig_Man_t *p, int nRealPis, Abc_Cex_t *pCex, int nTryCexes, int fCheck, int fVerbose)
Definition bmcCexCare.c:426
Bmc_CexCareVerifyAnyPo
int Bmc_CexCareVerifyAnyPo(Aig_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexMin, int fVerbose)
Definition bmcCexCare.c:497
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
Bmc_CexCareSatBasedMinimize
Abc_Cex_t * Bmc_CexCareSatBasedMinimize(Aig_Man_t *p, int nRealPis, Abc_Cex_t *pCex, int fHighEffort, int fCheck, int fVerbose)
Definition bmcCexCare.c:433
Bmc_CexCarePropagateBwdOne
void Bmc_CexCarePropagateBwdOne(Gia_Man_t *p, Abc_Cex_t *pCex, int f, Abc_Cex_t *pCexMin)
Definition bmcCexCare.c:155
Bmc_CexCareTotal
Abc_Cex_t * Bmc_CexCareTotal(Abc_Cex_t **pCexes, int nCexes)
Definition bmcCexCare.c:240
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_CexCareExtendToObjects
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Bmc_CexCareExtendToObjects(Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexCare)
DECLARATIONS ///.
Definition bmcCexCare.c:46
Bmc_CexCareVerify
int Bmc_CexCareVerify(Aig_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexMin, int fVerbose)
Definition bmcCexCare.c:458
Bmc_CexPrint
void Bmc_CexPrint(Abc_Cex_t *pCex, int nRealPis, int fVerbose)
Definition bmcCexTools.c:307
Bmc_CexVerifyAnyPo
int Bmc_CexVerifyAnyPo(Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexCare)
Definition bmcCexTools.c:388
Bmc_CexVerify
int Bmc_CexVerify(Gia_Man_t *p, Abc_Cex_t *pCex, Abc_Cex_t *pCexCare)
Definition bmcCexTools.c:346
p
Cube * p
Definition exorList.c:222
Gia_ManFromAigSimple
Gia_Man_t * Gia_ManFromAigSimple(Aig_Man_t *p)
Definition giaAig.c:212
Bmc_CexCareSatBasedMinimizeAig
Abc_Cex_t * Bmc_CexCareSatBasedMinimizeAig(Gia_Man_t *p, Abc_Cex_t *pCex, int fHighEffort, int fVerbose)
Definition giaCex.c:517
Gia_ManStop
void Gia_ManStop(Gia_Man_t *p)
Definition giaMan.c:82
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_ManForEachAndReverse
#define Gia_ManForEachAndReverse(p, pObj, i)
Definition gia.h:1222
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_Man_t
struct Gia_Man_t_ Gia_Man_t
Definition gia.h:96
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_ManForEachCi
#define Gia_ManForEachCi(p, pObj, i)
Definition gia.h:1228
Gia_ManForEachRiRo
#define Gia_ManForEachRiRo(p, pObjRi, pObjRo, i)
Definition gia.h:1256
Gia_ManForEachRi
#define Gia_ManForEachRi(p, pObj, i)
Definition gia.h:1254
Gia_Obj_t_::Value
unsigned Value
Definition gia.h:89
Gia_Obj_t_::fPhase
unsigned fPhase
Definition gia.h:87
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
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