Version abc61216

6 files changed, 57 insertions, 38 deletions

diff --git a/src/map/if/if.h b/src/map/if/if.h
index 1bbed29d..eaa08a3a 100644
--- a/src/map/if/if.h
+++ b/src/map/if/if.h
@@ -273,10 +273,10 @@ static inline float      If_CutLutArea( If_Man_t * p, If_Cut_t * pCut )      { r
 #define If_ObjForEachCutStart( pObj, pCut, i, Start )                          \
     for ( i = Start; (i < (int)(pObj)->nCuts) && ((pCut) = (pObj)->Cuts + i); i++ )
 // iterator over the leaves of the cut
-//#define If_CutForEachLeaf( p, pCut, pLeaf, i )                                 \
-//    for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = If_ManObj(p, (pCut)->pLeaves[i])); i++ )
 #define If_CutForEachLeaf( p, pCut, pLeaf, i )                                 \
-    for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = If_ManObj(p, p->pPars->fLiftLeaves? (pCut)->pLeaves[i] >> 8 : (pCut)->pLeaves[i])); i++ )
+    for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = If_ManObj(p, (pCut)->pLeaves[i])); i++ )
+//#define If_CutForEachLeaf( p, pCut, pLeaf, i )                                 \
+//    for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = If_ManObj(p, p->pPars->fLiftLeaves? (pCut)->pLeaves[i] >> 8 : (pCut)->pLeaves[i])); i++ )
 // iterator over the leaves of the sequential cut
 #define If_CutForEachLeafSeq( p, pCut, pLeaf, Shift, i )                       \
     for ( i = 0; (i < (int)(pCut)->nLeaves) && ((pLeaf) = If_ManObj(p, (pCut)->pLeaves[i] >> 8)) && (((Shift) = ((pCut)->pLeaves[i] & 255)) >= 0); i++ )
diff --git a/src/map/if/ifCut.c b/src/map/if/ifCut.c
index 5366aaf5..8c092b99 100644
--- a/src/map/if/ifCut.c
+++ b/src/map/if/ifCut.c
@@ -257,9 +257,11 @@ static inline int If_CutMergeOrdered2( If_Cut_t * pC0, If_Cut_t * pC1, If_Cut_t
         pC->pLeaves[k++] = pC1->pLeaves[i];
         pC->nLeaves++;
     }
+/*
     assert( pC->nLeaves <= pC->nLimit );
     for ( i = 1; i < (int)pC->nLeaves; i++ )
         assert( pC->pLeaves[i-1] < pC->pLeaves[i] );
+*/
     return 1;
 }
 
@@ -574,7 +576,8 @@ float If_CutAreaDerefed( If_Man_t * p, If_Cut_t * pCut, int nLevels )
     assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
     aResult2 = If_CutRef( p, pCut, nLevels );
     aResult  = If_CutDeref( p, pCut, nLevels );
-    assert( aResult == aResult2 );
+    assert( aResult > aResult2 - p->fEpsilon );
+    assert( aResult < aResult2 + p->fEpsilon );
     return aResult;
 }
 
@@ -595,7 +598,8 @@ float If_CutAreaRefed( If_Man_t * p, If_Cut_t * pCut, int nLevels )
     assert( p->pPars->fSeqMap || pCut->nLeaves > 1 );
     aResult2 = If_CutDeref( p, pCut, nLevels );
     aResult  = If_CutRef( p, pCut, nLevels );
-    assert( aResult == aResult2 );
+    assert( aResult > aResult2 - p->fEpsilon );
+    assert( aResult < aResult2 + p->fEpsilon );
     return aResult;
 }
 
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index 4d422359..4cdd7a87 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -189,38 +189,43 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode )
     pCut = p->ppCuts[iCut];
     // generate cuts
     for ( pTemp = pObj; pTemp; pTemp = pTemp->pEquiv )
-    If_ObjForEachCutStart( pTemp, pCutTemp, i, 1 )
     {
-        assert( pTemp->nCuts > 1 );
-        assert( pTemp == pObj || pTemp->nRefs == 0 );
-        // copy the cut into storage
-        If_CutCopy( pCut, pCutTemp );
-        // check if this cut is contained in any of the available cuts
-        if ( If_CutFilter( p, pCut ) )
-            continue;
-        // the cuts have been successfully merged
-        // check if the cut satisfies the required times
-        assert( pCut->Delay == If_CutDelay( p, pCut ) );
-        if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon )
-            continue;
-        // set the phase attribute
-        pCut->fCompl ^= (pObj->fPhase ^ pTemp->fPhase);
-        // compute area of the cut (this area may depend on the application specific cost)
-        pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut );
-        pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut );
-        // make sure the cut is the last one (after filtering it may not be so)
-        assert( pCut == p->ppCuts[iCut] );
-        p->ppCuts[iCut] = p->ppCuts[p->nCuts];
-        p->ppCuts[p->nCuts] = pCut;
-        // count the cut
-        p->nCuts++;
-        // prepare room for the next cut
-        iCut = p->nCuts;
-        pCut = p->ppCuts[iCut];
+        If_ObjForEachCutStart( pTemp, pCutTemp, i, 1 )
+        {
+            assert( pTemp->nCuts > 1 );
+            assert( pTemp == pObj || pTemp->nRefs == 0 );
+            // copy the cut into storage
+            If_CutCopy( pCut, pCutTemp );
+            // check if this cut is contained in any of the available cuts
+            if ( If_CutFilter( p, pCut ) )
+                continue;
+            // the cuts have been successfully merged
+            // check if the cut satisfies the required times
+            assert( pCut->Delay == If_CutDelay( p, pCut ) );
+            if ( Mode && pCut->Delay > pObj->Required + p->fEpsilon )
+                continue;
+            // set the phase attribute
+            pCut->fCompl ^= (pObj->fPhase ^ pTemp->fPhase);
+            // compute area of the cut (this area may depend on the application specific cost)
+            pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut, 100 ) : If_CutFlow( p, pCut );
+            pCut->AveRefs = (Mode == 0)? (float)0.0 : If_CutAverageRefs( p, pCut );
+            // make sure the cut is the last one (after filtering it may not be so)
+            assert( pCut == p->ppCuts[iCut] );
+            p->ppCuts[iCut] = p->ppCuts[p->nCuts];
+            p->ppCuts[p->nCuts] = pCut;
+            // count the cut
+            p->nCuts++;
+            // prepare room for the next cut
+            iCut = p->nCuts;
+            pCut = p->ppCuts[iCut];
+            // quit if we exceeded the number of cuts
+            if ( p->nCuts >= p->pPars->nCutsMax * p->pPars->nCutsMax )
+                break;
+        }
         // quit if we exceeded the number of cuts
         if ( p->nCuts >= p->pPars->nCutsMax * p->pPars->nCutsMax )
             break;
-    } 
+    }
     assert( p->nCuts > 0 );
     // sort if we have more cuts
     If_ManSortCuts( p, Mode );
diff --git a/src/map/if/ifSeq.c b/src/map/if/ifSeq.c
index ddc74a49..cd90a313 100644
--- a/src/map/if/ifSeq.c
+++ b/src/map/if/ifSeq.c
@@ -96,7 +96,7 @@ int If_ManPerformMappingSeq( If_Man_t * p )
     // print the statistic into a file
     {
         FILE * pTable;
-        pTable = fopen( "a/seqmap__stats.txt", "a+" );
+        pTable = fopen( "iscas/seqmap__stats.txt", "a+" );
         fprintf( pTable, "%d ", p->Period );
         fprintf( pTable, "\n" );
         fclose( pTable );
@@ -198,7 +198,7 @@ int If_ManBinarySearchPeriod( If_Man_t * p, int Mode )
     // report the results
     if ( p->pPars->fVerbose )
     {
-        p->AreaGlo = p->pPars->fLiftLeaves? If_ManScanMappingSeq(p) : If_ManScanMapping(p);
+        p->AreaGlo = p->pPars->fLiftLeaves? 0/*If_ManScanMappingSeq(p)*/ : If_ManScanMapping(p);
         printf( "Attempt = %2d.  Iters = %3d.  Area = %10.2f.  Fi = %6.2f.  ", p->nAttempts, c, p->AreaGlo, (float)p->Period );
         if ( fConverged )
             printf( "  Feasible" );
@@ -358,7 +358,9 @@ int If_ManPrepareMappingSeq( If_Man_t * p )
             pCut->Delay  -= p->Period;
             pCut->fCompl ^= pObj->fCompl0;
 
-            pTemp = If_ManObj(p, pCut->pLeaves[0] >> 8);
+            // there is a bug here, which shows when there are choices...
+//            pTemp = If_ManObj(p, pCut->pLeaves[0] >> 8);
+            pTemp = If_ManObj(p, pCut->pLeaves[0]);
             assert( !If_ObjIsLatch(pTemp) );
         }
     }
diff --git a/src/map/if/ifTime.c b/src/map/if/ifTime.c
index f0041868..0cf2f73c 100644
--- a/src/map/if/ifTime.c
+++ b/src/map/if/ifTime.c
@@ -186,7 +186,7 @@ void If_CutSortInputPins( If_Man_t * p, If_Cut_t * pCut, int * pPinPerm, float *
     If_Obj_t * pLeaf;
     int i, j, best_i, temp;
     // start the trivial permutation and collect pin delays
-    If_CutForEachLeaf( p, pCut, pLeaf, i );
+    If_CutForEachLeaf( p, pCut, pLeaf, i )
     {
         pPinPerm[i] = i;
         pPinDelays[i] = If_ObjCutBest(pLeaf)->Delay;
@@ -206,8 +206,12 @@ void If_CutSortInputPins( If_Man_t * p, If_Cut_t * pCut, int * pPinPerm, float *
         pPinPerm[best_i] = temp;
     }
     // verify
+    assert( pPinPerm[0] < pCut->nLeaves );
     for ( i = 1; i < (int)pCut->nLeaves; i++ )
+    {
+        assert( pPinPerm[i] < (int)pCut->nLeaves );
         assert( pPinDelays[pPinPerm[i-1]] >= pPinDelays[pPinPerm[i]] );
+    }
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/map/if/ifUtil.c b/src/map/if/ifUtil.c
index 4b136f55..797d853d 100644
--- a/src/map/if/ifUtil.c
+++ b/src/map/if/ifUtil.c
@@ -269,7 +269,11 @@ float If_ManScanMappingSeq_rec( If_Man_t * p, If_Obj_t * pObj, Vec_Ptr_t * vMapp
     If_Cut_t * pCutBest;
     float aArea;
     int i, Shift;
-    if ( pObj->nRefs++ || If_ObjIsCi(pObj) || If_ObjIsConst1(pObj) )
+    // treat latches transparently
+    if ( If_ObjIsLatch(pObj) )
+        return If_ManScanMappingSeq_rec( p, If_ObjFanin0(pObj), vMapped );
+    // consider trivial cases
+    if ( pObj->nRefs++ || If_ObjIsPi(pObj) || If_ObjIsConst1(pObj) )
         return 0.0;
     // store the node in the structure by level
     assert( If_ObjIsAnd(pObj) );