ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
llb1Reach.c
Go to the documentation of this file.
1
20
21#include "llbInt.h"
22
23ABC_NAMESPACE_IMPL_START
24
25
29
33
45DdNode * Llb_ManConstructOutBdd( Aig_Man_t * pAig, Aig_Obj_t * pNode, DdManager * dd )
46{
47 DdNode * bBdd0, * bBdd1, * bFunc;
48 Vec_Ptr_t * vNodes;
49 Aig_Obj_t * pObj = NULL;
50 int i;
51 abctime TimeStop;
52 if ( Aig_ObjFanin0(pNode) == Aig_ManConst1(pAig) )
53 return Cudd_NotCond( Cudd_ReadOne(dd), Aig_ObjFaninC0(pNode) );
54 TimeStop = dd->TimeStop; dd->TimeStop = 0;
55 vNodes = Aig_ManDfsNodes( pAig, &pNode, 1 );
56 assert( Vec_PtrSize(vNodes) > 0 );
57 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
58 {
59 if ( !Aig_ObjIsNode(pObj) )
60 continue;
61 bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
62 bBdd1 = Cudd_NotCond( Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
63 pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 ); Cudd_Ref( (DdNode *)pObj->pData );
64 }
65 bFunc = (DdNode *)pObj->pData; Cudd_Ref( bFunc );
66 Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
67 {
68 if ( !Aig_ObjIsNode(pObj) )
69 continue;
70 Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
71 }
72 Vec_PtrFree( vNodes );
73 if ( Aig_ObjIsCo(pNode) )
74 bFunc = Cudd_NotCond( bFunc, Aig_ObjFaninC0(pNode) );
75 Cudd_Deref( bFunc );
76 dd->TimeStop = TimeStop;
77 return bFunc;
78}
79
91DdNode * Llb_ManConstructGroupBdd( Llb_Man_t * p, Llb_Grp_t * pGroup )
92{
93 Aig_Obj_t * pObj;
94 DdNode * bBdd0, * bBdd1, * bRes, * bXor, * bTemp;
95 int i, k;
96 Aig_ManConst1(p->pAig)->pData = Cudd_ReadOne( p->dd );
97 Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
98 pObj->pData = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
99 Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vNodes, pObj, i )
100 {
101 bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
102 bBdd1 = Cudd_NotCond( Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
103// pObj->pData = Extra_bddAndTime( p->dd, bBdd0, bBdd1, p->pPars->TimeTarget );
104 pObj->pData = Cudd_bddAnd( p->dd, bBdd0, bBdd1 );
105 if ( pObj->pData == NULL )
106 {
107 Vec_PtrForEachEntryStop( Aig_Obj_t *, pGroup->vNodes, pObj, k, i )
108 if ( pObj->pData )
109 Cudd_RecursiveDeref( p->dd, (DdNode *)pObj->pData );
110 return NULL;
111 }
112 Cudd_Ref( (DdNode *)pObj->pData );
113 }
114 bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes );
115 Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
116 {
117 if ( Aig_ObjIsCo(pObj) )
118 bBdd0 = Cudd_NotCond( Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
119 else
120 bBdd0 = (DdNode *)pObj->pData;
121 bBdd1 = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
122 bXor = Cudd_bddXor( p->dd, bBdd0, bBdd1 ); Cudd_Ref( bXor );
123// bRes = Extra_bddAndTime( p->dd, bTemp = bRes, Cudd_Not(bXor), p->pPars->TimeTarget );
124 bRes = Cudd_bddAnd( p->dd, bTemp = bRes, Cudd_Not(bXor) );
125 if ( bRes == NULL )
126 {
127 Cudd_RecursiveDeref( p->dd, bTemp );
128 Cudd_RecursiveDeref( p->dd, bXor );
129 Vec_PtrForEachEntryStop( Aig_Obj_t *, pGroup->vNodes, pObj, k, i )
130 if ( pObj->pData )
131 Cudd_RecursiveDeref( p->dd, (DdNode *)pObj->pData );
132 return NULL;
133 }
134 Cudd_Ref( bRes );
135 Cudd_RecursiveDeref( p->dd, bTemp );
136 Cudd_RecursiveDeref( p->dd, bXor );
137 }
138 Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vNodes, pObj, i )
139 Cudd_RecursiveDeref( p->dd, (DdNode *)pObj->pData );
140 Cudd_Deref( bRes );
141 return bRes;
142}
143
155DdNode * Llb_ManConstructQuantCubeIntern( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace, int fBackward )
156{
157 Aig_Obj_t * pObj;
158 DdNode * bRes, * bTemp, * bVar;
159 int i, iGroupFirst, iGroupLast;
160 abctime TimeStop;
161 TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
162 bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes );
163 Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
164 {
165 if ( fBackward && Saig_ObjIsPi(p->pAig, pObj) )
166 continue;
167 iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj));
168 iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj));
169 assert( iGroupFirst <= iGroupLast );
170 if ( iGroupFirst < iGroupLast )
171 continue;
172 bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
173 bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
174 Cudd_RecursiveDeref( p->dd, bTemp );
175 }
176 Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
177 {
178 if ( fBackward && Saig_ObjIsPi(p->pAig, pObj) )
179 continue;
180 iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj));
181 iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj));
182 assert( iGroupFirst <= iGroupLast );
183 if ( iGroupFirst < iGroupLast )
184 continue;
185 bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
186 bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
187 Cudd_RecursiveDeref( p->dd, bTemp );
188 }
189 Cudd_Deref( bRes );
190 p->dd->TimeStop = TimeStop;
191 return bRes;
192}
193
205DdNode * Llb_ManConstructQuantCubeFwd( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace )
206{
207 Aig_Obj_t * pObj;
208 DdNode * bRes, * bTemp, * bVar;
209 int i, iGroupLast;
210 abctime TimeStop;
211 TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
212 bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes );
213 Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
214 {
215 iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj));
216 assert( iGroupLast >= iGrpPlace );
217 if ( iGroupLast > iGrpPlace )
218 continue;
219 bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
220 bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
221 Cudd_RecursiveDeref( p->dd, bTemp );
222 }
223 Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
224 {
225 iGroupLast = Vec_IntEntry(p->vVarEnds, Aig_ObjId(pObj));
226 assert( iGroupLast >= iGrpPlace );
227 if ( iGroupLast > iGrpPlace )
228 continue;
229 bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
230 bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
231 Cudd_RecursiveDeref( p->dd, bTemp );
232 }
233 Cudd_Deref( bRes );
234 p->dd->TimeStop = TimeStop;
235 return bRes;
236}
237
249DdNode * Llb_ManConstructQuantCubeBwd( Llb_Man_t * p, Llb_Grp_t * pGroup, int iGrpPlace )
250{
251 Aig_Obj_t * pObj;
252 DdNode * bRes, * bTemp, * bVar;
253 int i, iGroupFirst;
254 abctime TimeStop;
255 TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
256 bRes = Cudd_ReadOne( p->dd ); Cudd_Ref( bRes );
257 Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vIns, pObj, i )
258 {
259 if ( Saig_ObjIsPi(p->pAig, pObj) )
260 continue;
261 iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj));
262 assert( iGroupFirst <= iGrpPlace );
263 if ( iGroupFirst < iGrpPlace )
264 continue;
265 bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
266 bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
267 Cudd_RecursiveDeref( p->dd, bTemp );
268 }
269 Vec_PtrForEachEntry( Aig_Obj_t *, pGroup->vOuts, pObj, i )
270 {
271 if ( Saig_ObjIsPi(p->pAig, pObj) )
272 continue;
273 iGroupFirst = Vec_IntEntry(p->vVarBegs, Aig_ObjId(pObj));
274 assert( iGroupFirst <= iGrpPlace );
275 if ( iGroupFirst < iGrpPlace )
276 continue;
277 bVar = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj)) );
278 bRes = Cudd_bddAnd( p->dd, bTemp = bRes, bVar ); Cudd_Ref( bRes );
279 Cudd_RecursiveDeref( p->dd, bTemp );
280 }
281 Cudd_Deref( bRes );
282 p->dd->TimeStop = TimeStop;
283 return bRes;
284}
285
297DdNode * Llb_ManComputeInitState( Llb_Man_t * p, DdManager * dd )
298{
299 Aig_Obj_t * pObj;
300 DdNode * bRes, * bVar, * bTemp;
301 int i, iVar;
302 abctime TimeStop;
303 TimeStop = dd->TimeStop; dd->TimeStop = 0;
304 bRes = Cudd_ReadOne( dd ); Cudd_Ref( bRes );
305 Saig_ManForEachLo( p->pAig, pObj, i )
306 {
307 iVar = (dd == p->ddG) ? i : Vec_IntEntry(p->vObj2Var, Aig_ObjId(pObj));
308 bVar = Cudd_bddIthVar( dd, iVar );
309 bRes = Cudd_bddAnd( dd, bTemp = bRes, Cudd_Not(bVar) ); Cudd_Ref( bRes );
310 Cudd_RecursiveDeref( dd, bTemp );
311 }
312 Cudd_Deref( bRes );
313 dd->TimeStop = TimeStop;
314 return bRes;
315}
316
328DdNode * Llb_ManComputeImage( Llb_Man_t * p, DdNode * bInit, int fBackward )
329{
330 int fCheckSupport = 0;
331 Llb_Grp_t * pGroup;
332 DdNode * bImage, * bGroup, * bCube, * bTemp;
333 int k, Index;
334 bImage = bInit; Cudd_Ref( bImage );
335 for ( k = 1; k < p->pMatrix->nCols-1; k++ )
336 {
337 if ( fBackward )
338 Index = p->pMatrix->nCols - 1 - k;
339 else
340 Index = k;
341
342 // compute group BDD
343 pGroup = p->pMatrix->pColGrps[Index];
344 bGroup = Llb_ManConstructGroupBdd( p, pGroup );
345 if ( bGroup == NULL )
346 {
347 Cudd_RecursiveDeref( p->dd, bImage );
348 return NULL;
349 }
350 Cudd_Ref( bGroup );
351 // quantify variables appearing only in this group
352 bCube = Llb_ManConstructQuantCubeIntern( p, pGroup, Index, fBackward ); Cudd_Ref( bCube );
353 bGroup = Cudd_bddExistAbstract( p->dd, bTemp = bGroup, bCube );
354 if ( bGroup == NULL )
355 {
356 Cudd_RecursiveDeref( p->dd, bTemp );
357 Cudd_RecursiveDeref( p->dd, bCube );
358 return NULL;
359 }
360 Cudd_Ref( bGroup );
361 Cudd_RecursiveDeref( p->dd, bTemp );
362 Cudd_RecursiveDeref( p->dd, bCube );
363 // perform partial product
364 if ( fBackward )
365 bCube = Llb_ManConstructQuantCubeBwd( p, pGroup, Index );
366 else
367 bCube = Llb_ManConstructQuantCubeFwd( p, pGroup, Index );
368 Cudd_Ref( bCube );
369// bImage = Extra_bddAndAbstractTime( p->dd, bTemp = bImage, bGroup, bCube, p->pPars->TimeTarget );
370 bImage = Cudd_bddAndAbstract( p->dd, bTemp = bImage, bGroup, bCube );
371 if ( bImage == NULL )
372 {
373 Cudd_RecursiveDeref( p->dd, bTemp );
374 Cudd_RecursiveDeref( p->dd, bGroup );
375 Cudd_RecursiveDeref( p->dd, bCube );
376 return NULL;
377 }
378 Cudd_Ref( bImage );
379 Cudd_RecursiveDeref( p->dd, bTemp );
380 Cudd_RecursiveDeref( p->dd, bGroup );
381 Cudd_RecursiveDeref( p->dd, bCube );
382 }
383
384 // make sure image depends on next state vars
385 if ( fCheckSupport )
386 {
387 bCube = Cudd_Support( p->dd, bImage ); Cudd_Ref( bCube );
388 for ( bTemp = bCube; bTemp != p->dd->one; bTemp = cuddT(bTemp) )
389 {
390 int ObjId = Vec_IntEntry( p->vVar2Obj, bTemp->index );
391 Aig_Obj_t * pObj = Aig_ManObj( p->pAig, ObjId );
392 if ( !Saig_ObjIsLi(p->pAig, pObj) )
393 printf( "Var %d assigned to obj %d that is not LI\n", bTemp->index, ObjId );
394 }
395 Cudd_RecursiveDeref( p->dd, bCube );
396 }
397 Cudd_Deref( bImage );
398 return bImage;
399}
400
412DdNode * Llb_ManCreateConstraints( Llb_Man_t * p, Vec_Int_t * vHints, int fUseNsVars )
413{
414 DdNode * bConstr, * bFunc, * bTemp;
415 Aig_Obj_t * pObj;
416 int i, Entry;
417 abctime TimeStop;
418 if ( vHints == NULL )
419 return Cudd_ReadOne( p->dd );
420 TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
421 assert( Aig_ManCiNum(p->pAig) == Aig_ManCiNum(p->pAigGlo) );
422 // assign const and PI nodes to the original AIG
423 Aig_ManCleanData( p->pAig );
424 Aig_ManConst1( p->pAig )->pData = Cudd_ReadOne( p->dd );
425 Saig_ManForEachPi( p->pAig, pObj, i )
426 pObj->pData = Cudd_bddIthVar( p->dd, Vec_IntEntry(p->vObj2Var,Aig_ObjId(pObj)) );
427 Saig_ManForEachLo( p->pAig, pObj, i )
428 {
429 if ( fUseNsVars )
430 Entry = Vec_IntEntry( p->vObj2Var, Aig_ObjId(Saig_ObjLoToLi(p->pAig, pObj)) );
431 else
432 Entry = Vec_IntEntry( p->vObj2Var, Aig_ObjId(pObj) );
433 pObj->pData = Cudd_bddIthVar( p->dd, Entry );
434 }
435 // transfer them to the global AIG
436 Aig_ManCleanData( p->pAigGlo );
437 Aig_ManConst1( p->pAigGlo )->pData = Cudd_ReadOne( p->dd );
438 Aig_ManForEachCi( p->pAigGlo, pObj, i )
439 pObj->pData = Aig_ManCi(p->pAig, i)->pData;
440 // derive consraints
441 bConstr = Cudd_ReadOne( p->dd ); Cudd_Ref( bConstr );
442 Vec_IntForEachEntry( vHints, Entry, i )
443 {
444 if ( Entry != 0 && Entry != 1 )
445 continue;
446 bFunc = Llb_ManConstructOutBdd( p->pAigGlo, Aig_ManObj(p->pAigGlo, i), p->dd ); Cudd_Ref( bFunc );
447 bFunc = Cudd_NotCond( bFunc, Entry ); // restrict to not constraint
448 // make the product
449 bConstr = Cudd_bddAnd( p->dd, bTemp = bConstr, bFunc ); Cudd_Ref( bConstr );
450 Cudd_RecursiveDeref( p->dd, bTemp );
451 Cudd_RecursiveDeref( p->dd, bFunc );
452 }
453 Cudd_Deref( bConstr );
454 p->dd->TimeStop = TimeStop;
455 return bConstr;
456}
457
469Abc_Cex_t * Llb_ManReachDeriveCex( Llb_Man_t * p )
470{
471 Abc_Cex_t * pCex;
472 Aig_Obj_t * pObj;
473 DdNode * bState = NULL, * bImage, * bOneCube, * bTemp, * bRing;
474 int i, v, RetValue, nPiOffset;
475 char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->ddR) );
476 assert( Vec_PtrSize(p->vRings) > 0 );
477
478 p->dd->TimeStop = 0;
479 p->ddR->TimeStop = 0;
480
481/*
482 Saig_ManForEachLo( p->pAig, pObj, i )
483 printf( "%d ", pObj->Id );
484 printf( "\n" );
485 Saig_ManForEachLi( p->pAig, pObj, i )
486 printf( "%d(%d) ", pObj->Id, Aig_ObjFaninId0(pObj) );
487 printf( "\n" );
488*/
489 // allocate room for the counter-example
490 pCex = Abc_CexAlloc( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
491 pCex->iFrame = Vec_PtrSize(p->vRings) - 1;
492 pCex->iPo = -1;
493
494 // get the last cube
495 bOneCube = Cudd_bddIntersect( p->ddR, (DdNode *)Vec_PtrEntryLast(p->vRings), p->ddR->bFunc ); Cudd_Ref( bOneCube );
496 RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
497 Cudd_RecursiveDeref( p->ddR, bOneCube );
498 assert( RetValue );
499
500 // write PIs of counter-example
501 nPiOffset = Saig_ManRegNum(p->pAig) + Saig_ManPiNum(p->pAig) * (Vec_PtrSize(p->vRings) - 1);
502 Saig_ManForEachPi( p->pAig, pObj, i )
503 if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
504 Abc_InfoSetBit( pCex->pData, nPiOffset + i );
505
506 // write state in terms of NS variables
507 if ( Vec_PtrSize(p->vRings) > 1 )
508 {
509 bState = Llb_CoreComputeCube( p->dd, p->vGlo2Ns, 1, pValues ); Cudd_Ref( bState );
510 }
511 // perform backward analysis
512 Vec_PtrForEachEntryReverse( DdNode *, p->vRings, bRing, v )
513 {
514 if ( v == Vec_PtrSize(p->vRings) - 1 )
515 continue;
516//Extra_bddPrintSupport( p->dd, bState ); printf( "\n" );
517//Extra_bddPrintSupport( p->dd, bRing ); printf( "\n" );
518 // compute the next states
519 bImage = Llb_ManComputeImage( p, bState, 1 );
520 assert( bImage != NULL );
521 Cudd_Ref( bImage );
522 Cudd_RecursiveDeref( p->dd, bState );
523//Extra_bddPrintSupport( p->dd, bImage ); printf( "\n" );
524
525 // move reached states into ring manager
526 bImage = Extra_TransferPermute( p->dd, p->ddR, bTemp = bImage, Vec_IntArray(p->vCs2Glo) ); Cudd_Ref( bImage );
527 Cudd_RecursiveDeref( p->dd, bTemp );
528//Extra_bddPrintSupport( p->ddR, bImage ); printf( "\n" );
529
530 // intersect with the previous set
531 bOneCube = Cudd_bddIntersect( p->ddR, bImage, bRing ); Cudd_Ref( bOneCube );
532 Cudd_RecursiveDeref( p->ddR, bImage );
533
534 // find any assignment of the BDD
535 RetValue = Cudd_bddPickOneCube( p->ddR, bOneCube, pValues );
536 Cudd_RecursiveDeref( p->ddR, bOneCube );
537 assert( RetValue );
538/*
539 for ( i = 0; i < p->ddR->size; i++ )
540 printf( "%d ", pValues[i] );
541 printf( "\n" );
542*/
543 // write PIs of counter-example
544 nPiOffset -= Saig_ManPiNum(p->pAig);
545 Saig_ManForEachPi( p->pAig, pObj, i )
546 if ( pValues[Saig_ManRegNum(p->pAig)+i] == 1 )
547 Abc_InfoSetBit( pCex->pData, nPiOffset + i );
548
549 // check that we get the init state
550 if ( v == 0 )
551 {
552 Saig_ManForEachLo( p->pAig, pObj, i )
553 assert( pValues[i] == 0 );
554 break;
555 }
556
557 // write state in terms of NS variables
558 bState = Llb_CoreComputeCube( p->dd, p->vGlo2Ns, 1, pValues ); Cudd_Ref( bState );
559 }
560 assert( nPiOffset == Saig_ManRegNum(p->pAig) );
561 // update the output number
562//Abc_CexPrint( pCex );
563 RetValue = Saig_ManFindFailedPoCex( p->pAigGlo, pCex );
564 assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pAigGlo) ); // invalid CEX!!!
565 pCex->iPo = RetValue;
566 // cleanup
567 ABC_FREE( pValues );
568 return pCex;
569}
570
582int Llb_ManReachability( Llb_Man_t * p, Vec_Int_t * vHints, DdManager ** pddGlo )
583{
584 int * pNs2Glo = Vec_IntArray( p->vNs2Glo );
585 int * pCs2Glo = Vec_IntArray( p->vCs2Glo );
586 int * pGlo2Cs = Vec_IntArray( p->vGlo2Cs );
587 DdNode * bCurrent, * bReached, * bNext, * bTemp, * bCube;
588 DdNode * bConstrCs, * bConstrNs;
589 abctime clk2, clk = Abc_Clock();
590 int nIters, nBddSize = 0;
591// int nThreshold = 10000;
592
593 // compute time to stop
594 p->pPars->TimeTarget = p->pPars->TimeLimit ? p->pPars->TimeLimit * CLOCKS_PER_SEC + Abc_Clock(): 0;
595
596 // define variable limits
597 Llb_ManPrepareVarLimits( p );
598
599 // start the managers
600 assert( p->dd == NULL );
601 assert( p->ddG == NULL );
602 assert( p->ddR == NULL );
603 p->dd = Cudd_Init( Vec_IntSize(p->vVar2Obj), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
604 p->ddR = Cudd_Init( Aig_ManCiNum(p->pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
605 if ( pddGlo && *pddGlo )
606 p->ddG = *pddGlo, *pddGlo = NULL;
607 else
608 p->ddG = Cudd_Init( Aig_ManRegNum(p->pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
609
610 if ( p->pPars->fReorder )
611 {
612 Cudd_AutodynEnable( p->dd, CUDD_REORDER_SYMM_SIFT );
613 Cudd_AutodynEnable( p->ddG, CUDD_REORDER_SYMM_SIFT );
614 Cudd_AutodynEnable( p->ddR, CUDD_REORDER_SYMM_SIFT );
615 }
616 else
617 {
618 Cudd_AutodynDisable( p->dd );
619 Cudd_AutodynDisable( p->ddG );
620 Cudd_AutodynDisable( p->ddR );
621 }
622
623 // set the stop time parameter
624 p->dd->TimeStop = p->pPars->TimeTarget;
625 p->ddG->TimeStop = p->pPars->TimeTarget;
626 p->ddR->TimeStop = p->pPars->TimeTarget;
627
628 // create bad state in the ring manager
629 p->ddR->bFunc = Llb_BddComputeBad( p->pAigGlo, p->ddR, p->pPars->TimeTarget );
630 if ( p->ddR->bFunc == NULL )
631 {
632 if ( !p->pPars->fSilent )
633 printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
634 p->pPars->iFrame = -1;
635 return -1;
636 }
637 Cudd_Ref( p->ddR->bFunc );
638
639 // derive constraints
640 bConstrCs = Llb_ManCreateConstraints( p, vHints, 0 ); Cudd_Ref( bConstrCs );
641 bConstrNs = Llb_ManCreateConstraints( p, vHints, 1 ); Cudd_Ref( bConstrNs );
642//Extra_bddPrint( p->dd, bConstrCs ); printf( "\n" );
643//Extra_bddPrint( p->dd, bConstrNs ); printf( "\n" );
644
645 // perform reachability analysis
646 // compute the starting set of states
647 if ( p->ddG->bFunc )
648 {
649 bReached = p->ddG->bFunc; p->ddG->bFunc = NULL;
650 bCurrent = Extra_TransferPermute( p->ddG, p->dd, bReached, pGlo2Cs ); Cudd_Ref( bCurrent );
651 }
652 else
653 {
654 bReached = Llb_ManComputeInitState( p, p->ddG ); Cudd_Ref( bReached );
655 bCurrent = Llb_ManComputeInitState( p, p->dd ); Cudd_Ref( bCurrent );
656 }
657//Extra_bddPrintSupport( p->ddG, bReached ); printf( "\n" );
658//Extra_bddPrintSupport( p->dd, bCurrent ); printf( "\n" );
659
660//Extra_bddPrintSupport( p->dd, bCurrent ); printf( "\n" );
661 for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ )
662 {
663 clk2 = Abc_Clock();
664 // check the runtime limit
665 if ( p->pPars->TimeLimit && Abc_Clock() > p->pPars->TimeTarget )
666 {
667 if ( !p->pPars->fSilent )
668 printf( "Reached timeout during image computation (%d seconds).\n", p->pPars->TimeLimit );
669 p->pPars->iFrame = nIters - 1;
670 Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
671 Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
672 Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
673 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
674 return -1;
675 }
676
677 // save the onion ring
678 bTemp = Extra_TransferPermute( p->dd, p->ddR, bCurrent, pCs2Glo );
679 if ( bTemp == NULL )
680 {
681 if ( !p->pPars->fSilent )
682 printf( "Reached timeout (%d seconds) during ring transfer.\n", p->pPars->TimeLimit );
683 p->pPars->iFrame = nIters - 1;
684 Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
685 Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
686 Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
687 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
688 return -1;
689 }
690 Cudd_Ref( bTemp );
691 Vec_PtrPush( p->vRings, bTemp );
692
693 // check it for bad states
694 if ( !p->pPars->fSkipOutCheck && !Cudd_bddLeq( p->ddR, bTemp, Cudd_Not(p->ddR->bFunc) ) )
695 {
696 assert( p->pAigGlo->pSeqModel == NULL );
697 if ( !p->pPars->fBackward )
698 p->pAigGlo->pSeqModel = Llb_ManReachDeriveCex( p );
699 if ( !p->pPars->fSilent )
700 {
701 if ( !p->pPars->fBackward )
702 Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", p->pAigGlo->pSeqModel->iPo, p->pAigGlo->pName, p->pAigGlo->pName, nIters );
703 else
704 Abc_Print( 1, "Output ??? of miter \"%s\" was asserted in frame %d (counter-example is not produced). ", p->pAigGlo->pName, nIters );
705 Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
706 }
707 p->pPars->iFrame = nIters - 1;
708 Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
709 Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
710 Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
711 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
712 return 0;
713 }
714
715 // restrict reachable states using constraints
716 if ( vHints )
717 {
718 bCurrent = Cudd_bddAnd( p->dd, bTemp = bCurrent, bConstrCs ); Cudd_Ref( bCurrent );
719 Cudd_RecursiveDeref( p->dd, bTemp );
720 }
721
722 // quantify variables appearing only in the init state
723 bCube = Llb_ManConstructQuantCubeIntern( p, (Llb_Grp_t *)Vec_PtrEntry(p->vGroups,0), 0, 0 ); Cudd_Ref( bCube );
724 bCurrent = Cudd_bddExistAbstract( p->dd, bTemp = bCurrent, bCube ); Cudd_Ref( bCurrent );
725 Cudd_RecursiveDeref( p->dd, bTemp );
726 Cudd_RecursiveDeref( p->dd, bCube );
727
728 // compute the next states
729 bNext = Llb_ManComputeImage( p, bCurrent, 0 );
730 if ( bNext == NULL )
731 {
732 if ( !p->pPars->fSilent )
733 printf( "Reached timeout (%d seconds) during image computation.\n", p->pPars->TimeLimit );
734 p->pPars->iFrame = nIters - 1;
735 Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
736 Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
737 Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
738 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
739 return -1;
740 }
741 Cudd_Ref( bNext );
742 Cudd_RecursiveDeref( p->dd, bCurrent ); bCurrent = NULL;
743
744 // restrict reachable states using constraints
745 if ( vHints )
746 {
747 bNext = Cudd_bddAnd( p->dd, bTemp = bNext, bConstrNs ); Cudd_Ref( bNext );
748 Cudd_RecursiveDeref( p->dd, bTemp );
749 }
750//Extra_bddPrintSupport( p->dd, bNext ); printf( "\n" );
751
752 // remap these states into the current state vars
753// bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pNs2Glo ); Cudd_Ref( bNext );
754// Cudd_RecursiveDeref( p->dd, bTemp );
755// bNext = Extra_TransferPermuteTime( p->dd, p->ddG, bTemp = bNext, pNs2Glo, p->pPars->TimeTarget );
756 bNext = Extra_TransferPermute( p->dd, p->ddG, bTemp = bNext, pNs2Glo );
757 if ( bNext == NULL )
758 {
759 if ( !p->pPars->fSilent )
760 printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n", p->pPars->TimeLimit );
761 p->pPars->iFrame = nIters - 1;
762 Cudd_RecursiveDeref( p->dd, bTemp );
763 Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
764 Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
765 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
766 return -1;
767 }
768 Cudd_Ref( bNext );
769 Cudd_RecursiveDeref( p->dd, bTemp );
770
771
772 // check if there are any new states
773 if ( Cudd_bddLeq( p->ddG, bNext, bReached ) ) // implication = no new states
774 {
775 Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL;
776 break;
777 }
778
779 // check the BDD size
780 nBddSize = Cudd_DagSize(bNext);
781 if ( nBddSize > p->pPars->nBddMax )
782 {
783 Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL;
784 break;
785 }
786
787 // get the new states
788 bCurrent = Cudd_bddAnd( p->ddG, bNext, Cudd_Not(bReached) );
789 if ( bCurrent == NULL )
790 {
791 Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL;
792 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
793 break;
794 }
795 Cudd_Ref( bCurrent );
796 // minimize the new states with the reached states
797// bCurrent = Cudd_bddConstrain( p->ddG, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
798// bCurrent = Cudd_bddRestrict( p->ddG, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
799// Cudd_RecursiveDeref( p->ddG, bTemp );
800//printf( "Initial BDD =%7d. Constrained BDD =%7d.\n", Cudd_DagSize(bTemp), Cudd_DagSize(bCurrent) );
801
802 // remap these states into the current state vars
803// bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs ); Cudd_Ref( bCurrent );
804// Cudd_RecursiveDeref( p->ddG, bTemp );
805// bCurrent = Extra_TransferPermuteTime( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs, p->pPars->TimeTarget );
806 bCurrent = Extra_TransferPermute( p->ddG, p->dd, bTemp = bCurrent, pGlo2Cs );
807 if ( bCurrent == NULL )
808 {
809 if ( !p->pPars->fSilent )
810 printf( "Reached timeout (%d seconds) during image computation in transfer 2.\n", p->pPars->TimeLimit );
811 p->pPars->iFrame = nIters - 1;
812 Cudd_RecursiveDeref( p->ddG, bTemp );
813 Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
814 Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
815 Cudd_RecursiveDeref( p->ddG, bReached ); bReached = NULL;
816 return -1;
817 }
818 Cudd_Ref( bCurrent );
819 Cudd_RecursiveDeref( p->ddG, bTemp );
820
821
822 // add to the reached states
823 bReached = Cudd_bddOr( p->ddG, bTemp = bReached, bNext );
824 if ( bReached == NULL )
825 {
826 Cudd_RecursiveDeref( p->ddG, bTemp ); bTemp = NULL;
827 Cudd_RecursiveDeref( p->ddG, bNext ); bNext = NULL;
828 break;
829 }
830 Cudd_Ref( bReached );
831 Cudd_RecursiveDeref( p->ddG, bTemp );
832 Cudd_RecursiveDeref( p->ddG, bNext );
833 bNext = NULL;
834
835 if ( p->pPars->fVerbose )
836 {
837 fprintf( stdout, "F =%5d : ", nIters );
838 fprintf( stdout, "Im =%6d ", nBddSize );
839 fprintf( stdout, "(%4d %3d) ", Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) );
840 fprintf( stdout, "Rea =%6d ", Cudd_DagSize(bReached) );
841 fprintf( stdout, "(%4d%4d) ", Cudd_ReadReorderings(p->ddG), Cudd_ReadGarbageCollections(p->ddG) );
842 Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
843 }
844/*
845 if ( p->pPars->fVerbose )
846 {
847 double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) );
848// Extra_bddPrint( p->ddG, bReached );printf( "\n" );
849 fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
850 fflush( stdout );
851 }
852*/
853 }
854 Cudd_RecursiveDeref( p->dd, bConstrCs ); bConstrCs = NULL;
855 Cudd_RecursiveDeref( p->dd, bConstrNs ); bConstrNs = NULL;
856 if ( bReached == NULL )
857 {
858 p->pPars->iFrame = nIters - 1;
859 return 0; // reachable
860 }
861// assert( bCurrent == NULL );
862 if ( bCurrent )
863 Cudd_RecursiveDeref( p->dd, bCurrent );
864 // report the stats
865 if ( p->pPars->fVerbose )
866 {
867 double nMints = Cudd_CountMinterm(p->ddG, bReached, Saig_ManRegNum(p->pAig) );
868 if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax )
869 fprintf( stdout, "Reachability analysis is stopped after %d frames.\n", nIters );
870 else
871 fprintf( stdout, "Reachability analysis completed after %d frames.\n", nIters );
872 fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
873 fflush( stdout );
874 }
875 if ( nIters >= p->pPars->nIterMax || nBddSize > p->pPars->nBddMax )
876 {
877 if ( !p->pPars->fSilent )
878 printf( "Verified only for states reachable in %d frames. ", nIters );
879 p->pPars->iFrame = p->pPars->nIterMax;
880 Cudd_RecursiveDeref( p->ddG, bReached );
881 return -1; // undecided
882 }
883 if ( pddGlo )
884 {
885 assert( p->ddG->bFunc == NULL );
886 p->ddG->bFunc = bReached; bReached = NULL;
887 assert( *pddGlo == NULL );
888 *pddGlo = p->ddG; p->ddG = NULL;
889 }
890 else
891 Cudd_RecursiveDeref( p->ddG, bReached );
892 if ( !p->pPars->fSilent )
893 printf( "The miter is proved unreachable after %d iterations. ", nIters );
894 p->pPars->iFrame = nIters - 1;
895 return 1; // unreachable
896}
897
901
902
903ABC_NAMESPACE_IMPL_END
904
abctime
ABC_INT64_T abctime
Definition abc_global.h:332
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition abc_global.h:264
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
Aig_ManForEachCi
#define Aig_ManForEachCi(p, pObj, i)
ITERATORS ///.
Definition aig.h:393
Aig_Obj_t
struct Aig_Obj_t_ Aig_Obj_t
Definition aig.h:51
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition aig.h:50
Aig_ManDfsNodes
Vec_Ptr_t * Aig_ManDfsNodes(Aig_Man_t *p, Aig_Obj_t **ppNodes, int nNodes)
Definition aigDfs.c:347
Aig_ManCleanData
void Aig_ManCleanData(Aig_Man_t *p)
Definition aigUtil.c:205
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
p
Cube * p
Definition exorList.c:222
Extra_TransferPermute
DdNode * Extra_TransferPermute(DdManager *ddSource, DdManager *ddDestination, DdNode *f, int *Permute)
Definition extraBddMisc.c:87
Llb_ManPrepareVarLimits
void Llb_ManPrepareVarLimits(Llb_Man_t *p)
Definition llb1Man.c:88
Llb_ManConstructQuantCubeFwd
DdNode * Llb_ManConstructQuantCubeFwd(Llb_Man_t *p, Llb_Grp_t *pGroup, int iGrpPlace)
Definition llb1Reach.c:205
Llb_ManReachDeriveCex
Abc_Cex_t * Llb_ManReachDeriveCex(Llb_Man_t *p)
Definition llb1Reach.c:469
Llb_ManComputeImage
DdNode * Llb_ManComputeImage(Llb_Man_t *p, DdNode *bInit, int fBackward)
Definition llb1Reach.c:328
Llb_ManConstructQuantCubeBwd
DdNode * Llb_ManConstructQuantCubeBwd(Llb_Man_t *p, Llb_Grp_t *pGroup, int iGrpPlace)
Definition llb1Reach.c:249
Llb_ManCreateConstraints
DdNode * Llb_ManCreateConstraints(Llb_Man_t *p, Vec_Int_t *vHints, int fUseNsVars)
Definition llb1Reach.c:412
Llb_ManConstructOutBdd
ABC_NAMESPACE_IMPL_START DdNode * Llb_ManConstructOutBdd(Aig_Man_t *pAig, Aig_Obj_t *pNode, DdManager *dd)
DECLARATIONS ///.
Definition llb1Reach.c:45
Llb_ManReachability
int Llb_ManReachability(Llb_Man_t *p, Vec_Int_t *vHints, DdManager **pddGlo)
Definition llb1Reach.c:582
Llb_ManComputeInitState
DdNode * Llb_ManComputeInitState(Llb_Man_t *p, DdManager *dd)
Definition llb1Reach.c:297
Llb_ManConstructGroupBdd
DdNode * Llb_ManConstructGroupBdd(Llb_Man_t *p, Llb_Grp_t *pGroup)
Definition llb1Reach.c:91
Llb_ManConstructQuantCubeIntern
DdNode * Llb_ManConstructQuantCubeIntern(Llb_Man_t *p, Llb_Grp_t *pGroup, int iGrpPlace, int fBackward)
Definition llb1Reach.c:155
Llb_BddComputeBad
ABC_NAMESPACE_IMPL_START DdNode * Llb_BddComputeBad(Aig_Man_t *pInit, DdManager *dd, abctime TimeOut)
DECLARATIONS ///.
Definition llb2Bad.c:45
Llb_CoreComputeCube
DdNode * Llb_CoreComputeCube(DdManager *dd, Vec_Int_t *vVars, int fUseVarIndex, char *pValues)
FUNCTION DEFINITIONS ///.
Definition llb2Core.c:68
Llb_Man_t
typedefABC_NAMESPACE_HEADER_START struct Llb_Man_t_ Llb_Man_t
INCLUDES ///.
Definition llbInt.h:47
Llb_Grp_t
struct Llb_Grp_t_ Llb_Grp_t
Definition llbInt.h:49
Saig_ManFindFailedPoCex
int Saig_ManFindFailedPoCex(Aig_Man_t *pAig, Abc_Cex_t *p)
Definition saigDup.c:436
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition saig.h:96
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition saig.h:91
Aig_Obj_t_::pData
void * pData
Definition aig.h:87
Llb_Grp_t_::vNodes
Vec_Ptr_t * vNodes
Definition llbInt.h:100
Llb_Grp_t_::vIns
Vec_Ptr_t * vIns
Definition llbInt.h:98
Llb_Grp_t_::vOuts
Vec_Ptr_t * vOuts
Definition llbInt.h:99
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition utilCex.c:51
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition utilCex.h:39
assert
#define assert(ex)
Definition util_old.h:213
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54
Vec_PtrForEachEntryReverse
#define Vec_PtrForEachEntryReverse(Type, vVec, pEntry, i)
Definition vecPtr.h:63
Vec_PtrForEachEntryStop
#define Vec_PtrForEachEntryStop(Type, vVec, pEntry, i, Stop)
Definition vecPtr.h:59
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition vecPtr.h:42
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition vecPtr.h:55