abc/src/base/wlc/wlcAbs2.c
/**Function*************************************************************

  Synopsis    [Performs abstraction.]

  Description [Derives initial abstraction based on user-specified
  parameter values, which tell what is the smallest bit-width of a
  primitive that is being abstracted away.  Currently only add/sub,
  mul/div, mux, and flop are supported with individual parameters.
  The second step is to refine the initial abstraction until the
  point when the property is proved.]
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
Function
Synopsis    [Performs abstraction.]

Description [Derives initial abstraction based on user-specified
parameter values, which tell what is the smallest bit-width of a
primitive that is being abstracted away.  Currently only add/sub,
mul/div, mux, and flop are supported with individual parameters.
The second step is to refine the initial abstraction until the
point when the property is proved.]




Function Synopsis [ Performs abstraction . ] Description [ Derives initial abstraction based on user - specified parameter values which tell what is the smallest bit - width of a primitive that is being abstracted away . Currently only add / sub mul / div mux and flop are supported with individual parameters . The second step is to refine the initial abstraction until the point when the property is proved . ]
int Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
{
    abctime clk = Abc_Clock();
    int nIters, nNodes, nDcFlops, RetValue = -1;
    Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) );
    Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
    Pdr_ManSetDefaultParams( pPdrPars );
    pPdrPars->fUseAbs    = 1;   
    pPdrPars->fCtgs      = 1;   
    pPdrPars->fSkipDown  = 0;   
    pPdrPars->fVerbose   = pPars->fPdrVerbose;
    for ( nIters = 1; nIters < pPars->nIterMax; nIters++ )
    {
        Aig_Man_t * pAig;
        Abc_Cex_t * pCex;
        Vec_Int_t * vPisNew, * vRefine;  
        Gia_Man_t * pGia, * pTemp;
        Wlc_Ntk_t * pAbs;
        if ( pPars->fVerbose )
            printf( "\nIteration %d:\n", nIters );
        pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, pPars->fVerbose );
        pGia = Wlc_NtkBitBlast( pAbs, NULL );
        nDcFlops = Wlc_NtkDcFlopNum(pAbs);
        if ( nDcFlops > 0 ) 
        {
            pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops );
            Gia_ManStop( pTemp );
        }
        if ( pPars->fXorOutput )
        {
            pGia = Gia_ManTransformMiter2( pTemp = pGia );
            Gia_ManStop( pTemp );
        }
        if ( pPars->fVerbose )
        {
            printf( "Derived abstraction with %d objects and %d PPIs. Bit-blasted AIG stats are:\n", Wlc_NtkObjNum(pAbs), Vec_IntSize(vPisNew) ); 
            Gia_ManPrintStats( pGia, NULL );
        }
        Wlc_NtkFree( pAbs );
        pAig = Gia_ManToAigSimple( pGia );
        RetValue = Pdr_ManSolve( pAig, pPdrPars );
        pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
        Aig_ManStop( pAig );
        if ( pCex == NULL ) 
        {
            assert( RetValue ); 
            Gia_ManStop( pGia );
            Vec_IntFree( vPisNew );
            break;
        }
        vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
        Gia_ManStop( pGia );
        Vec_IntFree( vPisNew );
        if ( vRefine == NULL ) 
        {
            Abc_CexFree( pCex ); 
            break;
        }
        nNodes = Wlc_NtkRemoveFromAbstraction( p, vRefine, vUnmark );
        if ( pPars->fVerbose )
            printf( "Refinement of CEX in frame %d came up with %d un-abstacted PPIs, whose MFFCs include %d objects.\n", pCex->iFrame, Vec_IntSize(vRefine), nNodes );
        Vec_IntFree( vRefine );
        Abc_CexFree( pCex );
    }
    Vec_BitFree( vUnmark );
    if ( pPars->fVerbose )
        printf( "\n" );
    printf( "Abstraction " );
    if ( RetValue == 0 )
        printf( "resulted in a real CEX" );
    else if ( RetValue == 1 )
        printf( "is successfully proved" );
    else 
        printf( "timed out" );
    printf( " after %d iterations. ", nIters );
    Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
    return RetValue;
}
int Wlc_NtkAbsCore2 ( Wlc_Ntk_t * p , Wlc_Par_t * pPars ) { abctime clk = Abc_Clock ( ) ; int nIters , nNodes , nDcFlops , RetValue = -1 ; Vec_Bit_t * vUnmark = Vec_BitStart ( Wlc_NtkObjNumMax ( p ) ) ; Pdr_Par_t PdrPars , * pPdrPars = & PdrPars ; Pdr_ManSetDefaultParams ( pPdrPars ) ; pPdrPars -> fUseAbs = 1 ; pPdrPars -> fCtgs = 1 ; pPdrPars -> fSkipDown = 0 ; pPdrPars -> fVerbose = pPars -> fPdrVerbose ; for ( nIters = 1 ; nIters < pPars -> nIterMax ; nIters ++ ) { Aig_Man_t * pAig ; Abc_Cex_t * pCex ; Vec_Int_t * vPisNew , * vRefine ; Gia_Man_t * pGia , * pTemp ; Wlc_Ntk_t * pAbs ; if ( pPars -> fVerbose ) printf ( " \n \n " , nIters ) ; pAbs = Wlc_NtkAbs ( p , pPars , vUnmark , & vPisNew , pPars -> fVerbose ) ; pGia = Wlc_NtkBitBlast ( pAbs , NULL ) ; nDcFlops = Wlc_NtkDcFlopNum ( pAbs ) ; if ( nDcFlops > 0 ) { pGia = Gia_ManPermuteInputs ( pTemp = pGia , Wlc_NtkCountObjBits ( p , vPisNew ) , nDcFlops ) ; Gia_ManStop ( pTemp ) ; } if ( pPars -> fXorOutput ) { pGia = Gia_ManTransformMiter2 ( pTemp = pGia ) ; Gia_ManStop ( pTemp ) ; } if ( pPars -> fVerbose ) { printf ( " \n " , Wlc_NtkObjNum ( pAbs ) , Vec_IntSize ( vPisNew ) ) ; Gia_ManPrintStats ( pGia , NULL ) ; } Wlc_NtkFree ( pAbs ) ; pAig = Gia_ManToAigSimple ( pGia ) ; RetValue = Pdr_ManSolve ( pAig , pPdrPars ) ; pCex = pAig -> pSeqModel ; pAig -> pSeqModel = NULL ; Aig_ManStop ( pAig ) ; if ( pCex == NULL ) { assert ( RetValue ) ; Gia_ManStop ( pGia ) ; Vec_IntFree ( vPisNew ) ; break ; } vRefine = Wlc_NtkAbsRefinement ( p , pGia , pCex , vPisNew ) ; Gia_ManStop ( pGia ) ; Vec_IntFree ( vPisNew ) ; if ( vRefine == NULL ) { Abc_CexFree ( pCex ) ; break ; } nNodes = Wlc_NtkRemoveFromAbstraction ( p , vRefine , vUnmark ) ; if ( pPars -> fVerbose ) printf ( " \n " , pCex -> iFrame , Vec_IntSize ( vRefine ) , nNodes ) ; Vec_IntFree ( vRefine ) ; Abc_CexFree ( pCex ) ; } Vec_BitFree ( vUnmark ) ; if ( pPars -> fVerbose ) printf ( " \n " ) ; printf ( " " ) ; if ( RetValue == 0 ) printf ( " " ) ; else if ( RetValue == 1 ) printf ( " " ) ; else printf ( " " ) ; printf ( " " , nIters ) ; Abc_PrintTime ( 1 , " " , Abc_Clock ( ) - clk ) ; return RetValue ; }
Function
Synopsis    [Performs abstraction.]
Function Synopsis [ Performs abstraction . ]
// start the bitmap to mark objects that cannot be abstracted because of refinement // currently, this bitmap is empty because abstraction begins without refinement // set up parameters to run PDR // use 'pdr -t'  (on-the-fly abstraction) // use 'pdr -nc' (improved generalization) // use 'pdr -nc' (improved generalization) //pPdrPars->nRestLimit = 500; // reset queue or proof-obligations when it gets larger than this // perform refinement iterations // get abstracted GIA and the set of pseudo-PIs (vPisNew) // if the abstraction has flops with DC-init state, // new PIs were introduced by bit-blasting at the end of the PI list // here we move these variables to be *before* PPIs, because // PPIs are supposed to be at the end of the PI list for refinement // DC-init flops are present // if the word-level outputs have to be XORs, this is a place to do it // try to prove abstracted GIA by converting it to AIG and calling PDR // consider outcomes // proved or undecided // perform refinement // real CEX // return CEX in the future // update the set of objects to be un-abstracted // report the result