merge pyabc changes into mainline

3 files changed, 134 insertions, 14 deletions

diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
index 194add25..938a66e2 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -22,6 +22,7 @@
 #include "ssw.h"
 #include "fra.h"
 #include "bbr.h"
+#include "pdr.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -173,15 +174,32 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
 { 
     extern int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames );
     Vec_Int_t * vFlopsNew;
-    int i, Entry;
+    int i, Entry, RetValue;
     *piRetValue = -1;
     if ( fUseDprove && Aig_ManRegNum(pAbs) > 0 )
     {
+/*
         Fra_Sec_t SecPar, * pSecPar = &SecPar;
-        int RetValue;
         Fra_SecSetDefaultParams( pSecPar );
         pSecPar->fVerbose       = fVerbose;
         RetValue = Fra_FraigSec( pAbs, pSecPar, NULL );
+*/
+        Abc_Cex_t * pCex = NULL;
+        Aig_Man_t * pAbsOrpos = Saig_ManDupOrpos( pAbs );
+        Pdr_Par_t Pars, * pPars = &Pars;
+        Pdr_ManSetDefaultParams( pPars );
+        pPars->nTimeOut = 10;
+        pPars->fVerbose = fVerbose;
+        if ( pPars->fVerbose )
+            printf( "Running property directed reachability...\n" );
+        RetValue = Pdr_ManSolve( pAbsOrpos, pPars, &pCex );
+        if ( pCex )
+            pCex->iPo = Ssw_SmlFindOutputCounterExample( pAbs, pCex );
+        Aig_ManStop( pAbsOrpos );
+        pAbs->pSeqModel = pCex;
+        if ( RetValue )
+            *piRetValue = 1;
+
     }
     else if ( fUseBdds && (Aig_ManRegNum(pAbs) > 0 && Aig_ManRegNum(pAbs) <= 80) )
     {
@@ -195,7 +213,9 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
         pPars->fReorderImage = 1;
         pPars->fVerbose      = fVerbose;
         pPars->fSilent       = 0;
-        Aig_ManVerifyUsingBdds( pAbs, pPars );
+        RetValue = Aig_ManVerifyUsingBdds( pAbs, pPars );
+        if ( RetValue )
+            *piRetValue = 1;
     }
     else 
     {
diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c
index 4a23ecf3..fad77020 100644
--- a/src/aig/saig/saigPhase.c
+++ b/src/aig/saig/saigPhase.c
@@ -222,7 +222,7 @@ int Saig_TsiStateHash( unsigned * pState, int nWords, int nTableSize )
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_TsiCountNonXValuedRegisters( Saig_Tsim_t * p, int nWords, int nPref )
+int Saig_TsiCountNonXValuedRegisters( Saig_Tsim_t * p, int nPref )
 {
     unsigned * pState;
     int nRegs = p->pAig->nRegs;
@@ -242,6 +242,53 @@ int Saig_TsiCountNonXValuedRegisters( Saig_Tsim_t * p, int nWords, int nPref )
             Vec_IntPush( p->vNonXRegs, i );
     }
     return Vec_IntSize(p->vNonXRegs);
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Computes flops that are stuck-at constant.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Saig_TsiComputeTransient( Saig_Tsim_t * p, int nPref )
+{
+    Vec_Int_t * vCounters;
+    unsigned * pState;
+    int ValueThis, ValuePrev = -1, StepPrev = -1;
+    int i, k, nRegs = p->pAig->nRegs;
+    vCounters = Vec_IntStart( nPref );
+    for ( i = 0; i < nRegs; i++ )
+    {
+        Vec_PtrForEachEntry( unsigned *, p->vStates, pState, k )
+        {
+            ValueThis = (Aig_InfoHasBit( pState, 2 * i + 1 ) << 1) | Aig_InfoHasBit( pState, 2 * i );
+//printf( "%s", (ValueThis == 1)? "0" : ((ValueThis == 2)? "1" : "x") );
+            assert( ValueThis != 0 );
+            if ( ValuePrev != ValueThis )
+            {
+                ValuePrev = ValueThis;
+                StepPrev  = k;
+            }
+        }
+//printf( "\n" );
+        if ( ValueThis == SAIG_XVSX )
+            continue;
+        if ( StepPrev >= nPref )
+            continue;
+        Vec_IntAddToEntry( vCounters, StepPrev, 1 );
+    }
+    Vec_IntForEachEntry( vCounters, ValueThis, i )
+    {
+        if ( ValueThis == 0 )
+            continue;
+//        printf( "%3d : %3d\n", i, ValueThis );
+    }
+    return vCounters;
 }
 
 /**Function*************************************************************
@@ -821,7 +868,7 @@ int Saig_ManPhaseFrameNum( Aig_Man_t * p, Vec_Int_t * vInits )
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose )
+int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose, Vec_Int_t ** pvTrans )
 {
     Saig_Tsim_t * pTsi;
     int nFrames, nPrefix, nNonXRegs;
@@ -835,7 +882,11 @@ int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose )
     // derive information
     nPrefix   = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
     nFrames   = Vec_PtrSize(pTsi->vStates) - 1 - nPrefix;
-    nNonXRegs = Saig_TsiCountNonXValuedRegisters( pTsi, pTsi->nWords, nPrefix );
+    nNonXRegs = Saig_TsiCountNonXValuedRegisters( pTsi, nPrefix );
+
+    if ( pvTrans )
+        *pvTrans = Saig_TsiComputeTransient( pTsi, nPrefix );
+
     // print statistics
     if ( fVerbose )
         printf( "Lead = %5d. Loop = %5d.  Total flops = %5d. Binary flops = %5d.\n", nPrefix, nFrames, p->nRegs, nNonXRegs );
@@ -871,7 +922,7 @@ Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrame
     // derive information
     pTsi->nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
     pTsi->nCycle = Vec_PtrSize(pTsi->vStates) - 1 - pTsi->nPrefix;
-    pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, pTsi->nWords, ABC_MIN(pTsi->nPrefix,nPref));
+    pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, ABC_MIN(pTsi->nPrefix,nPref));
     // print statistics
     if ( fVerbose )
     {
@@ -927,7 +978,7 @@ Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose )
     // derive information
     pTsi->nPrefix = Saig_TsiComputePrefix( pTsi, (unsigned *)Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
     pTsi->nCycle = Vec_PtrSize(pTsi->vStates) - 1 - pTsi->nPrefix;
-    pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, pTsi->nWords, 0);
+    pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, 0);
     // print statistics
     if ( fVerbose )
     {
diff --git a/src/aig/saig/saigTempor.c b/src/aig/saig/saigTempor.c
index 80bde75c..74f4a9d3 100644
--- a/src/aig/saig/saigTempor.c
+++ b/src/aig/saig/saigTempor.c
@@ -147,6 +147,32 @@ Aig_Man_t * Saig_ManTemporDecompose( Aig_Man_t * pAig, int nFrames )
 
 /**Function*************************************************************
 
+  Synopsis    [Find index of first non-zero entry.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Vec_IntLastNonZeroBeforeLimit( Vec_Int_t * vTemp, int Limit )
+{
+    int Entry, i;
+    if ( vTemp == NULL )
+        return -1;
+    Vec_IntForEachEntryReverse( vTemp, Entry, i )
+    {
+        if ( i >= Limit )
+            continue;
+        if ( Entry )
+            return i;
+    }
+    return -1;
+}
+
+/**Function*************************************************************
+
   Synopsis    []
 
   Description []
@@ -156,19 +182,33 @@ Aig_Man_t * Saig_ManTemporDecompose( Aig_Man_t * pAig, int nFrames )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fVerbose, int fVeryVerbose )
+Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nConfLimit, int fUseBmc, int fUseTransSigs, int fVerbose, int fVeryVerbose )
 { 
-    extern int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose );
+    extern int Saig_ManPhasePrefixLength( Aig_Man_t * p, int fVerbose, int fVeryVerbose, Vec_Int_t ** pvTrans );
+
+    Vec_Int_t * vTransSigs = NULL;
     int RetValue, nFramesFinished = -1;
     assert( nFrames >= 0 ); 
     if ( nFrames == 0 )
     {
-        nFrames = Saig_ManPhasePrefixLength( pAig, fVerbose, fVeryVerbose );
+        nFrames = Saig_ManPhasePrefixLength( pAig, fVerbose, fVeryVerbose, &vTransSigs );
         if ( nFrames == 1 )
         {
+            Vec_IntFreeP( &vTransSigs );
             printf( "The leading sequence has length 1. Temporal decomposition is not performed.\n" );
             return NULL;
         }
+        if ( fUseTransSigs )
+        {
+            int Entry, i, iLast = -1;
+            Vec_IntForEachEntry( vTransSigs, Entry, i )
+                iLast = Entry ? i :iLast;
+            if ( iLast > 0 && iLast < nFrames )
+            {
+                Abc_Print( 1, "Reducing frame count from %d to %d to fit the last transient.\n", nFrames, iLast );
+                nFrames = iLast;
+            }
+        }
         Abc_Print( 1, "Using computed frame number (%d).\n", nFrames );
     }
     else
@@ -176,18 +216,27 @@ Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nCon
     // run BMC2
     if ( fUseBmc )
     {
-        RetValue = Saig_BmcPerform( pAig, 0, nFrames, 5000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished );
+        RetValue = Saig_BmcPerform( pAig, 0, nFrames, 2000, TimeOut, nConfLimit, 0, fVerbose, 0, &nFramesFinished );
         if ( RetValue == 0 )
         {
+            Vec_IntFreeP( &vTransSigs );
             printf( "A cex found in the first %d frames.\n", nFrames );
             return NULL;
         }
         if ( nFramesFinished < nFrames )
         {
-            printf( "BMC for %d frames could not be completed. A cex may exist!\n", nFrames );
-            return NULL;
+            int iLastBefore = Vec_IntLastNonZeroBeforeLimit( vTransSigs, nFramesFinished );
+            if ( iLastBefore < 1 || !fUseTransSigs )
+            {
+                Vec_IntFreeP( &vTransSigs );
+                printf( "BMC for %d frames could not be completed. A cex may exist!\n", nFrames );
+                return NULL;
+            }
+            assert( iLastBefore < nFramesFinished );
+            printf( "BMC succeeded to frame %d. Adjusting frame count to be (%d) based on the last transient signal.\n", nFramesFinished, iLastBefore );
         }
     }
+    Vec_IntFreeP( &vTransSigs );
     return Saig_ManTemporDecompose( pAig, nFrames );
 }