Version abc70225

1 files changed, 209 insertions, 239 deletions

diff --git a/src/map/if/ifSeq.c b/src/map/if/ifSeq.c
index cd90a313..e6528233 100644
--- a/src/map/if/ifSeq.c
+++ b/src/map/if/ifSeq.c
@@ -24,19 +24,13 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static int  If_ManBinarySearchPeriod( If_Man_t * p, int Mode );
-static int  If_ManBinarySearch_rec( If_Man_t * p, int Mode, int FiMin, int FiMax );
-static int  If_ManPerformMappingRoundSeq( If_Man_t * p, int Mode, int nIter, char * pLabel );
-static int  If_ManPrepareMappingSeq( If_Man_t * p );
-static int  If_ObjPerformMappingLatch( If_Man_t * p, If_Obj_t * pObj );
-
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Performs sequential mapping.]
+  Synopsis    [Prepares for sequential mapping by linking the latches.]
 
   Description []
                
@@ -45,102 +39,46 @@ static int  If_ObjPerformMappingLatch( If_Man_t * p, If_Obj_t * pObj );
   SeeAlso     []
 
 ***********************************************************************/
-int If_ManPerformMappingSeq( If_Man_t * p )
+void If_ManPrepareMappingSeq( If_Man_t * p )
 {
-    int PeriodBest, Mode = 0;
-
-    // collect nodes in the sequential order
-    If_ManPrepareMappingSeq( p );
-
-    // perform combinational mapping to get the upper bound on the clock period
-    If_ManPerformMappingRound( p, 2, 0, 0, NULL );
-    p->RequiredGlo = If_ManDelayMax( p, 0 );
-
-    // set parameters
-    p->nCutsUsed = p->pPars->nCutsMax;
-    p->nAttempts = 0;
-    p->nMaxIters = 50;
-    p->Period    = (int)p->RequiredGlo;
-
-    // make sure the clock period words
-    if ( !If_ManBinarySearchPeriod( p, Mode ) )
-    {
-        printf( "If_ManPerformMappingSeq(): The upper bound on the clock period cannot be computed.\n" );
-        return 0;
-    }
-
-    // perform binary search
-    PeriodBest = If_ManBinarySearch_rec( p, Mode, 0, p->Period );
+    If_Obj_t * pObjLi, * pObjLo;
+    int i;
 
-    // recompute the best l-values
-    if ( p->Period != PeriodBest )
-    {
-        p->Period = PeriodBest;
-        if ( !If_ManBinarySearchPeriod( p, Mode ) )
-        {
-            printf( "If_ManPerformMappingSeq(): The final clock period cannot be confirmed.\n" );
-            return 0;
-        }
-    }
-/*
-    // fix the problem with non-converged delays
-    If_ManForEachNode( p, pObj, i )
-        if ( pObj->LValue < -ABC_INFINITY/2 )
-            pObj->LValue = (float)0.0;
-    // write the retiming lags
-    p->vLags = Vec_IntStart( If_ManObjNum(p) + 1 );
-    If_ManForEachNode( p, pObj, i )
-        Vec_IntWriteEntry( vLags, i, Abc_NodeComputeLag(pObj->LValue, p->Period) );
-*/
-/*
-    // print the statistic into a file
-    {
-        FILE * pTable;
-        pTable = fopen( "iscas/seqmap__stats.txt", "a+" );
-        fprintf( pTable, "%d ", p->Period );
-        fprintf( pTable, "\n" );
-        fclose( pTable );
-    }
-*/
-    // print the result
-    if ( p->pPars->fLiftLeaves )
+    // link the latch outputs (CIs) directly to the drivers of latch inputs (COs)
+    for ( i = 0; i < p->pPars->nLatches; i++ )
     {
-//        if ( p->pPars->fVerbose )   
-            printf( "The best clock period is %3d. (Currently, network is not modified, so mapping will fail.)\n", p->Period );
-        return 0;
+        pObjLi = If_ManLi( p, i );
+        pObjLo = If_ManLo( p, i );
+        pObjLo->pFanin0 = If_ObjFanin0( pObjLi );
+        pObjLo->fCompl0 = If_ObjFaninC0( pObjLi );
     }
-//    if ( p->pPars->fVerbose )   
-        printf( "The best clock period is %3d.\n", p->Period );
-    return 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Performs binary search for the optimal clock period.]
+  Synopsis    [Collects latches in the topological order.]
 
-  Description [Assumes that FiMin is infeasible while FiMax is feasible.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
-
+ 
 ***********************************************************************/
-int If_ManBinarySearch_rec( If_Man_t * p, int Mode, int FiMin, int FiMax )
+void If_ManCollectLatches_rec( If_Obj_t * pObj, Vec_Ptr_t * vLatches )
 {
-    assert( FiMin < FiMax );
-    if ( FiMin + 1 == FiMax )
-        return FiMax;
-    // compute the median
-    p->Period = FiMin + (FiMax - FiMin)/2;
-    if ( If_ManBinarySearchPeriod( p, Mode ) )
-        return If_ManBinarySearch_rec( p, Mode, FiMin, p->Period ); // Median is feasible
-    else 
-        return If_ManBinarySearch_rec( p, Mode, p->Period, FiMax ); // Median is infeasible
+    if ( !If_ObjIsLatch(pObj) )
+        return;
+    if ( pObj->fMark )
+        return;
+    pObj->fMark = 1;
+    If_ManCollectLatches_rec( pObj->pFanin0, vLatches );
+    Vec_PtrPush( vLatches, pObj );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns 1 if retiming with this clock period is feasible.]
+  Synopsis    [Collects latches in the topological order.]
 
   Description []
                
@@ -149,66 +87,20 @@ int If_ManBinarySearch_rec( If_Man_t * p, int Mode, int FiMin, int FiMax )
   SeeAlso     []
 
 ***********************************************************************/
-int If_ManBinarySearchPeriod( If_Man_t * p, int Mode )
+Vec_Ptr_t * If_ManCollectLatches( If_Man_t * p )
 {
+    Vec_Ptr_t * vLatches;
     If_Obj_t * pObj;
-    int i, c, fConverged;
-    int fResetRefs = 0;
-
-    p->nAttempts++;
-
-    // set l-values of all nodes to be minus infinity, except PIs and constants
-    If_ManForEachObj( p, pObj, i )
-    {
-        pObj->nCuts = 1;
-        If_ObjSetLValue( pObj, -IF_FLOAT_LARGE );
-        if ( fResetRefs )
-            pObj->nRefs = 0;
-    }
-    If_ObjSetLValue( If_ManConst1(p), (float)0.0 );
-    If_ManForEachPi( p, pObj, i )
-        If_ObjSetLValue( pObj, (float)0.0 );
-
-    // reset references to their original state
-    if ( fResetRefs )
-    {
-        If_ManForEachObj( p, pObj, i )
-        {
-            if ( If_ObjIsCo(pObj) )
-                continue;
-            if ( pObj->pFanin0 ) pObj->pFanin0->nRefs++;
-            if ( pObj->pFanin1 ) pObj->pFanin1->nRefs++;
-        }
-    }
-
-    // update all values iteratively
-    fConverged = 0;
-    for ( c = 1; c <= p->nMaxIters; c++ )
-    {
-        if ( !If_ManPerformMappingRoundSeq( p, Mode, c, NULL ) )
-        {
-            fConverged = 1;
-            break;
-        }
-        p->RequiredGlo = If_ManDelayMax( p, 1 );
-        if ( p->RequiredGlo > p->Period + p->fEpsilon )
-            break; 
-    }
-
-    // report the results
-    if ( p->pPars->fVerbose )
-    {
-        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" );
-        else if ( c > p->nMaxIters )
-            printf( "Infeasible (timeout)" );
-        else
-            printf( "Infeasible" );
-        printf( "\n" );
-    }
-    return fConverged;
+    int i;
+    // collect latches 
+    vLatches = Vec_PtrAlloc( p->pPars->nLatches );
+    If_ManForEachLatchOutput( p, pObj, i )
+        If_ManCollectLatches_rec( pObj, vLatches );
+    // clean marks
+    Vec_PtrForEachEntry( vLatches, pObj, i )
+        pObj->fMark = 0;
+    assert( Vec_PtrSize(vLatches) == p->pPars->nLatches );
+    return vLatches;
 }
 
 /**Function*************************************************************
@@ -223,49 +115,53 @@ int If_ManBinarySearchPeriod( If_Man_t * p, int Mode )
   SeeAlso     []
 
 ***********************************************************************/
-int If_ManPerformMappingRoundSeq( If_Man_t * p, int Mode, int nIter, char * pLabel )
+int If_ManPerformMappingRoundSeq( If_Man_t * p, int nIter )
 {
-    ProgressBar * pProgress;
     If_Obj_t * pObj;
     int i, clk = clock();
     int fVeryVerbose = 0;
     int fChange = 0;
-    assert( Mode >= 0 && Mode <= 2 );
-    if ( !p->pPars->fVerbose )
-        pProgress = Extra_ProgressBarStart( stdout, If_ManObjNum(p) );
+
     // map the internal nodes
     p->nCutsMerged = 0;
     If_ManForEachNode( p, pObj, i )
     {
-        if ( !p->pPars->fVerbose )
-            Extra_ProgressBarUpdate( pProgress, i, pLabel );
-        // consider the camse of an AND gate
-        assert( If_ObjIsAnd(pObj) );
-        If_ObjPerformMappingAnd( p, pObj, Mode );
+        If_ObjPerformMappingAnd( p, pObj, 0, 0 );
         if ( pObj->fRepr )
-            If_ObjPerformMappingChoice( p, pObj, Mode );
-        // check if updating happens
+            If_ObjPerformMappingChoice( p, pObj, 0, 0 );
+    }
+
+    // postprocess the mapping
+//printf( "Itereation %d: \n", nIter );
+    If_ManForEachNode( p, pObj, i )
+    {
+        // update the LValues stored separately
         if ( If_ObjLValue(pObj) < If_ObjCutBest(pObj)->Delay - p->fEpsilon )
         {
             If_ObjSetLValue( pObj, If_ObjCutBest(pObj)->Delay );
             fChange = 1;
         }
-//if ( If_ObjLValue(pObj) > -1000.0 )
-//printf( "Node %d %.2f  ", pObj->Id, If_ObjLValue(pObj) );
+//printf( "%d ", (int)If_ObjLValue(pObj) );
+        // reset the visit counters
+        assert( pObj->nVisits == 0 );
+        pObj->nVisits = pObj->nVisitsCopy;
     }
-    if ( !p->pPars->fVerbose )
-        Extra_ProgressBarStop( pProgress );
-    // propagate arrival times from the registers
+//printf( "\n" );
+
+    // propagate LValues over the registers
     Vec_PtrForEachEntry( p->vLatchOrder, pObj, i )
-        fChange |= If_ObjPerformMappingLatch( p, pObj );
-//printf( "\n\n" );
+    {
+        If_ObjSetLValue( pObj, If_ObjLValue(If_ObjFanin0(pObj)) - p->Period );
+        If_ObjSetArrTime( pObj, If_ObjLValue(pObj) );
+    }
+
     // compute area and delay
     if ( fVeryVerbose )
     {
         p->RequiredGlo = If_ManDelayMax( p, 1 );
-        p->AreaGlo = p->pPars->fLiftLeaves? If_ManScanMappingSeq(p) : If_ManScanMapping(p);
-        printf( "S%d:  Fi = %6.2f. Del = %6.2f. Area = %8.2f. Cuts = %8d. Lim = %2d. Ave = %5.2f. ", 
-             nIter, (float)p->Period, p->RequiredGlo, p->AreaGlo, p->nCutsMerged, p->nCutsUsed, 1.0 * p->nCutsMerged / If_ManAndNum(p) );
+        p->AreaGlo = If_ManScanMapping(p);
+        printf( "S%d:  Fi = %6.2f. Del = %6.2f. Area = %8.2f. Cuts = %8d. ", 
+             nIter, (float)p->Period, p->RequiredGlo, p->AreaGlo, p->nCutsMerged );
         PRT( "T", clock() - clk );
     }
     return fChange;
@@ -273,56 +169,96 @@ int If_ManPerformMappingRoundSeq( If_Man_t * p, int Mode, int nIter, char * pLab
 
 /**Function*************************************************************
 
-  Synopsis    [Collects latches in the topological order.]
+  Synopsis    [Returns 1 if retiming with this clock period is feasible.]
 
   Description []
                
   SideEffects []
 
   SeeAlso     []
- 
+
 ***********************************************************************/
-void If_ManCollectLatches_rec( If_Obj_t * pObj, Vec_Ptr_t * vLatches )
+int If_ManBinarySearchPeriod( If_Man_t * p )
 {
-    if ( !If_ObjIsLatch(pObj) )
-        return;
-    if ( pObj->fMark )
-        return;
-    pObj->fMark = 1;
-    If_ManCollectLatches_rec( pObj->pFanin0, vLatches );
-    Vec_PtrPush( vLatches, pObj );
+    If_Obj_t * pObj;
+    int i, c, fConverged;
+    int fResetRefs = 0;
+
+    p->nAttempts++;
+
+    // set LValues of of PIs to be 0 and other nodes to be -infinity
+    // LValues of the PIs are already set to 0
+    // undo any previous mapping, except for CIs
+    If_ManForEachObj( p, pObj, i )
+    {
+        if ( If_ObjIsPi(pObj) || If_ObjIsConst1(pObj) )
+            If_ObjSetLValue( pObj, (float)0.0 );
+        else
+            If_ObjSetLValue( pObj, (float)-IF_INFINITY );
+        if ( If_ObjIsAnd(pObj) )
+            If_ObjCutBest(pObj)->nLeaves = 0;
+    }
+
+    // update all values iteratively
+    fConverged = 0;
+    for ( c = 1; c <= p->nMaxIters; c++ )
+    {
+        if ( !If_ManPerformMappingRoundSeq( p, c ) )
+        {
+            p->RequiredGlo = If_ManDelayMax( p, 1 );
+            fConverged = 1;
+            break;
+        }
+        p->RequiredGlo = If_ManDelayMax( p, 1 );
+//printf( "Global = %d \n", (int)p->RequiredGlo );
+        if ( p->RequiredGlo > p->Period + p->fEpsilon )
+            break; 
+    }
+
+    // report the results
+    if ( p->pPars->fVerbose )
+    {
+        p->AreaGlo = 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" );
+        else if ( c > p->nMaxIters )
+            printf( "Infeasible (timeout)" );
+        else
+            printf( "Infeasible" );
+        printf( "\n" );
+    }
+    return fConverged;
 }
 
+
 /**Function*************************************************************
 
-  Synopsis    [Collects latches in the topological order.]
+  Synopsis    [Performs binary search for the optimal clock period.]
 
-  Description []
+  Description [Assumes that FiMin is infeasible while FiMax is feasible.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * If_ManCollectLatches( If_Man_t * p )
+int If_ManBinarySearch_rec( If_Man_t * p, int FiMin, int FiMax )
 {
-    Vec_Ptr_t * vLatches;
-    If_Obj_t * pObj;
-    int i;
-    // collect latches 
-    vLatches = Vec_PtrAlloc( p->pPars->nLatches );
-    Vec_PtrForEachEntryStart( p->vCis, pObj, i, If_ManCiNum(p) - p->pPars->nLatches )
-        If_ManCollectLatches_rec( pObj, vLatches );
-    // clean marks
-    Vec_PtrForEachEntry( vLatches, pObj, i )
-        pObj->fMark = 0;
-    assert( Vec_PtrSize(vLatches) == p->pPars->nLatches );
-    return vLatches;
+    assert( FiMin < FiMax );
+    if ( FiMin + 1 == FiMax )
+        return FiMax;
+    // compute the median
+    p->Period = FiMin + (FiMax - FiMin)/2;
+    if ( If_ManBinarySearchPeriod( p ) )
+        return If_ManBinarySearch_rec( p, FiMin, p->Period ); // Median is feasible
+    else 
+        return If_ManBinarySearch_rec( p, p->Period, FiMax ); // Median is infeasible
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Prepares for sequential mapping by linking the latches.]
+  Synopsis    [Performs sequential mapping.]
 
   Description []
                
@@ -331,45 +267,53 @@ Vec_Ptr_t * If_ManCollectLatches( If_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int If_ManPrepareMappingSeq( If_Man_t * p )
+void If_ManPerformMappingSeqPost( If_Man_t * p )
 {
-    If_Obj_t * pObj, * pObjLi, * pObjLo, * pTemp;
-    If_Cut_t * pCut;
+    If_Obj_t * pObjLi, * pObjLo, * pObj;
     int i;
-    // link the latch outputs (PIs) directly to the drivers of latch inputs (POs)
+
+    // link the latch outputs (CIs) directly to the drivers of latch inputs (COs)
     for ( i = 0; i < p->pPars->nLatches; i++ )
     {
-        pObjLo = If_ManCi( p, If_ManCiNum(p) - p->pPars->nLatches + i );
-        pObjLi = If_ManCo( p, If_ManCoNum(p) - p->pPars->nLatches + i );
-        pObjLo->pFanin0 = If_ObjFanin0( pObjLi );
-        pObjLo->fCompl0 = If_ObjFaninC0( pObjLi );
-//        pObjLo->pFanin0 = pObjLi;
+        pObjLi = If_ManLi( p, i );
+        pObjLo = If_ManLo( p, i );
+//        printf( "%3d : %2d -> %2d   \n", i, 
+//            (int)If_ObjLValue(If_ObjFanin0(pObjLo)), (int)If_ObjLValue(pObjLo) );
     }
-    // collect latches
-    p->vLatchOrder = If_ManCollectLatches( p );
-    // propagate elementary cuts 
-    if ( p->pPars->fLiftLeaves )
+
+    // set arrival times
+    assert( p->pPars->pTimesArr != NULL );
+    If_ManForEachLatchOutput( p, pObjLo, i )
+        p->pPars->pTimesArr[i] = If_ObjLValue(pObjLo);
+
+    // set the required times
+    assert( p->pPars->pTimesReq == NULL );
+    p->pPars->pTimesReq = ALLOC( float, If_ManCoNum(p) );
+    If_ManForEachPo( p, pObj, i )
     {
-        Vec_PtrForEachEntry( p->vLatchOrder, pObj, i )
-        {
-            pCut = If_ObjCutTriv(pObj);
-            If_CutCopy( pCut, If_ObjFanin0(pObj)->Cuts );
-            If_CutLift( pCut );
-            pCut->Delay  -= p->Period;
-            pCut->fCompl ^= pObj->fCompl0;
-
-            // 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) );
-        }
+        p->pPars->pTimesReq[i] = p->RequiredGlo2;
+//        printf( "Out %3d : %2d   \n", i, (int)p->pPars->pTimesReq[i] );
     }
-    return 1;
+    If_ManForEachLatchInput( p, pObjLi, i )
+    {
+        p->pPars->pTimesReq[i] = If_ObjLValue(If_ObjFanin0(pObjLi));
+//        printf( "Out %3d : %2d   \n", i, (int)p->pPars->pTimesReq[i] );
+    }
+
+    // undo previous mapping
+    If_ManForEachObj( p, pObj, i )
+        if ( If_ObjIsAnd(pObj) )
+            If_ObjCutBest(pObj)->nLeaves = 0;
+
+    // map again combinationally
+    p->pPars->fSeqMap = 0;
+    If_ManPerformMappingComb( p );
+    p->pPars->fSeqMap = 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Performs mapping of the latches.]
+  Synopsis    [Performs sequential mapping.]
 
   Description []
                
@@ -378,34 +322,60 @@ int If_ManPrepareMappingSeq( If_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int If_ObjPerformMappingLatch( If_Man_t * p, If_Obj_t * pObj )
+int If_ManPerformMappingSeq( If_Man_t * p )
 {
-    If_Obj_t * pFanin;
-    If_Cut_t * pCut;
-    float LValueOld;
-    int i;
-    assert( If_ObjIsLatch(pObj) );
-    // save old l-value
-    LValueOld = If_ObjLValue(pObj);
-    pFanin = If_ObjFanin0(pObj);
-    assert( pFanin->nCuts > 0 );
-    if ( !p->pPars->fLiftLeaves )
+    int clkTotal = clock();
+    int PeriodBest;
+
+    p->SortMode = 0;
+
+    // perform combinational mapping to get the upper bound on the clock period
+    If_ManPerformMappingRound( p, 1, 0, 0, NULL );
+    p->RequiredGlo = If_ManDelayMax( p, 0 );
+    p->RequiredGlo2 = p->RequiredGlo;
+
+    // set direct linking of latches with their inputs
+    If_ManPrepareMappingSeq( p );
+
+    // collect latches
+    p->vLatchOrder = If_ManCollectLatches( p );
+
+    // set parameters
+    p->nCutsUsed = p->pPars->nCutsMax;
+    p->nAttempts = 0;
+    p->nMaxIters = 50;
+    p->Period    = (int)p->RequiredGlo;
+
+    // make sure the clock period works
+    if ( !If_ManBinarySearchPeriod( p ) )
     {
-        pObj->nCuts = 1;
-        If_ObjSetLValue( pObj, If_ObjLValue(pFanin) - p->Period );
+        printf( "If_ManPerformMappingSeq(): The upper bound on the clock period cannot be computed.\n" );
+        return 0;
     }
-    else
+
+    // perform binary search
+    PeriodBest = If_ManBinarySearch_rec( p, 0, p->Period );
+
+    // recompute the best l-values
+    if ( p->Period != PeriodBest )
     {
-        pObj->nCuts = pFanin->nCuts;
-        If_ObjForEachCut( pObj, pCut, i )
+        p->Period = PeriodBest;
+        if ( !If_ManBinarySearchPeriod( p ) )
         {
-            If_CutCopy( pCut, pFanin->Cuts + i );
-            If_CutLift( pCut );
-            pCut->Delay  -= p->Period;
-            pCut->fCompl ^= pObj->fCompl0;
+            printf( "If_ManPerformMappingSeq(): The final clock period cannot be confirmed.\n" );
+            return 0;
         }
     }
-    return LValueOld != If_ObjLValue(pObj);
+    if ( p->pPars->fVerbose )
+    {
+        printf( "The best clock period is %3d.  ", p->Period );
+        PRT( "Sequential time", clock() - clkTotal );
+    }
+    p->RequiredGlo = (float)PeriodBest;
+
+    // postprocess it using combinational mapping
+    If_ManPerformMappingSeqPost( p );
+    return 1;
 }
 
 ////////////////////////////////////////////////////////////////////////