1 /**CFile****************************************************************
2
3 FileName [absOut.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [Abstraction package.]
8
9 Synopsis [Abstraction refinement outside of abstraction engines.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: absOut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "abs.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 ////////////////////////////////////////////////////////////////////////
31 /// FUNCTION DEFINITIONS ///
32 ////////////////////////////////////////////////////////////////////////
33
34 /**Function*************************************************************
35
36 Synopsis [Derive a new counter-example.]
37
38 Description []
39
40 SideEffects []
41
42 SeeAlso []
43
44 ***********************************************************************/
Gia_ManCexRemap(Gia_Man_t * p,Abc_Cex_t * pCexAbs,Vec_Int_t * vPis)45 Abc_Cex_t * Gia_ManCexRemap( Gia_Man_t * p, Abc_Cex_t * pCexAbs, Vec_Int_t * vPis )
46 {
47 Abc_Cex_t * pCex;
48 int i, f, iPiNum;
49 assert( pCexAbs->iPo == 0 );
50 // start the counter-example
51 pCex = Abc_CexAlloc( Gia_ManRegNum(p), Gia_ManPiNum(p), pCexAbs->iFrame+1 );
52 pCex->iFrame = pCexAbs->iFrame;
53 pCex->iPo = pCexAbs->iPo;
54 // copy the bit data
55 for ( f = 0; f <= pCexAbs->iFrame; f++ )
56 for ( i = 0; i < Vec_IntSize(vPis); i++ )
57 {
58 if ( Abc_InfoHasBit( pCexAbs->pData, pCexAbs->nRegs + pCexAbs->nPis * f + i ) )
59 {
60 iPiNum = Gia_ObjCioId( Gia_ManObj(p, Vec_IntEntry(vPis, i)) );
61 Abc_InfoSetBit( pCex->pData, pCex->nRegs + pCex->nPis * f + iPiNum );
62 }
63 }
64 // verify the counter example
65 if ( !Gia_ManVerifyCex( p, pCex, 0 ) )
66 {
67 Abc_Print( 1, "Gia_ManCexRemap(): Counter-example is invalid.\n" );
68 Abc_CexFree( pCex );
69 pCex = NULL;
70 }
71 else
72 {
73 Abc_Print( 1, "Counter-example verification is successful.\n" );
74 Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. \n", pCex->iPo, p->pName, pCex->iFrame );
75 }
76 return pCex;
77 }
78
79 /**Function*************************************************************
80
81 Synopsis [Refines gate-level abstraction using the counter-example.]
82
83 Description []
84
85 SideEffects []
86
87 SeeAlso []
88
89 ***********************************************************************/
Gia_ManGlaRefine(Gia_Man_t * p,Abc_Cex_t * pCex,int fMinCut,int fVerbose)90 int Gia_ManGlaRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int fMinCut, int fVerbose )
91 {
92 extern void Nwk_ManDeriveMinCut( Gia_Man_t * p, int fVerbose );
93 int fAddOneLayer = 1;
94 Abc_Cex_t * pCexNew = NULL;
95 Gia_Man_t * pAbs;
96 Aig_Man_t * pAig;
97 Abc_Cex_t * pCare;
98 Vec_Int_t * vPis, * vPPis;
99 int f, i, iObjId;
100 abctime clk = Abc_Clock();
101 int nOnes = 0, Counter = 0;
102 if ( p->vGateClasses == NULL )
103 {
104 Abc_Print( 1, "Gia_ManGlaRefine(): Abstraction gate map is missing.\n" );
105 return -1;
106 }
107 // derive abstraction
108 pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
109 Gia_ManStop( pAbs );
110 pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
111 if ( Gia_ManPiNum(pAbs) != pCex->nPis )
112 {
113 Abc_Print( 1, "Gia_ManGlaRefine(): The PI counts in GLA and in CEX do not match.\n" );
114 Gia_ManStop( pAbs );
115 return -1;
116 }
117 if ( !Gia_ManVerifyCex( pAbs, pCex, 0 ) )
118 {
119 Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is invalid.\n" );
120 // Gia_ManStop( pAbs );
121 // return -1;
122 }
123 // else
124 // Abc_Print( 1, "Gia_ManGlaRefine(): The initial counter-example is correct.\n" );
125 // get inputs
126 Gia_ManGlaCollect( p, p->vGateClasses, &vPis, &vPPis, NULL, NULL );
127 assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) );
128 // add missing logic
129 if ( fAddOneLayer )
130 {
131 Gia_Obj_t * pObj;
132 // check if this is a real counter-example
133 Gia_ObjTerSimSet0( Gia_ManConst0(pAbs) );
134 for ( f = 0; f <= pCex->iFrame; f++ )
135 {
136 Gia_ManForEachPi( pAbs, pObj, i )
137 {
138 if ( i >= Vec_IntSize(vPis) ) // PPIs
139 Gia_ObjTerSimSetX( pObj );
140 else if ( Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) )
141 Gia_ObjTerSimSet1( pObj );
142 else
143 Gia_ObjTerSimSet0( pObj );
144 }
145 Gia_ManForEachRo( pAbs, pObj, i )
146 {
147 if ( f == 0 )
148 Gia_ObjTerSimSet0( pObj );
149 else
150 Gia_ObjTerSimRo( pAbs, pObj );
151 }
152 Gia_ManForEachAnd( pAbs, pObj, i )
153 Gia_ObjTerSimAnd( pObj );
154 Gia_ManForEachCo( pAbs, pObj, i )
155 Gia_ObjTerSimCo( pObj );
156 }
157 pObj = Gia_ManPo( pAbs, 0 );
158 if ( Gia_ObjTerSimGet1(pObj) )
159 {
160 pCexNew = Gia_ManCexRemap( p, pCex, vPis );
161 Abc_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame );
162 }
163 // else
164 // Abc_Print( 1, "CEX is not real.\n" );
165 Gia_ManForEachObj( pAbs, pObj, i )
166 Gia_ObjTerSimSetC( pObj );
167 if ( pCexNew == NULL )
168 {
169 // grow one layer
170 Vec_IntForEachEntry( vPPis, iObjId, i )
171 {
172 assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
173 Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
174 }
175 if ( fVerbose )
176 {
177 Abc_Print( 1, "Additional objects = %d. ", Vec_IntSize(vPPis) );
178 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
179 }
180 }
181 }
182 else
183 {
184 // minimize the CEX
185 pAig = Gia_ManToAigSimple( pAbs );
186 pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, Vec_IntSize(vPis), fVerbose );
187 Aig_ManStop( pAig );
188 if ( pCare == NULL )
189 Abc_Print( 1, "Counter-example minimization has failed.\n" );
190 // add new objects to the map
191 iObjId = -1;
192 for ( f = 0; f <= pCare->iFrame; f++ )
193 for ( i = 0; i < pCare->nPis; i++ )
194 if ( Abc_InfoHasBit( pCare->pData, pCare->nRegs + f * pCare->nPis + i ) )
195 {
196 nOnes++;
197 assert( i >= Vec_IntSize(vPis) );
198 iObjId = Vec_IntEntry( vPPis, i - Vec_IntSize(vPis) );
199 assert( iObjId > 0 && iObjId < Gia_ManObjNum(p) );
200 if ( Vec_IntEntry( p->vGateClasses, iObjId ) > 0 )
201 continue;
202 assert( Vec_IntEntry( p->vGateClasses, iObjId ) == 0 );
203 Vec_IntWriteEntry( p->vGateClasses, iObjId, 1 );
204 // Abc_Print( 1, "Adding object %d.\n", iObjId );
205 // Gia_ObjPrint( p, Gia_ManObj(p, iObjId) );
206 Counter++;
207 }
208 Abc_CexFree( pCare );
209 if ( fVerbose )
210 {
211 Abc_Print( 1, "Essential bits = %d. Additional objects = %d. ", nOnes, Counter );
212 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
213 }
214 // consider the case of SAT
215 if ( iObjId == -1 )
216 {
217 pCexNew = Gia_ManCexRemap( p, pCex, vPis );
218 Abc_Print( 1, "Procedure &gla_refine found a real counter-example in frame %d.\n", pCexNew->iFrame );
219 }
220 }
221 Vec_IntFree( vPis );
222 Vec_IntFree( vPPis );
223 Gia_ManStop( pAbs );
224 if ( pCexNew )
225 {
226 ABC_FREE( p->pCexSeq );
227 p->pCexSeq = pCexNew;
228 return 0;
229 }
230 // extract abstraction to include min-cut
231 if ( fMinCut )
232 Nwk_ManDeriveMinCut( p, fVerbose );
233 return -1;
234 }
235
236
237
238
239
240 /**Function*************************************************************
241
242 Synopsis [Resimulates the counter-example and returns flop values.]
243
244 Description []
245
246 SideEffects []
247
248 SeeAlso []
249
250 ***********************************************************************/
Gia_ManGetStateAndCheckCex(Gia_Man_t * pAig,Abc_Cex_t * p,int iFrame)251 Vec_Int_t * Gia_ManGetStateAndCheckCex( Gia_Man_t * pAig, Abc_Cex_t * p, int iFrame )
252 {
253 Vec_Int_t * vInit = Vec_IntAlloc( Gia_ManRegNum(pAig) );
254 Gia_Obj_t * pObj, * pObjRi, * pObjRo;
255 int RetValue, i, k, iBit = 0;
256 assert( iFrame >= 0 && iFrame <= p->iFrame );
257 Gia_ManCleanMark0(pAig);
258 Gia_ManForEachRo( pAig, pObj, i )
259 pObj->fMark0 = 0;//Abc_InfoHasBit(p->pData, iBit++);
260 for ( i = 0, iBit = p->nRegs; i <= p->iFrame; i++ )
261 {
262 if ( i == iFrame )
263 {
264 Gia_ManForEachRo( pAig, pObjRo, k )
265 Vec_IntPush( vInit, pObjRo->fMark0 );
266 }
267 Gia_ManForEachPi( pAig, pObj, k )
268 pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
269 Gia_ManForEachAnd( pAig, pObj, k )
270 pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
271 (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
272 Gia_ManForEachCo( pAig, pObj, k )
273 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
274 if ( i == p->iFrame )
275 break;
276 Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
277 pObjRo->fMark0 = pObjRi->fMark0;
278 }
279 assert( iBit == p->nBits );
280 RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
281 if ( RetValue != 1 )
282 Vec_IntFreeP( &vInit );
283 Gia_ManCleanMark0(pAig);
284 return vInit;
285 }
286
287 /**Function*************************************************************
288
289 Synopsis [Verify counter-example starting in the given timeframe.]
290
291 Description []
292
293 SideEffects []
294
295 SeeAlso []
296
297 ***********************************************************************/
Gia_ManCheckCex(Gia_Man_t * pAig,Abc_Cex_t * p,int iFrame)298 void Gia_ManCheckCex( Gia_Man_t * pAig, Abc_Cex_t * p, int iFrame )
299 {
300 Gia_Obj_t * pObj, * pObjRi, * pObjRo;
301 int RetValue, i, k, iBit = 0;
302 assert( iFrame >= 0 && iFrame <= p->iFrame );
303 Gia_ManCleanMark0(pAig);
304 Gia_ManForEachRo( pAig, pObj, i )
305 pObj->fMark0 = 0;//Abc_InfoHasBit(p->pData, iBit++);
306 for ( i = iFrame, iBit += p->nRegs + Gia_ManPiNum(pAig) * iFrame; i <= p->iFrame; i++ )
307 {
308 Gia_ManForEachPi( pAig, pObj, k )
309 pObj->fMark0 = Abc_InfoHasBit(p->pData, iBit++);
310 Gia_ManForEachAnd( pAig, pObj, k )
311 pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) &
312 (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
313 Gia_ManForEachCo( pAig, pObj, k )
314 pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj);
315 if ( i == p->iFrame )
316 break;
317 Gia_ManForEachRiRo( pAig, pObjRi, pObjRo, k )
318 pObjRo->fMark0 = pObjRi->fMark0;
319 }
320 assert( iBit == p->nBits );
321 RetValue = Gia_ManPo(pAig, p->iPo)->fMark0;
322 Gia_ManCleanMark0(pAig);
323 if ( RetValue == 1 )
324 printf( "Shortened CEX holds for the abstraction of the fast-forwarded model.\n" );
325 else
326 printf( "Shortened CEX does not hold for the abstraction of the fast-forwarded model.\n" );
327 }
328
329 /**Function*************************************************************
330
331 Synopsis []
332
333 Description []
334
335 SideEffects []
336
337 SeeAlso []
338
339 ***********************************************************************/
Gia_ManTransformFlops(Gia_Man_t * p,Vec_Int_t * vFlops,Vec_Int_t * vInit)340 Gia_Man_t * Gia_ManTransformFlops( Gia_Man_t * p, Vec_Int_t * vFlops, Vec_Int_t * vInit )
341 {
342 Vec_Bit_t * vInitNew;
343 Gia_Man_t * pNew;
344 Gia_Obj_t * pObj;
345 int i, iFlopId;
346 assert( Vec_IntSize(vInit) == Vec_IntSize(vFlops) );
347 vInitNew = Vec_BitStart( Gia_ManRegNum(p) );
348 Gia_ManForEachObjVec( vFlops, p, pObj, i )
349 {
350 assert( Gia_ObjIsRo(p, pObj) );
351 if ( Vec_IntEntry(vInit, i) == 0 )
352 continue;
353 iFlopId = Gia_ObjCioId(pObj) - Gia_ManPiNum(p);
354 assert( iFlopId >= 0 && iFlopId < Gia_ManRegNum(p) );
355 Vec_BitWriteEntry( vInitNew, iFlopId, 1 );
356 }
357 pNew = Gia_ManDupFlip( p, Vec_BitArray(vInitNew) );
358 Vec_BitFree( vInitNew );
359 return pNew;
360 }
361
362 /**Function*************************************************************
363
364 Synopsis []
365
366 Description []
367
368 SideEffects []
369
370 SeeAlso []
371
372 ***********************************************************************/
Gia_ManNewRefine(Gia_Man_t * p,Abc_Cex_t * pCex,int iFrameStart,int iFrameExtra,int fVerbose)373 int Gia_ManNewRefine( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int iFrameExtra, int fVerbose )
374 {
375 Gia_Man_t * pAbs, * pNew;
376 Vec_Int_t * vFlops, * vInit;
377 Vec_Int_t * vCopy;
378 // abctime clk = Abc_Clock();
379 int RetValue;
380 ABC_FREE( p->pCexSeq );
381 if ( p->vGateClasses == NULL )
382 {
383 Abc_Print( 1, "Gia_ManNewRefine(): Abstraction gate map is missing.\n" );
384 return -1;
385 }
386 vCopy = Vec_IntDup( p->vGateClasses );
387 Abc_Print( 1, "Refining with %d-frame CEX, starting in frame %d, with %d extra frames.\n", pCex->iFrame, iFrameStart, iFrameExtra );
388 // derive abstraction
389 pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
390 Gia_ManStop( pAbs );
391 pAbs = Gia_ManDupAbsGates( p, p->vGateClasses );
392 if ( Gia_ManPiNum(pAbs) != pCex->nPis )
393 {
394 Abc_Print( 1, "Gia_ManNewRefine(): The PI counts in GLA and in CEX do not match.\n" );
395 Gia_ManStop( pAbs );
396 Vec_IntFree( vCopy );
397 return -1;
398 }
399 // get the state in frame iFrameStart
400 vInit = Gia_ManGetStateAndCheckCex( pAbs, pCex, iFrameStart );
401 if ( vInit == NULL )
402 {
403 Abc_Print( 1, "Gia_ManNewRefine(): The initial counter-example is invalid.\n" );
404 Gia_ManStop( pAbs );
405 Vec_IntFree( vCopy );
406 return -1;
407 }
408 if ( fVerbose )
409 Abc_Print( 1, "Gia_ManNewRefine(): The initial counter-example is correct.\n" );
410 // get inputs
411 Gia_ManGlaCollect( p, p->vGateClasses, NULL, NULL, &vFlops, NULL );
412 // assert( Vec_IntSize(vPis) + Vec_IntSize(vPPis) == Gia_ManPiNum(pAbs) );
413 Gia_ManStop( pAbs );
414 //Vec_IntPrint( vFlops );
415 //Vec_IntPrint( vInit );
416 // transform the manager to have new init state
417 pNew = Gia_ManTransformFlops( p, vFlops, vInit );
418 Vec_IntFree( vFlops );
419 Vec_IntFree( vInit );
420 // verify abstraction
421 {
422 Gia_Man_t * pAbs = Gia_ManDupAbsGates( pNew, p->vGateClasses );
423 Gia_ManCheckCex( pAbs, pCex, iFrameStart );
424 Gia_ManStop( pAbs );
425 }
426 // transfer abstraction
427 assert( pNew->vGateClasses == NULL );
428 pNew->vGateClasses = Vec_IntDup( p->vGateClasses );
429 // perform abstraction for the new AIG
430 {
431 Abs_Par_t Pars, * pPars = &Pars;
432 Abs_ParSetDefaults( pPars );
433 pPars->nFramesMax = pCex->iFrame - iFrameStart + 1 + iFrameExtra;
434 pPars->fVerbose = fVerbose;
435 RetValue = Gia_ManPerformGla( pNew, pPars );
436 if ( RetValue == 0 ) // spurious SAT
437 {
438 Vec_IntFreeP( &pNew->vGateClasses );
439 pNew->vGateClasses = Vec_IntDup( vCopy );
440 }
441 }
442 // move the abstraction map
443 Vec_IntFreeP( &p->vGateClasses );
444 p->vGateClasses = pNew->vGateClasses;
445 pNew->vGateClasses = NULL;
446 // cleanup
447 Gia_ManStop( pNew );
448 Vec_IntFree( vCopy );
449 return -1;
450 }
451
452 ////////////////////////////////////////////////////////////////////////
453 /// END OF FILE ///
454 ////////////////////////////////////////////////////////////////////////
455
456
457 ABC_NAMESPACE_IMPL_END
458
459