1 /**CFile****************************************************************
2 
3   FileName    [sswSemi.c]
4 
5   SystemName  [ABC: Logic synthesis and verification system.]
6 
7   PackageName [Inductive prover with constraints.]
8 
9   Synopsis    [Semiformal for equivalence classes.]
10 
11   Author      [Alan Mishchenko]
12 
13   Affiliation [UC Berkeley]
14 
15   Date        [Ver. 1.0. Started - September 1, 2008.]
16 
17   Revision    [$Id: sswSemi.c,v 1.00 2008/09/01 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "sswInt.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 ///                        DECLARATIONS                              ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 typedef struct Ssw_Sem_t_ Ssw_Sem_t; // BMC manager
31 
32 struct Ssw_Sem_t_
33 {
34     // parameters
35     int              nConfMaxStart;  // the starting conflict limit
36     int              nConfMax;       // the intermediate conflict limit
37     int              nFramesSweep;   // the number of frames to sweep
38     int              fVerbose;       // prints output statistics
39     // equivalences considered
40     Ssw_Man_t *      pMan;           // SAT sweeping manager
41     Vec_Ptr_t *      vTargets;       // the nodes that are watched
42     // storage for patterns
43     int              nPatternsAlloc; // the max number of interesting states
44     int              nPatterns;      // the number of patterns
45     Vec_Ptr_t *      vPatterns;      // storage for the interesting states
46     Vec_Int_t *      vHistory;       // what state and how many steps
47 };
48 
49 ////////////////////////////////////////////////////////////////////////
50 ///                     FUNCTION DEFINITIONS                         ///
51 ////////////////////////////////////////////////////////////////////////
52 
53 /**Function*************************************************************
54 
55   Synopsis    []
56 
57   Description []
58 
59   SideEffects []
60 
61   SeeAlso     []
62 
63 ***********************************************************************/
Ssw_SemManStart(Ssw_Man_t * pMan,int nConfMax,int fVerbose)64 Ssw_Sem_t * Ssw_SemManStart( Ssw_Man_t * pMan, int nConfMax, int fVerbose )
65 {
66     Ssw_Sem_t * p;
67     Aig_Obj_t * pObj;
68     int i;
69     // create interpolation manager
70     p = ABC_ALLOC( Ssw_Sem_t, 1 );
71     memset( p, 0, sizeof(Ssw_Sem_t) );
72     p->nConfMaxStart  = nConfMax;
73     p->nConfMax       = nConfMax;
74     p->nFramesSweep   = Abc_MaxInt( (1<<21)/Aig_ManNodeNum(pMan->pAig), pMan->nFrames );
75     p->fVerbose       = fVerbose;
76     // equivalences considered
77     p->pMan           = pMan;
78     p->vTargets       = Vec_PtrAlloc( Saig_ManPoNum(p->pMan->pAig) );
79     Saig_ManForEachPo( p->pMan->pAig, pObj, i )
80         Vec_PtrPush( p->vTargets, Aig_ObjFanin0(pObj) );
81     // storage for patterns
82     p->nPatternsAlloc = 512;
83     p->nPatterns      = 1;
84     p->vPatterns      = Vec_PtrAllocSimInfo( Aig_ManRegNum(p->pMan->pAig), Abc_BitWordNum(p->nPatternsAlloc) );
85     Vec_PtrCleanSimInfo( p->vPatterns, 0, Abc_BitWordNum(p->nPatternsAlloc) );
86     p->vHistory       = Vec_IntAlloc( 100 );
87     Vec_IntPush( p->vHistory, 0 );
88     // update arrays of the manager
89     assert( 0 );
90 /*
91     ABC_FREE( p->pMan->pNodeToFrames );
92     Vec_IntFree( p->pMan->vSatVars );
93     p->pMan->pNodeToFrames = ABC_CALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pMan->pAig) * p->nFramesSweep );
94     p->pMan->vSatVars      = Vec_IntStart( Aig_ManObjNumMax(p->pMan->pAig) * (p->nFramesSweep+1) );
95 */
96     return p;
97 }
98 
99 /**Function*************************************************************
100 
101   Synopsis    []
102 
103   Description []
104 
105   SideEffects []
106 
107   SeeAlso     []
108 
109 ***********************************************************************/
Ssw_SemManStop(Ssw_Sem_t * p)110 void Ssw_SemManStop( Ssw_Sem_t * p )
111 {
112     Vec_PtrFree( p->vTargets );
113     Vec_PtrFree( p->vPatterns );
114     Vec_IntFree( p->vHistory );
115     ABC_FREE( p );
116 }
117 
118 /**Function*************************************************************
119 
120   Synopsis    []
121 
122   Description []
123 
124   SideEffects []
125 
126   SeeAlso     []
127 
128 ***********************************************************************/
Ssw_SemCheckTargets(Ssw_Sem_t * p)129 int Ssw_SemCheckTargets( Ssw_Sem_t * p )
130 {
131     Aig_Obj_t * pObj;
132     int i;
133     Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
134         if ( !Ssw_ObjIsConst1Cand(p->pMan->pAig, pObj) )
135             return 1;
136     return 0;
137 }
138 
139 /**Function*************************************************************
140 
141   Synopsis    []
142 
143   Description []
144 
145   SideEffects []
146 
147   SeeAlso     []
148 
149 ***********************************************************************/
Ssw_ManFilterBmcSavePattern(Ssw_Sem_t * p)150 void Ssw_ManFilterBmcSavePattern( Ssw_Sem_t * p )
151 {
152     unsigned * pInfo;
153     Aig_Obj_t * pObj;
154     int i;
155     if ( p->nPatterns >= p->nPatternsAlloc )
156         return;
157     Saig_ManForEachLo( p->pMan->pAig, pObj, i )
158     {
159         pInfo = (unsigned *)Vec_PtrEntry( p->vPatterns, i );
160         if ( Abc_InfoHasBit( p->pMan->pPatWords, Saig_ManPiNum(p->pMan->pAig) + i ) )
161             Abc_InfoSetBit( pInfo, p->nPatterns );
162     }
163     p->nPatterns++;
164 }
165 
166 /**Function*************************************************************
167 
168   Synopsis    [Performs fraiging for the internal nodes.]
169 
170   Description []
171 
172   SideEffects []
173 
174   SeeAlso     []
175 
176 ***********************************************************************/
Ssw_ManFilterBmc(Ssw_Sem_t * pBmc,int iPat,int fCheckTargets)177 int Ssw_ManFilterBmc( Ssw_Sem_t * pBmc, int iPat, int fCheckTargets )
178 {
179     Ssw_Man_t * p = pBmc->pMan;
180     Aig_Obj_t * pObj, * pObjNew, * pObjLi, * pObjLo;
181     unsigned * pInfo;
182     int i, f, RetValue, fFirst = 0;
183     abctime clk;
184 clk = Abc_Clock();
185 
186     // start initialized timeframes
187     p->pFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * 3 );
188     Saig_ManForEachLo( p->pAig, pObj, i )
189     {
190         pInfo = (unsigned *)Vec_PtrEntry( pBmc->vPatterns, i );
191         pObjNew = Aig_NotCond( Aig_ManConst1(p->pFrames), !Abc_InfoHasBit(pInfo, iPat) );
192         Ssw_ObjSetFrame( p, pObj, 0, pObjNew );
193     }
194 
195     // sweep internal nodes
196     RetValue = pBmc->nFramesSweep;
197     for ( f = 0; f < pBmc->nFramesSweep; f++ )
198     {
199         // map constants and PIs
200         Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
201         Saig_ManForEachPi( p->pAig, pObj, i )
202             Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
203         // sweep internal nodes
204         Aig_ManForEachNode( p->pAig, pObj, i )
205         {
206             pObjNew = Aig_And( p->pFrames, Ssw_ObjChild0Fra(p, pObj, f), Ssw_ObjChild1Fra(p, pObj, f) );
207             Ssw_ObjSetFrame( p, pObj, f, pObjNew );
208             if ( Ssw_ManSweepNode( p, pObj, f, 1, NULL ) )
209             {
210                 Ssw_ManFilterBmcSavePattern( pBmc );
211                 if ( fFirst == 0 )
212                 {
213                     fFirst = 1;
214                     pBmc->nConfMax *= 10;
215                 }
216             }
217             if ( f > 0 && p->pMSat->pSat->stats.conflicts >= pBmc->nConfMax )
218             {
219                 RetValue = -1;
220                 break;
221             }
222         }
223         // quit if this is the last timeframe
224         if ( p->pMSat->pSat->stats.conflicts >= pBmc->nConfMax )
225         {
226             RetValue += f + 1;
227             break;
228         }
229         if ( fCheckTargets && Ssw_SemCheckTargets( pBmc ) )
230             break;
231         // transfer latch input to the latch outputs
232         // build logic cones for register outputs
233         Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
234         {
235             pObjNew = Ssw_ObjChild0Fra(p, pObjLi,f);
236             Ssw_ObjSetFrame( p, pObjLo, f+1, pObjNew );
237             Ssw_CnfNodeAddToSolver( p->pMSat, Aig_Regular(pObjNew) );
238         }
239 //Abc_Print( 1, "Frame %2d : Conflicts = %6d. \n", f, p->pSat->stats.conflicts );
240     }
241     if ( fFirst )
242         pBmc->nConfMax /= 10;
243 
244     // cleanup
245     Ssw_ClassesCheck( p->ppClasses );
246 p->timeBmc += Abc_Clock() - clk;
247     return RetValue;
248 }
249 
250 /**Function*************************************************************
251 
252   Synopsis    [Returns 1 if one of the targets has failed.]
253 
254   Description []
255 
256   SideEffects []
257 
258   SeeAlso     []
259 
260 ***********************************************************************/
Ssw_FilterUsingSemi(Ssw_Man_t * pMan,int fCheckTargets,int nConfMax,int fVerbose)261 int Ssw_FilterUsingSemi( Ssw_Man_t * pMan, int fCheckTargets, int nConfMax, int fVerbose )
262 {
263     Ssw_Sem_t * p;
264     int RetValue, Frames, Iter;
265     abctime clk = Abc_Clock();
266     p = Ssw_SemManStart( pMan, nConfMax, fVerbose );
267     if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
268     {
269         assert( 0 );
270         Ssw_SemManStop( p );
271         return 1;
272     }
273     if ( fVerbose )
274     {
275         Abc_Print( 1, "AIG : C = %6d. Cl = %6d. Nodes = %6d.  ConfMax = %6d. FramesMax = %6d.\n",
276             Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
277             Aig_ManNodeNum(p->pMan->pAig), p->nConfMax, p->nFramesSweep );
278     }
279     RetValue = 0;
280     for ( Iter = 0; Iter < p->nPatterns; Iter++ )
281     {
282 clk = Abc_Clock();
283         pMan->pMSat = Ssw_SatStart( 0 );
284         Frames = Ssw_ManFilterBmc( p, Iter, fCheckTargets );
285         if ( fVerbose )
286         {
287             Abc_Print( 1, "%3d : C = %6d. Cl = %6d. NR = %6d. F = %3d. C = %5d. P = %3d. %s ",
288                 Iter, Ssw_ClassesCand1Num(p->pMan->ppClasses), Ssw_ClassesClassNum(p->pMan->ppClasses),
289                 Aig_ManNodeNum(p->pMan->pFrames), Frames, (int)p->pMan->pMSat->pSat->stats.conflicts, p->nPatterns,
290                 p->pMan->nSatFailsReal? "f" : " " );
291             ABC_PRT( "T", Abc_Clock() - clk );
292         }
293         Ssw_ManCleanup( p->pMan );
294         if ( fCheckTargets && Ssw_SemCheckTargets( p ) )
295         {
296             Abc_Print( 1, "Target is hit!!!\n" );
297             RetValue = 1;
298         }
299         if ( p->nPatterns >= p->nPatternsAlloc )
300             break;
301     }
302     Ssw_SemManStop( p );
303 
304     pMan->nStrangers = 0;
305     pMan->nSatCalls = 0;
306     pMan->nSatProof = 0;
307     pMan->nSatFailsReal = 0;
308     pMan->nSatCallsUnsat = 0;
309     pMan->nSatCallsSat = 0;
310     pMan->timeSimSat = 0;
311     pMan->timeSat = 0;
312     pMan->timeSatSat = 0;
313     pMan->timeSatUnsat = 0;
314     pMan->timeSatUndec = 0;
315     return RetValue;
316 }
317 
318 ////////////////////////////////////////////////////////////////////////
319 ///                       END OF FILE                                ///
320 ////////////////////////////////////////////////////////////////////////
321 
322 
323 ABC_NAMESPACE_IMPL_END
324