1 /**CFile****************************************************************
2
3 FileName [llb2Nonlin.c]
4
5 SystemName [ABC: Logic synthesis and verification system.]
6
7 PackageName [BDD based reachability.]
8
9 Synopsis [Non-linear quantification scheduling.]
10
11 Author [Alan Mishchenko]
12
13 Affiliation [UC Berkeley]
14
15 Date [Ver. 1.0. Started - June 20, 2005.]
16
17 Revision [$Id: llb2Nonlin.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_Mnn_t_ Llb_Mnn_t;
31 struct Llb_Mnn_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 * vRings; // onion rings in ddR
41
42 Vec_Ptr_t * vLeaves;
43 Vec_Ptr_t * vRoots;
44 int * pVars2Q;
45 int * pOrderL;
46 int * pOrderL2;
47 int * pOrderG;
48
49 Vec_Int_t * vCs2Glo; // cur state variables into global variables
50 Vec_Int_t * vNs2Glo; // next state variables into global variables
51 Vec_Int_t * vGlo2Cs; // global variables into cur state variables
52 Vec_Int_t * vGlo2Ns; // global variables into next state variables
53
54 int ddLocReos;
55 int ddLocGrbs;
56
57 abctime timeImage;
58 abctime timeTran1;
59 abctime timeTran2;
60 abctime timeGloba;
61 abctime timeOther;
62 abctime timeTotal;
63 abctime timeReo;
64 abctime timeReoG;
65
66 };
67
68 extern abctime timeBuild, timeAndEx, timeOther;
69 extern int nSuppMax;
70
71 ////////////////////////////////////////////////////////////////////////
72 /// FUNCTION DEFINITIONS ///
73 ////////////////////////////////////////////////////////////////////////
74
75 /**Function*************************************************************
76
77 Synopsis [Finds variable whose 0-cofactor is the smallest.]
78
79 Description []
80
81 SideEffects []
82
83 SeeAlso []
84
85 ***********************************************************************/
Llb_NonlinFindBestVar(DdManager * dd,DdNode * bFunc,Aig_Man_t * pAig)86 int Llb_NonlinFindBestVar( DdManager * dd, DdNode * bFunc, Aig_Man_t * pAig )
87 {
88 int fVerbose = 0;
89 Aig_Obj_t * pObj;
90 DdNode * bCof, * bVar;
91 int i, iVar, iVarBest = -1, iValue, iValueBest = ABC_INFINITY, Size0Best = -1;
92 int Size, Size0, Size1;
93 abctime clk = Abc_Clock();
94 Size = Cudd_DagSize(bFunc);
95 // printf( "Original = %6d. SuppSize = %3d. Vars = %3d.\n",
96 // Size = Cudd_DagSize(bFunc), Cudd_SupportSize(dd, bFunc), Aig_ManRegNum(pAig) );
97 Saig_ManForEachLo( pAig, pObj, i )
98 {
99 iVar = Aig_ObjId(pObj);
100
101 if ( fVerbose )
102 printf( "Var =%3d : ", iVar );
103 bVar = Cudd_bddIthVar(dd, iVar);
104
105 bCof = Cudd_bddAnd( dd, bFunc, Cudd_Not(bVar) ); Cudd_Ref( bCof );
106 Size0 = Cudd_DagSize(bCof);
107 if ( fVerbose )
108 printf( "Supp0 =%3d ", Cudd_SupportSize(dd, bCof) );
109 if ( fVerbose )
110 printf( "Size0 =%6d ", Size0 );
111 Cudd_RecursiveDeref( dd, bCof );
112
113 bCof = Cudd_bddAnd( dd, bFunc, bVar ); Cudd_Ref( bCof );
114 Size1 = Cudd_DagSize(bCof);
115 if ( fVerbose )
116 printf( "Supp1 =%3d ", Cudd_SupportSize(dd, bCof) );
117 if ( fVerbose )
118 printf( "Size1 =%6d ", Size1 );
119 Cudd_RecursiveDeref( dd, bCof );
120
121 iValue = Abc_MaxInt(Size0, Size1) - Abc_MinInt(Size0, Size1) + Size0 + Size1 - Size;
122 if ( fVerbose )
123 printf( "D =%6d ", Size0 + Size1 - Size );
124 if ( fVerbose )
125 printf( "B =%6d ", Abc_MaxInt(Size0, Size1) - Abc_MinInt(Size0, Size1) );
126 if ( fVerbose )
127 printf( "S =%6d\n", iValue );
128 if ( Size0 > 1 && Size1 > 1 && iValueBest > iValue )
129 {
130 iValueBest = iValue;
131 iVarBest = i;
132 Size0Best = Size0;
133 }
134 }
135 printf( "BestVar = %4d/%4d. Value =%6d. Orig =%6d. Size0 =%6d. ",
136 iVarBest, Aig_ObjId(Saig_ManLo(pAig,iVarBest)), iValueBest, Size, Size0Best );
137 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
138 return iVarBest;
139 }
140
141
142 /**Function*************************************************************
143
144 Synopsis [Finds variable whose 0-cofactor is the smallest.]
145
146 Description []
147
148 SideEffects []
149
150 SeeAlso []
151
152 ***********************************************************************/
Llb_NonlinTrySubsetting(DdManager * dd,DdNode * bFunc)153 void Llb_NonlinTrySubsetting( DdManager * dd, DdNode * bFunc )
154 {
155 DdNode * bNew;
156 printf( "Original = %6d. SuppSize = %3d. ",
157 Cudd_DagSize(bFunc), Cudd_SupportSize(dd, bFunc) );
158 bNew = Cudd_SubsetHeavyBranch( dd, bFunc, Cudd_SupportSize(dd, bFunc), 1000 ); Cudd_Ref( bNew );
159 printf( "Result = %6d. SuppSize = %3d.\n",
160 Cudd_DagSize(bNew), Cudd_SupportSize(dd, bNew) );
161 Cudd_RecursiveDeref( dd, bNew );
162 }
163
164 /**Function*************************************************************
165
166 Synopsis []
167
168 Description []
169
170 SideEffects []
171
172 SeeAlso []
173
174 ***********************************************************************/
Llb_NonlinPrepareVarMap(Llb_Mnn_t * p)175 void Llb_NonlinPrepareVarMap( Llb_Mnn_t * p )
176 {
177 Aig_Obj_t * pObjLi, * pObjLo, * pObj;
178 int i, iVarLi, iVarLo;
179 p->vCs2Glo = Vec_IntStartFull( Aig_ManObjNumMax(p->pAig) );
180 p->vNs2Glo = Vec_IntStartFull( Aig_ManObjNumMax(p->pAig) );
181 p->vGlo2Cs = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
182 p->vGlo2Ns = Vec_IntStartFull( Aig_ManRegNum(p->pAig) );
183 Saig_ManForEachLiLo( p->pAig, pObjLi, pObjLo, i )
184 {
185 iVarLi = Aig_ObjId(pObjLi);
186 iVarLo = Aig_ObjId(pObjLo);
187 assert( iVarLi >= 0 && iVarLi < Aig_ManObjNumMax(p->pAig) );
188 assert( iVarLo >= 0 && iVarLo < Aig_ManObjNumMax(p->pAig) );
189 Vec_IntWriteEntry( p->vCs2Glo, iVarLo, i );
190 Vec_IntWriteEntry( p->vNs2Glo, iVarLi, i );
191 Vec_IntWriteEntry( p->vGlo2Cs, i, iVarLo );
192 Vec_IntWriteEntry( p->vGlo2Ns, i, iVarLi );
193 }
194 // add mapping of the PIs
195 Saig_ManForEachPi( p->pAig, pObj, i )
196 {
197 Vec_IntWriteEntry( p->vCs2Glo, Aig_ObjId(pObj), Aig_ManRegNum(p->pAig)+i );
198 Vec_IntWriteEntry( p->vNs2Glo, Aig_ObjId(pObj), Aig_ManRegNum(p->pAig)+i );
199 }
200 }
201
202
203 /**Function*************************************************************
204
205 Synopsis []
206
207 Description []
208
209 SideEffects []
210
211 SeeAlso []
212
213 ***********************************************************************/
Llb_NonlinComputeInitState(Aig_Man_t * pAig,DdManager * dd)214 DdNode * Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd )
215 {
216 Aig_Obj_t * pObj;
217 DdNode * bRes, * bVar, * bTemp;
218 int i, iVar;
219 abctime TimeStop;
220 TimeStop = dd->TimeStop; dd->TimeStop = 0;
221 bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes );
222 Saig_ManForEachLo( pAig, pObj, i )
223 {
224 iVar = (Cudd_ReadSize(dd) == Aig_ManRegNum(pAig)) ? i : Aig_ObjId(pObj);
225 bVar = Cudd_bddIthVar( dd, iVar );
226 bRes = Cudd_bddAnd( dd, bTemp = bRes, Cudd_Not(bVar) ); Cudd_Ref( bRes );
227 Cudd_RecursiveDeref( dd, bTemp );
228 }
229 Cudd_Deref( bRes );
230 dd->TimeStop = TimeStop;
231 return bRes;
232 }
233
234
235 /**Function*************************************************************
236
237 Synopsis [Derives counter-example by backward reachability.]
238
239 Description []
240
241 SideEffects []
242
243 SeeAlso []
244
245 ***********************************************************************/
Llb_NonlinDeriveCex(Llb_Mnn_t * p)246 Abc_Cex_t * Llb_NonlinDeriveCex( Llb_Mnn_t * p )
247 {
248 Abc_Cex_t * pCex;
249 Aig_Obj_t * pObj;
250 Vec_Int_t * vVarsNs;
251 DdNode * bState = NULL, * bImage, * bOneCube, * bTemp, * bRing;
252 int i, v, RetValue, nPiOffset;
253 char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) );
254 assert( Vec_PtrSize(p->vRings) > 0 );
255
256 p->dd->TimeStop = 0;
257 p->ddR->TimeStop = 0;
258
259 // update quantifiable vars
260 memset( p->pVars2Q, 0, sizeof(int) * Cudd_ReadSize(p->dd) );
261 vVarsNs = Vec_IntAlloc( Aig_ManRegNum(p->pAig) );
262 Saig_ManForEachLi( p->pAig, pObj, i )
263 {
264 p->pVars2Q[Aig_ObjId(pObj)] = 1;
265 Vec_IntPush( vVarsNs, Aig_ObjId(pObj) );
266 }
267 /*
268 Saig_ManForEachLo( p->pAig, pObj, i )
269 printf( "%d ", pObj->Id );
270 printf( "\n" );
271 Saig_ManForEachLi( p->pAig, pObj, i )
272 printf( "%d(%d) ", pObj->Id, Aig_ObjFaninId0(pObj) );
273 printf( "\n" );
274 */
275 // allocate room for the counter-example
276 pCex = Abc_CexAlloc( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
277 pCex->iFrame = Vec_PtrSize(p->vRings) - 1;
278 pCex->iPo = -1;
279
280 // get the last cube
281 bOneCube = Cudd_bddIntersect( p->ddR, (DdNode *)Vec_PtrEntryLast(p->vRings), p->ddR->bFunc ); Cudd_Ref( bOneCube );
282 RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
283 Cudd_RecursiveDeref( p->ddR, bOneCube );
284 assert( RetValue );
285
286 // write PIs of counter-example
287 nPiOffset = Saig_ManRegNum(p->pAig) + Saig_ManPiNum(p->pAig) * (Vec_PtrSize(p->vRings) - 1);
288 Saig_ManForEachPi( p->pAig, pObj, i )
289 if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
290 Abc_InfoSetBit( pCex->pData, nPiOffset + i );
291
292 // write state in terms of NS variables
293 if ( Vec_PtrSize(p->vRings) > 1 )
294 {
295 bState = Llb_CoreComputeCube( p->dd, vVarsNs, 1, pValues ); Cudd_Ref( bState );
296 }
297 // perform backward analysis
298 Vec_PtrForEachEntryReverse( DdNode *, p->vRings, bRing, v )
299 {
300 if ( v == Vec_PtrSize(p->vRings) - 1 )
301 continue;
302 //Extra_bddPrintSupport( p->dd, bState ); printf( "\n" );
303 //Extra_bddPrintSupport( p->dd, bRing ); printf( "\n" );
304 // compute the next states
305 bImage = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bState,
306 p->pPars->fReorder, p->pPars->fVeryVerbose, NULL ); // consumed reference
307 assert( bImage != NULL );
308 Cudd_Ref( bImage );
309 //Extra_bddPrintSupport( p->dd, bImage ); printf( "\n" );
310
311 // move reached states into ring manager
312 bImage = Extra_TransferPermute( p->dd, p->ddR, bTemp = bImage, Vec_IntArray(p->vCs2Glo) ); Cudd_Ref( bImage );
313 Cudd_RecursiveDeref( p->dd, bTemp );
314
315 // intersect with the previous set
316 bOneCube = Cudd_bddIntersect( p->ddR, bImage, bRing ); Cudd_Ref( bOneCube );
317 Cudd_RecursiveDeref( p->ddR, bImage );
318
319 // find any assignment of the BDD
320 RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
321 Cudd_RecursiveDeref( p->ddR, bOneCube );
322 assert( RetValue );
323
324 // write PIs of counter-example
325 nPiOffset -= Saig_ManPiNum(p->pAig);
326 Saig_ManForEachPi( p->pAig, pObj, i )
327 if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
328 Abc_InfoSetBit( pCex->pData, nPiOffset + i );
329
330 // check that we get the init state
331 if ( v == 0 )
332 {
333 Saig_ManForEachLo( p->pAig, pObj, i )
334 assert( pValues[i] == 0 );
335 break;
336 }
337
338 // write state in terms of NS variables
339 bState = Llb_CoreComputeCube( p->dd, vVarsNs, 1, pValues ); Cudd_Ref( bState );
340 }
341 assert( nPiOffset == Saig_ManRegNum(p->pAig) );
342 // update the output number
343 //Abc_CexPrint( pCex );
344 RetValue = Saig_ManFindFailedPoCex( p->pInit, pCex );
345 assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pInit) ); // invalid CEX!!!
346 pCex->iPo = RetValue;
347 // cleanup
348 ABC_FREE( pValues );
349 Vec_IntFree( vVarsNs );
350 return pCex;
351 }
352
353
354 /**Function*************************************************************
355
356 Synopsis [Perform reachability with hints.]
357
358 Description []
359
360 SideEffects []
361
362 SeeAlso []
363
364 ***********************************************************************/
Llb_NonlinReoHook(DdManager * dd,char * Type,void * Method)365 int Llb_NonlinReoHook( DdManager * dd, char * Type, void * Method )
366 {
367 Aig_Man_t * pAig = (Aig_Man_t *)dd->bFunc;
368 Aig_Obj_t * pObj;
369 int i;
370 printf( "Order: " );
371 for ( i = 0; i < Cudd_ReadSize(dd); i++ )
372 {
373 pObj = Aig_ManObj( pAig, i );
374 if ( pObj == NULL )
375 continue;
376 if ( Saig_ObjIsPi(pAig, pObj) )
377 printf( "pi" );
378 else if ( Saig_ObjIsLo(pAig, pObj) )
379 printf( "lo" );
380 else if ( Saig_ObjIsPo(pAig, pObj) )
381 printf( "po" );
382 else if ( Saig_ObjIsLi(pAig, pObj) )
383 printf( "li" );
384 else continue;
385 printf( "%d=%d ", i, dd->perm[i] );
386 }
387 printf( "\n" );
388 return 1;
389 }
390
391 /**Function*************************************************************
392
393 Synopsis [Perform reachability with hints.]
394
395 Description []
396
397 SideEffects []
398
399 SeeAlso []
400
401 ***********************************************************************/
Llb_NonlinCompPerms(DdManager * dd,int * pVar2Lev)402 int Llb_NonlinCompPerms( DdManager * dd, int * pVar2Lev )
403 {
404 DdSubtable * pSubt;
405 int i, Sum = 0, Entry;
406 for ( i = 0; i < dd->size; i++ )
407 {
408 pSubt = &(dd->subtables[dd->perm[i]]);
409 if ( pSubt->keys == pSubt->dead + 1 )
410 continue;
411 Entry = Abc_MaxInt(dd->perm[i], pVar2Lev[i]) - Abc_MinInt(dd->perm[i], pVar2Lev[i]);
412 Sum += Entry;
413 //printf( "%d-%d(%d) ", dd->perm[i], pV2L[i], Entry );
414 }
415 return Sum;
416 }
417
418 /**Function*************************************************************
419
420 Synopsis [Perform reachability with hints.]
421
422 Description []
423
424 SideEffects []
425
426 SeeAlso []
427
428 ***********************************************************************/
Llb_NonlinReachability(Llb_Mnn_t * p)429 int Llb_NonlinReachability( Llb_Mnn_t * p )
430 {
431 DdNode * bTemp, * bNext;
432 int nIters, nBddSize0, nBddSize = -1, NumCmp;//, Limit = p->pPars->nBddMax;
433 abctime clk2, clk3, clk = Abc_Clock();
434 assert( Aig_ManRegNum(p->pAig) > 0 );
435
436 // compute time to stop
437 p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
438
439 // set the stop time parameter
440 p->dd->TimeStop = p->pPars->TimeTarget;
441 p->ddG->TimeStop = p->pPars->TimeTarget;
442 p->ddR->TimeStop = p->pPars->TimeTarget;
443
444 // set reordering hooks
445 assert( p->dd->bFunc == NULL );
446 // p->dd->bFunc = (DdNode *)p->pAig;
447 // Cudd_AddHook( p->dd, Llb_NonlinReoHook, CUDD_POST_REORDERING_HOOK );
448
449 // create bad state in the ring manager
450 p->ddR->bFunc = Llb_BddComputeBad( p->pInit, p->ddR, p->pPars->TimeTarget );
451 if ( p->ddR->bFunc == NULL )
452 {
453 if ( !p->pPars->fSilent )
454 printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
455 p->pPars->iFrame = -1;
456 return -1;
457 }
458 Cudd_Ref( p->ddR->bFunc );
459 // compute the starting set of states
460 Cudd_Quit( p->dd );
461 p->dd = Llb_NonlinImageStart( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->pOrderL, 1, p->pPars->TimeTarget );
462 if ( p->dd == NULL )
463 {
464 if ( !p->pPars->fSilent )
465 printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
466 p->pPars->iFrame = -1;
467 return -1;
468 }
469 p->dd->bFunc = Llb_NonlinComputeInitState( p->pAig, p->dd ); Cudd_Ref( p->dd->bFunc ); // current
470 p->ddG->bFunc = Llb_NonlinComputeInitState( p->pAig, p->ddG ); Cudd_Ref( p->ddG->bFunc ); // reached
471 p->ddG->bFunc2 = Llb_NonlinComputeInitState( p->pAig, p->ddG ); Cudd_Ref( p->ddG->bFunc2 ); // frontier
472 for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ )
473 {
474 // check the runtime limit
475 clk2 = Abc_Clock();
476 if ( p->pPars->TimeLimit && Abc_Clock() > p->pPars->TimeTarget )
477 {
478 if ( !p->pPars->fSilent )
479 printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit );
480 p->pPars->iFrame = nIters - 1;
481 Llb_NonlinImageQuit();
482 return -1;
483 }
484
485 // save the onion ring
486 bTemp = Extra_TransferPermute( p->dd, p->ddR, p->dd->bFunc, Vec_IntArray(p->vCs2Glo) );
487 if ( bTemp == NULL )
488 {
489 if ( !p->pPars->fSilent )
490 printf( "Reached timeout (%d seconds) during ring transfer.\n", p->pPars->TimeLimit );
491 p->pPars->iFrame = nIters - 1;
492 Llb_NonlinImageQuit();
493 return -1;
494 }
495 Cudd_Ref( bTemp );
496 Vec_PtrPush( p->vRings, bTemp );
497
498 // check it for bad states
499 if ( !p->pPars->fSkipOutCheck && !Cudd_bddLeq( p->ddR, bTemp, Cudd_Not(p->ddR->bFunc) ) )
500 {
501 assert( p->pInit->pSeqModel == NULL );
502 if ( !p->pPars->fBackward )
503 p->pInit->pSeqModel = Llb_NonlinDeriveCex( p );
504 if ( !p->pPars->fSilent )
505 {
506 if ( !p->pPars->fBackward )
507 Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pInit->pSeqModel->iPo, nIters );
508 else
509 Abc_Print( 1, "Output ??? was asserted in frame %d (counter-example is not produced). ", nIters );
510 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
511 }
512 p->pPars->iFrame = nIters - 1;
513 Llb_NonlinImageQuit();
514 return 0;
515 }
516
517 // compute the next states
518 clk3 = Abc_Clock();
519 nBddSize0 = Cudd_DagSize( p->dd->bFunc );
520 bNext = Llb_NonlinImageCompute( p->dd->bFunc, p->pPars->fReorder, 0, 1, p->pOrderL ); // consumes ref
521 // bNext = Llb_NonlinImage( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->dd, bCurrent,
522 // p->pPars->fReorder, p->pPars->fVeryVerbose, NULL, ABC_INFINITY, p->pPars->TimeTarget );
523 if ( bNext == NULL )
524 {
525 if ( !p->pPars->fSilent )
526 printf( "Reached timeout (%d seconds) during image computation in quantification.\n", p->pPars->TimeLimit );
527 p->pPars->iFrame = nIters - 1;
528 Llb_NonlinImageQuit();
529 return -1;
530 }
531 Cudd_Ref( bNext );
532 nBddSize = Cudd_DagSize( bNext );
533 p->timeImage += Abc_Clock() - clk3;
534
535
536 // transfer to the state manager
537 clk3 = Abc_Clock();
538 Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 );
539 p->ddG->bFunc2 = Extra_TransferPermute( p->dd, p->ddG, bNext, Vec_IntArray(p->vNs2Glo) );
540 // p->ddG->bFunc2 = Extra_bddAndPermute( p->ddG, Cudd_Not(p->ddG->bFunc), p->dd, bNext, Vec_IntArray(p->vNs2Glo) );
541 if ( p->ddG->bFunc2 == NULL )
542 {
543 if ( !p->pPars->fSilent )
544 printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit );
545 p->pPars->iFrame = nIters - 1;
546 Cudd_RecursiveDeref( p->dd, bNext );
547 Llb_NonlinImageQuit();
548 return -1;
549 }
550 Cudd_Ref( p->ddG->bFunc2 );
551 Cudd_RecursiveDeref( p->dd, bNext );
552 p->timeTran1 += Abc_Clock() - clk3;
553
554 // save permutation
555 NumCmp = Llb_NonlinCompPerms( p->dd, p->pOrderL2 );
556 // save order before image computation
557 memcpy( p->pOrderL2, p->dd->perm, sizeof(int) * p->dd->size );
558 // update the image computation manager
559 p->timeReo += Cudd_ReadReorderingTime(p->dd);
560 p->ddLocReos += Cudd_ReadReorderings(p->dd);
561 p->ddLocGrbs += Cudd_ReadGarbageCollections(p->dd);
562 Llb_NonlinImageQuit();
563 p->dd = Llb_NonlinImageStart( p->pAig, p->vLeaves, p->vRoots, p->pVars2Q, p->pOrderL, 0, p->pPars->TimeTarget );
564 if ( p->dd == NULL )
565 {
566 if ( !p->pPars->fSilent )
567 printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
568 p->pPars->iFrame = nIters - 1;
569 return -1;
570 }
571 //Extra_TestAndPerm( p->ddG, Cudd_Not(p->ddG->bFunc), p->ddG->bFunc2 );
572
573 // derive new states
574 clk3 = Abc_Clock();
575 p->ddG->bFunc2 = Cudd_bddAnd( p->ddG, bTemp = p->ddG->bFunc2, Cudd_Not(p->ddG->bFunc) );
576 if ( p->ddG->bFunc2 == NULL )
577 {
578 if ( !p->pPars->fSilent )
579 printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit );
580 p->pPars->iFrame = nIters - 1;
581 Cudd_RecursiveDeref( p->ddG, bTemp );
582 Llb_NonlinImageQuit();
583 return -1;
584 }
585 Cudd_Ref( p->ddG->bFunc2 );
586 Cudd_RecursiveDeref( p->ddG, bTemp );
587 p->timeGloba += Abc_Clock() - clk3;
588
589 if ( Cudd_IsConstant(p->ddG->bFunc2) )
590 break;
591 // add to the reached set
592 clk3 = Abc_Clock();
593 p->ddG->bFunc = Cudd_bddOr( p->ddG, bTemp = p->ddG->bFunc, p->ddG->bFunc2 );
594 if ( p->ddG->bFunc == NULL )
595 {
596 if ( !p->pPars->fSilent )
597 printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit );
598 p->pPars->iFrame = nIters - 1;
599 Cudd_RecursiveDeref( p->ddG, bTemp );
600 Llb_NonlinImageQuit();
601 return -1;
602 }
603 Cudd_Ref( p->ddG->bFunc );
604 Cudd_RecursiveDeref( p->ddG, bTemp );
605 p->timeGloba += Abc_Clock() - clk3;
606
607 // reset permutation
608 // RetValue = Cudd_CheckZeroRef( dd );
609 // assert( RetValue == 0 );
610 // Cudd_ShuffleHeap( dd, pOrderG );
611
612 // move new states to the working manager
613 clk3 = Abc_Clock();
614 p->dd->bFunc = Extra_TransferPermute( p->ddG, p->dd, p->ddG->bFunc2, Vec_IntArray(p->vGlo2Cs) );
615 if ( p->dd->bFunc == NULL )
616 {
617 if ( !p->pPars->fSilent )
618 printf( "Reached timeout (%d seconds) during image computation in transfer 2.\n", p->pPars->TimeLimit );
619 p->pPars->iFrame = nIters - 1;
620 Llb_NonlinImageQuit();
621 return -1;
622 }
623 Cudd_Ref( p->dd->bFunc );
624 p->timeTran2 += Abc_Clock() - clk3;
625
626 // report the results
627 if ( p->pPars->fVerbose )
628 {
629 printf( "I =%3d : ", nIters );
630 printf( "Fr =%7d ", nBddSize0 );
631 printf( "Im =%7d ", nBddSize );
632 printf( "(%4d %4d) ", p->ddLocReos, p->ddLocGrbs );
633 printf( "Rea =%6d ", Cudd_DagSize(p->ddG->bFunc) );
634 printf( "(%4d %4d) ", Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) );
635 printf( "S =%4d ", nSuppMax );
636 printf( "cL =%5d ", NumCmp );
637 printf( "cG =%5d ", Llb_NonlinCompPerms( p->ddG, p->pOrderG ) );
638 Abc_PrintTime( 1, "T", Abc_Clock() - clk2 );
639 memcpy( p->pOrderG, p->ddG->perm, sizeof(int) * p->ddG->size );
640 }
641 /*
642 if ( pPars->fVerbose )
643 {
644 double nMints = Cudd_CountMinterm(ddG, bReached, Saig_ManRegNum(pAig) );
645 // Extra_bddPrint( ddG, bReached );printf( "\n" );
646 printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(pAig)) );
647 fflush( stdout );
648 }
649 */
650 if ( nIters == p->pPars->nIterMax - 1 )
651 {
652 if ( !p->pPars->fSilent )
653 printf( "Reached limit on the number of timeframes (%d).\n", p->pPars->nIterMax );
654 p->pPars->iFrame = nIters;
655 Llb_NonlinImageQuit();
656 return -1;
657 }
658 }
659 Llb_NonlinImageQuit();
660
661 // report the stats
662 if ( p->pPars->fVerbose )
663 {
664 double nMints = Cudd_CountMinterm(p->ddG, p->ddG->bFunc, Saig_ManRegNum(p->pAig) );
665 if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax )
666 printf( "Reachability analysis is stopped after %d frames.\n", nIters );
667 else
668 printf( "Reachability analysis completed after %d frames.\n", nIters );
669 printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
670 fflush( stdout );
671 }
672 if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax )
673 {
674 if ( !p->pPars->fSilent )
675 printf( "Verified only for states reachable in %d frames. ", nIters );
676 p->pPars->iFrame = p->pPars->nIterMax;
677 return -1; // undecided
678 }
679 // report
680 if ( !p->pPars->fSilent )
681 printf( "The miter is proved unreachable after %d iterations. ", nIters );
682 p->pPars->iFrame = nIters - 1;
683 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
684 return 1; // unreachable
685 }
686
687 /**Function*************************************************************
688
689 Synopsis []
690
691 Description []
692
693 SideEffects []
694
695 SeeAlso []
696
697 ***********************************************************************/
Llb_MnnStart(Aig_Man_t * pInit,Aig_Man_t * pAig,Gia_ParLlb_t * pPars)698 Llb_Mnn_t * Llb_MnnStart( Aig_Man_t * pInit, Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
699 {
700 Llb_Mnn_t * p;
701 Aig_Obj_t * pObj;
702 int i;
703 p = ABC_CALLOC( Llb_Mnn_t, 1 );
704 p->pInit = pInit;
705 p->pAig = pAig;
706 p->pPars = pPars;
707 p->dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
708 p->ddG = Cudd_Init( Aig_ManRegNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
709 p->ddR = Cudd_Init( Aig_ManCiNum(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
710 Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT );
711 Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT );
712 Cudd_AutodynEnable( p->ddR, CUDD_REORDER_SYMM_SIFT );
713 p->vRings = Vec_PtrAlloc( 100 );
714 // create leaves
715 p->vLeaves = Vec_PtrAlloc( Aig_ManCiNum(pAig) );
716 Aig_ManForEachCi( pAig, pObj, i )
717 Vec_PtrPush( p->vLeaves, pObj );
718 // create roots
719 p->vRoots = Vec_PtrAlloc( Aig_ManCoNum(pAig) );
720 Saig_ManForEachLi( pAig, pObj, i )
721 Vec_PtrPush( p->vRoots, pObj );
722 // variables to quantify
723 p->pOrderL = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
724 p->pOrderL2= ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
725 p->pOrderG = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
726 p->pVars2Q = ABC_CALLOC( int, Aig_ManObjNumMax(pAig) );
727 Aig_ManForEachCi( pAig, pObj, i )
728 p->pVars2Q[Aig_ObjId(pObj)] = 1;
729 for ( i = 0; i < Aig_ManObjNumMax(pAig); i++ )
730 p->pOrderL[i] = p->pOrderL2[i] = p->pOrderG[i] = i;
731 Llb_NonlinPrepareVarMap( p );
732 return p;
733 }
734
735 /**Function*************************************************************
736
737 Synopsis []
738
739 Description []
740
741 SideEffects []
742
743 SeeAlso []
744
745 ***********************************************************************/
Llb_MnnStop(Llb_Mnn_t * p)746 void Llb_MnnStop( Llb_Mnn_t * p )
747 {
748 DdNode * bTemp;
749 int i;
750 if ( p->pPars->fVerbose )
751 {
752 p->timeOther = p->timeTotal - p->timeImage - p->timeTran1 - p->timeTran2 - p->timeGloba;
753 p->timeReoG = Cudd_ReadReorderingTime(p->ddG);
754 ABC_PRTP( "Image ", p->timeImage, p->timeTotal );
755 ABC_PRTP( " build ", timeBuild, p->timeTotal );
756 ABC_PRTP( " and-ex ", timeAndEx, p->timeTotal );
757 ABC_PRTP( " other ", timeOther, p->timeTotal );
758 ABC_PRTP( "Transfer1", p->timeTran1, p->timeTotal );
759 ABC_PRTP( "Transfer2", p->timeTran2, p->timeTotal );
760 ABC_PRTP( "Global ", p->timeGloba, p->timeTotal );
761 ABC_PRTP( "Other ", p->timeOther, p->timeTotal );
762 ABC_PRTP( "TOTAL ", p->timeTotal, p->timeTotal );
763 ABC_PRTP( " reo ", p->timeReo, p->timeTotal );
764 ABC_PRTP( " reoG ", p->timeReoG, p->timeTotal );
765 }
766 if ( p->ddR->bFunc )
767 Cudd_RecursiveDeref( p->ddR, p->ddR->bFunc );
768 Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
769 Cudd_RecursiveDeref( p->ddR, bTemp );
770 Vec_PtrFree( p->vRings );
771 if ( p->ddG->bFunc )
772 Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc );
773 if ( p->ddG->bFunc2 )
774 Cudd_RecursiveDeref( p->ddG, p->ddG->bFunc2 );
775 // printf( "manager1\n" );
776 // Extra_StopManager( p->dd );
777 // printf( "manager2\n" );
778 Extra_StopManager( p->ddG );
779 // printf( "manager3\n" );
780 Extra_StopManager( p->ddR );
781 Vec_IntFreeP( &p->vCs2Glo );
782 Vec_IntFreeP( &p->vNs2Glo );
783 Vec_IntFreeP( &p->vGlo2Cs );
784 Vec_IntFreeP( &p->vGlo2Ns );
785 Vec_PtrFree( p->vLeaves );
786 Vec_PtrFree( p->vRoots );
787 ABC_FREE( p->pVars2Q );
788 ABC_FREE( p->pOrderL );
789 ABC_FREE( p->pOrderL2 );
790 ABC_FREE( p->pOrderG );
791 ABC_FREE( p );
792 }
793
794
795 /**Function*************************************************************
796
797 Synopsis [Finds balanced cut.]
798
799 Description []
800
801 SideEffects []
802
803 SeeAlso []
804
805 ***********************************************************************/
Llb_NonlinExperiment(Aig_Man_t * pAig,int Num)806 void Llb_NonlinExperiment( Aig_Man_t * pAig, int Num )
807 {
808 Llb_Mnn_t * pMnn;
809 Gia_ParLlb_t Pars, * pPars = &Pars;
810 Aig_Man_t * p;
811 abctime clk = Abc_Clock();
812
813 Llb_ManSetDefaultParams( pPars );
814 pPars->fVerbose = 1;
815
816 p = Aig_ManDupFlopsOnly( pAig );
817 //Aig_ManShow( p, 0, NULL );
818 Aig_ManPrintStats( pAig );
819 Aig_ManPrintStats( p );
820
821 pMnn = Llb_MnnStart( pAig, p, pPars );
822 Llb_NonlinReachability( pMnn );
823 pMnn->timeTotal = Abc_Clock() - clk;
824 Llb_MnnStop( pMnn );
825
826 Aig_ManStop( p );
827 }
828
829 /**Function*************************************************************
830
831 Synopsis [Finds balanced cut.]
832
833 Description []
834
835 SideEffects []
836
837 SeeAlso []
838
839 ***********************************************************************/
Llb_NonlinCoreReach(Aig_Man_t * pAig,Gia_ParLlb_t * pPars)840 int Llb_NonlinCoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
841 {
842 Llb_Mnn_t * pMnn;
843 Aig_Man_t * p;
844 int RetValue = -1;
845
846 p = Aig_ManDupFlopsOnly( pAig );
847 //Aig_ManShow( p, 0, NULL );
848 if ( pPars->fVerbose )
849 Aig_ManPrintStats( pAig );
850 if ( pPars->fVerbose )
851 Aig_ManPrintStats( p );
852
853 if ( !pPars->fSkipReach )
854 {
855 abctime clk = Abc_Clock();
856 pMnn = Llb_MnnStart( pAig, p, pPars );
857 RetValue = Llb_NonlinReachability( pMnn );
858 pMnn->timeTotal = Abc_Clock() - clk;
859 Llb_MnnStop( pMnn );
860 }
861
862 Aig_ManStop( p );
863 return RetValue;
864 }
865
866 ////////////////////////////////////////////////////////////////////////
867 /// END OF FILE ///
868 ////////////////////////////////////////////////////////////////////////
869
870
871 ABC_NAMESPACE_IMPL_END
872
873