bbrReach.c 20.5 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22
/**CFile****************************************************************

  FileName    [bbrReach.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [BDD-based reachability analysis.]

  Synopsis    [Procedures to perform reachability analysis.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - June 20, 2005.]

  Revision    [$Id: bbrReach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]

***********************************************************************/

#include "bbr.h"

23 24 25
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
26 27 28 29
////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

30
extern Abc_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, 
Alan Mishchenko committed
31 32 33
    DdNode ** pbParts, Vec_Ptr_t * vOnionRings, DdNode * bCubeFirst, 
    int iOutput, int fVerbose, int fSilent );

Alan Mishchenko committed
34 35 36 37
////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62
/**Function*************************************************************

  Synopsis    [This procedure sets default resynthesis parameters.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Bbr_ManSetDefaultParams( Saig_ParBbr_t * p )
{
    memset( p, 0, sizeof(Saig_ParBbr_t) );
    p->TimeLimit     =     0;
    p->nBddMax       = 50000;
    p->nIterMax      =  1000;
    p->fPartition    =     1;
    p->fReorder      =     1;
    p->fReorderImage =     1;
    p->fVerbose      =     0;
    p->fSilent       =     0;
    p->iFrame        =    -1;
}

Alan Mishchenko committed
63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113 114 115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131
/**Function********************************************************************

  Synopsis    [Performs the reordering-sensitive step of Extra_bddMove().]

  Description []

  SideEffects []

  SeeAlso     []

******************************************************************************/
DdNode * Bbr_bddComputeRangeCube( DdManager * dd, int iStart, int iStop )
{
    DdNode * bTemp, * bProd;
    int i;
    assert( iStart <= iStop );
    assert( iStart >= 0 && iStart <= dd->size );
    assert( iStop >= 0  && iStop  <= dd->size );
    bProd = (dd)->one;         Cudd_Ref( bProd );
    for ( i = iStart; i < iStop; i++ )
    {
        bProd = Cudd_bddAnd( dd, bTemp = bProd, dd->vars[i] );      Cudd_Ref( bProd );
        Cudd_RecursiveDeref( dd, bTemp ); 
    }
    Cudd_Deref( bProd );
    return bProd;
}

/**Function*************************************************************

  Synopsis    []

  Description []

  SideEffects []

  SeeAlso     []

***********************************************************************/
void Bbr_StopManager( DdManager * dd )
{
    int RetValue;
    // check for remaining references in the package
    RetValue = Cudd_CheckZeroRef( dd );
    if ( RetValue > 0 )
        printf( "\nThe number of referenced nodes = %d\n\n", RetValue );
//  Cudd_PrintInfo( dd, stdout );
    Cudd_Quit( dd );
}

/**Function*************************************************************

  Synopsis    [Computes the initial state and sets up the variable map.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * Aig_ManInitStateVarMap( DdManager * dd, Aig_Man_t * p, int fVerbose )
{
    DdNode ** pbVarsX, ** pbVarsY;
    DdNode * bTemp, * bProd;
    Aig_Obj_t * pLatch;
    int i;

    // set the variable mapping for Cudd_bddVarMap()
Alan Mishchenko committed
132 133
    pbVarsX = ABC_ALLOC( DdNode *, dd->size );
    pbVarsY = ABC_ALLOC( DdNode *, dd->size );
Alan Mishchenko committed
134 135 136 137 138 139 140 141 142 143
    bProd = (dd)->one;         Cudd_Ref( bProd );
    Saig_ManForEachLo( p, pLatch, i )
    {
        pbVarsX[i] = dd->vars[ Saig_ManPiNum(p) + i ];
        pbVarsY[i] = dd->vars[ Saig_ManCiNum(p) + i ];
        // get the initial value of the latch
        bProd = Cudd_bddAnd( dd, bTemp = bProd, Cudd_Not(pbVarsX[i]) );      Cudd_Ref( bProd );
        Cudd_RecursiveDeref( dd, bTemp ); 
    }
    Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Saig_ManRegNum(p) );
Alan Mishchenko committed
144 145
    ABC_FREE( pbVarsX );
    ABC_FREE( pbVarsY );
Alan Mishchenko committed
146 147 148 149 150 151 152 153 154 155 156 157 158 159 160 161 162 163 164 165 166 167

    Cudd_Deref( bProd );
    return bProd;
}

/**Function*************************************************************

  Synopsis    [Collects the array of output BDDs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode ** Aig_ManCreateOutputs( DdManager * dd, Aig_Man_t * p )
{
    DdNode ** pbOutputs;
    Aig_Obj_t * pNode;
    int i;
    // compute the transition relation
Alan Mishchenko committed
168
    pbOutputs = ABC_ALLOC( DdNode *, Saig_ManPoNum(p) );
Alan Mishchenko committed
169 170 171 172 173 174 175 176 177 178 179 180 181 182 183 184 185 186 187 188 189 190 191 192 193 194 195 196 197 198 199 200 201 202 203 204
    Saig_ManForEachPo( p, pNode, i )
    {
        pbOutputs[i] = Aig_ObjGlobalBdd(pNode);  Cudd_Ref( pbOutputs[i] );
    }
    return pbOutputs;
}

/**Function*************************************************************

  Synopsis    [Collects the array of partition BDDs.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode ** Aig_ManCreatePartitions( DdManager * dd, Aig_Man_t * p, int fReorder, int fVerbose )
{
    DdNode ** pbParts;
    DdNode * bVar;
    Aig_Obj_t * pNode;
    int i;

    // extand the BDD manager to represent NS variables
    assert( dd->size == Saig_ManCiNum(p) );
    Cudd_bddIthVar( dd, Saig_ManCiNum(p) + Saig_ManRegNum(p) - 1 );

    // enable reordering
    if ( fReorder )
        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
    else
        Cudd_AutodynDisable( dd );

    // compute the transition relation
Alan Mishchenko committed
205
    pbParts = ABC_ALLOC( DdNode *, Saig_ManRegNum(p) );
Alan Mishchenko committed
206 207 208 209 210
    Saig_ManForEachLi( p, pNode, i )
    {
        bVar  = Cudd_bddIthVar( dd, Saig_ManCiNum(p) + i );
        pbParts[i] = Cudd_bddXnor( dd, bVar, Aig_ObjGlobalBdd(pNode) );  Cudd_Ref( pbParts[i] );
    }
Alan Mishchenko committed
211
    // free global BDDs
Alan Mishchenko committed
212 213 214 215 216 217 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237
    Aig_ManFreeGlobalBdds( p, dd );

    // reorder and disable reordering
    if ( fReorder )
    {
        if ( fVerbose )
            fprintf( stdout, "BDD nodes in the partitions before reordering %d.\n", Cudd_SharingSize(pbParts,Saig_ManRegNum(p)) );
        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
        Cudd_AutodynDisable( dd );
        if ( fVerbose )
            fprintf( stdout, "BDD nodes in the partitions after reordering %d.\n", Cudd_SharingSize(pbParts,Saig_ManRegNum(p)) );
    }
    return pbParts;
}

/**Function*************************************************************

  Synopsis    [Computes the set of unreachable states.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
238
int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, DdNode * bInitial, DdNode ** pbOutputs, Saig_ParBbr_t * pPars, int fCheckOutputs )
Alan Mishchenko committed
239 240
{
    int fInternalReorder = 0;
Alan Mishchenko committed
241 242
    Bbr_ImageTree_t * pTree = NULL; // Suppress "might be used uninitialized"
    Bbr_ImageTree2_t * pTree2 = NULL; // Supprses "might be used uninitialized"
Alan Mishchenko committed
243
    DdNode * bReached, * bCubeCs;
Alan Mishchenko committed
244 245 246
    DdNode * bCurrent;
    DdNode * bNext = NULL; // Suppress "might be used uninitialized"
    DdNode * bTemp;
247
    Cudd_ReorderingType method;
248
    int i, nIters, nBddSize = 0, status;
249
    int nThreshold = 10000;
250
    abctime clk = Abc_Clock();
Alan Mishchenko committed
251
    Vec_Ptr_t * vOnionRings;
252
    int fixedPoint = 0;
Alan Mishchenko committed
253 254 255 256

    status = Cudd_ReorderingStatus( dd, &method );
    if ( status )
        Cudd_AutodynDisable( dd );
Alan Mishchenko committed
257 258 259

    // start the image computation
    bCubeCs  = Bbr_bddComputeRangeCube( dd, Saig_ManPiNum(p), Saig_ManCiNum(p) );    Cudd_Ref( bCubeCs );
260 261
    if ( pPars->fPartition )
        pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), pPars->nBddMax, pPars->fVerbose );
Alan Mishchenko committed
262
    else
263
        pTree2 = Bbr_bddImageStart2( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), pPars->fVerbose );
Alan Mishchenko committed
264 265 266
    Cudd_RecursiveDeref( dd, bCubeCs );
    if ( pTree == NULL )
    {
267
        if ( !pPars->fSilent )
Alan Mishchenko committed
268
            printf( "BDDs blew up during qualitification scheduling.  " );
Alan Mishchenko committed
269 270 271
        return -1;
    }

Alan Mishchenko committed
272 273 274
    if ( status )
        Cudd_AutodynEnable( dd, method );

Alan Mishchenko committed
275 276 277
    // start the onion rings
    vOnionRings = Vec_PtrAlloc( 1000 );

278
    // perform reachability analysis
Alan Mishchenko committed
279 280
    bCurrent = bInitial;   Cudd_Ref( bCurrent );
    bReached = bInitial;   Cudd_Ref( bReached );
Alan Mishchenko committed
281
    Vec_PtrPush( vOnionRings, bCurrent );  Cudd_Ref( bCurrent );
282
    for ( nIters = 0; nIters < pPars->nIterMax; nIters++ )
Alan Mishchenko committed
283
    { 
284
        // check the runtime limit
285
        if ( pPars->TimeLimit && pPars->TimeLimit <= (Abc_Clock()-clk)/CLOCKS_PER_SEC )
286 287 288 289 290 291 292 293 294 295 296 297
        {
            printf( "Reached timeout after image computation (%d seconds).\n",  pPars->TimeLimit );
            Vec_PtrFree( vOnionRings );
            // undo the image tree
            if ( pPars->fPartition )
                Bbr_bddImageTreeDelete( pTree );
            else
                Bbr_bddImageTreeDelete2( pTree2 );
            pPars->iFrame = nIters - 1;
            return -1;
        }

Alan Mishchenko committed
298
        // compute the next states
299
        if ( pPars->fPartition )
Alan Mishchenko committed
300 301 302 303 304
            bNext = Bbr_bddImageCompute( pTree, bCurrent );           
        else
            bNext = Bbr_bddImageCompute2( pTree2, bCurrent );  
        if ( bNext == NULL )
        {
305
            if ( !pPars->fSilent )
Alan Mishchenko committed
306
                printf( "BDDs blew up during image computation.  " );
307
            if ( pPars->fPartition )
Alan Mishchenko committed
308 309 310
                Bbr_bddImageTreeDelete( pTree );
            else
                Bbr_bddImageTreeDelete2( pTree2 );
Alan Mishchenko committed
311
            Vec_PtrFree( vOnionRings );
312
            pPars->iFrame = nIters - 1;
Alan Mishchenko committed
313 314 315 316
            return -1;
        }
        Cudd_Ref( bNext );
        Cudd_RecursiveDeref( dd, bCurrent );
317

Alan Mishchenko committed
318 319 320 321
        // remap these states into the current state vars
        bNext = Cudd_bddVarMap( dd, bTemp = bNext );                    Cudd_Ref( bNext );
        Cudd_RecursiveDeref( dd, bTemp );
        // check if there are any new states
322 323
        if ( Cudd_bddLeq( dd, bNext, bReached ) ) {
            fixedPoint = 1;
Alan Mishchenko committed
324
            break;
325
        }
Alan Mishchenko committed
326 327
        // check the BDD size
        nBddSize = Cudd_DagSize(bNext);
328
        if ( nBddSize > pPars->nBddMax )
Alan Mishchenko committed
329 330 331 332
            break;
        // check the result
        for ( i = 0; i < Saig_ManPoNum(p); i++ )
        {
333
            if ( fCheckOutputs && !Cudd_bddLeq( dd, bNext, Cudd_Not(pbOutputs[i]) ) )
Alan Mishchenko committed
334
            {
Alan Mishchenko committed
335 336 337 338
                DdNode * bIntersect;
                bIntersect = Cudd_bddIntersect( dd, bNext, pbOutputs[i] );  Cudd_Ref( bIntersect );
                assert( p->pSeqModel == NULL );
                p->pSeqModel = Aig_ManVerifyUsingBddsCountExample( p, dd, pbParts, 
339
                    vOnionRings, bIntersect, i, pPars->fVerbose, pPars->fSilent ); 
Alan Mishchenko committed
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) );
Alan Mishchenko committed
343 344
                Cudd_RecursiveDeref( dd, bReached );
                bReached = NULL;
345
                pPars->iFrame = nIters;
Alan Mishchenko committed
346 347 348 349 350 351 352
                break;
            }
        }
        if ( i < Saig_ManPoNum(p) )
            break;
        // get the new states
        bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) );        Cudd_Ref( bCurrent );
Alan Mishchenko committed
353
        Vec_PtrPush( vOnionRings, bCurrent );  Cudd_Ref( bCurrent );
Alan Mishchenko committed
354 355 356 357 358 359 360
        // minimize the new states with the reached states
//        bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
//        Cudd_RecursiveDeref( dd, bTemp );
        // add to the reached states
        bReached = Cudd_bddOr( dd, bTemp = bReached, bNext );           Cudd_Ref( bReached );
        Cudd_RecursiveDeref( dd, bTemp );
        Cudd_RecursiveDeref( dd, bNext );
361
        if ( pPars->fVerbose )
Alan Mishchenko committed
362
            fprintf( stdout, "Frame = %3d. BDD = %5d. ", nIters, nBddSize );
363
        if ( fInternalReorder && pPars->fReorder && nBddSize > nThreshold )
Alan Mishchenko committed
364
        {
365
            if ( pPars->fVerbose )
Alan Mishchenko committed
366 367 368
                fprintf( stdout, "Reordering... Before = %5d. ", Cudd_DagSize(bReached) );
            Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
            Cudd_AutodynDisable( dd );
369
            if ( pPars->fVerbose )
Alan Mishchenko committed
370 371 372
                fprintf( stdout, "After = %5d.\r", Cudd_DagSize(bReached) );
            nThreshold *= 2;
        }
373 374 375
        if ( pPars->fVerbose )
//            fprintf( stdout, "\r" );
            fprintf( stdout, "\n" );
376 377 378 379 380 381 382 383 384

        if ( pPars->fVerbose )
        {
            double nMints = Cudd_CountMinterm(dd, bReached, Saig_ManRegNum(p) );
//            Extra_bddPrint( dd, bReached );printf( "\n" );
            fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p)) );
            fflush( stdout ); 
        }

Alan Mishchenko committed
385 386
    }
    Cudd_RecursiveDeref( dd, bNext );
Alan Mishchenko committed
387
    // free the onion rings
388
    Vec_PtrForEachEntry( DdNode *, vOnionRings, bTemp, i )
Alan Mishchenko committed
389 390
        Cudd_RecursiveDeref( dd, bTemp );
    Vec_PtrFree( vOnionRings );
Alan Mishchenko committed
391
    // undo the image tree
392
    if ( pPars->fPartition )
Alan Mishchenko committed
393 394 395 396 397 398
        Bbr_bddImageTreeDelete( pTree );
    else
        Bbr_bddImageTreeDelete2( pTree2 );
    if ( bReached == NULL )
        return 0; // proved reachable
    // report the stats
399
    if ( pPars->fVerbose )
Alan Mishchenko committed
400 401
    {
        double nMints = Cudd_CountMinterm(dd, bReached, Saig_ManRegNum(p) );
402
        if ( nIters > pPars->nIterMax || nBddSize > pPars->nBddMax )
Alan Mishchenko committed
403 404 405 406 407 408
            fprintf( stdout, "Reachability analysis is stopped after %d frames.\n", nIters );
        else
            fprintf( stdout, "Reachability analysis completed after %d frames.\n", nIters );
        fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p)) );
        fflush( stdout );
    }
Alan Mishchenko committed
409
//ABC_PRB( dd, bReached );
Alan Mishchenko committed
410
    Cudd_RecursiveDeref( dd, bReached );
411 412 413 414 415 416 417 418
    // SPG
    //
    if ( fixedPoint ) {
      if ( !pPars->fSilent ) {
        printf( "The miter is proved unreachable after %d iterations.  ", nIters );
      }
      pPars->iFrame = nIters - 1;
      return 1;
Alan Mishchenko committed
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
Alan Mishchenko committed
425 426 427 428
}

/**Function*************************************************************

Alan Mishchenko committed
429
  Synopsis    [Performs reachability to see if any PO can be asserted.]
Alan Mishchenko committed
430 431 432 433

  Description []
               
  SideEffects []
Alan Mishchenko committed
434
 
Alan Mishchenko committed
435 436 437
  SeeAlso     []

***********************************************************************/
438
int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, Saig_ParBbr_t * pPars )
Alan Mishchenko committed
439
{
440
    int fCheckOutputs = !pPars->fSkipOutCheck;
Alan Mishchenko committed
441 442
    DdManager * dd;
    DdNode ** pbParts, ** pbOutputs;
Alan Mishchenko committed
443
    DdNode * bInitial, * bTemp;
444
    int RetValue, i;
445
    abctime clk = Abc_Clock();
Alan Mishchenko committed
446
    Vec_Ptr_t * vOnionRings;
Alan Mishchenko committed
447 448 449 450

    assert( Saig_ManRegNum(p) > 0 );

    // compute the global BDDs of the latches
451
    dd = Aig_ManComputeGlobalBdds( p, pPars->nBddMax, 1, pPars->fReorder, pPars->fVerbose );    
Alan Mishchenko committed
452 453
    if ( dd == NULL )
    {
454 455
        if ( !pPars->fSilent )
            printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", pPars->nBddMax );
Alan Mishchenko committed
456 457
        return -1;
    }
458
    if ( pPars->fVerbose )
Alan Mishchenko committed
459 460
        printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );

461
    // check the runtime limit
462
    if ( pPars->TimeLimit && pPars->TimeLimit <= (Abc_Clock()-clk)/CLOCKS_PER_SEC )
463 464 465 466 467 468
    {
        printf( "Reached timeout after constructing global BDDs (%d seconds).\n",  pPars->TimeLimit );
        Cudd_Quit( dd );
        return -1;
    }

Alan Mishchenko committed
469 470 471
    // start the onion rings
    vOnionRings = Vec_PtrAlloc( 1000 );

Alan Mishchenko committed
472 473 474 475
    // save outputs
    pbOutputs = Aig_ManCreateOutputs( dd, p );

    // create partitions
476
    pbParts = Aig_ManCreatePartitions( dd, p, pPars->fReorder, pPars->fVerbose );
Alan Mishchenko committed
477 478

    // create the initial state and the variable map
479
    bInitial  = Aig_ManInitStateVarMap( dd, p, pPars->fVerbose );  Cudd_Ref( bInitial );
Alan Mishchenko committed
480

Alan Mishchenko committed
481
    // set reordering
482
    if ( pPars->fReorderImage )
Alan Mishchenko committed
483 484
        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );

Alan Mishchenko committed
485 486 487 488
    // check the result
    RetValue = -1;
    for ( i = 0; i < Saig_ManPoNum(p); i++ )
    {
489
        if ( fCheckOutputs && !Cudd_bddLeq( dd, bInitial, Cudd_Not(pbOutputs[i]) ) )
Alan Mishchenko committed
490
        {
Alan Mishchenko committed
491 492 493 494
            DdNode * bIntersect;
            bIntersect = Cudd_bddIntersect( dd, bInitial, pbOutputs[i] );  Cudd_Ref( bIntersect );
            assert( p->pSeqModel == NULL );
            p->pSeqModel = Aig_ManVerifyUsingBddsCountExample( p, dd, pbParts, 
495
                vOnionRings, bIntersect, i, pPars->fVerbose, pPars->fSilent ); 
Alan Mishchenko committed
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 );
Alan Mishchenko committed
499 500 501 502
            RetValue = 0;
            break;
        }
    }
Alan Mishchenko committed
503
    // free the onion rings
504
    Vec_PtrForEachEntry( DdNode *, vOnionRings, bTemp, i )
Alan Mishchenko committed
505 506
        Cudd_RecursiveDeref( dd, bTemp );
    Vec_PtrFree( vOnionRings );
Alan Mishchenko committed
507 508
    // explore reachable states
    if ( RetValue == -1 )
509
        RetValue = Aig_ManComputeReachable( dd, p, pbParts, bInitial, pbOutputs, pPars, fCheckOutputs ); 
Alan Mishchenko committed
510 511 512 513 514

    // cleanup
    Cudd_RecursiveDeref( dd, bInitial );
    for ( i = 0; i < Saig_ManRegNum(p); i++ )
        Cudd_RecursiveDeref( dd, pbParts[i] );
Alan Mishchenko committed
515
    ABC_FREE( pbParts );
Alan Mishchenko committed
516 517
    for ( i = 0; i < Saig_ManPoNum(p); i++ )
        Cudd_RecursiveDeref( dd, pbOutputs[i] );
Alan Mishchenko committed
518
    ABC_FREE( pbOutputs );
519
//    if ( RetValue == -1 )
Alan Mishchenko committed
520
        Cudd_Quit( dd );
521 522
//    else
//        Bbr_StopManager( dd );
Alan Mishchenko committed
523 524

    // report the runtime
525
    if ( !pPars->fSilent )
Alan Mishchenko committed
526
    {
527
    ABC_PRT( "Time", Abc_Clock() - clk );
Alan Mishchenko committed
528
    fflush( stdout );
Alan Mishchenko committed
529
    }
Alan Mishchenko committed
530 531 532
    return RetValue;
}

Alan Mishchenko committed
533 534 535 536 537 538 539 540 541 542 543
/**Function*************************************************************

  Synopsis    [Performs reachability to see if any PO can be asserted.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
544
int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, Saig_ParBbr_t * pPars )
Alan Mishchenko committed
545
{
546
    Abc_Cex_t * pCexOld, * pCexNew;
Alan Mishchenko committed
547 548 549 550
    Aig_Man_t * p;
    Aig_Obj_t * pObj;
    Vec_Int_t * vInputMap;
    int i, k, Entry, iBitOld, iBitNew, RetValue;
551
//    pPars->fVerbose = 1;
Alan Mishchenko committed
552 553 554 555 556
    // check if there are PIs without fanout
    Saig_ManForEachPi( pInit, pObj, i )
        if ( Aig_ObjRefs(pObj) == 0 )
            break;
    if ( i == Saig_ManPiNum(pInit) )
557
        return Aig_ManVerifyUsingBdds_int( pInit, pPars );
Alan Mishchenko committed
558 559
    // create new AIG
    p = Aig_ManDupTrim( pInit );
560
    assert( Aig_ManCiNum(p) < Aig_ManCiNum(pInit) );
Alan Mishchenko committed
561
    assert( Aig_ManRegNum(p) == Aig_ManRegNum(pInit) );
562
    RetValue = Aig_ManVerifyUsingBdds_int( p, pPars );
Alan Mishchenko committed
563 564 565 566 567 568 569 570 571 572 573 574
    if ( RetValue != 0 )
    {
        Aig_ManStop( p );
        return RetValue;
    }
    // the problem is satisfiable - remap the pattern
    pCexOld = p->pSeqModel;
    assert( pCexOld != NULL );
    // create input map
    vInputMap = Vec_IntAlloc( Saig_ManPiNum(pInit) );
    Saig_ManForEachPi( pInit, pObj, i )
        if ( pObj->pData != NULL )
575
            Vec_IntPush( vInputMap, Aig_ObjCioId((Aig_Obj_t *)pObj->pData) );
Alan Mishchenko committed
576 577 578
        else
            Vec_IntPush( vInputMap, -1 );
    // create new pattern
579
    pCexNew = Abc_CexAlloc( Saig_ManRegNum(pInit), Saig_ManPiNum(pInit), pCexOld->iFrame+1 );
Alan Mishchenko committed
580 581 582 583
    pCexNew->iFrame = pCexOld->iFrame;
    pCexNew->iPo    = pCexOld->iPo;
    // copy the bit-data
    for ( iBitOld = 0; iBitOld < pCexOld->nRegs; iBitOld++ )
584 585
        if ( Abc_InfoHasBit( pCexOld->pData, iBitOld ) )
            Abc_InfoSetBit( pCexNew->pData, iBitOld );
Alan Mishchenko committed
586 587 588 589 590 591 592 593
    // copy the primary input data
    iBitNew = iBitOld;
    for ( i = 0; i <= pCexNew->iFrame; i++ )
    {
        Vec_IntForEachEntry( vInputMap, Entry, k )
        {
            if ( Entry == -1 )
                continue;
594 595
            if ( Abc_InfoHasBit( pCexOld->pData, iBitOld + Entry ) )
                Abc_InfoSetBit( pCexNew->pData, iBitNew + k );
Alan Mishchenko committed
596 597 598 599 600 601 602 603 604 605 606 607
        }
        iBitOld += Saig_ManPiNum(p);
        iBitNew += Saig_ManPiNum(pInit);
    }
    assert( iBitOld < iBitNew );
    assert( iBitOld == pCexOld->nBits );
    assert( iBitNew == pCexNew->nBits );
    Vec_IntFree( vInputMap );
    pInit->pSeqModel = pCexNew;
    Aig_ManStop( p );
    return 0;
}
Alan Mishchenko committed
608 609 610 611 612 613

////////////////////////////////////////////////////////////////////////
///                       END OF FILE                                ///
////////////////////////////////////////////////////////////////////////


614 615
ABC_NAMESPACE_IMPL_END