Version abc80527

4 files changed, 73 insertions, 57 deletions

diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 49d3f5ef..67f38758 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -89,6 +89,7 @@ extern int               Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int
 /*=== saigPhase.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose );
 /*=== saigRetFwd.c ==========================================================*/
+extern void              Saig_ManMarkAutonomous( Aig_Man_t * p );
 extern Aig_Man_t *       Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose );
 /*=== saigRetMin.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManRetimeDupForward( Aig_Man_t * p, Vec_Ptr_t * vCut );
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index 2d5af2d3..32b2d186 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -191,7 +191,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
     }
     else
         pFrames = Saig_ManFramesBmc( pAig, nFrames );
-    *piFrame = nFrames;
+    if ( piFrame )
+        *piFrame = nFrames;
     if ( fVerbose )
     {
         printf( "AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n", 
@@ -281,7 +282,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
             }
             else
             {
-                *piFrame = i / Saig_ManPoNum(pAig);
+                if ( piFrame )
+                    *piFrame = i / Saig_ManPoNum(pAig);
                 RetValue = -1;
                 break;
             }
diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c
index 4250ca79..8a75ae1f 100644
--- a/src/aig/saig/saigHaig.c
+++ b/src/aig/saig/saigHaig.c
@@ -195,7 +195,7 @@ int Aig_ManMapHaigNodes( Aig_Man_t * pHaig )
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
+int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames, int clkSynth )
 {
     int nBTLimit = 0;
     Aig_Man_t * pFrames, * pTemp;
@@ -203,7 +203,7 @@ int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int n
     sat_solver * pSat;
     Aig_Obj_t * pObj1, * pObj2;
     int i, RetValue1, RetValue2, Counter, Lits[2], nOvers;
-    int clk = clock();
+    int clk = clock(), clkVerif;
 
     nOvers = Aig_ManMapHaigNodes( pHaig );
 
@@ -226,57 +226,6 @@ clk = clock();
 //    pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) );
     pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );
 
-/*
-    // print the statistic into a file
-    {
-        FILE * pTable;
-        Aig_Man_t * pTemp, * pHaig2;
-
-        pHaig2 = pAig->pManHaig; 
-        pAig->pManHaig = NULL;
-        pTemp = Aig_ManDupDfs( pAig );
-        pAig->pManHaig = pHaig2;
-
-        Aig_ManSeqCleanup( pTemp );
-
-        pTable = fopen( "stats.txt", "a+" );
-        fprintf( pTable, "%s ",  p->pName );
-        fprintf( pTable, "%d ", Saig_ManPiNum(p) );
-        fprintf( pTable, "%d ", Saig_ManPoNum(p) );
-
-        fprintf( pTable, "%d ", Saig_ManRegNum(p) );
-        fprintf( pTable, "%d ", Aig_ManNodeNum(p) );
-        fprintf( pTable, "%d ", Aig_ManLevelNum(p) );
-
-        fprintf( pTable, "%d ", Saig_ManRegNum(pTemp) );
-        fprintf( pTable, "%d ", Aig_ManNodeNum(pTemp) );
-        fprintf( pTable, "%d ", Aig_ManLevelNum(pTemp) );
-
-        fprintf( pTable, "%d ", Saig_ManRegNum(pHaig) );
-        fprintf( pTable, "%d ", Aig_ManNodeNum(pHaig) );
-        fprintf( pTable, "%d ", Aig_ManLevelNum(pHaig) );
-        fprintf( pTable, "\n" );
-        fclose( pTable );
-
-
-        pTable = fopen( "stats2.txt", "a+" );
-        fprintf( pTable, "%s ",  p->pSpec );
-        fprintf( pTable, "%d ", Aig_ManNodeNum(pFrames) );
-        fprintf( pTable, "%d ", Aig_ManLevelNum(pFrames) );
-
-        fprintf( pTable, "%d ", pCnf->nVars );
-        fprintf( pTable, "%d ", pCnf->nClauses );
-        fprintf( pTable, "%d ", pCnf->nLiterals );
-
-        fprintf( pTable, "%d ", Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2 );
-        fprintf( pTable, "%d ", pFrames->nAsserts/2 );
-        fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 );
-        fprintf( pTable, "\n" );
-        fclose( pTable );
-
-        Aig_ManStop( pTemp );
-    }
-*/
 
 
 //    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
@@ -375,11 +324,66 @@ clk = clock();
     }
     printf( "                                                          \r" );
 PRT( "Solving    ", clock() - clk );
+clkVerif = clock() - clk;
     if ( Counter )
         printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 );
     else
         printf( "Verification is successful for all %d assertions.\n", pFrames->nAsserts/2 );
 
+    // print the statistic into a file
+    {
+        FILE * pTable;
+        Aig_Man_t * pTemp, * pHaig2;
+
+        pHaig2 = pAig->pManHaig; 
+        pAig->pManHaig = NULL;
+        pTemp = Aig_ManDupDfs( pAig );
+        pAig->pManHaig = pHaig2;
+
+        Aig_ManSeqCleanup( pTemp );
+
+        pTable = fopen( "stats.txt", "a+" );
+        fprintf( pTable, "%s ",  p->pName );
+        fprintf( pTable, "%d ", Saig_ManPiNum(p) );
+        fprintf( pTable, "%d ", Saig_ManPoNum(p) );
+
+        fprintf( pTable, "%d ", Saig_ManRegNum(p) );
+        fprintf( pTable, "%d ", Aig_ManNodeNum(p) );
+        fprintf( pTable, "%d ", Aig_ManLevelNum(p) );
+
+        fprintf( pTable, "%d ", Saig_ManRegNum(pTemp) );
+        fprintf( pTable, "%d ", Aig_ManNodeNum(pTemp) );
+        fprintf( pTable, "%d ", Aig_ManLevelNum(pTemp) );
+
+        fprintf( pTable, "%d ", Saig_ManRegNum(pHaig) );
+        fprintf( pTable, "%d ", Aig_ManNodeNum(pHaig) );
+        fprintf( pTable, "%d ", Aig_ManLevelNum(pHaig) );
+
+        fprintf( pTable, "%.2f", (float)(clkSynth)/(float)(CLOCKS_PER_SEC) );
+        fprintf( pTable, "\n" );
+        fclose( pTable );
+
+
+        pTable = fopen( "stats2.txt", "a+" );
+        fprintf( pTable, "%s ",  p->pName );
+        fprintf( pTable, "%d ", Aig_ManNodeNum(pFrames) );
+        fprintf( pTable, "%d ", Aig_ManLevelNum(pFrames) );
+
+        fprintf( pTable, "%d ", pCnf->nVars );
+        fprintf( pTable, "%d ", pCnf->nClauses );
+        fprintf( pTable, "%d ", pCnf->nLiterals );
+
+        fprintf( pTable, "%d ", Aig_ManPoNum(pFrames)/2 - pFrames->nAsserts/2 );
+        fprintf( pTable, "%d ", pFrames->nAsserts/2 );
+        fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 );
+
+        fprintf( pTable, "%.2f", (float)(clkVerif)/(float)(CLOCKS_PER_SEC) );
+        fprintf( pTable, "\n" );
+        fclose( pTable );
+
+        Aig_ManStop( pTemp );
+    }
+
     // clean up
     Aig_ManStop( pFrames );
     Cnf_DataFree( pCnf );
@@ -617,7 +621,7 @@ Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fReti
     Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
     Aig_Man_t * pNew, * pTemp;
     Aig_Obj_t * pObj;
-    int i, k, nStepsReal, clk = clock();
+    int i, k, nStepsReal, clk = clock(), clkSynth;
     Dar_ManDefaultRwrParams( pParsRwr );
 
 clk = clock();
@@ -679,6 +683,7 @@ clk = clock();
         }
     } 
 PRT( "Synthesis time ", clock() - clk );
+clkSynth = clock() - clk;
 
     // use the haig for verification
 //    Aig_ManAntiCleanup( pNew->pManHaig );
@@ -699,7 +704,7 @@ PRT( "Synthesis time ", clock() - clk );
     }
     else
     {
-        if ( !Aig_ManHaigVerify( p, pNew, pNew->pManHaig, 1+fSeqHaig ) )
+        if ( !Aig_ManHaigVerify( p, pNew, pNew->pManHaig, 1+fSeqHaig, clkSynth ) )
             printf( "Constructing SAT solver has failed.\n" );         
     }
 
diff --git a/src/aig/saig/saigRetStep.c b/src/aig/saig/saigRetStep.c
index fe726702..e2502761 100644
--- a/src/aig/saig/saigRetStep.c
+++ b/src/aig/saig/saigRetStep.c
@@ -62,6 +62,10 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug
     assert( Aig_ObjPioNum(pFanin0) > 0 );
     assert( Aig_ObjPioNum(pFanin1) > 0 );
 
+    // skip latch guns
+    if ( !Aig_ObjIsTravIdCurrent(p, pFanin0) && !Aig_ObjIsTravIdCurrent(p, pFanin1) )
+        return NULL;
+
     // get the inputs of these registers
     pInput0 = Saig_ManLi( p, Aig_ObjPioNum(pFanin0) - Saig_ManPiNum(p) );
     pInput1 = Saig_ManLi( p, Aig_ObjPioNum(pFanin1) - Saig_ManPiNum(p) );
@@ -90,6 +94,9 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj, int fMakeBug
     pObjLo->PioNum = Aig_ManPiNum(p) - 1;
     p->nRegs++;
 
+    // make sure the register is retimable.
+    Aig_ObjSetTravIdCurrent(p, pObjLo);
+
 //printf( "Reg = %4d. Reg = %4d. Compl = %d. Phase = %d.\n", 
 //       pFanin0->PioNum, pFanin1->PioNum, Aig_IsComplement(pObjNew), fCompl );
 
@@ -177,6 +184,7 @@ int Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward, int fAddBugs )
     p->fCreatePios = 1;
     if ( fForward )
     {
+        Saig_ManMarkAutonomous( p );
         for ( s = 0; s < nSteps; s++ )
         {
             Aig_ManForEachNode( p, pObj, i )