1 /**CFile****************************************************************
2
3 FileName [llb2Core.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [BDD based reachability.]
8
9 Synopsis [Core procedure.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: llb2Core.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18
19 ***********************************************************************/
20
21 #include "llbInt.h"
22
23 ABC_NAMESPACE_IMPL_START
24
25
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29
30 typedef struct Llb_Img_t_ Llb_Img_t;
31 struct Llb_Img_t_
32 {
33 Aig_Man_t * pInit; // AIG manager
34 Aig_Man_t * pAig; // AIG manager
35 Gia_ParLlb_t * pPars; // parameters
36
37 DdManager * dd; // BDD manager
38 DdManager * ddG; // BDD manager
39 DdManager * ddR; // BDD manager
40 Vec_Ptr_t * vDdMans; // BDD managers for each partition
41 Vec_Ptr_t * vRings; // onion rings in ddR
42
43 Vec_Int_t * vDriRefs; // driver references
44 Vec_Int_t * vVarsCs; // cur state variables
45 Vec_Int_t * vVarsNs; // next state variables
46
47 Vec_Int_t * vCs2Glo; // cur state variables into global variables
48 Vec_Int_t * vNs2Glo; // next state variables into global variables
49 Vec_Int_t * vGlo2Cs; // global variables into cur state variables
50 Vec_Int_t * vGlo2Ns; // global variables into next state variables
51 };
52
53 ////////////////////////////////////////////////////////////////////////
54 /// FUNCTION DEFINITIONS ///
55 ////////////////////////////////////////////////////////////////////////
56
57 /**Function*************************************************************
58
59 Synopsis [Computes cube composed of given variables with given values.]
60
61 Description []
62
63 SideEffects []
64
65 SeeAlso []
66
67 ***********************************************************************/
Llb_CoreComputeCube(DdManager * dd,Vec_Int_t * vVars,int fUseVarIndex,char * pValues)68 DdNode * Llb_CoreComputeCube( DdManager * dd, Vec_Int_t * vVars, int fUseVarIndex, char * pValues )
69 {
70 DdNode * bRes, * bVar, * bTemp;
71 int i, iVar, Index;
72 abctime TimeStop;
73 TimeStop = dd->TimeStop; dd->TimeStop = 0;
74 bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes );
75 Vec_IntForEachEntry( vVars, Index, i )
76 {
77 iVar = fUseVarIndex ? Index : i;
78 bVar = Cudd_NotCond( Cudd_bddIthVar(dd, iVar), (int)(pValues == NULL || pValues[i] != 1) );
79 bRes = Cudd_bddAnd( dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
80 Cudd_RecursiveDeref( dd, bTemp );
81 }
82 Cudd_Deref( bRes );
83 dd->TimeStop = TimeStop;
84 return bRes;
85 }
86
87 /**Function*************************************************************
88
89 Synopsis [Derives counter-example by backward reachability.]
90
91 Description []
92
93 SideEffects []
94
95 SeeAlso []
96
97 ***********************************************************************/
Llb_CoreDeriveCex(Llb_Img_t * p)98 Abc_Cex_t * Llb_CoreDeriveCex( Llb_Img_t * p )
99 {
100 Abc_Cex_t * pCex;
101 Aig_Obj_t * pObj;
102 Vec_Ptr_t * vSupps, * vQuant0, * vQuant1;
103 DdNode * bState = NULL, * bImage, * bOneCube, * bTemp, * bRing;
104 int i, v, RetValue, nPiOffset;
105 char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) );
106 assert( Vec_PtrSize(p->vRings) > 0 );
107
108 p->dd->TimeStop = 0;
109 p->ddR->TimeStop = 0;
110
111 // get supports and quantified variables
112 Vec_PtrReverseOrder( p->vDdMans );
113 vSupps = Llb_ImgSupports( p->pAig, p->vDdMans, p->vVarsNs, p->vVarsCs, 1, 0 );
114 Llb_ImgSchedule( vSupps, &vQuant0, &vQuant1, 0 );
115 Vec_VecFree( (Vec_Vec_t *)vSupps );
116 Llb_ImgQuantifyReset( p->vDdMans );
117 // Llb_ImgQuantifyFirst( p->pAig, p->vDdMans, vQuant0 );
118
119 // allocate room for the counter-example
120 pCex = Abc_CexAlloc( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
121 pCex->iFrame = Vec_PtrSize(p->vRings) - 1;
122 pCex->iPo = -1;
123
124 // get the last cube
125 bOneCube = Cudd_bddIntersect( p->ddR, (DdNode *)Vec_PtrEntryLast(p->vRings), p->ddR->bFunc ); Cudd_Ref( bOneCube );
126 RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
127 Cudd_RecursiveDeref( p->ddR, bOneCube );
128 assert( RetValue );
129
130 // write PIs of counter-example
131 nPiOffset = Saig_ManRegNum(p->pAig) + Saig_ManPiNum(p->pAig) * (Vec_PtrSize(p->vRings) - 1);
132 Saig_ManForEachPi( p->pAig, pObj, i )
133 if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
134 Abc_InfoSetBit( pCex->pData, nPiOffset + i );
135
136 // write state in terms of NS variables
137 if ( Vec_PtrSize(p->vRings) > 1 )
138 {
139 bState = Llb_CoreComputeCube( p->dd, p->vVarsNs, 1, pValues ); Cudd_Ref( bState );
140 }
141 // perform backward analysis
142 Vec_PtrForEachEntryReverse( DdNode *, p->vRings, bRing, v )
143 {
144 if ( v == Vec_PtrSize(p->vRings) - 1 )
145 continue;
146 // compute the next states
147 bImage = Llb_ImgComputeImage( p->pAig, p->vDdMans, p->dd, bState,
148 vQuant0, vQuant1, p->vDriRefs, p->pPars->TimeTarget, 1, 0, 0 );
149 assert( bImage != NULL );
150 Cudd_Ref( bImage );
151 Cudd_RecursiveDeref( p->dd, bState );
152 //Extra_bddPrintSupport( p->dd, bImage ); printf( "\n" );
153
154 // move reached states into ring manager
155 bImage = Extra_TransferPermute( p->dd, p->ddR, bTemp = bImage, Vec_IntArray(p->vCs2Glo) ); Cudd_Ref( bImage );
156 Cudd_RecursiveDeref( p->dd, bTemp );
157
158 // intersect with the previous set
159 bOneCube = Cudd_bddIntersect( p->ddR, bImage, bRing ); Cudd_Ref( bOneCube );
160 Cudd_RecursiveDeref( p->ddR, bImage );
161
162 // find any assignment of the BDD
163 RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
164 Cudd_RecursiveDeref( p->ddR, bOneCube );
165 assert( RetValue );
166
167 // write PIs of counter-example
168 nPiOffset -= Saig_ManPiNum(p->pAig);
169 Saig_ManForEachPi( p->pAig, pObj, i )
170 if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
171 Abc_InfoSetBit( pCex->pData, nPiOffset + i );
172
173 // check that we get the init state
174 if ( v == 0 )
175 {
176 Saig_ManForEachLo( p->pAig, pObj, i )
177 assert( pValues[i] == 0 );
178 break;
179 }
180
181 // write state in terms of NS variables
182 bState = Llb_CoreComputeCube( p->dd, p->vVarsNs, 1, pValues ); Cudd_Ref( bState );
183 }
184 assert( nPiOffset == Saig_ManRegNum(p->pAig) );
185 // update the output number
186 RetValue = Saig_ManFindFailedPoCex( p->pInit, pCex );
187 assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pInit) ); // invalid CEX!!!
188 pCex->iPo = RetValue;
189 // cleanup
190 ABC_FREE( pValues );
191 Vec_VecFree( (Vec_Vec_t *)vQuant0 );
192 Vec_VecFree( (Vec_Vec_t *)vQuant1 );
193 return pCex;
194 }
195
196 /**Function*************************************************************
197
198 Synopsis []
199
200 Description []
201
202 SideEffects []
203
204 SeeAlso []
205
206 ***********************************************************************/
Llb_CoreReachability_int(Llb_Img_t * p,Vec_Ptr_t * vQuant0,Vec_Ptr_t * vQuant1)207 int Llb_CoreReachability_int( Llb_Img_t * p, Vec_Ptr_t * vQuant0, Vec_Ptr_t * vQuant1 )
208 {
209 int * pLoc2Glo = p->pPars->fBackward? Vec_IntArray( p->vCs2Glo ) : Vec_IntArray( p->vNs2Glo );
210 int * pLoc2GloR = p->pPars->fBackward? Vec_IntArray( p->vNs2Glo ) : Vec_IntArray( p->vCs2Glo );
211 int * pGlo2Loc = p->pPars->fBackward? Vec_IntArray( p->vGlo2Ns ) : Vec_IntArray( p->vGlo2Cs );
212 DdNode * bCurrent, * bReached, * bNext, * bTemp;
213 abctime clk2, clk = Abc_Clock();
214 int nIters, nBddSize;//, iOutFail = -1;
215 /*
216 // compute time to stop
217 if ( p->pPars->TimeLimit )
218 p->pPars->TimeTarget = Abc_Clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC;
219 else
220 p->pPars->TimeTarget = 0;
221 */
222
223 if ( Abc_Clock() > p->pPars->TimeTarget )
224 {
225 if ( !p->pPars->fSilent )
226 printf( "Reached timeout (%d seconds) before image computation.\n", p->pPars->TimeLimit );
227 p->pPars->iFrame = -1;
228 return -1;
229 }
230
231 // set the stop time parameter
232 p->dd->TimeStop = p->pPars->TimeTarget;
233 p->ddG->TimeStop = p->pPars->TimeTarget;
234 p->ddR->TimeStop = p->pPars->TimeTarget;
235
236 // compute initial states
237 if ( p->pPars->fBackward )
238 {
239 // create init state in the global manager
240 bTemp = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeTarget );
241 if ( bTemp == NULL )
242 {
243 if ( !p->pPars->fSilent )
244 printf( "Reached timeout (%d seconds) while computing bad states.\n", p->pPars->TimeLimit );
245 p->pPars->iFrame = -1;
246 return -1;
247 }
248 Cudd_Ref( bTemp );
249 // create bad state in the ring manager
250 p->ddR->bFunc = Llb_CoreComputeCube( p->ddR, p->vVarsCs, 0, NULL ); Cudd_Ref( p->ddR->bFunc );
251 bCurrent = Llb_BddQuantifyPis( p->pInit, p->ddR, bTemp ); Cudd_Ref( bCurrent );
252 Cudd_RecursiveDeref( p->ddR, bTemp );
253 bReached = Cudd_bddTransfer( p->ddR, p->ddG, bCurrent ); Cudd_Ref( bReached );
254 Cudd_RecursiveDeref( p->ddR, bCurrent );
255 // move init state to the working manager
256 bCurrent = Extra_TransferPermute( p->ddG, p->dd, bReached, pGlo2Loc );
257 if ( bCurrent == NULL )
258 {
259 Cudd_RecursiveDeref( p->ddG, bReached );
260 if ( !p->pPars->fSilent )
261 printf( "Reached timeout (%d seconds) during transfer 0.\n", p->pPars->TimeLimit );
262 p->pPars->iFrame = -1;
263 return -1;
264 }
265 Cudd_Ref( bCurrent );
266 }
267 else
268 {
269 // create bad state in the ring manager
270 p->ddR->bFunc = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeTarget );
271 if ( p->ddR->bFunc == NULL )
272 {
273 if ( !p->pPars->fSilent )
274 printf( "Reached timeout (%d seconds) while computing bad states.\n", p->pPars->TimeLimit );
275 p->pPars->iFrame = -1;
276 return -1;
277 }
278 Cudd_Ref( p->ddR->bFunc );
279 // create init state in the working and global manager
280 bCurrent = Llb_CoreComputeCube( p->dd, p->vVarsCs, 1, NULL ); Cudd_Ref( bCurrent );
281 bReached = Llb_CoreComputeCube( p->ddG, p->vVarsCs, 0, NULL ); Cudd_Ref( bReached );
282 //Extra_bddPrint( p->dd, bCurrent ); printf( "\n" );
283 //Extra_bddPrint( p->ddG, bReached ); printf( "\n" );
284 }
285
286 // compute onion rings
287 for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ )
288 {
289 clk2 = Abc_Clock();
290 // check the runtime limit
291 if ( p->pPars->TimeLimit && Abc_Clock() > p->pPars->TimeTarget )
292 {
293 if ( !p->pPars->fSilent )
294 printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit );
295 p->pPars->iFrame = nIters - 1;
296 Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
297 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
298 return -1;
299 }
300
301 // save the onion ring
302 bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, pLoc2GloR );
303 if ( bTemp == NULL )
304 {
305 if ( !p->pPars->fSilent )
306 printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit );
307 p->pPars->iFrame = nIters - 1;
308 Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
309 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
310 return -1;
311 }
312 Cudd_Ref( bTemp );
313 Vec_PtrPush( p->vRings, bTemp );
314
315 // check it for bad states
316 if ( !p->pPars->fSkipOutCheck && !Cudd_bddLeq( p->ddR, bTemp, Cudd_Not(p->ddR->bFunc) ) )
317 {
318 assert( p->pInit->pSeqModel == NULL );
319 if ( !p->pPars->fBackward )
320 p->pInit->pSeqModel = Llb_CoreDeriveCex( p );
321 Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
322 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
323 if ( !p->pPars->fSilent )
324 {
325 if ( !p->pPars->fBackward )
326 Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pInit->pSeqModel->iPo, p->pInit->pName, nIters );
327 else
328 Abc_Print( 1, "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters );
329 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
330 }
331 p->pPars->iFrame = nIters - 1;
332 return 0;
333 }
334
335 // compute the next states
336 bNext = Llb_ImgComputeImage( p->pAig, p->vDdMans, p->dd, bCurrent,
337 vQuant0, vQuant1, p->vDriRefs, p->pPars->TimeTarget,
338 p->pPars->fBackward, p->pPars->fReorder, p->pPars->fVeryVerbose );
339 if ( bNext == NULL )
340 {
341 if ( !p->pPars->fSilent )
342 printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit );
343 p->pPars->iFrame = nIters - 1;
344 Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
345 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
346 return -1;
347 }
348 Cudd_Ref( bNext );
349 Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
350 //Extra_bddPrintSupport( p->dd, bNext ); printf( "\n" );
351
352 // remap these states into the global manager
353 // bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pLoc2Glo ); Cudd_Ref( bNext );
354 // Cudd_RecursiveDeref( p->dd, bTemp );
355
356 // bNext = Extra_TransferPermuteTime( p->dd, p->ddG, bTemp = bNext, pLoc2Glo, p->pPars->TimeTarget );
357 bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pLoc2Glo );
358 if ( bNext == NULL )
359 {
360 if ( !p->pPars->fSilent )
361 printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit );
362 p->pPars->iFrame = nIters - 1;
363 Cudd_RecursiveDeref( p->dd, bTemp );
364 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
365 return -1;
366 }
367 Cudd_Ref( bNext );
368 Cudd_RecursiveDeref( p->dd, bTemp );
369
370 nBddSize = Cudd_DagSize(bNext);
371 // check if there are any new states
372 if ( Cudd_bddLeq( p->ddG, bNext, bReached ) ) // implication = no new states
373 {
374 Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL;
375 break;
376 }
377
378 // get the new states
379 bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) );
380 if ( bCurrent == NULL )
381 {
382 if ( !p->pPars->fSilent )
383 printf( "Reached timeout (%d seconds) during image computation in transfer 2.\n", p->pPars->TimeLimit );
384 p->pPars->iFrame = nIters - 1;
385 Cudd_RecursiveDeref( p->ddG, bNext );
386 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
387 return -1;
388 }
389 Cudd_Ref( bCurrent );
390
391 // remap these states into the current state vars
392 // bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc ); Cudd_Ref( bCurrent );
393 // Cudd_RecursiveDeref( p->ddG, bTemp );
394
395 // bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc, p->pPars->TimeTarget );
396 bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Loc );
397 if ( bCurrent == NULL )
398 {
399 if ( !p->pPars->fSilent )
400 printf( "Reached timeout (%d seconds) during image computation in transfer 2.\n", p->pPars->TimeLimit );
401 p->pPars->iFrame = nIters - 1;
402 Cudd_RecursiveDeref( p->ddG, bTemp );
403 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
404 return -1;
405 }
406 Cudd_Ref( bCurrent );
407 Cudd_RecursiveDeref( p->ddG, bTemp );
408
409 // add to the reached states
410 bReached = Cudd_bddOr( p->ddG, bTemp = bReached, bNext ); Cudd_Ref( bReached );
411 Cudd_RecursiveDeref( p->ddG, bTemp );
412 Cudd_RecursiveDeref( p->ddG, bNext );
413 bNext = NULL;
414
415 if ( p->pPars->fVeryVerbose )
416 {
417 double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) );
418 // Extra_bddPrint( p->ddG, bReached );printf( "\n" );
419 fprintf( stdout, " Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
420 fflush( stdout );
421 }
422 if ( p->pPars->fVerbose )
423 {
424 fprintf( stdout, "F =%3d : ", nIters );
425 fprintf( stdout, "Image =%6d ", nBddSize );
426 fprintf( stdout, "(%4d%4d) ",
427 Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) );
428 fprintf( stdout, "Reach =%6d ", Cudd_DagSize(bReached) );
429 fprintf( stdout, "(%4d%4d) ",
430 Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) );
431 Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
432 }
433
434 // check timeframe limit
435 if ( nIters == p->pPars->nIterMax - 1 )
436 {
437 if ( !p->pPars->fSilent )
438 printf( "Reached limit on the number of timeframes (%d).\n", p->pPars->nIterMax );
439 p->pPars->iFrame = nIters;
440 Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
441 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
442 return -1;
443 }
444 }
445 if ( bReached == NULL )
446 {
447 p->pPars->iFrame = nIters - 1;
448 return 0; // reachable
449 }
450 if ( bCurrent )
451 Cudd_RecursiveDeref( p->dd, bCurrent );
452 // report the stats
453 if ( p->pPars->fVerbose )
454 {
455 double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) );
456 if ( nIters >= p->pPars->nIterMax )
457 fprintf( stdout, "Reachability analysis is stopped after %d frames.\n", nIters );
458 else
459 fprintf( stdout, "Reachability analysis completed after %d frames.\n", nIters );
460 fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
461 fflush( stdout );
462 }
463 if ( p->pPars->fDumpReached )
464 {
465 Llb_ManDumpReached( p->ddG, bReached, p->pAig->pName, "reached.blif" );
466 printf( "Reached states with %d BDD nodes are dumpted into file \"reached.blif\".\n", Cudd_DagSize(bReached) );
467 }
468 Cudd_RecursiveDeref( p->ddG, bReached );
469 if ( nIters >= p->pPars->nIterMax )
470 {
471 if ( !p->pPars->fSilent )
472 {
473 printf( "Verified only for states reachable in %d frames. ", nIters );
474 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
475 }
476 p->pPars->iFrame = p->pPars->nIterMax;
477 return -1; // undecided
478 }
479 if ( !p->pPars->fSilent )
480 {
481 printf( "The miter is proved unreachable after %d iterations. ", nIters );
482 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
483 }
484 p->pPars->iFrame = nIters - 1;
485 return 1; // unreachable
486 }
487
488 /**Function*************************************************************
489
490 Synopsis []
491
492 Description []
493
494 SideEffects []
495
496 SeeAlso []
497
498 ***********************************************************************/
Llb_CoreReachability(Llb_Img_t * p)499 int Llb_CoreReachability( Llb_Img_t * p )
500 {
501 Vec_Ptr_t * vSupps, * vQuant0, * vQuant1;
502 int RetValue;
503 // get supports and quantified variables
504 if ( p->pPars->fBackward )
505 {
506 Vec_PtrReverseOrder( p->vDdMans );
507 vSupps = Llb_ImgSupports( p->pAig, p->vDdMans, p->vVarsNs, p->vVarsCs, 0, p->pPars->fVeryVerbose );
508 }
509 else
510 vSupps = Llb_ImgSupports( p->pAig, p->vDdMans, p->vVarsCs, p->vVarsNs, 0, p->pPars->fVeryVerbose );
511 Llb_ImgSchedule( vSupps, &vQuant0, &vQuant1, p->pPars->fVeryVerbose );
512 Vec_VecFree( (Vec_Vec_t *)vSupps );
513 // remove variables
514 Llb_ImgQuantifyFirst( p->pAig, p->vDdMans, vQuant0, p->pPars->fVeryVerbose );
515 // perform reachability
516 RetValue = Llb_CoreReachability_int( p, vQuant0, vQuant1 );
517 Vec_VecFree( (Vec_Vec_t *)vQuant0 );
518 Vec_VecFree( (Vec_Vec_t *)vQuant1 );
519 return RetValue;
520 }
521
522
523 /**Function*************************************************************
524
525 Synopsis []
526
527 Description []
528
529 SideEffects []
530
531 SeeAlso []
532
533 ***********************************************************************/
Llb_CoreConstructAll(Aig_Man_t * p,Vec_Ptr_t * vResult,Vec_Int_t * vVarsNs,abctime TimeTarget)534 Vec_Ptr_t * Llb_CoreConstructAll( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Int_t * vVarsNs, abctime TimeTarget )
535 {
536 DdManager * dd;
537 Vec_Ptr_t * vDdMans;
538 Vec_Ptr_t * vLower, * vUpper = NULL;
539 int i;
540 vDdMans = Vec_PtrStart( Vec_PtrSize(vResult) );
541 Vec_PtrForEachEntryReverse( Vec_Ptr_t *, vResult, vLower, i )
542 {
543 if ( i < Vec_PtrSize(vResult) - 1 )
544 dd = Llb_ImgPartition( p, vLower, vUpper, TimeTarget );
545 else
546 dd = Llb_DriverLastPartition( p, vVarsNs, TimeTarget );
547 if ( dd == NULL )
548 {
549 Vec_PtrForEachEntry( DdManager *, vDdMans, dd, i )
550 {
551 if ( dd == NULL )
552 continue;
553 if ( dd->bFunc )
554 Cudd_RecursiveDeref( dd, dd->bFunc );
555 Extra_StopManager( dd );
556 }
557 Vec_PtrFree( vDdMans );
558 return NULL;
559 }
560 Vec_PtrWriteEntry( vDdMans, i, dd );
561 vUpper = vLower;
562 }
563 return vDdMans;
564 }
565
566 /**Function*************************************************************
567
568 Synopsis []
569
570 Description []
571
572 SideEffects []
573
574 SeeAlso []
575
576 ***********************************************************************/
Llb_CoreSetVarMaps(Llb_Img_t * p)577 void Llb_CoreSetVarMaps( Llb_Img_t * p )
578 {
579 Aig_Obj_t * pObj;
580 int i, iVarCs, iVarNs;
581 assert( p->vVarsCs != NULL );
582 assert( p->vVarsNs != NULL );
583 assert( p->vCs2Glo == NULL );
584 assert( p->vNs2Glo == NULL );
585 assert( p->vGlo2Cs == NULL );
586 assert( p->vGlo2Ns == NULL );
587 p->vCs2Glo = Vec_IntStartFull( Aig_ManObjNumMax(p->pAig) );
588 p->vNs2Glo = Vec_IntStartFull( Aig_ManObjNumMax(p->pAig) );
589 p->vGlo2Cs = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
590 p->vGlo2Ns = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
591 for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
592 {
593 iVarCs = Vec_IntEntry( p->vVarsCs, i );
594 iVarNs = Vec_IntEntry( p->vVarsNs, i );
595 assert( iVarCs >= 0 && iVarCs < Aig_ManObjNumMax(p->pAig) );
596 assert( iVarNs >= 0 && iVarNs < Aig_ManObjNumMax(p->pAig) );
597 Vec_IntWriteEntry( p->vCs2Glo, iVarCs, i );
598 Vec_IntWriteEntry( p->vNs2Glo, iVarNs, i );
599 Vec_IntWriteEntry( p->vGlo2Cs, i, iVarCs );
600 Vec_IntWriteEntry( p->vGlo2Ns, i, iVarNs );
601 }
602 // add mapping of the PIs
603 Saig_ManForEachPi( p->pAig, pObj, i )
604 Vec_IntWriteEntry( p->vCs2Glo, Aig_ObjId(pObj), Aig_ManRegNum(p->pAig)+i );
605 }
606
607 /**Function*************************************************************
608
609 Synopsis []
610
611 Description []
612
613 SideEffects []
614
615 SeeAlso []
616
617 ***********************************************************************/
Llb_CoreStart(Aig_Man_t * pInit,Aig_Man_t * pAig,Gia_ParLlb_t * pPars)618 Llb_Img_t * Llb_CoreStart( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
619 {
620 Llb_Img_t * p;
621 p = ABC_CALLOC( Llb_Img_t, 1 );
622 p->pInit = pInit;
623 p->pAig = pAig;
624 p->pPars = pPars;
625 p->dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
626 p->ddG = Cudd_Init( Aig_ManRegNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
627 p->ddR = Cudd_Init( Aig_ManCiNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
628 Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT );
629 Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT );
630 Cudd_AutodynEnable( p->ddR, CUDD_REORDER_SYMM_SIFT );
631 p->vRings = Vec_PtrAlloc( 100 );
632 p->vDriRefs = Llb_DriverCountRefs( pAig );
633 p->vVarsCs = Llb_DriverCollectCs( pAig );
634 p->vVarsNs = Llb_DriverCollectNs( pAig, p->vDriRefs );
635 Llb_CoreSetVarMaps( p );
636 return p;
637 }
638
639 /**Function*************************************************************
640
641 Synopsis []
642
643 Description []
644
645 SideEffects []
646
647 SeeAlso []
648
649 ***********************************************************************/
Llb_CoreStop(Llb_Img_t * p)650 void Llb_CoreStop( Llb_Img_t * p )
651 {
652 DdManager * dd;
653 DdNode * bTemp;
654 int i;
655 if ( p->vDdMans )
656 Vec_PtrForEachEntry( DdManager *, p->vDdMans, dd, i )
657 {
658 if ( dd->bFunc )
659 Cudd_RecursiveDeref( dd, dd->bFunc );
660 if ( dd->bFunc2 )
661 Cudd_RecursiveDeref( dd, dd->bFunc2 );
662 Extra_StopManager( dd );
663 }
664 Vec_PtrFreeP( &p->vDdMans );
665 if ( p->ddR->bFunc )
666 Cudd_RecursiveDeref( p->ddR, p->ddR->bFunc );
667 Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
668 Cudd_RecursiveDeref( p->ddR, bTemp );
669 Vec_PtrFree( p->vRings );
670 Extra_StopManager( p->dd );
671 Extra_StopManager( p->ddG );
672 Extra_StopManager( p->ddR );
673 Vec_IntFreeP( &p->vDriRefs );
674 Vec_IntFreeP( &p->vVarsCs );
675 Vec_IntFreeP( &p->vVarsNs );
676 Vec_IntFreeP( &p->vCs2Glo );
677 Vec_IntFreeP( &p->vNs2Glo );
678 Vec_IntFreeP( &p->vGlo2Cs );
679 Vec_IntFreeP( &p->vGlo2Ns );
680 ABC_FREE( p );
681 }
682
683 /**Function*************************************************************
684
685 Synopsis []
686
687 Description []
688
689 SideEffects []
690
691 SeeAlso []
692
693 ***********************************************************************/
Llb_CoreExperiment(Aig_Man_t * pInit,Aig_Man_t * pAig,Gia_ParLlb_t * pPars,Vec_Ptr_t * vResult,abctime TimeTarget)694 int Llb_CoreExperiment( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars, Vec_Ptr_t * vResult, abctime TimeTarget )
695 {
696 int RetValue;
697 Llb_Img_t * p;
698 // printf( "\n" );
699 // pPars->fVerbose = 1;
700 p = Llb_CoreStart( pInit, pAig, pPars );
701 p->vDdMans = Llb_CoreConstructAll( pAig, vResult, p->vVarsNs, TimeTarget );
702 if ( p->vDdMans == NULL )
703 {
704 if ( !pPars->fSilent )
705 printf( "Reached timeout (%d seconds) while deriving the partitions.\n", pPars->TimeLimit );
706 Llb_CoreStop( p );
707 return -1;
708 }
709 RetValue = Llb_CoreReachability( p );
710 Llb_CoreStop( p );
711 return RetValue;
712 }
713
714 /**Function*************************************************************
715
716 Synopsis [Finds balanced cut.]
717
718 Description []
719
720 SideEffects []
721
722 SeeAlso []
723
724 ***********************************************************************/
Llb_ManReachMinCut(Aig_Man_t * pAig,Gia_ParLlb_t * pPars)725 int Llb_ManReachMinCut( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
726 {
727 extern Vec_Ptr_t * Llb_ManComputeCuts( Aig_Man_t * p, int Num, int fVerbose, int fVeryVerbose );
728 Vec_Ptr_t * vResult;
729 Aig_Man_t * p;
730 int RetValue = -1;
731 abctime clk = Abc_Clock();
732
733 // compute time to stop
734 pPars->TimeTarget = pPars->TimeLimit ? pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
735
736 p = Aig_ManDupFlopsOnly( pAig );
737 //Aig_ManShow( p, 0, NULL );
738 if ( pPars->fVerbose )
739 Aig_ManPrintStats( pAig );
740 if ( pPars->fVerbose )
741 Aig_ManPrintStats( p );
742 Aig_ManFanoutStart( p );
743
744 vResult = Llb_ManComputeCuts( p, pPars->nPartValue, pPars->fVerbose, pPars->fVeryVerbose );
745
746 if ( pPars->TimeLimit && Abc_Clock() > pPars->TimeTarget )
747 {
748 if ( !pPars->fSilent )
749 printf( "Reached timeout (%d seconds) after partitioning.\n", pPars->TimeLimit );
750
751 Vec_VecFree( (Vec_Vec_t *)vResult );
752 Aig_ManFanoutStop( p );
753 Aig_ManCleanMarkAB( p );
754 Aig_ManStop( p );
755 return RetValue;
756 }
757
758 if ( !pPars->fSkipReach )
759 RetValue = Llb_CoreExperiment( pAig, p, pPars, vResult, pPars->TimeTarget );
760
761 Vec_VecFree( (Vec_Vec_t *)vResult );
762 Aig_ManFanoutStop( p );
763 Aig_ManCleanMarkAB( p );
764 Aig_ManStop( p );
765
766 if ( RetValue == -1 )
767 Abc_PrintTime( 1, "Total runtime of the min-cut-based reachability engine", Abc_Clock() - clk );
768 return RetValue;
769 }
770
771 ////////////////////////////////////////////////////////////////////////
772 /// END OF FILE ///
773 ////////////////////////////////////////////////////////////////////////
774
775
776 ABC_NAMESPACE_IMPL_END
777
778