working on pdr with wla

3 files changed, 113 insertions, 1 deletions

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index 91dc0573..9ca56917 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -277,6 +277,7 @@ static inline Wlc_Obj_t *  Wlc_ObjCo2PoFo( Wlc_Ntk_t * p, int iCoId )
 
 /*=== wlcAbs.c ========================================================*/
 extern int            Wlc_NtkAbsCore( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
+extern int            Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
 /*=== wlcAbs2.c ========================================================*/
 extern int            Wlc_NtkAbsCore2( Wlc_Ntk_t * p, Wlc_Par_t * pPars );
 /*=== wlcBlast.c ========================================================*/
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index 318df4dd..cfd1155d 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -285,6 +285,117 @@ static int Wlc_NtkRemoveFromAbstraction( Wlc_Ntk_t * p, Vec_Int_t * vRefine, Vec
 
 /**Function*************************************************************
 
+  Synopsis    [Performs PDR with word-level abstraction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
+{
+    abctime clk = Abc_Clock();
+    int nIters, nNodes, nDcFlops, RetValue = -1;
+    // start the bitmap to mark objects that cannot be abstracted because of refinement
+    // currently, this bitmap is empty because abstraction begins without refinement
+    Vec_Bit_t * vUnmark = Vec_BitStart( Wlc_NtkObjNumMax(p) );
+    // set up parameters to run PDR
+    Pdr_Par_t PdrPars, * pPdrPars = &PdrPars;
+    Pdr_ManSetDefaultParams( pPdrPars );
+    pPdrPars->fVerbose   = pPars->fPdrVerbose;
+    
+    // perform refinement iterations
+    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 );
+
+        // get abstracted GIA and the set of pseudo-PIs (vPisNew)
+        pAbs = Wlc_NtkAbs( p, pPars, vUnmark, &vPisNew, pPars->fVerbose );
+        pGia = Wlc_NtkBitBlast( pAbs, NULL, -1, 0, 0, 0, 0 );
+
+        // 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
+        nDcFlops = Wlc_NtkDcFlopNum(pAbs);
+        if ( nDcFlops > 0 ) // DC-init flops are present
+        {
+            pGia = Gia_ManPermuteInputs( pTemp = pGia, Wlc_NtkCountObjBits(p, vPisNew), nDcFlops );
+            Gia_ManStop( pTemp );
+        }
+        // if the word-level outputs have to be XORs, this is a place to do it
+        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 );
+
+        // try to prove abstracted GIA by converting it to AIG and calling PDR
+        pAig = Gia_ManToAigSimple( pGia );
+        RetValue = Pdr_ManSolve( pAig, pPdrPars );
+        pCex = pAig->pSeqModel; pAig->pSeqModel = NULL;
+        Aig_ManStop( pAig );
+
+        // consider outcomes
+        if ( pCex == NULL ) 
+        {
+            assert( RetValue ); // proved or undecided
+            Gia_ManStop( pGia );
+            Vec_IntFree( vPisNew );
+            break;
+        }
+
+        // perform refinement
+        vRefine = Wlc_NtkAbsRefinement( p, pGia, pCex, vPisNew );
+        Gia_ManStop( pGia );
+        Vec_IntFree( vPisNew );
+        if ( vRefine == NULL ) // real CEX
+        {
+            Abc_CexFree( pCex ); // return CEX in the future
+            break;
+        }
+
+        // update the set of objects to be un-abstracted
+        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 );
+    // report the result
+    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;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs abstraction.]
 
   Description [Derives initial abstraction based on user-specified
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 6b542b94..e980752b 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -541,7 +541,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( 1, "Abc_CommandCone(): There is no current design.\n" );
         return 0;
     }
-    Wlc_NtkAbsCore( pNtk, pPars );
+    Wlc_NtkPdrAbs( pNtk, pPars );
     return 0;
 usage:
     Abc_Print( -2, "usage: %%pdra [-AMXFI num] [-xvwh]\n" );