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