Version abc70911

14 files changed, 491 insertions, 38 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index d5c2a4db..fe237142 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -50,6 +50,7 @@ typedef struct Aig_Obj_t_            Aig_Obj_t;
 typedef struct Aig_MmFixed_t_        Aig_MmFixed_t;    
 typedef struct Aig_MmFlex_t_         Aig_MmFlex_t;     
 typedef struct Aig_MmStep_t_         Aig_MmStep_t;     
+typedef struct Aig_TMan_t_           Aig_TMan_t;
 
 // object types
 typedef enum { 
@@ -131,6 +132,7 @@ struct Aig_Man_t_
     Aig_Obj_t **     pObjCopies;     // mapping of AIG nodes into FRAIG nodes
     void (*pImpFunc) (void*, void*); // implication checking precedure
     void *           pImpData;       // implication checking data
+    Aig_TMan_t *     pManTime;       // the timing manager
     // timing statistics
     int              time1;
     int              time2;
@@ -520,6 +522,19 @@ extern char *          Aig_MmStepEntryFetch( Aig_MmStep_t * p, int nBytes );
 extern void            Aig_MmStepEntryRecycle( Aig_MmStep_t * p, char * pEntry, int nBytes );
 extern int             Aig_MmStepReadMemUsage( Aig_MmStep_t * p );
 
+/*=== aigTime.c ===========================================================*/
+extern Aig_TMan_t *    Aig_TManStart( int nPis, int nPos );
+extern void            Aig_TManStop( Aig_TMan_t * p );
+extern void            Aig_TManCreateBox( Aig_TMan_t * p, int * pPis, int nPis, int * pPos, int nPos, float * pPiTimes, float * pPoTimes );
+extern void            Aig_TManSetPiDelay( Aig_TMan_t * p, int iPi, float Delay );
+extern void            Aig_TManSetPoDelay( Aig_TMan_t * p, int iPo, float Delay );
+extern void            Aig_TManSetPiArrival( Aig_TMan_t * p, int iPi, float Delay );
+extern void            Aig_TManSetPoRequired( Aig_TMan_t * p, int iPo, float Delay );
+extern void            Aig_TManIncrementTravId( Aig_TMan_t * p );
+extern float           Aig_TManGetPiArrival( Aig_TMan_t * p, int iPi );
+extern float           Aig_TManGetPoRequired( Aig_TMan_t * p, int iPo );
+
+
 #ifdef __cplusplus
 }
 #endif
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 30a7991a..1e0ee278 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -229,6 +229,9 @@ void Aig_ManStop( Aig_Man_t * p )
     // print time
     if ( p->time1 ) { PRT( "time1", p->time1 ); }
     if ( p->time2 ) { PRT( "time2", p->time2 ); }
+    // delete timing
+    if ( p->pManTime )
+        Aig_TManStop( p->pManTime );
     // delete fanout
     if ( p->pFanData ) 
         Aig_ManFanoutStop( p );
@@ -304,6 +307,8 @@ void Aig_ManPrintStats( Aig_Man_t * p )
 //    printf( "Lev = %3d. ",  Aig_ManCountLevels(p) );
     printf( "Max = %7d. ",  Aig_ManObjNumMax(p) );
     printf( "Lev = %3d. ",  Aig_ManLevels(p) );
+    if ( Aig_ManRegNum(p) )
+        printf( "Lat = %5d. ", Aig_ManRegNum(p) );
     printf( "\n" );
 }
 
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index 166377bf..2f00a7eb 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -157,12 +157,21 @@ int Aig_ManSeqCleanup( Aig_Man_t * p )
         Aig_ManForEachPi( p, pObj, i )
             if ( Aig_ObjIsTravIdCurrent(p, pObj) )
                 Vec_PtrPush( vCis, pObj );
+            else
+            {
+                Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
+//                Aig_ManRecycleMemory( p, pObj );
+            }
         vCos = Vec_PtrAlloc( Aig_ManPoNum(p) );
         Aig_ManForEachPo( p, pObj, i )
             if ( Aig_ObjIsTravIdCurrent(p, pObj) )
                 Vec_PtrPush( vCos, pObj );
             else
+            {
                 Aig_ObjDisconnect( p, pObj );
+                Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
+//                Aig_ManRecycleMemory( p, pObj );
+            }
         // remember the number of true PIs/POs
         nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p);
         nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p);
diff --git a/src/aig/aig/aigTime.c b/src/aig/aig/aigTime.c
new file mode 100644
index 00000000..42f5f575
--- /dev/null
+++ b/src/aig/aig/aigTime.c
@@ -0,0 +1,299 @@
+/**CFile****************************************************************
+
+  FileName    [aigTime.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [AIG package.]
+
+  Synopsis    [Representation of timing information.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: aigTime.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Aig_TBox_t_           Aig_TBox_t;
+typedef struct Aig_TObj_t_           Aig_TObj_t;
+
+// timing manager
+struct Aig_TMan_t_
+{
+    Vec_Ptr_t *      vBoxes;         // the timing boxes
+    Aig_MmFlex_t *   pMemObj;        // memory manager for boxes
+    int              nTravIds;       // traversal ID of the manager
+    int              nPis;           // the number of PIs
+    int              nPos;           // the number of POs
+    Aig_TObj_t *     pPis;           // timing info for the PIs
+    Aig_TObj_t *     pPos;           // timing info for the POs
+};
+
+// timing box
+struct Aig_TBox_t_
+{
+    int              iBox;           // the unique ID of this box
+    int              TravId;         // traversal ID of this box
+    int              nInputs;        // the number of box inputs 
+    int              nOutputs;       // the number of box outputs
+    int              Inouts[0];      // the int numbers of PIs and POs
+};
+
+// timing object
+struct Aig_TObj_t_
+{
+    int              iObj2Box;       // mapping of the object into its box
+    float            timeOffset;     // the static timing of the node
+    float            timeActual;     // the actual timing of the node
+};
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the network manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_TMan_t * Aig_TManStart( int nPis, int nPos )
+{
+    Aig_TMan_t * p;
+    int i;
+    p = ALLOC( Aig_TMan_t, 1 );
+    memset( p, 0, sizeof(Aig_TMan_t) );
+    p->pMemObj = Aig_MmFlexStart();
+    p->vBoxes  = Vec_PtrAlloc( 100 );
+    Vec_PtrPush( p->vBoxes, NULL );
+    p->nPis = nPis;
+    p->nPos = nPos;
+    p->pPis = ALLOC( Aig_TObj_t, nPis );
+    memset( p->pPis, 0, sizeof(Aig_TObj_t) * nPis );
+    p->pPos = ALLOC( Aig_TObj_t, nPos );
+    memset( p->pPos, 0, sizeof(Aig_TObj_t) * nPos );
+    for ( i = 0; i < nPis; i++ )
+        p->pPis[i].iObj2Box = -1;
+    for ( i = 0; i < nPos; i++ )
+        p->pPos[i].iObj2Box = -1;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the network manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TManStop( Aig_TMan_t * p )
+{
+    Vec_PtrFree( p->vBoxes );
+    Aig_MmFlexStop( p->pMemObj, 0 );
+    free( p->pPis );
+    free( p->pPos );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the new timing box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TManCreateBox( Aig_TMan_t * p, int * pPis, int nPis, int * pPos, int nPos, float * pPiTimes, float * pPoTimes )
+{
+    Aig_TBox_t * pBox;
+    int i;
+    pBox = (Aig_TBox_t *)Aig_MmFlexEntryFetch( p->pMemObj, sizeof(Aig_TBox_t) + sizeof(int) * (nPis+nPos) );
+    memset( pBox, 0, sizeof(Aig_TBox_t) );
+    pBox->iBox = Vec_PtrSize( p->vBoxes );
+    Vec_PtrPush( p->vBoxes, pBox );
+    pBox->nInputs = nPis;
+    pBox->nOutputs = nPos;
+    for ( i = 0; i < nPis; i++ )
+    {
+        assert( pPis[i] < p->nPis );
+        pBox->Inouts[i] = pPis[i];
+        Aig_TManSetPiArrival( p, pPis[i], pPiTimes[i] );
+        p->pPis[pPis[i]].iObj2Box = pBox->iBox;
+    }
+    for ( i = 0; i < nPos; i++ )
+    {
+        assert( pPos[i] < p->nPos );
+        pBox->Inouts[nPis+i] = pPos[i];
+        Aig_TManSetPoRequired( p, pPos[i], pPoTimes[i] );
+        p->pPos[pPos[i]].iObj2Box = pBox->iBox;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the new timing box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TManSetPiDelay( Aig_TMan_t * p, int iPi, float Delay )
+{
+    assert( iPi < p->nPis );
+    p->pPis[iPi].timeActual = Delay;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the new timing box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TManSetPoDelay( Aig_TMan_t * p, int iPo, float Delay )
+{
+    assert( iPo < p->nPos );
+    p->pPos[iPo].timeActual = Delay;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the new timing box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TManSetPiArrival( Aig_TMan_t * p, int iPi, float Delay )
+{
+    assert( iPi < p->nPis );
+    p->pPis[iPi].timeOffset = Delay;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the new timing box.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TManSetPoRequired( Aig_TMan_t * p, int iPo, float Delay )
+{
+    assert( iPo < p->nPos );
+    p->pPos[iPo].timeOffset = Delay;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Increments the trav ID of the manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_TManIncrementTravId( Aig_TMan_t * p )
+{
+    p->nTravIds++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns PI arrival time.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Aig_TManGetPiArrival( Aig_TMan_t * p, int iPi )
+{
+    Aig_TBox_t * pBox;
+    Aig_TObj_t * pObj;
+    float DelayMax;
+    int i;
+    assert( iPi < p->nPis );
+    if ( p->pPis[iPi].iObj2Box < 0 )
+        return p->pPis[iPi].timeOffset;
+    pBox = Vec_PtrEntry( p->vBoxes, p->pPis[iPi].iObj2Box );
+    // check if box timing is updated
+    if ( pBox->TravId == p->nTravIds )
+        return p->pPis[iPi].timeOffset;
+    pBox->TravId = p->nTravIds;
+    // update box timing
+    DelayMax = -1.0e+20F;
+    for ( i = 0; i < pBox->nOutputs; i++ )
+    {
+        pObj = p->pPos + pBox->Inouts[pBox->nInputs+i];
+        DelayMax = AIG_MAX( DelayMax, pObj->timeActual + pObj->timeOffset );
+    }
+    for ( i = 0; i < pBox->nInputs; i++ )
+    {
+        pObj = p->pPis + pBox->Inouts[i];
+        pObj->timeActual = DelayMax + pObj->timeOffset;
+    }
+    return p->pPis[iPi].timeActual;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns PO required time.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+float Aig_TManGetPoRequired( Aig_TMan_t * p, int iPo )
+{
+    return 0.0;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index cd6bdfd4..210af244 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -111,6 +111,7 @@ struct Fra_Sml_t_
     int              nWordsFrame;       // the number of words in each time frame
     int              nWordsTotal;       // the total number of words at a node
     int              nWordsPref;        // the number of word in the prefix
+    int              fNonConstOut;      // have seen a non-const-0 output during simulation
     int              nSimRounds;        // statistics
     int              timeSim;           // statistics
     unsigned         pData[0];          // simulation data for the nodes
@@ -256,7 +257,7 @@ extern void                Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pN
 /*=== fraInd.c ========================================================*/
 extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter );
 /*=== fraLcr.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fVerbose, int * pnIter );
+extern Aig_Man_t *         Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter );
 /*=== fraMan.c ========================================================*/
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
 extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c
index 1df25c0a..1140f3a4 100644
--- a/src/aig/fra/fraBmc.c
+++ b/src/aig/fra/fraBmc.c
@@ -128,7 +128,7 @@ void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc )
     {
         if ( Imp == 0 )
             continue;
-        Left = Fra_ImpLeft(Imp);
+        Left  = Fra_ImpLeft(Imp);
         Right = Fra_ImpRight(Imp);
         // get the corresponding nodes
         pLeft  = Aig_ManObj( pBmc->pAig, Left );
@@ -136,7 +136,7 @@ void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc )
         // iterate through the timeframes
         for ( f = pBmc->nPref; f < pBmc->nFramesAll; f++ )
         {
-            // get timeframes nodes
+            // get timeframe nodes
             pLeftT  = Bmc_ObjFrames( pLeft, f );
             pRightT = Bmc_ObjFrames( pRight, f );
             // get the corresponding FRAIG nodes
@@ -148,14 +148,21 @@ void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc )
             // check equality
             if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
             {
-                if ( fComplL != fComplR )
-                    Vec_IntWriteEntry( pBmc->vImps, i, 0 );
+                if ( fComplL == fComplR ) // x => x  - always true
+                    continue;
+                assert( fComplL != fComplR );
+                // consider 4 possibilities:
+                // NOT(1) => 1    or   0 => 1  - always true
+                // 1 => NOT(1)    or   1 => 0  - never true
+                // NOT(x) => x    or   x       - not always true
+                // x => NOT(x)    or   NOT(x)  - not always true
+                if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication
+                    continue;
+                // disproved implication
+                Vec_IntWriteEntry( pBmc->vImps, i, 0 ); 
                 break;
             }
             // check the implication 
-            // - if true, a clause is added
-            // - if false, a cex is simulated
-            // make sure the implication is refined
             if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) != 1 )
             {
                 Vec_IntWriteEntry( pBmc->vImps, i, 0 );
@@ -320,7 +327,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
 //        Fra_ClassesPrint( p->pCla, 0 );
         printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
             Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
-        if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) > 0 )
+        if ( p->pCla->vImps )
             printf( "Imp = %5d. ", nImpsOld );
         printf( "\n" );
     }
@@ -338,7 +345,7 @@ void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
 //        Fra_ClassesPrint( p->pCla, 0 );
         printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
             Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
-        if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) > 0 )
+        if ( p->pCla->vImps )
             printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) );
         printf( "\n" );
     }
diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c
index d8bf4e48..a5fc7d58 100644
--- a/src/aig/fra/fraImp.c
+++ b/src/aig/fra/fraImp.c
@@ -96,7 +96,7 @@ static inline int Sml_NodeCheckImp( Fra_Sml_t * p, int Left, int Right )
 
 /**Function*************************************************************
 
-  Synopsis    [Counts the number of 1s in the reverse implication.]
+  Synopsis    [Counts the number of 1s in the complement of the implication.]
 
   Description []
                
@@ -118,7 +118,7 @@ static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right )
 
 /**Function*************************************************************
 
-  Synopsis    [Counts the number of 1s in the reverse implication.]
+  Synopsis    [Computes the complement of the implication.]
 
   Description []
                
@@ -495,7 +495,7 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in
 {
     Aig_Obj_t * pLeft, * pRight;
     Aig_Obj_t * pLeftF, * pRightF;
-    int i, Imp, Left, Right, Max;
+    int i, Imp, Left, Right, Max, RetValue;
     int fComplL, fComplR;
     Vec_IntForEachEntryStart( vImps, Imp, i, Pos )
     {
@@ -519,18 +519,31 @@ int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, in
         // check equality
         if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
         {
-            if ( fComplL != fComplR )
-                Vec_IntWriteEntry( vImps, i, 0 );
+            if ( fComplL == fComplR ) // x => x  - always true
+                continue;
+            assert( fComplL != fComplR );
+            // consider 4 possibilities:
+            // NOT(1) => 1    or   0 => 1  - always true
+            // 1 => NOT(1)    or   1 => 0  - never true
+            // NOT(x) => x    or   x       - not always true
+            // x => NOT(x)    or   NOT(x)  - not always true
+            if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication
+                continue;
+            // disproved implication
+            p->pCla->fRefinement = 1;
+            Vec_IntWriteEntry( vImps, i, 0 );
             continue;
         }
         // check the implication 
         // - if true, a clause is added
         // - if false, a cex is simulated
         // make sure the implication is refined
-        if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) == 0 )
+        RetValue = Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR );
+        if ( RetValue != 1 )
         {
             p->pCla->fRefinement = 1;
-            Fra_SmlResimulate( p );
+            if ( RetValue == 0 )
+                Fra_SmlResimulate( p );
             if ( Vec_IntEntry(vImps, i) != 0 )
                 printf( "Fra_ImpCheckForNode(): Implication is not refined!\n" );
             assert( Vec_IntEntry(vImps, i) == 0 );
@@ -642,14 +655,15 @@ double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p )
 ***********************************************************************/
 int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p )
 {
-    int nSimWords = 2000;
+    int nFrames = 2000;
+    int nSimWords = 8;
     Fra_Sml_t * pSeq;
     char * pfFails;
     int Left, Right, Imp, i, Counter;
     if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
         return 0;
     // simulate the AIG manager with combinational patterns
-    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 4 );
+    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nFrames, nSimWords );
     // go through the implications and check how many of them do not hold
     pfFails = ALLOC( char, Vec_IntSize(p->pCla->vImps) );
     memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) );
@@ -664,6 +678,7 @@ int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p )
     for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ )
         Counter += pfFails[i];
     free( pfFails );
+    Fra_SmlStop( pSeq );
     return Counter;
 }
 
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 14fba9ba..98025280 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -257,7 +257,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK,
     Aig_Obj_t * pObj;
     Cnf_Dat_t * pCnf;
     Aig_Man_t * pManAigNew;
-    int nNodesBeg, nRegsBeg, Temp;
+    int nNodesBeg, nRegsBeg;
     int nIter, i, clk = clock(), clk2;
 
     if ( Aig_ManNodeNum(pManAig) == 0 )
@@ -424,17 +424,18 @@ PRT( "Time", clock() - clk );
             break;
         }
     }
+/*
     // check implications using simulation
     if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
     {
-        int clk = clock();
+        int Temp, clk = clock();
         if ( Temp = Fra_ImpVerifyUsingSimulation( p ) )
             printf( "Implications failing the simulation test = %d (out of %d).  ", Temp, Vec_IntSize(p->pCla->vImps) );
         else
             printf( "All %d implications have passed the simulation test.  ", Vec_IntSize(p->pCla->vImps) );
         PRT( "Time", clock() - clk );
     }
-
+*/
 
     // move the classes into representatives and reduce AIG
 clk2 = clock();
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
index e73d610f..50fd6687 100644
--- a/src/aig/fra/fraLcr.c
+++ b/src/aig/fra/fraLcr.c
@@ -500,17 +500,18 @@ void Fra_ClassNodesUnmark( Fra_Lcr_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter )
 {
     int nPartSize    = 200;
     int fReprSelect  = 0;
 
     Fra_Lcr_t * p;
+    Fra_Sml_t * pSml;
     Fra_Man_t * pTemp;
     Aig_Man_t * pAigPart, * pAigNew = NULL;
     Vec_Int_t * vPart;
 //    Aig_Obj_t * pObj = Aig_ManObj(pAig, 2078);
-    int i, nIter, clk = clock(), clk2, clk3;
+    int i, nIter, timeSim, clk = clock(), clk2, clk3;
     if ( Aig_ManNodeNum(pAig) == 0 )
     {
         if ( pnIter ) *pnIter = 0;
@@ -519,23 +520,33 @@ Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nC
     assert( Aig_ManLatchNum(pAig) == 0 );
     assert( Aig_ManRegNum(pAig) > 0 );
 
-    // start the manager
-    p = Lcr_ManAlloc( pAig );
-    p->nFramesP = nFramesP;
-    p->fVerbose = fVerbose;
-
     // simulate the AIG 
 clk2 = clock();
 if ( fVerbose )
 printf( "Simulating AIG with %d nodes for %d cycles ...  ", Aig_ManNodeNum(pAig), nFramesP + 32 );
-    pTemp = Fra_LcrAigPrepare( p->pAig );
-    pTemp->pBmc = (Fra_Bmc_t *)p;
-    pTemp->pSml = Fra_SmlSimulateSeq( p->pAig, p->nFramesP, 32, 1 ); 
+    pSml = Fra_SmlSimulateSeq( pAig, nFramesP, 32, 1 ); 
 if ( fVerbose ) 
 {
 PRT( "Time", clock() - clk2 );
-p->timeSim += clock() - clk2;
+timeSim = clock() - clk2;
 }
+    // check if simulation discovered non-constant-0 POs
+    if ( fProve && pSml->fNonConstOut )
+    {
+        Fra_SmlStop( pSml );
+        return NULL;
+    }
+
+    // start the manager
+    p = Lcr_ManAlloc( pAig );
+    p->nFramesP = nFramesP;
+    p->fVerbose = fVerbose;
+    p->timeSim += timeSim;
+
+    pTemp = Fra_LcrAigPrepare( pAig );
+    pTemp->pBmc = (Fra_Bmc_t *)p;
+    pTemp->pSml = pSml;
+
     // get preliminary info about equivalence classes
     pTemp->pCla = p->pCla = Fra_ClassesStart( p->pAig );
     Fra_ClassesPrepare( p->pCla, 1 );
diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c
index e1cc4c32..11029b69 100644
--- a/src/aig/fra/fraSat.c
+++ b/src/aig/fra/fraSat.c
@@ -75,6 +75,9 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
         p->pSat = sat_solver_new();
         p->nSatVars = 1;
         sat_solver_setnvars( p->pSat, 1000 );
+        // var 0 is reserved for const1 node - add the clause
+        pLits[0] = toLit( 0 );
+        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
     }
 
     // if the nodes do not have SAT variables, allocate them
@@ -232,6 +235,9 @@ int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fCom
         p->pSat = sat_solver_new();
         p->nSatVars = 1;
         sat_solver_setnvars( p->pSat, 1000 );
+        // var 0 is reserved for const1 node - add the clause
+        pLits[0] = toLit( 0 );
+        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
     }
 
     // if the nodes do not have SAT variables, allocate them
@@ -318,6 +324,9 @@ int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew )
         p->pSat = sat_solver_new();
         p->nSatVars = 1;
         sat_solver_setnvars( p->pSat, 1000 );
+        // var 0 is reserved for const1 node - add the clause
+        pLits[0] = toLit( 0 );
+        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
     }
 
     // if the nodes do not have SAT variables, allocate them
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 0146ac5a..0919e035 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -103,6 +103,7 @@ PRT( "Time", clock() - clkTotal );
 ***********************************************************************/
 int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fVerbose, int fVeryVerbose )
 {
+    Fra_Sml_t * pSml;
     Aig_Man_t * pNew, * pTemp;
     int nFrames, RetValue, nIter, clk, clkTotal = clock();
     int fLatchCorr = 0;
@@ -148,8 +149,16 @@ clk = clock();
     {
     pNew = Aig_ManDup( pTemp = pNew, 1 );
     Aig_ManStop( pTemp );
-    pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, fVeryVerbose, &nIter );
+    pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter );
     Aig_ManStop( pTemp );
+    if ( pNew == NULL )
+    {
+        RetValue = 0;
+        printf( "Networks are NOT EQUIVALENT after simulation.   " );
+PRT( "Time", clock() - clkTotal );
+        return RetValue;
+    }
+
     if ( fVerbose )
     {
         printf( "Latch-corr (I=%3d):   Latches = %5d. Nodes = %6d. ", 
@@ -196,7 +205,7 @@ clk = clock();
             printf( "Rewriting:            Latches = %5d. Nodes = %6d. ", 
                 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
 PRT( "Time", clock() - clk );
-        }
+        } 
         // perform retiming
 clk = clock();
         pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
@@ -211,6 +220,26 @@ PRT( "Time", clock() - clk );
         }
         if ( pNew->nRegs )
         pNew = Aig_ManConstReduce( pNew, 0 );
+
+        // perform sequential simulation
+clk = clock();
+        pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000) ); 
+        if ( fVerbose )
+        {
+            printf( "Seq simulation  :     Latches = %5d. Nodes = %6d. ", 
+                Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+        }
+        if ( pSml->fNonConstOut )
+        {
+            Fra_SmlStop( pSml );
+            Aig_ManStop( pNew );
+            RetValue = 0;
+            printf( "Networks are NOT EQUIVALENT after simulation.   " );
+PRT( "Time", clock() - clkTotal );
+            return RetValue;
+        }
+        Fra_SmlStop( pSml );
     }
 
     // get the miter status
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index d6f6d74a..d379cf53 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -137,6 +137,28 @@ int Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right )
     return Counter;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if simulation info is composed of all zeros.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_SmlNodeIsZero( Fra_Sml_t * p, Aig_Obj_t * pObj )
+{
+    unsigned * pSims;
+    int i;
+    pSims = Fra_ObjSim(p, pObj->Id);
+    for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
+        if ( pSims[i] )
+            return 0;
+    return 1;
+}
+
 
 
 /**Function*************************************************************
@@ -550,6 +572,27 @@ void Fra_SmlNodeTransferNext( Fra_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn,
 
 /**Function*************************************************************
 
+  Synopsis    [Check if any of the POs becomes non-constant.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_SmlCheckNonConstOutputs( Fra_Sml_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManForEachPoSeq( p->pAig, pObj, i )
+        if ( !Fra_SmlNodeIsZero(p, pObj) )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Simulates AIG manager.]
 
   Description [Assumes that the PI simulation info is attached.]
@@ -569,14 +612,16 @@ clk = clock();
         // simulate the nodes
         Aig_ManForEachNode( p->pAig, pObj, i )
             Fra_SmlNodeSimulate( p, pObj, f );
+        // copy simulation info into outputs
+        Aig_ManForEachPoSeq( p->pAig, pObj, i )
+            Fra_SmlNodeCopyFanin( p, pObj, f );
+        // quit if this is the last timeframe
         if ( f == p->nFrames - 1 )
             break;
         // copy simulation info into outputs
         Aig_ManForEachLiSeq( p->pAig, pObj, i )
             Fra_SmlNodeCopyFanin( p, pObj, f );
         // copy simulation info into the inputs
-//        for ( i = 0; i < Aig_ManRegNum(p->pAig); i++ )
-//            Fra_SmlNodeTransferNext( p, Aig_ManLi(p->pAig, i), Aig_ManLo(p->pAig, i), f );
         Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
             Fra_SmlNodeTransferNext( p, pObjLi, pObjLo, f );
     }
@@ -768,6 +813,7 @@ Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nW
     p = Fra_SmlStart( pAig, nPref, nFrames, nWords );
     Fra_SmlInitialize( p, 1 );
     Fra_SmlSimulateOne( p );
+    p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p );
     return p;
 }
 
diff --git a/src/aig/ivy/ivyFraig.c b/src/aig/ivy/ivyFraig.c
index a922674d..81ed895e 100644
--- a/src/aig/ivy/ivyFraig.c
+++ b/src/aig/ivy/ivyFraig.c
@@ -2100,6 +2100,9 @@ int Ivy_FraigNodesAreEquiv( Ivy_FraigMan_t * p, Ivy_Obj_t * pOld, Ivy_Obj_t * pN
         p->pSat = sat_solver_new();
         p->nSatVars = 1;
         sat_solver_setnvars( p->pSat, 1000 );
+        // var 0 is reserved for const1 node - add the clause
+        pLits[0] = toLit( 0 );
+        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
     }
 
     // if the nodes do not have SAT variables, allocate them
@@ -2231,6 +2234,9 @@ int Ivy_FraigNodeIsConst( Ivy_FraigMan_t * p, Ivy_Obj_t * pNew )
         p->pSat = sat_solver_new();
         p->nSatVars = 1;
         sat_solver_setnvars( p->pSat, 1000 );
+        // var 0 is reserved for const1 node - add the clause
+        pLits[0] = toLit( 0 );
+        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
     }
 
     // if the nodes do not have SAT variables, allocate them
diff --git a/src/aig/kit/kitDsd.c b/src/aig/kit/kitDsd.c
index ada4ef09..abd07e68 100644
--- a/src/aig/kit/kitDsd.c
+++ b/src/aig/kit/kitDsd.c
@@ -48,7 +48,7 @@ Kit_DsdMan_t * Kit_DsdManAlloc( int nVars, int nNodes )
     p->nWords   = Kit_TruthWordNum( p->nVars );
     p->vTtElems = Vec_PtrAllocTruthTables( p->nVars );
     p->vTtNodes = Vec_PtrAllocSimInfo( nNodes, p->nWords );
-    p->dd       = Cloud_Init( 16, 13 );
+    p->dd       = Cloud_Init( 16, 14 );
     p->vTtBdds  = Vec_PtrAllocSimInfo( (1<<12), p->nWords );
     p->vNodes   = Vec_IntAlloc( 512 );
     return p;