1 /**CFile****************************************************************
2
3 FileName [pdrMan.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Property driven reachability.]
8
9 Synopsis [Manager procedures.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - November 20, 2010.]
16
17 Revision [$Id: pdrMan.c,v 1.00 2010/11/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "pdrInt.h"
22 #include "sat/bmc/bmc.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 [Structural analysis.]
38
39 Description []
40
41 SideEffects []
42
43 SeeAlso []
44
45 ***********************************************************************/
Pdr_ManDeriveFlopPriorities3(Gia_Man_t * p,int fMuxCtrls)46 Vec_Int_t * Pdr_ManDeriveFlopPriorities3( Gia_Man_t * p, int fMuxCtrls )
47 {
48 int fDiscount = 0;
49 Vec_Wec_t * vLevels;
50 Vec_Int_t * vRes, * vLevel, * vCosts;
51 Gia_Obj_t * pObj, * pCtrl, * pData0, * pData1;
52 int i, k, Entry, MaxEntry = 0;
53 Gia_ManCreateRefs(p);
54 // discount references
55 if ( fDiscount )
56 {
57 Gia_ManForEachAnd( p, pObj, i )
58 {
59 if ( !Gia_ObjIsMuxType(pObj) )
60 continue;
61 pCtrl = Gia_Regular(Gia_ObjRecognizeMux(pObj, &pData1, &pData0));
62 pData0 = Gia_Regular(pData0);
63 pData1 = Gia_Regular(pData1);
64 p->pRefs[Gia_ObjId(p, pCtrl)]--;
65 if ( pData0 == pData1 )
66 p->pRefs[Gia_ObjId(p, pData0)]--;
67 }
68 }
69 // create flop costs
70 vCosts = Vec_IntAlloc( Gia_ManRegNum(p) );
71 Gia_ManForEachRo( p, pObj, i )
72 {
73 Vec_IntPush( vCosts, Gia_ObjRefNum(p, pObj) );
74 MaxEntry = Abc_MaxInt( MaxEntry, Gia_ObjRefNum(p, pObj) );
75 //printf( "%d(%d) ", i, Gia_ObjRefNum(p, pObj) );
76 }
77 //printf( "\n" );
78 MaxEntry++;
79 // add costs due to MUX inputs
80 if ( fMuxCtrls )
81 {
82 int fVerbose = 0;
83 Vec_Bit_t * vCtrls = Vec_BitStart( Gia_ManObjNum(p) );
84 Vec_Bit_t * vDatas = Vec_BitStart( Gia_ManObjNum(p) );
85 Gia_Obj_t * pCtrl, * pData1, * pData0;
86 int nCtrls = 0, nDatas = 0, nBoth = 0;
87 Gia_ManForEachAnd( p, pObj, i )
88 {
89 if ( !Gia_ObjIsMuxType(pObj) )
90 continue;
91 pCtrl = Gia_ObjRecognizeMux( pObj, &pData1, &pData0 );
92 pCtrl = Gia_Regular(pCtrl);
93 pData1 = Gia_Regular(pData1);
94 pData0 = Gia_Regular(pData0);
95 Vec_BitWriteEntry( vCtrls, Gia_ObjId(p, pCtrl), 1 );
96 Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData1), 1 );
97 Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData0), 1 );
98 }
99 Gia_ManForEachRo( p, pObj, i )
100 if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) )
101 Vec_IntAddToEntry( vCosts, i, MaxEntry );
102 //else if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
103 // Vec_IntAddToEntry( vCosts, i, MaxEntry );
104 MaxEntry = 2*MaxEntry + 1;
105 // print out
106 if ( fVerbose )
107 {
108 Gia_ManForEachRo( p, pObj, i )
109 {
110 if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) )
111 nCtrls++;
112 if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
113 nDatas++;
114 if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) && Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
115 nBoth++;
116 }
117 printf( "%10s : Flops = %5d. Ctrls = %5d. Datas = %5d. Both = %5d.\n", Gia_ManName(p), Gia_ManRegNum(p), nCtrls, nDatas, nBoth );
118 }
119 Vec_BitFree( vCtrls );
120 Vec_BitFree( vDatas );
121 }
122 // create levelized structure
123 vLevels = Vec_WecStart( MaxEntry );
124 Vec_IntForEachEntry( vCosts, Entry, i )
125 Vec_WecPush( vLevels, Entry, i );
126 // collect in this order
127 MaxEntry = 0;
128 vRes = Vec_IntStart( Gia_ManRegNum(p) );
129 Vec_WecForEachLevel( vLevels, vLevel, i )
130 Vec_IntForEachEntry( vLevel, Entry, k )
131 Vec_IntWriteEntry( vRes, Entry, MaxEntry++ );
132 //printf( "%d ", Gia_ObjRefNum(p, Gia_ManCi(p, Gia_ManPiNum(p)+Entry)) );
133 //printf( "\n" );
134 assert( MaxEntry == Gia_ManRegNum(p) );
135 Vec_WecFree( vLevels );
136 Vec_IntFree( vCosts );
137 ABC_FREE( p->pRefs );
138 //Vec_IntPrint( vRes );
139 return vRes;
140 }
141
142 /**Function*************************************************************
143
144 Synopsis [Structural analysis.]
145
146 Description []
147
148 SideEffects []
149
150 SeeAlso []
151
152 ***********************************************************************/
Pdr_ManDeriveFlopPriorities2(Gia_Man_t * p,int fMuxCtrls)153 Vec_Int_t * Pdr_ManDeriveFlopPriorities2( Gia_Man_t * p, int fMuxCtrls )
154 {
155 int fDiscount = 0;
156 Vec_Int_t * vRes = NULL;
157 Gia_Obj_t * pObj, * pCtrl, * pData0, * pData1;
158 int MaxEntry = 0;
159 int i, * pPerm;
160 // create flop costs
161 Vec_Int_t * vCosts = Vec_IntStart( Gia_ManRegNum(p) );
162 Gia_ManCreateRefs(p);
163 // discount references
164 if ( fDiscount )
165 {
166 Gia_ManForEachAnd( p, pObj, i )
167 {
168 if ( !Gia_ObjIsMuxType(pObj) )
169 continue;
170 pCtrl = Gia_Regular(Gia_ObjRecognizeMux(pObj, &pData1, &pData0));
171 pData0 = Gia_Regular(pData0);
172 pData1 = Gia_Regular(pData1);
173 p->pRefs[Gia_ObjId(p, pCtrl)]--;
174 if ( pData0 == pData1 )
175 p->pRefs[Gia_ObjId(p, pData0)]--;
176 }
177 }
178 Gia_ManForEachRo( p, pObj, i )
179 {
180 Vec_IntWriteEntry( vCosts, i, Gia_ObjRefNum(p, pObj) );
181 MaxEntry = Abc_MaxInt( MaxEntry, Gia_ObjRefNum(p, pObj) );
182 }
183 MaxEntry++;
184 ABC_FREE( p->pRefs );
185 // add costs due to MUX inputs
186 if ( fMuxCtrls )
187 {
188 int fVerbose = 0;
189 Vec_Bit_t * vCtrls = Vec_BitStart( Gia_ManObjNum(p) );
190 Vec_Bit_t * vDatas = Vec_BitStart( Gia_ManObjNum(p) );
191 Gia_Obj_t * pCtrl, * pData1, * pData0;
192 int nCtrls = 0, nDatas = 0, nBoth = 0;
193 Gia_ManForEachAnd( p, pObj, i )
194 {
195 if ( !Gia_ObjIsMuxType(pObj) )
196 continue;
197 pCtrl = Gia_ObjRecognizeMux( pObj, &pData1, &pData0 );
198 pCtrl = Gia_Regular(pCtrl);
199 pData1 = Gia_Regular(pData1);
200 pData0 = Gia_Regular(pData0);
201 Vec_BitWriteEntry( vCtrls, Gia_ObjId(p, pCtrl), 1 );
202 Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData1), 1 );
203 Vec_BitWriteEntry( vDatas, Gia_ObjId(p, pData0), 1 );
204 }
205 Gia_ManForEachRo( p, pObj, i )
206 if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) )
207 Vec_IntAddToEntry( vCosts, i, MaxEntry );
208 //else if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
209 // Vec_IntAddToEntry( vCosts, i, MaxEntry );
210 // print out
211 if ( fVerbose )
212 {
213 Gia_ManForEachRo( p, pObj, i )
214 {
215 if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) )
216 nCtrls++;
217 if ( Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
218 nDatas++;
219 if ( Vec_BitEntry(vCtrls, Gia_ObjId(p, pObj)) && Vec_BitEntry(vDatas, Gia_ObjId(p, pObj)) )
220 nBoth++;
221 }
222 printf( "%10s : Flops = %5d. Ctrls = %5d. Datas = %5d. Both = %5d.\n", Gia_ManName(p), Gia_ManRegNum(p), nCtrls, nDatas, nBoth );
223 }
224 Vec_BitFree( vCtrls );
225 Vec_BitFree( vDatas );
226 }
227 // create ordering based on costs
228 pPerm = Abc_MergeSortCost( Vec_IntArray(vCosts), Vec_IntSize(vCosts) );
229 vRes = Vec_IntAllocArray( pPerm, Vec_IntSize(vCosts) );
230 Vec_IntFree( vCosts );
231 vCosts = Vec_IntInvert( vRes, -1 );
232 Vec_IntFree( vRes );
233 //Vec_IntPrint( vCosts );
234 return vCosts;
235 }
236
237 /**Function*************************************************************
238
239 Synopsis [Creates manager.]
240
241 Description []
242
243 SideEffects []
244
245 SeeAlso []
246
247 ***********************************************************************/
Pdr_ManStart(Aig_Man_t * pAig,Pdr_Par_t * pPars,Vec_Int_t * vPrioInit)248 Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit )
249 {
250 Pdr_Man_t * p;
251 p = ABC_CALLOC( Pdr_Man_t, 1 );
252 p->pPars = pPars;
253 p->pAig = pAig;
254 p->pGia = (pPars->fFlopPrio || p->pPars->fNewXSim || p->pPars->fUseAbs) ? Gia_ManFromAigSimple(pAig) : NULL;
255 p->vSolvers = Vec_PtrAlloc( 0 );
256 p->vClauses = Vec_VecAlloc( 0 );
257 p->pQueue = NULL;
258 p->pOrder = ABC_ALLOC( int, Aig_ManRegNum(pAig) );
259 p->vActVars = Vec_IntAlloc( 256 );
260 if ( !p->pPars->fMonoCnf )
261 p->vVLits = Vec_WecStart( 1+Abc_MaxInt(1, Aig_ManLevels(pAig)) );
262 // internal use
263 p->nPrioShift = Abc_Base2Log(Aig_ManRegNum(pAig));
264 if ( vPrioInit )
265 p->vPrio = vPrioInit;
266 else if ( pPars->fFlopPrio )
267 p->vPrio = Pdr_ManDeriveFlopPriorities2(p->pGia, 1);
268 // else if ( p->pPars->fNewXSim )
269 // p->vPrio = Vec_IntStartNatural( Aig_ManRegNum(pAig) );
270 else
271 p->vPrio = Vec_IntStart( Aig_ManRegNum(pAig) );
272 p->vLits = Vec_IntAlloc( 100 ); // array of literals
273 p->vCiObjs = Vec_IntAlloc( 100 ); // cone leaves
274 p->vCoObjs = Vec_IntAlloc( 100 ); // cone roots
275 p->vCiVals = Vec_IntAlloc( 100 ); // cone leaf values
276 p->vCoVals = Vec_IntAlloc( 100 ); // cone root values
277 p->vNodes = Vec_IntAlloc( 100 ); // cone nodes
278 p->vUndo = Vec_IntAlloc( 100 ); // cone undos
279 p->vVisits = Vec_IntAlloc( 100 ); // intermediate
280 p->vCi2Rem = Vec_IntAlloc( 100 ); // CIs to be removed
281 p->vRes = Vec_IntAlloc( 100 ); // final result
282 p->pCnfMan = Cnf_ManStart();
283 // ternary simulation
284 p->pTxs3 = pPars->fNewXSim ? Txs3_ManStart( p, pAig, p->vPrio ) : NULL;
285 // additional AIG data-members
286 if ( pAig->pFanData == NULL )
287 Aig_ManFanoutStart( pAig );
288 if ( pAig->pTerSimData == NULL )
289 pAig->pTerSimData = ABC_CALLOC( unsigned, 1 + (Aig_ManObjNumMax(pAig) / 16) );
290 // time spent on each outputs
291 if ( pPars->nTimeOutOne )
292 {
293 int i;
294 p->pTime4Outs = ABC_ALLOC( abctime, Saig_ManPoNum(pAig) );
295 for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
296 p->pTime4Outs[i] = pPars->nTimeOutOne * CLOCKS_PER_SEC / 1000 + 1;
297 }
298 if ( pPars->fSolveAll )
299 {
300 p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
301 p->pPars->vOutMap = Vec_IntAlloc( Saig_ManPoNum(pAig) );
302 Vec_IntFill( p->pPars->vOutMap, Saig_ManPoNum(pAig), -2 );
303 }
304 return p;
305 }
306
307 /**Function*************************************************************
308
309 Synopsis [Frees manager.]
310
311 Description []
312
313 SideEffects []
314
315 SeeAlso []
316
317 ***********************************************************************/
Pdr_ManStop(Pdr_Man_t * p)318 void Pdr_ManStop( Pdr_Man_t * p )
319 {
320 Pdr_Set_t * pCla;
321 sat_solver * pSat;
322 int i, k;
323 Gia_ManStopP( &p->pGia );
324 Aig_ManCleanMarkAB( p->pAig );
325 if ( p->pPars->fVerbose )
326 {
327 Abc_Print( 1, "Block =%5d Oblig =%6d Clause =%6d Call =%6d (sat=%.1f%%) Cex =%4d Start =%4d\n",
328 p->nBlocks, p->nObligs, p->nCubes, p->nCalls, 100.0 * p->nCallsS / p->nCalls, p->nCexesTotal, p->nStarts );
329 ABC_PRTP( "SAT solving", p->tSat, p->tTotal );
330 ABC_PRTP( " unsat ", p->tSatUnsat, p->tTotal );
331 ABC_PRTP( " sat ", p->tSatSat, p->tTotal );
332 ABC_PRTP( "Generalize ", p->tGeneral, p->tTotal );
333 ABC_PRTP( "Push clause", p->tPush, p->tTotal );
334 ABC_PRTP( "Ternary sim", p->tTsim, p->tTotal );
335 ABC_PRTP( "Containment", p->tContain, p->tTotal );
336 ABC_PRTP( "CNF compute", p->tCnf, p->tTotal );
337 ABC_PRTP( "Refinement ", p->tAbs, p->tTotal );
338 ABC_PRTP( "TOTAL ", p->tTotal, p->tTotal );
339 fflush( stdout );
340 }
341 // Abc_Print( 1, "SS =%6d. SU =%6d. US =%6d. UU =%6d.\n", p->nCasesSS, p->nCasesSU, p->nCasesUS, p->nCasesUU );
342 Vec_PtrForEachEntry( sat_solver *, p->vSolvers, pSat, i )
343 sat_solver_delete( pSat );
344 Vec_PtrFree( p->vSolvers );
345 Vec_VecForEachEntry( Pdr_Set_t *, p->vClauses, pCla, i, k )
346 Pdr_SetDeref( pCla );
347 Vec_VecFree( p->vClauses );
348 Pdr_QueueStop( p );
349 ABC_FREE( p->pOrder );
350 Vec_IntFree( p->vActVars );
351 // static CNF
352 Cnf_DataFree( p->pCnf1 );
353 Vec_IntFreeP( &p->vVar2Reg );
354 // dynamic CNF
355 Cnf_DataFree( p->pCnf2 );
356 if ( p->pvId2Vars )
357 for ( i = 0; i < Aig_ManObjNumMax(p->pAig); i++ )
358 ABC_FREE( p->pvId2Vars[i].pArray );
359 ABC_FREE( p->pvId2Vars );
360 // Vec_VecFreeP( (Vec_Vec_t **)&p->vVar2Ids );
361 for ( i = 0; i < Vec_PtrSize(&p->vVar2Ids); i++ )
362 Vec_IntFree( (Vec_Int_t *)Vec_PtrEntry(&p->vVar2Ids, i) );
363 ABC_FREE( p->vVar2Ids.pArray );
364 Vec_WecFreeP( &p->vVLits );
365 // CNF manager
366 Cnf_ManStop( p->pCnfMan );
367 Vec_IntFreeP( &p->vAbsFlops );
368 Vec_IntFreeP( &p->vMapFf2Ppi );
369 Vec_IntFreeP( &p->vMapPpi2Ff );
370 // terminary simulation
371 if ( p->pPars->fNewXSim )
372 Txs3_ManStop( p->pTxs3 );
373 // internal use
374 Vec_IntFreeP( &p->vPrio ); // priority flops
375 Vec_IntFree( p->vLits ); // array of literals
376 Vec_IntFree( p->vCiObjs ); // cone leaves
377 Vec_IntFree( p->vCoObjs ); // cone roots
378 Vec_IntFree( p->vCiVals ); // cone leaf values
379 Vec_IntFree( p->vCoVals ); // cone root values
380 Vec_IntFree( p->vNodes ); // cone nodes
381 Vec_IntFree( p->vUndo ); // cone undos
382 Vec_IntFree( p->vVisits ); // intermediate
383 Vec_IntFree( p->vCi2Rem ); // CIs to be removed
384 Vec_IntFree( p->vRes ); // final result
385 Vec_PtrFreeP( &p->vInfCubes );
386 ABC_FREE( p->pTime4Outs );
387 if ( p->vCexes )
388 Vec_PtrFreeFree( p->vCexes );
389 // additional AIG data-members
390 if ( p->pAig->pFanData != NULL )
391 Aig_ManFanoutStop( p->pAig );
392 if ( p->pAig->pTerSimData != NULL )
393 ABC_FREE( p->pAig->pTerSimData );
394 ABC_FREE( p );
395 }
396
397 /**Function*************************************************************
398
399 Synopsis [Derives counter-example.]
400
401 Description []
402
403 SideEffects []
404
405 SeeAlso []
406
407 ***********************************************************************/
Pdr_ManDeriveCex(Pdr_Man_t * p)408 Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
409 {
410 Abc_Cex_t * pCex;
411 Pdr_Obl_t * pObl;
412 int i, f, Lit, nFrames = 0;
413 // count the number of frames
414 for ( pObl = p->pQueue; pObl; pObl = pObl->pNext )
415 nFrames++;
416 // create the counter-example
417 pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames );
418 pCex->iPo = p->iOutCur;
419 pCex->iFrame = nFrames-1;
420 for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )
421 for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
422 {
423 Lit = pObl->pState->Lits[i];
424 if ( Abc_LitIsCompl(Lit) )
425 continue;
426 if ( Abc_Lit2Var(Lit) >= pCex->nPis ) // allows PPI literals to be thrown away
427 continue;
428 assert( Abc_Lit2Var(Lit) < pCex->nPis );
429 Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Abc_Lit2Var(Lit) );
430 }
431 assert( f == nFrames );
432 if ( !Saig_ManVerifyCex(p->pAig, pCex) )
433 printf( "CEX for output %d is not valid.\n", p->iOutCur );
434 return pCex;
435 }
436
437 /**Function*************************************************************
438
439 Synopsis [Derives counter-example when abstraction is used.]
440
441 Description []
442
443 SideEffects []
444
445 SeeAlso []
446
447 ***********************************************************************/
Pdr_ManDeriveCexAbs(Pdr_Man_t * p)448 Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p )
449 {
450 extern Gia_Man_t * Gia_ManDupAbs( Gia_Man_t * p, Vec_Int_t * vMapPpi2Ff, Vec_Int_t * vMapFf2Ppi );
451
452 Gia_Man_t * pAbs;
453 Abc_Cex_t * pCex, * pCexCare;
454 Pdr_Obl_t * pObl;
455 int i, f, Lit, Flop, nFrames = 0;
456 int nPis = Saig_ManPiNum(p->pAig);
457 int nFfRefined = 0;
458 if ( !p->pPars->fUseAbs || !p->vMapPpi2Ff )
459 return Pdr_ManDeriveCex(p);
460 // restore previous map
461 Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i )
462 {
463 assert( Vec_IntEntry( p->vMapFf2Ppi, Flop ) == i );
464 Vec_IntWriteEntry( p->vMapFf2Ppi, Flop, -1 );
465 }
466 Vec_IntClear( p->vMapPpi2Ff );
467 // count the number of frames
468 for ( pObl = p->pQueue; pObl; pObl = pObl->pNext )
469 {
470 for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
471 {
472 Lit = pObl->pState->Lits[i];
473 if ( Abc_Lit2Var(Lit) < nPis ) // PI literal
474 continue;
475 Flop = Abc_Lit2Var(Lit) - nPis;
476 if ( Vec_IntEntry(p->vMapFf2Ppi, Flop) >= 0 ) // already used PPI literal
477 continue;
478 Vec_IntWriteEntry( p->vMapFf2Ppi, Flop, Vec_IntSize(p->vMapPpi2Ff) );
479 Vec_IntPush( p->vMapPpi2Ff, Flop );
480 }
481 nFrames++;
482 }
483 if ( Vec_IntSize(p->vMapPpi2Ff) == 0 ) // no PPIs -- this is a real CEX
484 return Pdr_ManDeriveCex(p);
485 if ( p->pPars->fUseSimpleRef )
486 {
487 // rely on ternary simulation to perform refinement
488 Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i )
489 {
490 assert( Vec_IntEntry(p->vAbsFlops, Flop) == 0 );
491 Vec_IntWriteEntry( p->vAbsFlops, Flop, 1 );
492 nFfRefined++;
493 }
494 }
495 else
496 {
497 // create the counter-example
498 pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig) - Vec_IntSize(p->vMapPpi2Ff), Saig_ManPiNum(p->pAig) + Vec_IntSize(p->vMapPpi2Ff), nFrames );
499 pCex->iPo = p->iOutCur;
500 pCex->iFrame = nFrames-1;
501 for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )
502 for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
503 {
504 Lit = pObl->pState->Lits[i];
505 if ( Abc_LitIsCompl(Lit) )
506 continue;
507 if ( Abc_Lit2Var(Lit) < nPis ) // PI literal
508 Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + Abc_Lit2Var(Lit) );
509 else
510 {
511 int iPPI = nPis + Vec_IntEntry(p->vMapFf2Ppi, Abc_Lit2Var(Lit) - nPis);
512 assert( iPPI < pCex->nPis );
513 Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + iPPI );
514 }
515 }
516 assert( f == nFrames );
517 // perform CEX minimization
518 pAbs = Gia_ManDupAbs( p->pGia, p->vMapPpi2Ff, p->vMapFf2Ppi );
519 pCexCare = Bmc_CexCareMinimizeAig( pAbs, nPis, pCex, 1, 0, 0 );
520 Gia_ManStop( pAbs );
521 assert( pCexCare->nPis == pCex->nPis );
522 Abc_CexFree( pCex );
523 // detect care PPIs
524 for ( f = 0; f < nFrames; f++ )
525 {
526 for ( i = nPis; i < pCexCare->nPis; i++ )
527 if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) )
528 {
529 if ( Vec_IntEntry(p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis)) == 0 ) // currently abstracted
530 Vec_IntWriteEntry( p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis), 1 ), nFfRefined++;
531 }
532 }
533 Abc_CexFree( pCexCare );
534 if ( nFfRefined == 0 ) // no refinement -- this is a real CEX
535 return Pdr_ManDeriveCex(p);
536 }
537 //printf( "CEX-based refinement refined %d flops.\n", nFfRefined );
538 p->nCexesTotal++;
539 p->nCexes++;
540 return NULL;
541 }
542
543 ////////////////////////////////////////////////////////////////////////
544 /// END OF FILE ///
545 ////////////////////////////////////////////////////////////////////////
546
547
548 ABC_NAMESPACE_IMPL_END
549
550