1 /**CFile****************************************************************
2
3 FileName [saigAbsCba.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Sequential AIG package.]
8
9 Synopsis [CEX-based abstraction.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: saigAbsCba.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "abs.h"
22 #include "sat/bmc/bmc.h"
23
24 ABC_NAMESPACE_IMPL_START
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 // local manager
31 typedef struct Saig_ManCba_t_ Saig_ManCba_t;
32 struct Saig_ManCba_t_
33 {
34 // user data
35 Aig_Man_t * pAig; // user's AIG
36 Abc_Cex_t * pCex; // user's CEX
37 int nInputs; // the number of first inputs to skip
38 int fVerbose; // verbose flag
39 // unrolling
40 Aig_Man_t * pFrames; // unrolled timeframes
41 Vec_Int_t * vMapPiF2A; // mapping of frame PIs into real PIs
42 // additional information
43 Vec_Vec_t * vReg2Frame; // register to frame mapping
44 Vec_Vec_t * vReg2Value; // register to value mapping
45 };
46
47 ////////////////////////////////////////////////////////////////////////
48 /// FUNCTION DEFINITIONS ///
49 ////////////////////////////////////////////////////////////////////////
50
51
52 /**Function*************************************************************
53
54 Synopsis [Selects the best flops from the given array.]
55
56 Description [Selects the best 'nFfsToSelect' flops among the array
57 'vAbsFfsToAdd' of flops that should be added to the abstraction.
58 To this end, this procedure simulates the original AIG (pAig) using
59 the given CEX (pAbsCex), which was detected for the abstraction.]
60
61 SideEffects []
62
63 SeeAlso []
64
65 ***********************************************************************/
Saig_ManCbaFilterFlops(Aig_Man_t * pAig,Abc_Cex_t * pAbsCex,Vec_Int_t * vFlopClasses,Vec_Int_t * vAbsFfsToAdd,int nFfsToSelect)66 Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect )
67 {
68 Aig_Obj_t * pObj, * pObjRi, * pObjRo;
69 Vec_Int_t * vMapEntries, * vFlopCosts, * vFlopAddCosts, * vFfsToAddBest;
70 int i, k, f, Entry, iBit, * pPerm;
71 assert( Aig_ManRegNum(pAig) == Vec_IntSize(vFlopClasses) );
72 assert( Vec_IntSize(vAbsFfsToAdd) > nFfsToSelect );
73 // map previously abstracted flops into their original numbers
74 vMapEntries = Vec_IntAlloc( Vec_IntSize(vFlopClasses) );
75 Vec_IntForEachEntry( vFlopClasses, Entry, i )
76 if ( Entry == 0 )
77 Vec_IntPush( vMapEntries, i );
78 // simulate one frame at a time
79 assert( Saig_ManPiNum(pAig) + Vec_IntSize(vMapEntries) == pAbsCex->nPis );
80 vFlopCosts = Vec_IntStart( Vec_IntSize(vMapEntries) );
81 // initialize the flops
82 Aig_ManCleanMarkB(pAig);
83 Aig_ManConst1(pAig)->fMarkB = 1;
84 Saig_ManForEachLo( pAig, pObj, i )
85 pObj->fMarkB = 0;
86 for ( f = 0; f < pAbsCex->iFrame; f++ )
87 {
88 // override the flop values according to the cex
89 iBit = pAbsCex->nRegs + f * pAbsCex->nPis + Saig_ManPiNum(pAig);
90 Vec_IntForEachEntry( vMapEntries, Entry, k )
91 Saig_ManLo(pAig, Entry)->fMarkB = Abc_InfoHasBit(pAbsCex->pData, iBit + k);
92 // simulate
93 Aig_ManForEachNode( pAig, pObj, k )
94 pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) &
95 (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
96 Aig_ManForEachCo( pAig, pObj, k )
97 pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
98 // transfer
99 Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
100 pObjRo->fMarkB = pObjRi->fMarkB;
101 // compare
102 iBit = pAbsCex->nRegs + (f + 1) * pAbsCex->nPis + Saig_ManPiNum(pAig);
103 Vec_IntForEachEntry( vMapEntries, Entry, k )
104 if ( Saig_ManLi(pAig, Entry)->fMarkB != (unsigned)Abc_InfoHasBit(pAbsCex->pData, iBit + k) )
105 Vec_IntAddToEntry( vFlopCosts, k, 1 );
106 }
107 // Vec_IntForEachEntry( vFlopCosts, Entry, i )
108 // printf( "%d ", Entry );
109 // printf( "\n" );
110 // remap the cost
111 vFlopAddCosts = Vec_IntAlloc( Vec_IntSize(vAbsFfsToAdd) );
112 Vec_IntForEachEntry( vAbsFfsToAdd, Entry, i )
113 Vec_IntPush( vFlopAddCosts, -Vec_IntEntry(vFlopCosts, Entry) );
114 // sort the flops
115 pPerm = Abc_MergeSortCost( Vec_IntArray(vFlopAddCosts), Vec_IntSize(vFlopAddCosts) );
116 // shrink the array
117 vFfsToAddBest = Vec_IntAlloc( nFfsToSelect );
118 for ( i = 0; i < nFfsToSelect; i++ )
119 {
120 // printf( "%d ", Vec_IntEntry(vFlopAddCosts, pPerm[i]) );
121 Vec_IntPush( vFfsToAddBest, Vec_IntEntry(vAbsFfsToAdd, pPerm[i]) );
122 }
123 // printf( "\n" );
124 // cleanup
125 ABC_FREE( pPerm );
126 Vec_IntFree( vMapEntries );
127 Vec_IntFree( vFlopCosts );
128 Vec_IntFree( vFlopAddCosts );
129 Aig_ManCleanMarkB(pAig);
130 // return the computed flops
131 return vFfsToAddBest;
132 }
133
134
135 /**Function*************************************************************
136
137 Synopsis [Duplicate with literals.]
138
139 Description []
140
141 SideEffects []
142
143 SeeAlso []
144
145 ***********************************************************************/
Saig_ManDupWithCubes(Aig_Man_t * pAig,Vec_Vec_t * vReg2Value)146 Aig_Man_t * Saig_ManDupWithCubes( Aig_Man_t * pAig, Vec_Vec_t * vReg2Value )
147 {
148 Vec_Int_t * vLevel;
149 Aig_Man_t * pAigNew;
150 Aig_Obj_t * pObj, * pMiter;
151 int i, k, Lit;
152 assert( pAig->nConstrs == 0 );
153 // start the new manager
154 pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) + Vec_VecSizeSize(vReg2Value) );
155 pAigNew->pName = Abc_UtilStrsav( pAig->pName );
156 // map the constant node
157 Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
158 // create variables for PIs
159 Aig_ManForEachCi( pAig, pObj, i )
160 pObj->pData = Aig_ObjCreateCi( pAigNew );
161 // add internal nodes of this frame
162 Aig_ManForEachNode( pAig, pObj, i )
163 pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
164 // create POs for cubes
165 Vec_VecForEachLevelInt( vReg2Value, vLevel, i )
166 {
167 pMiter = Aig_ManConst1( pAigNew );
168 Vec_IntForEachEntry( vLevel, Lit, k )
169 {
170 pObj = Saig_ManLi( pAig, Abc_Lit2Var(Lit) );
171 pMiter = Aig_And( pAigNew, pMiter, Aig_NotCond(Aig_ObjChild0Copy(pObj), Abc_LitIsCompl(Lit)) );
172 }
173 Aig_ObjCreateCo( pAigNew, pMiter );
174 }
175 // transfer to register outputs
176 Saig_ManForEachLi( pAig, pObj, i )
177 Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
178 // finalize
179 Aig_ManCleanup( pAigNew );
180 Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
181 return pAigNew;
182 }
183
184 /**Function*************************************************************
185
186 Synopsis [Maps array of frame PI IDs into array of additional PI IDs.]
187
188 Description []
189
190 SideEffects []
191
192 SeeAlso []
193
194 ***********************************************************************/
Saig_ManCbaReason2Inputs(Saig_ManCba_t * p,Vec_Int_t * vReasons)195 Vec_Int_t * Saig_ManCbaReason2Inputs( Saig_ManCba_t * p, Vec_Int_t * vReasons )
196 {
197 Vec_Int_t * vOriginal, * vVisited;
198 int i, Entry;
199 vOriginal = Vec_IntAlloc( Saig_ManPiNum(p->pAig) );
200 vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) );
201 Vec_IntForEachEntry( vReasons, Entry, i )
202 {
203 int iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry );
204 assert( iInput >= p->nInputs && iInput < Aig_ManCiNum(p->pAig) );
205 if ( Vec_IntEntry(vVisited, iInput) == 0 )
206 Vec_IntPush( vOriginal, iInput - p->nInputs );
207 Vec_IntAddToEntry( vVisited, iInput, 1 );
208 }
209 Vec_IntFree( vVisited );
210 return vOriginal;
211 }
212
213 /**Function*************************************************************
214
215 Synopsis [Creates the counter-example.]
216
217 Description []
218
219 SideEffects []
220
221 SeeAlso []
222
223 ***********************************************************************/
Saig_ManCbaReason2Cex(Saig_ManCba_t * p,Vec_Int_t * vReasons)224 Abc_Cex_t * Saig_ManCbaReason2Cex( Saig_ManCba_t * p, Vec_Int_t * vReasons )
225 {
226 Abc_Cex_t * pCare;
227 int i, Entry, iInput, iFrame;
228 pCare = Abc_CexDup( p->pCex, p->pCex->nRegs );
229 memset( pCare->pData, 0, sizeof(unsigned) * Abc_BitWordNum(pCare->nBits) );
230 Vec_IntForEachEntry( vReasons, Entry, i )
231 {
232 assert( Entry >= 0 && Entry < Aig_ManCiNum(p->pFrames) );
233 iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry );
234 iFrame = Vec_IntEntry( p->vMapPiF2A, 2*Entry+1 );
235 Abc_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput );
236 }
237 /*
238 for ( iFrame = 0; iFrame <= pCare->iFrame; iFrame++ )
239 {
240 int Count = 0;
241 for ( i = 0; i < pCare->nPis; i++ )
242 Count += Abc_InfoHasBit(pCare->pData, pCare->nRegs + pCare->nPis * iFrame + i);
243 printf( "%d ", Count );
244 }
245 printf( "\n" );
246 */
247 return pCare;
248 }
249
250 /**Function*************************************************************
251
252 Synopsis [Returns reasons for the property to fail.]
253
254 Description []
255
256 SideEffects []
257
258 SeeAlso []
259
260 ***********************************************************************/
Saig_ManCbaFindReason_rec(Aig_Man_t * p,Aig_Obj_t * pObj,Vec_Int_t * vPrios,Vec_Int_t * vReasons)261 void Saig_ManCbaFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPrios, Vec_Int_t * vReasons )
262 {
263 if ( Aig_ObjIsTravIdCurrent(p, pObj) )
264 return;
265 Aig_ObjSetTravIdCurrent(p, pObj);
266 if ( Aig_ObjIsConst1(pObj) )
267 return;
268 if ( Aig_ObjIsCi(pObj) )
269 {
270 Vec_IntPush( vReasons, Aig_ObjCioId(pObj) );
271 return;
272 }
273 assert( Aig_ObjIsNode(pObj) );
274 if ( pObj->fPhase )
275 {
276 Saig_ManCbaFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
277 Saig_ManCbaFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
278 }
279 else
280 {
281 int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
282 int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase;
283 assert( !fPhase0 || !fPhase1 );
284 if ( !fPhase0 && fPhase1 )
285 Saig_ManCbaFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
286 else if ( fPhase0 && !fPhase1 )
287 Saig_ManCbaFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
288 else
289 {
290 int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) );
291 int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) );
292 if ( iPrio0 <= iPrio1 )
293 Saig_ManCbaFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
294 else
295 Saig_ManCbaFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
296 }
297 }
298 }
299
300 /**Function*************************************************************
301
302 Synopsis [Returns reasons for the property to fail.]
303
304 Description []
305
306 SideEffects []
307
308 SeeAlso []
309
310 ***********************************************************************/
Saig_ManCbaFindReason(Saig_ManCba_t * p)311 Vec_Int_t * Saig_ManCbaFindReason( Saig_ManCba_t * p )
312 {
313 Aig_Obj_t * pObj;
314 Vec_Int_t * vPrios, * vReasons;
315 int i;
316
317 // set PI values according to CEX
318 vPrios = Vec_IntStartFull( Aig_ManObjNumMax(p->pFrames) );
319 Aig_ManConst1(p->pFrames)->fPhase = 1;
320 Aig_ManForEachCi( p->pFrames, pObj, i )
321 {
322 int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i );
323 int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 );
324 pObj->fPhase = Abc_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
325 Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), i );
326 }
327
328 // traverse and set the priority
329 Aig_ManForEachNode( p->pFrames, pObj, i )
330 {
331 int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
332 int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase;
333 int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) );
334 int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) );
335 pObj->fPhase = fPhase0 && fPhase1;
336 if ( fPhase0 && fPhase1 ) // both are one
337 Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MaxInt(iPrio0, iPrio1) );
338 else if ( !fPhase0 && fPhase1 )
339 Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio0 );
340 else if ( fPhase0 && !fPhase1 )
341 Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio1 );
342 else // both are zero
343 Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MinInt(iPrio0, iPrio1) );
344 }
345 // check the property output
346 pObj = Aig_ManCo( p->pFrames, 0 );
347 pObj->fPhase = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
348 assert( !pObj->fPhase );
349
350 // select the reason
351 vReasons = Vec_IntAlloc( 100 );
352 Aig_ManIncrementTravId( p->pFrames );
353 Saig_ManCbaFindReason_rec( p->pFrames, Aig_ObjFanin0(pObj), vPrios, vReasons );
354 Vec_IntFree( vPrios );
355 // assert( !Aig_ObjIsTravIdCurrent(p->pFrames, Aig_ManConst1(p->pFrames)) );
356 return vReasons;
357 }
358
359
360 /**Function*************************************************************
361
362 Synopsis [Collect nodes in the unrolled timeframes.]
363
364 Description []
365
366 SideEffects []
367
368 SeeAlso []
369
370 ***********************************************************************/
Saig_ManCbaUnrollCollect_rec(Aig_Man_t * pAig,Aig_Obj_t * pObj,Vec_Int_t * vObjs,Vec_Int_t * vRoots)371 void Saig_ManCbaUnrollCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vObjs, Vec_Int_t * vRoots )
372 {
373 if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
374 return;
375 Aig_ObjSetTravIdCurrent(pAig, pObj);
376 if ( Aig_ObjIsCo(pObj) )
377 Saig_ManCbaUnrollCollect_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots );
378 else if ( Aig_ObjIsNode(pObj) )
379 {
380 Saig_ManCbaUnrollCollect_rec( pAig, Aig_ObjFanin0(pObj), vObjs, vRoots );
381 Saig_ManCbaUnrollCollect_rec( pAig, Aig_ObjFanin1(pObj), vObjs, vRoots );
382 }
383 if ( vRoots && Saig_ObjIsLo( pAig, pObj ) )
384 Vec_IntPush( vRoots, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) );
385 Vec_IntPush( vObjs, Aig_ObjId(pObj) );
386 }
387
388 /**Function*************************************************************
389
390 Synopsis [Derive unrolled timeframes.]
391
392 Description []
393
394 SideEffects []
395
396 SeeAlso []
397
398 ***********************************************************************/
Saig_ManCbaUnrollWithCex(Aig_Man_t * pAig,Abc_Cex_t * pCex,int nInputs,Vec_Int_t ** pvMapPiF2A,Vec_Vec_t ** pvReg2Frame)399 Aig_Man_t * Saig_ManCbaUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, Vec_Int_t ** pvMapPiF2A, Vec_Vec_t ** pvReg2Frame )
400 {
401 Aig_Man_t * pFrames; // unrolled timeframes
402 Vec_Vec_t * vFrameCos; // the list of COs per frame
403 Vec_Vec_t * vFrameObjs; // the list of objects per frame
404 Vec_Int_t * vRoots, * vObjs;
405 Aig_Obj_t * pObj;
406 int i, f;
407 // sanity checks
408 assert( Saig_ManPiNum(pAig) == pCex->nPis );
409 // assert( Saig_ManRegNum(pAig) == pCex->nRegs );
410 assert( pCex->iPo >= 0 && pCex->iPo < Saig_ManPoNum(pAig) );
411
412 // map PIs of the unrolled frames into PIs of the original design
413 *pvMapPiF2A = Vec_IntAlloc( 1000 );
414
415 // collect COs and Objs visited in each frame
416 vFrameCos = Vec_VecStart( pCex->iFrame+1 );
417 vFrameObjs = Vec_VecStart( pCex->iFrame+1 );
418 // initialized the topmost frame
419 pObj = Aig_ManCo( pAig, pCex->iPo );
420 Vec_VecPushInt( vFrameCos, pCex->iFrame, Aig_ObjId(pObj) );
421 for ( f = pCex->iFrame; f >= 0; f-- )
422 {
423 // collect nodes starting from the roots
424 Aig_ManIncrementTravId( pAig );
425 vRoots = Vec_VecEntryInt( vFrameCos, f );
426 Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
427 Saig_ManCbaUnrollCollect_rec( pAig, pObj,
428 Vec_VecEntryInt(vFrameObjs, f),
429 (Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) );
430 }
431
432 // derive unrolled timeframes
433 pFrames = Aig_ManStart( 10000 );
434 pFrames->pName = Abc_UtilStrsav( pAig->pName );
435 pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
436 // initialize the flops
437 if ( Saig_ManRegNum(pAig) == pCex->nRegs )
438 {
439 Saig_ManForEachLo( pAig, pObj, i )
440 pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, i) );
441 }
442 else // this is the case when synthesis was applied, assume all-0 init state
443 {
444 Saig_ManForEachLo( pAig, pObj, i )
445 pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), 1 );
446 }
447 // iterate through the frames
448 for ( f = 0; f <= pCex->iFrame; f++ )
449 {
450 // construct
451 vObjs = Vec_VecEntryInt( vFrameObjs, f );
452 Aig_ManForEachObjVec( vObjs, pAig, pObj, i )
453 {
454 if ( Aig_ObjIsNode(pObj) )
455 pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
456 else if ( Aig_ObjIsCo(pObj) )
457 pObj->pData = Aig_ObjChild0Copy(pObj);
458 else if ( Aig_ObjIsConst1(pObj) )
459 pObj->pData = Aig_ManConst1(pFrames);
460 else if ( Saig_ObjIsPi(pAig, pObj) )
461 {
462 if ( Aig_ObjCioId(pObj) < nInputs )
463 {
464 int iBit = pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj);
465 pObj->pData = Aig_NotCond( Aig_ManConst1(pFrames), !Abc_InfoHasBit(pCex->pData, iBit) );
466 }
467 else
468 {
469 pObj->pData = Aig_ObjCreateCi( pFrames );
470 Vec_IntPush( *pvMapPiF2A, Aig_ObjCioId(pObj) );
471 Vec_IntPush( *pvMapPiF2A, f );
472 }
473 }
474 }
475 if ( f == pCex->iFrame )
476 break;
477 // transfer
478 vRoots = Vec_VecEntryInt( vFrameCos, f );
479 Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
480 {
481 Saig_ObjLiToLo( pAig, pObj )->pData = pObj->pData;
482 if ( *pvReg2Frame )
483 {
484 Vec_VecPushInt( *pvReg2Frame, f, Aig_ObjId(pObj) ); // record LO
485 Vec_VecPushInt( *pvReg2Frame, f, Aig_ObjToLit((Aig_Obj_t *)pObj->pData) ); // record its literal
486 }
487 }
488 }
489 // create output
490 pObj = Aig_ManCo( pAig, pCex->iPo );
491 Aig_ObjCreateCo( pFrames, Aig_Not((Aig_Obj_t *)pObj->pData) );
492 Aig_ManSetRegNum( pFrames, 0 );
493 // cleanup
494 Vec_VecFree( vFrameCos );
495 Vec_VecFree( vFrameObjs );
496 // finallize
497 Aig_ManCleanup( pFrames );
498 // return
499 return pFrames;
500 }
501
502 /**Function*************************************************************
503
504 Synopsis [Creates refinement manager.]
505
506 Description []
507
508 SideEffects []
509
510 SeeAlso []
511
512 ***********************************************************************/
Saig_ManCbaStart(Aig_Man_t * pAig,Abc_Cex_t * pCex,int nInputs,int fVerbose)513 Saig_ManCba_t * Saig_ManCbaStart( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose )
514 {
515 Saig_ManCba_t * p;
516 p = ABC_CALLOC( Saig_ManCba_t, 1 );
517 p->pAig = pAig;
518 p->pCex = pCex;
519 p->nInputs = nInputs;
520 p->fVerbose = fVerbose;
521 return p;
522 }
523
524 /**Function*************************************************************
525
526 Synopsis [Destroys refinement manager.]
527
528 Description []
529
530 SideEffects []
531
532 SeeAlso []
533
534 ***********************************************************************/
Saig_ManCbaStop(Saig_ManCba_t * p)535 void Saig_ManCbaStop( Saig_ManCba_t * p )
536 {
537 Vec_VecFreeP( &p->vReg2Frame );
538 Vec_VecFreeP( &p->vReg2Value );
539 Aig_ManStopP( &p->pFrames );
540 Vec_IntFreeP( &p->vMapPiF2A );
541 ABC_FREE( p );
542 }
543
544 /**Function*************************************************************
545
546 Synopsis [Destroys refinement manager.]
547
548 Description []
549
550 SideEffects []
551
552 SeeAlso []
553
554 ***********************************************************************/
Saig_ManCbaShrink(Saig_ManCba_t * p)555 void Saig_ManCbaShrink( Saig_ManCba_t * p )
556 {
557 Aig_Man_t * pManNew;
558 Aig_Obj_t * pObjLi, * pObjFrame;
559 Vec_Int_t * vLevel, * vLevel2;
560 int f, k, ObjId, Lit;
561 // assuming that important objects are labeled in Saig_ManCbaFindReason()
562 Vec_VecForEachLevelInt( p->vReg2Frame, vLevel, f )
563 {
564 Vec_IntForEachEntryDouble( vLevel, ObjId, Lit, k )
565 {
566 pObjFrame = Aig_ManObj( p->pFrames, Abc_Lit2Var(Lit) );
567 if ( pObjFrame == NULL || (!Aig_ObjIsConst1(pObjFrame) && !Aig_ObjIsTravIdCurrent(p->pFrames, pObjFrame)) )
568 continue;
569 pObjLi = Aig_ManObj( p->pAig, ObjId );
570 assert( Saig_ObjIsLi(p->pAig, pObjLi) );
571 Vec_VecPushInt( p->vReg2Value, f, Abc_Var2Lit( Aig_ObjCioId(pObjLi) - Saig_ManPoNum(p->pAig), Abc_LitIsCompl(Lit) ^ !pObjFrame->fPhase ) );
572 }
573 }
574 // print statistics
575 Vec_VecForEachLevelInt( p->vReg2Frame, vLevel, k )
576 {
577 vLevel2 = Vec_VecEntryInt( p->vReg2Value, k );
578 printf( "Level = %4d StateBits = %4d (%6.2f %%) CareBits = %4d (%6.2f %%)\n", k,
579 Vec_IntSize(vLevel)/2, 100.0 * (Vec_IntSize(vLevel)/2) / Aig_ManRegNum(p->pAig),
580 Vec_IntSize(vLevel2), 100.0 * Vec_IntSize(vLevel2) / Aig_ManRegNum(p->pAig) );
581 }
582 // try reducing the frames
583 pManNew = Saig_ManDupWithCubes( p->pAig, p->vReg2Value );
584 // Ioa_WriteAiger( pManNew, "aigcube.aig", 0, 0 );
585 Aig_ManStop( pManNew );
586 }
587
Saig_ObjCexMinSet0(Aig_Obj_t * pObj)588 static inline void Saig_ObjCexMinSet0( Aig_Obj_t * pObj ) { pObj->fMarkA = 1; pObj->fMarkB = 0; }
Saig_ObjCexMinSet1(Aig_Obj_t * pObj)589 static inline void Saig_ObjCexMinSet1( Aig_Obj_t * pObj ) { pObj->fMarkA = 0; pObj->fMarkB = 1; }
Saig_ObjCexMinSetX(Aig_Obj_t * pObj)590 static inline void Saig_ObjCexMinSetX( Aig_Obj_t * pObj ) { pObj->fMarkA = 1; pObj->fMarkB = 1; }
591
Saig_ObjCexMinGet0(Aig_Obj_t * pObj)592 static inline int Saig_ObjCexMinGet0( Aig_Obj_t * pObj ) { return pObj->fMarkA && !pObj->fMarkB; }
Saig_ObjCexMinGet1(Aig_Obj_t * pObj)593 static inline int Saig_ObjCexMinGet1( Aig_Obj_t * pObj ) { return !pObj->fMarkA && pObj->fMarkB; }
Saig_ObjCexMinGetX(Aig_Obj_t * pObj)594 static inline int Saig_ObjCexMinGetX( Aig_Obj_t * pObj ) { return pObj->fMarkA && pObj->fMarkB; }
595
Saig_ObjCexMinGet0Fanin0(Aig_Obj_t * pObj)596 static inline int Saig_ObjCexMinGet0Fanin0( Aig_Obj_t * pObj ) { return (Saig_ObjCexMinGet1(Aig_ObjFanin0(pObj)) && Aig_ObjFaninC0(pObj)) || (Saig_ObjCexMinGet0(Aig_ObjFanin0(pObj)) && !Aig_ObjFaninC0(pObj)); }
Saig_ObjCexMinGet1Fanin0(Aig_Obj_t * pObj)597 static inline int Saig_ObjCexMinGet1Fanin0( Aig_Obj_t * pObj ) { return (Saig_ObjCexMinGet0(Aig_ObjFanin0(pObj)) && Aig_ObjFaninC0(pObj)) || (Saig_ObjCexMinGet1(Aig_ObjFanin0(pObj)) && !Aig_ObjFaninC0(pObj)); }
598
Saig_ObjCexMinGet0Fanin1(Aig_Obj_t * pObj)599 static inline int Saig_ObjCexMinGet0Fanin1( Aig_Obj_t * pObj ) { return (Saig_ObjCexMinGet1(Aig_ObjFanin1(pObj)) && Aig_ObjFaninC1(pObj)) || (Saig_ObjCexMinGet0(Aig_ObjFanin1(pObj)) && !Aig_ObjFaninC1(pObj)); }
Saig_ObjCexMinGet1Fanin1(Aig_Obj_t * pObj)600 static inline int Saig_ObjCexMinGet1Fanin1( Aig_Obj_t * pObj ) { return (Saig_ObjCexMinGet0(Aig_ObjFanin1(pObj)) && Aig_ObjFaninC1(pObj)) || (Saig_ObjCexMinGet1(Aig_ObjFanin1(pObj)) && !Aig_ObjFaninC1(pObj)); }
601
Saig_ObjCexMinSim(Aig_Obj_t * pObj)602 static inline void Saig_ObjCexMinSim( Aig_Obj_t * pObj )
603 {
604 if ( Aig_ObjIsAnd(pObj) )
605 {
606 if ( Saig_ObjCexMinGet0Fanin0(pObj) || Saig_ObjCexMinGet0Fanin1(pObj) )
607 Saig_ObjCexMinSet0( pObj );
608 else if ( Saig_ObjCexMinGet1Fanin0(pObj) && Saig_ObjCexMinGet1Fanin1(pObj) )
609 Saig_ObjCexMinSet1( pObj );
610 else
611 Saig_ObjCexMinSetX( pObj );
612 }
613 else if ( Aig_ObjIsCo(pObj) )
614 {
615 if ( Saig_ObjCexMinGet0Fanin0(pObj) )
616 Saig_ObjCexMinSet0( pObj );
617 else if ( Saig_ObjCexMinGet1Fanin0(pObj) )
618 Saig_ObjCexMinSet1( pObj );
619 else
620 Saig_ObjCexMinSetX( pObj );
621 }
622 else assert( 0 );
623 }
624
Saig_ObjCexMinPrint(Aig_Obj_t * pObj)625 static inline void Saig_ObjCexMinPrint( Aig_Obj_t * pObj )
626 {
627 if ( Saig_ObjCexMinGet0(pObj) )
628 printf( "0" );
629 else if ( Saig_ObjCexMinGet1(pObj) )
630 printf( "1" );
631 else if ( Saig_ObjCexMinGetX(pObj) )
632 printf( "X" );
633 }
634
635 /**Function*************************************************************
636
637 Synopsis []
638
639 Description []
640
641
642 SideEffects []
643
644 SeeAlso []
645
646 ***********************************************************************/
Saig_ManCexVerifyUsingTernary(Aig_Man_t * pAig,Abc_Cex_t * pCex,Abc_Cex_t * pCare)647 int Saig_ManCexVerifyUsingTernary( Aig_Man_t * pAig, Abc_Cex_t * pCex, Abc_Cex_t * pCare )
648 {
649 Aig_Obj_t * pObj, * pObjRi, * pObjRo;
650 int i, f, iBit = 0;
651 assert( pCex->iFrame == pCare->iFrame );
652 assert( pCex->nBits == pCare->nBits );
653 assert( pCex->iPo < Saig_ManPoNum(pAig) );
654 Saig_ObjCexMinSet1( Aig_ManConst1(pAig) );
655 // set flops to the init state
656 Saig_ManForEachLo( pAig, pObj, i )
657 {
658 assert( !Abc_InfoHasBit(pCex->pData, iBit) );
659 assert( !Abc_InfoHasBit(pCare->pData, iBit) );
660 // if ( Abc_InfoHasBit(pCare->pData, iBit++) )
661 Saig_ObjCexMinSet0( pObj );
662 // else
663 // Saig_ObjCexMinSetX( pObj );
664 }
665 iBit = pCex->nRegs;
666 for ( f = 0; f <= pCex->iFrame; f++ )
667 {
668 // init inputs
669 Saig_ManForEachPi( pAig, pObj, i )
670 {
671 if ( Abc_InfoHasBit(pCare->pData, iBit++) )
672 {
673 if ( Abc_InfoHasBit(pCex->pData, iBit-1) )
674 Saig_ObjCexMinSet1( pObj );
675 else
676 Saig_ObjCexMinSet0( pObj );
677 }
678 else
679 Saig_ObjCexMinSetX( pObj );
680 }
681 // simulate internal nodes
682 Aig_ManForEachNode( pAig, pObj, i )
683 Saig_ObjCexMinSim( pObj );
684 // simulate COs
685 Aig_ManForEachCo( pAig, pObj, i )
686 Saig_ObjCexMinSim( pObj );
687 /*
688 Aig_ManForEachObj( pAig, pObj, i )
689 {
690 Aig_ObjPrint(pAig, pObj);
691 printf( " Value = " );
692 Saig_ObjCexMinPrint( pObj );
693 printf( "\n" );
694 }
695 */
696 // transfer
697 Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, i )
698 pObjRo->fMarkA = pObjRi->fMarkA,
699 pObjRo->fMarkB = pObjRi->fMarkB;
700 }
701 assert( iBit == pCex->nBits );
702 return Saig_ObjCexMinGet1( Aig_ManCo( pAig, pCex->iPo ) );
703 }
704
705 /**Function*************************************************************
706
707 Synopsis [SAT-based refinement of the counter-example.]
708
709 Description [The first parameter (nInputs) indicates how many first
710 primary inputs to skip without considering as care candidates.]
711
712
713 SideEffects []
714
715 SeeAlso []
716
717 ***********************************************************************/
Saig_ManCbaFindCexCareBits(Aig_Man_t * pAig,Abc_Cex_t * pCex,int nInputs,int fVerbose)718 Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose )
719 {
720 Saig_ManCba_t * p;
721 Vec_Int_t * vReasons;
722 Abc_Cex_t * pCare;
723 abctime clk = Abc_Clock();
724
725 clk = Abc_Clock();
726 p = Saig_ManCbaStart( pAig, pCex, nInputs, fVerbose );
727
728 // p->vReg2Frame = Vec_VecStart( pCex->iFrame );
729 // p->vReg2Value = Vec_VecStart( pCex->iFrame );
730 p->pFrames = Saig_ManCbaUnrollWithCex( pAig, pCex, nInputs, &p->vMapPiF2A, &p->vReg2Frame );
731 vReasons = Saig_ManCbaFindReason( p );
732 if ( p->vReg2Frame )
733 Saig_ManCbaShrink( p );
734
735
736 //if ( fVerbose )
737 //Aig_ManPrintStats( p->pFrames );
738
739 if ( fVerbose )
740 {
741 Vec_Int_t * vRes = Saig_ManCbaReason2Inputs( p, vReasons );
742 printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ",
743 Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
744 Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
745 Vec_IntFree( vRes );
746 ABC_PRT( "Time", Abc_Clock() - clk );
747 }
748
749 pCare = Saig_ManCbaReason2Cex( p, vReasons );
750 Vec_IntFree( vReasons );
751 Saig_ManCbaStop( p );
752
753 if ( fVerbose )
754 {
755 printf( "Real " );
756 Abc_CexPrintStats( pCex );
757 }
758 if ( fVerbose )
759 {
760 printf( "Care " );
761 Abc_CexPrintStats( pCare );
762 }
763 /*
764 // verify the reduced counter-example using ternary simulation
765 if ( !Saig_ManCexVerifyUsingTernary( pAig, pCex, pCare ) )
766 printf( "Saig_ManCbaFindCexCareBits(): Minimized counter-example verification has failed!!!\n" );
767 else if ( fVerbose )
768 printf( "Saig_ManCbaFindCexCareBits(): Minimized counter-example verification is successful.\n" );
769 */
770 Aig_ManCleanMarkAB( pAig );
771 return pCare;
772 }
773
774 /**Function*************************************************************
775
776 Synopsis [Returns the array of PIs for flops that should not be absracted.]
777
778 Description []
779
780 SideEffects []
781
782 SeeAlso []
783
784 ***********************************************************************/
Saig_ManCbaFilterInputs(Aig_Man_t * pAig,int iFirstFlopPi,Abc_Cex_t * pCex,int fVerbose)785 Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose )
786 {
787 Saig_ManCba_t * p;
788 Vec_Int_t * vRes, * vReasons;
789 abctime clk;
790 if ( Saig_ManPiNum(pAig) != pCex->nPis )
791 {
792 printf( "Saig_ManCbaFilterInputs(): The PI count of AIG (%d) does not match that of cex (%d).\n",
793 Aig_ManCiNum(pAig), pCex->nPis );
794 return NULL;
795 }
796
797 clk = Abc_Clock();
798 p = Saig_ManCbaStart( pAig, pCex, iFirstFlopPi, fVerbose );
799 p->pFrames = Saig_ManCbaUnrollWithCex( pAig, pCex, iFirstFlopPi, &p->vMapPiF2A, &p->vReg2Frame );
800 vReasons = Saig_ManCbaFindReason( p );
801 vRes = Saig_ManCbaReason2Inputs( p, vReasons );
802 if ( fVerbose )
803 {
804 printf( "Frame PIs = %4d (essential = %4d) AIG PIs = %4d (essential = %4d) ",
805 Aig_ManCiNum(p->pFrames), Vec_IntSize(vReasons),
806 Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
807 ABC_PRT( "Time", Abc_Clock() - clk );
808 }
809
810 Vec_IntFree( vReasons );
811 Saig_ManCbaStop( p );
812 return vRes;
813 }
814
815
816
817
818 /**Function*************************************************************
819
820 Synopsis [Checks the abstracted model for a counter-example.]
821
822 Description [Returns the array of abstracted flops that should be added
823 to the abstraction.]
824
825 SideEffects []
826
827 SeeAlso []
828
829 ***********************************************************************/
Saig_ManCbaPerform(Aig_Man_t * pAbs,int nInputs,Saig_ParBmc_t * pPars)830 Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAbs, int nInputs, Saig_ParBmc_t * pPars )
831 {
832 Vec_Int_t * vAbsFfsToAdd;
833 int RetValue;
834 abctime clk = Abc_Clock();
835 // assert( pAbs->nRegs > 0 );
836 // perform BMC
837 RetValue = Saig_ManBmcScalable( pAbs, pPars );
838 if ( RetValue == -1 ) // time out - nothing to add
839 {
840 printf( "Resource limit is reached during BMC.\n" );
841 assert( pAbs->pSeqModel == NULL );
842 return Vec_IntAlloc( 0 );
843 }
844 if ( pAbs->pSeqModel == NULL )
845 {
846 printf( "BMC did not detect a CEX with the given depth.\n" );
847 return Vec_IntAlloc( 0 );
848 }
849 if ( pPars->fVerbose )
850 Abc_CexPrintStats( pAbs->pSeqModel );
851 // CEX is detected - refine the flops
852 vAbsFfsToAdd = Saig_ManCbaFilterInputs( pAbs, nInputs, pAbs->pSeqModel, pPars->fVerbose );
853 if ( Vec_IntSize(vAbsFfsToAdd) == 0 )
854 {
855 Vec_IntFree( vAbsFfsToAdd );
856 return NULL;
857 }
858 if ( pPars->fVerbose )
859 {
860 printf( "Adding %d registers to the abstraction (total = %d). ",
861 Vec_IntSize(vAbsFfsToAdd), Aig_ManRegNum(pAbs)+Vec_IntSize(vAbsFfsToAdd) );
862 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
863 }
864 return vAbsFfsToAdd;
865 }
866
867 ////////////////////////////////////////////////////////////////////////
868 /// END OF FILE ///
869 ////////////////////////////////////////////////////////////////////////
870
871
872 ABC_NAMESPACE_IMPL_END
873
874