abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
bbrReach.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [bbrReach.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [BDD-based reachability analysis.]
8 
9  Synopsis [Procedures to perform reachability analysis.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: bbrReach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include "bbr.h"
22 
23 ABC_NAMESPACE_IMPL_START
24 
25 
26 ////////////////////////////////////////////////////////////////////////
27 /// DECLARATIONS ///
28 ////////////////////////////////////////////////////////////////////////
29 
30 extern Abc_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd,
31  DdNode ** pbParts, Vec_Ptr_t * vOnionRings, DdNode * bCubeFirst,
32  int iOutput, int fVerbose, int fSilent );
33 
34 ////////////////////////////////////////////////////////////////////////
35 /// FUNCTION DEFINITIONS ///
36 ////////////////////////////////////////////////////////////////////////
37 
38 /**Function*************************************************************
39 
40  Synopsis [This procedure sets default resynthesis parameters.]
41 
42  Description []
43 
44  SideEffects []
45 
46  SeeAlso []
47 
48 ***********************************************************************/
49 void Bbr_ManSetDefaultParams( Saig_ParBbr_t * p )
50 {
51  memset( p, 0, sizeof(Saig_ParBbr_t) );
52  p->TimeLimit = 0;
53  p->nBddMax = 50000;
54  p->nIterMax = 1000;
55  p->fPartition = 1;
56  p->fReorder = 1;
57  p->fReorderImage = 1;
58  p->fVerbose = 0;
59  p->fSilent = 0;
60  p->iFrame = -1;
61 }
62 
63 /**Function********************************************************************
64 
65  Synopsis [Performs the reordering-sensitive step of Extra_bddMove().]
66 
67  Description []
68 
69  SideEffects []
70 
71  SeeAlso []
72 
73 ******************************************************************************/
74 DdNode * Bbr_bddComputeRangeCube( DdManager * dd, int iStart, int iStop )
75 {
76  DdNode * bTemp, * bProd;
77  int i;
78  assert( iStart <= iStop );
79  assert( iStart >= 0 && iStart <= dd->size );
80  assert( iStop >= 0 && iStop <= dd->size );
81  bProd = (dd)->one; Cudd_Ref( bProd );
82  for ( i = iStart; i < iStop; i++ )
83  {
84  bProd = Cudd_bddAnd( dd, bTemp = bProd, dd->vars[i] ); Cudd_Ref( bProd );
85  Cudd_RecursiveDeref( dd, bTemp );
86  }
87  Cudd_Deref( bProd );
88  return bProd;
89 }
90 
91 /**Function*************************************************************
92 
93  Synopsis []
94 
95  Description []
96 
97  SideEffects []
98 
99  SeeAlso []
100 
101 ***********************************************************************/
102 void Bbr_StopManager( DdManager * dd )
103 {
104  int RetValue;
105  // check for remaining references in the package
106  RetValue = Cudd_CheckZeroRef( dd );
107  if ( RetValue > 0 )
108  printf( "\nThe number of referenced nodes = %d\n\n", RetValue );
109 // Cudd_PrintInfo( dd, stdout );
110  Cudd_Quit( dd );
111 }
112 
113 /**Function*************************************************************
114 
115  Synopsis [Computes the initial state and sets up the variable map.]
116 
117  Description []
118 
119  SideEffects []
120 
121  SeeAlso []
122 
123 ***********************************************************************/
124 DdNode * Aig_ManInitStateVarMap( DdManager * dd, Aig_Man_t * p, int fVerbose )
125 {
126  DdNode ** pbVarsX, ** pbVarsY;
127  DdNode * bTemp, * bProd;
128  Aig_Obj_t * pLatch;
129  int i;
130 
131  // set the variable mapping for Cudd_bddVarMap()
132  pbVarsX = ABC_ALLOC( DdNode *, dd->size );
133  pbVarsY = ABC_ALLOC( DdNode *, dd->size );
134  bProd = (dd)->one; Cudd_Ref( bProd );
135  Saig_ManForEachLo( p, pLatch, i )
136  {
137  pbVarsX[i] = dd->vars[ Saig_ManPiNum(p) + i ];
138  pbVarsY[i] = dd->vars[ Saig_ManCiNum(p) + i ];
139  // get the initial value of the latch
140  bProd = Cudd_bddAnd( dd, bTemp = bProd, Cudd_Not(pbVarsX[i]) ); Cudd_Ref( bProd );
141  Cudd_RecursiveDeref( dd, bTemp );
142  }
143  Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Saig_ManRegNum(p) );
144  ABC_FREE( pbVarsX );
145  ABC_FREE( pbVarsY );
146 
147  Cudd_Deref( bProd );
148  return bProd;
149 }
150 
151 /**Function*************************************************************
152 
153  Synopsis [Collects the array of output BDDs.]
154 
155  Description []
156 
157  SideEffects []
158 
159  SeeAlso []
160 
161 ***********************************************************************/
162 DdNode ** Aig_ManCreateOutputs( DdManager * dd, Aig_Man_t * p )
163 {
164  DdNode ** pbOutputs;
165  Aig_Obj_t * pNode;
166  int i;
167  // compute the transition relation
168  pbOutputs = ABC_ALLOC( DdNode *, Saig_ManPoNum(p) );
169  Saig_ManForEachPo( p, pNode, i )
170  {
171  pbOutputs[i] = Aig_ObjGlobalBdd(pNode); Cudd_Ref( pbOutputs[i] );
172  }
173  return pbOutputs;
174 }
175 
176 /**Function*************************************************************
177 
178  Synopsis [Collects the array of partition BDDs.]
179 
180  Description []
181 
182  SideEffects []
183 
184  SeeAlso []
185 
186 ***********************************************************************/
187 DdNode ** Aig_ManCreatePartitions( DdManager * dd, Aig_Man_t * p, int fReorder, int fVerbose )
188 {
189  DdNode ** pbParts;
190  DdNode * bVar;
191  Aig_Obj_t * pNode;
192  int i;
193 
194  // extand the BDD manager to represent NS variables
195  assert( dd->size == Saig_ManCiNum(p) );
196  Cudd_bddIthVar( dd, Saig_ManCiNum(p) + Saig_ManRegNum(p) - 1 );
197 
198  // enable reordering
199  if ( fReorder )
200  Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
201  else
202  Cudd_AutodynDisable( dd );
203 
204  // compute the transition relation
205  pbParts = ABC_ALLOC( DdNode *, Saig_ManRegNum(p) );
206  Saig_ManForEachLi( p, pNode, i )
207  {
208  bVar = Cudd_bddIthVar( dd, Saig_ManCiNum(p) + i );
209  pbParts[i] = Cudd_bddXnor( dd, bVar, Aig_ObjGlobalBdd(pNode) ); Cudd_Ref( pbParts[i] );
210  }
211  // free global BDDs
212  Aig_ManFreeGlobalBdds( p, dd );
213 
214  // reorder and disable reordering
215  if ( fReorder )
216  {
217  if ( fVerbose )
218  fprintf( stdout, "BDD nodes in the partitions before reordering %d.\n", Cudd_SharingSize(pbParts,Saig_ManRegNum(p)) );
219  Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
220  Cudd_AutodynDisable( dd );
221  if ( fVerbose )
222  fprintf( stdout, "BDD nodes in the partitions after reordering %d.\n", Cudd_SharingSize(pbParts,Saig_ManRegNum(p)) );
223  }
224  return pbParts;
225 }
226 
227 /**Function*************************************************************
228 
229  Synopsis [Computes the set of unreachable states.]
230 
231  Description []
232 
233  SideEffects []
234 
235  SeeAlso []
236 
237 ***********************************************************************/
238 int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, DdNode * bInitial, DdNode ** pbOutputs, Saig_ParBbr_t * pPars, int fCheckOutputs )
239 {
240  int fInternalReorder = 0;
241  Bbr_ImageTree_t * pTree = NULL; // Suppress "might be used uninitialized"
242  Bbr_ImageTree2_t * pTree2 = NULL; // Supprses "might be used uninitialized"
243  DdNode * bReached, * bCubeCs;
244  DdNode * bCurrent;
245  DdNode * bNext = NULL; // Suppress "might be used uninitialized"
246  DdNode * bTemp;
247  Cudd_ReorderingType method;
248  int i, nIters, nBddSize = 0, status;
249  int nThreshold = 10000;
250  abctime clk = Abc_Clock();
251  Vec_Ptr_t * vOnionRings;
252  int fixedPoint = 0;
253 
254  status = Cudd_ReorderingStatus( dd, &method );
255  if ( status )
256  Cudd_AutodynDisable( dd );
257 
258  // start the image computation
259  bCubeCs = Bbr_bddComputeRangeCube( dd, Saig_ManPiNum(p), Saig_ManCiNum(p) ); Cudd_Ref( bCubeCs );
260  if ( pPars->fPartition )
261  pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), pPars->nBddMax, pPars->fVerbose );
262  else
263  pTree2 = Bbr_bddImageStart2( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), pPars->fVerbose );
264  Cudd_RecursiveDeref( dd, bCubeCs );
265  if ( pTree == NULL )
266  {
267  if ( !pPars->fSilent )
268  printf( "BDDs blew up during qualitification scheduling. " );
269  return -1;
270  }
271 
272  if ( status )
273  Cudd_AutodynEnable( dd, method );
274 
275  // start the onion rings
276  vOnionRings = Vec_PtrAlloc( 1000 );
277 
278  // perform reachability analysis
279  bCurrent = bInitial; Cudd_Ref( bCurrent );
280  bReached = bInitial; Cudd_Ref( bReached );
281  Vec_PtrPush( vOnionRings, bCurrent ); Cudd_Ref( bCurrent );
282  for ( nIters = 0; nIters < pPars->nIterMax; nIters++ )
283  {
284  // check the runtime limit
285  if ( pPars->TimeLimit && pPars->TimeLimit <= (Abc_Clock()-clk)/CLOCKS_PER_SEC )
286  {
287  printf( "Reached timeout after image computation (%d seconds).\n", pPars->TimeLimit );
288  Vec_PtrFree( vOnionRings );
289  // undo the image tree
290  if ( pPars->fPartition )
291  Bbr_bddImageTreeDelete( pTree );
292  else
293  Bbr_bddImageTreeDelete2( pTree2 );
294  pPars->iFrame = nIters - 1;
295  return -1;
296  }
297 
298  // compute the next states
299  if ( pPars->fPartition )
300  bNext = Bbr_bddImageCompute( pTree, bCurrent );
301  else
302  bNext = Bbr_bddImageCompute2( pTree2, bCurrent );
303  if ( bNext == NULL )
304  {
305  if ( !pPars->fSilent )
306  printf( "BDDs blew up during image computation. " );
307  if ( pPars->fPartition )
308  Bbr_bddImageTreeDelete( pTree );
309  else
310  Bbr_bddImageTreeDelete2( pTree2 );
311  Vec_PtrFree( vOnionRings );
312  pPars->iFrame = nIters - 1;
313  return -1;
314  }
315  Cudd_Ref( bNext );
316  Cudd_RecursiveDeref( dd, bCurrent );
317 
318  // remap these states into the current state vars
319  bNext = Cudd_bddVarMap( dd, bTemp = bNext ); Cudd_Ref( bNext );
320  Cudd_RecursiveDeref( dd, bTemp );
321  // check if there are any new states
322  if ( Cudd_bddLeq( dd, bNext, bReached ) ) {
323  fixedPoint = 1;
324  break;
325  }
326  // check the BDD size
327  nBddSize = Cudd_DagSize(bNext);
328  if ( nBddSize > pPars->nBddMax )
329  break;
330  // check the result
331  for ( i = 0; i < Saig_ManPoNum(p); i++ )
332  {
333  if ( fCheckOutputs && !Cudd_bddLeq( dd, bNext, Cudd_Not(pbOutputs[i]) ) )
334  {
335  DdNode * bIntersect;
336  bIntersect = Cudd_bddIntersect( dd, bNext, pbOutputs[i] ); Cudd_Ref( bIntersect );
337  assert( p->pSeqModel == NULL );
338  p->pSeqModel = Aig_ManVerifyUsingBddsCountExample( p, dd, pbParts,
339  vOnionRings, bIntersect, i, pPars->fVerbose, pPars->fSilent );
340  Cudd_RecursiveDeref( dd, bIntersect );
341  if ( !pPars->fSilent )
342  Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", i, p->pName, Vec_PtrSize(vOnionRings) );
343  Cudd_RecursiveDeref( dd, bReached );
344  bReached = NULL;
345  pPars->iFrame = nIters;
346  break;
347  }
348  }
349  if ( i < Saig_ManPoNum(p) )
350  break;
351  // get the new states
352  bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
353  Vec_PtrPush( vOnionRings, bCurrent ); Cudd_Ref( bCurrent );
354  // minimize the new states with the reached states
355 // bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
356 // Cudd_RecursiveDeref( dd, bTemp );
357  // add to the reached states
358  bReached = Cudd_bddOr( dd, bTemp = bReached, bNext ); Cudd_Ref( bReached );
359  Cudd_RecursiveDeref( dd, bTemp );
360  Cudd_RecursiveDeref( dd, bNext );
361  if ( pPars->fVerbose )
362  fprintf( stdout, "Frame = %3d. BDD = %5d. ", nIters, nBddSize );
363  if ( fInternalReorder && pPars->fReorder && nBddSize > nThreshold )
364  {
365  if ( pPars->fVerbose )
366  fprintf( stdout, "Reordering... Before = %5d. ", Cudd_DagSize(bReached) );
367  Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
368  Cudd_AutodynDisable( dd );
369  if ( pPars->fVerbose )
370  fprintf( stdout, "After = %5d.\r", Cudd_DagSize(bReached) );
371  nThreshold *= 2;
372  }
373  if ( pPars->fVerbose )
374 // fprintf( stdout, "\r" );
375  fprintf( stdout, "\n" );
376 
377  if ( pPars->fVerbose )
378  {
379  double nMints = Cudd_CountMinterm(dd, bReached, Saig_ManRegNum(p) );
380 // Extra_bddPrint( dd, bReached );printf( "\n" );
381  fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p)) );
382  fflush( stdout );
383  }
384 
385  }
386  Cudd_RecursiveDeref( dd, bNext );
387  // free the onion rings
388  Vec_PtrForEachEntry( DdNode *, vOnionRings, bTemp, i )
389  Cudd_RecursiveDeref( dd, bTemp );
390  Vec_PtrFree( vOnionRings );
391  // undo the image tree
392  if ( pPars->fPartition )
393  Bbr_bddImageTreeDelete( pTree );
394  else
395  Bbr_bddImageTreeDelete2( pTree2 );
396  if ( bReached == NULL )
397  return 0; // proved reachable
398  // report the stats
399  if ( pPars->fVerbose )
400  {
401  double nMints = Cudd_CountMinterm(dd, bReached, Saig_ManRegNum(p) );
402  if ( nIters > pPars->nIterMax || nBddSize > pPars->nBddMax )
403  fprintf( stdout, "Reachability analysis is stopped after %d frames.\n", nIters );
404  else
405  fprintf( stdout, "Reachability analysis completed after %d frames.\n", nIters );
406  fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p)) );
407  fflush( stdout );
408  }
409 //ABC_PRB( dd, bReached );
410  Cudd_RecursiveDeref( dd, bReached );
411  // SPG
412  //
413  if ( fixedPoint ) {
414  if ( !pPars->fSilent ) {
415  printf( "The miter is proved unreachable after %d iterations. ", nIters );
416  }
417  pPars->iFrame = nIters - 1;
418  return 1;
419  }
420  assert(nIters >= pPars->nIterMax || nBddSize >= pPars->nBddMax);
421  if ( !pPars->fSilent )
422  printf( "Verified only for states reachable in %d frames. ", nIters );
423  pPars->iFrame = nIters - 1;
424  return -1; // undecided
425 }
426 
427 /**Function*************************************************************
428 
429  Synopsis [Performs reachability to see if any PO can be asserted.]
430 
431  Description []
432 
433  SideEffects []
434 
435  SeeAlso []
436 
437 ***********************************************************************/
438 int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, Saig_ParBbr_t * pPars )
439 {
440  int fCheckOutputs = !pPars->fSkipOutCheck;
441  DdManager * dd;
442  DdNode ** pbParts, ** pbOutputs;
443  DdNode * bInitial, * bTemp;
444  int RetValue, i;
445  abctime clk = Abc_Clock();
446  Vec_Ptr_t * vOnionRings;
447 
448  assert( Saig_ManRegNum(p) > 0 );
449 
450  // compute the global BDDs of the latches
451  dd = Aig_ManComputeGlobalBdds( p, pPars->nBddMax, 1, pPars->fReorder, pPars->fVerbose );
452  if ( dd == NULL )
453  {
454  if ( !pPars->fSilent )
455  printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", pPars->nBddMax );
456  return -1;
457  }
458  if ( pPars->fVerbose )
459  printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
460 
461  // check the runtime limit
462  if ( pPars->TimeLimit && pPars->TimeLimit <= (Abc_Clock()-clk)/CLOCKS_PER_SEC )
463  {
464  printf( "Reached timeout after constructing global BDDs (%d seconds).\n", pPars->TimeLimit );
465  Cudd_Quit( dd );
466  return -1;
467  }
468 
469  // start the onion rings
470  vOnionRings = Vec_PtrAlloc( 1000 );
471 
472  // save outputs
473  pbOutputs = Aig_ManCreateOutputs( dd, p );
474 
475  // create partitions
476  pbParts = Aig_ManCreatePartitions( dd, p, pPars->fReorder, pPars->fVerbose );
477 
478  // create the initial state and the variable map
479  bInitial = Aig_ManInitStateVarMap( dd, p, pPars->fVerbose ); Cudd_Ref( bInitial );
480 
481  // set reordering
482  if ( pPars->fReorderImage )
483  Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
484 
485  // check the result
486  RetValue = -1;
487  for ( i = 0; i < Saig_ManPoNum(p); i++ )
488  {
489  if ( fCheckOutputs && !Cudd_bddLeq( dd, bInitial, Cudd_Not(pbOutputs[i]) ) )
490  {
491  DdNode * bIntersect;
492  bIntersect = Cudd_bddIntersect( dd, bInitial, pbOutputs[i] ); Cudd_Ref( bIntersect );
493  assert( p->pSeqModel == NULL );
494  p->pSeqModel = Aig_ManVerifyUsingBddsCountExample( p, dd, pbParts,
495  vOnionRings, bIntersect, i, pPars->fVerbose, pPars->fSilent );
496  Cudd_RecursiveDeref( dd, bIntersect );
497  if ( !pPars->fSilent )
498  Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", i, p->pName, -1 );
499  RetValue = 0;
500  break;
501  }
502  }
503  // free the onion rings
504  Vec_PtrForEachEntry( DdNode *, vOnionRings, bTemp, i )
505  Cudd_RecursiveDeref( dd, bTemp );
506  Vec_PtrFree( vOnionRings );
507  // explore reachable states
508  if ( RetValue == -1 )
509  RetValue = Aig_ManComputeReachable( dd, p, pbParts, bInitial, pbOutputs, pPars, fCheckOutputs );
510 
511  // cleanup
512  Cudd_RecursiveDeref( dd, bInitial );
513  for ( i = 0; i < Saig_ManRegNum(p); i++ )
514  Cudd_RecursiveDeref( dd, pbParts[i] );
515  ABC_FREE( pbParts );
516  for ( i = 0; i < Saig_ManPoNum(p); i++ )
517  Cudd_RecursiveDeref( dd, pbOutputs[i] );
518  ABC_FREE( pbOutputs );
519 // if ( RetValue == -1 )
520  Cudd_Quit( dd );
521 // else
522 // Bbr_StopManager( dd );
523 
524  // report the runtime
525  if ( !pPars->fSilent )
526  {
527  ABC_PRT( "Time", Abc_Clock() - clk );
528  fflush( stdout );
529  }
530  return RetValue;
531 }
532 
533 /**Function*************************************************************
534 
535  Synopsis [Performs reachability to see if any PO can be asserted.]
536 
537  Description []
538 
539  SideEffects []
540 
541  SeeAlso []
542 
543 ***********************************************************************/
544 int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, Saig_ParBbr_t * pPars )
545 {
546  Abc_Cex_t * pCexOld, * pCexNew;
547  Aig_Man_t * p;
548  Aig_Obj_t * pObj;
549  Vec_Int_t * vInputMap;
550  int i, k, Entry, iBitOld, iBitNew, RetValue;
551 // pPars->fVerbose = 1;
552  // check if there are PIs without fanout
553  Saig_ManForEachPi( pInit, pObj, i )
554  if ( Aig_ObjRefs(pObj) == 0 )
555  break;
556  if ( i == Saig_ManPiNum(pInit) )
557  return Aig_ManVerifyUsingBdds_int( pInit, pPars );
558  // create new AIG
559  p = Aig_ManDupTrim( pInit );
560  assert( Aig_ManCiNum(p) < Aig_ManCiNum(pInit) );
561  assert( Aig_ManRegNum(p) == Aig_ManRegNum(pInit) );
562  RetValue = Aig_ManVerifyUsingBdds_int( p, pPars );
563  if ( RetValue != 0 )
564  {
565  Aig_ManStop( p );
566  return RetValue;
567  }
568  // the problem is satisfiable - remap the pattern
569  pCexOld = p->pSeqModel;
570  assert( pCexOld != NULL );
571  // create input map
572  vInputMap = Vec_IntAlloc( Saig_ManPiNum(pInit) );
573  Saig_ManForEachPi( pInit, pObj, i )
574  if ( pObj->pData != NULL )
575  Vec_IntPush( vInputMap, Aig_ObjCioId((Aig_Obj_t *)pObj->pData) );
576  else
577  Vec_IntPush( vInputMap, -1 );
578  // create new pattern
579  pCexNew = Abc_CexAlloc( Saig_ManRegNum(pInit), Saig_ManPiNum(pInit), pCexOld->iFrame+1 );
580  pCexNew->iFrame = pCexOld->iFrame;
581  pCexNew->iPo = pCexOld->iPo;
582  // copy the bit-data
583  for ( iBitOld = 0; iBitOld < pCexOld->nRegs; iBitOld++ )
584  if ( Abc_InfoHasBit( pCexOld->pData, iBitOld ) )
585  Abc_InfoSetBit( pCexNew->pData, iBitOld );
586  // copy the primary input data
587  iBitNew = iBitOld;
588  for ( i = 0; i <= pCexNew->iFrame; i++ )
589  {
590  Vec_IntForEachEntry( vInputMap, Entry, k )
591  {
592  if ( Entry == -1 )
593  continue;
594  if ( Abc_InfoHasBit( pCexOld->pData, iBitOld + Entry ) )
595  Abc_InfoSetBit( pCexNew->pData, iBitNew + k );
596  }
597  iBitOld += Saig_ManPiNum(p);
598  iBitNew += Saig_ManPiNum(pInit);
599  }
600  assert( iBitOld < iBitNew );
601  assert( iBitOld == pCexOld->nBits );
602  assert( iBitNew == pCexNew->nBits );
603  Vec_IntFree( vInputMap );
604  pInit->pSeqModel = pCexNew;
605  Aig_ManStop( p );
606  return 0;
607 }
608 
609 ////////////////////////////////////////////////////////////////////////
610 /// END OF FILE ///
611 ////////////////////////////////////////////////////////////////////////
612 
613 
614 ABC_NAMESPACE_IMPL_END
615 
Aig_ManComputeReachable
int Aig_ManComputeReachable(DdManager *dd, Aig_Man_t *p, DdNode **pbParts, DdNode *bInitial, DdNode **pbOutputs, Saig_ParBbr_t *pPars, int fCheckOutputs)
Definition: bbrReach.c:238
memset
char * memset()
Saig_ParBbr_t_::fReorder
int fReorder
Definition: saig.h:60
Vec_Ptr_t
typedefABC_NAMESPACE_HEADER_START struct Vec_Ptr_t_ Vec_Ptr_t
INCLUDES ///.
Definition: vecPtr.h:42
Saig_ParBbr_t_::iFrame
int iFrame
Definition: saig.h:65
Saig_ParBbr_t_::fPartition
int fPartition
Definition: saig.h:59
Cudd_RecursiveDeref
void Cudd_RecursiveDeref(DdManager *table, DdNode *n)
Definition: cuddRef.c:154
Cudd_CountMinterm
double Cudd_CountMinterm(DdManager *manager, DdNode *node, int nvars)
Definition: cuddUtil.c:578
Aig_ManCreatePartitions
DdNode ** Aig_ManCreatePartitions(DdManager *dd, Aig_Man_t *p, int fReorder, int fVerbose)
Definition: bbrReach.c:187
DdNode
Definition: cudd.h:278
Cudd_Not
#define Cudd_Not(node)
Definition: cudd.h:367
Saig_ParBbr_t_::fSkipOutCheck
int fSkipOutCheck
Definition: saig.h:64
Saig_ManPoNum
static int Saig_ManPoNum(Aig_Man_t *p)
Definition: saig.h:74
Aig_Man_t
typedefABC_NAMESPACE_HEADER_START struct Aig_Man_t_ Aig_Man_t
INCLUDES ///.
Definition: aig.h:50
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Aig_ManStop
void Aig_ManStop(Aig_Man_t *p)
Definition: aigMan.c:187
Abc_InfoHasBit
static int Abc_InfoHasBit(unsigned *p, int i)
Definition: abc_global.h:258
Abc_CexAlloc
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Abc_CexAlloc(int nRegs, int nRealPis, int nFrames)
DECLARATIONS ///.
Definition: utilCex.c:51
Cudd_Deref
void Cudd_Deref(DdNode *node)
Definition: cuddRef.c:438
DdManager::size
int size
Definition: cuddInt.h:361
Saig_ParBbr_t_::nBddMax
int nBddMax
Definition: saig.h:57
Aig_Obj_t_::pData
void * pData
Definition: aig.h:87
Bbr_ImageTree_t_
Definition: bbrImage.c:46
Aig_ObjGlobalBdd
static ABC_NAMESPACE_HEADER_START DdNode * Aig_ObjGlobalBdd(Aig_Obj_t *pObj)
INCLUDES ///.
Definition: bbr.h:51
Cudd_SetVarMap
int Cudd_SetVarMap(DdManager *manager, DdNode **x, DdNode **y, int n)
Definition: cuddCompose.c:416
Aig_ManFreeGlobalBdds
void Aig_ManFreeGlobalBdds(Aig_Man_t *p, DdManager *dd)
Definition: bbrNtbdd.c:112
Vec_PtrPush
static void Vec_PtrPush(Vec_Ptr_t *p, void *Entry)
Definition: vecPtr.h:606
Aig_ManInitStateVarMap
DdNode * Aig_ManInitStateVarMap(DdManager *dd, Aig_Man_t *p, int fVerbose)
Definition: bbrReach.c:124
ABC_ALLOC
#define ABC_ALLOC(type, num)
Definition: abc_global.h:229
Bbr_ManSetDefaultParams
void Bbr_ManSetDefaultParams(Saig_ParBbr_t *p)
FUNCTION DEFINITIONS ///.
Definition: bbrReach.c:49
Aig_ManVerifyUsingBddsCountExample
ABC_NAMESPACE_IMPL_START Abc_Cex_t * Aig_ManVerifyUsingBddsCountExample(Aig_Man_t *p, DdManager *dd, DdNode **pbParts, Vec_Ptr_t *vOnionRings, DdNode *bCubeFirst, int iOutput, int fVerbose, int fSilent)
DECLARATIONS ///.
Definition: bbrCex.c:47
Bbr_bddImageStart
Bbr_ImageTree_t * Bbr_bddImageStart(DdManager *dd, DdNode *bCare, int nParts, DdNode **pbParts, int nVars, DdNode **pbVars, int nBddMax, int fVerbose)
Definition: bbrImage.c:168
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
Vec_PtrSize
static int Vec_PtrSize(Vec_Ptr_t *p)
Definition: vecPtr.h:295
Saig_ParBbr_t_::nIterMax
int nIterMax
Definition: saig.h:58
Bbr_ImageTree2_t_
Definition: bbrImage.c:1212
Aig_ManCreateOutputs
DdNode ** Aig_ManCreateOutputs(DdManager *dd, Aig_Man_t *p)
Definition: bbrReach.c:162
Bbr_bddImageStart2
Bbr_ImageTree2_t * Bbr_bddImageStart2(DdManager *dd, DdNode *bCare, int nParts, DdNode **pbParts, int nVars, DdNode **pbVars, int fVerbose)
Definition: bbrImage.c:1231
Aig_ManVerifyUsingBdds_int
int Aig_ManVerifyUsingBdds_int(Aig_Man_t *p, Saig_ParBbr_t *pPars)
Definition: bbrReach.c:438
Cudd_bddVarMap
DdNode * Cudd_bddVarMap(DdManager *manager, DdNode *f)
Definition: cuddCompose.c:373
Saig_ParBbr_t_::TimeLimit
int TimeLimit
Definition: saig.h:56
Vec_IntAlloc
static Vec_Int_t * Vec_IntAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: bblif.c:149
Bbr_bddImageTreeDelete
void Bbr_bddImageTreeDelete(Bbr_ImageTree_t *pTree)
Definition: bbrImage.c:307
Cudd_ReorderingStatus
int Cudd_ReorderingStatus(DdManager *unique, Cudd_ReorderingType *method)
Definition: cuddAPI.c:735
one
static DdNode * one
Definition: cuddDecomp.c:112
Bbr_bddImageCompute2
DdNode * Bbr_bddImageCompute2(Bbr_ImageTree2_t *pTree, DdNode *bCare)
Definition: bbrImage.c:1273
Saig_ManForEachLi
#define Saig_ManForEachLi(p, pObj, i)
Definition: saig.h:98
Aig_ManCiNum
static int Aig_ManCiNum(Aig_Man_t *p)
Definition: aig.h:251
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Saig_ParBbr_t_::fReorderImage
int fReorderImage
Definition: saig.h:61
size
static int size
Definition: cuddSign.c:86
Aig_Obj_t_
Definition: aig.h:69
Vec_IntPush
static void Vec_IntPush(Vec_Int_t *p, int Entry)
Definition: bblif.c:468
Saig_ManForEachLo
#define Saig_ManForEachLo(p, pObj, i)
Definition: saig.h:96
Saig_ManCiNum
static int Saig_ManCiNum(Aig_Man_t *p)
Definition: saig.h:75
Cudd_bddXnor
DdNode * Cudd_bddXnor(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:507
Cudd_bddOr
DdNode * Cudd_bddOr(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:381
Abc_Print
static void Abc_Print(int level, const char *format,...)
Definition: abc_global.h:313
Saig_ManRegNum
static int Saig_ManRegNum(Aig_Man_t *p)
Definition: saig.h:77
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Cudd_CheckZeroRef
int Cudd_CheckZeroRef(DdManager *manager)
Definition: cuddRef.c:466
Abc_InfoSetBit
static void Abc_InfoSetBit(unsigned *p, int i)
Definition: abc_global.h:259
Cudd_AutodynDisable
void Cudd_AutodynDisable(DdManager *unique)
Definition: cuddAPI.c:708
Saig_ParBbr_t_
Definition: saig.h:54
Aig_ManRegNum
static int Aig_ManRegNum(Aig_Man_t *p)
Definition: aig.h:260
Aig_ManDupTrim
Aig_Man_t * Aig_ManDupTrim(Aig_Man_t *p)
Definition: aigDup.c:413
Cudd_bddLeq
int Cudd_bddLeq(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:536
Aig_ManVerifyUsingBdds
int Aig_ManVerifyUsingBdds(Aig_Man_t *pInit, Saig_ParBbr_t *pPars)
Definition: bbrReach.c:544
Vec_PtrAlloc
static Vec_Ptr_t * Vec_PtrAlloc(int nCap)
FUNCTION DEFINITIONS ///.
Definition: vecPtr.h:83
Saig_ManPiNum
static int Saig_ManPiNum(Aig_Man_t *p)
MACRO DEFINITIONS ///.
Definition: saig.h:73
Bbr_bddImageCompute
DdNode * Bbr_bddImageCompute(Bbr_ImageTree_t *pTree, DdNode *bCare)
Definition: bbrImage.c:253
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
DdManager::vars
DdNode ** vars
Definition: cuddInt.h:390
ABC_PRT
#define ABC_PRT(a, t)
Definition: abc_global.h:220
Bbr_StopManager
void Bbr_StopManager(DdManager *dd)
Definition: bbrReach.c:102
Cudd_bddIthVar
DdNode * Cudd_bddIthVar(DdManager *dd, int i)
Definition: cuddAPI.c:416
Bbr_bddComputeRangeCube
DdNode * Bbr_bddComputeRangeCube(DdManager *dd, int iStart, int iStop)
DECLARATIONS ///.
Definition: bbrReach.c:74
Cudd_ReadKeys
unsigned int Cudd_ReadKeys(DdManager *dd)
Definition: cuddAPI.c:1626
Cudd_bddAnd
DdNode * Cudd_bddAnd(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:314
Saig_ManForEachPo
#define Saig_ManForEachPo(p, pObj, i)
Definition: saig.h:93
assert
#define assert(ex)
Definition: util_old.h:213
Abc_Cex_t
typedefABC_NAMESPACE_HEADER_START struct Abc_Cex_t_ Abc_Cex_t
INCLUDES ///.
Definition: utilCex.h:39
Cudd_Quit
void Cudd_Quit(DdManager *unique)
Definition: cuddInit.c:225
Cudd_ReduceHeap
int Cudd_ReduceHeap(DdManager *table, Cudd_ReorderingType heuristic, int minsize)
Definition: cuddReorder.c:176
Cudd_AutodynEnable
void Cudd_AutodynEnable(DdManager *unique, Cudd_ReorderingType method)
Definition: cuddAPI.c:669
Aig_ObjRefs
static int Aig_ObjRefs(Aig_Obj_t *pObj)
Definition: aig.h:300
Saig_ParBbr_t_::fSilent
int fSilent
Definition: saig.h:63
Cudd_Ref
void Cudd_Ref(DdNode *n)
Definition: cuddRef.c:129
Cudd_ReadDead
unsigned int Cudd_ReadDead(DdManager *dd)
Definition: cuddAPI.c:1646
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Vec_PtrForEachEntry
#define Vec_PtrForEachEntry(Type, vVec, pEntry, i)
MACRO DEFINITIONS ///.
Definition: vecPtr.h:55
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition: vecInt.h:54
Cudd_ReorderingType
Cudd_ReorderingType
Definition: cudd.h:151
Cudd_bddIntersect
DdNode * Cudd_bddIntersect(DdManager *dd, DdNode *f, DdNode *g)
Definition: cuddBddIte.c:282
Cudd_SharingSize
int Cudd_SharingSize(DdNode **nodeArray, int n)
Definition: cuddUtil.c:544
Aig_ObjCioId
static int Aig_ObjCioId(Aig_Obj_t *pObj)
Definition: aig.h:285
Cudd_DagSize
int Cudd_DagSize(DdNode *node)
Definition: cuddUtil.c:442
Vec_PtrFree
static void Vec_PtrFree(Vec_Ptr_t *p)
Definition: vecPtr.h:223
Saig_ParBbr_t_::fVerbose
int fVerbose
Definition: saig.h:62
Saig_ManForEachPi
#define Saig_ManForEachPi(p, pObj, i)
Definition: saig.h:91
Aig_ManComputeGlobalBdds
DdManager * Aig_ManComputeGlobalBdds(Aig_Man_t *p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose)
Definition: bbrNtbdd.c:157
Bbr_bddImageTreeDelete2
void Bbr_bddImageTreeDelete2(Bbr_ImageTree2_t *pTree)
Definition: bbrImage.c:1293