abc/src/base/abci/abcSense.c
/**Function*************************************************************

  Synopsis    [Computing sensitivity of POs to POs under constraints.]

  Description [The input network is a combinatonal AIG. The last output
  is a constraint. The procedure returns the list of number of PIs, 
  such that at least one PO depends on this PI, under the constraint.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Function
Synopsis    [Computing sensitivity of POs to POs under constraints.]

Description [The input network is a combinatonal AIG. The last output
is a constraint. The procedure returns the list of number of PIs,
such that at least one PO depends on this PI, under the constraint.]




Function Synopsis [ Computing sensitivity of POs to POs under constraints . ] Description [ The input network is a combinatonal AIG . The last output is a constraint . The procedure returns the list of number of PIs such that at least one PO depends on this PI under the constraint . ]
Vec_Int_t * Abc_NtkSensitivity( Abc_Ntk_t * pNtk, int nConfLim, int fVerbose )
{
    ProgressBar * pProgress;
    Prove_Params_t Params, * pParams = &Params;
    Vec_Int_t * vResult = NULL;
    Abc_Ntk_t * pMiter;
    Abc_Obj_t * pObj;
    int RetValue, i;
    assert( Abc_NtkIsStrash(pNtk) );
    assert( Abc_NtkLatchNum(pNtk) == 0 );
    Prove_ParamsSetDefault( pParams );
    pParams->nItersMax = 3;
    pParams->nMiteringLimitLast = nConfLim;
    vResult = Vec_IntAlloc( 100 );
    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCiNum(pNtk) );
    Abc_NtkForEachCi( pNtk, pObj, i )
    {
        Extra_ProgressBarUpdate( pProgress, i, NULL );
        pMiter = Abc_NtkSensitivityMiter( pNtk, i );
        RetValue = Abc_NtkIvyProve( &pMiter, pParams );
        if ( RetValue == -1 ) 
            Vec_IntPush( vResult, i );
        else if ( RetValue == 0 )
        {
            int * pSimInfo = Abc_NtkVerifySimulatePattern( pMiter, pMiter->pModel );
            if ( pSimInfo[0] != 1 )
                printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
            ABC_FREE( pSimInfo );
            Vec_IntPush( vResult, i );
        }
        Abc_NtkDelete( pMiter );
    }
    Extra_ProgressBarStop( pProgress );
    if ( fVerbose )
    {
        printf( "The outputs are sensitive to %d (out of %d) inputs:\n", 
            Vec_IntSize(vResult), Abc_NtkCiNum(pNtk) );
        Vec_IntForEachEntry( vResult, RetValue, i )
            printf( "%d ", RetValue );
        printf( "\n" );
    }
    return vResult;
}
Vec_Int_t * Abc_NtkSensitivity ( Abc_Ntk_t * pNtk , int nConfLim , int fVerbose ) { ProgressBar * pProgress ; Prove_Params_t Params , * pParams = & Params ; Vec_Int_t * vResult = NULL ; Abc_Ntk_t * pMiter ; Abc_Obj_t * pObj ; int RetValue , i ; assert ( Abc_NtkIsStrash ( pNtk ) ) ; assert ( Abc_NtkLatchNum ( pNtk ) == 0 ) ; Prove_ParamsSetDefault ( pParams ) ; pParams -> nItersMax = 3 ; pParams -> nMiteringLimitLast = nConfLim ; vResult = Vec_IntAlloc ( 100 ) ; pProgress = Extra_ProgressBarStart ( stdout , Abc_NtkCiNum ( pNtk ) ) ; Abc_NtkForEachCi ( pNtk , pObj , i ) { Extra_ProgressBarUpdate ( pProgress , i , NULL ) ; pMiter = Abc_NtkSensitivityMiter ( pNtk , i ) ; RetValue = Abc_NtkIvyProve ( & pMiter , pParams ) ; if ( RetValue == -1 ) Vec_IntPush ( vResult , i ) ; else if ( RetValue == 0 ) { int * pSimInfo = Abc_NtkVerifySimulatePattern ( pMiter , pMiter -> pModel ) ; if ( pSimInfo [ 0 ] != 1 ) printf ( " \n " ) ; ABC_FREE ( pSimInfo ) ; Vec_IntPush ( vResult , i ) ; } Abc_NtkDelete ( pMiter ) ; } Extra_ProgressBarStop ( pProgress ) ; if ( fVerbose ) { printf ( " \n " , Vec_IntSize ( vResult ) , Abc_NtkCiNum ( pNtk ) ) ; Vec_IntForEachEntry ( vResult , RetValue , i ) printf ( " " , RetValue ) ; printf ( " \n " ) ; } return vResult ; }
Function
Synopsis    [Computing sensitivity of POs to POs under constraints.]
Function Synopsis [ Computing sensitivity of POs to POs under constraints . ]
// set up solving parameters // iterate through the PIs // generate the sensitivity miter // solve the miter using CEC engine // undecided //            else //                printf( "Networks are NOT EQUIVALENT.\n" );