/**CFile****************************************************************

  FileName    [abcReach.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [Network and node package.]

  Synopsis    [Performs reachability analysis.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

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

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

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

#include "base/abc/abc.h"
#include "misc/extra/extraBdd.h"

ABC_NAMESPACE_IMPL_START


////////////////////////////////////////////////////////////////////////
///                        DECLARATIONS                              ///
////////////////////////////////////////////////////////////////////////

////////////////////////////////////////////////////////////////////////
///                     FUNCTION DEFINITIONS                         ///
////////////////////////////////////////////////////////////////////////

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

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

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * Abc_NtkInitStateVarMap( DdManager * dd, Abc_Ntk_t * pNtk, int fVerbose )
{
    DdNode ** pbVarsX, ** pbVarsY;
    DdNode * bTemp, * bProd, * bVar;
    Abc_Obj_t * pLatch;
    int i;

    // set the variable mapping for Cudd_bddVarMap()
    pbVarsX = ABC_ALLOC( DdNode *, dd->size );
    pbVarsY = ABC_ALLOC( DdNode *, dd->size );
    bProd = b1;         Cudd_Ref( bProd );
    Abc_NtkForEachLatch( pNtk, pLatch, i )
    {
        pbVarsX[i] = dd->vars[ Abc_NtkPiNum(pNtk) + i ];
        pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ];
        // get the initial value of the latch
        bVar  = Cudd_NotCond( pbVarsX[i], !Abc_LatchIsInit1(pLatch) );
        bProd = Cudd_bddAnd( dd, bTemp = bProd, bVar );      Cudd_Ref( bProd );
        Cudd_RecursiveDeref( dd, bTemp ); 
    }
    Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Abc_NtkLatchNum(pNtk) );
    ABC_FREE( pbVarsX );
    ABC_FREE( pbVarsY );

    Cudd_Deref( bProd );
    return bProd;
}

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

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode ** Abc_NtkCreatePartitions( DdManager * dd, Abc_Ntk_t * pNtk, int fReorder, int fVerbose )
{
    DdNode ** pbParts;
    DdNode * bVar;
    Abc_Obj_t * pNode;
    int i;

    // extand the BDD manager to represent NS variables
    assert( dd->size == Abc_NtkCiNum(pNtk) );
    Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + Abc_NtkLatchNum(pNtk) - 1 );

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

    // compute the transition relation
    pbParts = ABC_ALLOC( DdNode *, Abc_NtkLatchNum(pNtk) );
    Abc_NtkForEachLatch( pNtk, pNode, i )
    {
        bVar  = Cudd_bddIthVar( dd, Abc_NtkCiNum(pNtk) + i );
        pbParts[i] = Cudd_bddXnor( dd, bVar, (DdNode *)Abc_ObjGlobalBdd(Abc_ObjFanin0(pNode)) );  Cudd_Ref( pbParts[i] );
    }
    // free the global BDDs
    Abc_NtkFreeGlobalBdds( pNtk, 0 );

    // reorder and disable reordering
    if ( fReorder )
    {
        if ( fVerbose )
            fprintf( stdout, "BDD nodes in the partitions before reordering %d.\n", Cudd_SharingSize(pbParts,Abc_NtkLatchNum(pNtk)) );
        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,Abc_NtkLatchNum(pNtk)) );
    }
    return pbParts;
}

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

  Synopsis    [Computes the set of unreachable states.]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * Abc_NtkComputeReachable( DdManager * dd, Abc_Ntk_t * pNtk, DdNode ** pbParts, DdNode * bInitial, DdNode * bOutput, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
{
    int fInternalReorder = 0;
    Extra_ImageTree_t * pTree = NULL;
    Extra_ImageTree2_t * pTree2 = NULL;
    DdNode * bReached, * bCubeCs;
    DdNode * bCurrent, * bNext = NULL, * bTemp;
    DdNode ** pbVarsY;
    Abc_Obj_t * pLatch;
    int i, nIters, nBddSize;
    int nThreshold = 10000;

    // collect the NS variables
    // set the variable mapping for Cudd_bddVarMap()
    pbVarsY = ABC_ALLOC( DdNode *, dd->size );
    Abc_NtkForEachLatch( pNtk, pLatch, i )
        pbVarsY[i] = dd->vars[ Abc_NtkCiNum(pNtk) + i ];

    // start the image computation
    bCubeCs  = Extra_bddComputeRangeCube( dd, Abc_NtkPiNum(pNtk), Abc_NtkCiNum(pNtk) );    Cudd_Ref( bCubeCs );
    if ( fPartition )
        pTree = Extra_bddImageStart( dd, bCubeCs, Abc_NtkLatchNum(pNtk), pbParts, Abc_NtkLatchNum(pNtk), pbVarsY, fVerbose );
    else
        pTree2 = Extra_bddImageStart2( dd, bCubeCs, Abc_NtkLatchNum(pNtk), pbParts, Abc_NtkLatchNum(pNtk), pbVarsY, fVerbose );
    ABC_FREE( pbVarsY );
    Cudd_RecursiveDeref( dd, bCubeCs );

    // perform reachability analisys
    bCurrent = bInitial;   Cudd_Ref( bCurrent );
    bReached = bInitial;   Cudd_Ref( bReached );
    assert( nIterMax > 1 ); // required to not deref uninitialized bNext
    for ( nIters = 1; nIters <= nIterMax; nIters++ )
    {
        // compute the next states
        if ( fPartition )
            bNext = Extra_bddImageCompute( pTree, bCurrent );           
        else
            bNext = Extra_bddImageCompute2( pTree2, bCurrent );         
        Cudd_Ref( bNext );
        Cudd_RecursiveDeref( dd, bCurrent );
        // 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
        if ( Cudd_bddLeq( dd, bNext, bReached ) )
            break;
        // check the BDD size
        nBddSize = Cudd_DagSize(bNext);
        if ( nBddSize > nBddMax )
            break;
        // check the result
        if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(bOutput) ) )
        {
            printf( "The miter is proved REACHABLE in %d iterations.  ", nIters );
            Cudd_RecursiveDeref( dd, bReached );
            bReached = NULL;
            break;
        }
        // get the new states
        bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) );        Cudd_Ref( bCurrent );
        // 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 );
        if ( fVerbose )
            fprintf( stdout, "Iteration = %3d. BDD = %5d. ", nIters, nBddSize );
        if ( fInternalReorder && fReorder && nBddSize > nThreshold )
        {
            if ( fVerbose )
                fprintf( stdout, "Reordering... Before = %5d. ", Cudd_DagSize(bReached) );
            Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
            Cudd_AutodynDisable( dd );
            if ( fVerbose )
                fprintf( stdout, "After = %5d.\r", Cudd_DagSize(bReached) );
            nThreshold *= 2;
        }
        if ( fVerbose )
            fprintf( stdout, "\r" );
    }
    Cudd_RecursiveDeref( dd, bNext );
    // undo the image tree
    if ( fPartition )
        Extra_bddImageTreeDelete( pTree );
    else
        Extra_bddImageTreeDelete2( pTree2 );
    if ( bReached == NULL )
        return NULL;
    // report the stats
    if ( fVerbose )
    {
        double nMints = Cudd_CountMinterm(dd, bReached, Abc_NtkLatchNum(pNtk) );
        if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax )
            fprintf( stdout, "Reachability analysis is stopped after %d iterations.\n", nIters );
        else
            fprintf( stdout, "Reachability analysis completed in %d iterations.\n", nIters );
        fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Abc_NtkLatchNum(pNtk)) );
        fflush( stdout );
    }
//ABC_PRB( dd, bReached );
    Cudd_Deref( bReached );
    if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax )
         printf( "Verified ONLY FOR STATES REACHED in %d iterations. \n", nIters );
    printf( "The miter is proved unreachable in %d iteration.  ", nIters );
    return bReached;
}

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

  Synopsis    [Performs reachability to see if any .]

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
{
    DdManager * dd;
    DdNode ** pbParts;
    DdNode * bOutput, * bReached, * bInitial;
    int i;
    abctime clk = Abc_Clock();

    assert( Abc_NtkIsStrash(pNtk) );
    assert( Abc_NtkPoNum(pNtk) == 1 );
    assert( Abc_ObjFanoutNum(Abc_NtkPo(pNtk,0)) == 0 ); // PO should go first

    // compute the global BDDs of the latches
    dd = (DdManager *)Abc_NtkBuildGlobalBdds( pNtk, nBddMax, 1, fReorder, fVerbose );    
    if ( dd == NULL )
    {
        printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", nBddMax );
        return;
    }
    if ( fVerbose )
        printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );

    // save the output BDD
    bOutput = (DdNode *)Abc_ObjGlobalBdd(Abc_NtkPo(pNtk,0)); Cudd_Ref( bOutput );

    // create partitions
    pbParts = Abc_NtkCreatePartitions( dd, pNtk, fReorder, fVerbose );

    // create the initial state and the variable map
    bInitial  = Abc_NtkInitStateVarMap( dd, pNtk, fVerbose );  Cudd_Ref( bInitial );

    // check the result
    if ( !Cudd_bddLeq( dd, bInitial, Cudd_Not(bOutput) ) )
        printf( "The miter is proved REACHABLE in the initial state.  " );
    else
    {
        // compute the reachable states
        bReached = Abc_NtkComputeReachable( dd, pNtk, pbParts, bInitial, bOutput, nBddMax, nIterMax, fPartition, fReorder, fVerbose ); 
        if ( bReached != NULL )
        {
            Cudd_Ref( bReached );
            Cudd_RecursiveDeref( dd, bReached );
        }
    }

    // cleanup
    Cudd_RecursiveDeref( dd, bOutput );
    Cudd_RecursiveDeref( dd, bInitial );
    for ( i = 0; i < Abc_NtkLatchNum(pNtk); i++ )
        Cudd_RecursiveDeref( dd, pbParts[i] );
    ABC_FREE( pbParts );
    Extra_StopManager( dd );

    // report the runtime
    ABC_PRT( "Time", Abc_Clock() - clk );
    fflush( stdout );
}


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


ABC_NAMESPACE_IMPL_END